CristalCaveGem » LustreC » Lustrec-Tests

-- This file has been generated by cocoSim

-- System nodes

-- Entry action for state :Arrays2_B

node Arrays2_B_en(idArrays2_Arrays2_1:int;

	x_1_2_1:real;

	x_2_2_1:real;

	isInner:bool)

returns (idArrays2_Arrays2:int;

	x_1_2:real;

	x_2_2:real);

var 	idArrays2_Arrays2_2:int;

	x_1_2_2:real;

	x_2_2_2:real;

let

	-- set state as active 

	idArrays2_Arrays2_2 

	= 525;

	x_1_2_2 

	= if (not isInner) then  x_1_2_1  + 1.

	 else x_1_2_1;

	x_2_2_2 

	= if (not isInner) then  x_2_2_1  - 1.

	 else x_2_2_1;

	(idArrays2_Arrays2, x_1_2, x_2_2) 

	= (idArrays2_Arrays2_2, x_1_2_2, x_2_2_2);

tel

-- Exit action for state :Arrays2_B

node Arrays2_B_ex(idArrays2_Arrays2_1:int;

	isInner:bool)

returns (idArrays2_Arrays2:int);

var 	idArrays2_Arrays2_2:int;

let

	-- set state as inactive 

	idArrays2_Arrays2_2

	 = if (not isInner) then 0 else idArrays2_Arrays2_1;

	(idArrays2_Arrays2) 

	= (idArrays2_Arrays2_1);

tel

-- Entry action for state :Arrays2_A

node Arrays2_A_en(idArrays2_Arrays2_1:int;

	x_1_1_1:real;

	x_2_1_1:real;

	isInner:bool)

returns (idArrays2_Arrays2:int;

	x_1_1:real;

	x_2_1:real);

var 	idArrays2_Arrays2_2:int;

	x_1_1_2:real;

	x_2_1_2:real;

let

	-- set state as active 

	idArrays2_Arrays2_2 

	= 524;

	x_1_1_2 

	= if (not isInner) then  x_1_1_1  + 1.

	 else x_1_1_1;

	x_2_1_2 

	= if (not isInner) then  x_2_1_1  - 1.

	 else x_2_1_1;

	(idArrays2_Arrays2, x_1_1, x_2_1) 

	= (idArrays2_Arrays2_2, x_1_1_2, x_2_1_2);

tel

-- Exit action for state :Arrays2_A

node Arrays2_A_ex(idArrays2_Arrays2_1:int;

	isInner:bool)

returns (idArrays2_Arrays2:int);

var 	idArrays2_Arrays2_2:int;

let

	-- set state as inactive 

	idArrays2_Arrays2_2

	 = if (not isInner) then 0 else idArrays2_Arrays2_1;

	(idArrays2_Arrays2) 

	= (idArrays2_Arrays2_1);

tel

-- Entry action for state :Arrays2_C

node Arrays2_C_en(idArrays2_Arrays2_1:int;

	x_1_3_1:real;

	x_2_3_1:real;

	isInner:bool)

returns (idArrays2_Arrays2:int;

	x_1_3:real;

	x_2_3:real);

var 	idArrays2_Arrays2_2:int;

	x_1_3_2:real;

	x_2_3_2:real;

let

	-- set state as active 

	idArrays2_Arrays2_2 

	= 526;

	x_1_3_2 

	= if (not isInner) then  x_1_3_1  + 1.

	 else x_1_3_1;

	x_2_3_2 

	= if (not isInner) then  x_2_3_1  - 1.

	 else x_2_3_1;

	(idArrays2_Arrays2, x_1_3, x_2_3) 

	= (idArrays2_Arrays2_2, x_1_3_2, x_2_3_2);

tel

-- Exit action for state :Arrays2_C

node Arrays2_C_ex(idArrays2_Arrays2_1:int;

	isInner:bool)

returns (idArrays2_Arrays2:int);

var 	idArrays2_Arrays2_2:int;

let

	-- set state as inactive 

	idArrays2_Arrays2_2

	 = if (not isInner) then 0 else idArrays2_Arrays2_1;

	(idArrays2_Arrays2) 

	= (idArrays2_Arrays2_1);

tel

--***************************************************State :Arrays2_Arrays2 Automaton***************************************************

node Arrays2_Arrays2_node(idArrays2_Arrays2_1:int;

	x_1_1_1:real;

	x_2_1_1:real;

	E:bool;

	x_1_2_1:real;

	x_2_2_1:real;

	x_1_3_1:real;

	x_2_3_1:real)

returns (idArrays2_Arrays2:int;

	x_1_1:real;

	x_2_1:real;

	x_1_2:real;

	x_2_2:real;

	x_1_3:real;

	x_2_3:real);

let

	 automaton arrays2_arrays2

	state POINTArrays2_Arrays2:

	unless (idArrays2_Arrays2_1=0) restart POINT__TO__ARRAYS2_A_1

	unless (idArrays2_Arrays2_1=524) and E restart ARRAYS2_A__TO__ARRAYS2_B_1

	unless (idArrays2_Arrays2_1=525) and E restart ARRAYS2_B__TO__ARRAYS2_C_1

	unless (idArrays2_Arrays2_1=526) and E restart ARRAYS2_C__TO__ARRAYS2_A_1

	unless (idArrays2_Arrays2_1=524) restart ARRAYS2_A_IDL

	unless (idArrays2_Arrays2_1=525) restart ARRAYS2_B_IDL

	unless (idArrays2_Arrays2_1=526) restart ARRAYS2_C_IDL

	let

		(idArrays2_Arrays2, x_1_1, x_2_1, x_1_2, x_2_2, x_1_3, x_2_3) 

	= (idArrays2_Arrays2_1, x_1_1_1, x_2_1_1, x_1_2_1, x_2_2_1, x_1_3_1, x_2_3_1);

	tel

	state POINT__TO__ARRAYS2_A_1:

	 var 	idArrays2_Arrays2_2:int;

	x_1_1_2:real;

	x_2_1_2:real;

	let

		-- transition trace :

	--POINT__To__Arrays2_A_1

		(idArrays2_Arrays2_2, x_1_1_2, x_2_1_2) 

	= Arrays2_A_en(idArrays2_Arrays2_1, x_1_1_1, x_2_1_1, false);

	(idArrays2_Arrays2, x_1_1, x_2_1) 

	=  (idArrays2_Arrays2_2, x_1_1_2, x_2_1_2);

	--add unused variables

	(x_1_2, x_1_3, x_2_2, x_2_3) 

	= (x_1_2_1, x_1_3_1, x_2_2_1, x_2_3_1);

	tel

	until true restart POINTArrays2_Arrays2

	state ARRAYS2_A__TO__ARRAYS2_B_1:

	 var 	idArrays2_Arrays2_2, idArrays2_Arrays2_3:int;

	x_1_2_2:real;

	x_2_2_2:real;

	let

		-- transition trace :

	--Arrays2_A__To__Arrays2_B_1

		(idArrays2_Arrays2_2) 

	= Arrays2_A_ex(idArrays2_Arrays2_1, false);

		(idArrays2_Arrays2_3, x_1_2_2, x_2_2_2) 

	= Arrays2_B_en(idArrays2_Arrays2_2, x_1_2_1, x_2_2_1, false);

	(idArrays2_Arrays2, x_1_1, x_2_1, x_1_2, x_2_2) 

	=  (idArrays2_Arrays2_3, x_1_1_1, x_2_1_1, x_1_2_2, x_2_2_2);

	--add unused variables

	(x_1_3, x_2_3) 

	= (x_1_3_1, x_2_3_1);

	tel

	until true restart POINTArrays2_Arrays2

	state ARRAYS2_B__TO__ARRAYS2_C_1:

	 var 	idArrays2_Arrays2_2, idArrays2_Arrays2_3:int;

	x_1_3_2:real;

	x_2_3_2:real;

	let

		-- transition trace :

	--Arrays2_B__To__Arrays2_C_1

		(idArrays2_Arrays2_2) 

	= Arrays2_B_ex(idArrays2_Arrays2_1, false);

		(idArrays2_Arrays2_3, x_1_3_2, x_2_3_2) 

	= Arrays2_C_en(idArrays2_Arrays2_2, x_1_3_1, x_2_3_1, false);

	(idArrays2_Arrays2, x_1_1, x_2_1, x_1_2, x_2_2, x_1_3, x_2_3) 

	=  (idArrays2_Arrays2_3, x_1_1_1, x_2_1_1, x_1_2_1, x_2_2_1, x_1_3_2, x_2_3_2);

	tel

	until true restart POINTArrays2_Arrays2

	state ARRAYS2_C__TO__ARRAYS2_A_1:

	 var 	idArrays2_Arrays2_2, idArrays2_Arrays2_3:int;

	x_1_1_2:real;

	x_2_1_2:real;

	let

		-- transition trace :

	--Arrays2_C__To__Arrays2_A_1

		(idArrays2_Arrays2_2) 

	= Arrays2_C_ex(idArrays2_Arrays2_1, false);

		(idArrays2_Arrays2_3, x_1_1_2, x_2_1_2) 

	= Arrays2_A_en(idArrays2_Arrays2_2, x_1_1_1, x_2_1_1, false);

	(idArrays2_Arrays2, x_1_1, x_2_1, x_1_2, x_2_2, x_1_3, x_2_3) 

	=  (idArrays2_Arrays2_3, x_1_1_2, x_2_1_2, x_1_2_1, x_2_2_1, x_1_3_1, x_2_3_1);

	tel

	until true restart POINTArrays2_Arrays2

	state ARRAYS2_A_IDL:

	 	let

	(idArrays2_Arrays2, x_1_1, x_2_1, x_1_2, x_2_2, x_1_3, x_2_3) 

	= (idArrays2_Arrays2_1, x_1_1_1, x_2_1_1, x_1_2_1, x_2_2_1, x_1_3_1, x_2_3_1);

	tel

	until true restart POINTArrays2_Arrays2

	state ARRAYS2_B_IDL:

	 	let

	(idArrays2_Arrays2, x_1_1, x_2_1, x_1_2, x_2_2, x_1_3, x_2_3) 

	= (idArrays2_Arrays2_1, x_1_1_1, x_2_1_1, x_1_2_1, x_2_2_1, x_1_3_1, x_2_3_1);

	tel

	until true restart POINTArrays2_Arrays2

	state ARRAYS2_C_IDL:

	 	let

	(idArrays2_Arrays2, x_1_1, x_2_1, x_1_2, x_2_2, x_1_3, x_2_3) 

	= (idArrays2_Arrays2_1, x_1_1_1, x_2_1_1, x_1_2_1, x_2_2_1, x_1_3_1, x_2_3_1);

	tel

	until true restart POINTArrays2_Arrays2

tel

--***************************************************State :Arrays2_Arrays2 Automaton***************************************************

node Arrays2_Arrays2(E:bool)

returns (x_1_1:real;

	x_1_2:real;

	x_1_3:real;

	x_2_1:real;

	x_2_2:real;

	x_2_3:real);

var x_1_1_1: real;

	x_1_2_1: real;

	x_1_3_1: real;

	x_2_1_1: real;

	x_2_2_1: real;

	x_2_3_1: real;

	idArrays2_Arrays2, idArrays2_Arrays2_1: int;

	let

	x_1_1_1 = 1.0 -> pre x_1_1;

	x_1_2_1 = 1.0 -> pre x_1_2;

	x_1_3_1 = 1.0 -> pre x_1_3;

	x_2_1_1 = 1.0 -> pre x_2_1;

	x_2_2_1 = 1.0 -> pre x_2_2;

	x_2_3_1 = 1.0 -> pre x_2_3;

	idArrays2_Arrays2_1 = 0 -> pre idArrays2_Arrays2;

	(idArrays2_Arrays2, x_1_1, x_2_1, x_1_2, x_2_2, x_1_3, x_2_3)

	 = 

	 if E then Arrays2_Arrays2_node(idArrays2_Arrays2_1, x_1_1_1, x_2_1_1, E, x_1_2_1, x_2_2_1, x_1_3_1, x_2_3_1)

	 else (idArrays2_Arrays2_1, x_1_1_1, x_2_1_1, x_1_2_1, x_2_2_1, x_1_3_1, x_2_3_1);

--unused outputs

tel

node Arrays2 (In1_1_1 : real)

returns (Out1_1_1 : real; Out1_1_2 : real; Out1_1_3 : real; Out1_1_4 : real; Out1_1_5 : real; Out1_1_6 : real); 

var

	Arrays2_1_1 : real; Arrays2_1_2 : real; Arrays2_1_3 : real; Arrays2_1_4 : real; Arrays2_1_5 : real; Arrays2_1_6 : real;

	i_virtual_local : real;

	Arrays2In1_1_1_event: bool;

let 

	Arrays2In1_1_1_event = false -> (pre(In1_1_1) <= 0.0 and In1_1_1 > 0.0);

	(Arrays2_1_1, Arrays2_1_2, Arrays2_1_3, Arrays2_1_4, Arrays2_1_5, Arrays2_1_6) =  Arrays2_Arrays2(Arrays2In1_1_1_event);

	Out1_1_1 = Arrays2_1_1;

	Out1_1_2 = Arrays2_1_2;

	Out1_1_3 = Arrays2_1_3;

	Out1_1_4 = Arrays2_1_4;

	Out1_1_5 = Arrays2_1_5;

	Out1_1_6 = Arrays2_1_6;

	i_virtual_local= 0.0 -> 1.0;

tel