/*	Author: Magdin Stoica
	Supervisor: Dr. Ryan Leduc
	
	Project created in conformity with the requirements for the Degree of Master of Engineering in Software Engineering, 
	Computing and Software Department, 
	McMaster University
	2003 - 2007
*/

#pragma once

#include <vector>
#include <deque>
#include <list>
#include <memory>

#include "DesAlgo.h"
#include "Des.h"
#include "DesState.h"
#include "ListIterator.h"

namespace DESpot
{
	class DesStatePool;

	/* 
	*/
	class ReachabilityAlgo : public DesAlgo
	{
		//Types
		public:
			typedef Iterator<DesState*, const DesState*> StateIterator;
			typedef std::auto_ptr<StateIterator> StateIteratorPtr;

		public:
			ReachabilityAlgo(bool checkIntegrity = false);
			ReachabilityAlgo(UpdateProgressInterface* progress, bool checkIntegrity = false);
			ReachabilityAlgo(const Des* inDes, bool checkIntegrity = false);
			virtual ~ReachabilityAlgo(void);

			void setInputDes(const Des* des);

			//this method is called by the input DES itself that provides its state pool
			//so the algorithm can save the reachability information in the states in the pool
			//Note that nobody but the Des has access to its state pool and the algorithm only
			//receives a constant DES which means it can't change it
			void saveReachability(StatePool* statePool);

		public:
			//runs the algorithm and returns true if the the DES is reachable
			virtual bool runAlgo();

			bool isReachable() const;

			//Returns the number of unreachable states
			DesState::Count getUnreachStateCount();

			//Returns an iterator that allows the user to iterate through the unreachable states
			StateIteratorPtr createUnreachStateIterator();

		protected:
			//Prepares the informaiton necessary for the algorithm to run
			virtual void prepareRun();

			//Pushes the given state into the pending queue for further processing
			virtual void pushPending(const DesState& state);

			//Pops the oldest pending state for processing
			virtual const DesState& popPending();

			//marks the given state as reachable. If the user requested it sets the reachability
			//informaiton in the state itself through its owner DES
			virtual void setReachable(const DesState& state);

			//return true if the algorithm has found the state to be reachable
			bool foundReachable(const DesState& state);

			//returns true if the algorithm found the state. In the case of the Reachability algorithm
			//it is equivalent to foundReachable but sub-classes (e.g. Nonblocking) might interpret it differently
			virtual bool found(const DesState& state);

			//create a transition iterator for transition exiting the given state. Since
			//the iterator decides the direction and order of DES traversal other algorithms
			//can override to create a differnt iterator. 
			virtual Des::TransIteratorPtr  createTransIterator(const DesState& state);

			//check if can use the transition to reach other states
			virtual bool canUseTransition(const DesTransition& trans);

			//Counts the erroneous states (in this case unreachable) by testing each state of the DES
			//against the "found() == false" predicate. The result is returned and also saved in m_errStateCount
			virtual DesState::Count countErroneousStates();

		public:
			//The input DES whose reachability is being checked
			const Des* m_inDes;
			
			//The list of states found by the algorithm but not yet processed
			std::deque<const DesState*> m_pendingStates;
			
			//A vector holding the reachability status of each state in DES. The index in this vector
			//represents the ID of the state whose reachability is recorded
			std::vector<bool> m_desReachStatus;

			//When initialized by the DES itself, the algorithm saves the reachability status of every state
			//in the state itself
			StatePool* m_statePool;

			//the number of erroneous states
			DesState::Count m_errStateCount;

			//The list of unreachable states	
			typedef std::list<const DesState*> UnreachStateList;
			typedef UnreachStateList::iterator UnreachStateIt;
			typedef ListIterator UnreachStateIterator;
			UnreachStateList m_unreachStateList;

			//true if the algorithm must check the integrity of the input components before running the algorithm
			bool m_checkDesIntegrity;

		private:
			static const std::wstring cReachabilityAlgoDesc;
			static const std::wstring cReachIntegError;
	};

} //end of namespace DESpot
