CristalCaveGem » LustreC » Lustrec-Tests

-- This file has been generated by cocoSim

-- System nodes

node Junctions5_A__To__Junctions5_Junctions5Junction1286_2_Condition_Action(a_1:real)

returns (a:real);

var 	a_2:real;

let

	a_2 

	=  a_1 +1.;

	(a) 

	= (a_2);

tel

node Junctions5_A__To__Junctions5_Junctions5Junction1286_1_Condition_Action(a_1:real)

returns (a:real);

var 	a_2:real;

let

	a_2 

	=  a_1 +10.;

	(a) 

	= (a_2);

tel

node Junctions5_Junctions5Junction1287__To__Junctions5_B_1_Condition_Action(a_1:real)

returns (a:real);

var 	a_2:real;

let

	a_2 

	=  a_1 +1000.;

	(a) 

	= (a_2);

tel

node Junctions5_Junctions5Junction1286__To__Junctions5_Junctions5Junction1287_1_Condition_Action(a_1:real)

returns (a:real);

var 	a_2:real;

let

	a_2 

	=  a_1 +100.;

	(a) 

	= (a_2);

tel

-- Exit action for state :Junctions5_A

node Junctions5_A_ex(a_1:real;

	idJunctions5_Junctions5_1:int;

	isInner:bool)

returns (a:real;

	idJunctions5_Junctions5:int);

var 	a_2:real;

	idJunctions5_Junctions5_2:int;

let

	a_2 

	= if (not isInner) then  a_1 +10000.

	 else a_1;

	-- set state as inactive 

	idJunctions5_Junctions5_2

	 = if (not isInner) then 0 else idJunctions5_Junctions5_1;

	(a, idJunctions5_Junctions5) 

	= (a_2, idJunctions5_Junctions5_1);

tel

-- Entry action for state :Junctions5_A

node Junctions5_A_en(idJunctions5_Junctions5_1:int;

	isInner:bool)

returns (idJunctions5_Junctions5:int);

var 	idJunctions5_Junctions5_2:int;

let

	-- set state as active 

	idJunctions5_Junctions5_2 

	= 1282;

	(idJunctions5_Junctions5) 

	= (idJunctions5_Junctions5_2);

tel

-- Exit action for state :Junctions5_B

node Junctions5_B_ex(a_1:real;

	idJunctions5_Junctions5_1:int;

	isInner:bool)

returns (a:real;

	idJunctions5_Junctions5:int);

var 	a_2:real;

	idJunctions5_Junctions5_2:int;

let

	a_2 

	= if (not isInner) then 0.

	 else a_1;

	-- set state as inactive 

	idJunctions5_Junctions5_2

	 = if (not isInner) then 0 else idJunctions5_Junctions5_1;

	(a, idJunctions5_Junctions5) 

	= (a_2, idJunctions5_Junctions5_1);

tel

-- Entry action for state :Junctions5_B

node Junctions5_B_en(idJunctions5_Junctions5_1:int;

	isInner:bool)

returns (idJunctions5_Junctions5:int);

var 	idJunctions5_Junctions5_2:int;

let

	-- set state as active 

	idJunctions5_Junctions5_2 

	= 1283;

	(idJunctions5_Junctions5) 

	= (idJunctions5_Junctions5_2);

tel

--***************************************************State :Junctions5_Junctions5 Automaton***************************************************

node Junctions5_Junctions5_node(idJunctions5_Junctions5_1:int;

	x:int;

	a_1:real)

returns (idJunctions5_Junctions5:int;

	a:real);

let

	 automaton junctions5_junctions5

	state POINTJunctions5_Junctions5:

	unless (idJunctions5_Junctions5_1=0) restart POINT__TO__JUNCTIONS5_A_1

	unless (idJunctions5_Junctions5_1=1282) and ( x mod 3=1 ) restart JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1

	unless (idJunctions5_Junctions5_1=1282) and ( x mod 3=0 ) restart JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2

	unless (idJunctions5_Junctions5_1=1282) restart JUNCTIONS5_A_IDL

	unless (idJunctions5_Junctions5_1=1283) restart JUNCTIONS5_B_IDL

	let

		(idJunctions5_Junctions5, a) 

	= (idJunctions5_Junctions5_1, a_1);

	tel

	state POINT__TO__JUNCTIONS5_A_1:

	 var 	idJunctions5_Junctions5_2:int;

	let

		-- transition trace :

	--POINT__To__Junctions5_A_1

		(idJunctions5_Junctions5_2) 

	= Junctions5_A_en(idJunctions5_Junctions5_1, false);

	(idJunctions5_Junctions5) 

	=  (idJunctions5_Junctions5_2);

	--add unused variables

	(a) 

	= (a_1);

	tel

	until true restart POINTJunctions5_Junctions5

	state JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1:

	 var 	idJunctions5_Junctions5_2, idJunctions5_Junctions5_3:int;

	a_2, a_3, a_4, a_5:real;

	let

-- transition trace :

	--Junctions5_A__To__Junction1286_1, Junction1286__To__Junction1287_1, Junction1287__To__Junctions5_B_1

		-- condition Action : a+=10

		(a_2) 

	= Junctions5_A__To__Junctions5_Junctions5Junction1286_1_Condition_Action(a_1);

		-- condition Action : a+=100

		(a_3) 

	= 

		 if (( x>=2 )) then 

		Junctions5_Junctions5Junction1286__To__Junctions5_Junctions5Junction1287_1_Condition_Action(a_2)

		 else (a_2);

		-- condition Action : a+=1000

		(a_4) 

	= 

		 if (( x>=2 ) and ( x>=4 )) then 

		Junctions5_Junctions5Junction1287__To__Junctions5_B_1_Condition_Action(a_3)

		 else (a_3);

		(a_5, idJunctions5_Junctions5_2) 

	= 

		 if (( x>=2 ) and ( x>=4 )) then 

		Junctions5_A_ex(a_4, idJunctions5_Junctions5_1, false)

		 else (a_4, idJunctions5_Junctions5_1);

		(idJunctions5_Junctions5_3) 

	= 

		 if (( x>=2 ) and ( x>=4 )) then 

		Junctions5_B_en(idJunctions5_Junctions5_2, false)

		 else (idJunctions5_Junctions5_2);

	(idJunctions5_Junctions5, a) 

	= 

		 if (( x>=2 ) and ( x>=4 )) then 

		(idJunctions5_Junctions5_3, a_5)

		 else

		 if (( x>=2 )) then 

		(idJunctions5_Junctions5_1, a_3)

		 else (idJunctions5_Junctions5_1, a_2);

	tel

	until true restart POINTJunctions5_Junctions5

	state JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2:

	 var 	idJunctions5_Junctions5_2, idJunctions5_Junctions5_3:int;

	a_2, a_3, a_4, a_5:real;

	let

-- transition trace :

	--Junctions5_A__To__Junction1286_2, Junction1286__To__Junction1287_1, Junction1287__To__Junctions5_B_1

		-- condition Action : a+=1

		(a_2) 

	= Junctions5_A__To__Junctions5_Junctions5Junction1286_2_Condition_Action(a_1);

		-- condition Action : a+=100

		(a_3) 

	= 

		 if (( x>=2 )) then 

		Junctions5_Junctions5Junction1286__To__Junctions5_Junctions5Junction1287_1_Condition_Action(a_2)

		 else (a_2);

		-- condition Action : a+=1000

		(a_4) 

	= 

		 if (( x>=2 ) and ( x>=4 )) then 

		Junctions5_Junctions5Junction1287__To__Junctions5_B_1_Condition_Action(a_3)

		 else (a_3);

		(a_5, idJunctions5_Junctions5_2) 

	= 

		 if (( x>=2 ) and ( x>=4 )) then 

		Junctions5_A_ex(a_4, idJunctions5_Junctions5_1, false)

		 else (a_4, idJunctions5_Junctions5_1);

		(idJunctions5_Junctions5_3) 

	= 

		 if (( x>=2 ) and ( x>=4 )) then 

		Junctions5_B_en(idJunctions5_Junctions5_2, false)

		 else (idJunctions5_Junctions5_2);

	(idJunctions5_Junctions5, a) 

	= 

		 if (( x>=2 ) and ( x>=4 )) then 

		(idJunctions5_Junctions5_3, a_5)

		 else

		 if (( x>=2 )) then 

		(idJunctions5_Junctions5_1, a_3)

		 else (idJunctions5_Junctions5_1, a_2);

	tel

	until true restart POINTJunctions5_Junctions5

	state JUNCTIONS5_A_IDL:

	 	let

	(idJunctions5_Junctions5, a) 

	= (idJunctions5_Junctions5_1, a_1);

	tel

	until true restart POINTJunctions5_Junctions5

	state JUNCTIONS5_B_IDL:

	 	let

	(idJunctions5_Junctions5, a) 

	= (idJunctions5_Junctions5_1, a_1);

	tel

	until true restart POINTJunctions5_Junctions5

tel

--***************************************************State :Junctions5_Junctions5 Automaton***************************************************

node Junctions5_Junctions5(x:int)

returns (a:real);

var a_1: real;

	idJunctions5_Junctions5, idJunctions5_Junctions5_1: int;

	let

	a_1 = 0.0 -> pre a;

	idJunctions5_Junctions5_1 = 0 -> pre idJunctions5_Junctions5;

	(idJunctions5_Junctions5, a)

	 = Junctions5_Junctions5_node(idJunctions5_Junctions5_1, x, a_1);

--unused outputs

tel

node Junctions5 (x_1_1 : int)

returns (a_1_1 : real); 

var

	Junctions5_1_1 : real;

	i_virtual_local : real;

let 

	Junctions5_1_1 =  Junctions5_Junctions5(x_1_1);

	a_1_1 = Junctions5_1_1;

	i_virtual_local= 0.0 -> 1.0;

tel