CristalCaveGem » LustreC » Lustrec-Tests

-- This file has been generated by cocoSim

-- System nodes

node Flowchart4_A__To__Flowchart4_Flowchart4Junction799_1_Condition_Action(x_1:int)

returns (x:int);

var 	x_2:int;

let

	x_2 

	=  x_1  + 1;

	(x) 

	= (x_2);

tel

-- Entry action for state :Flowchart4_A

node Flowchart4_A_en(idFlowchart4_A_1:int;

	idFlowchart4_Flowchart4_1:int;

	isInner:bool)

returns (idFlowchart4_A:int;

	idFlowchart4_Flowchart4:int);

var 	idFlowchart4_A_2:int;

	idFlowchart4_Flowchart4_2:int;

let

	-- set state as active 

	idFlowchart4_Flowchart4_2 

	= 798;

	-- case of state without states but contains transitions 

	idFlowchart4_A_2 

	= -1;

	(idFlowchart4_A, idFlowchart4_Flowchart4) 

	= (idFlowchart4_A_2, idFlowchart4_Flowchart4_2);

tel

-- Exit action for state :Flowchart4_A

node Flowchart4_A_ex(idFlowchart4_Flowchart4_1:int;

	isInner:bool)

returns (idFlowchart4_Flowchart4:int);

var 	idFlowchart4_Flowchart4_2:int;

let

	-- set state as inactive 

	idFlowchart4_Flowchart4_2

	 = if (not isInner) then 0 else idFlowchart4_Flowchart4_1;

	(idFlowchart4_Flowchart4) 

	= (idFlowchart4_Flowchart4_1);

tel

--During action for state :Flowchart4_A

node Flowchart4_A_du(x_1:int)

returns (x:int);

let

		 automaton flowchart4_a_INNER

	state POINTFlowchart4_A_INNER:

	unless true restart FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1

	let

		(x) 

	= (x_1);

	tel

	state FLOWCHART4_A__TO__FLOWCHART4_FLOWCHART4JUNCTION799_1:

	 var 	x_2:int;

	let

		-- transition trace :

	--Flowchart4_A__To__Junction799_1

		-- condition Action : x++;

		(x_2) 

	= Flowchart4_A__To__Flowchart4_Flowchart4Junction799_1_Condition_Action(x_1);

	(x) 

	=  (x_2);

	tel

	until true restart POINTFlowchart4_A_INNER

tel

--***************************************************State :Flowchart4_A Automaton***************************************************

node Flowchart4_A_node(idFlowchart4_A_1:int)

returns (idFlowchart4_A:int);

let

	 automaton flowchart4_a

	state POINTFlowchart4_A:

	let

		(idFlowchart4_A) 

	= (idFlowchart4_A_1);

	tel

tel

--***************************************************State :Flowchart4_Flowchart4 Automaton***************************************************

node Flowchart4_Flowchart4_node(idFlowchart4_Flowchart4_1:int;

	idFlowchart4_A_1:int;

	x_1:int)

returns (idFlowchart4_Flowchart4:int;

	idFlowchart4_A:int;

	x:int);

let

	 automaton flowchart4_flowchart4

	state POINTFlowchart4_Flowchart4:

	unless (idFlowchart4_Flowchart4_1=0) restart POINT__TO__FLOWCHART4_A_1

	unless (idFlowchart4_Flowchart4_1=798) restart FLOWCHART4_A_IDL

	let

		(idFlowchart4_Flowchart4, idFlowchart4_A, x) 

	= (idFlowchart4_Flowchart4_1, idFlowchart4_A_1, x_1);

	tel

	state POINT__TO__FLOWCHART4_A_1:

	 var 	idFlowchart4_Flowchart4_2:int;

	idFlowchart4_A_2:int;

	let

		-- transition trace :

	--POINT__To__Flowchart4_A_1

		(idFlowchart4_A_2, idFlowchart4_Flowchart4_2) 

	= Flowchart4_A_en(idFlowchart4_A_1, idFlowchart4_Flowchart4_1, false);

	(idFlowchart4_Flowchart4, idFlowchart4_A) 

	=  (idFlowchart4_Flowchart4_2, idFlowchart4_A_2);

	--add unused variables

	(x) 

	= (x_1);

	tel

	until true restart POINTFlowchart4_Flowchart4

	state FLOWCHART4_A_IDL:

	 var 	idFlowchart4_A_2:int;

	x_2:int;

	let

	(x_2) 

	= Flowchart4_A_du(x_1);

	(idFlowchart4_A_2) 

	= Flowchart4_A_node(idFlowchart4_A_1);

	(idFlowchart4_Flowchart4, idFlowchart4_A, x) 

	= (idFlowchart4_Flowchart4_1, idFlowchart4_A_2, x_2);

	tel

	until true restart POINTFlowchart4_Flowchart4

tel

--***************************************************State :Flowchart4_Flowchart4 Automaton***************************************************

node Flowchart4_Flowchart4(noInput :bool)

returns (x:int);

var x_1: int;

	idFlowchart4_Flowchart4, idFlowchart4_Flowchart4_1: int;

	idFlowchart4_A, idFlowchart4_A_1: int;

	let

	x_1 = 0 -> pre x;

	idFlowchart4_Flowchart4_1 = 0 -> pre idFlowchart4_Flowchart4;

	idFlowchart4_A_1 = 0 -> pre idFlowchart4_A;

	(idFlowchart4_Flowchart4, idFlowchart4_A, x)

	 = Flowchart4_Flowchart4_node(idFlowchart4_Flowchart4_1, idFlowchart4_A_1, x_1);

--unused outputs

tel

node Flowchart4 (i_virtual : real)

returns (Out1_1_1 : int); 

var

	Flowchart4_1_1 : int;

	i_virtual_local : real;

let 

	Flowchart4_1_1 =  Flowchart4_Flowchart4(true);

	Out1_1_1 = Flowchart4_1_1;

	i_virtual_local= 0.0 -> 1.0;

tel