Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / large / steam_boiler_no_arr2.lus @ 22fe1c93

History | View | Annotate | Download (24.2 KB)

1
-- STEAM BOILER example
2
-- from The Steam Boiler Problem in Lustre
3
-- by Thierry Cattel and Gregory Duval
4

    
5

    
6

    
7

    
8
node REDGE(S:bool) returns(REDGE:bool); 
9
let 
10
  REDGE= S -> S and not(pre(S)); 
11
tel
12

    
13
 
14

    
15
node sum(a_0,a_1,a_2,a_3:int) returns(sum:int); 
16
let 
17
  sum = a_0 + a_1 + a_2 + a_3; 
18
tel
19

    
20
 
21
node AND(a_0,a_1,a_2,a_3:bool) returns(AND:bool); 
22
let 
23
  AND = a_0 and a_1 and a_2 and a_3;
24
tel
25

    
26
node OR(a_0,a_1,a_2,a_3:bool) returns(OR:bool); 
27
let 
28
  OR = a_0 or a_1 or a_2 or a_3;
29
tel
30

    
31

    
32
node NOT(a_0,a_1,a_2,a_3:bool) returns(NOT_0,NOT_1,NOT_2,NOT_3:bool); 
33
let 
34
  NOT_0 = not a_0;
35
  NOT_1 = not a_1;
36
  NOT_2 = not a_2;
37
  NOT_3 = not a_3;
38
tel
39

    
40
 
41

    
42
node FEDGE1(S:bool) returns(FEDGE1:bool); 
43
let 
44
  FEDGE1= not(S) -> not(S) and pre(S); 
45
tel
46

    
47
 
48

    
49
node FEDGE2(S:bool) returns(FEDGE2:bool); 
50
let 
51
  FEDGE2= REDGE(not(S)); 
52
tel
53

    
54
 
55

    
56
node Verification(S1,S2:bool) returns(property_ok:bool); 
57
var property1,property2:bool; 
58
let 
59
  property1=FEDGE1(S1)=FEDGE2(S1); 
60

    
61
--  assert(S2=not(S1)); 
62
  property2=FEDGE1(S1)=REDGE(S2);
63

    
64
  property_ok=if (S2=not(S1)) then
65
(property1 and property2)
66
else true;
67
tel
68

    
69
 
70

    
71
node Operator(stop:bool) returns (stop_request:bool); 
72
var nb_stops:int; 
73
let 
74
  nb_stops = (if stop then 1 else 0) -> 
75
    if stop then pre(nb_stops)+1 else 0; 
76
  stop_request = (nb_stops>=3); 
77
tel
78

    
79
 
80

    
81
node Defect(statein:int; fail_cond,ack_chan,repair_chan:bool) 
82
  returns(stateout:int); 
83
let 
84
  stateout = if (statein=0) then 
85
    if fail_cond then 1 else 0 
86
    else 
87
      if (statein=1) then 
88
        if ack_chan then 2 else 1 
89
      else -- statein=2 
90
        if repair_chan then 0 else 2; 
91
tel
92

    
93

    
94
node level_failure_detect(level:int) returns(level_failure_detect:bool); 
95
let 
96
  level_failure_detect = ((level < 0) or (level > 1000)); 
97
tel
98

    
99
node steam_failure_detect(steam:int) returns(steam_failure_detect:bool); 
100
let 
101
  steam_failure_detect = ((steam < 0) or (steam > 25)); 
102
tel
103

    
104
node LevelDefect(level_failure_acknowledgement,level_repaired:bool; 
105
  level:int) 
106
  returns( LevelDefect:int); 
107
let 
108
  LevelDefect = 0 -> 
109
    Defect(pre(LevelDefect), level_failure_detect(level), level_failure_acknowledgement, level_repaired); 
110
tel
111

    
112

    
113
node SteamDefect(steam_failure_acknowledgement,steam_repaired:bool; 
114
  steam:int) 
115
  returns( SteamDefect:int); 
116
let 
117
  SteamDefect = 0 -> 
118
    Defect(pre(SteamDefect), steam_failure_detect(steam), steam_failure_acknowledgement, steam_repaired); 
119
tel
120

    
121

    
122
node pump_failure_detect(pump_status,pump_state:int; 
123
  pump_control_state:bool) 
124
  returns(pump_failure_detect,pump_control_failure_detect,flow:bool); 
125
let 
126
  pump_failure_detect = ((pump_status=0) and pump_state=1) 
127
    or (((pump_status=1) or (pump_status=2))and pump_state=0); 
128
  pump_control_failure_detect = (((pump_status=0) or 
129
    (pump_status=2)) and pump_state=0 and pump_control_state) 
130
    or ((pump_status=1) and pump_state=1 and not(pump_control_state)) 
131
    or ((pump_status=2) and pump_state=1 and pump_control_state); 
132
  flow = ((pump_status=0) and pump_state=1 and pump_control_state) 
133
    or ((pump_status=1) and pump_state=0 and pump_control_state) 
134
    or ((pump_status=1) and pump_state=1); 
135
tel
136

    
137
 
138

    
139

    
140
node PumpDefect( 
141
  pump_failure_acknowledgement,pump_repaired, 
142
  pump_control_failure_acknowledgement,pump_control_repaired:bool; 
143
  pump_status,pump_state:int; 
144
  pump_control_state:bool) 
145
  returns(PumpDefect,PumpControlDefect:int;Flow:bool); 
146
var 
147
  pump_failure_d, pump_control_failure_d:bool; 
148
let 
149
  (pump_failure_d, pump_control_failure_d, Flow) = pump_failure_detect(pump_status, pump_state, pump_control_state); 
150
  PumpDefect = 0 -> 
151
    Defect(pre(PumpDefect), pump_failure_d, pump_failure_acknowledgement, pump_repaired); 
152
  PumpControlDefect = 0 -> 
153
    Defect(pre(PumpControlDefect), pump_control_failure_d, pump_control_failure_acknowledgement, pump_control_repaired); 
154
tel
155

    
156
 
157

    
158
node level_failure(level_defect:int) returns(level_failure:bool); 
159
let 
160
  level_failure = (level_defect<>0); 
161
tel
162

    
163
node steam_failure(steam_defect:int) returns(steam_failure:bool); 
164
let 
165
  steam_failure = (steam_defect<>0); 
166
tel
167
 
168
node pump_failure(pump_defect:int) returns(pump_failure:bool); 
169
let 
170
  pump_failure = (pump_defect<>0); 
171
tel
172
 
173
node pump_control_failure(pump_defect:int) returns(pump_failure:bool); 
174
let 
175
  pump_failure = (pump_defect<>0); 
176
tel
177

    
178

    
179
node Dynamics(valve_state,level,steam,level_defect,steam_defect:int; 
180
  flow_0,flow_1,flow_2,flow_3:bool) 
181
  returns (q,v:int; p_0,p_1,p_2,p_3:int); 
182
let 
183
  q = level-> 
184
    if level_failure(level_defect) then 
185
      pre(q) - steam*5 + sum(p_0,p_1,p_2,p_3)*5 - (if valve_state=1 then 10*5 else 0) 
186
    else 
187
      level; 
188
  v = steam-> 
189
    if steam_failure(steam_defect) then 
190
      (pre(q) -q) div 5 + sum(p_0,p_1,p_2,p_3)*5 
191
    else 
192
      steam; 
193
  p_0 = 0-> 
194
    if (not(flow_0)) then 
195
      0 
196
    else 
197
      15; 
198
  p_1 = 0-> 
199
    if (not(flow_1)) then 
200
      0 
201
    else 
202
      15; 
203
  p_2 = 0-> 
204
    if (not(flow_2)) then 
205
      0 
206
    else 
207
      15; 
208
  p_3 = 0-> 
209
    if (not(flow_3)) then 
210
      0 
211
    else 
212
      15; 
213
      
214
tel
215

    
216
 
217

    
218
node PumpsDecision(q,v:int) returns (n_pumps:int); 
219
let 
220
  n_pumps = if q>600 then 
221
      (v div 15) 
222
    else 
223
      if q<400 then 
224
        (v div 15) +1 
225
      else 
226
        pre(n_pumps) ; 
227
tel
228

    
229
 
230

    
231

    
232

    
233
node operate_pumps(n, n_pumps_to_open:int; 
234
  pump_status_0,pump_status_1,pump_status_2,pump_status_3,
235
  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3:int; 
236
  flow_0,flow_1,flow_2,flow_3:bool) 
237
  returns(operate_pumps_0,operate_pumps_1,operate_pumps_2,operate_pumps_3:int); 
238
let 
239
  operate_pumps_0 =  
240
      if ((n_pumps_to_open>0) and 
241
        not(flow_0) and 
242
        not(pump_failure(pump_defect_0)) and 
243
        (pump_status_0=0)) then 
244
        2 
245
      else 
246
        if ((n_pumps_to_open<0) and 
247
          flow_0 and 
248
          not(pump_failure(pump_defect_0)) and 
249
          (pump_status_0=1)) then 
250
          0 
251
        else 
252
          if (pump_status_0=2) then 
253
            1 
254
          else 
255
            if (pre(pump_defect_0)=2 and 
256
              pump_defect_0=0) then 
257
              if pump_status_0=1 then 
258
                0 
259
              else --necessarily 0 
260
                1 
261
            else 
262
              pump_status_0; 
263

    
264
  operate_pumps_1 =  
265
      if ((n_pumps_to_open>0) and 
266
        not(flow_1) and 
267
        not(pump_failure(pump_defect_1)) and 
268
        (pump_status_1=0)) then 
269
        2 
270
      else 
271
        if ((n_pumps_to_open<0) and 
272
          flow_1 and 
273
          not(pump_failure(pump_defect_1)) and 
274
          (pump_status_1=1)) then 
275
          0 
276
        else 
277
          if (pump_status_1=2) then 
278
            1 
279
          else 
280
            if (pre(pump_defect_1)=2 and 
281
              pump_defect_1=0) then 
282
              if pump_status_1=1 then 
283
                0 
284
              else --necessarily 0 
285
                1 
286
            else 
287
              pump_status_1; 
288

    
289
  operate_pumps_2 =  
290
      if ((n_pumps_to_open>0) and 
291
        not(flow_2) and 
292
        not(pump_failure(pump_defect_2)) and 
293
        (pump_status_2=0)) then 
294
        2 
295
      else 
296
        if ((n_pumps_to_open<0) and 
297
          flow_2 and 
298
          not(pump_failure(pump_defect_2)) and 
299
          (pump_status_2=1)) then 
300
          0 
301
        else 
302
          if (pump_status_2=2) then 
303
            1 
304
          else 
305
            if (pre(pump_defect_2)=2 and 
306
              pump_defect_2=0) then 
307
              if pump_status_2=1 then 
308
                0 
309
              else --necessarily 0 
310
                1 
311
            else 
312
              pump_status_2; 
313

    
314
  operate_pumps_3 =  
315
      if ((n_pumps_to_open>0) and 
316
        not(flow_3) and 
317
        not(pump_failure(pump_defect_3)) and 
318
        (pump_status_3=0)) then 
319
        2 
320
      else 
321
        if ((n_pumps_to_open<0) and 
322
          flow_3 and 
323
          not(pump_failure(pump_defect_3)) and 
324
          (pump_status_3=1)) then 
325
          0 
326
        else 
327
          if (pump_status_3=2) then 
328
            1 
329
          else 
330
            if (pre(pump_defect_3)=2 and 
331
              pump_defect_3=0) then 
332
              if pump_status_3=1 then 
333
                0 
334
              else --necessarily 0 
335
                1 
336
            else 
337
              pump_status_3; 
338

    
339
tel
340

    
341
node PumpsStatus( 
342
  n_pumps:int; 
343
  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3:int; 
344
  flow_0,flow_1,flow_2,flow_3:bool) 
345
  returns(pump_status_0,pump_status_1,pump_status_2,pump_status_3:int); 
346
var 
347
  n_pumps_flow,n_pumps_to_open:int; 
348
  t0,t1,t2,t3:int;
349
let 
350
  n_pumps_flow = (if flow_0 then 1 else 0) + (if flow_1 then 1 else 0) + 
351
    (if flow_2 then 1 else 0) + (if flow_3 then 1 else 0); 
352
  n_pumps_to_open = n_pumps-n_pumps_flow; 
353
  
354
  pump_status_0 = 0 ->t0;
355
  pump_status_1 = 0 ->t1;
356
  pump_status_2 = 0 ->t2;
357
  pump_status_3 = 0 ->t3;
358
  
359
  (t0,t1,t2,t3) =
360
    operate_pumps(4, n_pumps_to_open, 
361
      pre(pump_status_0),pre(pump_status_1),pre(pump_status_2),pre(pump_status_3), 
362
      pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3, 
363
      flow_0,flow_1,flow_2,flow_3); 
364
tel
365

    
366
node transmission_failure(pump_state_0,pump_state_1,pump_state_2,pump_state_3:int) 
367
  returns(transmission_failure:bool); 
368
let 
369
  transmission_failure = pump_state_0=3 or pump_state_1=3 or pump_state_2=3 or pump_state_3=3; 
370
tel
371

    
372

    
373
node dangerous_level(q:int) returns(dangerous_level:bool); 
374
let 
375
  dangerous_level = (q <= 150) or (q >= 850); 
376
tel
377

    
378
node steam_failure_startup(steam:int) returns(steam_failure_startup:bool); 
379
let 
380
  steam_failure_startup=(steam<>0); 
381
tel
382

    
383

    
384
node critical_failure( 
385
  op_mode,steam,level_defect,steam_defect:int; 
386
  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3:int; 
387
  q:int; 
388
  pump_state_0,pump_state_1,pump_state_2,pump_state_3:int) 
389
  returns(critical_failure:bool); 
390
let 
391
  critical_failure = transmission_failure(pump_state_0,pump_state_1,pump_state_2,pump_state_3) or 
392
    (op_mode=1 and steam_failure_startup(steam)) or 
393
    (op_mode=2 and (level_failure(level_defect) or steam_failure(steam_defect))) or 
394
    (op_mode=3 and dangerous_level(q)) or 
395
    (op_mode=4 and dangerous_level(q)) or 
396
    (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)))); 
397
tel
398
  
399
node failure( 
400
  level_defect,steam_defect:int; 
401
  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) 
402
  returns(failure:bool); 
403
let 
404
  failure = level_failure(level_defect) or 
405
    steam_failure(steam_defect) or 
406
    OR(pump_failure(pump_defect_0),pump_failure(pump_defect_1),pump_failure(pump_defect_2),pump_failure(pump_defect_3)) or 
407
    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)); 
408
tel
409

    
410
node ControlMode( 
411
  steam_boiler_waiting,physical_units_ready,stop_request:bool; 
412
  steam,level_defect,steam_defect:int; 
413
  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; 
414
  q:int; 
415
  pump_state_0,pump_state_1,pump_state_2,pump_state_3:int) 
416
  returns(op_mode :int); 
417
let 
418
  op_mode= 1-> 
419
    if (critical_failure(pre(op_mode), 
420
      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 
421
      stop_request or pre(op_mode)=6) then 
422
      6 
423
    else 
424
      if (pre(op_mode)=1) then 
425
        if steam_boiler_waiting then 2 else 1 
426
      else 
427
        if (pre(op_mode)=2 and not physical_units_ready) then 
428
          2 
429
        else 
430
          if level_failure(level_defect) then 
431
            5 
432
          else 
433
            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 
434
              4 
435
            else 
436
              3; 
437
tel
438

    
439
 
440

    
441
 
442

    
443
 
444
 
445

    
446

    
447
node Valve(op_mode:int;q:int) returns (valve:bool;valve_state:int); 
448
let 
449
  valve_state=0-> 
450
    if (op_mode=2) then 
451
      if (q>600) then 
452
        1 
453
      else 
454
        if (q<=600) then 0 else pre(valve_state) 
455
    else 
456
      pre(valve_state); 
457
  valve =false-> 
458
    (valve_state<>pre(valve_state)); 
459
tel
460

    
461
 
462

    
463
node initialization_complete(op_mode,level:int;valve:bool) 
464
  returns(initialization_complete:bool); 
465
let 
466
  initialization_complete =(op_mode=2) and 
467
    ((400<=level) and (level<=600))and 
468
    not(valve); 
469
tel
470

    
471
 
472
node ControlOutput(op_mode,level:int;valve:bool) 
473
  returns(program_ready:bool;mode:int); 
474
let 
475
  program_ready=initialization_complete(op_mode,level,valve); 
476
  mode =op_mode; 
477
tel
478

    
479
 
480
node LevelOutput(op_mode,level_defect:int; level_repaired:bool) 
481
  returns (level_outcome_failure_detection, 
482
level_outcome_repaired_acknowledgement : bool); 
483
let 
484
  level_outcome_failure_detection= 
485
    not ((op_mode=6) or (op_mode=1)) and 
486
    (level_defect=1); 
487
  level_outcome_repaired_acknowledgement = 
488
    not ((op_mode=6) or (op_mode=1)) and 
489
    level_repaired; 
490
tel
491

    
492

    
493
node SteamOutput(op_mode,steam_defect:int; steam_repaired:bool) 
494
  returns (steam_outcome_failure_detection, 
495
steam_outcome_repaired_acknowledgement : bool); 
496
let 
497
  steam_outcome_failure_detection= 
498
    not ((op_mode=6) or (op_mode=1)) and 
499
    (steam_defect=1); 
500
  steam_outcome_repaired_acknowledgement = 
501
    not ((op_mode=6) or (op_mode=1)) and 
502
    steam_repaired; 
503
tel
504

    
505
 
506

    
507
node PumpsOutput(op_mode:int; 
508
  pump_status_0,pump_status_1,pump_status_2,pump_status_3,
509
  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3,
510
  pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3:int; 
511
  pump_repaired_0,pump_repaired_1,pump_repaired_2,pump_repaired_3,
512
  pump_control_repaired_0,pump_control_repaired_1,pump_control_repaired_2,pump_control_repaired_3:bool) 
513
  returns (open_pump_0,open_pump_1,open_pump_2,open_pump_3,
514
  close_pump_0,close_pump_1,close_pump_2,close_pump_3,
515
  pump_failure_detection_0,pump_failure_detection_1,pump_failure_detection_2,pump_failure_detection_3, 
516
  pump_repaired_acknowledgement_0,pump_repaired_acknowledgement_1,pump_repaired_acknowledgement_2,pump_repaired_acknowledgement_3,
517
  pump_control_failure_detection_0,pump_control_failure_detection_1,pump_control_failure_detection_2,pump_control_failure_detection_3, 
518
  pump_control_repaired_acknowledgement_0,pump_control_repaired_acknowledgement_1,pump_control_repaired_acknowledgement_2,pump_control_repaired_acknowledgement_3 : bool); 
519
let 
520
  open_pump_0 = 
521
     op_mode<>6 and op_mode<>1 and pump_status_0=2;
522
  open_pump_1 = 
523
     op_mode<>6 and op_mode<>1 and pump_status_1=2;
524
  open_pump_2 = 
525
     op_mode<>6 and op_mode<>1 and pump_status_2=2;
526
  open_pump_3 = 
527
     op_mode<>6 and op_mode<>1 and pump_status_3=2; 
528
    
529
  close_pump_0 = 
530
     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;
531
  close_pump_1 = 
532
     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;
533
  close_pump_2 = 
534
     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;
535
  close_pump_3 = 
536
     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;
537
    
538
  pump_failure_detection_0 = 
539
    op_mode<>6 and op_mode<>1 and pump_defect_0=1;
540
  pump_failure_detection_1 = 
541
     op_mode<>6 and op_mode<>1 and pump_defect_1=1;
542
  pump_failure_detection_2 = 
543
     op_mode<>6 and op_mode<>1 and pump_defect_2=1;
544
  pump_failure_detection_3 = 
545
     op_mode<>6 and op_mode<>1 and pump_defect_3=1;
546
    
547
  pump_repaired_acknowledgement_0 = 
548
    op_mode<>6 and op_mode<>1 and pump_repaired_0;
549
  pump_repaired_acknowledgement_1 = 
550
     op_mode<>6 and op_mode<>1 and pump_repaired_1;
551
  pump_repaired_acknowledgement_2 = 
552
     op_mode<>6 and op_mode<>1 and pump_repaired_2;
553
  pump_repaired_acknowledgement_3 = 
554
     op_mode<>6 and op_mode<>1 and pump_repaired_3;
555
    
556
  pump_control_failure_detection_0 = 
557
    op_mode<>6 and op_mode<>1 and pump_control_defect_0=1;
558
  pump_control_failure_detection_1 = 
559
    op_mode<>6 and op_mode<>1 and pump_control_defect_1=1;
560
  pump_control_failure_detection_2 = 
561
    op_mode<>6 and op_mode<>1 and pump_control_defect_2=1;
562
  pump_control_failure_detection_3 = 
563
    op_mode<>6 and op_mode<>1 and pump_control_defect_3=1;
564
    
565
  pump_control_repaired_acknowledgement_0 = 
566
    op_mode<>6 and op_mode<>1 and pump_control_repaired_0;
567
  pump_control_repaired_acknowledgement_1 = 
568
    op_mode<>6 and op_mode<>1 and pump_control_repaired_1;
569
  pump_control_repaired_acknowledgement_2 = 
570
    op_mode<>6 and op_mode<>1 and pump_control_repaired_2;
571
  pump_control_repaired_acknowledgement_3 = 
572
    op_mode<>6 and op_mode<>1 and pump_control_repaired_3;
573
tel
574

    
575
 
576

    
577
node BoilerController( 
578
  stop, 
579
  steam_boiler_waiting, 
580
  physical_units_ready : bool; 
581
  level : int; 
582
  steam : int; 
583
  pump_state_0,pump_state_1,pump_state_2,pump_state_3 : int; 
584
  pump_control_state_0,pump_control_state_1,pump_control_state_2,pump_control_state_3 : bool; 
585
  pump_repaired_0,pump_repaired_1,pump_repaired_2,pump_repaired_3 : bool; 
586
  pump_control_repaired_0,pump_control_repaired_1,pump_control_repaired_2,pump_control_repaired_3 : bool; 
587
  level_repaired : bool; 
588
  steam_repaired : bool; 
589
  pump_failure_acknowledgement_0,pump_failure_acknowledgement_1,pump_failure_acknowledgement_2,pump_failure_acknowledgement_3 : bool; 
590
  pump_control_failure_acknowledgement_0,pump_control_failure_acknowledgement_1,pump_control_failure_acknowledgement_2,pump_control_failure_acknowledgement_3 : bool; 
591
  level_failure_acknowledgement : bool; 
592
  steam_failure_acknowledgement : bool) 
593
  
594
  returns(
595
  program_ready : bool; 
596
  mode : int; 
597
  valve : bool; 
598
  open_pump_0,open_pump_1,open_pump_2,open_pump_3 : bool; 
599
  close_pump_0,close_pump_1,close_pump_2,close_pump_3 : bool; 
600
  pump_failure_detection_0,pump_failure_detection_1,pump_failure_detection_2,pump_failure_detection_3 : bool; 
601
  pump_control_failure_detection_0,pump_control_failure_detection_1,pump_control_failure_detection_2,pump_control_failure_detection_3 : bool; 
602
  level_failure_detection : bool; 
603
  steam_outcome_failure_detection : bool; 
604
  pump_repaired_acknowledgement_0,pump_repaired_acknowledgement_1,pump_repaired_acknowledgement_2,pump_repaired_acknowledgement_3 : bool; 
605
  pump_control_repaired_acknowledgement_0,pump_control_repaired_acknowledgement_1,pump_control_repaired_acknowledgement_2,pump_control_repaired_acknowledgement_3 : bool; 
606
  level_repaired_acknowledgement : bool; 
607
  steam_outcome_repaired_acknowledgement: bool); 
608
var 
609
  stop_request : bool; 
610
  op_mode : int; 
611
  q : int; 
612
  v : int; 
613
  p_0,p_1,p_2,p_3 : int; 
614
  valve_state : int; 
615
  n_pumps : int; 
616
  pump_status_0,pump_status_1,pump_status_2,pump_status_3 : int; 
617
  level_defect : int; 
618
  steam_defect : int; 
619
  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3 : int; 
620
  pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3 : int; 
621
  flow_0,flow_1,flow_2,flow_3 : bool; 
622
  t00,t01,t10,t20,t30,t11,t21,t31:int;
623
  t02,t12,t22,t32,u4,u6:bool;
624
  t4,t5,t6,t7,t8,t9,u0,u1,u2,u3,u5,u7:int;
625
  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;
626
  b0,b1,b2,b3:bool;
627
let 
628
  stop_request = Operator(stop); 
629

    
630
  level_defect = 0-> 
631
    LevelDefect(level_failure_acknowledgement, level_repaired, level); 
632

    
633
  steam_defect = 0-> 
634
    SteamDefect(steam_failure_acknowledgement, steam_repaired, steam); 
635

    
636
  pump_defect_0 = 0 -> t00;
637
  pump_control_defect_0 = 0 -> t01;
638
  flow_0 = false -> t02;
639

    
640
  (t00,t01,t02) =
641
       PumpDefect(pump_failure_acknowledgement_0, pump_repaired_0, 
642
         pump_control_failure_acknowledgement_0, pump_control_repaired_0,
643
         pre(pump_status_0), pump_state_0, pump_control_state_0); 
644
         
645
  pump_defect_1 = 0 -> t10;
646
  pump_control_defect_1 = 0 -> t11;
647
  flow_1 = false -> t12;
648

    
649
  (t10,t11,t12) =
650
       PumpDefect(pump_failure_acknowledgement_1, pump_repaired_1, 
651
         pump_control_failure_acknowledgement_1, pump_control_repaired_1,
652
         pre(pump_status_1), pump_state_1, pump_control_state_1); 
653
         
654
  pump_defect_2 = 0 -> t20;
655
  pump_control_defect_2 = 0 -> t21;
656
  flow_2 = false -> t22;
657

    
658
  (t20,t21,t22) =
659
       PumpDefect(pump_failure_acknowledgement_2, pump_repaired_2, 
660
         pump_control_failure_acknowledgement_2, pump_control_repaired_2,
661
         pre(pump_status_2), pump_state_2, pump_control_state_2); 
662
         
663
  pump_defect_3 = 0 -> t30;
664
  pump_control_defect_3 = 0 -> t31;
665
  flow_3 = false -> t32;
666

    
667
  (t30,t31,t32) =
668
       PumpDefect(pump_failure_acknowledgement_3, pump_repaired_3, 
669
         pump_control_failure_acknowledgement_3, pump_control_repaired_3,
670
         pre(pump_status_3), pump_state_3, pump_control_state_3); 
671

    
672
  q = level -> t4;
673
  v = steam -> t5;
674
  p_0 = 0 -> t6;
675
  p_1 = 0 -> t7;
676
  p_2 = 0 -> t8;
677
  p_3 = 0 -> t9;
678

    
679
  (t4,t5,t6,t7,t8,t9) =
680
    Dynamics(pre(valve_state), level, steam, level_defect, steam_defect, flow_0,flow_1,flow_2,flow_3); 
681

    
682
  n_pumps = 0-> PumpsDecision(q,v); 
683

    
684
  pump_status_0 = 0 -> u0;
685
  pump_status_1 = 0 -> u1;
686
  pump_status_2 = 0 -> u2;
687
  pump_status_3 = 0 -> u3;
688
  
689
  (u0,u1,u2,u3) =
690
    PumpsStatus(n_pumps, pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3,
691
      flow_0,flow_1,flow_2,flow_3); 
692

    
693
  op_mode = 1-> 
694
    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); 
695

    
696

    
697
  valve = false -> u4;
698
  valve_state = 0 -> u5;
699
  (u4,u5) =
700
    Valve(op_mode,q); 
701

    
702

    
703
  program_ready = false -> u6;
704
  mode = 1-> u7;
705
  
706
  (u6,u7) =
707
    ControlOutput(op_mode,level,valve); 
708

    
709
  open_pump_0=a1;
710
  open_pump_1=a2;
711
  open_pump_2=a3;
712
  open_pump_3=a4;
713
  close_pump_0=a5;
714
  close_pump_1=a6;
715
  close_pump_2=a7;
716
  close_pump_3=a8;
717
  pump_failure_detection_0=a9;
718
  pump_failure_detection_1=a10;
719
  pump_failure_detection_2=a11;
720
  pump_failure_detection_3=a12;
721
  pump_repaired_acknowledgement_0=a13;
722
  pump_repaired_acknowledgement_1=a14;
723
  pump_repaired_acknowledgement_2=a15;
724
  pump_repaired_acknowledgement_3=a16;
725
  pump_control_failure_detection_0=a17;
726
  pump_control_failure_detection_1=a18;
727
  pump_control_failure_detection_2=a19;
728
  pump_control_failure_detection_3=a20;
729
  pump_control_repaired_acknowledgement_0=a21;
730
  pump_control_repaired_acknowledgement_1=a22;
731
  pump_control_repaired_acknowledgement_2=a23;
732
  pump_control_repaired_acknowledgement_3=a24;
733
  
734
   (a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24)=
735
      PumpsOutput(op_mode, pump_status_0,pump_status_1,pump_status_2,pump_status_3,
736
        pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3,
737
        pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3,
738
        pump_repaired_0,pump_repaired_1,pump_repaired_2,pump_repaired_3,
739
        pump_control_repaired_0,pump_control_repaired_1,pump_control_repaired_2,pump_control_repaired_3); 
740

    
741
  level_failure_detection = false -> b0;
742
  level_repaired_acknowledgement = false -> b1;
743

    
744
  (b0,b1)=
745
    LevelOutput(op_mode,level_defect,level_repaired); 
746

    
747
  steam_outcome_failure_detection = false -> b2;
748
  steam_outcome_repaired_acknowledgement = false -> b3;
749
  (b2,b3)=
750
    SteamOutput(op_mode,steam_defect,steam_repaired); 
751
tel
752

    
753

    
754
node top(
755
  steam_boiler_waiting,physical_units_ready,stop_request:bool; 
756
  steam,level_defect,steam_defect:int; 
757
  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; 
758
  q:int; 
759
  pump_state_0,pump_state_1,pump_state_2,pump_state_3:int) 
760
  returns(OK:bool); 
761
var 
762
  op_mode :int; 
763
  mode_normal_then_water_level_ok, 
764
  mode_normal_then_no_stop_request:bool; 
765
let 
766
  op_mode= 
767
    ControlMode(
768
      steam_boiler_waiting,physical_units_ready,stop_request,
769
      steam,level_defect,steam_defect,
770
      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,
771
      q, pump_state_0,pump_state_1,pump_state_2,pump_state_3); 
772

    
773
  OK = 
774
    mode_normal_then_water_level_ok and 
775
    mode_normal_then_no_stop_request; 
776

    
777
  mode_normal_then_no_stop_request = 
778
    (op_mode=3 => not(stop_request)); 
779

    
780
  mode_normal_then_water_level_ok = 
781
    true ->
782
    (op_mode=3 and pre(op_mode)=3 =>
783
    not(dangerous_level(q))); 
784
  --%PROPERTY OK=true;
785
  --%MAIN;
786
tel
787

    
788
 
789