Use luciole if vars are missing in the new lurettetop version.

Also, add the oracle outputs in the '.rif'.

Use luciole if vars are missing in the new lurettetop version.
Also, add the oracle outputs in the '.rif'.
7bb02d3b · Erwan Jahier · f59bc4de · 7bb02d3b · 7bb02d3b · 7bb02d3b
Commit 7bb02d3b authored Jun 24, 2011 by Erwan Jahier
--- a/examples/Makefile
+++ b/examples/Makefile

 # run all the non-regression tests

+
+# a faire coté lutin: luckyDraw, xlurette/Gyro, crazy-rabbit
 test-lucky: 
 	rm -f  */.lurette_rc */*/.lurette_rc */*/*/.lurette_rc
-	cd lucky/external_code && make test;
+	cd lucky/external_code && make test; 
 	cd lucky/other && make test ;
 	cd lucky/tut-examples/ && make test;
 	cd xlurette/Gyro && make test ;
 	cd xlurette/fault-tolerant-heater/ && make test ;
-#	cd xlurette/tram/ && make test ;
 	cd xlurette/heater/ && make test ;
 	cd luckyDraw/ocaml/ && make test ;
 	cd luckyDraw/c/ && make test ;
 	cd lucky/C && make test ;
 	cd lucky/lustre && make test 
 	cd lucky/luciole && make test ;
-	cd xlurette/call-luciole  && make test ;
 	cd ocaml/xlurette && make test ;
 ifneq ($(HOST_TYPE),mac)
 #	cd xlurette/Sildex/ && make test ;
@@ -39,6 +39,7 @@ test-lutin:
 	cd lutin/up_and_down && make test;
 	cd lutin/test_ok && make test;
 	cd lutin/xlurette && make test;
+	cd lutin/xlurette/call-luciole  && make test ;
 	cd lutin/ocaml && make test;
 	cd lutin/external_code && make test;
 	cd lutin/luciole && make test ;

--- a/examples/lutin/xlurette/call-luciole/Makefile
+++ b/examples/lutin/xlurette/call-luciole/Makefile
+
+LTOP=/usr/local/tools/lustre-misc/lurette/i386-linux-gcc3/bin/lurettetop
+LTOP=../../../../$(HOSTTYPE)/bin/lurettetop 
+
+
+
+LURETTETOP=$(LTOP)  --old-mode --precision 2 --sut heater_control.lus \
+	  --main-sut-node heater_control --oracle heater_control.lus \
+	  --main-oracle-node not_a_sauna --sut-compiler verimag \
+	  --oracle-compiler verimag --test-length 1 --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
+
+LURETTETOP=$(LTOP)  --precision 2 \
+	  -rp "sut:v4:heater_control.lus:heater_control"  \
+	  -rp "oracle:v4:heater_control.lus:not_a_sauna"  \
+	  -rp "env:lutin:env.lut:main"  \
+	  --test-length 2 --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
+
+
+test:
+	rm -f test.rif .lurette_rc
+	$(LURETTETOP) -go --output test.rif0 env.lut && \
+	grep -v "lurette chronogram" test.rif0  | \
+	grep -v "This is lurettop Version" test.rif0  | \
+	grep -v "The execution lasted"| sed -e "s/^M//" > test.rif  &&\
+	rm -f test.res
+	diff -B -u -i  test.rif.exp test.rif > test.res || true
+	cat test.res
+	[ ! -s test.res ] && make clean
+	make clean 
+
+utest:
+	cp test.rif test.rif.exp
+
+clean:
+	rm -rf *.ec *.log *~ .*~ *.o *rif0 *rif Data *.pp_luc *.plot *.gp *.dro  *_luciole.c test.res
+
+
+
+dontgo:
+	rm -f test.rif0 .lurette_rc
+	$(LURETTETOP)  env.lut --output test.rif
+
+
--- a/examples/lutin/xlurette/call-luciole/env.lut
+++ b/examples/lutin/xlurette/call-luciole/env.lut
+
+let abs(x : real) : real = 
+    if x > 0.0 then x else -x
+
+
+node main(T : real; Heat_on : bool) returns ( 
+--	T1 : real;
+	T2 : real;
+	T3 : real) =
+
+-- assert abs(T-T1) < 0.5 in
+assert abs(T-T2) < 0.5 in
+assert abs(T-T3) < 0.5 in
+
+   loop true
--- a/examples/lutin/xlurette/call-luciole/heater_control.lus
+++ b/examples/lutin/xlurette/call-luciole/heater_control.lus
+--
+-- 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:bool;LT1, LT2, LT3 : real);
+let
+  LT1 = T1;
+  LT2 = T2;
+  LT3 = T3;
+  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
--- a/examples/lutin/xlurette/call-luciole/test.rif.exp
+++ b/examples/lutin/xlurette/call-luciole/test.rif.exp
+# The random engine was initialized with the seed 3
+#inputs "T":real "T1":real "T2":real "T3":real 
+#outputs "Heat_on":bool 
+
+#oracle_outputs "ok":bool "LT1":real "LT2":real "LT3":real 
+#step 0
+0.00 0.00 0.34 0.03 #outs t
+#oracle_outs t 0.00 0.34 0.03
+#step 1
+0.00 0.00 0.12 -0.09 #outs t
+#oracle_outs t 0.00 0.12 -0.09
+#step 2
+0.00 0.00 0.11 -0.41 #outs t
+#oracle_outs t 0.00 0.11 -0.41
--- a/examples/lutin/xlurette/test.rif.exp
+++ b/examples/lutin/xlurette/test.rif.exp
 # The random engine was initialized with the seed 3
 #inputs "T":real "T1":real "T2":real "T3":real 
 #outputs "Heat_on":bool 
+#oracle_outputs "ok":bool "c4":bool "c5":bool "c6":bool "ok":bool "c1":bool "c2":bool "c3":bool 
 #step 0
 8.85 8.35 9.22 8.87 #outs t
+#oracle_outs t f f f t f f t
 #step 1
 8.86 8.84 8.44 9.25 #outs t
+#oracle_outs t f f f t f f t
 #step 2
 9.61 9.77 9.59 9.80 #outs f
+#oracle_outs t f f f t t f f
 #step 3
 8.99 9.47 9.17 9.15 #outs f
+#oracle_outs t f f f t f f t
 #step 4
 8.66 8.87 8.53 9.08 #outs f
+#oracle_outs t f f f t f f t
 #step 5
 8.38 8.53 8.10 8.07 #outs f
+#oracle_outs t f f f t f f t
 #step 6
 7.77 8.06 8.02 7.65 #outs f
+#oracle_outs t f f f t f f t
 #step 7
 7.19 6.92 7.31 6.96 #outs f
+#oracle_outs t f f f t f f t
 #step 8
 6.27 6.20 6.73 5.93 #outs f
+#oracle_outs t f f f t f f t
 #step 9
 6.04 5.96 6.53 5.64 #outs t
+#oracle_outs t f f f t f f t
 #step 10
 6.04 5.87 6.41 6.33 #outs t
+#oracle_outs t f f f t f f t
 #step 11
 6.04 6.47 6.30 6.31 #outs t
+#oracle_outs t f f f t f f t
 #step 12
 6.83 6.94 6.45 6.45 #outs t
+#oracle_outs t f f f t f f t
 #step 13
 6.83 6.51 6.42 6.50 #outs t
+#oracle_outs t f f f t f f t
 #step 14
 7.30 6.87 6.84 7.28 #outs t
+#oracle_outs t f f f t f f t
 #step 15
 7.30 7.61 7.45 7.00 #outs t
+#oracle_outs t f f f t f f t
 #step 16
 7.71 7.36 7.37 7.67 #outs t
+#oracle_outs t f f f t f f t
 #step 17
 7.71 7.38 8.02 7.25 #outs t
+#oracle_outs t f f f t f f t
 #step 18
 7.71 7.98 8.15 7.66 #outs t
+#oracle_outs t f f f t f f t
 #step 19
 7.71 8.11 7.45 7.32 #outs t
+#oracle_outs t f f f t f f t
 #step 20
 7.71 7.36 8.10 7.25 #outs t
+#oracle_outs t f f f t f f t
 #step 21
 7.71 7.29 7.26 7.36 #outs t
+#oracle_outs t f f f t f f t
 #step 22
 7.71 7.68 7.78 8.05 #outs t
+#oracle_outs t f f f t f f t
 #step 23
 7.90 7.82 8.01 7.60 #outs t
+#oracle_outs t f f f t f f t
 #step 24
 8.09 8.09 8.08 7.68 #outs t
+#oracle_outs t f f f t f f t
 #step 25
 8.09 8.51 8.50 8.22 #outs t
+#oracle_outs t f f f t f f t
 #step 26
 8.49 8.81 8.93 8.93 #outs t
+#oracle_outs t f f f t f f t
 #step 27
 9.01 9.07 8.52 9.22 #outs f
+#oracle_outs t f f f t t f f
 #step 28
 8.54 8.66 8.28 8.68 #outs f
+#oracle_outs t f f f t f f t
 #step 29
 8.40 8.33 8.82 8.90 #outs f
+#oracle_outs t f f f t f f t
 #step 30
 8.18 7.78 8.10 8.22 #outs f
+#oracle_outs t f f f t f f t
 #step 31
 7.52 7.27 7.94 7.24 #outs f
+#oracle_outs t f f f t f f t
 #step 32
 6.76 6.36 6.44 7.07 #outs f
+#oracle_outs t f f f t f f t
 #step 33
 6.26 5.79 6.07 6.01 #outs f
+#oracle_outs t f f f t f f t
 #step 34
 6.26 5.80 6.19 6.73 #outs f
+#oracle_outs t f f f t f f t
 #step 35
 5.39 5.67 5.27 5.52 #outs t
+#oracle_outs t t f t t f f t
 #step 36
 6.23 5.82 6.37 6.10 #outs t
+#oracle_outs t f f f t f f t
 #step 37
 6.23 5.76 6.44 6.26 #outs t
+#oracle_outs t f f f t f f t
 #step 38
 6.23 6.19 5.97 6.39 #outs t
+#oracle_outs t f f f t f f t
 #step 39
 6.23 6.43 6.56 5.86 #outs t
+#oracle_outs t f f f t f f t
 #step 40
 7.01 7.50 7.28 6.87 #outs t
+#oracle_outs t f f f t f f t
 #step 41
 7.01 6.54 6.54 6.67 #outs t
+#oracle_outs t f f f t f f t
 #step 42
 7.47 6.97 7.85 7.20 #outs t
+#oracle_outs t f f f t f f t
 #step 43
 7.58 7.16 8.04 7.62 #outs t
+#oracle_outs t f f f t f f t
 #step 44
 7.58 7.29 7.51 7.95 #outs t
+#oracle_outs t f f f t f f t
 #step 45
 8.56 8.96 8.54 8.97 #outs t
+#oracle_outs t f f f t f f t
 #step 46
 9.16 8.91 9.37 8.97 #outs t
+#oracle_outs t f f f t t f f
 #step 47
 9.82 9.38 9.84 9.44 #outs f
+#oracle_outs t f f f t t f f
 #step 48
 8.92 9.29 9.25 8.59 #outs f
+#oracle_outs t f f f t f f t
 #step 49
 8.06 8.06 7.99 8.52 #outs f
+#oracle_outs t f f f t f f t
 #step 50
 7.60 7.78 7.88 7.56 #outs f
+#oracle_outs t f f f t f f t
 #step 51
 7.20 7.24 6.72 6.98 #outs f
+#oracle_outs t f f f t f f t
 #step 52
 6.76 6.90 6.32 7.26 #outs f
+#oracle_outs t f f f t f f t
 #step 53
 5.84 5.40 5.77 5.85 #outs t
+#oracle_outs t t f t t f f t
 #step 54
 6.10 5.64 5.66 6.13 #outs t
+#oracle_outs t f f f t f f t
 #step 55
 6.74 6.67 6.43 6.44 #outs t
+#oracle_outs t f f f t f f t
 #step 56
 7.73 7.87 7.58 7.73 #outs t
+#oracle_outs t f f f t f f t
 #step 57
 7.73 7.58 7.73 7.73 #outs t
+#oracle_outs t f f f t f f t
 #step 58
 8.42 8.57 8.36 8.60 #outs t
+#oracle_outs t f f f t f f t
 #step 59
 9.37 9.60 9.73 9.80 #outs f
+#oracle_outs t f f f t t f f
 #step 60
 8.65 9.15 9.04 8.63 #outs f
+#oracle_outs t f f f t f f t
 #step 61
 8.61 8.15 8.57 8.66 #outs f
+#oracle_outs t f f f t f f t
 #step 62
 7.65 7.16 7.51 7.61 #outs f
+#oracle_outs t f f f t f f t
 #step 63
 7.05 6.59 7.42 7.26 #outs f
+#oracle_outs t f f f t f f t
 #step 64
 6.36 6.03 6.86 6.20 #outs f
+#oracle_outs t f f f t f f t
 #step 65
 6.03 5.81 5.93 6.23 #outs t
+#oracle_outs t f f f t f f t
 #step 66
 6.04 6.08 6.06 6.04 #outs t
+#oracle_outs t f f f t f f t
 #step 67
 6.49 6.04 6.42 6.39 #outs t
+#oracle_outs t f f f t f f t
 #step 68
 7.29 7.07 7.65 7.02 #outs t
+#oracle_outs t f f f t f f t
 #step 69
 7.29 6.81 6.89 7.52 #outs t
+#oracle_outs t f f f t f f t
 #step 70
 7.29 7.55 7.39 7.24 #outs t
+#oracle_outs t f f f t f f t
 #step 71
 7.29 6.82 7.33 6.87 #outs t
+#oracle_outs t f f f t f f t
 #step 72
 7.47 7.34 7.06 7.38 #outs t
+#oracle_outs t f f f t f f t
 #step 73
 7.66 7.20 7.28 8.02 #outs t
+#oracle_outs t f f f t f f t
 #step 74
 8.60 8.47 8.24 8.57 #outs t
+#oracle_outs t f f f t f f t
 #step 75
 8.60 8.22 8.19 8.67 #outs t
+#oracle_outs t f f f t f f t
 #step 76
 8.60 8.12 8.17 8.43 #outs t
+#oracle_outs t f f f t f f t
 #step 77
 8.60 9.02 8.17 9.05 #outs f
+#oracle_outs t f f f t f f t
 #step 78
 7.95 8.16 8.16 7.80 #outs f
+#oracle_outs t f f f t f f t
 #step 79
 6.98 7.27 6.98 7.20 #outs f
+#oracle_outs t f f f t f f t
 #step 80
 6.16 6.57 6.07 6.66 #outs f
+#oracle_outs t f f f t f f t
 #step 81
 6.13 5.94 5.94 5.91 #outs t
+#oracle_outs t f f f t f f t
 #step 82
 6.58 6.30 6.32 6.62 #outs t
+#oracle_outs t f f f t f f t
 #step 83
 7.22 7.32 7.69 6.82 #outs t
+#oracle_outs t f f f t f f t
 #step 84
 7.46 7.08 7.62 7.83 #outs t
+#oracle_outs t f f f t f f t
 #step 85
 7.62 7.29 7.44 7.95 #outs t
+#oracle_outs t f f f t f f t
 #step 86
 7.75 7.75 7.81 7.70 #outs t
+#oracle_outs t f f f t f f t
 #step 87
 7.75 7.61 8.22 7.47 #outs t
+#oracle_outs t f f f t f f t
 #step 88
 7.75 8.01 7.93 7.44 #outs t
+#oracle_outs t f f f t f f t
 #step 89
 7.75 7.31 7.98 7.49 #outs t
+#oracle_outs t f f f t f f t
 #step 90
 7.75 8.13 7.42 7.27 #outs t
+#oracle_outs t f f f t f f t
 #step 91
 7.75 7.63 7.96 7.86 #outs t
+#oracle_outs t f f f t f f t
 #step 92
 7.75 7.95 7.36 8.14 #outs t
+#oracle_outs t f f f t f f t
 #step 93
 7.77 8.16 7.73 7.82 #outs t
+#oracle_outs t f f f t f f t
 #step 94
 7.77 7.81 7.90 7.81 #outs t
+#oracle_outs t f f f t f f t
 #step 95
 7.77 8.15 8.18 8.12 #outs t
+#oracle_outs t f f f t f f t
 #step 96
 7.77 8.21 7.84 8.07 #outs t
+#oracle_outs t f f f t f f t
 #step 97
 7.77 8.04 7.56 7.66 #outs t
+#oracle_outs t f f f t f f t
 #step 98
 7.87 8.00 8.28 7.45 #outs t
+#oracle_outs t f f f t f f t
 #step 99
 7.87 7.72 8.13 7.62 #outs t
+#oracle_outs t f f f t f f t
 #step 100
 8.85 8.74 9.31 8.65 #outs t
+#oracle_outs t f f f t f f t
--- a/examples/ocaml/xlurette/Makefile
+++ b/examples/ocaml/xlurette/Makefile
@@ -8,8 +8,16 @@ LURETTETOP=$(LTOP)   --precision 2 --sut heat_ctrl.ml \
 	  --step-mode Inside --local-var  --no-sim2chro  --seed 3 \
 	  --do-not-show-step --old-mode

-# XXX
-# --oracle oracle.ml \
+# XXX make it work!
+NEW_LURETTETOP=$(LTOP)   --precision 2 \
+	  -rp "sut:ocaml:heat_ctrl.ml:" \
+	  -rp "oracle:ocaml:not_a_sauna.ml:" \
+	  -rp "env:lutin:env.lut:main" \
+	  --test-length 500 --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 
+


 test:
@@ -25,6 +33,9 @@ utest:
 	cp test.rif test.rif.exp


+
+
+
 clean:
 	rm -rf *.ec *.cm* *.log *~ .*~ *.o *rif0 *rif Data *.pp_luc *.plot *.gp


--- a/source/Lucky/luc2c.ml
+++ b/source/Lucky/luc2c.ml
@@ -479,7 +479,7 @@ Input procedures must be used:
      in_vars;
    
    let lut_file = (List.hd option.env) (* only work with lutin XXX fixme? *) in
-    let lut_dir = Filename.dirname lut_file in
+(*     let lut_dir = Filename.dirname lut_file in *)
    putln ("
 /*--------
 launch the lutin interpreter and init socket stuff
@@ -947,7 +947,6 @@ let (main : unit -> unit) =
    let env_list = option.env in
    let state = LucProg.make_state option.pp env_list in
    let _ =  assert (env_list <> []) in
-    let from_lutin = Util.get_extension (List.hd env_list) = ".lut"  in
    let fn = build_file_name env_list in
    let _ = 
      gen_c_file fn state.s.in_vars state.s.out_vars state.s.loc_vars;
@@ -967,7 +966,7 @@ let (main : unit -> unit) =
                Type.to_cstring (Var.typ v)
               )
             in
-               Luciole.gen_stubs false from_lutin 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)
         | Scade -> ()

--- a/source/Lucky/luc2luciole.ml
+++ b/source/Lucky/luc2luciole.ml
@@ -46,7 +46,10 @@ let usage = (usage_begin ^ usage_end)

 let more_usage = (usage_begin ^ "
 luc2luciole generates a lurette_luciole.c file so that lurette 
-  can use luciole to generate missing sur inputs.
+ can use luciole to generate missing sut inputs.
+
+ nb : it is obselete with the new version of lurettetop (since version 1.55)
+
 " ^ usage_end)

 let rec speclist =
@@ -65,7 +68,7 @@ let rec speclist =
    "-sut-header",  Arg.String (fun s -> flag.sut_header <- s), "\t\tThe h (poc) file\n";

    "--help", Arg.Unit (fun _ -> (Arg.usage_out speclist more_usage ; exit 0)),
-       "\tTo display this list of options." ;
+       "\tto obtain help." ;
    "-help", Arg.Unit (fun _ -> (Arg.usage_out speclist more_usage ; exit 0)),
    "";