CristalCaveGem » LustreC » Lustrec-Tests

-- This file has been generated by cocoSim

-- System nodes

node Chart_ChartJunction314__To__Chart_ChartJunction315_1_Condition_Action(cent_1:int;

	sec_1:int)

returns (cent:int;

	sec:int);

var 	cent_2:int;

	sec_2:int;

let

	cent_2 

	= 0;

	sec_2 

	=  sec_1 +1;

	(cent, sec) 

	= (cent_2, sec_2);

tel

node Chart_Run__To__Chart_ChartJunction314_1_Condition_Action(cent_1:int)

returns (cent:int);

var 	cent_2:int;

let

	cent_2 

	=  cent_1 +1;

	(cent) 

	= (cent_2);

tel

node Stop_Reset__To__Chart_ChartJunction300_1_Condition_Action(cent_1:int;

	sec_1:int;

	min_1:int;

	disp_cent_1:int;

	disp_sec_1:int;

	disp_min_1:int)

returns (cent:int;

	sec:int;

	min:int;

	disp_cent:int;

	disp_sec:int;

	disp_min:int);

var 	cent_2:int;

	sec_2:int;

	min_2:int;

	disp_cent_2:int;

	disp_sec_2:int;

	disp_min_2:int;

let

	cent_2 

	= 0;

	sec_2 

	= 0;

	min_2 

	= 0;

	disp_cent_2 

	= 0;

	disp_sec_2 

	= 0;

	disp_min_2 

	= 0;

	(cent, sec, min, disp_cent, disp_sec, disp_min) 

	= (cent_2, sec_2, min_2, disp_cent_2, disp_sec_2, disp_min_2);

tel

node Chart_ChartJunction315__To__Chart_ChartJunction316_1_Condition_Action(sec_1:int;

	min_1:int)

returns (sec:int;

	min:int);

var 	sec_2:int;

	min_2:int;

let

	sec_2 

	= 0;

	min_2 

	=  min_1 +1;

	(sec, min) 

	= (sec_2, min_2);

tel

-- Entry action for state :Run_Lap

node Run_Lap_en(idChart_Run_1:int;

	isInner:bool)

returns (idChart_Run:int);

var 	idChart_Run_2:int;

let

	-- set state as active 

	idChart_Run_2 

	= 306;

	(idChart_Run) 

	= (idChart_Run_2);

tel

-- Exit action for state :Run_Lap

node Run_Lap_ex(idChart_Run_1:int;

	isInner:bool)

returns (idChart_Run:int);

var 	idChart_Run_2:int;

let

	-- set state as inactive 

	idChart_Run_2

	 = if (not isInner) then 0 else idChart_Run_1;

	(idChart_Run) 

	= (idChart_Run_1);

tel

-- Entry action for state :Run_Running

node Run_Running_en(idChart_Run_1:int;

	x_1:int;

	isInner:bool)

returns (idChart_Run:int;

	x:int);

var 	idChart_Run_2:int;

	x_2:int;

let

	-- set state as active 

	idChart_Run_2 

	= 305;

	x_2 

	= if (not isInner) then  x_1  + 1

	 else x_1;

	(idChart_Run, x) 

	= (idChart_Run_2, x_2);

tel

--During action for state :Run_Running

node Run_Running_du(cent_1:int;

	disp_cent_1:int;

	sec_1:int;

	disp_sec_1:int;

	min_1:int;

	disp_min_1:int)

returns (cent:int;

	disp_cent:int;

	sec:int;

	disp_sec:int;

	min:int;

	disp_min:int);

var 	disp_cent_2:int;

	disp_sec_2:int;

	disp_min_2:int;

let

	disp_cent_2 

	=  cent_1 ;

	disp_sec_2 

	=  sec_1 ;

	disp_min_2 

	=  min_1 ;

	(cent, disp_cent, sec, disp_sec, min, disp_min) 

	= (cent_1, disp_cent_2, sec_1, disp_sec_2, min_1, disp_min_2);

tel

-- Exit action for state :Run_Running

node Run_Running_ex(x_1:int;

	idChart_Run_1:int;

	isInner:bool)

returns (x:int;

	idChart_Run:int);

var 	x_2:int;

	idChart_Run_2:int;

let

	x_2 

	= if (not isInner) then  x_1  - 1

	 else x_1;

	-- set state as inactive 

	idChart_Run_2

	 = if (not isInner) then 0 else idChart_Run_1;

	(x, idChart_Run) 

	= (x_2, idChart_Run_1);

tel

-- Entry action for state :Chart_Run

node Chart_Run_en(idChart_Run_1:int;

	idChart_Chart_1:int;

	x_1:int;

	isInner:bool)

returns (idChart_Run:int;

	idChart_Chart:int;

	x:int);

var 	idChart_Run_2, idChart_Run_3, idChart_Run_4:int;

	idChart_Chart_2, idChart_Chart_3:int;

	x_2, x_3:int;

let

	-- set state as active 

	idChart_Chart_2 

	= 304;

	(idChart_Run_2, x_2) 

	= 

	if ( idChart_Run_1 = 305) then

	Run_Running_en(idChart_Run_1, x_1, false)

	 else (idChart_Run_1, x_1);

	(idChart_Run_3) 

	= 

	if ( idChart_Run_1 = 306) then

	Run_Lap_en(idChart_Run_1, false)

	 else (idChart_Run_1);

	(idChart_Run_4, idChart_Chart_3, x_3) 

	= 

		 if ( idChart_Run_1 = 305) then 

		(idChart_Run_2, idChart_Chart_2, x_2)

		 else

		 if ( idChart_Run_1 = 306) then 

		(idChart_Run_3, idChart_Chart_2, x_1)

		 else (idChart_Run_1, idChart_Chart_2, x_1);

	(idChart_Run, idChart_Chart, x) 

	= (idChart_Run_4, idChart_Chart_3, x_3);

tel

-- Exit action for state :Chart_Run

node Chart_Run_ex(x_1:int;

	idChart_Run_1:int;

	idChart_Chart_1:int;

	isInner:bool)

returns (x:int;

	idChart_Run:int;

	idChart_Chart:int);

var 	x_2, x_3:int;

	idChart_Run_2, idChart_Run_3, idChart_Run_4, idChart_Run_5:int;

	idChart_Chart_2:int;

let

	(x_2, idChart_Run_2) 

	= 

	if ( idChart_Run_1 = 305) then

	Run_Running_ex(x_1, idChart_Run_1, false)

	 else (x_1, idChart_Run_1);

	(idChart_Run_3) 

	= 

	if ( idChart_Run_1 = 306) then

	Run_Lap_ex(idChart_Run_1, false)

	 else (idChart_Run_1);

	(x_3, idChart_Run_4) 

	= 

		 if ( idChart_Run_1 = 305) then 

		(x_2, idChart_Run_2)

		 else

		 if ( idChart_Run_1 = 306) then 

		(x_1, idChart_Run_3)

		 else (x_1, idChart_Run_1);

	-- set state as inactive 

	idChart_Chart_2

	 = if (not isInner) then 0 else idChart_Chart_1;

	idChart_Run_5 

	= 0;

	(x, idChart_Run, idChart_Chart) 

	= (x_3, idChart_Run_5, idChart_Chart_1);

tel

--During action for state :Chart_Run

node Chart_Run_du(TIC:bool;

	cent_1:int;

	sec_1:int;

	min_1:int)

returns (cent:int;

	sec:int;

	min:int);

let

		 automaton chart_run_INNER

	state POINTChart_Run_INNER:

	unless true and TIC restart CHART_RUN__TO__CHART_CHARTJUNCTION314_1

	let

		(cent, sec, min) 

	= (cent_1, sec_1, min_1);

	tel

	state CHART_RUN__TO__CHART_CHARTJUNCTION314_1:

	 var 	cent_2, cent_3, cent_4, cent_5, cent_6:int;

	sec_2, sec_3, sec_4:int;

	min_2:int;

	let

-- transition trace :

	--Chart_Run__To__Junction314_1, Junction314__To__Junction315_1, Junction315__To__Junction316_1

		-- condition Action : cent=cent+1;

		(cent_2) 

	= Chart_Run__To__Chart_ChartJunction314_1_Condition_Action(cent_1);

		-- condition Action : cent=0;sec=sec+1;

		(cent_3, sec_2) 

	= 

		 if ((  cent_2 =100 )) then 

		Chart_ChartJunction314__To__Chart_ChartJunction315_1_Condition_Action(cent_2, sec_1)

		 else (cent_2, sec_1);

		-- condition Action : sec=0;min=min+1;

		(sec_3, min_2) 

	= 

		 if ((  cent_2 =100 ) and (  sec_2 =60 )) then 

		Chart_ChartJunction315__To__Chart_ChartJunction316_1_Condition_Action(sec_2, min_1)

		 else (sec_2, min_1);

-- transition trace :

	--Chart_Run__To__Junction314_1, Junction314__To__Junction315_1, Junction315__To__Junction316_2

		-- condition Action : cent=cent+1;

		(cent_4) 

	= Chart_Run__To__Chart_ChartJunction314_1_Condition_Action(cent_1);

		-- condition Action : cent=0;sec=sec+1;

		(cent_5, sec_4) 

	= 

		 if ((  cent_4 =100 )) then 

		Chart_ChartJunction314__To__Chart_ChartJunction315_1_Condition_Action(cent_4, sec_1)

		 else (cent_4, sec_1);

-- transition trace :

	--Chart_Run__To__Junction314_1, Junction314__To__Junction316_2

		-- condition Action : cent=cent+1;

		(cent_6) 

	= Chart_Run__To__Chart_ChartJunction314_1_Condition_Action(cent_1);

	(cent, sec, min) 

	= 

		 if ((  cent_2 =100 ) and (  sec_2 =60 )) then 

		(cent_3, sec_3, min_2)

		 else

		 if ((  cent_4 =100 )) then 

		(cent_5, sec_4, min_1)

		 else

		 if ((  cent_4 =100 )) then 

		(cent_5, sec_4, min_1)

		 else (cent_6, sec_1, min_1);

	tel

	until true restart POINTChart_Run_INNER

tel

-- Entry action for state :Stop_Lap_stop

node Stop_Lap_stop_en(idChart_Stop_1:int;

	isInner:bool)

returns (idChart_Stop:int);

var 	idChart_Stop_2:int;

let

	-- set state as active 

	idChart_Stop_2 

	= 301;

	(idChart_Stop) 

	= (idChart_Stop_2);

tel

-- Exit action for state :Stop_Lap_stop

node Stop_Lap_stop_ex(idChart_Stop_1:int;

	isInner:bool)

returns (idChart_Stop:int);

var 	idChart_Stop_2:int;

let

	-- set state as inactive 

	idChart_Stop_2

	 = if (not isInner) then 0 else idChart_Stop_1;

	(idChart_Stop) 

	= (idChart_Stop_1);

tel

-- Entry action for state :Stop_Reset

node Stop_Reset_en(idStop_Reset_1:int;

	idChart_Stop_1:int;

	isInner:bool)

returns (idStop_Reset:int;

	idChart_Stop:int);

var 	idStop_Reset_2:int;

	idChart_Stop_2:int;

let

	-- set state as active 

	idChart_Stop_2 

	= 298;

	-- case of state without states but contains transitions 

	idStop_Reset_2 

	= -1;

	(idStop_Reset, idChart_Stop) 

	= (idStop_Reset_2, idChart_Stop_2);

tel

-- Exit action for state :Stop_Reset

node Stop_Reset_ex(idChart_Stop_1:int;

	isInner:bool)

returns (idChart_Stop:int);

var 	idChart_Stop_2:int;

let

	-- set state as inactive 

	idChart_Stop_2

	 = if (not isInner) then 0 else idChart_Stop_1;

	(idChart_Stop) 

	= (idChart_Stop_1);

tel

--During action for state :Stop_Reset

node Stop_Reset_du(LAP:bool;

	cent_1:int;

	disp_cent_1:int;

	disp_min_1:int;

	disp_sec_1:int;

	min_1:int;

	sec_1:int)

returns (cent:int;

	sec:int;

	min:int;

	disp_cent:int;

	disp_sec:int;

	disp_min:int);

let

		 automaton stop_reset_INNER

	state POINTStop_Reset_INNER:

	unless true and LAP restart STOP_RESET__TO__CHART_CHARTJUNCTION300_1

	let

		(cent, sec, min, disp_cent, disp_sec, disp_min) 

	= (cent_1, sec_1, min_1, disp_cent_1, disp_sec_1, disp_min_1);

	tel

	state STOP_RESET__TO__CHART_CHARTJUNCTION300_1:

	 var 	cent_2:int;

	sec_2:int;

	min_2:int;

	disp_cent_2:int;

	disp_sec_2:int;

	disp_min_2:int;

	let

		-- transition trace :

	--Stop_Reset__To__Junction300_1

		-- condition Action : cent=0;sec=0;min=0;disp_cent=0;disp_sec=0;disp_min=0;

		(cent_2, sec_2, min_2, disp_cent_2, disp_sec_2, disp_min_2) 

	= Stop_Reset__To__Chart_ChartJunction300_1_Condition_Action(cent_1, sec_1, min_1, disp_cent_1, disp_sec_1, disp_min_1);

	(cent, sec, min, disp_cent, disp_sec, disp_min) 

	=  (cent_2, sec_2, min_2, disp_cent_2, disp_sec_2, disp_min_2);

	tel

	until true restart POINTStop_Reset_INNER

tel

-- Entry action for state :Chart_Stop

node Chart_Stop_en(idChart_Stop_1:int;

	idChart_Chart_1:int;

	idStop_Reset_1:int;

	isInner:bool)

returns (idChart_Stop:int;

	idChart_Chart:int;

	idStop_Reset:int);

var 	idChart_Stop_2, idChart_Stop_3, idChart_Stop_4, idChart_Stop_5, idChart_Stop_6:int;

	idChart_Chart_2, idChart_Chart_3, idChart_Chart_4:int;

	idStop_Reset_2, idStop_Reset_3, idStop_Reset_4, idStop_Reset_5:int;

let

	-- set state as active 

	idChart_Chart_2 

	= 297;

-- transition trace :

	--POINT__To__Stop_Reset_1

		(idStop_Reset_2, idChart_Stop_2) 

	= Stop_Reset_en(idStop_Reset_1, idChart_Stop_1, false);

	(idChart_Stop_3, idChart_Chart_3, idStop_Reset_3) 

	= 

	if ( idChart_Stop_1 = 0) then

	 (idChart_Stop_2, idChart_Chart_2, idStop_Reset_2)

	 else(idChart_Stop_1, idChart_Chart_2, idStop_Reset_1);

	(idStop_Reset_4, idChart_Stop_4) 

	= 

	if ( idChart_Stop_1 = 298) then

	Stop_Reset_en(idStop_Reset_1, idChart_Stop_1, false)

	 else (idStop_Reset_1, idChart_Stop_1);

	(idChart_Stop_5) 

	= 

	if ( idChart_Stop_1 = 301) then

	Stop_Lap_stop_en(idChart_Stop_1, false)

	 else (idChart_Stop_1);

	(idChart_Stop_6, idChart_Chart_4, idStop_Reset_5) 

	= 

		 if ( idChart_Stop_1 = 0) then 

		(idChart_Stop_3, idChart_Chart_3, idStop_Reset_3)

		 else

		 if ( idChart_Stop_1 = 298) then 

		(idChart_Stop_4, idChart_Chart_3, idStop_Reset_4)

		 else

		 if ( idChart_Stop_1 = 301) then 

		(idChart_Stop_5, idChart_Chart_3, idStop_Reset_1)

		 else (idChart_Stop_1, idChart_Chart_2, idStop_Reset_1);

	(idChart_Stop, idChart_Chart, idStop_Reset) 

	= (idChart_Stop_6, idChart_Chart_4, idStop_Reset_5);

tel

-- Exit action for state :Chart_Stop

node Chart_Stop_ex(idChart_Stop_1:int;

	idChart_Chart_1:int;

	isInner:bool)

returns (idChart_Stop:int;

	idChart_Chart:int);

var 	idChart_Stop_2, idChart_Stop_3, idChart_Stop_4, idChart_Stop_5:int;

	idChart_Chart_2:int;

let

	(idChart_Stop_2) 

	= 

	if ( idChart_Stop_1 = 298) then

	Stop_Reset_ex(idChart_Stop_1, false)

	 else (idChart_Stop_1);

	(idChart_Stop_3) 

	= 

	if ( idChart_Stop_1 = 301) then

	Stop_Lap_stop_ex(idChart_Stop_1, false)

	 else (idChart_Stop_1);

	(idChart_Stop_4) 

	= 

		 if ( idChart_Stop_1 = 298) then 

		(idChart_Stop_2)

		 else

		 if ( idChart_Stop_1 = 301) then 

		(idChart_Stop_3)

		 else (idChart_Stop_1);

	-- set state as inactive 

	idChart_Chart_2

	 = if (not isInner) then 0 else idChart_Chart_1;

	idChart_Stop_5 

	= 0;

	(idChart_Stop, idChart_Chart) 

	= (idChart_Stop_5, idChart_Chart_1);

tel

--***************************************************State :Chart_Run Automaton***************************************************

node Chart_Run_node(idChart_Run_1:int;

	START:bool;

	idChart_Chart_1:int;

	x_1:int;

	idChart_Stop_1:int;

	idStop_Reset_1:int;

	LAP:bool;

	cent_1:int;

	disp_cent_1:int;

	disp_min_1:int;

	disp_sec_1:int;

	min_1:int;

	sec_1:int)

returns (idChart_Run:int;

	idChart_Chart:int;

	x:int;

	idChart_Stop:int;

	idStop_Reset:int;

	cent:int;

	disp_cent:int;

	disp_min:int;

	disp_sec:int;

	min:int;

	sec:int);

let

	 automaton chart_run

	state POINTChart_Run:

	unless (idChart_Run_1=305) and START restart RUN_RUNNING__TO__STOP_RESET_1

	unless (idChart_Run_1=305) and LAP restart RUN_RUNNING__TO__RUN_LAP_2

	unless (idChart_Run_1=306) and LAP restart RUN_LAP__TO__RUN_RUNNING_1

	unless (idChart_Run_1=306) and START restart RUN_LAP__TO__STOP_LAP_STOP_2

	unless (idChart_Run_1=305) restart RUN_RUNNING_IDL

	unless (idChart_Run_1=306) restart RUN_LAP_IDL

	let

		(idChart_Run, idChart_Chart, x, idChart_Stop, idStop_Reset, cent, disp_cent, disp_min, disp_sec, min, sec) 

	= (idChart_Run_1, idChart_Chart_1, x_1, idChart_Stop_1, idStop_Reset_1, cent_1, disp_cent_1, disp_min_1, disp_sec_1, min_1, sec_1);

	tel

	state RUN_RUNNING__TO__STOP_RESET_1:

	 var 	idChart_Run_2:int;

	idChart_Chart_2, idChart_Chart_3:int;

	x_2:int;

	idChart_Stop_2, idChart_Stop_3:int;

	idStop_Reset_2:int;

	let

		-- transition trace :

	--Run_Running__To__Stop_Reset_1

		(x_2, idChart_Run_2, idChart_Chart_2) 

	= Chart_Run_ex(x_1, idChart_Run_1, idChart_Chart_1, false);

		idChart_Stop_2 

	= 298;

		(idChart_Stop_3, idChart_Chart_3, idStop_Reset_2) 

	= Chart_Stop_en(idChart_Stop_2, idChart_Chart_2, idStop_Reset_1, false);

	(idChart_Run, idChart_Chart, x, idChart_Stop, idStop_Reset) 

	=  (idChart_Run_2, idChart_Chart_3, x_2, idChart_Stop_3, idStop_Reset_2);

	--add unused variables

	(cent, disp_cent, disp_min, disp_sec, min, sec) 

	= (cent_1, disp_cent_1, disp_min_1, disp_sec_1, min_1, sec_1);

	tel

	until true restart POINTChart_Run

	state RUN_RUNNING__TO__RUN_LAP_2:

	 var 	idChart_Run_2, idChart_Run_3:int;

	x_2:int;

	let

		-- transition trace :

	--Run_Running__To__Run_Lap_2

		(x_2, idChart_Run_2) 

	= Run_Running_ex(x_1, idChart_Run_1, false);

		(idChart_Run_3) 

	= Run_Lap_en(idChart_Run_2, false);

	(idChart_Run, idChart_Chart, x, idChart_Stop, idStop_Reset) 

	=  (idChart_Run_3, idChart_Chart_1, x_2, idChart_Stop_1, idStop_Reset_1);

	--add unused variables

	(cent, disp_cent, disp_min, disp_sec, min, sec) 

	= (cent_1, disp_cent_1, disp_min_1, disp_sec_1, min_1, sec_1);

	tel

	until true restart POINTChart_Run

	state RUN_LAP__TO__RUN_RUNNING_1:

	 var 	idChart_Run_2, idChart_Run_3:int;

	x_2:int;

	let

		-- transition trace :

	--Run_Lap__To__Run_Running_1

		(idChart_Run_2) 

	= Run_Lap_ex(idChart_Run_1, false);