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

namespace DESpot
{

const std::wstring LowSubsysIConsistAlgo::cLowSubsysIConsistAlgoDesc = L"Low Level Subsystem IConsist Algo";

//_________________________________________________________________________________________________

LowSubsysIConsistAlgo::LowSubsysIConsistAlgo(const DesSubsystem& subsystem) : 
			m_subsystem(subsystem),
			m_subsysReqAcceptAlgo(subsystem),
			m_subsysInterfImplCheckAlgo(subsystem)
{
	m_description = cLowSubsysIConsistAlgoDesc;
}

//_________________________________________________________________________________________________

LowSubsysIConsistAlgo::~LowSubsysIConsistAlgo(void)
{
}

//_________________________________________________________________________________________________

bool LowSubsysIConsistAlgo::isSubsysInterfConsist()	const
{
	return (m_subsysReqAcceptAlgo.allRequestEventsAccepted() && m_subsysInterfImplCheckAlgo.isSubsysImplCorrect());
}

//_________________________________________________________________________________________________
const DesSubsystem& LowSubsysIConsistAlgo::getInputSubsystem() const
{
	return m_subsystem;
}

//_________________________________________________________________________________________________
//Step4: verify that all requests enabled by the interface are accepted by the subsystem
bool LowSubsysIConsistAlgo::verifySubsysAcceptsRequests()
{
	if (m_subsysReqAcceptAlgo.runEx(m_progress) == false)
	{
		addError(m_subsysReqAcceptAlgo.getError());

		//Added by zain for counter example generation
		if(LowSubsysIConsistAlgo::isfirsterror)
			{
				LowSubsysIConsistAlgo::setIFailureType(m_subsysReqAcceptAlgo.getIFailureType());
				LowSubsysIConsistAlgo::ErrorSubSystem=m_subsysReqAcceptAlgo.getErrorSubsystem();
				this->CE_tuplemap=m_subsysReqAcceptAlgo.CE_tuplemap;			
				LowSubsysIConsistAlgo::isfirsterror=false;
				LowSubsysIConsistAlgo::IsFirstErrorSubSystem=false;
			}
		return false;
	}

	return true;
}

//_________________________________________________________________________________________________

//Step 5 and 6: verify that the subsystem implements the interface correctly: all answers possible
//in the interface are implemented as such and all interface commands end in marked states in the low level
bool LowSubsysIConsistAlgo::verifySubsysImplementation()
{
	if (m_subsysInterfImplCheckAlgo.runEx(m_progress) == false)
	{
		addError(m_subsysInterfImplCheckAlgo.getErrorList());

		//Added by zain for counter example generation
		if(LowSubsysIConsistAlgo::isfirsterror)
			{
				LowSubsysIConsistAlgo::setIFailureType(m_subsysInterfImplCheckAlgo.getIFailureType());
				LowSubsysIConsistAlgo::ErrorSubSystemName=m_subsysInterfImplCheckAlgo.getErrorSubsystemName();
				LowSubsysIConsistAlgo::ErrorSubSystem=m_subsysInterfImplCheckAlgo.getErrorSubsystem();
				LowSubsysIConsistAlgo::CE_tuplemap=m_subsysInterfImplCheckAlgo.CE_tuplemap;
				this->CE_tuplemap=m_subsysInterfImplCheckAlgo.CE_tuplemap;				
				LowSubsysIConsistAlgo::isfirsterror=false;	
				LowSubsysIConsistAlgo::IsFirstErrorSubSystem=false;
			}
		return false;
	}

	return true;
}

//_________________________________________________________________________________________________

void LowSubsysIConsistAlgo::prepareRun()
{
	//clear any errors from previous runs
	m_errorList.clear();

	// Xu Han removed this in rev 399. RJL added this back

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

}

//_________________________________________________________________________________________________

bool LowSubsysIConsistAlgo::runAlgo()
{
	ProgressUpdater updater(m_progress);

	prepareRun();

	//Step4: verify that all requests enabled by the interface are accepted by the subsystem
	verifySubsysAcceptsRequests();
	
	//Step 5 and 6: verify that the subsystem implements the interface correctly: all answers possible
	//in the interface are implemented as such and all interface commands end in marked states in the low level
	verifySubsysImplementation();

	//save the interface consistent property in the input subsystem
	bool isInterfConsist = isSubsysInterfConsist(); 
	m_subsystem.setInterfConsist(isInterfConsist);

	return	isInterfConsist;
}

} //end of namespace DESpot
