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


namespace DESpot
{

const std::wstring HighSubsysCtrlAlgo::cHighSubsysCtrlAlgoDesc = L"High Level Subsystem Controllability Algo";
const std::wstring HighSubsysCtrlAlgo::cHighSubsysCtrlError = L"The high-level subsystem '%ls' is uncontrollable at state '%ls' for event '%ls'. State '%ls' of DES '%ls' is blocking the event.";

//_________________________________________________________________________________________________

HighSubsysCtrlAlgo::HighSubsysCtrlAlgo(DesHierProject& project) : m_project(project)
{ 
	m_description = cHighSubsysCtrlAlgoDesc;
	m_checkDesIntegrity = false;
}

//_________________________________________________________________________________________________

HighSubsysCtrlAlgo::~HighSubsysCtrlAlgo(void)
{
}

//_________________________________________________________________________________________________

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

//_________________________________________________________________________________________________

std::wstring HighSubsysCtrlAlgo::prepareErrorDescription()
{
		std::wstring closedStateName = formatUnctrlStateName();
	return errorMessage(cHighSubsysCtrlError, m_project.getRootSubsys().getName(),
		                            closedStateName, 
									getUnctrlBehaviour().exitEvent->getName(), 
									getUnctrlBehaviour().blockingState->getName(), 
									getUnctrlBehaviour().blockingDes->getName());
}

//_________________________________________________________________________________________________

void HighSubsysCtrlAlgo::prepareRun()
{
	//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.");		
	}
	
	addInputPlantDes(rootSubsys.createDesIterator(ePlantDes));

	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.");
		}

		addInputPlantDes(interf.createDesIterator());
	}

	addInputSupDes(rootSubsys.createDesIterator(eSupervisorDes));

	MultiCtrlAlgo::prepareRun();
}

//_________________________________________________________________________________________________

bool HighSubsysCtrlAlgo::runAlgo()
{

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

    this->setIntegrity(tmp);

	bool isCtrl = MultiCtrlAlgo::runAlgo();
	
	//save the controllability property in the subsystem
	DesSubsystem& rootSubsys = m_project.getRootSubsys();
	rootSubsys.setControllable(isCtrl);

	// Added by zain for subsystem Ld controllability counter example generation
	if(isfirsterror==false)
	{
		ErrorSubSystem=&rootSubsys;
		IsFirstErrorSubSystem=false;
	}

	return isCtrl;
}

}
