lustrec-tests / tests / external_code / mydouble / s_function / example1.lus @ f5c07b4e
History | View | Annotate | Download (1.22 KB)
1 |
-- This file has been generated by CoCoSim |
---|---|
2 |
|
3 |
|
4 |
-- Extern nodes |
5 |
node ControlSys_SFunction (in1_1: int; in2_1: int) |
6 |
returns (SFunction_1_1: int) |
7 |
let |
8 |
--! c_code: mydouble; |
9 |
|
10 |
SFunction_1_1 = 0; |
11 |
|
12 |
tel |
13 |
|
14 |
|
15 |
-- Properties nodes |
16 |
node example1_SafetyProp (In1_1_1 : int; In2_1_1 : int) |
17 |
returns (Out1_1_1 : bool); |
18 |
var |
19 |
LogicalOperator_1_1 : bool; |
20 |
RelationalOperator_1_1 : bool; |
21 |
In5_1_1 : int; |
22 |
i_virtual_local : real; |
23 |
let |
24 |
LogicalOperator_1_1 = RelationalOperator_1_1 and (In5_1_1 != 0); |
25 |
RelationalOperator_1_1 = In1_1_1 >= In2_1_1; |
26 |
Out1_1_1 = LogicalOperator_1_1; |
27 |
i_virtual_local= 0.0 -> 1.0; |
28 |
|
29 |
In5_1_1 = example1(In2_1_1, In1_1_1); |
30 |
--%PROPERTY Out1_1_1; |
31 |
|
32 |
tel |
33 |
|
34 |
|
35 |
-- System nodes |
36 |
node example1 (In1_1_1 : int; In2_1_1 : int) |
37 |
returns (Out1_1_1 : int); |
38 |
var |
39 |
ControlSys_SFunction_1_1 : int; |
40 |
ControlSys_System_RelationalOperator_1_1 : bool; |
41 |
ControlSys_System_Switch_1_1 : int; |
42 |
i_virtual_local : real; |
43 |
let |
44 |
(ControlSys_SFunction_1_1) = ControlSys_SFunction(In1_1_1, In2_1_1); |
45 |
ControlSys_System_RelationalOperator_1_1 = In1_1_1 >= ControlSys_SFunction_1_1; |
46 |
ControlSys_System_Switch_1_1 = if ControlSys_System_RelationalOperator_1_1 then In1_1_1 else ControlSys_SFunction_1_1; |
47 |
Out1_1_1 = ControlSys_System_Switch_1_1; |
48 |
i_virtual_local= 0.0 -> 1.0; |
49 |
tel |
50 |
|