Commit a919ca61 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Take into account the change in Rdbg.event w.r.t. event number (rdbg 1.51).

Also correct a lot of bugs.

Indeed, this module was not tested when I initially wrote it, because
of the sig faults pbs.

Not that it is still not working properly, as the CPS transformation
breaks Pascal's way of handling Lutin choice points backtracking, that
is based on ocaml exception. Indeed consider this exemple:

try
   call_to_a_func_that_traverse_the_lutin_FT ()
with Deadlock _ ->
   the_backtrack code

now, if call_to_a_func_that_traverse_the_lutin_FT returns an event,
the ocaml try is deleted !!!
parent 440b75db
......@@ -19,7 +19,7 @@ BuildTools: ocamlbuild
Executable lutin
Path: lutin/src
MainIs: main.ml
BuildDepends: str,unix,num,rdbg-plugin,lutin-utils,ezdl,gbddml,polka,camlp4,camlidl
BuildDepends: str,unix,num,rdbg-plugin (>= 1.51),lutin-utils,ezdl,gbddml,polka,camlp4,camlidl
NativeOpt: -package num # XXX turn around a bug in oasis/ocamlbuild/ocamlfind?
Build: true
Install:true
......@@ -43,7 +43,7 @@ Library lut4c
Path: lutin/src
Modules: Lut4c
FindlibParent: lutin
BuildDepends: str,unix,num,rdbg-plugin,lutin-utils,ezdl,gbddml,polka,camlp4
BuildDepends: str,unix,num,rdbg-plugin (>= 1.51),lutin-utils,ezdl,gbddml,polka,camlp4
Install: true
CSources: lut4c_stubs.h,lut4c_stubs.c
CCOpt: -fPIC
......@@ -109,7 +109,7 @@ Library polka
Executable "check-rif"
Path: ltop/src
MainIs: checkRif.ml
BuildDepends: num,str,unix,rdbg-plugin,ezdl,lustre-v6
BuildDepends: num,str,unix,lutils,ezdl,lustre-v6
NativeOpt: -package num # XXX turn around a bug in oasis/ocamlbuild/ocamlfind?
Build: true
Install:true
......
# OASIS_START
# DO NOT EDIT (digest: a9cc155d53b009a6a454d738b3ca1969)
# DO NOT EDIT (digest: cc49fecfccfabb8b8c35ce58808d3cc7)
# Ignore VCS directories, you can use the same kind of rule outside
# OASIS_START/STOP if you want to exclude directories that contains
# useless stuff for the build process
......@@ -142,14 +142,14 @@ true: annot, bin_annot
"ltop/src/checkRif.native": oasis_executable_check_rif_native
<ltop/src/*.ml{,i,y}>: oasis_executable_check_rif_native
"ltop/src/checkRif.native": package(lustre-v6)
"ltop/src/checkRif.native": package(lutils)
"ltop/src/checkRif.native": package(num)
"ltop/src/checkRif.native": package(rdbg-plugin)
"ltop/src/checkRif.native": package(str)
"ltop/src/checkRif.native": package(unix)
"ltop/src/checkRif.native": use_ezdl
<ltop/src/*.ml{,i,y}>: package(lustre-v6)
<ltop/src/*.ml{,i,y}>: package(lutils)
<ltop/src/*.ml{,i,y}>: package(num)
<ltop/src/*.ml{,i,y}>: package(rdbg-plugin)
<ltop/src/*.ml{,i,y}>: use_ezdl
# Executable call-via-socket
"ltop/src/call-via-socket.native": package(str)
......
(* Time-stamp: <modified the 21/10/2015 (at 16:32) by Erwan Jahier> *)
(* Time-stamp: <modified the 05/02/2016 (at 14:59) by Erwan Jahier> *)
open RdbgPlugin
type vars = (string * Data.t) list
......@@ -53,75 +53,77 @@ let get_io_from_lustre a b =
let (make_ec : string -> RdbgPlugin.t) =
fun ec_file ->
let ec_in, ec_out = get_io_from_lustre ec_file None in
let (ec_stdin_in, ec_stdin_out) = Unix.pipe () in
let (ec_stdout_in, ec_stdout_out) = Unix.pipe () in
let ec_ic = Unix.in_channel_of_descr ec_stdout_in in
let ec_oc = Unix.out_channel_of_descr ec_stdin_out in
let ec_in, ec_out = get_io_from_lustre ec_file None in
let (ec_stdin_in, ec_stdin_out) = Unix.pipe () in
let (ec_stdout_in, ec_stdout_out) = Unix.pipe () in
let ec_ic = Unix.in_channel_of_descr ec_stdout_in in
let ec_oc = Unix.out_channel_of_descr ec_stdin_out in
let _ =
set_binary_mode_in ec_ic false;
set_binary_mode_out ec_oc false
in
let pid_lustre =
let arg_list = ["ecexe"^(Util.exe ()); "-r"; "-rif"; ec_file] in
let arg_array = Array.of_list arg_list in
let prog = List.hd arg_list in
try
if !debug then (
List.iter (fun x -> output_string stderr (x ^ " ")) arg_list;
output_string stderr "\n";
flush stderr
);
Unix.create_process prog arg_array
ec_stdin_in ec_stdout_out ec_stdout_out
with Unix.Unix_error(e,_, prog) ->
let msg = Unix.error_message e in
Printf.eprintf "*** Error when creating process with %s: %s\n" prog msg;
exit 2
in
let _ = Printf.eprintf "Process %d (ecexe) created\n" pid_lustre; flush stderr in
let kill msg =
(* Printf.print "EOF" *)
Unix.close ec_stdin_in;
Unix.close ec_stdin_out;
Unix.close ec_stdout_in;
Unix.close ec_stdout_out;
(try
Printf.eprintf "%s\nKilling process %d\n" msg pid_lustre;
flush stderr;
Unix.kill pid_lustre Sys.sigterm
with e -> (Printf.printf "Killing of ecexe process failed: %s\n" (Printexc.to_string e) ))
in
let step = step_channel ec_ic ec_oc ec_in ec_out in
let step_dbg sl ctx cont =
{
Event.nb = Event.get_nb ();
Event.step = ctx.Event.ctx_step;
Event.depth = ctx.Event.ctx_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.next = (fun () -> cont (step sl) ctx);
Event.terminate = ctx.Event.ctx_terminate;
}
in
let _ =
set_binary_mode_in ec_ic false;
set_binary_mode_out ec_oc false
in
let pid_lustre =
let arg_list = ["ecexe"^(Util.exe ()); "-r"; "-rif"; ec_file] in
let arg_array = Array.of_list arg_list in
let prog = List.hd arg_list in
try
if !debug then (
List.iter (fun x -> output_string stderr (x ^ " ")) arg_list;
output_string stderr "\n";
flush stderr
);
Unix.create_process prog arg_array
ec_stdin_in ec_stdout_out ec_stdout_out
with Unix.Unix_error(e,_, prog) ->
let msg = Unix.error_message e in
Printf.eprintf "*** Error when creating process with %s: %s\n" prog msg;
exit 2
in
let _ = Printf.eprintf "Process %d (ecexe) created\n" pid_lustre; flush stderr in
let kill msg =
(* Printf.print "EOF" *)
Unix.close ec_stdin_in;
Unix.close ec_stdin_out;
Unix.close ec_stdout_in;
Unix.close ec_stdout_out;
(try
Printf.eprintf "%s\nKilling process %d\n" msg pid_lustre;
flush stderr;
Unix.kill pid_lustre Sys.sigterm
with e -> (Printf.printf "Killing of ecexe process failed: %s\n" (Printexc.to_string e) ))
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 ctx = Event.incr_event_nb ctx in
{
id = "";
inputs = ec_in;
outputs= ec_out;
kill= kill;
init_inputs= [];
init_outputs= [];
step = step;
step_dbg = step_dbg
}
Event.nb = enb;
Event.step = ctx.Event.ctx_step;
Event.depth = ctx.Event.ctx_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.next = (fun () -> cont (step sl) ctx);
Event.terminate = ctx.Event.ctx_terminate;
}
in
{
id = "";
inputs = ec_in;
outputs= ec_out;
kill= kill;
init_inputs= [];
init_outputs= [];
step = step;
step_dbg = step_dbg
}
(* Via une edition de liens dynamique *)
let (make_ec_dynlink: string -> string -> string -> RdbgPlugin.t) =
......@@ -215,11 +217,13 @@ 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 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.nb = Event.get_nb ();
Event.nb = enb;
Event.kind = Event.Exit;
Event.lang = "socket";
Event.name=sock_adr ^ ":" ^ (string_of_int port);
......@@ -318,10 +322,12 @@ 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 ctx = Event.incr_event_nb ctx in
{
Event.step = ctx.Event.ctx_step;
Event.data = ctx.Event.ctx_data;
Event.nb = Event.get_nb ();
Event.nb = enb;
Event.depth = ctx.Event.ctx_depth;
Event.kind = Event.Exit;
Event.lang = "ec";
......
......@@ -9,7 +9,8 @@ type vars = (string * Data.t) list
let list_minus a b = List.filter (fun v -> not (List.mem v b)) a
(* returns a U b *)
let list_union a b = List.fold_left (fun acc x -> if (List.mem x acc) then acc else x::acc) a b
let list_union a b =
List.fold_left (fun acc x -> if (List.mem x acc) then acc else x::acc) a b
(* I defined mine because i need to know the seed that has been drawn by self_init. *)
let random_seed () =
......@@ -22,7 +23,8 @@ let gnuplot_pid_ref = ref None
let gnuplot_oc = ref None
(* Returns luciole io if necessary *)
let (check_compat : vars -> vars -> vars -> vars -> vars -> vars -> int * (vars * vars) option) =
let (check_compat : vars -> vars -> vars -> vars -> vars -> vars ->
int * (vars * vars) option) =
fun env_in env_out sut_in sut_out oracle_in oracle_out ->
(* cf lurette.set_luciole_mode_if_necessary to add a call to luciole *)
......@@ -50,12 +52,14 @@ let (check_compat : vars -> vars -> vars -> vars -> vars -> vars -> int * (vars
)
else if missing_oracle_in <> [] then (
let missing_str = vars_to_string missing_oracle_in in
Printf.printf "Some variables are missing in input of the oracle: %s\n" missing_str;
Printf.printf "Some variables are missing in input of the oracle: %s\n"
missing_str;
2,None
)
else (
if List.mem ("Step") (fst(List.split luciole_in)) then (
Printf.printf "*** You cannot use the name 'Step' for a variable with lurette, sorry.\n";
Printf.printf
"*** You cannot use the name 'Step' for a variable with lurette, sorry.\n";
flush stdout;
2,None
) else (
......@@ -69,8 +73,8 @@ 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) -> Event.t) list *
Data.subst list list * Data.subst list list) =
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.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
let aux rp =
......@@ -118,7 +122,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 -> Event.ctx ->
(Data.subst list -> Event.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...
......@@ -131,7 +136,8 @@ let (step_dbg_sl :
fun stepl res_stepl sl ->
match stepl with
| [] -> cont (List.flatten (res_stepl))
| step::stepl -> step sl ctx (fun res_sl ctx -> iter_step stepl (res_sl::res_stepl) sl)
| step::stepl ->
step sl ctx (fun res_sl ctx -> iter_step stepl (res_sl::res_stepl) sl)
in
iter_step step_dbg_sl_l [] sl
......@@ -149,7 +155,8 @@ let (start : unit -> Event.t) =
let sut_init_out = List.flatten sut_init_out_l in
(* Get oracle info (var names, step func, etc.)*)
let oracle_in_l, oracle_out_l, oracle_kill_l, oracle_step_sl_l, oracle_step_dbg_sl_l, _, _ =
let oracle_in_l, oracle_out_l, oracle_kill_l, oracle_step_sl_l,
oracle_step_dbg_sl_l, _, _ =
make_rp_list args.oracles
in
let oracle_kill msg = List.iter (fun f -> f msg) oracle_kill_l in
......@@ -186,25 +193,29 @@ let (start : unit -> Event.t) =
Printf.printf "env input : \n%s\n" env_input_str;
Printf.printf "env output : \n%s\n" env_output_str;
Printf.printf "oracle(s) input : \n%s\n" oracle_input_str;
List.iter (fun str -> Printf.printf "oracle output : \n%s\n" str) oracle_output_str_l;
List.iter (fun str -> Printf.printf "oracle output : \n%s\n" str)
oracle_output_str_l;
flush stdout
in
(* Check var names and types compat. *)
let res_compat, luciole_io_opt =
check_compat flat_env_in flat_env_out flat_sut_in flat_sut_out flat_oracle_in flat_oracle_out
check_compat flat_env_in flat_env_out flat_sut_in flat_sut_out
flat_oracle_in flat_oracle_out
in
let (luciole_kill, luciole_step), luciole_outputs_vars =
match luciole_io_opt with
| None -> ((fun _ -> ()),(fun _ -> [])),[]
| Some (luciole_in, luciole_out) ->
(LustreRun.make_luciole "./lurette_luciole.dro" luciole_in luciole_out), luciole_out
(LustreRun.make_luciole "./lurette_luciole.dro" luciole_in luciole_out),
luciole_out
in
let seed =
match args.seed with
| None -> random_seed ()
| Some seed -> seed
in
let cov_init = (* XXX faut-il renommer les sorties de l'oracle ou raler en cas de clash ? *)
let cov_init = (* XXX faut-il renommer les sorties de l'oracle ou raler en
cas de clash ? *)
if List.flatten oracle_out_l = [] then NO else
let oracle_out = List.flatten (List.map List.tl oracle_out_l) in
if List.length oracle_out < 1 then OO else
......@@ -214,8 +225,9 @@ let (start : unit -> Event.t) =
OC (Coverage.init names args.cov_file args.reset_cov_file)
in
let oc = open_out args.output in
let sim2chro_oc = if args.display_sim2chro then Util2.sim2chro_dyn () else open_out "/dev/null" in
let sim2chro_oc =
if args.display_sim2chro then Util2.sim2chro_dyn () else open_out "/dev/null"
in
let filter vals vars =
List.map (fun (n,t) -> n,
try List.assoc n vals
......@@ -237,7 +249,9 @@ let (start : unit -> Event.t) =
OC cov -> Coverage.dump_oracle_io oracle_in_vals tail cov
| _ -> ""
in
let msg = Printf.sprintf "\n*** The oracle returned false at step %i\n%s" i msg in
let msg =
Printf.sprintf "\n*** The oracle returned false at step %i\n%s" i msg
in
print_string msg;
flush stdout;
if args.stop_on_oracle_error then raise (OracleError msg) else tail
......@@ -266,7 +280,9 @@ let (start : unit -> Event.t) =
| NO -> ()
| OO -> ()
| OC cov ->
let str = String.concat ", " (List.map reactive_program_to_string args.oracles) in
let str =
String.concat ", " (List.map reactive_program_to_string args.oracles)
in
Coverage.dump str args.output cov
in
(* The main loop *)
......@@ -329,13 +345,17 @@ let (start : unit -> Event.t) =
Event.ctx_data = edata;
}
in
let cont = loop3 cov env_in_vals pre_env_out_vals env_out_vals ctx i luciole_outs in
let cont =
loop3 cov env_in_vals pre_env_out_vals env_out_vals ctx i luciole_outs
in
step_dbg_sl sut_step_dbg_sl_l sut_in_vals ctx cont
else
let sut_step_sl sl = List.flatten (List.map (fun f -> f sl) sut_step_sl_l) in
let sut_out_vals = sut_step_sl sut_in_vals in
loop3 cov env_in_vals pre_env_out_vals env_out_vals ctx i luciole_outs sut_out_vals
and loop3 cov env_in_vals pre_env_out_vals env_out_vals ctx i luciole_outs sut_out_vals =
loop3 cov env_in_vals pre_env_out_vals env_out_vals ctx i
luciole_outs sut_out_vals
and loop3 cov env_in_vals pre_env_out_vals env_out_vals ctx i
luciole_outs sut_out_vals =
let sut_out_vals =
try List.map (fun (v,vt) -> v,List.assoc v sut_out_vals) flat_sut_out
with Not_found -> sut_out_vals
......@@ -364,7 +384,8 @@ let (start : unit -> Event.t) =
if args.delay_env_outputs then (
output_string oc (String.concat " " (List.map print_val (pre_env_out_vals)));
output_string sim2chro_oc (String.concat " " (List.map print_val (pre_env_out_vals)));
output_string
sim2chro_oc (String.concat " " (List.map print_val (pre_env_out_vals)));
)
else (
output_string oc (String.concat " " (List.map print_val env_out_vals));
......@@ -385,7 +406,6 @@ let (start : unit -> Event.t) =
output_string sim2chro_oc "\n";
flush sim2chro_oc;
Event.incr_nb ();
if not args.go && args.display_gnuplot then (
if i = 0 then (
let oc, pid =
......@@ -415,8 +435,9 @@ let (start : unit -> Event.t) =
gnuplot_pid_ref := None);
killem_all cov
in
let enb = ctx.Event.ctx_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;
......@@ -425,7 +446,7 @@ let (start : unit -> Event.t) =
}
in
{
Event.nb = Event.get_nb ();
Event.nb = enb;
Event.step = i;
Event.kind = Event.Ltop;
Event.depth = 1;
......@@ -450,11 +471,13 @@ let (start : unit -> Event.t) =
let loc = None in
let _ =
if args.compute_volume then Solver.set_fair_mode () else Solver.set_efficient_mode ();
if args.compute_volume then Solver.set_fair_mode ()
else Solver.set_efficient_mode ();
!Solver.init_snt ();
Random.init seed;
Rif.write oc ("# This is lurette Version " ^ Version.str ^ " (\"" ^Version.sha^"\")\n");
Rif.write oc ("# This is lurette Version " ^ Version.str ^
" (\"" ^Version.sha^"\")\n");
Rif.write oc ("# The random engine was initialized with the seed " ^
(string_of_int seed) ^ "\n" );
RifIO.write_interface oc
......@@ -467,6 +490,7 @@ let (start : unit -> Event.t) =
in
let ctx =
{
Event.ctx_nb = 1;
Event.ctx_step = 1;
Event.ctx_name = "ltop";
Event.ctx_depth = 1;
......
This diff is collapsed.
......@@ -67,7 +67,7 @@ type behavior =
(* lazzy-like list *)
type behavior_gen =
| NoMoreBehavior of int
| NoMoreBehavior of int (* event number *)
| SomeBehavior of behavior * (unit -> behavior_gen)
......@@ -89,7 +89,7 @@ val make_pre : t -> Var.env_in -> Var.env_out -> Var.env_loc -> Var.env
*)
val step: t -> control_state -> data_state -> control_state * data_state
val step_ldbg: Event.ctx -> string -> t -> control_state -> data_state ->
(control_state -> data_state -> Event.t) -> Event.t
(Event.ctx -> control_state -> data_state -> Event.t) -> Event.t
(***** Interface for building simple step main loop (e.g. for run statements *)
......
(* Time-stamp: <modified the 21/10/2015 (at 11:52) by Erwan Jahier> *)
(* Time-stamp: <modified the 08/02/2016 (at 15:57) by Erwan Jahier> *)
(**********************************************************************************)
type vars = (string * Data.t) list
......@@ -50,16 +50,17 @@ let make argv =
to_subst_list lut_out new_ds.LutExe.outs
in
let (lut_step_dbg:
Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t) =
Data.subst list -> Event.ctx ->
(Data.subst list -> Event.ctx -> Event.t) -> Event.t) =
fun sl ctx cont ->
let cont_lut_step =
let cont_lut_step ctx =
fun new_cs new_ds ->
ctrl_state := new_cs;
data_state := new_ds;
cont (to_subst_list lut_out new_ds.LutExe.outs) ctx
in
data_state := { !data_state with LutExe.ins = to_vals sl };
(* { (* XXX l'enlever quand j'aurais trouvé le bon endroit dans lutExe ?? *) *)
(* { (* XXX l'enlever quand j'aurais trouvé le bon endroit dans lutExe ?? *) *)
(* Event.step = ctx.Event.ctx_step; *)
(* Event.kind = "lutin_step prog='" ^ (String.concat "," prog) ^ *)
(* "' node ='" ^ node ^ "' \n dump expr =" ^ *)
......
......@@ -240,6 +240,8 @@ let dbgexe = Verbose.get_flag "LutExe"
let quit oc = Rif.write oc "q\n"; Rif.flush oc
(* simu with LutExe *)
let to_exe oc infile mnode opt = (
let exe = LutExe.make opt infile mnode in
......@@ -274,7 +276,7 @@ let to_exe oc infile mnode opt = (
match b with
| LutExe.Goto (zeguard, ctrl') -> (
(* THIS IS THE NORMAL BEHAVIOR *)
Event.incr_nb ();
MainArg.event_incr opt;
let (outs, locs) = try LutExe.find_one_sol exe zeguard
with Not_found -> assert false
in
......@@ -327,13 +329,15 @@ let to_exe oc infile mnode opt = (
Rif.flush oc
);
let pres' = LutExe.make_pre exe ins outs locs in
let ins' = Rif.read (Verbose.level()>0) stdin (if noo then Some oc else None) in_vars in
Event.incr_nb ();
let ins' = Rif.read (Verbose.level()>0) stdin
(if noo then Some oc else None) in_vars in
MainArg.event_incr opt;
do_step (cpt+1) ctrl' ins' pres'
)
)
| LutExe.Raise x -> (
Rif.write oc ("\n#end. Simulation ended with uncaught user exception \""^x^"\"\n");
Rif.write
oc ("\n#end. Simulation ended with uncaught user exception \""^x^"\"\n");
quit oc;
Rif.flush oc;
exit 2
......@@ -467,7 +471,6 @@ let main () = (
Rif.flush oc;
exit 1
)
| Global_error s -> (
print_global_error s;
Rif.write oc ("\n#end.\n# "^s^"\n");
......
......@@ -44,6 +44,7 @@ type t = {
mutable _call_gnuplot: bool;
mutable _run:bool;
mutable _boot:bool;
mutable _event_nb:int;
}
let (make_opt : unit -> t) =
......@@ -78,6 +79,7 @@ let (make_opt : unit -> t) =
_call_gnuplot = false;
_run=true;
_boot=false;
_event_nb=0;
}
......@@ -99,6 +101,21 @@ let set_seed opt s =
| None -> ());
opt._seed <- s
(* Emulate the event number when not run under rdbg so that we are able
to tell at which event we reached a deadlock
*)
(* let event_nb = ref 0 *)
let event_incr opt =
let seed = match opt._seed with Some i -> i | None -> assert false in
opt._event_nb <- opt._event_nb + 1;
Random.init (seed + opt._event_nb)
let (get_event_nb : t -> int) =
fun opt ->
opt._event_nb
(* all unrecognized options are accumulated *)
let (add_other : t -> string -> unit) =
fun opt s ->
......
......@@ -43,6 +43,9 @@ val load_mem : t -> bool
val seed : t -> int
val set_seed : t -> int option -> unit
val event_incr : t -> unit
val get_event_nb : t -> int
(* n.b. if "Some l", l is certainly non-empty ! *)
val libs : t -> string list option
val set_libs : t -> string list -> t
......
......@@ -5,8 +5,14 @@ type prg = DoStep of (Value.t list -> Value.t list * prg)
let step p = match p with DoStep _p -> _p
type prg_ldbg = DoStep_ldbg of ( Value.t list -> (prg_ldbg -> Value.t list -> Event.t) -> Event.t)
type prg_ldbg =
DoStep_ldbg of (Event.ctx -> Value.t list ->
(Event.ctx -> prg_ldbg -> Value.t list -> Event.t) -> Event.t)
let (step_ldbg : prg_ldbg -> Value.t list -> (prg_ldbg -> Value.t list -> Event.t) -> Event.t) =
fun p vl cont ->
match p with DoStep_ldbg _p -> _p vl cont
let (step_ldbg : Event.ctx ->
prg_ldbg -> Value.t list -> (Event.ctx -> prg_ldbg -> Value.t list -> Event.t)
-> Event.t) =
fun ctx p vl cont ->
<