Skip to content

GitLab

Commit 79a03e8f authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Add a -boot option that force lutin to generate its first step without reading inputs. 

Also, -rif now points to -quiet (so that it has the same meaning as for ecexe),
and the previous -rif is obtained via -o.
parent 1ecf703d
Hide whitespace changes
Inline Side-by-side
examples/lutin/socket-from-c/call_foo_via_socket.c
View file @ 79a03e8f
......@@ -18,7 +18,7 @@
#include <string.h>
#endif
// Demonstrate the use of a ocaml programs that calls the lutin interpreter via sockets.
// Demonstrate the use of a C program that calls the lutin interpreter via sockets.
#define MAX_BUFF_SIZE 256
......
source/Lutin/main.ml
View file @ 79a03e8f
......@@ -122,7 +122,7 @@ let gnuplot_oc = ref None
let rec to_simu oc infile mnode opt = (
(* Parse and build the internal structure *)
let (zelutprog, zeprog) = LutProg.make ~libs:(MainArg.libs opt) infile mnode in
(* zelutprog is necessary for extracting initial data store *)
(* zelutprog is necessary for extracting initial data store *)
let state0 = LutProg.get_init_state zelutprog zeprog in
let init_state_dyn = { state0.Prog.d with Prog.verbose = Verbose.level () } in
let init_state = { state0 with Prog.d = init_state_dyn } in
......@@ -135,33 +135,31 @@ let rec to_simu oc infile mnode opt = (
Version.str Version.sha seed
in
let noo = not (MainArg.only_outputs opt) in
Random.init seed;
Random.init seed;
if MainArg.compute_volume opt then Solver.set_fair_mode () else Solver.set_efficient_mode ();
!Solver.init_snt ();
if noo then (
Rif.write oc msg;
Rif.write_interface oc init_state.Prog.s.Prog.in_vars init_state.Prog.s.Prog.out_vars loc None;
Rif.flush oc
);
let next_state = init_state in
let lut_memories =
if MainArg.load_mem opt then (
output_string oc "#lutin_outputs_memories ";
Rif.read stdin (if noo then Some oc else None) init_state.Prog.s.Prog.out_vars)
else
Value.OfIdent.empty
in
(* first main_loop : no pre context *)
main_loop oc opt 1 next_state lut_memories
if MainArg.compute_volume opt then Solver.set_fair_mode () else Solver.set_efficient_mode ();
!Solver.init_snt ();
Rif.write oc msg;
Rif.write_interface oc init_state.Prog.s.Prog.in_vars init_state.Prog.s.Prog.out_vars loc None;
Rif.flush oc;
let next_state = init_state in
let lut_memories =
if MainArg.load_mem opt then (
output_string oc "#lutin_outputs_memories ";
Rif.read stdin (if noo then Some oc else None) init_state.Prog.s.Prog.out_vars)
else
Value.OfIdent.empty
in
(* first main_loop : no pre context *)
main_loop oc opt 1 next_state lut_memories
)
and main_loop oc opt 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 ctrl_state=%s\n" csnme;
);
let csnme = (Prog.ctrl_state_to_string_long state.Prog.d.Prog.ctrl_state) in
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 oc opt t state pre_lut_output
......@@ -176,65 +174,65 @@ and main_loop_core oc opt t state pre_lut_output = (
in
let noo = not (MainArg.only_outputs opt) in
let _ = if noo then Rif.write oc step_str in
let lut_input = Rif.read stdin (if noo then Some oc else None) state.Prog.s.Prog.in_vars in
let lut_input = if t=1 && (boot opt) then Value.OfIdent.empty else
Rif.read stdin (if noo then Some oc else None) state.Prog.s.Prog.in_vars in
let generator = LucFGen.get lut_input state in
(*
Call Lucky explorer/solver
env_step : step_mode -> Var.env_in -> Prog.state -> FGen.t list -> Prog.state * solution
where type solution = Var.env_out * Var.env_loc
*)
(*
Call Lucky explorer/solver
env_step : step_mode -> Var.env_in -> Prog.state -> FGen.t list -> Prog.state * solution
where type solution = Var.env_out * Var.env_loc
*)
let (next_state, (lut_output, loc)) = try (
Lucky.env_step (MainArg.step_mode opt) lut_input state generator
) with
| FGen.NoMoreFormula ->
Rif.write oc ("# " ^ (Prog.ctrl_state_to_string_long state.Prog.d.Prog.ctrl_state));
Rif.write oc "# No transition is labelled by a satisfiable formula.\n" ;
Rif.write oc "# The Lucky automata is blocked.\n";
Rif.flush oc;
if state.Prog.s.Prog.is_final state.Prog.d.Prog.ctrl_state
then exit 0
else exit 2
Rif.write oc ("# " ^ (Prog.ctrl_state_to_string_long state.Prog.d.Prog.ctrl_state));
Rif.write oc "# No transition is labelled by a satisfiable formula.\n" ;
Rif.write oc "# The Lutin program is blocked.\n";
Rif.flush oc;
if state.Prog.s.Prog.is_final state.Prog.d.Prog.ctrl_state
then exit 0
else exit 2
| FGen.NormalStop msg -> (
(if (msg = "vanish")
then Rif.write oc "# Simulation ended normally.\n"
else Rif.write oc ("# Simulation ended with uncaught exception \""^msg^"\"\n")
);
Rif.flush oc;
exit 0
)
(if (msg = "vanish")
then Rif.write oc "# Simulation ended normally.\n"
else Rif.write oc ("# Simulation ended with uncaught exception \""^msg^"\"\n")
);
Rif.flush oc;
exit 0
)
in
Verbose.exe ~level:3
(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 noo then Rif.write oc " #outs ";
Rif.write_outputs oc next_state.Prog.s.Prog.out_vars lut_output;
Verbose.exe ~level:3
(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 noo then Rif.write oc " #outs ";
Rif.write_outputs oc next_state.Prog.s.Prog.out_vars lut_output;
if noo && MainArg.show_locals opt then (
Rif.write oc "\n#locs ";
Rif.write_outputs oc next_state.Prog.s.Prog.loc_vars loc;
);
if noo && MainArg.show_locals opt then (
Rif.write oc "\n#locs ";
Rif.write_outputs oc next_state.Prog.s.Prog.loc_vars loc;
);
Rif.write oc "\n";
Rif.flush oc;
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 ();
Formula_to_bdd.clear_step ();
!Solver.clear_snt ();
match MainArg.max_steps opt with
| None -> main_loop oc opt (t+1) next_state lut_output
| Some max -> (
if (t < max) then (
match MainArg.max_steps opt with
| None -> main_loop oc opt (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 opt(t+1) next_state lut_output
) else (
if noo then (Rif.write oc "\n#end\n"; Rif.flush oc)
)
)
main_loop oc opt(t+1) next_state lut_output
) else (
if noo then (Rif.write oc "\n#end\n"; Rif.flush oc)
)
)
)
let dbgexe = Verbose.get_flag "LutExe"
......@@ -256,7 +254,7 @@ let to_exe oc infile mnode opt = (
let noo = not (MainArg.only_outputs opt) in
let rec do_step cpt ctrl ins pres = (
(* Clean-up cached info that depend on pre or inputs *)
(* Clean-up cached info that depend on pre or inputs *)
Formula_to_bdd.clear_step ();
!Solver.clear_snt ();
......@@ -272,7 +270,7 @@ let to_exe oc infile mnode opt = (
| LutExe.SomeBehavior (b, bg') -> (
match b with
| LutExe.Goto (zeguard, ctrl') -> (
(* THIS IS THE NORMAL BEHAVIOR *)
(* THIS IS THE NORMAL BEHAVIOR *)
Event.incr_nb ();
let (outs, locs) = try LutExe.find_one_sol exe zeguard
with Not_found -> assert false
......@@ -330,50 +328,50 @@ let to_exe oc infile mnode opt = (
Event.incr_nb ();
do_step (cpt+1) ctrl' ins' pres'
)
)
| LutExe.Raise x -> (
Rif.write oc ("\n#end. Simulation ended with uncaught user exception \""^x^"\"\n");
Rif.flush oc;
exit 2
)
| LutExe.Vanish -> (
if noo then (
Rif.write oc "\n#end. Simulation ended normally.\n";
Rif.flush oc
);
exit 0
)
)
| LutExe.Raise x -> (
Rif.write oc ("\n#end. Simulation ended with uncaught user exception \""^x^"\"\n");
Rif.flush oc;
exit 2
)
| LutExe.Vanish -> (
if noo then (
Rif.write oc "\n#end. Simulation ended normally.\n";
Rif.flush oc
);
exit 0
)
)
)
in
let seed = MainArg.seed opt in
)
in
let seed = MainArg.seed opt in
let msg =
Printf.sprintf
"# This is lutin Version %s (%s)\n# The random engine was initialized with the seed %d\n"
Version.str Version.sha seed
in
Random.init seed;
if noo then (
let msg =
Printf.sprintf
"# This is lutin Version %s (%s)\n# The random engine was initialized with the seed %d\n"
Version.str Version.sha seed
in
Random.init seed;
Rif.write oc msg;
Rif.write_interface oc in_vars out_vars
(if (MainArg.show_locals opt) then Some loc_vars else None) None;
Rif.flush oc
);
Rif.flush oc;
(* prepare first step *)
Verbose.put "#Main.to_exe: prepare first step\n";
let ctrl = LutExe.get_init_state exe in
let cpt = 1 in
let step_str = Printf.sprintf "#step %d\n" cpt in
if noo then (
Rif.write oc step_str;
Rif.flush oc
);
let ins = Rif.read stdin (if noo then Some oc else None) in_vars in
(* HERE: init input/output pres *)
let pres = LutExe.get_init_pres exe in
do_step cpt ctrl ins pres
(* prepare first step *)
Verbose.put "#Main.to_exe: prepare first step\n";
let ctrl = LutExe.get_init_state exe in
let cpt = 1 in
let step_str = Printf.sprintf "#step %d\n" cpt in
if noo then (
Rif.write oc step_str;
Rif.flush oc
);
let ins = if (boot opt) then Value.OfIdent.empty else
Rif.read stdin (if noo then Some oc else None) in_vars
in
(* HERE: init input/output pres *)
let pres = LutExe.get_init_pres exe in
do_step cpt ctrl ins pres
)
(* TEST
......
source/Lutin/mainArg.ml
View file @ 79a03e8f
......@@ -2,7 +2,7 @@ open Version
open Arg
let version =
Printf.sprintf "lang: %s.%s, tool: %s (%s)"
Printf.sprintf "lang: %s.%s, tool: %s (%s)\n"
LutVersion.number
LutVersion.release
Version.str
......@@ -43,6 +43,7 @@ type t = {
mutable _only_outputs: bool;
mutable _call_gnuplot: bool;
mutable _run:bool;
mutable _boot:bool;
}
let (make_opt : unit -> t) =
......@@ -76,6 +77,7 @@ let (make_opt : unit -> t) =
_only_outputs = false;
_call_gnuplot = false;
_run=true;
_boot=false;
}
......@@ -122,6 +124,7 @@ let set_step_mode opt sm = opt._step_mode <- sm
let compute_volume opt = opt._compute_volume
let set_compute_volume opt b = opt._compute_volume <- b
let run opt = opt._run
let boot opt = opt._boot
let pspec os opt (c, ml) = (
......@@ -152,8 +155,6 @@ let help opt ()= (
)
let full_usage os opt = (
Printf.fprintf os "%s\n" usage_msg;
let l = List.rev opt._user_man in
List.iter (pspec os opt) l;
let l = List.rev (opt._hidden_man) in
List.iter (pspec os opt) l
)
......@@ -203,22 +204,21 @@ let (mkopt : t -> string list -> ?hide:bool -> ?arg:string -> Arg.spec -> string
let (mkoptab : t -> unit) =
fun opt -> (
mkopt opt
["-m";"-main"]
["-n";"-m";"-node";"-main"]
~arg:" <string>"
(Arg.String(function s ->
Luc2c.option.Luc2c.main_node <- s;
opt._main_node <- s))
["Set the main node"]
;
mkopt opt
mkopt opt ~hide:true
["-check"]
(Arg.Unit(function _ -> opt._run<-false))
["check the program is correct and exit"]
;
mkopt opt
["-version"]
(Arg.Unit(function _ -> print_string version; exit 0))
["--version";"-version"]
(Arg.Unit(function _ -> print_string version; flush stdout;exit 0))
["Print the current version and exit"]
;
mkopt opt ~hide:true
......@@ -238,23 +238,23 @@ let (mkoptab : t -> unit) =
(Arg.Int(function i -> Verbose.set i))
["Set the verbose level"]
;
(* ---- COMPILE OPTIONS *)
mkopt opt
["-luc"]
(Arg.Unit(function _ -> opt._gen_mode <- GenLuc ; ()))
["Generate a lucky program"]
;
mkopt opt (* XXX Merge it with -luc !!! *)
["-o"]
~arg:" <string>"
(Arg.String(function s -> opt._outfile <- Some s))
["with -luc: write to specified file (default is infile_main.luc)"]
;
mkopt opt
["-os"]
(Arg.Unit(function s -> opt._outpipe <- true))
["with -luc: write to stdout"]
;
(* ---- COMPILE OPTIONS: broken...*)
(* mkopt opt *)
(* ["-luc"] *)
(* (Arg.Unit(function _ -> opt._gen_mode <- GenLuc ; ())) *)
(* ["Generate a lucky program"] *)
(* ; *)
(* mkopt opt (* XXX Merge it with -luc !!! *) *)
(* ["-o"] *)
(* ~arg:" <string>" *)
(* (Arg.String(function s -> opt._outfile <- Some s)) *)
(* ["with -luc: write to specified file (default is infile_main.luc)"] *)
(* ; *)
(* mkopt opt *)
(* ["-os"] *)
(* (Arg.Unit(function s -> opt._outpipe <- true)) *)
(* ["write to stdout"] *)
(* ; *)
mkopt opt
["-gnuplot";"-gp"]
(Arg.Unit(function s ->
......@@ -266,12 +266,12 @@ let (mkoptab : t -> unit) =
["call gnuplot-rif to display data (type 'a' in the gnuplot window to refresh it)."]
;
mkopt opt
["-quiet";"-q";"-only-outputs"]
["-rif";"-quiet";"-q";"-only-outputs"]
(Arg.Unit(function s -> opt._only_outputs <- true))
["display only outputs on stdout (no #step, #outs, etc.)"]
["display only outputs on stdout (i.e., behave as a rif input file)"]
;
mkopt opt
["-rif"]
["-o"]
~arg:" <string>"
(Arg.String(function s ->
let s = if not (Sys.file_exists s) then s else
......@@ -287,7 +287,7 @@ let (mkoptab : t -> unit) =
opt._riffile <- Some s;
Luc2c.option.Luc2c.rif <- Some s
))
["Save the generated data using the RIF format"]
["output file name (RIF)"]
;
mkopt opt
......@@ -306,7 +306,12 @@ let (mkoptab : t -> unit) =
["Set a seed for the pseudo-random generator"]
;
mkopt opt
["-l"; "--max-steps"]
["-boot"]
(Arg.Unit(function _ -> opt._boot<-true))
["Perform ther first step without reading inputs"]
;
mkopt opt
["--max-steps";"-l"]
~arg:" <int>"
(Arg.Int(function i -> opt._max_steps <- Some i ; ()))
["Set a maximum number of simulation steps to perform"]
......@@ -327,7 +332,7 @@ let (mkoptab : t -> unit) =
(Arg.Unit(function _ -> opt._step_mode <- Lucky.StepVertices))
["Draw among the vertices of the convex hull of solutions"]
;
mkopt opt
mkopt opt ~hide:true
["-fair"; "--compute-poly-volume"]
(Arg.Unit (fun () -> opt._compute_volume <- true))
[ "Compute polyhedron volume before drawing";
......@@ -347,7 +352,7 @@ let (mkoptab : t -> unit) =
];
(* ---- luc2c OPTIONS *)
mkopt opt
mkopt opt ~hide:true
["--2c-4c"]
(Arg.Unit(fun () ->
opt._gen_mode <- Cstubs;
......@@ -371,7 +376,7 @@ let (mkoptab : t -> unit) =
["to set the port number; meaningful only if --2c-4c-socks is used."]
;
mkopt opt
mkopt opt ~hide:true
["--2c-4lustre"]
~arg:" <string>"
(Arg.String(fun str ->
......@@ -380,7 +385,7 @@ let (mkoptab : t -> unit) =
Luc2c.option.Luc2c.calling_module_name <- str))
["Generate C code to be called from Lustre V4 "];
mkopt opt
mkopt opt ~hide:true
["--2c-4scade"]
~arg:" <string>"
(Arg.String(fun str ->
......@@ -405,7 +410,7 @@ let (mkoptab : t -> unit) =
Luc2c.option.Luc2c.calling_module_name <- str))
["Generate C and C++ code to be called from Alice"];
mkopt opt
mkopt opt ~hide:true
["--2c-output-dir"]
~arg:" <string>"
(Arg.String(fun str -> Luc2c.option.Luc2c.output_dir <- str))
......
source/Lutin/mainArg.mli
View file @ 79a03e8f
......@@ -27,6 +27,7 @@ val main_node : t -> string
val test_exe : t -> bool
val run : t -> bool
val boot : t -> bool
(* Simulation *)
val max_steps : t -> int option
......
source/lus2lic/lus2licRun.ml
View file @ 79a03e8f
(* Time-stamp: <modified the 29/11/2013 (at 12:56) by Erwan Jahier> *)
(*-----------------------------------------------------------------------
** Copyright (C) - Verimag.
*)
type vars = (string * string) list
......
source/lus2lic/socExec.ml
View file @ 79a03e8f
(* Time-stamp: <modified the 21/11/2013 (at 11:28) by Erwan Jahier> *)
(* Time-stamp: <modified the 29/11/2013 (at 15:26) by Erwan Jahier> *)
open Soc
open Data
......@@ -248,6 +248,7 @@ let (unexpand_profile : sl -> Soc.var list -> sl) =
(* Returns the (accumulated) result and the unused subst
(which should be empty at the top-level call) *)
match sl_todo, vl with
| [],_::_ -> sl_done,[] (* should not occur? *)
| _,[] -> sl_done, sl_todo
| s::sl, (_, (Bool| Int | Real))::vl -> aux (s::sl_done) sl vl
| (id,v)::sl, (_,Enum(n,el))::vl ->
......@@ -275,7 +276,6 @@ let (unexpand_profile : sl -> Soc.var list -> sl) =
| _, (vn,Extern id)::_ -> assert false (* finish me! *)
| _, (vn,Alpha _ )::_ -> assert false (* should not occur *)
| [],_::_ -> assert false (* should not occur *)
and (aux_field : sl * (ident * Data.v) list -> ident * Data.t -> sl * (ident * Data.v) list ) =
fun (sl_todo, fl) (fn, t) ->
......
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