lustrec / test / src / kind_fmcad08 / large / steam_boiler_no_arr1.lus @ 0cbf0839
History | View | Annotate | Download (27.2 KB)
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 |
node top( |
760 |
stop, |
761 |
steam_boiler_waiting, |
762 |
physical_units_ready : bool; |
763 |
level : int; |
764 |
steam : int; |
765 |
pump_state_0,pump_state_1,pump_state_2,pump_state_3 : int; |
766 |
pump_control_state_0,pump_control_state_1,pump_control_state_2,pump_control_state_3 : bool; |
767 |
pump_repaired_0,pump_repaired_1,pump_repaired_2,pump_repaired_3 : bool; |
768 |
pump_control_repaired_0,pump_control_repaired_1,pump_control_repaired_2,pump_control_repaired_3 : bool; |
769 |
level_repaired : bool; |
770 |
steam_repaired : bool; |
771 |
pump_failure_acknowledgement_0,pump_failure_acknowledgement_1,pump_failure_acknowledgement_2,pump_failure_acknowledgement_3 : bool; |
772 |
pump_control_failure_acknowledgement_0,pump_control_failure_acknowledgement_1,pump_control_failure_acknowledgement_2,pump_control_failure_acknowledgement_3 : bool; |
773 |
level_failure_acknowledgement : bool; |
774 |
steam_failure_acknowledgement : bool) |
775 |
returns(OK:bool); |
776 |
var |
777 |
program_ready,mode_ok,mode_normal_then_no_failure,mode_normal_then_valve_off : bool; |
778 |
mode : int; |
779 |
valve : bool; |
780 |
open_pump_0,open_pump_1,open_pump_2,open_pump_3 : bool; |
781 |
close_pump_0,close_pump_1,close_pump_2,close_pump_3 : bool; |
782 |
pump_failure_detection_0,pump_failure_detection_1,pump_failure_detection_2,pump_failure_detection_3 : bool; |
783 |
pump_control_failure_detection_0,pump_control_failure_detection_1,pump_control_failure_detection_2,pump_control_failure_detection_3 : bool; |
784 |
level_failure_detection : bool; |
785 |
steam_outcome_failure_detection : bool; |
786 |
pump_repaired_acknowledgement_0,pump_repaired_acknowledgement_1,pump_repaired_acknowledgement_2,pump_repaired_acknowledgement_3 : bool; |
787 |
pump_control_repaired_acknowledgement_0,pump_control_repaired_acknowledgement_1,pump_control_repaired_acknowledgement_2,pump_control_repaired_acknowledgement_3 : bool; |
788 |
level_repaired_acknowledgement : bool; |
789 |
steam_outcome_repaired_acknowledgement : bool; |
790 |
let |
791 |
(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, |
792 |
level_failure_detection, steam_outcome_failure_detection, pump_repaired_acknowledgement_0,pump_repaired_acknowledgement_1,pump_repaired_acknowledgement_2,pump_repaired_acknowledgement_3, |
793 |
pump_control_repaired_acknowledgement_0,pump_control_repaired_acknowledgement_1,pump_control_repaired_acknowledgement_2,pump_control_repaired_acknowledgement_3, level_repaired_acknowledgement, |
794 |
steam_outcome_repaired_acknowledgement) = |
795 |
BoilerController(stop, steam_boiler_waiting, physical_units_ready, level, steam, pump_state_0,pump_state_1,pump_state_2,pump_state_3, |
796 |
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, |
797 |
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, |
798 |
steam_failure_acknowledgement); |
799 |
|
800 |
OK= |
801 |
mode_ok and |
802 |
mode_normal_then_no_failure and |
803 |
mode_normal_then_valve_off; |
804 |
|
805 |
mode_ok = |
806 |
mode=1 or |
807 |
mode=2 or |
808 |
mode=3 or |
809 |
mode=4 or |
810 |
mode=5 or |
811 |
mode=6; |
812 |
|
813 |
mode_normal_then_valve_off = mode=3 => not(valve); |
814 |
|
815 |
mode_normal_then_no_failure = |
816 |
(mode=3 => |
817 |
not(level_failure_detection) and |
818 |
not(steam_outcome_failure_detection) and |
819 |
AND(not(pump_failure_detection_0),not(pump_failure_detection_1),not(pump_failure_detection_2),not(pump_failure_detection_3)) and |
820 |
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))); |
821 |
--%PROPERTY OK=true; |
822 |
--%MAIN; |
823 |
tel |
824 |
|