Project

General

Profile

Download (27.2 KB) Statistics
| Branch: | Tag: | Revision:
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
node AND(a_0,a_1,a_2,a_3:bool) returns(AND:bool); 
21
let 
22
  AND = a_0 and a_1 and a_2 and a_3;
23
tel
24

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

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

    
39
 
40

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

    
46
 
47

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

    
53
 
54

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

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

    
63
  property_ok=
64
if S2=not(S1) then
65
property1 and property2
66
 else true
67
; 
68
tel
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
node level_failure(level_defect:int) returns(level_failure:bool); 
158
let 
159
  level_failure = (level_defect<>0); 
160
tel
161
 
162
node steam_failure(steam_defect:int) returns(steam_failure:bool); 
163
let 
164
  steam_failure = (steam_defect<>0); 
165
tel
166

    
167
node pump_failure(pump_defect:int) returns(pump_failure:bool); 
168
let 
169
  pump_failure = (pump_defect<>0); 
170
tel
171

    
172
node pump_control_failure(pump_defect:int) returns(pump_failure:bool); 
173
let 
174
  pump_failure = (pump_defect<>0); 
175
tel
176
 
177

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

    
215
 
216

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

    
228
 
229

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

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

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

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

    
336
tel
337

    
338

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

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

    
370
node steam_failure_startup(steam:int) returns(steam_failure_startup:bool); 
371
let 
372
  steam_failure_startup=(steam<>0); 
373
tel
374

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

    
380
 
381

    
382
node critical_failure( 
383
  op_mode,steam,level_defect,steam_defect:int; 
384
  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3:int; 
385
  q:int; 
386
  pump_state_0,pump_state_1,pump_state_2,pump_state_3:int) 
387
  returns(critical_failure:bool); 
388
let 
389
  critical_failure = transmission_failure(pump_state_0,pump_state_1,pump_state_2,pump_state_3) or 
390
    (op_mode=1 and steam_failure_startup(steam)) or 
391
    (op_mode=2 and (level_failure(level_defect) or steam_failure(steam_defect))) or 
392
    (op_mode=3 and dangerous_level(q)) or 
393
    (op_mode=4 and dangerous_level(q)) or 
394
    (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)))); 
395
tel
396

    
397

    
398
node failure( 
399
  level_defect,steam_defect:int; 
400
  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) 
401
  returns(failure:bool); 
402
let 
403
  failure = level_failure(level_defect) or 
404
    steam_failure(steam_defect) or 
405
    OR(pump_failure(pump_defect_0),pump_failure(pump_defect_1),pump_failure(pump_defect_2),pump_failure(pump_defect_3)) or 
406
    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)); 
407
tel
408

    
409
 
410

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

    
440
 
441

    
442
 
443

    
444
 
445
 
446

    
447
 
448

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

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

    
472

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

    
480
 
481

    
482
 
483

    
484
node SteamOutput(op_mode,steam_defect:int; steam_repaired:bool) 
485
  returns (steam_outcome_failure_detection, 
486
steam_outcome_repaired_acknowledgement : bool); 
487
let 
488
  steam_outcome_failure_detection= 
489
    not ((op_mode=6) or (op_mode=1)) and 
490
    (steam_defect=1); 
491
  steam_outcome_repaired_acknowledgement = 
492
    not ((op_mode=6) or (op_mode=1)) and 
493
    steam_repaired; 
494
tel
495

    
496
node LevelOutput(op_mode,level_defect:int; level_repaired:bool) 
497
  returns (level_outcome_failure_detection, 
498
level_outcome_repaired_acknowledgement : bool); 
499
let 
500
  level_outcome_failure_detection= 
501
    not ((op_mode=6) or (op_mode=1)) and 
502
    (level_defect=1); 
503
  level_outcome_repaired_acknowledgement = 
504
    not ((op_mode=6) or (op_mode=1)) and 
505
    level_repaired; 
506
tel
507

    
508
 
509

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

    
579
 
580

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

    
634
  level_defect = 0-> 
635
    LevelDefect(level_failure_acknowledgement, level_repaired, level); 
636

    
637
  steam_defect = 0-> 
638
    SteamDefect(steam_failure_acknowledgement, steam_repaired, steam); 
639

    
640
  pump_defect_0 = 0 -> t00;
641
  pump_control_defect_0 = 0 -> t01;
642
  flow_0 = false -> t02;
643

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

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

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

    
671
  (t30,t31,t32) =
672
       PumpDefect(pump_failure_acknowledgement_3, pump_repaired_3, 
673
         pump_control_failure_acknowledgement_3, pump_control_repaired_3,
674
         pre(pump_status_3), pump_state_3, pump_control_state_3); 
675

    
676
  q = level -> t4;
677
  v = steam -> t5;
678
  p_0 = 0 -> t6;
679
  p_1 = 0 -> t7;
680
  p_2 = 0 -> t8;
681
  p_3 = 0 -> t9;
682

    
683
  (t4,t5,t6,t7,t8,t9) =
684
    Dynamics(pre(valve_state), level, steam, level_defect, steam_defect, flow_0,flow_1,flow_2,flow_3); 
685

    
686
  n_pumps = 0-> PumpsDecision(q,v); 
687

    
688
  pump_status_0 = 0 -> u0;
689
  pump_status_1 = 0 -> u1;
690
  pump_status_2 = 0 -> u2;
691
  pump_status_3 = 0 -> u3;
692
  
693
  (u0,u1,u2,u3) =
694
    PumpsStatus(n_pumps, pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3,
695
      flow_0,flow_1,flow_2,flow_3); 
696

    
697
  op_mode = 1-> 
698
    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); 
699

    
700

    
701
  valve = false -> u4;
702
  valve_state = 0 -> u5;
703
  (u4,u5) =
704
    Valve(op_mode,q); 
705

    
706

    
707
  program_ready = false -> u6;
708
  mode = 1-> u7;
709
  
710
  (u6,u7) =
711
    ControlOutput(op_mode,level,valve); 
712

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

    
745
  level_failure_detection = false -> b0;
746
  level_repaired_acknowledgement = false -> b1;
747

    
748
  (b0,b1)=
749
    LevelOutput(op_mode,level_defect,level_repaired); 
750

    
751
  steam_outcome_failure_detection = false -> b2;
752
  steam_outcome_repaired_acknowledgement = false -> b3;
753
  (b2,b3)=
754
    SteamOutput(op_mode,steam_defect,steam_repaired); 
755
tel
756

    
757
 
758

    
759
--@ ensures OK;
760
node top( 
761
  stop, 
762
  steam_boiler_waiting, 
763
  physical_units_ready : bool; 
764
  level : int; 
765
  steam : int; 
766
  pump_state_0,pump_state_1,pump_state_2,pump_state_3 : int; 
767
  pump_control_state_0,pump_control_state_1,pump_control_state_2,pump_control_state_3 : bool; 
768
  pump_repaired_0,pump_repaired_1,pump_repaired_2,pump_repaired_3 : bool; 
769
  pump_control_repaired_0,pump_control_repaired_1,pump_control_repaired_2,pump_control_repaired_3 : bool; 
770
  level_repaired : bool; 
771
  steam_repaired : bool; 
772
  pump_failure_acknowledgement_0,pump_failure_acknowledgement_1,pump_failure_acknowledgement_2,pump_failure_acknowledgement_3 : bool; 
773
  pump_control_failure_acknowledgement_0,pump_control_failure_acknowledgement_1,pump_control_failure_acknowledgement_2,pump_control_failure_acknowledgement_3 : bool; 
774
  level_failure_acknowledgement : bool; 
775
  steam_failure_acknowledgement : bool) 
776
  returns(OK:bool); 
777
var 
778
  program_ready,mode_ok,mode_normal_then_no_failure,mode_normal_then_valve_off : bool; 
779
  mode : int; 
780
  valve : bool; 
781
  open_pump_0,open_pump_1,open_pump_2,open_pump_3 : bool; 
782
  close_pump_0,close_pump_1,close_pump_2,close_pump_3 : bool; 
783
  pump_failure_detection_0,pump_failure_detection_1,pump_failure_detection_2,pump_failure_detection_3 : bool; 
784
  pump_control_failure_detection_0,pump_control_failure_detection_1,pump_control_failure_detection_2,pump_control_failure_detection_3 : bool; 
785
  level_failure_detection : bool; 
786
  steam_outcome_failure_detection : bool; 
787
  pump_repaired_acknowledgement_0,pump_repaired_acknowledgement_1,pump_repaired_acknowledgement_2,pump_repaired_acknowledgement_3 : bool; 
788
  pump_control_repaired_acknowledgement_0,pump_control_repaired_acknowledgement_1,pump_control_repaired_acknowledgement_2,pump_control_repaired_acknowledgement_3 : bool; 
789
  level_repaired_acknowledgement : bool; 
790
  steam_outcome_repaired_acknowledgement : bool;
791
let 
792
  (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,
793
      level_failure_detection, steam_outcome_failure_detection, pump_repaired_acknowledgement_0,pump_repaired_acknowledgement_1,pump_repaired_acknowledgement_2,pump_repaired_acknowledgement_3,
794
      pump_control_repaired_acknowledgement_0,pump_control_repaired_acknowledgement_1,pump_control_repaired_acknowledgement_2,pump_control_repaired_acknowledgement_3, level_repaired_acknowledgement, 
795
      steam_outcome_repaired_acknowledgement) = 
796
    BoilerController(stop, steam_boiler_waiting, physical_units_ready, level, steam, pump_state_0,pump_state_1,pump_state_2,pump_state_3, 
797
      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, 
798
      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, 
799
      steam_failure_acknowledgement); 
800

    
801
  OK= 
802
    mode_ok and 
803
    mode_normal_then_no_failure and 
804
    mode_normal_then_valve_off; 
805

    
806
  mode_ok = 
807
    mode=1 or 
808
    mode=2 or 
809
    mode=3 or 
810
    mode=4 or 
811
    mode=5 or 
812
    mode=6; 
813

    
814
  mode_normal_then_valve_off = mode=3 => not(valve); 
815

    
816
  mode_normal_then_no_failure = 
817
    (mode=3 =>
818
      not(level_failure_detection) and 
819
      not(steam_outcome_failure_detection) and 
820
      AND(not(pump_failure_detection_0),not(pump_failure_detection_1),not(pump_failure_detection_2),not(pump_failure_detection_3)) and 
821
      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))); 
822
--!k:2;
823
--!PROPERTY: OK=true;
824
  --%MAIN;
825
tel
826

    
(16-16/23)