CristalCaveGem » LustreC » Lustrec-Tests

-- This file has been generated by cocoSim

-- System nodes

node Flowchart5_Flowchart5Junction807__To__Flowchart5_Flowchart5Junction808_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 :Flowchart5_A

node Flowchart5_A_en(idFlowchart5_A_1:int;

	idFlowchart5_Flowchart5_1:int;

	x_1:int;

	isInner:bool)

returns (idFlowchart5_A:int;

	idFlowchart5_Flowchart5:int;

	x:int);

var 	idFlowchart5_A_2, idFlowchart5_A_3, idFlowchart5_A_4:int;

	idFlowchart5_Flowchart5_2, idFlowchart5_Flowchart5_3, idFlowchart5_Flowchart5_4:int;

	x_2, x_3, x_4:int;

let

	-- set state as active 

	idFlowchart5_Flowchart5_2 

	= 806;

-- transition trace :

	--POINT__To__Junction807_1, Junction807__To__Junction808_1

		-- condition Action : x++;

		(x_2) 

	= Flowchart5_Flowchart5Junction807__To__Flowchart5_Flowchart5Junction808_1_Condition_Action(x_1);

	(idFlowchart5_A_2, idFlowchart5_Flowchart5_3, x_3) 

	= 

	if ( idFlowchart5_A_1 = 0) then

	 (idFlowchart5_A_1, idFlowchart5_Flowchart5_2, x_2)

	 else(idFlowchart5_A_1, idFlowchart5_Flowchart5_2, x_1);

	(idFlowchart5_A_3, idFlowchart5_Flowchart5_4, x_4) 

	= 

		 if ( idFlowchart5_A_1 = 0) then 

		(idFlowchart5_A_2, idFlowchart5_Flowchart5_3, x_3)

		 else (idFlowchart5_A_1, idFlowchart5_Flowchart5_2, x_1);

-- case of state without states but contains transitions 

	idFlowchart5_A_4 

	= -1;

	(idFlowchart5_A, idFlowchart5_Flowchart5, x) 

	= (idFlowchart5_A_4, idFlowchart5_Flowchart5_4, x_4);

tel

-- Exit action for state :Flowchart5_A

node Flowchart5_A_ex(idFlowchart5_Flowchart5_1:int;

	isInner:bool)

returns (idFlowchart5_Flowchart5:int);

var 	idFlowchart5_Flowchart5_2:int;

let

	-- set state as inactive 

	idFlowchart5_Flowchart5_2

	 = if (not isInner) then 0 else idFlowchart5_Flowchart5_1;

	(idFlowchart5_Flowchart5) 

	= (idFlowchart5_Flowchart5_1);

tel

--During action for state :Flowchart5_A

node Flowchart5_A_du(x_1:int)

returns (x:int);

let

		 automaton flowchart5_a_INNER

	state POINTFlowchart5_A_INNER:

	unless true restart FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1

	let

		(x) 

	= (x_1);

	tel

	state FLOWCHART5_A__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1:

	 var 	x_2:int;

	let

-- transition trace :

	--Flowchart5_A__To__Junction807_1, Junction807__To__Junction808_1

		-- condition Action : x++;

		(x_2) 

	= Flowchart5_Flowchart5Junction807__To__Flowchart5_Flowchart5Junction808_1_Condition_Action(x_1);

	(x) 

	=  (x_2);

	tel

	until true restart POINTFlowchart5_A_INNER

tel

--***************************************************State :Flowchart5_A Automaton***************************************************

node Flowchart5_A_node(idFlowchart5_A_1:int;

	x_1:int)

returns (idFlowchart5_A:int;

	x:int);

let

	 automaton flowchart5_a

	state POINTFlowchart5_A:

	unless (idFlowchart5_A_1=0) restart POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1

	let

		(idFlowchart5_A, x) 

	= (idFlowchart5_A_1, x_1);

	tel

	state POINT__TO__FLOWCHART5_FLOWCHART5JUNCTION807_1:

	 var 	x_2:int;

	let

-- transition trace :

	--POINT__To__Junction807_1, Junction807__To__Junction808_1

		-- condition Action : x++;

		(x_2) 

	= Flowchart5_Flowchart5Junction807__To__Flowchart5_Flowchart5Junction808_1_Condition_Action(x_1);

	(idFlowchart5_A, x) 

	=  (idFlowchart5_A_1, x_2);

	tel

	until true restart POINTFlowchart5_A

tel

--***************************************************State :Flowchart5_Flowchart5 Automaton***************************************************

node Flowchart5_Flowchart5_node(idFlowchart5_Flowchart5_1:int;

	idFlowchart5_A_1:int;

	x_1:int)

returns (idFlowchart5_Flowchart5:int;

	idFlowchart5_A:int;

	x:int);

let

	 automaton flowchart5_flowchart5

	state POINTFlowchart5_Flowchart5:

	unless (idFlowchart5_Flowchart5_1=0) restart POINT__TO__FLOWCHART5_A_1

	unless true  restart FLOWCHART5_FLOWCHART5_PARALLEL_IDL

	let

		(idFlowchart5_Flowchart5, idFlowchart5_A, x) 

	= (idFlowchart5_Flowchart5_1, idFlowchart5_A_1, x_1);

	tel

	state POINT__TO__FLOWCHART5_A_1:

	 var 	idFlowchart5_Flowchart5_2:int;

	idFlowchart5_A_2:int;

	x_2:int;

	let

		-- transition trace :

	--POINT__To__Flowchart5_A_1

		(idFlowchart5_A_2, idFlowchart5_Flowchart5_2, x_2) 

	= Flowchart5_A_en(idFlowchart5_A_1, idFlowchart5_Flowchart5_1, x_1, false);

	(idFlowchart5_Flowchart5, idFlowchart5_A, x) 

	=  (idFlowchart5_Flowchart5_2, idFlowchart5_A_2, x_2);

	tel

	until true restart POINTFlowchart5_Flowchart5

	state FLOWCHART5_FLOWCHART5_PARALLEL_IDL:

	 var 	idFlowchart5_A_2:int;

	x_2:int;

	let

		(idFlowchart5_A_2, x_2)

	= if not (idFlowchart5_A_1= 0 ) then Flowchart5_A_node(idFlowchart5_A_1, x_1)

		 else (idFlowchart5_A_1, x_1);

	(idFlowchart5_Flowchart5, idFlowchart5_A, x) 

	= (idFlowchart5_Flowchart5_1, idFlowchart5_A_2, x_2);

	tel

	until true restart POINTFlowchart5_Flowchart5

tel

--***************************************************State :Flowchart5_Flowchart5 Automaton***************************************************

node Flowchart5_Flowchart5(noInput :bool)

returns (x:int);

var x_1: int;

	idFlowchart5_Flowchart5, idFlowchart5_Flowchart5_1: int;

	idFlowchart5_A, idFlowchart5_A_1: int;

	let

	x_1 = 0 -> pre x;

	idFlowchart5_Flowchart5_1 = 0 -> pre idFlowchart5_Flowchart5;

	idFlowchart5_A_1 = 0 -> pre idFlowchart5_A;

	(idFlowchart5_Flowchart5, idFlowchart5_A, x)

	 = Flowchart5_Flowchart5_node(idFlowchart5_Flowchart5_1, idFlowchart5_A_1, x_1);

--unused outputs

tel

node Flowchart5 (i_virtual : real)

returns (Out1_1_1 : int); 

var

	Flowchart5_1_1 : int;

	i_virtual_local : real;

let 

	Flowchart5_1_1 =  Flowchart5_Flowchart5(true);

	Out1_1_1 = Flowchart5_1_1;

	i_virtual_local= 0.0 -> 1.0;

tel