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

namespace DESpot
{

const std::wstring LowSubsysCtrlAlgo::cLowSubsysCtrlAlgoDesc = L"Level Wise Controllability Algo";
const std::wstring LowSubsysCtrlAlgo::cLowSubsysCtrlError = L"The low-level subsystem '%ls' is uncontrollable at state '%ls' for event '%ls'. State '%ls' of DES '%ls' is blocking the event.";


//_________________________________________________________________________________________________

LowSubsysCtrlAlgo::LowSubsysCtrlAlgo(const DesSubsystem& subsystem) : m_subsystem(subsystem)
{ 
	m_description = cLowSubsysCtrlAlgoDesc;
	m_checkDesIntegrity = false;
}

//_________________________________________________________________________________________________

LowSubsysCtrlAlgo::~LowSubsysCtrlAlgo(void)
{
}

//_________________________________________________________________________________________________

std::wstring LowSubsysCtrlAlgo::prepareErrorDescription()
{
	std::wstring closedStateName = formatUnctrlStateName();
	return errorMessage(cLowSubsysCtrlError, m_subsystem.getName(),
		                            closedStateName, 
									getUnctrlBehaviour().exitEvent->getName(), 
									getUnctrlBehaviour().blockingState->getName(), 
									getUnctrlBehaviour().blockingDes->getName());
}

//_________________________________________________________________________________________________

void LowSubsysCtrlAlgo::prepareRun()
{
	//verify that the subsystem is valid
	if (m_subsystem.isValid() == false)
	{
		throw EX("The low-level subsystem is not valid or it has not been verified to be valid.");
	}

	addInputPlantDes(m_subsystem.createDesIterator(ePlantDes));

	addInputSupDes(m_subsystem.createDesIterator(eSupervisorDes));

	const DesInterface& interf = m_subsystem.getInterface();
	if (interf.isValid() == false)
	{
		throw EX("The interface implemented by the low-level subsystem is not valid or it has not been verified to be valid.");
	}
	
	addInputSupDes(interf.createDesIterator());

	MultiCtrlAlgo::prepareRun();

}

//_________________________________________________________________________________________________

bool LowSubsysCtrlAlgo::runAlgo()
{
	//run the algorithm	
    bool tmp = m_subsystem.getValidProp() == eIntegYes ? true : false;

    this->setIntegrity(tmp);

	bool isCtrl = MultiCtrlAlgo::runAlgo();

	//save the controllability property in the subsystem
	m_subsystem.setControllable(isCtrl);
	// Added by zain for subsystem Ld controllability counter example generation
	if(isfirsterror==false)
	{
		ErrorSubSystem=&m_subsystem;
		IsFirstErrorSubSystem=false;
	}

	return isCtrl;
}


} //end of namespace DESpot
