CristalCaveGem » LustreC » Lustrec-Tests

-- This file has been generated by cocoSim

-- External Stateflow functions

node after(n:int; E : bool; id:int ) returns ( Y : bool );

var count:int;

let

	count = 0 -> if (pre id != id) then

		 if E then 1 else 0 

	else

	 if E then (pre count) + 1 else pre count;

	 Y =  count >= n ;

tel

-- System nodes

-- Entry action for state :Temporal1_B

node Temporal1_B_en(idTemporal1_Temporal1_1:int;

	x_1:int;

	isInner:bool)

returns (idTemporal1_Temporal1:int;

	x:int);

var 	idTemporal1_Temporal1_2:int;

	x_2:int;

let

	-- set state as active 

	idTemporal1_Temporal1_2 

	= 123;

	x_2 

	= if (not isInner) then  x_1  + 1

	 else x_1;

	(idTemporal1_Temporal1, x) 

	= (idTemporal1_Temporal1_2, x_2);

tel

-- Exit action for state :Temporal1_B

node Temporal1_B_ex(idTemporal1_Temporal1_1:int;

	isInner:bool)

returns (idTemporal1_Temporal1:int);

var 	idTemporal1_Temporal1_2:int;

let

	-- set state as inactive 

	idTemporal1_Temporal1_2

	 = if (not isInner) then 0 else idTemporal1_Temporal1_1;

	(idTemporal1_Temporal1) 

	= (idTemporal1_Temporal1_1);

tel

-- Entry action for state :Temporal1_A

node Temporal1_A_en(idTemporal1_Temporal1_1:int;

	x_1:int;

	isInner:bool)

returns (idTemporal1_Temporal1:int;

	x:int);

var 	idTemporal1_Temporal1_2:int;

	x_2:int;

let

	-- set state as active 

	idTemporal1_Temporal1_2 

	= 122;

	x_2 

	= if (not isInner) then  x_1  + 1

	 else x_1;

	(idTemporal1_Temporal1, x) 

	= (idTemporal1_Temporal1_2, x_2);

tel

-- Exit action for state :Temporal1_A

node Temporal1_A_ex(idTemporal1_Temporal1_1:int;

	isInner:bool)

returns (idTemporal1_Temporal1:int);

var 	idTemporal1_Temporal1_2:int;

let

	-- set state as inactive 

	idTemporal1_Temporal1_2

	 = if (not isInner) then 0 else idTemporal1_Temporal1_1;

	(idTemporal1_Temporal1) 

	= (idTemporal1_Temporal1_1);

tel

--***************************************************State :Temporal1_Temporal1 Automaton***************************************************

node Temporal1_Temporal1_node(idTemporal1_Temporal1_1:int;

	x_1:int;

	E:bool)

returns (idTemporal1_Temporal1:int;

	x:int);

var 	after_E_2_output: bool;

 	after_E_3_output: bool;

let

	after_E_2_output =after(2,E,idTemporal1_Temporal1_1);

 	after_E_3_output =after(3,E,idTemporal1_Temporal1_1);

	 automaton temporal1_temporal1

	state POINTTemporal1_Temporal1:

	unless (idTemporal1_Temporal1_1=0) restart POINT__TO__TEMPORAL1_A_1

	unless (idTemporal1_Temporal1_1=122) and E and ( after_E_2_output ) restart TEMPORAL1_A__TO__TEMPORAL1_B_1

	unless (idTemporal1_Temporal1_1=123) and after_E_3_output restart TEMPORAL1_B__TO__TEMPORAL1_A_1

	unless (idTemporal1_Temporal1_1=122) restart TEMPORAL1_A_IDL

	unless (idTemporal1_Temporal1_1=123) restart TEMPORAL1_B_IDL

	let

		(idTemporal1_Temporal1, x) 

	= (idTemporal1_Temporal1_1, x_1);

	tel

	state POINT__TO__TEMPORAL1_A_1:

	 var 	idTemporal1_Temporal1_2:int;

	x_2:int;

	let

		-- transition trace :

	--POINT__To__Temporal1_A_1

		(idTemporal1_Temporal1_2, x_2) 

	= Temporal1_A_en(idTemporal1_Temporal1_1, x_1, false);

	(idTemporal1_Temporal1, x) 

	=  (idTemporal1_Temporal1_2, x_2);

	tel

	until true restart POINTTemporal1_Temporal1

	state TEMPORAL1_A__TO__TEMPORAL1_B_1:

	 var 	idTemporal1_Temporal1_2, idTemporal1_Temporal1_3:int;

	x_2:int;

	let

		-- transition trace :

	--Temporal1_A__To__Temporal1_B_1

		(idTemporal1_Temporal1_2) 

	= Temporal1_A_ex(idTemporal1_Temporal1_1, false);

		(idTemporal1_Temporal1_3, x_2) 

	= Temporal1_B_en(idTemporal1_Temporal1_2, x_1, false);

	(idTemporal1_Temporal1, x) 

	=  (idTemporal1_Temporal1_3, x_2);

	tel

	until true restart POINTTemporal1_Temporal1

	state TEMPORAL1_B__TO__TEMPORAL1_A_1:

	 var 	idTemporal1_Temporal1_2, idTemporal1_Temporal1_3:int;

	x_2:int;

	let

		-- transition trace :

	--Temporal1_B__To__Temporal1_A_1

		(idTemporal1_Temporal1_2) 

	= Temporal1_B_ex(idTemporal1_Temporal1_1, false);

		(idTemporal1_Temporal1_3, x_2) 

	= Temporal1_A_en(idTemporal1_Temporal1_2, x_1, false);

	(idTemporal1_Temporal1, x) 

	=  (idTemporal1_Temporal1_3, x_2);

	tel

	until true restart POINTTemporal1_Temporal1

	state TEMPORAL1_A_IDL:

	 	let

	(idTemporal1_Temporal1, x) 

	= (idTemporal1_Temporal1_1, x_1);

	tel

	until true restart POINTTemporal1_Temporal1

	state TEMPORAL1_B_IDL:

	 	let

	(idTemporal1_Temporal1, x) 

	= (idTemporal1_Temporal1_1, x_1);

	tel

	until true restart POINTTemporal1_Temporal1

tel

--***************************************************State :Temporal1_Temporal1 Automaton***************************************************

node Temporal1_Temporal1(E:bool)

returns (x:int);

var x_1: int;

	idTemporal1_Temporal1, idTemporal1_Temporal1_1: int;

	let

	x_1 = 0 -> pre x;

	idTemporal1_Temporal1_1 = 0 -> pre idTemporal1_Temporal1;

	(idTemporal1_Temporal1, x)

	 = 

	 if E then Temporal1_Temporal1_node(idTemporal1_Temporal1_1, x_1, E)

	 else (idTemporal1_Temporal1_1, x_1);

--unused outputs

tel

node Temporal1 (E_1_1 : real)

returns (x_1_1 : int); 

var

	Temporal1_1_1 : int;

	i_virtual_local : real;

	Temporal1E_1_1_event: bool;

let 

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

	Temporal1_1_1 =  Temporal1_Temporal1(Temporal1E_1_1_event);

	x_1_1 = Temporal1_1_1;

	i_virtual_local= 0.0 -> 1.0;

tel