Commit 30964784 authored by Erwan Jahier's avatar Erwan Jahier

Implement a --luciole option that lauch luciole even if no input is missing.

This is very handy  to see inline what's going on.
parent 4b836d2e
......@@ -12,7 +12,7 @@ LURETTETOP=$(LTOP) \
test1:heater_control.ec heater_control$(EXE)
rm -f test1.rif0 .lurette_rc
$(LURETTETOP) -go --output test1.rif0 \
$(LURETTETOP) -go --output test1.rif0 \
-rp "sut:ec_exe:./heater_control.ec:" \
-rp "oracle:v4:heater_control.lus:not_a_sauna" \
-rp "oracle:v6:heater_control.lus:not_a_fridge" \
......@@ -43,7 +43,7 @@ test2:
# Calling the native step function via a cmxs
test3: heater_control.cmxs
rm -f test3.rif0 .lurette_rc
$(LURETTETOP) -go --output test3.rif0 \
$(LURETTETOP) --luciole -go --output test3.rif0 \
-rp "sut:ocaml:heater_control.cmxs:" \
-rp "env:lutin:degradable-sensors.lut:-m:main" && \
grep -v "lurette chronogram" test3.rif0 | \
......@@ -101,7 +101,7 @@ sut:
clean:
rm -rf *.h *.c *.ec *.log *~ .*~ *.o *rif0 *rif Data *.pp_luc *.plot *.gp heater_control not_a_sauna* *.cov
rm -rf *.h *.c *.ec *.log *~ .*~ *.o *rif0 *rif Data *.pp_luc *.plot *.gp heater_control not_a_sauna* *.cov *.cm* *.dro
......
......@@ -54,8 +54,8 @@ let (gen_makefile :string -> unit) =
^str^"_luciole.o "^str^".dro "^str^".h Makefile."^str);
print_string ("File Makefile." ^ str ^ " has been created. Launch \n");
print_string (" make -f Makefile." ^ str ^ "\n to run luciole\n");
ignore (Util.my_create_process "make" ["-f";("Makefile." ^ str)]);
close_out oc
close_out oc;
ignore (Util.my_create_process "make" ["-f";("Makefile." ^ str)])
(* exported *)
......
......@@ -27,10 +27,8 @@ let (check_compat : vars -> vars -> vars -> vars -> vars -> vars -> int * (vars
and missing_oracle_in = list_minus oracle_in (sut_out @env_out) in
let luciole_out = list_union missing_sut_in missing_env_in in
let luciole_in = list_minus (env_out@sut_out) luciole_out in
(* let luciole_in = [] in *)
(* let luciole_in = [] in *)
(* XXX use me! *)
let vars_to_string vars = String.concat "," (List.map (fun (n,t) -> n^":"^t) vars) in
if missing_sut_in <> [] then (
let missing_str = vars_to_string missing_sut_in in
......@@ -41,8 +39,8 @@ let (check_compat : vars -> vars -> vars -> vars -> vars -> vars -> int * (vars
Printf.printf "Some variables are missing in input of lutin: %s\n" missing_str
);
if luciole_out <> [] then (
Printf.printf "try with luciole!\n";
0, Some(luciole_in,luciole_out)
Printf.printf "try with luciole!\n";
0, Some(luciole_in,luciole_out)
)
else if missing_oracle_in <> [] then (
let missing_str = vars_to_string missing_oracle_in in
......@@ -50,9 +48,15 @@ let (check_compat : vars -> vars -> vars -> vars -> vars -> vars -> int * (vars
2,None
)
else (
Printf.printf "Variables are compatible.\n";
flush stdout;
0,None
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";
flush stdout;
2,None
) else (
Printf.eprintf "RP Variables are compatible.\n";
flush stderr;
0, if args.luciole_mode then Some(luciole_in, ["Step","bool"]) else None
)
)
......
......@@ -233,7 +233,7 @@ let (mkoptab : t -> unit) =
["with -luc: write to stdout"]
;
mkopt opt
["-only-outputs"]
["-quiet";"-only-outputs"]
(Arg.Unit(function s -> opt._only_outputs <- true))
["display only outputs on stdout (no #step, #outs, etc."]
;
......@@ -350,7 +350,7 @@ let (mkoptab : t -> unit) =
["Generate C code to be called from Scade "];
mkopt opt
["--2c-4luciole"]
["-luciole"; "--2c-4luciole"]
(Arg.Unit(fun _ ->
opt._gen_mode <- Cstubs;
Luc2c.option.Luc2c.gen_mode <- Luc2c.Luciole))
......
......@@ -99,6 +99,9 @@ $(LURETTE_RELEASE_NAME).tgz: strip
`which getsaonodes` \
`which lus2ec` \
`which ec2c` \
`which ecexe` \
`which simec` \
`which luciole` \
$(LURETTE_PATH)/$(HOSTTYPE)/bin/lurettetop_exe$(EXE) \
$(LURETTE_PATH)/$(HOSTTYPE)/bin/show_luc$(EXE) \
$(LURETTE_PATH)/$(HOSTTYPE)/bin/gen_fake_lucky$(EXE) \
......
......@@ -81,8 +81,6 @@ let (print_vn_str : (string * string) list -> unit) =
let sut_i_vntl = Sut.get_input_var_name_and_type ()
let sut_o_vntl = Sut.get_output_var_name_and_type ()
let oracle_i_vntl = Oracle.get_input_var_name_and_type ()
let oracle_o_vntl = Oracle.get_output_var_name_and_type ()
let arg_nb = (Array.length Sys.argv)
......@@ -143,58 +141,6 @@ let print_failure i o oo l t locals rif =
let soi = string_of_int
let check_oracle
(inputs:Value.OfIdent.t list)
(sut_outputs: Value.OfIdent.t list)
(locals: Value.OfIdent.t list)
(local_var_name_and_type_list: (string * string) list)
(memory: Value.OfIdent.t)
t rif state
= (
if options.oracle then (
(* Tries the oracle `n*p'^nth times *)
let (results: (bool * Value.OfIdent.t) list) =
List.map2
(fun x y -> Oracle.trie x y)
inputs
sut_outputs
in
let results, oracle_outputs = List.split results in
(* Aborts if at least one of the pairs (input, sut_output) breaks the oracle *)
if (List.mem false results) then (
(* print inputs and outputs of all wrong tuple *)
output_msg2 rif (
"\n*** An assertion of the oracle returned false at step "^(soi t)^
" with the following values:\n ");
let rec print_failures li lo loo ll lr = (
let i = List.hd li
and o = List.hd lo
and oo = List.hd loo
and l = List.hd ll
and r = List.hd lr
in
if (not r) then print_failure i o oo l t local_var_name_and_type_list rif
else print_failures (List.tl li) (List.tl lo) (List.tl loo) (List.tl ll) (List.tl lr)
) in
print_failures inputs sut_outputs oracle_outputs locals results ;
if memory <> Value.OfIdent.empty then (
output_msg "\n* Memories:\n" ;
Value.OfIdent.print memory stdout;
flush rif
);
if options.display_sim2chro
then Sim2chro.call_sim2chro state options.output
else () ;
let msg = "" (* Coverage.dump_oracle_io in_vals tail !cov *) in
output_msg (
"\n*** Lurette stops because the oracle returned false at step "
^(soi t)^".\n"^msg);
false
) else true
) else true
)
(**************************************************************************)
......@@ -506,13 +452,12 @@ and
None -> random_seed ()
| Some seed -> seed
in
set_luciole_mode_if_necessary init_state sut_i_vntl sut_o_vntl oracle_i_vntl oracle_o_vntl;
set_luciole_mode_if_necessary init_state sut_i_vntl sut_o_vntl [] [];
Random.init seed ;
output_msg ("\nThe random engine was initialized with the seed "^(soi seed)^"\n");
(* Initialisation of the sut and the oracle *)
Sut.init ();
Oracle.init ();
(* Sim2chro *)
output_string rif ("# seed = " ^ (soi seed) ^ "\n");
......@@ -788,14 +733,6 @@ and (main_loop :
(* Tries the sut `n*p'^nth times *)
let (inputs: env_in list) = List.map Sut.trie outputs in
let _ =
if not (check_oracle outputs inputs locals local_var_name_and_type_list state.d.memory t rif state)
then (
output_msg ("The generated data can be found in the file "^
options.output^"\n");
lurette_exit 2
);
in
let l = (List.length inputs) in
l_average := !l_average +. (float_of_int l)
......@@ -823,35 +760,7 @@ and (main_loop :
read_luciole_outputs sut_output
) else ( sut_output, Value.OfIdent.empty )
in
let _ =
if
not (check_oracle [output] [new_input] [loc] local_var_name_and_type_list state.d.memory t rif next_state)
then
(
output_msg ("The generated data can be found in the file " ^
options.output ^ "\n");
lurette_exit 2
);
in
let oracle_outputs =
if (options.oracle) then
let r, oracle_outputs = Oracle.step output new_input in
Sim2chro.put_oracle_step_values rif oracle_outputs;
if (not r) then (
print_failure output new_input oracle_outputs loc t local_var_name_and_type_list rif;
lurette_exit 1
);
oracle_outputs
else
Value.OfIdent.empty
in
let new_input = Value.OfIdent.union new_input oracle_outputs
(*
List.iter (fun (name, value) -> Hashtbl.add new_input name value) oracle_outputs;
new_input
*)
in
let _ =
if options.show_step then
(
......@@ -897,8 +806,6 @@ and (main_loop :
sut_o_vntl
sut_i_vntl
local_var_name_and_type_list;
if options.oracle then (
Sim2chro.put_oracle_step_values rif oracle_outputs);
if
skip
then
......@@ -940,33 +847,6 @@ and (main_loop :
read_luciole_outputs new_luciole_outputs
else
(
if options.oracle then (
output_msg2 rif
"\n ==> The test completed; no property has been violated.\n\n";
output_msg2 rif "\n Coverage:\n" ;
let (n,i) = ref 0, ref 0 in
Value.OfIdent.iter
(fun vn e ->
let covered = "covered_" in
if String.length vn > 9 && String.sub vn 0 (String.length covered) = covered then (
incr n;
if (e = Value.B true) then incr i;
output_msg2 rif "\t";
output_msg2 rif (Prevar.format vn);
output_msg2 rif " = ";
Value.print stdout e;
Value.print rif e;
output_msg2 rif "\n")
)
oracle_outputs;
if !n>0 then (
let msg = (
"The coverage rate is " ^
(my_string_of_float_precision (100. *. (float_of_int !i) /. (float_of_int !n)) 1) ^ "%\n")
in
output_msg2 rif msg;
)
);
let exec_times =
let ptime = Unix.times () in
ptime.Unix.tms_utime +. ptime.Unix.tms_stime
......
......@@ -252,19 +252,21 @@ let (make_ec_exe : string -> vars * vars * (string -> unit) *
let (make_luciole : string -> vars -> vars ->
(string -> unit) * (Data.subst list -> Data.subst list)) =
fun dro_file luciole_inputs luciole_outputs ->
Printf.eprintf "*** Inputs are missing. Try to generate them with luciole\n";
Printf.eprintf "*** luciole: generate lurette_luciole.c\n";
if luciole_outputs <> ["Step","bool"] || luciole_outputs <> [] then (
Printf.eprintf "Inputs are missing. Try to generate them with luciole\n";
Printf.eprintf "Luciole: generate lurette_luciole.c\n"
);
Luciole.gen_stubs true "lurette" luciole_outputs luciole_inputs;
Printf.eprintf "*** luciole: generate lurette.dro from lurette_luciole.c\n";
Printf.eprintf "Luciole: generate lurette.dro from lurette_luciole.c\n";
flush stderr;
if Util2.c2dro "lurette_luciole.c" then () else
(
Printf.eprintf "*** Fail to generate lurette.dro! bye...\n";
Printf.eprintf "*** Lurette: Fail to generate lurette.dro for luciole! bye...\n";
flush stderr;
exit 2
);
Printf.eprintf "\n*** luciole: launch simec_trap on lurette.dro\n";
Printf.eprintf "\nluciole: launch simec_trap on lurette.dro\n";
let (luciole_stdin_in, luciole_stdin_out ) = Unix.pipe () in
let (luciole_stdout_in, luciole_stdout_out) = Unix.pipe () in
......
......@@ -27,7 +27,7 @@
(setq lutin-font-lock-keywords
'(("--.*$" . font-lock-comment-face)
("\\<\\(loop\\|fby\\|try\\|trap\\|catch\\|do\\)\\>" . font-lock-builtin-face)
("\\<\\(loop\\|fby\\||raise\\|try\\|trap\\|catch\\|do\\)\\>" . font-lock-builtin-face)
("\\<\\(const\\|extern\\|node\\|run\\|include\\|returns\\|type\\)\\>" . font-lock-keyword-face)
("\\<\\(let\\|assert\\|exist\\|in\\|if\\|then\\|else\\)\\>" . font-lock-keyword-face)
("\\<\\(true\\|pre\\|and\\|or\\|not\\|false\\)\\>" . font-lock-reference-face)
......
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