Skip to content

GitLab

Commit 9b3e5fc8 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

A temporary snapshot of the situation, where lutin works in combination of Alices. 

Most of the change will be undone latter, because my plan is to use lurettetop
instead, and therefore to remove all those warts in Lutin. However, as this is
currently working, I take a snapshot before breaking everything.

nb : non-reg test don't event pass.
parent ccb14ac1
Hide whitespace changes
Inline Side-by-side
examples/lutin/oracle/Makefile
View file @ 9b3e5fc8
......@@ -7,10 +7,10 @@ ifeq ($(HOSTTYPE),cross-win32)
EXE=.exe
endif
LUTIN=../../../$(HOSTTYPE)/bin/lutin$(EXE) -seed 1
LUTIN=../../../$(HOSTTYPE)/bin/lutin$(EXE) -seed 1 -boot --load-mem
test : test1 test2
test : test1 test2 clear
not_a_sauna.ec: heater_control.lus
lus2lic -n not_a_sauna -ec $< -o $@
......@@ -19,17 +19,22 @@ not_a_sauna.ec: heater_control.lus
test1 : not_a_sauna.ec
echo -e "t\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\n" | \
$(LUTIN) env.lut -main main --oracle-ec $< | sed -e "s/^M//" | grep -v "This is lutin" > test1.rif
rm -f test1.rif
echo -e "0.0 0.0 0.0 0.0\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\nt\n" | \
$(LUTIN) env.lut -main main --oracle-ec $< -rif test1.rif || true
cat test1.rif | sed -e "s/^M//" | grep -v "This is lutin" > test1.rif
rm -f test1.res && diff -B -u -i -w test1.rif.exp test1.rif > test1.res
test2 : not_a_sauna.ec
echo -e "t\nf\nt\nf\nt\nf\nt\nf\nt\nf\nt\nf\nt\nf\nt\nf\nt\nf\nt\nf\nt\n" | \
rm -f test2.rif
echo -e "0.0 0.0 0.0 0.0\nt\nf\nt\nf\nt\nf\nt\nf\nt\nf\nt\nf\nt\nf\nt\nf\nt\nf\nt\nf\nt\n" | \
$(LUTIN) env.lut -main main --oracle-ec $< | sed -e "s/^M//" | grep -v "This is lutin" > test2.rif
rm -f test2.res && diff -B -u -i -w test2.rif.exp test2.rif > test2.res
[ ! -s test2.res ] && make clean
clear:
[ ! -s test1.res ] && [ ! -s test2.res ] && make clean
utest1:
......
examples/lutin/oracle/test1.rif.exp
View file @ 9b3e5fc8
# The random engine was initialized with the seed 1
#inputs "Heat_on":bool
#outputs "T":real "T1":real "T2":real "T3":real
#inputs "T":real "T1":real "T2":real "T3":real
#outputs "Heat_on":bool
#lutin_outputs_memories 0.0 0.0 0.0 0.0
#step 1
#outs 6.03 5.86 4.58 6.22
0.00 0.00 0.00 0.00 #outs t
#step 2
#outs 6.31 7.29 7.71 5.73
6.03 5.86 4.58 6.22 #outs t
#step 3
#outs 6.71 6.01 5.79 7.50
6.31 7.29 7.71 5.73 #outs t
#step 4
#outs 7.11 5.73 8.09 8.23
6.71 6.01 5.79 7.50 #outs t
#step 5
#outs 7.52 6.25 6.30 8.65
7.11 5.73 8.09 8.23 #outs t
#step 6
#outs 7.80 8.42 7.13 7.04
7.52 6.25 6.30 8.65 #outs t
#step 7
#outs 8.17 8.75 6.81 9.53
7.80 8.42 7.13 7.04 #outs t
#step 8
#outs 8.55 7.70 8.05 9.66
8.17 8.75 6.81 9.53 #outs t
#step 9
#outs 8.72 8.72 7.34 10.10
8.55 7.70 8.05 9.66 #outs t
#step 10
#outs 9.17 10.41 10.60 7.75
8.72 8.72 7.34 10.10 #outs t
#step 11
#outs 9.39 9.31 9.58 10.05
9.17 10.41 10.60 7.75 #outs t
#step 12
#outs 9.51 8.50 10.52 8.38
9.39 9.31 9.58 10.05 #outs t
#step 13
#outs 9.99 8.52 11.48 10.11
9.51 8.50 10.52 8.38 #outs t
#step 14
#outs 10.30 9.87 11.27 9.45
# The oracle returned false at step 14
9.99 8.52 11.48 10.11 #outs t
#step 15
10.30 9.87 11.27 9.45 #outs t# The oracle returned false at step 15
#step 16
10.49 11.92 10.86 9.05 #outs t
examples/lutin/oracle/test2.rif.exp
View file @ 9b3e5fc8
# The random engine was initialized with the seed 1
#inputs "Heat_on":bool
#outputs "T":real "T1":real "T2":real "T3":real
#inputs "T":real "T1":real "T2":real "T3":real
#outputs "Heat_on":bool
#lutin_outputs_memories 0.0 0.0 0.0 0.0
#step 1
#outs 6.03 5.86 4.58 6.22
0.00 0.00 0.00 0.00 #outs t
#step 2
#outs 5.81 6.79 7.21 5.23
6.03 5.86 4.58 6.22 #outs f
#step 3
#outs 6.21 5.51 5.29 7.00
6.31 7.29 7.71 5.73 #outs t
#step 4
#outs 6.11 4.73 7.09 7.23
6.21 5.51 5.29 7.00 #outs f
#step 5
#outs 6.52 5.25 5.30 7.65
6.61 5.23 7.59 7.73 #outs t
#step 6
#outs 6.30 6.92 5.63 5.54
6.52 5.25 5.30 7.65 #outs f
#step 7
#outs 6.67 7.25 5.31 8.03
6.80 7.42 6.13 6.04 #outs t
#step 8
#outs 6.55 5.70 6.05 7.66
6.67 7.25 5.31 8.03 #outs f
#step 9
#outs 6.72 6.72 5.34 8.10
7.05 6.20 6.55 8.16 #outs t
#step 10
#outs 6.67 7.91 8.10 5.25
6.72 6.72 5.34 8.10 #outs f
#step 11
#outs 6.89 6.81 7.08 7.55
7.17 8.41 8.60 5.75 #outs t
#step 12
#outs 6.51 5.50 7.52 5.38
6.89 6.81 7.08 7.55 #outs f
#step 13
#outs 6.99 5.52 8.48 7.11
7.01 6.00 8.02 5.88 #outs t
#step 14
#outs 6.80 6.37 7.77 5.95
6.99 5.52 8.48 7.11 #outs f
#step 15
#outs 6.99 8.42 7.36 5.55
7.30 6.87 8.27 6.45 #outs t
#step 16
#outs 6.52 6.22 6.09 5.42
6.99 8.42 7.36 5.55 #outs f
#step 17
#outs 6.71 6.01 7.06 7.22
7.02 6.72 6.59 5.92 #outs t
#step 18
#outs 6.23 7.71 5.62 4.76
6.71 6.01 7.06 7.22 #outs f
#step 19
#outs 6.45 6.54 7.41 5.18
6.73 8.21 6.12 5.26 #outs t
#step 20
#outs 6.40 5.12 5.10 7.62
6.45 6.54 7.41 5.18 #outs f
#step 21
#outs 6.89 7.39 8.37 6.39
6.90 5.62 5.60 8.12 #outs t
#step 22
The coverage file not_a_sauna.cov has been generated
6.89 7.39 8.37 6.39 #outs
The coverage rate is 100.0%
The coverage file not_a_sauna.cov has been updated/generated
source/Lucky/luc2c.ml
View file @ 9b3e5fc8
......@@ -7,7 +7,7 @@
** File: luc2c.ml
** Author: jahier@imag.fr
**
** Generates C files to call Lucky from C.
** Generates C files to call Lucky, Lutin, or Lurette from C.
**
*)
......@@ -27,6 +27,7 @@ type optionT = {
mutable env : string list;
mutable main_node : string option; (* Main node *)
mutable boot : bool;
mutable load_mem : bool;
mutable pp : string option; (* Pre-processor *)
mutable output : string option;
mutable rif : string option;
......@@ -38,6 +39,7 @@ type optionT = {
mutable use_sockets : bool;
mutable sock_addr : string;
mutable output_dir : string;
mutable oracle_ec : string option;
}
......@@ -46,6 +48,7 @@ let (option : optionT) = {
main_node = None;
pp = None;
boot = false;
load_mem = false;
output = None;
rif = None;
gen_mode = Nop;
......@@ -55,7 +58,8 @@ let (option : optionT) = {
seed = None;
precision = None;
sock_addr = "127.0.0.1";
output_dir = Filename.current_dir_name
output_dir = Filename.current_dir_name;
oracle_ec = None
}
......@@ -273,8 +277,11 @@ typedef float _float;
putln ("struct C_" ^ fn ^ ";");
putln ("struct _" ^ fn ^ "_ctx");
putln " {";
putln " void* client_data;";
putln " //INPUTS";
put "
void* client_data;
int step_number;
//INPUTS
";
List.iter put_var_decl_in_struct in_vars;
putln " //OUTPUTS";
List.iter put_var_decl_in_struct out_vars;
......@@ -381,6 +388,7 @@ let put_socket_func put fn in_vars out_vars loc_vars =
#include <stdio.h>
#include <sys/types.h>
#include <signal.h>
#include <locale.h>
#ifdef _WINSOCK
#include <windows.h>
#include <process.h>
......@@ -435,13 +443,15 @@ launch the lutin interpreter and init socket stuff
char *sock_addr = \""^option.sock_addr^"\";
const char *args[] = {
#ifdef _WIN32
\"call-via-socket.exe\", sock_addr, portno_str, \""^(String.escaped lutin)^"\",
\"call-via-socket.exe\", -addr, sock_addr, -port, portno_str, -server, \""^(String.escaped lutin)^"\",
#else
\"call-via-socket\", sock_addr, portno_str, \""^(String.escaped lutin)^"\",
\"call-via-socket\", -addr, sock_addr, -port, portno_str, -server, \""^(String.escaped lutin)^"\",
#endif
" ^ (match option.main_node with None -> "" | Some node -> ("\"-main\", \""^node^"\", "))
^ (match option.seed with None -> "" | Some i -> ("\"-seed\", \""^(string_of_int i)^"\", "))
^ (if option.boot then "-boot, " else "")
^ (if option.boot then "\"-boot\", " else "")
^ (if option.load_mem then "\"--load-mem\", " else "")
^ (match option.oracle_ec with Some f -> "\"--oracle-ec\", \"" ^ (String.escaped f) ^ "\", " | None -> "")
^ (match option.precision with None -> "" | Some i -> ("\"-precision\", \""^(string_of_int i)^"\", "))
^" \""^ (String.escaped lut_file) ^"\", \"-rif\",\""^(
match option.rif with
......@@ -458,7 +468,9 @@ launch the lutin interpreter and init socket stuff
ctx = malloc(sizeof("^ fn ^ "_ctx));
ctx->client_data = cdata;
ctx->step_number = 0;
setlocale(LC_ALL, \"English\");
sockfd = socket(AF_INET, SOCK_STREAM, 0);
if (sockfd < 0) printf(\"Error: opening socket\");
serv_addr.sin_family = AF_INET;
......@@ -528,29 +540,50 @@ in
let char_decl =
(String.concat "" (List.rev (List.fold_left decl_char [] out_vars)))
in
(if !cpt = 0 then "" else char_decl) ^ "
sprintf(ctx->buff, \""^(
let var_to_adress var ="ctx->_" ^ (Var.name var) in
(if !cpt = 0 then "" else char_decl) ^
(if option.load_mem then " if (ctx->step_number == 0) {
sprintf(ctx->buff, \""^(
List.fold_left
(fun acc var -> acc ^ (var_to_format_print var) ^ " ")
""
out_vars) ^"\\n\", "
^
(List.fold_left
(fun acc var -> acc ^ ", "^ (var_to_adress var))
(var_to_adress (List.hd out_vars))
((List.tl out_vars)))
^
");
dbg_printf(\"\\n\\n ---- Sending lutin memories: '%s'\\n\",ctx->buff);
send(ctx->sock, ctx->buff, (int) strlen(ctx->buff),0);
}; " else "") ^
(if option.boot then " if (ctx->step_number > 0) {
" else "
") ^
(if in_vars = [] then "" else
"sprintf(ctx->buff, \""^(
List.fold_left
(fun acc var -> acc ^ (var_to_format_print var) ^ " ")
""
in_vars) ^"\\n\", "
^
let var_to_adress var ="ctx->_" ^ (Var.name var) in
(List.fold_left
(List.fold_left
(fun acc var -> acc ^ ", "^ (var_to_adress var))
(var_to_adress (List.hd in_vars))
((List.tl in_vars)))
^
");
dbg_printf(\"\\n\\n ---- A new Step begins. Sending to sock: '%s'\\n\",ctx->buff);
send(ctx->sock, ctx->buff, (int) strlen(ctx->buff),0);
dbg_printf(\"\\n\\n ---- A new Step begins. Sending to sock: '%s'\\n\",ctx->buff);
send(ctx->sock, ctx->buff, (int) strlen(ctx->buff),0);
")^ (if option.boot then "} " else "") ^ "
dbg_printf(\"reading inputs\\n\");
rc = 0;
rc = recv(ctx->sock, ctx->buff, MAX_BUFF_SIZE, 0);
if (rc<0) { printf(\"Error: cannot read on socket\\n\"); exit(2); }
dbg_printf(\"reading '%s'\\n\",ctx->buff);
sscanf(ctx->buff, \"#step %d #outs " ^
sscanf(ctx->buff, \"" ^
let cpt = ref 0 in
let var_to_adress var =
if (Var.typ var= Type.BoolT) then (
......@@ -558,10 +591,19 @@ in
else
"&(ctx->_"^ (Var.name var)^")"
in
let scan_format =
(List.fold_left
(fun acc var -> acc ^ " " ^ (var_to_format_scan var))
""
out_vars)^"\", &i,"
out_vars)
in
(if option.boot then
("\\n#step %d " ^ scan_format ^ " #outs ")
else
("#step %d #outs " ^ scan_format)
)
^ "\", &i,"
^
(List.fold_left
(fun acc var -> acc^", "^(var_to_adress var))
......@@ -587,7 +629,8 @@ in
(String.concat ""
(List.rev (List.fold_left copy_char_to_ctx [] out_vars)))
^ "
memset(ctx->buff, 0, rc);
memset(ctx->buff, 0, rc);
ctx->step_number = 1+ctx->step_number;
dbg_printf(\"----- step done\\n\");
}
......@@ -706,6 +749,7 @@ Dynamic allocation of an internal structure
putln " lucky_caml_init();";
putln (" ctx = malloc(sizeof("^ fn ^ "_ctx));");
putln " ctx->client_data = cdata;";
putln " ctx->step_number = 0;";
put (" ctx->lp = make(" );
put (match option.pp with | None -> "\"\"" | Some pp -> ("\""^pp^"\""));
put (", \"");
......@@ -743,7 +787,10 @@ Step procedure
(Var.name var) ^ "\"));");
)
out_vars;
putln "}";
putln "
ctx->step_number = 1+ctx->step_number;
}
";
putln "
/*--------
......
source/Lucky/luc2c.mli
View file @ 9b3e5fc8
......@@ -23,6 +23,7 @@ type optionT = {
mutable env : string list; (* lutin/lucky files *)
mutable main_node : string option; (* Main node *)
mutable boot : bool;
mutable load_mem : bool;
mutable pp : string option; (* Pre-processor *)
mutable output : string option; (* A string used in generated files name *)
mutable rif : string option; (* Name of the rif file used to put generated data *)
......@@ -35,6 +36,7 @@ type optionT = {
instead of the interpreter embedded into the C libraries. *)
mutable sock_addr : string;
mutable output_dir : string;
mutable oracle_ec : string option;
}
val option : optionT
......
source/Lucky/luc4ocaml.ml
View file @ 9b3e5fc8
......@@ -159,7 +159,7 @@ let (string_of_subst_list : subst list -> string) =
let (rif_read : in_channel -> state -> inputs) =
fun ic st ->
let i = Rif.read ic st.s.in_vars in
let i = Rif.read ic None st.s.in_vars in
map2list i
......
source/Lucky/luc_exe.ml
View file @ 9b3e5fc8
......@@ -315,7 +315,7 @@ and
Rif.write stdout step_str;
)
in
let input = Rif.read stdin state.s.in_vars in
let input = Rif.read stdin (Some stdout) state.s.in_vars in
(* let input_list = Hashtbl.fold (fun vn x acc -> (vn,x)::acc) input [] in *)
let ral = LucFGen.get input state in
let (next_state, (out, loc)) =
......
source/Lutin/main.ml
View file @ 9b3e5fc8
......@@ -125,11 +125,11 @@ 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 inputs outputs t = (
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 inputs outputs in
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))
......@@ -138,63 +138,74 @@ let check_oracle inputs outputs t = (
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 true)::tail ->
cov := Coverage.update_cov tail !cov;
| (_, Rif_base.B false)::tail ->
let msg = Coverage.dump_oracle_io oracle_inputs tail !cov in
Printf.printf "# The oracle returned false at step %i\n" t;
Printf.eprintf "The oracle returned false at step %i\n%s" t msg;
kill_oracle();
flush stderr;
flush stdout;
exit 2
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 infile mnode = (
let rec to_simu oc infile mnode = (
(* Parse and build the internal structure *)
let (zelutprog, zeprog) = LutProg.make ~libs:(MainArg.libs()) infile mnode in
(* 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
let loc = if (MainArg.show_locals ()) then Some init_state.Prog.s.Prog.loc_vars else None in
let seed = MainArg.seed () in
Random.init seed ;
(match (MainArg.riffile()) with
| None -> ()
| Some file -> Rif.open_rif_file file
);
Rif.write stdout ("# This is lutin Version " ^ Version.str ^ " (" ^Version.sha^")\n");
Rif.write stdout ("# The random engine was initialized with the seed " ^
(string_of_int seed) ^ "\n" );
if MainArg.compute_volume () then
Solver.set_fair_mode ()
else
Solver.set_efficient_mode ();
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;
if MainArg.compute_volume () then Solver.set_fair_mode () else Solver.set_efficient_mode ();
!Solver.init_snt ();
Rif.write_interface stdout init_state.Prog.s.Prog.in_vars init_state.Prog.s.Prog.out_vars
(if (MainArg.show_locals ()) then Some init_state.Prog.s.Prog.loc_vars else None);
Rif.flush stdout;
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.flush oc;
let next_state = init_state in
let lut_memories =
if MainArg.load_mem () then (
output_string oc "#lutin_outputs_memories ";
Rif.read stdin (Some oc) init_state.Prog.s.Prog.out_vars)
else
Value.OfIdent.empty
in
(* first main_loop : no pre context *)
main_loop ~boot:(MainArg.boot()) 1 next_state;
Rif.flush stdout
main_loop ~boot:(MainArg.boot()) oc (if MainArg.boot() then 0 else 1) next_state lut_memories lut_memories
)
and main_loop ?(boot=false) t state = (
and main_loop ?(boot=false) oc t state pre_lut_output pre_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;
);
if state.Prog.s.Prog.is_final state.Prog.d.Prog.ctrl_state then (
) else main_loop_core ~boot:boot t state
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
)
and main_loop_core ?(boot=false) t state = (
and main_loop_core ?(boot=false) oc t state pre_lut_output pre_pre_lut_output = (
let step_str =
("#step " ^ (string_of_int t)) ^
(if state.Prog.d.Prog.verbose >= 1
......@@ -202,80 +213,99 @@ and main_loop_core ?(boot=false) t state = (
else ""
) ^ "\n"
in
Rif.write stdout step_str;
(* IF BOOT -> don't ask for input *)
let input =
if boot then Value.OfIdent.empty
else Rif.read stdin state.Prog.s.Prog.in_vars
in
Verbose.put "#Main.main_loop call LucFGen.get\n";
let generator = LucFGen.get 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
*)
let (next_state, (out, loc)) = try (
Verbose.put "#Main.main_loop call Lucky.env_step\n";
Lucky.env_step (MainArg.draw_mode()) input state generator
) with
| FGen.NoMoreFormula ->
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";
Rif.flush stdout;
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 stdout "# Simulation ended normally.\n"
else Rif.write stdout ("# Simulation ended with uncaught exception \""^msg^"\"\n")
);
Rif.flush stdout;
exit 0
)
in
Verbose.exe ~level:3
(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));
Rif.write stdout "#outs ";
Rif.write_outputs stdout next_state.Prog.s.Prog.out_vars out ;
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
(* 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 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
*)
let (next_state, (lut_output, loc)) = try (
Lucky.env_step (MainArg.draw_mode()) 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
| FGen.NormalStop msg -> (
(if (msg = "vanish")