Lustre v4 example

7 files changed, 567 insertions, 0 deletions

diff --git a/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control.lus b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control.lus
new file mode 100644
index 00000000..9a668a47
--- /dev/null
+++ b/test/monniaux/lustrev4_lv6-en-2cgc_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
+function abs (v : real) returns (a : real) ;
+let
+	a = if v >= 0.0 then v else -v ;
+tel
+
+-- returns the average values of 2 reals
+function Average(a, b: real) returns (z : real); 
+let 
+	z = (a+b)/2.0 ; 
+tel
+
+-- returns the median values of 3 reals
+function 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
+function max2 (one, two  : real) returns (m : real) ;
+let
+	m = if one > two then one else two ;
+tel
+
+-- returns the minimum values of 2 reals
+function min2 (one, two  : real) returns (m : real) ;
+let
+	m = if one < two then one else two ;
+tel
+
+
+function noneoftree (f1, f2, f3 : bool) returns (r : bool) 
+let
+	 r = not f1 and not f2 and not f3 ;
+tel 
+
+function alloftree (f1, f2, f3 : bool) returns (r : bool) 
+let
+	 r =  f1 and f2 and f3 ;
+tel 
+
+function 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
diff --git a/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control.c b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control.c
new file mode 100644
index 00000000..1b3cb947
--- /dev/null
+++ b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control.c
@@ -0,0 +1,302 @@
+/* This file was generated by lv6 version master.737 (2727a7744111c84f7984634d2bd3ad6f7c6c7ff9). */
+/*  lv6 -en -2cgc heater_control.lus -n heater_control */
+/* on vanoise the 15/05/2019 at 13:20:10 */
+#include "heater_control_heater_control.h"
+//// Defining step functions
+// Memory initialisation for Lustre_arrow_ctx
+void Lustre_arrow_ctx_reset(Lustre_arrow_ctx_type* ctx){
+  int _i;
+  ctx->_memory = _true;
+}
+
+// Initialisation of the  internal structure of Lustre_arrow_ctx
+void Lustre_arrow_ctx_init(Lustre_arrow_ctx_type* ctx){
+  // ctx->client_data = cdata;
+  Lustre_arrow_ctx_reset(ctx);
+ }
+// Step function(s) for Lustre_arrow_ctx
+void Lustre_arrow_step(_boolean i1,_boolean i2,_boolean *out,Lustre_arrow_ctx_type* ctx){  *out = ((ctx->_memory)? i1 : i2);
+  ctx->_memory = _false;
+
+} // End of Lustre_arrow_step
+
+// Memory initialisation for Lustre_pre_ctx
+void Lustre_pre_ctx_reset(Lustre_pre_ctx_type* ctx){
+  int _i;
+
+}
+
+// Initialisation of the  internal structure of Lustre_pre_ctx
+void Lustre_pre_ctx_init(Lustre_pre_ctx_type* ctx){
+  // ctx->client_data = cdata;
+  Lustre_pre_ctx_reset(ctx);
+ }
+// Step function(s) for Lustre_pre_ctx
+void Lustre_pre_get(_boolean *out,Lustre_pre_ctx_type* ctx){
+  *out = ctx->_memory;
+
+} // End of Lustre_pre_get
+
+void Lustre_pre_set(_boolean i1,Lustre_pre_ctx_type* ctx){
+  ctx->_memory = i1;
+
+} // End of Lustre_pre_set
+
+// Step function(s) for Lustre_slash_ctx
+void Lustre_slash_step(_real i1,_real i2,_real *out){
+  *out = (i1 / i2);
+
+} // End of Lustre_slash_step
+
+// Memory initialisation for heater_control_heater_control_ctx
+void heater_control_heater_control_ctx_reset(heater_control_heater_control_ctx_type* ctx){
+  int _i;
+
+    Lustre_pre_ctx_reset(&ctx->Lustre_pre_ctx_tab[0]);
+    Lustre_arrow_ctx_reset(&ctx->Lustre_arrow_ctx_tab[0]);
+}
+
+// Initialisation of the  internal structure of heater_control_heater_control_ctx
+void heater_control_heater_control_ctx_init(heater_control_heater_control_ctx_type* ctx){
+  // ctx->client_data = cdata;
+  heater_control_heater_control_ctx_reset(ctx);
+ }
+// Step function(s) for heater_control_heater_control_ctx
+void heater_control_heater_control_step(_real T,_real T1,_real T2,_real T3,_boolean *Heat_on,heater_control_heater_control_ctx_type* ctx){   _boolean __split_9_3;
+   _real __split_10_3;
+   _boolean __split_9_2;
+   _real __split_10_2;
+   _boolean __split_9_1;
+   _real __split_10_1;
+   _real __split_1_3;
+   _real __split_1_2;
+   _real __split_1_1;
+   _real __split_2_2;
+   _real __split_3_2;
+   _real __split_4_2;
+   _real __split_5_2;
+   _real __split_6_2;
+   _real __split_7_2;
+   _real __split_8_2;
+   _boolean ___split_38_1_2;
+   _boolean ___split_38_2_2;
+   _boolean ___split_37_1_2;
+   _boolean ___split_37_2_2;
+   _boolean __split_11_1;
+   _real __split_2_1;
+   _real __split_3_1;
+   _real __split_4_1;
+   _real __split_5_1;
+   _real __split_6_1;
+   _real __split_7_1;
+   _real __split_8_1;
+   _boolean ___split_38_1_1;
+   _boolean ___split_38_2_1;
+   _boolean ___split_37_1_1;
+   _boolean ___split_37_2_1;
+   _boolean __split_43_1;
+   _boolean __split_44_1;
+   _boolean __split_45_1;
+   _boolean __split_46_1;
+   _boolean __split_47_1;
+   _boolean __split_48_1;
+   _boolean __split_49_1;
+   _boolean __split_50_1;
+   _boolean __split_51_1;
+   _boolean __split_52_1;
+   _boolean __split_53_1;
+   _boolean __split_54_1;
+   _boolean __split_55_1;
+   _boolean __split_39_1;
+   _boolean __split_40_1;
+   _boolean __split_41_1;
+   _boolean __split_42_1;
+   _boolean _split_36;
+   _boolean _split_35;
+   _boolean _split_34;
+   _boolean _split_33;
+   _boolean _split_32;
+   _boolean _split_31;
+   _boolean _split_30;
+   _real _split_29;
+   _real _split_28;
+   _real _split_27;
+   _real _split_26;
+   _real _split_25;
+   _real _split_24;
+   _real _split_23;
+   _real _split_22;
+   _boolean _split_21;
+   _real _split_20;
+   _boolean _split_19;
+   _boolean _split_18;
+   _real _split_17;
+   _real _split_16;
+   _real _split_15;
+   _real _split_14;
+   _real _split_13;
+   _real _split_12;
+   _boolean V12;
+   _boolean V13;
+   _boolean V23;
+   _real Tguess;
+
+  _split_16 = T2 - T3;
+  __split_10_1 = - _split_16;
+  __split_9_1 = _split_16 >= 0.0;
+   if (__split_9_1 == _true) {
+     _split_17 = _split_16;
+   } else {
+     _split_17 = __split_10_1;
+   }
+  V23 = _split_17 < 0.5;
+  __split_42_1 = ! V23;
+  _split_12 = T1 - T2;
+  __split_10_3 = - _split_12;
+  __split_9_3 = _split_12 >= 0.0;
+   if (__split_9_3 == _true) {
+     _split_13 = _split_12;
+   } else {
+     _split_13 = __split_10_3;
+   }
+  V12 = _split_13 < 0.5;
+  __split_39_1 = ! V12;
+  _split_14 = T1 - T3;
+  __split_10_2 = - _split_14;
+  __split_9_2 = _split_14 >= 0.0;
+   if (__split_9_2 == _true) {
+     _split_15 = _split_14;
+   } else {
+     _split_15 = __split_10_2;
+   }
+  V13 = _split_15 < 0.5;
+  __split_40_1 = ! V13;
+  __split_41_1 = __split_39_1 & __split_40_1;
+  _split_18 = __split_41_1 & __split_42_1;
+  __split_43_1 = ! V13;
+  __split_44_1 = V12 & __split_43_1;
+  __split_45_1 = ! V23;
+  __split_46_1 = __split_44_1 & __split_45_1;
+  __split_47_1 = ! V12;
+  __split_48_1 = V13 & __split_47_1;
+  __split_49_1 = ! V23;
+  __split_50_1 = __split_48_1 & __split_49_1;
+  __split_51_1 = __split_46_1 | __split_50_1;
+  __split_54_1 = ! V13;
+  __split_52_1 = ! V12;
+  __split_53_1 = V23 & __split_52_1;
+  __split_55_1 = __split_53_1 & __split_54_1;
+  _split_19 = __split_51_1 | __split_55_1;
+  ___split_37_1_1 = T2 > T3;
+   if (___split_37_1_1 == _true) {
+     __split_7_1 = T2;
+   } else {
+     __split_7_1 = T3;
+   }
+  ___split_37_2_1 = T1 > __split_7_1;
+   if (___split_37_2_1 == _true) {
+     __split_8_1 = T1;
+   } else {
+     __split_8_1 = __split_7_1;
+   }
+  ___split_38_1_1 = T2 < T3;
+   if (___split_38_1_1 == _true) {
+     __split_4_1 = T2;
+   } else {
+     __split_4_1 = T3;
+   }
+  ___split_38_2_1 = T1 < __split_4_1;
+   if (___split_38_2_1 == _true) {
+     __split_5_1 = T1;
+   } else {
+     __split_5_1 = __split_4_1;
+   }
+  __split_2_1 = T1 + T2;
+  __split_3_1 = __split_2_1 + T3;
+  __split_6_1 = __split_3_1 - __split_5_1;
+  _split_20 = __split_6_1 - __split_8_1;
+  __split_1_2 = T1 + T3;
+  Lustre_slash_step(__split_1_2,2.0,&_split_24); 
+  __split_1_3 = T2 + T3;
+  Lustre_slash_step(__split_1_3,2.0,&_split_25); 
+   if (V13 == _true) {
+     _split_26 = _split_24;
+   } else {
+     _split_26 = _split_25;
+   }
+  __split_1_1 = T1 + T2;
+  Lustre_slash_step(__split_1_1,2.0,&_split_23); 
+   if (V12 == _true) {
+     _split_27 = _split_23;
+   } else {
+     _split_27 = _split_26;
+   }
+  __split_11_1 = V12 & V13;
+  _split_21 = __split_11_1 & V23;
+  ___split_37_1_2 = T2 > T3;
+   if (___split_37_1_2 == _true) {
+     __split_7_2 = T2;
+   } else {
+     __split_7_2 = T3;
+   }
+  ___split_37_2_2 = T1 > __split_7_2;
+   if (___split_37_2_2 == _true) {
+     __split_8_2 = T1;
+   } else {
+     __split_8_2 = __split_7_2;
+   }
+  ___split_38_1_2 = T2 < T3;
+   if (___split_38_1_2 == _true) {
+     __split_4_2 = T2;
+   } else {
+     __split_4_2 = T3;
+   }
+  ___split_38_2_2 = T1 < __split_4_2;
+   if (___split_38_2_2 == _true) {
+     __split_5_2 = T1;
+   } else {
+     __split_5_2 = __split_4_2;
+   }
+  __split_2_2 = T1 + T2;
+  __split_3_2 = __split_2_2 + T3;
+  __split_6_2 = __split_3_2 - __split_5_2;
+  _split_22 = __split_6_2 - __split_8_2;
+   if (_split_21 == _true) {
+     _split_28 = _split_22;
+   } else {
+     _split_28 = _split_27;
+   }
+   if (_split_19 == _true) {
+     _split_29 = _split_20;
+   } else {
+     _split_29 = _split_28;
+   }
+   if (_split_18 == _true) {
+     Tguess = -999.0;
+   } else {
+     Tguess = _split_29;
+   }
+  _split_30 = Tguess == -999.0;
+  _split_31 = Tguess < 6.0;
+  Lustre_pre_get(&_split_33,&ctx->Lustre_pre_ctx_tab[0]); 
+  _split_32 = Tguess > 9.0;
+   if (_split_32 == _true) {
+     _split_34 = _false;
+   } else {
+     _split_34 = _split_33;
+   }
+   if (_split_31 == _true) {
+     _split_35 = _true;
+   } else {
+     _split_35 = _split_34;
+   }
+   if (_split_30 == _true) {
+     _split_36 = _false;
+   } else {
+     _split_36 = _split_35;
+   }
+  Lustre_arrow_step(_true,_split_36,Heat_on,&ctx->Lustre_arrow_ctx_tab[0]); 
+  Lustre_pre_set(*Heat_on,&ctx->Lustre_pre_ctx_tab[0]); 
+
+} // End of heater_control_heater_control_step
+
diff --git a/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control.h b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control.h
new file mode 100644
index 00000000..bfe8df20
--- /dev/null
+++ b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control.h
@@ -0,0 +1,30 @@
+/* This file was generated by lv6 version master.737 (2727a7744111c84f7984634d2bd3ad6f7c6c7ff9). */
+/*  lv6 -en -2cgc heater_control.lus -n heater_control */
+/* on vanoise the 15/05/2019 at 13:20:10 */
+
+#include <stdlib.h>
+#include <string.h>
+
+#include "lustre_types.h"
+#include "lustre_consts.h"
+
+#ifndef _heater_control_heater_control_H_FILE
+#define _heater_control_heater_control_H_FILE
+void Lustre_arrow_ctx_reset(Lustre_arrow_ctx_type* ctx);
+void Lustre_arrow_ctx_init(Lustre_arrow_ctx_type* ctx);
+void Lustre_arrow_step(_boolean ,_boolean ,_boolean *,Lustre_arrow_ctx_type*);
+
+void Lustre_pre_ctx_reset(Lustre_pre_ctx_type* ctx);
+void Lustre_pre_ctx_init(Lustre_pre_ctx_type* ctx);
+void Lustre_pre_get(_boolean *,Lustre_pre_ctx_type*);
+
+void Lustre_pre_set(_boolean ,Lustre_pre_ctx_type*);
+
+void Lustre_slash_step(_real ,_real ,_real *);
+
+void heater_control_heater_control_ctx_reset(heater_control_heater_control_ctx_type* ctx);
+void heater_control_heater_control_ctx_init(heater_control_heater_control_ctx_type* ctx);
+void heater_control_heater_control_step(_real ,_real ,_real ,_real ,_boolean *,heater_control_heater_control_ctx_type*);
+
+/////////////////////////////////////////////////
+#endif
diff --git a/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control_loop.c b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control_loop.c
new file mode 100644
index 00000000..e4037e5a
--- /dev/null
+++ b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control_loop.c
@@ -0,0 +1,55 @@
+/* This file was generated by lv6 version master.737 (2727a7744111c84f7984634d2bd3ad6f7c6c7ff9). */
+/*  lv6 -en -2cgc heater_control.lus -n heater_control */
+/* on vanoise the 15/05/2019 at 13:20:10 */
+
+#include <stdlib.h>
+#include <stdio.h>
+#include <unistd.h>
+#include "../dm_random.c"
+#include "heater_control_heater_control.h" 
+
+/* MACROS DEFINITIONS ****************/
+#ifndef TT
+#define TT "1"
+#endif
+#ifndef FF
+#define FF "0"
+#endif
+#ifndef BB
+#define BB "bottom"
+#endif
+#ifdef CKCHECK
+/* set this macro for testing output clocks */
+#endif
+
+/* Standard Input procedures **************/
+_real _get_real(char* n){
+  return (dm_random_uint32()%70000U) * 1E-3 -20.0;
+}
+/* Standard Output procedures **************/
+void _put_bool(char* n, _boolean b){
+  printf("%s: %d\n", n, b);
+}
+/* Main procedure *************************/
+int main(){
+  _real T;
+  _real T1;
+  _real T2;
+  _real T3;
+  _boolean Heat_on;
+  heater_control_heater_control_ctx_type ctx_struct;
+  heater_control_heater_control_ctx_type* ctx = &ctx_struct;
+  heater_control_heater_control_ctx_init(ctx);
+
+  /* Main loop */
+  for(int step=0; step<1000; step++){
+     T = _get_real("T");
+     T1 = _get_real("T1");
+     T2 = _get_real("T2");
+     T3 = _get_real("T3");
+    heater_control_heater_control_step(T,T1,T2,T3,&Heat_on,ctx);
+    _put_bool("Heat_on", Heat_on);
+  }
+  return 1;
+   
+}
diff --git a/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_consts.c b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_consts.c
new file mode 100644
index 00000000..47bfb5f5
--- /dev/null
+++ b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_consts.c
@@ -0,0 +1,4 @@
+/* This file was generated by lv6 version master.737 (2727a7744111c84f7984634d2bd3ad6f7c6c7ff9). */
+/*  lv6 -en -2cgc heater_control.lus -n heater_control */
+/* on vanoise the 15/05/2019 at 13:20:10 */
+#include "lustre_consts.h"
\ No newline at end of file
diff --git a/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_consts.h b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_consts.h
new file mode 100644
index 00000000..c2f70459
--- /dev/null
+++ b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_consts.h
@@ -0,0 +1,9 @@
+/* This file was generated by lv6 version master.737 (2727a7744111c84f7984634d2bd3ad6f7c6c7ff9). */
+/*  lv6 -en -2cgc heater_control.lus -n heater_control */
+/* on vanoise the 15/05/2019 at 13:20:10 */
+
+// Constant definitions 
+#define heater_control_DELTA 0.5
+#define heater_control_FAILURE -999.0
+#define heater_control_TMAX 9.0
+#define heater_control_TMIN 6.0
diff --git a/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_types.h b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_types.h
new file mode 100644
index 00000000..7fdfa03e
--- /dev/null
+++ b/test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_types.h
@@ -0,0 +1,41 @@
+/* This file was generated by lv6 version master.737 (2727a7744111c84f7984634d2bd3ad6f7c6c7ff9). */
+/*  lv6 -en -2cgc heater_control.lus -n heater_control */
+/* on vanoise the 15/05/2019 at 13:20:10 */
+
+#ifndef _SOC2C_PREDEF_TYPES
+#define _SOC2C_PREDEF_TYPES
+typedef int _boolean;
+typedef int _integer;
+typedef char* _string;
+typedef double _real;
+typedef double _double;
+typedef float _float;
+#define _false 0
+#define _true 1
+#endif
+// end of _SOC2C_PREDEF_TYPES
+// User typedef 
+#ifndef _heater_control_heater_control_TYPES
+#define _heater_control_heater_control_TYPES
+#endif // enf of  _heater_control_heater_control_TYPES
+// Memoryless soc ctx typedef 
+// Memoryfull soc ctx typedef 
+/* Lustre_arrow_ctx */
+typedef struct {
+   /*Memory cell*/
+   _boolean _memory ;
+} Lustre_arrow_ctx_type;
+
+/* Lustre_pre_ctx */
+typedef struct {
+   /*Memory cell*/
+   _boolean _memory ;
+} Lustre_pre_ctx_type;
+
+/* heater_control_heater_control_ctx */
+typedef struct {
+   /*INSTANCES*/
+   Lustre_pre_ctx_type Lustre_pre_ctx_tab[1];
+   Lustre_arrow_ctx_type Lustre_arrow_ctx_tab[1];
+} heater_control_heater_control_ctx_type;
+