CristalCaveGem » LustreC » Lustrec-Tests

-- This file has been generated by CoCoSim

-- Extern nodes

node ControlSys_SFunction (in1_1: int; in2_1: int)

returns (SFunction_1_1: int)

let

	--! c_code: mydouble;

SFunction_1_1 = 0;

tel

-- Properties nodes

node example1_SafetyProp (In1_1_1 : int; In2_1_1 : int)

returns (Out1_1_1 : bool);

var

	LogicalOperator_1_1 : bool;

	RelationalOperator_1_1 : bool;

	In5_1_1 : int;

	i_virtual_local : real;

let

	LogicalOperator_1_1 = RelationalOperator_1_1 and (In5_1_1 != 0);

	RelationalOperator_1_1 = In1_1_1 >= In2_1_1;

	Out1_1_1 = LogicalOperator_1_1;

	i_virtual_local= 0.0 -> 1.0;

	In5_1_1 = example1(In2_1_1, In1_1_1);

	--%PROPERTY Out1_1_1; 

tel

-- System nodes

node example1 (In1_1_1 : int; In2_1_1 : int)

returns (Out1_1_1 : int); 

var

	ControlSys_SFunction_1_1 : int;

	ControlSys_System_RelationalOperator_1_1 : bool;

	ControlSys_System_Switch_1_1 : int;

	i_virtual_local : real;

let 

	(ControlSys_SFunction_1_1) = ControlSys_SFunction(In1_1_1, In2_1_1);

	ControlSys_System_RelationalOperator_1_1 = In1_1_1 >= ControlSys_SFunction_1_1;

	ControlSys_System_Switch_1_1 = if ControlSys_System_RelationalOperator_1_1 then In1_1_1 else ControlSys_SFunction_1_1;

	Out1_1_1 = ControlSys_System_Switch_1_1;

	i_virtual_local= 0.0 -> 1.0;

tel