Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / large / src / BROKEN / steam_boiler_no_arr2.smt2 @ fa9e78e5

History | View | Annotate | Download (175 KB)

1
; AND
2
(declare-var AND.a_0 Bool)
3
(declare-var AND.a_1 Bool)
4
(declare-var AND.a_2 Bool)
5
(declare-var AND.a_3 Bool)
6
(declare-var AND.AND Bool)
7
(declare-rel AND (Bool Bool Bool Bool Bool))
8
(rule (=> 
9
  (= AND.AND (and (and (and AND.a_0 AND.a_1) AND.a_2) AND.a_3))
10
  (AND AND.a_0 AND.a_1 AND.a_2 AND.a_3 AND.AND)
11
))
12

    
13
; dangerous_level
14
(declare-var dangerous_level.q Int)
15
(declare-var dangerous_level.dangerous_level Bool)
16
(declare-rel dangerous_level (Int Bool))
17
(rule (=> 
18
  (= dangerous_level.dangerous_level (or (<= dangerous_level.q 150) (>= dangerous_level.q 850)))
19
  (dangerous_level dangerous_level.q dangerous_level.dangerous_level)
20
))
21

    
22
; level_failure
23
(declare-var level_failure.level_defect Int)
24
(declare-var level_failure.level_failure Bool)
25
(declare-rel level_failure (Int Bool))
26
(rule (=> 
27
  (= level_failure.level_failure (not (= level_failure.level_defect 0)))
28
  (level_failure level_failure.level_defect level_failure.level_failure)
29
))
30

    
31
; pump_failure
32
(declare-var pump_failure.pump_defect Int)
33
(declare-var pump_failure.pump_failure Bool)
34
(declare-rel pump_failure (Int Bool))
35
(rule (=> 
36
  (= pump_failure.pump_failure (not (= pump_failure.pump_defect 0)))
37
  (pump_failure pump_failure.pump_defect pump_failure.pump_failure)
38
))
39

    
40
; steam_failure
41
(declare-var steam_failure.steam_defect Int)
42
(declare-var steam_failure.steam_failure Bool)
43
(declare-rel steam_failure (Int Bool))
44
(rule (=> 
45
  (= steam_failure.steam_failure (not (= steam_failure.steam_defect 0)))
46
  (steam_failure steam_failure.steam_defect steam_failure.steam_failure)
47
))
48

    
49
; steam_failure_startup
50
(declare-var steam_failure_startup.steam Int)
51
(declare-var steam_failure_startup.steam_failure_startup Bool)
52
(declare-rel steam_failure_startup (Int Bool))
53
(rule (=> 
54
  (= steam_failure_startup.steam_failure_startup (not (= steam_failure_startup.steam 0)))
55
  (steam_failure_startup steam_failure_startup.steam steam_failure_startup.steam_failure_startup)
56
))
57

    
58
; transmission_failure
59
(declare-var transmission_failure.pump_state_0 Int)
60
(declare-var transmission_failure.pump_state_1 Int)
61
(declare-var transmission_failure.pump_state_2 Int)
62
(declare-var transmission_failure.pump_state_3 Int)
63
(declare-var transmission_failure.transmission_failure Bool)
64
(declare-rel transmission_failure (Int Int Int Int Bool))
65
(rule (=> 
66
  (= transmission_failure.transmission_failure (or (or (or (= transmission_failure.pump_state_0 3) (= transmission_failure.pump_state_1 3)) (= transmission_failure.pump_state_2 3)) (= transmission_failure.pump_state_3 3)))
67
  (transmission_failure transmission_failure.pump_state_0 transmission_failure.pump_state_1 transmission_failure.pump_state_2 transmission_failure.pump_state_3 transmission_failure.transmission_failure)
68
))
69

    
70
; OR
71
(declare-var OR.a_0 Bool)
72
(declare-var OR.a_1 Bool)
73
(declare-var OR.a_2 Bool)
74
(declare-var OR.a_3 Bool)
75
(declare-var OR.OR Bool)
76
(declare-rel OR (Bool Bool Bool Bool Bool))
77
(rule (=> 
78
  (= OR.OR (or (or (or OR.a_0 OR.a_1) OR.a_2) OR.a_3))
79
  (OR OR.a_0 OR.a_1 OR.a_2 OR.a_3 OR.OR)
80
))
81

    
82
; pump_control_failure
83
(declare-var pump_control_failure.pump_defect Int)
84
(declare-var pump_control_failure.pump_failure Bool)
85
(declare-rel pump_control_failure (Int Bool))
86
(rule (=> 
87
  (= pump_control_failure.pump_failure (not (= pump_control_failure.pump_defect 0)))
88
  (pump_control_failure pump_control_failure.pump_defect pump_control_failure.pump_failure)
89
))
90

    
91
; REDGE
92
(declare-var REDGE.S Bool)
93
(declare-var REDGE.REDGE Bool)
94
(declare-var REDGE.__REDGE_2_c Bool)
95
(declare-var REDGE.ni_30._arrow._first_c Bool)
96
(declare-var REDGE.__REDGE_2_m Bool)
97
(declare-var REDGE.ni_30._arrow._first_m Bool)
98
(declare-var REDGE.__REDGE_2_x Bool)
99
(declare-var REDGE.ni_30._arrow._first_x Bool)
100
(declare-var REDGE.__REDGE_1 Bool)
101
(declare-rel REDGE_reset (Bool Bool Bool Bool))
102
(declare-rel REDGE_step (Bool Bool Bool Bool Bool Bool))
103

    
104
(rule (=> 
105
  (and 
106
       (= REDGE.__REDGE_2_m REDGE.__REDGE_2_c)
107
       (= REDGE.ni_30._arrow._first_m true)
108
  )
109
  (REDGE_reset REDGE.__REDGE_2_c
110
               REDGE.ni_30._arrow._first_c
111
               REDGE.__REDGE_2_m
112
               REDGE.ni_30._arrow._first_m)
113
))
114

    
115
(rule (=> 
116
  (and (= REDGE.ni_30._arrow._first_m REDGE.ni_30._arrow._first_c)(and (= REDGE.__REDGE_1 (ite REDGE.ni_30._arrow._first_m true false))
117
                                                                    (= REDGE.ni_30._arrow._first_x false))
118
       (and (or (not (= REDGE.__REDGE_1 true))
119
               (= REDGE.REDGE REDGE.S))
120
            (or (not (= REDGE.__REDGE_1 false))
121
               (= REDGE.REDGE (and REDGE.S (not REDGE.__REDGE_2_c))))
122
       )
123
       (= REDGE.__REDGE_2_x REDGE.S)
124
       )
125
  (REDGE_step REDGE.S
126
              REDGE.REDGE
127
              REDGE.__REDGE_2_c
128
              REDGE.ni_30._arrow._first_c
129
              REDGE.__REDGE_2_x
130
              REDGE.ni_30._arrow._first_x)
131
))
132

    
133
; critical_failure
134
(declare-var critical_failure.op_mode Int)
135
(declare-var critical_failure.steam Int)
136
(declare-var critical_failure.level_defect Int)
137
(declare-var critical_failure.steam_defect Int)
138
(declare-var critical_failure.pump_defect_0 Int)
139
(declare-var critical_failure.pump_defect_1 Int)
140
(declare-var critical_failure.pump_defect_2 Int)
141
(declare-var critical_failure.pump_defect_3 Int)
142
(declare-var critical_failure.q Int)
143
(declare-var critical_failure.pump_state_0 Int)
144
(declare-var critical_failure.pump_state_1 Int)
145
(declare-var critical_failure.pump_state_2 Int)
146
(declare-var critical_failure.pump_state_3 Int)
147
(declare-var critical_failure.critical_failure Bool)
148
(declare-var critical_failure.__critical_failure_1 Bool)
149
(declare-var critical_failure.__critical_failure_10 Bool)
150
(declare-var critical_failure.__critical_failure_2 Bool)
151
(declare-var critical_failure.__critical_failure_3 Bool)
152
(declare-var critical_failure.__critical_failure_4 Bool)
153
(declare-var critical_failure.__critical_failure_5 Bool)
154
(declare-var critical_failure.__critical_failure_6 Bool)
155
(declare-var critical_failure.__critical_failure_7 Bool)
156
(declare-var critical_failure.__critical_failure_8 Bool)
157
(declare-var critical_failure.__critical_failure_9 Bool)
158
(declare-rel critical_failure (Int Int Int Int Int Int Int Int Int Int Int Int Int Bool))
159
(rule (=> 
160
  (and (steam_failure_startup critical_failure.steam
161
                              critical_failure.__critical_failure_9)
162
       (level_failure critical_failure.level_defect
163
                      critical_failure.__critical_failure_8)
164
       (dangerous_level critical_failure.q
165
                        critical_failure.__critical_failure_7)
166
       (steam_failure critical_failure.steam_defect
167
                      critical_failure.__critical_failure_6)
168
       (pump_failure critical_failure.pump_defect_0
169
                     critical_failure.__critical_failure_4)
170
       (pump_failure critical_failure.pump_defect_1
171
                     critical_failure.__critical_failure_3)
172
       (pump_failure critical_failure.pump_defect_2
173
                     critical_failure.__critical_failure_2)
174
       (pump_failure critical_failure.pump_defect_3
175
                     critical_failure.__critical_failure_1)
176
       (AND critical_failure.__critical_failure_4
177
            critical_failure.__critical_failure_3
178
            critical_failure.__critical_failure_2
179
            critical_failure.__critical_failure_1
180
            critical_failure.__critical_failure_5)
181
       (transmission_failure critical_failure.pump_state_0
182
                             critical_failure.pump_state_1
183
                             critical_failure.pump_state_2
184
                             critical_failure.pump_state_3
185
                             critical_failure.__critical_failure_10)
186
       (= critical_failure.critical_failure (or (or (or (or (or critical_failure.__critical_failure_10 (and (= critical_failure.op_mode 1) critical_failure.__critical_failure_9)) (and (= critical_failure.op_mode 2) (or critical_failure.__critical_failure_8 critical_failure.__critical_failure_6))) (and (= critical_failure.op_mode 3) critical_failure.__critical_failure_7)) (and (= critical_failure.op_mode 4) critical_failure.__critical_failure_7)) (and (= critical_failure.op_mode 5) (or (or critical_failure.__critical_failure_7 critical_failure.__critical_failure_6) critical_failure.__critical_failure_5))))
187
       )
188
  (critical_failure critical_failure.op_mode critical_failure.steam critical_failure.level_defect critical_failure.steam_defect critical_failure.pump_defect_0 critical_failure.pump_defect_1 critical_failure.pump_defect_2 critical_failure.pump_defect_3 critical_failure.q critical_failure.pump_state_0 critical_failure.pump_state_1 critical_failure.pump_state_2 critical_failure.pump_state_3 critical_failure.critical_failure)
189
))
190

    
191
; failure
192
(declare-var failure.level_defect Int)
193
(declare-var failure.steam_defect Int)
194
(declare-var failure.pump_defect_0 Int)
195
(declare-var failure.pump_defect_1 Int)
196
(declare-var failure.pump_defect_2 Int)
197
(declare-var failure.pump_defect_3 Int)
198
(declare-var failure.pump_control_defect_0 Int)
199
(declare-var failure.pump_control_defect_1 Int)
200
(declare-var failure.pump_control_defect_2 Int)
201
(declare-var failure.pump_control_defect_3 Int)
202
(declare-var failure.failure Bool)
203
(declare-var failure.__failure_1 Bool)
204
(declare-var failure.__failure_10 Bool)
205
(declare-var failure.__failure_11 Bool)
206
(declare-var failure.__failure_12 Bool)
207
(declare-var failure.__failure_2 Bool)
208
(declare-var failure.__failure_3 Bool)
209
(declare-var failure.__failure_4 Bool)
210
(declare-var failure.__failure_5 Bool)
211
(declare-var failure.__failure_6 Bool)
212
(declare-var failure.__failure_7 Bool)
213
(declare-var failure.__failure_8 Bool)
214
(declare-var failure.__failure_9 Bool)
215
(declare-rel failure (Int Int Int Int Int Int Int Int Int Int Bool))
216
(rule (=> 
217
  (and (pump_failure failure.pump_defect_0
218
                     failure.__failure_9)
219
       (pump_failure failure.pump_defect_1
220
                     failure.__failure_8)
221
       (pump_failure failure.pump_defect_2
222
                     failure.__failure_7)
223
       (pump_failure failure.pump_defect_3
224
                     failure.__failure_6)
225
       (pump_control_failure failure.pump_control_defect_0
226
                             failure.__failure_4)
227
       (pump_control_failure failure.pump_control_defect_1
228
                             failure.__failure_3)
229
       (pump_control_failure failure.pump_control_defect_2
230
                             failure.__failure_2)
231
       (pump_control_failure failure.pump_control_defect_3
232
                             failure.__failure_1)
233
       (OR failure.__failure_4
234
           failure.__failure_3
235
           failure.__failure_2
236
           failure.__failure_1
237
           failure.__failure_5)
238
       (level_failure failure.level_defect
239
                      failure.__failure_12)
240
       (steam_failure failure.steam_defect
241
                      failure.__failure_11)
242
       (OR failure.__failure_9
243
           failure.__failure_8
244
           failure.__failure_7
245
           failure.__failure_6
246
           failure.__failure_10)
247
       (= failure.failure (or (or (or failure.__failure_12 failure.__failure_11) failure.__failure_10) failure.__failure_5))
248
       )
249
  (failure failure.level_defect failure.steam_defect failure.pump_defect_0 failure.pump_defect_1 failure.pump_defect_2 failure.pump_defect_3 failure.pump_control_defect_0 failure.pump_control_defect_1 failure.pump_control_defect_2 failure.pump_control_defect_3 failure.failure)
250
))
251

    
252
; initialization_complete
253
(declare-var initialization_complete.op_mode Int)
254
(declare-var initialization_complete.level Int)
255
(declare-var initialization_complete.valve Bool)
256
(declare-var initialization_complete.initialization_complete Bool)
257
(declare-rel initialization_complete (Int Int Bool Bool))
258
(rule (=> 
259
  (= initialization_complete.initialization_complete (and (and (= initialization_complete.op_mode 2) (and (<= 400 initialization_complete.level) (<= initialization_complete.level 600))) (not initialization_complete.valve)))
260
  (initialization_complete initialization_complete.op_mode initialization_complete.level initialization_complete.valve initialization_complete.initialization_complete)
261
))
262

    
263
; sum
264
(declare-var sum.a_0 Int)
265
(declare-var sum.a_1 Int)
266
(declare-var sum.a_2 Int)
267
(declare-var sum.a_3 Int)
268
(declare-var sum.sum Int)
269
(declare-rel sum (Int Int Int Int Int))
270
(rule (=> 
271
  (= sum.sum (+ (+ (+ sum.a_0 sum.a_1) sum.a_2) sum.a_3))
272
  (sum sum.a_0 sum.a_1 sum.a_2 sum.a_3 sum.sum)
273
))
274

    
275
; Defect
276
(declare-var Defect.statein Int)
277
(declare-var Defect.fail_cond Bool)
278
(declare-var Defect.ack_chan Bool)
279
(declare-var Defect.repair_chan Bool)
280
(declare-var Defect.stateout Int)
281
(declare-var Defect.__Defect_1 Bool)
282
(declare-var Defect.__Defect_2 Bool)
283
(declare-rel Defect (Int Bool Bool Bool Int))
284
(rule (=> 
285
  (and (= Defect.__Defect_2 (= Defect.statein 1))
286
       (= Defect.__Defect_1 (= Defect.statein 0))
287
       (and (or (not (= Defect.__Defect_1 true))
288
               (and (or (not (= Defect.fail_cond true))
289
                       (= Defect.stateout 1))
290
                    (or (not (= Defect.fail_cond false))
291
                       (= Defect.stateout 0))
292
               ))
293
            (or (not (= Defect.__Defect_1 false))
294
               (and (or (not (= Defect.__Defect_2 true))
295
                       (and (or (not (= Defect.ack_chan true))
296
                               (= Defect.stateout 2))
297
                            (or (not (= Defect.ack_chan false))
298
                               (= Defect.stateout 1))
299
                       ))
300
                    (or (not (= Defect.__Defect_2 false))
301
                       (and (or (not (= Defect.repair_chan true))
302
                               (= Defect.stateout 0))
303
                            (or (not (= Defect.repair_chan false))
304
                               (= Defect.stateout 2))
305
                       ))
306
               ))
307
       )
308
       )
309
  (Defect Defect.statein Defect.fail_cond Defect.ack_chan Defect.repair_chan Defect.stateout)
310
))
311

    
312
; level_failure_detect
313
(declare-var level_failure_detect.level Int)
314
(declare-var level_failure_detect.level_failure_detect Bool)
315
(declare-rel level_failure_detect (Int Bool))
316
(rule (=> 
317
  (= level_failure_detect.level_failure_detect (or (< level_failure_detect.level 0) (> level_failure_detect.level 1000)))
318
  (level_failure_detect level_failure_detect.level level_failure_detect.level_failure_detect)
319
))
320

    
321
; pump_failure_detect
322
(declare-var pump_failure_detect.pump_status Int)
323
(declare-var pump_failure_detect.pump_state Int)
324
(declare-var pump_failure_detect.pump_control_state Bool)
325
(declare-var pump_failure_detect.pump_failure_detect Bool)
326
(declare-var pump_failure_detect.pump_control_failure_detect Bool)
327
(declare-var pump_failure_detect.flow Bool)
328
(declare-rel pump_failure_detect (Int Int Bool Bool Bool Bool))
329
(rule (=> 
330
  (and (= pump_failure_detect.pump_failure_detect (or (and (= pump_failure_detect.pump_status 0) (= pump_failure_detect.pump_state 1)) (and (or (= pump_failure_detect.pump_status 1) (= pump_failure_detect.pump_status 2)) (= pump_failure_detect.pump_state 0))))
331
       (= pump_failure_detect.pump_control_failure_detect (or (or (and (and (or (= pump_failure_detect.pump_status 0) (= pump_failure_detect.pump_status 2)) (= pump_failure_detect.pump_state 0)) pump_failure_detect.pump_control_state) (and (and (= pump_failure_detect.pump_status 1) (= pump_failure_detect.pump_state 1)) (not pump_failure_detect.pump_control_state))) (and (and (= pump_failure_detect.pump_status 2) (= pump_failure_detect.pump_state 1)) pump_failure_detect.pump_control_state)))
332
       (= pump_failure_detect.flow (or (or (and (and (= pump_failure_detect.pump_status 0) (= pump_failure_detect.pump_state 1)) pump_failure_detect.pump_control_state) (and (and (= pump_failure_detect.pump_status 1) (= pump_failure_detect.pump_state 0)) pump_failure_detect.pump_control_state)) (and (= pump_failure_detect.pump_status 1) (= pump_failure_detect.pump_state 1))))
333
       )
334
  (pump_failure_detect pump_failure_detect.pump_status pump_failure_detect.pump_state pump_failure_detect.pump_control_state pump_failure_detect.pump_failure_detect pump_failure_detect.pump_control_failure_detect pump_failure_detect.flow)
335
))
336

    
337
; operate_pumps
338
(declare-var operate_pumps.n Int)
339
(declare-var operate_pumps.n_pumps_to_open Int)
340
(declare-var operate_pumps.pump_status_0 Int)
341
(declare-var operate_pumps.pump_status_1 Int)
342
(declare-var operate_pumps.pump_status_2 Int)
343
(declare-var operate_pumps.pump_status_3 Int)
344
(declare-var operate_pumps.pump_defect_0 Int)
345
(declare-var operate_pumps.pump_defect_1 Int)
346
(declare-var operate_pumps.pump_defect_2 Int)
347
(declare-var operate_pumps.pump_defect_3 Int)
348
(declare-var operate_pumps.flow_0 Bool)
349
(declare-var operate_pumps.flow_1 Bool)
350
(declare-var operate_pumps.flow_2 Bool)
351
(declare-var operate_pumps.flow_3 Bool)
352
(declare-var operate_pumps.operate_pumps_0 Int)
353
(declare-var operate_pumps.operate_pumps_1 Int)
354
(declare-var operate_pumps.operate_pumps_2 Int)
355
(declare-var operate_pumps.operate_pumps_3 Int)
356
(declare-var operate_pumps.__operate_pumps_12_c Int)
357
(declare-var operate_pumps.__operate_pumps_19_c Int)
358
(declare-var operate_pumps.__operate_pumps_26_c Int)
359
(declare-var operate_pumps.__operate_pumps_5_c Int)
360
(declare-var operate_pumps.__operate_pumps_12_m Int)
361
(declare-var operate_pumps.__operate_pumps_19_m Int)
362
(declare-var operate_pumps.__operate_pumps_26_m Int)
363
(declare-var operate_pumps.__operate_pumps_5_m Int)
364
(declare-var operate_pumps.__operate_pumps_12_x Int)
365
(declare-var operate_pumps.__operate_pumps_19_x Int)
366
(declare-var operate_pumps.__operate_pumps_26_x Int)
367
(declare-var operate_pumps.__operate_pumps_5_x Int)
368
(declare-var operate_pumps.__operate_pumps_1 Bool)
369
(declare-var operate_pumps.__operate_pumps_10 Bool)
370
(declare-var operate_pumps.__operate_pumps_11 Bool)
371
(declare-var operate_pumps.__operate_pumps_13 Bool)
372
(declare-var operate_pumps.__operate_pumps_14 Bool)
373
(declare-var operate_pumps.__operate_pumps_15 Bool)
374
(declare-var operate_pumps.__operate_pumps_16 Bool)
375
(declare-var operate_pumps.__operate_pumps_17 Bool)
376
(declare-var operate_pumps.__operate_pumps_18 Bool)
377
(declare-var operate_pumps.__operate_pumps_2 Bool)
378
(declare-var operate_pumps.__operate_pumps_20 Bool)
379
(declare-var operate_pumps.__operate_pumps_21 Bool)
380
(declare-var operate_pumps.__operate_pumps_22 Bool)
381
(declare-var operate_pumps.__operate_pumps_23 Bool)
382
(declare-var operate_pumps.__operate_pumps_24 Bool)
383
(declare-var operate_pumps.__operate_pumps_25 Bool)
384
(declare-var operate_pumps.__operate_pumps_27 Bool)
385
(declare-var operate_pumps.__operate_pumps_28 Bool)
386
(declare-var operate_pumps.__operate_pumps_3 Bool)
387
(declare-var operate_pumps.__operate_pumps_4 Bool)
388
(declare-var operate_pumps.__operate_pumps_6 Bool)
389
(declare-var operate_pumps.__operate_pumps_7 Bool)
390
(declare-var operate_pumps.__operate_pumps_8 Bool)
391
(declare-var operate_pumps.__operate_pumps_9 Bool)
392
(declare-rel operate_pumps_reset (Int Int Int Int Int Int Int Int))
393
(declare-rel operate_pumps_step (Int Int Int Int Int Int Int Int Int Int Bool Bool Bool Bool Int Int Int Int Int Int Int Int Int Int Int Int))
394

    
395
(rule (=> 
396
  (and 
397
       (= operate_pumps.__operate_pumps_12_m operate_pumps.__operate_pumps_12_c)
398
       (= operate_pumps.__operate_pumps_19_m operate_pumps.__operate_pumps_19_c)
399
       (= operate_pumps.__operate_pumps_26_m operate_pumps.__operate_pumps_26_c)
400
       (= operate_pumps.__operate_pumps_5_m operate_pumps.__operate_pumps_5_c)
401
       
402
  )
403
  (operate_pumps_reset operate_pumps.__operate_pumps_12_c
404
                       operate_pumps.__operate_pumps_19_c
405
                       operate_pumps.__operate_pumps_26_c
406
                       operate_pumps.__operate_pumps_5_c
407
                       operate_pumps.__operate_pumps_12_m
408
                       operate_pumps.__operate_pumps_19_m
409
                       operate_pumps.__operate_pumps_26_m
410
                       operate_pumps.__operate_pumps_5_m)
411
))
412

    
413
(rule (=> 
414
  (and (= operate_pumps.__operate_pumps_7 (= operate_pumps.pump_status_3 1))
415
       (= operate_pumps.__operate_pumps_6 (and (= operate_pumps.__operate_pumps_5_c 2) (= operate_pumps.pump_defect_3 0)))
416
       (= operate_pumps.__operate_pumps_4 (= operate_pumps.pump_status_3 2))
417
       (pump_failure operate_pumps.pump_defect_3
418
                     operate_pumps.__operate_pumps_1)
419
       (= operate_pumps.__operate_pumps_3 (and (and (and (< operate_pumps.n_pumps_to_open 0) operate_pumps.flow_3) (not operate_pumps.__operate_pumps_1)) (= operate_pumps.pump_status_3 1)))
420
       (= operate_pumps.__operate_pumps_2 (and (and (and (> operate_pumps.n_pumps_to_open 0) (not operate_pumps.flow_3)) (not operate_pumps.__operate_pumps_1)) (= operate_pumps.pump_status_3 0)))
421
       (and (or (not (= operate_pumps.__operate_pumps_2 true))
422
               (= operate_pumps.operate_pumps_3 2))
423
            (or (not (= operate_pumps.__operate_pumps_2 false))
424
               (and (or (not (= operate_pumps.__operate_pumps_3 true))
425
                       (= operate_pumps.operate_pumps_3 0))
426
                    (or (not (= operate_pumps.__operate_pumps_3 false))
427
                       (and (or (not (= operate_pumps.__operate_pumps_4 true))
428
                               (= operate_pumps.operate_pumps_3 1))
429
                            (or (not (= operate_pumps.__operate_pumps_4 false))
430
                               (and (or (not (= operate_pumps.__operate_pumps_6 true))
431
                                       (and (or (not (= operate_pumps.__operate_pumps_7 true))
432
                                               (= operate_pumps.operate_pumps_3 0))
433
                                            (or (not (= operate_pumps.__operate_pumps_7 false))
434
                                               (= operate_pumps.operate_pumps_3 1))
435
                                       ))
436
                                    (or (not (= operate_pumps.__operate_pumps_6 false))
437
                                       (= operate_pumps.operate_pumps_3 operate_pumps.pump_status_3))
438
                               ))
439
                       ))
440
               ))
441
       )
442
       (pump_failure operate_pumps.pump_defect_2
443
                     operate_pumps.__operate_pumps_8)
444
       (= operate_pumps.__operate_pumps_9 (and (and (and (> operate_pumps.n_pumps_to_open 0) (not operate_pumps.flow_2)) (not operate_pumps.__operate_pumps_8)) (= operate_pumps.pump_status_2 0)))
445
       (= operate_pumps.__operate_pumps_14 (= operate_pumps.pump_status_2 1))
446
       (= operate_pumps.__operate_pumps_13 (and (= operate_pumps.__operate_pumps_12_c 2) (= operate_pumps.pump_defect_2 0)))
447
       (= operate_pumps.__operate_pumps_11 (= operate_pumps.pump_status_2 2))
448
       (= operate_pumps.__operate_pumps_10 (and (and (and (< operate_pumps.n_pumps_to_open 0) operate_pumps.flow_2) (not operate_pumps.__operate_pumps_8)) (= operate_pumps.pump_status_2 1)))
449
       (and (or (not (= operate_pumps.__operate_pumps_9 true))
450
               (= operate_pumps.operate_pumps_2 2))
451
            (or (not (= operate_pumps.__operate_pumps_9 false))
452
               (and (or (not (= operate_pumps.__operate_pumps_10 true))
453
                       (= operate_pumps.operate_pumps_2 0))
454
                    (or (not (= operate_pumps.__operate_pumps_10 false))
455
                       (and (or (not (= operate_pumps.__operate_pumps_11 true))
456
                               (= operate_pumps.operate_pumps_2 1))
457
                            (or (not (= operate_pumps.__operate_pumps_11 false))
458
                               (and (or (not (= operate_pumps.__operate_pumps_13 true))
459
                                       (and (or (not (= operate_pumps.__operate_pumps_14 true))
460
                                               (= operate_pumps.operate_pumps_2 0))
461
                                            (or (not (= operate_pumps.__operate_pumps_14 false))
462
                                               (= operate_pumps.operate_pumps_2 1))
463
                                       ))
464
                                    (or (not (= operate_pumps.__operate_pumps_13 false))
465
                                       (= operate_pumps.operate_pumps_2 operate_pumps.pump_status_2))
466
                               ))
467
                       ))
468
               ))
469
       )
470
       (= operate_pumps.__operate_pumps_21 (= operate_pumps.pump_status_1 1))
471
       (= operate_pumps.__operate_pumps_20 (and (= operate_pumps.__operate_pumps_19_c 2) (= operate_pumps.pump_defect_1 0)))
472
       (= operate_pumps.__operate_pumps_18 (= operate_pumps.pump_status_1 2))
473
       (pump_failure operate_pumps.pump_defect_1
474
                     operate_pumps.__operate_pumps_15)
475
       (= operate_pumps.__operate_pumps_17 (and (and (and (< operate_pumps.n_pumps_to_open 0) operate_pumps.flow_1) (not operate_pumps.__operate_pumps_15)) (= operate_pumps.pump_status_1 1)))
476
       (= operate_pumps.__operate_pumps_16 (and (and (and (> operate_pumps.n_pumps_to_open 0) (not operate_pumps.flow_1)) (not operate_pumps.__operate_pumps_15)) (= operate_pumps.pump_status_1 0)))
477
       (and (or (not (= operate_pumps.__operate_pumps_16 true))
478
               (= operate_pumps.operate_pumps_1 2))
479
            (or (not (= operate_pumps.__operate_pumps_16 false))
480
               (and (or (not (= operate_pumps.__operate_pumps_17 true))
481
                       (= operate_pumps.operate_pumps_1 0))
482
                    (or (not (= operate_pumps.__operate_pumps_17 false))
483
                       (and (or (not (= operate_pumps.__operate_pumps_18 true))
484
                               (= operate_pumps.operate_pumps_1 1))
485
                            (or (not (= operate_pumps.__operate_pumps_18 false))
486
                               (and (or (not (= operate_pumps.__operate_pumps_20 true))
487
                                       (and (or (not (= operate_pumps.__operate_pumps_21 true))
488
                                               (= operate_pumps.operate_pumps_1 0))
489
                                            (or (not (= operate_pumps.__operate_pumps_21 false))
490
                                               (= operate_pumps.operate_pumps_1 1))
491
                                       ))
492
                                    (or (not (= operate_pumps.__operate_pumps_20 false))
493
                                       (= operate_pumps.operate_pumps_1 operate_pumps.pump_status_1))
494
                               ))
495
                       ))
496
               ))
497
       )
498
       (= operate_pumps.__operate_pumps_28 (= operate_pumps.pump_status_0 1))
499
       (= operate_pumps.__operate_pumps_27 (and (= operate_pumps.__operate_pumps_26_c 2) (= operate_pumps.pump_defect_0 0)))
500
       (= operate_pumps.__operate_pumps_25 (= operate_pumps.pump_status_0 2))
501
       (pump_failure operate_pumps.pump_defect_0
502
                     operate_pumps.__operate_pumps_22)
503
       (= operate_pumps.__operate_pumps_24 (and (and (and (< operate_pumps.n_pumps_to_open 0) operate_pumps.flow_0) (not operate_pumps.__operate_pumps_22)) (= operate_pumps.pump_status_0 1)))
504
       (= operate_pumps.__operate_pumps_23 (and (and (and (> operate_pumps.n_pumps_to_open 0) (not operate_pumps.flow_0)) (not operate_pumps.__operate_pumps_22)) (= operate_pumps.pump_status_0 0)))
505
       (and (or (not (= operate_pumps.__operate_pumps_23 true))
506
               (= operate_pumps.operate_pumps_0 2))
507
            (or (not (= operate_pumps.__operate_pumps_23 false))
508
               (and (or (not (= operate_pumps.__operate_pumps_24 true))
509
                       (= operate_pumps.operate_pumps_0 0))
510
                    (or (not (= operate_pumps.__operate_pumps_24 false))
511
                       (and (or (not (= operate_pumps.__operate_pumps_25 true))
512
                               (= operate_pumps.operate_pumps_0 1))
513
                            (or (not (= operate_pumps.__operate_pumps_25 false))
514
                               (and (or (not (= operate_pumps.__operate_pumps_27 true))
515
                                       (and (or (not (= operate_pumps.__operate_pumps_28 true))
516
                                               (= operate_pumps.operate_pumps_0 0))
517
                                            (or (not (= operate_pumps.__operate_pumps_28 false))
518
                                               (= operate_pumps.operate_pumps_0 1))
519
                                       ))
520
                                    (or (not (= operate_pumps.__operate_pumps_27 false))
521
                                       (= operate_pumps.operate_pumps_0 operate_pumps.pump_status_0))
522
                               ))
523
                       ))
524
               ))
525
       )
526
       (= operate_pumps.__operate_pumps_5_x operate_pumps.pump_defect_3)
527
       (= operate_pumps.__operate_pumps_26_x operate_pumps.pump_defect_0)
528
       (= operate_pumps.__operate_pumps_19_x operate_pumps.pump_defect_1)
529
       (= operate_pumps.__operate_pumps_12_x operate_pumps.pump_defect_2)
530
       )
531
  (operate_pumps_step operate_pumps.n
532
                      operate_pumps.n_pumps_to_open
533
                      operate_pumps.pump_status_0
534
                      operate_pumps.pump_status_1
535
                      operate_pumps.pump_status_2
536
                      operate_pumps.pump_status_3
537
                      operate_pumps.pump_defect_0
538
                      operate_pumps.pump_defect_1
539
                      operate_pumps.pump_defect_2
540
                      operate_pumps.pump_defect_3
541
                      operate_pumps.flow_0
542
                      operate_pumps.flow_1
543
                      operate_pumps.flow_2
544
                      operate_pumps.flow_3
545
                      operate_pumps.operate_pumps_0
546
                      operate_pumps.operate_pumps_1
547
                      operate_pumps.operate_pumps_2
548
                      operate_pumps.operate_pumps_3
549
                      operate_pumps.__operate_pumps_12_c
550
                      operate_pumps.__operate_pumps_19_c
551
                      operate_pumps.__operate_pumps_26_c
552
                      operate_pumps.__operate_pumps_5_c
553
                      operate_pumps.__operate_pumps_12_x
554
                      operate_pumps.__operate_pumps_19_x
555
                      operate_pumps.__operate_pumps_26_x
556
                      operate_pumps.__operate_pumps_5_x)
557
))
558

    
559
; steam_failure_detect
560
(declare-var steam_failure_detect.steam Int)
561
(declare-var steam_failure_detect.steam_failure_detect Bool)
562
(declare-rel steam_failure_detect (Int Bool))
563
(rule (=> 
564
  (= steam_failure_detect.steam_failure_detect (or (< steam_failure_detect.steam 0) (> steam_failure_detect.steam 25)))
565
  (steam_failure_detect steam_failure_detect.steam steam_failure_detect.steam_failure_detect)
566
))
567

    
568
; FEDGE1
569
(declare-var FEDGE1.S Bool)
570
(declare-var FEDGE1.FEDGE1 Bool)
571
(declare-var FEDGE1.__FEDGE1_2_c Bool)
572
(declare-var FEDGE1.ni_29._arrow._first_c Bool)
573
(declare-var FEDGE1.__FEDGE1_2_m Bool)
574
(declare-var FEDGE1.ni_29._arrow._first_m Bool)
575
(declare-var FEDGE1.__FEDGE1_2_x Bool)
576
(declare-var FEDGE1.ni_29._arrow._first_x Bool)
577
(declare-var FEDGE1.__FEDGE1_1 Bool)
578
(declare-rel FEDGE1_reset (Bool Bool Bool Bool))
579
(declare-rel FEDGE1_step (Bool Bool Bool Bool Bool Bool))
580

    
581
(rule (=> 
582
  (and 
583
       (= FEDGE1.__FEDGE1_2_m FEDGE1.__FEDGE1_2_c)
584
       (= FEDGE1.ni_29._arrow._first_m true)
585
  )
586
  (FEDGE1_reset FEDGE1.__FEDGE1_2_c
587
                FEDGE1.ni_29._arrow._first_c
588
                FEDGE1.__FEDGE1_2_m
589
                FEDGE1.ni_29._arrow._first_m)
590
))
591

    
592
(rule (=> 
593
  (and (= FEDGE1.ni_29._arrow._first_m FEDGE1.ni_29._arrow._first_c)(and (= FEDGE1.__FEDGE1_1 (ite FEDGE1.ni_29._arrow._first_m true false))
594
                                                                    (= FEDGE1.ni_29._arrow._first_x false))
595
       (and (or (not (= FEDGE1.__FEDGE1_1 true))
596
               (= FEDGE1.FEDGE1 (not FEDGE1.S)))
597
            (or (not (= FEDGE1.__FEDGE1_1 false))
598
               (= FEDGE1.FEDGE1 (and (not FEDGE1.S) FEDGE1.__FEDGE1_2_c)))
599
       )
600
       (= FEDGE1.__FEDGE1_2_x FEDGE1.S)
601
       )
602
  (FEDGE1_step FEDGE1.S
603
               FEDGE1.FEDGE1
604
               FEDGE1.__FEDGE1_2_c
605
               FEDGE1.ni_29._arrow._first_c
606
               FEDGE1.__FEDGE1_2_x
607
               FEDGE1.ni_29._arrow._first_x)
608
))
609

    
610
; FEDGE2
611
(declare-var FEDGE2.S Bool)
612
(declare-var FEDGE2.FEDGE2 Bool)
613
(declare-var FEDGE2.ni_28.REDGE.__REDGE_2_c Bool)
614
(declare-var FEDGE2.ni_28.REDGE.ni_30._arrow._first_c Bool)
615
(declare-var FEDGE2.ni_28.REDGE.__REDGE_2_m Bool)
616
(declare-var FEDGE2.ni_28.REDGE.ni_30._arrow._first_m Bool)
617
(declare-var FEDGE2.ni_28.REDGE.__REDGE_2_x Bool)
618
(declare-var FEDGE2.ni_28.REDGE.ni_30._arrow._first_x Bool)
619
(declare-rel FEDGE2_reset (Bool Bool Bool Bool))
620
(declare-rel FEDGE2_step (Bool Bool Bool Bool Bool Bool))
621

    
622
(rule (=> 
623
  (and 
624
       
625
       (REDGE_reset FEDGE2.ni_28.REDGE.__REDGE_2_c
626
                    FEDGE2.ni_28.REDGE.ni_30._arrow._first_c
627
                    FEDGE2.ni_28.REDGE.__REDGE_2_m
628
                    FEDGE2.ni_28.REDGE.ni_30._arrow._first_m)
629
  )
630
  (FEDGE2_reset FEDGE2.ni_28.REDGE.__REDGE_2_c
631
                FEDGE2.ni_28.REDGE.ni_30._arrow._first_c
632
                FEDGE2.ni_28.REDGE.__REDGE_2_m
633
                FEDGE2.ni_28.REDGE.ni_30._arrow._first_m)
634
))
635

    
636
(rule (=> 
637
  (and (= FEDGE2.ni_28.REDGE.__REDGE_2_m FEDGE2.ni_28.REDGE.__REDGE_2_c)
638
       (= FEDGE2.ni_28.REDGE.ni_30._arrow._first_m FEDGE2.ni_28.REDGE.ni_30._arrow._first_c)
639
       )
640
  (REDGE_step (not FEDGE2.S)
641
              FEDGE2.FEDGE2
642
              FEDGE2.ni_28.REDGE.__REDGE_2_m
643
              FEDGE2.ni_28.REDGE.ni_30._arrow._first_m
644
              FEDGE2.ni_28.REDGE.__REDGE_2_x
645
              FEDGE2.ni_28.REDGE.ni_30._arrow._first_x)
646
  (FEDGE2_step FEDGE2.S
647
               FEDGE2.FEDGE2
648
               FEDGE2.ni_28.REDGE.__REDGE_2_c
649
               FEDGE2.ni_28.REDGE.ni_30._arrow._first_c
650
               FEDGE2.ni_28.REDGE.__REDGE_2_x
651
               FEDGE2.ni_28.REDGE.ni_30._arrow._first_x)
652
))
653

    
654
; ControlMode
655
(declare-var ControlMode.steam_boiler_waiting Bool)
656
(declare-var ControlMode.physical_units_ready Bool)
657
(declare-var ControlMode.stop_request Bool)
658
(declare-var ControlMode.steam Int)
659
(declare-var ControlMode.level_defect Int)
660
(declare-var ControlMode.steam_defect Int)
661
(declare-var ControlMode.pump_defect_0 Int)
662
(declare-var ControlMode.pump_defect_1 Int)
663
(declare-var ControlMode.pump_defect_2 Int)
664
(declare-var ControlMode.pump_defect_3 Int)
665
(declare-var ControlMode.pump_control_defect_0 Int)
666
(declare-var ControlMode.pump_control_defect_1 Int)
667
(declare-var ControlMode.pump_control_defect_2 Int)
668
(declare-var ControlMode.pump_control_defect_3 Int)
669
(declare-var ControlMode.q Int)
670
(declare-var ControlMode.pump_state_0 Int)
671
(declare-var ControlMode.pump_state_1 Int)
672
(declare-var ControlMode.pump_state_2 Int)
673
(declare-var ControlMode.pump_state_3 Int)
674
(declare-var ControlMode.op_mode Int)
675
(declare-var ControlMode.__ControlMode_2_c Int)
676
(declare-var ControlMode.ni_27._arrow._first_c Bool)
677
(declare-var ControlMode.__ControlMode_2_m Int)
678
(declare-var ControlMode.ni_27._arrow._first_m Bool)
679
(declare-var ControlMode.__ControlMode_2_x Int)
680
(declare-var ControlMode.ni_27._arrow._first_x Bool)
681
(declare-var ControlMode.__ControlMode_1 Bool)
682
(declare-var ControlMode.__ControlMode_3 Bool)
683
(declare-var ControlMode.__ControlMode_4 Bool)
684
(declare-var ControlMode.__ControlMode_5 Bool)
685
(declare-var ControlMode.__ControlMode_6 Bool)
686
(declare-var ControlMode.__ControlMode_7 Bool)
687
(declare-var ControlMode.__ControlMode_8 Bool)
688
(declare-rel ControlMode_reset (Int Bool Int Bool))
689
(declare-rel ControlMode_step (Bool Bool Bool Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Bool Int Bool))
690

    
691
(rule (=> 
692
  (and 
693
       (= ControlMode.__ControlMode_2_m ControlMode.__ControlMode_2_c)
694
       (= ControlMode.ni_27._arrow._first_m true)
695
  )
696
  (ControlMode_reset ControlMode.__ControlMode_2_c
697
                     ControlMode.ni_27._arrow._first_c
698
                     ControlMode.__ControlMode_2_m
699
                     ControlMode.ni_27._arrow._first_m)
700
))
701

    
702
(rule (=> 
703
  (and (failure ControlMode.level_defect
704
                ControlMode.steam_defect
705
                ControlMode.pump_defect_0
706
                ControlMode.pump_defect_1
707
                ControlMode.pump_defect_2
708
                ControlMode.pump_defect_3
709
                ControlMode.pump_control_defect_0
710
                ControlMode.pump_control_defect_1
711
                ControlMode.pump_control_defect_2
712
                ControlMode.pump_control_defect_3
713
                ControlMode.__ControlMode_8)
714
       (level_failure ControlMode.level_defect
715
                      ControlMode.__ControlMode_7)
716
       (= ControlMode.__ControlMode_6 (and (= ControlMode.__ControlMode_2_c 2) (not ControlMode.physical_units_ready)))
717
       (= ControlMode.__ControlMode_5 (= ControlMode.__ControlMode_2_c 1))
718
       (critical_failure ControlMode.__ControlMode_2_c
719
                         ControlMode.steam
720
                         ControlMode.level_defect
721
                         ControlMode.steam_defect
722
                         ControlMode.pump_defect_0
723
                         ControlMode.pump_defect_1
724
                         ControlMode.pump_defect_2
725
                         ControlMode.pump_defect_3
726
                         ControlMode.q
727
                         ControlMode.pump_state_0
728
                         ControlMode.pump_state_1
729
                         ControlMode.pump_state_2
730
                         ControlMode.pump_state_3
731
                         ControlMode.__ControlMode_3)
732
       (= ControlMode.__ControlMode_4 (or (or ControlMode.__ControlMode_3 ControlMode.stop_request) (= ControlMode.__ControlMode_2_c 6)))
733
       (= ControlMode.ni_27._arrow._first_m ControlMode.ni_27._arrow._first_c)
734
       (and (= ControlMode.__ControlMode_1 (ite ControlMode.ni_27._arrow._first_m true false))
735
            (= ControlMode.ni_27._arrow._first_x false))
736
       (and (or (not (= ControlMode.__ControlMode_1 true))
737
               (= ControlMode.op_mode 1))
738
            (or (not (= ControlMode.__ControlMode_1 false))
739
               (and (or (not (= ControlMode.__ControlMode_4 true))
740
                       (= ControlMode.op_mode 6))
741
                    (or (not (= ControlMode.__ControlMode_4 false))
742
                       (and (or (not (= ControlMode.__ControlMode_5 true))
743
                               (and (or (not (= ControlMode.steam_boiler_waiting true))
744
                                       (= ControlMode.op_mode 2))
745
                                    (or (not (= ControlMode.steam_boiler_waiting false))
746
                                       (= ControlMode.op_mode 1))
747
                               ))
748
                            (or (not (= ControlMode.__ControlMode_5 false))
749
                               (and (or (not (= ControlMode.__ControlMode_6 true))
750
                                       (= ControlMode.op_mode 2))
751
                                    (or (not (= ControlMode.__ControlMode_6 false))
752
                                       (and (or (not (= ControlMode.__ControlMode_7 true))
753
                                               (= ControlMode.op_mode 5))
754
                                            (or (not (= ControlMode.__ControlMode_7 false))
755
                                               (and (or (not (= ControlMode.__ControlMode_8 true))
756
                                                       (= ControlMode.op_mode 4))
757
                                                    (or (not (= ControlMode.__ControlMode_8 false))
758
                                                       (= ControlMode.op_mode 3))
759
                                               ))
760
                                       ))
761
                               ))
762
                       ))
763
               ))
764
       )
765
       (= ControlMode.__ControlMode_2_x ControlMode.op_mode)
766
       )
767
  (ControlMode_step ControlMode.steam_boiler_waiting
768
                    ControlMode.physical_units_ready
769
                    ControlMode.stop_request
770
                    ControlMode.steam
771
                    ControlMode.level_defect
772
                    ControlMode.steam_defect
773
                    ControlMode.pump_defect_0
774
                    ControlMode.pump_defect_1
775
                    ControlMode.pump_defect_2
776
                    ControlMode.pump_defect_3
777
                    ControlMode.pump_control_defect_0
778
                    ControlMode.pump_control_defect_1
779
                    ControlMode.pump_control_defect_2
780
                    ControlMode.pump_control_defect_3
781
                    ControlMode.q
782
                    ControlMode.pump_state_0
783
                    ControlMode.pump_state_1
784
                    ControlMode.pump_state_2
785
                    ControlMode.pump_state_3
786
                    ControlMode.op_mode
787
                    ControlMode.__ControlMode_2_c
788
                    ControlMode.ni_27._arrow._first_c
789
                    ControlMode.__ControlMode_2_x
790
                    ControlMode.ni_27._arrow._first_x)
791
))
792

    
793
; ControlOutput
794
(declare-var ControlOutput.op_mode Int)
795
(declare-var ControlOutput.level Int)
796
(declare-var ControlOutput.valve Bool)
797
(declare-var ControlOutput.program_ready Bool)
798
(declare-var ControlOutput.mode Int)
799
(declare-rel ControlOutput (Int Int Bool Bool Int))
800
(rule (=> 
801
  (and (initialization_complete ControlOutput.op_mode
802
                                ControlOutput.level
803
                                ControlOutput.valve
804
                                ControlOutput.program_ready)
805
       (= ControlOutput.mode ControlOutput.op_mode)
806
       )
807
  (ControlOutput ControlOutput.op_mode ControlOutput.level ControlOutput.valve ControlOutput.program_ready ControlOutput.mode)
808
))
809

    
810
; Dynamics
811
(declare-var Dynamics.valve_state Int)
812
(declare-var Dynamics.level Int)
813
(declare-var Dynamics.steam Int)
814
(declare-var Dynamics.level_defect Int)
815
(declare-var Dynamics.steam_defect Int)
816
(declare-var Dynamics.flow_0 Bool)
817
(declare-var Dynamics.flow_1 Bool)
818
(declare-var Dynamics.flow_2 Bool)
819
(declare-var Dynamics.flow_3 Bool)
820
(declare-var Dynamics.q Int)
821
(declare-var Dynamics.v Int)
822
(declare-var Dynamics.p_0 Int)
823
(declare-var Dynamics.p_1 Int)
824
(declare-var Dynamics.p_2 Int)
825
(declare-var Dynamics.p_3 Int)
826
(declare-var Dynamics.__Dynamics_8_c Int)
827
(declare-var Dynamics.ni_26._arrow._first_c Bool)
828
(declare-var Dynamics.__Dynamics_8_m Int)
829
(declare-var Dynamics.ni_26._arrow._first_m Bool)
830
(declare-var Dynamics.__Dynamics_8_x Int)
831
(declare-var Dynamics.ni_26._arrow._first_x Bool)
832
(declare-var Dynamics.__Dynamics_1 Bool)
833
(declare-var Dynamics.__Dynamics_10 Bool)
834
(declare-var Dynamics.__Dynamics_11 Int)
835
(declare-var Dynamics.__Dynamics_2 Bool)
836
(declare-var Dynamics.__Dynamics_3 Bool)
837
(declare-var Dynamics.__Dynamics_4 Bool)
838
(declare-var Dynamics.__Dynamics_5 Bool)
839
(declare-var Dynamics.__Dynamics_6 Bool)
840
(declare-var Dynamics.__Dynamics_7 Int)
841
(declare-var Dynamics.__Dynamics_9 Bool)
842
(declare-rel Dynamics_reset (Int Bool Int Bool))
843
(declare-rel Dynamics_step (Int Int Int Int Int Bool Bool Bool Bool Int Int Int Int Int Int Int Bool Int Bool))
844

    
845
(rule (=> 
846
  (and 
847
       (= Dynamics.__Dynamics_8_m Dynamics.__Dynamics_8_c)
848
       (= Dynamics.ni_26._arrow._first_m true)
849
  )
850
  (Dynamics_reset Dynamics.__Dynamics_8_c
851
                  Dynamics.ni_26._arrow._first_c
852
                  Dynamics.__Dynamics_8_m
853
                  Dynamics.ni_26._arrow._first_m)
854
))
855

    
856
(rule (=> 
857
  (and (= Dynamics.__Dynamics_2 (not Dynamics.flow_3))
858
       (= Dynamics.ni_26._arrow._first_m Dynamics.ni_26._arrow._first_c)
859
       (and (= Dynamics.__Dynamics_1 (ite Dynamics.ni_26._arrow._first_m true false))
860
            (= Dynamics.ni_26._arrow._first_x false))
861
       (and (or (not (= Dynamics.__Dynamics_1 true))
862
               (= Dynamics.p_3 0))
863
            (or (not (= Dynamics.__Dynamics_1 false))
864
               (and (or (not (= Dynamics.__Dynamics_2 true))
865
                       (= Dynamics.p_3 0))
866
                    (or (not (= Dynamics.__Dynamics_2 false))
867
                       (= Dynamics.p_3 15))
868
               ))
869
       )
870
       (= Dynamics.__Dynamics_3 (not Dynamics.flow_2))
871
       (and (or (not (= Dynamics.__Dynamics_1 true))
872
               (= Dynamics.p_2 0))
873
            (or (not (= Dynamics.__Dynamics_1 false))
874
               (and (or (not (= Dynamics.__Dynamics_3 true))
875
                       (= Dynamics.p_2 0))
876
                    (or (not (= Dynamics.__Dynamics_3 false))
877
                       (= Dynamics.p_2 15))
878
               ))
879
       )
880
       (= Dynamics.__Dynamics_4 (not Dynamics.flow_1))
881
       (and (or (not (= Dynamics.__Dynamics_1 true))
882
               (= Dynamics.p_1 0))
883
            (or (not (= Dynamics.__Dynamics_1 false))
884
               (and (or (not (= Dynamics.__Dynamics_4 true))
885
                       (= Dynamics.p_1 0))
886
                    (or (not (= Dynamics.__Dynamics_4 false))
887
                       (= Dynamics.p_1 15))
888
               ))
889
       )
890
       (= Dynamics.__Dynamics_5 (not Dynamics.flow_0))
891
       (and (or (not (= Dynamics.__Dynamics_1 true))
892
               (= Dynamics.p_0 0))
893
            (or (not (= Dynamics.__Dynamics_1 false))
894
               (and (or (not (= Dynamics.__Dynamics_5 true))
895
                       (= Dynamics.p_0 0))
896
                    (or (not (= Dynamics.__Dynamics_5 false))
897
                       (= Dynamics.p_0 15))
898
               ))
899
       )
900
       (level_failure Dynamics.level_defect
901
                      Dynamics.__Dynamics_9)
902
       (sum Dynamics.p_0
903
            Dynamics.p_1
904
            Dynamics.p_2
905
            Dynamics.p_3
906
            Dynamics.__Dynamics_7)
907
       (= Dynamics.__Dynamics_10 (= Dynamics.valve_state 1))
908
       (and (or (not (= Dynamics.__Dynamics_10 true))
909
               (= Dynamics.__Dynamics_11 (* 10 5)))
910
            (or (not (= Dynamics.__Dynamics_10 false))
911
               (= Dynamics.__Dynamics_11 0))
912
       )
913
       (and (or (not (= Dynamics.__Dynamics_1 true))
914
               (= Dynamics.q Dynamics.level))
915
            (or (not (= Dynamics.__Dynamics_1 false))
916
               (and (or (not (= Dynamics.__Dynamics_9 true))
917
                       (= Dynamics.q (- (+ (- Dynamics.__Dynamics_8_c (* Dynamics.steam 5)) (* Dynamics.__Dynamics_7 5)) Dynamics.__Dynamics_11)))
918
                    (or (not (= Dynamics.__Dynamics_9 false))
919
                       (= Dynamics.q Dynamics.level))
920
               ))
921
       )
922
       (steam_failure Dynamics.steam_defect
923
                      Dynamics.__Dynamics_6)
924
       (and (or (not (= Dynamics.__Dynamics_1 true))
925
               (= Dynamics.v Dynamics.steam))
926
            (or (not (= Dynamics.__Dynamics_1 false))
927
               (and (or (not (= Dynamics.__Dynamics_6 true))
928
                       (= Dynamics.v (+ (div (- Dynamics.__Dynamics_8_c Dynamics.q) 5) (* Dynamics.__Dynamics_7 5))))
929
                    (or (not (= Dynamics.__Dynamics_6 false))
930
                       (= Dynamics.v Dynamics.steam))
931
               ))
932
       )
933
       (= Dynamics.__Dynamics_8_x Dynamics.q)
934
       )
935
  (Dynamics_step Dynamics.valve_state
936
                 Dynamics.level
937
                 Dynamics.steam
938
                 Dynamics.level_defect
939
                 Dynamics.steam_defect
940
                 Dynamics.flow_0
941
                 Dynamics.flow_1
942
                 Dynamics.flow_2
943
                 Dynamics.flow_3
944
                 Dynamics.q
945
                 Dynamics.v
946
                 Dynamics.p_0
947
                 Dynamics.p_1
948
                 Dynamics.p_2
949
                 Dynamics.p_3
950
                 Dynamics.__Dynamics_8_c
951
                 Dynamics.ni_26._arrow._first_c
952
                 Dynamics.__Dynamics_8_x
953
                 Dynamics.ni_26._arrow._first_x)
954
))
955

    
956
; LevelDefect
957
(declare-var LevelDefect.level_failure_acknowledgement Bool)
958
(declare-var LevelDefect.level_repaired Bool)
959
(declare-var LevelDefect.level Int)
960
(declare-var LevelDefect.LevelDefect Int)
961
(declare-var LevelDefect.__LevelDefect_3_c Int)
962
(declare-var LevelDefect.ni_25._arrow._first_c Bool)
963
(declare-var LevelDefect.__LevelDefect_3_m Int)
964
(declare-var LevelDefect.ni_25._arrow._first_m Bool)
965
(declare-var LevelDefect.__LevelDefect_3_x Int)
966
(declare-var LevelDefect.ni_25._arrow._first_x Bool)
967
(declare-var LevelDefect.__LevelDefect_1 Bool)
968
(declare-var LevelDefect.__LevelDefect_2 Bool)
969
(declare-var LevelDefect.__LevelDefect_4 Int)
970
(declare-rel LevelDefect_reset (Int Bool Int Bool))
971
(declare-rel LevelDefect_step (Bool Bool Int Int Int Bool Int Bool))
972

    
973
(rule (=> 
974
  (and 
975
       (= LevelDefect.__LevelDefect_3_m LevelDefect.__LevelDefect_3_c)
976
       (= LevelDefect.ni_25._arrow._first_m true)
977
  )
978
  (LevelDefect_reset LevelDefect.__LevelDefect_3_c
979
                     LevelDefect.ni_25._arrow._first_c
980
                     LevelDefect.__LevelDefect_3_m
981
                     LevelDefect.ni_25._arrow._first_m)
982
))
983

    
984
(rule (=> 
985
  (and (level_failure_detect LevelDefect.level
986
                             LevelDefect.__LevelDefect_2)
987
       (Defect LevelDefect.__LevelDefect_3_c
988
               LevelDefect.__LevelDefect_2
989
               LevelDefect.level_failure_acknowledgement
990
               LevelDefect.level_repaired
991
               LevelDefect.__LevelDefect_4)
992
       (= LevelDefect.ni_25._arrow._first_m LevelDefect.ni_25._arrow._first_c)
993
       (and (= LevelDefect.__LevelDefect_1 (ite LevelDefect.ni_25._arrow._first_m true false))
994
            (= LevelDefect.ni_25._arrow._first_x false))
995
       (and (or (not (= LevelDefect.__LevelDefect_1 true))
996
               (= LevelDefect.LevelDefect 0))
997
            (or (not (= LevelDefect.__LevelDefect_1 false))
998
               (= LevelDefect.LevelDefect LevelDefect.__LevelDefect_4))
999
       )
1000
       (= LevelDefect.__LevelDefect_3_x LevelDefect.LevelDefect)
1001
       )
1002
  (LevelDefect_step LevelDefect.level_failure_acknowledgement
1003
                    LevelDefect.level_repaired
1004
                    LevelDefect.level
1005
                    LevelDefect.LevelDefect
1006
                    LevelDefect.__LevelDefect_3_c
1007
                    LevelDefect.ni_25._arrow._first_c
1008
                    LevelDefect.__LevelDefect_3_x
1009
                    LevelDefect.ni_25._arrow._first_x)
1010
))
1011

    
1012
; LevelOutput
1013
(declare-var LevelOutput.op_mode Int)
1014
(declare-var LevelOutput.level_defect Int)
1015
(declare-var LevelOutput.level_repaired Bool)
1016
(declare-var LevelOutput.level_outcome_failure_detection Bool)
1017
(declare-var LevelOutput.level_outcome_repaired_acknowledgement Bool)
1018
(declare-rel LevelOutput (Int Int Bool Bool Bool))
1019
(rule (=> 
1020
  (and (= LevelOutput.level_outcome_repaired_acknowledgement (and (not (or (= LevelOutput.op_mode 6) (= LevelOutput.op_mode 1))) LevelOutput.level_repaired))
1021
       (= LevelOutput.level_outcome_failure_detection (and (not (or (= LevelOutput.op_mode 6) (= LevelOutput.op_mode 1))) (= LevelOutput.level_defect 1)))
1022
       )
1023
  (LevelOutput LevelOutput.op_mode LevelOutput.level_defect LevelOutput.level_repaired LevelOutput.level_outcome_failure_detection LevelOutput.level_outcome_repaired_acknowledgement)
1024
))
1025

    
1026
; Operator
1027
(declare-var Operator.stop Bool)
1028
(declare-var Operator.stop_request Bool)
1029
(declare-var Operator.__Operator_2_c Int)
1030
(declare-var Operator.ni_24._arrow._first_c Bool)
1031
(declare-var Operator.__Operator_2_m Int)
1032
(declare-var Operator.ni_24._arrow._first_m Bool)
1033
(declare-var Operator.__Operator_2_x Int)
1034
(declare-var Operator.ni_24._arrow._first_x Bool)
1035
(declare-var Operator.__Operator_1 Bool)
1036
(declare-var Operator.nb_stops Int)
1037
(declare-rel Operator_reset (Int Bool Int Bool))
1038
(declare-rel Operator_step (Bool Bool Int Bool Int Bool))
1039

    
1040
(rule (=> 
1041
  (and 
1042
       (= Operator.__Operator_2_m Operator.__Operator_2_c)
1043
       (= Operator.ni_24._arrow._first_m true)
1044
  )
1045
  (Operator_reset Operator.__Operator_2_c
1046
                  Operator.ni_24._arrow._first_c
1047
                  Operator.__Operator_2_m
1048
                  Operator.ni_24._arrow._first_m)
1049
))
1050

    
1051
(rule (=> 
1052
  (and (= Operator.ni_24._arrow._first_m Operator.ni_24._arrow._first_c)
1053
       (and (= Operator.__Operator_1 (ite Operator.ni_24._arrow._first_m true false))
1054
            (= Operator.ni_24._arrow._first_x false))
1055
       (and (or (not (= Operator.__Operator_1 true))
1056
               (and (or (not (= Operator.stop true))
1057
                       (= Operator.nb_stops 1))
1058
                    (or (not (= Operator.stop false))
1059
                       (= Operator.nb_stops 0))
1060
               ))
1061
            (or (not (= Operator.__Operator_1 false))
1062
               (and (or (not (= Operator.stop true))
1063
                       (= Operator.nb_stops (+ Operator.__Operator_2_c 1)))
1064
                    (or (not (= Operator.stop false))
1065
                       (= Operator.nb_stops 0))
1066
               ))
1067
       )
1068
       (= Operator.stop_request (>= Operator.nb_stops 3))
1069
       (= Operator.__Operator_2_x Operator.nb_stops)
1070
       )
1071
  (Operator_step Operator.stop
1072
                 Operator.stop_request
1073
                 Operator.__Operator_2_c
1074
                 Operator.ni_24._arrow._first_c
1075
                 Operator.__Operator_2_x
1076
                 Operator.ni_24._arrow._first_x)
1077
))
1078

    
1079
; PumpDefect
1080
(declare-var PumpDefect.pump_failure_acknowledgement Bool)
1081
(declare-var PumpDefect.pump_repaired Bool)
1082
(declare-var PumpDefect.pump_control_failure_acknowledgement Bool)
1083
(declare-var PumpDefect.pump_control_repaired Bool)
1084
(declare-var PumpDefect.pump_status Int)
1085
(declare-var PumpDefect.pump_state Int)
1086
(declare-var PumpDefect.pump_control_state Bool)
1087
(declare-var PumpDefect.PumpDefect Int)
1088
(declare-var PumpDefect.PumpControlDefect Int)
1089
(declare-var PumpDefect.Flow Bool)
1090
(declare-var PumpDefect.__PumpDefect_2_c Int)
1091
(declare-var PumpDefect.__PumpDefect_4_c Int)
1092
(declare-var PumpDefect.ni_23._arrow._first_c Bool)
1093
(declare-var PumpDefect.__PumpDefect_2_m Int)
1094
(declare-var PumpDefect.__PumpDefect_4_m Int)
1095
(declare-var PumpDefect.ni_23._arrow._first_m Bool)
1096
(declare-var PumpDefect.__PumpDefect_2_x Int)
1097
(declare-var PumpDefect.__PumpDefect_4_x Int)
1098
(declare-var PumpDefect.ni_23._arrow._first_x Bool)
1099
(declare-var PumpDefect.__PumpDefect_1 Bool)
1100
(declare-var PumpDefect.__PumpDefect_3 Int)
1101
(declare-var PumpDefect.__PumpDefect_5 Int)
1102
(declare-var PumpDefect.pump_control_failure_d Bool)
1103
(declare-var PumpDefect.pump_failure_d Bool)
1104
(declare-rel PumpDefect_reset (Int Int Bool Int Int Bool))
1105
(declare-rel PumpDefect_step (Bool Bool Bool Bool Int Int Bool Int Int Bool Int Int Bool Int Int Bool))
1106

    
1107
(rule (=> 
1108
  (and 
1109
       (= PumpDefect.__PumpDefect_2_m PumpDefect.__PumpDefect_2_c)
1110
       (= PumpDefect.__PumpDefect_4_m PumpDefect.__PumpDefect_4_c)
1111
       (= PumpDefect.ni_23._arrow._first_m true)
1112
  )
1113
  (PumpDefect_reset PumpDefect.__PumpDefect_2_c
1114
                    PumpDefect.__PumpDefect_4_c
1115
                    PumpDefect.ni_23._arrow._first_c
1116
                    PumpDefect.__PumpDefect_2_m
1117
                    PumpDefect.__PumpDefect_4_m
1118
                    PumpDefect.ni_23._arrow._first_m)
1119
))
1120

    
1121
(rule (=> 
1122
  (and (pump_failure_detect PumpDefect.pump_status
1123
                            PumpDefect.pump_state
1124
                            PumpDefect.pump_control_state
1125
                            PumpDefect.pump_failure_d
1126
                            PumpDefect.pump_control_failure_d
1127
                            PumpDefect.Flow)
1128
       (Defect PumpDefect.__PumpDefect_4_c
1129
               PumpDefect.pump_failure_d
1130
               PumpDefect.pump_failure_acknowledgement
1131
               PumpDefect.pump_repaired
1132
               PumpDefect.__PumpDefect_5)
1133
       (= PumpDefect.ni_23._arrow._first_m PumpDefect.ni_23._arrow._first_c)
1134
       (and (= PumpDefect.__PumpDefect_1 (ite PumpDefect.ni_23._arrow._first_m true false))
1135
            (= PumpDefect.ni_23._arrow._first_x false))
1136
       (and (or (not (= PumpDefect.__PumpDefect_1 true))
1137
               (= PumpDefect.PumpDefect 0))
1138
            (or (not (= PumpDefect.__PumpDefect_1 false))
1139
               (= PumpDefect.PumpDefect PumpDefect.__PumpDefect_5))
1140
       )
1141
       (= PumpDefect.__PumpDefect_4_x PumpDefect.PumpDefect)
1142
       (Defect PumpDefect.__PumpDefect_2_c
1143
               PumpDefect.pump_control_failure_d
1144
               PumpDefect.pump_control_failure_acknowledgement
1145
               PumpDefect.pump_control_repaired
1146
               PumpDefect.__PumpDefect_3)
1147
       (and (or (not (= PumpDefect.__PumpDefect_1 true))
1148
               (= PumpDefect.PumpControlDefect 0))
1149
            (or (not (= PumpDefect.__PumpDefect_1 false))
1150
               (= PumpDefect.PumpControlDefect PumpDefect.__PumpDefect_3))
1151
       )
1152
       (= PumpDefect.__PumpDefect_2_x PumpDefect.PumpControlDefect)
1153
       )
1154
  (PumpDefect_step PumpDefect.pump_failure_acknowledgement
1155
                   PumpDefect.pump_repaired
1156
                   PumpDefect.pump_control_failure_acknowledgement
1157
                   PumpDefect.pump_control_repaired
1158
                   PumpDefect.pump_status
1159
                   PumpDefect.pump_state
1160
                   PumpDefect.pump_control_state
1161
                   PumpDefect.PumpDefect
1162
                   PumpDefect.PumpControlDefect
1163
                   PumpDefect.Flow
1164
                   PumpDefect.__PumpDefect_2_c
1165
                   PumpDefect.__PumpDefect_4_c
1166
                   PumpDefect.ni_23._arrow._first_c
1167
                   PumpDefect.__PumpDefect_2_x
1168
                   PumpDefect.__PumpDefect_4_x
1169
                   PumpDefect.ni_23._arrow._first_x)
1170
))
1171

    
1172
; PumpsDecision
1173
(declare-var PumpsDecision.q Int)
1174
(declare-var PumpsDecision.v Int)
1175
(declare-var PumpsDecision.n_pumps Int)
1176
(declare-var PumpsDecision.__PumpsDecision_3_c Int)
1177
(declare-var PumpsDecision.__PumpsDecision_3_m Int)
1178
(declare-var PumpsDecision.__PumpsDecision_3_x Int)
1179
(declare-var PumpsDecision.__PumpsDecision_1 Bool)
1180
(declare-var PumpsDecision.__PumpsDecision_2 Bool)
1181
(declare-rel PumpsDecision_reset (Int Int))
1182
(declare-rel PumpsDecision_step (Int Int Int Int Int))
1183

    
1184
(rule (=> 
1185
  (and 
1186
       (= PumpsDecision.__PumpsDecision_3_m PumpsDecision.__PumpsDecision_3_c)
1187
       
1188
  )
1189
  (PumpsDecision_reset PumpsDecision.__PumpsDecision_3_c
1190
                       PumpsDecision.__PumpsDecision_3_m)
1191
))
1192

    
1193
(rule (=> 
1194
  (and (= PumpsDecision.__PumpsDecision_2 (< PumpsDecision.q 400))
1195
       (= PumpsDecision.__PumpsDecision_1 (> PumpsDecision.q 600))
1196
       (and (or (not (= PumpsDecision.__PumpsDecision_1 true))
1197
               (= PumpsDecision.n_pumps (div PumpsDecision.v 15)))
1198
            (or (not (= PumpsDecision.__PumpsDecision_1 false))
1199
               (and (or (not (= PumpsDecision.__PumpsDecision_2 true))
1200
                       (= PumpsDecision.n_pumps (+ (div PumpsDecision.v 15) 1)))
1201
                    (or (not (= PumpsDecision.__PumpsDecision_2 false))
1202
                       (= PumpsDecision.n_pumps PumpsDecision.__PumpsDecision_3_c))
1203
               ))
1204
       )
1205
       (= PumpsDecision.__PumpsDecision_3_x PumpsDecision.n_pumps)
1206
       )
1207
  (PumpsDecision_step PumpsDecision.q
1208
                      PumpsDecision.v
1209
                      PumpsDecision.n_pumps
1210
                      PumpsDecision.__PumpsDecision_3_c
1211
                      PumpsDecision.__PumpsDecision_3_x)
1212
))
1213

    
1214
; PumpsOutput
1215
(declare-var PumpsOutput.op_mode Int)
1216
(declare-var PumpsOutput.pump_status_0 Int)
1217
(declare-var PumpsOutput.pump_status_1 Int)
1218
(declare-var PumpsOutput.pump_status_2 Int)
1219
(declare-var PumpsOutput.pump_status_3 Int)
1220
(declare-var PumpsOutput.pump_defect_0 Int)
1221
(declare-var PumpsOutput.pump_defect_1 Int)
1222
(declare-var PumpsOutput.pump_defect_2 Int)
1223
(declare-var PumpsOutput.pump_defect_3 Int)
1224
(declare-var PumpsOutput.pump_control_defect_0 Int)
1225
(declare-var PumpsOutput.pump_control_defect_1 Int)
1226
(declare-var PumpsOutput.pump_control_defect_2 Int)
1227
(declare-var PumpsOutput.pump_control_defect_3 Int)
1228
(declare-var PumpsOutput.pump_repaired_0 Bool)
1229
(declare-var PumpsOutput.pump_repaired_1 Bool)
1230
(declare-var PumpsOutput.pump_repaired_2 Bool)
1231
(declare-var PumpsOutput.pump_repaired_3 Bool)
1232
(declare-var PumpsOutput.pump_control_repaired_0 Bool)
1233
(declare-var PumpsOutput.pump_control_repaired_1 Bool)
1234
(declare-var PumpsOutput.pump_control_repaired_2 Bool)
1235
(declare-var PumpsOutput.pump_control_repaired_3 Bool)
1236
(declare-var PumpsOutput.open_pump_0 Bool)
1237
(declare-var PumpsOutput.open_pump_1 Bool)
1238
(declare-var PumpsOutput.open_pump_2 Bool)
1239
(declare-var PumpsOutput.open_pump_3 Bool)
1240
(declare-var PumpsOutput.close_pump_0 Bool)
1241
(declare-var PumpsOutput.close_pump_1 Bool)
1242
(declare-var PumpsOutput.close_pump_2 Bool)
1243
(declare-var PumpsOutput.close_pump_3 Bool)
1244
(declare-var PumpsOutput.pump_failure_detection_0 Bool)
1245
(declare-var PumpsOutput.pump_failure_detection_1 Bool)
1246
(declare-var PumpsOutput.pump_failure_detection_2 Bool)
1247
(declare-var PumpsOutput.pump_failure_detection_3 Bool)
1248
(declare-var PumpsOutput.pump_repaired_acknowledgement_0 Bool)
1249
(declare-var PumpsOutput.pump_repaired_acknowledgement_1 Bool)
1250
(declare-var PumpsOutput.pump_repaired_acknowledgement_2 Bool)
1251
(declare-var PumpsOutput.pump_repaired_acknowledgement_3 Bool)
1252
(declare-var PumpsOutput.pump_control_failure_detection_0 Bool)
1253
(declare-var PumpsOutput.pump_control_failure_detection_1 Bool)
1254
(declare-var PumpsOutput.pump_control_failure_detection_2 Bool)
1255
(declare-var PumpsOutput.pump_control_failure_detection_3 Bool)
1256
(declare-var PumpsOutput.pump_control_repaired_acknowledgement_0 Bool)
1257
(declare-var PumpsOutput.pump_control_repaired_acknowledgement_1 Bool)
1258
(declare-var PumpsOutput.pump_control_repaired_acknowledgement_2 Bool)
1259
(declare-var PumpsOutput.pump_control_repaired_acknowledgement_3 Bool)
1260
(declare-var PumpsOutput.__PumpsOutput_1_c Int)
1261
(declare-var PumpsOutput.__PumpsOutput_2_c Int)
1262
(declare-var PumpsOutput.__PumpsOutput_3_c Int)
1263
(declare-var PumpsOutput.__PumpsOutput_4_c Int)
1264
(declare-var PumpsOutput.__PumpsOutput_5_c Int)
1265
(declare-var PumpsOutput.__PumpsOutput_6_c Int)
1266
(declare-var PumpsOutput.__PumpsOutput_7_c Int)
1267
(declare-var PumpsOutput.__PumpsOutput_8_c Int)
1268
(declare-var PumpsOutput.__PumpsOutput_1_m Int)
1269
(declare-var PumpsOutput.__PumpsOutput_2_m Int)
1270
(declare-var PumpsOutput.__PumpsOutput_3_m Int)
1271
(declare-var PumpsOutput.__PumpsOutput_4_m Int)
1272
(declare-var PumpsOutput.__PumpsOutput_5_m Int)
1273
(declare-var PumpsOutput.__PumpsOutput_6_m Int)
1274
(declare-var PumpsOutput.__PumpsOutput_7_m Int)
1275
(declare-var PumpsOutput.__PumpsOutput_8_m Int)
1276
(declare-var PumpsOutput.__PumpsOutput_1_x Int)
1277
(declare-var PumpsOutput.__PumpsOutput_2_x Int)
1278
(declare-var PumpsOutput.__PumpsOutput_3_x Int)
1279
(declare-var PumpsOutput.__PumpsOutput_4_x Int)
1280
(declare-var PumpsOutput.__PumpsOutput_5_x Int)
1281
(declare-var PumpsOutput.__PumpsOutput_6_x Int)
1282
(declare-var PumpsOutput.__PumpsOutput_7_x Int)
1283
(declare-var PumpsOutput.__PumpsOutput_8_x Int)
1284
(declare-rel PumpsOutput_reset (Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int))
1285
(declare-rel PumpsOutput_step (Int Int Int Int Int Int Int Int Int Int Int Int Int Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int))
1286

    
1287
(rule (=> 
1288
  (and 
1289
       (= PumpsOutput.__PumpsOutput_1_m PumpsOutput.__PumpsOutput_1_c)
1290
       (= PumpsOutput.__PumpsOutput_2_m PumpsOutput.__PumpsOutput_2_c)
1291
       (= PumpsOutput.__PumpsOutput_3_m PumpsOutput.__PumpsOutput_3_c)
1292
       (= PumpsOutput.__PumpsOutput_4_m PumpsOutput.__PumpsOutput_4_c)
1293
       (= PumpsOutput.__PumpsOutput_5_m PumpsOutput.__PumpsOutput_5_c)
1294
       (= PumpsOutput.__PumpsOutput_6_m PumpsOutput.__PumpsOutput_6_c)
1295
       (= PumpsOutput.__PumpsOutput_7_m PumpsOutput.__PumpsOutput_7_c)
1296
       (= PumpsOutput.__PumpsOutput_8_m PumpsOutput.__PumpsOutput_8_c)
1297
       
1298
  )
1299
  (PumpsOutput_reset PumpsOutput.__PumpsOutput_1_c
1300
                     PumpsOutput.__PumpsOutput_2_c
1301
                     PumpsOutput.__PumpsOutput_3_c
1302
                     PumpsOutput.__PumpsOutput_4_c
1303
                     PumpsOutput.__PumpsOutput_5_c
1304
                     PumpsOutput.__PumpsOutput_6_c
1305
                     PumpsOutput.__PumpsOutput_7_c
1306
                     PumpsOutput.__PumpsOutput_8_c
1307
                     PumpsOutput.__PumpsOutput_1_m
1308
                     PumpsOutput.__PumpsOutput_2_m
1309
                     PumpsOutput.__PumpsOutput_3_m
1310
                     PumpsOutput.__PumpsOutput_4_m
1311
                     PumpsOutput.__PumpsOutput_5_m
1312
                     PumpsOutput.__PumpsOutput_6_m
1313
                     PumpsOutput.__PumpsOutput_7_m
1314
                     PumpsOutput.__PumpsOutput_8_m)
1315
))
1316

    
1317
(rule (=> 
1318
  (and (= PumpsOutput.pump_repaired_acknowledgement_3 (and (and (not (= PumpsOutput.op_mode 6)) (not (= PumpsOutput.op_mode 1))) PumpsOutput.pump_repaired_3))
1319
       (= PumpsOutput.pump_repaired_acknowledgement_2 (and (and (not (= PumpsOutput.op_mode 6)) (not (= PumpsOutput.op_mode 1))) PumpsOutput.pump_repaired_2))
1320
       (= PumpsOutput.pump_repaired_acknowledgement_1 (and (and (not (= PumpsOutput.op_mode 6)) (not (= PumpsOutput.op_mode 1))) PumpsOutput.pump_repaired_1))
1321
       (= PumpsOutput.pump_repaired_acknowledgement_0 (and (and (not (= PumpsOutput.op_mode 6)) (not (= PumpsOutput.op_mode 1))) PumpsOutput.pump_repaired_0))
1322
       (= PumpsOutput.pump_failure_detection_3 (and (and (not (= PumpsOutput.op_mode 6)) (not (= PumpsOutput.op_mode 1))) (= PumpsOutput.pump_defect_3 1)))
1323
       (= PumpsOutput.pump_failure_detection_2 (and (and (not (= PumpsOutput.op_mode 6)) (not (= PumpsOutput.op_mode 1))) (= PumpsOutput.pump_defect_2 1)))
1324
       (= PumpsOutput.pump_failure_detection_1 (and (and (not (= PumpsOutput.op_mode 6)) (not (= PumpsOutput.op_mode 1))) (= PumpsOutput.pump_defect_1 1)))
1325
       (= PumpsOutput.pump_failure_detection_0 (and (and (not (= PumpsOutput.op_mode 6)) (not (= PumpsOutput.op_mode 1))) (= PumpsOutput.pump_defect_0 1)))
1326
       (= PumpsOutput.pump_control_repaired_acknowledgement_3 (and (and (not (= PumpsOutput.op_mode 6)) (not (= PumpsOutput.op_mode 1))) PumpsOutput.pump_control_repaired_3))
1327
       (= PumpsOutput.pump_control_repaired_acknowledgement_2 (and (and (not (= PumpsOutput.op_mode 6)) (not (= PumpsOutput.op_mode 1))) PumpsOutput.pump_control_repaired_2))
1328
       (= PumpsOutput.pump_control_repaired_acknowledgement_1 (and (and (not (= PumpsOutput.op_mode 6)) (not (= PumpsOutput.op_mode 1))) PumpsOutput.pump_control_repaired_1))
1329
       (= PumpsOutput.pump_control_repaired_acknowledgement_0 (and (and (not (= PumpsOutput.op_mode 6)) (not (= PumpsOutput.op_mode 1))) PumpsOutput.pump_control_repaired_0))
1330
       (= PumpsOutput.pump_control_failure_detection_3 (and (and (not (= PumpsOutput.op_mode 6)) (not (= PumpsOutput.op_mode 1))) (= PumpsOutput.pump_control_defect_3 1)))
1331
       (= PumpsOutput.pump_control_failure_detection_2 (and (and (not (= PumpsOutput.op_mode 6)) (not (= PumpsOutput.op_mode 1))) (= PumpsOutput.pump_control_defect_2 1)))
1332
       (= PumpsOutput.pump_control_failure_detection_1 (and (and (not (= PumpsOutput.op_mode 6)) (not (= PumpsOutput.op_mode 1))) (= PumpsOutput.pump_control_defect_1 1)))
1333
       (= PumpsOutput.pump_control_failure_detection_0 (and (and (not (= PumpsOutput.op_mode 6)) (not (= PumpsOutput.op_mode 1))) (= PumpsOutput.pump_control_defect_0 1)))
1334
       (= PumpsOutput.open_pump_3 (and (and (not (= PumpsOutput.op_mode 6)) (not (= PumpsOutput.op_mode 1))) (= PumpsOutput.pump_status_3 2)))
1335
       (= PumpsOutput.open_pump_2 (and (and (not (= PumpsOutput.op_mode 6)) (not (= PumpsOutput.op_mode 1))) (= PumpsOutput.pump_status_2 2)))
1336
       (= PumpsOutput.open_pump_1 (and (and (not (= PumpsOutput.op_mode 6)) (not (= PumpsOutput.op_mode 1))) (= PumpsOutput.pump_status_1 2)))
1337
       (= PumpsOutput.open_pump_0 (and (and (not (= PumpsOutput.op_mode 6)) (not (= PumpsOutput.op_mode 1))) (= PumpsOutput.pump_status_0 2)))
1338
       (= PumpsOutput.close_pump_3 (and (and (and (and (and (not (= PumpsOutput.op_mode 6)) (not (= PumpsOutput.op_mode 1))) (= PumpsOutput.pump_status_0 0)) (not (= PumpsOutput.__PumpsOutput_2_c 0))) (= PumpsOutput.pump_defect_0 0)) (= PumpsOutput.__PumpsOutput_1_c 0)))
1339
       (= PumpsOutput.close_pump_2 (and (and (and (and (and (not (= PumpsOutput.op_mode 6)) (not (= PumpsOutput.op_mode 1))) (= PumpsOutput.pump_status_0 0)) (not (= PumpsOutput.__PumpsOutput_4_c 0))) (= PumpsOutput.pump_defect_0 0)) (= PumpsOutput.__PumpsOutput_3_c 0)))
1340
       (= PumpsOutput.close_pump_1 (and (and (and (and (and (not (= PumpsOutput.op_mode 6)) (not (= PumpsOutput.op_mode 1))) (= PumpsOutput.pump_status_0 0)) (not (= PumpsOutput.__PumpsOutput_6_c 0))) (= PumpsOutput.pump_defect_0 0)) (= PumpsOutput.__PumpsOutput_5_c 0)))
1341
       (= PumpsOutput.close_pump_0 (and (and (and (and (and (not (= PumpsOutput.op_mode 6)) (not (= PumpsOutput.op_mode 1))) (= PumpsOutput.pump_status_0 0)) (not (= PumpsOutput.__PumpsOutput_8_c 0))) (= PumpsOutput.pump_defect_0 0)) (= PumpsOutput.__PumpsOutput_7_c 0)))
1342
       (= PumpsOutput.__PumpsOutput_8_x PumpsOutput.pump_status_0)
1343
       (= PumpsOutput.__PumpsOutput_7_x PumpsOutput.pump_defect_0)
1344
       (= PumpsOutput.__PumpsOutput_6_x PumpsOutput.pump_status_1)
1345
       (= PumpsOutput.__PumpsOutput_5_x PumpsOutput.pump_defect_1)
1346
       (= PumpsOutput.__PumpsOutput_4_x PumpsOutput.pump_status_2)
1347
       (= PumpsOutput.__PumpsOutput_3_x PumpsOutput.pump_defect_2)
1348
       (= PumpsOutput.__PumpsOutput_2_x PumpsOutput.pump_status_3)
1349
       (= PumpsOutput.__PumpsOutput_1_x PumpsOutput.pump_defect_3)
1350
       )
1351
  (PumpsOutput_step PumpsOutput.op_mode
1352
                    PumpsOutput.pump_status_0
1353
                    PumpsOutput.pump_status_1
1354
                    PumpsOutput.pump_status_2
1355
                    PumpsOutput.pump_status_3
1356
                    PumpsOutput.pump_defect_0
1357
                    PumpsOutput.pump_defect_1
1358
                    PumpsOutput.pump_defect_2
1359
                    PumpsOutput.pump_defect_3
1360
                    PumpsOutput.pump_control_defect_0
1361
                    PumpsOutput.pump_control_defect_1
1362
                    PumpsOutput.pump_control_defect_2
1363
                    PumpsOutput.pump_control_defect_3
1364
                    PumpsOutput.pump_repaired_0
1365
                    PumpsOutput.pump_repaired_1
1366
                    PumpsOutput.pump_repaired_2
1367
                    PumpsOutput.pump_repaired_3
1368
                    PumpsOutput.pump_control_repaired_0
1369
                    PumpsOutput.pump_control_repaired_1
1370
                    PumpsOutput.pump_control_repaired_2
1371
                    PumpsOutput.pump_control_repaired_3
1372
                    PumpsOutput.open_pump_0
1373
                    PumpsOutput.open_pump_1
1374
                    PumpsOutput.open_pump_2
1375
                    PumpsOutput.open_pump_3
1376
                    PumpsOutput.close_pump_0
1377
                    PumpsOutput.close_pump_1
1378
                    PumpsOutput.close_pump_2
1379
                    PumpsOutput.close_pump_3
1380
                    PumpsOutput.pump_failure_detection_0
1381
                    PumpsOutput.pump_failure_detection_1
1382
                    PumpsOutput.pump_failure_detection_2
1383
                    PumpsOutput.pump_failure_detection_3
1384
                    PumpsOutput.pump_repaired_acknowledgement_0
1385
                    PumpsOutput.pump_repaired_acknowledgement_1
1386
                    PumpsOutput.pump_repaired_acknowledgement_2
1387
                    PumpsOutput.pump_repaired_acknowledgement_3
1388
                    PumpsOutput.pump_control_failure_detection_0
1389
                    PumpsOutput.pump_control_failure_detection_1
1390
                    PumpsOutput.pump_control_failure_detection_2
1391
                    PumpsOutput.pump_control_failure_detection_3
1392
                    PumpsOutput.pump_control_repaired_acknowledgement_0
1393
                    PumpsOutput.pump_control_repaired_acknowledgement_1
1394
                    PumpsOutput.pump_control_repaired_acknowledgement_2
1395
                    PumpsOutput.pump_control_repaired_acknowledgement_3
1396
                    PumpsOutput.__PumpsOutput_1_c
1397
                    PumpsOutput.__PumpsOutput_2_c
1398
                    PumpsOutput.__PumpsOutput_3_c
1399
                    PumpsOutput.__PumpsOutput_4_c
1400
                    PumpsOutput.__PumpsOutput_5_c
1401
                    PumpsOutput.__PumpsOutput_6_c
1402
                    PumpsOutput.__PumpsOutput_7_c
1403
                    PumpsOutput.__PumpsOutput_8_c
1404
                    PumpsOutput.__PumpsOutput_1_x
1405
                    PumpsOutput.__PumpsOutput_2_x
1406
                    PumpsOutput.__PumpsOutput_3_x
1407
                    PumpsOutput.__PumpsOutput_4_x
1408
                    PumpsOutput.__PumpsOutput_5_x
1409
                    PumpsOutput.__PumpsOutput_6_x
1410
                    PumpsOutput.__PumpsOutput_7_x
1411
                    PumpsOutput.__PumpsOutput_8_x)
1412
))
1413

    
1414
; PumpsStatus
1415
(declare-var PumpsStatus.n_pumps Int)
1416
(declare-var PumpsStatus.pump_defect_0 Int)
1417
(declare-var PumpsStatus.pump_defect_1 Int)
1418
(declare-var PumpsStatus.pump_defect_2 Int)
1419
(declare-var PumpsStatus.pump_defect_3 Int)
1420
(declare-var PumpsStatus.flow_0 Bool)
1421
(declare-var PumpsStatus.flow_1 Bool)
1422
(declare-var PumpsStatus.flow_2 Bool)
1423
(declare-var PumpsStatus.flow_3 Bool)
1424
(declare-var PumpsStatus.pump_status_0 Int)
1425
(declare-var PumpsStatus.pump_status_1 Int)
1426
(declare-var PumpsStatus.pump_status_2 Int)
1427
(declare-var PumpsStatus.pump_status_3 Int)
1428
(declare-var PumpsStatus.__PumpsStatus_1_c Int)
1429
(declare-var PumpsStatus.__PumpsStatus_2_c Int)
1430
(declare-var PumpsStatus.__PumpsStatus_3_c Int)
1431
(declare-var PumpsStatus.__PumpsStatus_4_c Int)
1432
(declare-var PumpsStatus.ni_21._arrow._first_c Bool)
1433
(declare-var PumpsStatus.ni_22.operate_pumps.__operate_pumps_12_c Int)
1434
(declare-var PumpsStatus.ni_22.operate_pumps.__operate_pumps_19_c Int)
1435
(declare-var PumpsStatus.ni_22.operate_pumps.__operate_pumps_26_c Int)
1436
(declare-var PumpsStatus.ni_22.operate_pumps.__operate_pumps_5_c Int)
1437
(declare-var PumpsStatus.__PumpsStatus_1_m Int)
1438
(declare-var PumpsStatus.__PumpsStatus_2_m Int)
1439
(declare-var PumpsStatus.__PumpsStatus_3_m Int)
1440
(declare-var PumpsStatus.__PumpsStatus_4_m Int)
1441
(declare-var PumpsStatus.ni_21._arrow._first_m Bool)
1442
(declare-var PumpsStatus.ni_22.operate_pumps.__operate_pumps_12_m Int)
1443
(declare-var PumpsStatus.ni_22.operate_pumps.__operate_pumps_19_m Int)
1444
(declare-var PumpsStatus.ni_22.operate_pumps.__operate_pumps_26_m Int)
1445
(declare-var PumpsStatus.ni_22.operate_pumps.__operate_pumps_5_m Int)
1446
(declare-var PumpsStatus.__PumpsStatus_1_x Int)
1447
(declare-var PumpsStatus.__PumpsStatus_2_x Int)
1448
(declare-var PumpsStatus.__PumpsStatus_3_x Int)
1449
(declare-var PumpsStatus.__PumpsStatus_4_x Int)
1450
(declare-var PumpsStatus.ni_21._arrow._first_x Bool)
1451
(declare-var PumpsStatus.ni_22.operate_pumps.__operate_pumps_12_x Int)
1452
(declare-var PumpsStatus.ni_22.operate_pumps.__operate_pumps_19_x Int)
1453
(declare-var PumpsStatus.ni_22.operate_pumps.__operate_pumps_26_x Int)
1454
(declare-var PumpsStatus.ni_22.operate_pumps.__operate_pumps_5_x Int)
1455
(declare-var PumpsStatus.__PumpsStatus_5 Bool)
1456
(declare-var PumpsStatus.__PumpsStatus_6 Int)
1457
(declare-var PumpsStatus.__PumpsStatus_7 Int)
1458
(declare-var PumpsStatus.__PumpsStatus_8 Int)
1459
(declare-var PumpsStatus.__PumpsStatus_9 Int)
1460
(declare-var PumpsStatus.n_pumps_flow Int)
1461
(declare-var PumpsStatus.n_pumps_to_open Int)
1462
(declare-var PumpsStatus.t0 Int)
1463
(declare-var PumpsStatus.t1 Int)
1464
(declare-var PumpsStatus.t2 Int)
1465
(declare-var PumpsStatus.t3 Int)
1466
(declare-rel PumpsStatus_reset (Int Int Int Int Bool Int Int Int Int Int Int Int Int Bool Int Int Int Int))
1467
(declare-rel PumpsStatus_step (Int Int Int Int Int Bool Bool Bool Bool Int Int Int Int Int Int Int Int Bool Int Int Int Int Int Int Int Int Bool Int Int Int Int))
1468

    
1469
(rule (=> 
1470
  (and 
1471
       (= PumpsStatus.__PumpsStatus_1_m PumpsStatus.__PumpsStatus_1_c)
1472
       (= PumpsStatus.__PumpsStatus_2_m PumpsStatus.__PumpsStatus_2_c)
1473
       (= PumpsStatus.__PumpsStatus_3_m PumpsStatus.__PumpsStatus_3_c)
1474
       (= PumpsStatus.__PumpsStatus_4_m PumpsStatus.__PumpsStatus_4_c)
1475
       (operate_pumps_reset PumpsStatus.ni_22.operate_pumps.__operate_pumps_12_c
1476
                            PumpsStatus.ni_22.operate_pumps.__operate_pumps_19_c
1477
                            PumpsStatus.ni_22.operate_pumps.__operate_pumps_26_c
1478
                            PumpsStatus.ni_22.operate_pumps.__operate_pumps_5_c
1479
                            PumpsStatus.ni_22.operate_pumps.__operate_pumps_12_m
1480
                            PumpsStatus.ni_22.operate_pumps.__operate_pumps_19_m
1481
                            PumpsStatus.ni_22.operate_pumps.__operate_pumps_26_m
1482
                            PumpsStatus.ni_22.operate_pumps.__operate_pumps_5_m)
1483
       (= PumpsStatus.ni_21._arrow._first_m true)
1484
  )
1485
  (PumpsStatus_reset PumpsStatus.__PumpsStatus_1_c
1486
                     PumpsStatus.__PumpsStatus_2_c
1487
                     PumpsStatus.__PumpsStatus_3_c
1488
                     PumpsStatus.__PumpsStatus_4_c
1489
                     PumpsStatus.ni_21._arrow._first_c
1490
                     PumpsStatus.ni_22.operate_pumps.__operate_pumps_12_c
1491
                     PumpsStatus.ni_22.operate_pumps.__operate_pumps_19_c
1492
                     PumpsStatus.ni_22.operate_pumps.__operate_pumps_26_c
1493
                     PumpsStatus.ni_22.operate_pumps.__operate_pumps_5_c
1494
                     PumpsStatus.__PumpsStatus_1_m
1495
                     PumpsStatus.__PumpsStatus_2_m
1496
                     PumpsStatus.__PumpsStatus_3_m
1497
                     PumpsStatus.__PumpsStatus_4_m
1498
                     PumpsStatus.ni_21._arrow._first_m
1499
                     PumpsStatus.ni_22.operate_pumps.__operate_pumps_12_m
1500
                     PumpsStatus.ni_22.operate_pumps.__operate_pumps_19_m
1501
                     PumpsStatus.ni_22.operate_pumps.__operate_pumps_26_m
1502
                     PumpsStatus.ni_22.operate_pumps.__operate_pumps_5_m)
1503
))
1504

    
1505
(rule (=> 
1506
  (and (and (or (not (= PumpsStatus.flow_0 true))
1507
               (= PumpsStatus.__PumpsStatus_9 1))
1508
            (or (not (= PumpsStatus.flow_0 false))
1509
               (= PumpsStatus.__PumpsStatus_9 0))
1510
       )
1511
       (and (or (not (= PumpsStatus.flow_1 true))
1512
               (= PumpsStatus.__PumpsStatus_8 1))
1513
            (or (not (= PumpsStatus.flow_1 false))
1514
               (= PumpsStatus.__PumpsStatus_8 0))
1515
       )
1516
       (and (or (not (= PumpsStatus.flow_2 true))
1517
               (= PumpsStatus.__PumpsStatus_7 1))
1518
            (or (not (= PumpsStatus.flow_2 false))
1519
               (= PumpsStatus.__PumpsStatus_7 0))
1520
       )
1521
       (and (or (not (= PumpsStatus.flow_3 true))
1522
               (= PumpsStatus.__PumpsStatus_6 1))
1523
            (or (not (= PumpsStatus.flow_3 false))
1524
               (= PumpsStatus.__PumpsStatus_6 0))
1525
       )
1526
       (= PumpsStatus.n_pumps_flow (+ (+ (+ PumpsStatus.__PumpsStatus_9 PumpsStatus.__PumpsStatus_8) PumpsStatus.__PumpsStatus_7) PumpsStatus.__PumpsStatus_6))
1527
       (= PumpsStatus.n_pumps_to_open (- PumpsStatus.n_pumps PumpsStatus.n_pumps_flow))
1528
       (and (= PumpsStatus.ni_22.operate_pumps.__operate_pumps_12_m PumpsStatus.ni_22.operate_pumps.__operate_pumps_12_c)
1529
            (= PumpsStatus.ni_22.operate_pumps.__operate_pumps_19_m PumpsStatus.ni_22.operate_pumps.__operate_pumps_19_c)
1530
            (= PumpsStatus.ni_22.operate_pumps.__operate_pumps_26_m PumpsStatus.ni_22.operate_pumps.__operate_pumps_26_c)
1531
            (= PumpsStatus.ni_22.operate_pumps.__operate_pumps_5_m PumpsStatus.ni_22.operate_pumps.__operate_pumps_5_c)
1532
            )
1533
       (operate_pumps_step 4
1534
                           PumpsStatus.n_pumps_to_open
1535
                           PumpsStatus.__PumpsStatus_4_c
1536
                           PumpsStatus.__PumpsStatus_3_c
1537
                           PumpsStatus.__PumpsStatus_2_c
1538
                           PumpsStatus.__PumpsStatus_1_c
1539
                           PumpsStatus.pump_defect_0
1540
                           PumpsStatus.pump_defect_1
1541
                           PumpsStatus.pump_defect_2
1542
                           PumpsStatus.pump_defect_3
1543
                           PumpsStatus.flow_0
1544
                           PumpsStatus.flow_1
1545
                           PumpsStatus.flow_2
1546
                           PumpsStatus.flow_3
1547
                           PumpsStatus.t0
1548
                           PumpsStatus.t1
1549
                           PumpsStatus.t2
1550
                           PumpsStatus.t3
1551
                           PumpsStatus.ni_22.operate_pumps.__operate_pumps_12_m
1552
                           PumpsStatus.ni_22.operate_pumps.__operate_pumps_19_m
1553
                           PumpsStatus.ni_22.operate_pumps.__operate_pumps_26_m
1554
                           PumpsStatus.ni_22.operate_pumps.__operate_pumps_5_m
1555
                           PumpsStatus.ni_22.operate_pumps.__operate_pumps_12_x
1556
                           PumpsStatus.ni_22.operate_pumps.__operate_pumps_19_x
1557
                           PumpsStatus.ni_22.operate_pumps.__operate_pumps_26_x
1558
                           PumpsStatus.ni_22.operate_pumps.__operate_pumps_5_x)
1559
       (= PumpsStatus.ni_21._arrow._first_m PumpsStatus.ni_21._arrow._first_c)
1560
       (and (= PumpsStatus.__PumpsStatus_5 (ite PumpsStatus.ni_21._arrow._first_m true false))
1561
            (= PumpsStatus.ni_21._arrow._first_x false))
1562
       (and (or (not (= PumpsStatus.__PumpsStatus_5 false))
1563
               (and (= PumpsStatus.pump_status_3 PumpsStatus.t3)
1564
                    (= PumpsStatus.pump_status_2 PumpsStatus.t2)
1565
                    (= PumpsStatus.pump_status_1 PumpsStatus.t1)
1566
                    (= PumpsStatus.pump_status_0 PumpsStatus.t0)
1567
                    ))
1568
            (or (not (= PumpsStatus.__PumpsStatus_5 true))
1569
               (and (= PumpsStatus.pump_status_3 0)
1570
                    (= PumpsStatus.pump_status_2 0)
1571
                    (= PumpsStatus.pump_status_1 0)
1572
                    (= PumpsStatus.pump_status_0 0)
1573
                    ))
1574
       )
1575
       (= PumpsStatus.__PumpsStatus_4_x PumpsStatus.pump_status_0)
1576
       (= PumpsStatus.__PumpsStatus_3_x PumpsStatus.pump_status_1)
1577
       (= PumpsStatus.__PumpsStatus_2_x PumpsStatus.pump_status_2)
1578
       (= PumpsStatus.__PumpsStatus_1_x PumpsStatus.pump_status_3)
1579
       )
1580
  (PumpsStatus_step PumpsStatus.n_pumps
1581
                    PumpsStatus.pump_defect_0
1582
                    PumpsStatus.pump_defect_1
1583
                    PumpsStatus.pump_defect_2
1584
                    PumpsStatus.pump_defect_3
1585
                    PumpsStatus.flow_0
1586
                    PumpsStatus.flow_1
1587
                    PumpsStatus.flow_2
1588
                    PumpsStatus.flow_3
1589
                    PumpsStatus.pump_status_0
1590
                    PumpsStatus.pump_status_1
1591
                    PumpsStatus.pump_status_2
1592
                    PumpsStatus.pump_status_3
1593
                    PumpsStatus.__PumpsStatus_1_c
1594
                    PumpsStatus.__PumpsStatus_2_c
1595
                    PumpsStatus.__PumpsStatus_3_c
1596
                    PumpsStatus.__PumpsStatus_4_c
1597
                    PumpsStatus.ni_21._arrow._first_c
1598
                    PumpsStatus.ni_22.operate_pumps.__operate_pumps_12_c
1599
                    PumpsStatus.ni_22.operate_pumps.__operate_pumps_19_c
1600
                    PumpsStatus.ni_22.operate_pumps.__operate_pumps_26_c
1601
                    PumpsStatus.ni_22.operate_pumps.__operate_pumps_5_c
1602
                    PumpsStatus.__PumpsStatus_1_x
1603
                    PumpsStatus.__PumpsStatus_2_x
1604
                    PumpsStatus.__PumpsStatus_3_x
1605
                    PumpsStatus.__PumpsStatus_4_x
1606
                    PumpsStatus.ni_21._arrow._first_x
1607
                    PumpsStatus.ni_22.operate_pumps.__operate_pumps_12_x
1608
                    PumpsStatus.ni_22.operate_pumps.__operate_pumps_19_x
1609
                    PumpsStatus.ni_22.operate_pumps.__operate_pumps_26_x
1610
                    PumpsStatus.ni_22.operate_pumps.__operate_pumps_5_x)
1611
))
1612

    
1613
; SteamDefect
1614
(declare-var SteamDefect.steam_failure_acknowledgement Bool)
1615
(declare-var SteamDefect.steam_repaired Bool)
1616
(declare-var SteamDefect.steam Int)
1617
(declare-var SteamDefect.SteamDefect Int)
1618
(declare-var SteamDefect.__SteamDefect_3_c Int)
1619
(declare-var SteamDefect.ni_20._arrow._first_c Bool)
1620
(declare-var SteamDefect.__SteamDefect_3_m Int)
1621
(declare-var SteamDefect.ni_20._arrow._first_m Bool)
1622
(declare-var SteamDefect.__SteamDefect_3_x Int)
1623
(declare-var SteamDefect.ni_20._arrow._first_x Bool)
1624
(declare-var SteamDefect.__SteamDefect_1 Bool)
1625
(declare-var SteamDefect.__SteamDefect_2 Bool)
1626
(declare-var SteamDefect.__SteamDefect_4 Int)
1627
(declare-rel SteamDefect_reset (Int Bool Int Bool))
1628
(declare-rel SteamDefect_step (Bool Bool Int Int Int Bool Int Bool))
1629

    
1630
(rule (=> 
1631
  (and 
1632
       (= SteamDefect.__SteamDefect_3_m SteamDefect.__SteamDefect_3_c)
1633
       (= SteamDefect.ni_20._arrow._first_m true)
1634
  )
1635
  (SteamDefect_reset SteamDefect.__SteamDefect_3_c
1636
                     SteamDefect.ni_20._arrow._first_c
1637
                     SteamDefect.__SteamDefect_3_m
1638
                     SteamDefect.ni_20._arrow._first_m)
1639
))
1640

    
1641
(rule (=> 
1642
  (and (steam_failure_detect SteamDefect.steam
1643
                             SteamDefect.__SteamDefect_2)
1644
       (Defect SteamDefect.__SteamDefect_3_c
1645
               SteamDefect.__SteamDefect_2
1646
               SteamDefect.steam_failure_acknowledgement
1647
               SteamDefect.steam_repaired
1648
               SteamDefect.__SteamDefect_4)
1649
       (= SteamDefect.ni_20._arrow._first_m SteamDefect.ni_20._arrow._first_c)
1650
       (and (= SteamDefect.__SteamDefect_1 (ite SteamDefect.ni_20._arrow._first_m true false))
1651
            (= SteamDefect.ni_20._arrow._first_x false))
1652
       (and (or (not (= SteamDefect.__SteamDefect_1 true))
1653
               (= SteamDefect.SteamDefect 0))
1654
            (or (not (= SteamDefect.__SteamDefect_1 false))
1655
               (= SteamDefect.SteamDefect SteamDefect.__SteamDefect_4))
1656
       )
1657
       (= SteamDefect.__SteamDefect_3_x SteamDefect.SteamDefect)
1658
       )
1659
  (SteamDefect_step SteamDefect.steam_failure_acknowledgement
1660
                    SteamDefect.steam_repaired
1661
                    SteamDefect.steam
1662
                    SteamDefect.SteamDefect
1663
                    SteamDefect.__SteamDefect_3_c
1664
                    SteamDefect.ni_20._arrow._first_c
1665
                    SteamDefect.__SteamDefect_3_x
1666
                    SteamDefect.ni_20._arrow._first_x)
1667
))
1668

    
1669
; SteamOutput
1670
(declare-var SteamOutput.op_mode Int)
1671
(declare-var SteamOutput.steam_defect Int)
1672
(declare-var SteamOutput.steam_repaired Bool)
1673
(declare-var SteamOutput.steam_outcome_failure_detection Bool)
1674
(declare-var SteamOutput.steam_outcome_repaired_acknowledgement Bool)
1675
(declare-rel SteamOutput (Int Int Bool Bool Bool))
1676
(rule (=> 
1677
  (and (= SteamOutput.steam_outcome_repaired_acknowledgement (and (not (or (= SteamOutput.op_mode 6) (= SteamOutput.op_mode 1))) SteamOutput.steam_repaired))
1678
       (= SteamOutput.steam_outcome_failure_detection (and (not (or (= SteamOutput.op_mode 6) (= SteamOutput.op_mode 1))) (= SteamOutput.steam_defect 1)))
1679
       )
1680
  (SteamOutput SteamOutput.op_mode SteamOutput.steam_defect SteamOutput.steam_repaired SteamOutput.steam_outcome_failure_detection SteamOutput.steam_outcome_repaired_acknowledgement)
1681
))
1682

    
1683
; Valve
1684
(declare-var Valve.op_mode Int)
1685
(declare-var Valve.q Int)
1686
(declare-var Valve.valve Bool)
1687
(declare-var Valve.valve_state Int)
1688
(declare-var Valve.__Valve_2_c Int)
1689
(declare-var Valve.ni_19._arrow._first_c Bool)
1690
(declare-var Valve.__Valve_2_m Int)
1691
(declare-var Valve.ni_19._arrow._first_m Bool)
1692
(declare-var Valve.__Valve_2_x Int)
1693
(declare-var Valve.ni_19._arrow._first_x Bool)
1694
(declare-var Valve.__Valve_1 Bool)
1695
(declare-var Valve.__Valve_3 Bool)
1696
(declare-var Valve.__Valve_4 Bool)
1697
(declare-var Valve.__Valve_5 Bool)
1698
(declare-rel Valve_reset (Int Bool Int Bool))
1699
(declare-rel Valve_step (Int Int Bool Int Int Bool Int Bool))
1700

    
1701
(rule (=> 
1702
  (and 
1703
       (= Valve.__Valve_2_m Valve.__Valve_2_c)
1704
       (= Valve.ni_19._arrow._first_m true)
1705
  )
1706
  (Valve_reset Valve.__Valve_2_c
1707
               Valve.ni_19._arrow._first_c
1708
               Valve.__Valve_2_m
1709
               Valve.ni_19._arrow._first_m)
1710
))
1711

    
1712
(rule (=> 
1713
  (and (= Valve.__Valve_5 (<= Valve.q 600))
1714
       (= Valve.__Valve_4 (> Valve.q 600))
1715
       (= Valve.__Valve_3 (= Valve.op_mode 2))
1716
       (= Valve.ni_19._arrow._first_m Valve.ni_19._arrow._first_c)(and (= Valve.__Valve_1 (ite Valve.ni_19._arrow._first_m true false))
1717
                                                                    (= Valve.ni_19._arrow._first_x false))
1718
       (and (or (not (= Valve.__Valve_1 false))
1719
               (and (and (or (not (= Valve.__Valve_3 true))
1720
                            (and (or (not (= Valve.__Valve_4 true))
1721
                                    (= Valve.valve_state 1))
1722
                                 (or (not (= Valve.__Valve_4 false))
1723
                                    (and (or (not (= Valve.__Valve_5 true))
1724
                                            (= Valve.valve_state 0))
1725
                                         (or (not (= Valve.__Valve_5 false))
1726
                                            (= Valve.valve_state Valve.__Valve_2_c))
1727
                                    ))
1728
                            ))
1729
                         (or (not (= Valve.__Valve_3 false))
1730
                            (= Valve.valve_state Valve.__Valve_2_c))
1731
                    )
1732
                    (= Valve.valve (not (= Valve.valve_state Valve.__Valve_2_c)))
1733
                    ))
1734
            (or (not (= Valve.__Valve_1 true))
1735
               (and (= Valve.valve_state 0)
1736
                    (= Valve.valve false)
1737
                    ))
1738
       )
1739
       (= Valve.__Valve_2_x Valve.valve_state)
1740
       )
1741
  (Valve_step Valve.op_mode
1742
              Valve.q
1743
              Valve.valve
1744
              Valve.valve_state
1745
              Valve.__Valve_2_c
1746
              Valve.ni_19._arrow._first_c
1747
              Valve.__Valve_2_x
1748
              Valve.ni_19._arrow._first_x)
1749
))
1750

    
1751
; Verification
1752
(declare-var Verification.S1 Bool)
1753
(declare-var Verification.S2 Bool)
1754
(declare-var Verification.property_ok Bool)
1755
(declare-var Verification.ni_16.FEDGE2.ni_28.REDGE.__REDGE_2_c Bool)
1756
(declare-var Verification.ni_16.FEDGE2.ni_28.REDGE.ni_30._arrow._first_c Bool)
1757
(declare-var Verification.ni_17.REDGE.__REDGE_2_c Bool)
1758
(declare-var Verification.ni_17.REDGE.ni_30._arrow._first_c Bool)
1759
(declare-var Verification.ni_18.FEDGE1.__FEDGE1_2_c Bool)
1760
(declare-var Verification.ni_18.FEDGE1.ni_29._arrow._first_c Bool)
1761
(declare-var Verification.ni_16.FEDGE2.ni_28.REDGE.__REDGE_2_m Bool)
1762
(declare-var Verification.ni_16.FEDGE2.ni_28.REDGE.ni_30._arrow._first_m Bool)
1763
(declare-var Verification.ni_17.REDGE.__REDGE_2_m Bool)
1764
(declare-var Verification.ni_17.REDGE.ni_30._arrow._first_m Bool)
1765
(declare-var Verification.ni_18.FEDGE1.__FEDGE1_2_m Bool)
1766
(declare-var Verification.ni_18.FEDGE1.ni_29._arrow._first_m Bool)
1767
(declare-var Verification.ni_16.FEDGE2.ni_28.REDGE.__REDGE_2_x Bool)
1768
(declare-var Verification.ni_16.FEDGE2.ni_28.REDGE.ni_30._arrow._first_x Bool)
1769
(declare-var Verification.ni_17.REDGE.__REDGE_2_x Bool)
1770
(declare-var Verification.ni_17.REDGE.ni_30._arrow._first_x Bool)
1771
(declare-var Verification.ni_18.FEDGE1.__FEDGE1_2_x Bool)
1772
(declare-var Verification.ni_18.FEDGE1.ni_29._arrow._first_x Bool)
1773
(declare-var Verification.__Verification_1 Bool)
1774
(declare-var Verification.__Verification_2 Bool)
1775
(declare-var Verification.__Verification_3 Bool)
1776
(declare-var Verification.__Verification_4 Bool)
1777
(declare-var Verification.property1 Bool)
1778
(declare-var Verification.property2 Bool)
1779
(declare-rel Verification_reset (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool))
1780
(declare-rel Verification_step (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool))
1781

    
1782
(rule (=> 
1783
  (and 
1784
       
1785
       (FEDGE1_reset Verification.ni_18.FEDGE1.__FEDGE1_2_c
1786
                     Verification.ni_18.FEDGE1.ni_29._arrow._first_c
1787
                     Verification.ni_18.FEDGE1.__FEDGE1_2_m
1788
                     Verification.ni_18.FEDGE1.ni_29._arrow._first_m)
1789
       (REDGE_reset Verification.ni_17.REDGE.__REDGE_2_c
1790
                    Verification.ni_17.REDGE.ni_30._arrow._first_c
1791
                    Verification.ni_17.REDGE.__REDGE_2_m
1792
                    Verification.ni_17.REDGE.ni_30._arrow._first_m)
1793
       (FEDGE2_reset Verification.ni_16.FEDGE2.ni_28.REDGE.__REDGE_2_c
1794
                     Verification.ni_16.FEDGE2.ni_28.REDGE.ni_30._arrow._first_c
1795
                     Verification.ni_16.FEDGE2.ni_28.REDGE.__REDGE_2_m
1796
                     Verification.ni_16.FEDGE2.ni_28.REDGE.ni_30._arrow._first_m)
1797
  )
1798
  (Verification_reset Verification.ni_16.FEDGE2.ni_28.REDGE.__REDGE_2_c
1799
                      Verification.ni_16.FEDGE2.ni_28.REDGE.ni_30._arrow._first_c
1800
                      Verification.ni_17.REDGE.__REDGE_2_c
1801
                      Verification.ni_17.REDGE.ni_30._arrow._first_c
1802
                      Verification.ni_18.FEDGE1.__FEDGE1_2_c
1803
                      Verification.ni_18.FEDGE1.ni_29._arrow._first_c
1804
                      Verification.ni_16.FEDGE2.ni_28.REDGE.__REDGE_2_m
1805
                      Verification.ni_16.FEDGE2.ni_28.REDGE.ni_30._arrow._first_m
1806
                      Verification.ni_17.REDGE.__REDGE_2_m
1807
                      Verification.ni_17.REDGE.ni_30._arrow._first_m
1808
                      Verification.ni_18.FEDGE1.__FEDGE1_2_m
1809
                      Verification.ni_18.FEDGE1.ni_29._arrow._first_m)
1810
))
1811

    
1812
(rule (=> 
1813
  (and (and (= Verification.ni_18.FEDGE1.__FEDGE1_2_m Verification.ni_18.FEDGE1.__FEDGE1_2_c)
1814
            (= Verification.ni_18.FEDGE1.ni_29._arrow._first_m Verification.ni_18.FEDGE1.ni_29._arrow._first_c)
1815
            )
1816
       (FEDGE1_step Verification.S1
1817
                    Verification.__Verification_3
1818
                    Verification.ni_18.FEDGE1.__FEDGE1_2_m
1819
                    Verification.ni_18.FEDGE1.ni_29._arrow._first_m
1820
                    Verification.ni_18.FEDGE1.__FEDGE1_2_x
1821
                    Verification.ni_18.FEDGE1.ni_29._arrow._first_x)
1822
       (and (= Verification.ni_17.REDGE.__REDGE_2_m Verification.ni_17.REDGE.__REDGE_2_c)
1823
            (= Verification.ni_17.REDGE.ni_30._arrow._first_m Verification.ni_17.REDGE.ni_30._arrow._first_c)
1824
            )
1825
       (REDGE_step Verification.S2
1826
                   Verification.__Verification_2
1827
                   Verification.ni_17.REDGE.__REDGE_2_m
1828
                   Verification.ni_17.REDGE.ni_30._arrow._first_m
1829
                   Verification.ni_17.REDGE.__REDGE_2_x
1830
                   Verification.ni_17.REDGE.ni_30._arrow._first_x)
1831
       (= Verification.property2 (= Verification.__Verification_3 Verification.__Verification_2))
1832
       (and (= Verification.ni_16.FEDGE2.ni_28.REDGE.__REDGE_2_m Verification.ni_16.FEDGE2.ni_28.REDGE.__REDGE_2_c)
1833
            (= Verification.ni_16.FEDGE2.ni_28.REDGE.ni_30._arrow._first_m Verification.ni_16.FEDGE2.ni_28.REDGE.ni_30._arrow._first_c)
1834
            )
1835
       (FEDGE2_step Verification.S1
1836
                    Verification.__Verification_4
1837
                    Verification.ni_16.FEDGE2.ni_28.REDGE.__REDGE_2_m
1838
                    Verification.ni_16.FEDGE2.ni_28.REDGE.ni_30._arrow._first_m
1839
                    Verification.ni_16.FEDGE2.ni_28.REDGE.__REDGE_2_x
1840
                    Verification.ni_16.FEDGE2.ni_28.REDGE.ni_30._arrow._first_x)
1841
       (= Verification.property1 (= Verification.__Verification_3 Verification.__Verification_4))
1842
       (= Verification.__Verification_1 (= Verification.S2 (not Verification.S1)))
1843
       (and (or (not (= Verification.__Verification_1 true))
1844
               (= Verification.property_ok (and Verification.property1 Verification.property2)))
1845
            (or (not (= Verification.__Verification_1 false))
1846
               (= Verification.property_ok true))
1847
       )
1848
       )
1849
  (Verification_step Verification.S1
1850
                     Verification.S2
1851
                     Verification.property_ok
1852
                     Verification.ni_16.FEDGE2.ni_28.REDGE.__REDGE_2_c
1853
                     Verification.ni_16.FEDGE2.ni_28.REDGE.ni_30._arrow._first_c
1854
                     Verification.ni_17.REDGE.__REDGE_2_c
1855
                     Verification.ni_17.REDGE.ni_30._arrow._first_c
1856
                     Verification.ni_18.FEDGE1.__FEDGE1_2_c
1857
                     Verification.ni_18.FEDGE1.ni_29._arrow._first_c
1858
                     Verification.ni_16.FEDGE2.ni_28.REDGE.__REDGE_2_x
1859
                     Verification.ni_16.FEDGE2.ni_28.REDGE.ni_30._arrow._first_x
1860
                     Verification.ni_17.REDGE.__REDGE_2_x
1861
                     Verification.ni_17.REDGE.ni_30._arrow._first_x
1862
                     Verification.ni_18.FEDGE1.__FEDGE1_2_x
1863
                     Verification.ni_18.FEDGE1.ni_29._arrow._first_x)
1864
))
1865

    
1866
; BoilerController
1867
(declare-var BoilerController.stop Bool)
1868
(declare-var BoilerController.steam_boiler_waiting Bool)
1869
(declare-var BoilerController.physical_units_ready Bool)
1870
(declare-var BoilerController.level Int)
1871
(declare-var BoilerController.steam Int)
1872
(declare-var BoilerController.pump_state_0 Int)
1873
(declare-var BoilerController.pump_state_1 Int)
1874
(declare-var BoilerController.pump_state_2 Int)
1875
(declare-var BoilerController.pump_state_3 Int)
1876
(declare-var BoilerController.pump_control_state_0 Bool)
1877
(declare-var BoilerController.pump_control_state_1 Bool)
1878
(declare-var BoilerController.pump_control_state_2 Bool)
1879
(declare-var BoilerController.pump_control_state_3 Bool)
1880
(declare-var BoilerController.pump_repaired_0 Bool)
1881
(declare-var BoilerController.pump_repaired_1 Bool)
1882
(declare-var BoilerController.pump_repaired_2 Bool)
1883
(declare-var BoilerController.pump_repaired_3 Bool)
1884
(declare-var BoilerController.pump_control_repaired_0 Bool)
1885
(declare-var BoilerController.pump_control_repaired_1 Bool)
1886
(declare-var BoilerController.pump_control_repaired_2 Bool)
1887
(declare-var BoilerController.pump_control_repaired_3 Bool)
1888
(declare-var BoilerController.level_repaired Bool)
1889
(declare-var BoilerController.steam_repaired Bool)
1890
(declare-var BoilerController.pump_failure_acknowledgement_0 Bool)
1891
(declare-var BoilerController.pump_failure_acknowledgement_1 Bool)
1892
(declare-var BoilerController.pump_failure_acknowledgement_2 Bool)
1893
(declare-var BoilerController.pump_failure_acknowledgement_3 Bool)
1894
(declare-var BoilerController.pump_control_failure_acknowledgement_0 Bool)
1895
(declare-var BoilerController.pump_control_failure_acknowledgement_1 Bool)
1896
(declare-var BoilerController.pump_control_failure_acknowledgement_2 Bool)
1897
(declare-var BoilerController.pump_control_failure_acknowledgement_3 Bool)
1898
(declare-var BoilerController.level_failure_acknowledgement Bool)
1899
(declare-var BoilerController.steam_failure_acknowledgement Bool)
1900
(declare-var BoilerController.program_ready Bool)
1901
(declare-var BoilerController.mode Int)
1902
(declare-var BoilerController.valve Bool)
1903
(declare-var BoilerController.open_pump_0 Bool)
1904
(declare-var BoilerController.open_pump_1 Bool)
1905
(declare-var BoilerController.open_pump_2 Bool)
1906
(declare-var BoilerController.open_pump_3 Bool)
1907
(declare-var BoilerController.close_pump_0 Bool)
1908
(declare-var BoilerController.close_pump_1 Bool)
1909
(declare-var BoilerController.close_pump_2 Bool)
1910
(declare-var BoilerController.close_pump_3 Bool)
1911
(declare-var BoilerController.pump_failure_detection_0 Bool)
1912
(declare-var BoilerController.pump_failure_detection_1 Bool)
1913
(declare-var BoilerController.pump_failure_detection_2 Bool)
1914
(declare-var BoilerController.pump_failure_detection_3 Bool)
1915
(declare-var BoilerController.pump_control_failure_detection_0 Bool)
1916
(declare-var BoilerController.pump_control_failure_detection_1 Bool)
1917
(declare-var BoilerController.pump_control_failure_detection_2 Bool)
1918
(declare-var BoilerController.pump_control_failure_detection_3 Bool)
1919
(declare-var BoilerController.level_failure_detection Bool)
1920
(declare-var BoilerController.steam_outcome_failure_detection Bool)
1921
(declare-var BoilerController.pump_repaired_acknowledgement_0 Bool)
1922
(declare-var BoilerController.pump_repaired_acknowledgement_1 Bool)
1923
(declare-var BoilerController.pump_repaired_acknowledgement_2 Bool)
1924
(declare-var BoilerController.pump_repaired_acknowledgement_3 Bool)
1925
(declare-var BoilerController.pump_control_repaired_acknowledgement_0 Bool)
1926
(declare-var BoilerController.pump_control_repaired_acknowledgement_1 Bool)
1927
(declare-var BoilerController.pump_control_repaired_acknowledgement_2 Bool)
1928
(declare-var BoilerController.pump_control_repaired_acknowledgement_3 Bool)
1929
(declare-var BoilerController.level_repaired_acknowledgement Bool)
1930
(declare-var BoilerController.steam_outcome_repaired_acknowledgement Bool)
1931
(declare-var BoilerController.__BoilerController_4_c Int)
1932
(declare-var BoilerController.__BoilerController_5_c Int)
1933
(declare-var BoilerController.__BoilerController_6_c Int)
1934
(declare-var BoilerController.__BoilerController_7_c Int)
1935
(declare-var BoilerController.__BoilerController_8_c Int)
1936
(declare-var BoilerController.ni_10._arrow._first_c Bool)
1937
(declare-var BoilerController.ni_11.SteamDefect.__SteamDefect_3_c Int)
1938
(declare-var BoilerController.ni_11.SteamDefect.ni_20._arrow._first_c Bool)
1939
(declare-var BoilerController.ni_12.PumpDefect.__PumpDefect_2_c Int)
1940
(declare-var BoilerController.ni_12.PumpDefect.__PumpDefect_4_c Int)
1941
(declare-var BoilerController.ni_12.PumpDefect.ni_23._arrow._first_c Bool)
1942
(declare-var BoilerController.ni_13.PumpDefect.__PumpDefect_2_c Int)
1943
(declare-var BoilerController.ni_13.PumpDefect.__PumpDefect_4_c Int)
1944
(declare-var BoilerController.ni_13.PumpDefect.ni_23._arrow._first_c Bool)
1945
(declare-var BoilerController.ni_14.PumpDefect.__PumpDefect_2_c Int)
1946
(declare-var BoilerController.ni_14.PumpDefect.__PumpDefect_4_c Int)
1947
(declare-var BoilerController.ni_14.PumpDefect.ni_23._arrow._first_c Bool)
1948
(declare-var BoilerController.ni_15.PumpDefect.__PumpDefect_2_c Int)
1949
(declare-var BoilerController.ni_15.PumpDefect.__PumpDefect_4_c Int)
1950
(declare-var BoilerController.ni_15.PumpDefect.ni_23._arrow._first_c Bool)
1951
(declare-var BoilerController.ni_2.PumpsOutput.__PumpsOutput_1_c Int)
1952
(declare-var BoilerController.ni_2.PumpsOutput.__PumpsOutput_2_c Int)
1953
(declare-var BoilerController.ni_2.PumpsOutput.__PumpsOutput_3_c Int)
1954
(declare-var BoilerController.ni_2.PumpsOutput.__PumpsOutput_4_c Int)
1955
(declare-var BoilerController.ni_2.PumpsOutput.__PumpsOutput_5_c Int)
1956
(declare-var BoilerController.ni_2.PumpsOutput.__PumpsOutput_6_c Int)
1957
(declare-var BoilerController.ni_2.PumpsOutput.__PumpsOutput_7_c Int)
1958
(declare-var BoilerController.ni_2.PumpsOutput.__PumpsOutput_8_c Int)
1959
(declare-var BoilerController.ni_3.PumpsStatus.__PumpsStatus_1_c Int)
1960
(declare-var BoilerController.ni_3.PumpsStatus.__PumpsStatus_2_c Int)
1961
(declare-var BoilerController.ni_3.PumpsStatus.__PumpsStatus_3_c Int)
1962
(declare-var BoilerController.ni_3.PumpsStatus.__PumpsStatus_4_c Int)
1963
(declare-var BoilerController.ni_3.PumpsStatus.ni_21._arrow._first_c Bool)
1964
(declare-var BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_12_c Int)
1965
(declare-var BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_19_c Int)
1966
(declare-var BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_26_c Int)
1967
(declare-var BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_5_c Int)
1968
(declare-var BoilerController.ni_4.PumpsDecision.__PumpsDecision_3_c Int)
1969
(declare-var BoilerController.ni_5.Valve.__Valve_2_c Int)
1970
(declare-var BoilerController.ni_5.Valve.ni_19._arrow._first_c Bool)
1971
(declare-var BoilerController.ni_6.ControlMode.__ControlMode_2_c Int)
1972
(declare-var BoilerController.ni_6.ControlMode.ni_27._arrow._first_c Bool)
1973
(declare-var BoilerController.ni_7.Operator.__Operator_2_c Int)
1974
(declare-var BoilerController.ni_7.Operator.ni_24._arrow._first_c Bool)
1975
(declare-var BoilerController.ni_8.Dynamics.__Dynamics_8_c Int)
1976
(declare-var BoilerController.ni_8.Dynamics.ni_26._arrow._first_c Bool)
1977
(declare-var BoilerController.ni_9.LevelDefect.__LevelDefect_3_c Int)
1978
(declare-var BoilerController.ni_9.LevelDefect.ni_25._arrow._first_c Bool)
1979
(declare-var BoilerController.__BoilerController_4_m Int)
1980
(declare-var BoilerController.__BoilerController_5_m Int)
1981
(declare-var BoilerController.__BoilerController_6_m Int)
1982
(declare-var BoilerController.__BoilerController_7_m Int)
1983
(declare-var BoilerController.__BoilerController_8_m Int)
1984
(declare-var BoilerController.ni_10._arrow._first_m Bool)
1985
(declare-var BoilerController.ni_11.SteamDefect.__SteamDefect_3_m Int)
1986
(declare-var BoilerController.ni_11.SteamDefect.ni_20._arrow._first_m Bool)
1987
(declare-var BoilerController.ni_12.PumpDefect.__PumpDefect_2_m Int)
1988
(declare-var BoilerController.ni_12.PumpDefect.__PumpDefect_4_m Int)
1989
(declare-var BoilerController.ni_12.PumpDefect.ni_23._arrow._first_m Bool)
1990
(declare-var BoilerController.ni_13.PumpDefect.__PumpDefect_2_m Int)
1991
(declare-var BoilerController.ni_13.PumpDefect.__PumpDefect_4_m Int)
1992
(declare-var BoilerController.ni_13.PumpDefect.ni_23._arrow._first_m Bool)
1993
(declare-var BoilerController.ni_14.PumpDefect.__PumpDefect_2_m Int)
1994
(declare-var BoilerController.ni_14.PumpDefect.__PumpDefect_4_m Int)
1995
(declare-var BoilerController.ni_14.PumpDefect.ni_23._arrow._first_m Bool)
1996
(declare-var BoilerController.ni_15.PumpDefect.__PumpDefect_2_m Int)
1997
(declare-var BoilerController.ni_15.PumpDefect.__PumpDefect_4_m Int)
1998
(declare-var BoilerController.ni_15.PumpDefect.ni_23._arrow._first_m Bool)
1999
(declare-var BoilerController.ni_2.PumpsOutput.__PumpsOutput_1_m Int)
2000
(declare-var BoilerController.ni_2.PumpsOutput.__PumpsOutput_2_m Int)
2001
(declare-var BoilerController.ni_2.PumpsOutput.__PumpsOutput_3_m Int)
2002
(declare-var BoilerController.ni_2.PumpsOutput.__PumpsOutput_4_m Int)
2003
(declare-var BoilerController.ni_2.PumpsOutput.__PumpsOutput_5_m Int)
2004
(declare-var BoilerController.ni_2.PumpsOutput.__PumpsOutput_6_m Int)
2005
(declare-var BoilerController.ni_2.PumpsOutput.__PumpsOutput_7_m Int)
2006
(declare-var BoilerController.ni_2.PumpsOutput.__PumpsOutput_8_m Int)
2007
(declare-var BoilerController.ni_3.PumpsStatus.__PumpsStatus_1_m Int)
2008
(declare-var BoilerController.ni_3.PumpsStatus.__PumpsStatus_2_m Int)
2009
(declare-var BoilerController.ni_3.PumpsStatus.__PumpsStatus_3_m Int)
2010
(declare-var BoilerController.ni_3.PumpsStatus.__PumpsStatus_4_m Int)
2011
(declare-var BoilerController.ni_3.PumpsStatus.ni_21._arrow._first_m Bool)
2012
(declare-var BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_12_m Int)
2013
(declare-var BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_19_m Int)
2014
(declare-var BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_26_m Int)
2015
(declare-var BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_5_m Int)
2016
(declare-var BoilerController.ni_4.PumpsDecision.__PumpsDecision_3_m Int)
2017
(declare-var BoilerController.ni_5.Valve.__Valve_2_m Int)
2018
(declare-var BoilerController.ni_5.Valve.ni_19._arrow._first_m Bool)
2019
(declare-var BoilerController.ni_6.ControlMode.__ControlMode_2_m Int)
2020
(declare-var BoilerController.ni_6.ControlMode.ni_27._arrow._first_m Bool)
2021
(declare-var BoilerController.ni_7.Operator.__Operator_2_m Int)
2022
(declare-var BoilerController.ni_7.Operator.ni_24._arrow._first_m Bool)
2023
(declare-var BoilerController.ni_8.Dynamics.__Dynamics_8_m Int)
2024
(declare-var BoilerController.ni_8.Dynamics.ni_26._arrow._first_m Bool)
2025
(declare-var BoilerController.ni_9.LevelDefect.__LevelDefect_3_m Int)
2026
(declare-var BoilerController.ni_9.LevelDefect.ni_25._arrow._first_m Bool)
2027
(declare-var BoilerController.__BoilerController_4_x Int)
2028
(declare-var BoilerController.__BoilerController_5_x Int)
2029
(declare-var BoilerController.__BoilerController_6_x Int)
2030
(declare-var BoilerController.__BoilerController_7_x Int)
2031
(declare-var BoilerController.__BoilerController_8_x Int)
2032
(declare-var BoilerController.ni_10._arrow._first_x Bool)
2033
(declare-var BoilerController.ni_11.SteamDefect.__SteamDefect_3_x Int)
2034
(declare-var BoilerController.ni_11.SteamDefect.ni_20._arrow._first_x Bool)
2035
(declare-var BoilerController.ni_12.PumpDefect.__PumpDefect_2_x Int)
2036
(declare-var BoilerController.ni_12.PumpDefect.__PumpDefect_4_x Int)
2037
(declare-var BoilerController.ni_12.PumpDefect.ni_23._arrow._first_x Bool)
2038
(declare-var BoilerController.ni_13.PumpDefect.__PumpDefect_2_x Int)
2039
(declare-var BoilerController.ni_13.PumpDefect.__PumpDefect_4_x Int)
2040
(declare-var BoilerController.ni_13.PumpDefect.ni_23._arrow._first_x Bool)
2041
(declare-var BoilerController.ni_14.PumpDefect.__PumpDefect_2_x Int)
2042
(declare-var BoilerController.ni_14.PumpDefect.__PumpDefect_4_x Int)
2043
(declare-var BoilerController.ni_14.PumpDefect.ni_23._arrow._first_x Bool)
2044
(declare-var BoilerController.ni_15.PumpDefect.__PumpDefect_2_x Int)
2045
(declare-var BoilerController.ni_15.PumpDefect.__PumpDefect_4_x Int)
2046
(declare-var BoilerController.ni_15.PumpDefect.ni_23._arrow._first_x Bool)
2047
(declare-var BoilerController.ni_2.PumpsOutput.__PumpsOutput_1_x Int)
2048
(declare-var BoilerController.ni_2.PumpsOutput.__PumpsOutput_2_x Int)
2049
(declare-var BoilerController.ni_2.PumpsOutput.__PumpsOutput_3_x Int)
2050
(declare-var BoilerController.ni_2.PumpsOutput.__PumpsOutput_4_x Int)
2051
(declare-var BoilerController.ni_2.PumpsOutput.__PumpsOutput_5_x Int)
2052
(declare-var BoilerController.ni_2.PumpsOutput.__PumpsOutput_6_x Int)
2053
(declare-var BoilerController.ni_2.PumpsOutput.__PumpsOutput_7_x Int)
2054
(declare-var BoilerController.ni_2.PumpsOutput.__PumpsOutput_8_x Int)
2055
(declare-var BoilerController.ni_3.PumpsStatus.__PumpsStatus_1_x Int)
2056
(declare-var BoilerController.ni_3.PumpsStatus.__PumpsStatus_2_x Int)
2057
(declare-var BoilerController.ni_3.PumpsStatus.__PumpsStatus_3_x Int)
2058
(declare-var BoilerController.ni_3.PumpsStatus.__PumpsStatus_4_x Int)
2059
(declare-var BoilerController.ni_3.PumpsStatus.ni_21._arrow._first_x Bool)
2060
(declare-var BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_12_x Int)
2061
(declare-var BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_19_x Int)
2062
(declare-var BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_26_x Int)
2063
(declare-var BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_5_x Int)
2064
(declare-var BoilerController.ni_4.PumpsDecision.__PumpsDecision_3_x Int)
2065
(declare-var BoilerController.ni_5.Valve.__Valve_2_x Int)
2066
(declare-var BoilerController.ni_5.Valve.ni_19._arrow._first_x Bool)
2067
(declare-var BoilerController.ni_6.ControlMode.__ControlMode_2_x Int)
2068
(declare-var BoilerController.ni_6.ControlMode.ni_27._arrow._first_x Bool)
2069
(declare-var BoilerController.ni_7.Operator.__Operator_2_x Int)
2070
(declare-var BoilerController.ni_7.Operator.ni_24._arrow._first_x Bool)
2071
(declare-var BoilerController.ni_8.Dynamics.__Dynamics_8_x Int)
2072
(declare-var BoilerController.ni_8.Dynamics.ni_26._arrow._first_x Bool)
2073
(declare-var BoilerController.ni_9.LevelDefect.__LevelDefect_3_x Int)
2074
(declare-var BoilerController.ni_9.LevelDefect.ni_25._arrow._first_x Bool)
2075
(declare-var BoilerController.__BoilerController_1 Bool)
2076
(declare-var BoilerController.__BoilerController_10 Int)
2077
(declare-var BoilerController.__BoilerController_2 Int)
2078
(declare-var BoilerController.__BoilerController_3 Int)
2079
(declare-var BoilerController.__BoilerController_9 Int)
2080
(declare-var BoilerController.a1 Bool)
2081
(declare-var BoilerController.a10 Bool)
2082
(declare-var BoilerController.a11 Bool)
2083
(declare-var BoilerController.a12 Bool)
2084
(declare-var BoilerController.a13 Bool)
2085
(declare-var BoilerController.a14 Bool)
2086
(declare-var BoilerController.a15 Bool)
2087
(declare-var BoilerController.a16 Bool)
2088
(declare-var BoilerController.a17 Bool)
2089
(declare-var BoilerController.a18 Bool)
2090
(declare-var BoilerController.a19 Bool)
2091
(declare-var BoilerController.a2 Bool)
2092
(declare-var BoilerController.a20 Bool)
2093
(declare-var BoilerController.a21 Bool)
2094
(declare-var BoilerController.a22 Bool)
2095
(declare-var BoilerController.a23 Bool)
2096
(declare-var BoilerController.a24 Bool)
2097
(declare-var BoilerController.a3 Bool)
2098
(declare-var BoilerController.a4 Bool)
2099
(declare-var BoilerController.a5 Bool)
2100
(declare-var BoilerController.a6 Bool)
2101
(declare-var BoilerController.a7 Bool)
2102
(declare-var BoilerController.a8 Bool)
2103
(declare-var BoilerController.a9 Bool)
2104
(declare-var BoilerController.b0 Bool)
2105
(declare-var BoilerController.b1 Bool)
2106
(declare-var BoilerController.b2 Bool)
2107
(declare-var BoilerController.b3 Bool)
2108
(declare-var BoilerController.flow_0 Bool)
2109
(declare-var BoilerController.flow_1 Bool)
2110
(declare-var BoilerController.flow_2 Bool)
2111
(declare-var BoilerController.flow_3 Bool)
2112
(declare-var BoilerController.level_defect Int)
2113
(declare-var BoilerController.n_pumps Int)
2114
(declare-var BoilerController.op_mode Int)
2115
(declare-var BoilerController.p_0 Int)
2116
(declare-var BoilerController.p_1 Int)
2117
(declare-var BoilerController.p_2 Int)
2118
(declare-var BoilerController.p_3 Int)
2119
(declare-var BoilerController.pump_control_defect_0 Int)
2120
(declare-var BoilerController.pump_control_defect_1 Int)
2121
(declare-var BoilerController.pump_control_defect_2 Int)
2122
(declare-var BoilerController.pump_control_defect_3 Int)
2123
(declare-var BoilerController.pump_defect_0 Int)
2124
(declare-var BoilerController.pump_defect_1 Int)
2125
(declare-var BoilerController.pump_defect_2 Int)
2126
(declare-var BoilerController.pump_defect_3 Int)
2127
(declare-var BoilerController.pump_status_0 Int)
2128
(declare-var BoilerController.pump_status_1 Int)
2129
(declare-var BoilerController.pump_status_2 Int)
2130
(declare-var BoilerController.pump_status_3 Int)
2131
(declare-var BoilerController.q Int)
2132
(declare-var BoilerController.steam_defect Int)
2133
(declare-var BoilerController.stop_request Bool)
2134
(declare-var BoilerController.t00 Int)
2135
(declare-var BoilerController.t01 Int)
2136
(declare-var BoilerController.t02 Bool)
2137
(declare-var BoilerController.t10 Int)
2138
(declare-var BoilerController.t11 Int)
2139
(declare-var BoilerController.t12 Bool)
2140
(declare-var BoilerController.t20 Int)
2141
(declare-var BoilerController.t21 Int)
2142
(declare-var BoilerController.t22 Bool)
2143
(declare-var BoilerController.t30 Int)
2144
(declare-var BoilerController.t31 Int)
2145
(declare-var BoilerController.t32 Bool)
2146
(declare-var BoilerController.t4 Int)
2147
(declare-var BoilerController.t5 Int)
2148
(declare-var BoilerController.t6 Int)
2149
(declare-var BoilerController.t7 Int)
2150
(declare-var BoilerController.t8 Int)
2151
(declare-var BoilerController.t9 Int)
2152
(declare-var BoilerController.u0 Int)
2153
(declare-var BoilerController.u1 Int)
2154
(declare-var BoilerController.u2 Int)
2155
(declare-var BoilerController.u3 Int)
2156
(declare-var BoilerController.u4 Bool)
2157
(declare-var BoilerController.u5 Int)
2158
(declare-var BoilerController.u6 Bool)
2159
(declare-var BoilerController.u7 Int)
2160
(declare-var BoilerController.v Int)
2161
(declare-var BoilerController.valve_state Int)
2162
(declare-rel BoilerController_reset (Int Int Int Int Int Bool Int Bool Int Int Bool Int Int Bool Int Int Bool Int Int Bool Int Int Int Int Int Int Int Int Int Int Int Int Bool Int Int Int Int Int Int Bool Int Bool Int Bool Int Bool Int Bool Int Int Int Int Int Bool Int Bool Int Int Bool Int Int Bool Int Int Bool Int Int Bool Int Int Int Int Int Int Int Int Int Int Int Int Bool Int Int Int Int Int Int Bool Int Bool Int Bool Int Bool Int Bool))
2163
(declare-rel BoilerController_step (Bool Bool Bool Int Int Int Int Int Int Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Int Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Int Int Int Int Int Bool Int Bool Int Int Bool Int Int Bool Int Int Bool Int Int Bool Int Int Int Int Int Int Int Int Int Int Int Int Bool Int Int Int Int Int Int Bool Int Bool Int Bool Int Bool Int Bool Int Int Int Int Int Bool Int Bool Int Int Bool Int Int Bool Int Int Bool Int Int Bool Int Int Int Int Int Int Int Int Int Int Int Int Bool Int Int Int Int Int Int Bool Int Bool Int Bool Int Bool Int Bool))
2164

    
2165
(rule (=> 
2166
  (and 
2167
       (= BoilerController.__BoilerController_4_m BoilerController.__BoilerController_4_c)
2168
       (= BoilerController.__BoilerController_5_m BoilerController.__BoilerController_5_c)
2169
       (= BoilerController.__BoilerController_6_m BoilerController.__BoilerController_6_c)
2170
       (= BoilerController.__BoilerController_7_m BoilerController.__BoilerController_7_c)
2171
       (= BoilerController.__BoilerController_8_m BoilerController.__BoilerController_8_c)
2172
       (LevelDefect_reset BoilerController.ni_9.LevelDefect.__LevelDefect_3_c
2173
                          BoilerController.ni_9.LevelDefect.ni_25._arrow._first_c
2174
                          BoilerController.ni_9.LevelDefect.__LevelDefect_3_m
2175
                          BoilerController.ni_9.LevelDefect.ni_25._arrow._first_m)
2176
       (Dynamics_reset BoilerController.ni_8.Dynamics.__Dynamics_8_c
2177
                       BoilerController.ni_8.Dynamics.ni_26._arrow._first_c
2178
                       BoilerController.ni_8.Dynamics.__Dynamics_8_m
2179
                       BoilerController.ni_8.Dynamics.ni_26._arrow._first_m)
2180
       (Operator_reset BoilerController.ni_7.Operator.__Operator_2_c
2181
                       BoilerController.ni_7.Operator.ni_24._arrow._first_c
2182
                       BoilerController.ni_7.Operator.__Operator_2_m
2183
                       BoilerController.ni_7.Operator.ni_24._arrow._first_m)
2184
       (ControlMode_reset BoilerController.ni_6.ControlMode.__ControlMode_2_c
2185
                          BoilerController.ni_6.ControlMode.ni_27._arrow._first_c
2186
                          BoilerController.ni_6.ControlMode.__ControlMode_2_m
2187
                          BoilerController.ni_6.ControlMode.ni_27._arrow._first_m)
2188
       (Valve_reset BoilerController.ni_5.Valve.__Valve_2_c
2189
                    BoilerController.ni_5.Valve.ni_19._arrow._first_c
2190
                    BoilerController.ni_5.Valve.__Valve_2_m
2191
                    BoilerController.ni_5.Valve.ni_19._arrow._first_m)
2192
       (PumpsDecision_reset BoilerController.ni_4.PumpsDecision.__PumpsDecision_3_c
2193
                            BoilerController.ni_4.PumpsDecision.__PumpsDecision_3_m)
2194
       (PumpsStatus_reset BoilerController.ni_3.PumpsStatus.__PumpsStatus_1_c
2195
                          BoilerController.ni_3.PumpsStatus.__PumpsStatus_2_c
2196
                          BoilerController.ni_3.PumpsStatus.__PumpsStatus_3_c
2197
                          BoilerController.ni_3.PumpsStatus.__PumpsStatus_4_c
2198
                          BoilerController.ni_3.PumpsStatus.ni_21._arrow._first_c
2199
                          BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_12_c
2200
                          BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_19_c
2201
                          BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_26_c
2202
                          BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_5_c
2203
                          BoilerController.ni_3.PumpsStatus.__PumpsStatus_1_m
2204
                          BoilerController.ni_3.PumpsStatus.__PumpsStatus_2_m
2205
                          BoilerController.ni_3.PumpsStatus.__PumpsStatus_3_m
2206
                          BoilerController.ni_3.PumpsStatus.__PumpsStatus_4_m
2207
                          BoilerController.ni_3.PumpsStatus.ni_21._arrow._first_m
2208
                          BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_12_m
2209
                          BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_19_m
2210
                          BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_26_m
2211
                          BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_5_m)
2212
       (PumpsOutput_reset BoilerController.ni_2.PumpsOutput.__PumpsOutput_1_c
2213
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_2_c
2214
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_3_c
2215
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_4_c
2216
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_5_c
2217
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_6_c
2218
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_7_c
2219
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_8_c
2220
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_1_m
2221
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_2_m
2222
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_3_m
2223
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_4_m
2224
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_5_m
2225
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_6_m
2226
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_7_m
2227
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_8_m)
2228
       (PumpDefect_reset BoilerController.ni_15.PumpDefect.__PumpDefect_2_c
2229
                         BoilerController.ni_15.PumpDefect.__PumpDefect_4_c
2230
                         BoilerController.ni_15.PumpDefect.ni_23._arrow._first_c
2231
                         BoilerController.ni_15.PumpDefect.__PumpDefect_2_m
2232
                         BoilerController.ni_15.PumpDefect.__PumpDefect_4_m
2233
                         BoilerController.ni_15.PumpDefect.ni_23._arrow._first_m)
2234
       (PumpDefect_reset BoilerController.ni_14.PumpDefect.__PumpDefect_2_c
2235
                         BoilerController.ni_14.PumpDefect.__PumpDefect_4_c
2236
                         BoilerController.ni_14.PumpDefect.ni_23._arrow._first_c
2237
                         BoilerController.ni_14.PumpDefect.__PumpDefect_2_m
2238
                         BoilerController.ni_14.PumpDefect.__PumpDefect_4_m
2239
                         BoilerController.ni_14.PumpDefect.ni_23._arrow._first_m)
2240
       (PumpDefect_reset BoilerController.ni_13.PumpDefect.__PumpDefect_2_c
2241
                         BoilerController.ni_13.PumpDefect.__PumpDefect_4_c
2242
                         BoilerController.ni_13.PumpDefect.ni_23._arrow._first_c
2243
                         BoilerController.ni_13.PumpDefect.__PumpDefect_2_m
2244
                         BoilerController.ni_13.PumpDefect.__PumpDefect_4_m
2245
                         BoilerController.ni_13.PumpDefect.ni_23._arrow._first_m)
2246
       (PumpDefect_reset BoilerController.ni_12.PumpDefect.__PumpDefect_2_c
2247
                         BoilerController.ni_12.PumpDefect.__PumpDefect_4_c
2248
                         BoilerController.ni_12.PumpDefect.ni_23._arrow._first_c
2249
                         BoilerController.ni_12.PumpDefect.__PumpDefect_2_m
2250
                         BoilerController.ni_12.PumpDefect.__PumpDefect_4_m
2251
                         BoilerController.ni_12.PumpDefect.ni_23._arrow._first_m)
2252
       (SteamDefect_reset BoilerController.ni_11.SteamDefect.__SteamDefect_3_c
2253
                          BoilerController.ni_11.SteamDefect.ni_20._arrow._first_c
2254
                          BoilerController.ni_11.SteamDefect.__SteamDefect_3_m
2255
                          BoilerController.ni_11.SteamDefect.ni_20._arrow._first_m)
2256
       (= BoilerController.ni_10._arrow._first_m true)
2257
  )
2258
  (BoilerController_reset BoilerController.__BoilerController_4_c
2259
                          BoilerController.__BoilerController_5_c
2260
                          BoilerController.__BoilerController_6_c
2261
                          BoilerController.__BoilerController_7_c
2262
                          BoilerController.__BoilerController_8_c
2263
                          BoilerController.ni_10._arrow._first_c
2264
                          BoilerController.ni_11.SteamDefect.__SteamDefect_3_c
2265
                          BoilerController.ni_11.SteamDefect.ni_20._arrow._first_c
2266
                          BoilerController.ni_12.PumpDefect.__PumpDefect_2_c
2267
                          BoilerController.ni_12.PumpDefect.__PumpDefect_4_c
2268
                          BoilerController.ni_12.PumpDefect.ni_23._arrow._first_c
2269
                          BoilerController.ni_13.PumpDefect.__PumpDefect_2_c
2270
                          BoilerController.ni_13.PumpDefect.__PumpDefect_4_c
2271
                          BoilerController.ni_13.PumpDefect.ni_23._arrow._first_c
2272
                          BoilerController.ni_14.PumpDefect.__PumpDefect_2_c
2273
                          BoilerController.ni_14.PumpDefect.__PumpDefect_4_c
2274
                          BoilerController.ni_14.PumpDefect.ni_23._arrow._first_c
2275
                          BoilerController.ni_15.PumpDefect.__PumpDefect_2_c
2276
                          BoilerController.ni_15.PumpDefect.__PumpDefect_4_c
2277
                          BoilerController.ni_15.PumpDefect.ni_23._arrow._first_c
2278
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_1_c
2279
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_2_c
2280
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_3_c
2281
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_4_c
2282
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_5_c
2283
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_6_c
2284
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_7_c
2285
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_8_c
2286
                          BoilerController.ni_3.PumpsStatus.__PumpsStatus_1_c
2287
                          BoilerController.ni_3.PumpsStatus.__PumpsStatus_2_c
2288
                          BoilerController.ni_3.PumpsStatus.__PumpsStatus_3_c
2289
                          BoilerController.ni_3.PumpsStatus.__PumpsStatus_4_c
2290
                          BoilerController.ni_3.PumpsStatus.ni_21._arrow._first_c
2291
                          BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_12_c
2292
                          BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_19_c
2293
                          BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_26_c
2294
                          BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_5_c
2295
                          BoilerController.ni_4.PumpsDecision.__PumpsDecision_3_c
2296
                          BoilerController.ni_5.Valve.__Valve_2_c
2297
                          BoilerController.ni_5.Valve.ni_19._arrow._first_c
2298
                          BoilerController.ni_6.ControlMode.__ControlMode_2_c
2299
                          BoilerController.ni_6.ControlMode.ni_27._arrow._first_c
2300
                          BoilerController.ni_7.Operator.__Operator_2_c
2301
                          BoilerController.ni_7.Operator.ni_24._arrow._first_c
2302
                          BoilerController.ni_8.Dynamics.__Dynamics_8_c
2303
                          BoilerController.ni_8.Dynamics.ni_26._arrow._first_c
2304
                          BoilerController.ni_9.LevelDefect.__LevelDefect_3_c
2305
                          BoilerController.ni_9.LevelDefect.ni_25._arrow._first_c
2306
                          BoilerController.__BoilerController_4_m
2307
                          BoilerController.__BoilerController_5_m
2308
                          BoilerController.__BoilerController_6_m
2309
                          BoilerController.__BoilerController_7_m
2310
                          BoilerController.__BoilerController_8_m
2311
                          BoilerController.ni_10._arrow._first_m
2312
                          BoilerController.ni_11.SteamDefect.__SteamDefect_3_m
2313
                          BoilerController.ni_11.SteamDefect.ni_20._arrow._first_m
2314
                          BoilerController.ni_12.PumpDefect.__PumpDefect_2_m
2315
                          BoilerController.ni_12.PumpDefect.__PumpDefect_4_m
2316
                          BoilerController.ni_12.PumpDefect.ni_23._arrow._first_m
2317
                          BoilerController.ni_13.PumpDefect.__PumpDefect_2_m
2318
                          BoilerController.ni_13.PumpDefect.__PumpDefect_4_m
2319
                          BoilerController.ni_13.PumpDefect.ni_23._arrow._first_m
2320
                          BoilerController.ni_14.PumpDefect.__PumpDefect_2_m
2321
                          BoilerController.ni_14.PumpDefect.__PumpDefect_4_m
2322
                          BoilerController.ni_14.PumpDefect.ni_23._arrow._first_m
2323
                          BoilerController.ni_15.PumpDefect.__PumpDefect_2_m
2324
                          BoilerController.ni_15.PumpDefect.__PumpDefect_4_m
2325
                          BoilerController.ni_15.PumpDefect.ni_23._arrow._first_m
2326
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_1_m
2327
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_2_m
2328
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_3_m
2329
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_4_m
2330
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_5_m
2331
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_6_m
2332
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_7_m
2333
                          BoilerController.ni_2.PumpsOutput.__PumpsOutput_8_m
2334
                          BoilerController.ni_3.PumpsStatus.__PumpsStatus_1_m
2335
                          BoilerController.ni_3.PumpsStatus.__PumpsStatus_2_m
2336
                          BoilerController.ni_3.PumpsStatus.__PumpsStatus_3_m
2337
                          BoilerController.ni_3.PumpsStatus.__PumpsStatus_4_m
2338
                          BoilerController.ni_3.PumpsStatus.ni_21._arrow._first_m
2339
                          BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_12_m
2340
                          BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_19_m
2341
                          BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_26_m
2342
                          BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_5_m
2343
                          BoilerController.ni_4.PumpsDecision.__PumpsDecision_3_m
2344
                          BoilerController.ni_5.Valve.__Valve_2_m
2345
                          BoilerController.ni_5.Valve.ni_19._arrow._first_m
2346
                          BoilerController.ni_6.ControlMode.__ControlMode_2_m
2347
                          BoilerController.ni_6.ControlMode.ni_27._arrow._first_m
2348
                          BoilerController.ni_7.Operator.__Operator_2_m
2349
                          BoilerController.ni_7.Operator.ni_24._arrow._first_m
2350
                          BoilerController.ni_8.Dynamics.__Dynamics_8_m
2351
                          BoilerController.ni_8.Dynamics.ni_26._arrow._first_m
2352
                          BoilerController.ni_9.LevelDefect.__LevelDefect_3_m
2353
                          BoilerController.ni_9.LevelDefect.ni_25._arrow._first_m)
2354
))
2355

    
2356
(rule (=> 
2357
  (and (and (= BoilerController.ni_15.PumpDefect.__PumpDefect_2_m BoilerController.ni_15.PumpDefect.__PumpDefect_2_c)
2358
            (= BoilerController.ni_15.PumpDefect.__PumpDefect_4_m BoilerController.ni_15.PumpDefect.__PumpDefect_4_c)
2359
            (= BoilerController.ni_15.PumpDefect.ni_23._arrow._first_m BoilerController.ni_15.PumpDefect.ni_23._arrow._first_c)
2360
            )
2361
       (PumpDefect_step BoilerController.pump_failure_acknowledgement_3
2362
                        BoilerController.pump_repaired_3
2363
                        BoilerController.pump_control_failure_acknowledgement_3
2364
                        BoilerController.pump_control_repaired_3
2365
                        BoilerController.__BoilerController_5_c
2366
                        BoilerController.pump_state_3
2367
                        BoilerController.pump_control_state_3
2368
                        BoilerController.t30
2369
                        BoilerController.t31
2370
                        BoilerController.t32
2371
                        BoilerController.ni_15.PumpDefect.__PumpDefect_2_m
2372
                        BoilerController.ni_15.PumpDefect.__PumpDefect_4_m
2373
                        BoilerController.ni_15.PumpDefect.ni_23._arrow._first_m
2374
                        BoilerController.ni_15.PumpDefect.__PumpDefect_2_x
2375
                        BoilerController.ni_15.PumpDefect.__PumpDefect_4_x
2376
                        BoilerController.ni_15.PumpDefect.ni_23._arrow._first_x)
2377
       (and (= BoilerController.ni_14.PumpDefect.__PumpDefect_2_m BoilerController.ni_14.PumpDefect.__PumpDefect_2_c)
2378
            (= BoilerController.ni_14.PumpDefect.__PumpDefect_4_m BoilerController.ni_14.PumpDefect.__PumpDefect_4_c)
2379
            (= BoilerController.ni_14.PumpDefect.ni_23._arrow._first_m BoilerController.ni_14.PumpDefect.ni_23._arrow._first_c)
2380
            )
2381
       (PumpDefect_step BoilerController.pump_failure_acknowledgement_2
2382
                        BoilerController.pump_repaired_2
2383
                        BoilerController.pump_control_failure_acknowledgement_2
2384
                        BoilerController.pump_control_repaired_2
2385
                        BoilerController.__BoilerController_6_c
2386
                        BoilerController.pump_state_2
2387
                        BoilerController.pump_control_state_2
2388
                        BoilerController.t20
2389
                        BoilerController.t21
2390
                        BoilerController.t22
2391
                        BoilerController.ni_14.PumpDefect.__PumpDefect_2_m
2392
                        BoilerController.ni_14.PumpDefect.__PumpDefect_4_m
2393
                        BoilerController.ni_14.PumpDefect.ni_23._arrow._first_m
2394
                        BoilerController.ni_14.PumpDefect.__PumpDefect_2_x
2395
                        BoilerController.ni_14.PumpDefect.__PumpDefect_4_x
2396
                        BoilerController.ni_14.PumpDefect.ni_23._arrow._first_x)
2397
       (and (= BoilerController.ni_13.PumpDefect.__PumpDefect_2_m BoilerController.ni_13.PumpDefect.__PumpDefect_2_c)
2398
            (= BoilerController.ni_13.PumpDefect.__PumpDefect_4_m BoilerController.ni_13.PumpDefect.__PumpDefect_4_c)
2399
            (= BoilerController.ni_13.PumpDefect.ni_23._arrow._first_m BoilerController.ni_13.PumpDefect.ni_23._arrow._first_c)
2400
            )
2401
       (PumpDefect_step BoilerController.pump_failure_acknowledgement_1
2402
                        BoilerController.pump_repaired_1
2403
                        BoilerController.pump_control_failure_acknowledgement_1
2404
                        BoilerController.pump_control_repaired_1
2405
                        BoilerController.__BoilerController_7_c
2406
                        BoilerController.pump_state_1
2407
                        BoilerController.pump_control_state_1
2408
                        BoilerController.t10
2409
                        BoilerController.t11
2410
                        BoilerController.t12
2411
                        BoilerController.ni_13.PumpDefect.__PumpDefect_2_m
2412
                        BoilerController.ni_13.PumpDefect.__PumpDefect_4_m
2413
                        BoilerController.ni_13.PumpDefect.ni_23._arrow._first_m
2414
                        BoilerController.ni_13.PumpDefect.__PumpDefect_2_x
2415
                        BoilerController.ni_13.PumpDefect.__PumpDefect_4_x
2416
                        BoilerController.ni_13.PumpDefect.ni_23._arrow._first_x)
2417
       (and (= BoilerController.ni_12.PumpDefect.__PumpDefect_2_m BoilerController.ni_12.PumpDefect.__PumpDefect_2_c)
2418
            (= BoilerController.ni_12.PumpDefect.__PumpDefect_4_m BoilerController.ni_12.PumpDefect.__PumpDefect_4_c)
2419
            (= BoilerController.ni_12.PumpDefect.ni_23._arrow._first_m BoilerController.ni_12.PumpDefect.ni_23._arrow._first_c)
2420
            )
2421
       (PumpDefect_step BoilerController.pump_failure_acknowledgement_0
2422
                        BoilerController.pump_repaired_0
2423
                        BoilerController.pump_control_failure_acknowledgement_0
2424
                        BoilerController.pump_control_repaired_0
2425
                        BoilerController.__BoilerController_8_c
2426
                        BoilerController.pump_state_0
2427
                        BoilerController.pump_control_state_0
2428
                        BoilerController.t00
2429
                        BoilerController.t01
2430
                        BoilerController.t02
2431
                        BoilerController.ni_12.PumpDefect.__PumpDefect_2_m
2432
                        BoilerController.ni_12.PumpDefect.__PumpDefect_4_m
2433
                        BoilerController.ni_12.PumpDefect.ni_23._arrow._first_m
2434
                        BoilerController.ni_12.PumpDefect.__PumpDefect_2_x
2435
                        BoilerController.ni_12.PumpDefect.__PumpDefect_4_x
2436
                        BoilerController.ni_12.PumpDefect.ni_23._arrow._first_x)
2437
       (and (= BoilerController.ni_11.SteamDefect.__SteamDefect_3_m BoilerController.ni_11.SteamDefect.__SteamDefect_3_c)
2438
            (= BoilerController.ni_11.SteamDefect.ni_20._arrow._first_m BoilerController.ni_11.SteamDefect.ni_20._arrow._first_c)
2439
            )
2440
       (SteamDefect_step BoilerController.steam_failure_acknowledgement
2441
                         BoilerController.steam_repaired
2442
                         BoilerController.steam
2443
                         BoilerController.__BoilerController_9
2444
                         BoilerController.ni_11.SteamDefect.__SteamDefect_3_m
2445
                         BoilerController.ni_11.SteamDefect.ni_20._arrow._first_m
2446
                         BoilerController.ni_11.SteamDefect.__SteamDefect_3_x
2447
                         BoilerController.ni_11.SteamDefect.ni_20._arrow._first_x)
2448
       (= BoilerController.ni_10._arrow._first_m BoilerController.ni_10._arrow._first_c)
2449
       (and (= BoilerController.__BoilerController_1 (ite BoilerController.ni_10._arrow._first_m true false))
2450
            (= BoilerController.ni_10._arrow._first_x false))
2451
       (and (or (not (= BoilerController.__BoilerController_1 true))
2452
               (= BoilerController.steam_defect 0))
2453
            (or (not (= BoilerController.__BoilerController_1 false))
2454
               (= BoilerController.steam_defect BoilerController.__BoilerController_9))
2455
       )
2456
       (and (= BoilerController.ni_9.LevelDefect.__LevelDefect_3_m BoilerController.ni_9.LevelDefect.__LevelDefect_3_c)
2457
            (= BoilerController.ni_9.LevelDefect.ni_25._arrow._first_m BoilerController.ni_9.LevelDefect.ni_25._arrow._first_c)
2458
            )
2459
       (LevelDefect_step BoilerController.level_failure_acknowledgement
2460
                         BoilerController.level_repaired
2461
                         BoilerController.level
2462
                         BoilerController.__BoilerController_10
2463
                         BoilerController.ni_9.LevelDefect.__LevelDefect_3_m
2464
                         BoilerController.ni_9.LevelDefect.ni_25._arrow._first_m
2465
                         BoilerController.ni_9.LevelDefect.__LevelDefect_3_x
2466
                         BoilerController.ni_9.LevelDefect.ni_25._arrow._first_x)
2467
       (and (or (not (= BoilerController.__BoilerController_1 false))
2468
               (and (= BoilerController.level_defect BoilerController.__BoilerController_10)
2469
                    (= BoilerController.flow_3 BoilerController.t32)
2470
                    (= BoilerController.flow_2 BoilerController.t22)
2471
                    (= BoilerController.flow_1 BoilerController.t12)
2472
                    (= BoilerController.flow_0 BoilerController.t02)
2473
                    ))
2474
            (or (not (= BoilerController.__BoilerController_1 true))
2475
               (and (= BoilerController.level_defect 0)
2476
                    (= BoilerController.flow_3 false)
2477
                    (= BoilerController.flow_2 false)
2478
                    (= BoilerController.flow_1 false)
2479
                    (= BoilerController.flow_0 false)
2480
                    ))
2481
       )
2482
       (and (= BoilerController.ni_8.Dynamics.__Dynamics_8_m BoilerController.ni_8.Dynamics.__Dynamics_8_c)
2483
            (= BoilerController.ni_8.Dynamics.ni_26._arrow._first_m BoilerController.ni_8.Dynamics.ni_26._arrow._first_c)
2484
            )
2485
       (Dynamics_step BoilerController.__BoilerController_4_c
2486
                      BoilerController.level
2487
                      BoilerController.steam
2488
                      BoilerController.level_defect
2489
                      BoilerController.steam_defect
2490
                      BoilerController.flow_0
2491
                      BoilerController.flow_1
2492
                      BoilerController.flow_2
2493
                      BoilerController.flow_3
2494
                      BoilerController.t4
2495
                      BoilerController.t5
2496
                      BoilerController.t6
2497
                      BoilerController.t7
2498
                      BoilerController.t8
2499
                      BoilerController.t9
2500
                      BoilerController.ni_8.Dynamics.__Dynamics_8_m
2501
                      BoilerController.ni_8.Dynamics.ni_26._arrow._first_m
2502
                      BoilerController.ni_8.Dynamics.__Dynamics_8_x
2503
                      BoilerController.ni_8.Dynamics.ni_26._arrow._first_x)
2504
       (and (= BoilerController.ni_7.Operator.__Operator_2_m BoilerController.ni_7.Operator.__Operator_2_c)
2505
            (= BoilerController.ni_7.Operator.ni_24._arrow._first_m BoilerController.ni_7.Operator.ni_24._arrow._first_c)
2506
            )
2507
       (Operator_step BoilerController.stop
2508
                      BoilerController.stop_request
2509
                      BoilerController.ni_7.Operator.__Operator_2_m
2510
                      BoilerController.ni_7.Operator.ni_24._arrow._first_m
2511
                      BoilerController.ni_7.Operator.__Operator_2_x
2512
                      BoilerController.ni_7.Operator.ni_24._arrow._first_x)
2513
       (and (or (not (= BoilerController.__BoilerController_1 false))
2514
               (and (= BoilerController.q BoilerController.t4)
2515
                    (= BoilerController.pump_defect_3 BoilerController.t30)
2516
                    (= BoilerController.pump_defect_2 BoilerController.t20)
2517
                    (= BoilerController.pump_defect_1 BoilerController.t10)
2518
                    (= BoilerController.pump_defect_0 BoilerController.t00)
2519
                    (= BoilerController.pump_control_defect_3 BoilerController.t31)
2520
                    (= BoilerController.pump_control_defect_2 BoilerController.t21)
2521
                    (= BoilerController.pump_control_defect_1 BoilerController.t11)
2522
                    (= BoilerController.pump_control_defect_0 BoilerController.t01)
2523
                    ))
2524
            (or (not (= BoilerController.__BoilerController_1 true))
2525
               (and (= BoilerController.q BoilerController.level)
2526
                    (= BoilerController.pump_defect_3 0)
2527
                    (= BoilerController.pump_defect_2 0)
2528
                    (= BoilerController.pump_defect_1 0)
2529
                    (= BoilerController.pump_defect_0 0)
2530
                    (= BoilerController.pump_control_defect_3 0)
2531
                    (= BoilerController.pump_control_defect_2 0)
2532
                    (= BoilerController.pump_control_defect_1 0)
2533
                    (= BoilerController.pump_control_defect_0 0)
2534
                    ))
2535
       )
2536
       (and (= BoilerController.ni_6.ControlMode.__ControlMode_2_m BoilerController.ni_6.ControlMode.__ControlMode_2_c)
2537
            (= BoilerController.ni_6.ControlMode.ni_27._arrow._first_m BoilerController.ni_6.ControlMode.ni_27._arrow._first_c)
2538
            )
2539
       (ControlMode_step BoilerController.steam_boiler_waiting
2540
                         BoilerController.physical_units_ready
2541
                         BoilerController.stop_request
2542
                         BoilerController.steam
2543
                         BoilerController.level_defect
2544
                         BoilerController.steam_defect
2545
                         BoilerController.pump_defect_0
2546
                         BoilerController.pump_defect_1
2547
                         BoilerController.pump_defect_2
2548
                         BoilerController.pump_defect_3
2549
                         BoilerController.pump_control_defect_0
2550
                         BoilerController.pump_control_defect_1
2551
                         BoilerController.pump_control_defect_2
2552
                         BoilerController.pump_control_defect_3
2553
                         BoilerController.q
2554
                         BoilerController.pump_state_0
2555
                         BoilerController.pump_state_1
2556
                         BoilerController.pump_state_2
2557
                         BoilerController.pump_state_3
2558
                         BoilerController.__BoilerController_2
2559
                         BoilerController.ni_6.ControlMode.__ControlMode_2_m
2560
                         BoilerController.ni_6.ControlMode.ni_27._arrow._first_m
2561
                         BoilerController.ni_6.ControlMode.__ControlMode_2_x
2562
                         BoilerController.ni_6.ControlMode.ni_27._arrow._first_x)
2563
       (and (or (not (= BoilerController.__BoilerController_1 true))
2564
               (= BoilerController.op_mode 1))
2565
            (or (not (= BoilerController.__BoilerController_1 false))
2566
               (= BoilerController.op_mode BoilerController.__BoilerController_2))
2567
       )
2568
       (and (= BoilerController.ni_5.Valve.__Valve_2_m BoilerController.ni_5.Valve.__Valve_2_c)
2569
            (= BoilerController.ni_5.Valve.ni_19._arrow._first_m BoilerController.ni_5.Valve.ni_19._arrow._first_c)
2570
            )
2571
       (Valve_step BoilerController.op_mode
2572
                   BoilerController.q
2573
                   BoilerController.u4
2574
                   BoilerController.u5
2575
                   BoilerController.ni_5.Valve.__Valve_2_m
2576
                   BoilerController.ni_5.Valve.ni_19._arrow._first_m
2577
                   BoilerController.ni_5.Valve.__Valve_2_x
2578
                   BoilerController.ni_5.Valve.ni_19._arrow._first_x)
2579
       (and (or (not (= BoilerController.__BoilerController_1 false))
2580
               (and (= BoilerController.valve_state BoilerController.u5)
2581
                    (= BoilerController.valve BoilerController.u4)
2582
                    (= BoilerController.v BoilerController.t5)
2583
                    ))
2584
            (or (not (= BoilerController.__BoilerController_1 true))
2585
               (and (= BoilerController.valve_state 0)
2586
                    (= BoilerController.valve false)
2587
                    (= BoilerController.v BoilerController.steam)
2588
                    ))
2589
       )
2590
       (ControlOutput BoilerController.op_mode
2591
                      BoilerController.level
2592
                      BoilerController.valve
2593
                      BoilerController.u6
2594
                      BoilerController.u7)
2595
       (= BoilerController.ni_4.PumpsDecision.__PumpsDecision_3_m BoilerController.ni_4.PumpsDecision.__PumpsDecision_3_c)(PumpsDecision_step 
2596
       BoilerController.q
2597
       BoilerController.v
2598
       BoilerController.__BoilerController_3
2599
       BoilerController.ni_4.PumpsDecision.__PumpsDecision_3_m
2600
       BoilerController.ni_4.PumpsDecision.__PumpsDecision_3_x)
2601
       (and (or (not (= BoilerController.__BoilerController_1 true))
2602
               (= BoilerController.n_pumps 0))
2603
            (or (not (= BoilerController.__BoilerController_1 false))
2604
               (= BoilerController.n_pumps BoilerController.__BoilerController_3))
2605
       )
2606
       (and (= BoilerController.ni_3.PumpsStatus.__PumpsStatus_1_m BoilerController.ni_3.PumpsStatus.__PumpsStatus_1_c)
2607
            (= BoilerController.ni_3.PumpsStatus.__PumpsStatus_2_m BoilerController.ni_3.PumpsStatus.__PumpsStatus_2_c)
2608
            (= BoilerController.ni_3.PumpsStatus.__PumpsStatus_3_m BoilerController.ni_3.PumpsStatus.__PumpsStatus_3_c)
2609
            (= BoilerController.ni_3.PumpsStatus.__PumpsStatus_4_m BoilerController.ni_3.PumpsStatus.__PumpsStatus_4_c)
2610
            (= BoilerController.ni_3.PumpsStatus.ni_21._arrow._first_m BoilerController.ni_3.PumpsStatus.ni_21._arrow._first_c)
2611
            (= BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_12_m BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_12_c)
2612
            (= BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_19_m BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_19_c)
2613
            (= BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_26_m BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_26_c)
2614
            (= BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_5_m BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_5_c)
2615
            )
2616
       (PumpsStatus_step BoilerController.n_pumps
2617
                         BoilerController.pump_defect_0
2618
                         BoilerController.pump_defect_1
2619
                         BoilerController.pump_defect_2
2620
                         BoilerController.pump_defect_3
2621
                         BoilerController.flow_0
2622
                         BoilerController.flow_1
2623
                         BoilerController.flow_2
2624
                         BoilerController.flow_3
2625
                         BoilerController.u0
2626
                         BoilerController.u1
2627
                         BoilerController.u2
2628
                         BoilerController.u3
2629
                         BoilerController.ni_3.PumpsStatus.__PumpsStatus_1_m
2630
                         BoilerController.ni_3.PumpsStatus.__PumpsStatus_2_m
2631
                         BoilerController.ni_3.PumpsStatus.__PumpsStatus_3_m
2632
                         BoilerController.ni_3.PumpsStatus.__PumpsStatus_4_m
2633
                         BoilerController.ni_3.PumpsStatus.ni_21._arrow._first_m
2634
                         BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_12_m
2635
                         BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_19_m
2636
                         BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_26_m
2637
                         BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_5_m
2638
                         BoilerController.ni_3.PumpsStatus.__PumpsStatus_1_x
2639
                         BoilerController.ni_3.PumpsStatus.__PumpsStatus_2_x
2640
                         BoilerController.ni_3.PumpsStatus.__PumpsStatus_3_x
2641
                         BoilerController.ni_3.PumpsStatus.__PumpsStatus_4_x
2642
                         BoilerController.ni_3.PumpsStatus.ni_21._arrow._first_x
2643
                         BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_12_x
2644
                         BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_19_x
2645
                         BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_26_x
2646
                         BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_5_x)
2647
       (SteamOutput BoilerController.op_mode
2648
                    BoilerController.steam_defect
2649
                    BoilerController.steam_repaired
2650
                    BoilerController.b2
2651
                    BoilerController.b3)
2652
       (and (or (not (= BoilerController.__BoilerController_1 false))
2653
               (and (= BoilerController.steam_outcome_repaired_acknowledgement BoilerController.b3)
2654
                    (= BoilerController.steam_outcome_failure_detection BoilerController.b2)
2655
                    (= BoilerController.pump_status_3 BoilerController.u3)
2656
                    (= BoilerController.pump_status_2 BoilerController.u2)
2657
                    (= BoilerController.pump_status_1 BoilerController.u1)
2658
                    (= BoilerController.pump_status_0 BoilerController.u0)
2659
                    ))
2660
            (or (not (= BoilerController.__BoilerController_1 true))
2661
               (and (= BoilerController.steam_outcome_repaired_acknowledgement false)
2662
                    (= BoilerController.steam_outcome_failure_detection false)
2663
                    (= BoilerController.pump_status_3 0)
2664
                    (= BoilerController.pump_status_2 0)
2665
                    (= BoilerController.pump_status_1 0)
2666
                    (= BoilerController.pump_status_0 0)
2667
                    ))
2668
       )
2669
       (and (= BoilerController.ni_2.PumpsOutput.__PumpsOutput_1_m BoilerController.ni_2.PumpsOutput.__PumpsOutput_1_c)
2670
            (= BoilerController.ni_2.PumpsOutput.__PumpsOutput_2_m BoilerController.ni_2.PumpsOutput.__PumpsOutput_2_c)
2671
            (= BoilerController.ni_2.PumpsOutput.__PumpsOutput_3_m BoilerController.ni_2.PumpsOutput.__PumpsOutput_3_c)
2672
            (= BoilerController.ni_2.PumpsOutput.__PumpsOutput_4_m BoilerController.ni_2.PumpsOutput.__PumpsOutput_4_c)
2673
            (= BoilerController.ni_2.PumpsOutput.__PumpsOutput_5_m BoilerController.ni_2.PumpsOutput.__PumpsOutput_5_c)
2674
            (= BoilerController.ni_2.PumpsOutput.__PumpsOutput_6_m BoilerController.ni_2.PumpsOutput.__PumpsOutput_6_c)
2675
            (= BoilerController.ni_2.PumpsOutput.__PumpsOutput_7_m BoilerController.ni_2.PumpsOutput.__PumpsOutput_7_c)
2676
            (= BoilerController.ni_2.PumpsOutput.__PumpsOutput_8_m BoilerController.ni_2.PumpsOutput.__PumpsOutput_8_c)
2677
            )
2678
       (PumpsOutput_step BoilerController.op_mode
2679
                         BoilerController.pump_status_0
2680
                         BoilerController.pump_status_1
2681
                         BoilerController.pump_status_2
2682
                         BoilerController.pump_status_3
2683
                         BoilerController.pump_defect_0
2684
                         BoilerController.pump_defect_1
2685
                         BoilerController.pump_defect_2
2686
                         BoilerController.pump_defect_3
2687
                         BoilerController.pump_control_defect_0
2688
                         BoilerController.pump_control_defect_1
2689
                         BoilerController.pump_control_defect_2
2690
                         BoilerController.pump_control_defect_3
2691
                         BoilerController.pump_repaired_0
2692
                         BoilerController.pump_repaired_1
2693
                         BoilerController.pump_repaired_2
2694
                         BoilerController.pump_repaired_3
2695
                         BoilerController.pump_control_repaired_0
2696
                         BoilerController.pump_control_repaired_1
2697
                         BoilerController.pump_control_repaired_2
2698
                         BoilerController.pump_control_repaired_3
2699
                         BoilerController.a1
2700
                         BoilerController.a2
2701
                         BoilerController.a3
2702
                         BoilerController.a4
2703
                         BoilerController.a5
2704
                         BoilerController.a6
2705
                         BoilerController.a7
2706
                         BoilerController.a8
2707
                         BoilerController.a9
2708
                         BoilerController.a10
2709
                         BoilerController.a11
2710
                         BoilerController.a12
2711
                         BoilerController.a13
2712
                         BoilerController.a14
2713
                         BoilerController.a15
2714
                         BoilerController.a16
2715
                         BoilerController.a17
2716
                         BoilerController.a18
2717
                         BoilerController.a19
2718
                         BoilerController.a20
2719
                         BoilerController.a21
2720
                         BoilerController.a22
2721
                         BoilerController.a23
2722
                         BoilerController.a24
2723
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_1_m
2724
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_2_m
2725
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_3_m
2726
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_4_m
2727
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_5_m
2728
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_6_m
2729
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_7_m
2730
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_8_m
2731
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_1_x
2732
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_2_x
2733
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_3_x
2734
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_4_x
2735
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_5_x
2736
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_6_x
2737
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_7_x
2738
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_8_x)
2739
       (= BoilerController.pump_repaired_acknowledgement_3 BoilerController.a16)
2740
       (= BoilerController.pump_repaired_acknowledgement_2 BoilerController.a15)
2741
       (= BoilerController.pump_repaired_acknowledgement_1 BoilerController.a14)
2742
       (= BoilerController.pump_repaired_acknowledgement_0 BoilerController.a13)
2743
       (= BoilerController.pump_failure_detection_3 BoilerController.a12)
2744
       (= BoilerController.pump_failure_detection_2 BoilerController.a11)
2745
       (= BoilerController.pump_failure_detection_1 BoilerController.a10)
2746
       (= BoilerController.pump_failure_detection_0 BoilerController.a9)
2747
       (= BoilerController.pump_control_repaired_acknowledgement_3 BoilerController.a24)
2748
       (= BoilerController.pump_control_repaired_acknowledgement_2 BoilerController.a23)
2749
       (= BoilerController.pump_control_repaired_acknowledgement_1 BoilerController.a22)
2750
       (= BoilerController.pump_control_repaired_acknowledgement_0 BoilerController.a21)
2751
       (= BoilerController.pump_control_failure_detection_3 BoilerController.a20)
2752
       (= BoilerController.pump_control_failure_detection_2 BoilerController.a19)
2753
       (= BoilerController.pump_control_failure_detection_1 BoilerController.a18)
2754
       (= BoilerController.pump_control_failure_detection_0 BoilerController.a17)
2755
       (and (or (not (= BoilerController.__BoilerController_1 false))
2756
               (and (= BoilerController.program_ready BoilerController.u6)
2757
                    (= BoilerController.p_3 BoilerController.t9)
2758
                    (= BoilerController.p_2 BoilerController.t8)
2759
                    (= BoilerController.p_1 BoilerController.t7)
2760
                    (= BoilerController.p_0 BoilerController.t6)
2761
                    ))
2762
            (or (not (= BoilerController.__BoilerController_1 true))
2763
               (and (= BoilerController.program_ready false)
2764
                    (= BoilerController.p_3 0)
2765
                    (= BoilerController.p_2 0)
2766
                    (= BoilerController.p_1 0)
2767
                    (= BoilerController.p_0 0)
2768
                    ))
2769
       )
2770
       (= BoilerController.open_pump_3 BoilerController.a4)
2771
       (= BoilerController.open_pump_2 BoilerController.a3)
2772
       (= BoilerController.open_pump_1 BoilerController.a2)
2773
       (= BoilerController.open_pump_0 BoilerController.a1)
2774
       (and (or (not (= BoilerController.__BoilerController_1 true))
2775
               (= BoilerController.mode 1))
2776
            (or (not (= BoilerController.__BoilerController_1 false))
2777
               (= BoilerController.mode BoilerController.u7))
2778
       )
2779
       (LevelOutput BoilerController.op_mode
2780
                    BoilerController.level_defect
2781
                    BoilerController.level_repaired
2782
                    BoilerController.b0
2783
                    BoilerController.b1)
2784
       (and (or (not (= BoilerController.__BoilerController_1 false))
2785
               (and (= BoilerController.level_repaired_acknowledgement BoilerController.b1)
2786
                    (= BoilerController.level_failure_detection BoilerController.b0)
2787
                    ))
2788
            (or (not (= BoilerController.__BoilerController_1 true))
2789
               (and (= BoilerController.level_repaired_acknowledgement false)
2790
                    (= BoilerController.level_failure_detection false)
2791
                    ))
2792
       )
2793
       (= BoilerController.close_pump_3 BoilerController.a8)
2794
       (= BoilerController.close_pump_2 BoilerController.a7)
2795
       (= BoilerController.close_pump_1 BoilerController.a6)
2796
       (= BoilerController.close_pump_0 BoilerController.a5)
2797
       (= BoilerController.__BoilerController_8_x BoilerController.pump_status_0)
2798
       (= BoilerController.__BoilerController_7_x BoilerController.pump_status_1)
2799
       (= BoilerController.__BoilerController_6_x BoilerController.pump_status_2)
2800
       (= BoilerController.__BoilerController_5_x BoilerController.pump_status_3)
2801
       (= BoilerController.__BoilerController_4_x BoilerController.valve_state)
2802
       )
2803
  (BoilerController_step BoilerController.stop
2804
                         BoilerController.steam_boiler_waiting
2805
                         BoilerController.physical_units_ready
2806
                         BoilerController.level
2807
                         BoilerController.steam
2808
                         BoilerController.pump_state_0
2809
                         BoilerController.pump_state_1
2810
                         BoilerController.pump_state_2
2811
                         BoilerController.pump_state_3
2812
                         BoilerController.pump_control_state_0
2813
                         BoilerController.pump_control_state_1
2814
                         BoilerController.pump_control_state_2
2815
                         BoilerController.pump_control_state_3
2816
                         BoilerController.pump_repaired_0
2817
                         BoilerController.pump_repaired_1
2818
                         BoilerController.pump_repaired_2
2819
                         BoilerController.pump_repaired_3
2820
                         BoilerController.pump_control_repaired_0
2821
                         BoilerController.pump_control_repaired_1
2822
                         BoilerController.pump_control_repaired_2
2823
                         BoilerController.pump_control_repaired_3
2824
                         BoilerController.level_repaired
2825
                         BoilerController.steam_repaired
2826
                         BoilerController.pump_failure_acknowledgement_0
2827
                         BoilerController.pump_failure_acknowledgement_1
2828
                         BoilerController.pump_failure_acknowledgement_2
2829
                         BoilerController.pump_failure_acknowledgement_3
2830
                         BoilerController.pump_control_failure_acknowledgement_0
2831
                         BoilerController.pump_control_failure_acknowledgement_1
2832
                         BoilerController.pump_control_failure_acknowledgement_2
2833
                         BoilerController.pump_control_failure_acknowledgement_3
2834
                         BoilerController.level_failure_acknowledgement
2835
                         BoilerController.steam_failure_acknowledgement
2836
                         BoilerController.program_ready
2837
                         BoilerController.mode
2838
                         BoilerController.valve
2839
                         BoilerController.open_pump_0
2840
                         BoilerController.open_pump_1
2841
                         BoilerController.open_pump_2
2842
                         BoilerController.open_pump_3
2843
                         BoilerController.close_pump_0
2844
                         BoilerController.close_pump_1
2845
                         BoilerController.close_pump_2
2846
                         BoilerController.close_pump_3
2847
                         BoilerController.pump_failure_detection_0
2848
                         BoilerController.pump_failure_detection_1
2849
                         BoilerController.pump_failure_detection_2
2850
                         BoilerController.pump_failure_detection_3
2851
                         BoilerController.pump_control_failure_detection_0
2852
                         BoilerController.pump_control_failure_detection_1
2853
                         BoilerController.pump_control_failure_detection_2
2854
                         BoilerController.pump_control_failure_detection_3
2855
                         BoilerController.level_failure_detection
2856
                         BoilerController.steam_outcome_failure_detection
2857
                         BoilerController.pump_repaired_acknowledgement_0
2858
                         BoilerController.pump_repaired_acknowledgement_1
2859
                         BoilerController.pump_repaired_acknowledgement_2
2860
                         BoilerController.pump_repaired_acknowledgement_3
2861
                         BoilerController.pump_control_repaired_acknowledgement_0
2862
                         BoilerController.pump_control_repaired_acknowledgement_1
2863
                         BoilerController.pump_control_repaired_acknowledgement_2
2864
                         BoilerController.pump_control_repaired_acknowledgement_3
2865
                         BoilerController.level_repaired_acknowledgement
2866
                         BoilerController.steam_outcome_repaired_acknowledgement
2867
                         BoilerController.__BoilerController_4_c
2868
                         BoilerController.__BoilerController_5_c
2869
                         BoilerController.__BoilerController_6_c
2870
                         BoilerController.__BoilerController_7_c
2871
                         BoilerController.__BoilerController_8_c
2872
                         BoilerController.ni_10._arrow._first_c
2873
                         BoilerController.ni_11.SteamDefect.__SteamDefect_3_c
2874
                         BoilerController.ni_11.SteamDefect.ni_20._arrow._first_c
2875
                         BoilerController.ni_12.PumpDefect.__PumpDefect_2_c
2876
                         BoilerController.ni_12.PumpDefect.__PumpDefect_4_c
2877
                         BoilerController.ni_12.PumpDefect.ni_23._arrow._first_c
2878
                         BoilerController.ni_13.PumpDefect.__PumpDefect_2_c
2879
                         BoilerController.ni_13.PumpDefect.__PumpDefect_4_c
2880
                         BoilerController.ni_13.PumpDefect.ni_23._arrow._first_c
2881
                         BoilerController.ni_14.PumpDefect.__PumpDefect_2_c
2882
                         BoilerController.ni_14.PumpDefect.__PumpDefect_4_c
2883
                         BoilerController.ni_14.PumpDefect.ni_23._arrow._first_c
2884
                         BoilerController.ni_15.PumpDefect.__PumpDefect_2_c
2885
                         BoilerController.ni_15.PumpDefect.__PumpDefect_4_c
2886
                         BoilerController.ni_15.PumpDefect.ni_23._arrow._first_c
2887
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_1_c
2888
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_2_c
2889
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_3_c
2890
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_4_c
2891
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_5_c
2892
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_6_c
2893
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_7_c
2894
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_8_c
2895
                         BoilerController.ni_3.PumpsStatus.__PumpsStatus_1_c
2896
                         BoilerController.ni_3.PumpsStatus.__PumpsStatus_2_c
2897
                         BoilerController.ni_3.PumpsStatus.__PumpsStatus_3_c
2898
                         BoilerController.ni_3.PumpsStatus.__PumpsStatus_4_c
2899
                         BoilerController.ni_3.PumpsStatus.ni_21._arrow._first_c
2900
                         BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_12_c
2901
                         BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_19_c
2902
                         BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_26_c
2903
                         BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_5_c
2904
                         BoilerController.ni_4.PumpsDecision.__PumpsDecision_3_c
2905
                         BoilerController.ni_5.Valve.__Valve_2_c
2906
                         BoilerController.ni_5.Valve.ni_19._arrow._first_c
2907
                         BoilerController.ni_6.ControlMode.__ControlMode_2_c
2908
                         BoilerController.ni_6.ControlMode.ni_27._arrow._first_c
2909
                         BoilerController.ni_7.Operator.__Operator_2_c
2910
                         BoilerController.ni_7.Operator.ni_24._arrow._first_c
2911
                         BoilerController.ni_8.Dynamics.__Dynamics_8_c
2912
                         BoilerController.ni_8.Dynamics.ni_26._arrow._first_c
2913
                         BoilerController.ni_9.LevelDefect.__LevelDefect_3_c
2914
                         BoilerController.ni_9.LevelDefect.ni_25._arrow._first_c
2915
                         BoilerController.__BoilerController_4_x
2916
                         BoilerController.__BoilerController_5_x
2917
                         BoilerController.__BoilerController_6_x
2918
                         BoilerController.__BoilerController_7_x
2919
                         BoilerController.__BoilerController_8_x
2920
                         BoilerController.ni_10._arrow._first_x
2921
                         BoilerController.ni_11.SteamDefect.__SteamDefect_3_x
2922
                         BoilerController.ni_11.SteamDefect.ni_20._arrow._first_x
2923
                         BoilerController.ni_12.PumpDefect.__PumpDefect_2_x
2924
                         BoilerController.ni_12.PumpDefect.__PumpDefect_4_x
2925
                         BoilerController.ni_12.PumpDefect.ni_23._arrow._first_x
2926
                         BoilerController.ni_13.PumpDefect.__PumpDefect_2_x
2927
                         BoilerController.ni_13.PumpDefect.__PumpDefect_4_x
2928
                         BoilerController.ni_13.PumpDefect.ni_23._arrow._first_x
2929
                         BoilerController.ni_14.PumpDefect.__PumpDefect_2_x
2930
                         BoilerController.ni_14.PumpDefect.__PumpDefect_4_x
2931
                         BoilerController.ni_14.PumpDefect.ni_23._arrow._first_x
2932
                         BoilerController.ni_15.PumpDefect.__PumpDefect_2_x
2933
                         BoilerController.ni_15.PumpDefect.__PumpDefect_4_x
2934
                         BoilerController.ni_15.PumpDefect.ni_23._arrow._first_x
2935
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_1_x
2936
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_2_x
2937
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_3_x
2938
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_4_x
2939
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_5_x
2940
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_6_x
2941
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_7_x
2942
                         BoilerController.ni_2.PumpsOutput.__PumpsOutput_8_x
2943
                         BoilerController.ni_3.PumpsStatus.__PumpsStatus_1_x
2944
                         BoilerController.ni_3.PumpsStatus.__PumpsStatus_2_x
2945
                         BoilerController.ni_3.PumpsStatus.__PumpsStatus_3_x
2946
                         BoilerController.ni_3.PumpsStatus.__PumpsStatus_4_x
2947
                         BoilerController.ni_3.PumpsStatus.ni_21._arrow._first_x
2948
                         BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_12_x
2949
                         BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_19_x
2950
                         BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_26_x
2951
                         BoilerController.ni_3.PumpsStatus.ni_22.operate_pumps.__operate_pumps_5_x
2952
                         BoilerController.ni_4.PumpsDecision.__PumpsDecision_3_x
2953
                         BoilerController.ni_5.Valve.__Valve_2_x
2954
                         BoilerController.ni_5.Valve.ni_19._arrow._first_x
2955
                         BoilerController.ni_6.ControlMode.__ControlMode_2_x
2956
                         BoilerController.ni_6.ControlMode.ni_27._arrow._first_x
2957
                         BoilerController.ni_7.Operator.__Operator_2_x
2958
                         BoilerController.ni_7.Operator.ni_24._arrow._first_x
2959
                         BoilerController.ni_8.Dynamics.__Dynamics_8_x
2960
                         BoilerController.ni_8.Dynamics.ni_26._arrow._first_x
2961
                         BoilerController.ni_9.LevelDefect.__LevelDefect_3_x
2962
                         BoilerController.ni_9.LevelDefect.ni_25._arrow._first_x)
2963
))
2964

    
2965
; NOT
2966
(declare-var NOT.a_0 Bool)
2967
(declare-var NOT.a_1 Bool)
2968
(declare-var NOT.a_2 Bool)
2969
(declare-var NOT.a_3 Bool)
2970
(declare-var NOT.NOT_0 Bool)
2971
(declare-var NOT.NOT_1 Bool)
2972
(declare-var NOT.NOT_2 Bool)
2973
(declare-var NOT.NOT_3 Bool)
2974
(declare-rel NOT (Bool Bool Bool Bool Bool Bool Bool Bool))
2975
(rule (=> 
2976
  (and (= NOT.NOT_3 (not NOT.a_3))
2977
       (= NOT.NOT_2 (not NOT.a_2))
2978
       (= NOT.NOT_1 (not NOT.a_1))
2979
       (= NOT.NOT_0 (not NOT.a_0))
2980
       )
2981
  (NOT NOT.a_0 NOT.a_1 NOT.a_2 NOT.a_3 NOT.NOT_0 NOT.NOT_1 NOT.NOT_2 NOT.NOT_3)
2982
))
2983

    
2984
; top
2985
(declare-var top.steam_boiler_waiting Bool)
2986
(declare-var top.physical_units_ready Bool)
2987
(declare-var top.stop_request Bool)
2988
(declare-var top.steam Int)
2989
(declare-var top.level_defect Int)
2990
(declare-var top.steam_defect Int)
2991
(declare-var top.pump_defect_0 Int)
2992
(declare-var top.pump_defect_1 Int)
2993
(declare-var top.pump_defect_2 Int)
2994
(declare-var top.pump_defect_3 Int)
2995
(declare-var top.pump_control_defect_0 Int)
2996
(declare-var top.pump_control_defect_1 Int)
2997
(declare-var top.pump_control_defect_2 Int)
2998
(declare-var top.pump_control_defect_3 Int)
2999
(declare-var top.q Int)
3000
(declare-var top.pump_state_0 Int)
3001
(declare-var top.pump_state_1 Int)
3002
(declare-var top.pump_state_2 Int)
3003
(declare-var top.pump_state_3 Int)
3004
(declare-var top.OK Bool)
3005
(declare-var top.__top_3_c Int)
3006
(declare-var top.ni_0._arrow._first_c Bool)
3007
(declare-var top.ni_1.ControlMode.__ControlMode_2_c Int)
3008
(declare-var top.ni_1.ControlMode.ni_27._arrow._first_c Bool)
3009
(declare-var top.__top_3_m Int)
3010
(declare-var top.ni_0._arrow._first_m Bool)
3011
(declare-var top.ni_1.ControlMode.__ControlMode_2_m Int)
3012
(declare-var top.ni_1.ControlMode.ni_27._arrow._first_m Bool)
3013
(declare-var top.__top_3_x Int)
3014
(declare-var top.ni_0._arrow._first_x Bool)
3015
(declare-var top.ni_1.ControlMode.__ControlMode_2_x Int)
3016
(declare-var top.ni_1.ControlMode.ni_27._arrow._first_x Bool)
3017
(declare-var top.__top_1 Bool)
3018
(declare-var top.__top_2 Bool)
3019
(declare-var top.mode_normal_then_no_stop_request Bool)
3020
(declare-var top.mode_normal_then_water_level_ok Bool)
3021
(declare-var top.op_mode Int)
3022
(declare-rel top_reset (Int Bool Int Bool Int Bool Int Bool))
3023
(declare-rel top_step (Bool Bool Bool Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Bool Int Bool Int Bool Int Bool Int Bool))
3024

    
3025
(rule (=> 
3026
  (and 
3027
       (= top.__top_3_m top.__top_3_c)
3028
       (ControlMode_reset top.ni_1.ControlMode.__ControlMode_2_c
3029
                          top.ni_1.ControlMode.ni_27._arrow._first_c
3030
                          top.ni_1.ControlMode.__ControlMode_2_m
3031
                          top.ni_1.ControlMode.ni_27._arrow._first_m)
3032
       (= top.ni_0._arrow._first_m true)
3033
  )
3034
  (top_reset top.__top_3_c
3035
             top.ni_0._arrow._first_c
3036
             top.ni_1.ControlMode.__ControlMode_2_c
3037
             top.ni_1.ControlMode.ni_27._arrow._first_c
3038
             top.__top_3_m
3039
             top.ni_0._arrow._first_m
3040
             top.ni_1.ControlMode.__ControlMode_2_m
3041
             top.ni_1.ControlMode.ni_27._arrow._first_m)
3042
))
3043

    
3044
(rule (=> 
3045
  (and (and (= top.ni_1.ControlMode.__ControlMode_2_m top.ni_1.ControlMode.__ControlMode_2_c)
3046
            (= top.ni_1.ControlMode.ni_27._arrow._first_m top.ni_1.ControlMode.ni_27._arrow._first_c)
3047
            )
3048
       (ControlMode_step top.steam_boiler_waiting
3049
                         top.physical_units_ready
3050
                         top.stop_request
3051
                         top.steam
3052
                         top.level_defect
3053
                         top.steam_defect
3054
                         top.pump_defect_0
3055
                         top.pump_defect_1
3056
                         top.pump_defect_2
3057
                         top.pump_defect_3
3058
                         top.pump_control_defect_0
3059
                         top.pump_control_defect_1
3060
                         top.pump_control_defect_2
3061
                         top.pump_control_defect_3
3062
                         top.q
3063
                         top.pump_state_0
3064
                         top.pump_state_1
3065
                         top.pump_state_2
3066
                         top.pump_state_3
3067
                         top.op_mode
3068
                         top.ni_1.ControlMode.__ControlMode_2_m
3069
                         top.ni_1.ControlMode.ni_27._arrow._first_m
3070
                         top.ni_1.ControlMode.__ControlMode_2_x
3071
                         top.ni_1.ControlMode.ni_27._arrow._first_x)
3072
       (dangerous_level top.q
3073
                        top.__top_2)
3074
       (= top.ni_0._arrow._first_m top.ni_0._arrow._first_c)(and (= top.__top_1 (ite top.ni_0._arrow._first_m true false))
3075
                                                                 (= top.ni_0._arrow._first_x false))
3076
       (and (or (not (= top.__top_1 true))
3077
               (= top.mode_normal_then_water_level_ok true))
3078
            (or (not (= top.__top_1 false))
3079
               (= top.mode_normal_then_water_level_ok (=> (and (= top.op_mode 3) (= top.__top_3_c 3)) (not top.__top_2))))
3080
       )
3081
       (= top.mode_normal_then_no_stop_request (=> (= top.op_mode 3) (not top.stop_request)))
3082
       (= top.__top_3_x top.op_mode)
3083
       (= top.OK (and top.mode_normal_then_water_level_ok top.mode_normal_then_no_stop_request))
3084
       )
3085
  (top_step top.steam_boiler_waiting
3086
            top.physical_units_ready
3087
            top.stop_request
3088
            top.steam
3089
            top.level_defect
3090
            top.steam_defect
3091
            top.pump_defect_0
3092
            top.pump_defect_1
3093
            top.pump_defect_2
3094
            top.pump_defect_3
3095
            top.pump_control_defect_0
3096
            top.pump_control_defect_1
3097
            top.pump_control_defect_2
3098
            top.pump_control_defect_3
3099
            top.q
3100
            top.pump_state_0
3101
            top.pump_state_1
3102
            top.pump_state_2
3103
            top.pump_state_3
3104
            top.OK
3105
            top.__top_3_c
3106
            top.ni_0._arrow._first_c
3107
            top.ni_1.ControlMode.__ControlMode_2_c
3108
            top.ni_1.ControlMode.ni_27._arrow._first_c
3109
            top.__top_3_x
3110
            top.ni_0._arrow._first_x
3111
            top.ni_1.ControlMode.__ControlMode_2_x
3112
            top.ni_1.ControlMode.ni_27._arrow._first_x)
3113
))
3114

    
3115
; Collecting semantics for node top
3116

    
3117
(declare-rel MAIN (Int Bool Int Bool Bool))
3118
; Initial set: Reset(c,m) + One Step(m,x) 
3119
(declare-rel INIT_STATE ())
3120
(rule INIT_STATE)
3121
(rule (=> 
3122
  (and INIT_STATE
3123
       (top_reset top.__top_3_c top.ni_0._arrow._first_c top.ni_1.ControlMode.__ControlMode_2_c top.ni_1.ControlMode.ni_27._arrow._first_c top.__top_3_m top.ni_0._arrow._first_m top.ni_1.ControlMode.__ControlMode_2_m top.ni_1.ControlMode.ni_27._arrow._first_m)
3124
       (top_step top.steam_boiler_waiting top.physical_units_ready top.stop_request top.steam top.level_defect top.steam_defect top.pump_defect_0 top.pump_defect_1 top.pump_defect_2 top.pump_defect_3 top.pump_control_defect_0 top.pump_control_defect_1 top.pump_control_defect_2 top.pump_control_defect_3 top.q top.pump_state_0 top.pump_state_1 top.pump_state_2 top.pump_state_3 top.OK top.__top_3_m top.ni_0._arrow._first_m top.ni_1.ControlMode.__ControlMode_2_m top.ni_1.ControlMode.ni_27._arrow._first_m top.__top_3_x top.ni_0._arrow._first_x top.ni_1.ControlMode.__ControlMode_2_x top.ni_1.ControlMode.ni_27._arrow._first_x)
3125
  )
3126
  (MAIN top.__top_3_x top.ni_0._arrow._first_x top.ni_1.ControlMode.__ControlMode_2_x top.ni_1.ControlMode.ni_27._arrow._first_x top.OK)
3127
))
3128

    
3129
; Inductive def
3130
(declare-var dummytop.OK Bool)
3131
(rule (=> 
3132
  (and (MAIN top.__top_3_c top.ni_0._arrow._first_c top.ni_1.ControlMode.__ControlMode_2_c top.ni_1.ControlMode.ni_27._arrow._first_c dummytop.OK)
3133
       (top_step top.steam_boiler_waiting top.physical_units_ready top.stop_request top.steam top.level_defect top.steam_defect top.pump_defect_0 top.pump_defect_1 top.pump_defect_2 top.pump_defect_3 top.pump_control_defect_0 top.pump_control_defect_1 top.pump_control_defect_2 top.pump_control_defect_3 top.q top.pump_state_0 top.pump_state_1 top.pump_state_2 top.pump_state_3 top.OK top.__top_3_c top.ni_0._arrow._first_c top.ni_1.ControlMode.__ControlMode_2_c top.ni_1.ControlMode.ni_27._arrow._first_c top.__top_3_x top.ni_0._arrow._first_x top.ni_1.ControlMode.__ControlMode_2_x top.ni_1.ControlMode.ni_27._arrow._first_x)
3134
  )
3135
  (MAIN top.__top_3_x top.ni_0._arrow._first_x top.ni_1.ControlMode.__ControlMode_2_x top.ni_1.ControlMode.ni_27._arrow._first_x top.OK)
3136
))
3137

    
3138
; Property def
3139
(declare-rel ERR ())
3140
(rule (=> 
3141
  (and (not top.OK)
3142
       (MAIN top.__top_3_x top.ni_0._arrow._first_x top.ni_1.ControlMode.__ControlMode_2_x top.ni_1.ControlMode.ni_27._arrow._first_x top.OK))
3143
  ERR))
3144
(query ERR)