CristalCaveGem » LustreC » Lustrec-Tests

-- This file has been generated by cocoSim

-- System nodes

node N1_B__To__N1_A_1_Condition_Action(x_1:real)

returns (x:real);

var 	x_2:real;

let

	x_2 

	=  x_1 -1.;

	(x) 

	= (x_2);

tel

node N2_C__To__N2_D_1_Condition_Action(x_1:real)

returns (x:real);

var 	x_2:real;

let

	x_2 

	=  x_1 +100.;

	(x) 

	= (x_2);

tel

node N2_D__To__N2_C_1_Condition_Action(x_1:real)

returns (x:real);

var 	x_2:real;

let

	x_2 

	=  x_1 -100.;

	(x) 

	= (x_2);

tel

node N1_A__To__N1_B_1_Condition_Action(x_1:real)

returns (x:real);

var 	x_2:real;

let

	x_2 

	=  x_1 +1.;

	(x) 

	= (x_2);

tel

-- Entry action for state :N2_C

node N2_C_en(idTOP_N2_1:int;

	x_1:real;

	isInner:bool)

returns (idTOP_N2:int;

	x:real);

var 	idTOP_N2_2:int;

	x_2:real;

let

	-- set state as active 

	idTOP_N2_2 

	= 901;

	x_2 

	= if (not isInner) then  x_1 +1000.

	 else x_1;

	(idTOP_N2, x) 

	= (idTOP_N2_2, x_2);

tel

-- Exit action for state :N2_C

node N2_C_ex(idTOP_N2_1:int;

	isInner:bool)

returns (idTOP_N2:int);

var 	idTOP_N2_2:int;

let

	-- set state as inactive 

	idTOP_N2_2

	 = if (not isInner) then 0 else idTOP_N2_1;

	(idTOP_N2) 

	= (idTOP_N2_1);

tel

-- Entry action for state :N2_D

node N2_D_en(idTOP_N2_1:int;

	x_1:real;

	isInner:bool)

returns (idTOP_N2:int;

	x:real);

var 	idTOP_N2_2:int;

	x_2:real;

let

	-- set state as active 

	idTOP_N2_2 

	= 902;

	x_2 

	= if (not isInner) then  x_1 -1000.

	 else x_1;

	(idTOP_N2, x) 

	= (idTOP_N2_2, x_2);

tel

-- Exit action for state :N2_D

node N2_D_ex(idTOP_N2_1:int;

	isInner:bool)

returns (idTOP_N2:int);

var 	idTOP_N2_2:int;

let

	-- set state as inactive 

	idTOP_N2_2

	 = if (not isInner) then 0 else idTOP_N2_1;

	(idTOP_N2) 

	= (idTOP_N2_1);

tel

-- Entry action for state :TOP_N2

node TOP_N2_en(idTOP_N2_1:int;

	idHierarchy1_TOP_1:int;

	x_1:real;

	isInner:bool)

returns (idTOP_N2:int;

	idHierarchy1_TOP:int;

	x:real);

var 	idTOP_N2_2, idTOP_N2_3, idTOP_N2_4, idTOP_N2_5, idTOP_N2_6:int;

	idHierarchy1_TOP_2, idHierarchy1_TOP_3, idHierarchy1_TOP_4:int;

	x_2, x_3, x_4, x_5, x_6, x_7:real;

let

	-- set state as active 

	idHierarchy1_TOP_2 

	= 898;

	x_2 

	= if (not isInner) then  x_1 +100000.

	 else x_1;

-- transition trace :

	--POINT__To__N2_C_1

		(idTOP_N2_2, x_3) 

	= N2_C_en(idTOP_N2_1, x_2, false);

	(idTOP_N2_3, idHierarchy1_TOP_3, x_4) 

	= 

	if ( idTOP_N2_1 = 0) then

	 (idTOP_N2_2, idHierarchy1_TOP_2, x_3)

	 else(idTOP_N2_1, idHierarchy1_TOP_2, x_2);

	(idTOP_N2_4, x_5) 

	= 

	if ( idTOP_N2_1 = 901) then

	N2_C_en(idTOP_N2_1, x_2, false)

	 else (idTOP_N2_1, x_2);

	(idTOP_N2_5, x_6) 

	= 

	if ( idTOP_N2_1 = 902) then

	N2_D_en(idTOP_N2_1, x_2, false)

	 else (idTOP_N2_1, x_2);

	(idTOP_N2_6, idHierarchy1_TOP_4, x_7) 

	= 

		 if ( idTOP_N2_1 = 0) then 

		(idTOP_N2_3, idHierarchy1_TOP_3, x_4)

		 else

		 if ( idTOP_N2_1 = 901) then 

		(idTOP_N2_4, idHierarchy1_TOP_3, x_5)

		 else

		 if ( idTOP_N2_1 = 902) then 

		(idTOP_N2_5, idHierarchy1_TOP_3, x_6)

		 else (idTOP_N2_1, idHierarchy1_TOP_2, x_2);

	(idTOP_N2, idHierarchy1_TOP, x) 

	= (idTOP_N2_6, idHierarchy1_TOP_4, x_7);

tel

-- Exit action for state :TOP_N2

node TOP_N2_ex(idTOP_N2_1:int;

	x_1:real;

	idHierarchy1_TOP_1:int;

	isInner:bool)

returns (idTOP_N2:int;

	x:real;

	idHierarchy1_TOP:int);

var 	idTOP_N2_2, idTOP_N2_3, idTOP_N2_4, idTOP_N2_5:int;

	x_2:real;

	idHierarchy1_TOP_2:int;

let

	(idTOP_N2_2) 

	= 

	if ( idTOP_N2_1 = 901) then

	N2_C_ex(idTOP_N2_1, false)

	 else (idTOP_N2_1);

	(idTOP_N2_3) 

	= 

	if ( idTOP_N2_1 = 902) then

	N2_D_ex(idTOP_N2_1, false)

	 else (idTOP_N2_1);

	(idTOP_N2_4) 

	= 

		 if ( idTOP_N2_1 = 901) then 

		(idTOP_N2_2)

		 else

		 if ( idTOP_N2_1 = 902) then 

		(idTOP_N2_3)

		 else (idTOP_N2_1);

	x_2 

	= if (not isInner) then  x_1 -100000.

	 else x_1;

	-- set state as inactive 

	idHierarchy1_TOP_2

	 = if (not isInner) then 0 else idHierarchy1_TOP_1;

	idTOP_N2_5 

	= 0;

	(idTOP_N2, x, idHierarchy1_TOP) 

	= (idTOP_N2_5, x_2, idHierarchy1_TOP_1);

tel

-- Entry action for state :N1_A

node N1_A_en(idTOP_N1_1:int;

	x_1:real;

	isInner:bool)

returns (idTOP_N1:int;

	x:real);

var 	idTOP_N1_2:int;

	x_2:real;

let

	-- set state as active 

	idTOP_N1_2 

	= 899;

	x_2 

	= if (not isInner) then  x_1 +10.

	 else x_1;

	(idTOP_N1, x) 

	= (idTOP_N1_2, x_2);

tel

-- Exit action for state :N1_A

node N1_A_ex(idTOP_N1_1:int;

	isInner:bool)

returns (idTOP_N1:int);

var 	idTOP_N1_2:int;

let

	-- set state as inactive 

	idTOP_N1_2

	 = if (not isInner) then 0 else idTOP_N1_1;

	(idTOP_N1) 

	= (idTOP_N1_1);

tel

-- Entry action for state :N1_B

node N1_B_en(idTOP_N1_1:int;

	x_1:real;

	isInner:bool)

returns (idTOP_N1:int;

	x:real);

var 	idTOP_N1_2:int;

	x_2:real;

let

	-- set state as active 

	idTOP_N1_2 

	= 900;

	x_2 

	= if (not isInner) then  x_1 -10.

	 else x_1;

	(idTOP_N1, x) 

	= (idTOP_N1_2, x_2);

tel

-- Exit action for state :N1_B

node N1_B_ex(idTOP_N1_1:int;

	isInner:bool)

returns (idTOP_N1:int);

var 	idTOP_N1_2:int;

let

	-- set state as inactive 

	idTOP_N1_2

	 = if (not isInner) then 0 else idTOP_N1_1;

	(idTOP_N1) 

	= (idTOP_N1_1);

tel

-- Entry action for state :TOP_N1

node TOP_N1_en(idTOP_N1_1:int;

	idHierarchy1_TOP_1:int;

	x_1:real;

	isInner:bool)

returns (idTOP_N1:int;

	idHierarchy1_TOP:int;

	x:real);

var 	idTOP_N1_2, idTOP_N1_3, idTOP_N1_4, idTOP_N1_5, idTOP_N1_6:int;

	idHierarchy1_TOP_2, idHierarchy1_TOP_3, idHierarchy1_TOP_4:int;

	x_2, x_3, x_4, x_5, x_6, x_7:real;

let

	-- set state as active 

	idHierarchy1_TOP_2 

	= 897;

	x_2 

	= if (not isInner) then  x_1 +10000.

	 else x_1;

-- transition trace :

	--POINT__To__N1_A_1

		(idTOP_N1_2, x_3) 

	= N1_A_en(idTOP_N1_1, x_2, false);

	(idTOP_N1_3, idHierarchy1_TOP_3, x_4) 

	= 

	if ( idTOP_N1_1 = 0) then

	 (idTOP_N1_2, idHierarchy1_TOP_2, x_3)

	 else(idTOP_N1_1, idHierarchy1_TOP_2, x_2);

	(idTOP_N1_4, x_5) 

	= 

	if ( idTOP_N1_1 = 899) then

	N1_A_en(idTOP_N1_1, x_2, false)

	 else (idTOP_N1_1, x_2);

	(idTOP_N1_5, x_6) 

	= 

	if ( idTOP_N1_1 = 900) then

	N1_B_en(idTOP_N1_1, x_2, false)

	 else (idTOP_N1_1, x_2);

	(idTOP_N1_6, idHierarchy1_TOP_4, x_7) 

	= 

		 if ( idTOP_N1_1 = 0) then 

		(idTOP_N1_3, idHierarchy1_TOP_3, x_4)

		 else

		 if ( idTOP_N1_1 = 899) then 

		(idTOP_N1_4, idHierarchy1_TOP_3, x_5)

		 else

		 if ( idTOP_N1_1 = 900) then 

		(idTOP_N1_5, idHierarchy1_TOP_3, x_6)

		 else (idTOP_N1_1, idHierarchy1_TOP_2, x_2);

	(idTOP_N1, idHierarchy1_TOP, x) 

	= (idTOP_N1_6, idHierarchy1_TOP_4, x_7);

tel

-- Exit action for state :TOP_N1

node TOP_N1_ex(idTOP_N1_1:int;

	x_1:real;

	idHierarchy1_TOP_1:int;

	isInner:bool)

returns (idTOP_N1:int;

	x:real;

	idHierarchy1_TOP:int);

var 	idTOP_N1_2, idTOP_N1_3, idTOP_N1_4, idTOP_N1_5:int;

	x_2:real;

	idHierarchy1_TOP_2:int;

let

	(idTOP_N1_2) 

	= 

	if ( idTOP_N1_1 = 899) then

	N1_A_ex(idTOP_N1_1, false)

	 else (idTOP_N1_1);

	(idTOP_N1_3) 

	= 

	if ( idTOP_N1_1 = 900) then

	N1_B_ex(idTOP_N1_1, false)

	 else (idTOP_N1_1);

	(idTOP_N1_4) 

	= 

		 if ( idTOP_N1_1 = 899) then 

		(idTOP_N1_2)

		 else

		 if ( idTOP_N1_1 = 900) then 

		(idTOP_N1_3)

		 else (idTOP_N1_1);

	x_2 

	= if (not isInner) then  x_1 -10000.

	 else x_1;

	-- set state as inactive 

	idHierarchy1_TOP_2

	 = if (not isInner) then 0 else idHierarchy1_TOP_1;

	idTOP_N1_5 

	= 0;

	(idTOP_N1, x, idHierarchy1_TOP) 

	= (idTOP_N1_5, x_2, idHierarchy1_TOP_1);

tel

-- Entry action for state :Hierarchy1_TOP

node Hierarchy1_TOP_en(idHierarchy1_TOP_1:int;

	idHierarchy1_Hierarchy1_1:int;

	x_1:real;

	idTOP_N1_1:int;

	idTOP_N2_1:int;

	isInner:bool)

returns (idHierarchy1_TOP:int;

	idHierarchy1_Hierarchy1:int;

	x:real;

	idTOP_N1:int;

	idTOP_N2:int);

var 	idHierarchy1_TOP_2, idHierarchy1_TOP_3, idHierarchy1_TOP_4, idHierarchy1_TOP_5, idHierarchy1_TOP_6:int;

	idHierarchy1_Hierarchy1_2, idHierarchy1_Hierarchy1_3, idHierarchy1_Hierarchy1_4:int;

	x_2, x_3, x_4, x_5, x_6, x_7:real;

	idTOP_N1_2, idTOP_N1_3, idTOP_N1_4, idTOP_N1_5:int;

	idTOP_N2_2, idTOP_N2_3:int;

let

	-- set state as active 

	idHierarchy1_Hierarchy1_2 

	= 903;

	x_2 

	= if (not isInner) then  x_1 +1000000.

	 else x_1;

-- transition trace :

	--POINT__To__TOP_N1_1

		(idTOP_N1_2, idHierarchy1_TOP_2, x_3) 

	= TOP_N1_en(idTOP_N1_1, idHierarchy1_TOP_1, x_2, false);

	(idHierarchy1_TOP_3, idHierarchy1_Hierarchy1_3, x_4, idTOP_N1_3) 

	= 

	if ( idHierarchy1_TOP_1 = 0) then

	 (idHierarchy1_TOP_2, idHierarchy1_Hierarchy1_2, x_3, idTOP_N1_2)

	 else(idHierarchy1_TOP_1, idHierarchy1_Hierarchy1_2, x_2, idTOP_N1_1);

	(idTOP_N1_4, idHierarchy1_TOP_4, x_5) 

	= 

	if ( idHierarchy1_TOP_1 = 897) then

	TOP_N1_en(idTOP_N1_1, idHierarchy1_TOP_1, x_2, false)

	 else (idTOP_N1_1, idHierarchy1_TOP_1, x_2);

	(idTOP_N2_2, idHierarchy1_TOP_5, x_6) 

	= 

	if ( idHierarchy1_TOP_1 = 898) then

	TOP_N2_en(idTOP_N2_1, idHierarchy1_TOP_1, x_2, false)

	 else (idTOP_N2_1, idHierarchy1_TOP_1, x_2);

	(idHierarchy1_TOP_6, idHierarchy1_Hierarchy1_4, x_7, idTOP_N1_5, idTOP_N2_3) 

	= 

		 if ( idHierarchy1_TOP_1 = 0) then 

		(idHierarchy1_TOP_3, idHierarchy1_Hierarchy1_3, x_4, idTOP_N1_3, idTOP_N2_1)

		 else

		 if ( idHierarchy1_TOP_1 = 897) then 

		(idHierarchy1_TOP_4, idHierarchy1_Hierarchy1_3, x_5, idTOP_N1_4, idTOP_N2_1)

		 else

		 if ( idHierarchy1_TOP_1 = 898) then 

		(idHierarchy1_TOP_5, idHierarchy1_Hierarchy1_3, x_6, idTOP_N1_1, idTOP_N2_2)

		 else (idHierarchy1_TOP_1, idHierarchy1_Hierarchy1_2, x_2, idTOP_N1_1, idTOP_N2_1);

	(idHierarchy1_TOP, idHierarchy1_Hierarchy1, x, idTOP_N1, idTOP_N2) 

	= (idHierarchy1_TOP_6, idHierarchy1_Hierarchy1_4, x_7, idTOP_N1_5, idTOP_N2_3);

tel

-- Exit action for state :Hierarchy1_TOP

node Hierarchy1_TOP_ex(idTOP_N1_1:int;

	x_1:real;

	idHierarchy1_TOP_1:int;

	idTOP_N2_1:int;

	idHierarchy1_Hierarchy1_1:int;

	isInner:bool)

returns (idTOP_N1:int;

	x:real;

	idHierarchy1_TOP:int;

	idTOP_N2:int;

	idHierarchy1_Hierarchy1:int);

var 	idTOP_N1_2, idTOP_N1_3:int;

	x_2, x_3, x_4, x_5:real;

	idHierarchy1_TOP_2, idHierarchy1_TOP_3, idHierarchy1_TOP_4, idHierarchy1_TOP_5:int;

	idTOP_N2_2, idTOP_N2_3:int;

	idHierarchy1_Hierarchy1_2:int;

let

	(idTOP_N1_2, x_2, idHierarchy1_TOP_2) 

	= 

	if ( idHierarchy1_TOP_1 = 897) then

	TOP_N1_ex(idTOP_N1_1, x_1, idHierarchy1_TOP_1, false)

	 else (idTOP_N1_1, x_1, idHierarchy1_TOP_1);

	(idTOP_N2_2, x_3, idHierarchy1_TOP_3) 

	= 

	if ( idHierarchy1_TOP_1 = 898) then

	TOP_N2_ex(idTOP_N2_1, x_1, idHierarchy1_TOP_1, false)

	 else (idTOP_N2_1, x_1, idHierarchy1_TOP_1);

	(idTOP_N1_3, x_4, idHierarchy1_TOP_4, idTOP_N2_3) 

	= 

		 if ( idHierarchy1_TOP_1 = 897) then 

		(idTOP_N1_2, x_2, idHierarchy1_TOP_2, idTOP_N2_1)

		 else

		 if ( idHierarchy1_TOP_1 = 898) then 

		(idTOP_N1_1, x_3, idHierarchy1_TOP_3, idTOP_N2_2)

		 else (idTOP_N1_1, x_1, idHierarchy1_TOP_1, idTOP_N2_1);

	x_5 

	= if (not isInner) then 0.

	 else x_4;

	-- set state as inactive 

	idHierarchy1_Hierarchy1_2

	 = if (not isInner) then 0 else idHierarchy1_Hierarchy1_1;

	idHierarchy1_TOP_5 

	= 0;

	(idTOP_N1, x, idHierarchy1_TOP, idTOP_N2, idHierarchy1_Hierarchy1) 

	= (idTOP_N1_3, x_5, idHierarchy1_TOP_5, idTOP_N2_3, idHierarchy1_Hierarchy1_1);

tel

--***************************************************State :TOP_N2 Automaton***************************************************

node TOP_N2_node(idTOP_N2_1:int;

	x_1:real;

	S:bool;

	R:bool)

returns (idTOP_N2:int;

	x:real);

let

	 automaton top_n2

	state POINTTOP_N2:

	unless (idTOP_N2_1=0) restart POINT__TO__N2_C_1

	unless (idTOP_N2_1=901) and S restart N2_C__TO__N2_D_1

	unless (idTOP_N2_1=902) and R restart N2_D__TO__N2_C_1

	unless (idTOP_N2_1=901) restart N2_C_IDL

	unless (idTOP_N2_1=902) restart N2_D_IDL

	let

		(idTOP_N2, x) 

	= (idTOP_N2_1, x_1);

	tel

	state POINT__TO__N2_C_1:

	 var 	idTOP_N2_2:int;

	x_2:real;

	let

		-- transition trace :

	--POINT__To__N2_C_1

		(idTOP_N2_2, x_2) 

	= N2_C_en(idTOP_N2_1, x_1, false);

	(idTOP_N2, x) 

	=  (idTOP_N2_2, x_2);

	tel

	until true restart POINTTOP_N2

	state N2_C__TO__N2_D_1:

	 var 	idTOP_N2_2, idTOP_N2_3:int;

	x_2, x_3:real;

	let

		-- transition trace :

	--N2_C__To__N2_D_1

		-- condition Action : x+=100;

		(x_2) 

	= N2_C__To__N2_D_1_Condition_Action(x_1);

		(idTOP_N2_2) 

	= N2_C_ex(idTOP_N2_1, false);

		(idTOP_N2_3, x_3) 

	= N2_D_en(idTOP_N2_2, x_2, false);

	(idTOP_N2, x) 

	=  (idTOP_N2_3, x_3);

	tel

	until true restart POINTTOP_N2

	state N2_D__TO__N2_C_1:

	 var 	idTOP_N2_2, idTOP_N2_3:int;

	x_2, x_3:real;

	let

		-- transition trace :

	--N2_D__To__N2_C_1

		-- condition Action : x-=100;

		(x_2) 

	= N2_D__To__N2_C_1_Condition_Action(x_1);

		(idTOP_N2_2) 

	= N2_D_ex(idTOP_N2_1, false);

		(idTOP_N2_3, x_3) 

	= N2_C_en(idTOP_N2_2, x_2, false);

	(idTOP_N2, x) 

	=  (idTOP_N2_3, x_3);

	tel

	until true restart POINTTOP_N2

	state N2_C_IDL:

	 	let

	(idTOP_N2, x) 

	= (idTOP_N2_1, x_1);

	tel

	until true restart POINTTOP_N2

	state N2_D_IDL:

	 	let

	(idTOP_N2, x) 

	= (idTOP_N2_1, x_1);

	tel

	until true restart POINTTOP_N2

tel

--***************************************************State :TOP_N1 Automaton***************************************************

node TOP_N1_node(idTOP_N1_1:int;

	x_1:real;

	S:bool;

	R:bool)

returns (idTOP_N1:int;

	x:real);

let

	 automaton top_n1

	state POINTTOP_N1:

	unless (idTOP_N1_1=0) restart POINT__TO__N1_A_1

	unless (idTOP_N1_1=899) and S restart N1_A__TO__N1_B_1

	unless (idTOP_N1_1=900) and R restart N1_B__TO__N1_A_1

	unless (idTOP_N1_1=899) restart N1_A_IDL

	unless (idTOP_N1_1=900) restart N1_B_IDL

	let

		(idTOP_N1, x) 

	= (idTOP_N1_1, x_1);

	tel

	state POINT__TO__N1_A_1:

	 var 	idTOP_N1_2:int;