CristalCaveGem » LustreC » Lustrec-Tests

-- This file has been generated by cocoSim

-- System nodes

node Flowchart7_Flowchart7Junction833__To__Flowchart7_Flowchart7Junction834_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

node POINT__To__Flowchart7_Flowchart7Junction832_1_Condition_Action(cent_1:int)

returns (cent:int);

var 	cent_2:int;

let

	cent_2 

	=  cent_1  + 1;

	(cent) 

	= (cent_2);

tel

node Flowchart7_Flowchart7Junction832__To__Flowchart7_Flowchart7Junction833_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

--***************************************************State :Flowchart7_Flowchart7 Automaton***************************************************

node Flowchart7_Flowchart7_node(idFlowchart7_Flowchart7_1:int;

	TIC:bool;

	cent_1:int;

	sec_1:int;

	min_1:int)

returns (idFlowchart7_Flowchart7:int;

	cent:int;

	sec:int;

	min:int);

let

	 automaton flowchart7_flowchart7

	state POINTFlowchart7_Flowchart7:

	unless (idFlowchart7_Flowchart7_1=0) and TIC restart POINT__TO__FLOWCHART7_FLOWCHART7JUNCTION832_1

	let

		(idFlowchart7_Flowchart7, cent, sec, min) 

	= (idFlowchart7_Flowchart7_1, cent_1, sec_1, min_1);

	tel

	state POINT__TO__FLOWCHART7_FLOWCHART7JUNCTION832_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 :

	--POINT__To__Junction832_1, Junction832__To__Junction833_1, Junction833__To__Junction834_1

		-- condition Action : cent++

		(cent_2) 

	= POINT__To__Flowchart7_Flowchart7Junction832_1_Condition_Action(cent_1);

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

		(cent_3, sec_2) 

	= 

		 if ((  cent_2 =2 )) then 

		Flowchart7_Flowchart7Junction832__To__Flowchart7_Flowchart7Junction833_1_Condition_Action(cent_2, sec_1)

		 else (cent_2, sec_1);

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

		(sec_3, min_2) 

	= 

		 if ((  cent_2 =2 ) and (  sec_2 =3 )) then 

		Flowchart7_Flowchart7Junction833__To__Flowchart7_Flowchart7Junction834_1_Condition_Action(sec_2, min_1)

		 else (sec_2, min_1);

-- transition trace :

	--POINT__To__Junction832_1, Junction832__To__Junction833_1, Junction833__To__Junction834_2

		-- condition Action : cent++

		(cent_4) 

	= POINT__To__Flowchart7_Flowchart7Junction832_1_Condition_Action(cent_1);

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

		(cent_5, sec_4) 

	= 

		 if ((  cent_4 =2 )) then 

		Flowchart7_Flowchart7Junction832__To__Flowchart7_Flowchart7Junction833_1_Condition_Action(cent_4, sec_1)

		 else (cent_4, sec_1);

-- transition trace :

	--POINT__To__Junction832_1, Junction832__To__Junction834_2

		-- condition Action : cent++

		(cent_6) 

	= POINT__To__Flowchart7_Flowchart7Junction832_1_Condition_Action(cent_1);

	(idFlowchart7_Flowchart7, cent, sec, min) 

	= 

		 if ((  cent_2 =2 ) and (  sec_2 =3 )) then 

		(idFlowchart7_Flowchart7_1, cent_3, sec_3, min_2)

		 else

		 if ((  cent_4 =2 )) then 

		(idFlowchart7_Flowchart7_1, cent_5, sec_4, min_1)

		 else

		 if ((  cent_4 =2 )) then 

		(idFlowchart7_Flowchart7_1, cent_5, sec_4, min_1)

		 else (idFlowchart7_Flowchart7_1, cent_6, sec_1, min_1);

	tel

	until true restart POINTFlowchart7_Flowchart7

tel

--***************************************************State :Flowchart7_Flowchart7 Automaton***************************************************

node Flowchart7_Flowchart7(TIC:bool)

returns (cent:int;

	sec:int;

	min:int);

var cent_1: int;

	sec_1: int;

	min_1: int;

	idFlowchart7_Flowchart7, idFlowchart7_Flowchart7_1: int;

	let

	cent_1 = 0 -> pre cent;

	sec_1 = 0 -> pre sec;

	min_1 = 0 -> pre min;

	idFlowchart7_Flowchart7_1 = 0 -> pre idFlowchart7_Flowchart7;

	(idFlowchart7_Flowchart7, cent, sec, min)

	 = 

	 if TIC then Flowchart7_Flowchart7_node(idFlowchart7_Flowchart7_1, TIC, cent_1, sec_1, min_1)

	 else (idFlowchart7_Flowchart7_1, cent_1, sec_1, min_1);

--unused outputs

tel

node Flowchart7 (TIC_1_1 : real)

returns (Out1_1_1 : int;

	Out2_2_1 : int;

	Out3_3_1 : int); 

var

	Flowchart7_1_1 : int; Flowchart7_2_1 : int; Flowchart7_3_1 : int;

	i_virtual_local : real;

	Flowchart7TIC_1_1_event: bool;

let 

	Flowchart7TIC_1_1_event = false -> ((pre(TIC_1_1) > 0.0 and TIC_1_1 <= 0.0) or (pre(TIC_1_1) <= 0.0 and TIC_1_1 > 0.0));

	(Flowchart7_1_1, Flowchart7_2_1, Flowchart7_3_1) =  Flowchart7_Flowchart7(Flowchart7TIC_1_1_event);

	Out1_1_1 = Flowchart7_1_1;

	Out2_2_1 = Flowchart7_2_1;

	Out3_3_1 = Flowchart7_3_1;

	i_virtual_local= 0.0 -> 1.0;

tel