/regression_tests/lustre_files/success/Stateflow/src_Events2/Events2.lus - Lustrec-Tests

lustrec-tests/regression_tests/lustre_files/success/Stateflow/src_Events2/Events2.lus @ 79ef5fc5

       -- This file has been generated by cocoSim
       -- System nodes
       -- Entry action for state :D_Da
       node D_Da_en(idEvents2_D_1:int;
       	x:int;
       	d_1:int;
       	isInner:bool)
       returns (idEvents2_D:int;
       	d:int);
       var 	idEvents2_D_2:int;
       	d_2:int;
       let
       	-- set state as active
       	idEvents2_D_2
       	= 620;
       	d_2
       	= if (not isInner) then x+7
       	 else d_1;
       	(idEvents2_D, d)
       	= (idEvents2_D_2, d_2);
       tel
       -- Exit action for state :D_Da
       node D_Da_ex(idEvents2_D_1:int;
       	isInner:bool)
       returns (idEvents2_D:int);
       var 	idEvents2_D_2:int;
       let
       	-- set state as inactive
       	idEvents2_D_2
       	 = if (not isInner) then 0 else idEvents2_D_1;
       	(idEvents2_D)
       	= (idEvents2_D_1);
       tel
       -- Entry action for state :D_Db
       node D_Db_en(idEvents2_D_1:int;
       	x:int;
       	d_1:int;
       	isInner:bool)
       returns (idEvents2_D:int;
       	d:int);
       var 	idEvents2_D_2:int;
       	d_2:int;
       let
       	-- set state as active
       	idEvents2_D_2
       	= 621;
       	d_2
       	= if (not isInner) then x+8
       	 else d_1;
       	(idEvents2_D, d)
       	= (idEvents2_D_2, d_2);
       tel
       -- Exit action for state :D_Db
       node D_Db_ex(idEvents2_D_1:int;
       	isInner:bool)
       returns (idEvents2_D:int);
       var 	idEvents2_D_2:int;
       let
       	-- set state as inactive
       	idEvents2_D_2
       	 = if (not isInner) then 0 else idEvents2_D_1;
       	(idEvents2_D)
       	= (idEvents2_D_1);
       tel
       -- Entry action for state :Events2_D
       node Events2_D_en(idEvents2_D_1:int;
       	idEvents2_Events2_1:int;
       	d_1:int;
       	x:int;
       	isInner:bool)
       returns (idEvents2_D:int;
       	idEvents2_Events2:int;
       	d:int);
       var 	idEvents2_D_2, idEvents2_D_3, idEvents2_D_4, idEvents2_D_5, idEvents2_D_6:int;
       	idEvents2_Events2_2, idEvents2_Events2_3, idEvents2_Events2_4:int;
       	d_2, d_3, d_4, d_5, d_6:int;
       let
       	-- set state as active
       	idEvents2_Events2_2
       	= 619;
       -- transition trace :
       	--POINT__To__D_Da_1
       		(idEvents2_D_2, d_2)
       	= D_Da_en(idEvents2_D_1, x, d_1, false);
       	(idEvents2_D_3, idEvents2_Events2_3, d_3)
+      	=
       	if ( idEvents2_D_1 = 0) then
       	 (idEvents2_D_2, idEvents2_Events2_2, d_2)
       	 else(idEvents2_D_1, idEvents2_Events2_2, d_1);
       	(idEvents2_D_4, d_4)
+      	=
       	if ( idEvents2_D_1 = 620) then
       	D_Da_en(idEvents2_D_1, x, d_1, false)
       	 else (idEvents2_D_1, d_1);
       	(idEvents2_D_5, d_5)
+      	=
       	if ( idEvents2_D_1 = 621) then
       	D_Db_en(idEvents2_D_1, x, d_1, false)
       	 else (idEvents2_D_1, d_1);
       	(idEvents2_D_6, idEvents2_Events2_4, d_6)
+      	=
       		 if ( idEvents2_D_1 = 0) then
       		(idEvents2_D_3, idEvents2_Events2_3, d_3)
       		 else
       		 if ( idEvents2_D_1 = 620) then
       		(idEvents2_D_4, idEvents2_Events2_3, d_4)
       		 else
       		 if ( idEvents2_D_1 = 621) then
       		(idEvents2_D_5, idEvents2_Events2_3, d_5)
       		 else (idEvents2_D_1, idEvents2_Events2_2, d_1);
       	(idEvents2_D, idEvents2_Events2, d)
       	= (idEvents2_D_6, idEvents2_Events2_4, d_6);
       tel
       -- Exit action for state :Events2_D
       node Events2_D_ex(idEvents2_D_1:int;
       	idEvents2_Events2_1:int;
       	isInner:bool)
       returns (idEvents2_D:int;
       	idEvents2_Events2:int);
       var 	idEvents2_D_2, idEvents2_D_3, idEvents2_D_4, idEvents2_D_5:int;
       	idEvents2_Events2_2:int;
       let
       	(idEvents2_D_2)
+      	=
       	if ( idEvents2_D_1 = 620) then
       	D_Da_ex(idEvents2_D_1, false)
       	 else (idEvents2_D_1);
       	(idEvents2_D_3)
+      	=
       	if ( idEvents2_D_1 = 621) then
       	D_Db_ex(idEvents2_D_1, false)
       	 else (idEvents2_D_1);
       	(idEvents2_D_4)
+      	=
       		 if ( idEvents2_D_1 = 620) then
       		(idEvents2_D_2)
       		 else
       		 if ( idEvents2_D_1 = 621) then
       		(idEvents2_D_3)
       		 else (idEvents2_D_1);
       	-- set state as inactive
       	idEvents2_Events2_2
       	 = if (not isInner) then 0 else idEvents2_Events2_1;
       	idEvents2_D_5
       	= 0;
       	(idEvents2_D, idEvents2_Events2)
       	= (idEvents2_D_5, idEvents2_Events2_1);
       tel
       -- Entry action for state :C_Ca
       node C_Ca_en(idEvents2_C_1:int;
       	x:int;
       	c_1:int;
       	isInner:bool)
       returns (idEvents2_C:int;
       	c:int);
       var 	idEvents2_C_2:int;
       	c_2:int;
       let
       	-- set state as active
       	idEvents2_C_2
       	= 618;
       	c_2
       	= if (not isInner) then x+5
       	 else c_1;
       	(idEvents2_C, c)
       	= (idEvents2_C_2, c_2);
       tel
       -- Exit action for state :C_Ca
       node C_Ca_ex(idEvents2_C_1:int;
       	isInner:bool)
       returns (idEvents2_C:int);
       var 	idEvents2_C_2:int;
       let
       	-- set state as inactive
       	idEvents2_C_2
       	 = if (not isInner) then 0 else idEvents2_C_1;
       	(idEvents2_C)
       	= (idEvents2_C_1);
       tel
       -- Entry action for state :C_Cb
       node C_Cb_en(idEvents2_C_1:int;
       	x:int;
       	c_1:int;
       	isInner:bool)
       returns (idEvents2_C:int;
       	c:int);
       var 	idEvents2_C_2:int;
       	c_2:int;
       let
       	-- set state as active
       	idEvents2_C_2
       	= 611;
       	c_2
       	= if (not isInner) then x+6
       	 else c_1;
       	(idEvents2_C, c)
       	= (idEvents2_C_2, c_2);
       tel
       -- Exit action for state :C_Cb
       node C_Cb_ex(idEvents2_C_1:int;
       	isInner:bool)
       returns (idEvents2_C:int);
       var 	idEvents2_C_2:int;
       let
       	-- set state as inactive
       	idEvents2_C_2
       	 = if (not isInner) then 0 else idEvents2_C_1;
       	(idEvents2_C)
       	= (idEvents2_C_1);
       tel
       -- Entry action for state :Events2_C
       node Events2_C_en(idEvents2_C_1:int;
       	idEvents2_Events2_1:int;
       	c_1:int;
       	x:int;
       	isInner:bool)
       returns (idEvents2_C:int;
       	idEvents2_Events2:int;
       	c:int);
       var 	idEvents2_C_2, idEvents2_C_3, idEvents2_C_4, idEvents2_C_5, idEvents2_C_6:int;
       	idEvents2_Events2_2, idEvents2_Events2_3, idEvents2_Events2_4:int;
       	c_2, c_3, c_4, c_5, c_6:int;
       let
       	-- set state as active
       	idEvents2_Events2_2
       	= 622;
       -- transition trace :
       	--POINT__To__C_Ca_1
       		(idEvents2_C_2, c_2)
       	= C_Ca_en(idEvents2_C_1, x, c_1, false);
       	(idEvents2_C_3, idEvents2_Events2_3, c_3)
+      	=
       	if ( idEvents2_C_1 = 0) then
       	 (idEvents2_C_2, idEvents2_Events2_2, c_2)
       	 else(idEvents2_C_1, idEvents2_Events2_2, c_1);
       	(idEvents2_C_4, c_4)
+      	=
       	if ( idEvents2_C_1 = 618) then
       	C_Ca_en(idEvents2_C_1, x, c_1, false)
       	 else (idEvents2_C_1, c_1);
       	(idEvents2_C_5, c_5)
+      	=
       	if ( idEvents2_C_1 = 611) then
       	C_Cb_en(idEvents2_C_1, x, c_1, false)
       	 else (idEvents2_C_1, c_1);
       	(idEvents2_C_6, idEvents2_Events2_4, c_6)
+      	=
       		 if ( idEvents2_C_1 = 0) then
       		(idEvents2_C_3, idEvents2_Events2_3, c_3)
       		 else
       		 if ( idEvents2_C_1 = 618) then
       		(idEvents2_C_4, idEvents2_Events2_3, c_4)
       		 else
       		 if ( idEvents2_C_1 = 611) then
       		(idEvents2_C_5, idEvents2_Events2_3, c_5)
       		 else (idEvents2_C_1, idEvents2_Events2_2, c_1);
       	(idEvents2_C, idEvents2_Events2, c)
       	= (idEvents2_C_6, idEvents2_Events2_4, c_6);
       tel
       -- Exit action for state :Events2_C
       node Events2_C_ex(idEvents2_C_1:int;
       	idEvents2_Events2_1:int;
       	isInner:bool)
       returns (idEvents2_C:int;
       	idEvents2_Events2:int);
       var 	idEvents2_C_2, idEvents2_C_3, idEvents2_C_4, idEvents2_C_5:int;
       	idEvents2_Events2_2:int;
       let
       	(idEvents2_C_2)
+      	=
       	if ( idEvents2_C_1 = 618) then
       	C_Ca_ex(idEvents2_C_1, false)
       	 else (idEvents2_C_1);
       	(idEvents2_C_3)
+      	=
       	if ( idEvents2_C_1 = 611) then
       	C_Cb_ex(idEvents2_C_1, false)
       	 else (idEvents2_C_1);
       	(idEvents2_C_4)
+      	=
       		 if ( idEvents2_C_1 = 618) then
       		(idEvents2_C_2)
       		 else
       		 if ( idEvents2_C_1 = 611) then
       		(idEvents2_C_3)
       		 else (idEvents2_C_1);
       	-- set state as inactive
       	idEvents2_Events2_2
       	 = if (not isInner) then 0 else idEvents2_Events2_1;
       	idEvents2_C_5
       	= 0;
       	(idEvents2_C, idEvents2_Events2)
       	= (idEvents2_C_5, idEvents2_Events2_1);
       tel
       -- Entry action for state :B_Ba
       node B_Ba_en(idEvents2_B_1:int;
       	x:int;
       	b_1:int;
       	isInner:bool)
       returns (idEvents2_B:int;
       	b:int);
       var 	idEvents2_B_2:int;
       	b_2:int;
       let
       	-- set state as active
       	idEvents2_B_2
       	= 613;
       	b_2
       	= if (not isInner) then x+3
       	 else b_1;
       	(idEvents2_B, b)
       	= (idEvents2_B_2, b_2);
       tel
       -- Exit action for state :B_Ba
       node B_Ba_ex(idEvents2_B_1:int;
       	isInner:bool)
       returns (idEvents2_B:int);
       var 	idEvents2_B_2:int;
       let
       	-- set state as inactive
       	idEvents2_B_2
       	 = if (not isInner) then 0 else idEvents2_B_1;
       	(idEvents2_B)
       	= (idEvents2_B_1);
       tel
       -- Entry action for state :B_Bb
       node B_Bb_en(idEvents2_B_1:int;
       	x:int;
       	b_1:int;
       	isInner:bool)
       returns (idEvents2_B:int;
       	b:int);
       var 	idEvents2_B_2:int;
       	b_2:int;
       let
       	-- set state as active
       	idEvents2_B_2
       	= 614;
       	b_2
       	= if (not isInner) then x+4
       	 else b_1;
       	(idEvents2_B, b)
       	= (idEvents2_B_2, b_2);
       tel
       -- Exit action for state :B_Bb
       node B_Bb_ex(idEvents2_B_1:int;
       	isInner:bool)
       returns (idEvents2_B:int);
       var 	idEvents2_B_2:int;
       let
       	-- set state as inactive
       	idEvents2_B_2
       	 = if (not isInner) then 0 else idEvents2_B_1;
       	(idEvents2_B)
       	= (idEvents2_B_1);
       tel
       -- Entry action for state :Events2_B
       node Events2_B_en(idEvents2_B_1:int;
       	idEvents2_Events2_1:int;
       	b_1:int;
       	x:int;
       	isInner:bool)
       returns (idEvents2_B:int;
       	idEvents2_Events2:int;
       	b:int);
       var 	idEvents2_B_2, idEvents2_B_3, idEvents2_B_4, idEvents2_B_5, idEvents2_B_6:int;
       	idEvents2_Events2_2, idEvents2_Events2_3, idEvents2_Events2_4:int;
       	b_2, b_3, b_4, b_5, b_6:int;
       let
       	-- set state as active
       	idEvents2_Events2_2
       	= 612;
       -- transition trace :
       	--POINT__To__B_Ba_1
       		(idEvents2_B_2, b_2)
       	= B_Ba_en(idEvents2_B_1, x, b_1, false);
       	(idEvents2_B_3, idEvents2_Events2_3, b_3)
+      	=
       	if ( idEvents2_B_1 = 0) then
       	 (idEvents2_B_2, idEvents2_Events2_2, b_2)
       	 else(idEvents2_B_1, idEvents2_Events2_2, b_1);
       	(idEvents2_B_4, b_4)
+      	=
       	if ( idEvents2_B_1 = 613) then
       	B_Ba_en(idEvents2_B_1, x, b_1, false)
       	 else (idEvents2_B_1, b_1);
       	(idEvents2_B_5, b_5)
+      	=
       	if ( idEvents2_B_1 = 614) then
       	B_Bb_en(idEvents2_B_1, x, b_1, false)
       	 else (idEvents2_B_1, b_1);
       	(idEvents2_B_6, idEvents2_Events2_4, b_6)
+      	=
       		 if ( idEvents2_B_1 = 0) then
       		(idEvents2_B_3, idEvents2_Events2_3, b_3)
       		 else
       		 if ( idEvents2_B_1 = 613) then
       		(idEvents2_B_4, idEvents2_Events2_3, b_4)
       		 else
       		 if ( idEvents2_B_1 = 614) then
       		(idEvents2_B_5, idEvents2_Events2_3, b_5)
       		 else (idEvents2_B_1, idEvents2_Events2_2, b_1);
       	(idEvents2_B, idEvents2_Events2, b)
       	= (idEvents2_B_6, idEvents2_Events2_4, b_6);
       tel
       -- Exit action for state :Events2_B
       node Events2_B_ex(idEvents2_B_1:int;
       	idEvents2_Events2_1:int;
       	isInner:bool)
       returns (idEvents2_B:int;
       	idEvents2_Events2:int);
       var 	idEvents2_B_2, idEvents2_B_3, idEvents2_B_4, idEvents2_B_5:int;
       	idEvents2_Events2_2:int;
       let
       	(idEvents2_B_2)
+      	=
       	if ( idEvents2_B_1 = 613) then
       	B_Ba_ex(idEvents2_B_1, false)
       	 else (idEvents2_B_1);
       	(idEvents2_B_3)
+      	=
       	if ( idEvents2_B_1 = 614) then
       	B_Bb_ex(idEvents2_B_1, false)
       	 else (idEvents2_B_1);
       	(idEvents2_B_4)
+      	=
       		 if ( idEvents2_B_1 = 613) then
       		(idEvents2_B_2)
       		 else
       		 if ( idEvents2_B_1 = 614) then
       		(idEvents2_B_3)
       		 else (idEvents2_B_1);
       	-- set state as inactive
       	idEvents2_Events2_2
       	 = if (not isInner) then 0 else idEvents2_Events2_1;
       	idEvents2_B_5
       	= 0;
       	(idEvents2_B, idEvents2_Events2)
       	= (idEvents2_B_5, idEvents2_Events2_1);
       tel
       -- Entry action for state :A_Aa
       node A_Aa_en(idEvents2_A_1:int;
       	x:int;
       	a_1:int;
       	isInner:bool)
       returns (idEvents2_A:int;
       	a:int);
       var 	idEvents2_A_2:int;
       	a_2:int;
       let
       	-- set state as active
       	idEvents2_A_2
       	= 616;
       	a_2
       	= if (not isInner) then x+1
       	 else a_1;
       	(idEvents2_A, a)
       	= (idEvents2_A_2, a_2);
       tel
       -- Exit action for state :A_Aa
       node A_Aa_ex(idEvents2_A_1:int;
       	isInner:bool)
       returns (idEvents2_A:int);
       var 	idEvents2_A_2:int;
       let
       	-- set state as inactive
       	idEvents2_A_2
       	 = if (not isInner) then 0 else idEvents2_A_1;
       	(idEvents2_A)
       	= (idEvents2_A_1);
       tel
       -- Entry action for state :A_Ab
       node A_Ab_en(idEvents2_A_1:int;
       	x:int;
       	a_1:int;
       	isInner:bool)
       returns (idEvents2_A:int;
       	a:int);
       var 	idEvents2_A_2:int;
       	a_2:int;
       let
       	-- set state as active
       	idEvents2_A_2
       	= 617;
       	a_2
       	= if (not isInner) then x+2
       	 else a_1;
       	(idEvents2_A, a)
       	= (idEvents2_A_2, a_2);
       tel
       -- Exit action for state :A_Ab
       node A_Ab_ex(idEvents2_A_1:int;
       	isInner:bool)
       returns (idEvents2_A:int);
       var 	idEvents2_A_2:int;
       let
       	-- set state as inactive
       	idEvents2_A_2
       	 = if (not isInner) then 0 else idEvents2_A_1;
       	(idEvents2_A)
       	= (idEvents2_A_1);
       tel
       -- Entry action for state :Events2_A
       node Events2_A_en(idEvents2_A_1:int;
       	idEvents2_Events2_1:int;
       	a_1:int;
       	x:int;
       	isInner:bool)
       returns (idEvents2_A:int;
       	idEvents2_Events2:int;
       	a:int);
       var 	idEvents2_A_2, idEvents2_A_3, idEvents2_A_4, idEvents2_A_5, idEvents2_A_6:int;
       	idEvents2_Events2_2, idEvents2_Events2_3, idEvents2_Events2_4:int;
       	a_2, a_3, a_4, a_5, a_6:int;
       let
       	-- set state as active
       	idEvents2_Events2_2
       	= 615;
       -- transition trace :
       	--POINT__To__A_Aa_1
       		(idEvents2_A_2, a_2)
       	= A_Aa_en(idEvents2_A_1, x, a_1, false);
       	(idEvents2_A_3, idEvents2_Events2_3, a_3)
+      	=
       	if ( idEvents2_A_1 = 0) then
       	 (idEvents2_A_2, idEvents2_Events2_2, a_2)
       	 else(idEvents2_A_1, idEvents2_Events2_2, a_1);
       	(idEvents2_A_4, a_4)
+      	=
       	if ( idEvents2_A_1 = 616) then
       	A_Aa_en(idEvents2_A_1, x, a_1, false)
       	 else (idEvents2_A_1, a_1);
       	(idEvents2_A_5, a_5)
+      	=
       	if ( idEvents2_A_1 = 617) then
       	A_Ab_en(idEvents2_A_1, x, a_1, false)
       	 else (idEvents2_A_1, a_1);
       	(idEvents2_A_6, idEvents2_Events2_4, a_6)
+      	=
       		 if ( idEvents2_A_1 = 0) then
       		(idEvents2_A_3, idEvents2_Events2_3, a_3)
       		 else
       		 if ( idEvents2_A_1 = 616) then
       		(idEvents2_A_4, idEvents2_Events2_3, a_4)
       		 else
       		 if ( idEvents2_A_1 = 617) then
       		(idEvents2_A_5, idEvents2_Events2_3, a_5)
       		 else (idEvents2_A_1, idEvents2_Events2_2, a_1);
       	(idEvents2_A, idEvents2_Events2, a)
       	= (idEvents2_A_6, idEvents2_Events2_4, a_6);
       tel
       -- Exit action for state :Events2_A
       node Events2_A_ex(idEvents2_A_1:int;
       	idEvents2_Events2_1:int;
       	isInner:bool)
       returns (idEvents2_A:int;
       	idEvents2_Events2:int);
       var 	idEvents2_A_2, idEvents2_A_3, idEvents2_A_4, idEvents2_A_5:int;
       	idEvents2_Events2_2:int;
       let
       	(idEvents2_A_2)
+      	=
       	if ( idEvents2_A_1 = 616) then
       	A_Aa_ex(idEvents2_A_1, false)
       	 else (idEvents2_A_1);
       	(idEvents2_A_3)
+      	=
       	if ( idEvents2_A_1 = 617) then
       	A_Ab_ex(idEvents2_A_1, false)
       	 else (idEvents2_A_1);
       	(idEvents2_A_4)
+      	=
       		 if ( idEvents2_A_1 = 616) then
       		(idEvents2_A_2)
       		 else
       		 if ( idEvents2_A_1 = 617) then
       		(idEvents2_A_3)
       		 else (idEvents2_A_1);
       	-- set state as inactive
       	idEvents2_Events2_2
       	 = if (not isInner) then 0 else idEvents2_Events2_1;
       	idEvents2_A_5
       	= 0;
       	(idEvents2_A, idEvents2_Events2)
       	= (idEvents2_A_5, idEvents2_Events2_1);
       tel
       --***************************************************State :Events2_D Automaton***************************************************
       node Events2_D_node(idEvents2_D_1:int;
       	d_1:int;
       	x:int;
       	S3:bool;
       	R3:bool)
       returns (idEvents2_D:int;
       	d:int);
       let
       	 automaton events2_d
       	state POINTEvents2_D:
       	unless (idEvents2_D_1=0) restart POINT__TO__D_DA_1
       	unless (idEvents2_D_1=620) and S3 restart D_DA__TO__D_DB_1
       	unless (idEvents2_D_1=621) and R3 restart D_DB__TO__D_DA_1
       	unless (idEvents2_D_1=620) restart D_DA_IDL
       	unless (idEvents2_D_1=621) restart D_DB_IDL
       	let
       		(idEvents2_D, d)
       	= (idEvents2_D_1, d_1);
       	tel
       	state POINT__TO__D_DA_1:
       	 var 	idEvents2_D_2:int;
       	d_2:int;
       	let
       		-- transition trace :
       	--POINT__To__D_Da_1
       		(idEvents2_D_2, d_2)
       	= D_Da_en(idEvents2_D_1, x, d_1, false);
       	(idEvents2_D, d)
       	=  (idEvents2_D_2, d_2);
       	tel
       	until true restart POINTEvents2_D
       	state D_DA__TO__D_DB_1:
       	 var 	idEvents2_D_2, idEvents2_D_3:int;
       	d_2:int;
       	let
       		-- transition trace :
       	--D_Da__To__D_Db_1
       		(idEvents2_D_2)
       	= D_Da_ex(idEvents2_D_1, false);
       		(idEvents2_D_3, d_2)
       	= D_Db_en(idEvents2_D_2, x, d_1, false);
       	(idEvents2_D, d)
       	=  (idEvents2_D_3, d_2);
       	tel
       	until true restart POINTEvents2_D
       	state D_DB__TO__D_DA_1:
       	 var 	idEvents2_D_2, idEvents2_D_3:int;
       	d_2:int;
       	let
       		-- transition trace :
       	--D_Db__To__D_Da_1
       		(idEvents2_D_2)
       	= D_Db_ex(idEvents2_D_1, false);
       		(idEvents2_D_3, d_2)
       	= D_Da_en(idEvents2_D_2, x, d_1, false);
       	(idEvents2_D, d)
       	=  (idEvents2_D_3, d_2);
       	tel
       	until true restart POINTEvents2_D
       	state D_DA_IDL:
       	 	let
       	(idEvents2_D, d)
       	= (idEvents2_D_1, d_1);
       	tel
       	until true restart POINTEvents2_D
       	state D_DB_IDL:
       	 	let
       	(idEvents2_D, d)
       	= (idEvents2_D_1, d_1);
       	tel
       	until true restart POINTEvents2_D
       tel
       node C_Cb__To__C_Ca_1_Transition_Action(idEvents2_D_1:int;
       	d_1:int;
       	x:int;
       	S3:bool;
       	R3:bool)
       returns (idEvents2_D:int;
       	d:int);
       var 	idEvents2_D_2:int;
       	d_2:int;
       let
       	(idEvents2_D_2, d_2)
       	= Events2_D_node(idEvents2_D_1, d_1, x, S3, true);
       	(idEvents2_D, d)
       	= (idEvents2_D_2, d_2);
       tel
       node C_Ca__To__C_Cb_1_Transition_Action(idEvents2_D_1:int;
       	d_1:int;
       	x:int;
       	S3:bool;
       	R3:bool)
       returns (idEvents2_D:int;
       	d:int);
       var 	idEvents2_D_2:int;
       	d_2:int;
       let
       	(idEvents2_D_2, d_2)
       	= Events2_D_node(idEvents2_D_1, d_1, x, true, R3);
       	(idEvents2_D, d)
       	= (idEvents2_D_2, d_2);
       tel
       --***************************************************State :Events2_C Automaton***************************************************
       node Events2_C_node(idEvents2_C_1:int;
       	c_1:int;
       	x:int;
       	S2:bool;
       	R3:bool;
       	S3:bool;
       	d_1:int;
       	idEvents2_D_1:int;
       	R2:bool)
       returns (idEvents2_C:int;
       	c:int;
       	d:int;
       	idEvents2_D:int);
       let
       	 automaton events2_c
       	state POINTEvents2_C:
       	unless (idEvents2_C_1=0) restart POINT__TO__C_CA_1
       	unless (idEvents2_C_1=618) and S2 restart C_CA__TO__C_CB_1
       	unless (idEvents2_C_1=611) and R2 restart C_CB__TO__C_CA_1
       	unless (idEvents2_C_1=618) restart C_CA_IDL
       	unless (idEvents2_C_1=611) restart C_CB_IDL
       	let
       		(idEvents2_C, c, d, idEvents2_D)
       	= (idEvents2_C_1, c_1, d_1, idEvents2_D_1);
       	tel
       	state POINT__TO__C_CA_1:
       	 var 	idEvents2_C_2:int;
       	c_2:int;
       	let
       		-- transition trace :
       	--POINT__To__C_Ca_1
       		(idEvents2_C_2, c_2)
       	= C_Ca_en(idEvents2_C_1, x, c_1, false);
       	(idEvents2_C, c)
       	=  (idEvents2_C_2, c_2);
       	--add unused variables
       	(d, idEvents2_D)
       	= (d_1, idEvents2_D_1);
       	tel
       	until true restart POINTEvents2_C
       	state C_CA__TO__C_CB_1:
       	 var 	idEvents2_C_2, idEvents2_C_3:int;
       	c_2:int;
       	d_2:int;
       	idEvents2_D_2:int;
       	let
       		-- transition trace :
       	--C_Ca__To__C_Cb_1
       		(idEvents2_C_2)
       	= C_Ca_ex(idEvents2_C_1, false);
       		(idEvents2_D_2, d_2)
       	= C_Ca__To__C_Cb_1_Transition_Action(idEvents2_D_1, d_1, x, S3, R3);
       		(idEvents2_C_3, c_2)
       	= C_Cb_en(idEvents2_C_2, x, c_1, false);
       	(idEvents2_C, c, d, idEvents2_D)
       	=  (idEvents2_C_3, c_2, d_2, idEvents2_D_2);
       	tel
       	until true restart POINTEvents2_C
       	state C_CB__TO__C_CA_1:
       	 var 	idEvents2_C_2, idEvents2_C_3:int;
       	c_2:int;
       	d_2:int;
       	idEvents2_D_2:int;
       	let
       		-- transition trace :
       	--C_Cb__To__C_Ca_1
       		(idEvents2_C_2)
       	= C_Cb_ex(idEvents2_C_1, false);
       		(idEvents2_D_2, d_2)
       	= C_Cb__To__C_Ca_1_Transition_Action(idEvents2_D_1, d_1, x, S3, R3);
       		(idEvents2_C_3, c_2)
       	= C_Ca_en(idEvents2_C_2, x, c_1, false);
       	(idEvents2_C, c, d, idEvents2_D)
       	=  (idEvents2_C_3, c_2, d_2, idEvents2_D_2);
       	tel
       	until true restart POINTEvents2_C
       	state C_CA_IDL:
       	 	let
       	(idEvents2_C, c, d, idEvents2_D)
       	= (idEvents2_C_1, c_1, d_1, idEvents2_D_1);
       	tel
       	until true restart POINTEvents2_C
       	state C_CB_IDL:
       	 	let
       	(idEvents2_C, c, d, idEvents2_D)
       	= (idEvents2_C_1, c_1, d_1, idEvents2_D_1);
       	tel
       	until true restart POINTEvents2_C
       tel
       node B_Bb__To__B_Ba_1_Transition_Action(idEvents2_C_1:int;
       	c_1:int;
       	x:int;
       	S2:bool;
       	R3:bool;
       	S3:bool;
       	d_1:int;
       	idEvents2_D_1:int;
       	R2:bool)
       returns (idEvents2_C:int;
       	c:int;
       	d:int;
       	idEvents2_D:int);
       var 	idEvents2_C_2:int;
       	c_2:int;
       	d_2:int;
       	idEvents2_D_2:int;
       let
       	(idEvents2_C_2, c_2, d_2, idEvents2_D_2)
       	= Events2_C_node(idEvents2_C_1, c_1, x, S2, R3, S3, d_1, idEvents2_D_1, true);
       	(idEvents2_C, c, d, idEvents2_D)
       	= (idEvents2_C_2, c_2, d_2, idEvents2_D_2);
       tel
       node B_Ba__To__B_Bb_1_Transition_Action(idEvents2_C_1:int;
       	c_1:int;
       	x:int;
       	S2:bool;
       	R3:bool;
       	S3:bool;
       	d_1:int;
       	idEvents2_D_1:int;
       	R2:bool)
       returns (idEvents2_C:int;
       	c:int;
       	d:int;
       	idEvents2_D:int);
       var 	idEvents2_C_2:int;
       	c_2:int;
       	d_2:int;
       	idEvents2_D_2:int;
       let
       	(idEvents2_C_2, c_2, d_2, idEvents2_D_2)
       	= Events2_C_node(idEvents2_C_1, c_1, x, true, R3, S3, d_1, idEvents2_D_1, R2);
       	(idEvents2_C, c, d, idEvents2_D)
       	= (idEvents2_C_2, c_2, d_2, idEvents2_D_2);
       tel
       --***************************************************State :Events2_B Automaton***************************************************
       node Events2_B_node(idEvents2_B_1:int;
       	b_1:int;
       	x:int;
       	S1:bool;
       	R2:bool;
       	R3:bool;
       	S2:bool;
       	S3:bool;
       	c_1:int;
       	d_1:int;
       	idEvents2_C_1:int;
       	idEvents2_D_1:int;
       	R1:bool)
       returns (idEvents2_B:int;
       	b:int;
       	c:int;
       	d:int;
       	idEvents2_C:int;
       	idEvents2_D:int);
       let
       	 automaton events2_b
       	state POINTEvents2_B:
       	unless (idEvents2_B_1=0) restart POINT__TO__B_BA_1
       	unless (idEvents2_B_1=613) and S1 restart B_BA__TO__B_BB_1
       	unless (idEvents2_B_1=614) and R1 restart B_BB__TO__B_BA_1
       	unless (idEvents2_B_1=613) restart B_BA_IDL
       	unless (idEvents2_B_1=614) restart B_BB_IDL
       	let
       		(idEvents2_B, b, c, d, idEvents2_C, idEvents2_D)
       	= (idEvents2_B_1, b_1, c_1, d_1, idEvents2_C_1, idEvents2_D_1);
       	tel
       	state POINT__TO__B_BA_1:
       	 var 	idEvents2_B_2:int;
       	b_2:int;
       	let
       		-- transition trace :
       	--POINT__To__B_Ba_1
       		(idEvents2_B_2, b_2)
       	= B_Ba_en(idEvents2_B_1, x, b_1, false);
       	(idEvents2_B, b)
       	=  (idEvents2_B_2, b_2);
       	--add unused variables
       	(c, d, idEvents2_C, idEvents2_D)
       	= (c_1, d_1, idEvents2_C_1, idEvents2_D_1);
       	tel
       	until true restart POINTEvents2_B
       	state B_BA__TO__B_BB_1:
       	 var 	idEvents2_B_2, idEvents2_B_3:int;
       	b_2:int;
       	c_2:int;
       	d_2:int;
       	idEvents2_C_2:int;
       	idEvents2_D_2:int;
       	let
       		-- transition trace :
       	--B_Ba__To__B_Bb_1
       		(idEvents2_B_2)
       	= B_Ba_ex(idEvents2_B_1, false);
       		(idEvents2_C_2, c_2, d_2, idEvents2_D_2)
       	= B_Ba__To__B_Bb_1_Transition_Action(idEvents2_C_1, c_1, x, S2, R3, S3, d_1, idEvents2_D_1, R2);
       		(idEvents2_B_3, b_2)
       	= B_Bb_en(idEvents2_B_2, x, b_1, false);
       	(idEvents2_B, b, c, d, idEvents2_C, idEvents2_D)
       	=  (idEvents2_B_3, b_2, c_2, d_2, idEvents2_C_2, idEvents2_D_2);
       	tel
       	until true restart POINTEvents2_B
       	state B_BB__TO__B_BA_1:
       	 var 	idEvents2_B_2, idEvents2_B_3:int;
       	b_2:int;
       	c_2:int;
       	d_2:int;
       	idEvents2_C_2:int;
       	idEvents2_D_2:int;
       	let
       		-- transition trace :
       	--B_Bb__To__B_Ba_1
       		(idEvents2_B_2)
       	= B_Bb_ex(idEvents2_B_1, false);
       		(idEvents2_C_2, c_2, d_2, idEvents2_D_2)
       	= B_Bb__To__B_Ba_1_Transition_Action(idEvents2_C_1, c_1, x, S2, R3, S3, d_1, idEvents2_D_1, R2);
       		(idEvents2_B_3, b_2)
       	= B_Ba_en(idEvents2_B_2, x, b_1, false);
       	(idEvents2_B, b, c, d, idEvents2_C, idEvents2_D)
       	=  (idEvents2_B_3, b_2, c_2, d_2, idEvents2_C_2, idEvents2_D_2);
       	tel
       	until true restart POINTEvents2_B
       	state B_BA_IDL:
       	 	let
       	(idEvents2_B, b, c, d, idEvents2_C, idEvents2_D)
       	= (idEvents2_B_1, b_1, c_1, d_1, idEvents2_C_1, idEvents2_D_1);
       	tel
       	until true restart POINTEvents2_B
       	state B_BB_IDL:
       	 	let
       	(idEvents2_B, b, c, d, idEvents2_C, idEvents2_D)
       	= (idEvents2_B_1, b_1, c_1, d_1, idEvents2_C_1, idEvents2_D_1);
       	tel
       	until true restart POINTEvents2_B
       tel
       node A_Aa__To__A_Ab_1_Transition_Action(idEvents2_B_1:int;
       	b_1:int;
       	x:int;
       	S1:bool;
       	R2:bool;
       	R3:bool;
       	S2:bool;
       	S3:bool;
       	c_1:int;
       	d_1:int;
       	idEvents2_C_1:int;
       	idEvents2_D_1:int;
       	R1:bool)
       returns (idEvents2_B:int;
       	b:int;
       	c:int;
       	d:int;
       	idEvents2_C:int;
       	idEvents2_D:int);
       var 	idEvents2_B_2:int;
       	b_2:int;
       	c_2:int;
       	d_2:int;
       	idEvents2_C_2:int;
       	idEvents2_D_2:int;
       let
       	(idEvents2_B_2, b_2, c_2, d_2, idEvents2_C_2, idEvents2_D_2)
       	= Events2_B_node(idEvents2_B_1, b_1, x, true, R2, R3, S2, S3, c_1, d_1, idEvents2_C_1, idEvents2_D_1, R1);
       	(idEvents2_B, b, c, d, idEvents2_C, idEvents2_D)
       	= (idEvents2_B_2, b_2, c_2, d_2, idEvents2_C_2, idEvents2_D_2);
       tel
       node A_Ab__To__A_Aa_1_Transition_Action(idEvents2_B_1:int;
       	b_1:int;
       	x:int;
       	S1:bool;
       	R2:bool;
       	R3:bool;
       	S2:bool;
       	S3:bool;
       	c_1:int;
       	d_1:int;
       	idEvents2_C_1:int;
       	idEvents2_D_1:int;
       	R1:bool)
       returns (idEvents2_B:int;
       	b:int;
       	c:int;
       	d:int;
       	idEvents2_C:int;
       	idEvents2_D:int);
       var 	idEvents2_B_2:int;
       	b_2:int;
       	c_2:int;
       	d_2:int;
       	idEvents2_C_2:int;
       	idEvents2_D_2:int;
       let
       	(idEvents2_B_2, b_2, c_2, d_2, idEvents2_C_2, idEvents2_D_2)
       	= Events2_B_node(idEvents2_B_1, b_1, x, S1, R2, R3, S2, S3, c_1, d_1, idEvents2_C_1, idEvents2_D_1, true);
       	(idEvents2_B, b, c, d, idEvents2_C, idEvents2_D)
       	= (idEvents2_B_2, b_2, c_2, d_2, idEvents2_C_2, idEvents2_D_2);
       tel
       --***************************************************State :Events2_A Automaton***************************************************
       node Events2_A_node(idEvents2_A_1:int;
       	a_1:int;
       	x:int;
       	S:bool;
       	R1:bool;
       	R2:bool;
       	R3:bool;
       	S1:bool;
       	S2:bool;
       	S3:bool;
       	b_1:int;
       	c_1:int;
       	d_1:int;
       	idEvents2_B_1:int;
       	idEvents2_C_1:int;
       	idEvents2_D_1:int;
       	R:bool)
       returns (idEvents2_A:int;
       	a:int;
       	b:int;
       	c:int;
       	d:int;
       	idEvents2_B:int;
       	idEvents2_C:int;
       	idEvents2_D:int);
       let
       	 automaton events2_a
       	state POINTEvents2_A:
       	unless (idEvents2_A_1=0) restart POINT__TO__A_AA_1
       	unless (idEvents2_A_1=616) and S restart A_AA__TO__A_AB_1
       	unless (idEvents2_A_1=617) and R restart A_AB__TO__A_AA_1
       	unless (idEvents2_A_1=616) restart A_AA_IDL
       	unless (idEvents2_A_1=617) restart A_AB_IDL
       	let
       		(idEvents2_A, a, b, c, d, idEvents2_B, idEvents2_C, idEvents2_D)
       	= (idEvents2_A_1, a_1, b_1, c_1, d_1, idEvents2_B_1, idEvents2_C_1, idEvents2_D_1);
       	tel
       	state POINT__TO__A_AA_1:
       	 var 	idEvents2_A_2:int;
       	a_2:int;
       	let
       		-- transition trace :
       	--POINT__To__A_Aa_1
       		(idEvents2_A_2, a_2)
       	= A_Aa_en(idEvents2_A_1, x, a_1, false);
       	(idEvents2_A, a)
       	=  (idEvents2_A_2, a_2);
       	--add unused variables
       	(b, c, d, idEvents2_B, idEvents2_C, idEvents2_D)
       	= (b_1, c_1, d_1, idEvents2_B_1, idEvents2_C_1, idEvents2_D_1);
       	tel
       	until true restart POINTEvents2_A
       	state A_AA__TO__A_AB_1:
       	 var 	idEvents2_A_2, idEvents2_A_3:int;
       	a_2:int;
       	b_2:int;
       	c_2:int;
       	d_2:int;
       	idEvents2_B_2:int;
       	idEvents2_C_2:int;
       	idEvents2_D_2:int;
       	let
       		-- transition trace :
       	--A_Aa__To__A_Ab_1
       		(idEvents2_A_2)
       	= A_Aa_ex(idEvents2_A_1, false);
       		(idEvents2_B_2, b_2, c_2, d_2, idEvents2_C_2, idEvents2_D_2)
       	= A_Aa__To__A_Ab_1_Transition_Action(idEvents2_B_1, b_1, x, S1, R2, R3, S2, S3, c_1, d_1, idEvents2_C_1, idEvents2_D_1, R1);
       		(idEvents2_A_3, a_2)
       	= A_Ab_en(idEvents2_A_2, x, a_1, false);
       	(idEvents2_A, a, b, c, d, idEvents2_B, idEvents2_C, idEvents2_D)
       	=  (idEvents2_A_3, a_2, b_2, c_2, d_2, idEvents2_B_2, idEvents2_C_2, idEvents2_D_2);
       	tel
       	until true restart POINTEvents2_A
       	state A_AB__TO__A_AA_1:
       	 var 	idEvents2_A_2, idEvents2_A_3:int;
       	a_2:int;
       	b_2:int;
       	c_2:int;
       	d_2:int;
       	idEvents2_B_2:int;
       	idEvents2_C_2:int;
       	idEvents2_D_2:int;
       	let
       		-- transition trace :
       	--A_Ab__To__A_Aa_1
       		(idEvents2_A_2)
       	= A_Ab_ex(idEvents2_A_1, false);
       		(idEvents2_B_2, b_2, c_2, d_2, idEvents2_C_2, idEvents2_D_2)
       	= A_Ab__To__A_Aa_1_Transition_Action(idEvents2_B_1, b_1, x, S1, R2, R3, S2, S3, c_1, d_1, idEvents2_C_1, idEvents2_D_1, R1);
       		(idEvents2_A_3, a_2)
       	= A_Aa_en(idEvents2_A_2, x, a_1, false);
       	(idEvents2_A, a, b, c, d, idEvents2_B, idEvents2_C, idEvents2_D)
       	=  (idEvents2_A_3, a_2, b_2, c_2, d_2, idEvents2_B_2, idEvents2_C_2, idEvents2_D_2);
       	tel
       	until true restart POINTEvents2_A
       	state A_AA_IDL:
       	 	let
       	(idEvents2_A, a, b, c, d, idEvents2_B, idEvents2_C, idEvents2_D)
       	= (idEvents2_A_1, a_1, b_1, c_1, d_1, idEvents2_B_1, idEvents2_C_1, idEvents2_D_1);
       	tel
       	until true restart POINTEvents2_A
       	state A_AB_IDL:
       	 	let
       	(idEvents2_A, a, b, c, d, idEvents2_B, idEvents2_C, idEvents2_D)
       	= (idEvents2_A_1, a_1, b_1, c_1, d_1, idEvents2_B_1, idEvents2_C_1, idEvents2_D_1);
       	tel
       	until true restart POINTEvents2_A
       tel
       --***************************************************State :Events2_Events2 Automaton***************************************************
       node Events2_Events2_node(idEvents2_Events2_1:int;
       	a_1:int;
       	idEvents2_A_1:int;
       	x:int;
       	b_1:int;
       	idEvents2_B_1:int;
       	c_1:int;
       	idEvents2_C_1:int;
       	d_1:int;
       	idEvents2_D_1:int;
       	R:bool;
       	R1:bool;
       	R2:bool;
       	R3:bool;
       	S:bool;
       	S1:bool;
       	S2:bool;
       	S3:bool)
       returns (idEvents2_Events2:int;
       	a:int;
       	idEvents2_A:int;
       	b:int;
       	idEvents2_B:int;
       	c:int;
       	idEvents2_C:int;
       	d:int;
       	idEvents2_D:int);
       let
       	 automaton events2_events2
       	state POINTEvents2_Events2:
       	unless (idEvents2_Events2_1=0) restart EVENTS2_EVENTS2_PARALLEL_ENTRY
       	unless true  restart EVENTS2_EVENTS2_PARALLEL_IDL
       	let
       		(idEvents2_Events2, a, idEvents2_A, b, idEvents2_B, c, idEvents2_C, d, idEvents2_D)
       	= (idEvents2_Events2_1, a_1, idEvents2_A_1, b_1, idEvents2_B_1, c_1, idEvents2_C_1, d_1, idEvents2_D_1);
       	tel
       	state EVENTS2_EVENTS2_PARALLEL_ENTRY:
       	 var 	idEvents2_Events2_2, idEvents2_Events2_3, idEvents2_Events2_4, idEvents2_Events2_5:int;
       	a_2:int;
       	idEvents2_A_2:int;
       	b_2:int;
       	idEvents2_B_2:int;
       	c_2:int;
       	idEvents2_C_2:int;
       	d_2:int;
       	idEvents2_D_2:int;
       	let
       	(idEvents2_A_2, idEvents2_Events2_2, a_2)
       	= Events2_A_en(idEvents2_A_1, idEvents2_Events2_1, a_1, x, false);
       	(idEvents2_B_2, idEvents2_Events2_3, b_2)
       	= Events2_B_en(idEvents2_B_1, idEvents2_Events2_2, b_1, x, false);
       	(idEvents2_C_2, idEvents2_Events2_4, c_2)
       	= Events2_C_en(idEvents2_C_1, idEvents2_Events2_3, c_1, x, false);
       	(idEvents2_D_2, idEvents2_Events2_5, d_2)
       	= Events2_D_en(idEvents2_D_1, idEvents2_Events2_4, d_1, x, false);
       	(idEvents2_Events2, a, idEvents2_A, b, idEvents2_B, c, idEvents2_C, d, idEvents2_D)
       	= (idEvents2_Events2_5, a_2, idEvents2_A_2, b_2, idEvents2_B_2, c_2, idEvents2_C_2, d_2, idEvents2_D_2);
       	tel
       	until true restart POINTEvents2_Events2
       	state EVENTS2_EVENTS2_PARALLEL_IDL:
       	 var 	a_2:int;
       	idEvents2_A_2:int;
       	b_2, b_3:int;
       	idEvents2_B_2, idEvents2_B_3:int;
       	c_2, c_3, c_4:int;
       	idEvents2_C_2, idEvents2_C_3, idEvents2_C_4:int;
       	d_2, d_3, d_4, d_5:int;
       	idEvents2_D_2, idEvents2_D_3, idEvents2_D_4, idEvents2_D_5:int;
       	let
       		(idEvents2_A_2, a_2, b_2, c_2, d_2, idEvents2_B_2, idEvents2_C_2, idEvents2_D_2)
       	= if not (idEvents2_A_1= 0 ) then Events2_A_node(idEvents2_A_1, a_1, x, S, R1, R2, R3, S1, S2, S3, b_1, c_1, d_1, idEvents2_B_1, idEvents2_C_1, idEvents2_D_1, R)
       		 else (idEvents2_A_1, a_1, b_1, c_1, d_1, idEvents2_B_1, idEvents2_C_1, idEvents2_D_1);
       		(idEvents2_B_3, b_3, c_3, d_3, idEvents2_C_3, idEvents2_D_3)
       	= if not (idEvents2_B_2= 0 ) then Events2_B_node(idEvents2_B_2, b_2, x, S1, R2, R3, S2, S3, c_2, d_2, idEvents2_C_2, idEvents2_D_2, R1)
       		 else (idEvents2_B_2, b_2, c_2, d_2, idEvents2_C_2, idEvents2_D_2);
       		(idEvents2_C_4, c_4, d_4, idEvents2_D_4)
       	= if not (idEvents2_C_3= 0 ) then Events2_C_node(idEvents2_C_3, c_3, x, S2, R3, S3, d_3, idEvents2_D_3, R2)
       		 else (idEvents2_C_3, c_3, d_3, idEvents2_D_3);
       		(idEvents2_D_5, d_5)
       	= if not (idEvents2_D_4= 0 ) then Events2_D_node(idEvents2_D_4, d_4, x, S3, R3)
       		 else (idEvents2_D_4, d_4);
       	(idEvents2_Events2, a, idEvents2_A, b, idEvents2_B, c, idEvents2_C, d, idEvents2_D)
       	= (idEvents2_Events2_1, a_2, idEvents2_A_2, b_3, idEvents2_B_3, c_4, idEvents2_C_4, d_5, idEvents2_D_5);
       	tel
       	until true restart POINTEvents2_Events2
       tel
       --***************************************************State :Events2_Events2 Automaton***************************************************
       node Events2_Events2(x:int;
       	R:bool;
       	S:bool)
       returns (a:int;
       	b:int;
       	c:int;
       	d:int);
       var a_1: int;
       	b_1: int;
       	c_1: int;
       	d_1: int;
       	R1, R1_1: bool;
       	R2, R2_1: bool;
       	R3, R3_1: bool;
       	S1, S1_1: bool;
       	S2, S2_1: bool;
       	S3, S3_1: bool;
       	idEvents2_Events2, idEvents2_Events2_1: int;
       	idEvents2_D, idEvents2_D_1: int;
       	idEvents2_C, idEvents2_C_1: int;
       	idEvents2_B, idEvents2_B_1: int;
       	idEvents2_A, idEvents2_A_1: int;
       		idEvents2_Events2_2:int;
       	a_2:int;
       	idEvents2_A_2:int;
       	b_2:int;
       	idEvents2_B_2:int;
       	c_2:int;
       	idEvents2_C_2:int;
       	d_2:int;
       	idEvents2_D_2:int;
       let
       	a_1 = 0 -> pre a;
       	b_1 = 0 -> pre b;
       	c_1 = 0 -> pre c;
       	d_1 = 0 -> pre d;
       	R1_1 = false -> pre R1;
       	R2_1 = false -> pre R2;
       	R3_1 = false -> pre R3;
       	S1_1 = false -> pre S1;
       	S2_1 = false -> pre S2;
       	S3_1 = false -> pre S3;
       	idEvents2_Events2_1 = 0 -> pre idEvents2_Events2;
       	idEvents2_D_1 = 0 -> pre idEvents2_D;
       	idEvents2_C_1 = 0 -> pre idEvents2_C;
       	idEvents2_B_1 = 0 -> pre idEvents2_B;
       	idEvents2_A_1 = 0 -> pre idEvents2_A;
       	(idEvents2_Events2_2, a_2, idEvents2_A_2, b_2, idEvents2_B_2, c_2, idEvents2_C_2, d_2, idEvents2_D_2)
+      	 =
       	 if R then Events2_Events2_node(idEvents2_Events2_1, a_1, idEvents2_A_1, x, b_1, idEvents2_B_1, c_1, idEvents2_C_1, d_1, idEvents2_D_1, R, R1, R2, R3, false, S1, S2, S3)
       	 else (idEvents2_Events2_1, a_1, idEvents2_A_1, b_1, idEvents2_B_1, c_1, idEvents2_C_1, d_1, idEvents2_D_1);
       	(idEvents2_Events2, a, idEvents2_A, b, idEvents2_B, c, idEvents2_C, d, idEvents2_D)
+      	 =
       	 if S then Events2_Events2_node(idEvents2_Events2_2, a_2, idEvents2_A_2, x, b_2, idEvents2_B_2, c_2, idEvents2_C_2, d_2, idEvents2_D_2, false, R1, R2, R3, S, S1, S2, S3)
       	 else (idEvents2_Events2_2, a_2, idEvents2_A_2, b_2, idEvents2_B_2, c_2, idEvents2_C_2, d_2, idEvents2_D_2);
       --unused outputs
       	R1 = false;
       	R2 = false;
       	R3 = false;
       	S1 = false;
       	S2 = false;
       	S3 = false;
       tel
       node Events2 (x_1_1 : int; R_1_1 : real; S_1_1 : real)
       returns (a_1_1 : int;
       	b_2_1 : int;
       	c_3_1 : int;
       	d_4_1 : int);
       var
       	Events2_1_1 : int; Events2_2_1 : int; Events2_3_1 : int; Events2_4_1 : int;
       	Mux_1_1 : real; Mux_1_2 : real;
       	i_virtual_local : real;
       	Events2Mux_1_1_event: bool;
       	Events2Mux_1_2_event: bool;
       let
       	Events2Mux_1_1_event = false -> ((pre(Mux_1_1) > 0.0 and Mux_1_1 <= 0.0) or (pre(Mux_1_1) <= 0.0 and Mux_1_1 > 0.0));
       	Events2Mux_1_2_event = false -> ((pre(Mux_1_2) > 0.0 and Mux_1_2 <= 0.0) or (pre(Mux_1_2) <= 0.0 and Mux_1_2 > 0.0));
       	(Events2_1_1, Events2_2_1, Events2_3_1, Events2_4_1) =  Events2_Events2(x_1_1, Events2Mux_1_1_event, Events2Mux_1_2_event);
       	Mux_1_1 = R_1_1 ;
       	Mux_1_2 = S_1_1 ;
       	a_1_1 = Events2_1_1;
       	b_2_1 = Events2_2_1;
       	c_3_1 = Events2_3_1;
       	d_4_1 = Events2_4_1;
       	i_virtual_local= 0.0 -> 1.0;
       tel

« Previous
1
2
3
4
Next »

(1-1/4)

Project

General

Profile

CristalCaveGem » LustreC » Lustrec-Tests