Commit ccb14ac1 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

A lot of work on the new execution mode for lurettetop (a.k.a, the direct mode).

In the short term, it will be the only supported mode. The idea is to
run lurette test session without generating any lurette_exe
executable.

It's not finished, but yet usable.
parent 1889ad3b
......@@ -200,6 +200,141 @@ endif
endif
endif
LURETTE_SOURCES_C = \
$(OBJDIR)/liblutin_c.c \
$(OBJDIR)/liblutin.idl \
$(OBJDIR)/Ezdl_c.c \
LURETTE_SOURCES=\
$(OBJDIR)/util.ml \
$(OBJDIR)/util2.ml \
$(OBJDIR)/error.ml \
$(OBJDIR)/graphUtil.ml \
$(OBJDIR)/graphUtil.mli \
$(OBJDIR)/sol_nb.mli \
$(OBJDIR)/sol_nb.ml \
$(OBJDIR)/graph.ml \
$(OBJDIR)/graph.mli \
$(OBJDIR)/genlex.mli \
$(OBJDIR)/genlex.ml \
$(OBJDIR)/Ezdl.ml \
$(OBJDIR)/Ezdl.mli \
$(OBJDIR)/type.ml \
$(OBJDIR)/type.mli \
$(OBJDIR)/prevar.ml \
$(OBJDIR)/prevar.mli \
$(OBJDIR)/value.ml \
$(OBJDIR)/value.mli \
$(OBJDIR)/var.ml \
$(OBJDIR)/var.mli \
$(OBJDIR)/exp.ml \
$(OBJDIR)/exp.mli \
$(OBJDIR)/ne.mli \
$(OBJDIR)/ne.ml \
$(OBJDIR)/constraint.ml \
$(OBJDIR)/constraint.mli \
$(OBJDIR)/lustreExp.ml \
$(OBJDIR)/lustreExp.mli \
$(OBJDIR)/parser.mly \
$(OBJDIR)/lexer.mll \
$(OBJDIR)/gne.mli \
$(OBJDIR)/gne.ml \
$(OBJDIR)/thickness.ml \
$(OBJDIR)/poly_draw.mli \
$(OBJDIR)/poly_draw.ml \
$(OBJDIR)/polyhedron.mli \
$(OBJDIR)/polyhedron.ml \
$(OBJDIR)/formula_to_bdd.mli \
$(OBJDIR)/formula_to_bdd.ml \
$(OBJDIR)/store.mli \
$(OBJDIR)/store.ml \
$(OBJDIR)/draw.mli \
$(OBJDIR)/draw.ml \
$(OBJDIR)/bddd.mli \
$(OBJDIR)/bddd.ml \
$(OBJDIR)/fair_bddd.mli \
$(OBJDIR)/fair_bddd.ml \
$(OBJDIR)/solver.mli \
$(OBJDIR)/solver.ml \
$(OBJDIR)/prog.ml \
$(OBJDIR)/prog.mli \
$(OBJDIR)/fGen.mli \
$(OBJDIR)/fGen.ml \
$(OBJDIR)/lucFGen.mli \
$(OBJDIR)/lucFGen.ml \
$(OBJDIR)/lucky.mli \
$(OBJDIR)/lucky.ml \
$(OBJDIR)/rif_base.mli \
$(OBJDIR)/rif_base.ml \
$(OBJDIR)/rif.mli \
$(OBJDIR)/rif.ml \
$(OBJDIR)/coverage.mli \
$(OBJDIR)/coverage.ml \
$(OBJDIR)/lustreRun.mli \
$(OBJDIR)/lustreRun.ml \
LUTIN_SOURCES = \
$(OBJDIR)/version.ml \
$(OBJDIR)/lutVersion.ml \
$(OBJDIR)/lexeme.mli \
$(OBJDIR)/lexeme.ml \
$(OBJDIR)/utils.ml \
$(OBJDIR)/utils.mli \
$(LURETTE_SOURCES_C) \
$(LURETTE_SOURCES) \
$(OBJDIR)/expEval.mli \
$(OBJDIR)/expEval.ml \
$(OBJDIR)/verbose.ml \
$(OBJDIR)/verbose.mli \
$(OBJDIR)/errors.ml \
$(OBJDIR)/$(ZELANG)Parser.mly \
$(OBJDIR)/$(ZELANG)Lexer.mll \
$(OBJDIR)/syntaxe.ml \
$(OBJDIR)/parsers.ml \
$(OBJDIR)/parsers.mli \
$(OBJDIR)/syntaxeDump.ml \
$(OBJDIR)/ckTypeEff.ml \
$(OBJDIR)/ckTypeEff.mli \
$(OBJDIR)/ckIdentInfo.ml \
$(OBJDIR)/ckIdentInfo.mli \
$(OBJDIR)/checkEnv.ml \
$(OBJDIR)/checkEnv.mli \
$(OBJDIR)/predef.ml \
$(OBJDIR)/checkType.ml \
$(OBJDIR)/coIdent.mli \
$(OBJDIR)/coIdent.ml \
$(OBJDIR)/coAlgExp.mli \
$(OBJDIR)/coAlgExp.ml \
$(OBJDIR)/coTraceExp.mli \
$(OBJDIR)/coTraceExp.ml \
$(OBJDIR)/glue.mli \
$(OBJDIR)/glue.ml \
$(OBJDIR)/guard.ml \
$(OBJDIR)/guard.mli \
$(OBJDIR)/expand.ml \
$(OBJDIR)/expand.mli \
$(OBJDIR)/loopWeights.mli \
$(OBJDIR)/loopWeights.ml \
$(OBJDIR)/lutExe.mli \
$(OBJDIR)/lutExe.ml \
$(OBJDIR)/autoExplore.ml \
$(OBJDIR)/autoExplore.mli \
$(OBJDIR)/autoGen.ml \
$(OBJDIR)/autoGen.mli \
$(OBJDIR)/auto2Lucky.ml \
$(OBJDIR)/auto2Lucky.mli \
$(OBJDIR)/show_env.ml \
$(OBJDIR)/show_env.mli \
$(OBJDIR)/lucParse.ml \
$(OBJDIR)/lucParse.mli \
$(OBJDIR)/lutProg.ml \
$(OBJDIR)/lutProg.mli \
$(OBJDIR)/lucProg.ml \
$(OBJDIR)/lucProg.mli \
$(OBJDIR)/luciole.ml \
$(OBJDIR)/luc2alice.ml \
$(OBJDIR)/luc2c.mli \
$(OBJDIR)/luc2c.ml
LUTIN_FILES = \
$(OBJDIR)/lutVersion.ml \
......
......@@ -5,6 +5,8 @@ let abs_real(x: real) = if x>=0.0 then x else -x
node main(a:int; b:bool; c:real) returns ( x:int; y:bool; z:real) =
z=0.0 and x = 0
fby
loop
{
(b=>y) and abs_int(x - a) < 5 and abs_real(z - c) < 5.0
......
#inputs "a":int "b":bool "c":real
#outputs "x":int "y":bool "z":real
# step 1
1 1 1.000000 #outs -1 1 -1.810000
1 1 1.000000 #outs 0 1 0.000000
# step 2
2 0 2.000000 #outs 6 0 5.690000
2 0 2.000000 #outs -2 1 1.610000
# step 3
3 1 3.000000 #outs 5 1 2.040000
3 1 3.000000 #outs 1 1 -0.960000
# step 4
4 0 4.000000 #outs 3 0 7.970000
4 0 4.000000 #outs 3 0 3.330000
# step 5
5 1 5.000000 #outs 7 1 4.810000
5 1 5.000000 #outs 6 1 6.510000
# step 6
6 0 6.000000 #outs 4 1 6.990000
6 0 6.000000 #outs 8 0 2.890000
# step 7
7 1 7.000000 #outs 3 1 9.590000
7 1 7.000000 #outs 4 1 10.120000
# step 8
8 0 8.000000 #outs 7 0 9.140000
8 0 8.000000 #outs 9 0 12.570000
# step 9
9 1 9.000000 #outs 8 1 5.030000
9 1 9.000000 #outs 13 1 7.670000
......@@ -19,6 +19,29 @@ test:
[ ! -s test.res ] && make clean
sut:
call-via-socket -addr 127.0.0.1 -port 2000 -server ./not_a_sauna.sh
xxx:
$(LTOP) --precision 2 \
-rp "oracle:socket:127.0.0.1:2000" \
-rp "env:lutin:env.lut:main" \
-rp "sut:v6:heater_control.lus:heater_control" \
--no-sim2chro --seed 3 \
--do-not-show-step -v 3 --output test.rif --direct
xxx2:
$(LTOP) --precision 2 \
-rp "sut:v6:heater_control.lus:heater_control" \
-rp "oracle:v6:heater_control.lus:not_a_sauna" \
-rp "env:lutin:env.lut:main" \
--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 -v 3 --output test.rif --direct
utest:
cp test.rif test.rif.exp
......
......@@ -5,18 +5,8 @@ let abs(x : real) : real =
if x > 0.0 then x else -x
let up_and_down(x : real ref; min, max, delta : real) =
exist px : real in
assert px = pre x in
if (pre x < min) or (
(pre x < max) and (pre px <= pre x)
) then (
between(x, pre x, pre x + delta)
) else (
between(x, pre x - delta, pre x)
)
node toto(t:real) returns ( y:real [ -1e50 ; 1e50]) =
loop {y = t}
node main(Heat_on : bool) returns (
T : real;
......@@ -28,10 +18,12 @@ assert abs(T-T1) < 0.5 in
assert abs(T-T2) < 0.5 in
assert abs(T-T3) < 0.5 in
loop [2]
{
(6.0 < T) and (T < 9.0)
}
between(T, 6.0, 9.0)
fby
loop { up_and_down(T, 6.0, 9.0, 0.2) }
assert (abs(T - pre T) < 1.0 ) in
loop
{ if Heat_on then T >= pre T else T <= pre T }
......@@ -14,7 +14,7 @@
-- o Otherwise, it keeps its previous state.
const FAILURE = - 999.0; -- a fake temperature given when all sensors are broken
const FAILURE = -999.0; -- a fake temperature given when all sensors are broken
const TMIN = 6.0;
const TMAX = 9.0;
......
......@@ -5,22 +5,37 @@
include $(LURETTE_PATH)/Makefile.common.source
include $(LURETTE_PATH)/source/Makefile.ln
LIBS = unix str
CLIBS =
OCAMLFLAGS += -I $(OBJDIR) -I $(OCAMLLIB) -I $(PREFIX)/$(HOSTTYPE)/lib
IDLFLAGS=-nocpp
POLKA=polkag
ifdef STATIC
OCAMLLDFLAGS = -cclib -ldl -cclib -lm -cclib -lc -ccopt -static
OCAMLLDFLAGS = -cclib -lstdc++ -cclib -lm -cclib -lc -ccopt -static\
-cclib -l$(POLKA)_caml -cclib -l$(POLKA) -cclib -lgmp $(OCAMLOPTFLAG)
else
OCAMLLDFLAGS= -cclib -lstdc++ -cclib -I/usr/lib/w32api \
-cclib -l$(POLKA)_caml \
-cclib -l$(POLKA) -cclib -lgmp $(OCAMLOPTFLAG)
endif
CC= $(GCC) $(DWIN32)
LIBS = unix str nums polka bdd
CLIBS = camlidl $(CLIBS_WIN32) bdd_stubs
#USE_CAMLP4 = yes
ZELANG=lut
USE_CAMLP4 = yes
SOURCES = \
$(OBJDIR)/genlex.mli $(OBJDIR)/genlex.ml \
$(OBJDIR)/version.ml \
$(OBJDIR)/util.ml \
$(OBJDIR)/util2.ml \
SOURCES = $(LUTIN_SOURCES) \
$(OBJDIR)/ltopArg.ml \
$(OBJDIR)/ocaml.mli \
$(OBJDIR)/ocaml.ml \
......@@ -30,6 +45,8 @@ SOURCES = \
$(OBJDIR)/build.ml \
$(OBJDIR)/runBin.mli \
$(OBJDIR)/runBin.ml \
$(OBJDIR)/runDirect.mli \
$(OBJDIR)/runDirect.ml \
$(OBJDIR)/runPipe.mli \
$(OBJDIR)/runPipe.ml \
$(OBJDIR)/run.mli \
......
......@@ -24,7 +24,7 @@ let chop_ext = Util.chop_ext_no_excp
(* XXX bien compliqué tout ca. A reprendre proprement *)
let (f : LtopArg.t -> bool) =
fun args ->
if args.sut_compiler = Stdin then true else
if args.sut_compiler = Stdin || args.direct_mode then true else
let sut_path = Filename.concat args.sut_dir args.sut in
let _ =
check_config_types_exist args;
......
......@@ -17,9 +17,9 @@ user queries. One first need at least to set the sut (system
under test) and the environement fields like that:
[your shell prompt] lurettetop
<lurette> set_sut my_program_to_test
<lurette> set_oracle my_oracle
<lurette> set_env my_env_file1 my_env_file2 my_env_file3
<lurette> add_rp \"sut:v6:heater_control.lus:heater_control\"
<lurette> add_rp \"oracle:v6:heater_control.lus:not_a_sauna\"
<lurette> add_rp \"env:lutin:env.lut:main\"
And then the testing process can start:
......@@ -28,9 +28,9 @@ And then the testing process can start:
Equivalently, you can directly set values at the command line:
[your shell prompt] lurettetop --sut my_program_to_test \\
--oracle my_oracle \\
my_env_file1 my_env_file2 x my_env_file3
[your shell prompt] lurettetop -rp \"sut:v6:heater_control.lus:heater_control\"
-rp \"oracle:v6:heater_control.lus:not_a_sauna\"
-rp \"env:lutin:env.lut:main\"
<lurette> run
... [... testing ...]
"
......@@ -47,81 +47,83 @@ run, r
quit q, bye
to quit the lurette top level
help, h, ?
display this list of commands
man
display a small user manual
clean
clean-up temporary files (you can try it if <<run>> failed)
show
show of post-script version of the current environment
set_env \"<env (env)+>\" (env=<file name>)
to set the environment field (.luc files). Automata of
environments separated by \"x\" are multiplied.
The current value of this field is "
^
(if args.env = ""
then "Unset!"
else ("\"" ^ args.env ^ "\" ")) ^ "
set_sut <file name> [<sut file name> <main node name>]
to set the sut field. Its current value is " ^
(if args.sut = ""
then "Unset!"
else("\"" ^ args.sut ^ " " ^ args.sut_node ^ "\"")) ^ "
set_sut_cmd \"shell command\"
to set the sut field in stdin/stdout mode. Its current value is " ^
(if args.sut_cmd = ""
then "Unset!"
else("\"" ^ args.sut_cmd ^ "\"")) ^ "
set_oracle <file name> [<oracle file name> <main node name>]
to set the oracle field. Its current value is " ^
(match args.oracle with
None -> "unset"
| Some str -> ("\"" ^ str ^ " " ^ args.oracle_node ^ "\"")) ^ "
set_oracle_cmd <shell command>
to set the oracle field in stdin/stdout mode. Its current value is " ^
(if args.oracle_cmd = ""
then "Unset!"
else("\"" ^ args.oracle_cmd ^ "\"")) ^ "
set_sut_compiler <string>
to set the compiler used for the sut. Its current value is " ^
(match args.sut_compiler with
| VerimagV4 -> "\"lv4\""
| VerimagV6 -> "\"lv6\""
| Scade -> "\"scade\""
| ScadeGUI -> "\"scade-gui\""
| Sildex -> "\"sildex\""
| Stdin -> "\"stdin\""
| Ocaml -> "\"ocaml\""
) ^ "
set_oracle_compiler <string>
to set the compiler used for the oracle. Its current value is " ^
(match args.oracle_compiler with
| VerimagV4 -> "\"lv4\""
| VerimagV6 -> "\"lv6\""
| Scade -> "\"scade\""
| ScadeGUI -> "\"scade-gui\""
| Sildex -> "\"sildex\""
| Stdin -> "\"stdin\""
| Ocaml -> "\"ocaml\""
) ^ "
set_test_length <integer>
to set the test length. Its current value is \"" ^
add_rp "^rp_help^"
The current value of the rp fields 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)) ^ "
reset_rp sut
Reset the sut field. Its current value is: "
^ (String.concat "," (List.map reactive_program_to_string args.suts)) ^ "
reset_rp env
Reset the env field. Its current value is: "
^ (String.concat "," (List.map reactive_program_to_string args.envs)) ^ "
reset_rp oracle
Reset the oracle field. Its current value is: "
^ (String.concat "," (List.map reactive_program_to_string args.oracles)) ^ "
stl <integer>, set_test_length <integer>
Set the test length. Its current value is \"" ^
(string_of_int args.step_nb) ^ "\"
set_precision <int>
to set te number of digit after the dot used for real computation.
current precision is " ^ (string_of_int args.precision) ^ "
set_seed <integer>
to set the seed the random engine is initialised with.
Its current value is " ^ (match args.seed with
None -> "chose randomly"
| Some i -> ("\"" ^ (string_of_int i) ^ "\"")) ^ "
set_seed_randomly
to let the system set a seed randomly.
set_verbose (0,1,2)
to set on and off a verbose mode. Its current value is "
^ (string_of_int (args.verbose)) ^ "
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
call sim2chro to visualize (rif) data
gnuplot
gnuplot_ps
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.
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.
"
in
output_string args.ocr msg;
flush args.ocr
let (display2 : unit -> unit) =
fun _ ->
let msg = "The advanced commands are:
set_draw_nb <integer>
to set the number of draw to be done in each formula at each step
......@@ -163,29 +165,10 @@ set_compute_volume <Boolean>
to set a Boolean that indicates whether lurette should compute
polyhedra volumes (achieve fairness, but more expensive).
Its current value is "
^ (if !(args.compute_volume)
^ (if (args.compute_volume)
then "\"true\""
else "\"false\"") ^ "
set_precision <int>
to set te number of digit after the dot used for real computation.
current precision is " ^ (string_of_int args.precision) ^ "
set_preprocessor <string>
to set the pre-processot used for Lucky files.
current pre processor is " ^
(match args.pp with
None -> "None"
| Some pp -> "\"" ^ pp ^ "\"") ^ "
set_seed <integer>
to set the seed the random engine is initialised with.
Its current value is " ^ (match args.seed with
None -> "chose randomly"
| Some i -> ("\"" ^ (string_of_int i) ^ "\"")) ^ "
set_seed_randomly
to let the system set a seed randomly.
set_extra_source_files <string>
to set the EXTRA_SOURCE_FILES environment variable.
Its current value is " ^
......@@ -213,43 +196,9 @@ set_extra_includedirs <string>
(match args.extra_includedirs with
None -> "unset"
| Some str -> ("\"" ^ str ^ "\"")) ^ "
set_step_by_step <int>
to set the step_by_step mode on. " ^
(match !(args.step_by_step) with
None -> "This mode is currently off."
| Some i -> ("\"Its current value is "^ (string_of_int i) ^" \"")) ^ "
set_step_by_step_off
to set the step_by_step mode off.
set_display_sim2chro <boolean>
to set a flag saying whether or not sim2chro is called when
lurette resumes. Its current value is "
^ (if !(args.display_sim2chro)
then "\"true\""
else "\"false\"") ^ "
set_display_local_var <boolean>
to set a flag saying whether or not the local var be displayed in
sim2chro. Its current value is " ^ (if !(args.display_local_var)
then "\"true\""
else "\"false\"") ^ "
set_verbose (0,1,2)
to set on and off a verbose mode. Its current value is "
^ (string_of_int (args.verbose)) ^ "
set_reactive <boolean>
to set on and off a reactive mode. Its current value is "
^ (if !(args.reactive)
then "\"true\""
else "\"false\"") ^ "
set_show_step <boolean>
to set on and off a show step mode. Its current value is "
^ (if !(args.show_step)
sim2chro. Its current value is " ^ (if (args.display_local_var)
then "\"true\""
else "\"false\"") ^ "
......@@ -258,16 +207,11 @@ set_prefix <string>
This useful, e.g., for timings.
Its current value is \"" ^ args.prefix ^ "\"
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
call sim2chro to visualize (rif) data
set_step_by_step <int>
to set the step_by_step mode on.
gnuplot
gnuplot_ps
call gnuplot (> 3.7) to visualize (rif) data.
set_step_by_step_off
to set the step_by_step mode off.
change_dir <string>
Change the current directory.
......@@ -276,14 +220,15 @@ change_dir <string>
set_tmp_dir <string>
Change the temporary directory.
The current dir is \"" ^ args.tmp_dir ^ "\"
"
in
output_string args.ocr msg;
flush args.ocr
(***********************************************************************)
(* XXX Ca sert pas à grand chose de passe par ca, si ? *)
type t =
Sut of string * string
| Oracle of string * string
......@@ -312,6 +257,7 @@ type t =
| ChDir of string
| ChTmpDir of string
| Clean
| Log
| Run