1 files changed, 126 insertions, 0 deletions
diff --git a/test/monniaux/lustrev4_lv4_heater_control/heater_control.lus b/test/monniaux/lustrev4_lv4_heater_control/heater_control.lus
new file mode 100644
index 00000000..5d0db95f
--- /dev/null
+++ b/test/monniaux/lustrev4_lv4_heater_control/heater_control.lus
@@ -0,0 +1,126 @@
+--
+-- 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);
+
+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