Project

General

Profile

Download (9.75 KB) Statistics
| Branch: | Tag: | Revision:
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(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 (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
-- it checks to make sure that there is no aberrant input value
111
-- i.e. here, if there isn't a value which is too remote from the other two.
112
-- delta is a safe range
113

    
114
--@ requires delta > 0.0;
115
--@ observer obs_aberration(s1,s2,s3,ab1,ab2,ab3,ok_ab1, ok_ab2, ok_ab3, ok_rev1, ok_rev2, ok_rev3);
116
node aberration (s1,s2,s3, delta: real) returns (ab1, ab2, ab3: bool);
117
var
118
  diff12, diff13, diff23: real;
119
let
120
  diff12 = abs(s1 - s2);
121
  diff13 = abs(s1 - s3);
122
  diff23 = abs(s2 - s3);
123

    
124
  ab1 = (diff12 > delta) and (diff13 > delta);
125
  ab2 = (diff12 > delta) and (diff23 > delta);
126
  ab3 = (diff13 > delta) and (diff23 > delta);
127
tel
128

    
129
-- checks if the node "aberration" has valid outputs 
130

    
131
node obs_aberration(s1,s2,s3,delta: real; ab1,ab2,ab3: bool) 
132
returns (ok_ab1, ok_ab2, ok_ab3, ok_rev1, ok_rev2, ok_rev3: bool);
133
var
134
  diff12, diff13, diff23: real;
135
let
136
  diff12 = abs(s1 - s2);
137
  diff13 = abs(s1 - s3);
138
  diff23 = abs(s2 - s3);
139
  ok_ab1 = (ab1 => (diff12 > delta and diff13 > delta));
140
  ok_ab2 = (ab2 => (diff12 > delta and diff23 > delta));
141
  ok_ab3 = (ab3 => (diff13 > delta and diff23 > delta));
142
  ok_rev1 = ((diff12 > delta and diff13 > delta) => ab1 );
143
  ok_rev2 = ((diff12 > delta and diff23 > delta) => ab2);
144
  ok_rev3 = ((diff13 > delta and diff23 > delta) => ab3);
145
tel 
146

    
147

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

    
170

    
171

    
172

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

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

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

    
203

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

    
214

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

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

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

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

    
235
  error1, error2, error3: bool;
236

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

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

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

    
255
  warning_stMin = (stmin1 and stmin2) or (stmin1 and stmin3) or (stmin2 and stmin3);
256
  warning_stMax = (stmax1 and stmax2) or (stmax1 and stmax3) or (stmax2 and stmax3);
257

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

    
264
  error_ab1 = check_validity_lock (ab1, 16);  
265

    
266
  error_ab2 = check_validity_lock (ab2, 18);
267

    
268
  error_ab3 = check_validity_lock (ab3, 22);
269

    
270
  nb_errors = nb_err(error_ab1, error_ab2, error_ab3);
271

    
272
  value = calc_value(nb_errors, error_ab1, error_ab2, error_ab3, r_s1, r_s2, r_s3);
273

    
274
tel
275

    
276
-- it checks if the warnings are valid
277

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

    
288
  stmax1 = s1 > max + delta;
289
  stmax2 = s2 > max + delta;
290
  stmax3 = s3 > max + delta;
291

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

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

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

    
304
node voter_alt (s1, s2, s3: real) returns (value: real; warningMax, warningMin: bool; nb_err: int);
305
let
306
  (value, warningMax, warningMin, nb_err) = simple_voter (s1, s2, s3, 0.0, 15000.0, 120.0);
307
tel
    (1-1/1)