From 8a456dbb08948c1c24076cea6b87dc938276263b Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 15 May 2019 13:13:46 +0200 Subject: example from Lustre v4 compiled with ONERA's lustrec compiler --- .../heater_control.c | 342 +++++++++++++++++++++ .../heater_control.h | 96 ++++++ .../heater_control.lus | 126 ++++++++ .../heater_control_alloc.h | 73 +++++ .../heater_control_main.c | 42 +++ 5 files changed, 679 insertions(+) create mode 100644 test/monniaux/lustrev4_lustrec_heater_control/heater_control.c create mode 100644 test/monniaux/lustrev4_lustrec_heater_control/heater_control.h create mode 100644 test/monniaux/lustrev4_lustrec_heater_control/heater_control.lus create mode 100644 test/monniaux/lustrev4_lustrec_heater_control/heater_control_alloc.h create mode 100644 test/monniaux/lustrev4_lustrec_heater_control/heater_control_main.c (limited to 'test/monniaux/lustrev4_lustrec_heater_control') diff --git a/test/monniaux/lustrev4_lustrec_heater_control/heater_control.c b/test/monniaux/lustrev4_lustrec_heater_control/heater_control.c new file mode 100644 index 00000000..6025cd13 --- /dev/null +++ b/test/monniaux/lustrev4_lustrec_heater_control/heater_control.c @@ -0,0 +1,342 @@ +#include +#include "heater_control.h" + +/* C code generated by lustrec + Version number 1.6-@GITBRANCH@ + Code is C99 compliant + Using (double) floating-point numbers */ + +/* Import dependencies */ + +/* Global constants (definitions) */ +double FAILURE = -999.0; +double TMIN = 6.0; +double TMAX = 9.0; +double DELTA = 0.5; + +/* Struct definitions */ +struct not_a_sauna2_mem {struct not_a_sauna2_reg {double __not_a_sauna2_2; + } _reg; + struct _arrow_mem *ni_0; + }; +struct heater_control_mem {struct heater_control_reg {_Bool __heater_control_16; + } _reg; + struct _arrow_mem *ni_1; + }; +struct not_a_sauna_mem {struct not_a_sauna_reg {double __not_a_sauna_2; + } _reg; + struct _arrow_mem *ni_2; + }; + + +void not_a_sauna2_reset (struct not_a_sauna2_mem *self) { + + _arrow_reset(self->ni_0); + return; +} + +void not_a_sauna2_step (double T, double T1, double T2, double T3, + _Bool Heat_on, + _Bool (*ok), + struct not_a_sauna2_mem *self) { + _Bool __not_a_sauna2_1; + + + _arrow_step (1, 0, &__not_a_sauna2_1, self->ni_0); + if (__not_a_sauna2_1) { + *ok = 1; + } else { + *ok = (self->_reg.__not_a_sauna2_2 < (9.0 - 6.0)); + } + self->_reg.__not_a_sauna2_2 = T; + + return; +} + +void heater_control_reset (struct heater_control_mem *self) { + + _arrow_reset(self->ni_1); + return; +} + +void heater_control_step (double T, double T1, double T2, double T3, + _Bool (*Heat_on), + struct heater_control_mem *self) { + double Median_42_max2_150_m; + double Median_42_max2_152_m; + double Median_42_min2_141_m; + double Median_42_min2_143_m; + double Median_52_max2_150_m; + double Median_52_max2_152_m; + double Median_52_min2_141_m; + double Median_52_min2_143_m; + double Tguess; + _Bool V12; + _Bool V13; + _Bool V23; + _Bool __heater_control_12; + double abs_15_a; + double abs_15_v; + double abs_23_a; + double abs_23_v; + double abs_7_a; + double abs_7_v; + + + + + + + + + + + + + + + + + + + + + abs_7_v = (T1 - T2); + if ((abs_7_v >= 0.0)) { + abs_7_a = abs_7_v; + } else { + abs_7_a = (- abs_7_v); + } + abs_23_v = (T2 - T3); + if ((abs_23_v >= 0.0)) { + abs_23_a = abs_23_v; + } else { + abs_23_a = (- abs_23_v); + } + abs_15_v = (T1 - T3); + if ((abs_15_v >= 0.0)) { + abs_15_a = abs_15_v; + } else { + abs_15_a = (- abs_15_v); + } + V23 = (abs_23_a < 0.5); + V13 = (abs_15_a < 0.5); + V12 = (abs_7_a < 0.5); + if ((T2 < T3)) { + Median_52_min2_141_m = T2; + } else { + Median_52_min2_141_m = T3; + } + if ((T2 > T3)) { + Median_42_max2_150_m = T2; + } else { + Median_42_max2_150_m = T3; + } + if ((T2 < T3)) { + Median_42_min2_141_m = T2; + } else { + Median_42_min2_141_m = T3; + } + if ((T2 > T3)) { + Median_52_max2_150_m = T2; + } else { + Median_52_max2_150_m = T3; + } + if ((T1 < Median_52_min2_141_m)) { + Median_52_min2_143_m = T1; + } else { + Median_52_min2_143_m = Median_52_min2_141_m; + } + if ((T1 > Median_52_max2_150_m)) { + Median_52_max2_152_m = T1; + } else { + Median_52_max2_152_m = Median_52_max2_150_m; + } + if ((T1 < Median_42_min2_141_m)) { + Median_42_min2_143_m = T1; + } else { + Median_42_min2_143_m = Median_42_min2_141_m; + } + if ((T1 > Median_42_max2_150_m)) { + Median_42_max2_152_m = T1; + } else { + Median_42_max2_152_m = Median_42_max2_150_m; + } + if ((((!V12) && (!V13)) && (!V23))) { + Tguess = -999.0; + } else { + if (((((V12 && (!V13)) && (!V23)) || ((V13 && (!V12)) && (!V23))) || ((V23 && (!V12)) && (!V13)))) { + Tguess = ((((T1 + T2) + T3) - Median_42_min2_143_m) - Median_42_max2_152_m); + } else { + if (((V12 && V13) && V23)) { + Tguess = ((((T1 + T2) + T3) - Median_52_min2_143_m) - Median_52_max2_152_m); + } else { + if (V12) { + Tguess = ((T1 + T2) / 2.0); + } else { + if (V13) { + Tguess = ((T1 + T3) / 2.0); + } else { + Tguess = ((T2 + T3) / 2.0); + } + } + } + } + } + _arrow_step (1, 0, &__heater_control_12, self->ni_1); + if (__heater_control_12) { + *Heat_on = 1; + } else { + if ((Tguess == -999.0)) { + *Heat_on = 0; + } else { + if ((Tguess < 6.0)) { + *Heat_on = 1; + } else { + if ((Tguess > 9.0)) { + *Heat_on = 0; + } else { + *Heat_on = self->_reg.__heater_control_16; + } + } + } + } + self->_reg.__heater_control_16 = *Heat_on; + + + + + + + + + + + + + + + + + + + + return; +} + +void not_a_sauna_reset (struct not_a_sauna_mem *self) { + + _arrow_reset(self->ni_2); + return; +} + +void not_a_sauna_step (double T, double T1, double T2, double T3, + _Bool Heat_on, + _Bool (*ok), + struct not_a_sauna_mem *self) { + _Bool __not_a_sauna_1; + + + _arrow_step (1, 0, &__not_a_sauna_1, self->ni_2); + if (__not_a_sauna_1) { + *ok = 1; + } else { + *ok = (self->_reg.__not_a_sauna_2 < (9.0 + 1.0)); + } + self->_reg.__not_a_sauna_2 = T; + + return; +} + +void oneoftree_step (_Bool f1, _Bool f2, _Bool f3, + _Bool (*r) + ) { + + *r = ((((f1 && (!f2)) && (!f3)) || ((f2 && (!f1)) && (!f3))) || ((f3 && (!f1)) && (!f2))); + return; +} + +void noneoftree_step (_Bool f1, _Bool f2, _Bool f3, + _Bool (*r) + ) { + + *r = (((!f1) && (!f2)) && (!f3)); + return; +} + +void alloftree_step (_Bool f1, _Bool f2, _Bool f3, + _Bool (*r) + ) { + + *r = ((f1 && f2) && f3); + return; +} + +void abs_step (double v, + double (*a) + ) { + + if ((v >= 0.0)) { + *a = v; + } else { + *a = (- v); + } + return; +} + +void Median_step (double a, double b, double c, + double (*z) + ) { + double __Median_1; + double __Median_2; + double __Median_3; + double __Median_4; + + + + + + min2_step (b, c, &__Median_3); + min2_step (a, __Median_3, &__Median_4); + max2_step (b, c, &__Median_1); + max2_step (a, __Median_1, &__Median_2); + *z = ((((a + b) + c) - __Median_4) - __Median_2); + + + + + return; +} + +void Average_step (double a, double b, + double (*z) + ) { + + *z = ((a + b) / 2.0); + return; +} + +void min2_step (double one, double two, + double (*m) + ) { + + if ((one < two)) { + *m = one; + } else { + *m = two; + } + return; +} + +void max2_step (double one, double two, + double (*m) + ) { + + if ((one > two)) { + *m = one; + } else { + *m = two; + } + return; +} + diff --git a/test/monniaux/lustrev4_lustrec_heater_control/heater_control.h b/test/monniaux/lustrev4_lustrec_heater_control/heater_control.h new file mode 100644 index 00000000..d25a7d52 --- /dev/null +++ b/test/monniaux/lustrev4_lustrec_heater_control/heater_control.h @@ -0,0 +1,96 @@ +/* C code generated by lustrec + Version number 1.6-@GITBRANCH@ + Code is C99 compliant + Using (double) floating-point numbers */ + +#ifndef _HEATER_CONTROL +#define _HEATER_CONTROL + +/* Imports standard library */ +#include +#include "/opt/lustrec/1.6/include/lustrec/arrow.h" + + +/* Import dependencies */ + +/* Types definitions */ + +/* Global constant (declarations, definitions are in C file) */ +extern double FAILURE; +extern double TMIN; +extern double TMAX; +extern double DELTA; + +/* Structs declarations */ +struct not_a_sauna2_mem; +struct heater_control_mem; +struct not_a_sauna_mem; + +/* Nodes declarations */ +extern void not_a_sauna2_reset (struct not_a_sauna2_mem *self); + +extern void not_a_sauna2_init (struct not_a_sauna2_mem *self); + +extern void not_a_sauna2_clear (struct not_a_sauna2_mem *self); + +extern void not_a_sauna2_step (double T, double T1, double T2, double T3, + _Bool Heat_on, + _Bool (*ok), + struct not_a_sauna2_mem *self); + +extern void heater_control_reset (struct heater_control_mem *self); + +extern void heater_control_init (struct heater_control_mem *self); + +extern void heater_control_clear (struct heater_control_mem *self); + +extern void heater_control_step (double T, double T1, double T2, double T3, + _Bool (*Heat_on), + struct heater_control_mem *self); + +extern void not_a_sauna_reset (struct not_a_sauna_mem *self); + +extern void not_a_sauna_init (struct not_a_sauna_mem *self); + +extern void not_a_sauna_clear (struct not_a_sauna_mem *self); + +extern void not_a_sauna_step (double T, double T1, double T2, double T3, + _Bool Heat_on, + _Bool (*ok), + struct not_a_sauna_mem *self); + +extern void oneoftree_step (_Bool f1, _Bool f2, _Bool f3, + _Bool (*r) + ); + +extern void noneoftree_step (_Bool f1, _Bool f2, _Bool f3, + _Bool (*r) + ); + +extern void alloftree_step (_Bool f1, _Bool f2, _Bool f3, + _Bool (*r) + ); + +extern void abs_step (double v, + double (*a) + ); + +extern void Median_step (double a, double b, double c, + double (*z) + ); + +extern void Average_step (double a, double b, + double (*z) + ); + +extern void min2_step (double one, double two, + double (*m) + ); + +extern void max2_step (double one, double two, + double (*m) + ); + + +#endif + diff --git a/test/monniaux/lustrev4_lustrec_heater_control/heater_control.lus b/test/monniaux/lustrev4_lustrec_heater_control/heater_control.lus new file mode 100644 index 00000000..9a668a47 --- /dev/null +++ b/test/monniaux/lustrev4_lustrec_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_lustrec_heater_control/heater_control_alloc.h b/test/monniaux/lustrev4_lustrec_heater_control/heater_control_alloc.h new file mode 100644 index 00000000..270ed4a3 --- /dev/null +++ b/test/monniaux/lustrev4_lustrec_heater_control/heater_control_alloc.h @@ -0,0 +1,73 @@ +/* C code generated by lustrec + Version number 1.6-@GITBRANCH@ + Code is C99 compliant + Using (double) floating-point numbers */ + +#ifndef _HEATER_CONTROL_alloc +#define _HEATER_CONTROL_alloc + +/* Import header from heater_control */ +#include "heater_control.h" + +/* Import dependencies */ + +/* Struct definitions */ +struct not_a_sauna2_mem {struct not_a_sauna2_reg {double __not_a_sauna2_2; + } _reg; + struct _arrow_mem *ni_0; + }; +struct heater_control_mem {struct heater_control_reg {_Bool __heater_control_16; + } _reg; + struct _arrow_mem *ni_1; + }; +struct not_a_sauna_mem {struct not_a_sauna_reg {double __not_a_sauna_2; + } _reg; + struct _arrow_mem *ni_2; + }; + +/* Node allocation function/macro prototypes */ +#define not_a_sauna2_DECLARE(attr, inst)\ + attr struct not_a_sauna2_mem inst;\ + _arrow_DECLARE(attr, inst ## _ni_0); + +#define not_a_sauna2_LINK(inst) do {\ + _arrow_LINK(inst ## _ni_0);\ + inst.ni_0 = &inst ## _ni_0;\ +} while (0) + +#define not_a_sauna2_ALLOC(attr, inst)\ + not_a_sauna2_DECLARE(attr, inst);\ + not_a_sauna2_LINK(inst); + + +#define heater_control_DECLARE(attr, inst)\ + attr struct heater_control_mem inst;\ + _arrow_DECLARE(attr, inst ## _ni_1); + +#define heater_control_LINK(inst) do {\ + _arrow_LINK(inst ## _ni_1);\ + inst.ni_1 = &inst ## _ni_1;\ +} while (0) + +#define heater_control_ALLOC(attr, inst)\ + heater_control_DECLARE(attr, inst);\ + heater_control_LINK(inst); + + +#define not_a_sauna_DECLARE(attr, inst)\ + attr struct not_a_sauna_mem inst;\ + _arrow_DECLARE(attr, inst ## _ni_2); + +#define not_a_sauna_LINK(inst) do {\ + _arrow_LINK(inst ## _ni_2);\ + inst.ni_2 = &inst ## _ni_2;\ +} while (0) + +#define not_a_sauna_ALLOC(attr, inst)\ + not_a_sauna_DECLARE(attr, inst);\ + not_a_sauna_LINK(inst); + + + +#endif + diff --git a/test/monniaux/lustrev4_lustrec_heater_control/heater_control_main.c b/test/monniaux/lustrev4_lustrec_heater_control/heater_control_main.c new file mode 100644 index 00000000..f985e2af --- /dev/null +++ b/test/monniaux/lustrev4_lustrec_heater_control/heater_control_main.c @@ -0,0 +1,42 @@ +#include +#include +#include +#include +#include "heater_control_alloc.h" +#include "../dm_random.c" + +static double _get_double(void) { + return (dm_random_uint32()%70000U) * 1E-3 -20.0; +} + +static void _put_bool(const char *name, _Bool b) { + printf("%s: %d\n", name, b); +} + +/* C code generated by lustrec + Version number 1.6-@GITBRANCH@ + Code is C99 compliant + Using (double) floating-point numbers */ + +int main (int argc, char *argv[]) { + + /* Main memory allocation */ + heater_control_ALLOC(static,main_mem); + + /* Initialize the main memory */ + heater_control_reset(&main_mem); + + /* Infinite loop */ + while(1){ + double T = _get_double(); + double T1 = _get_double(); + double T2 = _get_double(); + double T3 = _get_double(); + _Bool Heat_on; + heater_control_step (T, T1, T2, T3, &Heat_on, &main_mem); + _put_bool("Heat_on", Heat_on); + } + + + return 1; +} -- cgit 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 --- test/monniaux/lustrev4_lustrec_heater_control/heater_control_main.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test/monniaux/lustrev4_lustrec_heater_control') diff --git a/test/monniaux/lustrev4_lustrec_heater_control/heater_control_main.c b/test/monniaux/lustrev4_lustrec_heater_control/heater_control_main.c index f985e2af..351deed6 100644 --- a/test/monniaux/lustrev4_lustrec_heater_control/heater_control_main.c +++ b/test/monniaux/lustrev4_lustrec_heater_control/heater_control_main.c @@ -27,7 +27,7 @@ int main (int argc, char *argv[]) { heater_control_reset(&main_mem); /* Infinite loop */ - while(1){ + for(int loop_count=0; loop_count<1000; loop_count++){ double T = _get_double(); double T1 = _get_double(); double T2 = _get_double(); -- cgit From 355a9272b5a800f9652707ed5854d7be529b872c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 15 May 2019 13:39:01 +0200 Subject: Heater example from Lustre v4 --- .../lustrev4_lustrec_heater_control/heater_control_main.c | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'test/monniaux/lustrev4_lustrec_heater_control') diff --git a/test/monniaux/lustrev4_lustrec_heater_control/heater_control_main.c b/test/monniaux/lustrev4_lustrec_heater_control/heater_control_main.c index 351deed6..d0298840 100644 --- a/test/monniaux/lustrev4_lustrec_heater_control/heater_control_main.c +++ b/test/monniaux/lustrev4_lustrec_heater_control/heater_control_main.c @@ -3,6 +3,7 @@ #include #include #include "heater_control_alloc.h" +#include "../clock.h" #include "../dm_random.c" static double _get_double(void) { @@ -22,6 +23,9 @@ int main (int argc, char *argv[]) { /* Main memory allocation */ heater_control_ALLOC(static,main_mem); + + clock_prepare(); + clock_start(); /* Initialize the main memory */ heater_control_reset(&main_mem); @@ -34,9 +38,11 @@ int main (int argc, char *argv[]) { double T3 = _get_double(); _Bool Heat_on; heater_control_step (T, T1, T2, T3, &Heat_on, &main_mem); - _put_bool("Heat_on", Heat_on); + // _put_bool("Heat_on", Heat_on); } + clock_stop(); + print_total_clock(); return 1; } -- cgit From 33cc0aeef68f3adbb51484dbeafccfca5735f8ee Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 6 Jun 2019 12:01:53 +0200 Subject: some more benchmarks --- test/monniaux/lustrev4_lustrec_heater_control/make.proto | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 test/monniaux/lustrev4_lustrec_heater_control/make.proto (limited to 'test/monniaux/lustrev4_lustrec_heater_control') diff --git a/test/monniaux/lustrev4_lustrec_heater_control/make.proto b/test/monniaux/lustrev4_lustrec_heater_control/make.proto new file mode 100644 index 00000000..ccb0e684 --- /dev/null +++ b/test/monniaux/lustrev4_lustrec_heater_control/make.proto @@ -0,0 +1,3 @@ +sources: "$(wildcard *.c)" +target: lustrec_heater_control +measures: [cycles] -- cgit From c1af49a809efe593317c2b836be115e24e7b8f18 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 19 Jun 2019 11:31:04 +0200 Subject: add arrow.h from LustreC --- .../lustrev4_lustrec_heater_control/arrow.h | 34 ++++++ .../heater_control.h | 2 +- .../heater_control.lus | 126 --------------------- .../lustrev4_lustrec_heater_control/make.proto | 3 - 4 files changed, 35 insertions(+), 130 deletions(-) create mode 100644 test/monniaux/lustrev4_lustrec_heater_control/arrow.h delete mode 100644 test/monniaux/lustrev4_lustrec_heater_control/heater_control.lus delete mode 100644 test/monniaux/lustrev4_lustrec_heater_control/make.proto (limited to 'test/monniaux/lustrev4_lustrec_heater_control') diff --git a/test/monniaux/lustrev4_lustrec_heater_control/arrow.h b/test/monniaux/lustrev4_lustrec_heater_control/arrow.h new file mode 100644 index 00000000..802057da --- /dev/null +++ b/test/monniaux/lustrev4_lustrec_heater_control/arrow.h @@ -0,0 +1,34 @@ + +#ifndef _ARROW +#define _ARROW + +struct _arrow_mem {struct _arrow_reg {_Bool _first; } _reg; }; + +extern struct _arrow_mem *_arrow_alloc (); + +extern void _arrow_dealloc (struct _arrow_mem *); + +#define _arrow_DECLARE(attr, inst)\ + attr struct _arrow_mem inst; + +#define _arrow_LINK(inst) do {\ + ;\ +} while (0) + +#define _arrow_ALLOC(attr, inst)\ + _arrow_DECLARE(attr, inst);\ + _arrow_LINK(inst) + +#define _arrow_init(self) {} + +#define _arrow_clear(self) {} + +#define _arrow_step(x,y,output,self) ((self)->_reg._first?((self)->_reg._first=0,(*output = x)):(*output = y)) + +#define _arrow_reset(self) {(self)->_reg._first = 1;} + +/* Step macro for specialized arrows of the form: (true -> false) */ + +#define _once_step(output,self) { *output = (self)->_reg._first; if ((self)->_reg._first) { (self)->_reg._first=0; }; } + +#endif diff --git a/test/monniaux/lustrev4_lustrec_heater_control/heater_control.h b/test/monniaux/lustrev4_lustrec_heater_control/heater_control.h index d25a7d52..405f9a74 100644 --- a/test/monniaux/lustrev4_lustrec_heater_control/heater_control.h +++ b/test/monniaux/lustrev4_lustrec_heater_control/heater_control.h @@ -8,7 +8,7 @@ /* Imports standard library */ #include -#include "/opt/lustrec/1.6/include/lustrec/arrow.h" +#include "arrow.h" /* Import dependencies */ diff --git a/test/monniaux/lustrev4_lustrec_heater_control/heater_control.lus b/test/monniaux/lustrev4_lustrec_heater_control/heater_control.lus deleted file mode 100644 index 9a668a47..00000000 --- a/test/monniaux/lustrev4_lustrec_heater_control/heater_control.lus +++ /dev/null @@ -1,126 +0,0 @@ --- --- 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_lustrec_heater_control/make.proto b/test/monniaux/lustrev4_lustrec_heater_control/make.proto deleted file mode 100644 index ccb0e684..00000000 --- a/test/monniaux/lustrev4_lustrec_heater_control/make.proto +++ /dev/null @@ -1,3 +0,0 @@ -sources: "$(wildcard *.c)" -target: lustrec_heater_control -measures: [cycles] -- cgit From 83f7c0dfc0454b7b457bc55f352133fa831cc861 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 19 Jun 2019 14:36:32 +0200 Subject: Missing make.proto of lustrev4_lustrec --- test/monniaux/lustrev4_lustrec_heater_control/make.proto | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 test/monniaux/lustrev4_lustrec_heater_control/make.proto (limited to 'test/monniaux/lustrev4_lustrec_heater_control') diff --git a/test/monniaux/lustrev4_lustrec_heater_control/make.proto b/test/monniaux/lustrev4_lustrec_heater_control/make.proto new file mode 100644 index 00000000..ccb0e684 --- /dev/null +++ b/test/monniaux/lustrev4_lustrec_heater_control/make.proto @@ -0,0 +1,3 @@ +sources: "$(wildcard *.c)" +target: lustrec_heater_control +measures: [cycles] -- cgit From b288b587378984c3c419d26a13dcf93686d1b779 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 17 Jul 2019 12:03:39 +0200 Subject: All working benches ported --- test/monniaux/lustrev4_lustrec_heater_control/Makefile | 3 +++ test/monniaux/lustrev4_lustrec_heater_control/make.proto | 3 --- 2 files changed, 3 insertions(+), 3 deletions(-) create mode 100644 test/monniaux/lustrev4_lustrec_heater_control/Makefile delete mode 100644 test/monniaux/lustrev4_lustrec_heater_control/make.proto (limited to 'test/monniaux/lustrev4_lustrec_heater_control') diff --git a/test/monniaux/lustrev4_lustrec_heater_control/Makefile b/test/monniaux/lustrev4_lustrec_heater_control/Makefile new file mode 100644 index 00000000..df7c9e0a --- /dev/null +++ b/test/monniaux/lustrev4_lustrec_heater_control/Makefile @@ -0,0 +1,3 @@ +TARGET=lustrec_heater_control + +include ../rules.mk diff --git a/test/monniaux/lustrev4_lustrec_heater_control/make.proto b/test/monniaux/lustrev4_lustrec_heater_control/make.proto deleted file mode 100644 index ccb0e684..00000000 --- a/test/monniaux/lustrev4_lustrec_heater_control/make.proto +++ /dev/null @@ -1,3 +0,0 @@ -sources: "$(wildcard *.c)" -target: lustrec_heater_control -measures: [cycles] -- cgit