Commit 69ac49f9 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Add a --oracle-ec option to lutin.

This was done by moving most of the code from checkRif.ml to
lustreRun.ml (new module) and coverage.ml, so that checkRif only
contains administration stuff (dealing with options) plus a simple
top-level loop.

I've added some tests in exemple/lutin/oracle.
parent 2d1cd4ed
......@@ -45,6 +45,7 @@ test-lutin:
cd lutin/lustre && make test ;
cd lutin/test_ok && make test ;
cd lutin/C && make test;
cd lutin/oracle && make test;
echo "All lutin tests ran correctly."
# problem ~
......
#
# Testing the use of the --oracle-* option
#
EXE=
ifeq ($(HOSTTYPE),win32)
EXE=.exe
endif
LUTIN=../../../$(HOSTTYPE)/bin/lutin$(EXE) -seed 1
test : test1 test2
not_a_sauna.ec: heater_control.lus
lus2lic -n not_a_sauna -ec $< -o $@
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//" > 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" | \
$(LUTIN) env.lut -main main --oracle-ec $< | sed -e "s/^M//" > test2.rif
rm -f test2.res && diff -B -u -i -w test2.rif.exp test2.rif > test2.res
[ ! -s test2.res ] && make clean
utest1:
cp test1.rif test1.rif.exp ; true
utest2:
cp test2.rif test2.rif.exp ; true
utest:utest1 utest2
clean:
rm -rf $(OBJDIR) rm -rf *.res *.log *~ *.rif0 *.rif *.gp *.plot *.ec *.cov
let between(x, min, max : real) : bool =
((min < x) and (x < max))
node main(Heat_on : bool) returns (
T : real;
T1 : real;
T2 : real;
T3 : real) =
assert between(T1, T-1.5, T + 1.5) in
assert between(T2, T-1.5, T + 1.5) in
assert between(T3, T-1.5, T + 1.5) in
{
(6.0 < T) and (T < 9.0)
}
fby
loop { if Heat_on then
between(T, pre T, pre T + 0.5)
else
between(T, pre T - 0.5, pre T)
}
--
-- A fault-tolerant heater controller with 3 sensors.
--
-- To guess the temperature (T),
--
-- (1) It compares the value of the 3 sensors 2 by 2 to determine
-- which ones seem are broken -- we consider then broken if they
-- differ too much.
--
-- (2) then, it performs a vote:
-- o If the tree sensors are broken, it does not heat;
-- o If the temperature is bigger than TMAX, it does not heat;
-- o If the temperature is smaller than TMIN, it heats;
-- o Otherwise, it keeps its previous state.
const FAILURE = - 999.0; -- a fake temperature given when all sensors are broken
const TMIN = 6.0;
const TMAX = 9.0;
const DELTA = 0.5;
-- const DELTA : real;
-----------------------------------------------------------------------
-----------------------------------------------------------------------
node heater_control(T, T1, T2, T3 : real) returns (Heat_on:bool);
-- T is supposed to be the real temperature and is not
-- used in the controller; we add it here in oder to test the
-- controller to be able to write a sensible oracle.
var
V12, V13, V23 : bool;
Tguess : real;
let
V12 = abs(T1-T2) < DELTA; -- Are T1 and T2 valid?
V13 = abs(T1-T3) < DELTA; -- Are T1 and T3 valid?
V23 = abs(T2-T3) < DELTA; -- Are T2 and T3 valid?
Tguess =
if noneoftree(V12, V13, V23) then FAILURE else
if oneoftree(V12, V13, V23) then Median(T1, T2, T3) else
if alloftree(V12, V13, V23) then Median(T1, T2, T3) else
-- 2 among V1, V2, V3 are false
if V12 then Average(T1, T2) else
if V13 then Average(T1, T3) else
-- V23 is necessarily true, hence T1 is wrong
Average(T2, T3) ;
Heat_on = true ->
if Tguess = FAILURE then false else
if Tguess < TMIN then true else
if Tguess > TMAX then false else
pre Heat_on;
tel
-----------------------------------------------------------------------
-----------------------------------------------------------------------
node not_a_sauna(T, T1, T2, T3 : real; Heat_on: bool) returns (ok, C1, C2, C3:bool);
let
-- Some stupid coverage criteria...
C1 = T > T1;
C2 = T > T2;
C3 = T > T3;
ok =
(C1 => (T < TMAX + 1.0)) and
(C2 => (T < TMAX + 1.0)) and
(C3 => (T < TMAX + 1.0)) ;
tel
node not_a_fridge(T, T1, T2, T3 : real; Heat_on: bool) returns (ok:bool);
let
ok = true -> pre T < TMAX - 6.0 ;
tel
-----------------------------------------------------------------------
-----------------------------------------------------------------------
-- returns the absolute value of 2 reals
node abs (v : real) returns (a : real) ;
let
a = if v >= 0.0 then v else -v ;
tel
-- returns the average values of 2 reals
node Average(a, b: real) returns (z : real);
let
z = (a+b)/2.0 ;
tel
-- returns the median values of 3 reals
node Median(a, b, c : real) returns (z : real);
let
z = a + b + c - min2 (a, min2(b,c)) - max2 (a, max2(b,c)) ;
tel
-- returns the maximum values of 2 reals
node max2 (one, two : real) returns (m : real) ;
let
m = if one > two then one else two ;
tel
-- returns the minimum values of 2 reals
node min2 (one, two : real) returns (m : real) ;
let
m = if one < two then one else two ;
tel
node noneoftree (f1, f2, f3 : bool) returns (r : bool)
let
r = not f1 and not f2 and not f3 ;
tel
node alloftree (f1, f2, f3 : bool) returns (r : bool)
let
r = f1 and f2 and f3 ;
tel
node oneoftree (f1, f2, f3 : bool) returns (r : bool)
let
r = f1 and not f2 and not f3 or
f2 and not f1 and not f3 or
f3 and not f1 and not f2 ;
tel
#inputs "Heat_on":bool
#outputs "T":real "T1":real "T2":real "T3":real
#step 1
#outs 6.03 5.86 4.58 6.22
#step 2
#outs 6.31 7.29 7.71 5.73
#step 3
#outs 6.71 6.01 5.79 7.50
#step 4
#outs 7.11 5.73 8.09 8.23
#step 5
#outs 7.52 6.25 6.30 8.65
#step 6
#outs 7.80 8.42 7.13 7.04
#step 7
#outs 8.17 8.75 6.81 9.53
#step 8
#outs 8.55 7.70 8.05 9.66
#step 9
#outs 8.72 8.72 7.34 10.10
#step 10
#outs 9.17 10.41 10.60 7.75
#step 11
#outs 9.39 9.31 9.58 10.05
#step 12
#outs 9.51 8.50 10.52 8.38
#step 13
#outs 9.99 8.52 11.48 10.11
#step 14
#outs 10.30 9.87 11.27 9.45
The oracle returned false at step 14
#inputs "Heat_on":bool
#outputs "T":real "T1":real "T2":real "T3":real
#step 1
#outs 6.03 5.86 4.58 6.22
#step 2
#outs 5.81 6.79 7.21 5.23
#step 3
#outs 6.21 5.51 5.29 7.00
#step 4
#outs 6.11 4.73 7.09 7.23
#step 5
#outs 6.52 5.25 5.30 7.65
#step 6
#outs 6.30 6.92 5.63 5.54
#step 7
#outs 6.67 7.25 5.31 8.03
#step 8
#outs 6.55 5.70 6.05 7.66
#step 9
#outs 6.72 6.72 5.34 8.10
#step 10
#outs 6.67 7.91 8.10 5.25
#step 11
#outs 6.89 6.81 7.08 7.55
#step 12
#outs 6.51 5.50 7.52 5.38
#step 13
#outs 6.99 5.52 8.48 7.11
#step 14
#outs 6.80 6.37 7.77 5.95
#step 15
#outs 6.99 8.42 7.36 5.55
#step 16
#outs 6.52 6.22 6.09 5.42
#step 17
#outs 6.71 6.01 7.06 7.22
#step 18
#outs 6.23 7.71 5.62 4.76
#step 19
#outs 6.45 6.54 7.41 5.18
#step 20
#outs 6.40 5.12 5.10 7.62
#step 21
#outs 6.89 7.39 8.37 6.39
#step 22
The coverage file not_a_sauna.cov has been generated
......@@ -105,6 +105,10 @@ LURETTE_SOURCES=\
$(OBJDIR)/rif_base.ml \
$(OBJDIR)/rif.mli \
$(OBJDIR)/rif.ml \
$(OBJDIR)/coverage.mli \
$(OBJDIR)/coverage.ml \
$(OBJDIR)/lustreRun.mli \
$(OBJDIR)/lustreRun.ml \
......
This diff is collapsed.
......@@ -59,6 +59,25 @@ let gen_mode () = !_gen_mode
let _boot = ref false
let boot () = !_boot
type oracle =
NoOracle
| Oracle of
(string * string) list *
(string * string) list *
(unit -> unit) *
(Rif_base.subst list -> Rif_base.subst list)
let _oracle = ref NoOracle
let oracle () = !_oracle
let _oracle_file = ref ""
let oracle_file () = !_oracle_file
let _cov_file = ref ""
let cov_file () = !_cov_file
let _reset_cov = ref false
let reset_cov () = !_reset_cov
let _draw_mode = ref Lucky.StepInside
let draw_mode () = !_draw_mode
......@@ -188,32 +207,32 @@ let mkoptab () = (
["-m";"-main"]
~arg:" <string>"
(Arg.String(function s -> _main_node := s))
["set main node"]
["Set the main node"]
;
mkopt
["-version"]
(Arg.Unit(function _ -> print_string version; exit 0))
["print the current version then exit"]
["Print the current version and exit"]
;
(* verbose *)
mkopt
["-v"]
(Arg.Unit(function _ -> Verbose.on () ))
["set verbose mode"]
["Set the verbose level to 1"]
;
mkopt
["-vl"]
~arg:" <int>"
(Arg.Int(function i -> Verbose.set i))
["set verbose level"]
["Set the verbose level"]
;
(* ---- COMPILE OPTIONS *)
mkopt
["-luc"]
(Arg.Unit(function _ -> _gen_mode := GenLuc ; ()))
["generate a lucky program"]
["Generate a lucky program"]
;
mkopt
mkopt (* XXX Merge it with -luc !!! *)
["-o"]
~arg:" <string>"
(Arg.String(function s -> _outfile := Some s))
......@@ -231,22 +250,46 @@ let mkoptab () = (
_riffile := Some s;
Luc2c.option.Luc2c.rif <- Some s
))
["save the generated data in a file using the RIF format"]
["Save the generated data using the RIF format"]
;
mkopt
["--oracle-ec"]
~arg:" <.ec file>"
(Arg.String(function f ->
let i,o,kill,step = LustreRun.make_ec f in
if !_cov_file = "" then _cov_file := (Filename.chop_extension f) ^ ".cov";
_oracle_file := f;
_oracle := Oracle(i,o,kill,step)
))
["Check the lutin I/O against the oracle (.ec)";
"The oracle inputs should be included in the set of the lutin I/O. "]
;
mkopt
["--cov"]
~arg:" <cov file>"
(Arg.String(function f -> _cov_file := f))
["Override the default coverage file name (<oracle name>.cov by default)"]
;
mkopt
["--reset-cov"]
(Arg.Unit(function f -> _reset_cov := true))
["Reset the coverage rate before running"]
;
mkopt
["-L"; "-lib"]
~arg:"<string>"
~arg:" <string>"
(Arg.String(function s -> _libs := s::!_libs))
["add a dynamic library where to search for external code"]
["Add a dynamic library where external code will be searched in"]
;
(* ---- SIMU/SOLVER OPTIONS *)
(* simu *)
mkopt
["-b";"-boot"]
(Arg.Set _boot)
["perform a first step without requiring inputs";
("fails if inputs are actually required at first step (default: "
["Perform a first step without requiring inputs";
("Fails if inputs are actually required at first step (default: "
^(if !_boot then "on" else "off")^")")
]
......@@ -255,55 +298,55 @@ let mkoptab () = (
["-seed"]
~arg:" <int>"
(Arg.Int(function i -> _seed := Some i ; ()))
["set a seed for the pseudo-random generator"]
["Set a seed for the pseudo-random generator"]
;
mkopt
["-l"; "--max-steps"]
~arg:" <int>"
(Arg.Int(function i -> _max_steps := Some i ; ()))
["set a maximum number of simulation steps to perform"]
["Set a maximum number of simulation steps to perform"]
;
mkopt
["--step-inside"]
(Arg.Unit(function _ -> _draw_mode := Lucky.StepInside))
["draw inside the convex hull of solutions (default)"]
["Draw inside the convex hull of solutions (default)"]
;
mkopt
["--step-edges"]
(Arg.Unit(function _ -> _draw_mode := Lucky.StepEdges))
(* "draw inside the convex hull of solutions, but a little bit more at edges and vertices" *)
["draw a little bit more at edges and vertices"]
["Draw a little bit more at edges and vertices"]
;
mkopt
["--step-vertices"]
(Arg.Unit(function _ -> _draw_mode := Lucky.StepVertices))
["draw among the vertices of the convex hull of solutions"]
["Draw among the vertices of the convex hull of solutions"]
;
mkopt
["-fair"; "--compute-poly-volume"]
(Arg.Set _compute_volume)
[ "Compute polyhedron volume before drawing";
"more fair, but more expensive"
"More fair, but more expensive"
];
mkopt
["-precision";"-p"]
(Arg.Set_int Util.precision)
~arg:" <int>"
[ "precision used for converting float to rational (default: "^(string_of_int !Util.precision)^")"
[ "Set the precision used for converting float to rational (default: "^(string_of_int !Util.precision)^")"
];
mkopt
["-locals";"-loc"]
(Arg.Set _show_locals)
[ "show local variables"
[ "Show local variables in the generated data."
];
(* ---- luc2c OPTIONS *)
mkopt
["--2c-4c"]
(Arg.Unit(fun () ->
_gen_mode := Cstubs;
Luc2c.option.Luc2c.gen_mode <- Luc2c.Nop))
["generate C code to be called from C "];
_gen_mode := Cstubs;
Luc2c.option.Luc2c.gen_mode <- Luc2c.Nop))
["Generate C code to be called from C "];
mkopt ~hide:true
["--2c-4c-socks"]
......@@ -312,8 +355,8 @@ let mkoptab () = (
_gen_mode := Cstubs;
Luc2c.option.Luc2c.use_sockets <- true;
Luc2c.option.Luc2c.sock_addr <- str
))
["the same as --2c-4c, but using lutin via sockets."]
))
["The same as --2c-4c, but using sockets."]
;
mkopt
......@@ -323,7 +366,7 @@ let mkoptab () = (
_gen_mode := Cstubs;
Luc2c.option.Luc2c.gen_mode <- Luc2c.Lustre;
Luc2c.option.Luc2c.calling_module_name <- str))
["generate C code to be called from Lustre V4 "];
["Generate C code to be called from Lustre V4 "];
mkopt
["--2c-4scade"]
......@@ -332,14 +375,14 @@ let mkoptab () = (
_gen_mode := Cstubs;
Luc2c.option.Luc2c.gen_mode <- Luc2c.Scade;
Luc2c.option.Luc2c.calling_module_name <- str))
["generate C code to be called from Scade "];
["Generate C code to be called from Scade "];
mkopt
["--2c-4luciole"]
(Arg.Unit(fun _ ->
_gen_mode := Cstubs;
Luc2c.option.Luc2c.gen_mode <- Luc2c.Luciole))
["generate a C file containing the necessary stuff to call the lucky file with luciole"];
["Generate a C file containing the necessary stuff to call the lucky file with luciole"];
mkopt
["--2c-4alice"]
......@@ -348,92 +391,90 @@ let mkoptab () = (
_gen_mode := Cstubs;
Luc2c.option.Luc2c.gen_mode <- Luc2c.Alice;
Luc2c.option.Luc2c.calling_module_name <- str))
["generate C and C++ code to be called from Alice"];
["Generate C and C++ code to be called from Alice"];
mkopt
["--2c-output-dir"]
~arg:" <string>"
(Arg.String(fun str -> Luc2c.option.Luc2c.output_dir <- str))
["Directory where C files are generated"];
["Set the directory where C files are generated"];
mkopt
["-h";"-help"; "--help"]
(Arg.Unit help)
["Display this message"]
;
(* to show Hidden opt *)
mkopt
["-more"]
(Arg.Unit(fun _ -> _see_all_options := true))
["show hidden options (for dev purposes)"];
["Show hidden options (for dev purposes)"];
(* HIDDEN *)
(* test lexical *)
mkopt ~hide:true
["-tlex"]
(Arg.Unit(function _ -> _gen_mode := GenLuc ; _test_lex := true ; ()))
["TEST lexical analysis"]
["Test the lexical analysis"]
;
(* test syntaxique *)
mkopt ~hide:true
["-tparse"]
(Arg.Unit(function _ -> _gen_mode := GenLuc ; _test_parse := true ; ()))
["TEST syntactic analysis"]
["Test the syntactic analysis"]
;
(* test type-checking *)
mkopt ~hide:true
["-tcheck"]
(Arg.Unit(function _ -> _gen_mode := GenLuc ; _test_check := true ; ()))
["TEST type/binding checking"]
["Test the type/binding checking"]
;
(* test expansion *)
mkopt ~hide:true
["-texpand"]
(Arg.Unit(function _ -> _gen_mode := GenLuc ; _test_expand := true ; ()))
["TEST expansion"]
["Test the expansion"]
;
(* test autogen *)
mkopt ~hide:true
["-tauto"]
(Arg.Unit(function _ -> _gen_mode := GenLuc ; _test_auto := true ; ()))
["test automaton generation"]
["Test the automaton generation"]
;
(* test new LutExe based simu *)
mkopt ~hide:true
["-exe"]
(Arg.Unit(function _ -> _gen_mode := Simu; _test_exe := true ; ()))
["simulation with LutExe based algo"]
;
mkopt ~hide:true
["-h";"-help"; "--help"]
(Arg.Unit help)
[]
["Simulation with LutExe based algo"]
;
(* paranoid/debug *)
mkopt ~hide:true
["-paranoid"]
(Arg.Unit(function _ -> Utils.set_paranoid ()))
["paranoid mode (slow)"]
["Set on the paranoid mode (slower)"]
;