Commit 5e274bbc authored by Erwan Jahier's avatar Erwan Jahier

Enhance the gnuplot-rif visualiser

parent b8d06ba6
......@@ -200,3 +200,4 @@
#step 50
1.1005 1.1065 1.0838 1.0901 1.0854 1.0888 1.0854 1.0790 F F F F F F F F F F #outs 1.0854 F F F F F F F F F F F F 1 1 1 1
#locs -0.0017 0.0066 0.0062 0.0078 0.0142 0.0036 -0.0117 -0.0062 1.0859 -0.1186
#
......@@ -2015,3 +2015,9 @@
#step 500
6.42 6.45 7.41 7.97 #outs F
#locs 63 0.01 0.02 -0.06 -0.06
#
# ==> The test completed; no property has been violated.
#
##
# Coverage:
#
......@@ -32,8 +32,8 @@ test2:
grep -v "lurette chronogram" test2.rif0 | \
grep -v "The execution lasted"| sed -e "s/^M//"\
> test2.rif &&\
$(RM) test3.res && diff -u -i test2.rif.exp test2.rif \
> test3.res
$(RM) test2.res && diff -u -i test2.rif.exp test2.rif \
> test2.res
[ ! -s test2.res ] && make clean
test3 :
......@@ -41,8 +41,8 @@ test3 :
$(LURETTETOP) -l 100 -go -seed 1 \
--do-not-show-step -ns2c -sut heater_ctrl2.lus -msn heater_ctrl2 -o test3.rif0 window.luc &&\
grep -v "lurette chronogram" test3.rif0 | \
grep -v "The execution lasted"| sed -e "s/^M//" > test3.rif
$(RM) test3.res && diff -u -i test3.rif.exp test3.rif > test3.res
grep -v "The execution lasted"| sed -e "s/^M//" > test3.rif && \
$(RM) test3.res && diff -u -i test3.rif.exp test3.rif > test3.res
[ ! -s test3.res ] && make clean
......
......@@ -99,3 +99,4 @@
#step 30
10 #outs T
#locs -1 F
#
......@@ -98,3 +98,4 @@
#step 30
17.8512 #outs F
#locs -0.8882
#
......@@ -310,3 +310,4 @@
#step 100
16.04 #outs 10.00 T
#locs 0.18 0
#
This diff is collapsed.
......@@ -416,3 +416,9 @@ T F T F T T #outs F F F T F
#step 100
T F T T T F #outs F F F T F
#locs
#
# ==> The test completed; no property has been violated.
#
##
# Coverage:
#
......@@ -416,3 +416,9 @@ F T F F F F #outs F F F F F
#step 100
F F F F T F #outs T F F F F
#locs
#
# ==> The test completed; no property has been violated.
#
##
# Coverage:
#
......@@ -344,6 +344,7 @@ lib_prof:liblurette_prof.a
##############################################################################"
.PHONY: gnuplot-rif
gnuplot-rif:
make -k nc -f Makefile.gnuplot-rif
......
......@@ -47,7 +47,7 @@ SOURCES_C = \
$(HERE)/liblutin.idl \
$(HERE)/Ezdl_c.c \
SOURCES_OCAML := \
SOURCES_OCAML0:= \
$(HERE)/Ezdl.ml \
$(HERE)/Ezdl.mli \
$(HERE)/error.ml \
......@@ -89,8 +89,6 @@ SOURCES_OCAML := \
$(HERE)/lucParse.mli \
$(HERE)/lucParse.ml \
$(HERE)/lucParse.mli \
$(HERE)/lucProg.mli \
$(HERE)/lucProg.ml \
$(HERE)/polyhedron.mli \
$(HERE)/polyhedron.ml \
$(HERE)/formula_to_bdd.mli \
......@@ -107,6 +105,8 @@ SOURCES_OCAML := \
$(HERE)/solver.ml \
$(HERE)/show_env.mli \
$(HERE)/show_env.ml \
$(HERE)/lucProg.mli \
$(HERE)/lucProg.ml \
$(HERE)/prog.mli \
$(HERE)/prog.ml \
$(HERE)/fGen.mli \
......@@ -129,8 +129,9 @@ SOURCES_OCAML := \
./luc4ocaml_nolbl.ml
ifdef MLONLY
SOURCES_OCAML =$(filter %.ml, $(SOURCES_OCAML))
SOURCES_OCAML =$(filter %.ml, $(SOURCES_OCAML0))
endif
SOURCES_OCAML=$(SOURCES_OCAML0)
SOURCES = $(SOURCES_C) $(SOURCES_OCAML)
......
......@@ -16,7 +16,7 @@ open Var
open Type
open List
open Util
open Prog
open Prog
(****************************************************************************)
......@@ -31,20 +31,20 @@ open Prog
type t =
| Cont of (unit -> t * Exp.formula * LucParse.node list)
| Finish (* no more solutions *)
| RStop of string (* Normal Termination (for Lutin) *)
(** wt is traversed using continuations *)
type wt_cont =
| WCont of (unit -> wt_cont * Exp.formula * LucParse.node)
| WFinish (* no more solutions *)
| WStop of string (* ditto, but stop at once raising an exception *)
(****************************************************************************)
(* Exported *)
exception NoMoreFormula
exception NormalStop of string
let (call_cont : t -> t * formula * LucParse.node list) =
fun cont ->
......@@ -52,13 +52,16 @@ let (call_cont : t -> t * formula * LucParse.node list) =
match cont with
| Cont f -> f ()
| Finish -> raise NoMoreFormula
| RStop str -> raise (NormalStop str)
let (call_wt_cont : wt_cont -> wt_cont * formula * LucParse.node) =
fun cont ->
let _ = if debug then (print_string "XXX call_wt_cont\n"; flush stdout) in
match cont with
| WCont f -> f ()
| WFinish -> WFinish, False, ""
| WFinish -> WFinish, False, "" (* dummy *)
| WStop msg -> cont, True (* dummy *), "" (* dummy *)
(* exported *)
let (choose_one_formula: t -> t * Exp.formula * Prog.ctrl_state) =
......@@ -81,8 +84,7 @@ let (get_all_formula: t -> formula list) =
(****************************************************************************)
let rec (wt_list_to_cont : Var.env_in -> Prog.state -> wt_cont list ->
let rec (wt_list_to_cont : Var.env_in -> Prog.state -> wt_cont list ->
formula -> LucParse.node list -> t -> t) =
fun input state wtl facc nl fgen ->
(* [nl] is the list of nodes that correspond to [facc] *)
......@@ -90,12 +92,14 @@ let rec (wt_list_to_cont : Var.env_in -> Prog.state -> wt_cont list ->
match wtl with
| [] -> Cont (fun () -> (fgen, facc, nl))
| wt::wtl' ->
if wt = WFinish then
if wt = WFinish then
fgen
else
match choose_one_formula_atomic input state facc wt with
| WFinish, False, "" ->
fgen
| WStop str, _, "" ->
RStop str
| wt2, f2, n ->
let fgen' =
Cont (fun () ->
......@@ -109,6 +113,9 @@ and
let _ = if debug then (print_string "XXX choose_one_formula_atomic\n"; flush stdout) in
if cont = WFinish then
WFinish, False, ""
else
if cont = WStop str then
WStop str, True, ""
else
let (cont', f, n) = call_wt_cont cont in
let _ = if debug then (print_string ("XXX "^ n ^ "\n"); flush stdout) in
......@@ -133,7 +140,8 @@ and (wt_to_cont : Var.env_in -> Prog.state -> wt -> wt_cont -> wt_cont) =
let _ = if debug then (print_string ("XXX wt_to_cont "^ n ^"\n"); flush stdout) in
let children = Util.StringMap.find n tbl in
match children with
| Leave f -> WCont(fun () -> (cont, f, LucProg.get_original_name n))
| Prog.Stop str -> WStop str
| Leave (f,nstate) -> WCont(fun () -> (cont, f, nstate))
| Children l ->
if l = [] then
cont
......
......@@ -68,6 +68,9 @@ val get : Var.env_in -> Prog.state -> t list
(** Raised by choose_one_formula no more transitions can be taken *)
exception NoMoreFormula
(** Raised by choose_one_formula when a Prog.Stop is chosen (For Lutin) *)
exception NormalStop of string
val choose_one_formula : t -> t * Exp.formula * Prog.ctrl_state
(** [choose_one_formula run_aut] draws a formula accessible from
......
This diff is collapsed.
......@@ -184,6 +184,12 @@ let (print_debug_no_ic : string -> unit) =
else
()
(*******************************************************************************)
let set_min v x = match x with None -> v | Some x -> Var.set_min v x
let set_max v x = match x with None -> v | Some x -> Var.set_max v x
let set_init v x = match x with None -> v | Some x -> Var.set_init v x
let set_alias v x = match x with None -> v | Some x -> Var.set_alias v x
let set_default v x = match x with None -> v | Some x -> Var.set_default v x
(*******************************************************************************)
(** Parsing pragmas *)
......@@ -590,11 +596,11 @@ and (flatten_user_type : Exp.var -> Exp.var_tbl * LustreExp.vut) =
| UT(EnumT(el)) ->
let var1 = Var.make !loc_var_prefix (Var.name var) (UT(EnumT(el))) (Var.mode var) in
let var2 = Var.set_min var1 (Some (Numer(Ival 0))) in
let var3 = Var.set_max var2 (Some (Numer(Ival((List.length el) - 1)))) in
let var4 = Var.set_alias var3 (Var.alias var) in
let var5 = Var.set_default var4 (Var.default var) in
let var6 = Var.set_init var5 (Var.init var) in
let var2 = Var.set_min var1 ((Numer(Ival 0))) in
let var3 = Var.set_max var2 ((Numer(Ival((List.length el) - 1)))) in
let var4 = set_alias var3 ((Var.alias var)) in
let var5 = set_default var4 ( (Var.default var)) in
let var6 = set_init var5 ( (Var.init var)) in
let var6_tbl = Exp.add_var (Var.name var6) var6 empty_var_tbl in
(
var6_tbl,
......@@ -677,11 +683,11 @@ and (fill_var_options : Exp.var -> Exp.var_tbl -> Exp.var_tbl) =
and default = StringMap.find vn default_tbl
and init = StringMap.find vn init_tbl
in
let var1 = if min = None then var else Var.set_min var min in
let var2 = if max = None then var1 else Var.set_max var1 max in
let var3 = if alias = None then var2 else Var.set_alias var2 alias in
let var4 = if default = None then var3 else Var.set_default var3 default in
if init = None then var4 else Var.set_init var4 init
let var1 = set_min var min in
let var2 = set_max var1 max in
let var3 = set_alias var2 alias in
let var4 = set_default var3 default in
if init = None then var4 else set_init var4 init
with
_ ->
let print_tbl tbl =
......@@ -1163,11 +1169,11 @@ and (var_options_to_var : Lexing.lexbuf -> typedef list -> string -> Type.t ->
Not_found -> None (* no init value *)
in
let var0 = (Var.make !loc_var_prefix vn vt vm) in
let var1 = Var.set_min var0 min in
let var2 = Var.set_max var1 max in
let var3 = Var.set_alias var2 alias in
let var4 = Var.set_default var3 default in
let var5 = Var.set_init var4 init in
let var1 = set_min var0 min in
let var2 = set_max var1 max in
let var3 = set_alias var2 alias in
let var4 = set_default var3 default in
let var5 = set_init var4 init in
var5
and (parse_options_list : Exp.var_tbl -> LustreExp.vut -> typedef list ->
......
......@@ -56,6 +56,13 @@ let empty = {
graph = Graph.create ()
}
let set_min v x = match x with None -> v | Some x -> Var.set_min v x
let set_max v x = match x with None -> v | Some x -> Var.set_max v x
let set_init v x = match x with None -> v | Some x -> Var.set_init v x
let set_alias v x = match x with None -> v | Some x -> Var.set_alias v x
let set_default v x = match x with None -> v | Some x -> Var.set_default v x
(****************************************************************************)
let (merge_var : Exp.var list -> Exp.var list -> Exp.var list) =
(*
......@@ -165,11 +172,11 @@ let (merge_var : Exp.var list -> Exp.var list -> Exp.var list) =
Some v
in
let var1' =
(Var.set_min
(Var.set_max
(Var.set_alias
(Var.set_default
(Var.set_init
(set_min
(set_max
(set_alias
(set_default
(set_init
var1
init)
default)
......@@ -287,7 +294,7 @@ let (make_one : t -> LucParse.t -> t) =
let var' =
try
let init_var = (Var.init (StringMap.find vn all_vars)) in
Var.set_init var init_var
set_init var init_var
with _ ->
(* The1 var corresponding to "pre var" should exists in that table *)
assert false
......@@ -379,10 +386,10 @@ let (make_one : t -> LucParse.t -> t) =
| Some (Numer e) -> set var (Some (Numer (cnc vars e)))
| Some (Liste _) -> assert false
in
let nvar = aux Var.min Var.set_min
(aux Var.max Var.set_max
(aux Var.init Var.set_init
(aux Var.alias Var.set_alias var)))
let nvar = aux Var.min set_min
(aux Var.max set_max
(aux Var.init set_init
(aux Var.alias set_alias var)))
in
(StringMap.add (Var.name nvar) nvar vars), nvar
......@@ -623,14 +630,4 @@ let (is_node_final : LucParse.node -> t -> bool) =
assert false
(* exported *)
let (get_original_name : LucParse.node -> LucParse.node) =
fun n ->
let res =
if String.sub n 0 1 <> "_" then n else
try
let idx = 2 + Str.search_forward (Str.regexp "__") n 0 in
String.sub n idx ((String.length n) - idx)
with _ -> assert false
in
res
......@@ -35,5 +35,3 @@ val make : string option -> string list -> t
val is_node_transient : LucParse.node -> t -> bool
val is_node_final : LucParse.node -> t -> bool
(** exploit the internal naming convention to get the original name (XXX beurk). *)
val get_original_name : LucParse.node -> LucParse.node
......@@ -134,12 +134,12 @@ let (make_bool_expr : (var_name * var_type) list -> string -> bool_expr) =
match t with
Int ->
let v = Var.make "" x (var_type_to_type t) Var.Output in
let v1 = Var.set_max v (Some (Numer(Ival !default_max_int))) in
Var.set_min v1 (Some (Numer(Ival !default_min_int)))
let v1 = Var.set_max v ((Numer(Ival !default_max_int))) in
Var.set_min v1 ((Numer(Ival !default_min_int)))
| Float ->
let v = Var.make "" x (var_type_to_type t) Var.Output in
let v1 = Var.set_max v (Some (Numer(Fval (!default_max_float)))) in
Var.set_min v1 (Some (Numer(Fval (-.(!default_max_float)))))
let v1 = Var.set_max v ((Numer(Fval (!default_max_float)))) in
Var.set_min v1 ((Numer(Fval (-.(!default_max_float)))))
| Bool ->
Var.make "" x (var_type_to_type t) Var.Output
)
......
......@@ -53,6 +53,14 @@ let output_msg msg =
output_string stdout msg;
flush stdout
let output_msg2 rif msg =
let rif_msg = "#" ^ (Str.global_replace (Str.regexp "\n") "\n#") msg in
output_string stdout msg;
output_string rif (rif_msg);
flush stdout
let debug_msg msg = if options.verb > 1 then output_msg msg else ()
let (print_vn_str : (string * string) list -> unit) =
......@@ -152,7 +160,10 @@ let print_failure i o oo l t rif =
l
options.display_local_var
sut_o_vntl
sut_i_vntl
sut_i_vntl;
output_string rif "\n# oracle output variables:\n" ;
output_string rif (Var.subst_list_to_string "#" oo)
let soi = string_of_int
......@@ -177,7 +188,7 @@ let check_oracle inputs sut_outputs locals memory t rif state =
then
(
(* print inputs and outputs of all wrong tuple *)
output_msg (
output_msg2 rif (
"\n*** An assertion of the oracle has been violated at step "^(soi t)^
" with the following values:\n ");
......@@ -635,19 +646,19 @@ and
match Var.typ var with
| Type.BoolT ->
if str = "t" then Value.B(true) else if str = "f" then Value.B(false) else (
output_msg ("Can not convert into a bool:'"^str^"'\n");
output_msg2 rif ("Can not convert into a bool:'"^str^"'\n");
lurette_exit 2
)
| Type.IntT -> (
try Value.N(Value.I(int_of_string str))
with _ ->
output_msg ("Can not convert into an int:'"^str^"'\n");
output_msg2 rif ("Can not convert into an int:'"^str^"'\n");
lurette_exit 2
)
| Type.FloatT -> (
try Value.N(Value.F(float_of_string str))
with _ ->
output_msg ("Can not convert into a float:'"^str^"'\n");
output_msg2 rif ("Can not convert into a float:'"^str^"'\n");
lurette_exit 2)
| Type.UT _ -> assert false
in
......@@ -662,7 +673,7 @@ and
List.iter
(fun var ->
let value = try List.assoc (Var.name var) sl with Not_found ->
output_msg ("Reading luciole inputs: the value of " ^ (Var.name var) ^ " is unknown.\n");
output_msg2 rif ("Reading luciole inputs: the value of " ^ (Var.name var) ^ " is unknown.\n");
lurette_exit 2
in
let val_str = (Value.to_string value) ^"\n" in
......@@ -839,7 +850,8 @@ and
options.display_local_var
sut_o_vntl
sut_i_vntl ;
Sim2chro.put_oracle_step_values rif oracle_outputs;
if options.oracle then (
Sim2chro.put_oracle_step_values rif oracle_outputs);
if
skip
then
......@@ -882,9 +894,9 @@ and
else
(
if options.oracle then (
output_msg
output_msg2 rif
"\n ==> The test completed; no property has been violated.\n\n";
output_msg "\n Coverage:\n" ;
output_msg2 rif "\n Coverage:\n" ;
let (n,i) = ref 0, ref 0 in
List.iter
(fun (vn, e) ->
......@@ -892,17 +904,20 @@ and
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 " = ";
output_msg2 rif "\t";
output_msg2 rif (Prevar.format vn);
output_msg2 rif " = ";
Value.print stdout e;
output_msg "\n")
Value.print rif e;
output_msg2 rif "\n")
)
oracle_outputs;
if !n>0 then (
output_msg (
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 =
......@@ -918,8 +933,7 @@ and
(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;
output_string rif time_msg;
output_msg2 rif time_msg;
next_state
)
......
This diff is collapsed.
......@@ -11,7 +11,7 @@
(****************************************************************************)
(* exported *)
type atomic_ctrl_state = LucParse.node
type atomic_ctrl_state = string
type ctrl_state = atomic_ctrl_state list
......@@ -24,7 +24,8 @@ type wt = children Util.StringMap.t * string (* the top-level node of the wt *)
and children =
| Children of (dyn_weight * string) list
| Leave of Exp.formula
| Leave of Exp.formula * atomic_ctrl_state
| Stop of string
(****************************************************************************)
......@@ -114,7 +115,20 @@ let (compute_weight : Exp.weight -> Var.env_in -> state -> dyn_weight) =
| Some (Value.F _) -> assert false
(****************************************************************************)
type static_trans_list = (LucParse.node, LucParse.arc_info) Graph.t
type static_trans_list = (atomic_ctrl_state, LucParse.arc_info) Graph.t
(** exploit the internal naming convention to get the original name (XXX beurk). *)
let (get_original_name : atomic_ctrl_state -> atomic_ctrl_state) =
fun n ->
let res =
if String.sub n 0 1 <> "_" then n else
try
let idx = 2 + Str.search_forward (Str.regexp "__") n 0 in
String.sub n idx ((String.length n) - idx)
with _ -> assert false
in
res
(** Computes the weigthed tree from the static graph
......@@ -144,9 +158,9 @@ and
nb: it is safe to suppose that node does not begin by "__" because
I have renamed all nodes by adding the module name in parse_luc.
*)
(rename_node : LucParse.node -> int Util.StringMap.t -> LucParse.node * int Util.StringMap.t) =
(rename_node : atomic_ctrl_state -> int Util.StringMap.t -> atomic_ctrl_state * int Util.StringMap.t) =
fun node0 tbl ->
let node = try LucProg.get_original_name node0 with _ -> assert false in
let node = try get_original_name node0 with _ -> assert false in
let res =
try
let i = Util.StringMap.find node tbl in
......@@ -160,17 +174,17 @@ and
and
(get_children: Var.env_in -> LucProg.t -> state -> static_trans_list ->
Exp.formula -> bool -> LucParse.node -> children Util.StringMap.t * int Util.StringMap.t ->
Exp.formula -> bool -> atomic_ctrl_state -> children Util.StringMap.t * int Util.StringMap.t ->
children Util.StringMap.t * int Util.StringMap.t) =
fun input luc_prog state g facc toplevel n0 (tbl0, ntbl0) ->
let n_orig = (LucProg.get_original_name n0) in
let n_orig = (get_original_name n0) in
if
not (LucProg.is_node_transient n_orig luc_prog)
&& (not toplevel)
then
(* We stop the recursion when we encounter a stable node, except for
the top-level node (which can be stable obviously) *)
(Util.StringMap.add n0 (Leave facc) tbl0), ntbl0
(Util.StringMap.add n0 (Leave (facc, n_orig)) tbl0), ntbl0
else
let tnl = Graph.get_list_of_target_nodes g n_orig in
let child_list_formula, ntbl1 =
......@@ -248,8 +262,9 @@ and
print_string (":" ^ n ^ ", ");
)
l
| Leave f ->
print_string (Exp.formula_to_string f)
| Leave (f,next_state) ->
print_string ((Exp.formula_to_string f) ^ "->"^next_state)
| Stop str -> print_string ("Stop " ^ str)
(****************************************************************************)
let luc_to_dot graph csl1 csl2 file =
......
......@@ -9,7 +9,9 @@
*)
type atomic_ctrl_state
(* XXX should be abstract! *)
type atomic_ctrl_state = string
type ctrl_state = atomic_ctrl_state list
......@@ -21,8 +23,8 @@ type dyn_weight = V of int | Infin
type wt = children Util.StringMap.t * string (* the top-level node of the wt *)
and children =
| Children of (dyn_weight * string) list
| Leave of Exp.formula
| Leave of Exp.formula * atomic_ctrl_state
| Stop of string
(** The Digested Lucky program (form the static part of the state).
Holds a list of independant programs (i.e., they don't share any I/O).
......@@ -82,3 +84,5 @@ val ctrl_state_to_string_long : ctrl_state list -> string
val print_mem : state -> unit
val string_to_atomic_ctrl_state : string -> atomic_ctrl_state
val get_original_name : LucParse.node -> LucParse.node
......@@ -1064,11 +1064,8 @@ and (add_eq_to_store : t -> Ne.t -> t) =
(Value.mult_num coef_neg vn_max,
Value.mult_num coef_neg vn_min)
in
let cstr_min =
Ineq (GeqZ(Ne.diff ne_rest (Ne.make "" vn_min1)))
and cstr_max =
Ineq (GeqZ(Ne.diff (Ne.make "" vn_max1) ne_rest))
in
let cstr_min = Ineq (GeqZ(Ne.diff ne_rest (Ne.make "" vn_min1)))
and cstr_max = Ineq (GeqZ(Ne.diff (Ne.make "" vn_max1) ne_rest)) in
let new_store_var =
(* We do not need the bounds of [vn] anymore *)
Range(StringMap.remove vn tbl)
......