Commit 0097b051 authored by Erwan Jahier's avatar Erwan Jahier

New feature: when some SUT or environement inputs are missing, use

luciole to generate them.
parent f8491fcc
......@@ -18,9 +18,12 @@ clean:
VERSION:=$(shell E=`git log --oneline | wc -l` ; echo "$$E-166" | bc )
VERSION:="1.$(VERSION)"
VERSION:="1.50"
SHA:=`git log -1 --pretty=format:"%h"`
gen_version:
rm -f source/version.ml
echo "let str=\"$(VERSION)\"" > source/version.ml
echo "let sha=\"$(SHA)\"" >> source/version.ml
rm version.tex
date +VERSION_DATE=%d-%m-%y > version.tex
echo "\\newcommand{\\version}{$(VERSION)}" > version.tex
......@@ -32,8 +35,10 @@ gen_version:
ci:
cia:
git commit -a -F log
ci:
git commit -F log
lci:
......@@ -44,7 +49,7 @@ ldiff:
pdiff -r unstable
diff:
git diff > diff.diff
git diff HEAD -w > diff.diff
touch:
......
V1.50 (11/05/2010)
* Compute a coverage rate. It looks at oracle outputs which names
begins with "covered_", and compute the rate of true values among
those.
V1.50 (18/05/2010)
* New feature: Compute a coverage rate. It looks at oracle outputs
which names begins with "covered_", and compute the rate of true
values among those.
* New feature: when some SUT or some environment inputs are missing,
use luciole to generate them.
When a SUT or an environment input is missing, call luciole to
generate it.
V1.49 (8/04/2010)
......
......@@ -14,6 +14,7 @@ test:
cd luckyDraw/c/ && make test ;
cd lucky/C && make test ;
cd lucky/lustre && make test ;
cd lucky/luciole && make test ;
ifneq ($(HOST_TYPE),mac)
# cd xlurette/Sildex/ && make test ;
cd ocaml/crazy-rabbit/ && make test ;
......
CC=cc
all:lurette.dro
simec ./lurette.dro
heater_control.h:
lus2ec heater_control.lus heater_control
ec2c heater_control.ec
lurette_luciole.c: heater_control.h
luc2luciole -env sensors.luc -sut-header heater_control.h
lurette.dro: lurette_luciole.o
$(CC) -I$(LURETTE_PATH)/include lurette_luciole.o -shared -o lurette.dro
%.o: %.c
$(CC) -I$(LURETTE_PATH)/include -c $<
clean:
rm -f lurette_luciole.* lurette.dro heater_control.h heater_control.c heater_control.ec sensors.pp_luc
--
-- 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(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 =
if Tguess = FAILURE then false else
if Tguess < TMIN then true else
if Tguess > TMAX then false else
true -> pre Heat_on;
tel
-----------------------------------------------------------------------
-----------------------------------------------------------------------
node not_a_sauna(T, T1, T2, T3 : real; Heat_on: bool) returns (ok:bool);
let
ok = true -> pre T < TMAX + 1.0 ;
tel
node not_a_sauna2(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
-- Simulate perfect sensors that never get worn
inputs {
T : float;
-- Heat_on : bool
}
outputs {
T1 : real;
T2 : real;
T3 : real
}
locals {
eps1 : real ~min -0.1 ~max 0.1;
eps2 : real ~min -0.1 ~max 0.1;
eps3 : real ~min -0.1 ~max 0.1;
}
nodes { 1 : stable }
start_node { 1 }
transitions {
1 -> 1 ~ cond T1 = T + eps1 and
T2 = T + eps2
and T3 = T + eps3
}
-include Makefile.foo
go:
../../bin/luc2c --luciole foo.luc
test: go
make -f Makefile.foo && make clean
\ No newline at end of file
--
inputs {
a:int;
b:bool;
c:float
}
outputs {
x:int;
y:bool;
z:float
}
states { 0:stable }
start_state { 0 }
transitions { 0 -> 0
~cond
b=>y and abs(x - a) < 5
and abs(z - c) < 5.0
}
......@@ -63,12 +63,21 @@ dc:
$(CC) -g -o lurette $(LIBDIRS) $(INCLUDEDIRS) $(SOURCES_C) \
-lnsl -lsocket -llurette_dc -llucky_dc $(LIBS)
nc:
nc: lurette.dro
$(CC) -c $(LIBDIRS) $(INCLUDEDIRS) $(SOURCES_C)
$(LINKER) -o lurette $(LIBDIRS) $(INCLUDEDIRS) *.o \
-llurette_nc -llucky_nc $(LIBS)
lurette_luciole.c: $(SUT).h
luc2luciole -env $(ENV) -sut-header $(SUT).h
lurette_luciole.o: lurette_luciole.c
$(CC) $(INCLUDEDIRS) -c lurette_luciole.c
lurette.dro: lurette_luciole.o
$(CC) $(INCLUDEDIRS) lurette_luciole.o -shared -o lurette.dro
all: nc
......
......@@ -45,9 +45,11 @@ liblucky_nc.a:
ar q liblucky_nc.a *.o && rm *.o &&\
cp liblucky_nc.a ..
liblutin_stubs.o:
make -f Makefine.lutinlib all
# un petit essai pour les gens de Corys
.PHONY:liblucky_nc.so
liblucky_nc.so:
.PHONY:liblucky_nc.so liblutin_stubs.o
liblucky_nc.so: ../liblutin_stubs.o
[ -d lurette_util ] || mkdir lurette_util && \
cd lurette_util && rm -f * && \
cp ../Ezdl_c.o . &&\
......@@ -560,6 +562,22 @@ luc2c_debug:
luc2c_assert:
make -k nc -f Makefile.luc2c OCAMLFLAGS=""
cp luc2c_exe luc2c_exe_assert
##############################################################################"
luc2luciole:
make -k nc -f Makefile.luc2luciole OCAMLFLAGS="-unsafe"
luc2luciole_clean:
make -k clean -f Makefile.luc2luciole
luc2luciole_static:
make -k nc -f Makefile.luc2luciole OCAMLFLAGS="-noassert -unsafe" STATIC=yes
luc2luciole_debug:
make -k dc -f Makefile.luc2luciole OCAMLFLAGS=""
luc2luciole_assert:
make -k nc -f Makefile.luc2luciole OCAMLFLAGS=""
cp luc2luciole_exe luc2luciole_exe_assert
......@@ -684,9 +702,9 @@ all_assert: clean libnc_assert lucky_assert ltop_assert show_assert luc4ocaml_as
check:
echo "A faire dans le repertoire test, sinon, ca vaut pas !!! "
allw:libnc lucky ltop show stubs gnuplot-rif gnuplot-socket gen_luc luc2c luc4c libluc4c_nc.a draw-all luc4ocaml-all
all: libnc lucky ltop show stubs gnuplot-rif gnuplot-socket gen_luc luc2c luc4c libluc4c draw-all luc4ocaml-all
allnc: libncnc lucky ltop show stubs gnuplot-rif gnuplot-socket gen_luc luc2c luc4c libluc4c draw-all luc4ocaml-all
allw:libnc lucky ltop show stubs gnuplot-rif gnuplot-socket gen_luc luc2c luc2luciole luc4c libluc4c_nc.a draw-all luc4ocaml-all
all: libnc lucky ltop show stubs gnuplot-rif gnuplot-socket gen_luc luc2c luc2luciole luc4c libluc4c draw-all luc4ocaml-all
allnc: libncnc lucky ltop show stubs gnuplot-rif gnuplot-socket gen_luc luc2c luc2luciole luc4c libluc4c draw-all luc4ocaml-all
static: libnc lucky_static ltop_static show_static stubs_static gen_luc_static
......@@ -706,7 +724,7 @@ unixtop:
clean_exe:
rm -f gen_stubs_exe lucky lurettetop_exe lurette_lib.* \
gen_fake_lutin gen_fake_lucky luc2c show_luc *_assert \
gen_fake_lutin gen_fake_lucky luc2c luc2luciole show_luc *_assert \
liblurette_lib*
clean: clean_exe
......@@ -721,6 +739,7 @@ clean: clean_exe
make -k clean -f Makefile.luc4ocaml ; \
make -k clean -f Makefile.luckyDraw ; \
make -k clean -f Makefile.luc2c ; \
make -k clean -f Makefile.luc2luciole ; \
make -k clean -f Makefile.luc4c ; \
make -k clean -f Makefile.show_luc ; \
rm -f *.a *.o
......@@ -738,6 +757,7 @@ cp:
cp lucky$(EXE) $(BIN_INSTALL_DIR) ; \
cp show_luc$(EXE) $(BIN_INSTALL_DIR) ; \
cp luc2c$(EXE) $(BIN_INSTALL_DIR) ; \
cp luc2luciole$(EXE) $(BIN_INSTALL_DIR) ; \
cp lurettetop_exe$(EXE) $(BIN_INSTALL_DIR) ; \
cp liblurette_nc.a $(LIB_INSTALL_DIR) ;\
cp liblucky_nc.a $(LIB_INSTALL_DIR) ;\
......@@ -759,6 +779,7 @@ cp-verimag:
cp lucky$(EXE) $(BIN_VERIMAG_INSTALL_DIR) ; \
cp show_luc$(EXE) $(BIN_VERIMAG_INSTALL_DIR) ; \
cp luc2c$(EXE) $(BIN_VERIMAG_INSTALL_DIR) ; \
cp luc2luciole$(EXE) $(BIN_VERIMAG_INSTALL_DIR) ; \
cp lurettetop_exe$(EXE) $(BIN_VERIMAG_INSTALL_DIR) ; \
cp liblurette_nc.a $(LIB_VERIMAG_INSTALL_DIR) ;\
cp liblucky_nc.a $(LIB_VERIMAG_INSTALL_DIR) ;\
......
#
# Make file for show_luc (to display env files with dot)
#
-include ../Makefile.common.source
......
#
#
-include ../Makefile.common.source
######################################################################
OCAMLNCFLAGS = -inline 10
ifdef STATIC
OCAMLLDFLAGS = -cclib -ldl -cclib -lm -cclib -lc -ccopt -static
endif
LIBS = str unix
#CLIBS =
USE_CAMLP4 = yes
HERE=$(LURETTE_PATH)/source/
HERE=./
SOURCES_OCAML = \
$(HERE)/Ezdl_c.c \
$(HERE)/Ezdl.ml \
$(HERE)/Ezdl.mli \
$(HERE)/version.ml \
$(HERE)/util.ml \
$(HERE)/graphUtil.ml \
$(HERE)/graphUtil.mli \
$(HERE)/graphUtil.mli \
$(HERE)/type.mli \
$(HERE)/type.ml \
$(HERE)/luciole.ml \
$(HERE)/genlex.mli $(HERE)/genlex.ml \
$(HERE)/lexeme.mli $(HERE)/lexeme.ml \
$(HERE)/prevar.mli $(HERE)/prevar.ml \
$(HERE)/value.mli $(HERE)/value.ml \
$(HERE)/graph.mli $(HERE)/graph.ml \
$(HERE)/var.mli \
$(HERE)/var.ml \
$(HERE)/exp.mli \
$(HERE)/exp.ml \
$(HERE)/lustreExp.mli $(HERE)/lustreExp.ml \
$(HERE)/parser.mly $(HERE)/lexer.mll \
$(HERE)/parse_luc.mli $(HERE)/parse_luc.ml \
$(HERE)/gen_stubs_common.mli \
$(HERE)/gen_stubs_common.ml \
$(HERE)/parse_poc.mli \
$(HERE)/parse_poc.ml \
$(HERE)/env_state.mli $(HERE)/env_state.ml \
$(HERE)/luc2luciole.ml
SOURCES = $(SOURCES_OCAML)
RESULT = luc2luciole
-include $(OCAMLMAKEFILE)
......@@ -24,11 +24,13 @@ type optionsT = {
mutable draw_all_vertices : bool;
mutable compute_volume : bool;
mutable step_mode : Lucky.step_mode;
mutable luciole_mode : bool;
mutable oracle : bool ;
mutable pp : string option ;
mutable scade_gui : bool;
mutable is_reactive : bool;
mutable stdin : bool
mutable stdin : bool;
mutable tmp_dir : string;
}
type cmd_line_optionT =
......@@ -39,7 +41,7 @@ type cmd_line_optionT =
(* | CuddHeapInit *)
| Seed | Precision | NoOracle | Verbose | ShowStep | Output
| ComputeVolume | StepInside | StepEdges | StepVertices | Stdin | PP | Reactive
| ScadeGui
| ScadeGui | TmpDir
(* Names of the command line options to override the defaults. *)
let (string_to_option: (string * cmd_line_optionT) list) = [
......@@ -88,6 +90,8 @@ let (string_to_option: (string * cmd_line_optionT) list) = [
("--fair", ComputeVolume);
("--compute-poly-volume", ComputeVolume);
("--tmp-dir", TmpDir);
("--step-inside", StepInside);
("--step-edges", StepEdges);
("--step-vertices", StepVertices);
......@@ -124,6 +128,7 @@ let (option_to_usage: cmd_line_optionT -> string) =
| StepEdges -> "Step at edges\n"
| StepVertices -> "Step at vertices\n"
| PP -> "Pipe lucky file(s) through a preprocessor (e.g., cpp)"
| TmpDir -> "Set the tmp dir"
| ScadeGui -> "indicate that lurette is launched from the Scade GUI."
| Reactive -> "Set on a reactive mode, in which, when no transition is possible, the previous values are returned.\n"
| Stdin -> "Use apps that reads and writes RIF on stdin/stdout"
......
......@@ -28,11 +28,13 @@ type optionsT = {
mutable draw_all_vertices : bool;
mutable compute_volume : bool;
mutable step_mode : Lucky.step_mode;
mutable luciole_mode : bool;
mutable oracle : bool ;
mutable pp : string option ;
mutable scade_gui : bool;
mutable is_reactive : bool;
mutable stdin : bool
mutable stdin : bool;
mutable tmp_dir : string;
}
val usage : string
......@@ -52,7 +54,7 @@ type cmd_line_optionT =
| AllVertices | AllFormula
| Seed | Precision | NoOracle | Verbose | ShowStep | Output
| ComputeVolume | StepInside | StepEdges | StepVertices | Stdin | PP
| Reactive | ScadeGui
| Reactive | ScadeGui | TmpDir
val string_to_option: (string * cmd_line_optionT) list
(** Mapping from options string (e.g., "--no-step") to the cmd_line_optionT
......
......@@ -16,6 +16,7 @@ type optionsT = {
mutable max_step_number : int option ;
mutable locals : bool ;
mutable draw_mode : Lucky.step_mode ;
mutable luciole_mode : bool;
mutable compute_volume : bool;
mutable user_seed : int option ;
mutable oracle : string ;
......
......@@ -18,6 +18,7 @@ type optionsT = {
mutable max_step_number : int option ;
mutable locals : bool ;
mutable draw_mode : Lucky.step_mode ;
mutable luciole_mode : bool;
mutable compute_volume : bool;
mutable user_seed : int option ;
mutable oracle : string ;
......
......@@ -68,11 +68,11 @@ let (string_to_compiler:string -> compiler) =
fun s ->
match s with
| "verimag" -> VerimagV4
| "verimag" -> VerimagV4
| "lv4" -> VerimagV4
| "Verimag" -> VerimagV4
| "lv4" -> VerimagV4
| "v4" -> VerimagV4
| "lv6" -> VerimagV6
| "lv6" -> VerimagV6
| "v6" -> VerimagV6
| "scade-gui" -> ScadeGUI
| "scade" -> Scade
| "Scade" -> Scade
......@@ -623,8 +623,8 @@ let (typedef_to_type : (string * string) list -> (string * Type.t) list) =
let lexer =
Genlex.make_lexer ["^";"(";")";"{";":";",";";";"}"] (Stream.of_string str)
in
let tok_list = Stream.npeek 10 lexer in
let tok_list2 = Stream.npeek 10 lexer in
let _tok_list = Stream.npeek 10 lexer in
let _tok_list2 = Stream.npeek 10 lexer in
(* print_string ("\nGetting types of " ^str ^ "\n"); *)
get_types [] lexer
......
......@@ -697,7 +697,7 @@ let rec (main : unit -> 'a) =
Type.to_cstring (Var.typ v)
)
in
Luciole.gen_stubs fn
Luciole.gen_stubs false fn
(List.map var_to_vn_ct state.s.in_vars)
(List.map var_to_vn_ct state.s.out_vars)
)
......
......@@ -26,6 +26,7 @@ let (options:Command_line_luc_exe.optionsT) = {
max_step_number = None ;
locals = false ;
draw_mode = Lucky.StepInside;
luciole_mode = false;
compute_volume = false;
boot = false ;
oracle = "";
......@@ -436,7 +437,7 @@ and
try
print_string ("# This is Lucky Version " ^ Version.str ^ "\n\n");
print_string ("# This is Lucky Version " ^ Version.str ^ " (" ^Version.sha^")\n\n");
flush stdout
with _ ->
();;
......
......@@ -12,6 +12,7 @@
(* Var name and C type *)
type vn_ct = string * string
let soi = string_of_int
(** Generates stub files for calling luciole. *)
let gen_makefile str =
......@@ -50,16 +51,24 @@ let gen_makefile str =
ignore (Util.my_create_process "make" ["-f";("Makefile." ^ str)]);
close_out oc
let (gen_stubs : string -> vn_ct list -> vn_ct list -> unit) =
fun str inputs outputs ->
let oc = open_out (str^"_luciole.c") in
let (gen_stubs : bool -> string -> vn_ct list -> vn_ct list -> unit) =
fun from_lurette str inputs outputs ->
let oc =
if from_lurette then
open_out ("lurette_luciole.c")
else
open_out (str^"_luciole.c")
in
let p s = output_string oc s in
let pn s = p (s^"\n") in
let d2r = function
"double" -> "real"
| "_real" -> "real"
| "_int" -> "int"
| "_bool" -> "bool"
| e -> e
in
let vn_ct_to_array (vn, ct) =
......@@ -81,17 +90,87 @@ let (gen_stubs : string -> vn_ct list -> vn_ct list -> unit) =
pn (" _outab["^(string_of_int i)^"].valptr = (void*)(& _THIS->_"^vn^");");
(i+1)
in
let simec_version_number = "1.1" in
p (Util.entete "// ");
p "#include \"droconf.h\"
#include \"stdlib.h\"
#include \"";
p str; pn ".h\"
#include \"stdlib.h\"
";
if (not from_lurette) then (
p "#include \"";
p str;
pn ".h\"
";
pn ("static " ^ str ^ "_ctx* _THIS = NULL;");
pn ("static " ^ str ^ "_ctx* _THIS = NULL;")
)
else
(
pn "#include <stdio.h>";
pn "typedef int _bool;";
pn "typedef int _int;";
pn "typedef double _real;";
pn "struct _luciole_ctx {";
pn "// INPUTS";
List.iter
(fun (vn,t) -> pn (" _"^ t ^ " _" ^ vn ^";"))
inputs;
pn "// OUTPUTS";
List.iter
(fun (vn,t) -> pn (" _"^ t ^ " _" ^ vn ^";"))
outputs;
pn "};";
pn "typedef struct _luciole_ctx luciole_ctx;";
pn "static luciole_ctx* _THIS = NULL;";
pn "/* Standard Input procedures **************/
_bool _get_bool(){
char b[512];
_bool r = 0;
int s = 1;
char c;
do {
if(scanf(\"%s\", b)==EOF) exit(0);
s = sscanf(b, \"%c\", &c);
r = -1;
if((c == '0') || (c == 'f') || (c == 'F')) r = 0;
if((c == '1') || (c == 't') || (c == 'T')) r = 1;
} while((s != 1) || (r == -1));
return r;
}
_int _get_int(){
char b[512];
_int r;
int s = 1;
do {
if(scanf(\"%s\", b)==EOF) exit(0);
s = sscanf(b, \"%d\", &r);
} while(s != 1);
return r;
}
_real _get_real(){
char b[512];
_real r;
int s = 1;
do {
if(scanf(\"%s\", b)==EOF) exit(0);
s = sscanf(b, \"%lf\", &r);
} while(s != 1);
return r;
}
/* Standard Output procedures **************/
void _put_bool(_bool _V){
printf(\"%s\\n\", (_V)? \"t\" : \"f\");
}
void _put_int(_int _V){
printf(\"%d\\n\", _V);
}
void _put_real(_real _V){
printf(\"%f\\n\", _V);
}
";
);
pn "int __do_step();";
pn "int internal_step(){";
pn " return __do_step();";
......@@ -128,34 +207,55 @@ let (gen_stubs : string -> vn_ct list -> vn_ct list -> unit) =
pn " internal_init";
pn "};";
pn "";
pn "//output functions";
ignore (List.fold_left vn_ct_to_output_functions 0 outputs);
pn "";
if (not from_lurette) then (
pn "//output functions";
ignore (List.fold_left vn_ct_to_output_functions 0 outputs);
pn ""
);