From f72612aed2b9ec147b5e60a53c9e13b94aa71cdb Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 15 May 2019 16:44:04 +0200 Subject: compiled with Lustre v4 --- .../lustrev4_lv4_heater_control/heater_control.c | 275 +++++++++++++++++++++ .../lustrev4_lv4_heater_control/heater_control.h | 47 ++++ .../lustrev4_lv4_heater_control/heater_control.lus | 126 ++++++++++ .../heater_control_loop.c | 64 +++++ 4 files changed, 512 insertions(+) create mode 100644 test/monniaux/lustrev4_lv4_heater_control/heater_control.c create mode 100644 test/monniaux/lustrev4_lv4_heater_control/heater_control.h create mode 100644 test/monniaux/lustrev4_lv4_heater_control/heater_control.lus create mode 100644 test/monniaux/lustrev4_lv4_heater_control/heater_control_loop.c (limited to 'test/monniaux/lustrev4_lv4_heater_control') diff --git a/test/monniaux/lustrev4_lv4_heater_control/heater_control.c b/test/monniaux/lustrev4_lv4_heater_control/heater_control.c new file mode 100644 index 00000000..4a2b8174 --- /dev/null +++ b/test/monniaux/lustrev4_lv4_heater_control/heater_control.c @@ -0,0 +1,275 @@ +/******** +* ec2c version 0.67 +* c file generated for node : heater_control +* context method = HEAP +* ext call method = PROCEDURES +********/ +#include +#include +#define _heater_control_EC2C_SRC_FILE +#include "heater_control.h" +/*-------- +Internal structure for the call +--------*/ +typedef struct { + void* client_data; + //INPUTS + _real _T; + _real _T1; + _real _T2; + _real _T3; + //OUTPUTS + _boolean _Heat_on; + //REGISTERS + _boolean M73; + _boolean M73_nil; + _boolean M5; +} heater_control_ctx; +/*-------- +Output procedures must be defined, +Input procedures must be used: +--------*/ +void heater_control_I_T(heater_control_ctx* ctx, _real V){ + ctx->_T = V; +} +void heater_control_I_T1(heater_control_ctx* ctx, _real V){ + ctx->_T1 = V; +} +void heater_control_I_T2(heater_control_ctx* ctx, _real V){ + ctx->_T2 = V; +} +void heater_control_I_T3(heater_control_ctx* ctx, _real V){ + ctx->_T3 = V; +} +extern void heater_control_O_Heat_on(void* cdata, _boolean); +#ifdef CKCHECK +extern void heater_control_BOT_Heat_on(void* cdata); +#endif +/*-------- +Internal reset input procedure +--------*/ +static void heater_control_reset_input(heater_control_ctx* ctx){ + //NOTHING FOR THIS VERSION... +} +/*-------- +Reset procedure +--------*/ +void heater_control_reset(heater_control_ctx* ctx){ + ctx->M73_nil = _true; + ctx->M5 = _true; + heater_control_reset_input(ctx); +} +/*-------- +Copy the value of an internal structure +--------*/ +void heater_control_copy_ctx(heater_control_ctx* dest, heater_control_ctx +* src){ + memcpy((void*)dest, (void*)src, sizeof(heater_control_ctx)); +} +/*-------- +Dynamic allocation of an internal structure +--------*/ +heater_control_ctx* heater_control_new_ctx(void* cdata){ + heater_control_ctx* ctx = (heater_control_ctx*)calloc(1, sizeof( +heater_control_ctx)); + ctx->client_data = cdata; + heater_control_reset(ctx); + return ctx; +} +/*-------- +Step procedure +--------*/ +void heater_control_step(heater_control_ctx* ctx){ +//LOCAL VARIABLES + _real L16; + _boolean L15; + _real L18; + _real L14; + _boolean L13; + _boolean L12; + _real L24; + _boolean L23; + _real L25; + _real L22; + _boolean L21; + _boolean L20; + _boolean L11; + _real L30; + _boolean L29; + _real L31; + _real L28; + _boolean L27; + _boolean L26; + _boolean L10; + _real L32; + _boolean L38; + _boolean L37; + _boolean L40; + _boolean L39; + _boolean L36; + _boolean L42; + _boolean L41; + _boolean L35; + _real L46; + _real L45; + _boolean L50; + _real L49; + _boolean L48; + _real L47; + _real L44; + _boolean L54; + _real L53; + _boolean L52; + _real L51; + _real L43; + _boolean L57; + _boolean L56; + _real L59; + _real L63; + _real L62; + _real L65; + _real L64; + _real L61; + _real L58; + _real L55; + _real L34; + _real L9; + _boolean L8; + _boolean L68; + _boolean L71; + _boolean L70; + _boolean L67; + _boolean L7; + _boolean L4; + _boolean T73; +//CODE + L16 = (ctx->_T1 - ctx->_T2); + L15 = (L16 >= 0.000000); + L18 = (- L16); + if (L15) { + L14 = L16; + } else { + L14 = L18; + } + L13 = (L14 < 0.500000); + L12 = (! L13); + L24 = (ctx->_T1 - ctx->_T3); + L23 = (L24 >= 0.000000); + L25 = (- L24); + if (L23) { + L22 = L24; + } else { + L22 = L25; + } + L21 = (L22 < 0.500000); + L20 = (! L21); + L11 = (L12 && L20); + L30 = (ctx->_T2 - ctx->_T3); + L29 = (L30 >= 0.000000); + L31 = (- L30); + if (L29) { + L28 = L30; + } else { + L28 = L31; + } + L27 = (L28 < 0.500000); + L26 = (! L27); + L10 = (L11 && L26); + L32 = (- 999.000000); + L38 = (L13 && L20); + L37 = (L38 && L26); + L40 = (L21 && L12); + L39 = (L40 && L26); + L36 = (L37 || L39); + L42 = (L27 && L12); + L41 = (L42 && L20); + L35 = (L36 || L41); + L46 = (ctx->_T1 + ctx->_T2); + L45 = (L46 + ctx->_T3); + L50 = (ctx->_T2 < ctx->_T3); + if (L50) { + L49 = ctx->_T2; + } else { + L49 = ctx->_T3; + } + L48 = (ctx->_T1 < L49); + if (L48) { + L47 = ctx->_T1; + } else { + L47 = L49; + } + L44 = (L45 - L47); + L54 = (ctx->_T2 > ctx->_T3); + if (L54) { + L53 = ctx->_T2; + } else { + L53 = ctx->_T3; + } + L52 = (ctx->_T1 > L53); + if (L52) { + L51 = ctx->_T1; + } else { + L51 = L53; + } + L43 = (L44 - L51); + L57 = (L13 && L21); + L56 = (L57 && L27); + L59 = (L46 / 2.000000); + L63 = (ctx->_T1 + ctx->_T3); + L62 = (L63 / 2.000000); + L65 = (ctx->_T2 + ctx->_T3); + L64 = (L65 / 2.000000); + if (L21) { + L61 = L62; + } else { + L61 = L64; + } + if (L13) { + L58 = L59; + } else { + L58 = L61; + } + if (L56) { + L55 = L43; + } else { + L55 = L58; + } + if (L35) { + L34 = L43; + } else { + L34 = L55; + } + if (L10) { + L9 = L32; + } else { + L9 = L34; + } + L8 = (L9 == L32); + L68 = (L9 < 6.000000); + L71 = (L9 > 9.000000); + if (L71) { + L70 = _false; + } else { + L70 = ctx->M73; + } + if (L68) { + L67 = _true; + } else { + L67 = L70; + } + if (L8) { + L7 = _false; + } else { + L7 = L67; + } + if (ctx->M5) { + L4 = _true; + } else { + L4 = L7; + } + heater_control_O_Heat_on(ctx->client_data, L4); + T73 = L4; + ctx->M73 = T73; + ctx->M73_nil = _false; + ctx->M5 = ctx->M5 && !(_true); +} diff --git a/test/monniaux/lustrev4_lv4_heater_control/heater_control.h b/test/monniaux/lustrev4_lv4_heater_control/heater_control.h new file mode 100644 index 00000000..64be774b --- /dev/null +++ b/test/monniaux/lustrev4_lv4_heater_control/heater_control.h @@ -0,0 +1,47 @@ +/******** +* ec2c version 0.67 +* context method = HEAP +* ext call method = PROCEDURES +* c header file generated for node : heater_control +* to be used with : heater_control.c +********/ +#ifndef _heater_control_EC2C_H_FILE +#define _heater_control_EC2C_H_FILE +/*-------- Predefined types ---------*/ +#ifndef _EC2C_PREDEF_TYPES +#define _EC2C_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 +/*--------- Pragmas ----------------*/ +//MODULE: heater_control 4 1 +//IN: _real T +//IN: _real T1 +//IN: _real T2 +//IN: _real T3 +//OUT: _boolean Heat_on +#ifndef _heater_control_EC2C_SRC_FILE +/*--------Context type -------------*/ +struct heater_control_ctx; +/*-------- Input procedures -------------*/ +extern void heater_control_I_T(struct heater_control_ctx* ctx, _real); +extern void heater_control_I_T1(struct heater_control_ctx* ctx, _real); +extern void heater_control_I_T2(struct heater_control_ctx* ctx, _real); +extern void heater_control_I_T3(struct heater_control_ctx* ctx, _real); +/*-------- Reset procedure -----------*/ +extern void heater_control_reset(struct heater_control_ctx* ctx); +/*--------Context copy -------------*/ +extern void heater_control_copy_ctx(struct heater_control_ctx* dest, struct +heater_control_ctx* src); +/*--------Context allocation --------*/ +extern struct heater_control_ctx* heater_control_new_ctx(void* client_data); +/*-------- Step procedure -----------*/ +extern void heater_control_step(struct heater_control_ctx* ctx); +#endif +#endif 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 diff --git a/test/monniaux/lustrev4_lv4_heater_control/heater_control_loop.c b/test/monniaux/lustrev4_lv4_heater_control/heater_control_loop.c new file mode 100644 index 00000000..06bad418 --- /dev/null +++ b/test/monniaux/lustrev4_lv4_heater_control/heater_control_loop.c @@ -0,0 +1,64 @@ +/******** +* ec2c version 0.67 +* c main file generated for node : heater_control +* to be used with : heater_control.c +* and : heater_control.h +* context method = HEAP +* ext call method = PROCEDURES +********/ +#include +#include +#include +#include "../clock.h" +#include "../dm_random.c" +#include "heater_control.h" + +/* Print a promt ? ************************/ +static int ISATTY; +/* MACROS DEFINITIONS ****************/ +#ifndef TT +#define TT "true" +#endif +#ifndef FF +#define FF "false" +#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); +} +/* Output procedures **********************/ +void heater_control_O_Heat_on(void* cdata, _boolean _V) { + // _put_bool("Heat_on", _V); +} +/* Main procedure *************************/ +int main(){ + + /* Context allocation */ + struct heater_control_ctx* ctx = heater_control_new_ctx(NULL); + /* Main loop */ + clock_prepare(); + clock_start(); + heater_control_reset(ctx); + for(int count=0; count<1000; count++){ + heater_control_I_T(ctx, _get_real("T")); + heater_control_I_T1(ctx, _get_real("T1")); + heater_control_I_T2(ctx, _get_real("T2")); + heater_control_I_T3(ctx, _get_real("T3")); + heater_control_step(ctx); + + } + clock_stop(); + print_total_clock(); + return 0; +} -- 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_lv4_heater_control/make.proto | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 test/monniaux/lustrev4_lv4_heater_control/make.proto (limited to 'test/monniaux/lustrev4_lv4_heater_control') diff --git a/test/monniaux/lustrev4_lv4_heater_control/make.proto b/test/monniaux/lustrev4_lv4_heater_control/make.proto new file mode 100644 index 00000000..f19fec0f --- /dev/null +++ b/test/monniaux/lustrev4_lv4_heater_control/make.proto @@ -0,0 +1,3 @@ +sources: "$(wildcard *.c)" +target: lv4_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_lv4_heater_control/Makefile | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 test/monniaux/lustrev4_lv4_heater_control/Makefile (limited to 'test/monniaux/lustrev4_lv4_heater_control') diff --git a/test/monniaux/lustrev4_lv4_heater_control/Makefile b/test/monniaux/lustrev4_lv4_heater_control/Makefile new file mode 100644 index 00000000..cfd37921 --- /dev/null +++ b/test/monniaux/lustrev4_lv4_heater_control/Makefile @@ -0,0 +1,3 @@ +TARGET=lv4_heater_control + +include ../rules.mk -- cgit