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


	Modified by Xu Han
*/

#include "MultiCtrlAlgo.h"

namespace DESpot
{

const std::wstring MultiCtrlAlgo::cMultiCtrlAlgoDesc = L"Sync-Based Controllability Algorithm";
const std::wstring MultiCtrlAlgo::cCtrlError = L"The system is uncontrollable at state '%ls' for event '%ls'. State '%ls' of DES '%ls' is blocking the event.";

MultiCtrlAlgo::MultiCtrlAlgo(void)
{
}

//_________________________________________________________________________________________________

MultiCtrlAlgo::MultiCtrlAlgo(DesProject::DesIteratorPtr plantDesIt, DesProject::DesIteratorPtr supDesIt)
{
	addInputPlantDes(plantDesIt);
	addInputSupDes(supDesIt);
}

//_________________________________________________________________________________________________

MultiCtrlAlgo::~MultiCtrlAlgo(void)
{
}

//_________________________________________________________________________________________________

void MultiCtrlAlgo::addInputPlantDes(DesProject::DesIteratorPtr plantDesIt)
{
	for(plantDesIt->first(); plantDesIt->notDone(); plantDesIt->next())
	{
		addInputPlantDes(&plantDesIt->currentItem());
	}

}

//_________________________________________________________________________________________________

void MultiCtrlAlgo::addInputPlantDes(const Des* inPlantDes)
{
	//Make sure the same Des is not added twice
	for (unsigned int iDes = 0; iDes < m_inPlantDesSet.size(); ++iDes)
	{
		if (inPlantDes == m_inPlantDesSet[iDes])
		{
			throw EX("A DES with the same name already exists in the list of input plant DES. Cannot add.")
		}
	}
	
	m_inPlantDesSet.push_back(inPlantDes);
}

//_________________________________________________________________________________________________

void MultiCtrlAlgo::addInputSupDes(DesProject::DesIteratorPtr supDesIt)
{
	for(supDesIt->first(); supDesIt->notDone(); supDesIt->next())
	{
		addInputSupDes(&supDesIt->currentItem());
	}
}

//_________________________________________________________________________________________________

void MultiCtrlAlgo::addInputSupDes(const Des* inSupDes)
{
	//Make sure the same Des is not added twice
	for (unsigned int iDes = 0; iDes < m_inSupDesSet.size(); ++iDes)
	{
		if (inSupDes == m_inSupDesSet[iDes])
		{
			throw EX("A DES with the same name already exists in the list of input superivsor DES. Cannot add.")
		}
	}
	
	m_inSupDesSet.push_back(inSupDes);
}

//_________________________________________________________________________________________________

//If the supervisor is not controllable for the plant (isControllable() == false) this method
//provides the counter example: the state of the plant, the state of the DES and the uncontrollable event 
//being blocked by the supervisor 
const MultiCtrlAlgo::BlockedBehaviour& MultiCtrlAlgo::getUnctrlBehaviour()
{
	return m_unctrlBehaviour;
}


std::wstring MultiCtrlAlgo::formatUnctrlStateName()
{
	std::wstring closedStateName = L"(";
	for(unsigned int iSrcState = 0; iSrcState < getUnctrlBehaviour().closedState.size(); iSrcState++)
	{
	        // get DES that matches state
	        const Des*  blockingDes = m_inDesSet[iSrcState];

		if (iSrcState > 0)
		{
			closedStateName += L", ";
		}

		// prepend state by DES name so we can
		// distinguish which DES the state name
		// belongs to 
		closedStateName += blockingDes->getName() + L"/";

		closedStateName += getUnctrlBehaviour().closedState[iSrcState]->getName();
	}

	closedStateName += L")";

	return closedStateName;
}

//_________________________________________________________________________________________________


std::wstring MultiCtrlAlgo::prepareErrorDescription()
{

	std::wstring closedStateName = formatUnctrlStateName();
	return errorMessage(cCtrlError, closedStateName, 
		                            getUnctrlBehaviour().exitEvent->getName(), 
									getUnctrlBehaviour().blockingState->getName(), 
									getUnctrlBehaviour().blockingDes->getName());
}

//_________________________________________________________________________________________________

void MultiCtrlAlgo::onEventBlocked(short eventId,  SrcStateTuple& srcStateTuple, short iSrc)
{
	//if the iSrc des is a supervisor and blocked event is not controllable ==> 
	//uncontrollable at state srcStateTuple for event blocked event
	if (iSrc>= m_supCriteria  && (tranMap->isControllable(eventId) == false))
	{

	      const Des*		blockingDes = m_inDesSet[iSrc];
	      short state_id=srcStateTuple[iSrc];
	      const DesState& blockingState = blockingDes->getState(state_id);

		DesEvent* blockedEvent=tranMap->getEvent(eventId);
		StateTuple *tmp=new StateTuple(m_inDesSet.size());

	    for(int i=0;i<(int)m_inDesSet.size();i++)
		{
		    short theid= srcStateTuple[i];
		    (*tmp)[i]=&(m_inDesSet[i]->getState((unsigned long long)theid));

	    }

		//Added by zain for counter example generation
			if(isfirsterror==true)
			{
				for(int i=0;i<(int)m_inDesSet.size();i++)
				{
				  this->CE_tuplemap[m_inDesSet[i]->getName()]=srcStateTuple[i];
				}				
				isfirsterror=false;
			}
		throw CtrlException(blockingDes, &blockingState, *blockedEvent, *tmp);
	}
}

//_________________________________________________________________________________________________

void MultiCtrlAlgo::prepareRun()
{
	
	if (m_inDesSet.empty())
	{
		for (unsigned int iDes = 0; iDes < m_inPlantDesSet.size(); ++iDes)
		{
			addInputDes(m_inPlantDesSet[iDes]);
		}
		//m_supCriteria.setStartSupIndex(m_inPlantDesSet.size());
		m_supCriteria=m_inPlantDesSet.size();

		for (unsigned int iDes = 0; iDes < m_inSupDesSet.size(); ++iDes)
		{
			addInputDes(m_inSupDesSet[iDes]);
		}
	}

	//1) first add the plantDes and supDes into the DesSet, and mark which one is the plant and which one is the sup
	newSyncAlgo::prepareRun();

	m_unctrlBehaviour.clear();
	m_isControllable = false;
   //throw EX("controll algo");
	


}

//_________________________________________________________________________________________________

bool MultiCtrlAlgo::runAlgo()
{
	try
	{//throw EX("controll algo");
		newSyncAlgo::runAlgo();
		
		return m_isControllable = true; // "=" is intentional
	}
	catch(CtrlException& ctrlEx)
	{
		m_unctrlBehaviour.set(ctrlEx.unctrlSupDes, ctrlEx.unctrlSupState, ctrlEx.srcStateTuple, &ctrlEx.blockedEvent);
		
		std::wstring error = prepareErrorDescription();
		addError(error);


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

}
