/regression_tests/lustre_files/success/Stateflow/src_EventsOrder/EventsOrder.lus - Lustrec-Tests

lustrec-tests/regression_tests/lustre_files/success/Stateflow/src_EventsOrder/EventsOrder.lus @ 79ef5fc5

       -- This file has been generated by cocoSim
       -- System nodes
       -- Entry action for state :A2_A2a
       node A2_A2a_en(idA_A2_1:int;
       	a_1:int;
       	isInner:bool)
       returns (idA_A2:int;
       	a:int);
       var 	idA_A2_2:int;
       	a_2:int;
       let
       	-- set state as active
       	idA_A2_2
       	= 696;
       	a_2
       	= if (not isInner) then  a_1 +3
       	 else a_1;
       	(idA_A2, a)
       	= (idA_A2_2, a_2);
       tel
       -- Exit action for state :A2_A2a
       node A2_A2a_ex(idA_A2_1:int;
       	isInner:bool)
       returns (idA_A2:int);
       var 	idA_A2_2:int;
       let
       	-- set state as inactive
       	idA_A2_2
       	 = if (not isInner) then 0 else idA_A2_1;
       	(idA_A2)
       	= (idA_A2_1);
       tel
       -- Entry action for state :A2_A2b
       node A2_A2b_en(idA_A2_1:int;
       	a_1:int;
       	isInner:bool)
       returns (idA_A2:int;
       	a:int);
       var 	idA_A2_2:int;
       	a_2:int;
       let
       	-- set state as active
       	idA_A2_2
       	= 697;
       	a_2
       	= if (not isInner) then  a_1 +4
       	 else a_1;
       	(idA_A2, a)
       	= (idA_A2_2, a_2);
       tel
       -- Exit action for state :A2_A2b
       node A2_A2b_ex(idA_A2_1:int;
       	isInner:bool)
       returns (idA_A2:int);
       var 	idA_A2_2:int;
       let
       	-- set state as inactive
       	idA_A2_2
       	 = if (not isInner) then 0 else idA_A2_1;
       	(idA_A2)
       	= (idA_A2_1);
       tel
       -- Entry action for state :A_A2
       node A_A2_en(idA_A2_1:int;
       	idEvents1_A_1:int;
       	a_1:int;
       	isInner:bool)
       returns (idA_A2:int;
       	idEvents1_A:int;
       	a:int);
       var 	idA_A2_2, idA_A2_3, idA_A2_4, idA_A2_5, idA_A2_6:int;
       	idEvents1_A_2, idEvents1_A_3, idEvents1_A_4:int;
       	a_2, a_3, a_4, a_5, a_6:int;
       let
       	-- set state as active
       	idEvents1_A_2
       	= 695;
       -- transition trace :
       	--POINT__To__A2_A2a_1
       		(idA_A2_2, a_2)
       	= A2_A2a_en(idA_A2_1, a_1, false);
       	(idA_A2_3, idEvents1_A_3, a_3)
+      	=
       	if ( idA_A2_1 = 0) then
       	 (idA_A2_2, idEvents1_A_2, a_2)
       	 else(idA_A2_1, idEvents1_A_2, a_1);
       	(idA_A2_4, a_4)
+      	=
       	if ( idA_A2_1 = 696) then
       	A2_A2a_en(idA_A2_1, a_1, false)
       	 else (idA_A2_1, a_1);
       	(idA_A2_5, a_5)
+      	=
       	if ( idA_A2_1 = 697) then
       	A2_A2b_en(idA_A2_1, a_1, false)
       	 else (idA_A2_1, a_1);
       	(idA_A2_6, idEvents1_A_4, a_6)
+      	=
       		 if ( idA_A2_1 = 0) then
       		(idA_A2_3, idEvents1_A_3, a_3)
       		 else
       		 if ( idA_A2_1 = 696) then
       		(idA_A2_4, idEvents1_A_3, a_4)
       		 else
       		 if ( idA_A2_1 = 697) then
       		(idA_A2_5, idEvents1_A_3, a_5)
       		 else (idA_A2_1, idEvents1_A_2, a_1);
       	(idA_A2, idEvents1_A, a)
       	= (idA_A2_6, idEvents1_A_4, a_6);
       tel
       -- Exit action for state :A_A2
       node A_A2_ex(idA_A2_1:int;
       	idEvents1_A_1:int;
       	isInner:bool)
       returns (idA_A2:int;
       	idEvents1_A:int);
       var 	idA_A2_2, idA_A2_3, idA_A2_4, idA_A2_5:int;
       	idEvents1_A_2:int;
       let
       	(idA_A2_2)
+      	=
       	if ( idA_A2_1 = 696) then
       	A2_A2a_ex(idA_A2_1, false)
       	 else (idA_A2_1);
       	(idA_A2_3)
+      	=
       	if ( idA_A2_1 = 697) then
       	A2_A2b_ex(idA_A2_1, false)
       	 else (idA_A2_1);
       	(idA_A2_4)
+      	=
       		 if ( idA_A2_1 = 696) then
       		(idA_A2_2)
       		 else
       		 if ( idA_A2_1 = 697) then
       		(idA_A2_3)
       		 else (idA_A2_1);
       	-- set state as inactive
       	idEvents1_A_2
       	 = if (not isInner) then 0 else idEvents1_A_1;
       	idA_A2_5
       	= 0;
       	(idA_A2, idEvents1_A)
       	= (idA_A2_5, idEvents1_A_1);
       tel
       -- Entry action for state :A1_A1b
       node A1_A1b_en(idA_A1_1:int;
       	a_1:int;
       	isInner:bool)
       returns (idA_A1:int;
       	a:int);
       var 	idA_A1_2:int;
       	a_2:int;
       let
       	-- set state as active
       	idA_A1_2
       	= 700;
       	a_2
       	= if (not isInner) then  a_1 +2
       	 else a_1;
       	(idA_A1, a)
       	= (idA_A1_2, a_2);
       tel
       -- Exit action for state :A1_A1b
       node A1_A1b_ex(idA_A1_1:int;
       	isInner:bool)
       returns (idA_A1:int);
       var 	idA_A1_2:int;
       let
       	-- set state as inactive
       	idA_A1_2
       	 = if (not isInner) then 0 else idA_A1_1;
       	(idA_A1)
       	= (idA_A1_1);
       tel
       -- Entry action for state :A1_A1a
       node A1_A1a_en(idA_A1_1:int;
       	a_1:int;
       	isInner:bool)
       returns (idA_A1:int;
       	a:int);
       var 	idA_A1_2:int;
       	a_2:int;
       let
       	-- set state as active
       	idA_A1_2
       	= 699;
       	a_2
       	= if (not isInner) then  a_1 +1
       	 else a_1;
       	(idA_A1, a)
       	= (idA_A1_2, a_2);
       tel
       -- Exit action for state :A1_A1a
       node A1_A1a_ex(idA_A1_1:int;
       	isInner:bool)
       returns (idA_A1:int);
       var 	idA_A1_2:int;
       let
       	-- set state as inactive
       	idA_A1_2
       	 = if (not isInner) then 0 else idA_A1_1;
       	(idA_A1)
       	= (idA_A1_1);
       tel
       -- Entry action for state :A_A1
       node A_A1_en(idA_A1_1:int;
       	idEvents1_A_1:int;
       	a_1:int;
       	isInner:bool)
       returns (idA_A1:int;
       	idEvents1_A:int;
       	a:int);
       var 	idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5, idA_A1_6:int;
       	idEvents1_A_2, idEvents1_A_3, idEvents1_A_4:int;
       	a_2, a_3, a_4, a_5, a_6:int;
       let
       	-- set state as active
       	idEvents1_A_2
       	= 698;
       -- transition trace :
       	--POINT__To__A1_A1a_1
       		(idA_A1_2, a_2)
       	= A1_A1a_en(idA_A1_1, a_1, false);
       	(idA_A1_3, idEvents1_A_3, a_3)
+      	=
       	if ( idA_A1_1 = 0) then
       	 (idA_A1_2, idEvents1_A_2, a_2)
       	 else(idA_A1_1, idEvents1_A_2, a_1);
       	(idA_A1_4, a_4)
+      	=
       	if ( idA_A1_1 = 699) then
       	A1_A1a_en(idA_A1_1, a_1, false)
       	 else (idA_A1_1, a_1);
       	(idA_A1_5, a_5)
+      	=
       	if ( idA_A1_1 = 700) then
       	A1_A1b_en(idA_A1_1, a_1, false)
       	 else (idA_A1_1, a_1);
       	(idA_A1_6, idEvents1_A_4, a_6)
+      	=
       		 if ( idA_A1_1 = 0) then
       		(idA_A1_3, idEvents1_A_3, a_3)
       		 else
       		 if ( idA_A1_1 = 699) then
       		(idA_A1_4, idEvents1_A_3, a_4)
       		 else
       		 if ( idA_A1_1 = 700) then
       		(idA_A1_5, idEvents1_A_3, a_5)
       		 else (idA_A1_1, idEvents1_A_2, a_1);
       	(idA_A1, idEvents1_A, a)
       	= (idA_A1_6, idEvents1_A_4, a_6);
       tel
       -- Exit action for state :A_A1
       node A_A1_ex(idA_A1_1:int;
       	idEvents1_A_1:int;
       	isInner:bool)
       returns (idA_A1:int;
       	idEvents1_A:int);
       var 	idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5:int;
       	idEvents1_A_2:int;
       let
       	(idA_A1_2)
+      	=
       	if ( idA_A1_1 = 699) then
       	A1_A1a_ex(idA_A1_1, false)
       	 else (idA_A1_1);
       	(idA_A1_3)
+      	=
       	if ( idA_A1_1 = 700) then
       	A1_A1b_ex(idA_A1_1, false)
       	 else (idA_A1_1);
       	(idA_A1_4)
+      	=
       		 if ( idA_A1_1 = 699) then
       		(idA_A1_2)
       		 else
       		 if ( idA_A1_1 = 700) then
       		(idA_A1_3)
       		 else (idA_A1_1);
       	-- set state as inactive
       	idEvents1_A_2
       	 = if (not isInner) then 0 else idEvents1_A_1;
       	idA_A1_5
       	= 0;
       	(idA_A1, idEvents1_A)
       	= (idA_A1_5, idEvents1_A_1);
       tel
       -- Entry action for state :Events1_A
       node Events1_A_en(idEvents1_A_1:int;
       	idEvents1_Events1_1:int;
       	a_1:int;
       	idA_A1_1:int;
       	idA_A2_1:int;
       	isInner:bool)
       returns (idEvents1_A:int;
       	idEvents1_Events1:int;
       	a:int;
       	idA_A1:int;
       	idA_A2:int);
       var 	idEvents1_A_2, idEvents1_A_3, idEvents1_A_4, idEvents1_A_5, idEvents1_A_6:int;
       	idEvents1_Events1_2, idEvents1_Events1_3, idEvents1_Events1_4:int;
       	a_2, a_3, a_4, a_5, a_6:int;
       	idA_A1_2, idA_A1_3, idA_A1_4, idA_A1_5:int;
       	idA_A2_2, idA_A2_3:int;
       let
       	-- set state as active
       	idEvents1_Events1_2
       	= 694;
       -- transition trace :
       	--POINT__To__A_A1_1
       		(idA_A1_2, idEvents1_A_2, a_2)
       	= A_A1_en(idA_A1_1, idEvents1_A_1, a_1, false);
       	(idEvents1_A_3, idEvents1_Events1_3, a_3, idA_A1_3)
+      	=
       	if ( idEvents1_A_1 = 0) then
       	 (idEvents1_A_2, idEvents1_Events1_2, a_2, idA_A1_2)
       	 else(idEvents1_A_1, idEvents1_Events1_2, a_1, idA_A1_1);
       	(idA_A2_2, idEvents1_A_4, a_4)
+      	=
       	if ( idEvents1_A_1 = 695) then
       	A_A2_en(idA_A2_1, idEvents1_A_1, a_1, false)
       	 else (idA_A2_1, idEvents1_A_1, a_1);
       	(idA_A1_4, idEvents1_A_5, a_5)
+      	=
       	if ( idEvents1_A_1 = 698) then
       	A_A1_en(idA_A1_1, idEvents1_A_1, a_1, false)
       	 else (idA_A1_1, idEvents1_A_1, a_1);
       	(idEvents1_A_6, idEvents1_Events1_4, a_6, idA_A1_5, idA_A2_3)
+      	=
       		 if ( idEvents1_A_1 = 0) then
       		(idEvents1_A_3, idEvents1_Events1_3, a_3, idA_A1_3, idA_A2_1)
       		 else
       		 if ( idEvents1_A_1 = 695) then
       		(idEvents1_A_4, idEvents1_Events1_3, a_4, idA_A1_1, idA_A2_2)
       		 else
       		 if ( idEvents1_A_1 = 698) then
       		(idEvents1_A_5, idEvents1_Events1_3, a_5, idA_A1_4, idA_A2_1)
       		 else (idEvents1_A_1, idEvents1_Events1_2, a_1, idA_A1_1, idA_A2_1);
       	(idEvents1_A, idEvents1_Events1, a, idA_A1, idA_A2)
       	= (idEvents1_A_6, idEvents1_Events1_4, a_6, idA_A1_5, idA_A2_3);
       tel
       -- Exit action for state :Events1_A
       node Events1_A_ex(idA_A2_1:int;
       	idEvents1_A_1:int;
       	idA_A1_1:int;
       	idEvents1_Events1_1:int;
       	isInner:bool)
       returns (idA_A2:int;
       	idEvents1_A:int;
       	idA_A1:int;
       	idEvents1_Events1:int);
       var 	idA_A2_2, idA_A2_3:int;
       	idEvents1_A_2, idEvents1_A_3, idEvents1_A_4, idEvents1_A_5:int;
       	idA_A1_2, idA_A1_3:int;
       	idEvents1_Events1_2:int;
       let
       	(idA_A2_2, idEvents1_A_2)
+      	=
       	if ( idEvents1_A_1 = 695) then
       	A_A2_ex(idA_A2_1, idEvents1_A_1, false)
       	 else (idA_A2_1, idEvents1_A_1);
       	(idA_A1_2, idEvents1_A_3)
+      	=
       	if ( idEvents1_A_1 = 698) then
       	A_A1_ex(idA_A1_1, idEvents1_A_1, false)
       	 else (idA_A1_1, idEvents1_A_1);
       	(idA_A2_3, idEvents1_A_4, idA_A1_3)
+      	=
       		 if ( idEvents1_A_1 = 695) then
       		(idA_A2_2, idEvents1_A_2, idA_A1_1)
       		 else
       		 if ( idEvents1_A_1 = 698) then
       		(idA_A2_1, idEvents1_A_3, idA_A1_2)
       		 else (idA_A2_1, idEvents1_A_1, idA_A1_1);
       	-- set state as inactive
       	idEvents1_Events1_2
       	 = if (not isInner) then 0 else idEvents1_Events1_1;
       	idEvents1_A_5
       	= 0;
       	(idA_A2, idEvents1_A, idA_A1, idEvents1_Events1)
       	= (idA_A2_3, idEvents1_A_5, idA_A1_3, idEvents1_Events1_1);
       tel
       --***************************************************State :A_A2 Automaton***************************************************
       node A_A2_node(idA_A2_1:int;
       	a_1:int;
       	S:bool;
       	R:bool)
       returns (idA_A2:int;
       	a:int);
       let
       	 automaton a_a2
       	state POINTA_A2:
       	unless (idA_A2_1=0) restart POINT__TO__A2_A2A_1
       	unless (idA_A2_1=696) and S restart A2_A2A__TO__A2_A2B_1
       	unless (idA_A2_1=697) and R restart A2_A2B__TO__A2_A2A_1
       	unless (idA_A2_1=696) restart A2_A2A_IDL
       	unless (idA_A2_1=697) restart A2_A2B_IDL
       	let
       		(idA_A2, a)
       	= (idA_A2_1, a_1);
       	tel
       	state POINT__TO__A2_A2A_1:
       	 var 	idA_A2_2:int;
       	a_2:int;
       	let
       		-- transition trace :
       	--POINT__To__A2_A2a_1
       		(idA_A2_2, a_2)
       	= A2_A2a_en(idA_A2_1, a_1, false);
       	(idA_A2, a)
       	=  (idA_A2_2, a_2);
       	tel
       	until true restart POINTA_A2
       	state A2_A2A__TO__A2_A2B_1:
       	 var 	idA_A2_2, idA_A2_3:int;
       	a_2:int;
       	let
       		-- transition trace :
       	--A2_A2a__To__A2_A2b_1
       		(idA_A2_2)
       	= A2_A2a_ex(idA_A2_1, false);
       		(idA_A2_3, a_2)
       	= A2_A2b_en(idA_A2_2, a_1, false);
       	(idA_A2, a)
       	=  (idA_A2_3, a_2);
       	tel
       	until true restart POINTA_A2
       	state A2_A2B__TO__A2_A2A_1:
       	 var 	idA_A2_2, idA_A2_3:int;
       	a_2:int;
       	let
       		-- transition trace :
       	--A2_A2b__To__A2_A2a_1
       		(idA_A2_2)
       	= A2_A2b_ex(idA_A2_1, false);
       		(idA_A2_3, a_2)
       	= A2_A2a_en(idA_A2_2, a_1, false);
       	(idA_A2, a)
       	=  (idA_A2_3, a_2);
       	tel
       	until true restart POINTA_A2
       	state A2_A2A_IDL:
       	 	let
       	(idA_A2, a)
       	= (idA_A2_1, a_1);
       	tel
       	until true restart POINTA_A2
       	state A2_A2B_IDL:
       	 	let
       	(idA_A2, a)
       	= (idA_A2_1, a_1);
       	tel
       	until true restart POINTA_A2
       tel
       --***************************************************State :A_A1 Automaton***************************************************
       node A_A1_node(idA_A1_1:int;
       	a_1:int;
       	S:bool;
       	R:bool)
       returns (idA_A1:int;
       	a:int);
       let
       	 automaton a_a1
       	state POINTA_A1:
       	unless (idA_A1_1=0) restart POINT__TO__A1_A1A_1
       	unless (idA_A1_1=699) and S restart A1_A1A__TO__A1_A1B_1
       	unless (idA_A1_1=700) and R restart A1_A1B__TO__A1_A1A_1
       	unless (idA_A1_1=699) restart A1_A1A_IDL
       	unless (idA_A1_1=700) restart A1_A1B_IDL
       	let
       		(idA_A1, a)
       	= (idA_A1_1, a_1);
       	tel
       	state POINT__TO__A1_A1A_1:
       	 var 	idA_A1_2:int;
       	a_2:int;
       	let
       		-- transition trace :
       	--POINT__To__A1_A1a_1
       		(idA_A1_2, a_2)
       	= A1_A1a_en(idA_A1_1, a_1, false);
       	(idA_A1, a)
       	=  (idA_A1_2, a_2);
       	tel
       	until true restart POINTA_A1
       	state A1_A1A__TO__A1_A1B_1:
       	 var 	idA_A1_2, idA_A1_3:int;
       	a_2:int;
       	let
       		-- transition trace :
       	--A1_A1a__To__A1_A1b_1
       		(idA_A1_2)
       	= A1_A1a_ex(idA_A1_1, false);
       		(idA_A1_3, a_2)
       	= A1_A1b_en(idA_A1_2, a_1, false);
       	(idA_A1, a)
       	=  (idA_A1_3, a_2);
       	tel
       	until true restart POINTA_A1
       	state A1_A1B__TO__A1_A1A_1:
       	 var 	idA_A1_2, idA_A1_3:int;
       	a_2:int;
       	let
       		-- transition trace :
       	--A1_A1b__To__A1_A1a_1
       		(idA_A1_2)
       	= A1_A1b_ex(idA_A1_1, false);
       		(idA_A1_3, a_2)
       	= A1_A1a_en(idA_A1_2, a_1, false);
       	(idA_A1, a)
       	=  (idA_A1_3, a_2);
       	tel
       	until true restart POINTA_A1
       	state A1_A1A_IDL:
       	 	let
       	(idA_A1, a)
       	= (idA_A1_1, a_1);
       	tel
       	until true restart POINTA_A1
       	state A1_A1B_IDL:
       	 	let
       	(idA_A1, a)
       	= (idA_A1_1, a_1);
       	tel
       	until true restart POINTA_A1
       tel
       --***************************************************State :Events1_A Automaton***************************************************
       node Events1_A_node(idEvents1_A_1:int;
       	a_1:int;
       	idA_A1_1:int;
       	T:bool;
       	idA_A2_1:int;
       	R:bool;
       	S:bool)
       returns (idEvents1_A:int;
       	a:int;
       	idA_A1:int;
       	idA_A2:int);
       let
       	 automaton events1_a
       	state POINTEvents1_A:
       	unless (idEvents1_A_1=0) restart POINT__TO__A_A1_1
       	unless (idEvents1_A_1=695) and T restart A_A2__TO__A_A1_1
       	unless (idEvents1_A_1=698) and T restart A_A1__TO__A_A2_1
       	unless (idEvents1_A_1=695) restart A_A2_IDL
       	unless (idEvents1_A_1=698) restart A_A1_IDL
       	let
       		(idEvents1_A, a, idA_A1, idA_A2)
       	= (idEvents1_A_1, a_1, idA_A1_1, idA_A2_1);
       	tel
       	state POINT__TO__A_A1_1:
       	 var 	idEvents1_A_2:int;
       	a_2:int;
       	idA_A1_2:int;
       	let
       		-- transition trace :
       	--POINT__To__A_A1_1
       		(idA_A1_2, idEvents1_A_2, a_2)
       	= A_A1_en(idA_A1_1, idEvents1_A_1, a_1, false);
       	(idEvents1_A, a, idA_A1)
       	=  (idEvents1_A_2, a_2, idA_A1_2);
       	--add unused variables
       	(idA_A2)
       	= (idA_A2_1);
       	tel
       	until true restart POINTEvents1_A
       	state A_A2__TO__A_A1_1:
       	 var 	idEvents1_A_2, idEvents1_A_3:int;
       	a_2:int;
       	idA_A1_2:int;
       	idA_A2_2:int;
       	let
       		-- transition trace :
       	--A_A2__To__A_A1_1
       		(idA_A2_2, idEvents1_A_2)
       	= A_A2_ex(idA_A2_1, idEvents1_A_1, false);
       		(idA_A1_2, idEvents1_A_3, a_2)
       	= A_A1_en(idA_A1_1, idEvents1_A_2, a_1, false);
       	(idEvents1_A, a, idA_A1, idA_A2)
       	=  (idEvents1_A_3, a_2, idA_A1_2, idA_A2_2);
       	tel
       	until true restart POINTEvents1_A
       	state A_A1__TO__A_A2_1:
       	 var 	idEvents1_A_2, idEvents1_A_3:int;
       	a_2:int;
       	idA_A1_2:int;
       	idA_A2_2:int;
       	let
       		-- transition trace :
       	--A_A1__To__A_A2_1
       		(idA_A1_2, idEvents1_A_2)
       	= A_A1_ex(idA_A1_1, idEvents1_A_1, false);
       		(idA_A2_2, idEvents1_A_3, a_2)
       	= A_A2_en(idA_A2_1, idEvents1_A_2, a_1, false);
       	(idEvents1_A, a, idA_A1, idA_A2)
       	=  (idEvents1_A_3, a_2, idA_A1_2, idA_A2_2);
       	tel
       	until true restart POINTEvents1_A
       	state A_A2_IDL:
       	 var 	a_2:int;
       	idA_A2_2:int;
       	let
       	(idA_A2_2, a_2)
       	= A_A2_node(idA_A2_1, a_1, S, R);
       	(idEvents1_A, a, idA_A1, idA_A2)
       	= (idEvents1_A_1, a_2, idA_A1_1, idA_A2_2);
       	tel
       	until true restart POINTEvents1_A
       	state A_A1_IDL:
       	 var 	a_2:int;
       	idA_A1_2:int;
       	let
       	(idA_A1_2, a_2)
       	= A_A1_node(idA_A1_1, a_1, S, R);
       	(idEvents1_A, a, idA_A1, idA_A2)
       	= (idEvents1_A_1, a_2, idA_A1_2, idA_A2_1);
       	tel
       	until true restart POINTEvents1_A
       tel
       --***************************************************State :Events1_Events1 Automaton***************************************************
       node Events1_Events1_node(idEvents1_Events1_1:int;
       	a_1:int;
       	idA_A1_1:int;
       	idA_A2_1:int;
       	idEvents1_A_1:int;
       	R:bool;
       	S:bool;
       	T:bool)
       returns (idEvents1_Events1:int;
       	a:int;
       	idA_A1:int;
       	idA_A2:int;
       	idEvents1_A:int);
       let
       	 automaton events1_events1
       	state POINTEvents1_Events1:
       	unless (idEvents1_Events1_1=0) restart POINT__TO__EVENTS1_A_1
       	unless true  restart EVENTS1_EVENTS1_PARALLEL_IDL
       	let
       		(idEvents1_Events1, a, idA_A1, idA_A2, idEvents1_A)
       	= (idEvents1_Events1_1, a_1, idA_A1_1, idA_A2_1, idEvents1_A_1);
       	tel
       	state POINT__TO__EVENTS1_A_1:
       	 var 	idEvents1_Events1_2:int;
       	a_2:int;
       	idA_A1_2:int;
       	idA_A2_2:int;
       	idEvents1_A_2:int;
       	let
       		-- transition trace :
       	--POINT__To__Events1_A_1
       		(idEvents1_A_2, idEvents1_Events1_2, a_2, idA_A1_2, idA_A2_2)
       	= Events1_A_en(idEvents1_A_1, idEvents1_Events1_1, a_1, idA_A1_1, idA_A2_1, false);
       	(idEvents1_Events1, a, idA_A1, idA_A2, idEvents1_A)
       	=  (idEvents1_Events1_2, a_2, idA_A1_2, idA_A2_2, idEvents1_A_2);
       	tel
       	until true restart POINTEvents1_Events1
       	state EVENTS1_EVENTS1_PARALLEL_IDL:
       	 var 	a_2:int;
       	idA_A1_2:int;
       	idA_A2_2:int;
       	idEvents1_A_2:int;
       	let
       		(idEvents1_A_2, a_2, idA_A1_2, idA_A2_2)
       	= if not (idEvents1_A_1= 0 ) then Events1_A_node(idEvents1_A_1, a_1, idA_A1_1, T, idA_A2_1, R, S)
       		 else (idEvents1_A_1, a_1, idA_A1_1, idA_A2_1);
       	(idEvents1_Events1, a, idA_A1, idA_A2, idEvents1_A)
       	= (idEvents1_Events1_1, a_2, idA_A1_2, idA_A2_2, idEvents1_A_2);
       	tel
       	until true restart POINTEvents1_Events1
       tel
       --***************************************************State :Events1_Events1 Automaton***************************************************
       node EventsOrder_Events1(R:bool;
       	S:bool;
       	T:bool)
       returns (a:int);
       var a_1: int;
       	idEvents1_Events1, idEvents1_Events1_1: int;
       	idA_A2, idA_A2_1: int;
       	idA_A1, idA_A1_1: int;
       	idEvents1_A, idEvents1_A_1: int;
       		idEvents1_Events1_2, idEvents1_Events1_3:int;
       	a_2, a_3:int;
       	idA_A1_2, idA_A1_3:int;
       	idA_A2_2, idA_A2_3:int;
       	idEvents1_A_2, idEvents1_A_3:int;
       let
       	a_1 = 0 -> pre a;
       	idEvents1_Events1_1 = 0 -> pre idEvents1_Events1;
       	idA_A2_1 = 0 -> pre idA_A2;
       	idA_A1_1 = 0 -> pre idA_A1;
       	idEvents1_A_1 = 0 -> pre idEvents1_A;
       	(idEvents1_Events1_2, a_2, idA_A1_2, idA_A2_2, idEvents1_A_2)
+      	 =
       	 if R then Events1_Events1_node(idEvents1_Events1_1, a_1, idA_A1_1, idA_A2_1, idEvents1_A_1, R, false, false)
       	 else (idEvents1_Events1_1, a_1, idA_A1_1, idA_A2_1, idEvents1_A_1);
       	(idEvents1_Events1_3, a_3, idA_A1_3, idA_A2_3, idEvents1_A_3)
+      	 =
       	 if S then Events1_Events1_node(idEvents1_Events1_2, a_2, idA_A1_2, idA_A2_2, idEvents1_A_2, false, S, false)
       	 else (idEvents1_Events1_2, a_2, idA_A1_2, idA_A2_2, idEvents1_A_2);
       	(idEvents1_Events1, a, idA_A1, idA_A2, idEvents1_A)
+      	 =
       	 if T then Events1_Events1_node(idEvents1_Events1_3, a_3, idA_A1_3, idA_A2_3, idEvents1_A_3, false, false, T)
       	 else (idEvents1_Events1_3, a_3, idA_A1_3, idA_A2_3, idEvents1_A_3);
       --unused outputs
       tel
       node EventsOrder (R_1_1 : real; S_1_1 : real; T_1_1 : real)
       returns (Out1_1_1 : int);
       var
       	Events1_1_1 : int;
       	Mux_1_1 : real; Mux_1_2 : real; Mux_1_3 : real;
       	i_virtual_local : real;
       	Events1Mux_1_1_event: bool;
       	Events1Mux_1_2_event: bool;
       	Events1Mux_1_3_event: bool;
       let
       	Events1Mux_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));
       	Events1Mux_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));
       	Events1Mux_1_3_event = false -> ((pre(Mux_1_3) > 0.0 and Mux_1_3 <= 0.0) or (pre(Mux_1_3) <= 0.0 and Mux_1_3 > 0.0));
       	Events1_1_1 =  EventsOrder_Events1(Events1Mux_1_1_event, Events1Mux_1_2_event, Events1Mux_1_3_event);
       	Mux_1_1 = R_1_1 ;
       	Mux_1_2 = S_1_1 ;
       	Mux_1_3 = T_1_1 ;
       	Out1_1_1 = Events1_1_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