Skip to content

GitLab

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

Big spring cleaning in the lutin interpreter. 

remove useless options: -boot, -oracle, -cov*

Also, split LustreRun in 2: LutinRun and LustreRun, so that check-rif compiles.
parent 76cc6c4f
Hide whitespace changes
Inline Side-by-side
source/Lutin/main.ml
View file @ a6fa295e
......@@ -116,45 +116,6 @@ let dump_prog p = (
Printf.fprintf stderr "\n";
)
(* Because of lutin migth terminates normally via an exception, it's
easier to store the coverage into in a reference. Indeed, the
alternative would be to store the cov info inside each normal
exception, which would be rather tedious IMHO. R1.
*)
let dummy_cov = Coverage.init [] "" false
let cov = ref dummy_cov (* a dummy cov instead of an option type
to avoid boring match/with. *)
let check_oracle oc lut_in lut_out t = (
match MainArg.oracle () with
| MainArg.NoOracle -> ()
| MainArg.Oracle(in_decl, _, kill_oracle, step_oracle) ->
let all_vals = Value.OfIdent.union lut_in lut_out in
let oracle_inputs =
List.map
(fun (vn,_ )-> vn, Value.to_rif_val (Value.OfIdent.get all_vals vn))
in_decl
in
let oracle_vals = step_oracle oracle_inputs in
match oracle_vals with
| [] -> assert false
| (_, Rif_base.B true)::tail ->
cov := Coverage.update_cov tail !cov;
| (_, Rif_base.B false)::tail ->
let msg = Coverage.dump_oracle_io oracle_inputs tail !cov in
output_string oc (Printf.sprintf "# The oracle returned false at step %i\n" t);
Printf.eprintf "The oracle returned false at step %i\n%s" t msg;
flush stderr;
flush stdout
(* XXX en commentaire en attendant de savoir comment terminer proprement dans Alices *)
(* kill_oracle(); *)
(* ; exit 2 *)
| _ ->
Printf.eprintf "*** Error: the oracle first output ougth to be a Boolean\n";
kill_oracle();
flush stderr;
exit 2
)
(* simu *)
let rec to_simu oc infile mnode = (
......@@ -177,12 +138,7 @@ let rec to_simu oc infile mnode = (
if MainArg.compute_volume () then Solver.set_fair_mode () else Solver.set_efficient_mode ();
!Solver.init_snt ();
if MainArg.boot () then (
Rif.write_interface oc init_state.Prog.s.Prog.out_vars init_state.Prog.s.Prog.in_vars loc
)
else (
Rif.write_interface oc init_state.Prog.s.Prog.in_vars init_state.Prog.s.Prog.out_vars loc;
);
Rif.write_interface oc init_state.Prog.s.Prog.in_vars init_state.Prog.s.Prog.out_vars loc;
Rif.flush oc;
let next_state = init_state in
let lut_memories =
......@@ -193,19 +149,19 @@ let rec to_simu oc infile mnode = (
Value.OfIdent.empty
in
(* first main_loop : no pre context *)
main_loop ~boot:(MainArg.boot()) oc (if MainArg.boot() then 0 else 1) next_state lut_memories lut_memories
main_loop oc 1 next_state lut_memories
)
and main_loop ?(boot=false) oc t state pre_lut_output pre_pre_lut_output = (
and main_loop oc t state pre_lut_output = (
Verbose.exe ( fun () ->
let csnme = (Prog.ctrl_state_to_string_long state.Prog.d.Prog.ctrl_state) in
Verbose.put "#Main.main_loop boot=%b ctrl_state=%s\n" boot csnme;
Verbose.put "#Main.main_loop ctrl_state=%s\n" csnme;
);
if state.Prog.s.Prog.is_final state.Prog.d.Prog.ctrl_state
then ()
else main_loop_core ~boot:boot oc t state pre_lut_output pre_pre_lut_output
else main_loop_core oc t state pre_lut_output
)
and main_loop_core ?(boot=false) oc t state pre_lut_output pre_pre_lut_output = (
and main_loop_core oc t state pre_lut_output = (
let step_str =
("#step " ^ (string_of_int t)) ^
(if state.Prog.d.Prog.verbose >= 1
......@@ -213,27 +169,9 @@ and main_loop_core ?(boot=false) oc t state pre_lut_output pre_pre_lut_output =
else ""
) ^ "\n"
in
let _ =
if MainArg.boot ()
then (
if boot then () else (
Rif.write oc ("\n"^step_str);
if pre_pre_lut_output <> Value.OfIdent.empty then (
Rif.write_outputs oc state.Prog.s.Prog.out_vars pre_pre_lut_output; (* XXX 4 ALICES! *)
);
Rif.write oc "#outs ";
Rif.flush oc;
))
else (
Rif.write oc step_str;
)
in
let _ = Rif.write oc step_str in
(* IF BOOT -> don't ask for input *)
let lut_input =
if boot then Value.OfIdent.empty
else Rif.read stdin (Some oc) state.Prog.s.Prog.in_vars
in
let lut_input =Rif.read stdin (Some oc) state.Prog.s.Prog.in_vars in
let generator = LucFGen.get lut_input state in
(*
Call Lucky explorer/solver
......@@ -241,7 +179,7 @@ and main_loop_core ?(boot=false) oc t state pre_lut_output pre_pre_lut_output =
where type solution = Var.env_out * Var.env_loc
*)
let (next_state, (lut_output, loc)) = try (
Lucky.env_step (MainArg.draw_mode()) lut_input state generator
Lucky.env_step (MainArg.step_mode()) lut_input state generator
) with
| FGen.NoMoreFormula ->
Rif.write oc ("# " ^ (Prog.ctrl_state_to_string_long state.Prog.d.Prog.ctrl_state));
......@@ -264,13 +202,10 @@ and main_loop_core ?(boot=false) oc t state pre_lut_output pre_pre_lut_output =
(fun () -> Printf.fprintf oc "#OUT SUBST LIST=%s\n" (Value.OfIdent.to_string ";" lut_output));
Verbose.exe ~level:3
(fun () -> Printf.fprintf oc "#LOC SUBST LIST=%s\n" (Value.OfIdent.to_string ";" loc));
if not (MainArg.boot ()) then (
Rif.write oc "#outs ";
Rif.write_outputs oc next_state.Prog.s.Prog.out_vars lut_output;
(* XXX faire comme pour les lut_output (ie, en argument de main_loop) *)
if MainArg.show_locals () then (
Rif.write oc "\n#locs ";
Rif.write_outputs oc next_state.Prog.s.Prog.loc_vars loc;
......@@ -278,23 +213,18 @@ and main_loop_core ?(boot=false) oc t state pre_lut_output pre_pre_lut_output =
Rif.write oc "\n";
Rif.flush oc;
);
(* Clean-up cached info that depend on pre or inputs *)
Formula_to_bdd.clear_step ();
!Solver.clear_snt ();
(match MainArg.oracle () with
NoOracle -> ()
| Oracle _ -> if boot then () else check_oracle oc lut_input pre_pre_lut_output t (* XXX 4 ALICES! *)
);
match MainArg.max_steps () with
| None -> main_loop oc (t+1) next_state lut_output pre_lut_output (* XXX 4 ALICES! *)
| None -> main_loop oc (t+1) next_state lut_output
| Some max -> (
if (t < max) then (
(* next pre's are current vals *)
(* let next_state = LutProg.memorize_data next_state lut_input lut_output loc in *)
main_loop oc (t+1) next_state lut_output pre_lut_output (* XXX 4 ALICES! *)
main_loop oc (t+1) next_state lut_output
) else (
Rif.write oc "\n#end\n";
Rif.flush oc
......@@ -314,8 +244,8 @@ let to_exe oc infile mnode = (
let loc_vars = LutExe.loc_var_list exe in
let do_stop = match MainArg.max_steps () with
| None -> fun _ -> false
| Some max -> fun c -> (c >= max)
| None -> (fun _ -> false)
| Some max -> (fun c -> (c >= max))
in
let rec do_step cpt ctrl ins pres = (
......@@ -389,11 +319,7 @@ let to_exe oc infile mnode = (
let step_str = Printf.sprintf "#step %d\n" cpt in
Rif.write oc step_str;
Rif.flush oc;
let ins = if (MainArg.boot()) then
Value.OfIdent.empty
else
Rif.read stdin (Some oc) in_vars
in
let ins = Rif.read stdin (Some oc) in_vars in
(* HERE: init input/output pres *)
let pres = LutExe.get_init_pres exe in
do_step cpt ctrl ins pres
......@@ -423,23 +349,12 @@ let main () = (
in
match MainArg.gen_mode () with
| Simu ->
(match MainArg.oracle (), MainArg.cov_file (), MainArg.reset_cov () with
| Oracle(_,outs,_,_), cov_file, reset ->
let names =
List.fold_left
(fun acc (vn,vt) -> if vt = "bool" then vn::acc else acc)
[]
(List.rev (List.tl outs))
in
cov := (Coverage.init names cov_file reset)
| NoOracle, _, _ -> ()
);
if (MainArg.test_exe ()) then to_exe oc infile mnode else to_simu oc infile mnode
| Cstubs -> (
Luc2c.option.Luc2c.output <- MainArg.outfile () ;
Luc2c.option.Luc2c.seed <- (Some(MainArg.seed ()));
Luc2c.option.Luc2c.step_mode <- (
match (MainArg.draw_mode ()) with
match (MainArg.step_mode ()) with
| Lucky.StepInside -> Luc2c.Inside
| Lucky.StepEdges -> Luc2c.Edges
| Lucky.StepVertices -> Luc2c.Vertices)
......@@ -487,18 +402,6 @@ let main () = (
| End_of_file -> (
(* Terminaison normale ??? *)
)
);
(match MainArg.oracle () with
NoOracle -> ()
| Oracle (_,_, kill_oracle,_) ->
let rif_file =
match riffile () with
None -> "stdout"
| Some f -> f
in
Coverage.dump (MainArg.oracle_file ()) rif_file !cov;
kill_oracle()
)
)
......
source/Lutin/mainArg.ml
View file @ a6fa295e
......@@ -56,51 +56,31 @@ type gen_mode = Simu | GenLuc | Cstubs
let _gen_mode = ref Simu
let gen_mode () = !_gen_mode
let _boot = ref false
let boot () = !_boot
let _step_mode = ref Lucky.StepInside
let step_mode () = !_step_mode
let set_step_mode v = _step_mode := v
let set_precision v = Util.precision := v
let _load_mem = ref false
let load_mem () = !_load_mem
type oracle =
NoOracle
| Oracle of
(string * string) list *
(string * string) list *
(unit -> unit) *
(Rif_base.subst list -> Rif_base.subst list)
let _oracle = ref NoOracle
let oracle () = !_oracle
let _oracle_file = ref ""
let oracle_file () = !_oracle_file
let _cov_file = ref ""
let cov_file () = !_cov_file
let _reset_cov = ref false
let reset_cov () = !_reset_cov
let _draw_mode = ref Lucky.StepInside
let draw_mode () = !_draw_mode
let _seed : int option ref = ref None
let seed () = match !_seed with
| Some i -> i
| None -> (
Random.self_init ();
Random.int max_int
)
| Some i -> i
| None -> ( Random.self_init (); Random.int max_int)
let set_seed s = _seed := s
let _compute_volume = ref false
let compute_volume () = !_compute_volume
let set_compute_volume v = _compute_volume := v
let _max_steps : int option ref = ref None
let max_steps () = !_max_steps
let _show_locals = ref false
let show_locals () = !_show_locals
let set_show_locals v = _show_locals := v
let _see_all_options = ref false
let see_all_options () = !_see_all_options
......@@ -266,18 +246,6 @@ let mkoptab () = (
["Save the generated data using the RIF format"]
;
mkopt
["--cov"]
~arg:" <cov file>"
(Arg.String(function f -> _cov_file := f))
["Override the default coverage file name (<oracle name>.cov by default)"]
;
mkopt
["--reset-cov"]
(Arg.Unit(function f -> _reset_cov := true))
["Reset the coverage rate before running"]
;
mkopt
["-L"; "-lib"]
~arg:" <string>"
......@@ -286,24 +254,7 @@ let mkoptab () = (
;
(* ---- SIMU/SOLVER OPTIONS *)
(* simu *)
mkopt
["-b";"-boot"]
(Arg.Unit(fun () ->
_boot := true;
Luc2c.option.Luc2c.boot <- true
))
["Perform a first step without requiring inputs";
("Fails if inputs are actually required at first step (default: "
^(if !_boot then "on" else "off")^")");
"nb : in this mode, I/O are considered w.r.t. the system being ";
"stimulated by the lutin program."
]
;
mkopt
["--load-mem"]
(Arg.Unit(function () -> _load_mem := true; Luc2c.option.Luc2c.load_mem <- true))
["Read the output memories before the first instant." ]
;
mkopt
["-seed"]
~arg:" <int>"
......@@ -318,18 +269,18 @@ let mkoptab () = (
;
mkopt
["--step-inside"]
(Arg.Unit(function _ -> _draw_mode := Lucky.StepInside))
(Arg.Unit(function _ -> _step_mode := Lucky.StepInside))
["Draw inside the convex hull of solutions (default)"]
;
mkopt
["--step-edges"]
(Arg.Unit(function _ -> _draw_mode := Lucky.StepEdges))
(Arg.Unit(function _ -> _step_mode := Lucky.StepEdges))
(* "draw inside the convex hull of solutions, but a little bit more at edges and vertices" *)
["Draw a little bit more at edges and vertices"]
;
mkopt
["--step-vertices"]
(Arg.Unit(function _ -> _draw_mode := Lucky.StepVertices))
(Arg.Unit(function _ -> _step_mode := Lucky.StepVertices))
["Draw among the vertices of the convex hull of solutions"]
;
mkopt
......
source/Lutin/mainArg.mli
View file @ a6fa295e
......@@ -31,14 +31,14 @@ type gen_mode =
| Cstubs (* Generate C stubs files *)
val gen_mode : unit -> gen_mode
val boot : unit -> bool
val load_mem : unit -> bool
val seed : unit -> int
val set_seed : int option -> unit
(* n.b. if "Some l", l is certainly non-empty ! *)
val libs : unit -> string list option
(* Output *)
val outfile : unit -> string option
val outpipe : unit -> bool
......@@ -47,22 +47,17 @@ val outpipe : unit -> bool
val riffile : unit -> string option
val show_locals : unit -> bool
val set_show_locals : bool -> unit
val see_all_options : unit -> bool
(* Options du solver *)
val draw_mode : unit -> Lucky.step_mode
val step_mode : unit -> Lucky.step_mode
val set_step_mode : Lucky.step_mode -> unit
val compute_volume : unit -> bool
val set_compute_volume : bool -> unit
val set_precision : int -> unit
type oracle =
| NoOracle
| Oracle of
(string * string) list *
(string * string) list *
(unit -> unit) *
(Rif_base.subst list -> Rif_base.subst list)
val oracle : unit -> oracle
val oracle_file : unit -> string
val cov_file : unit -> string
val reset_cov : unit -> bool
source/common/lustreRun.ml
View file @ a6fa295e
......@@ -165,50 +165,6 @@ let (make_socket_init : string -> int ->
vars_in, vars_out, kill, step, in_init, out_init
(**********************************************************************************)
let (var_to_string_pair: Exp.var -> string * string) =
fun v -> Var.name v, Type.to_string2 (Var.typ v)
let (to_subst_list : (string * string) list -> Value.OfIdent.t -> Rif_base.subst list) =
fun var_decl vals ->
List.map (fun (n,_) -> n, Value.to_rif_val (Value.OfIdent.get vals n)) var_decl
let (to_vals : Rif_base.subst list -> Value.OfIdent.t) =
List.fold_left
(fun acc (n,v) -> Value.OfIdent.add acc (n, Value.from_rif_val v))
Value.OfIdent.empty
let (make_lut: ?verb:int -> ?libs:string list option -> string -> string ->
vars * vars * (string -> unit) * (Rif_base.subst list -> Rif_base.subst list)) =
fun ?(verb = 0) ?(libs = None) prog node ->
let lut_mach = LutExe.make ~libs:libs prog node in
let lut_in = List.map var_to_string_pair (LutExe.in_var_list lut_mach) in
let lut_out = List.map var_to_string_pair (LutExe.out_var_list lut_mach) in
let lut_memories =
if LtopArg.args.LtopArg.delay_env_outputs then
LutExe.get_init_pres lut_mach
(* XXX Lire les valeurs des mémoires des programmes lutin dans fichier. *)
else
Value.OfIdent.empty
in
let ctrl_state = ref (LutExe.get_init_state lut_mach) in
let data_state = ref
{ LutExe.ins = Value.OfIdent.empty ;
LutExe.outs = lut_memories;
LutExe.mems = LutExe.get_init_pres lut_mach
}
in
let lut_step sl =
let _ = data_state := { !data_state with LutExe.ins = to_vals sl } in
let new_cs, new_ds = LutExe.step lut_mach !ctrl_state !data_state in
ctrl_state := new_cs;
data_state := new_ds;
to_subst_list lut_out new_ds.LutExe.outs
in
Verbose.set (verb);
lut_in, lut_out, (fun _ -> ()), lut_step
(**********************************************************************************)
......
source/common/lustreRun.mli
View file @ a6fa295e
......@@ -50,12 +50,6 @@ val make_socket_init : string -> int ->
vars * vars * (string -> unit) * (Rif_base.subst list -> Rif_base.subst list)
* Rif_base.subst list * Rif_base.subst list
val make_lut: ?verb:int -> ?libs:string list option -> string -> string ->
vars * vars * (string -> unit) * (Rif_base.subst list -> Rif_base.subst list)
(** [make_luciole inputs outputs dro_file]
fails if dro_file does not exists, or if its interface is not
......
source/common/lutinRun.ml 0 → 100644
View file @ a6fa295e
(**********************************************************************************)
let (var_to_string_pair: Exp.var -> string * string) =
fun v -> Var.name v, Type.to_string2 (Var.typ v)
let (to_subst_list : (string * string) list -> Value.OfIdent.t -> Rif_base.subst list) =
fun var_decl vals ->
List.map (fun (n,_) -> n, Value.to_rif_val (Value.OfIdent.get vals n)) var_decl
let (to_vals : Rif_base.subst list -> Value.OfIdent.t) =
List.fold_left
(fun acc (n,v) -> Value.OfIdent.add acc (n, Value.from_rif_val v))
Value.OfIdent.empty
let make_lut
?(verb = 0) ?(libs = None) ?(step_mode = Lucky.StepInside) ?(seed: int option = None)
?(fair_mode:bool = false) ?(show_locals: bool = false) ?(precision: int = 2)
prog node =
let lut_mach =
LutExe.make
~libs:libs ~verb:verb ~step_mode:step_mode ~seed:seed ~fair_mode:fair_mode
~show_locals:show_locals ~precision:precision
prog node
in
let lut_in = List.map var_to_string_pair (LutExe.in_var_list lut_mach) in
let lut_out = List.map var_to_string_pair (LutExe.out_var_list lut_mach) in
let lut_memories =
if LtopArg.args.LtopArg.delay_env_outputs then
LutExe.get_init_pres lut_mach
(* XXX Lire les valeurs des mémoires des programmes lutin dans fichier. *)
else
Value.OfIdent.empty
in
let ctrl_state = ref (LutExe.get_init_state lut_mach) in
let data_state = ref
{ LutExe.ins = Value.OfIdent.empty;
LutExe.outs = lut_memories;
LutExe.mems = LutExe.get_init_pres lut_mach
}
in
let lut_step sl =
let _ = data_state := { !data_state with LutExe.ins = to_vals sl } in
let new_cs, new_ds = LutExe.step lut_mach !ctrl_state !data_state in
ctrl_state := new_cs;
data_state := new_ds;
to_subst_list lut_out new_ds.LutExe.outs
in
lut_in, lut_out, (fun _ -> ()), lut_step
source/common/lutinRun.mli 0 → 100644
View file @ a6fa295e
(* *)
val make_lut: ?verb:int -> ?libs:string list option -> ?step_mode: Lucky.step_mode ->
?seed: int option -> ?fair_mode:bool -> ?show_locals: bool -> ?precision: int ->
string -> string ->
vars * vars * (string -> unit) * (Rif_base.subst list -> Rif_base.subst list)
source/misc/checkRif.ml
View file @ a6fa295e
......@@ -172,7 +172,7 @@ let main () =
"\nData in %s are ok with respect to %s\n"
(match arg.rif with Some f -> f | None -> "stdin") arg.ec;
close_in rif_ic;
kill_oracle ();
kill_oracle str;
print_string str;
flush_all();
in
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment