Project

General

Profile

Revision b8dc00eb

View differences:

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

  
3

  
4

  
5
if(ZUSTRE_COMPILER)
6
  message(STATUS "Found zustre: ${ZUSTRE_COMPILER} ")
7
else(ZUSTRE_COMPILER)
8
  message(FATAL_ERROR "zustre not found")
9
endif(ZUSTRE_COMPILER)
10

  
11
#take all lustre files
12
  set(GLOBAL_LUSTRE_FILES "")
13
  LUSTREFILES(LFILES ${CMAKE_CURRENT_SOURCE_DIR} )
14
  list(APPEND GLOBAL_LUSTRE_FILES ${LFILES})
15
  FOREACH(lfile ${LFILES})
16
	  get_filename_component(L ${lfile} NAME_WE)
17
	  set(LUSTRE_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/${L}")
18
	  file(COPY ${lfile}   DESTINATION  ${LUSTRE_OUTPUT_DIR})
19
  ENDFOREACH()
20

  
21

  
22
#first combination :no option
23
set(ZUSTRE_OPTIONS_OPT "--timeout" "60" "--xml" )
24

  
25
FOREACH(lus_file ${GLOBAL_LUSTRE_FILES})
26
	get_filename_component(L ${lus_file} NAME_WE)
27
	set(ZUSTRE_NODE_OPT  "top")
28

  
29
	Lustre_Compile(LUS_FILE ${lus_file}
30
					NODE ""
31
					OPTS "-horn")
32
					
33
	set(LUS_OPTS_CUT ${LUSTRE_OPTS_POSTFIX_${L}})
34
	add_test(NAME Kind_fmcad08_large_BROKEN_COMPIL_LUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
35
			COMMAND  ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}} 
36
	)
37

  
38
	Zustre_Compile(LUS_FILE ${lus_file}
39
					NODE ${ZUSTRE_NODE_OPT}
40
					OPTS ${ZUSTRE_OPTIONS_OPT})
41
	set(ZUS_OPTS_CUT ${ZUSTRE_OPTS_POSTFIX_${L}})
42
	
43
	
44
	add_test(NAME Kind_fmcad08_large_BROKEN_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
45
			COMMAND  ${ZUSTRE_COMPILER} ${ZUSTRE_ARGS_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}} 
46
			WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}}
47
	)
48
	SET_TESTS_PROPERTIES (  Kind_fmcad08_large_BROKEN_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
49
			PROPERTIES FAIL_REGULAR_EXPRESSION "AssertionError;ERROR;Failed"
50
					DEPENDS Kind_fmcad08_large_BROKEN_COMPIL_LUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT})
51
				
52

  
53
ENDFOREACH()
54

  
55

  
regression_tests/lustre_files/success/kind_fmcad08/large/BROKEN/steam_boiler_no_arr1.lus
1
-- STEAM BOILER example
2
-- from The Steam Boiler Problem in Lustre
3
-- by Thierry Cattel and Gregory Duval
4

  
5

  
6

  
7

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

  
13
 
14

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

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

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

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

  
39
 
40

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

  
46
 
47

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

  
53
 
54

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

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

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

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

  
79
 
80

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

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

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

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

  
112

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

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

  
137

  
138
 
139

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

  
156

  
157
node level_failure(level_defect:int) returns(level_failure:bool); 
158
let 
159
  level_failure = (level_defect<>0); 
160
tel
161
 
162
node steam_failure(steam_defect:int) returns(steam_failure:bool); 
163
let 
164
  steam_failure = (steam_defect<>0); 
165
tel
166

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

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

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

  
215
 
216

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

  
228
 
229

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

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

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

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

  
336
tel
337

  
338

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

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

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

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

  
380
 
381

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

  
397

  
398
node failure( 
399
  level_defect,steam_defect:int; 
400
  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3,pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3:int) 
401
  returns(failure:bool); 
402
let 
403
  failure = level_failure(level_defect) or 
404
    steam_failure(steam_defect) or 
405
    OR(pump_failure(pump_defect_0),pump_failure(pump_defect_1),pump_failure(pump_defect_2),pump_failure(pump_defect_3)) or 
406
    OR(pump_control_failure(pump_control_defect_0),pump_control_failure(pump_control_defect_1),pump_control_failure(pump_control_defect_2),pump_control_failure(pump_control_defect_3)); 
407
tel
408

  
409
 
410

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

  
440
 
441

  
442
 
443

  
444
 
445
 
446

  
447
 
448

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

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

  
472

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

  
480
 
481

  
482
 
483

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

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

  
508
 
509

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

  
579
 
580

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

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

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

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

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

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

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

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

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

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

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

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

  
697
  op_mode = 1-> 
698
    ControlMode( steam_boiler_waiting, physical_units_ready, stop_request, steam, level_defect, steam_defect, pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3, pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3, q, pump_state_0,pump_state_1,pump_state_2,pump_state_3); 
699

  
700

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

  
706

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

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

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

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

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

  
757
 
758

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

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

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

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

  
816
  mode_normal_then_no_failure = 
817
    (mode=3 =>
818
      not(level_failure_detection) and 
819
      not(steam_outcome_failure_detection) and 
820
      AND(not(pump_failure_detection_0),not(pump_failure_detection_1),not(pump_failure_detection_2),not(pump_failure_detection_3)) and 
821
      AND(not(pump_control_failure_detection_0),not(pump_control_failure_detection_1),not(pump_control_failure_detection_2),not(pump_control_failure_detection_3))); 
822
  --%PROPERTY OK=true;
823
  --%MAIN;
824
tel
825

  
regression_tests/lustre_files/success/kind_fmcad08/large/BROKEN/steam_boiler_no_arr1.lusi
1
(* Generated Lustre Interface file from steam_boiler_no_arr1.lus *)
2
(* generated by Lustre-C compiler version 284, 2014/5/25, 15:2:21 *)
3
(* feel free to mask some of the nodes by removing them from this file. *)
4

  
5
function pump_failure (pump_defect: int) returns (pump_failure: bool);
6

  
7

  
8
function steam_failure (steam_defect: int) returns (steam_failure: bool);
9

  
10

  
11
function pump_control_failure (pump_defect: int) returns (pump_failure: bool);
12

  
13

  
14
function level_failure (level_defect: int) returns (level_failure: bool);
15

  
16

  
17
function OR (a_0: bool; a_1: bool; a_2: bool; a_3: bool) returns (OR: bool);
18

  
19

  
20
function transmission_failure (pump_state_0: int; pump_state_1: int; pump_state_2: int; pump_state_3: int) returns (transmission_failure: bool);
21

  
22

  
23
function steam_failure_startup (steam: int) returns (steam_failure_startup: bool);
24

  
25

  
26
function dangerous_level (q: int) returns (dangerous_level: bool);
27

  
28

  
29
function AND (a_0: bool; a_1: bool; a_2: bool; a_3: bool) returns (AND: bool);
30

  
31

  
32
function steam_failure_detect (steam: int) returns (steam_failure_detect: bool);
33

  
34

  
35
function Defect (statein: int; fail_cond: bool; ack_chan: bool; repair_chan: bool) returns (stateout: int);
36

  
37

  
38
node operate_pumps (n: int; n_pumps_to_open: int; pump_status_0: int; pump_status_1: int; pump_status_2: int; pump_status_3: int; pump_defect_0: int; pump_defect_1: int; pump_defect_2: int; pump_defect_3: int; flow_0: bool; flow_1: bool; flow_2: bool; flow_3: bool) returns (operate_pumps_0: int; operate_pumps_1: int; operate_pumps_2: int; operate_pumps_3: int);
39

  
40

  
41
function pump_failure_detect (pump_status: int; pump_state: int; pump_control_state: bool) returns (pump_failure_detect: bool; pump_control_failure_detect: bool; flow: bool);
42

  
43

  
44
function level_failure_detect (level: int) returns (level_failure_detect: bool);
45

  
46

  
47
function sum (a_0: int; a_1: int; a_2: int; a_3: int) returns (sum: int);
48

  
49

  
50
function initialization_complete (op_mode: int; level: int; valve: bool) returns (initialization_complete: bool);
51

  
52

  
53
function failure (level_defect: int; steam_defect: int; pump_defect_0: int; pump_defect_1: int; pump_defect_2: int; pump_defect_3: int; pump_control_defect_0: int; pump_control_defect_1: int; pump_control_defect_2: int; pump_control_defect_3: int) returns (failure: bool);
54

  
55

  
56
function critical_failure (op_mode: int; steam: int; level_defect: int; steam_defect: int; pump_defect_0: int; pump_defect_1: int; pump_defect_2: int; pump_defect_3: int; q: int; pump_state_0: int; pump_state_1: int; pump_state_2: int; pump_state_3: int) returns (critical_failure: bool);
57

  
58

  
59
node Valve (op_mode: int; q: int) returns (valve: bool; valve_state: int);
60

  
61

  
62
function SteamOutput (op_mode: int; steam_defect: int; steam_repaired: bool) returns (steam_outcome_failure_detection: bool; steam_outcome_repaired_acknowledgement: bool);
63

  
64

  
65
node SteamDefect (steam_failure_acknowledgement: bool; steam_repaired: bool; steam: int) returns (SteamDefect: int);
66

  
67

  
68
node PumpsStatus (n_pumps: int; pump_defect_0: int; pump_defect_1: int; pump_defect_2: int; pump_defect_3: int; flow_0: bool; flow_1: bool; flow_2: bool; flow_3: bool) returns (pump_status_0: int; pump_status_1: int; pump_status_2: int; pump_status_3: int);
69

  
70

  
71
node PumpsOutput (op_mode: int; pump_status_0: int; pump_status_1: int; pump_status_2: int; pump_status_3: int; pump_defect_0: int; pump_defect_1: int; pump_defect_2: int; pump_defect_3: int; pump_control_defect_0: int; pump_control_defect_1: int; pump_control_defect_2: int; pump_control_defect_3: int; pump_repaired_0: bool; pump_repaired_1: bool; pump_repaired_2: bool; pump_repaired_3: bool; pump_control_repaired_0: bool; pump_control_repaired_1: bool; pump_control_repaired_2: bool; pump_control_repaired_3: bool) returns (open_pump_0: bool; open_pump_1: bool; open_pump_2: bool; open_pump_3: bool; close_pump_0: bool; close_pump_1: bool; close_pump_2: bool; close_pump_3: bool; pump_failure_detection_0: bool; pump_failure_detection_1: bool; pump_failure_detection_2: bool; pump_failure_detection_3: bool; pump_repaired_acknowledgement_0: bool; pump_repaired_acknowledgement_1: bool; pump_repaired_acknowledgement_2: bool; pump_repaired_acknowledgement_3: bool; pump_control_failure_detection_0: bool; pump_control_failure_detection_1: bool; pump_control_failure_detection_2: bool; pump_control_failure_detection_3: bool; pump_control_repaired_acknowledgement_0: bool; pump_control_repaired_acknowledgement_1: bool; pump_control_repaired_acknowledgement_2: bool; pump_control_repaired_acknowledgement_3: bool);
72

  
73

  
74
node PumpsDecision (q: int; v: int) returns (n_pumps: int);
75

  
76

  
77
node PumpDefect (pump_failure_acknowledgement: bool; pump_repaired: bool; pump_control_failure_acknowledgement: bool; pump_control_repaired: bool; pump_status: int; pump_state: int; pump_control_state: bool) returns (PumpDefect: int; PumpControlDefect: int; Flow: bool);
78

  
79

  
80
node Operator (stop: bool) returns (stop_request: bool);
81

  
82

  
83
function LevelOutput (op_mode: int; level_defect: int; level_repaired: bool) returns (level_outcome_failure_detection: bool; level_outcome_repaired_acknowledgement: bool);
84

  
85

  
86
node LevelDefect (level_failure_acknowledgement: bool; level_repaired: bool; level: int) returns (LevelDefect: int);
87

  
88

  
89
node Dynamics (valve_state: int; level: int; steam: int; level_defect: int; steam_defect: int; flow_0: bool; flow_1: bool; flow_2: bool; flow_3: bool) returns (q: int; v: int; p_0: int; p_1: int; p_2: int; p_3: int);
90

  
91

  
92
function ControlOutput (op_mode: int; level: int; valve: bool) returns (program_ready: bool; mode: int);
93

  
94

  
95
node ControlMode (steam_boiler_waiting: bool; physical_units_ready: bool; stop_request: bool; steam: int; level_defect: int; steam_defect: int; pump_defect_0: int; pump_defect_1: int; pump_defect_2: int; pump_defect_3: int; pump_control_defect_0: int; pump_control_defect_1: int; pump_control_defect_2: int; pump_control_defect_3: int; q: int; pump_state_0: int; pump_state_1: int; pump_state_2: int; pump_state_3: int) returns (op_mode: int);
96

  
97

  
98
node REDGE (S: bool) returns (REDGE: bool);
99

  
100

  
101
node BoilerController (stop: bool; steam_boiler_waiting: bool; physical_units_ready: bool; level: int; steam: int; pump_state_0: int; pump_state_1: int; pump_state_2: int; pump_state_3: int; pump_control_state_0: bool; pump_control_state_1: bool; pump_control_state_2: bool; pump_control_state_3: bool; pump_repaired_0: bool; pump_repaired_1: bool; pump_repaired_2: bool; pump_repaired_3: bool; pump_control_repaired_0: bool; pump_control_repaired_1: bool; pump_control_repaired_2: bool; pump_control_repaired_3: bool; level_repaired: bool; steam_repaired: bool; pump_failure_acknowledgement_0: bool; pump_failure_acknowledgement_1: bool; pump_failure_acknowledgement_2: bool; pump_failure_acknowledgement_3: bool; pump_control_failure_acknowledgement_0: bool; pump_control_failure_acknowledgement_1: bool; pump_control_failure_acknowledgement_2: bool; pump_control_failure_acknowledgement_3: bool; level_failure_acknowledgement: bool; steam_failure_acknowledgement: bool) returns (program_ready: bool; mode: int; valve: bool; open_pump_0: bool; open_pump_1: bool; open_pump_2: bool; open_pump_3: bool; close_pump_0: bool; close_pump_1: bool; close_pump_2: bool; close_pump_3: bool; pump_failure_detection_0: bool; pump_failure_detection_1: bool; pump_failure_detection_2: bool; pump_failure_detection_3: bool; pump_control_failure_detection_0: bool; pump_control_failure_detection_1: bool; pump_control_failure_detection_2: bool; pump_control_failure_detection_3: bool; level_failure_detection: bool; steam_outcome_failure_detection: bool; pump_repaired_acknowledgement_0: bool; pump_repaired_acknowledgement_1: bool; pump_repaired_acknowledgement_2: bool; pump_repaired_acknowledgement_3: bool; pump_control_repaired_acknowledgement_0: bool; pump_control_repaired_acknowledgement_1: bool; pump_control_repaired_acknowledgement_2: bool; pump_control_repaired_acknowledgement_3: bool; level_repaired_acknowledgement: bool; steam_outcome_repaired_acknowledgement: bool);
102

  
103

  
104
node FEDGE2 (S: bool) returns (FEDGE2: bool);
105

  
106

  
107
node FEDGE1 (S: bool) returns (FEDGE1: bool);
108

  
109

  
110
function NOT (a_0: bool; a_1: bool; a_2: bool; a_3: bool) returns (NOT_0: bool; NOT_1: bool; NOT_2: bool; NOT_3: bool);
111

  
112

  
113
node top (stop: bool; steam_boiler_waiting: bool; physical_units_ready: bool; level: int; steam: int; pump_state_0: int; pump_state_1: int; pump_state_2: int; pump_state_3: int; pump_control_state_0: bool; pump_control_state_1: bool; pump_control_state_2: bool; pump_control_state_3: bool; pump_repaired_0: bool; pump_repaired_1: bool; pump_repaired_2: bool; pump_repaired_3: bool; pump_control_repaired_0: bool; pump_control_repaired_1: bool; pump_control_repaired_2: bool; pump_control_repaired_3: bool; level_repaired: bool; steam_repaired: bool; pump_failure_acknowledgement_0: bool; pump_failure_acknowledgement_1: bool; pump_failure_acknowledgement_2: bool; pump_failure_acknowledgement_3: bool; pump_control_failure_acknowledgement_0: bool; pump_control_failure_acknowledgement_1: bool; pump_control_failure_acknowledgement_2: bool; pump_control_failure_acknowledgement_3: bool; level_failure_acknowledgement: bool; steam_failure_acknowledgement: bool) returns (OK: bool);
114

  
115

  
116
node Verification (S1: bool; S2: bool) returns (property_ok: bool);
117

  
118

  
regression_tests/lustre_files/success/kind_fmcad08/large/BROKEN/steam_boiler_no_arr1_e4_23904_e4_2384.lus
1

  
2
node REDGE(S:bool) returns(REDGE:bool); 
3
let 
4
  REDGE= S -> S and not(pre(S)); 
5
tel
6
node sum(a_0,a_1,a_2,a_3:int) returns(sum:int); 
7
let 
8
  sum = a_0 + a_1 + a_2 + a_3; 
9
tel
10
node AND(a_0,a_1,a_2,a_3:bool) returns(AND:bool); 
11
let 
12
  AND = a_0 and a_1 and a_2 and a_3;
13
tel
14
node OR(a_0,a_1,a_2,a_3:bool) returns(OR:bool); 
15
let 
16
  OR = a_0 or a_1 or a_2 or a_3;
17
tel
18
node NOT(a_0,a_1,a_2,a_3:bool) returns(NOT_0,NOT_1,NOT_2,NOT_3:bool); 
19
let 
20
  NOT_0 = not a_0;
21
  NOT_1 = not a_1;
22
  NOT_2 = not a_2;
23
  NOT_3 = not a_3;
24
tel
25
node FEDGE1(S:bool) returns(FEDGE1:bool); 
26
let 
27
  FEDGE1= not(S) -> not(S) and pre(S); 
28
tel
29
node FEDGE2(S:bool) returns(FEDGE2:bool); 
30
let 
31
  FEDGE2= REDGE(not(S)); 
32
tel
33
node Verification(S1,S2:bool) returns(property_ok:bool); 
34
var property1,property2:bool; 
35
let 
36
  property1=FEDGE1(S1)=FEDGE2(S1); 
37
  property2= FEDGE1(S1)=REDGE(S2); 
38
  property_ok=
39
if S2=not(S1) then
40
property1 and property2
41
 else true
42
; 
43
tel
44
node Operator(stop:bool) returns (stop_request:bool); 
45
var nb_stops:int; 
46
let 
47
  nb_stops = (if stop then 1 else 0) -> 
48
    if stop then pre(nb_stops)+1 else 0; 
49
  stop_request = (nb_stops>=3); 
50
tel
51
node Defect(statein:int; fail_cond,ack_chan,repair_chan:bool) 
52
  returns(stateout:int); 
53
let 
54
  stateout = if (statein=0) then 
55
    if fail_cond then 1 else 0 
56
    else 
57
      if (statein=1) then 
58
        if ack_chan then 2 else 1 
59
      else 
60
        if repair_chan then 0 else 2; 
61
tel
62
node level_failure_detect(level:int) returns(level_failure_detect:bool); 
63
let 
64
  level_failure_detect = ((level < 0) or (level > 1000)); 
65
tel
66
node steam_failure_detect(steam:int) returns(steam_failure_detect:bool); 
67
let 
68
  steam_failure_detect = ((steam < 0) or (steam > 25)); 
69
tel
70
node LevelDefect(level_failure_acknowledgement,level_repaired:bool; 
71
  level:int) 
72
  returns( LevelDefect:int); 
73
let 
74
  LevelDefect = 0 -> 
75
    Defect(pre(LevelDefect), level_failure_detect(level), level_failure_acknowledgement, level_repaired); 
76
tel
77
node SteamDefect(steam_failure_acknowledgement,steam_repaired:bool; 
78
  steam:int) 
79
  returns( SteamDefect:int); 
80
let 
81
  SteamDefect = 0 -> 
82
    Defect(pre(SteamDefect), steam_failure_detect(steam), steam_failure_acknowledgement, steam_repaired); 
83
tel
84
node pump_failure_detect(pump_status,pump_state:int; 
85
  pump_control_state:bool) 
86
  returns(pump_failure_detect,pump_control_failure_detect,flow:bool); 
87
let 
88
  pump_failure_detect = ((pump_status=0) and pump_state=1) 
89
    or (((pump_status=1) or (pump_status=2))and pump_state=0); 
90
  pump_control_failure_detect = (((pump_status=0) or 
91
    (pump_status=2)) and pump_state=0 and pump_control_state) 
92
    or ((pump_status=1) and pump_state=1 and not(pump_control_state)) 
93
    or ((pump_status=2) and pump_state=1 and pump_control_state); 
94
  flow = ((pump_status=0) and pump_state=1 and pump_control_state) 
95
    or ((pump_status=1) and pump_state=0 and pump_control_state) 
96
    or ((pump_status=1) and pump_state=1); 
97
tel
98
node PumpDefect( 
99
  pump_failure_acknowledgement,pump_repaired, 
100
  pump_control_failure_acknowledgement,pump_control_repaired:bool; 
101
  pump_status,pump_state:int; 
102
  pump_control_state:bool) 
103
  returns(PumpDefect,PumpControlDefect:int;Flow:bool); 
104
var 
105
  pump_failure_d, pump_control_failure_d:bool; 
106
let 
107
  (pump_failure_d, pump_control_failure_d, Flow) = pump_failure_detect(pump_status, pump_state, pump_control_state); 
108
  PumpDefect = 0 -> 
109
    Defect(pre(PumpDefect), pump_failure_d, pump_failure_acknowledgement, pump_repaired); 
110
  PumpControlDefect = 0 -> 
111
    Defect(pre(PumpControlDefect), pump_control_failure_d, pump_control_failure_acknowledgement, pump_control_repaired); 
112
tel
113
node level_failure(level_defect:int) returns(level_failure:bool); 
114
let 
115
  level_failure = (level_defect<>0); 
116
tel
117
node steam_failure(steam_defect:int) returns(steam_failure:bool); 
118
let 
119
  steam_failure = (steam_defect<>0); 
120
tel
121
node pump_failure(pump_defect:int) returns(pump_failure:bool); 
122
let 
123
  pump_failure = (pump_defect<>0); 
124
tel
125
node pump_control_failure(pump_defect:int) returns(pump_failure:bool); 
126
let 
127
  pump_failure = (pump_defect<>0); 
128
tel
129
node Dynamics(valve_state,level,steam,level_defect,steam_defect:int; 
130
  flow_0,flow_1,flow_2,flow_3:bool) 
131
  returns (q,v:int; p_0,p_1,p_2,p_3:int); 
132
let 
133
  q = level-> 
134
    if level_failure(level_defect) then 
135
      pre(q) +1- steam*5 + sum(p_0,p_1,p_2,p_3)*5 +1- (if valve_state=1 then 10*5 else 0) 
136
    else 
137
      level; 
138
  v = steam-> 
139
    if steam_failure(steam_defect) then 
140
      (pre(q) -q) div 5 + sum(p_0,p_1,p_2,p_3)*5 
141
    else 
142
      steam; 
143
  p_0 = 0-> 
144
    if (not(flow_0)) then 
145
      0 
146
    else 
147
      15; 
148
  p_1 = 0-> 
149
    if (not(flow_1)) then 
150
      0 
151
    else 
152
      15; 
153
  p_2 = 0-> 
154
    if (not(flow_2)) then 
155
      0 
156
    else 
157
      15; 
158
  p_3 = 0-> 
159
    if (not(flow_3)) then 
160
      0 
161
    else 
162
      15; 
163
tel
164
node PumpsDecision(q,v:int) returns (n_pumps:int); 
165
let 
166
  n_pumps = if q>600 then 
167
      (v div 15) 
168
    else 
169
      if q<400 then 
170
        (v div 15) +1 
171
      else 
172
        pre(n_pumps) ; 
173
tel
174
node operate_pumps( n, n_pumps_to_open:int; 
175
  pump_status_0,pump_status_1,pump_status_2,pump_status_3,
176
  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3:int; 
177
  flow_0,flow_1,flow_2,flow_3:bool) 
178
  returns(operate_pumps_0,operate_pumps_1,operate_pumps_2,operate_pumps_3:int); 
179
let 
180
  operate_pumps_0 =  
181
      if ((n_pumps_to_open>0) and 
182
        not(flow_0) and 
183
        not(pump_failure(pump_defect_0)) and 
184
        (pump_status_0=0)) then 
185
        2 
186
      else 
187
        if ((n_pumps_to_open<0) and 
188
          flow_0 and 
189
          not(pump_failure(pump_defect_0)) and 
190
          (pump_status_0=1)) then 
191
          0 
192
        else 
193
          if (pump_status_0=2) then 
194
            1 
195
          else 
196
            if (pre(pump_defect_0)=2 and 
197
              pump_defect_0=0) then 
198
              if pump_status_0=1 then 
199
                0 
200
              else 
201
                1 
202
            else 
203
              pump_status_0; 
204
  operate_pumps_1 =  
205
      if ((n_pumps_to_open>0) and 
206
        not(flow_1) and 
207
        not(pump_failure(pump_defect_1)) and 
208
        (pump_status_1=0)) then 
209
        2 
210
      else 
211
        if ((n_pumps_to_open<0) and 
212
          flow_1 and 
213
          not(pump_failure(pump_defect_1)) and 
214
          (pump_status_1=1)) then 
215
          0 
216
        else 
217
          if (pump_status_1=2) then 
218
            1 
219
          else 
220
            if (pre(pump_defect_1)=2 and 
221
              pump_defect_1=0) then 
222
              if pump_status_1=1 then 
223
                0 
224
              else 
225
                1 
226
            else 
227
              pump_status_1; 
228
  operate_pumps_2 =  
229
      if ((n_pumps_to_open>0) and 
230
        not(flow_2) and 
231
        not(pump_failure(pump_defect_2)) and 
232
        (pump_status_2=0)) then 
233
        2 
234
      else 
235
        if ((n_pumps_to_open<0) and 
236
          flow_2 and 
237
          not(pump_failure(pump_defect_2)) and 
238
          (pump_status_2=1)) then 
239
          0 
240
        else 
241
          if (pump_status_2=2) then 
242
            1 
243
          else 
244
            if (pre(pump_defect_2)=2 and 
245
              pump_defect_2=0) then 
246
              if pump_status_2=1 then 
247
                0 
248
              else 
249
                1 
250
            else 
251
              pump_status_2; 
252
  operate_pumps_3 =  
253
      if ((n_pumps_to_open>0) and 
254
        not(flow_3) and 
255
        not(pump_failure(pump_defect_3)) and 
256
        (pump_status_3=0)) then 
257
        2 
258
      else 
259
        if ((n_pumps_to_open<0) and 
260
          flow_3 and 
261
          not(pump_failure(pump_defect_3)) and 
262
          (pump_status_3=1)) then 
263
          0 
264
        else 
265
          if (pump_status_3=2) then 
266
            1 
267
          else 
268
            if (pre(pump_defect_3)=2 and 
269
              pump_defect_3=0) then 
270
              if pump_status_3=1 then 
271
                0 
272
              else 
273
                1 
274
            else 
275
              pump_status_3; 
276
tel
277
node PumpsStatus( 
278
  n_pumps:int; 
279
  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3:int; 
280
  flow_0,flow_1,flow_2,flow_3:bool) 
281
  returns(pump_status_0,pump_status_1,pump_status_2,pump_status_3:int); 
282
var 
283
  n_pumps_flow,n_pumps_to_open:int; 
284
  t0,t1,t2,t3:int;
285
let 
286
  n_pumps_flow = (if flow_0 then 1 else 0) + (if flow_1 then 1 else 0) + 
287
    (if flow_2 then 1 else 0) + (if flow_3 then 1 else 0); 
288
  n_pumps_to_open = n_pumps-n_pumps_flow; 
289
  pump_status_0 = 0 ->t0;
290
  pump_status_1 = 0 ->t1;
291
  pump_status_2 = 0 ->t2;
292
  pump_status_3 = 0 ->t3;
293
  (t0,t1,t2,t3) =
294
    operate_pumps(4, n_pumps_to_open, 
295
      pre(pump_status_0),pre(pump_status_1),pre(pump_status_2),pre(pump_status_3), 
296
      pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3, 
297
      flow_0,flow_1,flow_2,flow_3); 
298
tel
299
node transmission_failure(pump_state_0,pump_state_1,pump_state_2,pump_state_3:int) 
300
  returns(transmission_failure:bool); 
301
let 
302
  transmission_failure = pump_state_0=3 or pump_state_1=3 or pump_state_2=3 or pump_state_3=3; 
303
tel
304
node steam_failure_startup(steam:int) returns(steam_failure_startup:bool); 
305
let 
306
  steam_failure_startup=(steam<>0); 
307
tel
308
node dangerous_level(q:int) returns(dangerous_level:bool); 
309
let 
310
  dangerous_level = (q <= 150) or (q >= 850); 
311
tel
312
node critical_failure( 
313
  op_mode,steam,level_defect,steam_defect:int; 
314
  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3:int; 
315
  q:int; 
316
  pump_state_0,pump_state_1,pump_state_2,pump_state_3:int) 
317
  returns(critical_failure:bool); 
318
let 
319
  critical_failure = transmission_failure(pump_state_0,pump_state_1,pump_state_2,pump_state_3) or 
320
    (op_mode=1 and steam_failure_startup(steam)) or 
321
    (op_mode=2 and (level_failure(level_defect) or steam_failure(steam_defect))) or 
322
    (op_mode=3 and dangerous_level(q)) or 
323
    (op_mode=4 and dangerous_level(q)) or 
324
    (op_mode=5 and (dangerous_level(q) or steam_failure(steam_defect) or AND(pump_failure(pump_defect_0),pump_failure(pump_defect_1),pump_failure(pump_defect_2),pump_failure(pump_defect_3)))); 
325
tel
326
node failure( 
327
  level_defect,steam_defect:int; 
328
  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3,pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3:int) 
329
  returns(failure:bool); 
330
let 
331
  failure = level_failure(level_defect) or 
332
    steam_failure(steam_defect) or 
333
    OR(pump_failure(pump_defect_0),pump_failure(pump_defect_1),pump_failure(pump_defect_2),pump_failure(pump_defect_3)) or 
334
    OR(pump_control_failure(pump_control_defect_0),pump_control_failure(pump_control_defect_1),pump_control_failure(pump_control_defect_2),pump_control_failure(pump_control_defect_3)); 
335
tel
336
node ControlMode( 
337
  steam_boiler_waiting,physical_units_ready,stop_request:bool; 
338
  steam,level_defect,steam_defect:int; 
339
  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3,pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3:int; 
340
  q:int; 
341
  pump_state_0,pump_state_1,pump_state_2,pump_state_3:int) 
342
  returns(op_mode :int); 
343
let 
344
  op_mode= 1-> 
345
    if (critical_failure(pre(op_mode), 
346
      steam, level_defect, steam_defect, pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3, q, pump_state_0,pump_state_1,pump_state_2,pump_state_3) or 
347
      stop_request or pre(op_mode)=6) then 
348
      6 
349
    else 
350
      if (pre(op_mode)=1) then 
351
        if steam_boiler_waiting then 2 else 1 
352
      else 
353
        if (pre(op_mode)=2 and not physical_units_ready) then 
354
          2 
355
        else 
356
          if level_failure(level_defect) then 
357
            5 
358
          else 
359
            if failure(level_defect, steam_defect, pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3, pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3) then 
360
              4 
361
            else 
362
              3; 
363
tel
364
node Valve(op_mode:int;q:int) returns (valve:bool;valve_state:int); 
365
let 
366
  valve_state=0-> 
367
    if (op_mode=2) then 
368
      if (q>600) then 
369
        1 
370
      else 
371
        if (q<=600) then 0 else pre(valve_state) 
372
    else 
373
      pre(valve_state); 
374
  valve =false-> 
375
    (valve_state<>pre(valve_state)); 
376
tel
377
node initialization_complete(op_mode,level:int;valve:bool) 
378
  returns(initialization_complete:bool); 
379
let 
380
  initialization_complete =(op_mode=2) and 
381
    ((400<=level) and (level<=600))and 
382
    not(valve); 
383
tel
384
node ControlOutput(op_mode,level:int;valve:bool) 
385
  returns(program_ready:bool;mode:int); 
386
let 
387
  program_ready=initialization_complete(op_mode,level,valve); 
388
  mode =op_mode; 
389
tel
390
node SteamOutput(op_mode,steam_defect:int; steam_repaired:bool) 
391
  returns (steam_outcome_failure_detection, 
392
steam_outcome_repaired_acknowledgement : bool); 
393
let 
394
  steam_outcome_failure_detection= 
395
    not ((op_mode=6) or (op_mode=1)) and 
396
    (steam_defect=1); 
397
  steam_outcome_repaired_acknowledgement = 
398
    not ((op_mode=6) or (op_mode=1)) and 
399
    steam_repaired; 
400
tel
401
node LevelOutput(op_mode,level_defect:int; level_repaired:bool) 
402
  returns (level_outcome_failure_detection, 
403
level_outcome_repaired_acknowledgement : bool); 
404
let 
405
  level_outcome_failure_detection= 
406
    not ((op_mode=6) or (op_mode=1)) and 
407
    (level_defect=1); 
408
  level_outcome_repaired_acknowledgement = 
409
    not ((op_mode=6) or (op_mode=1)) and 
410
    level_repaired; 
411
tel
412
node PumpsOutput(op_mode:int; 
413
  pump_status_0,pump_status_1,pump_status_2,pump_status_3,
414
  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3,
415
  pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3:int; 
416
  pump_repaired_0,pump_repaired_1,pump_repaired_2,pump_repaired_3,
417
  pump_control_repaired_0,pump_control_repaired_1,pump_control_repaired_2,pump_control_repaired_3:bool) 
418
  returns (open_pump_0,open_pump_1,open_pump_2,open_pump_3,
419
  close_pump_0,close_pump_1,close_pump_2,close_pump_3,
420
  pump_failure_detection_0,pump_failure_detection_1,pump_failure_detection_2,pump_failure_detection_3, 
421
  pump_repaired_acknowledgement_0,pump_repaired_acknowledgement_1,pump_repaired_acknowledgement_2,pump_repaired_acknowledgement_3,
422
  pump_control_failure_detection_0,pump_control_failure_detection_1,pump_control_failure_detection_2,pump_control_failure_detection_3, 
423
  pump_control_repaired_acknowledgement_0,pump_control_repaired_acknowledgement_1,pump_control_repaired_acknowledgement_2,pump_control_repaired_acknowledgement_3 : bool); 
424
let 
425
  open_pump_0 = 
426
     op_mode<>6 and op_mode<>1 and pump_status_0=2;
427
  open_pump_1 = 
428
     op_mode<>6 and op_mode<>1 and pump_status_1=2;
429
  open_pump_2 = 
430
     op_mode<>6 and op_mode<>1 and pump_status_2=2;
431
  open_pump_3 = 
432
     op_mode<>6 and op_mode<>1 and pump_status_3=2; 
433
    
434
  close_pump_0 = 
435
     op_mode<>6 and op_mode<>1 and pump_status_0=0 and pre(pump_status_0)<>0 and pump_defect_0=0 and pre(pump_defect_0)=0;
436
  close_pump_1 = 
437
     op_mode<>6 and op_mode<>1 and pump_status_0=0 and pre(pump_status_1)<>0 and pump_defect_0=0 and pre(pump_defect_1)=0;
438
  close_pump_2 = 
439
     op_mode<>6 and op_mode<>1 and pump_status_0=0 and pre(pump_status_2)<>0 and pump_defect_0=0 and pre(pump_defect_2)=0;
440
  close_pump_3 = 
441
     op_mode<>6 and op_mode<>1 and pump_status_0=0 and pre(pump_status_3)<>0 and pump_defect_0=0 and pre(pump_defect_3)=0;
442
    
443
  pump_failure_detection_0 = 
444
    op_mode<>6 and op_mode<>1 and pump_defect_0=1;
445
  pump_failure_detection_1 = 
446
     op_mode<>6 and op_mode<>1 and pump_defect_1=1;
447
  pump_failure_detection_2 = 
448
     op_mode<>6 and op_mode<>1 and pump_defect_2=1;
449
  pump_failure_detection_3 = 
450
     op_mode<>6 and op_mode<>1 and pump_defect_3=1;
451
    
452
  pump_repaired_acknowledgement_0 = 
453
    op_mode<>6 and op_mode<>1 and pump_repaired_0;
454
  pump_repaired_acknowledgement_1 = 
455
     op_mode<>6 and op_mode<>1 and pump_repaired_1;
456
  pump_repaired_acknowledgement_2 = 
457
     op_mode<>6 and op_mode<>1 and pump_repaired_2;
458
  pump_repaired_acknowledgement_3 = 
459
     op_mode<>6 and op_mode<>1 and pump_repaired_3;
460
    
461
  pump_control_failure_detection_0 = 
462
    op_mode<>6 and op_mode<>1 and pump_control_defect_0=1;
463
  pump_control_failure_detection_1 = 
464
    op_mode<>6 and op_mode<>1 and pump_control_defect_1=1;
465
  pump_control_failure_detection_2 = 
466
    op_mode<>6 and op_mode<>1 and pump_control_defect_2=1;
467
  pump_control_failure_detection_3 = 
468
    op_mode<>6 and op_mode<>1 and pump_control_defect_3=1;
469
    
470
  pump_control_repaired_acknowledgement_0 = 
471
    op_mode<>6 and op_mode<>1 and pump_control_repaired_0;
472
  pump_control_repaired_acknowledgement_1 = 
473
    op_mode<>6 and op_mode<>1 and pump_control_repaired_1;
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff