Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / safety / safety_plane_archi.lus @ 47714cf4

History | View | Annotate | Download (10.1 KB)

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