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

#include "DesInterface.h"
#include "DesSubsystem.h"

namespace DESpot
{

const std::wstring LowSubsysNonBlockAlgo::cLowSubsysNonBlockAlgoDesc = L"Low Level Subsystem Nonblocking Algo";
const std::wstring
LowSubsysNonBlockAlgo::cLowSubsysNonBlockingAlgoErr=L"The low-level subsystem '%ls' blocks at state '%ls'.";

  //L"Low - State '%ls' is blocking.";


//_________________________________________________________________________________________________

LowSubsysNonBlockAlgo::LowSubsysNonBlockAlgo(const DesSubsystem& subsystem) : m_subsystem(subsystem)
{
	m_description = cLowSubsysNonBlockAlgoDesc;
}

//_________________________________________________________________________________________________

LowSubsysNonBlockAlgo::~LowSubsysNonBlockAlgo(void)
{
}

//_________________________________________________________________________________________________

const DesAlgo::ErrorList& LowSubsysNonBlockAlgo::getErrorList()
{
	
	for(ErrorListIt it=m_inErrorList.begin();it!=m_inErrorList.end();it++)
	{
	  addError(errorMessage(cLowSubsysNonBlockingAlgoErr,
	m_subsystem.getName(), *it));
	}
	return m_errorList;
}

//_________________________________________________________________________________________________

void LowSubsysNonBlockAlgo::prepareRun()
{

	if (m_subsystem.isValid() == false)
	{
		throw EX("The low-level subsystem is not valid or it has not been verified to be valid.");
	}

	DesSubsystem::DesIteratorPtr lowDesIt = m_subsystem.createDesIterator();
	for(lowDesIt->first(); lowDesIt->notDone(); lowDesIt->next())
	{
		const Des& lowDes = lowDesIt->currentItem();

		if (lowDes.getIntegrity() != eIntegYes)
		{
			throw EX("A low-level DES is not valid or it has not been verified to be valid. Cannot check low-level subsystem.");
		}


		MultiNonBlockingAlgo::addInputDes(&lowDes);
	}

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

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

		if (des.getIntegrity() != eIntegYes)
		{
			throw EX("Interface DES is not valid or it has not been verified to be valid. Cannot check high-level subsystem.");
		}


		MultiNonBlockingAlgo::addInputDes(&des);
	}		



	MultiNonBlockingAlgo::prepareRun();
}

//_________________________________________________________________________________________________

bool LowSubsysNonBlockAlgo::runAlgo()

{

	bool tmp = m_subsystem.getValidProp() == eIntegYes ? true : false;
    m_subsystem.setNonBlocking(tmp);
	setIntegrity(tmp);


	bool isNonBlocking = MultiNonBlockingAlgo::runAlgo();

	//save the non-blocking property of the subystem
	m_subsystem.setNonBlocking(isNonBlocking);

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

	return isNonBlocking;
}

} //end of namespace DESpot
