CristalCaveGem » LustreC » Lustrec-Tests

-- This file has been generated by cocoSim

-- System nodes

node Flowchart3_A__To__Flowchart3_Flowchart3Junction791_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 :Flowchart3_A

node Flowchart3_A_en(idFlowchart3_A_1:int;

	idFlowchart3_Flowchart3_1:int;

	isInner:bool)

returns (idFlowchart3_A:int;

	idFlowchart3_Flowchart3:int);

var 	idFlowchart3_A_2:int;

	idFlowchart3_Flowchart3_2:int;

let

	-- set state as active 

	idFlowchart3_Flowchart3_2 

	= 790;

	-- case of state without states but contains transitions 

	idFlowchart3_A_2 

	= -1;

	(idFlowchart3_A, idFlowchart3_Flowchart3) 

	= (idFlowchart3_A_2, idFlowchart3_Flowchart3_2);

tel

-- Exit action for state :Flowchart3_A

node Flowchart3_A_ex(idFlowchart3_Flowchart3_1:int;

	isInner:bool)

returns (idFlowchart3_Flowchart3:int);

var 	idFlowchart3_Flowchart3_2:int;

let

	-- set state as inactive 

	idFlowchart3_Flowchart3_2

	 = if (not isInner) then 0 else idFlowchart3_Flowchart3_1;

	(idFlowchart3_Flowchart3) 

	= (idFlowchart3_Flowchart3_1);

tel

--During action for state :Flowchart3_A

node Flowchart3_A_du(x_1:int)

returns (x:int);

let

		 automaton flowchart3_a_INNER

	state POINTFlowchart3_A_INNER:

	unless true restart FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1

	let

		(x) 

	= (x_1);

	tel

	state FLOWCHART3_A__TO__FLOWCHART3_FLOWCHART3JUNCTION791_1:

	 var 	x_2:int;

	let

		-- transition trace :

	--Flowchart3_A__To__Junction791_1

		-- condition Action : x++;

		(x_2) 

	= Flowchart3_A__To__Flowchart3_Flowchart3Junction791_1_Condition_Action(x_1);

	(x) 

	=  (x_2);

	tel

	until true restart POINTFlowchart3_A_INNER

tel

--***************************************************State :Flowchart3_A Automaton***************************************************

node Flowchart3_A_node(idFlowchart3_A_1:int)

returns (idFlowchart3_A:int);

let

	 automaton flowchart3_a

	state POINTFlowchart3_A:

	let

		(idFlowchart3_A) 

	= (idFlowchart3_A_1);

	tel

tel

--***************************************************State :Flowchart3_Flowchart3 Automaton***************************************************

node Flowchart3_Flowchart3_node(idFlowchart3_Flowchart3_1:int;

	idFlowchart3_A_1:int)

returns (idFlowchart3_Flowchart3:int;

	idFlowchart3_A:int);

let

	 automaton flowchart3_flowchart3

	state POINTFlowchart3_Flowchart3:

	unless (idFlowchart3_Flowchart3_1=0) restart POINT__TO__FLOWCHART3_A_1

	unless true  restart FLOWCHART3_FLOWCHART3_PARALLEL_IDL

	let

		(idFlowchart3_Flowchart3, idFlowchart3_A) 

	= (idFlowchart3_Flowchart3_1, idFlowchart3_A_1);

	tel

	state POINT__TO__FLOWCHART3_A_1:

	 var 	idFlowchart3_Flowchart3_2:int;

	idFlowchart3_A_2:int;

	let

		-- transition trace :

	--POINT__To__Flowchart3_A_1

		(idFlowchart3_A_2, idFlowchart3_Flowchart3_2) 

	= Flowchart3_A_en(idFlowchart3_A_1, idFlowchart3_Flowchart3_1, false);

	(idFlowchart3_Flowchart3, idFlowchart3_A) 

	=  (idFlowchart3_Flowchart3_2, idFlowchart3_A_2);

	tel

	until true restart POINTFlowchart3_Flowchart3

	state FLOWCHART3_FLOWCHART3_PARALLEL_IDL:

	 var 	idFlowchart3_A_2:int;

	let

		(idFlowchart3_A_2)

	= if not (idFlowchart3_A_1= 0 ) then Flowchart3_A_node(idFlowchart3_A_1)

		 else (idFlowchart3_A_1);

	(idFlowchart3_Flowchart3, idFlowchart3_A) 

	= (idFlowchart3_Flowchart3_1, idFlowchart3_A_2);

	tel

	until true restart POINTFlowchart3_Flowchart3

tel

--***************************************************State :Flowchart3_Flowchart3 Automaton***************************************************

node Flowchart3_Flowchart3(noInput :bool)

returns (x:int);

var x_1: int;

	idFlowchart3_Flowchart3, idFlowchart3_Flowchart3_1: int;

	idFlowchart3_A, idFlowchart3_A_1: int;

	let

	x_1 = 0 -> pre x;

	idFlowchart3_Flowchart3_1 = 0 -> pre idFlowchart3_Flowchart3;

	idFlowchart3_A_1 = 0 -> pre idFlowchart3_A;

	(idFlowchart3_Flowchart3, idFlowchart3_A)

	 = Flowchart3_Flowchart3_node(idFlowchart3_Flowchart3_1, idFlowchart3_A_1);

--unused outputs

	x = 0;

tel

node Flowchart3 (i_virtual : real)

returns (Out1_1_1 : int); 

var

	Flowchart3_1_1 : int;

	i_virtual_local : real;

let 

	Flowchart3_1_1 =  Flowchart3_Flowchart3(true);

	Out1_1_1 = Flowchart3_1_1;

	i_virtual_local= 0.0 -> 1.0;

tel