CristalCaveGem » LustreC » Lustrec-Tests

-- This file has been generated by cocoSim

-- System nodes

node Flowchart10_A__To__Flowchart10_Flowchart10Junction755_2_Condition_Action(y_1:int)

returns (y:int);

var 	y_2:int;

let

	y_2 

	=  y_1 +2;

	(y) 

	= (y_2);

tel

node Flowchart10_A__To__Flowchart10_Flowchart10Junction756_1_Condition_Action(y_1:int)

returns (y:int);

var 	y_2:int;

let

	y_2 

	=  y_1 -2;

	(y) 

	= (y_2);

tel

node POINT__To__Flowchart10_Flowchart10Junction754_2_Condition_Action(y_1:int)

returns (y:int);

var 	y_2:int;

let

	y_2 

	=  y_1  - 1;

	(y) 

	= (y_2);

tel

node POINT__To__Flowchart10_Flowchart10Junction753_1_Condition_Action(y_1:int)

returns (y:int);

var 	y_2:int;

let

	y_2 

	=  y_1  + 1;

	(y) 

	= (y_2);

tel

-- Entry action for state :Flowchart10_A

node Flowchart10_A_en(idFlowchart10_A_1:int;

	idFlowchart10_Flowchart10_1:int;

	x:int;

	y_1:int;

	isInner:bool)

returns (idFlowchart10_A:int;

	idFlowchart10_Flowchart10:int;

	y:int);

var 	idFlowchart10_A_2, idFlowchart10_A_3, idFlowchart10_A_4:int;

	idFlowchart10_Flowchart10_2, idFlowchart10_Flowchart10_3, idFlowchart10_Flowchart10_4:int;

	y_2, y_3, y_4, y_5:int;

let

	-- set state as active 

	idFlowchart10_Flowchart10_2 

	= 752;

-- transition trace :

	--POINT__To__Junction753_1

		-- condition Action : y++;

		(y_2) 

	= 

		 if (( x=0 )) then 

		POINT__To__Flowchart10_Flowchart10Junction753_1_Condition_Action(y_1)

		 else (y_1);

-- transition trace :

	--POINT__To__Junction754_2

		-- condition Action : y--;

		(y_3) 

	= 

		 if (( x>0 )) then 

		POINT__To__Flowchart10_Flowchart10Junction754_2_Condition_Action(y_1)

		 else (y_1);

	(idFlowchart10_A_2, idFlowchart10_Flowchart10_3, y_4) 

	= 

	if ( idFlowchart10_A_1 = 0) then

		 if (( x=0 )) then 

		(idFlowchart10_A_1, idFlowchart10_Flowchart10_2, y_2)

		 else

		 if (( x>0 )) then 

		(idFlowchart10_A_1, idFlowchart10_Flowchart10_2, y_3)

		 else (idFlowchart10_A_1, idFlowchart10_Flowchart10_2, y_1)

	 else(idFlowchart10_A_1, idFlowchart10_Flowchart10_2, y_1);

	(idFlowchart10_A_3, idFlowchart10_Flowchart10_4, y_5) 

	= 

		 if ( idFlowchart10_A_1 = 0) then 

		(idFlowchart10_A_2, idFlowchart10_Flowchart10_3, y_4)

		 else (idFlowchart10_A_1, idFlowchart10_Flowchart10_2, y_1);

-- case of state without states but contains transitions 

	idFlowchart10_A_4 

	= -1;

	(idFlowchart10_A, idFlowchart10_Flowchart10, y) 

	= (idFlowchart10_A_4, idFlowchart10_Flowchart10_4, y_5);

tel

-- Exit action for state :Flowchart10_A

node Flowchart10_A_ex(idFlowchart10_Flowchart10_1:int;

	isInner:bool)

returns (idFlowchart10_Flowchart10:int);

var 	idFlowchart10_Flowchart10_2:int;

let

	-- set state as inactive 

	idFlowchart10_Flowchart10_2

	 = if (not isInner) then 0 else idFlowchart10_Flowchart10_1;

	(idFlowchart10_Flowchart10) 

	= (idFlowchart10_Flowchart10_1);

tel

--During action for state :Flowchart10_A

node Flowchart10_A_du(x:int;

	y_1:int)

returns (y:int);

let

		 automaton flowchart10_a_INNER

	state POINTFlowchart10_A_INNER:

	unless true and ( x>0 ) restart FLOWCHART10_A__TO__FLOWCHART10_FLOWCHART10JUNCTION756_1

	unless true and ( x=0 ) restart FLOWCHART10_A__TO__FLOWCHART10_FLOWCHART10JUNCTION755_2

	let

		(y) 

	= (y_1);

	tel

	state FLOWCHART10_A__TO__FLOWCHART10_FLOWCHART10JUNCTION756_1:

	 var 	y_2:int;

	let

		-- transition trace :

	--Flowchart10_A__To__Junction756_1

		-- condition Action : y-=2;

		(y_2) 

	= Flowchart10_A__To__Flowchart10_Flowchart10Junction756_1_Condition_Action(y_1);

	(y) 

	=  (y_2);

	tel

	until true restart POINTFlowchart10_A_INNER

	state FLOWCHART10_A__TO__FLOWCHART10_FLOWCHART10JUNCTION755_2:

	 var 	y_2:int;

	let

		-- transition trace :

	--Flowchart10_A__To__Junction755_2

		-- condition Action : y+=2;

		(y_2) 

	= Flowchart10_A__To__Flowchart10_Flowchart10Junction755_2_Condition_Action(y_1);

	(y) 

	=  (y_2);

	tel

	until true restart POINTFlowchart10_A_INNER

tel

--***************************************************State :Flowchart10_A Automaton***************************************************

node Flowchart10_A_node(idFlowchart10_A_1:int;

	x:int;

	y_1:int)

returns (idFlowchart10_A:int;

	y:int);

let

	 automaton flowchart10_a

	state POINTFlowchart10_A:

	unless (idFlowchart10_A_1=0) and ( x=0 ) restart POINT__TO__FLOWCHART10_FLOWCHART10JUNCTION753_1

	unless (idFlowchart10_A_1=0) and ( x>0 ) restart POINT__TO__FLOWCHART10_FLOWCHART10JUNCTION754_2

	let

		(idFlowchart10_A, y) 

	= (idFlowchart10_A_1, y_1);

	tel

	state POINT__TO__FLOWCHART10_FLOWCHART10JUNCTION753_1:

	 var 	y_2:int;

	let

		-- transition trace :

	--POINT__To__Junction753_1

		-- condition Action : y++;

		(y_2) 

	= POINT__To__Flowchart10_Flowchart10Junction753_1_Condition_Action(y_1);

	(idFlowchart10_A, y) 

	=  (idFlowchart10_A_1, y_2);

	tel

	until true restart POINTFlowchart10_A

	state POINT__TO__FLOWCHART10_FLOWCHART10JUNCTION754_2:

	 var 	y_2:int;

	let

		-- transition trace :

	--POINT__To__Junction754_2

		-- condition Action : y--;

		(y_2) 

	= POINT__To__Flowchart10_Flowchart10Junction754_2_Condition_Action(y_1);

	(idFlowchart10_A, y) 

	=  (idFlowchart10_A_1, y_2);

	tel

	until true restart POINTFlowchart10_A

tel

--***************************************************State :Flowchart10_Flowchart10 Automaton***************************************************

node Flowchart10_Flowchart10_node(idFlowchart10_Flowchart10_1:int;

	idFlowchart10_A_1:int;

	x:int;

	y_1:int)

returns (idFlowchart10_Flowchart10:int;

	idFlowchart10_A:int;

	y:int);

let

	 automaton flowchart10_flowchart10

	state POINTFlowchart10_Flowchart10:

	unless (idFlowchart10_Flowchart10_1=0) restart POINT__TO__FLOWCHART10_A_1

	unless true  restart FLOWCHART10_FLOWCHART10_PARALLEL_IDL

	let

		(idFlowchart10_Flowchart10, idFlowchart10_A, y) 

	= (idFlowchart10_Flowchart10_1, idFlowchart10_A_1, y_1);

	tel

	state POINT__TO__FLOWCHART10_A_1:

	 var 	idFlowchart10_Flowchart10_2:int;

	idFlowchart10_A_2:int;

	y_2:int;

	let

		-- transition trace :

	--POINT__To__Flowchart10_A_1

		(idFlowchart10_A_2, idFlowchart10_Flowchart10_2, y_2) 

	= Flowchart10_A_en(idFlowchart10_A_1, idFlowchart10_Flowchart10_1, x, y_1, false);

	(idFlowchart10_Flowchart10, idFlowchart10_A, y) 

	=  (idFlowchart10_Flowchart10_2, idFlowchart10_A_2, y_2);

	tel

	until true restart POINTFlowchart10_Flowchart10

	state FLOWCHART10_FLOWCHART10_PARALLEL_IDL:

	 var 	idFlowchart10_A_2:int;

	y_2:int;

	let

		(idFlowchart10_A_2, y_2)

	= if not (idFlowchart10_A_1= 0 ) then Flowchart10_A_node(idFlowchart10_A_1, x, y_1)

		 else (idFlowchart10_A_1, y_1);

	(idFlowchart10_Flowchart10, idFlowchart10_A, y) 

	= (idFlowchart10_Flowchart10_1, idFlowchart10_A_2, y_2);

	tel

	until true restart POINTFlowchart10_Flowchart10

tel

--***************************************************State :Flowchart10_Flowchart10 Automaton***************************************************

node Flowchart10_Flowchart10(x:int)

returns (y:int);

var y_1: int;

	idFlowchart10_Flowchart10, idFlowchart10_Flowchart10_1: int;

	idFlowchart10_A, idFlowchart10_A_1: int;

	let

	y_1 = 0 -> pre y;

	idFlowchart10_Flowchart10_1 = 0 -> pre idFlowchart10_Flowchart10;

	idFlowchart10_A_1 = 0 -> pre idFlowchart10_A;

	(idFlowchart10_Flowchart10, idFlowchart10_A, y)

	 = Flowchart10_Flowchart10_node(idFlowchart10_Flowchart10_1, idFlowchart10_A_1, x, y_1);

--unused outputs

tel

node Flowchart10 (x_1_1 : int)

returns (y_1_1 : int); 

var

	Flowchart10_1_1 : int;

	i_virtual_local : real;

let 

	Flowchart10_1_1 =  Flowchart10_Flowchart10(x_1_1);

	y_1_1 = Flowchart10_1_1;

	i_virtual_local= 0.0 -> 1.0;

tel