CristalCaveGem » LustreC » Lustrec-Tests

-- This file has been generated by cocoSim

-- System nodes

node Chart_A__To__Chart_ChartJunction1192_1_Condition_Action(y_1:int)

returns (y:int);

var 	y_2:int;

let

	y_2 

	=  y_1  + 1;

	(y) 

	= (y_2);

tel

node Chart_A__To__Chart_ChartJunction1192_1_Transition_Action(z_1:int)

returns (z:int);

var 	z_2:int;

let

	z_2 

	=  z_1 +2;

	(z) 

	= (z_2);

tel

node Chart_ChartJunction1192__To__Chart_C_2_Condition_Action(y_1:int)

returns (y:int);

var 	y_2:int;

let

	y_2 

	=  y_1  + 1;

	(y) 

	= (y_2);

tel

node Chart_ChartJunction1192__To__Chart_C_2_Transition_Action(z_1:int)

returns (z:int);

var 	z_2:int;

let

	z_2 

	=  z_1  + 1;

	(z) 

	= (z_2);

tel

node Chart_ChartJunction1192__To__Chart_B_1_Condition_Action(y_1:int)

returns (y:int);

var 	y_2:int;

let

	y_2 

	=  y_1 +2;

	(y) 

	= (y_2);

tel

node Chart_ChartJunction1192__To__Chart_B_1_Transition_Action(z_1:int)

returns (z:int);

var 	z_2, z_3:int;

let

	z_2 

	=  z_1  + 1;

	z_3 

	=  z_2  + 1;

	(z) 

	= (z_3);

tel

-- Entry action for state :Chart_B

node Chart_B_en(idChart_Chart_1:int;

	isInner:bool)

returns (idChart_Chart:int);

var 	idChart_Chart_2:int;

let

	-- set state as active 

	idChart_Chart_2 

	= 1186;

	(idChart_Chart) 

	= (idChart_Chart_2);

tel

-- Exit action for state :Chart_B

node Chart_B_ex(idChart_Chart_1:int;

	isInner:bool)

returns (idChart_Chart:int);

var 	idChart_Chart_2:int;

let

	-- set state as inactive 

	idChart_Chart_2

	 = if (not isInner) then 0 else idChart_Chart_1;

	(idChart_Chart) 

	= (idChart_Chart_1);

tel

-- Entry action for state :Chart_A

node Chart_A_en(idChart_Chart_1:int;

	isInner:bool)

returns (idChart_Chart:int);

var 	idChart_Chart_2:int;

let

	-- set state as active 

	idChart_Chart_2 

	= 1185;

	(idChart_Chart) 

	= (idChart_Chart_2);

tel

-- Exit action for state :Chart_A

node Chart_A_ex(idChart_Chart_1:int;

	isInner:bool)

returns (idChart_Chart:int);

var 	idChart_Chart_2:int;

let

	-- set state as inactive 

	idChart_Chart_2

	 = if (not isInner) then 0 else idChart_Chart_1;

	(idChart_Chart) 

	= (idChart_Chart_1);

tel

-- Entry action for state :Chart_C

node Chart_C_en(idChart_Chart_1:int;

	isInner:bool)

returns (idChart_Chart:int);

var 	idChart_Chart_2:int;

let

	-- set state as active 

	idChart_Chart_2 

	= 1187;

	(idChart_Chart) 

	= (idChart_Chart_2);

tel

-- Exit action for state :Chart_C

node Chart_C_ex(idChart_Chart_1:int;

	isInner:bool)

returns (idChart_Chart:int);

var 	idChart_Chart_2:int;

let

	-- set state as inactive 

	idChart_Chart_2

	 = if (not isInner) then 0 else idChart_Chart_1;

	(idChart_Chart) 

	= (idChart_Chart_1);

tel

--***************************************************State :Chart_Chart Automaton***************************************************

node Chart_Chart_node(idChart_Chart_1:int;

	E1:bool;

	x:int;

	y_1:int;

	z_1:int)

returns (idChart_Chart:int;

	y:int;

	z:int);

let

	 automaton chart_chart

	state POINTChart_Chart:

	unless (idChart_Chart_1=0) restart POINT__TO__CHART_A_1

	unless (idChart_Chart_1=1185) and E1 and ( x>0 ) restart CHART_A__TO__CHART_CHARTJUNCTION1192_1

	unless (idChart_Chart_1=1186) and ( x>3 ) restart CHART_B__TO__CHART_A_1

	unless (idChart_Chart_1=1187) and ( x>3 ) restart CHART_C__TO__CHART_A_1

	unless (idChart_Chart_1=1185) restart CHART_A_IDL

	unless (idChart_Chart_1=1186) restart CHART_B_IDL

	unless (idChart_Chart_1=1187) restart CHART_C_IDL

	let

		(idChart_Chart, y, z) 

	= (idChart_Chart_1, y_1, z_1);

	tel

	state POINT__TO__CHART_A_1:

	 var 	idChart_Chart_2:int;

	let

		-- transition trace :

	--POINT__To__Chart_A_1

		(idChart_Chart_2) 

	= Chart_A_en(idChart_Chart_1, false);

	(idChart_Chart) 

	=  (idChart_Chart_2);

	--add unused variables

	(y, z) 

	= (y_1, z_1);

	tel

	until true restart POINTChart_Chart

	state CHART_A__TO__CHART_CHARTJUNCTION1192_1:

	 var 	idChart_Chart_2, idChart_Chart_3, idChart_Chart_4, idChart_Chart_5:int;

	y_2, y_3, y_4, y_5:int;

	z_2, z_3, z_4, z_5:int;

	let

-- transition trace :

	--Chart_A__To__Junction1192_1, Junction1192__To__Chart_B_1

		-- condition Action : y++

		(y_2) 

	= Chart_A__To__Chart_ChartJunction1192_1_Condition_Action(y_1);

		-- condition Action : y+=2

		(y_3) 

	= 

		 if (( x>2 )) then 

		Chart_ChartJunction1192__To__Chart_B_1_Condition_Action(y_2)

		 else (y_2);

		(idChart_Chart_2) 

	= 

		 if (( x>2 )) then 

		Chart_A_ex(idChart_Chart_1, false)

		 else (idChart_Chart_1);

		(z_2) 

	= 

		 if (( x>2 )) then 

		Chart_A__To__Chart_ChartJunction1192_1_Transition_Action(z_1)

		 else (z_1);

		(z_3) 

	= 

		 if (( x>2 )) then 

		Chart_ChartJunction1192__To__Chart_B_1_Transition_Action(z_2)

		 else (z_2);

		(idChart_Chart_3) 

	= 

		 if (( x>2 )) then 

		Chart_B_en(idChart_Chart_2, false)

		 else (idChart_Chart_2);

-- transition trace :

	--Chart_A__To__Junction1192_1, Junction1192__To__Chart_C_2

		-- condition Action : y++

		(y_4) 

	= Chart_A__To__Chart_ChartJunction1192_1_Condition_Action(y_1);

		-- condition Action : y++

		(y_5) 

	= 

		 if (( x<=2 )) then 

		Chart_ChartJunction1192__To__Chart_C_2_Condition_Action(y_4)

		 else (y_4);

		(idChart_Chart_4) 

	= 

		 if (( x<=2 )) then 

		Chart_A_ex(idChart_Chart_1, false)

		 else (idChart_Chart_1);

		(z_4) 

	= 

		 if (( x<=2 )) then 

		Chart_A__To__Chart_ChartJunction1192_1_Transition_Action(z_1)

		 else (z_1);

		(z_5) 

	= 

		 if (( x<=2 )) then 

		Chart_ChartJunction1192__To__Chart_C_2_Transition_Action(z_4)

		 else (z_4);

		(idChart_Chart_5) 

	= 

		 if (( x<=2 )) then 

		Chart_C_en(idChart_Chart_4, false)

		 else (idChart_Chart_4);

	(idChart_Chart, y, z) 

	= 

		 if (( x>2 )) then 

		(idChart_Chart_3, y_3, z_3)

		 else

		 if (( x<=2 )) then 

		(idChart_Chart_5, y_5, z_5)

		 else (idChart_Chart_1, y_4, z_1);

	tel

	until true restart POINTChart_Chart

	state CHART_B__TO__CHART_A_1:

	 var 	idChart_Chart_2, idChart_Chart_3:int;

	let

		-- transition trace :

	--Chart_B__To__Chart_A_1

		(idChart_Chart_2) 

	= Chart_B_ex(idChart_Chart_1, false);

		(idChart_Chart_3) 

	= Chart_A_en(idChart_Chart_2, false);

	(idChart_Chart, y, z) 

	=  (idChart_Chart_3, y_1, z_1);

	tel

	until true restart POINTChart_Chart

	state CHART_C__TO__CHART_A_1:

	 var 	idChart_Chart_2, idChart_Chart_3:int;

	let

		-- transition trace :

	--Chart_C__To__Chart_A_1

		(idChart_Chart_2) 

	= Chart_C_ex(idChart_Chart_1, false);

		(idChart_Chart_3) 

	= Chart_A_en(idChart_Chart_2, false);

	(idChart_Chart, y, z) 

	=  (idChart_Chart_3, y_1, z_1);

	tel

	until true restart POINTChart_Chart

	state CHART_A_IDL:

	 	let

	(idChart_Chart, y, z) 

	= (idChart_Chart_1, y_1, z_1);

	tel

	until true restart POINTChart_Chart

	state CHART_B_IDL:

	 	let

	(idChart_Chart, y, z) 

	= (idChart_Chart_1, y_1, z_1);

	tel

	until true restart POINTChart_Chart

	state CHART_C_IDL:

	 	let

	(idChart_Chart, y, z) 

	= (idChart_Chart_1, y_1, z_1);

	tel

	until true restart POINTChart_Chart

tel

--***************************************************State :Chart_Chart Automaton***************************************************

node Junctions1V0_Chart(x:int;

	E1:bool)

returns (y:int;

	z:int);

var y_1: int;

	z_1: int;

	idChart_Chart, idChart_Chart_1: int;

	let

	y_1 = 1 -> pre y;

	z_1 = 2 -> pre z;

	idChart_Chart_1 = 0 -> pre idChart_Chart;

	(idChart_Chart, y, z)

	 = 

	 if E1 then Chart_Chart_node(idChart_Chart_1, E1, x, y_1, z_1)

	 else (idChart_Chart_1, y_1, z_1);

--unused outputs

tel

node Junctions1V0 (x_1_1 : int; E1_1_1 : real)

returns (y_1_1 : int;

	z_2_1 : int); 

var

	Chart_1_1 : int; Chart_2_1 : int;

	i_virtual_local : real;

	ChartE1_1_1_event: bool;

let 

	ChartE1_1_1_event = false -> ((pre(E1_1_1) > 0.0 and E1_1_1 <= 0.0) or (pre(E1_1_1) <= 0.0 and E1_1_1 > 0.0));

	(Chart_1_1, Chart_2_1) =  Junctions1V0_Chart(x_1_1, ChartE1_1_1_event);

	y_1_1 = Chart_1_1;

	z_2_1 = Chart_2_1;

	i_virtual_local= 0.0 -> 1.0;

tel