CristalCaveGem » LustreC » Lustrec-Tests

    SteamOutput(op_mode,steam_defect,steam_repaired); 

tel

--ensures OK;

  steam_boiler_waiting,physical_units_ready,stop_request:bool; 

  steam,level_defect,steam_defect:int; 

  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;