Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / large / all files / steam_boiler_no_arr1_e4_23904_e4_2384.lus @ b8dc00eb

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