/*	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
*/

#include "ReachabilityAlgo.h"
#include "DesStatePool.h"

namespace DESpot
{

const std::wstring ReachabilityAlgo::cReachabilityAlgoDesc = L"Reachability Algorithm";
const std::wstring ReachabilityAlgo::cReachIntegError = L"Input DES '%ls' is either not valid or not verified to be valid.";

//_________________________________________________________________________________________________

ReachabilityAlgo::ReachabilityAlgo(bool checkIntegrity) : DesAlgo(cReachabilityAlgoDesc), 
			m_checkDesIntegrity(checkIntegrity),
			m_inDes(null), 
			m_statePool(null),
            m_errStateCount((DesState::Count)-1)
{
}

//_________________________________________________________________________________________________

ReachabilityAlgo::ReachabilityAlgo(UpdateProgressInterface* progress, bool checkIntegrity) : DesAlgo(progress, cReachabilityAlgoDesc), 
			m_checkDesIntegrity(checkIntegrity),
			m_inDes(null), 
			m_statePool(null),
                        m_errStateCount((DesState::Count)-1)
{
}

//_________________________________________________________________________________________________

ReachabilityAlgo::ReachabilityAlgo(const Des* inDes, bool checkIntegrity) : DesAlgo(cReachabilityAlgoDesc), 
			m_checkDesIntegrity(checkIntegrity),
			m_inDes(inDes),
			m_statePool(null),
                        m_errStateCount((DesState::Count)-1)
{
}

//_________________________________________________________________________________________________

ReachabilityAlgo::~ReachabilityAlgo(void)
{
}

//_________________________________________________________________________________________________

void ReachabilityAlgo::setInputDes(const Des* des)
{
	m_inDes = des;
        m_errStateCount = (DesState::Count)-1;
}

//_________________________________________________________________________________________________

//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 ReachabilityAlgo::saveReachability(StatePool* statePool)
{
	m_statePool = statePool;
}

//_________________________________________________________________________________________________

bool ReachabilityAlgo::isReachable() const
{
	return m_errStateCount == 0;
}

//_________________________________________________________________________________________________

//Returns the number of blocking states
DesState::Count ReachabilityAlgo::getUnreachStateCount()
{
	return m_errStateCount;
}

//_________________________________________________________________________________________________

//Returns an iterator that allows the user to iterate through the unreachable states
ReachabilityAlgo::StateIteratorPtr ReachabilityAlgo::createUnreachStateIterator()
{
	//make sure the list of unreachable states is clear so we can compute it from scratch
	m_unreachStateList.clear();

	if (isReachable() == false)
	{
		//Go thourgh the list of states and find out which ones were not reachable
		Des::StateIteratorPtr desStateIt = m_inDes->createStateIterator();
		for(desStateIt->first(); desStateIt->notDone(); desStateIt->next())
		{
			const DesState& state = desStateIt->currentItem();
			if (found(state) == false)
			{
				m_unreachStateList.push_back(&state);
			}
		}
	}
	
	//create the iterator so the caller can iterator through them
	UnreachStateIterator* stateIt = new UnreachStateIterator(m_unreachStateList);
	return StateIteratorPtr(stateIt);
}

//_________________________________________________________________________________________________

//Pushes the given state into the pending queue for further processing
void ReachabilityAlgo::pushPending(const DesState& state)
{
	m_pendingStates.push_back(&state);
}

//_________________________________________________________________________________________________

//Pops the oldest pending state for processing
const DesState& ReachabilityAlgo::popPending()
{
	const DesState* state = m_pendingStates.front();
	m_pendingStates.pop_front();
	return *state;
}

//_________________________________________________________________________________________________

void ReachabilityAlgo::setReachable(const DesState& state)
{
	m_desReachStatus[state.getId()] = true;

	if (m_statePool)
	{
		m_statePool->getState(state.getId())->setReachable();
	}
}

//_________________________________________________________________________________________________

bool ReachabilityAlgo::foundReachable(const DesState& state)
{
	return m_desReachStatus[state.getId()];
}

//_________________________________________________________________________________________________

//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
bool ReachabilityAlgo::found(const DesState& state)
{
	return foundReachable(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. 
Des::TransIteratorPtr ReachabilityAlgo::createTransIterator(const DesState& state)
{
	return m_inDes->createStateTransIterator(state);
}

//_________________________________________________________________________________________________

bool ReachabilityAlgo::canUseTransition(const DesTransition& /*trans*/)
{
	//in the basic reach algo we can use any transition
	return true;
}

//_________________________________________________________________________________________________

//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
DesState::Count ReachabilityAlgo::countErroneousStates()
{
	//Go thourgh the list of states and count the erroneous states
	m_errStateCount = 0;
	
	Des::StateIteratorPtr desStateIt = m_inDes->createStateIterator();
	for(desStateIt->first(); desStateIt->notDone(); desStateIt->next())
	{
		const DesState& state = desStateIt->currentItem();
		if (found(state) == false)
		{
			m_errStateCount++;
		}
	}

	return m_errStateCount;
}

//_________________________________________________________________________________________________

//Prepares the information necessary for the algorithm to run
void ReachabilityAlgo::prepareRun()
{
	startAlgo();

	m_errStateCount = 0;

	if (m_checkDesIntegrity)
	{
		//make sure that all input DES are valid
		if (m_inDes->getIntegrity() != eIntegYes)
		{			
			throw errorMessage(cReachIntegError, m_inDes->getName());
		}		
	}

	//initialize the des reability status vector to false = not reachable which means
	//we start by assuming that none of the states are reachable
	m_desReachStatus.resize(m_inDes->getLastUsedStateId()  + 1, false);
	m_pendingStates.clear();

	if (m_statePool)
	{
		//reset the reachability in the DES as well since we are supposed to save the reachable states as we find them
		m_statePool->resetReachability(eReachableNo);
	}

	const DesState& initState = m_inDes->getInitialState();
	setReachable(initState);

	//start the reachability search with the initial state
	pushPending(m_inDes->getInitialState());
}


//_________________________________________________________________________________________________

//runs the algorithm and returns true if the the DES is reachable
bool ReachabilityAlgo::runAlgo()
{
	ProgressUpdater updater(m_progress);

	//initialize the list of pending states we start with, in the case of reachability is the initial state
	//which is by definition reachable
	prepareRun();

	//check the easy way out. If the all states were marked reached by definition then it's reachable
	if (m_pendingStates.size() == m_inDes->getStateCount())
		return true;
	
	//as long as there are pending states keep processing to find out their reachability
	while(m_pendingStates.empty() == false)
	{
		const DesState& crtState = popPending();

		//go through all the transitions out of the current state and process each "next state"
		Des::TransIteratorPtr  transIt = createTransIterator(crtState);
		for(transIt->first(); transIt->notDone(); transIt->next())
		{
			const DesTransition& crtTrans = transIt->currentItem();
			if (canUseTransition(crtTrans) == false)
				continue; //can't use this transition; must reach somehowelse

			const DesState& nextState = crtTrans.toState();
			
			//check if the algorithm found the next state to be reachable
			if (foundReachable(nextState) == false)
			{				
				//this is the first we see this state; mark it as reachable a
				setReachable(nextState);
				
				//add it to pending so we can process its transitions to find more states
				pushPending(nextState);
			}
		}

		updateProgress();
	}

	//no more pending states, see if we went through all
	return (countErroneousStates() == 0);
}

} //end of namespace DESpot
