Print "Loading Synthesis.tlv $Revision: 1.0.3 $\n\n";

--
-- GENERAL NOTES FOR DOCUMENTATION.
-- =================================
-- In addition to a full method documentation, and sectional API distributed
-- in the document, a complete API from the entire document is gathered at
-- the end of the document.
-- 
-- comments special words: 
-- * TODO:   - still needs to implement.
-- * FIXME:  - a known bug
-- * WARNING: - might react unexpectedly
-- * REVIEW:  - still needs to be checked
-- 
-- methods signature comment notations:
-- * (public)    - un-restricted method which can be used freely.
-- * (protected) - internal methods which can be use, however their context is
--                 important for the correctness. It is recommended to
--                 understand the context of usage.
-- * (private)   - restricted methods, which are tightly related on their
--                 context. It is not recommended to use these methods without,
--                 fully understanding their implementations.
-- 
-- work in the current version:
-- * taking care of the API.
-- * fixing deletion of states.
-- * adding another condition for the elimination of state in the optimization.
-- * picking a kind of strategy.
-- * fixing the states enumations.
-- 
-- 
-- Added feature to version:
-- ==========================
-- * (v1.0.1) - looking for the smallest 'r' in the strategy.
-- * (v1.0.1) - added to the "find_strategy" signature, a parameter to choose
--              the kind of desired strategy.
-- * (v1.0.2) - added optimizations to the loop in optimize_aut.
-- * (v1.0.2) - changed the delete_vertex to not perform a shift.
-- * (v1.0.2) - chenged the optimize_aut sig to add whether to shift or not,
--              and if shifting then perform the new "To shift_all_state".
-- * (v1.0.2) - added "To shift_all_state".
-- * (v1.0.3) - small bug fix to shifting.
-- 
-- Known Bugs:
-- ============
-- * 
-- 

--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
--------------- basic utilities (originate from synt_basic.tlv) ----------------
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------

--==============================================================================
--================== General Operations API ====================================
--==============================================================================
-- 
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ flags and internals. ++++++++++++++++++++++++++++++++++++++
-- NA
-- 
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To eol; ++++++++++++++++++++++++++++++++++++++++++
-- Print a new line.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To abort; ++++++++++++++++++++++++++++++++++++++++
-- Completely ends the program.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To assert bool, 'diagnostic; +++++++++++++++++++++
-- assertion utility.
-- 
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func null(bdd); ++++++++++++++++++++++++++++++++++
-- Checking whether this is an empty bdd or not
-- 
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (protected) To prepare_synt tsCs := 1, ++++++++++++++++++++
-- +++++++++++++++++                             tsAs := 2; ++++++++++++++++++++
-- Preparing the transition systems for the game.
-- 
-- +++++++++++++++++ (public) Func cox(state); +++++++++++++++++++++++++++++++++
-- The basic step of the game. Namely, forall the first player transitions 
-- there exists a second player transition which leads into 'state'.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func exist_in_array(&arr, to_check); +++++++++++++
-- Check whether an element exists in an array.
--
--==============================================================================
--==============================================================================
--==============================================================================

--------------------------------------------------------------------------------
-- Method      : (public) To eol
-- Description : Print a new line.
-- Parameters  : Void.
-- Return Val  : Void.
--------------------------------------------------------------------------------
To eol;
    Print ("\n");
End -- To eol;

--------------------------------------------------------------------------------
-- Method      : (public) To abort
-- Description : Completely ends the program.
-- Parameters  : Void. 
-- Return Val  : Void. 
--------------------------------------------------------------------------------
To abort;
    Print ("\n\tExecution Aborted\n");
    Local aaa := ___error___abort___;
End -- To abort;

--------------------------------------------------------------------------------
-- Method      : (public) To assert
-- Description : assertion utility.
-- Parameters  : bool       - the boolean assertional check that has to pass.
--               diagnostic - a string describing the failure reason. 
-- Return Val  : Void. 
--------------------------------------------------------------------------------
To assert bool, 'diagnostic;
    If (bool)
	Return;
    End
    --Let 'internal_print := ltl(bool);
    Print "\n\t*** Internal Error!!!";
    Print "\n\tDiagnostic: ", 'diagnostic, "\n";
    abort;
End -- To assert bool, 'diagnostic;

--------------------------------------------------------------------------------
-- Method      : (public) Func null
-- Description : Checking whether this is an empty bdd or not
-- Parameters  : bdd - the bdd to check
-- Return Val  : TRUE if the bdd has an assignment, FALSE otherwise.
--------------------------------------------------------------------------------
Func null(bdd);
    If (bdd)
	Return 0;
    Else
	Return 1;
    End
End -- Func null(bdd);

--------------------------------------------------------------------------------
-- Method      : (protected) To prepare_synt
-- Description : Preparing the transition systems for the game.
-- Parameters  : tsCs - the first transition system (i.e. player 1), default
--               is 1.
--               tsAs - the second transition system (i.e. player 2), default
--               is 2.
-- Return Val  : void
--------------------------------------------------------------------------------
To prepare_synt tsCs := 1, tsAs := 2;
    Let vars1 := V(tsCs);
    Let vars2 := V(tsAs);
    Let vars  := vars1 & vars2;
    Let prv1 := prime(V(tsCs));
    Let prv2 := prime(V(tsAs));
    Let trans1 := T(tsCs);
    Let trans2 := T(tsAs);   
    Let nps := nJ(tsCs);
    Let nqs := nJ(tsAs);
End -- To prepare_synt;

--------------------------------------------------------------------------------
-- Method      : (public) Func cox
-- Description : The basic step of the game. Namely, forall the first player 
--               transitions there exists a second player transition which
--               leads into 'state'.
-- Parameters  : state - the set of state that the step should reach.
-- Return Val  : the set of states that can reach 'state' in such a step.
--------------------------------------------------------------------------------
Func cox(state);
    Let rec_state := state;
    Let exy := ((trans2 & prime(state)) forsome prv2);
    Let rcox := ((trans1 -> exy) forall prv1);
    Let prcox := prime(rcox);
    Return rcox;
End -- Func cox(state);

--------------------------------------------------------------------------------
-- Method      : (public) Func exist_in_array
-- Description : Check whether an element exists in an array.
-- Parameters  : arr      - the array to look at.
--               to_check - the element to check for its existence.
-- Return Val  : TRUE if the element exists, otherwise FALSE.
--------------------------------------------------------------------------------
Func exist_in_array(&arr, to_check);
    For(i in 1...length(arr))
	If (to_check = arr[i])
	    Return TRUE;
	End
    End
    Return FALSE;
End -- Func exist_in_array(&arr, to_check);


--==============================================================================
--================== Automata API ==============================================
--==============================================================================
-- Utilizing the enumerated automaton using a stack technique
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ flags and internals. ++++++++++++++++++++++++++++++++++++++
-- Let __STATE := 1; - internal automata variables.
-- Let __RANK  := 2; - internal automata variables.
-- Let __SUCC  := 3; - internal automata variables.
--
-- GENERAL AUTOMATA
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To new_automaton &aut; +++++++++++++++++++++++++++
-- creating a new automaton
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To delaut &aut; ++++++++++++++++++++++++++++++++++
-- Delete an automaton.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (protected) To push_state &aut, st, rank:=-1; +++++++++++++
-- Pushing a new state to the end of the automaton. It is recommend to use 
-- mk_state.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func mk_state(&aut, state, rank); ++++++++++++++++
-- Inserting a new state and rank only if not existing, and returning its index.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func exist_state(&aut, state, rank); +++++++++++++
-- Checking if a state exists in the automata.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To push_succ &aut, src, dest; ++++++++++++++++++++
-- push a new successor to some existing state
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (protected) To pop_state &aut, &res; ++++++++++++++++++++++
-- Extract and return the last state in the automata.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (private) To shift_state &aut, st; ++++++++++++++++++++++++
-- Shifting a state in the automaton to decrease all higher enumerated state.
-- 
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (private) To shift_all_state &aut, st; +++++++++++++++++++
-- Shifting all states in the automaton to decrease all higher enumerated 
-- state. It is important to send a state to this method only after edges to
-- it has been removed.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To delete_vertex &aut, src, dest; ++++++++++++++++
-- Removing a vertex from the aut.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func pop_succ(&aut, st); +++++++++++++++++++++++++
-- Popping the last successor from a state.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To top &aut, &res; +++++++++++++++++++++++++++++++
-- Returning the last state of the automata.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func aut_length(&aut); +++++++++++++++++++++++++++
-- The number of states in this automaton.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func number_of_succ(&aut, st); +++++++++++++++++++
-- The number of successors for a state in this automaton.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func has_succ(&aut, src, dest); ++++++++++++++++++
-- Check whether there exists an edge.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func has_the_same_succs(&aut, v1, v2); +++++++++++
-- Check whether given two vertexes has the same successors.
--
--
-- GETTERS
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func state_at(&aut, index); ++++++++++++++++++++++
-- Getter for a state at an index in the automata.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func rank_at(&aut, index); +++++++++++++++++++++++
-- Getter for a rank at an index in the automata.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func succ_at(&aut, index, succ_index); +++++++++++
-- Getter for a successor at an index in the automata, at an index of the
-- array of successors.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To pop_all_succs &aut, st, &res; +++++++++++++++++
-- Popping the whole array of successors from a state.
--
--
-- SETTERS
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To set_state_at &aut, index, val; ++++++++++++++++
-- Setter for a state at an index in the automata.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To set_rank_at &aut, index, val; +++++++++++++++++
-- Setter for a rank at an index in the automata.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To set_succ_at &aut, index, succ, val; +++++++++++
-- Setter for a successor at an index in the automata, at an index of the
-- array of successors.
--
--
-- PRINTING
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To print_aut &aut; +++++++++++++++++++++++++++++++
-- Print the automaton.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To print_dotty_aut &aut; +++++++++++++++++++++++++
-- Print the automaton in a dotty format to file "automata.dot".
--
--==============================================================================
--==============================================================================
--==============================================================================

-- This internal variables can not be changed!!!!!!!
Let __STATE := 1;
Let __RANK := 2;
Let __SUCC := 3;

--------------------------------------------------------------------------------
-- Method      : (public) To new_automaton;
-- Description : Creating a new automaton.
-- Parameters  : aut - the name of the automaton.
-- Return Val  : Void.
--------------------------------------------------------------------------------
To new_automaton &aut;
    -- deleting existing arrays
    If ( exist(aut[__STATE][0]) ) 
	delarr aut[__STATE]; 
    End
    If ( exist(aut[__RANK][0]) ) 
	delarr aut[__RANK]; 
    End
    If ( exist(aut[__SUCC][0]) ) 
	For(i in 1...aut[__SUCC][0]) 
	    delarr aut[__SUCC][i]; 
	End
	delarr aut[__SUCC];
    End
    
    -- building all arrays
    new aut[__STATE];
    new aut[__RANK];
    new aut[__SUCC];
End -- To new_automaton &aut;

--------------------------------------------------------------------------------
-- Method      : (public) To delaut
-- Description : Delete an automaton.
-- Parameters  : aut - the name of the automaton.
-- Return Val  : Void.
--------------------------------------------------------------------------------
To delaut &aut;
    If ( exist(aut[__STATE][0]) ) 
	delarr aut[__STATE]; 
    End
    If ( exist(aut[__RANK][0]) ) 
	delarr aut[__RANK]; 
    End
    If ( exist(aut[__SUCC][0]) ) 
	For(i in 1...aut[__SUCC][0]) 
	    delarr aut[__SUCC][i]; 
	End
	delarr aut[__SUCC];
    End
End -- To delaut &aut;

--------------------------------------------------------------------------------
-- Method      : (protected) To push_state
-- Description : Pushing a new state to the end of the automaton.
-- Parameters  : aut  - the name of the automaton.
--               st   - the new state to insert.
--               rank - the rank of the state, default is -1.
-- Return Val  : Void.
--------------------------------------------------------------------------------
To push_state &aut, st, rank:=-1;
    If ( !exist(aut[__STATE][0]) )
		new_automaton aut;
    End
    
    push aut[__STATE], st;
    push aut[__RANK], rank;
    
    -- making new room in the __SUCC array
    If ( !exist(aut[__SUCC][0]) )
		Let aut[__SUCC][0] := 0;
    End
    Let aut[__SUCC][0] := aut[__SUCC][0] + 1;
    -- building new array in this new room
    new aut[__SUCC][aut[__SUCC][0]];
End -- To push_state &aut, st, rank:=-1;

--------------------------------------------------------------------------------
-- Method      : (public) To push_succ
-- Description : Push a new successor to some existing state.
-- Parameters  : aut  - the name of the automaton.
--               src  - the source of this edge.
--               dest - the destination of this edge.
-- Return Val  : Void.
--------------------------------------------------------------------------------
To push_succ &aut, src, dest;
    assert ((src > 0) & (src <= aut_length(aut))),
           "Trying to reach an un-allocated place in the automaton stack.";
    assert ((dest > 0) & (dest <= aut_length(aut))),
           "Trying to reach an un-allocated place in the automaton stack.";
    If ( !exist(aut[__SUCC][src][0]) )
	Let aut[__SUCC][src][0] := 0;
    End
    
    Let aut[__SUCC][src][0] := aut[__SUCC][src][0] + 1;
    Let aut[__SUCC][src][aut[__SUCC][src][0]] := dest;
End -- To push_succ &aut, src, dest;

--------------------------------------------------------------------------------
-- Method      : (public) Func mk_state
-- Description : Inserting a new state and rank only if not existing.
-- Parameters  : aut   - the name of the automaton.
--               state - the new state to create.
--               rank  - the rank of the state.
-- Return Val  : The index of the state that was created.
--------------------------------------------------------------------------------
Func mk_state(&aut, state, rank);
    Local ret := exist_state(aut, state, rank);
    If (ret = -1)
		push_state aut, state, rank;
		Let ret := aut_length(aut);
    End
    Return ret;
End -- Func mk_state(&aut, state, rank);

--------------------------------------------------------------------------------
-- Method      : (public) Func exist_state
-- Description : Checking if a state exists in the automata.
-- Parameters  : aut   - the name of the automaton.
--               state - the state to check.
--               rank  - the rank of the state.
-- Return Val  : The index of the state that was created, or -1 if not found.
--------------------------------------------------------------------------------
Func exist_state(&aut, state, rank);
    For(i in 1...aut_length(aut))
		If( (state & aut[__STATE][i]) & (rank = aut[__RANK][i]) )
			Return i;
		End
    End
    
    Return -1;
End -- Func exist_state(&aut, state, rank);

--------------------------------------------------------------------------------
-- Method      : (protected) To pop_state
-- Description : Extract and return the last state in the automata.
-- Parameters  : aut    - the name of the automaton.
--               res    - an array of three values containing the followings:
--               res[1] - the state it self.
--               res[2] - the state's rank.
--               res[3] - an array of successors to this state.
-- Return Val  : Void. (return by reference)
--------------------------------------------------------------------------------
To pop_state &aut, &res;
    If ( aut[__STATE][0] )
		top aut, res;
		Local top_index := aut_length(aut);
		Local dummy := pop(aut[__STATE]);
		Let   dummy := pop(aut[__RANK]);
		delarr(aut[__SUCC][top_index]);
		Let aut[__SUCC][0] := aut[__SUCC][0] - 1;
		Return;
	Else
		Print "Warning: stack is empty\n";
		Let res := -1;
		Return;
	End
End -- To pop_state &aut, &res;
	
--------------------------------------------------------------------------------
-- Method      : (private) To shift_state
-- Description : Shifting a state in the automaton to decrease all higher
--               enumerated state. It is important to send a state to this 
--               method only after edges to it has been removed.
-- Parameters  : aut - the name of the automaton.
--               st  - the state to override.
-- Return Val  : Void.
--------------------------------------------------------------------------------
To shift_state &aut, st;
    assert ((st > 0) & (st <= aut_length(aut))),
           "Trying to delete an un-allocated place in the automaton stack.";
    For (i in st...(aut_length(aut) - 1))
		Let aut[__STATE][i] := aut[__STATE][i + 1];
		Let aut[__RANK][i] := aut[__RANK][i + 1];
		new aut[__SUCC][i];
		copy aut[__SUCC][i], aut[__SUCC][i + 1];
		For(ii in 1...aut_length(aut)) 
			For(jj in 1...number_of_succ(aut, ii))
				If(succ_at(aut, ii, jj) = (i + 1))
					set_succ_at aut, ii, jj, i;
				End
			End
		End
    End
	-- popping the last one.
	pop_state aut, dummy;
    
	-- op b - previous version.
	--    If(aut_length(aut) = st) -- if this is the last state
	--		pop_state aut, dummy;
	--    Else
	--		Let aut[__STATE][st] := aut[__STATE][st + 1];
	--		Let aut[__RANK][st] := aut[__RANK][st + 1];
	--		new aut[__SUCC][st];
	--		copy aut[__SUCC][st], aut[__SUCC][st + 1];
	--		For(i in 1...aut_length(aut)) 
	--			For(j in 1...number_of_succ(aut, i))
	--				If(succ_at(aut, i, j) = (st + 1))
	--					set_succ_at aut, i, j, st;
	--				End
	--			End
	--		End
	
	--		shift_state aut, (st + 1);
	--    End
End -- To shift_state &aut, st;

--------------------------------------------------------------------------------
-- Method      : (private) To shift_all_state
-- Description : Shifting all states in the automaton to decrease all higher
--               enumerated state. It is important to send a state to this 
--               method only after edges to it has been removed.
-- Parameters  : aut - the name of the automaton.
-- Return Val  : Void.
--------------------------------------------------------------------------------
To shift_all_state &aut;
    Local del := 0;
	For (look in 1...aut_length(aut))
		If (is_false(aut[__STATE][look]))
			Let del := del + 1;
		End
	End
	Print "deleting ", del, " states\n";

	Local first := 1;
	While (!is_false(aut[__STATE][first]))
		Let first := first + 1;
	End
	
	-- dummy extra step for stop.
	Let aut[__STATE][aut_length(aut) + 1] := 0;

	For (curr_del in 1...del)
		Local i := first;
		
		While (!is_false(aut[__STATE][i + curr_del]))
			Let aut[__STATE][i] := aut[__STATE][i + curr_del];
			Let aut[__RANK][i] := aut[__RANK][i + curr_del];
			new aut[__SUCC][i];
			copy aut[__SUCC][i], aut[__SUCC][i + curr_del];
			For(ii in 1...aut_length(aut)) 
				For(jj in 1...number_of_succ(aut, ii))
					If(succ_at(aut, ii, jj) = (i + curr_del))
						set_succ_at aut, ii, jj, i;
					End
				End
			End
			Let i := i + 1;
		End
		Let first := i;
	End
	
	-- removing dummy.
	delvar aut[__STATE][aut_length(aut) + 1];

	For (i in 1...del)
		-- popping all.
		pop_state aut, dummy;
	End
End -- To shift_all_state &aut;


--------------------------------------------------------------------------------
-- Method      : (public) To delete_vertex
-- Description : Removing a vertex from the aut.
-- Parameters  : aut     - the name of the automaton.
--               del     - the vertex to delete.
--               replace - the vertex to redirect to.
-- Return Val  : Void.
--------------------------------------------------------------------------------
To delete_vertex &aut, del, replace;
    assert ((del > 0) & (del <= aut_length(aut))),
           "Trying to replace a not existing state.";
    assert ((replace > 0) & (replace <= aut_length(aut))),
           "Trying to replace with a not existing state.";
    -- taking care of edges from del
    While(number_of_succ(aut, del) > 0)
		Local tmp := pop_succ(aut, del);
		-- inserting unique values
		If((tmp != replace) & (tmp != del))
			push_succ aut, replace, tmp;
		End
    End
	
    -- taking care of edges to del
    For(i in 1...aut_length(aut)) 
		For(j in 1...number_of_succ(aut, i))
			If(succ_at(aut, i, j) = del)
				set_succ_at aut, i, j, replace;
			End
		End
    End
	
	-- deleting del
	Let aut[__STATE][del] := 0;
	Let aut[__RANK] [del] := 0;

    -- shift_state aut, del;
End -- To delete_vertex &aut, del, replace;

--------------------------------------------------------------------------------
-- Method      : (public) Func pop_succ
-- Description : Popping the last successor from a state.
-- Parameters  : aut - the name of the automaton.
--               st  - the state from which to pop a successor.
-- Return Val  : The successor of the state.
--------------------------------------------------------------------------------
Func pop_succ(&aut, st);
    assert ((st > 0) & (st <= aut_length(aut))),
           "Trying to pop an un-allocated place in the automaton stack.";
    Return pop(aut[__SUCC][st]);
End -- Func pop_succ(&aut, st);

--------------------------------------------------------------------------------
-- Method      : (public) To top
-- Description : Returning the last state of the automata.
-- Parameters  : aut    - the name of the automaton.
--               res    - an array of three values containing the followings:
--               res[1] - the state it self.
--               res[2] - the state's rank.
--               res[3] - an array of successors to this state.
-- Return Val  : Void. (return by reference)
--------------------------------------------------------------------------------
To top &aut, &res;
    Let res[1] := aut[__STATE][aut[__STATE][0]];
    Let res[2] := aut[__RANK][aut[__RANK][0]];
    new res[3];
    copy res[3], aut[__SUCC][aut[__SUCC][0]];
    Return;
End -- To top &aut, &res;

--------------------------------------------------------------------------------
-- Method      : (public) Func aut_length
-- Description : The number of states in this automaton.
-- Parameters  : aut - the name of the automaton.
-- Return Val  : The number of states.
--------------------------------------------------------------------------------
Func aut_length(&aut);
    Return aut[__SUCC][0];
End -- Func aut_length(&aut);

--------------------------------------------------------------------------------
-- Method      : (public) Func number_of_succ
-- Description : The number of successors for a state in this automaton
-- Parameters  : aut - the name of the automaton.
--               st  - the state to be checked.
-- Return Val  : The number of successors.
--------------------------------------------------------------------------------
Func number_of_succ(&aut, st);
    assert ((st > 0) & (st <= aut_length(aut))),
           "Trying to reach an un-allocated place in the automaton stack.";
    Return length(aut[__SUCC][st]);
End -- Func number_of_succ(&aut, st);

--------------------------------------------------------------------------------
-- Method      : (public) Func has_succ
-- Description : Check whether there exists an edge.
-- Parameters  : aut  - the name of the automaton.
--               src  - the source of the edge.
--               dest - the destination of the edge.
-- Return Val  : TRUE if this edge exists, FALSE otherwise.
--------------------------------------------------------------------------------
Func has_succ(&aut, src, dest);
    assert ((src > 0) & (src <= aut_length(aut))),
           "Trying to check succ for a not existing state.";
    assert ((dest > 0) & (dest <= aut_length(aut))),
           "Trying to check succ for a not existing state.";
    For(i in 1...length(aut[__SUCC][src]))
	If(aut[__SUCC][src][i] = dest)
	    Return 1;
	End
    End
    Return 0;
End -- Func has_succ(&aut, src, dest);

--------------------------------------------------------------------------------
-- Method      : (public) Func has_the_same_succs
-- Description : Check whether given two states has the same successors.
-- Parameters  : aut - the name of the automaton.
--               v1  - the first state.
--               v2  - the second state.
-- Return Val  : TRUE if both states has the same successors, FALSE otherwise.
--------------------------------------------------------------------------------
Func has_the_same_succs(&aut, v1, v2);
    assert ((v1 > 0) & (v1 <= aut_length(aut))),
           "Trying to check succ for a not existing state.";
    assert ((v2 > 0) & (v2 <= aut_length(aut))),
           "Trying to check succ for a not existing state.";
    -- checking the length in this case is not enough, since there could 
    -- be duplications.
    For(i in 1...length(aut[__SUCC][v1]))
	If(!has_succ(aut, v2, aut[__SUCC][v1][i]))
	    Return 0;
	End
    End
    For(i in 1...length(aut[__SUCC][v2]))
	If(!has_succ(aut, v1, aut[__SUCC][v2][i]))
	    Return 0;
	End
    End
    Return 1;
End -- Func has_the_same_succs(&aut, v1, v2);

--------------------------------------------------------------------------------
-- Method      : (public) Func state_at
-- Description : Getter for a state at an index in the automata.
-- Parameters  : aut   - the name of the automaton.
--               index - the index of the state at the automata.
-- Return Val  : The state.
--------------------------------------------------------------------------------
Func state_at(&aut, index);
    assert ((index > 0) & (index <= aut_length(aut))),
           "Trying to retrieve state for a not existing state.";
    Return aut[__STATE][index];
End -- Func state_at(&aut, index);

--------------------------------------------------------------------------------
-- Method      : (public) Func rank_at
-- Description : Getter for a rank at an index in the automata.
-- Parameters  : aut   - the name of the automaton.
--               index - the index of the state at the automata.
-- Return Val  : The rank.
--------------------------------------------------------------------------------
Func rank_at(&aut, index);
    assert ((index > 0) & (index <= aut_length(aut))),
           "Trying to retrieve rank for a not existing state.";
    Return aut[__RANK][index];
End -- Func rank_at(&aut, index);

--------------------------------------------------------------------------------
-- Method      : (public) Func succ_at
-- Description : Getter for a successor at an index in the automata, at an 
--               index of the array of successors.
-- Parameters  : aut        - the name of the automaton.
--               index      - the index of the state at the automata.
--               succ_index - the index of the successor.
-- Return Val  : The successor state.
--------------------------------------------------------------------------------
Func succ_at(&aut, index, succ_index);
    assert ((index > 0) & (index <= aut_length(aut))),
           "Trying to retrieve succ for a not existing state.";
    assert ((succ_index > 0) & (succ_index <= aut[__SUCC][index][0])),
           "Trying to retrieve a not existing succ.";
    Return aut[__SUCC][index][succ_index];
End -- Func succ_at(&aut, index, succ);

--------------------------------------------------------------------------------
-- Method      : (public) To set_state_at
-- Description : Setter for a state at an index in the automata.
-- Parameters  : aut   - the name of the automaton.
--               index - the index of the state at the automata.
--               val   - the value to set.
-- Return Val  : Void.
--------------------------------------------------------------------------------
To set_state_at &aut, index, val;
    assert ((index > 0) & (index <= aut_length(aut))),
           "Trying to set value for a not existing state.";
    Let aut[__STATE][index] := val;
End -- To set_state_at &aut, index, val;

--------------------------------------------------------------------------------
-- Method      : (public) To set_rank_at
-- Description : Setter for a rank at an index in the automata.
-- Parameters  : aut   - the name of the automaton.
--               index - the index of the state at the automata.
--               val   - the value to set.
-- Return Val  : Void.
--------------------------------------------------------------------------------
To set_rank_at &aut, index, val;
    assert ((index > 0) & (index <= aut_length(aut))),
           "Trying to set rank for a not existing state.";
    Let aut[__RANK][index] := val;
End -- To set_rank_at &aut, index, val;

--------------------------------------------------------------------------------
-- Method      : (public) To set_succ_at
-- Description : Setter for a successor at an index in the automata, at an 
--               index of the array of successors.
-- Parameters  : aut        - the name of the automaton.
--               index      - the index of the state at the automata.
--               succ_index - the index of the successor.
--               val   - the value to set.
-- Return Val  : Void.
--------------------------------------------------------------------------------
To set_succ_at &aut, index, succ, val;
    assert ((index > 0) & (index <= aut_length(aut))),
           "Trying to set succ for a not existing state.";
    assert ((succ > 0) & (succ <= aut_length(aut))),
           "Trying to set succ a not existing succ.";
    Let aut[__SUCC][index][succ] := val;
End -- To set_succ_at &aut, index, succ, val;

--------------------------------------------------------------------------------
-- Method      : (public) Func pop_all_succs
-- Description : Popping the whole array of successors from a state.
-- Parameters  : aut - the name of the automaton.
--               st  - the state from which to pop a successor.
--               res - the resulting array of successors.
-- Return Val  : The array of successors.
--------------------------------------------------------------------------------
To pop_all_succs &aut, st, &res;
    assert ((st > 0) & (st <= aut_length(aut))),
           "Trying to retrieve succs for a not existing state.";
    copy res, aut[__SUCC][st];
    -- TODO: re-implement for efficiency.
    While(number_of_succ(aut, st) > 0)
	Local dummy := pop_succ(aut, st);
    End
End -- To pop_all_succs &aut, st, &res;

--------------------------------------------------------------------------------
-- Method      : (public) To print_aut
-- Description : Print the automaton.
-- Parameters  : aut - the name of the automaton.
-- Return Val  : Void.
--------------------------------------------------------------------------------
To print_aut &aut;
    Print "\n Automaton States\n\n";
    For (i in 1...aut_length(aut))
	If(aut[__STATE][i]) -- if the state hasn't been zeroed
	    Print "State ", i, " rank ",aut[__RANK][i], "\n", aut[__STATE][i],
	    "\n";
	End
    End
    Print "\n Automaton Transitions\n\n";
    For (i in 1...aut_length(aut))
	If(aut[__STATE][i]) -- if the state hasn't been zeroed
	    Print "From ", i, " to ";
	    For (j in 1...number_of_succ(aut, i))
		Print " ", aut[__SUCC][i][j];
	    End
	    Print "\n";
	End
    End
End -- To print_aut &aut;

--------------------------------------------------------------------------------
-- Method      : (public) To print_dotty_aut
-- Description : Print the automaton in a dotty format to file "automata.dot".
-- Parameters  : aut - the name of the automaton.
-- Return Val  : Void.
--------------------------------------------------------------------------------
To print_dotty_aut &aut;
    Print "\n Printing Automaton to DOTTY file name 'automaton.dot'\n\n";
    Local max_rank := 0;
    For(i in 1...aut_length(aut)) -- finding the maximum rank 
	If(max_rank < rank_at(aut, i))
	    Let max_rank := rank_at(aut, i);
	End
    End
    
    log "automata.dot";
    Print "digraph A {\n";
    Print "\trankdir=TB;\n";
    Print "\tdesc -> s1;\n";
    For (i in 1...aut_length(aut))
	If(aut[__STATE][i]) -- if the state hasn't been zeroed
	    Print "\ts", i, " [color=BLUE,width=0,height=0];\n";
	Else
	    Print "\ts", i, " [color=RED,width=0,height=0];\n";
	End
    End
    For (i in 1...aut_length(aut))
	If(aut[__STATE][i]) -- if the state hasn't been zeroed
	    For (j in 1...number_of_succ(aut, i))
		Print "\ts", i, " -> s", aut[__SUCC][i][j], ";\n";
	    End
	End
    End
    Print "}\n";
    log;
    
End -- To print_dotty_aut &aut;





--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
-------------------- the synthesis algorithm (originate from synthesis.tlv) ----
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------

--==============================================================================
--================== Realization API ===========================================
--==============================================================================
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ flags and internals. ++++++++++++++++++++++++++++++++++++++
-- Let debug  := 0;             -- general debugging flag.
-- Let doform := 0;             -- debugging with form operation.
-- Let onlyy  := 0;             -- debugging main algorithm nested y.
-- Let onlyz  := 0;             -- debugging main algorithm nested z.
-- Let syn_debug := 0;          -- debugging flag for synthesis.
-- Let construction_debug := 0; -- debugging flag for compiling construction.
-- 
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To check_realizability tsCs := 1, ++++++++++++++++
-- +++++++++++++++++                                 tsAs := 2; ++++++++++++++++
-- The main realizability method, which checks whether there exist a strategy 
-- for the system player against the environment player.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (protected) Func winm(tsCs, tsAs); ++++++++++++++++++++++++
-- Compute the winning states for the second player in the game played between 
-- two players.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To find_strategy &my_aut,       ++++++++++++++++++
-- +++++++++++++++++                           tsCs := 1,     ++++++++++++++++++
-- +++++++++++++++++                           tsAs := 2,     ++++++++++++++++++
-- +++++++++++++++++                           sig_arb := -1; ++++++++++++++++++
-- Computing a concrete strategy (an automata) according to the last game 
-- played in Func winm.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (protected) Func pop_strategy_menu(); +++++++++++++++++++++
-- This method is a pop menu which allows the user to pick a strategy priority.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To optimize_aut &aut; ++++++++++++++++++++++++++++
-- Optimizing the resulting automata.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (protected) Func compile_spec('_property, +++++++++++++++++
-- +++++++++++++++++                               VarCs,      +++++++++++++++++
-- +++++++++++++++++                               VarAs);     +++++++++++++++++
-- Given a temporal formula, create the corresponding game. According to the
-- variable division between the environment and the system. (The variable 
-- division is needed only for the cox operator in the game).
-- WARNING: currently we are only supporting the implication form of
-- specification.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (protected) To create_player '_property,  +++++++++++++++++
-- +++++++++++++++++                              env_tsn,     +++++++++++++++++
-- +++++++++++++++++                              sys_tsn,     +++++++++++++++++
-- +++++++++++++++++                              isEnvPlayer; +++++++++++++++++
-- This method takes the left or right side of the implication specification,
-- and construct a player.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (protected) To add_spec '_property,  ++++++++++++++++++++++
-- +++++++++++++++++                         env_tsn,     ++++++++++++++++++++++
-- +++++++++++++++++                         sys_tsn,     ++++++++++++++++++++++
-- +++++++++++++++++                         isEnvPlayer; ++++++++++++++++++++++
-- Adding a formula to a player.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (private) Func ntp('__pc); ++++++++++++++++++++++++++++++++
-- The mapping NTP(Non Temporal Prop): maps a parse tree of a non temporal 
-- formula to its corresponding bdd.
--
-- Let _jj := 0; -- uniqueness index
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (private) Func create_unique_tester('__p,     +++++++++++++
-- +++++++++++++++++                                     env_tsn,  +++++++++++++
-- +++++++++++++++++                                     sys_tsn); +++++++++++++
-- Given a past formula, this method construct the bdd. The difference with 
-- this method from ntp, is that it also creates a temporal tester (and new 
-- variables), in order to allow past LTL formulas.
-- WARNING: I haven't check past formula too much. It, as I remember, still
-- makes problems.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func rename_var(_p, from_var, 'to_var); ++++++++++
-- Given a propositional formula, this method changes one variable in it to 
-- other variable.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func is_past_formula('_p); +++++++++++++++++++++++
-- Check whether a given temporal formula is a pure past formula.
--
--==============================================================================
--==============================================================================
--==============================================================================


-- debugging flags.
Let debug  := 0;             -- general debugging flag.
Let doform := 0;             -- debugging with form operation.
Let onlyy  := 0;             -- debugging main algorithm nested y.
Let onlyz  := 0;             -- debugging main algorithm nested z.
Let syn_debug := 0;          -- debugging flag for synthesis.
Let construction_debug := 0; -- debugging flag for compiling construction.

--------------------------------------------------------------------------------
-- Method      : (public) To check_realizability
-- Description : The main realizability method, which checks whether there
--               exist a strategy for the system player against the 
--               environment player.
-- Parameters  : tsCs - the first transition system (i.e. environment player), 
--               default is 1.
--               tsAs - the second transition system (i.e. system player), 
--               default is 2.
-- Return Val  : Void.
--------------------------------------------------------------------------------
To check_realizability tsCs := 1, tsAs := 2;
    Print "!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!",
    "!!!!!!!!!!\n";
    Print "!!!!!!!!!! Checking If Specification Is Realizable\n";
    prepare_synt tsCs, tsAs;
    Let win := winm(tsCs, tsAs); --(nps,nqs);
    Print "!!!!!!!!!! Done -->\n";
    Let initial := I(tsCs) & I(tsAs);
    Let counter := initial & !win;
    If (counter)
	Print "!!!!!!!!!!          Specification is unrealizable.\n";
	Print counter;
	Return;
    End -- If (counter)
    Print "!!!!!!!!!!          Specification is realizable.\n";
    Print "!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!",
    "!!!!!!!!!!\n";
End -- To check_realizability;

--------------------------------------------------------------------------------
-- Method      : (protected) Func winm
-- Description : Compute the winning states for the second player in the game
--               played between two players. 
-- Parameters  : tsCs - the first transition system (i.e. environment player).
--               tsAs - the second transition system (i.e. system player).
-- Return Val  : The winning states for player tsAs.
--------------------------------------------------------------------------------
Func winm(tsCs, tsAs);
    Local x; Local y; Local z;
    Local ix := 0; Local iy := 0; Local iz := 0;
    
    Let z := 1;
    Fix(z)
	For(j in 1...nJ(tsAs))
	    Let y := 0; Let cy := 1;
	    Fix(y)
		Let start := Ji(j,tsAs) & cox(z) | cox(y);
		Let y := 0;
		For(i in 1...nJ(tsCs))
		    Let negp := !Ji(i,tsCs);
		    Let x    := z;
		    Fix(x)
			Let x := start | negp & cox(x);
			Let ix := ix + 1;
			If (debug)
			    Print "x[",i,"][",ix,"]= "; numstate(x); Print "\n";
			    If (doform) 
				form x; 
			    End
			End
		    End
		    Let x[j][cy][i] := x;   --!!!!(memory -- x iterations)!!!!
		    Let y := y | x;
		End
		Let y[j][cy] := y;          --!!!!(memory -- y iterations)!!!!
		Let cy := cy + 1;           --!!!!(counting the y's)!!!!!!!!!!
		Let iy := iy + 1;
		If (debug | onlyy)
		    Print "  y[",iy,"]= "; numstate(y); Print "\n";
		    If (doform) 
			form y; 
		    End
		End
	    End
	    Let z := y;
	    Let maxcy[j] := cy - 2;         --!!!!(memory -- maximum y)!!!!!!!
	    Let z[j] := z;                  --!!!!(memory -- z iterations)!!!!
	    Let iz := iz+1;
	    If (debug | onlyz)
		Print "    z[",iz,"]= "; numstate(z); Print "\n";
		Print "    maxcy[",j,"]= ",maxcy[j],"\n";
		If (doform) 
		    form z; 
		End
	    End
	End
    End
    Return z;
End -- Func winm(tsCs, tsAs);

--------------------------------------------------------------------------------
-- Method      : (public) To find_strategy
-- Description : Computing a concrete strategy (an automata) according to the
--               last game played in Func winm.
-- Parameters  : my_aut  - the name of the automaton.
--               tsCs    - the first transition system (i.e. environment
--               player), default is 1.
--               tsAs    - the second transition system (i.e. system player), 
--               default is 2.
--               sig_arb - the kind of strategy to be used, the default if to 
--                         pop the menu. Possible values are:
--                             ZYX ==> 3 , ZXY ==> 7 , YZX ==> 11
--                             YXZ ==> 15, XZY ==> 19, XYZ ==> 23
-- Return Val  : Void.
-- Notes       : Must be called after winm.
--------------------------------------------------------------------------------
To find_strategy &my_aut, tsCs := 1, tsAs := 2, sig_arb := -1;
    -- picking the kind of strategy.
    Local global_arb := 0;
    If ( (sig_arb != 3 ) & (sig_arb != 7 ) & (sig_arb != 11) & 
	 (sig_arb != 15) & (sig_arb != 19) & (sig_arb != 23) )
	Let global_arb := pop_strategy_menu();
    Else
	Let global_arb := sig_arb;
    End

    -- the stacks for the current state we are working on
    new st_stack; new j_stack;
    -- the automaton to be built
    new_automaton my_aut;
    
    -- Place all initial states in stack with ranking 1
    Local iset := I(tsCs) & I(tsAs); -- initial;
    While (iset)
	-- ignoring all vars other then the systems
	Local state := fsat(iset, V(tsCs) & V(tsAs));
	push st_stack, state; push j_stack ,1;
	Let iset := iset & !state;
    End
    
    -- Repeat until stack is empty
    While (length(st_stack))
	-- popping a new state to work on.
	Local p_st := pop(st_stack); Local p_j := pop(j_stack);
	-- creating a state in the automaton if not existed.
	Local new_state := mk_state(my_aut, p_st, p_j);
	
	
	-- Find minimal cy and i such that p_st \in x[p_j][cy][i]
	Local p_cy := 0;
	For (cy in reverse 1...maxcy[p_j])
	    If (p_st & y[p_j][cy])
		Let p_cy := cy;
	    End
	End
	assert (p_cy != 0), "p_st is not in z[] - at method find_strategy";
	
	Local p_i := 0;
	For (i in reverse 1...nJ(tsCs))
	    If (p_st & x[p_j][p_cy][i])
		Let p_i := i;
	    End
	End
	assert (p_i != 0),
	       "p_i is not in y[p_j][p_cy] - at method find_strategy";
	
	-- Compute set of environment successors
	Local envs := succ(T(tsCs),p_st) & V(tsAs);
	new env_succs;
	While (envs)
	    Let ones := fsat(envs, V(tsCs) & V(tsAs));
	    Let envs := envs & !ones;
	    push env_succs, (ones forsome V(tsAs));
	End
	
	
	-- For each environment successor, find a strategy successor
	For (e in 1...length(env_succs))
	    Local p_fulls := (T(tsAs) & p_st & prime(env_succs[e]));
	    Local fulls :=  unprime(p_fulls forsome (V(tsCs) & V(tsAs)));
	    Local candidate := 0;
	    Local jcand := p_j;
	    
	    Local arb := global_arb;
	    -- Mapping results for arb.
	    -- 3  --> Z[3] , Y[2] , X[1] , error[0]
	    -- 7  --> Z[7] , X[6] , Y[5] , error[4]
	    -- 11 --> Y[11], Z[10], X[9] , error[8]
	    -- 15 --> Y[15], X[14], Z[13], error[12]
	    -- 19 --> X[19], Z[18], Y[17], error[16]
	    -- 23 --> X[23], Y[22], Z[21], error[20]
	    While(null(candidate) & (arb >= 0)) -- with safe stop.
		-- a - first successor option in the strategy. (old second op)
		If ((arb = 3 ) | (arb = 7 ) | (arb = 10) | 
		    (arb = 13) | (arb = 18) | (arb = 21))
		    Local next_p_j := (p_j mod nJ(tsAs)) + 1;
		    If (p_st & Ji(p_j,tsAs))
			If (fulls & z[next_p_j])
			    Let candidate := fulls & z[next_p_j]; 
			    Let jcand     := next_p_j;
			End
		    End
		End
		
		-- b - second successor option in the strategy. (old third op)
		If ((arb = 2 ) | (arb = 5 ) | (arb = 11) | 
		    (arb = 15) | (arb = 17) | (arb = 22))
		    If (p_cy>1)
			Local look_r := 1;
			-- looking for the farest r.
			While ( is_false(fulls & y[p_j][look_r]) & (look_r < p_cy) )
			    Let look_r := look_r + 1;
			End
			
			-- a look_r with a candidate was found.
			If (fulls & y[p_j][look_r])
			    Let candidate := fulls & y[p_j][look_r];
			End
			
			-- old with no minimal 'r'.
			-- If (fulls & y[p_j][p_cy - 1])
			--     Let candidate := fulls & y[p_j][p_cy - 1]; 
			-- End
		    End
		End

		-- c - third successor option in the strategy. (old first op)
		If ((arb = 1 ) | (arb = 6 ) | (arb = 9 ) | 
		    (arb = 14) | (arb = 19) | (arb = 23))
		    If (p_st & !Ji(p_i,tsCs))
			If (fulls & x[p_j][p_cy][p_i])
			    Let candidate := fulls & x[p_j][p_cy][p_i];
			End
		    End
		End
		
		-- no successor was found yet.
		assert ((arb != 0 ) & (arb != 4 ) & (arb != 8 ) & 
		        (arb != 12) & (arb != 16) & (arb != 20)), 
		       "A state which is not winning had been found";

		Let arb := arb - 1;
	    End

	    -- TODO: think of optimization
	    --!!! While(candidate) -- option to add all
	    -- Add candidate to successors of "new_state"
	    Local size_before := aut_length(my_aut);
	    -- picking one candidate.
	    Local one := fsat(candidate, V(tsCs) & V(tsAs));
	    Let candidate := candidate & !one;
	    Local gsucc := mk_state(my_aut, one, jcand);
	    -- if never seen before this candidate
	    If(gsucc > size_before)
		push st_stack, one; push j_stack, jcand;
	    End
	    push_succ my_aut, new_state, gsucc;
	    --!!! End -- option to add all

	    -- another try to pick a candidate.
	    -- -- Add candidate to successors of "new_state"
	    -- Local size_before := aut_length(my_aut);
	    -- -- trying to find an existing candidate
	    -- Local one := 0;
	    -- While(candidate)
	    -- 	Let one := fsat(candidate, V(tsCs) & V(tsAs));
	    -- 	Let candidate := candidate & !one;
	    -- 	-- if this is the last candidate then create the state.
	    -- 	If(null(candidate))
	    -- 		Local dummy := mk_state(my_aut, one, jcand);
	    -- 	End
	    -- 	-- if one is a good candidate then ending the loop
	    -- 	If(exist_state(my_aut, one, jcand) != -1)
	    -- 		Let candidate := 0;
	    -- 	End
	    -- End
	    -- -- `one` exist, just find it.
	    -- Local gsucc := mk_state(my_aut, one, jcand);
	    -- -- if never seen before this candidate
	    -- If(gsucc > size_before)
	    -- 	push st_stack, one; push j_stack, jcand;
	    -- End
	    -- push_succ my_aut, new_state, gsucc;
	End
    End
End -- To find_strategy &my_aut, tsCs := 1, tsAs := 2;

--------------------------------------------------------------------------------
-- Method      : (protected) Func pop_strategy_menu
-- Description : This method is a pop menu which allows the user to pick a
--               strategy priority.
-- Parameters  : Void.
-- Return Val  : The return value can be one of the following:
--               ZYX ==> 3 , ZXY ==> 7 , YZX ==> 11
--               YXZ ==> 15, XZY ==> 19, XYZ ==> 23
--------------------------------------------------------------------------------
Func pop_strategy_menu();
    Local prompt := 0;
    While(prompt = 0)
        Print "\n";
	Print "????????????????????????????????????????????????????????????",
	"??????????\n";
        Print "??????????????? STRATEGY MENU ??????????????????????????????",
        "??????????\n";
        Print "????????????????????????????????????????????????????????????",
        "??????????\n";
        Print "There are few ways for constructing a strategy,\n";
        Print "depending on the preferred possible system's reaction.\n";
        Print "What is your preferred priory?\n";
        Print "1  - Z, Y, X. (naive)\n";
        Print "2  - Z, X, Y.\n";
        Print "3  - Y, Z, X.\n";
        Print "4  - Y, X, Z.\n";
        Print "5  - X, Z, Y.\n";
        Print "6  - X, Y, Z. (heuristically recommended)\n";
        Print "Where Intuitively:\n";
        Print "Z - satisfying the sys justice\n";
        Print "Y - avoid satisfying env justice in a finite number of steps\n";
        Print "X - avoid satisfying env justice\n";
        Print "????????????????????????????????????????????????????????????",
        "??????????\n";
        Print "--> ";
        Let prompt := read_num( );
        If ((prompt > 6) | (prompt < 1))
            Let prompt := 0;
            Print "Illegal command option. try again\n";
        End
    End
    -- Mapping results
    Let result := 
    (prompt = 1) ? 3  : (prompt = 2) ? 7  : (prompt = 3) ? 11 :
    (prompt = 4) ? 15 :	(prompt = 5) ? 19 :	(prompt = 6) ? 23 : -1;
    Return result;
End -- Func pop_strategy_menu();

--------------------------------------------------------------------------------
-- Method      : (public) To optimize_aut
-- Description : Optimizing the resulting automata.
-- Parameters  : aut        - the name of the automaton.
--               with_shift - whether to shift state enumaration or not. 
--                            The default is to shift.
-- Return Val  : Void.
--------------------------------------------------------------------------------
To optimize_aut &aut, with_shift := 1;
    -- repository for loops
    new loop_registry;
    
    -- self loop at the given automata.
    For(i in 1...aut_length(aut))
		If(has_succ(aut, i, i))
			push loop_registry, i;
		End
    End

    For(i in 1...aut_length(aut))
		For(j in (i + 1)...aut_length(aut))
			-- TODO: think of other optimization conditions.
			If(state_at(aut, i) & state_at(aut, j))
				assert (rank_at(aut, i) != rank_at(aut, j)), 
				"There are two exact states with the same rank";
				-- if there is a succ from on to the other
				If(has_succ(aut, i, j))
					-- if bidirectional, then faking an original loop.
					If(has_succ(aut, j, i))
						push loop_registry, j;
					End
					Print "deleting state ", j;
					If (with_shift = 1)
						Print ", all higher enumeration will be shifted",
						" down.\n";
					Else
						Print ".\n";
					End
					delete_vertex aut, j, i;
					-- updating the registry
					update_array loop_registry, j, i;
				Else
					-- adding another condition for deletion, if they are 
					-- identical in their successors.
					If(has_the_same_succs(aut, i, j))
						Print "deleting state ", j;
						If (with_shift = 1)
							Print ", all higher enumeration will be shifted",
							" down.\n";
						Else
							Print ".\n";
						End
						delete_vertex aut, j, i;
						-- updating the registry
						update_array loop_registry, j, i;
					End
				End
			End
		End
    End
    
    -- removing self loop and duplicity.
    For(i in 1...aut_length(aut))
		pop_all_succs aut, i, tmp_succs;
		While(length(tmp_succs) > 0)
			Local dummy := pop(tmp_succs);
			If ( (!has_succ(aut, i, dummy)) &
				((dummy != i) | exist_in_array(loop_registry, i)) )
				push_succ aut, i, dummy;
			End
		End
    End
    
	Print "shifting\n";
	
	If (with_shift = 1)
		shift_all_state aut;
	End
	
End -- To optimize_aut &aut;

-- completely PRIVATE method, only for readability of the optimization code.
-- this method decrease by 1 all values above val. if the val itself was enter,
-- then the alternative is registered as an original loop.
To update_array &arr, val, alt;
    For(lr in 1...length(arr))
	-- if the val itself was deleted, then change to the alt[ernative].
	If(arr[lr] = val)
	    Let arr[lr] := alt;
	End
	If(arr[lr] > val)
	    Let arr[lr] := arr[lr] - 1;
	End
    End
End -- To update_array

--------------------------------------------------------------------------------
-- Method      : (protected) Func compile_spec
-- Description : Given a temporal formula, create the corresponding game.
--               according to the variable division between the environment
--               and the system. (The variable division is needed only for the
--               cox operator in the game).
-- Parameters  : '_property - the LTL main property to synthesis.
--               VarCs      - the variable set of the environment.
--               VarAs      - the variable set of the system.
-- Return Val  : The number of TLV transition system for the 'environment', the
--               (result+1) is the number of the 'system'. In case of failure
--               the return value is -1.
-- Note        : WARNING: currently we are only supporting the implication form
--               of specification.
--------------------------------------------------------------------------------
Func compile_spec('_property, VarCs, VarAs);
    -- looking for an implication as a top operator.
    If(root(_property) == "->")
	-- If the top operator is an implication
	
	Local tsCs := new_ts();
	Local tsAs := new_ts();  
	
	set_V support(VarCs), tsCs;
	set_V support(VarAs), tsAs;
	
	
	Print "!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!",
	"!!!!!!!!!!\n";
	Print "!!!!!!!!!! Constructing the Environment player....\n";
	-- set_V support(VarCs), tsCs;
	add_disjunct_T TRUE, tsCs;
	create_player op(1, _property), tsCs, tsAs, 1;
	Print "!!!!!!!!!! Construction Done.\n";
	Print "!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!",
	"!!!!!!!!!!\n\n";
	
	Print "!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!",
	"!!!!!!!!!!\n";
	Print "!!!!!!!!!! Constructing the System player....\n";
	-- set_V support(VarAs), tsAs;
	add_disjunct_T TRUE, tsAs;
	create_player op(2, _property), tsCs, tsAs, 0;
	Print "!!!!!!!!!! Construction Done.\n";
	Print "!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!",
	"!!!!!!!!!!\n\n";
	
	set_V (V(tsCs) forsome support(VarAs)), tsCs;
	set_V (V(tsAs) forsome support(VarCs)), tsAs;
	
	Return tsCs;
    End
    
    assert FALSE, "Formula not in the expected form";
    Return -1;
End -- Func compile_spec('_property, VarCs, VarAs);

--------------------------------------------------------------------------------
-- Method      : (protected) To create_player
-- Description : This method takes the left or right side of the implication 
--               specification, and construct a player.
-- Parameters  : '_property  - the sub formula for an entire player.
--               env_tsn     - the environment TLV transition system.
--               sys_tsn     - the system TLV transition system.
--               isEnvPlayer - is this an environment or system construction.
-- Return Val  : Void.
--------------------------------------------------------------------------------
To create_player '_property, env_tsn, sys_tsn, isEnvPlayer;
    -- looking for an implication as a top operator.
    If(syn_debug) 
	Print "sub-property : ", '_property, "\n";
	Print "============================================================\n";
    End
    -- breaking into smaller conjuncts
    If(root(_property) == "&")
	create_player op(1, _property), env_tsn, sys_tsn, isEnvPlayer;
	create_player op(2, _property), env_tsn, sys_tsn, isEnvPlayer;
    Else
	If(syn_debug | construction_debug) 
	    Print "adding element: ", '_property, "\n"; 
	End
	-- if this is the smallest conjunct, then adding it to the player.
	add_spec _property, env_tsn, sys_tsn, isEnvPlayer;
    End
End -- To create_player '_property, env_tsn, sys_tsn, isEnvPlayer;

--------------------------------------------------------------------------------
-- Method      : (protected) To add_spec
-- Description : Adding a formula to a player.
-- Parameters  : '_property  - the sub formula to add to the player.
--               env_tsn     - the environment TLV transition system.
--               sys_tsn     - the system TLV transition system.
--               isEnvPlayer - is this an environment or system construction.
-- Return Val  : Void.
-- Note        : WARNING: For now the basic formula for '[]<>' must be a simple
--               propositional (i.e. not a past formula) formula, a check for
--               that is not perform!
--------------------------------------------------------------------------------
To add_spec '_property, env_tsn, sys_tsn, isEnvPlayer;
    -- if the root operator is 'always'.
    If(root(_property) == "[]")
	
	-- the first option is the regular winning condition
	If(root(op(1, _property)) == "<>")
	    -- TODO: for now we are not checking if this is a past formula. To 
	    -- support it I have to closely go over create_unique_tester.
	    Local to_add := create_unique_tester(op(1, op(1, _property)), 
	                                         env_tsn,
	                                         sys_tsn);
	    If(syn_debug | construction_debug) 
		Print "---------- Adding justice ------------------------",
		"--------->";
		form to_add; 
		Print "--------------------------------------------------",
		"----------\n"; 
	    End
	    add_J to_add, (isEnvPlayer ? env_tsn : sys_tsn);
	    Return;
	End
		
	-- the second option is the macro winning condition
	If( (root(op(1,_property)) == "->") & 
	    (root(op(2, op(1,_property))) == "<>") )
	    Let '__neg_p :=   addneg(op(1, op(1,_property)));
	    Let '__q := op(1, op(2, op(1,_property)));
	    -- equivalent macro.
	    Let 'macro :=  always(eventually(backto(__neg_p, __q)));
	    If(syn_debug) 
		Print "macro-property : ", 'macro, "\n";
		Print "==================================================",
		"==========\n";
	    End
	    add_spec macro, env_tsn, sys_tsn, isEnvPlayer;
	    Return;
	End
	
	-- TODO: for now we depend on the construction phase for deciding 
	-- whose safety this is.
	-- the third option is transitional safety
	If(isEnvPlayer)
	    If(syn_debug) 
		Print  "Transitional safety over f(V,x')\n";
	    End
	    Local safety := ntp(op(1, _property));
	    -- assert that there are no primed system variables.
	    assert is_true( set_minus( support(safety) , 
	                               support(_vars, prime(V(env_tsn))) ) ),
	           "Formula not in the expected form";
	    
	    If(syn_debug | construction_debug)
		Print "~~~~~~~~~~ Adding conjunct_T to Env ~~~~~~~~~~~~~~",
		"~~~~~~~~~>";
		form safety;
		Print "~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~",
		"~~~~~~~~~~\n";
	    End
	    add_conjunct_T safety, env_tsn;
	Else -- is System Player
	    If(syn_debug) 
		Print  "Safety specification over f(V,V')\n"; 
	    End
	    Local safety := ntp(op(1, _property));
	    If(syn_debug | construction_debug) 
		Print "~~~~~~~~~~ Adding conjunct_T to Sys ~~~~~~~~~~~~~~",
		"~~~~~~~~~>";
		form safety;
		Print "~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~",
		"~~~~~~~~~~\n";
	    End
	    add_conjunct_T safety, sys_tsn;
	End
	Return;
    End 
    -- Else and "&"
    
    -- And adding transitions and initials.
    Local p_form := ntp(_property);
    -- if there are some prime variables then goes to the transitions
    If(! is_true( set_minus( support(p_form) , support(_vars) ) ) )
	If(isEnvPlayer)
	    If(syn_debug) 
		Print  "Safety specification over f(V,x')\n"; 
	    End
	    
	    -- check that there are no primed system variables
	    assert is_true( set_minus( support(p_form) , 
	                    support(_vars, prime(V(env_tsn))) ) ), 
	           "Formula not in the expected form";

	    If(syn_debug | construction_debug) 
		Print "########## Adding conjunct_T to Env ##############",
		"#########>"; 
		form p_form; 
		Print "##################################################",
		"##########\n";
	    End
	    add_conjunct_T p_form, env_tsn;
	Else -- is System Player
	    If(syn_debug) 
		Print  "Safety specification over f(V)\n"; 
	    End
	    If(syn_debug | construction_debug) 
		Print "########## Adding conjunct_T to Sys ##############",
		"#########>"; 
		form p_form;
		Print "##################################################",
		"##########\n";
	    End
	    add_conjunct_T p_form, sys_tsn;
	End
	Return;
    End
    
    -- finally, if all failed then, goes to the initial
    If(syn_debug | construction_debug) 
	Print "iiiiiiiiii Adding initial safety iiiiiiiiiiiiiiiiiiiiiiiiiii\n"; 
    End
    Local which_tsn := isEnvPlayer ? env_tsn : sys_tsn;
    set_I (I(which_tsn) & p_form), which_tsn;
    Return;
End -- To add_spec '_property, env_tsn, sys_tsn, isEnvPlayer;

--------------------------------------------------------------------------------
-- Method      : (private) Func ntp
-- Description : The mapping NTP(Non Temporal Prop): maps a parse tree of a 
--               non temporal formula to its corresponding bdd.
-- Parameters  : '_pc - parse tree to evaluate.
-- Return Val  : BDD representation of the parse tree.
--------------------------------------------------------------------------------
Func ntp('__pc);
    --	Print '__pc, "\n";
    Case (root(__pc))
	
	-- Basic state formulas.
	"ident", "number", "TRUE","FALSE", "next", 
	"=", "!=", "<", ">", "<=", ">=", "in", "notin", "union",
	"+", "-", "*", "/" : 
	Return __pc;
	
	-- an hijack of the func for the next (due to the bug in TLV)
	"func" :
	If(op(1,__pc) == "PeqNP")
	    Return ntp(ltl_next(op(1, op(1, op(2,__pc)))))
	    = ntp(op(2, op(1, op(2,__pc))));
	End
	If(op(1,__pc) == "PeqP")
	    Return ntp(ltl_next(op(1, op(1, op(2,__pc))))) 
	    = ntp(ltl_next(op(2, op(1, op(2,__pc)))));
	End
	If(op(1,__pc) == "X")
	    Return ntp(ltl_next(op(1, op(2,__pc))));
	End
	"()" : Return prime(ntp(op(1,__pc)));
	
	
	
	-- Unary operators
	"!"     : Return ! ntp(op(1,__pc));
	-- Boolean operators
	"|"     : Return (ntp(op(1,__pc)) | ntp(op(2,__pc)));
	"&"     : Return (ntp(op(1,__pc)) & ntp(op(2,__pc)));
	"->"    : Return (ntp(op(1,__pc)) -> ntp(op(2,__pc)));
	"<->"   : Return (ntp(op(1,__pc)) <-> ntp(op(2,__pc)));
	
	-- Temporal operators.
	"<>","[]","(~)","(_)","<_>","[_]",
	"Since", "Until", "Awaits", "Backto": 
	Print "  sub-formula: ", '__pc, "\n  is out of place\n";
	assert FALSE, "Formula not in the expected form";
    End
End -- Func ntp('__pc);

-- renames the tester auxiliary variables to have a unique variables names
-- returns the unique variable.
Let _jj := 0; -- uniqueness index

--------------------------------------------------------------------------------
-- Method      : (private) Func create_unique_tester
-- Description : Given a past formula, this method construct the bdd. The
--               difference with this method from ntp, is that it also creates
--               a temporal tester (and new variables), in order to allow 
--               past LTL formulas.
-- Parameters  : '_p     - the sub formula to construct a tester to.
--               env_tsn - the environment TLV transition system.
--               sys_tsn - the system TLV transition system.
-- Return Val  : The tester main var.
-- Note        : WARNING: I haven't check past formula too much. It, as I
--               remember, still makes problems.
--------------------------------------------------------------------------------
Func create_unique_tester('__p, env_tsn, sys_tsn);
    -- for finding the vars to rename (the ones that are not in all_variables).
    Local all_variables := V(env_tsn) & V(sys_tsn);
    -- creating the tester.
    Local tester_ts := create_tester(__p, 1);
    -- making sure that this is a not future formula
    assert (nJ(tester_ts) = 0), "Can not use future LTL as a winning property.";
    
    -- while looping I'm looking for the chi too.
    Local the_chi := chi(__p); 
    Local iter_var := set_minus(V(tester_ts), support(all_variables));
    Local one_iter := FALSE;
    While( !is_true(iter_var) )
	-- taking one variable.
	Let one_iter := set_member(iter_var);
	Let iter_var := set_minus(iter_var, support(one_iter));
	
	-- new unique variable
	Let _jj := _jj + 1;
	yy[_jj] : boolean;
	
	-- renaming
	set_I rename_var(I(tester_ts), one_iter, yy[_jj]), tester_ts;
	set_V rename_var(V(tester_ts), one_iter, yy[_jj]), tester_ts;
	Local transi := rename_var(T(tester_ts), one_iter, yy[_jj]);
	add_disjunct_T TRUE, tester_ts;
	add_conjunct_T transi, tester_ts;
	
	If(support(the_chi) = one_iter)
	    Let the_chi := rename_var(the_chi, one_iter, yy[_jj]);
	End
    End
    
    -- composing the tester to the system part.
    Local comp := sync(sys_tsn, tester_ts);
    copy_ts sys_tsn, comp;
    
    If(syn_debug) 
	Print "===== tester is: ", tester_ts, " ===== comp is: ", comp, "\n"; 
    End
    delete_last_ts; -- deleting the composition TS
    delete_last_ts; -- deleting the tester TS
    
    Return the_chi;
End -- Func create_unique_tester('__p, env_tsn, sys_tsn);


--------------------------------------------------------------------------------
-- Method      : (public) Func rename_var
-- Description : Given a propositional formula, this method changes one
--               variable in it to other variable.
-- Parameters  : _p       - the formula.
--               from_var - the variable to change.
--               'to_var  - the variable to change to.
-- Return Val  : Returns the newly composed formula.
--------------------------------------------------------------------------------
Func rename_var(_p, from_var, 'to_var);
    Local ret := _p;
    
    Local all_vars := support(_p);
    Local one_var := FALSE;
    While( !is_true(all_vars) )
	Local old_all_vars := all_vars;
	
	-- this function always return the unprime version of the variable
	Let one_var := set_member(all_vars); 
	Let all_vars := set_minus(all_vars, support(one_var));
	-- checking whether this is a prime of unprime variable 
	If(is_false(all_vars & !old_all_vars))
	    Let one_var := prime(one_var);
	    Let all_vars := set_minus(all_vars, support(one_var));
	End
	
	If(is_true(support(from_var) = one_var))
	    If(syn_debug) 
		Print "changing unprime ", from_var, " to ", 'to_var, "\n"; 
	    End
	    Let ret := (ret & (one_var <-> to_var)) forsome from_var;
	End
	If(is_true(support(prime(from_var)) = one_var))
	    If(syn_debug)
		Print "changing prime ", prime(from_var), " to ", 
		prime(to_var), "\n"; 
	    End
	    Let ret := (ret & (one_var <-> prime(to_var)))
	    forsome prime(from_var);
	End
    End
    Return ret;
End -- Func rename_var(_p, from_var, 'to_var);

--------------------------------------------------------------------------------
-- Method      : (public) Func is_past_formula
-- Description : Check whether a given temporal formula is a pure past formula. 
-- Parameters  : '_p - a formula to check.
-- Return Val  : TRUE if this is a pure past formula, FALSE otherwise.
--------------------------------------------------------------------------------
Func is_past_formula('_p);
    Case (root(__pc))
	
	-- Future temporal operators.
	"Until", "Awaits", "<>", "[]" :
	Return FALSE;
	
	-- Past temporal operators.
	"(~)","(_)","<_>","[_]", "Since", "Backto": 
	Return TRUE;

	-- Simple terminals
	"func", "ident", "number", "TRUE", "FALSE", "next", "=", "!=", "<", 
	">", "<=", ">=", "in", "notin", "union", "+", "-", "*", "/" : 
	Return TRUE;
	
	-- Unary operators
	"!"     :
	Return is_past_formula(op(1,__pc));
	"()"    :
	Return is_past_formula(op(1,__pc));
	-- Boolean operators
	"|"     : 
	Return (is_past_formula(op(1,__pc)) | is_past_formula(op(2,__pc)));
	"&"     : 
	Return (is_past_formula(op(1,__pc)) | is_past_formula(op(2,__pc)));
	"->"    : 
	Return (is_past_formula(op(1,__pc)) | is_past_formula(op(2,__pc)));
	"<->"   : 
	Return (is_past_formula(op(1,__pc)) | is_past_formula(op(2,__pc)));

    End
End -- Func is_past_formula('_p);





--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
-------------------- the synthesis extention -----------------------------------
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------

--==============================================================================
--================== Extended Realization API ==================================
--==============================================================================
-- This is a new implementation to the compilation of specification. It provide
-- a general API in order to check the realizability of a given game, and to
-- synthesize and implementation to the spec. 
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ flags and internals. ++++++++++++++++++++++++++++++++++++++
-- Let debug_cnf := 0; -- cnf debugging flag.
-- Let index := 0;     -- index for allowing recursion on parse tree.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- ++++++++++++ (public) Func reduce_and_compile_game(VarCs,      ++++++++++++++
-- ++++++++++++                                       VarAs,      ++++++++++++++
-- ++++++++++++                                       'property); ++++++++++++++
-- The new reduction synthesis reduction which is less restrictive. Given a
-- temporal formula, create the corresponding game. according to the variable
-- division between the environment and the system. (The variable division is
-- needed only for the cox operator in the game).
-- 
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- ++++++++++++ (public) Func construct_game(VarCs,       ++++++++++++++++++++++
-- ++++++++++++                              VarAs,       ++++++++++++++++++++++
-- ++++++++++++                              ThetaCs,     ++++++++++++++++++++++
-- ++++++++++++                              ThetaAs,     ++++++++++++++++++++++
-- ++++++++++++                              RhoCs,       ++++++++++++++++++++++
-- ++++++++++++                              RhoAs,       ++++++++++++++++++++++
-- ++++++++++++                              '_property); ++++++++++++++++++++++
-- The most general game interface, which allows to set every possible game
-- parameter.
-- 
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- ++++++++++++ (protected) To identify_env_safety '_property, +++++++++++++++++
-- ++++++++++++                                    'res;       +++++++++++++++++
-- Identify the environment safety part of the property.
-- 
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- ++++++++++++ (protected) To identify_sys_safety '_property, +++++++++++++++++
-- ++++++++++++                                    'res;       +++++++++++++++++
-- Identify the system safety part of the property.
-- 
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- ++++++++++++ (protected) To spec2DNF '_property, &res; ++++++++++++++++++++++
-- Specification to Disjunctive Normal Form.
-- 
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- ++++++++++++ (protected) To spec2CNF '_property, &res; ++++++++++++++++++++++
-- Specification to Conjunctive Normal Form.
-- 
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- ++++++++++++ (private) To check_cnf_ltl 't; +++++++++++++++++++++++++++++++++
-- Internal testing method.
-- 
-- ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++(1)++++++
-- ++++++++++++ (private) To impl_free_ltl '__pc , &res; +++++++++++++++++++++++
-- Recursively removing implication from a formula.
-- 
-- ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++(2)++++++
-- ++++++++++++ (private) To not_normal_form '__pc , &res; +++++++++++++++++++++
-- Recursively removing negations from a formula (only negated literals are
-- allowed -- LTL operators are regarded for this method as literals too).
-- This phase was partially added to the impl_fee_ltl. this phase is performed
-- for completeness of the process, and must be applied after the spec is
-- without implications.
-- 
-- ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++(3.a)++++
-- ++++++++++++ (private) To con_normal_form '__pc , &res; +++++++++++++++++++++
-- The last phase for conjunctive normal form. it must be applied after the 
-- spec is without implications, and in a not normal form.
-- 
-- ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++(4.a)++++
-- ++++++++++++ (private) To cnf_distribute '__pc1, ++++++++++++++++++++++++++++
-- ++++++++++++                             '__pc2, ++++++++++++++++++++++++++++
-- ++++++++++++                             &res;   ++++++++++++++++++++++++++++
-- Perform the distribution of disjunct into few conjuncts.
-- 
-- ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++[3.b]++++
-- ++++++++++++ (private) To dis_normal_form '__pc , &res; +++++++++++++++++++++
-- The last phase for disjunctive normal form. it must be applied after the
-- spec is without implications, and in a not normal form.
-- 
-- ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++[4.b]++++
-- ++++++++++++ (private) To dnf_distribute '__pc1, ++++++++++++++++++++++++++++
-- ++++++++++++                             '__pc2, ++++++++++++++++++++++++++++
-- ++++++++++++                             &res;   ++++++++++++++++++++++++++++
-- Perform the distribution of conjunct into few disjuncts.
-- 
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- ++++++++++++ (public) To print_ltl '__pc , ind; +++++++++++++++++++++++++++++
-- Since there is a restriction for the printing size allowed for LTL formula
-- (a segmentation fault), this method is an implementation for printing and
-- LTL formula.
-- 
--==============================================================================
--==============================================================================
--==============================================================================

Let debug_cnf := 0; -- cnf debugging flag.
Let index := 0;     -- index for allowing recursion on parse tree.

--------------------------------------------------------------------------------
-- Method      : (public) Func reduce_and_compile_game
-- Description : The new reduction synthesis reduction which is less 
--               restrictive. Given a temporal formula, create the
--               corresponding game. according to the variable division
--               between the environment and the system. (The variable
--               division is needed only for the cox operator in the game).
-- Parameters  : 'property - the LTL main property to synthesis.
--               VarCs     - the variable set of the environment.
--               VarAs     - the variable set of the system.
-- Return Val  : The number of TLV transition system for the 'environment', the
--               (result+1) is the number of the 'system'. In case of failure
--               the return value is -1.
--------------------------------------------------------------------------------
Func reduce_and_compile_game('property, VarCs, VarAs);
    identify_env_safety property, res_e;
    identify_sys_safety res_e[3], res_s;
    Return construct_game (
    VarCs,
    VarAs, 
    res_e[1], 
    res_s[1], 
    res_e[2], 
    res_s[2], 
    res_s[3]                    );
End -- Func reduce_and_compile_game('property, VarCs, VarAs);

--------------------------------------------------------------------------------
-- Method      : (public) Func construct_game
-- Description : The most general game interface, which allows to set every
--               possible game parameter.
-- Parameters  : VarCs      - The set of environment variables.
--               VarAs      - The set of system variables.
--               ThetaCs    - The initial condition of the environment.
--               ThetaAs    - The initial condition of the system.
--               RhoCs      - The transition relation of the environment.
--               RhoAs      - The transition relation of the system.
--               '_property - the game LTL property. Suppose to hold only
--                            justice requirments.
-- Return Val  : The number of TLV transition system for the 'environment', the
--               (result+1) is the number of the 'system'. In case of failure
--               the return value is -1.
--------------------------------------------------------------------------------
Func construct_game (VarCs   , VarAs   ,
                     ThetaCs , ThetaAs ,
                     RhoCs   , RhoAs   , '_property);

    Local tsCs := new_ts();
    Local tsAs := new_ts();  
    
    Print "!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!",
    "!!!!!!!!!!\n";
    Print "!!!!!!!!!! 1. Setting the variable to both players...\n";
    set_V support(VarCs), tsCs;
    set_V support(VarAs), tsAs;
    Print "!!!!!!!!!! Done with variables.\n";
    Print "!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!",
    "!!!!!!!!!!\n\n";
    
    Print "!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!",
    "!!!!!!!!!!\n";
    Print "!!!!!!!!!! 2. Setting the initials to both players...\n";
    set_I ThetaCs, tsCs;
    set_I ThetaAs, tsAs;
    Print "!!!!!!!!!! Done with initials.\n";
    Print "!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!",
    "!!!!!!!!!!\n\n";

    If(root(_property) == "->") -- the right kind of property form
	Print "!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!",
	"!!!!!!!!!!\n";
	Print "!!!!!!!!!! 3. Setting the transitions fairness to both",
	" players...\n";
	
	Print "!!!!!!!!!!!!!!! 3.a. constructing the Environment transitions",
	" fairness requirements....\n";
	add_disjunct_T TRUE, tsCs;
	add_conjunct_T RhoCs, tsCs;
	-- _property is suppose to hold only justice requirments.
	create_player op(1, _property), tsCs, tsAs, 1;
	
	Print "!!!!!!!!!!!!!!! 3.b. constructing the System transitions",
	" fairness requirements....\n";
	add_disjunct_T TRUE, tsAs;
	add_conjunct_T RhoAs, tsAs;
	-- _property is suppose to hold only justice requirments.
	create_player op(2, _property), tsCs, tsAs, 0;
	
	set_V (V(tsCs) forsome support(VarAs)), tsCs;
	set_V (V(tsAs) forsome support(VarCs)), tsAs;
	
	Print "!!!!!!!!!! Done.\n";
	Print "!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!",
	"!!!!!!!!!!\n\n";
	
	Return tsCs;
    End
    
    assert FALSE,
           "Formula not in the expected form.";
    Return -1;
End -- Func construct_game(VarCs, VarAs, ...)

--------------------------------------------------------------------------------
-- Method      : (protected) To identify_env_safety
-- Description : identify the environment safety part of the property.
-- Parameters  : '_property - The LTL formula.
--               &res       - the result is returned by this variable, it
--                            consists result consist of three parts:
--                                res[1] - is the initial safety part of the 
--                                         specification.
--                                res[2] - is the transition safety part of the
--                                         specification.
--                                res[3] - is the actual specification for the
--                                         game. this part is in parsing ltl 
--                                         form and not in BDDs as the other
--                                         two.
--                            After this method had been the result would be:
--                            _property == res[1] \/ res[2] \/ res[3]
-- Return Val  : Void. (return by reference of res)
--------------------------------------------------------------------------------
To identify_env_safety '_property, &res;
    spec2DNF _property, _dnf_p;
    -- withdraw env disjuncts and add then to the environment TS.
End -- To identify_env_safety '_property, &res;

--------------------------------------------------------------------------------
-- Method      : (protected) To identify_sys_safety
-- Description : identify the system safety part of the property.
-- Parameters  : '_property - The LTL formula.
--               &res       - the result is returned by this variable, it
--                            consists result consist of three parts:
--                                res[1] - is the initial safety part of the 
--                                         specification.
--                                res[2] - is the transition safety part of the
--                                         specification.
--                                res[3] - is the actual specification for the
--                                         game. this part is in parsing ltl 
--                                         form and not in BDDs as the other
--                                         two.
--                            After this method had been the result would be:
--                            _property == res[1] /\ res[2] /\ res[3]
-- Return Val  : Void. (return by reference of res)
--------------------------------------------------------------------------------
To identify_sys_safety '_property, 'res;
    spec2CNF _property , cnf_p;
    -- withdraw sys disjuncts and add then to the system TS
End -- To identify_sys_safety '_property, 'res;

--------------------------------------------------------------------------------
-- Method      : (protected) To spec2DNF
-- Description : Specification to Disjunctive Normal Form.
-- Parameters  : '_property - the LTL specification.
--               &res       - the resulting DNF formula.
-- Return Val  : Void. (return by reference of res) 
--------------------------------------------------------------------------------
To spec2DNF '_property, &res;
    If(debug_cnf)
	Print "===== implication free ======================\n";
    End
    impl_free_ltl _property, _property1;
    
    If(debug_cnf)
	Print "===== not normal form =======================\n";
    End
    not_normal_form _property1, _property2;
    
    If(debug_cnf)
	Print "===== disjunctive normal form ===============\n";
    End
    dis_normal_form _property2, _property3;
    
    Let 'res := ltl(_property3);
End -- To spec2DNF '_property, &res;

--------------------------------------------------------------------------------
-- Method      : (protected) To spec2CNF
-- Description : Specification to Conjunctive Normal Form.
-- Parameters  : '_property - the LTL specification.
--               &res       - the resulting CNF formula.
-- Return Val  : Void. (return by reference of res) 
--------------------------------------------------------------------------------
To spec2CNF '_property, &res;
    If(debug_cnf)
	Print "===== implication free ======================\n";
    End
    impl_free_ltl _property, _property1;
    
    If(debug_cnf)
	Print "===== not normal form =======================\n";
    End
    not_normal_form _property1, _property2;
    
    If(debug_cnf)
	Print "===== conjunctive normal form ===============\n";
    End
    con_normal_form _property2, _property3;
    
    Let 'res := ltl(_property3);
End -- To spec2CNF '_property, &res;

--------------------------------------------------------------------------------
-- Method      : (private) To check_cnf_ltl
-- Description : Internal testing method.
-- Parameters  : Void.
-- Return Val  : Void.
--------------------------------------------------------------------------------
To check_cnf_ltl;
    Let 't := ltl(((    !r1 & 
                        ((r1 != g1) -> (r1 <-> X(r1))) & 
                        ( []<>(!(r1 & g1)) )) & 
                   (    !r2 & 
                        ((r2 != g2) -> (r2 <-> X(r2))) & 
                        ( []<>(!(r2 & g2)) )) ) 
                  -> 
                  (     ([](!(g1 & g2))) & 
                        (    !g1 & 
                             ((r1 = g1) -> (g1 <-> X(g1))) & 
                             ( []<>(r1 = g1) ) ) & 
                        (    !g2 & 
                             ((r2 = g2) -> (g2 <-> X(g2))) & 
                             ( []<>(r2 = g2) ) ) ) );
    
    Print "===== implication free ======================\n";
    Print "################################################################\n";
    impl_free_ltl t, ta;
    Print "===== not normal form =======================\n";
    Print "################################################################\n";
    not_normal_form ta, taa;
    Print "===== conjunctive normal form ===============\n";
    Print "################################################################\n";
    con_normal_form taa, taaa;
    Print "################################################################\n";
    
    --Print "===== original ==========\n";
    --Print 't, "\n";
    --Print "===== impl free =========\n";
    --Print 'ta, "\n";
    --Print "===== nnf ===============\n";
    --Print 'taa, "\n";
    --Print "===== cnf ===============\n";
    --Print 'taaa, "\n";

    --Print 'ta;
    --Print "\n**********************\n\n";
    --print_ltl ta, 0;
    --print_ltl ltop(ta), 0;
    --lprintarr ta;
    print_ltl taaa, 0;
End -- To check_cnf_ltl;

--------------------------------------------------------------------------------
-- Method      : (private) To impl_free_ltl 
-- Description : recursively removing implication from a formula.
-- Parameters  : '__pc - the original LTL formula.
--               &res  - the resulting LTL formula.
-- Return Val  : Void. (return by reference of res)
--------------------------------------------------------------------------------
To impl_free_ltl '__pc , &res;
    Local Lind1 := index;
    Local Lind2 := index + 1;
    Local Lind3 := index + 2;
    Local Lind4 := index + 3;
    Let index := index + 4;
    
    If (debug_cnf) 
	Print "\n\n======= implication free ltl ==================\n",
	'__pc, "\n";
    End
    Case (root(__pc))
	
	-- Basic state formulas.
	"ident", "number", "TRUE","FALSE", "next", "=", "!=", "<",
	">", "<=", ">=", "in", "notin", "union", "+", "-", "*", "/",
	-- Temporal operators are not handled, they are terminals in our case!!
	-- (hopefully the CNF and then DNF will eventually lead to "[]",
	-- "[]<>", or "[](... -> <>...)" or else, we do not know how to handle
	-- it at the end I'll perform a check that there is no "! any_ltl_op"). 
	"<>","[]","(~)","(_)","<_>","[_]", "Since", "Until", "Awaits", "Backto",
	"()"     :
	Let 'res := ltl(__pc);
	Return;
	
	-- Unary operators
	"!"     : 
	impl_free_ltl op(1,__pc), tmp[Lind1];
	If (root(ltl(tmp[Lind1])) == "!") -- removing double neg
	    impl_free_ltl op(1,tmp[Lind1]), tmp[Lind2];
	    Let 'res := ltl(tmp[Lind2]);
	    Return;
	Else
	    Let 'res := ltl(!tmp[Lind1]);
	    Return;
	End

	"func"   : 
	If(op(1,__pc) == "X")
	    impl_free_ltl op(1, op(2,__pc)), tmp[Lind1];
	    Let 'tmp[Lind2] := ltl(ltl_next(tmp[Lind1]));
	    Let 'res := ltl(tmp[Lind2]);
	    Return;
	End
	
	-- Binary operators
	"|"      :
	impl_free_ltl op(1,__pc), tmp[Lind1];
	If (debug_cnf)
	    Print "\ntmp[", Lind1, "] is:", 'tmp[Lind1];
	End
	
	impl_free_ltl op(2,__pc), tmp[Lind2];
	If (debug_cnf)
	    Print "\ntmp[", Lind2, "] is:", 'tmp[Lind2];
	End
	
	Let 'res := ltl(tmp[Lind1] | tmp[Lind2]);
	If (debug_cnf)
	    Print "\nres is:", 'res;
	End
	"&"      :
	impl_free_ltl op(1,__pc), tmp[Lind1];
	If (debug_cnf)
	    Print "\ntmp[", Lind1, "] is:", 'tmp[Lind1];
	End
	
	impl_free_ltl op(2,__pc), tmp[Lind2];
	If (debug_cnf)
	    Print "\ntmp[", Lind2, "] is:", 'tmp[Lind2];
	End
	
	Let 'res := ltl(tmp[Lind1] & tmp[Lind2]);
	If (debug_cnf)
	    Print "\nres is:", 'res;
	End
	"<->"    :
	impl_free_ltl op(1,__pc), tmp[Lind1];
	If (debug_cnf)
	    Print "\ntmp[", Lind1, "] is:", 'tmp[Lind1];
	End
	
	Let 'tmp[Lind2] := ltl(addneg(tmp[Lind1]));
	If (debug_cnf)
	    Print "\ntmp[", Lind2, "] is:", 'tmp[Lind2];
	End
	
	impl_free_ltl op(2,__pc), tmp[Lind3];
	If (debug_cnf)
	    Print "\ntmp[", Lind3, "] is:", 'tmp[Lind3];
	End
	
	Let 'tmp[Lind4] := ltl(addneg(tmp[Lind3]));
	If (debug_cnf)
	    Print "\ntmp[", Lind4, "] is:", 'tmp[Lind4];
	End
	
	Let 'res := ltl((tmp[Lind2] | tmp[Lind3]) & (tmp[Lind4] | tmp[Lind1])); 
	If (debug_cnf)
	    Print "\nres is:", 'res;
	End
	"->"     :
	impl_free_ltl op(1,__pc), tmp[Lind1];
	If (debug_cnf)
	    Print "\ntmp[", Lind1, "] is:", 'tmp[Lind1];
	End
	
	Let 'tmp[Lind2] := ltl(addneg(tmp[Lind1]));
	If (debug_cnf)
	    Print "\ntmp[", Lind2, "] is:", 'tmp[Lind2];
	End
	
	impl_free_ltl op(2,__pc), tmp[Lind3];
	If (debug_cnf)
	    Print "\ntmp[", Lind3, "] is:", 'tmp[Lind3];
	End
	
	Let 'res := ltl(tmp[Lind2] | tmp[Lind3]);
	If (debug_cnf)
	    Print "\nres is:", 'res;
	End
		
	-- not found
	default :
	--assert FALSE, "Un-handled operator";
	Print "\n\t*** Internal Error!!!\n";
	Print "\tDiagnostic: Un-handled operator ", 'root(__pc) ,"\n";
	abort;
    End
End -- To impl_free_ltl '__pc , &res;

--------------------------------------------------------------------------------
-- Method      : (private) To not_normal_form
-- Description : recursively removing negations from a formula (only negated 
--               literals are allowed). This phase was partially added to the
--               impl_fee_ltl. this phase is performed for completeness of the 
--               process, and must be applied after the spec is without
--               implications.
-- Parameters  : '__pc - the original LTL formula.
--               &res  - the resulting LTL formula.
-- Return Val  : Void. (return by reference of res)
--------------------------------------------------------------------------------
To not_normal_form '__pc , &res;
    Local Lind1 := index;
    Local Lind2 := index + 1;
    Local Lind3 := index + 2;
    Local Lind4 := index + 3;
    Local Lind5 := index + 4;
    Local Lind6 := index + 5;
    Local Lind7 := index + 6;
    Let   index := index + 7;
    
    If (debug_cnf)
	Print "\n\n======= not normal form ==================\n", '__pc, "\n";
    End
    Case (root(__pc))
	
	-- Basic state formulas.
	"ident", "number", "TRUE","FALSE", "next", "=", "!=", "<", 
	">", "<=", ">=", "in", "notin", "union", "+", "-", "*", "/",
	-- Temporal operators are not handled, they are terminals in our case!!
	-- (hopefully the CNF and then DNF will eventually lead to "[]",
	-- "[]<>", or "[](... -> <>...)" or else, we do not know how to handle
	-- it at the end I'll perform a check that there is no "! any_ltl_op"). 
	"<>","[]","(~)","(_)","<_>","[_]", "Since", "Until", "Awaits", "Backto",
	"()"     :
	Let 'res := ltl(__pc);
	Return;
	
	-- Unary operators
	"!"     : 
	not_normal_form op(1,__pc), tmp[Lind1];
	If (debug_cnf)
	    Print "\ntmp[", Lind1, "] is:", 'tmp[Lind1];
	End
	Case (root(tmp[Lind1]))
	    -- Basic state formulas.
	    "ident", "number", "TRUE","FALSE", "next", "=", "!=", "<", 
	    ">", "<=", ">=", "in", "notin", "union", "+", "-", "*", "/",
	    "<>","[]","(~)","(_)","<_>","[_]", "Since", "Until", "Awaits",
	    "Backto", "()"     :
	    Let 'res := ltl(__pc);
	    Return;
	    "|"      :
	    Let 'tmp[Lind2] := op(1, tmp[Lind1]);
	    Let 'tmp[Lind3] := ltl(addneg(tmp[Lind2]));
	    If (debug_cnf)
		Print "\ntmp[", Lind3, "] is:", 'tmp[Lind3];
	    End
	    
	    not_normal_form tmp[Lind3], tmp[Lind4];
	    If (debug_cnf)
		Print "\ntmp[", Lind4, "] is:", 'tmp[Lind4];
	    End
	    
	    Let 'tmp[Lind5] := op(2,tmp[Lind1]);
	    Let 'tmp[Lind6] := ltl(addneg(tmp[Lind5]));
	    If (debug_cnf)
		Print "\ntmp[", Lind6, "] is:", 'tmp[Lind6];
	    End
	    
	    not_normal_form tmp[Lind6], tmp[Lind7];
	    If (debug_cnf)
		Print "\ntmp[", Lind7, "] is:", 'tmp[Lind7];
	    End
	    
	    Let 'res := ltl(tmp[Lind4] & tmp[Lind7]);
	    If (debug_cnf)
		Print "\nres is:", 'res;
	    End
	    "&"      :
	    Let 'tmp[Lind2] := op(1,tmp[Lind1]);
	    Let 'tmp[Lind3] := ltl(addneg(tmp[Lind2]));
	    If (debug_cnf)
		Print "\ntmp[", Lind3, "] is:", 'tmp[Lind3];
	    End
	    
	    not_normal_form tmp[Lind3], tmp[Lind4];
	    If (debug_cnf)
		Print "\ntmp[", Lind4, "] is:", 'tmp[Lind4];
	    End
	    
	    Let 'tmp[Lind5] := op(2,tmp[Lind1]);
	    Let 'tmp[Lind6] := ltl(addneg(tmp[Lind5]));
	    If (debug_cnf)
		Print "\ntmp[", Lind6, "] is:", 'tmp[Lind6];
	    End
	    
	    not_normal_form tmp[Lind6], tmp[Lind7];
	    If (debug_cnf)
		Print "\ntmp[", Lind7, "] is:", 'tmp[Lind7];
	    End
	    
	    Let 'res := ltl(tmp[Lind4] | tmp[Lind7]);
	    If (debug_cnf)
		Print "\nres is:", 'res;
	    End
	    "!" : -- removing double neg
	    not_normal_form op(1,tmp[Lind1]), tmp[Lind2];
	    Let 'res := ltl(tmp[Lind2]);
	    Return;
	    
	    default:
	    -- assert FALSE,
	    --    "Un-handled operator, be sure to perform impl_free_ltl first";
	    Print "\n\t*** Internal Error!!!\n";
	    Print "\tDiagnostic: Un-handled operator ", 'root(__pc) ,"\n";
	    Print "\tSuggestion: be sure to perform the impl_free_ltl first.\n";
	    abort;
	End

	-- Binary operators
	"|"      :
	not_normal_form op(1,__pc), tmp[Lind1];
	If (debug_cnf)
	    Print "\ntmp[", Lind1, "] is:", 'tmp[Lind1];
	End
	
	not_normal_form op(2,__pc), tmp[Lind2];
	If (debug_cnf)
	    Print "\ntmp[", Lind2, "] is:", 'tmp[Lind2];
	End
	
	Let 'res := ltl(tmp[Lind1] | tmp[Lind2]);
	If (debug_cnf)
	    Print "\nres is:", 'res;
	End
	"&"      :
	not_normal_form op(1,__pc), tmp[Lind1];
	If (debug_cnf)
	    Print "\ntmp[", Lind1, "] is:", 'tmp[Lind1];
	End
	
	not_normal_form op(2,__pc), tmp[Lind2];
	If (debug_cnf)
	    Print "\ntmp[", Lind2, "] is:", 'tmp[Lind2];
	End
	
	Let 'res := ltl(tmp[Lind1] & tmp[Lind2]);
	If (debug_cnf)
	    Print "\nres is:", 'res;
	End
	
	-- not found
	default :
	-- assert FALSE,
	--    "Un-handled operator, be sure to perform impl_free_ltl first";
	Print "\n\t*** Internal Error!!!\n";
	Print "\tDiagnostic: Un-handled operator ", 'root(__pc) ,"\n";
	Print "\tSuggestion: be sure to perform the impl_free_ltl first.\n";
	abort;
    End
End -- To not_normal_form '__pc , &res;

--------------------------------------------------------------------------------
-- Method      : (private) To con_normal_form
-- Description : The last phase for conjunctive normal form. it must be applied
--               after the spec is without implications, and in a not normal
--               form.
-- Parameters  : '__pc - the original LTL formula.
--               &res  - the resulting LTL formula.
-- Return Val  : Void. (return by reference of res)
--------------------------------------------------------------------------------
To con_normal_form '__pc , &res;
    Local Lind1 := index;
    Local Lind2 := index + 1;
    Local Lind3 := index + 2;
    Let   index := index + 3;
    
    If (debug_cnf)
	Print "\n\n===== conjunctive normal form ====================\n",
	'__pc, "\n";
    End
    Case (root(__pc))
	-- Basic state formulas.
	"ident", "number", "TRUE","FALSE", "next", "=", "!=", "<", 
	">", "<=", ">=", "in", "notin", "union", "+", "-", "*", "/",
	-- Temporal operators are not handled, they are terminals in our case!!
	-- (hopefully the CNF and then DNF will eventually lead to "[]",
	-- "[]<>", or "[](... -> <>...)" or else, we do not know how to handle
	-- it at the end I'll perform a check that there is no "! any_ltl_op"). 
	"<>","[]","(~)","(_)","<_>","[_]", "Since", "Until", "Awaits", "Backto",
	"()", "!"    :
	Let 'res := ltl(__pc);
	Return;
	
	"&"      :
	con_normal_form op(1,__pc), tmp[Lind1];
	If (debug_cnf)
	    Print "\ntmp[aLind1:", Lind1, "] is:", 'tmp[Lind1];
	End
	
	con_normal_form op(2,__pc), tmp[Lind2];
	If (debug_cnf)
	    Print "\ntmp[aLind2:", Lind2, "] is:", 'tmp[Lind2];
	End
	
	Let 'res := ltl(tmp[Lind1] & tmp[Lind2]);
	If (debug_cnf)
	    Print "\nres is:", 'res;
	End
	    
	"|"      :
	con_normal_form op(1,__pc), tmp[Lind1];
	If (debug_cnf)
	    Print "\ntmp[oLind1:", Lind1, "] is:", 'tmp[Lind1];
	End
	
	con_normal_form op(2,__pc), tmp[Lind2];
	If (debug_cnf)
	    Print "\ntmp[oLind2:", Lind2, "] is:", 'tmp[Lind2];
	End
	
	cnf_distribute tmp[Lind1], tmp[Lind2], tmp[Lind3];
	If (debug_cnf)
	    Print "\ntmp[oLind3:", Lind3, "] is:", 'tmp[Lind3];
	End
	
	Let 'res := ltl(tmp[Lind3]);
	If (debug_cnf)
	    Print "\nres is:", 'res;
	End
	
	-- not found
	default :
	-- assert FALSE,
	--    "Un-handled operator, be sure to perform impl_free_ltl first";
	Print "\n\t*** Internal Error!!!\n";
	Print "\tDiagnostic: Un-handled operator ", 'root(__pc) ,"\n";
	Print "\tSuggestion: be sure to perform the impl_free_ltl first.\n";
	abort;
    End
End -- To con_normal_form '__pc , &res;

--------------------------------------------------------------------------------
-- Method      : (private) To cnf_distribute
-- Description : Perform the distribution of disjunct into few conjuncts.
-- Parameters  : '__pc1 - the formula to distribute.
--               '__pc2 - the formula conjunct with.
--               &res  - the resulting LTL formula.
-- Return Val  : Void. (return by reference of res)
--------------------------------------------------------------------------------
To cnf_distribute '__pc1, '__pc2 , &res;
    Local Lind1 := index;
    Local Lind2 := index + 1;
    Let   index := index + 2;
    
    If (debug_cnf) 
	Print "\n\n===== distributing the conjuncts ====================\n",
	'__pc1 , "\nand:\n", '__pc2, "\n";
    End
    If (root(__pc1) == "&")
	cnf_distribute op(1,__pc1), __pc2, tmp[Lind1];
	If (debug_cnf)
	    Print "\ntmp[", Lind1, "] is:", 'tmp[Lind1];
	End
	
	cnf_distribute op(2,__pc1), __pc2, tmp[Lind2];
	If (debug_cnf)
	    Print "\ntmp[", Lind2, "] is:", 'tmp[Lind2];
	End
	
	Let 'res := ltl(tmp[Lind1] & tmp[Lind2]);
	If (debug_cnf)
	    Print "\nres is:", 'res;
	End
	Return;
    End

    If (root(__pc2) == "&")
	cnf_distribute __pc1, op(1,__pc2), tmp[Lind1];
	If (debug_cnf)
	    Print "\ntmp[", Lind1, "] is:", 'tmp[Lind1];
	End
	
	cnf_distribute __pc1, op(2,__pc2), tmp[Lind2];
	If (debug_cnf)
	    Print "\ntmp[", Lind2, "] is:", 'tmp[Lind2];
	End
	
	Let 'res := ltl(tmp[Lind1] & tmp[Lind2]);
	If (debug_cnf)
	    Print "\nres is:", 'res;
	End
	Return;
    End
    
    Let 'res := ltl(__pc1 | __pc2);
    If (debug_cnf)
	Print "\nres is:", 'res;
    End
End -- To cnf_distribute '__pc1, '__pc2 , &res;

--------------------------------------------------------------------------------
-- Method      : (private) To dis_normal_form
-- Description : The last phase for disjunctive normal form. it must be applied
--               after the spec is without implications, and in a not normal
--               form.
-- Parameters  : '__pc - the original LTL formula.
--               &res  - the resulting LTL formula.
-- Return Val  : Void. (return by reference of res)
--------------------------------------------------------------------------------
To dis_normal_form '__pc , &res;
    Local Lind1 := index;
    Local Lind2 := index + 1;
    Local Lind3 := index + 2;
    Let   index := index + 3;
    
    If (debug_cnf)
	Print "\n\n===== disjunctive normal form ====================\n",
	'__pc, "\n"; 
    End
    Case (root(__pc))
	-- Basic state formulas.
	"ident", "number", "TRUE","FALSE", "next", "=", "!=", "<", 
	">", "<=", ">=", "in", "notin", "union", "+", "-", "*", "/",
	-- Temporal operators are not handled, they are terminals in our case!!
	-- (hopefully the CNF and then DNF will eventually lead to "[]",
	-- "[]<>", or "[](... -> <>...)" or else, we do not know how to handle
	-- it at the end I'll perform a check that there is no "! any_ltl_op"). 
	"<>","[]","(~)","(_)","<_>","[_]", "Since", "Until", "Awaits", "Backto",
	"()", "!"    :
	Let 'res := ltl(__pc);
	Return;
	
	"|"      :
	dis_normal_form op(1,__pc), tmp[Lind1];
	If (debug_cnf)
	    Print "\ntmp[aLind1:", Lind1, "] is:", 'tmp[Lind1];
	End
	
	dis_normal_form op(2,__pc), tmp[Lind2];
	If (debug_cnf)
	    Print "\ntmp[aLind2:", Lind2, "] is:", 'tmp[Lind2];
	End
	
	Let 'res := ltl(tmp[Lind1] | tmp[Lind2]);
	If (debug_cnf)
	    Print "\nres is:", 'res;
	End
	    
	"&"      :
	dis_normal_form op(1,__pc), tmp[Lind1];
	If (debug_cnf)
	    Print "\ntmp[oLind1:", Lind1, "] is:", 'tmp[Lind1];
	End
	
	dis_normal_form op(2,__pc), tmp[Lind2];
	If (debug_cnf)
	    Print "\ntmp[oLind2:", Lind2, "] is:", 'tmp[Lind2];
	End
	
	dnf_distribute tmp[Lind1], tmp[Lind2], tmp[Lind3];
	If (debug_cnf)
	    Print "\ntmp[oLind3:", Lind3, "] is:", 'tmp[Lind3];
	End
	
	Let 'res := ltl(tmp[Lind3]);
	If (debug_cnf)
	    Print "\nres is:", 'res;
	End
	
	-- not found
	default :
	-- assert FALSE,
	--    "Un-handled operator, be sure to perform impl_free_ltl first";
	Print "\n\t*** Internal Error!!!\n";
	Print "\tDiagnostic: Un-handled operator ", 'root(__pc) ,"\n";
	Print "\tSuggestion: be sure to perform the impl_free_ltl first.\n";
	abort;
    End
End -- To dis_normal_form '__pc , &res;

--------------------------------------------------------------------------------
-- Method      : (private) To dnf_distribute
-- Description : Perform the distribution of conjunct into few disjuncts.
-- Parameters  : '__pc1 - the formula to distribute.
--               '__pc2 - the formula disjunct with.
--               &res  - the resulting LTL formula.
-- Return Val  : Void. (return by reference of res)
--------------------------------------------------------------------------------
To dnf_distribute '__pc1, '__pc2 , &res;
    Local Lind1 := index;
    Local Lind2 := index + 1;
    Let   index := index + 2;
    
    If (debug_cnf)
	Print "\n\n===== distributing the disjuncts ====================\n",
	'__pc1 , "\nand:\n", '__pc2, "\n";
    End
    If (root(__pc1) == "|")
	dnf_distribute op(1,__pc1), __pc2, tmp[Lind1];
	If (debug_cnf)
	    Print "\ntmp[", Lind1, "] is:", 'tmp[Lind1];
	End
	
	dnf_distribute op(2,__pc1), __pc2, tmp[Lind2];
	If (debug_cnf)
	    Print "\ntmp[", Lind2, "] is:", 'tmp[Lind2];
	End
	
	Let 'res := ltl(tmp[Lind1] | tmp[Lind2]);
	If (debug_cnf)
	    Print "\nres is:", 'res;
	End
	Return;
    End

    If (root(__pc2) == "|")
	dnf_distribute __pc1, op(1,__pc2), tmp[Lind1];
	If (debug_cnf)
	    Print "\ntmp[", Lind1, "] is:", 'tmp[Lind1];
	End
	
	dnf_distribute __pc1, op(2,__pc2), tmp[Lind2];
	If (debug_cnf)
	    Print "\ntmp[", Lind2, "] is:", 'tmp[Lind2];
	End
	
	Let 'res := ltl(tmp[Lind1] | tmp[Lind2]);
	If (debug_cnf)
	    Print "\nres is:", 'res;
	End
	Return;
    End
    
    Let 'res := ltl(__pc1 & __pc2);
    If (debug_cnf)
	Print "\nres is:", 'res;
    End
End --To dnf_distribute '__pc1, '__pc2 , &res;

--------------------------------------------------------------------------------
-- Method      : (public) To print_ltl
-- Description : Since there is a restriction for the printing size allowed for
--               LTL formula (a segmentation fault), this method is an
--               implementation for printing and LTL formula.
-- Parameters  : '__pc - the LTL formula.
--               ind   - indentation for a recursive call.
-- Return Val  : Void.
--------------------------------------------------------------------------------
To print_ltl '__pc , ind;
    For (i in 1...ind) 
	Print "\t";
    End
    Local next_ind := ind + 1;

    Case (root(__pc))
	
	-- Basic state formulas.
	"ident", "number", "TRUE","FALSE", "next", 
	"=", "!=", "<", ">", "<=", ">=", "in", "notin", "union",
	"+", "-", "*", "/" : 
	Print '__pc;
	
	-- Unary operators
	"!"      : Print "!("; print_ltl op(1,__pc), 0; Print ")";
	"func"   : 
	If(op(1,__pc) == "X")
	    Print "X("; print_ltl op(1, op(2,__pc)), 0; Print ")";
	End
	"()"     : Print "()("; print_ltl op(1,__pc), 0; Print ")";
	
	-- Binary operators
	"|"      :
	Print "or( "; 
	print_ltl op(1,__pc), 0;
	Print " ,\n"; 
	print_ltl op(2,__pc), next_ind;
	Print ")";
	"&"      : 
	Print "and( "; 
	print_ltl op(1,__pc), 0;
	Print " ,\n"; 
	print_ltl op(2,__pc), next_ind; 
	Print ")";
	"<->"    : 
	Print "bimp( "; 
	print_ltl op(1,__pc), 0; 
	Print " ,\n";  
	print_ltl op(2,__pc), next_ind; 
	Print ")"; 
	 
	"->"     : 
	Print "imp( "; 
	print_ltl op(1,__pc), 0; 
	Print " ,\n";  
	print_ltl op(2,__pc), next_ind; 
	Print ")"; 
		
	-- Unary Temporal operators
	"<>"     : 
	Print "<>("; 
	print_ltl op(1,__pc), 0; 
	Print ")";
	"[]"     : 
	Print "[]("; 
	print_ltl op(1,__pc), 0; 
	Print ")";
	"(~)"    : 
	Print "(~)("; 
	print_ltl op(1,__pc), 0; 
	Print ")";
	"(_)"    : 
	Print "(_)("; 
	print_ltl op(1,__pc), 0; 
	Print ")";
	"<_>"    : 
	Print "<_>("; 
	print_ltl op(1,__pc), 0; 
	Print ")";
	"[_]"    : 
	Print "[_]("; 
	print_ltl op(1,__pc), 0; 
	Print ")";
	
	-- Binary Temporal operators
	"Since"  : 
	Print "Since( "; 
	print_ltl op(1,__pc), 0; 
	Print " ,\n"; 
	print_ltl op(2,__pc), next_ind; 
	Print ")";
	"Until"  : 
	Print "Until( "; 
	print_ltl op(1,__pc), 0; 
	Print " ,\n"; 
	print_ltl op(2,__pc), next_ind; 
	Print ")";
	"Awaits" : 
	Print "Awaits( "; 
	print_ltl op(1,__pc), 0; 
	Print " ,\n"; 
	print_ltl op(2,__pc), next_ind; 
	Print ")";
	"Backto" : 
	Print "Backto( "; 
	print_ltl op(1,__pc), 0; 
	Print " ,\n"; 
	print_ltl op(2,__pc), next_ind; 
	Print ")";

	-- not found
	default :
	-- assert FALSE,
	--    "Un-handled operator, be sure to perform impl_free_ltl first";
	Print "\n\t*** Internal Error!!!\n";
	Print "\tDiagnostic: Un-handled operator ", 'root(__pc) ,"\n";
	abort;
    End
End -- To print_ltl '__pc , ind;






--==============================================================================
--==============================================================================
--==============================================================================
--================== A Complete API Gathering ==================================
--==============================================================================
--==============================================================================
--==============================================================================
-- 
--==============================================================================
--================== General Operations API ====================================
--==============================================================================
-- 
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ flags and internals. ++++++++++++++++++++++++++++++++++++++
-- NA
-- 
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To eol; ++++++++++++++++++++++++++++++++++++++++++
-- Print a new line.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To abort; ++++++++++++++++++++++++++++++++++++++++
-- Completely ends the program.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To assert bool, 'diagnostic; +++++++++++++++++++++
-- assertion utility.
-- 
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func null(bdd); ++++++++++++++++++++++++++++++++++
-- Checking whether this is an empty bdd or not
-- 
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (protected) To prepare_synt tsCs := 1, ++++++++++++++++++++
-- +++++++++++++++++                             tsAs := 2; ++++++++++++++++++++
-- Preparing the transition systems for the game.
-- 
-- +++++++++++++++++ (public) Func cox(state); +++++++++++++++++++++++++++++++++
-- The basic step of the game. Namely, forall the first player transitions 
-- there exists a second player transition which leads into 'state'.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func exist_in_array(&arr, to_check); +++++++++++++
-- Check whether an element exists in an array.
--
--==============================================================================
--================== Automata API ==============================================
--==============================================================================
-- Utilizing the enumerated automaton using a stack technique
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ flags and internals. ++++++++++++++++++++++++++++++++++++++
-- Let __STATE := 1; - internal automata variables.
-- Let __RANK  := 2; - internal automata variables.
-- Let __SUCC  := 3; - internal automata variables.
--
-- GENERAL AUTOMATA
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To new_automaton &aut; +++++++++++++++++++++++++++
-- creating a new automaton
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To delaut &aut; ++++++++++++++++++++++++++++++++++
-- Delete an automaton.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (protected) To push_state &aut, st, rank:=-1; +++++++++++++
-- Pushing a new state to the end of the automaton. It is recommend to use 
-- mk_state.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func mk_state(&aut, state, rank); ++++++++++++++++
-- Inserting a new state and rank only if not existing, and returning its index.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func exist_state(&aut, state, rank); +++++++++++++
-- Checking if a state exists in the automata.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To push_succ &aut, src, dest; ++++++++++++++++++++
-- push a new successor to some existing state
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (protected) To pop_state &aut, &res; ++++++++++++++++++++++
-- Extract and return the last state in the automata.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (private) To shift_state &aut, st; ++++++++++++++++++++++++
-- Shifting a state in the automaton to decrease all higher enumerated state.
-- 
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (private) To shift_all_state &aut, st; +++++++++++++++++++
-- Shifting all states in the automaton to decrease all higher enumerated 
-- state. It is important to send a state to this method only after edges to
-- it has been removed.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To delete_vertex &aut, src, dest; ++++++++++++++++
-- Removing a vertex from the aut.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func pop_succ(&aut, st); +++++++++++++++++++++++++
-- Popping the last successor from a state.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To top &aut, &res; +++++++++++++++++++++++++++++++
-- Returning the last state of the automata.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func aut_length(&aut); +++++++++++++++++++++++++++
-- The number of states in this automaton.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func number_of_succ(&aut, st); +++++++++++++++++++
-- The number of successors for a state in this automaton.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func has_succ(&aut, src, dest); ++++++++++++++++++
-- Check whether there exists an edge.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func has_the_same_succs(&aut, v1, v2); +++++++++++
-- Check whether given two vertexes has the same successors.
--
--
-- GETTERS
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func state_at(&aut, index); ++++++++++++++++++++++
-- Getter for a state at an index in the automata.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func rank_at(&aut, index); +++++++++++++++++++++++
-- Getter for a rank at an index in the automata.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func succ_at(&aut, index, succ_index); +++++++++++
-- Getter for a successor at an index in the automata, at an index of the
-- array of successors.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To pop_all_succs &aut, st, &res; +++++++++++++++++
-- Popping the whole array of successors from a state.
--
--
-- SETTERS
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To set_state_at &aut, index, val; ++++++++++++++++
-- Setter for a state at an index in the automata.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To set_rank_at &aut, index, val; +++++++++++++++++
-- Setter for a rank at an index in the automata.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To set_succ_at &aut, index, succ, val; +++++++++++
-- Setter for a successor at an index in the automata, at an index of the
-- array of successors.
--
--
-- PRINTING
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To print_aut &aut; +++++++++++++++++++++++++++++++
-- Print the automaton.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To print_dotty_aut &aut; +++++++++++++++++++++++++
-- Print the automaton in a dotty format to file "automata.dot".
--
--==============================================================================
--================== Realization API ===========================================
--==============================================================================
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ flags and internals. ++++++++++++++++++++++++++++++++++++++
-- Let debug  := 0;             -- general debugging flag.
-- Let doform := 0;             -- debugging with form operation.
-- Let onlyy  := 0;             -- debugging main algorithm nested y.
-- Let onlyz  := 0;             -- debugging main algorithm nested z.
-- Let syn_debug := 0;          -- debugging flag for synthesis.
-- Let construction_debug := 0; -- debugging flag for compiling construction.
-- 
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To check_realizability tsCs := 1, ++++++++++++++++
-- +++++++++++++++++                                 tsAs := 2; ++++++++++++++++
-- The main realizability method, which checks whether there exist a strategy 
-- for the system player against the environment player.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (protected) Func winm(tsCs, tsAs); ++++++++++++++++++++++++
-- Compute the winning states for the second player in the game played between 
-- two players.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To find_strategy &my_aut,       ++++++++++++++++++
-- +++++++++++++++++                           tsCs := 1,     ++++++++++++++++++
-- +++++++++++++++++                           tsAs := 2,     ++++++++++++++++++
-- +++++++++++++++++                           sig_arb := -1; ++++++++++++++++++
-- Computing a concrete strategy (an automata) according to the last game 
-- played in Func winm.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (protected) Func pop_strategy_menu(); +++++++++++++++++++++
-- This method is a pop menu which allows the user to pick a strategy priority.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) To optimize_aut &aut; ++++++++++++++++++++++++++++
-- Optimizing the resulting automata.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (protected) Func compile_spec('_property, +++++++++++++++++
-- +++++++++++++++++                               VarCs,      +++++++++++++++++
-- +++++++++++++++++                               VarAs);     +++++++++++++++++
-- Given a temporal formula, create the corresponding game. According to the
-- variable division between the environment and the system. (The variable 
-- division is needed only for the cox operator in the game).
-- WARNING: currently we are only supporting the implication form of
-- specification.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (protected) To create_player '_property,  +++++++++++++++++
-- +++++++++++++++++                              env_tsn,     +++++++++++++++++
-- +++++++++++++++++                              sys_tsn,     +++++++++++++++++
-- +++++++++++++++++                              isEnvPlayer; +++++++++++++++++
-- This method takes the left or right side of the implication specification,
-- and construct a player.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (protected) To add_spec '_property,  ++++++++++++++++++++++
-- +++++++++++++++++                         env_tsn,     ++++++++++++++++++++++
-- +++++++++++++++++                         sys_tsn,     ++++++++++++++++++++++
-- +++++++++++++++++                         isEnvPlayer; ++++++++++++++++++++++
-- Adding a formula to a player.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (private) Func ntp('__pc); ++++++++++++++++++++++++++++++++
-- The mapping NTP(Non Temporal Prop): maps a parse tree of a non temporal 
-- formula to its corresponding bdd.
--
-- Let _jj := 0; -- uniqueness index
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (private) Func create_unique_tester('__p,     +++++++++++++
-- +++++++++++++++++                                     env_tsn,  +++++++++++++
-- +++++++++++++++++                                     sys_tsn); +++++++++++++
-- Given a past formula, this method construct the bdd. The difference with 
-- this method from ntp, is that it also creates a temporal tester (and new 
-- variables), in order to allow past LTL formulas.
-- WARNING: I haven't check past formula too much. It, as I remember, still
-- makes problems.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func rename_var(_p, from_var, 'to_var); ++++++++++
-- Given a propositional formula, this method changes one variable in it to 
-- other variable.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ (public) Func is_past_formula('_p); +++++++++++++++++++++++
-- Check whether a given temporal formula is a pure past formula.
--
--==============================================================================
--================== Extended Realization API ==================================
--==============================================================================
-- This is a new implementation to the compilation of specification. It provide
-- a general API in order to check the realizability of a given game, and to
-- synthesize and implementation to the spec. 
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- +++++++++++++++++ flags and internals. ++++++++++++++++++++++++++++++++++++++
-- Let debug_cnf := 0; -- cnf debugging flag.
-- Let index := 0;     -- index for allowing recursion on parse tree.
--
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- ++++++++++++ (public) Func reduce_and_compile_game(VarCs,      ++++++++++++++
-- ++++++++++++                                       VarAs,      ++++++++++++++
-- ++++++++++++                                       'property); ++++++++++++++
-- The new reduction synthesis reduction which is less restrictive. Given a
-- temporal formula, create the corresponding game. according to the variable
-- division between the environment and the system. (The variable division is
-- needed only for the cox operator in the game).
-- 
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- ++++++++++++ (public) Func construct_game(VarCs,       ++++++++++++++++++++++
-- ++++++++++++                              VarAs,       ++++++++++++++++++++++
-- ++++++++++++                              ThetaCs,     ++++++++++++++++++++++
-- ++++++++++++                              ThetaAs,     ++++++++++++++++++++++
-- ++++++++++++                              RhoCs,       ++++++++++++++++++++++
-- ++++++++++++                              RhoAs,       ++++++++++++++++++++++
-- ++++++++++++                              '_property); ++++++++++++++++++++++
-- The most general game interface, which allows to set every possible game
-- parameter.
-- 
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- ++++++++++++ (protected) To identify_env_safety '_property, +++++++++++++++++
-- ++++++++++++                                    'res;       +++++++++++++++++
-- Identify the environment safety part of the property.
-- 
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- ++++++++++++ (protected) To identify_sys_safety '_property, +++++++++++++++++
-- ++++++++++++                                    'res;       +++++++++++++++++
-- Identify the system safety part of the property.
-- 
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- ++++++++++++ (protected) To spec2DNF '_property, &res; ++++++++++++++++++++++
-- Specification to Disjunctive Normal Form.
-- 
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- ++++++++++++ (protected) To spec2CNF '_property, &res; ++++++++++++++++++++++
-- Specification to Conjunctive Normal Form.
-- 
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- ++++++++++++ (private) To check_cnf_ltl 't; +++++++++++++++++++++++++++++++++
-- Internal testing method.
-- 
-- ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++(1)++++++
-- ++++++++++++ (private) To impl_free_ltl '__pc , &res; +++++++++++++++++++++++
-- Recursively removing implication from a formula.
-- 
-- ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++(2)++++++
-- ++++++++++++ (private) To not_normal_form '__pc , &res; +++++++++++++++++++++
-- Recursively removing negations from a formula (only negated literals are
-- allowed -- LTL operators are regarded for this method as literals too).
-- This phase was partially added to the impl_fee_ltl. this phase is performed
-- for completeness of the process, and must be applied after the spec is
-- without implications.
-- 
-- ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++(3.a)++++
-- ++++++++++++ (private) To con_normal_form '__pc , &res; +++++++++++++++++++++
-- The last phase for conjunctive normal form. it must be applied after the 
-- spec is without implications, and in a not normal form.
-- 
-- ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++(4.a)++++
-- ++++++++++++ (private) To cnf_distribute '__pc1, ++++++++++++++++++++++++++++
-- ++++++++++++                             '__pc2, ++++++++++++++++++++++++++++
-- ++++++++++++                             &res;   ++++++++++++++++++++++++++++
-- Perform the distribution of disjunct into few conjuncts.
-- 
-- ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++[3.b]++++
-- ++++++++++++ (private) To dis_normal_form '__pc , &res; +++++++++++++++++++++
-- The last phase for disjunctive normal form. it must be applied after the
-- spec is without implications, and in a not normal form.
-- 
-- ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++[4.b]++++
-- ++++++++++++ (private) To dnf_distribute '__pc1, ++++++++++++++++++++++++++++
-- ++++++++++++                             '__pc2, ++++++++++++++++++++++++++++
-- ++++++++++++                             &res;   ++++++++++++++++++++++++++++
-- Perform the distribution of conjunct into few disjuncts.
-- 
-- +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
-- ++++++++++++ (public) To print_ltl '__pc , ind; +++++++++++++++++++++++++++++
-- Since there is a restriction for the printing size allowed for LTL formula
-- (a segmentation fault), this method is an implementation for printing and
-- LTL formula.
-- 
--==============================================================================
--==============================================================================
--==============================================================================
--==============================================================================
--==============================================================================
--==============================================================================
--==============================================================================