Project

General

Profile

Revision 47714cf4

View differences:

regression_tests/lustre_files/success/CMakeLists.txt
10 10
add_subdirectory(linear_ctl)
11 11
add_subdirectory(mpfr)
12 12
add_subdirectory(lusic)
13
add_subdirectory(safety)
regression_tests/lustre_files/success/safety/CMakeLists.txt
1
cmake_minimum_required(VERSION 2.8.4)
2
include(FindUnixCommands)
3

  
4
set(GLOBAL_LUSTRE_FILES "")
5
LUSTREFILES(LFILES ${CMAKE_CURRENT_SOURCE_DIR} )
6
list(APPEND GLOBAL_LUSTRE_FILES ${LFILES})
7
FOREACH(lfile ${LFILES})
8
	get_filename_component(L ${lfile} NAME_WE)
9
	set(LUSTRE_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/${L}")
10
	file(COPY ${lfile}   DESTINATION  ${LUSTRE_OUTPUT_DIR})
11
	if(EXISTS ${CMAKE_CURRENT_SOURCE_DIR}/${L}.lusi)
12
		file(COPY  ${L}.lusi DESTINATION  ${LUSTRE_OUTPUT_DIR})
13
	else()
14
		message("generate ${L}.lusi \n")
15
		Lustre_Compile(LUS_FILE ${lfile}
16
				NODE ""
17
				OPTS "-lusi")				
18
		set(LUS_OPTS_CUT ${LUSTRE_OPTS_POSTFIX_${L}})
19
		execute_process(RESULT_VARIABLE res 
20
					COMMAND ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}__${LUS_OPTS_CUT}} 
21
					WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR})
22
		if(${res} STREQUAL "0")
23
			file(COPY  ${L}.lusi DESTINATION  ${LUSTRE_OUTPUT_DIR})
24
		else()
25
			message("${L}.lusi Error")
26
		endif()
27
	endif()
28
	if(EXISTS ${CMAKE_CURRENT_SOURCE_DIR}/${L}_input_values)
29
		file(COPY  ${L}_input_values DESTINATION  ${LUSTRE_OUTPUT_DIR})
30
	elseif(EXISTS ${CMAKE_CURRENT_SOURCE_DIR}/${L}.lusi)
31
		message("generate input_values \n")
32
		execute_process(RESULT_VARIABLE res 
33
					COMMAND ${JAVA_RUNTIME} -cp ${CMAKE_BINARY_DIR}/modules/ Generate_inputs_lusi top ${L}.lusi 1
34
					WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR})
35
		if(${res} STREQUAL "0")
36
			file(COPY  ${L}_input_values DESTINATION  ${LUSTRE_OUTPUT_DIR})
37
		else()
38
			message("${L}_input_values Error")
39
		endif()
40
	endif()
41
	if(EXISTS ${CMAKE_CURRENT_SOURCE_DIR}/${L}_output_values)
42
		file(COPY  ${L}_output_values DESTINATION  ${LUSTRE_OUTPUT_DIR})
43
	elseif(EXISTS ${CMAKE_CURRENT_SOURCE_DIR}/${L}_input_values)
44
		message("generate output_values for reference \n")
45
		set(LUSTRE_NODE_OPT  "${L}")
46
		
47
		Lustre_Compile(LUS_FILE ${lfile}
48
						NODE ${LUSTRE_NODE_OPT} 
49
						OPTS ""
50
						DIR ${CMAKE_CURRENT_SOURCE_DIR})
51
						
52
		set(LUS_OPTS_CUT ${LUSTRE_OPTS_POSTFIX_${L}})
53
		
54
		execute_process(
55
					COMMAND ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}} 
56
					WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR})			
57
		execute_process(
58
					COMMAND  make -f ${L}.makefile
59
					WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR})	
60
		execute_process(RESULT_VARIABLE res 
61
					COMMAND ${BASH} -c "./${L}_${LUSTRE_NODE_OPT} < ${L}_input_values > ${L}_output_values"
62
					WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR})	
63
		file(REMOVE ${L}_${LUSTRE_NODE_OPT} io_frontend.o ${L}.c ${L}.h ${L}.lusic ${L}.makefile ${L}.o ${L}_alloc.h ${L}_main.c ${L}_main.o )
64
		if(${res} STREQUAL "0")
65
			file(COPY  ${L}_output_values DESTINATION  ${LUSTRE_OUTPUT_DIR})
66
		else()
67
			message("${L} output_values Error")
68
		endif()
69
	endif()
70
ENDFOREACH()
71

  
72

  
73
FOREACH(lus_file ${GLOBAL_LUSTRE_FILES})
74
	get_filename_component(L ${lus_file} NAME_WE)
75
	set(LUSTRE_NODE_OPT  "${L}")
76

  
77

  
78
	#first combination :mpfr
79
	set(LUSTRE_OPTIONS_OPT "-mpfr" "100")
80
	set(EPSILON "0.0001")
81
	
82
	# First command generate C files from Lustre file
83
	Lustre_Compile(LUS_FILE ${lus_file}
84
					NODE ${LUSTRE_NODE_OPT}
85
					OPTS ${LUSTRE_OPTIONS_OPT}
86
					CALL_ID "2")
87
					
88
	set(LUS_OPTS_CUT_2 "${LUSTRE_OPTS_POSTFIX_${L}_2}")
89
	add_test(NAME safety_plane_archi_COMPIL_LUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}
90
			COMMAND  ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}} 
91
	)
92

  
93
	 #********************* make -f ${L}.makefile ***************************
94
	 add_test(NAME safety_plane_archi_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}
95
			COMMAND  make -f ${L}.makefile
96
			WORKING_DIRECTORY ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}}
97
	)
98
	SET_TESTS_PROPERTIES ( safety_plane_archi_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}
99
	 PROPERTIES DEPENDS safety_plane_archi_COMPIL_LUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}
100
				REQUIRED_FILES ${L}.makefile
101
				)
102
	 
103
	 #************** execute C binary **********************************
104
	
105
	if (BASH)
106
		add_test(
107
			NAME safety_plane_archi_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2} 
108
			COMMAND ${BASH} -c "./${L}_${LUSTRE_NODE_OPT} < ../${L}_input_values > ${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}_outputs"
109
			WORKING_DIRECTORY ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}}
110
		)
111
		SET_TESTS_PROPERTIES ( safety_plane_archi_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}
112
			PROPERTIES REQUIRED_FILES ${L}_${LUSTRE_NODE_OPT}
113
				DEPENDS safety_plane_archi_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2})
114
	else()
115
		message(FATAL_ERROR "Unknown shell command ${BASH} -c for ${CMAKE_HOST_SYSTEM_NAME}")
116
	endif()
117
	
118
	 #************** execute C binary **********************************
119
	 add_test(NAME safety_plane_archi_DIFF_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}
120
COMMAND ${JAVA_RUNTIME} -cp ${CMAKE_BINARY_DIR}/modules/ compare_lustrec_outputs ${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}_outputs ../${L}_output_values ${EPSILON}
121
	   WORKING_DIRECTORY ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}}
122
	)
123
	SET_TESTS_PROPERTIES ( safety_plane_archi_DIFF_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}
124
	 PROPERTIES REQUIRED_FILES ${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2}_outputs
125
				DEPENDS safety_plane_archi_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT_2} )
126
	
127
ENDFOREACH()
128

  
129
add_custom_target(safety_plane_archi COMMAND ${CMAKE_CTEST_COMMAND} -R safety_plane_archi)
130

  
regression_tests/lustre_files/success/safety/safety_plane_archi.lus
1
-- y is true if the property x is true at least n succesive times.
2
-- nb_times is a positive integer which increases by 1 each time x is true
3
-- and decreases by 1 each time x is false.
4
-- the idea was: x is the error output of a sensor and y has been true
5
-- if nb_times equals 0 again, perhaps the sensor is fine again
6

  
7
--@ requires n > 0;
8
--@ ensures (not x) => (not y);
9
--@ ensures nb_times >= 0;
10
--@ ensures not x => ((pre nb_times > nb_times) or (pre nb_times = 0));
11
--@ ensures x => (pre nb_times < nb_times);
12
--@ ensures y => nb_times >= n;
13
node check_validity (x: bool; n: int) returns (y: bool; nb_times: int);
14
var
15
compt: int;
16
let
17
  compt = (if x then 1 else 0) -> if x then pre compt + 1 else 0;
18
  y = (compt >= n);
19
  nb_times= (if x then 1 else 0) -> 
20
    if x then pre nb_times + 1 else 
21
      (if pre nb_times > 0 then pre nb_times - 1 else 0);
22
tel
23

  
24

  
25
-- at the beginning, y = x
26
-- once x is true, y is true until reset is true
27
-- if reset is true, y = x
28

  
29
--@ ensures reset => y=x;
30
--@ ensures x => y;
31
--@ ensures pre y and not reset => y;
32
node lock (x, reset: bool) returns (y: bool);
33
let
34
y = x -> if reset then x else x or pre y;
35
tel
36

  
37

  
38
-- combination of check_validity and lock
39

  
40
--@ requires n > 0;
41
--@ ensures x => y;
42
--@ ensures (pre y and not y) => (not x);
43
node check_validity_lock (x: bool; n: int) returns (y: bool);
44
var
45
  nb_times: int;
46
  er: bool;
47
let
48
	(er, nb_times) = check_validity(x, n);
49
	y = x or lock(er, (nb_times = 0));
50
tel
51

  
52

  
53
-- check if the input is not changing too fast
54

  
55
--@ requires delta > 0.;
56
--@ ensures abs_1(v - pre v) <= delta;
57
node check_speed (s, delta: real) returns (v: real);
58
let
59
	v = s -> if s - pre v > delta 
60
	      	 then 
61
		      pre v + delta
62
		 else 
63
		      if pre v - s > delta
64
		      then
65
			  pre v - delta 
66
		       else s;
67
tel
68

  
69
-- the classic absolute value function
70

  
71
--@ ensures y >= 0.0;
72
--@ ensures (x >= 0.0) => (x = y);
73
--@ ensures (x <= 0.0) => (x = -y);
74
node abs_1 (x: real) returns (y: real);
75
let
76
  y= if x>0.0 then x else -x;
77
tel
78

  
79
-- ensures that the ranged_val output is between min and max.
80
-- [min , max] is the legal interval where the value must be
81
-- [min - delta , max + delta] is the interval the input value is allowed to be
82
-- delta can match for instance with the uncertainty of measurement
83
-- satmax => value > max
84
-- satmin => value < min
85
-- "error" occurs if the input value is out of [min - delta, max + delta]
86

  
87
--@ requires delta > 0.0;
88
--@ requires min <= max;
89
--@ ensures min <= ranged_val and ranged_val <= max;
90
--@ ensures ((min <= value) and (value <= max)) => (ranged_val = value);
91
--@ ensures (value < min) => satmin;
92
--@ ensures (max < value) => satmax;
93
--@ ensures satmin => (value < min);
94
--@ ensures satmax => (max <= value);
95
--@ ensures value < min => ranged_val = min;
96
--@ ensures value > value => ranged_val = max;
97
--@ ensures error => satmin or satmax;
98
--@ ensures delta + max < value => error;
99
--@ ensures value < min - delta => error;
100

  
101

  
102
node ranged_value (value, min, max, delta: real) returns (ranged_val:real; satmin, satmax, error: bool);
103
let
104
  satmin = value < min;
105
  satmax = value > max;
106
  error = (value > max + delta) or (value < min - delta);
107
  ranged_val = if value > max then max else (if value < min then min else value);
108
tel
109

  
110

  
111
-- checks if the node "aberration" has valid outputs 
112

  
113
node obs_aberration(s1,s2,s3,delta: real; ab1,ab2,ab3: bool) 
114
returns (ok_ab1, ok_ab2, ok_ab3, ok_rev1, ok_rev2, ok_rev3: bool);
115
var
116
  diff12, diff13, diff23: real;
117
let
118
  diff12 = abs_1(s1 - s2);
119
  diff13 = abs_1(s1 - s3);
120
  diff23 = abs_1(s2 - s3);
121
  ok_ab1 = (ab1 => (diff12 > delta and diff13 > delta));
122
  ok_ab2 = (ab2 => (diff12 > delta and diff23 > delta));
123
  ok_ab3 = (ab3 => (diff13 > delta and diff23 > delta));
124
  ok_rev1 = ((diff12 > delta and diff13 > delta) => ab1 );
125
  ok_rev2 = ((diff12 > delta and diff23 > delta) => ab2);
126
  ok_rev3 = ((diff13 > delta and diff23 > delta) => ab3);
127
tel 
128

  
129
-- it checks to make sure that there is no aberrant input value
130
-- i.e. here, if there isn't a value which is too remote from the other two.
131
-- delta is a safe range
132

  
133
--@ requires delta > 0.0;
134
--@ ensures exists ok_ab1, ok_ab2, ok_ab3, ok_rev1, ok_rev2, ok_rev3: bool; (ok_ab1, ok_ab2, ok_ab3, ok_rev1, ok_rev2, ok_rev3) = (obs_aberration (s1,s2,s3,delta,ab1,ab2,ab3));
135
node aberration (s1,s2,s3, delta: real) returns (ab1, ab2, ab3: bool);
136
var
137
  diff12, diff13, diff23: real;
138
let
139
  diff12 = abs_1(s1 - s2);
140
  diff13 = abs_1(s1 - s3);
141
  diff23 = abs_1(s2 - s3);
142

  
143
  ab1 = (diff12 > delta) and (diff13 > delta);
144
  ab2 = (diff12 > delta) and (diff23 > delta);
145
  ab3 = (diff13 > delta) and (diff23 > delta);
146
tel
147

  
148

  
149

  
150
--@ ensures (nb_errors = 0) => not (e1 or e2 or e3);
151
--@ ensures not (e1 or e2 or e3) => (nb_errors = 0);
152
--@ ensures e1 or e2 or e3 => nb_errors >= 1;
153
--@ ensures e1 and e2 and e3 => (nb_errors = 3);
154
--@ ensures e1 and e2 and not e3 => (nb_errors = 2);
155
--@ ensures e1 and not e2 and e3 => (nb_errors = 2);
156
--@ ensures not e1 and e2 and e3 => (nb_errors = 2);
157
--@ ensures not e1 and not e2 and e3 => (nb_errors = 1);
158
--@ ensures not e1 and e2 and not e3 => (nb_errors = 1);
159
--@ ensures e1 and not e2 and not e3 => (nb_errors = 1);
160
--@ ensures nb_errors = 0 or nb_errors = 1 or nb_errors = 2 or nb_errors =3;
161
node nb_err_calc( e1, e2, e3: bool) returns (nb_errors: int);
162
let
163
  nb_errors = if e1 and e2 and e3 
164
          then 3
165
          else if (e1 and e2) or (e2 and e3) or (e1 and e3)
166
             then 2
167
             else if e1 or e2 or e3
168
                then 1
169
                else 0;
170
tel
171

  
172

  
173

  
174

  
175
--@ requires nb_err = 0 or nb_err = 1 or nb_err = 2 or nb_err = 3;
176
--@ requires nb_err = nb_err_calc(e1, e2, e3);
177
--@ ensures nb_err = 2 => (v = s1 or v = s2 or v = s3);
178
--@ ensures nb_err = 3 => (v = pre v);
179
--@ ensures (nb_err = 1 and e1) => v = (s2 + s3) / 2.0;
180
--@ ensures (nb_err = 1 and e2) => v = (s1 + s3) / 2.0;
181
--@ ensures (nb_err = 1 and e3) => v = (s1 + s2) / 2.0;
182
--@ ensures nb_err = 0 => v = (s1 + s2 + s3) / 3.0;
183
node calc_value (nb_err: int; e1, e2, e3: bool; s1, s2, s3: real) returns (v: real);
184
var
185
  previous_good_value, v1, v2, v3, di: real;
186
let
187
  previous_good_value = 0.0 -> pre v;
188

  
189
  di = if nb_err = 0
190
	then 3.0
191
	else 
192
	     if nb_err = 1
193
	     then 2.0
194
	     else 1.0;
195
	
196
  v1 = if e1 then 0.0 else s1;
197
  v2 = if e2 then 0.0 else s2;
198
  v3 = if e3 then 0.0 else s3;
199

  
200
  v = if nb_err = 3 
201
	then  previous_good_value
202
	else (v1 + v2 + v3) / di;
203
tel
204

  
205

  
206
--@ requires min <= max;
207
--@ ensures min <= v and v <= max;
208
--@ ensures s < min => v = min;
209
--@ ensures s > max => v = max;
210
--@ ensures (min <= s and s <= max) => v = s;
211
node range(s, min, max: real) returns (v: real);
212
let
213
	v = if s < min then min else if s > max then max else s;
214
tel
215

  
216

  
217
 
218
    
219
--@ requires min <= max;
220
--@ requires delta > 0.0;
221
--@ ensures min <= value and value <= max; 
222
--@ ensures 0 <= nb_errors and nb_errors <= 3;
223
--@ ensures nb_errors = 3 => value = pre value;
224
--@ ensures exists ok_stMin, ok_stMax, ok_revMin, ok_revMax: bool; (ok_stMin, ok_stMax, ok_revMin, ok_revMax) = obs_simple_voter(s1, s2, s3, min, max, delta, value, warning_stMax, warning_stMin);
225

  
226
node simple_voter (s1, s2, s3, min, max, delta: real) returns (value: real; warning_stMax, warning_stMin: bool; nb_errors:int);
227

  
228
var 
229
  sp_s1, sp_s2, sp_s3: real;
230
--  sp_er1, sp_er2, sp_er3: bool;
231
--  speed_error1, speed_error2, speed_error3: bool;
232

  
233
  r_s1, r_s2, r_s3: real;
234
  stmin1, stmin2, stmin3, stmax1, stmax2, stmax3: bool;
235
  errorRange1, errorRange2, errorRange3: bool; 
236

  
237
  error1, error2, error3: bool;
238

  
239
  ab1, ab2, ab3: bool;
240
  error_ab1, error_ab2, error_ab3: bool;
241
let
242
  sp_s1 = check_speed (s1, delta);
243
--  speed_error1 = check_validity_lock(sp_er1, 20);
244
  (r_s1, stmin1, stmax1, errorRange1) = ranged_value(sp_s1, min, max, delta);
245
  error1 = errorRange1 or check_validity_lock (errorRange1, 12);
246

  
247
  sp_s2 = check_speed (s2, delta);
248
--  speed_error2 = check_validity_lock(sp_er2, 20);
249
  (r_s2, stmin2, stmax2, errorRange2) = ranged_value(sp_s2, min, max, delta);
250
  error2 = errorRange2 or check_validity_lock (errorRange2, 14);
251

  
252
  sp_s3 = check_speed (s3, delta);
253
--  speed_error3 = check_validity_lock(sp_er3, 20);
254
  (r_s3, stmin3, stmax3, errorRange3) = ranged_value(sp_s3, min, max, delta);
255
  error3 = errorRange3 or check_validity_lock (errorRange3, 16);   
256

  
257
  warning_stMin = (stmin1 and stmin2) or (stmin1 and stmin3) or (stmin2 and stmin3);
258
  warning_stMax = (stmax1 and stmax2) or (stmax1 and stmax3) or (stmax2 and stmax3);
259

  
260
  (ab1, ab2, ab3) = if error1 or error2 or error3 
261
            then
262
              (error1, error2, error3)  
263
            else 
264
                aberration(r_s1, r_s2, r_s3, delta);
265

  
266
  error_ab1 = check_validity_lock (ab1, 16);  
267

  
268
  error_ab2 = check_validity_lock (ab2, 18);
269

  
270
  error_ab3 = check_validity_lock (ab3, 22);
271

  
272
  nb_errors = nb_err_calc(error_ab1, error_ab2, error_ab3);
273

  
274
  value = calc_value(nb_errors, error_ab1, error_ab2, error_ab3, r_s1, r_s2, r_s3);
275

  
276
tel
277

  
278
-- it checks if the warnings are valid
279

  
280
node obs_simple_voter(s1, s2, s3, min, max, delta, value: real; warning_stMax, warning_stMin: bool)
281
returns (ok_stMin, ok_stMax, ok_revMin, ok_revMax : bool);
282
var
283
  stmin1, stmin2, stmin3 : bool;
284
  stmax1, stmax2, stmax3 : bool;
285
let
286
  stmin1 = s1 < min - delta;
287
  stmin2 = s2 < min - delta;
288
  stmin3 = s3 < min - delta;
289

  
290
  stmax1 = s1 > max + delta;
291
  stmax2 = s2 > max + delta;
292
  stmax3 = s3 > max + delta;
293

  
294
  ok_stMin = (warning_stMin => ((stmin1 and stmin2) or (stmin2 and stmin3) or (stmin1 and stmin3)));  
295
  ok_stMax = (warning_stMax => ((stmax1 and stmax2) or (stmax2 and stmax3) or (stmax1 and stmax3)));
296

  
297
  ok_revMin = (((stmin1 and stmin2) or (stmin2 and stmin3) or (stmin1 and stmin3)) => warning_stMin); 
298
  ok_revMax = (((stmax1 and stmax2) or (stmax2 and stmax3) or (stmax1 and stmax3)) => warning_stMax);
299
tel
300

  
301
node voter_temp (s1, s2, s3: real) returns (value: real; warningMax, warningMin: bool; nb_err: int);
302
let
303
  (value, warningMin, warningMax, nb_err) = simple_voter (s1, s2, s3, 200.0, 2000.0, 80.0);
304
tel
305

  
306
node voter_alt (s1, s2, s3: real) returns (value: real; warningMax, warningMin: bool; nb_err: int);
307
let
308
  (value, warningMax, warningMin, nb_err) = simple_voter (s1, s2, s3, 0.0, 15000.0, 120.0);
309
tel
310

  
311
node safety_plane_archi(s1, s2, s3: real) returns (value: real; warningMax, warningMin: bool; nb_err: int);
312
let
313
  (value, warningMax, warningMin, nb_err) = simple_voter (s1, s2, s3, 0.0, 15000.0, 120.0);
314
tel
315

  
regression_tests/lustre_files/success/safety/safety_plane_archi.lusi
1
(* Generated Lustre Interface file from safety_plane_archi.lus *)
2
(* by Lustre-C compiler version 1.3-458, 2016/10/25, 14:3:40 *)
3
(* Feel free to mask some of the definitions by removing them from this file. *)
4

  
5
function abs_1 (x: real) returns (y: real);
6

  
7
node check_validity (x: bool; n: int) returns (y: bool; nb_times: int);
8

  
9
node lock (x: bool; reset: bool) returns (y: bool);
10

  
11
function aberration (s1: real; s2: real; s3: real; delta: real) returns (ab1: bool; ab2: bool; ab3: bool);
12

  
13
node calc_value (nb_err: int; e1: bool; e2: bool; e3: bool; s1: real; s2: real; s3: real) returns (v: real);
14

  
15
node check_speed (s: real; delta: real) returns (v: real);
16

  
17
node check_validity_lock (x: bool; n: int) returns (y: bool);
18

  
19
function nb_err_calc (e1: bool; e2: bool; e3: bool) returns (nb_errors: int);
20

  
21
function ranged_value (value: real; min: real; max: real; delta: real) returns (ranged_val: real; satmin: bool; satmax: bool; error: bool);
22

  
23
node simple_voter (s1: real; s2: real; s3: real; min: real; max: real; delta: real) returns (value: real; warning_stMax: bool; warning_stMin: bool; nb_errors: int);
24

  
25
function range (s: real; min: real; max: real) returns (v: real);
26

  
27
node voter_alt (s1: real; s2: real; s3: real) returns (value: real; warningMax: bool; warningMin: bool; nb_err: int);
28

  
29
node safety_plane_archi (s1: real; s2: real; s3: real) returns (value: real; warningMax: bool; warningMin: bool; nb_err: int);
30

  
31
function obs_simple_voter (s1: real; s2: real; s3: real; min: real; max: real; delta: real; value: real; warning_stMax: bool; warning_stMin: bool) returns (ok_stMin: bool; ok_stMax: bool; ok_revMin: bool; ok_revMax: bool);
32

  
33
function obs_aberration (s1: real; s2: real; s3: real; delta: real; ab1: bool; ab2: bool; ab3: bool) returns (ok_ab1: bool; ok_ab2: bool; ok_ab3: bool; ok_rev1: bool; ok_rev2: bool; ok_rev3: bool);
34

  
35
node voter_temp (s1: real; s2: real; s3: real) returns (value: real; warningMax: bool; warningMin: bool; nb_err: int);
36

  

Also available in: Unified diff