Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / large / BROKEN / steam_boiler_no_arr2_e8_21449_e5_18210.lus @ b8dc00eb

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 + 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 and 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) -1- 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
--@ ensures OK;
626
node top(
627
  steam_boiler_waiting,physical_units_ready,stop_request:bool; 
628
  steam,level_defect,steam_defect:int; 
629
  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; 
630
  q:int; 
631
  pump_state_0,pump_state_1,pump_state_2,pump_state_3:int) 
632
  returns(OK:bool); 
633
var 
634
  op_mode :int; 
635
  mode_normal_then_water_level_ok, 
636
  mode_normal_then_no_stop_request:bool; 
637
let 
638
  op_mode= 
639
    ControlMode(
640
      steam_boiler_waiting,physical_units_ready,stop_request,
641
      steam,level_defect,steam_defect,
642
      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,
643
      q, pump_state_0,pump_state_1,pump_state_2,pump_state_3); 
644
  OK = 
645
    mode_normal_then_water_level_ok and 
646
    mode_normal_then_no_stop_request; 
647
  mode_normal_then_no_stop_request = 
648
    (op_mode=3 => not(stop_request)); 
649
  mode_normal_then_water_level_ok = 
650
    true ->
651
    (op_mode=3 and pre(op_mode)=3 =>
652
    not(dangerous_level(q))); 
653
  --%MAIN;
654
  --%PROPERTY  OK=true;
655
tel