/*	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 "IConsistAnsAcceptAlgo.h"
#include "DesSubsystem.h"
#include "DesInterface.h"

namespace DESpot
{

const std::wstring IConsistAnsAcceptAlgo::cIConsistAnsAcceptAlgoDesc = L"IConsist Answer Accept Algo";

const std::wstring IConsistAnsAcceptAlgo::cIConsistAcceptError = L"The high-level '%ls' does not accept event \
'%ls' at state: (%ls).  State '%ls' of DES '%ls' is blocking the event.";

const std::wstring IConsistAnsAcceptAlgo::cIConsistAnsAcceptError = L"The high-level '%ls' does not accept answer event \
'%ls' at state: (%ls).  State '%ls' of DES '%ls' is blocking the event.";

const std::wstring IConsistAnsAcceptAlgo::cIConsistLdAnsAcceptError = L"The high-level '%ls' does not accept low-data event \
'%ls' at state: (%ls).  State '%ls' of DES '%ls' is blocking the event.";

//_________________________________________________________________________________________________

IConsistAnsAcceptAlgo::IConsistAnsAcceptAlgo(DesHierProject& project) : m_project(project)
{
	m_description = cIConsistAnsAcceptAlgoDesc;
	m_checkDesIntegrity = false;
}

//_________________________________________________________________________________________________

IConsistAnsAcceptAlgo::~IConsistAnsAcceptAlgo(void)
{
}

//_________________________________________________________________________________________________

DesHierProject& IConsistAnsAcceptAlgo::getInputProject()
{
	return m_project;
}

//_________________________________________________________________________________________________

bool IConsistAnsAcceptAlgo::allAnsEventsAccepted()
{
	return MultiCtrlAlgo::isControllable();
}

//_________________________________________________________________________________________________

std::wstring IConsistAnsAcceptAlgo::getError()
{
	//Create the closed state name
		std::wstring closedStateName;
	for(unsigned int iSrcState = 0; iSrcState < MultiCtrlAlgo::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 += MultiCtrlAlgo::getUnctrlBehaviour().closedState[iSrcState]->getName();
	}



	std::wstring highLevelName = m_project.getRootSubsys().getName();
	std::wstring blockEventName = MultiCtrlAlgo::getUnctrlBehaviour().exitEvent->getName();
	EventType    blockEventType = MultiCtrlAlgo::getUnctrlBehaviour().exitEvent->getType();
	std::wstring blockingStateName = MultiCtrlAlgo::getUnctrlBehaviour().blockingState->getName();
	std::wstring blockingDesName = MultiCtrlAlgo::getUnctrlBehaviour().blockingDes->getName();
	
	switch(blockEventType)
	{
		case eAnswerEvent:
			//return errorMessage(cIConsistAnsAcceptError, blockEventName, closedStateName, blockingStateName, blockingDesName);		
			return errorMessage(cIConsistAnsAcceptError, highLevelName, blockEventName, closedStateName, 
											   blockingStateName, blockingDesName);	
		case eLDataEvent:
			return errorMessage(cIConsistLdAnsAcceptError, highLevelName,blockEventName, closedStateName, blockingStateName, blockingDesName);		

		default:
			//it should be either answer or Low Data
			assert(false);
			return errorMessage(cIConsistAcceptError, highLevelName,blockEventName, closedStateName, blockingStateName, blockingDesName);		
	}
	
}


bool IConsistAnsAcceptAlgo::isHighLevelDes(const Des* pDes, short iSrc)
{
	//Remove unused warning in release
	pDes = pDes;

	//all high-level des were added as "supervisors"; also des should be a subsystem des
	if (iSrc>= m_supCriteria)
	{
		assert(pDes->getType() == eSubsystemDes);
		return true;
	}

	return false;
}

//_________________________________________________________________________________________________

//Called when the eligible events are computed out of the given source state tuple AND an event is blocked
//by one of the states in the tuple. iSrc represents the index of the DES that contains the state that 
//doesn't allow the event (it doesn't have a transition that exist the state with that event)
void IConsistAnsAcceptAlgo::onEventBlocked(short eventId,  SrcStateTuple& srcStateTuple, short iSrc)
{
	const Des*	blockingDes = m_inDesSet[iSrc];





    DesEvent* blockedEvent=tranMap->getEvent(eventId);
	
	if (isHighLevelDes(blockingDes, iSrc) && ((blockedEvent->getType() == eAnswerEvent) || 
											  (blockedEvent->getType() == eLDataEvent)))
	{
			short state_id=srcStateTuple[iSrc];
	        const DesState& blockingState = blockingDes->getState(state_id);

			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)
			{
				for(int i=0;i<(int)m_inDesSet.size();i++)
				{
					this->CE_tuplemap[m_inDesSet[i]->getName()]=srcStateTuple[i];					
				}
				ErrorSubSystem=&m_project.getRootSubsys();				
				this->setIFailureType(AnsAcptAlgo);
				isfirsterror=false;
				IsFirstErrorSubSystem=false;
			}
			
		throw CtrlException(blockingDes, &blockingState, *blockedEvent, *tmp);
	}
}

//_________________________________________________________________________________________________

void IConsistAnsAcceptAlgo::prepareRun()
{
	//add all the interface DES as "plant DES" in the ctrl algorithm as they are the ones that
	//enable the answer events
	DesHierProject::InterfIteratorPtr interfIt = m_project.createInterfIterator();
	for(interfIt->first(); interfIt->notDone(); interfIt->next())
	{
		const DesInterface& interf = interfIt->currentItem();

		if (interf.isValid() == false)
		{
			throw EX("An interface was found to be invalid or was not verified to be valid. Cannot check the high-level subsystem.");
		}

		DesInterface::DesIteratorPtr desIt = interf.createDesIterator();
		for(desIt->first(); desIt->notDone(); desIt->next())
		{
			const Des& des = desIt->currentItem();
			addInputPlantDes(&des);
		}		
	}

	//verify that the root subsystem is valid
	DesSubsystem& rootSubsys = m_project.getRootSubsys();
	if (rootSubsys.isValid() == false)
	{
		throw EX("The high-level subsystem is not valid or it has not been verified to be valid.");		
	}

	//add all the DES of the high-level subsystem as the "supervisor DES" in the ctrl algo as
	//they are the ones that are not allowed to disable answer events. Note that to achieve this
	//we have to make the ctrl algo believe that answer events are the "uncontrollable" events that
	//cannot be blocked	
	DesSubsystem::DesIteratorPtr hDesIt = rootSubsys.createDesIterator();
	for(hDesIt->first(); hDesIt->notDone(); hDesIt->next())
	{
		const Des& hDes = hDesIt->currentItem();
		
		if (hDes.getIntegrity() != eIntegYes)
		{
			throw EX("A high-level DES is not valid or it has not been verified to be valid. Cannot check high-level subsystem.");
		}
		
		addInputSupDes(&hDes);
	}

	MultiCtrlAlgo::prepareRun();
}

//_________________________________________________________________________________________________

bool IConsistAnsAcceptAlgo::runAlgo()
{
	//run the algorithm (a controllability based algorithm applied to appropriate input DES)

	
	DesSubsystem& rootSubsys = m_project.getRootSubsys();

	bool tmp = m_project.getIntegrity() == eIntegYes ? true : false;

	rootSubsys.setInterfConsist(tmp);

    this->setIntegrity(tmp);


	bool isIConsAnsAccept = MultiCtrlAlgo::runAlgo();

	//save the subsystem's interface consistency property
	
	rootSubsys.setInterfConsist(isIConsAnsAccept);

	return isIConsAnsAccept;
}


} //end of namespace DESpot
