Project

General

Profile

Revision 9b45f3df regression_tests/lustre_files/success/kind_fmcad08/large/steam_boiler_no_arr2_e6_3003_e4_15091.lus

View differences:

regression_tests/lustre_files/success/kind_fmcad08/large/steam_boiler_no_arr2_e6_3003_e4_15091.lus
308 308
  steam_failure_startup=(steam<>0); 
309 309
tel
310 310
node critical_failure( 
311
  op_mode,steam,level_defect,steam_defect:int; 
311
  op_mode_,steam,level_defect,steam_defect:int; 
312 312
  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3:int; 
313 313
  q:int; 
314 314
  pump_state_0,pump_state_1,pump_state_2,pump_state_3:int) 
315 315
  returns(critical_failure:bool); 
316 316
let 
317 317
  critical_failure = transmission_failure(pump_state_0,pump_state_1,pump_state_2,pump_state_3) or 
318
    (op_mode=1 and steam_failure_startup(steam)) or 
319
    (op_mode=2 and (level_failure(level_defect) or steam_failure(steam_defect))) or 
320
    (op_mode=3 and dangerous_level(q)) or 
321
    (op_mode=4 and dangerous_level(q)) or 
322
    (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)))); 
318
    (op_mode_=1 and steam_failure_startup(steam)) or 
319
    (op_mode_=2 and (level_failure(level_defect) or steam_failure(steam_defect))) or 
320
    (op_mode_=3 and dangerous_level(q)) or 
321
    (op_mode_=4 and dangerous_level(q)) or 
322
    (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)))); 
323 323
tel
324 324
node failure( 
325 325
  level_defect,steam_defect:int; 
......
337 337
  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; 
338 338
  q:int; 
339 339
  pump_state_0,pump_state_1,pump_state_2,pump_state_3:int) 
340
  returns(op_mode :int); 
340
  returns(op_mode_ :int); 
341 341
let 
342
  op_mode= 1-> 
343
    if (critical_failure(pre(op_mode), 
342
  op_mode_= 1-> 
343
    if (critical_failure(pre(op_mode_), 
344 344
      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 
345
      stop_request or pre(op_mode)=6) then 
345
      stop_request or pre(op_mode_)=6) then 
346 346
      6 
347 347
    else 
348
      if (pre(op_mode)=1) then 
348
      if (pre(op_mode_)=1) then 
349 349
        if steam_boiler_waiting then 2 else 1 
350 350
      else 
351
        if (pre(op_mode)=2 and not physical_units_ready) then 
351
        if (pre(op_mode_)=2 and not physical_units_ready) then 
352 352
          2 
353 353
        else 
354 354
          if level_failure(level_defect) then 
......
359 359
            else 
360 360
              3; 
361 361
tel
362
node Valve(op_mode:int;q:int) returns (valve:bool;valve_state:int); 
362
node Valve(op_mode_:int;q:int) returns (valve:bool;valve_state:int); 
363 363
let 
364 364
  valve_state=0-> 
365
    if (op_mode=2) then 
365
    if (op_mode_=2) then 
366 366
      if (q>600) then 
367 367
        1 
368 368
      else 
......
372 372
  valve =false-> 
373 373
    (valve_state<>pre(valve_state)); 
374 374
tel
375
node initialization_complete(op_mode,level:int;valve:bool) 
375
node initialization_complete(op_mode_,level:int;valve:bool) 
376 376
  returns(initialization_complete:bool); 
377 377
let 
378
  initialization_complete =(op_mode=2) and 
378
  initialization_complete =(op_mode_=2) and 
379 379
    ((400<=level) and (level<=600))and 
380 380
    not(valve); 
381 381
tel
382
node ControlOutput(op_mode,level:int;valve:bool) 
383
  returns(program_ready:bool;mode:int); 
382
node ControlOutput(op_mode_,level:int;valve:bool) 
383
  returns(program_ready:bool;mode_:int); 
384 384
let 
385
  program_ready=initialization_complete(op_mode,level,valve); 
386
  mode =op_mode; 
385
  program_ready=initialization_complete(op_mode_,level,valve); 
386
  mode_ =op_mode_; 
387 387
tel
388
node LevelOutput(op_mode,level_defect:int; level_repaired:bool) 
388
node LevelOutput(op_mode_,level_defect:int; level_repaired:bool) 
389 389
  returns (level_outcome_failure_detection, 
390 390
level_outcome_repaired_acknowledgement : bool); 
391 391
let 
392 392
  level_outcome_failure_detection= 
393
    not ((op_mode=6) or (op_mode=1)) and 
393
    not ((op_mode_=6) or (op_mode_=1)) and 
394 394
    (level_defect=1); 
395 395
  level_outcome_repaired_acknowledgement = 
396
    not ((op_mode=6) or (op_mode=1)) and 
396
    not ((op_mode_=6) or (op_mode_=1)) and 
397 397
    level_repaired; 
398 398
tel
399
node SteamOutput(op_mode,steam_defect:int; steam_repaired:bool) 
399
node SteamOutput(op_mode_,steam_defect:int; steam_repaired:bool) 
400 400
  returns (steam_outcome_failure_detection, 
401 401
steam_outcome_repaired_acknowledgement : bool); 
402 402
let 
403 403
  steam_outcome_failure_detection= 
404
    not ((op_mode=6) or (op_mode=1)) and 
404
    not ((op_mode_=6) or (op_mode_=1)) and 
405 405
    (steam_defect=1); 
406 406
  steam_outcome_repaired_acknowledgement = 
407
    not ((op_mode=6) or (op_mode=1)) and 
407
    not ((op_mode_=6) or (op_mode_=1)) and 
408 408
    steam_repaired; 
409 409
tel
410
node PumpsOutput(op_mode:int; 
410
node PumpsOutput(op_mode_:int; 
411 411
  pump_status_0,pump_status_1,pump_status_2,pump_status_3,
412 412
  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3,
413 413
  pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3:int; 
......
421 421
  pump_control_repaired_acknowledgement_0,pump_control_repaired_acknowledgement_1,pump_control_repaired_acknowledgement_2,pump_control_repaired_acknowledgement_3 : bool); 
422 422
let 
423 423
  open_pump_0 = 
424
     op_mode<>6 and op_mode<>1 and pump_status_0=2;
424
     op_mode_<>6 and op_mode_<>1 and pump_status_0=2;
425 425
  open_pump_1 = 
426
     op_mode<>6 and op_mode<>1 and pump_status_1=2;
426
     op_mode_<>6 and op_mode_<>1 and pump_status_1=2;
427 427
  open_pump_2 = 
428
     op_mode<>6 and op_mode<>1 and pump_status_2=2;
428
     op_mode_<>6 and op_mode_<>1 and pump_status_2=2;
429 429
  open_pump_3 = 
430
     op_mode<>6 and op_mode<>1 and pump_status_3=2; 
430
     op_mode_<>6 and op_mode_<>1 and pump_status_3=2; 
431 431
    
432 432
  close_pump_0 = 
433
     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;
433
     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;
434 434
  close_pump_1 = 
435
     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;
435
     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;
436 436
  close_pump_2 = 
437
     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;
437
     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;
438 438
  close_pump_3 = 
439
     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;
439
     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;
440 440
    
441 441
  pump_failure_detection_0 = 
442
    op_mode<>6 and op_mode<>1 and pump_defect_0=1;
442
    op_mode_<>6 and op_mode_<>1 and pump_defect_0=1;
443 443
  pump_failure_detection_1 = 
444
     op_mode<>6 and op_mode<>1 and pump_defect_1=1;
444
     op_mode_<>6 and op_mode_<>1 and pump_defect_1=1;
445 445
  pump_failure_detection_2 = 
446
     op_mode<>6 and op_mode<>1 and pump_defect_2=1;
446
     op_mode_<>6 and op_mode_<>1 and pump_defect_2=1;
447 447
  pump_failure_detection_3 = 
448
     op_mode<>6 and op_mode<>1 and pump_defect_3=1;
448
     op_mode_<>6 and op_mode_<>1 and pump_defect_3=1;
449 449
    
450 450
  pump_repaired_acknowledgement_0 = 
451
    op_mode<>6 and op_mode<>1 and pump_repaired_0;
451
    op_mode_<>6 and op_mode_<>1 and pump_repaired_0;
452 452
  pump_repaired_acknowledgement_1 = 
453
     op_mode<>6 and op_mode<>1 and pump_repaired_1;
453
     op_mode_<>6 and op_mode_<>1 and pump_repaired_1;
454 454
  pump_repaired_acknowledgement_2 = 
455
     op_mode<>6 and op_mode<>1 and pump_repaired_2;
455
     op_mode_<>6 and op_mode_<>1 and pump_repaired_2;
456 456
  pump_repaired_acknowledgement_3 = 
457
     op_mode<>6 and op_mode<>1 and pump_repaired_3;
457
     op_mode_<>6 and op_mode_<>1 and pump_repaired_3;
458 458
    
459 459
  pump_control_failure_detection_0 = 
460
    op_mode<>6 and op_mode<>1 and pump_control_defect_0=1;
460
    op_mode_<>6 and op_mode_<>1 and pump_control_defect_0=1;
461 461
  pump_control_failure_detection_1 = 
462
    op_mode<>6 and op_mode<>1 and pump_control_defect_1=1;
462
    op_mode_<>6 and op_mode_<>1 and pump_control_defect_1=1;
463 463
  pump_control_failure_detection_2 = 
464
    op_mode<>6 and op_mode<>1 and pump_control_defect_2=1;
464
    op_mode_<>6 and op_mode_<>1 and pump_control_defect_2=1;
465 465
  pump_control_failure_detection_3 = 
466
    op_mode<>6 and op_mode<>1 and pump_control_defect_3=1;
466
    op_mode_<>6 and op_mode_<>1 and pump_control_defect_3=1;
467 467
    
468 468
  pump_control_repaired_acknowledgement_0 = 
469
    op_mode<>6 and op_mode<>1 and pump_control_repaired_0;
469
    op_mode_<>6 and op_mode_<>1 and pump_control_repaired_0;
470 470
  pump_control_repaired_acknowledgement_1 = 
471
    op_mode<>6 and op_mode<>1 and pump_control_repaired_1;
471
    op_mode_<>6 and op_mode_<>1 and pump_control_repaired_1;
472 472
  pump_control_repaired_acknowledgement_2 = 
473
    op_mode<>6 and op_mode<>1 and pump_control_repaired_2;
473
    op_mode_<>6 and op_mode_<>1 and pump_control_repaired_2;
474 474
  pump_control_repaired_acknowledgement_3 = 
475
    op_mode<>6 and op_mode<>1 and pump_control_repaired_3;
475
    op_mode_<>6 and op_mode_<>1 and pump_control_repaired_3;
476 476
tel
477 477
node BoilerController( 
478 478
  stop, 
......
492 492
  steam_failure_acknowledgement : bool) 
493 493
  returns(
494 494
  program_ready : bool; 
495
  mode : int; 
495
  mode_ : int; 
496 496
  valve : bool; 
497 497
  open_pump_0,open_pump_1,open_pump_2,open_pump_3 : bool; 
498 498
  close_pump_0,close_pump_1,close_pump_2,close_pump_3 : bool; 
......
506 506
  steam_outcome_repaired_acknowledgement: bool); 
507 507
var 
508 508
  stop_request : bool; 
509
  op_mode : int; 
509
  op_mode_ : int; 
510 510
  q : int; 
511 511
  v : int; 
512 512
  p_0,p_1,p_2,p_3 : int; 
......
573 573
  (u0,u1,u2,u3) =
574 574
    PumpsStatus(n_pumps, pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3,
575 575
      flow_0,flow_1,flow_2,flow_3); 
576
  op_mode = 1-> 
576
  op_mode_ = 1-> 
577 577
    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); 
578 578
  valve = false -> u4;
579 579
  valve_state = 0 -> u5;
580 580
  (u4,u5) =
581
    Valve(op_mode,q); 
581
    Valve(op_mode_,q); 
582 582
  program_ready = false -> u6;
583
  mode = 1-> u7;
583
  mode_ = 1-> u7;
584 584
  (u6,u7) =
585
    ControlOutput(op_mode,level,valve); 
585
    ControlOutput(op_mode_,level,valve); 
586 586
  open_pump_0=a1;
587 587
  open_pump_1=a2;
588 588
  open_pump_2=a3;
......
608 608
  pump_control_repaired_acknowledgement_2=a23;
609 609
  pump_control_repaired_acknowledgement_3=a24;
610 610
   (a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24)=
611
      PumpsOutput(op_mode, pump_status_0,pump_status_1,pump_status_2,pump_status_3,
611
      PumpsOutput(op_mode_, pump_status_0,pump_status_1,pump_status_2,pump_status_3,
612 612
        pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3,
613 613
        pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3,
614 614
        pump_repaired_0,pump_repaired_1,pump_repaired_2,pump_repaired_3,
......
616 616
  level_failure_detection = false -> b0;
617 617
  level_repaired_acknowledgement = false -> b1;
618 618
  (b0,b1)=
619
    LevelOutput(op_mode,level_defect,level_repaired); 
619
    LevelOutput(op_mode_,level_defect,level_repaired); 
620 620
  steam_outcome_failure_detection = false -> b2;
621 621
  steam_outcome_repaired_acknowledgement = false -> b3;
622 622
  (b2,b3)=
623
    SteamOutput(op_mode,steam_defect,steam_repaired); 
623
    SteamOutput(op_mode_,steam_defect,steam_repaired); 
624 624
tel
625 625
node top(
626 626
  steam_boiler_waiting,physical_units_ready,stop_request:bool; 
......
631 631
  returns(OK:bool); 
632 632
--@ contract guarantees OK;
633 633
var 
634
  op_mode :int; 
635
  mode_normal_then_water_level_ok, 
636
  mode_normal_then_no_stop_request:bool; 
634
  op_mode_ :int; 
635
  mode__normal_then_water_level_ok, 
636
  mode__normal_then_no_stop_request:bool; 
637 637
let 
638
  op_mode= 
638
  op_mode_= 
639 639
    ControlMode(
640 640
      steam_boiler_waiting,physical_units_ready,stop_request,
641 641
      steam,level_defect,steam_defect,
642 642
      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,
643 643
      q, pump_state_0,pump_state_1,pump_state_2,pump_state_3); 
644 644
  OK = 
645
    mode_normal_then_water_level_ok and 
646
    mode_normal_then_no_stop_request; 
647
  mode_normal_then_no_stop_request = 
648
    (op_mode=3 => not(stop_request)); 
649
  mode_normal_then_water_level_ok = 
645
    mode__normal_then_water_level_ok and 
646
    mode__normal_then_no_stop_request; 
647
  mode__normal_then_no_stop_request = 
648
    (op_mode_=3 => not(stop_request)); 
649
  mode__normal_then_water_level_ok = 
650 650
    true ->
651
    (op_mode=3 and pre(op_mode)=3 =>
651
    (op_mode_=3 and pre(op_mode_)=3 =>
652 652
    not(dangerous_level(q))); 
653 653
  --%MAIN;
654 654
  --%PROPERTY  OK=true;

Also available in: Unified diff