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