1
|
-- STEAM BOILER example
|
2
|
-- from The Steam Boiler Problem in Lustre
|
3
|
-- by Thierry Cattel and Gregory Duval
|
4
|
|
5
|
|
6
|
|
7
|
|
8
|
node REDGE(S:bool) returns(REDGE:bool);
|
9
|
let
|
10
|
REDGE= S -> S and not(pre(S));
|
11
|
tel
|
12
|
|
13
|
|
14
|
|
15
|
node sum(a_0,a_1,a_2,a_3:int) returns(sum:int);
|
16
|
let
|
17
|
sum = a_0 + a_1 + a_2 + a_3;
|
18
|
tel
|
19
|
|
20
|
node AND(a_0,a_1,a_2,a_3:bool) returns(AND:bool);
|
21
|
let
|
22
|
AND = a_0 and a_1 and a_2 and a_3;
|
23
|
tel
|
24
|
|
25
|
node OR(a_0,a_1,a_2,a_3:bool) returns(OR:bool);
|
26
|
let
|
27
|
OR = a_0 or a_1 or a_2 or a_3;
|
28
|
tel
|
29
|
|
30
|
|
31
|
node NOT(a_0,a_1,a_2,a_3:bool) returns(NOT_0,NOT_1,NOT_2,NOT_3:bool);
|
32
|
let
|
33
|
NOT_0 = not a_0;
|
34
|
NOT_1 = not a_1;
|
35
|
NOT_2 = not a_2;
|
36
|
NOT_3 = not a_3;
|
37
|
tel
|
38
|
|
39
|
|
40
|
|
41
|
node FEDGE1(S:bool) returns(FEDGE1:bool);
|
42
|
let
|
43
|
FEDGE1= not(S) -> not(S) and pre(S);
|
44
|
tel
|
45
|
|
46
|
|
47
|
|
48
|
node FEDGE2(S:bool) returns(FEDGE2:bool);
|
49
|
let
|
50
|
FEDGE2= REDGE(not(S));
|
51
|
tel
|
52
|
|
53
|
|
54
|
|
55
|
node Verification(S1,S2:bool) returns(property_ok:bool);
|
56
|
var property1,property2:bool;
|
57
|
let
|
58
|
property1=FEDGE1(S1)=FEDGE2(S1);
|
59
|
|
60
|
--assert(S2=not(S1));
|
61
|
property2= FEDGE1(S1)=REDGE(S2);
|
62
|
|
63
|
property_ok=
|
64
|
if S2=not(S1) then
|
65
|
property1 and property2
|
66
|
else true
|
67
|
;
|
68
|
tel
|
69
|
|
70
|
|
71
|
node Operator(stop:bool) returns (stop_request:bool);
|
72
|
var nb_stops:int;
|
73
|
let
|
74
|
nb_stops = (if stop then 1 else 0) ->
|
75
|
if stop then pre(nb_stops)+1 else 0;
|
76
|
stop_request = (nb_stops>=3);
|
77
|
tel
|
78
|
|
79
|
|
80
|
|
81
|
node Defect(statein:int; fail_cond,ack_chan,repair_chan:bool)
|
82
|
returns(stateout:int);
|
83
|
let
|
84
|
stateout = if (statein=0) then
|
85
|
if fail_cond then 1 else 0
|
86
|
else
|
87
|
if (statein=1) then
|
88
|
if ack_chan then 2 else 1
|
89
|
else --statein=2
|
90
|
if repair_chan then 0 else 2;
|
91
|
tel
|
92
|
|
93
|
|
94
|
node level_failure_detect(level:int) returns(level_failure_detect:bool);
|
95
|
let
|
96
|
level_failure_detect = ((level < 0) or (level > 1000));
|
97
|
tel
|
98
|
|
99
|
node steam_failure_detect(steam:int) returns(steam_failure_detect:bool);
|
100
|
let
|
101
|
steam_failure_detect = ((steam < 0) or (steam > 25));
|
102
|
tel
|
103
|
|
104
|
node LevelDefect(level_failure_acknowledgement,level_repaired:bool;
|
105
|
level:int)
|
106
|
returns( LevelDefect:int);
|
107
|
let
|
108
|
LevelDefect = 0 ->
|
109
|
Defect(pre(LevelDefect), level_failure_detect(level), level_failure_acknowledgement, level_repaired);
|
110
|
tel
|
111
|
|
112
|
|
113
|
node SteamDefect(steam_failure_acknowledgement,steam_repaired:bool;
|
114
|
steam:int)
|
115
|
returns( SteamDefect:int);
|
116
|
let
|
117
|
SteamDefect = 0 ->
|
118
|
Defect(pre(SteamDefect), steam_failure_detect(steam), steam_failure_acknowledgement, steam_repaired);
|
119
|
tel
|
120
|
|
121
|
|
122
|
node pump_failure_detect(pump_status,pump_state:int;
|
123
|
pump_control_state:bool)
|
124
|
returns(pump_failure_detect,pump_control_failure_detect,flow:bool);
|
125
|
let
|
126
|
pump_failure_detect = ((pump_status=0) and pump_state=1)
|
127
|
or (((pump_status=1) or (pump_status=2))and pump_state=0);
|
128
|
pump_control_failure_detect = (((pump_status=0) or
|
129
|
(pump_status=2)) and pump_state=0 and pump_control_state)
|
130
|
or ((pump_status=1) and pump_state=1 and not(pump_control_state))
|
131
|
or ((pump_status=2) and pump_state=1 and pump_control_state);
|
132
|
flow = ((pump_status=0) and pump_state=1 and pump_control_state)
|
133
|
or ((pump_status=1) and pump_state=0 and pump_control_state)
|
134
|
or ((pump_status=1) and pump_state=1);
|
135
|
tel
|
136
|
|
137
|
|
138
|
|
139
|
|
140
|
node PumpDefect(
|
141
|
pump_failure_acknowledgement,pump_repaired,
|
142
|
pump_control_failure_acknowledgement,pump_control_repaired:bool;
|
143
|
pump_status,pump_state:int;
|
144
|
pump_control_state:bool)
|
145
|
returns(PumpDefect,PumpControlDefect:int;Flow:bool);
|
146
|
var
|
147
|
pump_failure_d, pump_control_failure_d:bool;
|
148
|
let
|
149
|
(pump_failure_d, pump_control_failure_d, Flow) = pump_failure_detect(pump_status, pump_state, pump_control_state);
|
150
|
PumpDefect = 0 ->
|
151
|
Defect(pre(PumpDefect), pump_failure_d, pump_failure_acknowledgement, pump_repaired);
|
152
|
PumpControlDefect = 0 ->
|
153
|
Defect(pre(PumpControlDefect), pump_control_failure_d, pump_control_failure_acknowledgement, pump_control_repaired);
|
154
|
tel
|
155
|
|
156
|
|
157
|
node level_failure(level_defect:int) returns(level_failure:bool);
|
158
|
let
|
159
|
level_failure = (level_defect<>0);
|
160
|
tel
|
161
|
|
162
|
node steam_failure(steam_defect:int) returns(steam_failure:bool);
|
163
|
let
|
164
|
steam_failure = (steam_defect<>0);
|
165
|
tel
|
166
|
|
167
|
node pump_failure(pump_defect:int) returns(pump_failure:bool);
|
168
|
let
|
169
|
pump_failure = (pump_defect<>0);
|
170
|
tel
|
171
|
|
172
|
node pump_control_failure(pump_defect:int) returns(pump_failure:bool);
|
173
|
let
|
174
|
pump_failure = (pump_defect<>0);
|
175
|
tel
|
176
|
|
177
|
|
178
|
node Dynamics(valve_state,level,steam,level_defect,steam_defect:int;
|
179
|
flow_0,flow_1,flow_2,flow_3:bool)
|
180
|
returns (q,v:int; p_0,p_1,p_2,p_3:int);
|
181
|
let
|
182
|
q = level->
|
183
|
if level_failure(level_defect) then
|
184
|
pre(q) - steam*5 + sum(p_0,p_1,p_2,p_3)*5 - (if valve_state=1 then 10*5 else 0)
|
185
|
else
|
186
|
level;
|
187
|
v = steam->
|
188
|
if steam_failure(steam_defect) then
|
189
|
(pre(q) -q) div 5 + sum(p_0,p_1,p_2,p_3)*5
|
190
|
else
|
191
|
steam;
|
192
|
p_0 = 0->
|
193
|
if (not(flow_0)) then
|
194
|
0
|
195
|
else
|
196
|
15;
|
197
|
p_1 = 0->
|
198
|
if (not(flow_1)) then
|
199
|
0
|
200
|
else
|
201
|
15;
|
202
|
p_2 = 0->
|
203
|
if (not(flow_2)) then
|
204
|
0
|
205
|
else
|
206
|
15;
|
207
|
p_3 = 0->
|
208
|
if (not(flow_3)) then
|
209
|
0
|
210
|
else
|
211
|
15;
|
212
|
|
213
|
tel
|
214
|
|
215
|
|
216
|
|
217
|
node PumpsDecision(q,v:int) returns (n_pumps:int);
|
218
|
let
|
219
|
n_pumps = if q>600 then
|
220
|
(v div 15)
|
221
|
else
|
222
|
if q<400 then
|
223
|
(v div 15) +1
|
224
|
else
|
225
|
pre(n_pumps) ;
|
226
|
tel
|
227
|
|
228
|
|
229
|
|
230
|
node operate_pumps( n, n_pumps_to_open:int;
|
231
|
pump_status_0,pump_status_1,pump_status_2,pump_status_3,
|
232
|
pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3:int;
|
233
|
flow_0,flow_1,flow_2,flow_3:bool)
|
234
|
returns(operate_pumps_0,operate_pumps_1,operate_pumps_2,operate_pumps_3:int);
|
235
|
let
|
236
|
operate_pumps_0 =
|
237
|
if ((n_pumps_to_open>0) and
|
238
|
not(flow_0) and
|
239
|
not(pump_failure(pump_defect_0)) and
|
240
|
(pump_status_0=0)) then
|
241
|
2
|
242
|
else
|
243
|
if ((n_pumps_to_open<0) and
|
244
|
flow_0 and
|
245
|
not(pump_failure(pump_defect_0)) and
|
246
|
(pump_status_0=1)) then
|
247
|
0
|
248
|
else
|
249
|
if (pump_status_0=2) then
|
250
|
1
|
251
|
else
|
252
|
if (pre(pump_defect_0)=2 and
|
253
|
pump_defect_0=0) then
|
254
|
if pump_status_0=1 then
|
255
|
0
|
256
|
else --necessarily 0
|
257
|
1
|
258
|
else
|
259
|
pump_status_0;
|
260
|
|
261
|
operate_pumps_1 =
|
262
|
if ((n_pumps_to_open>0) and
|
263
|
not(flow_1) and
|
264
|
not(pump_failure(pump_defect_1)) and
|
265
|
(pump_status_1=0)) then
|
266
|
2
|
267
|
else
|
268
|
if ((n_pumps_to_open<0) and
|
269
|
flow_1 and
|
270
|
not(pump_failure(pump_defect_1)) and
|
271
|
(pump_status_1=1)) then
|
272
|
0
|
273
|
else
|
274
|
if (pump_status_1=2) then
|
275
|
1
|
276
|
else
|
277
|
if (pre(pump_defect_1)=2 and
|
278
|
pump_defect_1=0) then
|
279
|
if pump_status_1=1 then
|
280
|
0
|
281
|
else --necessarily 0
|
282
|
1
|
283
|
else
|
284
|
pump_status_1;
|
285
|
|
286
|
operate_pumps_2 =
|
287
|
if ((n_pumps_to_open>0) and
|
288
|
not(flow_2) and
|
289
|
not(pump_failure(pump_defect_2)) and
|
290
|
(pump_status_2=0)) then
|
291
|
2
|
292
|
else
|
293
|
if ((n_pumps_to_open<0) and
|
294
|
flow_2 and
|
295
|
not(pump_failure(pump_defect_2)) and
|
296
|
(pump_status_2=1)) then
|
297
|
0
|
298
|
else
|
299
|
if (pump_status_2=2) then
|
300
|
1
|
301
|
else
|
302
|
if (pre(pump_defect_2)=2 and
|
303
|
pump_defect_2=0) then
|
304
|
if pump_status_2=1 then
|
305
|
0
|
306
|
else --necessarily 0
|
307
|
1
|
308
|
else
|
309
|
pump_status_2;
|
310
|
|
311
|
operate_pumps_3 =
|
312
|
if ((n_pumps_to_open>0) and
|
313
|
not(flow_3) and
|
314
|
not(pump_failure(pump_defect_3)) and
|
315
|
(pump_status_3=0)) then
|
316
|
2
|
317
|
else
|
318
|
if ((n_pumps_to_open<0) and
|
319
|
flow_3 and
|
320
|
not(pump_failure(pump_defect_3)) and
|
321
|
(pump_status_3=1)) then
|
322
|
0
|
323
|
else
|
324
|
if (pump_status_3=2) then
|
325
|
1
|
326
|
else
|
327
|
if (pre(pump_defect_3)=2 and
|
328
|
pump_defect_3=0) then
|
329
|
if pump_status_3=1 then
|
330
|
0
|
331
|
else --necessarily 0
|
332
|
1
|
333
|
else
|
334
|
pump_status_3;
|
335
|
|
336
|
tel
|
337
|
|
338
|
|
339
|
node PumpsStatus(
|
340
|
n_pumps:int;
|
341
|
pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3:int;
|
342
|
flow_0,flow_1,flow_2,flow_3:bool)
|
343
|
returns(pump_status_0,pump_status_1,pump_status_2,pump_status_3:int);
|
344
|
var
|
345
|
n_pumps_flow,n_pumps_to_open:int;
|
346
|
t0,t1,t2,t3:int;
|
347
|
let
|
348
|
n_pumps_flow = (if flow_0 then 1 else 0) + (if flow_1 then 1 else 0) +
|
349
|
(if flow_2 then 1 else 0) + (if flow_3 then 1 else 0);
|
350
|
n_pumps_to_open = n_pumps-n_pumps_flow;
|
351
|
|
352
|
pump_status_0 = 0 ->t0;
|
353
|
pump_status_1 = 0 ->t1;
|
354
|
pump_status_2 = 0 ->t2;
|
355
|
pump_status_3 = 0 ->t3;
|
356
|
|
357
|
(t0,t1,t2,t3) =
|
358
|
operate_pumps(4, n_pumps_to_open,
|
359
|
pre(pump_status_0),pre(pump_status_1),pre(pump_status_2),pre(pump_status_3),
|
360
|
pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3,
|
361
|
flow_0,flow_1,flow_2,flow_3);
|
362
|
tel
|
363
|
|
364
|
node transmission_failure(pump_state_0,pump_state_1,pump_state_2,pump_state_3:int)
|
365
|
returns(transmission_failure:bool);
|
366
|
let
|
367
|
transmission_failure = pump_state_0=3 or pump_state_1=3 or pump_state_2=3 or pump_state_3=3;
|
368
|
tel
|
369
|
|
370
|
node steam_failure_startup(steam:int) returns(steam_failure_startup:bool);
|
371
|
let
|
372
|
steam_failure_startup=(steam<>0);
|
373
|
tel
|
374
|
|
375
|
node dangerous_level(q:int) returns(dangerous_level:bool);
|
376
|
let
|
377
|
dangerous_level = (q <= 150) or (q >= 850);
|
378
|
tel
|
379
|
|
380
|
|
381
|
|
382
|
node critical_failure(
|
383
|
op_mode,steam,level_defect,steam_defect:int;
|
384
|
pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3:int;
|
385
|
q:int;
|
386
|
pump_state_0,pump_state_1,pump_state_2,pump_state_3:int)
|
387
|
returns(critical_failure:bool);
|
388
|
let
|
389
|
critical_failure = transmission_failure(pump_state_0,pump_state_1,pump_state_2,pump_state_3) or
|
390
|
(op_mode=1 and steam_failure_startup(steam)) or
|
391
|
(op_mode=2 and (level_failure(level_defect) or steam_failure(steam_defect))) or
|
392
|
(op_mode=3 and dangerous_level(q)) or
|
393
|
(op_mode=4 and dangerous_level(q)) or
|
394
|
(op_mode=5 and (dangerous_level(q) or steam_failure(steam_defect) or AND(pump_failure(pump_defect_0),pump_failure(pump_defect_1),pump_failure(pump_defect_2),pump_failure(pump_defect_3))));
|
395
|
tel
|
396
|
|
397
|
|
398
|
node failure(
|
399
|
level_defect,steam_defect:int;
|
400
|
pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3,pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3:int)
|
401
|
returns(failure:bool);
|
402
|
let
|
403
|
failure = level_failure(level_defect) or
|
404
|
steam_failure(steam_defect) or
|
405
|
OR(pump_failure(pump_defect_0),pump_failure(pump_defect_1),pump_failure(pump_defect_2),pump_failure(pump_defect_3)) or
|
406
|
OR(pump_control_failure(pump_control_defect_0),pump_control_failure(pump_control_defect_1),pump_control_failure(pump_control_defect_2),pump_control_failure(pump_control_defect_3));
|
407
|
tel
|
408
|
|
409
|
|
410
|
|
411
|
node ControlMode(
|
412
|
steam_boiler_waiting,physical_units_ready,stop_request:bool;
|
413
|
steam,level_defect,steam_defect:int;
|
414
|
pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3,pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3:int;
|
415
|
q:int;
|
416
|
pump_state_0,pump_state_1,pump_state_2,pump_state_3:int)
|
417
|
returns(op_mode :int);
|
418
|
let
|
419
|
op_mode= 1->
|
420
|
if (critical_failure(pre(op_mode),
|
421
|
steam, level_defect, steam_defect, pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3, q, pump_state_0,pump_state_1,pump_state_2,pump_state_3) or
|
422
|
stop_request or pre(op_mode)=6) then
|
423
|
6
|
424
|
else
|
425
|
if (pre(op_mode)=1) then
|
426
|
if steam_boiler_waiting then 2 else 1
|
427
|
else
|
428
|
if (pre(op_mode)=2 and not physical_units_ready) then
|
429
|
2
|
430
|
else
|
431
|
if level_failure(level_defect) then
|
432
|
5
|
433
|
else
|
434
|
if failure(level_defect, steam_defect, pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3, pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3) then
|
435
|
4
|
436
|
else
|
437
|
3;
|
438
|
tel
|
439
|
|
440
|
|
441
|
|
442
|
|
443
|
|
444
|
|
445
|
|
446
|
|
447
|
|
448
|
|
449
|
node Valve(op_mode:int;q:int) returns (valve:bool;valve_state:int);
|
450
|
let
|
451
|
valve_state=0->
|
452
|
if (op_mode=2) then
|
453
|
if (q>600) then
|
454
|
1
|
455
|
else
|
456
|
if (q<=600) then 0 else pre(valve_state)
|
457
|
else
|
458
|
pre(valve_state);
|
459
|
valve =false->
|
460
|
(valve_state<>pre(valve_state));
|
461
|
tel
|
462
|
|
463
|
|
464
|
node initialization_complete(op_mode,level:int;valve:bool)
|
465
|
returns(initialization_complete:bool);
|
466
|
let
|
467
|
initialization_complete =(op_mode=2) and
|
468
|
((400<=level) and (level<=600))and
|
469
|
not(valve);
|
470
|
tel
|
471
|
|
472
|
|
473
|
node ControlOutput(op_mode,level:int;valve:bool)
|
474
|
returns(program_ready:bool;mode:int);
|
475
|
let
|
476
|
program_ready=initialization_complete(op_mode,level,valve);
|
477
|
mode =op_mode;
|
478
|
tel
|
479
|
|
480
|
|
481
|
|
482
|
|
483
|
|
484
|
node SteamOutput(op_mode,steam_defect:int; steam_repaired:bool)
|
485
|
returns (steam_outcome_failure_detection,
|
486
|
steam_outcome_repaired_acknowledgement : bool);
|
487
|
let
|
488
|
steam_outcome_failure_detection=
|
489
|
not ((op_mode=6) or (op_mode=1)) and
|
490
|
(steam_defect=1);
|
491
|
steam_outcome_repaired_acknowledgement =
|
492
|
not ((op_mode=6) or (op_mode=1)) and
|
493
|
steam_repaired;
|
494
|
tel
|
495
|
|
496
|
node LevelOutput(op_mode,level_defect:int; level_repaired:bool)
|
497
|
returns (level_outcome_failure_detection,
|
498
|
level_outcome_repaired_acknowledgement : bool);
|
499
|
let
|
500
|
level_outcome_failure_detection=
|
501
|
not ((op_mode=6) or (op_mode=1)) and
|
502
|
(level_defect=1);
|
503
|
level_outcome_repaired_acknowledgement =
|
504
|
not ((op_mode=6) or (op_mode=1)) and
|
505
|
level_repaired;
|
506
|
tel
|
507
|
|
508
|
|
509
|
|
510
|
node PumpsOutput(op_mode:int;
|
511
|
pump_status_0,pump_status_1,pump_status_2,pump_status_3,
|
512
|
pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3,
|
513
|
pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3:int;
|
514
|
pump_repaired_0,pump_repaired_1,pump_repaired_2,pump_repaired_3,
|
515
|
pump_control_repaired_0,pump_control_repaired_1,pump_control_repaired_2,pump_control_repaired_3:bool)
|
516
|
|
517
|
returns (open_pump_0,open_pump_1,open_pump_2,open_pump_3,
|
518
|
close_pump_0,close_pump_1,close_pump_2,close_pump_3,
|
519
|
pump_failure_detection_0,pump_failure_detection_1,pump_failure_detection_2,pump_failure_detection_3,
|
520
|
pump_repaired_acknowledgement_0,pump_repaired_acknowledgement_1,pump_repaired_acknowledgement_2,pump_repaired_acknowledgement_3,
|
521
|
pump_control_failure_detection_0,pump_control_failure_detection_1,pump_control_failure_detection_2,pump_control_failure_detection_3,
|
522
|
pump_control_repaired_acknowledgement_0,pump_control_repaired_acknowledgement_1,pump_control_repaired_acknowledgement_2,pump_control_repaired_acknowledgement_3 : bool);
|
523
|
let
|
524
|
open_pump_0 =
|
525
|
op_mode<>6 and op_mode<>1 and pump_status_0=2;
|
526
|
open_pump_1 =
|
527
|
op_mode<>6 and op_mode<>1 and pump_status_1=2;
|
528
|
open_pump_2 =
|
529
|
op_mode<>6 and op_mode<>1 and pump_status_2=2;
|
530
|
open_pump_3 =
|
531
|
op_mode<>6 and op_mode<>1 and pump_status_3=2;
|
532
|
|
533
|
close_pump_0 =
|
534
|
op_mode<>6 and op_mode<>1 and pump_status_0=0 and pre(pump_status_0)<>0 and pump_defect_0=0 and pre(pump_defect_0)=0;
|
535
|
close_pump_1 =
|
536
|
op_mode<>6 and op_mode<>1 and pump_status_0=0 and pre(pump_status_1)<>0 and pump_defect_0=0 and pre(pump_defect_1)=0;
|
537
|
close_pump_2 =
|
538
|
op_mode<>6 and op_mode<>1 and pump_status_0=0 and pre(pump_status_2)<>0 and pump_defect_0=0 and pre(pump_defect_2)=0;
|
539
|
close_pump_3 =
|
540
|
op_mode<>6 and op_mode<>1 and pump_status_0=0 and pre(pump_status_3)<>0 and pump_defect_0=0 and pre(pump_defect_3)=0;
|
541
|
|
542
|
pump_failure_detection_0 =
|
543
|
op_mode<>6 and op_mode<>1 and pump_defect_0=1;
|
544
|
pump_failure_detection_1 =
|
545
|
op_mode<>6 and op_mode<>1 and pump_defect_1=1;
|
546
|
pump_failure_detection_2 =
|
547
|
op_mode<>6 and op_mode<>1 and pump_defect_2=1;
|
548
|
pump_failure_detection_3 =
|
549
|
op_mode<>6 and op_mode<>1 and pump_defect_3=1;
|
550
|
|
551
|
pump_repaired_acknowledgement_0 =
|
552
|
op_mode<>6 and op_mode<>1 and pump_repaired_0;
|
553
|
pump_repaired_acknowledgement_1 =
|
554
|
op_mode<>6 and op_mode<>1 and pump_repaired_1;
|
555
|
pump_repaired_acknowledgement_2 =
|
556
|
op_mode<>6 and op_mode<>1 and pump_repaired_2;
|
557
|
pump_repaired_acknowledgement_3 =
|
558
|
op_mode<>6 and op_mode<>1 and pump_repaired_3;
|
559
|
|
560
|
pump_control_failure_detection_0 =
|
561
|
op_mode<>6 and op_mode<>1 and pump_control_defect_0=1;
|
562
|
pump_control_failure_detection_1 =
|
563
|
op_mode<>6 and op_mode<>1 and pump_control_defect_1=1;
|
564
|
pump_control_failure_detection_2 =
|
565
|
op_mode<>6 and op_mode<>1 and pump_control_defect_2=1;
|
566
|
pump_control_failure_detection_3 =
|
567
|
op_mode<>6 and op_mode<>1 and pump_control_defect_3=1;
|
568
|
|
569
|
pump_control_repaired_acknowledgement_0 =
|
570
|
op_mode<>6 and op_mode<>1 and pump_control_repaired_0;
|
571
|
pump_control_repaired_acknowledgement_1 =
|
572
|
op_mode<>6 and op_mode<>1 and pump_control_repaired_1;
|
573
|
pump_control_repaired_acknowledgement_2 =
|
574
|
op_mode<>6 and op_mode<>1 and pump_control_repaired_2;
|
575
|
pump_control_repaired_acknowledgement_3 =
|
576
|
op_mode<>6 and op_mode<>1 and pump_control_repaired_3;
|
577
|
tel
|
578
|
|
579
|
|
580
|
|
581
|
node BoilerController(
|
582
|
stop,
|
583
|
steam_boiler_waiting,
|
584
|
physical_units_ready : bool;
|
585
|
level : int;
|
586
|
steam : int;
|
587
|
pump_state_0,pump_state_1,pump_state_2,pump_state_3 : int;
|
588
|
pump_control_state_0,pump_control_state_1,pump_control_state_2,pump_control_state_3 : bool;
|
589
|
pump_repaired_0,pump_repaired_1,pump_repaired_2,pump_repaired_3 : bool;
|
590
|
pump_control_repaired_0,pump_control_repaired_1,pump_control_repaired_2,pump_control_repaired_3 : bool;
|
591
|
level_repaired : bool;
|
592
|
steam_repaired : bool;
|
593
|
pump_failure_acknowledgement_0,pump_failure_acknowledgement_1,pump_failure_acknowledgement_2,pump_failure_acknowledgement_3 : bool;
|
594
|
pump_control_failure_acknowledgement_0,pump_control_failure_acknowledgement_1,pump_control_failure_acknowledgement_2,pump_control_failure_acknowledgement_3 : bool;
|
595
|
level_failure_acknowledgement : bool;
|
596
|
steam_failure_acknowledgement : bool)
|
597
|
|
598
|
returns(
|
599
|
program_ready : bool;
|
600
|
mode : int;
|
601
|
valve : bool;
|
602
|
open_pump_0,open_pump_1,open_pump_2,open_pump_3 : bool;
|
603
|
close_pump_0,close_pump_1,close_pump_2,close_pump_3 : bool;
|
604
|
pump_failure_detection_0,pump_failure_detection_1,pump_failure_detection_2,pump_failure_detection_3 : bool;
|
605
|
pump_control_failure_detection_0,pump_control_failure_detection_1,pump_control_failure_detection_2,pump_control_failure_detection_3 : bool;
|
606
|
level_failure_detection : bool;
|
607
|
steam_outcome_failure_detection : bool;
|
608
|
pump_repaired_acknowledgement_0,pump_repaired_acknowledgement_1,pump_repaired_acknowledgement_2,pump_repaired_acknowledgement_3 : bool;
|
609
|
pump_control_repaired_acknowledgement_0,pump_control_repaired_acknowledgement_1,pump_control_repaired_acknowledgement_2,pump_control_repaired_acknowledgement_3 : bool;
|
610
|
level_repaired_acknowledgement : bool;
|
611
|
steam_outcome_repaired_acknowledgement: bool);
|
612
|
var
|
613
|
stop_request : bool;
|
614
|
op_mode : int;
|
615
|
q : int;
|
616
|
v : int;
|
617
|
p_0,p_1,p_2,p_3 : int;
|
618
|
valve_state : int;
|
619
|
n_pumps : int;
|
620
|
pump_status_0,pump_status_1,pump_status_2,pump_status_3 : int;
|
621
|
level_defect : int;
|
622
|
steam_defect : int;
|
623
|
pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3 : int;
|
624
|
pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3 : int;
|
625
|
flow_0,flow_1,flow_2,flow_3 : bool;
|
626
|
t00,t01,t10,t20,t30,t11,t21,t31:int;
|
627
|
t02,t12,t22,t32,u4,u6:bool;
|
628
|
t4,t5,t6,t7,t8,t9,u0,u1,u2,u3,u5,u7:int;
|
629
|
a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24:bool;
|
630
|
b0,b1,b2,b3:bool;
|
631
|
let
|
632
|
stop_request = Operator(stop);
|
633
|
|
634
|
level_defect = 0->
|
635
|
LevelDefect(level_failure_acknowledgement, level_repaired, level);
|
636
|
|
637
|
steam_defect = 0->
|
638
|
SteamDefect(steam_failure_acknowledgement, steam_repaired, steam);
|
639
|
|
640
|
pump_defect_0 = 0 -> t00;
|
641
|
pump_control_defect_0 = 0 -> t01;
|
642
|
flow_0 = false -> t02;
|
643
|
|
644
|
(t00,t01,t02) =
|
645
|
PumpDefect(pump_failure_acknowledgement_0, pump_repaired_0,
|
646
|
pump_control_failure_acknowledgement_0, pump_control_repaired_0,
|
647
|
pre(pump_status_0), pump_state_0, pump_control_state_0);
|
648
|
|
649
|
pump_defect_1 = 0 -> t10;
|
650
|
pump_control_defect_1 = 0 -> t11;
|
651
|
flow_1 = false -> t12;
|
652
|
|
653
|
(t10,t11,t12) =
|
654
|
PumpDefect(pump_failure_acknowledgement_1, pump_repaired_1,
|
655
|
pump_control_failure_acknowledgement_1, pump_control_repaired_1,
|
656
|
pre(pump_status_1), pump_state_1, pump_control_state_1);
|
657
|
|
658
|
pump_defect_2 = 0 -> t20;
|
659
|
pump_control_defect_2 = 0 -> t21;
|
660
|
flow_2 = false -> t22;
|
661
|
|
662
|
(t20,t21,t22) =
|
663
|
PumpDefect(pump_failure_acknowledgement_2, pump_repaired_2,
|
664
|
pump_control_failure_acknowledgement_2, pump_control_repaired_2,
|
665
|
pre(pump_status_2), pump_state_2, pump_control_state_2);
|
666
|
|
667
|
pump_defect_3 = 0 -> t30;
|
668
|
pump_control_defect_3 = 0 -> t31;
|
669
|
flow_3 = false -> t32;
|
670
|
|
671
|
(t30,t31,t32) =
|
672
|
PumpDefect(pump_failure_acknowledgement_3, pump_repaired_3,
|
673
|
pump_control_failure_acknowledgement_3, pump_control_repaired_3,
|
674
|
pre(pump_status_3), pump_state_3, pump_control_state_3);
|
675
|
|
676
|
q = level -> t4;
|
677
|
v = steam -> t5;
|
678
|
p_0 = 0 -> t6;
|
679
|
p_1 = 0 -> t7;
|
680
|
p_2 = 0 -> t8;
|
681
|
p_3 = 0 -> t9;
|
682
|
|
683
|
(t4,t5,t6,t7,t8,t9) =
|
684
|
Dynamics(pre(valve_state), level, steam, level_defect, steam_defect, flow_0,flow_1,flow_2,flow_3);
|
685
|
|
686
|
n_pumps = 0-> PumpsDecision(q,v);
|
687
|
|
688
|
pump_status_0 = 0 -> u0;
|
689
|
pump_status_1 = 0 -> u1;
|
690
|
pump_status_2 = 0 -> u2;
|
691
|
pump_status_3 = 0 -> u3;
|
692
|
|
693
|
(u0,u1,u2,u3) =
|
694
|
PumpsStatus(n_pumps, pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3,
|
695
|
flow_0,flow_1,flow_2,flow_3);
|
696
|
|
697
|
op_mode = 1->
|
698
|
ControlMode( steam_boiler_waiting, physical_units_ready, stop_request, steam, level_defect, steam_defect, pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3, pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3, q, pump_state_0,pump_state_1,pump_state_2,pump_state_3);
|
699
|
|
700
|
|
701
|
valve = false -> u4;
|
702
|
valve_state = 0 -> u5;
|
703
|
(u4,u5) =
|
704
|
Valve(op_mode,q);
|
705
|
|
706
|
|
707
|
program_ready = false -> u6;
|
708
|
mode = 1-> u7;
|
709
|
|
710
|
(u6,u7) =
|
711
|
ControlOutput(op_mode,level,valve);
|
712
|
|
713
|
open_pump_0=a1;
|
714
|
open_pump_1=a2;
|
715
|
open_pump_2=a3;
|
716
|
open_pump_3=a4;
|
717
|
close_pump_0=a5;
|
718
|
close_pump_1=a6;
|
719
|
close_pump_2=a7;
|
720
|
close_pump_3=a8;
|
721
|
pump_failure_detection_0=a9;
|
722
|
pump_failure_detection_1=a10;
|
723
|
pump_failure_detection_2=a11;
|
724
|
pump_failure_detection_3=a12;
|
725
|
pump_repaired_acknowledgement_0=a13;
|
726
|
pump_repaired_acknowledgement_1=a14;
|
727
|
pump_repaired_acknowledgement_2=a15;
|
728
|
pump_repaired_acknowledgement_3=a16;
|
729
|
pump_control_failure_detection_0=a17;
|
730
|
pump_control_failure_detection_1=a18;
|
731
|
pump_control_failure_detection_2=a19;
|
732
|
pump_control_failure_detection_3=a20;
|
733
|
pump_control_repaired_acknowledgement_0=a21;
|
734
|
pump_control_repaired_acknowledgement_1=a22;
|
735
|
pump_control_repaired_acknowledgement_2=a23;
|
736
|
pump_control_repaired_acknowledgement_3=a24;
|
737
|
|
738
|
(a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24)=
|
739
|
PumpsOutput(op_mode, pump_status_0,pump_status_1,pump_status_2,pump_status_3,
|
740
|
pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3,
|
741
|
pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3,
|
742
|
pump_repaired_0,pump_repaired_1,pump_repaired_2,pump_repaired_3,
|
743
|
pump_control_repaired_0,pump_control_repaired_1,pump_control_repaired_2,pump_control_repaired_3);
|
744
|
|
745
|
level_failure_detection = false -> b0;
|
746
|
level_repaired_acknowledgement = false -> b1;
|
747
|
|
748
|
(b0,b1)=
|
749
|
LevelOutput(op_mode,level_defect,level_repaired);
|
750
|
|
751
|
steam_outcome_failure_detection = false -> b2;
|
752
|
steam_outcome_repaired_acknowledgement = false -> b3;
|
753
|
(b2,b3)=
|
754
|
SteamOutput(op_mode,steam_defect,steam_repaired);
|
755
|
tel
|
756
|
|
757
|
|
758
|
|
759
|
--@ ensures OK;
|
760
|
node top(
|
761
|
stop,
|
762
|
steam_boiler_waiting,
|
763
|
physical_units_ready : bool;
|
764
|
level : int;
|
765
|
steam : int;
|
766
|
pump_state_0,pump_state_1,pump_state_2,pump_state_3 : int;
|
767
|
pump_control_state_0,pump_control_state_1,pump_control_state_2,pump_control_state_3 : bool;
|
768
|
pump_repaired_0,pump_repaired_1,pump_repaired_2,pump_repaired_3 : bool;
|
769
|
pump_control_repaired_0,pump_control_repaired_1,pump_control_repaired_2,pump_control_repaired_3 : bool;
|
770
|
level_repaired : bool;
|
771
|
steam_repaired : bool;
|
772
|
pump_failure_acknowledgement_0,pump_failure_acknowledgement_1,pump_failure_acknowledgement_2,pump_failure_acknowledgement_3 : bool;
|
773
|
pump_control_failure_acknowledgement_0,pump_control_failure_acknowledgement_1,pump_control_failure_acknowledgement_2,pump_control_failure_acknowledgement_3 : bool;
|
774
|
level_failure_acknowledgement : bool;
|
775
|
steam_failure_acknowledgement : bool)
|
776
|
returns(OK:bool);
|
777
|
var
|
778
|
program_ready,mode_ok,mode_normal_then_no_failure,mode_normal_then_valve_off : bool;
|
779
|
mode : int;
|
780
|
valve : bool;
|
781
|
open_pump_0,open_pump_1,open_pump_2,open_pump_3 : bool;
|
782
|
close_pump_0,close_pump_1,close_pump_2,close_pump_3 : bool;
|
783
|
pump_failure_detection_0,pump_failure_detection_1,pump_failure_detection_2,pump_failure_detection_3 : bool;
|
784
|
pump_control_failure_detection_0,pump_control_failure_detection_1,pump_control_failure_detection_2,pump_control_failure_detection_3 : bool;
|
785
|
level_failure_detection : bool;
|
786
|
steam_outcome_failure_detection : bool;
|
787
|
pump_repaired_acknowledgement_0,pump_repaired_acknowledgement_1,pump_repaired_acknowledgement_2,pump_repaired_acknowledgement_3 : bool;
|
788
|
pump_control_repaired_acknowledgement_0,pump_control_repaired_acknowledgement_1,pump_control_repaired_acknowledgement_2,pump_control_repaired_acknowledgement_3 : bool;
|
789
|
level_repaired_acknowledgement : bool;
|
790
|
steam_outcome_repaired_acknowledgement : bool;
|
791
|
let
|
792
|
(program_ready, mode, valve, open_pump_0,open_pump_1,open_pump_2,open_pump_3, close_pump_0,close_pump_1,close_pump_2,close_pump_3, pump_failure_detection_0,pump_failure_detection_1,pump_failure_detection_2,pump_failure_detection_3, pump_control_failure_detection_0,pump_control_failure_detection_1,pump_control_failure_detection_2,pump_control_failure_detection_3,
|
793
|
level_failure_detection, steam_outcome_failure_detection, pump_repaired_acknowledgement_0,pump_repaired_acknowledgement_1,pump_repaired_acknowledgement_2,pump_repaired_acknowledgement_3,
|
794
|
pump_control_repaired_acknowledgement_0,pump_control_repaired_acknowledgement_1,pump_control_repaired_acknowledgement_2,pump_control_repaired_acknowledgement_3, level_repaired_acknowledgement,
|
795
|
steam_outcome_repaired_acknowledgement) =
|
796
|
BoilerController(stop, steam_boiler_waiting, physical_units_ready, level, steam, pump_state_0,pump_state_1,pump_state_2,pump_state_3,
|
797
|
pump_control_state_0,pump_control_state_1,pump_control_state_2,pump_control_state_3, pump_repaired_0,pump_repaired_1,pump_repaired_2,pump_repaired_3, pump_control_repaired_0,pump_control_repaired_1,pump_control_repaired_2,pump_control_repaired_3, level_repaired, steam_repaired,
|
798
|
pump_failure_acknowledgement_0,pump_failure_acknowledgement_1,pump_failure_acknowledgement_2,pump_failure_acknowledgement_3, pump_control_failure_acknowledgement_0,pump_control_failure_acknowledgement_1,pump_control_failure_acknowledgement_2,pump_control_failure_acknowledgement_3, level_failure_acknowledgement,
|
799
|
steam_failure_acknowledgement);
|
800
|
|
801
|
OK=
|
802
|
mode_ok and
|
803
|
mode_normal_then_no_failure and
|
804
|
mode_normal_then_valve_off;
|
805
|
|
806
|
mode_ok =
|
807
|
mode=1 or
|
808
|
mode=2 or
|
809
|
mode=3 or
|
810
|
mode=4 or
|
811
|
mode=5 or
|
812
|
mode=6;
|
813
|
|
814
|
mode_normal_then_valve_off = mode=3 => not(valve);
|
815
|
|
816
|
mode_normal_then_no_failure =
|
817
|
(mode=3 =>
|
818
|
not(level_failure_detection) and
|
819
|
not(steam_outcome_failure_detection) and
|
820
|
AND(not(pump_failure_detection_0),not(pump_failure_detection_1),not(pump_failure_detection_2),not(pump_failure_detection_3)) and
|
821
|
AND(not(pump_control_failure_detection_0),not(pump_control_failure_detection_1),not(pump_control_failure_detection_2),not(pump_control_failure_detection_3)));
|
822
|
--!k:2;
|
823
|
--!PROPERTY: OK=true;
|
824
|
--%MAIN;
|
825
|
tel
|
826
|
|