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