CristalCaveGem » LustreC » Lustrec-Tests

-- This file has been generated by cocoSim

-- System nodes

node Outer1_A__To__Outer1_A_1_Condition_Action(x_1:int)

returns (x:int);

var 	x_2:int;

let

	x_2 

	=  x_1  + 1;

	(x) 

	= (x_2);

tel

node Outer1_A__To__Outer1_A_1_Transition_Action(y_1:int)

returns (y:int);

var 	y_2:int;

let

	y_2 

	=  y_1  + 1;

	(y) 

	= (y_2);

tel

-- Entry action for state :Outer1_A

node Outer1_A_en(idOuter1_Outer1_1:int;

	z_1:int;

	isInner:bool)

returns (idOuter1_Outer1:int;

	z:int);

var 	idOuter1_Outer1_2:int;

	z_2:int;

let

	-- set state as active 

	idOuter1_Outer1_2 

	= 1360;

	z_2 

	= if (not isInner) then  z_1  + 1

	 else z_1;

	(idOuter1_Outer1, z) 

	= (idOuter1_Outer1_2, z_2);

tel

-- Exit action for state :Outer1_A

node Outer1_A_ex(w_1:int;

	idOuter1_Outer1_1:int;

	isInner:bool)

returns (w:int;

	idOuter1_Outer1:int);

var 	w_2:int;

	idOuter1_Outer1_2:int;

let

	w_2 

	= if (not isInner) then  w_1  + 1

	 else w_1;

	-- set state as inactive 

	idOuter1_Outer1_2

	 = if (not isInner) then 0 else idOuter1_Outer1_1;

	(w, idOuter1_Outer1) 

	= (w_2, idOuter1_Outer1_1);

tel

--***************************************************State :Outer1_Outer1 Automaton***************************************************

node Outer1_Outer1_node(idOuter1_Outer1_1:int;

	z_1:int;

	E:bool;

	x_1:int;

	w_1:int;

	y_1:int)

returns (idOuter1_Outer1:int;

	z:int;

	x:int;

	w:int;

	y:int);

let

	 automaton outer1_outer1

	state POINTOuter1_Outer1:

	unless (idOuter1_Outer1_1=0) restart POINT__TO__OUTER1_A_1

	unless (idOuter1_Outer1_1=1360) and E restart OUTER1_A__TO__OUTER1_A_1

	unless (idOuter1_Outer1_1=1360) restart OUTER1_A_IDL

	let

		(idOuter1_Outer1, z, x, w, y) 

	= (idOuter1_Outer1_1, z_1, x_1, w_1, y_1);

	tel

	state POINT__TO__OUTER1_A_1:

	 var 	idOuter1_Outer1_2:int;

	z_2:int;

	let

		-- transition trace :

	--POINT__To__Outer1_A_1

		(idOuter1_Outer1_2, z_2) 

	= Outer1_A_en(idOuter1_Outer1_1, z_1, false);

	(idOuter1_Outer1, z) 

	=  (idOuter1_Outer1_2, z_2);

	--add unused variables

	(w, x, y) 

	= (w_1, x_1, y_1);

	tel

	until true restart POINTOuter1_Outer1

	state OUTER1_A__TO__OUTER1_A_1:

	 var 	idOuter1_Outer1_2, idOuter1_Outer1_3:int;

	z_2:int;

	x_2:int;

	w_2:int;

	y_2:int;

	let

		-- transition trace :

	--Outer1_A__To__Outer1_A_1

		-- condition Action : x++;

		(x_2) 

	= Outer1_A__To__Outer1_A_1_Condition_Action(x_1);

		(w_2, idOuter1_Outer1_2) 

	= Outer1_A_ex(w_1, idOuter1_Outer1_1, false);

		(y_2) 

	= Outer1_A__To__Outer1_A_1_Transition_Action(y_1);

		(idOuter1_Outer1_3, z_2) 

	= Outer1_A_en(idOuter1_Outer1_2, z_1, false);

	(idOuter1_Outer1, z, x, w, y) 

	=  (idOuter1_Outer1_3, z_2, x_2, w_2, y_2);

	tel

	until true restart POINTOuter1_Outer1

	state OUTER1_A_IDL:

	 	let

	(idOuter1_Outer1, z, x, w, y) 

	= (idOuter1_Outer1_1, z_1, x_1, w_1, y_1);

	tel

	until true restart POINTOuter1_Outer1

tel

--***************************************************State :Outer1_Outer1 Automaton***************************************************

node Outer1_Outer1(E:bool)

returns (w:int;

	x:int;

	z:int;

	y:int);

var w_1: int;

	x_1: int;

	z_1: int;

	y_1: int;

	idOuter1_Outer1, idOuter1_Outer1_1: int;

	let

	w_1 = 0 -> pre w;

	x_1 = 0 -> pre x;

	z_1 = 0 -> pre z;

	y_1 = 0 -> pre y;

	idOuter1_Outer1_1 = 0 -> pre idOuter1_Outer1;

	(idOuter1_Outer1, z, x, w, y)

	 = 

	 if E then Outer1_Outer1_node(idOuter1_Outer1_1, z_1, E, x_1, w_1, y_1)

	 else (idOuter1_Outer1_1, z_1, x_1, w_1, y_1);

--unused outputs

tel

node Outer1 (E_1_1 : real)

returns (w_1_1 : int;

	x_2_1 : int;

	z_3_1 : int;

	y_4_1 : int); 

var

	Outer1_1_1 : int; Outer1_2_1 : int; Outer1_3_1 : int; Outer1_4_1 : int;

	i_virtual_local : real;

	Outer1E_1_1_event: bool;

let 

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

	(Outer1_1_1, Outer1_2_1, Outer1_3_1, Outer1_4_1) =  Outer1_Outer1(Outer1E_1_1_event);

	w_1_1 = Outer1_1_1;

	x_2_1 = Outer1_2_1;

	z_3_1 = Outer1_3_1;

	y_4_1 = Outer1_4_1;

	i_virtual_local= 0.0 -> 1.0;

tel