Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / large / BROKEN / steam_boiler_no_arr2_e3_514_e4_11150.lusi @ b8dc00eb

History | View | Annotate | Download (8.52 KB)

1
(* Generated Lustre Interface file from steam_boiler_no_arr2_e3_514_e4_11150.lus *)
2
(* generated by Lustre-C compiler version 284, 2014/5/25, 15:2:25 *)
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 REDGE (S: bool) returns (REDGE: bool);
60

    
61

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

    
64

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

    
67

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

    
70

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

    
73

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

    
76

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

    
79

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

    
82

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

    
85

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

    
88

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

    
91

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

    
94

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

    
97

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

    
100

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

    
103

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

    
106

    
107
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);
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 (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);
114

    
115

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

    
118