### Profile

« Previous | Next »

## Revision e45f370e

add case where emf order is not good

View differences:

1

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

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

Also available in: Unified diff