Commit 9686ab43 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Take into account the change in the rdbg-plugin interface (V1.55)

parent bf5cb12d
(* Time-stamp: <modified the 05/02/2016 (at 14:59) by Erwan Jahier> *)
(* Time-stamp: <modified the 10/02/2016 (at 14:47) by Erwan Jahier> *)
open RdbgPlugin
type vars = (string * Data.t) list
......@@ -97,21 +97,21 @@ let (make_ec : string -> RdbgPlugin.t) =
in
let step = step_channel ec_ic ec_oc ec_in ec_out in
let step_dbg sl ctx cont =
let enb = ctx.Event.ctx_nb in
let enb = ctx.Event.nb in
let ctx = Event.incr_event_nb ctx in
{
Event.nb = enb;
Event.step = ctx.Event.ctx_step;
Event.depth = ctx.Event.ctx_depth;
Event.step = ctx.Event.step;
Event.depth = ctx.Event.depth;
Event.kind = Event.Exit;
Event.lang = "lustre";
Event.name=ec_file;
Event.inputs = [] ;
Event.outputs = [];
Event.sinfo = None;
Event.data = ctx.Event.ctx_data;
Event.data = ctx.Event.data;
Event.next = (fun () -> cont (step sl) ctx);
Event.terminate = ctx.Event.ctx_terminate;
Event.terminate = ctx.Event.terminate;
}
in
{
......@@ -217,12 +217,12 @@ let (make_socket_do : string -> int -> in_channel * RdbgPlugin.t) =
in
let step = step_channel sock_in sock_out vars_in vars_out in
let step_dbg sl ctx cont =
let enb = ctx.Event.ctx_nb in
let enb = ctx.Event.nb in
let ctx = Event.incr_event_nb ctx in
{
Event.step = ctx.Event.ctx_step;
Event.data = ctx.Event.ctx_data;
Event.depth = ctx.Event.ctx_depth;
Event.step = ctx.Event.step;
Event.data = ctx.Event.data;
Event.depth = ctx.Event.depth;
Event.nb = enb;
Event.kind = Event.Exit;
Event.lang = "socket";
......@@ -231,7 +231,7 @@ let (make_socket_do : string -> int -> in_channel * RdbgPlugin.t) =
Event.outputs = [];
Event.sinfo = None;
Event.next = (fun () -> cont (step sl) ctx);
Event.terminate = ctx.Event.ctx_terminate;
Event.terminate = ctx.Event.terminate;
}
in
let plugin = {
......@@ -322,13 +322,13 @@ let (make_ec_exe : string -> RdbgPlugin.t) =
in
let step = step_channel ec_ic ec_oc ec_in ec_out in
let step_dbg sl ctx cont =
let enb = ctx.Event.ctx_nb in
let enb = ctx.Event.nb in
let ctx = Event.incr_event_nb ctx in
{
Event.step = ctx.Event.ctx_step;
Event.data = ctx.Event.ctx_data;
Event.step = ctx.Event.step;
Event.data = ctx.Event.data;
Event.nb = enb;
Event.depth = ctx.Event.ctx_depth;
Event.depth = ctx.Event.depth;
Event.kind = Event.Exit;
Event.lang = "ec";
Event.name = ec_file;
......@@ -336,7 +336,7 @@ let (make_ec_exe : string -> RdbgPlugin.t) =
Event.outputs = [];
Event.sinfo = None;
Event.next = (fun () -> cont (step sl) ctx);
Event.terminate = ctx.Event.ctx_terminate;
Event.terminate = ctx.Event.terminate;
}
in
{
......
......@@ -69,11 +69,13 @@ let (check_compat : vars -> vars -> vars -> vars -> vars -> vars ->
)
)
type ctx = Event.t
type e = Event.t
open RdbgPlugin
let (make_rp_list : reactive_program list ->
vars list * vars list * (string -> unit) list *
(Data.subst list -> Data.subst list) list *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) ->
(Data.subst list -> ctx -> (Data.subst list -> ctx -> Event.t) ->
Event.t) list * Data.subst list list * Data.subst list list) =
fun rpl ->
let add_init init (a,b,c,d,e) = (a,b,c,d,e,init,init) in
......@@ -122,8 +124,8 @@ exception SutStop of cov_opt
(* Transform a map on a function list into CPS *)
let (step_dbg_sl :
(Data.subst list -> Event.ctx ->
(Data.subst list -> Event.ctx -> Event.t) -> Event.t) list ->
(Data.subst list -> ctx ->
(Data.subst list -> ctx -> Event.t) -> Event.t) list ->
's list -> 'ctx -> ('s list -> 'e) -> 'e) =
fun step_dbg_sl_l sl ctx cont ->
(* ouch! Celle-la est chevelue...
......@@ -308,10 +310,10 @@ let (start : unit -> Event.t) =
let edata = env_in_vals@pre_env_out_vals in
let ctx =
{ ctx with
Event.ctx_step = i;
Event.ctx_name = "ltop";
Event.ctx_depth = 1;
Event.ctx_data = edata;
Event.step = i;
Event.name = "ltop";
Event.depth = 1;
Event.data = edata;
}
in
let cont = loop2 cov env_in_vals pre_env_out_vals ctx i luciole_outs in
......@@ -339,10 +341,10 @@ let (start : unit -> Event.t) =
if args.ldbg then
let edata = sut_in_vals@ env_out_vals in
let ctx = { ctx with
Event.ctx_step = i;
Event.ctx_name = "ltop";
Event.ctx_depth = 1;
Event.ctx_data = edata;
Event.step = i;
Event.name = "ltop";
Event.depth = 1;
Event.data = edata;
}
in
let cont =
......@@ -435,14 +437,14 @@ let (start : unit -> Event.t) =
gnuplot_pid_ref := None);
killem_all cov
in
let enb = ctx.Event.ctx_nb in
let enb = ctx.Event.nb in
let ctx = { ctx with
Event.ctx_nb = ctx.Event.ctx_nb+1;
Event.ctx_step = i;
Event.ctx_name = "ltop";
Event.ctx_depth = 1;
Event.ctx_data = edata;
Event.ctx_terminate = term;
Event.nb = ctx.Event.nb+1;
Event.step = i;
Event.name = "ltop";
Event.depth = 1;
Event.data = edata;
Event.terminate = term;
}
in
{
......@@ -490,14 +492,18 @@ let (start : unit -> Event.t) =
in
let ctx =
{
Event.ctx_nb = 1;
Event.ctx_step = 1;
Event.ctx_name = "ltop";
Event.ctx_depth = 1;
Event.ctx_inputs = [];
Event.ctx_outputs = [];
Event.ctx_data = [];
Event.ctx_terminate = (fun () -> killem_all cov_init)
Event.nb = 1;
Event.step = 1;
Event.name = "ltop";
Event.depth = 1;
Event.inputs = [];
Event.outputs = [];
Event.data = [];
Event.terminate = (fun () -> killem_all cov_init);
Event.lang = "";
Event.next = (fun () -> assert false);
Event.kind = Event.Ltop;
Event.sinfo = None;
}
in
let (first_event : Event.t) =
......
......@@ -693,13 +693,16 @@ let string_of_cont_mnemo = function
| Crun (s) -> Printf.sprintf "!%s" s
type e = Event.t
type ctx = Event.t
type continuation = {
doit: behavior -> behavior;
dbg: cont_mnemo list
}
type continuation_ldbg = {
doit_ldbg:Event.ctx -> behavior -> (Event.ctx -> behavior -> Event.t)
-> (Event.ctx -> Event.t) -> (Event.ctx -> string -> Event.t) -> Event.t;
doit_ldbg:ctx -> behavior -> (ctx -> behavior -> e)
-> (ctx -> e) -> (ctx -> string -> e) -> e;
dbg_ldbg: cont_mnemo list
}
......@@ -709,11 +712,11 @@ let (mk_cont : (behavior -> behavior) -> cont_mnemo -> continuation -> continuat
dbg = d::(cin.dbg);
}
let (mk_cont_ldbg : Event.ctx ->
(Event.ctx -> behavior -> (Event.ctx -> behavior -> Event.t) ->
(Event.ctx -> Event.t) -> (Event.ctx -> string -> Event.t) -> Event.t) ->
let (mk_cont_ldbg : ctx ->
(ctx -> behavior -> (ctx -> behavior -> e) ->
(ctx -> e) -> (ctx -> string -> e) -> e) ->
cont_mnemo -> continuation_ldbg ->
(Event.ctx -> continuation_ldbg -> Event.t) -> Event.t) =
(ctx -> continuation_ldbg -> e) -> e) =
fun ctx f d cin cont ->
cont ctx {
doit_ldbg = f;
......@@ -761,7 +764,7 @@ let put_in_para te1 te2 = (
| (x,y) -> TE_para [x; y]
)
let (event_incr : Event.ctx -> MainArg.t -> Event.ctx) =
let (event_incr : ctx -> MainArg.t -> ctx) =
fun ctx opt ->
MainArg.event_incr opt;
Event.incr_event_nb ctx
......@@ -1431,11 +1434,11 @@ and to_reactive_prg (it:t) (curstate:internal_state) (invals: Value.t list) = (
let rec (genpath_ldbg :
t -> store -> CoTraceExp.t ->
Event.ctx ->
(Event.ctx -> behavior -> Event.t) ->
(Event.ctx -> Event.t) ->
(Event.ctx -> string -> Event.t) ->
Event.t) =
ctx ->
(ctx -> behavior -> e) ->
(ctx -> e) ->
(ctx -> string -> e) ->
e) =
fun it data x ctx cont fail_cont excn_cont-> (* data env = inputs + pres *) (
(*-------------------------------------------*)
(* Correspondance id de trace -> trace exp
......@@ -1448,11 +1451,11 @@ let rec (genpath_ldbg :
(*-------------------------------------------*
* Fonction récursive :
* --------------------------------------------*)
let rec (rec_genpath_ldbg : Event.ctx ->
branch_ldbg -> (Event.ctx -> behavior -> Event.t) ->
(Event.ctx -> Event.t) ->
(Event.ctx -> string -> Event.t) ->
Event.t
let rec (rec_genpath_ldbg : ctx ->
branch_ldbg -> (ctx -> behavior -> e) ->
(ctx -> e) ->
(ctx -> string -> e) ->
e
) =
fun ctx br cont fail_cont excn_cont-> (
let data = br.br_data_ldbg in
......@@ -1512,7 +1515,7 @@ let rec (genpath_ldbg :
let try_cont ctx () =
let is_sat = check_satisfiablity it new_acc in
if (is_sat) then
let enb = ctx.Event.ctx_nb in
let enb = ctx.Event.nb in
let ctx = event_incr ctx it.arg_opt in
{
Event.kind = Event.MicroStep "sat ";
......@@ -1526,13 +1529,13 @@ let rec (genpath_ldbg :
Event.more = None;
Event.atoms = si_atoms;
});
Event.depth = ctx.Event.ctx_depth;
Event.step = ctx.Event.ctx_step;
Event.name = ctx.Event.ctx_name;
Event.inputs = ctx.Event.ctx_inputs;
Event.outputs = ctx.Event.ctx_outputs;
Event.data = ctx.Event.ctx_data;
Event.terminate = ctx.Event.ctx_terminate;
Event.depth = ctx.Event.depth;
Event.step = ctx.Event.step;
Event.name = ctx.Event.name;
Event.inputs = ctx.Event.inputs;
Event.outputs = ctx.Event.outputs;
Event.data = ctx.Event.data;
Event.terminate = ctx.Event.terminate;
}
else (* the constraint is unsat *)
let lazy_ci = fun () ->
......@@ -1547,7 +1550,7 @@ let rec (genpath_ldbg :
let expr_cc = Exp.to_expr cc.g_form in
ExprUtil.get_info bdd bdd_acc (expr_cc, bdd_cc)
in
let enb = ctx.Event.ctx_nb in
let enb = ctx.Event.nb in
let ctx = event_incr ctx it.arg_opt in
let usat_event =
{
......@@ -1560,18 +1563,18 @@ let rec (genpath_ldbg :
Event.more = Some lazy_ci;
Event.atoms = si_atoms;
});
Event.depth = ctx.Event.ctx_depth;
Event.step = ctx.Event.ctx_step;
Event.name = ctx.Event.ctx_name;
Event.inputs = ctx.Event.ctx_inputs;
Event.outputs = ctx.Event.ctx_outputs;
Event.data = ctx.Event.ctx_data;
Event.terminate = ctx.Event.ctx_terminate;
Event.depth = ctx.Event.depth;
Event.step = ctx.Event.step;
Event.name = ctx.Event.name;
Event.inputs = ctx.Event.inputs;
Event.outputs = ctx.Event.outputs;
Event.data = ctx.Event.data;
Event.terminate = ctx.Event.terminate;
}
in
usat_event
in
let enb = ctx.Event.ctx_nb in
let enb = ctx.Event.nb in
let ctx = event_incr ctx it.arg_opt in
{
Event.nb = enb;
......@@ -1582,19 +1585,19 @@ let rec (genpath_ldbg :
Event.more = None;
Event.atoms = si_atoms;
});
Event.depth = ctx.Event.ctx_depth;
Event.step = ctx.Event.ctx_step;
Event.name = ctx.Event.ctx_name;
Event.inputs = ctx.Event.ctx_inputs;
Event.outputs = ctx.Event.ctx_outputs;
Event.data = ctx.Event.ctx_data;
Event.terminate = ctx.Event.ctx_terminate;
Event.depth = ctx.Event.depth;
Event.step = ctx.Event.step;
Event.name = ctx.Event.name;
Event.inputs = ctx.Event.inputs;
Event.outputs = ctx.Event.outputs;
Event.data = ctx.Event.data;
Event.terminate = ctx.Event.terminate;
Event.next = try_cont ctx;
}
)
(** Sequence *)
| TE_fby (te1, te2) -> (
let (cont2 : Event.ctx -> continuation_ldbg -> Event.t) =
let (cont2 : ctx -> continuation_ldbg -> e) =
fun ctx fby_cont ->
rec_genpath_ldbg ctx ({br with br_ctrl_ldbg=te1;
br_cont_ldbg=fby_cont}) cont fail_cont excn_cont
......@@ -1977,8 +1980,8 @@ let rec (genpath_ldbg :
(* build a slave LutExe *)
let zeexe = of_expanded_code it.arg_opt zecode in
let inits = get_init_internal_state zeexe in
let (cont2: Event.ctx -> Reactive.prg_ldbg -> (Event.ctx -> Event.t)
-> (Event.ctx -> string -> Event.t) -> Event.t) =
let (cont2: ctx -> Reactive.prg_ldbg -> (ctx -> e)
-> (ctx -> string -> e) -> e) =
fun ctx zereact fail_cont excn_cont->
let outids = List.map (fun (id,_) -> id) vars in
(* build the initial TE_dyn_erun *)
......@@ -2012,7 +2015,7 @@ let rec (genpath_ldbg :
in
let ins = List.map eval_arg args in
(* call the reactive prog *)
let (cont3 : Event.ctx -> Reactive.prg_ldbg -> Value.t list -> Event.t) =
let (cont3 : ctx -> Reactive.prg_ldbg -> Value.t list -> e) =
fun ctx react' outs ->
(* stores the values in the LocalIns vars *)
Verbose.exe ~flag:dbgrun
......@@ -2054,23 +2057,23 @@ let rec (genpath_ldbg :
cont2
in
(* exiting a run *)
let enb,d = ctx.Event.ctx_nb, ctx.Event.ctx_depth in
let enb,d = ctx.Event.nb, ctx.Event.depth in
let ctx = event_incr ctx it.arg_opt in
let event =
{
Event.step = ctx.Event.ctx_step;
Event.step = ctx.Event.step;
Event.nb = enb;
Event.depth = ctx.Event.ctx_depth;
Event.depth = ctx.Event.depth;
Event.kind = Event.MicroStep "quit";
Event.lang = "lutin";
Event.name = rid;
Event.inputs = ctx.Event.ctx_inputs;
Event.outputs = ctx.Event.ctx_outputs;
Event.data = ctx.Event.ctx_data;
Event.inputs = ctx.Event.inputs;
Event.outputs = ctx.Event.outputs;
Event.data = ctx.Event.data;
Event.sinfo = None;
Event.next =
(fun () -> Reactive.step_ldbg ctx react ins cont3 fail_cont excn_cont);
Event.terminate = ctx.Event.ctx_terminate;
Event.terminate = ctx.Event.terminate;
}
in
event
......@@ -2114,7 +2117,7 @@ let rec (genpath_ldbg :
(* build a slave LutExe *)
let zeexe = of_expanded_code it.arg_opt zecode in
let inits = get_init_internal_state zeexe in
let (cont2: Event.ctx -> Reactive.prg_ldbg -> Event.t) =
let (cont2: ctx -> Reactive.prg_ldbg -> e) =
fun ctx zereact ->
let e' = TE_dyn_run_ldbg (rid, zereact, andexp, vars, args, e, si) in
rec_genpath_ldbg ctx ({br with br_ctrl_ldbg=e';
......@@ -2143,7 +2146,7 @@ let rec (genpath_ldbg :
let excn_cont ctx x =
br_cont.doit_ldbg ctx (Raise x) cont fail_cont excn_cont
in
let (cont3 : Event.ctx -> Reactive.prg_ldbg -> Value.t list -> Event.t) =
let (cont3 : ctx -> Reactive.prg_ldbg -> Value.t list -> e) =
fun ctx react' outs ->
(* outs : Value.t list *)
(* stores the values in the LocalIns vars *)
......@@ -2252,12 +2255,12 @@ rec_genpath_ldbg ctx init_branch
a suitable Reactive.prg
*)
and (to_reactive_prg_ldbg :
string -> t -> internal_state -> Event.ctx -> Value.t list ->
(Event.ctx -> Reactive.prg_ldbg -> Value.t list -> Event.t) ->
(Event.ctx -> Event.t) -> (Event.ctx -> string -> Event.t) -> Event.t) =
string -> t -> internal_state -> ctx -> Value.t list ->
(ctx -> Reactive.prg_ldbg -> Value.t list -> e) ->
(ctx -> e) -> (ctx -> string -> e) -> e) =
fun rid it curstate ctx invals cont fail_cont excn_cont->
let rid_ctx = ctx.Event.ctx_name in
let d_ctx = ctx.Event.ctx_depth in
let rid_ctx = ctx.Event.name in
let d_ctx = ctx.Event.depth in
let (cstate, pres) = curstate in
let addin acc invar inval = Value.OfIdent.add acc (Var.name invar,inval) in
let ins = List.fold_left2 addin Value.OfIdent.empty (in_var_list it) invals in
......@@ -2267,13 +2270,13 @@ and (to_reactive_prg_ldbg :
let predata = (Value.OfIdent.content data.pres) in
let predata = List.map (fun (n,v) -> "pre_"^n, Value.to_data_val v) predata in
let ctx = { ctx with
Event.ctx_name = rid;
Event.ctx_data = edata@predata;
Event.ctx_inputs = List.map to_event_var (in_var_list it);
Event.ctx_outputs = List.map to_event_var (out_var_list it);
Event.name = rid;
Event.data = edata@predata;
Event.inputs = List.map to_event_var (in_var_list it);
Event.outputs = List.map to_event_var (out_var_list it);
}
in
let (cont2: Event.ctx -> behavior -> Event.t) = fun ctx b ->
let (cont2: ctx -> behavior -> e) = fun ctx b ->
match b with
| Raise x -> excn_cont ctx x
| Vanish -> fail_cont ctx
......@@ -2305,27 +2308,27 @@ and (to_reactive_prg_ldbg :
Value.to_data_val (Value.OfIdent.get locs (Var.name x)))
(loc_var_list it)
in
let enb,d = ctx.Event.ctx_nb, ctx.Event.ctx_depth in
let enb,d = ctx.Event.nb, ctx.Event.depth in
let ctx = event_incr ctx it.arg_opt in
let ctx = Event.decr_event_depth ctx in
let si_atoms = List.map to_src_info zeguard.g_src in
let cstr = Exp.to_expr zeguard.g_form in
let ctx = { ctx with
Event.ctx_name = rid_ctx;
Event.ctx_depth = d_ctx;
Event.name = rid_ctx;
Event.depth = d_ctx;
}
in
let event =
{
Event.step = ctx.Event.ctx_step;
Event.step = ctx.Event.step;
Event.nb = enb;
Event.depth = ctx.Event.ctx_depth;
Event.depth = ctx.Event.depth;
Event.kind = Event.Exit;
Event.lang = "lutin";
(* Event.port = Event.Exit (guard_to_string zeguard, cstr,lazy_si); *)
Event.name = rid;
Event.inputs = ctx.Event.ctx_inputs;
Event.outputs = ctx.Event.ctx_outputs;
Event.inputs = ctx.Event.inputs;
Event.outputs = ctx.Event.outputs;
Event.data = edata;
Event.sinfo = Some (fun () -> {
Event.expr = cstr;
......@@ -2337,26 +2340,26 @@ and (to_reactive_prg_ldbg :
(fun () ->
cont ctx (Reactive.DoStep_ldbg (to_reactive_prg_ldbg rid it state'))
outvals );
Event.terminate = ctx.Event.ctx_terminate;
Event.terminate = ctx.Event.terminate;
}
in
event
in
let enb = ctx.Event.ctx_nb in
let enb = ctx.Event.nb in
let ctx = event_incr ctx it.arg_opt in
let ctx = Event.incr_event_depth ctx in
{
Event.step = ctx.Event.ctx_step;
Event.step = ctx.Event.step;
Event.nb = enb ;
Event.depth = d_ctx;
Event.kind = Event.Call;
Event.lang = "lutin";
Event.name = rid;
Event.inputs = ctx.Event.ctx_inputs;
Event.outputs = ctx.Event.ctx_outputs;
Event.inputs = ctx.Event.inputs;
Event.outputs = ctx.Event.outputs;
Event.data = edata @ predata;
Event.next = (fun () -> genpath_ldbg it data cstate ctx cont2 fail_cont excn_cont);
Event.terminate = ctx.Event.ctx_terminate;
Event.terminate = ctx.Event.terminate;
Event.sinfo = None;
}
......@@ -2381,8 +2384,8 @@ let get_behavior_gen : t -> Var.env_in -> Var.env -> control_state ->
)
)
let get_behavior_gen_ldbg : t -> Var.env_in -> Var.env -> control_state -> Event.ctx ->
(Event.ctx -> behavior_gen -> Event.t) -> Event.t =
let get_behavior_gen_ldbg : t -> Var.env_in -> Var.env -> control_state -> ctx ->
(ctx -> behavior_gen -> e) -> e =
fun it ins pres cstate ctx cont ->
(* prépare les params pour l'appel de la fct. rec. de parcours de trace
on part du principe qu'on a la meme interface que le genpath (?)
......@@ -2449,8 +2452,8 @@ let (step: t -> control_state -> data_state -> control_state * data_state) =
)
(* CPS version of step *)
let (step_ldbg: Event.ctx -> string -> t -> control_state -> data_state ->
(Event.ctx -> control_state -> data_state -> Event.t) -> Event.t) =
let (step_ldbg: ctx -> string -> t -> control_state -> data_state ->
(ctx -> control_state -> data_state -> e) -> e) =
fun ctx node prog ctrl data cont ->
let _ =
(* clean tabulated results to avoid memory leaks.
......@@ -2465,11 +2468,11 @@ let (step_ldbg: Event.ctx -> string -> t -> control_state -> data_state ->
"pre_" ^ n, Value.to_data_val v) (Value.OfIdent.content data.mems))
in
let ctx = { ctx with
Event.ctx_name = node;
Event.ctx_depth = ctx.Event.ctx_depth+1;
Event.ctx_data = datal;
Event.ctx_inputs = List.map to_event_var (in_var_list prog);
Event.ctx_outputs = List.map to_event_var (out_var_list prog);
Event.name = node;
Event.depth = ctx.Event.depth+1;
Event.data = datal;
Event.inputs = List.map to_event_var (in_var_list prog);
Event.outputs = List.map to_event_var (out_var_list prog);
}
in
let cont2 = fun ctx bg ->
......@@ -2481,7 +2484,7 @@ let (step_ldbg: Event.ctx -> string -> t -> control_state -> data_state ->
(* let msg = *)
(* Printf.sprintf *)
(* "Run-time error: unexpected DEADLOCK at event nb %i" *)
(* (ctx.Event.ctx_depth) *)
(* (ctx.Event.depth) *)
(* in *)
(* raise (Global_error msg) *)
......@@ -2514,21 +2517,21 @@ let (step_ldbg: Event.ctx -> string -> t -> control_state -> data_state ->
in
let edata = edata @ (get_sl (out_var_list prog) outs) in
let edata = edata @ (get_sl (loc_var_list prog) locs) in
let enb,d = ctx.Event.ctx_nb, ctx.Event.ctx_depth in
let enb,d = ctx.Event.nb, ctx.Event.depth in
let ctx = event_incr ctx prog.arg_opt in
let ctx = Event.decr_event_depth ctx in
let si_atoms = List.map to_src_info zeguard.g_src in
let cstr = Exp.to_expr zeguard.g_form in
{
Event.step = ctx.Event.ctx_step;
Event.step = ctx.Event.step;
Event.nb = enb;
Event.depth = d;
Event.kind = Event.Exit;
Event.lang = "lutin";
Event.name = node;
Event.inputs = ctx.Event.ctx_inputs;