Commit e46a79dc authored by Erwan Jahier's avatar Erwan Jahier

Some improvements in lurettetop --direct:

 - fix the coverage stuff that was not working
 - add an 'info' command that display a sum-up of the test parameters
 - add support to compile Lustre V4 programs

Moreover, we now use the direct mdoe in the non-reg tests !!
parent 661cc7ad
......@@ -8,9 +8,18 @@ LURETTETOP=$(LTOP) --precision 2 --sut heater_control.lus \
--step-mode Inside --local-var --no-sim2chro --seed 3 \
--do-not-show-step
LURETTETOP_DIRECT=$(LTOP) --direct \
-rp "sut:v4:heater_control.lus:heater_control" \
-rp "oracle:v4:heater_control.lus:not_a_sauna" \
-rp "env:lutin:env.lut:main" \
--test-length 100 --thick-draw 1 \
--draw-inside 0 --draw-edges 0 --draw-vertices 0 --draw-all-vertices \
--step-mode Inside --local-var --no-sim2chro --seed 3 \
--do-not-show-step
#
test:
test_old:
rm -f test.rif0 .lurette_rc
$(LURETTETOP) -go --output test.rif0 env.lut && \
grep -v "lurette chronogram" test.rif0 | \
......@@ -18,6 +27,14 @@ test:
rm -f test.res && diff -B -u -i test.rif.exp test.rif > test.res
[ ! -s test.res ] && make clean
test:
rm -f test.rif0 .lurette_rc
$(LURETTETOP_DIRECT) -go --output test.rif0 && \
grep -v "lurette chronogram" test.rif0 | \
grep -v "The execution lasted"| sed -e "s/^M//" > test.rif &&\
rm -f test.res && diff -B -u -i test.rif.exp test.rif > test.res
[ ! -s test.res ] && make clean
sut:
call-via-socket -addr 127.0.0.1 -port 2000 -server ./not_a_sauna.sh
......
......@@ -59,10 +59,13 @@ tel
-----------------------------------------------------------------------
-----------------------------------------------------------------------
node not_a_sauna(T, T1, T2, T3 : real; Heat_on: bool) returns (ok:bool);
node not_a_sauna(T, T1, T2, T3 : real; Heat_on: bool) returns (ok, c1, c2, c3:bool);
let
ok = true -> pre T < TMAX + 1.0 ;
c1 = T> TMAX;
c2 = T= TMAX;
c3 = T< TMAX;
tel
node not_a_sauna2(T, T1, T2, T3 : real; Heat_on: bool) returns (ok:bool);
......
This diff is collapsed.
......@@ -37,7 +37,46 @@ Equivalently, you can directly set values at the command line:
... [... testing ...]
"
let (info : unit -> unit) =
fun _ ->
let msg = "The current test parameters are:
sut: "^ (String.concat "," (List.map reactive_program_to_string args.suts)) ^ "
env: "^ (String.concat "," (List.map reactive_program_to_string args.envs)) ^ "
oracle: "^ (String.concat "," (List.map reactive_program_to_string args.oracles)) ^ "
test length: " ^ (string_of_int args.step_nb) ^ "
precision: " ^ (string_of_int args.precision) ^ "
seed: " ^ (match args.seed with
None -> "chosen randomly"
| Some i -> (string_of_int i)) ^ "
verbosity level: " ^ (string_of_int (args.verbose)) ^ "
rif file name: " ^ args.output ^ "
coverage file name: " ^ args.cov_file ^ "
do we stop when an oracle returns false?: "
^ (if args.stop_on_oracle_error then "yes" else "no") ^
(match args.extra_cfiles with
None -> ""
| Some str -> ("
extra_source_files: " ^ str)) ^
(match args.extra_libs with
None -> ""
| Some str -> ("
extra_libs: " ^ str)) ^
(match args.extra_libdirs with
None -> ""
| Some str -> ("
extra_libdirs: " ^ str)) ^
(match args.extra_includedirs with
None -> ""
| Some str -> ("
extra_includedirs: " ^ str)) ^ "
display_local_var: " ^ (if (args.display_local_var) then "yes" else "no") ^ "
"
in
output_string args.ocr msg;
flush args.ocr
let (display : unit -> unit) =
fun _ ->
let msg = "The commands are:
......@@ -52,6 +91,9 @@ quit q, bye
help, h, ?
display this list of commands
info, i
Display a sum-up of the test parameters
man
display a small user manual
......@@ -97,24 +139,23 @@ set_rif <string>, set_output <string>
to set the name of the file the (rif) output of the test is
put into. Its current value is \"" ^ args.output ^ "\"
sim2chro
sim2chro, s
call sim2chro to visualize (rif) data
gnuplot
gnuplot_ps
gnuplot, g
call gnuplot (> 3.7) to visualize (rif) data.
set_cov_file <string>
set the coverage file name. Its current value is \"" ^ args.cov_file ^ "\"
reset_cov_file <bool>
reset the coverage info in the coverage file before the run.
reset the coverage info in the coverage file before the next run.
Its current value is \"" ^ (if args.reset_cov_file then "true" else "false") ^ "\"
stop_on_oracle_error <bool>
set a boolean flag stating what to do when an oracle returns false
Its current value is \"" ^ (if args.stop_on_oracle_error then "true" else "false") ^ "\"
more
Display advanded commands.
......@@ -292,6 +333,7 @@ type t =
| ResetCovFile of bool
| CovFile of string
| StopOnOracleError of bool
| Info
| Nop
let lexer = Genlex.make_lexer []
......@@ -305,6 +347,8 @@ let rec (parse_tok : tok -> t) =
| [< 'Genlex.Ident(_, "run") >] -> Run
| [< 'Genlex.Ident(_, "r") >] -> Run
| [< 'Genlex.Ident(_, "b") >] -> Build
| [< 'Genlex.Ident(_, "info") >] -> Info
| [< 'Genlex.Ident(_, "i") >] -> Info
| [< 'Genlex.Ident(_, "build") >] -> Build
| [< 'Genlex.Ident(_, "build_env") >] -> BuildEnv
| [< 'Genlex.Ident(_, "change_dir") ; 'Genlex.String(_, dir) >] -> ChDir(dir)
......@@ -415,6 +459,7 @@ let rec (parse_tok : tok -> t) =
| [< 'Genlex.Ident(_, "set_cov_file") ;'Genlex.String(_, str) >] ->
CovFile(str)
| [< 'Genlex.Ident(_, "stop_on_oracle_error") ;
str = parse_ident_or_string
>] ->
......@@ -452,7 +497,9 @@ let rec (parse_tok : tok -> t) =
| [< 'Genlex.Ident(_, "batch" ) ; str = parse_ident_or_string >] -> Batch(str)
| [< 'Genlex.Ident(_, "sim2chro") >] -> CallSim2chro
| [< 'Genlex.Ident(_, "s") >] -> CallSim2chro
| [< 'Genlex.Ident(_, "gen_fake_lucky") >] -> BuildEnv
| [< 'Genlex.Ident(_, "g") >] -> CallGnuplot
| [< 'Genlex.Ident(_, "gnuplot") >] -> CallGnuplot
| [< 'Genlex.Ident(_, "gnuplot_ps") >] -> CallGnuplotPs
......@@ -696,6 +743,7 @@ let (read : (unit -> string) -> bool) =
true
| ResetCovFile(b) -> args.reset_cov_file <- b; true
| CovFile(f) -> args.cov_file <- f; true
| Info -> info(); true
| StopOnOracleError(b) -> args.stop_on_oracle_error <- b ; true
| RootNode(node) -> args.root_node <- node; true
......@@ -800,6 +848,7 @@ let (read : (unit -> string) -> bool) =
output_string args.ocr "\n*** Cannot build lurette, sorry.\n \n \n";
flush args.ocr;
Unix.chdir args.tmp_dir;
args.reset_cov_file <- false;
true
)
| Show ->
......
......@@ -210,6 +210,12 @@ let gp_oc = Unix.out_channel_of_descr connected_gp_sock
let (gnuplot: string -> bool) =
fun file ->
if not (Sys.file_exists file) then (
output_string args.ecr ("*** File "^ file ^" not found.\n");
flush args.ecr;
false
)
else
try
if !gp_pid = 0 then
(
......
......@@ -106,8 +106,6 @@ type t = {
mutable sut_compiler : compiler ;
mutable oracle_compiler : compiler ;
mutable step_nb : int;
mutable draw_nb : int ;
......@@ -197,7 +195,7 @@ let (args : t) = {
delay_env_outputs = false;
step_by_step = None ;
show_step = false ;
display_local_var = true ;
display_local_var = false ;
display_sim2chro = false ;
seed = None ;
precision = 2;
......
......@@ -65,6 +65,7 @@ let (f : unit -> int) =
let sut_in, sut_out, sut_kill, sut_step_sl, sut_init_in, sut_init_out =
match args.suts with
[LustreV6(prog,node)] -> add_init [] (LustreRun.make_v6 prog node)
| [LustreV4(prog,node)] -> add_init [] (LustreRun.make_v4 prog node)
| [LustreEc(prog)] -> add_init [] (LustreRun.make_ec prog)
| [Lutin(prog,node)] -> add_init [] (make_lut prog node)
| [Socket(addr, port)] -> add_init [] (LustreRun.make_socket addr port)
......@@ -77,7 +78,7 @@ let (f : unit -> int) =
match args.oracles with
| [LustreEc(prog)] -> LustreRun.make_ec prog
| [LustreV6(prog,node)] -> LustreRun.make_v6 prog node
| [LustreV4(prog,node)] -> assert false (* LustreRun.make_v4 prog node *)
| [LustreV4(prog,node)] -> LustreRun.make_v4 prog node
| [Socket(addr, port)] -> LustreRun.make_socket addr port
| [Lutin(prog,node)] -> make_lut prog node
| [SocketInit(addr, port)] -> assert false
......@@ -88,6 +89,7 @@ let (f : unit -> int) =
match args.envs with
| [Lutin(prog,node)] -> add_init [] (make_lut prog node)
| [LustreV6(prog,node)] -> add_init [] (LustreRun.make_v6 prog node)
| [LustreV4(prog,node)] -> add_init [] (LustreRun.make_v4 prog node)
| [LustreEc(prog)] -> add_init [] (LustreRun.make_ec prog)
| [Socket(addr, port)] -> add_init [] (LustreRun.make_socket addr port)
| [SocketInit(addr, port)] -> LustreRun.make_socket_init addr port
......@@ -111,16 +113,16 @@ let (f : unit -> int) =
Printf.printf "oracle output : \n%s\n" oracle_output_str;
flush stdout
in
let seed =
match args.seed with
let seed =
match args.seed with
| None -> random_seed ()
| Some seed -> seed
in
let cov_init =
if oracle_out = [] then None else
if List.length oracle_out < 2 then None else
let is_bool (_,t) = (t = "bool") in
let names = List.filter is_bool (List.tl oracle_out) in
let names = snd (List.split names) in
let names = fst (List.split names) in
Some (Coverage.init names args.cov_file args.reset_cov_file)
in
let oc = open_out args.output in
......@@ -160,8 +162,7 @@ let (f : unit -> int) =
flush oc;
match oracle_out_vals, cov with
| [],_ -> loop cov sut_out_vals env_out_vals (i+1)
| _::_, None -> assert false
| _, None -> loop cov sut_out_vals env_out_vals (i+1)
| (_, Rif_base.B true)::tail, Some cov ->
let cov = Coverage.update_cov tail cov in
loop (Some cov) sut_out_vals env_out_vals (i+1)
......@@ -189,21 +190,21 @@ let (f : unit -> int) =
(string_of_int seed) ^ "\n" );
Rif_base.write_interface oc env_out sut_out loc;
Rif.flush oc;
in
in
let msg, res =
try
if res_compat = 0 then
let cov, res = loop cov_init sut_init_out sut_init_in 0 in
(match cov, args.oracle with
| None, None -> ()
| Some cov, Some oracle -> Coverage.dump oracle args.output cov
| None, Some _ -> assert false
| Some _, None -> assert false
(match cov, args.oracles with
| None, _ -> ()
| Some cov, _::_ ->
let str = String.concat ", " (List.map reactive_program_to_string args.oracles) in
Coverage.dump str args.output cov
| Some _, [] -> assert false
);
"#quit\n", res
"quit\n", res
else
"#quit\n", res_compat
"quit\n", res_compat
with e ->
(Printexc.to_string e), 2
in
......
......@@ -108,6 +108,16 @@ let (make_v6 : string -> string -> vars * vars * (string -> unit) *
else
failwith ("Error when compiling " ^ lus_file ^ " with node " ^ node ^"\n")
(**********************************************************************************)
let (make_v4 : string -> string -> vars * vars * (string -> unit) *
(Rif_base.subst list -> Rif_base.subst list)) =
fun lus_file node ->
let dir = Filename.dirname lus_file in
if Util2.lv42ec lus_file node dir then
make_ec (node ^ ".ec")
else
failwith ("Error when compiling " ^ lus_file ^ " with node " ^ node ^"\n")
(**********************************************************************************)
let rec connect_loop sock addr k =
......@@ -135,9 +145,14 @@ let (make_socket_do : string -> int -> in_channel *
"(" ^ funcstr ^ " " ^ paramstr ^")\n")
in
let kill msg =
print_string "Killing the socket process\n";
print_string ("'"^msg^"'");
flush stdout;
output_string sock_out msg;
let _ = input_line sock_in in
let str = input_line sock_in in
(* make sure that the sut process has read the quit before closing socks *)
print_string (str ^"\n");
flush stdout;
Unix.shutdown sock Unix.SHUTDOWN_ALL
in
let vars_in, vars_out =
......
......@@ -32,6 +32,8 @@ val make_ec : string ->
*)
val make_v6 : string -> string ->
vars * vars * (string -> unit) * (Rif_base.subst list -> Rif_base.subst list)
val make_v4 : string -> string -> vars * vars * (string -> unit) *
(Rif_base.subst list -> Rif_base.subst list)
(** [make_socket sock_addr port]
......
......@@ -59,7 +59,7 @@ let (lus2ec: string -> string -> string -> bool) =
print_string (Printexc.to_string e);
flush stdout;
false
let lv42ec = lus2ec
let (string_to_string_list : string -> string list) = Util.string_to_string_list
......
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