/*	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 "CoreachabilityAlgo.h"

namespace DESpot
{

const std::wstring CoreachabilityAlgo::cCoreachAlgoDesc = L"Coreachability Algorithm";
const std::wstring CoreachabilityAlgo::cCoreachNoMarkedStatesError = L"DES '%ls' has no marked states.";

CoreachabilityAlgo::CoreachabilityAlgo() : ReachabilityAlgo()
{
	m_description = cCoreachAlgoDesc;
}

//_________________________________________________________________________________________________

CoreachabilityAlgo::CoreachabilityAlgo(Des* inDes) : ReachabilityAlgo(inDes)
{
	m_description = cCoreachAlgoDesc;
}


//_________________________________________________________________________________________________

CoreachabilityAlgo::~CoreachabilityAlgo(void)
{
}

//_________________________________________________________________________________________________

//Returns true if all states are coreachable
bool CoreachabilityAlgo::isCoreachable() const
{
	return (m_errStateCount == 0);
}

//_________________________________________________________________________________________________

//Returns the number of non-coreachable states
DesState::Count CoreachabilityAlgo::getNonCoreachStateCount()
{
	return m_errStateCount;
}

//_________________________________________________________________________________________________

//Returns an iterator that allows the user to iterate through the non-coreachable states
CoreachabilityAlgo::StateIteratorPtr CoreachabilityAlgo::createNonCoreachStateIterator()
{
	return createUnreachStateIterator();
}

//_________________________________________________________________________________________________

//marks the given state as coreachable. 
void CoreachabilityAlgo::setCoreachable(const DesState& state)
{
	//Since the nonblocking algorithm reuses the reachability one (it just does reachability in reverse from marked states)
	//reachability in this algorithm means in fact coreachability. This method is only provided to reduce name confusion
	setReachable(state);
}

//_________________________________________________________________________________________________

//return true if the algorithm has found the state to be reachable
bool CoreachabilityAlgo::foundCoreachable(const DesState& state)
{
	//Since the nonblocking algorithm reuses the reachability one (it just does reachability in reverse from marked states)
	//reachability in this algorithm means in fact coreachability. This method is only provided to reduce name confusion
	return foundReachable(state);
}

//_________________________________________________________________________________________________

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

	if (m_inDes->getMarkedStateCount() == 0)
	{
        m_errStateCount = (DesState::Count)-1;
		throw errorMessage(cCoreachNoMarkedStatesError, m_inDes->getName());
	}

	m_errStateCount = 0;

	//In order to run the coreachability algorithm we must ensure the reachability is up-to-date in 
	//the input des, thus we need to run the reachability algorithm
	if (m_inDes->getReachableProp() == eReachableNotVerified)
	{
		ReachabilityAlgo reachAlgo(m_progress);
		m_inDes->checkReachability(reachAlgo);
	}

	//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();

	Des::StateIteratorPtr markedStateIt = m_inDes->createMarkedStateIterator();
	for(markedStateIt->first(); markedStateIt->notDone(); markedStateIt->next())
	{
		const DesState& markedState = markedStateIt->currentItem();
		if (markedState.isReachable())
		{
			//mark the state as coreachable
			setCoreachable(markedState);
			
			//add it to the pending states for further processing
			pushPending(markedState);
		}
	}	
}

//_________________________________________________________________________________________________

//create a transition iterator for inverse transitions entering the given state. 
//using DES's inverse transition function
Des::TransIteratorPtr CoreachabilityAlgo::createTransIterator(const DesState& state)
{
	return m_inDes->createStateInvTransIterator(state);
}

//_________________________________________________________________________________________________

//runs the algorithm and returns true if the the DES is non-blocking
bool CoreachabilityAlgo::runAlgo()
{
	//The non-blocking algorithm is a co-reachability algorithm which is basically a reverse rechability
	//algorithm. Thus we are reusing the reachability with two differences: 
	//	- instead of starting with the initial state we're starting with the list of MARKED states and 
	//	- instead of going through the transition function we're going through the INVERSE transition function
	return ReachabilityAlgo::runAlgo();
}

} //end of namespace DESpot
