Project

General

Profile

Revision 2d37a1e1 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
622 622
  (b2,b3)=
623 623
    SteamOutput(op_mode,steam_defect,steam_repaired); 
624 624
tel
625
--@ ensures OK;
626 625
node top(
627 626
  steam_boiler_waiting,physical_units_ready,stop_request:bool; 
628 627
  steam,level_defect,steam_defect:int; 
......
630 629
  q:int; 
631 630
  pump_state_0,pump_state_1,pump_state_2,pump_state_3:int) 
632 631
  returns(OK:bool); 
632
--@ contract guarantees OK;
633 633
var 
634 634
  op_mode :int; 
635 635
  mode_normal_then_water_level_ok, 

Also available in: Unified diff