Project

General

Profile

Revision 7d3c8bd3

View differences:

regression_tests/lustre_files/success/kind_fmcad08/CMakeLists.txt
1
cmake_minimum_required(VERSION 2.8.4)
2

  
3
add_subdirectory(large)
regression_tests/lustre_files/success/kind_fmcad08/large/src/BROKEN/steam_boiler_no_arr1.h
1
/* C code generated by lustrec
2
   Version number 1.3-458
3
   Code is C99 compliant
4
   Using (double) floating-point numbers */
5
   
6
#ifndef _STEAM_BOILER_NO_ARR1
7
#define _STEAM_BOILER_NO_ARR1
8

  
9
/* Imports standard library */
10
#include "/usr/local/include/lustrec/arrow.h"
11

  
12

  
13
/* Import dependencies */
14

  
15
/* Types definitions */
16

  
17
/* Global constant (declarations, definitions are in C file) */
18

  
19
/* Structs declarations */
20
struct top_mem;
21
struct Verification_mem;
22
struct BoilerController_mem;
23
struct FEDGE2_mem;
24
struct FEDGE1_mem;
25
struct Valve_mem;
26
struct SteamDefect_mem;
27
struct PumpsStatus_mem;
28
struct PumpsOutput_mem;
29
struct PumpsDecision_mem;
30
struct PumpDefect_mem;
31
struct Operator_mem;
32
struct LevelDefect_mem;
33
struct Dynamics_mem;
34
struct ControlMode_mem;
35
struct REDGE_mem;
36
struct operate_pumps_mem;
37

  
38
/* Nodes declarations */
39
extern void top_reset (struct top_mem *self);
40

  
41
extern void top_init (struct top_mem *self);
42

  
43
extern void top_clear (struct top_mem *self);
44

  
45
extern void top_step (_Bool stop, _Bool steam_boiler_waiting,
46
                      _Bool physical_units_ready, int level, int steam,
47
                      int pump_state_0, int pump_state_1, int pump_state_2,
48
                      int pump_state_3, _Bool pump_control_state_0,
49
                      _Bool pump_control_state_1, _Bool pump_control_state_2,
50
                      _Bool pump_control_state_3, _Bool pump_repaired_0,
51
                      _Bool pump_repaired_1, _Bool pump_repaired_2,
52
                      _Bool pump_repaired_3, _Bool pump_control_repaired_0,
53
                      _Bool pump_control_repaired_1,
54
                      _Bool pump_control_repaired_2,
55
                      _Bool pump_control_repaired_3, _Bool level_repaired,
56
                      _Bool steam_repaired,
57
                      _Bool pump_failure_acknowledgement_0,
58
                      _Bool pump_failure_acknowledgement_1,
59
                      _Bool pump_failure_acknowledgement_2,
60
                      _Bool pump_failure_acknowledgement_3,
61
                      _Bool pump_control_failure_acknowledgement_0,
62
                      _Bool pump_control_failure_acknowledgement_1,
63
                      _Bool pump_control_failure_acknowledgement_2,
64
                      _Bool pump_control_failure_acknowledgement_3,
65
                      _Bool level_failure_acknowledgement,
66
                      _Bool steam_failure_acknowledgement, 
67
                      _Bool (*OK),
68
                      struct top_mem *self);
69

  
70
extern void NOT_step (_Bool a_0, _Bool a_1, _Bool a_2, _Bool a_3, 
71
                      _Bool (*NOT_0), _Bool (*NOT_1), _Bool (*NOT_2),
72
                      _Bool (*NOT_3)
73
                      );
74

  
75
extern void Verification_reset (struct Verification_mem *self);
76

  
77
extern void Verification_init (struct Verification_mem *self);
78

  
79
extern void Verification_clear (struct Verification_mem *self);
80

  
81
extern void Verification_step (_Bool S1, _Bool S2, 
82
                               _Bool (*property_ok),
83
                               struct Verification_mem *self);
84

  
85
extern void BoilerController_reset (struct BoilerController_mem *self);
86

  
87
extern void BoilerController_init (struct BoilerController_mem *self);
88

  
89
extern void BoilerController_clear (struct BoilerController_mem *self);
90

  
91
extern void BoilerController_step (_Bool stop, _Bool steam_boiler_waiting,
92
                                   _Bool physical_units_ready, int level,
93
                                   int steam, int pump_state_0,
94
                                   int pump_state_1, int pump_state_2,
95
                                   int pump_state_3,
96
                                   _Bool pump_control_state_0,
97
                                   _Bool pump_control_state_1,
98
                                   _Bool pump_control_state_2,
99
                                   _Bool pump_control_state_3,
100
                                   _Bool pump_repaired_0,
101
                                   _Bool pump_repaired_1,
102
                                   _Bool pump_repaired_2,
103
                                   _Bool pump_repaired_3,
104
                                   _Bool pump_control_repaired_0,
105
                                   _Bool pump_control_repaired_1,
106
                                   _Bool pump_control_repaired_2,
107
                                   _Bool pump_control_repaired_3,
108
                                   _Bool level_repaired,
109
                                   _Bool steam_repaired,
110
                                   _Bool pump_failure_acknowledgement_0,
111
                                   _Bool pump_failure_acknowledgement_1,
112
                                   _Bool pump_failure_acknowledgement_2,
113
                                   _Bool pump_failure_acknowledgement_3,
114
                                   _Bool pump_control_failure_acknowledgement_0,
115
                                   _Bool pump_control_failure_acknowledgement_1,
116
                                   _Bool pump_control_failure_acknowledgement_2,
117
                                   _Bool pump_control_failure_acknowledgement_3,
118
                                   _Bool level_failure_acknowledgement,
119
                                   _Bool steam_failure_acknowledgement, 
120
                                   _Bool (*program_ready), int (*mode),
121
                                   _Bool (*valve), _Bool (*open_pump_0),
122
                                   _Bool (*open_pump_1),
123
                                   _Bool (*open_pump_2),
124
                                   _Bool (*open_pump_3),
125
                                   _Bool (*close_pump_0),
126
                                   _Bool (*close_pump_1),
127
                                   _Bool (*close_pump_2),
128
                                   _Bool (*close_pump_3),
129
                                   _Bool (*pump_failure_detection_0),
130
                                   _Bool (*pump_failure_detection_1),
131
                                   _Bool (*pump_failure_detection_2),
132
                                   _Bool (*pump_failure_detection_3),
133
                                   _Bool (*pump_control_failure_detection_0),
134
                                   _Bool (*pump_control_failure_detection_1),
135
                                   _Bool (*pump_control_failure_detection_2),
136
                                   _Bool (*pump_control_failure_detection_3),
137
                                   _Bool (*level_failure_detection),
138
                                   _Bool (*steam_outcome_failure_detection),
139
                                   _Bool (*pump_repaired_acknowledgement_0),
140
                                   _Bool (*pump_repaired_acknowledgement_1),
141
                                   _Bool (*pump_repaired_acknowledgement_2),
142
                                   _Bool (*pump_repaired_acknowledgement_3),
143
                                   _Bool (*pump_control_repaired_acknowledgement_0),
144
                                   _Bool (*pump_control_repaired_acknowledgement_1),
145
                                   _Bool (*pump_control_repaired_acknowledgement_2),
146
                                   _Bool (*pump_control_repaired_acknowledgement_3),
147
                                   _Bool (*level_repaired_acknowledgement),
148
                                   _Bool (*steam_outcome_repaired_acknowledgement),
149
                                   struct BoilerController_mem *self);
150

  
151
extern void FEDGE2_reset (struct FEDGE2_mem *self);
152

  
153
extern void FEDGE2_init (struct FEDGE2_mem *self);
154

  
155
extern void FEDGE2_clear (struct FEDGE2_mem *self);
156

  
157
extern void FEDGE2_step (_Bool S, 
158
                         _Bool (*FEDGE2),
159
                         struct FEDGE2_mem *self);
160

  
161
extern void FEDGE1_reset (struct FEDGE1_mem *self);
162

  
163
extern void FEDGE1_init (struct FEDGE1_mem *self);
164

  
165
extern void FEDGE1_clear (struct FEDGE1_mem *self);
166

  
167
extern void FEDGE1_step (_Bool S, 
168
                         _Bool (*FEDGE1),
169
                         struct FEDGE1_mem *self);
170

  
171
extern void Valve_reset (struct Valve_mem *self);
172

  
173
extern void Valve_init (struct Valve_mem *self);
174

  
175
extern void Valve_clear (struct Valve_mem *self);
176

  
177
extern void Valve_step (int op_mode, int q, 
178
                        _Bool (*valve), int (*valve_state),
179
                        struct Valve_mem *self);
180

  
181
extern void SteamOutput_step (int op_mode, int steam_defect,
182
                              _Bool steam_repaired, 
183
                              _Bool (*steam_outcome_failure_detection),
184
                              _Bool (*steam_outcome_repaired_acknowledgement)
185
                              );
186

  
187
extern void SteamDefect_reset (struct SteamDefect_mem *self);
188

  
189
extern void SteamDefect_init (struct SteamDefect_mem *self);
190

  
191
extern void SteamDefect_clear (struct SteamDefect_mem *self);
192

  
193
extern void SteamDefect_step (_Bool steam_failure_acknowledgement,
194
                              _Bool steam_repaired, int steam, 
195
                              int (*SteamDefect),
196
                              struct SteamDefect_mem *self);
197

  
198
extern void PumpsStatus_reset (struct PumpsStatus_mem *self);
199

  
200
extern void PumpsStatus_init (struct PumpsStatus_mem *self);
201

  
202
extern void PumpsStatus_clear (struct PumpsStatus_mem *self);
203

  
204
extern void PumpsStatus_step (int n_pumps, int pump_defect_0,
205
                              int pump_defect_1, int pump_defect_2,
206
                              int pump_defect_3, _Bool flow_0, _Bool flow_1,
207
                              _Bool flow_2, _Bool flow_3, 
208
                              int (*pump_status_0), int (*pump_status_1),
209
                              int (*pump_status_2), int (*pump_status_3),
210
                              struct PumpsStatus_mem *self);
211

  
212
extern void PumpsOutput_reset (struct PumpsOutput_mem *self);
213

  
214
extern void PumpsOutput_init (struct PumpsOutput_mem *self);
215

  
216
extern void PumpsOutput_clear (struct PumpsOutput_mem *self);
217

  
218
extern void PumpsOutput_step (int op_mode, int pump_status_0,
219
                              int pump_status_1, int pump_status_2,
220
                              int pump_status_3, int pump_defect_0,
221
                              int pump_defect_1, int pump_defect_2,
222
                              int pump_defect_3, int pump_control_defect_0,
223
                              int pump_control_defect_1,
224
                              int pump_control_defect_2,
225
                              int pump_control_defect_3,
226
                              _Bool pump_repaired_0, _Bool pump_repaired_1,
227
                              _Bool pump_repaired_2, _Bool pump_repaired_3,
228
                              _Bool pump_control_repaired_0,
229
                              _Bool pump_control_repaired_1,
230
                              _Bool pump_control_repaired_2,
231
                              _Bool pump_control_repaired_3, 
232
                              _Bool (*open_pump_0), _Bool (*open_pump_1),
233
                              _Bool (*open_pump_2), _Bool (*open_pump_3),
234
                              _Bool (*close_pump_0), _Bool (*close_pump_1),
235
                              _Bool (*close_pump_2), _Bool (*close_pump_3),
236
                              _Bool (*pump_failure_detection_0),
237
                              _Bool (*pump_failure_detection_1),
238
                              _Bool (*pump_failure_detection_2),
239
                              _Bool (*pump_failure_detection_3),
240
                              _Bool (*pump_repaired_acknowledgement_0),
241
                              _Bool (*pump_repaired_acknowledgement_1),
242
                              _Bool (*pump_repaired_acknowledgement_2),
243
                              _Bool (*pump_repaired_acknowledgement_3),
244
                              _Bool (*pump_control_failure_detection_0),
245
                              _Bool (*pump_control_failure_detection_1),
246
                              _Bool (*pump_control_failure_detection_2),
247
                              _Bool (*pump_control_failure_detection_3),
248
                              _Bool (*pump_control_repaired_acknowledgement_0),
249
                              _Bool (*pump_control_repaired_acknowledgement_1),
250
                              _Bool (*pump_control_repaired_acknowledgement_2),
251
                              _Bool (*pump_control_repaired_acknowledgement_3),
252
                              struct PumpsOutput_mem *self);
253

  
254
extern void PumpsDecision_reset (struct PumpsDecision_mem *self);
255

  
256
extern void PumpsDecision_init (struct PumpsDecision_mem *self);
257

  
258
extern void PumpsDecision_clear (struct PumpsDecision_mem *self);
259

  
260
extern void PumpsDecision_step (int q, int v, 
261
                                int (*n_pumps),
262
                                struct PumpsDecision_mem *self);
263

  
264
extern void PumpDefect_reset (struct PumpDefect_mem *self);
265

  
266
extern void PumpDefect_init (struct PumpDefect_mem *self);
267

  
268
extern void PumpDefect_clear (struct PumpDefect_mem *self);
269

  
270
extern void PumpDefect_step (_Bool pump_failure_acknowledgement,
271
                             _Bool pump_repaired,
272
                             _Bool pump_control_failure_acknowledgement,
273
                             _Bool pump_control_repaired, int pump_status,
274
                             int pump_state, _Bool pump_control_state, 
275
                             int (*PumpDefect), int (*PumpControlDefect),
276
                             _Bool (*Flow),
277
                             struct PumpDefect_mem *self);
278

  
279
extern void Operator_reset (struct Operator_mem *self);
280

  
281
extern void Operator_init (struct Operator_mem *self);
282

  
283
extern void Operator_clear (struct Operator_mem *self);
284

  
285
extern void Operator_step (_Bool stop, 
286
                           _Bool (*stop_request),
287
                           struct Operator_mem *self);
288

  
289
extern void LevelOutput_step (int op_mode, int level_defect,
290
                              _Bool level_repaired, 
291
                              _Bool (*level_outcome_failure_detection),
292
                              _Bool (*level_outcome_repaired_acknowledgement)
293
                              );
294

  
295
extern void LevelDefect_reset (struct LevelDefect_mem *self);
296

  
297
extern void LevelDefect_init (struct LevelDefect_mem *self);
298

  
299
extern void LevelDefect_clear (struct LevelDefect_mem *self);
300

  
301
extern void LevelDefect_step (_Bool level_failure_acknowledgement,
302
                              _Bool level_repaired, int level, 
303
                              int (*LevelDefect),
304
                              struct LevelDefect_mem *self);
305

  
306
extern void Dynamics_reset (struct Dynamics_mem *self);
307

  
308
extern void Dynamics_init (struct Dynamics_mem *self);
309

  
310
extern void Dynamics_clear (struct Dynamics_mem *self);
311

  
312
extern void Dynamics_step (int valve_state, int level, int steam,
313
                           int level_defect, int steam_defect, _Bool flow_0,
314
                           _Bool flow_1, _Bool flow_2, _Bool flow_3, 
315
                           int (*q), int (*v), int (*p_0), int (*p_1),
316
                           int (*p_2), int (*p_3),
317
                           struct Dynamics_mem *self);
318

  
319
extern void ControlOutput_step (int op_mode, int level, _Bool valve, 
320
                                _Bool (*program_ready), int (*mode)
321
                                );
322

  
323
extern void ControlMode_reset (struct ControlMode_mem *self);
324

  
325
extern void ControlMode_init (struct ControlMode_mem *self);
326

  
327
extern void ControlMode_clear (struct ControlMode_mem *self);
328

  
329
extern void ControlMode_step (_Bool steam_boiler_waiting,
330
                              _Bool physical_units_ready, _Bool stop_request,
331
                              int steam, int level_defect, int steam_defect,
332
                              int pump_defect_0, int pump_defect_1,
333
                              int pump_defect_2, int pump_defect_3,
334
                              int pump_control_defect_0,
335
                              int pump_control_defect_1,
336
                              int pump_control_defect_2,
337
                              int pump_control_defect_3, int q,
338
                              int pump_state_0, int pump_state_1,
339
                              int pump_state_2, int pump_state_3, 
340
                              int (*op_mode),
341
                              struct ControlMode_mem *self);
342

  
343
extern void REDGE_reset (struct REDGE_mem *self);
344

  
345
extern void REDGE_init (struct REDGE_mem *self);
346

  
347
extern void REDGE_clear (struct REDGE_mem *self);
348

  
349
extern void REDGE_step (_Bool S, 
350
                        _Bool (*REDGE),
351
                        struct REDGE_mem *self);
352

  
353
extern void steam_failure_detect_step (int steam, 
354
                                       _Bool (*steam_failure_detect)
355
                                       );
356

  
357
extern void operate_pumps_reset (struct operate_pumps_mem *self);
358

  
359
extern void operate_pumps_init (struct operate_pumps_mem *self);
360

  
361
extern void operate_pumps_clear (struct operate_pumps_mem *self);
362

  
363
extern void operate_pumps_step (int n, int n_pumps_to_open,
364
                                int pump_status_0, int pump_status_1,
365
                                int pump_status_2, int pump_status_3,
366
                                int pump_defect_0, int pump_defect_1,
367
                                int pump_defect_2, int pump_defect_3,
368
                                _Bool flow_0, _Bool flow_1, _Bool flow_2,
369
                                _Bool flow_3, 
370
                                int (*operate_pumps_0),
371
                                int (*operate_pumps_1),
372
                                int (*operate_pumps_2),
373
                                int (*operate_pumps_3),
374
                                struct operate_pumps_mem *self);
375

  
376
extern void pump_failure_detect_step (int pump_status, int pump_state,
377
                                      _Bool pump_control_state, 
378
                                      _Bool (*pump_failure_detect),
379
                                      _Bool (*pump_control_failure_detect),
380
                                      _Bool (*flow)
381
                                      );
382

  
383
extern void level_failure_detect_step (int level, 
384
                                       _Bool (*level_failure_detect)
385
                                       );
386

  
387
extern void Defect_step (int statein, _Bool fail_cond, _Bool ack_chan,
388
                         _Bool repair_chan, 
389
                         int (*stateout)
390
                         );
391

  
392
extern void sum_step (int a_0, int a_1, int a_2, int a_3, 
393
                      int (*sum)
394
                      );
395

  
396
extern void initialization_complete_step (int op_mode, int level,
397
                                          _Bool valve, 
398
                                          _Bool (*initialization_complete)
399
                                          );
400

  
401
extern void failure_step (int level_defect, int steam_defect,
402
                          int pump_defect_0, int pump_defect_1,
403
                          int pump_defect_2, int pump_defect_3,
404
                          int pump_control_defect_0,
405
                          int pump_control_defect_1,
406
                          int pump_control_defect_2,
407
                          int pump_control_defect_3, 
408
                          _Bool (*failure)
409
                          );
410

  
411
extern void critical_failure_step (int op_mode, int steam, int level_defect,
412
                                   int steam_defect, int pump_defect_0,
413
                                   int pump_defect_1, int pump_defect_2,
414
                                   int pump_defect_3, int q,
415
                                   int pump_state_0, int pump_state_1,
416
                                   int pump_state_2, int pump_state_3, 
417
                                   _Bool (*critical_failure)
418
                                   );
419

  
420
extern void pump_control_failure_step (int pump_defect, 
421
                                       _Bool (*pump_failure)
422
                                       );
423

  
424
extern void OR_step (_Bool a_0, _Bool a_1, _Bool a_2, _Bool a_3, 
425
                     _Bool (*OR)
426
                     );
427

  
428
extern void transmission_failure_step (int pump_state_0, int pump_state_1,
429
                                       int pump_state_2, int pump_state_3, 
430
                                       _Bool (*transmission_failure)
431
                                       );
432

  
433
extern void steam_failure_startup_step (int steam, 
434
                                        _Bool (*steam_failure_startup)
435
                                        );
436

  
437
extern void steam_failure_step (int steam_defect, 
438
                                _Bool (*steam_failure)
439
                                );
440

  
441
extern void pump_failure_step (int pump_defect, 
442
                               _Bool (*pump_failure)
443
                               );
444

  
445
extern void level_failure_step (int level_defect, 
446
                                _Bool (*level_failure)
447
                                );
448

  
449
extern void dangerous_level_step (int q, 
450
                                  _Bool (*dangerous_level)
451
                                  );
452

  
453
extern void AND_step (_Bool a_0, _Bool a_1, _Bool a_2, _Bool a_3, 
454
                      _Bool (*AND)
455
                      );
456

  
457

  
458
#endif
459

  
regression_tests/lustre_files/success/kind_fmcad08/large/src/BROKEN/steam_boiler_no_arr1.smt2
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
; critical_failure
92
(declare-var critical_failure.op_mode Int)
93
(declare-var critical_failure.steam Int)
94
(declare-var critical_failure.level_defect Int)
95
(declare-var critical_failure.steam_defect Int)
96
(declare-var critical_failure.pump_defect_0 Int)
97
(declare-var critical_failure.pump_defect_1 Int)
98
(declare-var critical_failure.pump_defect_2 Int)
99
(declare-var critical_failure.pump_defect_3 Int)
100
(declare-var critical_failure.q Int)
101
(declare-var critical_failure.pump_state_0 Int)
102
(declare-var critical_failure.pump_state_1 Int)
103
(declare-var critical_failure.pump_state_2 Int)
104
(declare-var critical_failure.pump_state_3 Int)
105
(declare-var critical_failure.critical_failure Bool)
106
(declare-var critical_failure.__critical_failure_1 Bool)
107
(declare-var critical_failure.__critical_failure_10 Bool)
108
(declare-var critical_failure.__critical_failure_2 Bool)
109
(declare-var critical_failure.__critical_failure_3 Bool)
110
(declare-var critical_failure.__critical_failure_4 Bool)
111
(declare-var critical_failure.__critical_failure_5 Bool)
112
(declare-var critical_failure.__critical_failure_6 Bool)
113
(declare-var critical_failure.__critical_failure_7 Bool)
114
(declare-var critical_failure.__critical_failure_8 Bool)
115
(declare-var critical_failure.__critical_failure_9 Bool)
116
(declare-rel critical_failure (Int Int Int Int Int Int Int Int Int Int Int Int Int Bool))
117
(rule (=> 
118
  (and (steam_failure_startup critical_failure.steam
119
                              critical_failure.__critical_failure_9)
120
       (level_failure critical_failure.level_defect
121
                      critical_failure.__critical_failure_8)
122
       (dangerous_level critical_failure.q
123
                        critical_failure.__critical_failure_7)
124
       (steam_failure critical_failure.steam_defect
125
                      critical_failure.__critical_failure_6)
126
       (pump_failure critical_failure.pump_defect_0
127
                     critical_failure.__critical_failure_4)
128
       (pump_failure critical_failure.pump_defect_1
129
                     critical_failure.__critical_failure_3)
130
       (pump_failure critical_failure.pump_defect_2
131
                     critical_failure.__critical_failure_2)
132
       (pump_failure critical_failure.pump_defect_3
133
                     critical_failure.__critical_failure_1)
134
       (AND critical_failure.__critical_failure_4
135
            critical_failure.__critical_failure_3
136
            critical_failure.__critical_failure_2
137
            critical_failure.__critical_failure_1
138
            critical_failure.__critical_failure_5)
139
       (transmission_failure critical_failure.pump_state_0
140
                             critical_failure.pump_state_1
141
                             critical_failure.pump_state_2
142
                             critical_failure.pump_state_3
143
                             critical_failure.__critical_failure_10)
144
       (= 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))))
145
       )
146
  (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)
147
))
148

  
149
; failure
150
(declare-var failure.level_defect Int)
151
(declare-var failure.steam_defect Int)
152
(declare-var failure.pump_defect_0 Int)
153
(declare-var failure.pump_defect_1 Int)
154
(declare-var failure.pump_defect_2 Int)
155
(declare-var failure.pump_defect_3 Int)
156
(declare-var failure.pump_control_defect_0 Int)
157
(declare-var failure.pump_control_defect_1 Int)
158
(declare-var failure.pump_control_defect_2 Int)
159
(declare-var failure.pump_control_defect_3 Int)
160
(declare-var failure.failure Bool)
161
(declare-var failure.__failure_1 Bool)
162
(declare-var failure.__failure_10 Bool)
163
(declare-var failure.__failure_11 Bool)
164
(declare-var failure.__failure_12 Bool)
165
(declare-var failure.__failure_2 Bool)
166
(declare-var failure.__failure_3 Bool)
167
(declare-var failure.__failure_4 Bool)
168
(declare-var failure.__failure_5 Bool)
169
(declare-var failure.__failure_6 Bool)
170
(declare-var failure.__failure_7 Bool)
171
(declare-var failure.__failure_8 Bool)
172
(declare-var failure.__failure_9 Bool)
173
(declare-rel failure (Int Int Int Int Int Int Int Int Int Int Bool))
174
(rule (=> 
175
  (and (pump_failure failure.pump_defect_0
176
                     failure.__failure_9)
177
       (pump_failure failure.pump_defect_1
178
                     failure.__failure_8)
179
       (pump_failure failure.pump_defect_2
180
                     failure.__failure_7)
181
       (pump_failure failure.pump_defect_3
182
                     failure.__failure_6)
183
       (pump_control_failure failure.pump_control_defect_0
184
                             failure.__failure_4)
185
       (pump_control_failure failure.pump_control_defect_1
186
                             failure.__failure_3)
187
       (pump_control_failure failure.pump_control_defect_2
188
                             failure.__failure_2)
189
       (pump_control_failure failure.pump_control_defect_3
190
                             failure.__failure_1)
191
       (OR failure.__failure_4
192
           failure.__failure_3
193
           failure.__failure_2
194
           failure.__failure_1
195
           failure.__failure_5)
196
       (level_failure failure.level_defect
197
                      failure.__failure_12)
198
       (steam_failure failure.steam_defect
199
                      failure.__failure_11)
200
       (OR failure.__failure_9
201
           failure.__failure_8
202
           failure.__failure_7
203
           failure.__failure_6
204
           failure.__failure_10)
205
       (= failure.failure (or (or (or failure.__failure_12 failure.__failure_11) failure.__failure_10) failure.__failure_5))
206
       )
207
  (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)
208
))
209

  
210
; initialization_complete
211
(declare-var initialization_complete.op_mode Int)
212
(declare-var initialization_complete.level Int)
213
(declare-var initialization_complete.valve Bool)
214
(declare-var initialization_complete.initialization_complete Bool)
215
(declare-rel initialization_complete (Int Int Bool Bool))
216
(rule (=> 
217
  (= initialization_complete.initialization_complete (and (and (= initialization_complete.op_mode 2) (and (<= 400 initialization_complete.level) (<= initialization_complete.level 600))) (not initialization_complete.valve)))
218
  (initialization_complete initialization_complete.op_mode initialization_complete.level initialization_complete.valve initialization_complete.initialization_complete)
219
))
220

  
221
; sum
222
(declare-var sum.a_0 Int)
223
(declare-var sum.a_1 Int)
224
(declare-var sum.a_2 Int)
225
(declare-var sum.a_3 Int)
226
(declare-var sum.sum Int)
227
(declare-rel sum (Int Int Int Int Int))
228
(rule (=> 
229
  (= sum.sum (+ (+ (+ sum.a_0 sum.a_1) sum.a_2) sum.a_3))
230
  (sum sum.a_0 sum.a_1 sum.a_2 sum.a_3 sum.sum)
231
))
232

  
233
; Defect
234
(declare-var Defect.statein Int)
235
(declare-var Defect.fail_cond Bool)
236
(declare-var Defect.ack_chan Bool)
237
(declare-var Defect.repair_chan Bool)
238
(declare-var Defect.stateout Int)
239
(declare-var Defect.__Defect_1 Bool)
240
(declare-var Defect.__Defect_2 Bool)
241
(declare-rel Defect (Int Bool Bool Bool Int))
242
(rule (=> 
243
  (and (= Defect.__Defect_2 (= Defect.statein 1))
244
       (= Defect.__Defect_1 (= Defect.statein 0))
245
       (and (or (not (= Defect.__Defect_1 true))
246
               (and (or (not (= Defect.fail_cond true))
247
                       (= Defect.stateout 1))
248
                    (or (not (= Defect.fail_cond false))
249
                       (= Defect.stateout 0))
250
               ))
251
            (or (not (= Defect.__Defect_1 false))
252
               (and (or (not (= Defect.__Defect_2 true))
253
                       (and (or (not (= Defect.ack_chan true))
254
                               (= Defect.stateout 2))
255
                            (or (not (= Defect.ack_chan false))
256
                               (= Defect.stateout 1))
257
                       ))
258
                    (or (not (= Defect.__Defect_2 false))
259
                       (and (or (not (= Defect.repair_chan true))
260
                               (= Defect.stateout 0))
261
                            (or (not (= Defect.repair_chan false))
262
                               (= Defect.stateout 2))
263
                       ))
264
               ))
265
       )
266
       )
267
  (Defect Defect.statein Defect.fail_cond Defect.ack_chan Defect.repair_chan Defect.stateout)
268
))
269

  
270
; level_failure_detect
271
(declare-var level_failure_detect.level Int)
272
(declare-var level_failure_detect.level_failure_detect Bool)
273
(declare-rel level_failure_detect (Int Bool))
274
(rule (=> 
275
  (= level_failure_detect.level_failure_detect (or (< level_failure_detect.level 0) (> level_failure_detect.level 1000)))
276
  (level_failure_detect level_failure_detect.level level_failure_detect.level_failure_detect)
277
))
278

  
279
; pump_failure_detect
280
(declare-var pump_failure_detect.pump_status Int)
281
(declare-var pump_failure_detect.pump_state Int)
282
(declare-var pump_failure_detect.pump_control_state Bool)
283
(declare-var pump_failure_detect.pump_failure_detect Bool)
284
(declare-var pump_failure_detect.pump_control_failure_detect Bool)
285
(declare-var pump_failure_detect.flow Bool)
286
(declare-rel pump_failure_detect (Int Int Bool Bool Bool Bool))
287
(rule (=> 
288
  (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))))
289
       (= 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)))
290
       (= 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))))
291
       )
292
  (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)
293
))
294

  
295
; operate_pumps
296
(declare-var operate_pumps.n Int)
297
(declare-var operate_pumps.n_pumps_to_open Int)
298
(declare-var operate_pumps.pump_status_0 Int)
299
(declare-var operate_pumps.pump_status_1 Int)
300
(declare-var operate_pumps.pump_status_2 Int)
301
(declare-var operate_pumps.pump_status_3 Int)
302
(declare-var operate_pumps.pump_defect_0 Int)
303
(declare-var operate_pumps.pump_defect_1 Int)
304
(declare-var operate_pumps.pump_defect_2 Int)
305
(declare-var operate_pumps.pump_defect_3 Int)
306
(declare-var operate_pumps.flow_0 Bool)
307
(declare-var operate_pumps.flow_1 Bool)
308
(declare-var operate_pumps.flow_2 Bool)
309
(declare-var operate_pumps.flow_3 Bool)
310
(declare-var operate_pumps.operate_pumps_0 Int)
311
(declare-var operate_pumps.operate_pumps_1 Int)
312
(declare-var operate_pumps.operate_pumps_2 Int)
313
(declare-var operate_pumps.operate_pumps_3 Int)
314
(declare-var operate_pumps.__operate_pumps_12_c Int)
315
(declare-var operate_pumps.__operate_pumps_19_c Int)
316
(declare-var operate_pumps.__operate_pumps_26_c Int)
317
(declare-var operate_pumps.__operate_pumps_5_c Int)
318
(declare-var operate_pumps.__operate_pumps_12_m Int)
319
(declare-var operate_pumps.__operate_pumps_19_m Int)
320
(declare-var operate_pumps.__operate_pumps_26_m Int)
321
(declare-var operate_pumps.__operate_pumps_5_m Int)
322
(declare-var operate_pumps.__operate_pumps_12_x Int)
323
(declare-var operate_pumps.__operate_pumps_19_x Int)
324
(declare-var operate_pumps.__operate_pumps_26_x Int)
325
(declare-var operate_pumps.__operate_pumps_5_x Int)
326
(declare-var operate_pumps.__operate_pumps_1 Bool)
327
(declare-var operate_pumps.__operate_pumps_10 Bool)
328
(declare-var operate_pumps.__operate_pumps_11 Bool)
329
(declare-var operate_pumps.__operate_pumps_13 Bool)
330
(declare-var operate_pumps.__operate_pumps_14 Bool)
331
(declare-var operate_pumps.__operate_pumps_15 Bool)
332
(declare-var operate_pumps.__operate_pumps_16 Bool)
333
(declare-var operate_pumps.__operate_pumps_17 Bool)
334
(declare-var operate_pumps.__operate_pumps_18 Bool)
335
(declare-var operate_pumps.__operate_pumps_2 Bool)
336
(declare-var operate_pumps.__operate_pumps_20 Bool)
337
(declare-var operate_pumps.__operate_pumps_21 Bool)
338
(declare-var operate_pumps.__operate_pumps_22 Bool)
339
(declare-var operate_pumps.__operate_pumps_23 Bool)
340
(declare-var operate_pumps.__operate_pumps_24 Bool)
341
(declare-var operate_pumps.__operate_pumps_25 Bool)
342
(declare-var operate_pumps.__operate_pumps_27 Bool)
343
(declare-var operate_pumps.__operate_pumps_28 Bool)
344
(declare-var operate_pumps.__operate_pumps_3 Bool)
345
(declare-var operate_pumps.__operate_pumps_4 Bool)
346
(declare-var operate_pumps.__operate_pumps_6 Bool)
347
(declare-var operate_pumps.__operate_pumps_7 Bool)
348
(declare-var operate_pumps.__operate_pumps_8 Bool)
349
(declare-var operate_pumps.__operate_pumps_9 Bool)
350
(declare-rel operate_pumps_reset (Int Int Int Int Int Int Int Int))
351
(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))
352

  
353
(rule (=> 
354
  (and 
355
       (= operate_pumps.__operate_pumps_12_m operate_pumps.__operate_pumps_12_c)
356
       (= operate_pumps.__operate_pumps_19_m operate_pumps.__operate_pumps_19_c)
357
       (= operate_pumps.__operate_pumps_26_m operate_pumps.__operate_pumps_26_c)
358
       (= operate_pumps.__operate_pumps_5_m operate_pumps.__operate_pumps_5_c)
359
       
360
  )
361
  (operate_pumps_reset operate_pumps.__operate_pumps_12_c
362
                       operate_pumps.__operate_pumps_19_c
363
                       operate_pumps.__operate_pumps_26_c
364
                       operate_pumps.__operate_pumps_5_c
365
                       operate_pumps.__operate_pumps_12_m
366
                       operate_pumps.__operate_pumps_19_m
367
                       operate_pumps.__operate_pumps_26_m
368
                       operate_pumps.__operate_pumps_5_m)
369
))
370

  
371
(rule (=> 
372
  (and (= operate_pumps.__operate_pumps_7 (= operate_pumps.pump_status_3 1))
373
       (= operate_pumps.__operate_pumps_6 (and (= operate_pumps.__operate_pumps_5_c 2) (= operate_pumps.pump_defect_3 0)))
374
       (= operate_pumps.__operate_pumps_4 (= operate_pumps.pump_status_3 2))
375
       (pump_failure operate_pumps.pump_defect_3
376
                     operate_pumps.__operate_pumps_1)
377
       (= 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)))
378
       (= 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)))
379
       (and (or (not (= operate_pumps.__operate_pumps_2 true))
380
               (= operate_pumps.operate_pumps_3 2))
381
            (or (not (= operate_pumps.__operate_pumps_2 false))
382
               (and (or (not (= operate_pumps.__operate_pumps_3 true))
383
                       (= operate_pumps.operate_pumps_3 0))
384
                    (or (not (= operate_pumps.__operate_pumps_3 false))
385
                       (and (or (not (= operate_pumps.__operate_pumps_4 true))
386
                               (= operate_pumps.operate_pumps_3 1))
387
                            (or (not (= operate_pumps.__operate_pumps_4 false))
388
                               (and (or (not (= operate_pumps.__operate_pumps_6 true))
389
                                       (and (or (not (= operate_pumps.__operate_pumps_7 true))
390
                                               (= operate_pumps.operate_pumps_3 0))
391
                                            (or (not (= operate_pumps.__operate_pumps_7 false))
392
                                               (= operate_pumps.operate_pumps_3 1))
393
                                       ))
394
                                    (or (not (= operate_pumps.__operate_pumps_6 false))
395
                                       (= operate_pumps.operate_pumps_3 operate_pumps.pump_status_3))
396
                               ))
397
                       ))
398
               ))
399
       )
400
       (pump_failure operate_pumps.pump_defect_2
401
                     operate_pumps.__operate_pumps_8)
402
       (= 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)))
403
       (= operate_pumps.__operate_pumps_14 (= operate_pumps.pump_status_2 1))
404
       (= operate_pumps.__operate_pumps_13 (and (= operate_pumps.__operate_pumps_12_c 2) (= operate_pumps.pump_defect_2 0)))
405
       (= operate_pumps.__operate_pumps_11 (= operate_pumps.pump_status_2 2))
406
       (= 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)))
407
       (and (or (not (= operate_pumps.__operate_pumps_9 true))
408
               (= operate_pumps.operate_pumps_2 2))
409
            (or (not (= operate_pumps.__operate_pumps_9 false))
410
               (and (or (not (= operate_pumps.__operate_pumps_10 true))
411
                       (= operate_pumps.operate_pumps_2 0))
412
                    (or (not (= operate_pumps.__operate_pumps_10 false))
413
                       (and (or (not (= operate_pumps.__operate_pumps_11 true))
414
                               (= operate_pumps.operate_pumps_2 1))
415
                            (or (not (= operate_pumps.__operate_pumps_11 false))
416
                               (and (or (not (= operate_pumps.__operate_pumps_13 true))
417
                                       (and (or (not (= operate_pumps.__operate_pumps_14 true))
418
                                               (= operate_pumps.operate_pumps_2 0))
419
                                            (or (not (= operate_pumps.__operate_pumps_14 false))
420
                                               (= operate_pumps.operate_pumps_2 1))
421
                                       ))
422
                                    (or (not (= operate_pumps.__operate_pumps_13 false))
423
                                       (= operate_pumps.operate_pumps_2 operate_pumps.pump_status_2))
424
                               ))
425
                       ))
426
               ))
427
       )
428
       (= operate_pumps.__operate_pumps_21 (= operate_pumps.pump_status_1 1))
429
       (= operate_pumps.__operate_pumps_20 (and (= operate_pumps.__operate_pumps_19_c 2) (= operate_pumps.pump_defect_1 0)))
430
       (= operate_pumps.__operate_pumps_18 (= operate_pumps.pump_status_1 2))
431
       (pump_failure operate_pumps.pump_defect_1
432
                     operate_pumps.__operate_pumps_15)
433
       (= 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)))
434
       (= 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)))
435
       (and (or (not (= operate_pumps.__operate_pumps_16 true))
436
               (= operate_pumps.operate_pumps_1 2))
437
            (or (not (= operate_pumps.__operate_pumps_16 false))
438
               (and (or (not (= operate_pumps.__operate_pumps_17 true))
439
                       (= operate_pumps.operate_pumps_1 0))
440
                    (or (not (= operate_pumps.__operate_pumps_17 false))
441
                       (and (or (not (= operate_pumps.__operate_pumps_18 true))
442
                               (= operate_pumps.operate_pumps_1 1))
443
                            (or (not (= operate_pumps.__operate_pumps_18 false))
444
                               (and (or (not (= operate_pumps.__operate_pumps_20 true))
445
                                       (and (or (not (= operate_pumps.__operate_pumps_21 true))
446
                                               (= operate_pumps.operate_pumps_1 0))
447
                                            (or (not (= operate_pumps.__operate_pumps_21 false))
448
                                               (= operate_pumps.operate_pumps_1 1))
449
                                       ))
450
                                    (or (not (= operate_pumps.__operate_pumps_20 false))
451
                                       (= operate_pumps.operate_pumps_1 operate_pumps.pump_status_1))
452
                               ))
453
                       ))
454
               ))
455
       )
456
       (= operate_pumps.__operate_pumps_28 (= operate_pumps.pump_status_0 1))
457
       (= operate_pumps.__operate_pumps_27 (and (= operate_pumps.__operate_pumps_26_c 2) (= operate_pumps.pump_defect_0 0)))
458
       (= operate_pumps.__operate_pumps_25 (= operate_pumps.pump_status_0 2))
459
       (pump_failure operate_pumps.pump_defect_0
460
                     operate_pumps.__operate_pumps_22)
461
       (= 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)))
462
       (= 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)))
463
       (and (or (not (= operate_pumps.__operate_pumps_23 true))
464
               (= operate_pumps.operate_pumps_0 2))
465
            (or (not (= operate_pumps.__operate_pumps_23 false))
466
               (and (or (not (= operate_pumps.__operate_pumps_24 true))
467
                       (= operate_pumps.operate_pumps_0 0))
468
                    (or (not (= operate_pumps.__operate_pumps_24 false))
469
                       (and (or (not (= operate_pumps.__operate_pumps_25 true))
470
                               (= operate_pumps.operate_pumps_0 1))
471
                            (or (not (= operate_pumps.__operate_pumps_25 false))
472
                               (and (or (not (= operate_pumps.__operate_pumps_27 true))
473
                                       (and (or (not (= operate_pumps.__operate_pumps_28 true))
474
                                               (= operate_pumps.operate_pumps_0 0))
475
                                            (or (not (= operate_pumps.__operate_pumps_28 false))
476
                                               (= operate_pumps.operate_pumps_0 1))
477
                                       ))
478
                                    (or (not (= operate_pumps.__operate_pumps_27 false))
479
                                       (= operate_pumps.operate_pumps_0 operate_pumps.pump_status_0))
480
                               ))
481
                       ))
482
               ))
483
       )
484
       (= operate_pumps.__operate_pumps_5_x operate_pumps.pump_defect_3)
485
       (= operate_pumps.__operate_pumps_26_x operate_pumps.pump_defect_0)
486
       (= operate_pumps.__operate_pumps_19_x operate_pumps.pump_defect_1)
487
       (= operate_pumps.__operate_pumps_12_x operate_pumps.pump_defect_2)
488
       )
489
  (operate_pumps_step operate_pumps.n
490
                      operate_pumps.n_pumps_to_open
491
                      operate_pumps.pump_status_0
492
                      operate_pumps.pump_status_1
493
                      operate_pumps.pump_status_2
494
                      operate_pumps.pump_status_3
495
                      operate_pumps.pump_defect_0
496
                      operate_pumps.pump_defect_1
497
                      operate_pumps.pump_defect_2
498
                      operate_pumps.pump_defect_3
499
                      operate_pumps.flow_0
500
                      operate_pumps.flow_1
501
                      operate_pumps.flow_2
502
                      operate_pumps.flow_3
503
                      operate_pumps.operate_pumps_0
504
                      operate_pumps.operate_pumps_1
505
                      operate_pumps.operate_pumps_2
506
                      operate_pumps.operate_pumps_3
507
                      operate_pumps.__operate_pumps_12_c
508
                      operate_pumps.__operate_pumps_19_c
509
                      operate_pumps.__operate_pumps_26_c
510
                      operate_pumps.__operate_pumps_5_c
511
                      operate_pumps.__operate_pumps_12_x
512
                      operate_pumps.__operate_pumps_19_x
513
                      operate_pumps.__operate_pumps_26_x
514
                      operate_pumps.__operate_pumps_5_x)
515
))
516

  
517
; steam_failure_detect
518
(declare-var steam_failure_detect.steam Int)
519
(declare-var steam_failure_detect.steam_failure_detect Bool)
520
(declare-rel steam_failure_detect (Int Bool))
521
(rule (=> 
522
  (= steam_failure_detect.steam_failure_detect (or (< steam_failure_detect.steam 0) (> steam_failure_detect.steam 25)))
523
  (steam_failure_detect steam_failure_detect.steam steam_failure_detect.steam_failure_detect)
524
))
525

  
526
; REDGE
527
(declare-var REDGE.S Bool)
528
(declare-var REDGE.REDGE Bool)
529
(declare-var REDGE.__REDGE_2_c Bool)
530
(declare-var REDGE.ni_29._arrow._first_c Bool)
531
(declare-var REDGE.__REDGE_2_m Bool)
532
(declare-var REDGE.ni_29._arrow._first_m Bool)
533
(declare-var REDGE.__REDGE_2_x Bool)
534
(declare-var REDGE.ni_29._arrow._first_x Bool)
535
(declare-var REDGE.__REDGE_1 Bool)
536
(declare-rel REDGE_reset (Bool Bool Bool Bool))
537
(declare-rel REDGE_step (Bool Bool Bool Bool Bool Bool))
538

  
539
(rule (=> 
540
  (and 
541
       (= REDGE.__REDGE_2_m REDGE.__REDGE_2_c)
542
       (= REDGE.ni_29._arrow._first_m true)
543
  )
544
  (REDGE_reset REDGE.__REDGE_2_c
545
               REDGE.ni_29._arrow._first_c
546
               REDGE.__REDGE_2_m
547
               REDGE.ni_29._arrow._first_m)
548
))
549

  
550
(rule (=> 
551
  (and (= REDGE.ni_29._arrow._first_m REDGE.ni_29._arrow._first_c)(and (= REDGE.__REDGE_1 (ite REDGE.ni_29._arrow._first_m true false))
552
                                                                    (= REDGE.ni_29._arrow._first_x false))
553
       (and (or (not (= REDGE.__REDGE_1 true))
554
               (= REDGE.REDGE REDGE.S))
555
            (or (not (= REDGE.__REDGE_1 false))
556
               (= REDGE.REDGE (and REDGE.S (not REDGE.__REDGE_2_c))))
557
       )
558
       (= REDGE.__REDGE_2_x REDGE.S)
559
       )
560
  (REDGE_step REDGE.S
561
              REDGE.REDGE
562
              REDGE.__REDGE_2_c
563
              REDGE.ni_29._arrow._first_c
564
              REDGE.__REDGE_2_x
565
              REDGE.ni_29._arrow._first_x)
566
))
567

  
568
; ControlMode
569
(declare-var ControlMode.steam_boiler_waiting Bool)
570
(declare-var ControlMode.physical_units_ready Bool)
571
(declare-var ControlMode.stop_request Bool)
572
(declare-var ControlMode.steam Int)
573
(declare-var ControlMode.level_defect Int)
574
(declare-var ControlMode.steam_defect Int)
575
(declare-var ControlMode.pump_defect_0 Int)
576
(declare-var ControlMode.pump_defect_1 Int)
577
(declare-var ControlMode.pump_defect_2 Int)
578
(declare-var ControlMode.pump_defect_3 Int)
579
(declare-var ControlMode.pump_control_defect_0 Int)
580
(declare-var ControlMode.pump_control_defect_1 Int)
581
(declare-var ControlMode.pump_control_defect_2 Int)
582
(declare-var ControlMode.pump_control_defect_3 Int)
583
(declare-var ControlMode.q Int)
584
(declare-var ControlMode.pump_state_0 Int)
585
(declare-var ControlMode.pump_state_1 Int)
586
(declare-var ControlMode.pump_state_2 Int)
587
(declare-var ControlMode.pump_state_3 Int)
588
(declare-var ControlMode.op_mode Int)
589
(declare-var ControlMode.__ControlMode_2_c Int)
590
(declare-var ControlMode.ni_28._arrow._first_c Bool)
591
(declare-var ControlMode.__ControlMode_2_m Int)
592
(declare-var ControlMode.ni_28._arrow._first_m Bool)
593
(declare-var ControlMode.__ControlMode_2_x Int)
594
(declare-var ControlMode.ni_28._arrow._first_x Bool)
595
(declare-var ControlMode.__ControlMode_1 Bool)
596
(declare-var ControlMode.__ControlMode_3 Bool)
597
(declare-var ControlMode.__ControlMode_4 Bool)
598
(declare-var ControlMode.__ControlMode_5 Bool)
599
(declare-var ControlMode.__ControlMode_6 Bool)
600
(declare-var ControlMode.__ControlMode_7 Bool)
601
(declare-var ControlMode.__ControlMode_8 Bool)
602
(declare-rel ControlMode_reset (Int Bool Int Bool))
603
(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))
604

  
605
(rule (=> 
606
  (and 
607
       (= ControlMode.__ControlMode_2_m ControlMode.__ControlMode_2_c)
608
       (= ControlMode.ni_28._arrow._first_m true)
609
  )
610
  (ControlMode_reset ControlMode.__ControlMode_2_c
611
                     ControlMode.ni_28._arrow._first_c
612
                     ControlMode.__ControlMode_2_m
613
                     ControlMode.ni_28._arrow._first_m)
614
))
615

  
616
(rule (=> 
617
  (and (failure ControlMode.level_defect
618
                ControlMode.steam_defect
619
                ControlMode.pump_defect_0
620
                ControlMode.pump_defect_1
621
                ControlMode.pump_defect_2
622
                ControlMode.pump_defect_3
623
                ControlMode.pump_control_defect_0
624
                ControlMode.pump_control_defect_1
625
                ControlMode.pump_control_defect_2
626
                ControlMode.pump_control_defect_3
627
                ControlMode.__ControlMode_8)
628
       (level_failure ControlMode.level_defect
629
                      ControlMode.__ControlMode_7)
630
       (= ControlMode.__ControlMode_6 (and (= ControlMode.__ControlMode_2_c 2) (not ControlMode.physical_units_ready)))
631
       (= ControlMode.__ControlMode_5 (= ControlMode.__ControlMode_2_c 1))
632
       (critical_failure ControlMode.__ControlMode_2_c
633
                         ControlMode.steam
634
                         ControlMode.level_defect
635
                         ControlMode.steam_defect
636
                         ControlMode.pump_defect_0
637
                         ControlMode.pump_defect_1
638
                         ControlMode.pump_defect_2
639
                         ControlMode.pump_defect_3
640
                         ControlMode.q
641
                         ControlMode.pump_state_0
642
                         ControlMode.pump_state_1
643
                         ControlMode.pump_state_2
644
                         ControlMode.pump_state_3
645
                         ControlMode.__ControlMode_3)
646
       (= ControlMode.__ControlMode_4 (or (or ControlMode.__ControlMode_3 ControlMode.stop_request) (= ControlMode.__ControlMode_2_c 6)))
647
       (= ControlMode.ni_28._arrow._first_m ControlMode.ni_28._arrow._first_c)
648
       (and (= ControlMode.__ControlMode_1 (ite ControlMode.ni_28._arrow._first_m true false))
649
            (= ControlMode.ni_28._arrow._first_x false))
650
       (and (or (not (= ControlMode.__ControlMode_1 true))
651
               (= ControlMode.op_mode 1))
652
            (or (not (= ControlMode.__ControlMode_1 false))
653
               (and (or (not (= ControlMode.__ControlMode_4 true))
654
                       (= ControlMode.op_mode 6))
655
                    (or (not (= ControlMode.__ControlMode_4 false))
656
                       (and (or (not (= ControlMode.__ControlMode_5 true))
657
                               (and (or (not (= ControlMode.steam_boiler_waiting true))
658
                                       (= ControlMode.op_mode 2))
659
                                    (or (not (= ControlMode.steam_boiler_waiting false))
660
                                       (= ControlMode.op_mode 1))
661
                               ))
662
                            (or (not (= ControlMode.__ControlMode_5 false))
663
                               (and (or (not (= ControlMode.__ControlMode_6 true))
664
                                       (= ControlMode.op_mode 2))
665
                                    (or (not (= ControlMode.__ControlMode_6 false))
666
                                       (and (or (not (= ControlMode.__ControlMode_7 true))
667
                                               (= ControlMode.op_mode 5))
668
                                            (or (not (= ControlMode.__ControlMode_7 false))
669
                                               (and (or (not (= ControlMode.__ControlMode_8 true))
670
                                                       (= ControlMode.op_mode 4))
671
                                                    (or (not (= ControlMode.__ControlMode_8 false))
672
                                                       (= ControlMode.op_mode 3))
673
                                               ))
674
                                       ))
675
                               ))
676
                       ))
677
               ))
678
       )
679
       (= ControlMode.__ControlMode_2_x ControlMode.op_mode)
680
       )
681
  (ControlMode_step ControlMode.steam_boiler_waiting
682
                    ControlMode.physical_units_ready
683
                    ControlMode.stop_request
684
                    ControlMode.steam
685
                    ControlMode.level_defect
686
                    ControlMode.steam_defect
687
                    ControlMode.pump_defect_0
688
                    ControlMode.pump_defect_1
689
                    ControlMode.pump_defect_2
690
                    ControlMode.pump_defect_3
691
                    ControlMode.pump_control_defect_0
692
                    ControlMode.pump_control_defect_1
693
                    ControlMode.pump_control_defect_2
694
                    ControlMode.pump_control_defect_3
695
                    ControlMode.q
696
                    ControlMode.pump_state_0
697
                    ControlMode.pump_state_1
698
                    ControlMode.pump_state_2
699
                    ControlMode.pump_state_3
700
                    ControlMode.op_mode
701
                    ControlMode.__ControlMode_2_c
702
                    ControlMode.ni_28._arrow._first_c
703
                    ControlMode.__ControlMode_2_x
704
                    ControlMode.ni_28._arrow._first_x)
705
))
706

  
707
; ControlOutput
708
(declare-var ControlOutput.op_mode Int)
709
(declare-var ControlOutput.level Int)
710
(declare-var ControlOutput.valve Bool)
711
(declare-var ControlOutput.program_ready Bool)
712
(declare-var ControlOutput.mode Int)
713
(declare-rel ControlOutput (Int Int Bool Bool Int))
714
(rule (=> 
715
  (and (initialization_complete ControlOutput.op_mode
716
                                ControlOutput.level
717
                                ControlOutput.valve
718
                                ControlOutput.program_ready)
719
       (= ControlOutput.mode ControlOutput.op_mode)
720
       )
721
  (ControlOutput ControlOutput.op_mode ControlOutput.level ControlOutput.valve ControlOutput.program_ready ControlOutput.mode)
722
))
723

  
724
; Dynamics
725
(declare-var Dynamics.valve_state Int)
726
(declare-var Dynamics.level Int)
727
(declare-var Dynamics.steam Int)
728
(declare-var Dynamics.level_defect Int)
729
(declare-var Dynamics.steam_defect Int)
730
(declare-var Dynamics.flow_0 Bool)
731
(declare-var Dynamics.flow_1 Bool)
732
(declare-var Dynamics.flow_2 Bool)
733
(declare-var Dynamics.flow_3 Bool)
734
(declare-var Dynamics.q Int)
735
(declare-var Dynamics.v Int)
736
(declare-var Dynamics.p_0 Int)
737
(declare-var Dynamics.p_1 Int)
738
(declare-var Dynamics.p_2 Int)
739
(declare-var Dynamics.p_3 Int)
740
(declare-var Dynamics.__Dynamics_8_c Int)
741
(declare-var Dynamics.ni_27._arrow._first_c Bool)
742
(declare-var Dynamics.__Dynamics_8_m Int)
743
(declare-var Dynamics.ni_27._arrow._first_m Bool)
744
(declare-var Dynamics.__Dynamics_8_x Int)
745
(declare-var Dynamics.ni_27._arrow._first_x Bool)
746
(declare-var Dynamics.__Dynamics_1 Bool)
747
(declare-var Dynamics.__Dynamics_10 Bool)
748
(declare-var Dynamics.__Dynamics_11 Int)
749
(declare-var Dynamics.__Dynamics_2 Bool)
750
(declare-var Dynamics.__Dynamics_3 Bool)
751
(declare-var Dynamics.__Dynamics_4 Bool)
752
(declare-var Dynamics.__Dynamics_5 Bool)
753
(declare-var Dynamics.__Dynamics_6 Bool)
754
(declare-var Dynamics.__Dynamics_7 Int)
755
(declare-var Dynamics.__Dynamics_9 Bool)
756
(declare-rel Dynamics_reset (Int Bool Int Bool))
757
(declare-rel Dynamics_step (Int Int Int Int Int Bool Bool Bool Bool Int Int Int Int Int Int Int Bool Int Bool))
758

  
759
(rule (=> 
760
  (and 
761
       (= Dynamics.__Dynamics_8_m Dynamics.__Dynamics_8_c)
762
       (= Dynamics.ni_27._arrow._first_m true)
763
  )
764
  (Dynamics_reset Dynamics.__Dynamics_8_c
765
                  Dynamics.ni_27._arrow._first_c
766
                  Dynamics.__Dynamics_8_m
767
                  Dynamics.ni_27._arrow._first_m)
768
))
769

  
770
(rule (=> 
771
  (and (= Dynamics.__Dynamics_2 (not Dynamics.flow_3))
772
       (= Dynamics.ni_27._arrow._first_m Dynamics.ni_27._arrow._first_c)
773
       (and (= Dynamics.__Dynamics_1 (ite Dynamics.ni_27._arrow._first_m true false))
774
            (= Dynamics.ni_27._arrow._first_x false))
775
       (and (or (not (= Dynamics.__Dynamics_1 true))
776
               (= Dynamics.p_3 0))
777
            (or (not (= Dynamics.__Dynamics_1 false))
778
               (and (or (not (= Dynamics.__Dynamics_2 true))
779
                       (= Dynamics.p_3 0))
780
                    (or (not (= Dynamics.__Dynamics_2 false))
781
                       (= Dynamics.p_3 15))
782
               ))
783
       )
784
       (= Dynamics.__Dynamics_3 (not Dynamics.flow_2))
785
       (and (or (not (= Dynamics.__Dynamics_1 true))
786
               (= Dynamics.p_2 0))
787
            (or (not (= Dynamics.__Dynamics_1 false))
788
               (and (or (not (= Dynamics.__Dynamics_3 true))
789
                       (= Dynamics.p_2 0))
790
                    (or (not (= Dynamics.__Dynamics_3 false))
791
                       (= Dynamics.p_2 15))
792
               ))
793
       )
794
       (= Dynamics.__Dynamics_4 (not Dynamics.flow_1))
795
       (and (or (not (= Dynamics.__Dynamics_1 true))
796
               (= Dynamics.p_1 0))
797
            (or (not (= Dynamics.__Dynamics_1 false))
798
               (and (or (not (= Dynamics.__Dynamics_4 true))
799
                       (= Dynamics.p_1 0))
800
                    (or (not (= Dynamics.__Dynamics_4 false))
801
                       (= Dynamics.p_1 15))
802
               ))
803
       )
804
       (= Dynamics.__Dynamics_5 (not Dynamics.flow_0))
805
       (and (or (not (= Dynamics.__Dynamics_1 true))
806
               (= Dynamics.p_0 0))
807
            (or (not (= Dynamics.__Dynamics_1 false))
808
               (and (or (not (= Dynamics.__Dynamics_5 true))
809
                       (= Dynamics.p_0 0))
810
                    (or (not (= Dynamics.__Dynamics_5 false))
811
                       (= Dynamics.p_0 15))
812
               ))
813
       )
814
       (level_failure Dynamics.level_defect
815
                      Dynamics.__Dynamics_9)
816
       (sum Dynamics.p_0
817
            Dynamics.p_1
818
            Dynamics.p_2
819
            Dynamics.p_3
820
            Dynamics.__Dynamics_7)
821
       (= Dynamics.__Dynamics_10 (= Dynamics.valve_state 1))
822
       (and (or (not (= Dynamics.__Dynamics_10 true))
823
               (= Dynamics.__Dynamics_11 (* 10 5)))
824
            (or (not (= Dynamics.__Dynamics_10 false))
825
               (= Dynamics.__Dynamics_11 0))
826
       )
827
       (and (or (not (= Dynamics.__Dynamics_1 true))
828
               (= Dynamics.q Dynamics.level))
829
            (or (not (= Dynamics.__Dynamics_1 false))
830
               (and (or (not (= Dynamics.__Dynamics_9 true))
831
                       (= Dynamics.q (- (+ (- Dynamics.__Dynamics_8_c (* Dynamics.steam 5)) (* Dynamics.__Dynamics_7 5)) Dynamics.__Dynamics_11)))
832
                    (or (not (= Dynamics.__Dynamics_9 false))
833
                       (= Dynamics.q Dynamics.level))
834
               ))
835
       )
836
       (steam_failure Dynamics.steam_defect
837
                      Dynamics.__Dynamics_6)
838
       (and (or (not (= Dynamics.__Dynamics_1 true))
839
               (= Dynamics.v Dynamics.steam))
840
            (or (not (= Dynamics.__Dynamics_1 false))
841
               (and (or (not (= Dynamics.__Dynamics_6 true))
842
                       (= Dynamics.v (+ (div (- Dynamics.__Dynamics_8_c Dynamics.q) 5) (* Dynamics.__Dynamics_7 5))))
843
                    (or (not (= Dynamics.__Dynamics_6 false))
844
                       (= Dynamics.v Dynamics.steam))
845
               ))
846
       )
847
       (= Dynamics.__Dynamics_8_x Dynamics.q)
848
       )
849
  (Dynamics_step Dynamics.valve_state
850
                 Dynamics.level
851
                 Dynamics.steam
852
                 Dynamics.level_defect
853
                 Dynamics.steam_defect
854
                 Dynamics.flow_0
855
                 Dynamics.flow_1
856
                 Dynamics.flow_2
857
                 Dynamics.flow_3
858
                 Dynamics.q
859
                 Dynamics.v
860
                 Dynamics.p_0
861
                 Dynamics.p_1
862
                 Dynamics.p_2
863
                 Dynamics.p_3
864
                 Dynamics.__Dynamics_8_c
865
                 Dynamics.ni_27._arrow._first_c
866
                 Dynamics.__Dynamics_8_x
867
                 Dynamics.ni_27._arrow._first_x)
868
))
869

  
870
; LevelDefect
871
(declare-var LevelDefect.level_failure_acknowledgement Bool)
872
(declare-var LevelDefect.level_repaired Bool)
873
(declare-var LevelDefect.level Int)
874
(declare-var LevelDefect.LevelDefect Int)
875
(declare-var LevelDefect.__LevelDefect_3_c Int)
876
(declare-var LevelDefect.ni_26._arrow._first_c Bool)
877
(declare-var LevelDefect.__LevelDefect_3_m Int)
878
(declare-var LevelDefect.ni_26._arrow._first_m Bool)
879
(declare-var LevelDefect.__LevelDefect_3_x Int)
880
(declare-var LevelDefect.ni_26._arrow._first_x Bool)
881
(declare-var LevelDefect.__LevelDefect_1 Bool)
882
(declare-var LevelDefect.__LevelDefect_2 Bool)
883
(declare-var LevelDefect.__LevelDefect_4 Int)
884
(declare-rel LevelDefect_reset (Int Bool Int Bool))
885
(declare-rel LevelDefect_step (Bool Bool Int Int Int Bool Int Bool))
886

  
887
(rule (=> 
888
  (and 
889
       (= LevelDefect.__LevelDefect_3_m LevelDefect.__LevelDefect_3_c)
890
       (= LevelDefect.ni_26._arrow._first_m true)
891
  )
892
  (LevelDefect_reset LevelDefect.__LevelDefect_3_c
893
                     LevelDefect.ni_26._arrow._first_c
894
                     LevelDefect.__LevelDefect_3_m
895
                     LevelDefect.ni_26._arrow._first_m)
896
))
897

  
898
(rule (=> 
899
  (and (level_failure_detect LevelDefect.level
900
                             LevelDefect.__LevelDefect_2)
901
       (Defect LevelDefect.__LevelDefect_3_c
902
               LevelDefect.__LevelDefect_2
903
               LevelDefect.level_failure_acknowledgement
904
               LevelDefect.level_repaired
905
               LevelDefect.__LevelDefect_4)
906
       (= LevelDefect.ni_26._arrow._first_m LevelDefect.ni_26._arrow._first_c)
907
       (and (= LevelDefect.__LevelDefect_1 (ite LevelDefect.ni_26._arrow._first_m true false))
908
            (= LevelDefect.ni_26._arrow._first_x false))
909
       (and (or (not (= LevelDefect.__LevelDefect_1 true))
910
               (= LevelDefect.LevelDefect 0))
911
            (or (not (= LevelDefect.__LevelDefect_1 false))
912
               (= LevelDefect.LevelDefect LevelDefect.__LevelDefect_4))
913
       )
914
       (= LevelDefect.__LevelDefect_3_x LevelDefect.LevelDefect)
915
       )
916
  (LevelDefect_step LevelDefect.level_failure_acknowledgement
917
                    LevelDefect.level_repaired
918
                    LevelDefect.level
919
                    LevelDefect.LevelDefect
920
                    LevelDefect.__LevelDefect_3_c
921
                    LevelDefect.ni_26._arrow._first_c
922
                    LevelDefect.__LevelDefect_3_x
923
                    LevelDefect.ni_26._arrow._first_x)
924
))
925

  
926
; LevelOutput
927
(declare-var LevelOutput.op_mode Int)
928
(declare-var LevelOutput.level_defect Int)
929
(declare-var LevelOutput.level_repaired Bool)
930
(declare-var LevelOutput.level_outcome_failure_detection Bool)
931
(declare-var LevelOutput.level_outcome_repaired_acknowledgement Bool)
932
(declare-rel LevelOutput (Int Int Bool Bool Bool))
933
(rule (=> 
934
  (and (= LevelOutput.level_outcome_repaired_acknowledgement (and (not (or (= LevelOutput.op_mode 6) (= LevelOutput.op_mode 1))) LevelOutput.level_repaired))
935
       (= LevelOutput.level_outcome_failure_detection (and (not (or (= LevelOutput.op_mode 6) (= LevelOutput.op_mode 1))) (= LevelOutput.level_defect 1)))
936
       )
937
  (LevelOutput LevelOutput.op_mode LevelOutput.level_defect LevelOutput.level_repaired LevelOutput.level_outcome_failure_detection LevelOutput.level_outcome_repaired_acknowledgement)
938
))
939

  
940
; Operator
941
(declare-var Operator.stop Bool)
942
(declare-var Operator.stop_request Bool)
943
(declare-var Operator.__Operator_2_c Int)
944
(declare-var Operator.ni_25._arrow._first_c Bool)
945
(declare-var Operator.__Operator_2_m Int)
946
(declare-var Operator.ni_25._arrow._first_m Bool)
947
(declare-var Operator.__Operator_2_x Int)
948
(declare-var Operator.ni_25._arrow._first_x Bool)
949
(declare-var Operator.__Operator_1 Bool)
950
(declare-var Operator.nb_stops Int)
951
(declare-rel Operator_reset (Int Bool Int Bool))
952
(declare-rel Operator_step (Bool Bool Int Bool Int Bool))
953

  
954
(rule (=> 
955
  (and 
956
       (= Operator.__Operator_2_m Operator.__Operator_2_c)
957
       (= Operator.ni_25._arrow._first_m true)
958
  )
959
  (Operator_reset Operator.__Operator_2_c
960
                  Operator.ni_25._arrow._first_c
961
                  Operator.__Operator_2_m
962
                  Operator.ni_25._arrow._first_m)
963
))
964

  
965
(rule (=> 
966
  (and (= Operator.ni_25._arrow._first_m Operator.ni_25._arrow._first_c)
967
       (and (= Operator.__Operator_1 (ite Operator.ni_25._arrow._first_m true false))
968
            (= Operator.ni_25._arrow._first_x false))
969
       (and (or (not (= Operator.__Operator_1 true))
970
               (and (or (not (= Operator.stop true))
971
                       (= Operator.nb_stops 1))
972
                    (or (not (= Operator.stop false))
973
                       (= Operator.nb_stops 0))
974
               ))
975
            (or (not (= Operator.__Operator_1 false))
976
               (and (or (not (= Operator.stop true))
977
                       (= Operator.nb_stops (+ Operator.__Operator_2_c 1)))
978
                    (or (not (= Operator.stop false))
979
                       (= Operator.nb_stops 0))
980
               ))
981
       )
982
       (= Operator.stop_request (>= Operator.nb_stops 3))
983
       (= Operator.__Operator_2_x Operator.nb_stops)
984
       )
985
  (Operator_step Operator.stop
986
                 Operator.stop_request
987
                 Operator.__Operator_2_c
988
                 Operator.ni_25._arrow._first_c
989
                 Operator.__Operator_2_x
990
                 Operator.ni_25._arrow._first_x)
991
))
992

  
993
; PumpDefect
994
(declare-var PumpDefect.pump_failure_acknowledgement Bool)
995
(declare-var PumpDefect.pump_repaired Bool)
996
(declare-var PumpDefect.pump_control_failure_acknowledgement Bool)
997
(declare-var PumpDefect.pump_control_repaired Bool)
998
(declare-var PumpDefect.pump_status Int)
999
(declare-var PumpDefect.pump_state Int)
1000
(declare-var PumpDefect.pump_control_state Bool)
1001
(declare-var PumpDefect.PumpDefect Int)
1002
(declare-var PumpDefect.PumpControlDefect Int)
1003
(declare-var PumpDefect.Flow Bool)
1004
(declare-var PumpDefect.__PumpDefect_2_c Int)
1005
(declare-var PumpDefect.__PumpDefect_4_c Int)
1006
(declare-var PumpDefect.ni_24._arrow._first_c Bool)
1007
(declare-var PumpDefect.__PumpDefect_2_m Int)
1008
(declare-var PumpDefect.__PumpDefect_4_m Int)
1009
(declare-var PumpDefect.ni_24._arrow._first_m Bool)
1010
(declare-var PumpDefect.__PumpDefect_2_x Int)
1011
(declare-var PumpDefect.__PumpDefect_4_x Int)
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff