From 0af2ea25f0df045d6d45ae0487c6d5022490a4c4 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 15 May 2019 13:26:34 +0200 Subject: Lustre v4 example --- .../heater_control.lus | 126 +++++++++ .../heater_control_heater_control.c | 302 +++++++++++++++++++++ .../heater_control_heater_control.h | 30 ++ .../heater_control_heater_control_loop.c | 55 ++++ .../lustre_consts.c | 4 + .../lustre_consts.h | 9 + .../lustre_types.h | 41 +++ 7 files changed, 567 insertions(+) create mode 100644 test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control.lus create mode 100644 test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control.c create mode 100644 test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control.h create mode 100644 test/monniaux/lustrev4_lv6-en-2cgc_heater_control/heater_control_heater_control_loop.c create mode 100644 test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_consts.c create mode 100644 test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_consts.h create mode 100644 test/monniaux/lustrev4_lv6-en-2cgc_heater_control/lustre_types.h (limited to 'test/monniaux/lustrev4_lv6-en-2cgc_heater_control') 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 +#include + +#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 +#include +#include +#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; + -- cgit