CristalCaveGem » LustreC » Lustrec-Tests

-- This file has been generated by cocoSim

-- System nodes

-- Entry action for state :Arrays1_B

node Arrays1_B_en(idArrays1_Arrays1_1:int;

	x_2_1:int;

	isInner:bool)

returns (idArrays1_Arrays1:int;

	x_2:int);

var 	idArrays1_Arrays1_2:int;

	x_2_2:int;

let

	-- set state as active 

	idArrays1_Arrays1_2 

	= 512;

	x_2_2 

	= if (not isInner) then  x_2_1  + 1

	 else x_2_1;

	(idArrays1_Arrays1, x_2) 

	= (idArrays1_Arrays1_2, x_2_2);

tel

-- Exit action for state :Arrays1_B

node Arrays1_B_ex(idArrays1_Arrays1_1:int;

	isInner:bool)

returns (idArrays1_Arrays1:int);

var 	idArrays1_Arrays1_2:int;

let

	-- set state as inactive 

	idArrays1_Arrays1_2

	 = if (not isInner) then 0 else idArrays1_Arrays1_1;

	(idArrays1_Arrays1) 

	= (idArrays1_Arrays1_1);

tel

-- Entry action for state :Arrays1_A

node Arrays1_A_en(idArrays1_Arrays1_1:int;

	x_1_1:int;

	isInner:bool)

returns (idArrays1_Arrays1:int;

	x_1:int);

var 	idArrays1_Arrays1_2:int;

	x_1_2:int;

let

	-- set state as active 

	idArrays1_Arrays1_2 

	= 511;

	x_1_2 

	= if (not isInner) then  x_1_1  + 1

	 else x_1_1;

	(idArrays1_Arrays1, x_1) 

	= (idArrays1_Arrays1_2, x_1_2);

tel

-- Exit action for state :Arrays1_A

node Arrays1_A_ex(idArrays1_Arrays1_1:int;

	isInner:bool)

returns (idArrays1_Arrays1:int);

var 	idArrays1_Arrays1_2:int;

let

	-- set state as inactive 

	idArrays1_Arrays1_2

	 = if (not isInner) then 0 else idArrays1_Arrays1_1;

	(idArrays1_Arrays1) 

	= (idArrays1_Arrays1_1);

tel

-- Entry action for state :Arrays1_C

node Arrays1_C_en(idArrays1_Arrays1_1:int;

	x_3_1:int;

	isInner:bool)

returns (idArrays1_Arrays1:int;

	x_3:int);

var 	idArrays1_Arrays1_2:int;

	x_3_2:int;

let

	-- set state as active 

	idArrays1_Arrays1_2 

	= 513;

	x_3_2 

	= if (not isInner) then  x_3_1  + 1

	 else x_3_1;

	(idArrays1_Arrays1, x_3) 

	= (idArrays1_Arrays1_2, x_3_2);

tel

-- Exit action for state :Arrays1_C

node Arrays1_C_ex(idArrays1_Arrays1_1:int;

	isInner:bool)

returns (idArrays1_Arrays1:int);

var 	idArrays1_Arrays1_2:int;

let

	-- set state as inactive 

	idArrays1_Arrays1_2

	 = if (not isInner) then 0 else idArrays1_Arrays1_1;

	(idArrays1_Arrays1) 

	= (idArrays1_Arrays1_1);

tel

--***************************************************State :Arrays1_Arrays1 Automaton***************************************************

node Arrays1_Arrays1_node(idArrays1_Arrays1_1:int;

	x_1_1:int;

	E:bool;

	x_2_1:int;

	x_3_1:int)

returns (idArrays1_Arrays1:int;

	x_1:int;

	x_2:int;

	x_3:int);

let

	 automaton arrays1_arrays1

	state POINTArrays1_Arrays1:

	unless (idArrays1_Arrays1_1=0) restart POINT__TO__ARRAYS1_A_1

	unless (idArrays1_Arrays1_1=511) and E restart ARRAYS1_A__TO__ARRAYS1_B_1

	unless (idArrays1_Arrays1_1=512) and E restart ARRAYS1_B__TO__ARRAYS1_C_1

	unless (idArrays1_Arrays1_1=513) and E restart ARRAYS1_C__TO__ARRAYS1_A_1

	unless (idArrays1_Arrays1_1=511) restart ARRAYS1_A_IDL

	unless (idArrays1_Arrays1_1=512) restart ARRAYS1_B_IDL

	unless (idArrays1_Arrays1_1=513) restart ARRAYS1_C_IDL

	let

		(idArrays1_Arrays1, x_1, x_2, x_3) 

	= (idArrays1_Arrays1_1, x_1_1, x_2_1, x_3_1);

	tel

	state POINT__TO__ARRAYS1_A_1:

	 var 	idArrays1_Arrays1_2:int;

	x_1_2:int;

	let

		-- transition trace :

	--POINT__To__Arrays1_A_1

		(idArrays1_Arrays1_2, x_1_2) 

	= Arrays1_A_en(idArrays1_Arrays1_1, x_1_1, false);

	(idArrays1_Arrays1, x_1) 

	=  (idArrays1_Arrays1_2, x_1_2);

	--add unused variables

	(x_2, x_3) 

	= (x_2_1, x_3_1);

	tel

	until true restart POINTArrays1_Arrays1

	state ARRAYS1_A__TO__ARRAYS1_B_1:

	 var 	idArrays1_Arrays1_2, idArrays1_Arrays1_3:int;

	x_2_2:int;

	let

		-- transition trace :

	--Arrays1_A__To__Arrays1_B_1

		(idArrays1_Arrays1_2) 

	= Arrays1_A_ex(idArrays1_Arrays1_1, false);

		(idArrays1_Arrays1_3, x_2_2) 

	= Arrays1_B_en(idArrays1_Arrays1_2, x_2_1, false);

	(idArrays1_Arrays1, x_1, x_2) 

	=  (idArrays1_Arrays1_3, x_1_1, x_2_2);

	--add unused variables

	(x_3) 

	= (x_3_1);

	tel

	until true restart POINTArrays1_Arrays1

	state ARRAYS1_B__TO__ARRAYS1_C_1:

	 var 	idArrays1_Arrays1_2, idArrays1_Arrays1_3:int;

	x_3_2:int;

	let

		-- transition trace :

	--Arrays1_B__To__Arrays1_C_1

		(idArrays1_Arrays1_2) 

	= Arrays1_B_ex(idArrays1_Arrays1_1, false);

		(idArrays1_Arrays1_3, x_3_2) 

	= Arrays1_C_en(idArrays1_Arrays1_2, x_3_1, false);

	(idArrays1_Arrays1, x_1, x_2, x_3) 

	=  (idArrays1_Arrays1_3, x_1_1, x_2_1, x_3_2);

	tel

	until true restart POINTArrays1_Arrays1

	state ARRAYS1_C__TO__ARRAYS1_A_1:

	 var 	idArrays1_Arrays1_2, idArrays1_Arrays1_3:int;

	x_1_2:int;

	let

		-- transition trace :

	--Arrays1_C__To__Arrays1_A_1

		(idArrays1_Arrays1_2) 

	= Arrays1_C_ex(idArrays1_Arrays1_1, false);

		(idArrays1_Arrays1_3, x_1_2) 

	= Arrays1_A_en(idArrays1_Arrays1_2, x_1_1, false);

	(idArrays1_Arrays1, x_1, x_2, x_3) 

	=  (idArrays1_Arrays1_3, x_1_2, x_2_1, x_3_1);

	tel

	until true restart POINTArrays1_Arrays1

	state ARRAYS1_A_IDL:

	 	let

	(idArrays1_Arrays1, x_1, x_2, x_3) 

	= (idArrays1_Arrays1_1, x_1_1, x_2_1, x_3_1);

	tel

	until true restart POINTArrays1_Arrays1

	state ARRAYS1_B_IDL:

	 	let

	(idArrays1_Arrays1, x_1, x_2, x_3) 

	= (idArrays1_Arrays1_1, x_1_1, x_2_1, x_3_1);

	tel

	until true restart POINTArrays1_Arrays1

	state ARRAYS1_C_IDL:

	 	let

	(idArrays1_Arrays1, x_1, x_2, x_3) 

	= (idArrays1_Arrays1_1, x_1_1, x_2_1, x_3_1);

	tel

	until true restart POINTArrays1_Arrays1

tel

--***************************************************State :Arrays1_Arrays1 Automaton***************************************************

node Arrays1_Arrays1(E:bool)

returns (x_1:int;

	x_2:int;

	x_3:int);

var x_1_1: int;

	x_2_1: int;

	x_3_1: int;

	idArrays1_Arrays1, idArrays1_Arrays1_1: int;

	let

	x_1_1 = 1 -> pre x_1;

	x_2_1 = 1 -> pre x_2;

	x_3_1 = 1 -> pre x_3;

	idArrays1_Arrays1_1 = 0 -> pre idArrays1_Arrays1;

	(idArrays1_Arrays1, x_1, x_2, x_3)

	 = 

	 if E then Arrays1_Arrays1_node(idArrays1_Arrays1_1, x_1_1, E, x_2_1, x_3_1)

	 else (idArrays1_Arrays1_1, x_1_1, x_2_1, x_3_1);

--unused outputs

tel

node Arrays1 (E_1_1 : real)

returns (x1_1_1 : int;

	x2_2_1 : int;

	x3_3_1 : int); 

var

	Arrays1_1_1 : int; Arrays1_1_2 : int; Arrays1_1_3 : int;

	Demux_1_1 : int; Demux_2_1 : int; Demux_3_1 : int;

	i_virtual_local : real;

	Arrays1E_1_1_event: bool;

let 

	Arrays1E_1_1_event = false -> (pre(E_1_1) <= 0.0 and E_1_1 > 0.0);

	(Arrays1_1_1, Arrays1_1_2, Arrays1_1_3) =  Arrays1_Arrays1(Arrays1E_1_1_event);

	Demux_1_1 = Arrays1_1_1 ;

	Demux_2_1 = Arrays1_1_2 ;

	Demux_3_1 = Arrays1_1_3 ;

	x1_1_1 = Demux_1_1;

	x2_2_1 = Demux_2_1;

	x3_3_1 = Demux_3_1;

	i_virtual_local= 0.0 -> 1.0;

tel