Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / large / steam_boiler.lus @ b745c1a8

History | View | Annotate | Download (23.9 KB)

1

    
2
node abs(x:int)
3
returns(y:int)
4
let y = if x >= 0 then x else -x ; tel
5

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