diff --git a/src/backends/Ada/ada_backend_adb.ml b/src/backends/Ada/ada_backend_adb.ml
index a34caf96b13a106f93960dd9fc2b58b5b4c8510d..9ab15e30a91112700909754b9bc8500d13438d54 100644
--- a/src/backends/Ada/ada_backend_adb.ml
+++ b/src/backends/Ada/ada_backend_adb.ml
@@ -127,8 +127,7 @@ struct
let pp_step_definition env typed_submachines fmt (m, m_spec_opt, guarantees) =
let transform_local_to_state_assign instr = match instr.instr_desc with
| MLocalAssign (ident, value) ->
- { instr_desc = MStateAssign (ident, value);
- lustre_eq= instr.lustre_eq }
+ { instr with instr_desc = MStateAssign (ident, value) }
| _ -> instr
in
let pp_local_ghost_list, spec_instrs = match m_spec_opt with
@@ -150,7 +149,7 @@ struct
**)
let pp_reset_definition env typed_submachines fmt (m, m_spec_opt) =
let build_assign = function var ->
- mkinstr (MStateAssign (var, mk_default_value var.var_type))
+ mkinstr Spec_types.True (MStateAssign (var, mk_default_value var.var_type))
in
let env, memory = match m_spec_opt with
| None -> env, m.mmemory
diff --git a/src/backends/Ada/misc_lustre_function.ml b/src/backends/Ada/misc_lustre_function.ml
index 4e39f980615beb2527b86cc15242cbc84475d53b..35fb018cf4764d64ad006d808949a9776405ef91 100644
--- a/src/backends/Ada/misc_lustre_function.ml
+++ b/src/backends/Ada/misc_lustre_function.ml
@@ -267,7 +267,8 @@ let rec push_if_in_expr = function
in
let assign = if state then MStateAssign (ident, value) else MLocalAssign (ident, value) in
{ instr_desc = assign;
- lustre_eq = None
+ lustre_eq = None;
+ instr_spec = Spec_types.True
}
in
let mkval_var id = {
diff --git a/src/corelang.ml b/src/corelang.ml
index d2d9508787870e10c1f39f895680fe0bfe7e88bc..8f89123c8eecd7cd517f9c18ed818a7dcce2ee17 100644
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -257,12 +257,12 @@ let update_expr_annot node_id e annot =
e
-let mkinstr ?lustre_eq i =
- {
- instr_desc = i;
- (* lustre_expr = lustre_expr; *)
- lustre_eq = lustre_eq;
- }
+let mkinstr ?lustre_eq instr_spec instr_desc = {
+ instr_desc;
+ (* lustre_expr = lustre_expr; *)
+ instr_spec;
+ lustre_eq;
+}
let get_instr_desc i = i.instr_desc
let update_instr_desc i id = { i with instr_desc = id }
diff --git a/src/corelang.mli b/src/corelang.mli
index d42e19db93ed05d39dbf64c9f119e3b59dededf1..0f099f0d7b19a58603fdb16ece3e652d33b00d84 100644
--- a/src/corelang.mli
+++ b/src/corelang.mli
@@ -45,7 +45,7 @@ val mk_new_node_name: node_desc -> ident -> ident
val mktop: top_decl_desc -> top_decl
(* constructor for machine types *)
-val mkinstr: (* ?lustre_expr:expr -> *)?lustre_eq: eq -> Machine_code_types.instr_t_desc -> Machine_code_types.instr_t
+val mkinstr: (* ?lustre_expr:expr -> *)?lustre_eq: eq -> Machine_code_types.value_t Spec_types.formula_t -> Machine_code_types.instr_t_desc -> Machine_code_types.instr_t
val get_instr_desc: Machine_code_types.instr_t -> Machine_code_types.instr_t_desc
val update_instr_desc: Machine_code_types.instr_t -> Machine_code_types.instr_t_desc -> Machine_code_types.instr_t
diff --git a/src/dune b/src/dune
index f795776f6fbb7ba218e854370c77a0024570ef84..b189c65355328e17d3a0863b52cfa2f9d5908d1e 100644
--- a/src/dune
+++ b/src/dune
@@ -22,6 +22,7 @@
delay
machine_code_types
spec_types
+ spec_common
scheduling_type
log
printers
diff --git a/src/machine_code.ml b/src/machine_code.ml
index e5d7e203ddcc8b1638b165e6dc30246bfe24f2c6..16fe106f7f204a22e7e08c60f9c8467678625ba2 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -12,9 +12,12 @@
open Lustre_types
open Machine_code_types
open Machine_code_common
+open Spec_types
+open Spec_common
open Corelang
open Clocks
open Causality
+open Utils
exception NormalizationError
@@ -58,17 +61,21 @@ let build_env locals non_locals =
let translate_ident env id =
(* Format.eprintf "trnaslating ident: %s@." id; *)
- try (* id is a var that shall be visible here , ie. in vars *)
+ (* id is a var that shall be visible here , ie. in vars *)
+ try
let var_id = env.get_var id in
mk_val (Var var_id) var_id.var_type
with Not_found ->
- try (* id is a constant *)
+
+ (* id is a constant *)
+ try
let vdecl = (Corelang.var_decl_of_const
(const_of_top (Hashtbl.find Corelang.consts_table id)))
in
mk_val (Var vdecl) vdecl.var_type
with Not_found ->
- (* id is a tag, getting its type in the list of declared enums *)
+
+ (* id is a tag, getting its type in the list of declared enums *)
try
let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in
mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
@@ -76,14 +83,6 @@ let translate_ident env id =
Format.eprintf "internal error: Machine_code.translate_ident %s@.@?" id;
assert false
-let rec control_on_clock env ck inst =
- match (Clocks.repr ck).cdesc with
- | Con (ck1, cr, l) ->
- let id = Clocks.const_of_carrier cr in
- control_on_clock env ck1
- (mkinstr (MBranch (translate_ident env id, [l, [inst]])))
- | _ -> inst
-
(* specialize predefined (polymorphic) operators wrt their instances,
so that the C semantics is preserved *)
@@ -158,48 +157,92 @@ let rec translate_act env (y, expr) =
[translate_act (y, t)]
[translate_act (y, e)]
| Expr_merge (x, hl) ->
- mkinstr ~lustre_eq
- (MBranch (translate_ident x,
- List.map (fun (t, h) -> t, [translate_act (y, h)]) hl))
- | _ -> mkinstr ~lustre_eq (MLocalAssign (y, translate_expr expr))
-
-let reset_instance env i r c =
- match r with
- | Some r ->
- [control_on_clock env c
- (mk_conditional
- (translate_guard env r)
- [mkinstr (MReset i)]
- [mkinstr (MNoReset i)])]
- | None -> []
-
+ mk_branch ~lustre_eq
+ (translate_ident x)
+ (List.map (fun (t, h) -> t, [translate_act (y, h)]) hl)
+ | _ ->
+ mk_assign ~lustre_eq y (translate_expr expr)
(* Datastructure updated while visiting equations *)
type machine_ctx = {
- m: VSet.t; (* Memories *)
+ (* Memories *)
+ m: VSet.t;
+ (* Reset instructions *)
si: instr_t list;
- j: (Lustre_types.top_decl * Dimension.dim_expr list) Utils.IMap.t;
+ (* Instances *)
+ j: (Lustre_types.top_decl * Dimension.dim_expr list) IMap.t;
+ (* Step instructions *)
s: instr_t list;
+ (* Memory pack spec *)
+ mp: mc_formula_t list;
+ (* Clocked spec *)
+ c: mc_formula_t IMap.t;
+ (* Transition spec *)
+ t: mc_formula_t list;
}
-let ctx_init = { m = VSet.empty; (* memories *)
- si = []; (* init instr *)
- j = Utils.IMap.empty;
- s = [] }
+let ctx_init = {
+ m = VSet.empty;
+ si = [];
+ j = IMap.empty;
+ s = [];
+ mp = [];
+ c = IMap.empty;
+ t = []
+}
(****************************************************************)
(* Main function to translate equations into this machine context we
are building *)
(****************************************************************)
+let mk_control id vs v l inst =
+ mkinstr
+ (Imply (mk_clocked_on id vs, inst.instr_spec))
+ (MBranch (v, [l, [inst]]))
+
+let control_on_clock env ctx ck inst =
+ let rec aux (ck_ids, vs, ctx, inst as acc) ck =
+ match (Clocks.repr ck).cdesc with
+ | Con (ck, cr, l) ->
+ let id = Clocks.const_of_carrier cr in
+ let v = translate_ident env id in
+ let ck_ids' = String.concat "_" ck_ids in
+ let id' = id ^ "_" ^ ck_ids' in
+ let ck_spec = mk_condition v l in
+ aux (id :: ck_ids,
+ v :: vs,
+ { ctx
+ with c = IMap.add id ck_spec
+ (IMap.add id'
+ (And [ck_spec; mk_clocked_on ck_ids' vs]) ctx.c)
+ },
+ mk_control id' (v :: vs) v l inst) ck
+ | _ -> acc
+ in
+ let _, _, ctx, inst = aux ([], [], ctx, inst) ck in
+ ctx, inst
+
+let reset_instance env i r c =
+ match r with
+ | Some r ->
+ [snd (control_on_clock env ctx_init c
+ (mk_conditional
+ (translate_guard env r)
+ [mkinstr True (MReset i)]
+ [mkinstr True (MNoReset i)]))]
+ | None -> []
let translate_eq env ctx eq =
let translate_expr = translate_expr env in
let translate_act = translate_act env in
- let control_on_clock = control_on_clock env in
+ let control_on_clock ck inst =
+ let ctx, ins = control_on_clock env ctx ck inst in
+ { ctx with s = ins :: ctx.s }
+ in
let reset_instance = reset_instance env in
- let mkinstr' = mkinstr ~lustre_eq:eq in
+ let mkinstr' = mkinstr ~lustre_eq:eq True in
let ctl ?(ck=eq.eq_rhs.expr_clock) instr =
control_on_clock ck (mkinstr' instr) in
@@ -211,23 +254,23 @@ let translate_eq env ctx eq =
let o = new_instance (Arrow.arrow_top_decl ()) eq.eq_rhs.expr_tag in
let c1 = translate_expr e1 in
let c2 = translate_expr e2 in
+ let ctx = ctl (MStep ([var_x], o, [c1;c2])) in
{ ctx with
- si = mkinstr (MReset o) :: ctx.si;
- j = Utils.IMap.add o (Arrow.arrow_top_decl (), []) ctx.j;
- s = ctl (MStep ([var_x], o, [c1;c2])) :: ctx.s
+ si = mkinstr True (MReset o) :: ctx.si;
+ j = IMap.add o (Arrow.arrow_top_decl (), []) ctx.j;
}
| [x], Expr_pre e1 when env.is_local x ->
let var_x = env.get_var x in
+ let ctx = ctl (MStateAssign (var_x, translate_expr e1)) in
{ ctx with
m = VSet.add var_x ctx.m;
- s = ctl (MStateAssign (var_x, translate_expr e1)) :: ctx.s
}
| [x], Expr_fby (e1, e2) when env.is_local x ->
let var_x = env.get_var x in
+ let ctx = ctl (MStateAssign (var_x, translate_expr e2)) in
{ ctx with
m = VSet.add var_x ctx.m;
si = mkinstr' (MStateAssign (var_x, translate_expr e1)) :: ctx.si;
- s = ctl (MStateAssign (var_x, translate_expr e2)) :: ctx.s
}
| p, Expr_appl (f, arg, r)
when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
@@ -241,25 +284,22 @@ let translate_eq env ctx eq =
el [eq.eq_rhs.expr_clock] in
let call_ck = Clock_calculus.compute_root_clock
(Clock_predef.ck_tuple env_cks) in
+ let ctx = ctl ~ck:call_ck (MStep (var_p, o, vl)) in
(*Clocks.new_var true in
Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;
Format.eprintf "call %a: %a: %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple env_cks) Clocks.print_ck call_ck;*)
{ ctx with
si = if Stateless.check_node node_f
- then ctx.si else mkinstr (MReset o) :: ctx.si;
- j = Utils.IMap.add o call_f ctx.j;
+ then ctx.si else mkinstr True (MReset o) :: ctx.si;
+ j = IMap.add o call_f ctx.j;
s = (if Stateless.check_node node_f
- then [] else reset_instance o r call_ck)
- @ ctl ~ck:call_ck (MStep (var_p, o, vl))
- :: ctx.s
+ then []
+ else reset_instance o r call_ck)
+ @ ctx.s
}
| [x], _ ->
let var_x = env.get_var x in
- { ctx with
- s = control_on_clock eq.eq_rhs.expr_clock
- (translate_act (var_x, eq.eq_rhs))
- :: ctx.s
- }
+ control_on_clock eq.eq_rhs.expr_clock (translate_act (var_x, eq.eq_rhs))
| _ ->
Format.eprintf "internal error: Machine_code.translate_eq %a@?"
Printers.pp_node_eq eq;
@@ -270,7 +310,7 @@ let constant_equations locals =
if vdecl.var_dec_const
then
{ eq_lhs = [vdecl.var_id];
- eq_rhs = Utils.desome vdecl.var_dec_value;
+ eq_rhs = desome vdecl.var_dec_value;
eq_loc = vdecl.var_loc
} :: eqs
else eqs)
@@ -326,7 +366,7 @@ let translate_core sorted_eqs locals other_vars =
let ctx0 = translate_eqs env ctx_init constant_eqs in
assert (VSet.is_empty ctx0.m);
assert (ctx0.si = []);
- assert (Utils.IMap.is_empty ctx0.j);
+ assert (IMap.is_empty ctx0.j);
(* Compute ctx for all eqs *)
let ctx = translate_eqs env ctx_init sorted_eqs in
@@ -371,7 +411,7 @@ let translate_decl nd sch =
let l = VSet.elements (VSet.diff locals ctx.m) in
List.fold_left (fun res v -> if List.mem v.var_id unused then res else v::res) [] l
in
- let mmap = Utils.IMap.bindings ctx.j in
+ let mmap = IMap.bindings ctx.j in
{
mname = nd;
mmemory = VSet.elements ctx.m;
@@ -417,7 +457,7 @@ let translate_prog decls node_schs =
List.map
(fun decl ->
let node = node_of_top decl in
- let sch = Utils.IMap.find node.node_id node_schs in
+ let sch = IMap.find node.node_id node_schs in
translate_decl node sch
) nodes
in
diff --git a/src/machine_code_common.ml b/src/machine_code_common.ml
index 6d5a4bf5bb029b4c184f4ee444f595a8ba444bea..b47810afb5d3cda6fc35adacf6d2f7de19fed8e2 100644
--- a/src/machine_code_common.ml
+++ b/src/machine_code_common.ml
@@ -1,5 +1,7 @@
open Lustre_types
open Machine_code_types
+open Spec_types
+open Spec_common
open Corelang
let print_statelocaltag = true
@@ -153,11 +155,28 @@ let is_stateless m = m.minstances = [] && m.mmemory = []
let is_output m id =
List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs
+let get_instr_spec i = i.instr_spec
let mk_conditional ?lustre_eq c t e =
- mkinstr ?lustre_eq:lustre_eq (MBranch(c, [ (tag_true, t); (tag_false, e) ]))
-
-
+ mkinstr ?lustre_eq
+ (Ternary (Val c,
+ And (List.map get_instr_spec t),
+ And (List.map get_instr_spec e)))
+ (MBranch(c, [
+ (tag_true, t);
+ (tag_false, e) ]))
+
+let mk_branch ?lustre_eq c br =
+ mkinstr ?lustre_eq
+ (And (List.map (fun (l, instrs) ->
+ Imply (Equal (Val c, Tag l), And (List.map get_instr_spec instrs)))
+ br))
+ (MBranch (c, br))
+
+let mk_assign ?lustre_eq x v =
+ mkinstr ?lustre_eq
+ (Equal (Var x, Val v))
+ (MLocalAssign (x, v))
let mk_val v t =
{ value_desc = v;
@@ -178,7 +197,7 @@ let arrow_machine =
mmemory = [var_state];
mcalls = [];
minstances = [];
- minit = [mkinstr (MStateAssign(var_state, cst true))];
+ minit = [mkinstr True (MStateAssign(var_state, cst true))];
mstatic = [];
mconst = [];
mstep = {
@@ -187,10 +206,10 @@ let arrow_machine =
step_locals = [];
step_checks = [];
step_instrs = [mk_conditional (mk_val (Var var_state) Type_predef.type_bool)
- (List.map mkinstr
+ (List.map (mkinstr True)
[MStateAssign(var_state, cst false);
MLocalAssign(var_output, mk_val (Var var_input1) t_arg)])
- (List.map mkinstr
+ (List.map (mkinstr True)
[MLocalAssign(var_output, mk_val (Var var_input2) t_arg)]) ];
step_asserts = [];
};
@@ -354,7 +373,7 @@ and join_guards inst1 insts2 =
| _ , [] ->
[inst1]
| MBranch (x1, hl1), MBranch (x2, hl2) :: _ when x1 = x2 ->
- mkinstr
+ mkinstr True
(* TODO on pourrait uniquement concatener les lustres de inst1 et hd(inst2) *)
(MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2)))
:: (List.tl insts2)
diff --git a/src/machine_code_common.mli b/src/machine_code_common.mli
index 3033bfe7f8d0ffa55472f422c0ecdf8f796c970a..341d81c4437f5bc98cdf63d935b6b8943f8dc5bb 100644
--- a/src/machine_code_common.mli
+++ b/src/machine_code_common.mli
@@ -8,6 +8,8 @@ val get_stateless_status_top_decl: Lustre_types.top_decl -> bool * bool
val is_stateless: Machine_code_types.machine_t -> bool
val mk_val: Machine_code_types.value_t_desc -> Types.type_expr -> Machine_code_types.value_t
val mk_conditional: ?lustre_eq:Lustre_types.eq -> Machine_code_types.value_t -> Machine_code_types.instr_t list -> Machine_code_types.instr_t list -> Machine_code_types.instr_t
+val mk_branch: ?lustre_eq:Lustre_types.eq -> Machine_code_types.value_t -> (Lustre_types.label * Machine_code_types.instr_t list) list -> Machine_code_types.instr_t
+val mk_assign: ?lustre_eq:Lustre_types.eq -> Lustre_types.var_decl -> Machine_code_types.value_t -> Machine_code_types.instr_t
val empty_machine: Machine_code_types.machine_t
val arrow_machine: Machine_code_types.machine_t
val new_instance: Lustre_types.top_decl -> Lustre_types.tag -> Lustre_types.ident
diff --git a/src/machine_code_types.ml b/src/machine_code_types.ml
index 6c57fd593dac38f61061560b0214e6c7084e0871..283c6ea1822b288e90ceaa2fc355343300c187ca 100644
--- a/src/machine_code_types.ml
+++ b/src/machine_code_types.ml
@@ -1,7 +1,7 @@
(************ Machine code types *************)
open Lustre_types
open Spec_types
-
+
type value_t =
{
value_desc: value_t_desc;
@@ -16,11 +16,14 @@ and value_t_desc =
| Access of value_t * value_t
| Power of value_t * value_t
+type mc_formula_t = value_t formula_t
+
type instr_t =
{
instr_desc: instr_t_desc; (* main data: the content *)
(* lustre_expr: expr option; (* possible representation as a lustre expression *) *)
lustre_eq: eq option; (* possible representation as a lustre flow equation *)
+ instr_spec: mc_formula_t
}
and instr_t_desc =
| MLocalAssign of var_decl * value_t
@@ -45,7 +48,7 @@ type static_call = top_decl * (Dimension.dim_expr list)
type machine_spec = {
mnode_spec: node_spec_t option;
- mtransitions: transition_t list
+ mtransitions: value_t transition_t list
}
type machine_t = {
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index 4dfe5ec0432be1149293c82d2a4606a301915440..ab06ccdfc478fd7ee453806fdd2b186e08a17d15 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -283,7 +283,8 @@ let instr_of_const top_const =
let vdecl = { vdecl with var_type = const.const_type } in
let lustre_eq = mkeq loc ([const.const_id], mkexpr loc (Expr_const const.const_value)) in
mkinstr
- ~lustre_eq:lustre_eq
+ ~lustre_eq
+ True
(MLocalAssign (vdecl, mk_val (Cst const.const_value) vdecl.var_type))
(* We do not perform this optimization on contract nodes since there
diff --git a/src/plugins/scopes/scopes.ml b/src/plugins/scopes/scopes.ml
index e6e961d3783dc795ea69a6b12b9f3f2ddd8b55d4..0772b160477b552a07d6dfa4f358afae679c8b9a 100644
--- a/src/plugins/scopes/scopes.ml
+++ b/src/plugins/scopes/scopes.ml
@@ -220,7 +220,7 @@ let pp_scopes fmt scopes =
let update_machine main_node machine scopes =
let stateassign (vdecl_mem, vdecl_orig) =
- mkinstr
+ mkinstr True
(MStateAssign (vdecl_mem, mk_val (Var vdecl_orig) vdecl_orig.var_type))
in
let selection =
@@ -248,7 +248,7 @@ let update_machine main_node machine scopes =
mstep = {
machine.mstep with
step_instrs = machine.mstep.step_instrs
- @ (mkinstr (MComment "Registering all flows"))::(List.map stateassign new_mems)
+ @ (mkinstr True (MComment "Registering all flows"))::(List.map stateassign new_mems)
}
}
diff --git a/src/spec_types.ml b/src/spec_types.ml
index b777a7e85ded7a13e93f938ed57cca6ffac4a2c0..d9136f7bb809f893c38d09ad8573d1a6a7df98ab 100644
--- a/src/spec_types.ml
+++ b/src/spec_types.ml
@@ -4,23 +4,42 @@ type state_t =
| In
| Out
-type expression_t =
- | Cst of constant
+type 'a expression_t =
+ | Val of 'a
+ | Tag of ident
| Var of var_decl
| Instance of state_t * ident
| Memory of state_t * ident
type predicate_t =
- | Atom of expression_t
- | Equal of predicate_t * predicate_t
- | Imply of predicate_t * predicate_t
- | Exists of var_decl list * predicate_t list
- | Forall of var_decl list * predicate_t list
+ (* | Memory_pack *)
+ | Clocked_on of ident
+ | Transition
+ | Initialization
-type transition_t = {
+type 'a formula_t =
+ | True
+ | False
+ | Equal of 'a expression_t * 'a expression_t
+ | And of 'a formula_t list
+ | Or of 'a formula_t list
+ | Imply of 'a formula_t * 'a formula_t
+ | Exists of var_decl list * 'a formula_t
+ | Forall of var_decl list * 'a formula_t
+ | Ternary of 'a expression_t * 'a formula_t * 'a formula_t
+ | Predicate of predicate_t * 'a expression_t list
+
+(* type 'a simulation_t = {
+ * sname: node_desc;
+ * sindex: option int;
+ * sformula: 'a formula_t;
+ * } *)
+
+type 'a transition_t = {
tname: node_desc;
- tindex: int;
+ tindex: int option;
tlocals: var_decl list;
toutputs: var_decl list;
- tpredicate: predicate_t list;
+ tformula: 'a formula_t;
}
+
diff --git a/src/utils/utils.ml b/src/utils/utils.ml
index 79ed9d701cfa794fd49162512aa60b08db5939e8..a298bd36a7ad6924e14346ddaf443c331d949859 100644
--- a/src/utils/utils.ml
+++ b/src/utils/utils.ml
@@ -32,7 +32,15 @@ struct (* Node module *)
let equal n1 n2 = n1 = n2
end
-module IMap = Map.Make(IdentModule)
+module IMap = struct
+ include Map.Make(IdentModule)
+ let union_l m1 m2 =
+ merge (fun _ o1 o2 -> match o1, o2 with
+ | None, None -> None
+ | Some _, _ -> o1
+ | _, Some _ -> o2) m1 m2
+end
+
module ISet = Set.Make(IdentModule)
module IdentDepGraph = Imperative.Digraph.ConcreteBidirectional (IdentModule)
module TopologicalDepGraph = Topological.Make(IdentDepGraph)