Project

General

Profile

Download (1.26 KB) Statistics
| Branch: | Tag: | Revision:
1
#open "mydouble_wrapper"
2
-- This file has been generated by CoCoSim
3

    
4

    
5
-- Extern nodes
6
node ControlSys_SFunction (in1_1: int; in2_1: int)
7
returns (SFunction_1_1: int)
8
let
9
	--! c_code: mydouble;
10
 
11
SFunction_1_1 = mydouble(in1_1, in2_1);
12

    
13
tel
14

    
15

    
16
-- Properties nodes
17
node example1_SafetyProp (In1_1_1 : int; In2_1_1 : int)
18
returns (Out1_1_1 : bool);
19
var
20
	LogicalOperator_1_1 : bool;
21
	RelationalOperator_1_1 : bool;
22
	In5_1_1 : int;
23
	i_virtual_local : real;
24
let
25
	LogicalOperator_1_1 = RelationalOperator_1_1 and (In5_1_1 != 0);
26
	RelationalOperator_1_1 = In1_1_1 >= In2_1_1;
27
	Out1_1_1 = LogicalOperator_1_1;
28
	i_virtual_local= 0.0 -> 1.0;
29

    
30
	In5_1_1 = example1(In2_1_1, In1_1_1);
31
	--%PROPERTY Out1_1_1; 
32
 
33
tel
34

    
35

    
36
-- System nodes
37
node example1 (In1_1_1 : int; In2_1_1 : int)
38
returns (Out1_1_1 : int); 
39
var
40
	ControlSys_SFunction_1_1 : int;
41
	ControlSys_System_RelationalOperator_1_1 : bool;
42
	ControlSys_System_Switch_1_1 : int;
43
	i_virtual_local : real;
44
let 
45
	(ControlSys_SFunction_1_1) = ControlSys_SFunction(In1_1_1, In2_1_1);
46
	ControlSys_System_RelationalOperator_1_1 = In1_1_1 >= ControlSys_SFunction_1_1;
47
	ControlSys_System_Switch_1_1 = if ControlSys_System_RelationalOperator_1_1 then In1_1_1 else ControlSys_SFunction_1_1;
48
	Out1_1_1 = ControlSys_System_Switch_1_1;
49
	i_virtual_local= 0.0 -> 1.0;
50
tel
51

    
(3-3/9)