Skip to content

GitLab

Commit 0c651611 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Add a -rif <file name> option to lutin, that stores all the exchanged data into a file 

using the RIF format.
parent ad110579
Hide whitespace changes
Inline Side-by-side
source/Lucky/luc_exe.ml
View file @ 0c651611
......@@ -230,9 +230,9 @@ and
| Some seed -> seed
in
Random.init seed ;
output_string stderr "#The random engine was initialized with the seed ";
output_string stderr (string_of_int seed);
output_string stderr "\n";
Rif.write stderr "#The random engine was initialized with the seed ";
Rif.write stderr (string_of_int seed);
Rif.write stderr "\n";
flush stderr ;
if options.verb > 1 then (
......@@ -270,8 +270,8 @@ and
Lucky.env_step options.draw_mode ins init_state ral
with
FGen.NoMoreFormula ->
print_string ("# " ^ (Prog.ctrl_state_to_string_long init_state.d.ctrl_state));
print_string (
Rif.write stdout ("# " ^ (Prog.ctrl_state_to_string_long init_state.d.ctrl_state));
Rif.write stdout (
"# No transition is labelled by a satisfiable formula.\n" ^
"# The Lucky automata is blocked.\n");
flush stdout;
......@@ -280,15 +280,15 @@ and
else
exit 2
in
print_string ("\n#step 1\n");
print_string "\n#outs ";
Rif.write stdout next_state.s.Prog.out_vars out ;
Rif.write stdout ("\n#step 1\n");
Rif.write stdout "\n#outs ";
Rif.write_outputs stdout next_state.s.Prog.out_vars out ;
flush stdout;
if options.locals then (
print_string "\n#locs ";
Rif.write stdout next_state.s.Prog.loc_vars loc
Rif.write stdout "\n#locs ";
Rif.write_outputs stdout next_state.s.Prog.loc_vars loc
);
print_string "\n";
Rif.write stdout "\n";
flush stdout;
next_state
else
......@@ -311,7 +311,7 @@ and
let _ =
if not options.boot then
(
print_string step_str;
Rif.write stdout step_str;
)
in
let (input, state') = Rif.read (LucProg.make_state None) stdin state in
......@@ -322,8 +322,8 @@ and
Lucky.env_step options.draw_mode input state' ral
with
FGen.NoMoreFormula ->
print_string ("# " ^ (Prog.ctrl_state_to_string_long state.d.ctrl_state));
print_string (
Rif.write stdout ("# " ^ (Prog.ctrl_state_to_string_long state.d.ctrl_state));
Rif.write stdout (
"# No transition is labelled by a satisfiable formula.\n" ^
"# The Lucky automata is blocked.\n");
flush stdout;
......@@ -350,18 +350,18 @@ and
read_oracle ()
in
if options.boot then print_string step_str;
if options.boot then Rif.write stdout step_str;
if state.d.verbose >= 1 then print_mem state;
print_string "\n#outs ";
Rif.write stdout next_state.s.Prog.out_vars out ;
Rif.write stdout "\n#outs ";
Rif.write_outputs stdout next_state.s.Prog.out_vars out ;
if options.locals then (
print_string "\n#locs ";
Rif.write stdout next_state.s.Prog.loc_vars loc
Rif.write stdout "\n#locs ";
Rif.write_outputs stdout next_state.s.Prog.loc_vars loc
);
print_string "\n";
Rif.write stdout "\n";
if options.show_automata then (
if (state.d.ctrl_state <> next_state.d.ctrl_state) then
......@@ -381,12 +381,12 @@ and
if !pid_oracle <> 0 then
(
Rif.write oracle_oc next_state.s.Prog.out_vars out ;
Rif.write oracle_oc next_state.s.Prog.in_vars input ;
Rif.write_outputs oracle_oc next_state.s.Prog.out_vars out ;
Rif.write_outputs oracle_oc next_state.s.Prog.in_vars input ;
flush oracle_oc;
if read_oracle () = "f" then
(
print_string "#oracle_violated\n";
Rif.write stdout "#oracle_violated\n";
flush stdout;
(try
Unix.kill (!pid_oracle) Sys.sigint ;
......@@ -407,14 +407,14 @@ and
let _ = snd (Unix.waitpid [Unix.WUNTRACED] !pid_oracle) in
()
);
print_string "\n#end\n";
Rif.write stdout "\n#end\n";
flush stdout
)
);;
try
print_string ("# Data generated by Lucky Version " ^ Version.str ^ " (" ^Version.sha^")\n\n");
Rif.write stdout ("# Data generated by Lucky Version " ^ Version.str ^ " (" ^Version.sha^")\n\n");
flush stdout
with _ ->
();;
......@@ -423,8 +423,8 @@ let _ =
try
main ();
with
| Error.Lucky err -> print_string (err ^ "\n"); flush stdout; exit 2
| Failure err -> print_string (err ^ "\n"); flush stdout; exit 2
| e -> print_string (((Printexc.to_string e) ^ "\n")); flush stdout
| Error.Lucky err -> Rif.write stdout (err ^ "\n"); flush stdout; exit 2
| Failure err -> Rif.write stdout (err ^ "\n"); flush stdout; exit 2
| e -> Rif.write stdout (((Printexc.to_string e) ^ "\n")); flush stdout
source/Lutin/main.ml
View file @ 0c651611
......@@ -153,11 +153,13 @@ let rec to_simu infile mnode = (
let seed = MainArg.seed () in
Random.init seed ;
output_string stderr "#The random engine was initialized with the seed ";
output_string stderr (string_of_int seed);
output_string stderr "\n";
flush stderr ;
(match (MainArg.riffile()) with
| None -> ()
| Some file -> Rif.open_rif_file file
);
Rif.write stderr ("# This is lutin Version " ^ Version.str ^ " (" ^Version.sha^")\n");
Rif.write stderr ("# The random engine was initialized with the seed " ^
(string_of_int seed) ^ "\n" );
if MainArg.compute_volume () then
Solver.set_fair_mode ()
else
......@@ -230,9 +232,9 @@ Utils.time_R "main_loop2";
Lucky.env_step (MainArg.draw_mode()) input state' generator
) with
| FGen.NoMoreFormula ->
print_string ("# " ^ (Prog.ctrl_state_to_string_long state.Prog.d.Prog.ctrl_state));
print_string "# No transition is labelled by a satisfiable formula.\n" ;
print_string "# The Lucky automata is blocked.\n";
Rif.write stdout ("# " ^ (Prog.ctrl_state_to_string_long state.Prog.d.Prog.ctrl_state));
Rif.write stdout "# No transition is labelled by a satisfiable formula.\n" ;
Rif.write stdout "# The Lucky automata is blocked.\n";
flush stdout;
if state.Prog.s.Prog.is_final state.Prog.d.Prog.ctrl_state
then exit 0
......@@ -240,9 +242,9 @@ Utils.time_R "main_loop2";
| FGen.NormalStop msg -> (
(if (msg = "vanish")
then
print_string "# Simulation ended normally.\n"
Rif.write stdout "# Simulation ended normally.\n"
else
print_string ("# Simulation ended with uncaught exception \""^msg^"\"\n")
Rif.write stdout ("# Simulation ended with uncaught exception \""^msg^"\"\n")
);
exit 0
)
......@@ -251,15 +253,15 @@ Utils.time_R "main_loop2";
(fun () -> Printf.fprintf stdout "#OUT SUBST LIST=%s\n" (Value.OfIdent.to_string ";" out));
Verbose.exe ~level:3
(fun () -> Printf.fprintf stdout "#LOC SUBST LIST=%s\n" (Value.OfIdent.to_string ";" loc));
print_string step_str;
print_string "#outs ";
Rif.write stdout next_state.Prog.s.Prog.out_vars out ;
Rif.write stdout step_str;
Rif.write stdout "#outs ";
Rif.write_outputs stdout next_state.Prog.s.Prog.out_vars out ;
if MainArg.show_locals () then (
print_string "\n#locs ";
Rif.write stdout next_state.Prog.s.Prog.loc_vars loc
Rif.write stdout "\n#locs ";
Rif.write_outputs stdout next_state.Prog.s.Prog.loc_vars loc
);
print_string "\n";
Rif.write stdout "\n";
(* Clean-up cached info that depend on pre or inputs *)
Formula_to_bdd.clear_step ();
......@@ -279,7 +281,7 @@ Utils.time_R "main_loop";
main_loop (t+1) next_state
) else (
(* HERE: oracle ? *)
print_string "\n#end\n";
Rif.write stdout "\n#end\n";
flush stdout;
)
)
......@@ -291,7 +293,7 @@ let main () = (
MainArg.parse () ;
let infile = MainArg.infile() in
let mnode = MainArg.main_node () in
let inchannel () =
let inchannel =
if (infile <> "") then
open_in infile
else
......@@ -303,11 +305,11 @@ let main () = (
raise (Global_error "no input file")
)
in
let mainprg = Parsers.read_lut (inchannel()) in
let mainprg = Parsers.read_lut inchannel in
let tlenv = CheckType.check_pack (MainArg.libs ()) mainprg in
let _ =
if MainArg.test_lex() then (
Parsers.lexemize_lut (inchannel())
Parsers.lexemize_lut inchannel
) else (
(* analyse syntaxique *)
if (MainArg.test_parse()) then (
......
source/Lutin/mainArg.ml
View file @ 0c651611
......@@ -147,6 +147,12 @@ let outpipe () = !_outpipe
let _outfile = ref None
let outfile () = !_outfile
(* riffile *)
let _riffile = ref None
let riffile () = !_riffile
(*
2 options tabs:
......@@ -203,6 +209,12 @@ let mkoptab () = (
(Arg.Unit(function _ -> _gen_mode := GenLuc ; ()))
["generate a lucky program"]
;
mkopt
["-rif"]
~arg:" <string>"
(Arg.String(function s -> _riffile := Some s))
["save the generated data in a file using the RIF format"]
;
mkopt
["-o"]
~arg:" <string>"
......
source/Lutin/mainArg.mli
View file @ 0c651611
......@@ -40,6 +40,9 @@ val libs : unit -> string list option
val outfile : unit -> string option
val outpipe : unit -> bool
(* Rif *)
val riffile : unit -> string option
val show_locals : unit -> bool
val see_all_options : unit -> bool
......
source/common/rif.ml
View file @ 0c651611
......@@ -20,8 +20,18 @@ let lexer = Genlex.make_lexer ["q"; "#"; "x"; "load_luc"; "#@"; "@#"]
let rif_pragmas = ["inputs"]
(* let rif_pragmas = ["outs";"outputs";"program";"inputs";"step";"reset"] *)
let write_rif = ref (fun str -> ())
let close_rif = ref (fun () -> ())
let (open_rif_file : string -> unit) =
fun file ->
let ic = open_out file in
write_rif := (fun str -> output_string ic str; flush ic);
close_rif := (fun () -> close_out ic)
let (close_rif_file : unit -> unit) =
!close_rif
type stream = Genlex.token Stream.t
......@@ -83,6 +93,7 @@ let rec (read : (string list -> Prog.state) -> in_channel -> Prog.state ->
if vntl = [] then (tbl, state) else
let line = input_line ic in
let stream = lexer (Stream.of_string line) in
!write_rif (line^"\n");
parse_rif_stream make_prog ic vntl stream tbl state
and (parse_rif_stream : (string list -> Prog.state) -> in_channel ->
......@@ -188,69 +199,72 @@ and (ignore_toks_until_end_of_pragmas : (string list -> Prog.state) ->
(lexer (Stream.of_string (input_line ic))) tbl state)
(*------------------------------------------------------------------------*)
(* exported *)
let (write : out_channel -> string -> unit) =
fun oc str ->
output_string oc str;
flush oc;
!write_rif str
(*------------------------------------------------------------------------*)
(* exported *)
let (write_interface : out_channel -> Prog.state -> bool -> unit) =
fun oc state print_locals ->
output_string oc"#inputs ";
List.iter
(fun v ->
output_string oc (
"\"" ^ (Var.name v) ^ "\":" ^ (Type.to_string2 (Var.typ v)) ^ " ")
)
state.s.in_vars;
output_string oc "\n";
output_string oc "#outputs "; flush stdout;
List.iter
(fun v ->
output_string oc(
"\"" ^ (Var.name v) ^ "\":" ^ (Type.to_string2 (Var.typ v)) ^ " ")
)
state.s.out_vars;
(* output_string oc "\n"; *)
if
print_locals
then
(
output_string oc "\n#locals ";
List.iter
(fun v ->
output_string oc (
"\"" ^ (Var.name v) ^ "\":" ^ (Type.to_string2 (Var.typ v)) ^ " ")
)
(fst (List.partition (fun v -> (Var.alias v) = None)
state.s.loc_vars ));
output_string oc "\n"
)
else
output_string oc "\n";
flush oc
let str =
(List.fold_left
(fun acc v ->
acc ^ "\"" ^ (Var.name v) ^ "\":" ^ (Type.to_string2 (Var.typ v)) ^ " ")
"#inputs "
state.s.in_vars) ^
"\n#outputs " ^
(List.fold_left
(fun acc v ->
acc ^ "\"" ^ (Var.name v) ^ "\":" ^ (Type.to_string2 (Var.typ v)) ^ " ")
""
state.s.out_vars) ^
(if print_locals then
((List.fold_left
(fun acc v ->
acc^"\"" ^ (Var.name v) ^ "\":" ^ (Type.to_string2 (Var.typ v)) ^ " ")
"\n#locals "
(fst (List.partition (fun v -> (Var.alias v) = None) state.s.loc_vars ))
) ^ "\n")
else
"\n")
in
write oc str
(*------------------------------------------------------------------------*)
(* exported *)
let (write : out_channel -> Exp.var list -> Value.OfIdent.t -> unit) =
let (write_outputs : out_channel -> Exp.var list -> Value.OfIdent.t -> unit) =
fun oc vntl sl ->
List.iter
(fun v ->
if (Var.alias v) <> None
then
(*
Do not show aliased var. Should I?
nb: anyway, they do not appear in [sl]
*)
()
else
(* let _ = assert (List.mem_assoc (Var.name v) sl) in *)
(* print_string ((Var.name v) ^ ":"); *)
try
(* Value.print oc (List.assoc (Var.name v) sl) *)
Value.print oc (Value.OfIdent.get sl (Var.name v))
with Not_found -> assert false
)
vntl
let str =
List.fold_left
(fun acc v ->
acc^ (if (Var.alias v) <> None
then
(*
Do not show aliased var. Should I?
nb: anyway, they do not appear in [sl]
*)
""
else
(* let _ = assert (List.mem_assoc (Var.name v) sl) in *)
(* print_string ((Var.name v) ^ ":"); *)
try
(* Value.print oc (List.assoc (Var.name v) sl) *)
Value.to_string (Value.OfIdent.get sl (Var.name v))
with Not_found -> assert false
)
)
""
vntl
in
write oc str
source/common/rif.mli
View file @ 0c651611
......@@ -11,6 +11,11 @@
(** RIF (Reactive Input Format) utilities *)
(** [open_rif_file f] will record *all* the data that are read/write
on the in_channel/out_channel into the f file. *)
val open_rif_file : string -> unit
(** Reads from stdin the inputs
The first parameter is used to dynamically change the env.
......@@ -21,8 +26,11 @@ val read : (string list -> Prog.state) -> in_channel ->
Prog.state -> Var.env_in * Prog.state
(** [write oc outputs ] writes the Lucky outputs *)
val write : out_channel -> Exp.var list -> Value.OfIdent.t -> unit
val write : out_channel -> string -> unit
(** [write_outputs oc outputs ] writes the Lucky outputs *)
val write_outputs : out_channel -> Exp.var list -> Value.OfIdent.t -> unit
(** writes the input and output var names and types *)
val write_interface : out_channel -> Prog.state -> bool -> unit
Supports Markdown
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