CristalCaveGem » LustreC » Lustrec-Tests

-- This file has been generated by cocoSim

-- System nodes

node POINT__To__Flowchart2_Flowchart2Junction783_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 :Flowchart2_A

node Flowchart2_A_en(idFlowchart2_A_1:int;

	idFlowchart2_Flowchart2_1:int;

	x_1:int;

	isInner:bool)

returns (idFlowchart2_A:int;

	idFlowchart2_Flowchart2:int;

	x:int);

var 	idFlowchart2_A_2, idFlowchart2_A_3, idFlowchart2_A_4:int;

	idFlowchart2_Flowchart2_2, idFlowchart2_Flowchart2_3, idFlowchart2_Flowchart2_4:int;

	x_2, x_3, x_4, x_5:int;

let

	-- set state as active 

	idFlowchart2_Flowchart2_2 

	= 782;

	x_2 

	= if (not isInner) then 1000

	 else x_1;

-- transition trace :

	--POINT__To__Junction783_1

		-- condition Action : x++;

		(x_3) 

	= POINT__To__Flowchart2_Flowchart2Junction783_1_Condition_Action(x_2);

	(idFlowchart2_A_2, idFlowchart2_Flowchart2_3, x_4) 

	= 

	if ( idFlowchart2_A_1 = 0) then

	 (idFlowchart2_A_1, idFlowchart2_Flowchart2_2, x_3)

	 else(idFlowchart2_A_1, idFlowchart2_Flowchart2_2, x_2);

	(idFlowchart2_A_3, idFlowchart2_Flowchart2_4, x_5) 

	= 

		 if ( idFlowchart2_A_1 = 0) then 

		(idFlowchart2_A_2, idFlowchart2_Flowchart2_3, x_4)

		 else (idFlowchart2_A_1, idFlowchart2_Flowchart2_2, x_2);

-- case of state without states but contains transitions 

	idFlowchart2_A_4 

	= -1;

	(idFlowchart2_A, idFlowchart2_Flowchart2, x) 

	= (idFlowchart2_A_4, idFlowchart2_Flowchart2_4, x_5);

tel

--During action for state :Flowchart2_A

node Flowchart2_A_du(x_1:int)

returns (x:int);

var 	x_2:int;

let

	x_2 

	=  x_1  - 1;

	(x) 

	= (x_2);

tel

-- Exit action for state :Flowchart2_A

node Flowchart2_A_ex(idFlowchart2_Flowchart2_1:int;

	isInner:bool)

returns (idFlowchart2_Flowchart2:int);

var 	idFlowchart2_Flowchart2_2:int;

let

	-- set state as inactive 

	idFlowchart2_Flowchart2_2

	 = if (not isInner) then 0 else idFlowchart2_Flowchart2_1;

	(idFlowchart2_Flowchart2) 

	= (idFlowchart2_Flowchart2_1);

tel

--***************************************************State :Flowchart2_A Automaton***************************************************

node Flowchart2_A_node(idFlowchart2_A_1:int;

	x_1:int)

returns (idFlowchart2_A:int;

	x:int);

let

	 automaton flowchart2_a

	state POINTFlowchart2_A:

	unless (idFlowchart2_A_1=0) restart POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1

	let

		(idFlowchart2_A, x) 

	= (idFlowchart2_A_1, x_1);

	tel

	state POINT__TO__FLOWCHART2_FLOWCHART2JUNCTION783_1:

	 var 	x_2:int;

	let

		-- transition trace :

	--POINT__To__Junction783_1

		-- condition Action : x++;

		(x_2) 

	= POINT__To__Flowchart2_Flowchart2Junction783_1_Condition_Action(x_1);

	(idFlowchart2_A, x) 

	=  (idFlowchart2_A_1, x_2);

	tel

	until true restart POINTFlowchart2_A

tel

--***************************************************State :Flowchart2_Flowchart2 Automaton***************************************************

node Flowchart2_Flowchart2_node(idFlowchart2_Flowchart2_1:int;

	idFlowchart2_A_1:int;

	x_1:int)

returns (idFlowchart2_Flowchart2:int;

	idFlowchart2_A:int;

	x:int);

let

	 automaton flowchart2_flowchart2

	state POINTFlowchart2_Flowchart2:

	unless (idFlowchart2_Flowchart2_1=0) restart POINT__TO__FLOWCHART2_A_1

	unless (idFlowchart2_Flowchart2_1=782) restart FLOWCHART2_A_IDL

	let

		(idFlowchart2_Flowchart2, idFlowchart2_A, x) 

	= (idFlowchart2_Flowchart2_1, idFlowchart2_A_1, x_1);

	tel

	state POINT__TO__FLOWCHART2_A_1:

	 var 	idFlowchart2_Flowchart2_2:int;

	idFlowchart2_A_2:int;

	x_2:int;

	let

		-- transition trace :

	--POINT__To__Flowchart2_A_1

		(idFlowchart2_A_2, idFlowchart2_Flowchart2_2, x_2) 

	= Flowchart2_A_en(idFlowchart2_A_1, idFlowchart2_Flowchart2_1, x_1, false);

	(idFlowchart2_Flowchart2, idFlowchart2_A, x) 

	=  (idFlowchart2_Flowchart2_2, idFlowchart2_A_2, x_2);

	tel

	until true restart POINTFlowchart2_Flowchart2

	state FLOWCHART2_A_IDL:

	 var 	idFlowchart2_A_2:int;

	x_2, x_3:int;

	let

	(x_2) 

	= Flowchart2_A_du(x_1);

	(idFlowchart2_A_2, x_3) 

	= Flowchart2_A_node(idFlowchart2_A_1, x_2);

	(idFlowchart2_Flowchart2, idFlowchart2_A, x) 

	= (idFlowchart2_Flowchart2_1, idFlowchart2_A_2, x_3);

	tel

	until true restart POINTFlowchart2_Flowchart2

tel

--***************************************************State :Flowchart2_Flowchart2 Automaton***************************************************

node Flowchart2_Flowchart2(noInput :bool)

returns (x:int);

var x_1: int;

	idFlowchart2_Flowchart2, idFlowchart2_Flowchart2_1: int;

	idFlowchart2_A, idFlowchart2_A_1: int;

	let

	x_1 = 0 -> pre x;

	idFlowchart2_Flowchart2_1 = 0 -> pre idFlowchart2_Flowchart2;

	idFlowchart2_A_1 = 0 -> pre idFlowchart2_A;

	(idFlowchart2_Flowchart2, idFlowchart2_A, x)

	 = Flowchart2_Flowchart2_node(idFlowchart2_Flowchart2_1, idFlowchart2_A_1, x_1);

--unused outputs

tel

node Flowchart2 (i_virtual : real)

returns (Out1_1_1 : int); 

var

	Flowchart2_1_1 : int;

	i_virtual_local : real;

let 

	Flowchart2_1_1 =  Flowchart2_Flowchart2(true);

	Out1_1_1 = Flowchart2_1_1;

	i_virtual_local= 0.0 -> 1.0;

tel