Commit f8491fcc authored by Erwan Jahier's avatar Erwan Jahier

Print all the oracle outputs when an oracle is violated, and compute

a coverage rate based on oracle outputs with a name that begins with
"covered_".

+ luc2c : synchronisation avec ec2c v 0.62 qui a change sa politique
de definition des types _int, _bool, et _real.
parent e8f21702
V1.49 (8/04/2010)
V1.50 (11/05/2010)
* Add support to compile Lustre V6 programs.
* Compute a coverage rate. It looks at oracle outputs which names
begins with "covered_", and compute the rate of true values among
those.
V1.49 (8/04/2010)
* Add support to compile Lustre V6 programs.
V1.48 (25/03/2010)
......
......@@ -39,7 +39,7 @@ call_foo.ec:
lus2ec call_foo.lus call_foo
call_foo.c: call_foo.ec
ec2c -loop call_foo.ec
ec2c -loop call_foo.ec
call_foo.o: call_foo.c
$(CC) -c $(CFLAGS) call_foo.c
......
......@@ -5,7 +5,7 @@ CC=g++
test1:
rm -f test1.rif0 .lurette_rc && \
$(LURETTETOP) --sut tramway.lus --sut-compiler lv4 --oracle-compiler lv4 \
$(LURETTETOP) --sut tramway.lus --sut-compiler lv6 --oracle-compiler lv6 \
-msn controller -go -l 100 --draw-all-formula -td 10 \
--draw-inside 1 --compute-poly-volume \
--do-not-show-step -o test1.rif0 \
......@@ -21,7 +21,7 @@ test1:
test2 :
rm -f test2.rif0 && \
$(LURETTETOP) -l 100 -go -seed 1 --sut-compiler lv4 --oracle-compiler lv4 \
$(LURETTETOP) -l 100 -go -seed 1 --sut-compiler lv6 --oracle-compiler lv6 \
--do-not-show-step -ns2c \
-sut tramway.lus --main-sut-node controller \
-oracle tramway.lus --main-oracle-node oracle \
......
......@@ -357,7 +357,7 @@ gnuplot-rif_clean:
lucky:
make -k nc -f Makefile.lucky OCAMLFLAGS=""
lucky_debug:
lucky_dc:
make -k dc -f Makefile.lucky OCAMLFLAGS=""
lucky_clean:
......@@ -690,9 +690,10 @@ allnc: libncnc lucky ltop show stubs gnuplot-rif gnuplot-socket gen_luc luc2c lu
static: libnc lucky_static ltop_static show_static stubs_static gen_luc_static
OTAGS=/local/jahier/otags-3.09.3.2/otags
OTAGS=/local/jahier/jahier/bin/otags
tags: $(REALLY_ALL_SOURCES)
$(OTAGS) -v $(REALLY_ALL_SOURCES) $(shell ocamlc -where)/*.mli
$(OTAGS) -v $(shell ocamlc -where)/*.mli $(REALLY_ALL_SOURCES)
# ne marche que si on lance cette commande A LA MAIN (!!!) depuis une fenetre DOS
strtopwin:
......@@ -702,8 +703,6 @@ strtop:
ocamlmktop -o strtop str.cma unix.cma graph.cma
unixtop:
ocamlmktop -o unixtop unix.cma str.cma
unixtop:
ocamlmktop -o unixtop unix.cma str.cma
clean_exe:
rm -f gen_stubs_exe lucky lurettetop_exe lurette_lib.* \
......
......@@ -42,10 +42,8 @@ let rec (lookup: Var.env_in -> Env_state.t -> Exp.var -> Value.t option) =
in
output_msg (
"*** The variable " ^ (Var.name var)
^ " is undefined at the first step " ^ node_msg
^ "*** You need to rewrite your environment"
^ " spec in such a way that\n sut outputs are not used"
^ " at the first step\n ");
^ " is undefined at this step " ^ node_msg
^ "\n");
exit 2
)
| Var.Pre ->
......
......@@ -39,6 +39,7 @@ let (go: module_name -> string -> typedef list -> vn_ct list -> vn_ct list ->
"#include <stdlib.h>\n" ^
"#include <stdio.h> \n" ^
"#include <ocaml2c.h>\n" ^
"#include <ocaml2c.h>\n" ^
"#include \"" ^ mod_name ^ ".h\" \n" ^
" \n") ;
......
......@@ -195,10 +195,20 @@ let (gen_h_file : string -> Exp.var list -> Exp.var list -> Exp.var list -> unit
putln "#include <luc4c_stubs.h> \n";
putln "//-------- Predefined types ---------";
putln ("#ifndef _"^ fn ^ "_LUC2C_PREDEF_TYPES");
putln ("#define _"^ fn ^ "_LUC2C_PREDEF_TYPES");
putln "typedef int bool;";
putln "#endif";
putln "#ifndef _EC2C_PREDEF_TYPES
#define _EC2C_PREDEF_TYPES
typedef int _bool;
typedef int _boolean;
typedef int _int;
typedef int _integer;
typedef char* _string;
typedef double _real;
typedef double _double;
typedef float _float;
#define _false 0
#define _true 1
#endif
";
putln "//--------- Pragmas ----------------";
putln ("//MODULE: " ^ fn ^ " " ^ (string_of_int (List.length in_vars))
^ " " ^ (string_of_int (List.length out_vars)));
......
......@@ -224,16 +224,20 @@ let lurette_exit i =
output_msg ("Lurette finished.\n");
exit i
let print_failure i o l t rif =
let print_failure i o oo l t rif =
if l<>[] then (
output_msg "\n* environment local variables:\n" ;
print_subst_list l stdout);
output_msg "\n* sut input variables:\n" ;
print_subst_list i stdout;
(* print_subst_list i stderr; *)
output_msg "\n* sut output variables:\n" ;
output_msg "\n* sut output variables:\n\t" ;
print_env_in o stdout;
output_msg "\n* environment local variables:\n" ;
print_subst_list l stdout;
output_msg "\n* oracle output variables:\n" ;
print_subst_list oo stdout;
(* print_subst_list l stderr; *)
output_string rif "\n#oracle_failure at\n";
Sim2chro.put_current_step_values
rif
......@@ -271,23 +275,25 @@ let check_oracle inputs sut_outputs locals memory t rif state =
" at step " ^ (string_of_int t) ^
" with the following values:\n ");
let rec print_failures li lo ll lr =
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 l t rif
print_failure i o oo l t rif
else
print_failures (List.tl li) (List.tl lo) (List.tl ll) (List.tl lr)
print_failures (List.tl li) (List.tl lo) (List.tl loo) (List.tl ll) (List.tl lr)
in
print_failures inputs sut_outputs locals results ;
print_failures inputs sut_outputs oracle_outputs locals results ;
output_msg "\n* Memories:\n\t" ;
if memory <> [] then (
output_msg "\n* Memories:\n" ;
print_subst_list memory stdout;
(* print_subst_list memory stderr; *)
flush rif;
flush rif);
if options.display_sim2chro
then Sim2chro.call_sim2chro state options.output
else () ;
......@@ -520,11 +526,11 @@ and
| Some seed -> seed
in
if not (check_var_decl_consistency
init_state sut_i_vntl sut_o_vntl oracle_i_vntl oracle_o_vntl)
then
None
else
(* if not (check_var_decl_consistency *)
(* init_state sut_i_vntl sut_o_vntl oracle_i_vntl oracle_o_vntl) *)
(* then *)
(* None *)
(* else *)
(
Random.init seed ;
output_msg
......@@ -591,7 +597,7 @@ and
if
not (options.help)
then
main_loop 1 s p k1 k2 k3 rif (Hashtbl.create 0) init_state
main_loop 1 s p k1 k2 k3 rif (Hashtbl.create 0) init_state
else
init_state
in
......@@ -631,8 +637,8 @@ and
(* Tries the sut `n*p'^nth times *)
let (inputs: env_in list) =
List.map (Sut.trie) outputs in
List.map Sut.trie outputs
in
let _ =
if
not (check_oracle outputs inputs locals state.d.memory t rif state)
......@@ -678,13 +684,17 @@ and
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 loc t rif;
print_failure output new_input oracle_outputs loc t rif;
lurette_exit 1
);
oracle_outputs
else
[]
in
let new_input =
List.iter (fun (name, value) -> Hashtbl.add new_input name value) oracle_outputs;
new_input
in
let _ =
if options.show_step then
(
......@@ -770,23 +780,44 @@ and
((str <> "s") && (s > t))
(* ((str = "" || str = " ") && (s > t)) *)
then
main_loop (t+1) s p k1 k2 k3 rif new_input next_state
main_loop (t+1) s p k1 k2 k3 rif new_input next_state
else
(
if options.oracle then
if options.oracle then (
output_msg
"\n ==> The test completed; no property has been violated.\n\n";
output_msg "\n Coverage:\n" ;
let (n,i) = ref 0, ref 0 in
List.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_msg "\t";
output_msg (Prevar.format vn);
output_msg " = ";
Value.print stdout e;
output_msg "\n")
)
oracle_outputs;
if !n>0 then (
output_msg (
"The coverage rate is " ^
(my_string_of_float_precision (100. *. (float_of_int !i) /. (float_of_int !n)) 1) ^ "%\n")
)
);
let exec_times =
let ptime = Unix.times () in
ptime.Unix.tms_utime +. ptime.Unix.tms_stime
in
let time_msg =
" The execution lasted " ^ (string_of_float exec_times) ^
" The execution lasted " ^ (my_string_of_float_precision exec_times 3) ^
" second"^ (if exec_times < 2.0 then ".\n" else "s.\n")
in
output_msg (
" The Test Thickness average was " ^
(string_of_float (1.0 +. !l_average /. (float_of_int t))) ^ "\n");
(my_string_of_float_precision (1.0 +. !l_average /. (float_of_int t)) 1) ^ "\n");
output_msg ("The generated data can be found in the file " ^
options.output ^ "\n");
output_msg time_msg;
......
......@@ -245,9 +245,9 @@ let (string_to_compiler:string -> compiler option) =
| "verimag" -> Some VerimagV4
| "Verimag" -> Some VerimagV4
| "lv4" -> Some VerimagV4
| "lv4" -> Some VerimagV4
| "lv6" -> Some VerimagV6
| "v4" -> Some VerimagV4
| "lv6" -> Some VerimagV6
| "v6" -> Some VerimagV6
| "scade-gui" -> Some ScadeGUI
| "scade_gui" -> Some ScadeGUI
| "scade" -> Some Scade
......
......@@ -97,7 +97,7 @@ let (put_oracle_step_values: out_channel -> Var.subst list -> unit) =
let put s = output_string oc s in
put "#oracle_outputs ";
List.iter
(fun (_,vv) -> put ((Value.to_string vv) ^ " "))
(fun (v,vv) -> put ((Value.to_string vv) ^ " "))
values;
put "\n"
......
......@@ -69,12 +69,13 @@ let structured_to_string = structured_to_string_param "real"
let rec (to_cstring : t -> string) =
fun vt ->
match vt with
BoolT -> "bool"
| IntT -> "int"
| FloatT -> "double"
BoolT -> "_bool"
| IntT -> "_int"
| FloatT -> "_real"
| UT(ut) -> structured_to_cstring ut
and
(structured_to_cstring : structured -> string) =
fun ut ->
match ut with
......
......@@ -461,6 +461,10 @@ let my_string_of_float f =
let precision_str = string_of_int !precision in
format_float ("%." ^ precision_str ^ "f") f
let my_string_of_float_precision f p =
let precision_str = string_of_int p in
format_float ("%." ^ precision_str ^ "f") f
(* external string_length : string -> int = "%string_length" *)
......
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