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

namespace DESpot
{

const std::wstring CtrlStdAlgo::cCtrlAlgoDesc = L"Standard Controllability Algorithm";

CtrlStdAlgo::CtrlStdAlgo(void) : 
		m_plantDes(null),
		m_supDes(null),
		m_eventTransl(true)
{
	m_description = cCtrlAlgoDesc;
}

//_________________________________________________________________________________________________

CtrlStdAlgo::CtrlStdAlgo(Des* plantDes, Des* supDes) :
		m_plantDes(plantDes),
		m_supDes(supDes),
		m_eventTransl(plantDes, m_supDes, false /*allow untranslated entries*/)
{
	m_description = cCtrlAlgoDesc;	
}

//_________________________________________________________________________________________________

CtrlStdAlgo::~CtrlStdAlgo(void)
{
}

//_________________________________________________________________________________________________

void CtrlStdAlgo::setPlantDes(Des* plantDes)
{
	m_plantDes = plantDes;
	
	//set the plant DES as the source of translation so we can translates it's events into supervisor
	//events
	m_eventTransl.addInputDes(m_plantDes);

	m_isControllable = false;
}

//_________________________________________________________________________________________________

void CtrlStdAlgo::setSupervisorDes(Des* supDes)
{
	m_supDes = supDes;

	//set the supervisor DES as the owner of the translated events
	m_eventTransl.setOutputDes(m_supDes);

	m_isControllable = false;
}

//_________________________________________________________________________________________________

//If the supervisor is not controllable for the plant (isControllable() == false) this method
//provides the uncontrolled behaviour information: the state of the plant, the state of the supervisor
//and the uncontrollable event being blocked by the supervisor 
const CtrlStdAlgo::CtrlBehaviour& CtrlStdAlgo::getUnctrlBehaviour()
{
	if (isControllable())
	{
		throw EX("The supervisor is controllable for the plant. There is no uncontrolled behaviour");
	}

	return m_unctrlBehaviour;
}

//_________________________________________________________________________________________________

//Returns a detailed counter example in the form of a trace of (plant-state, sup-state, event) tuples that
//lead to the uncontrolled behaviour
const CtrlStdAlgo::CounterExample& CtrlStdAlgo::getCounterExample()
{
	if (isControllable())
	{
		throw EX("The supervisor is controllable for the plant. There is no counterexample");
	}
	
	if (m_counterExample.empty())
	{
		//Construct the counter-example by traversing the "found states" data starting with the uncontrolled behaviour
		CtrlBehaviour ctrlBehav = m_unctrlBehaviour;
		while(ctrlBehav.plantState != null)
		{
			m_counterExample.push_front(ctrlBehav);

			//advanced to previous behaviour
			ctrlBehav = getPreviousBehaviour(ctrlBehav);
		}
	}

	return m_counterExample;
}

//_________________________________________________________________________________________________

Des::TransIteratorPtr CtrlStdAlgo::createTransIterator(const DesState* plantState)
{
	return m_plantDes->createStateTransIterator(*plantState);
}

//_________________________________________________________________________________________________

//retrives a pending closed loop state out of the pending queue
CtrlStdAlgo::ClosedState CtrlStdAlgo::popPending()
{
	ClosedState pendingState = m_pendStates.front();
	m_pendStates.pop_front();
	return pendingState;	
}

//_________________________________________________________________________________________________

//adds the given state to the pending state for futher processing
void CtrlStdAlgo::pushPending(ClosedState& state, const DesEvent* leadEvent, const ClosedState& parentState)
{
	//first mark the state as found. Together with the found information we save how the state was found: the 
	//state and event it was discovered from. This is useful to trace the counter example
	markFound(state, leadEvent, parentState);

	//add the state to the list of pending states
	m_pendStates.push_back(state);
}

//_________________________________________________________________________________________________

//returns true if the givve closed loop has been found before
bool CtrlStdAlgo::found(ClosedState& state)
{
	ClosedStateFindMap& foundSupStates = m_foundStates[state.plantState->getId()] ;
	return (foundSupStates.find(state.supState->getId()) != foundSupStates.end());
}

//_________________________________________________________________________________________________

//marks the given state as found
void CtrlStdAlgo::markFound(ClosedState& state, const DesEvent* leadEvent,const ClosedState& parentState)
{
	#ifdef _DEBUG_DESPOT
		assert(found(state) == false);
	#endif

	ClosedStateFindMap& foundSupStates = m_foundStates[state.plantState->getId()];

	foundSupStates[state.supState->getId()] = ParentInfo(parentState, leadEvent);
}

//_________________________________________________________________________________________________

//Obtain the previous behaviour in the system given one
CtrlStdAlgo::CtrlBehaviour CtrlStdAlgo::getPreviousBehaviour(ClosedState& state)
{
	#ifdef _DEBUG_DESPOT
		assert(found(state));
	#endif

	ClosedStateFindMap& foundSupStates = m_foundStates[state.plantState->getId()];
	ParentInfo& parentInfo = foundSupStates[state.supState->getId()];
	
	return CtrlBehaviour(parentInfo.parentState, parentInfo.exitEvent); 
}

//_________________________________________________________________________________________________

void CtrlStdAlgo::prepareRun()
{
	startAlgo();

	//reset the algorithm output in case it was run before
	m_foundStates.clear();
	m_foundStates.resize(m_plantDes->getLastUsedStateId() + 1);
	m_pendStates.clear();
	m_unctrlBehaviour.clear();
	m_counterExample.clear();
	m_isControllable = false;

	//compute the translation between plant and supervisor events
	m_eventTransl.computeTranslation();

	//initialize the pending list
	ClosedState state(&m_plantDes->getInitialState(), &m_supDes->getInitialState());
	pushPending(state);
}

//_________________________________________________________________________________________________

bool CtrlStdAlgo::runAlgo()
{
	ProgressUpdater updater(m_progress);

	//Start with the initial state of the plant and supervisor
	prepareRun();
	
	while(m_pendStates.empty() == false)
	{		
		ClosedState state = popPending();

		//go through all the events leaving the plant state
		Des::TransIteratorPtr plantTransIt = createTransIterator(state.plantState);
		for(plantTransIt->first(); plantTransIt->notDone(); plantTransIt->next())
		{
			const DesTransition& plantTrans = plantTransIt->currentItem();
			const DesEvent* plantEvent = &plantTrans.event();
			
			//assume the supervisor doesn't care about this event; if the supervisor 
			const DesState* supNextState = state.supState; 

			//check if the event  is allowed by the supervisor
			const DesEvent* supEvent = null;
			bool eventControlled = m_eventTransl.translate(plantEvent, supEvent);
			bool eventAllowed = eventControlled ? m_supDes->transExists(state.supState, supEvent, supNextState) : true;
			
			if (eventAllowed)
			{			
				//the plant event is allowed by the supervisor so process the next state
				ClosedState nextState(&plantTrans.toState(), supNextState);
				if (found(nextState) == false)
				{
					pushPending(nextState, plantEvent, state);
				}
			}
			else if (plantEvent->isControllable() == false)
			{
				//the supervisor is blocking an uncontrollable event thus it is not controllable
				m_unctrlBehaviour.set(state.plantState, state.supState, plantEvent);															

				finish();

				return m_isControllable = false;  // = is intentional
			}
		}

		updateProgress();
	}

	//If we got here it means all uncontrollable events were permitted by the supervisor 
	return m_isControllable = true; // = is intentional 
}

} //end of namespace DESpot
