CristalCaveGem » LustreC » Lustrec-Tests

(* Generated Lustre Interface file from steam_boiler_no_arr2_e1_17214_e5_18600.lus *)

(* generated by Lustre-C compiler version 284, 2014/5/25, 15:2:29 *)

(* feel free to mask some of the nodes by removing them from this file. *)

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

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

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

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

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

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

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

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

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

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

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

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);

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);

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

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

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

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);

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);

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

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

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

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

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);

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);

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

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);

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

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

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

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);

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

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);

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

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

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);

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);

node top (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 (OK: bool);

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