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

namespace DESpot
{
																		 
const std::wstring LdInterfaceCheckAlgo::cLdInterfaceAlgoDesc = L"LD Interface Check Algorithm";
const std::wstring LdInterfaceCheckAlgo::cInitStateNotMarkedMsg = L"Initial state is not marked in interface '%ls'";
const std::wstring LdInterfaceCheckAlgo::cAnswerLeavesMarkedStateMsg = L"Answer event '%ls' leaves marked state '%ls' in interface '%ls'";
const std::wstring LdInterfaceCheckAlgo::cLDataLeavesMarkedToUnmarkedMsg = L"Low data event '%ls' leaves marked state '%ls' to an unmarked state '%ls' in interface '%ls'";
const std::wstring LdInterfaceCheckAlgo::cReqLeavesUnmarkedStateMsg = L"Request event '%ls' leaves unmarked state '%ls' in interface '%ls'";
const std::wstring LdInterfaceCheckAlgo::cAnswerLeavesUnmarkedToUnmarkedMsg = L"Answer event '%ls' leaves unmarked state '%ls' to an unmarked state '%ls' in interface '%ls'";
const std::wstring LdInterfaceCheckAlgo::cLDataLeavesUnmarkedToUnmarkedMsg = L"Low data event '%ls' leaves unmarked state '%ls' to an unmarked state '%ls' in interface '%ls'";

//_________________________________________________________________________________________________

LdInterfaceCheckAlgo::LdInterfaceCheckAlgo(void) : DesAlgo(cLdInterfaceAlgoDesc), 
                m_interf(null),
                m_isLdInterface(false)
{
}

//_________________________________________________________________________________________________

LdInterfaceCheckAlgo::LdInterfaceCheckAlgo(const DesInterface& interf) : DesAlgo(cLdInterfaceAlgoDesc), 
                m_interf(&interf),
                m_isLdInterface(false)
{
}

//_________________________________________________________________________________________________

LdInterfaceCheckAlgo::~LdInterfaceCheckAlgo(void)
{
}

//_________________________________________________________________________________________________

void LdInterfaceCheckAlgo::setInputInterface(const DesInterface& interf)
{
	m_interf = &interf;
	
	//clear any information that might exist form previous interfaces
	m_isLdInterface = false;
	m_counterExample.clear();
}

//_________________________________________________________________________________________________

const DesInterface* LdInterfaceCheckAlgo::getInputInterface()
{
	return m_interf;
}

//_________________________________________________________________________________________________

//retruns true if the input interface is an Ld-interface
bool LdInterfaceCheckAlgo::isLdInterface()
{
	return m_isLdInterface;
}

//_________________________________________________________________________________________________

//if the interface is found not to be an Ld-interface the algorithm
//will provids a counter example
const LdInterfaceCheckAlgo::CounterExample& LdInterfaceCheckAlgo::getCounterExample()
{
	return m_counterExample;
}

//_________________________________________________________________________________________________

//Rule 1: - verifies that the initial state is marked
bool LdInterfaceCheckAlgo::verifyInitialState()
{
	if (m_interfDes->getInitialState().isMarked() == false)	  
	{
		m_counterExample.errState = &m_interfDes->getInitialState();
		m_counterExample.errMessage = errorMessage(cInitStateNotMarkedMsg, m_interf->getName());
		
		return false; 
	}

	//m_progress->updateProgress();
	return true;
}

//_________________________________________________________________________________________________

//Rule 2: verifies the all exit events of a marked state are either requests or low-data goint to marked states
bool LdInterfaceCheckAlgo::verifyMarkedStateRules(const DesState& state)
{
	bool bOk = true;

	//Verify each tranition leaving the state
	Des::TransIteratorPtr transIt = m_interfDes->createStateTransIterator(state);
	for(transIt->first(); transIt->notDone(); transIt->next())
	{
		const DesTransition& trans = transIt->currentItem();
		const DesEvent& exitEvent = trans.event();
		
		//verify that only request or low data events leave the marked state
		//if low data leaves make sure it goes to a marked state
		if (exitEvent.getType() == eAnswerEvent)
		{
			std::wstring error = errorMessage(cAnswerLeavesMarkedStateMsg, exitEvent.getName(), state.getName(), m_interf->getName());
			addError(error);
			
			if (m_counterExample.isSet() == false)
			{
				m_counterExample.errState = &state;
				m_counterExample.errEvent = &exitEvent;
				m_counterExample.errMessage = error;
			}

			bOk = false; 
		}
		else if ((exitEvent.getType() == eLDataEvent) && (trans.toState().isMarked() == false))
		{
			std::wstring error = errorMessage(cLDataLeavesMarkedToUnmarkedMsg, exitEvent.getName(), 
														   state.getName(), trans.toState().getName(), m_interf->getName());
			addError(error);
			
			if (m_counterExample.isSet() == false)
			{
				m_counterExample.errState = &state;
				m_counterExample.errEvent = &exitEvent;
				m_counterExample.errMessage = error;
			}			
			
			bOk = false; 
		}

		//m_progress->updateProgress();
	}

	//all exit events checked out
	return bOk;
}

//_________________________________________________________________________________________________
//Rule 3: Verifies that all events exiting an unmarked states are answer events or low-data events that are
//either self-looped or they go to a marked state
bool LdInterfaceCheckAlgo::verifyUnmarkedStateRules(const DesState& state)
{
	bool bOk = true;

	//Verify each tranition leaving the state
	Des::TransIteratorPtr transIt = m_interfDes->createStateTransIterator(state);
	for(transIt->first(); transIt->notDone(); transIt->next())
	{
		const DesTransition& trans = transIt->currentItem();
		const DesEvent& exitEvent = trans.event();

		//verify that only answer or low data events leave this state. If a low data event leaves the state
		//it is either self-looped or it goes to a marked state
		if (exitEvent.getType() == eRequestEvent)
		{
			//requests are not allowed to leave unmarked states
			std::wstring error = errorMessage(cReqLeavesUnmarkedStateMsg, exitEvent.getName(), state.getName(), m_interf->getName());
			addError(error);

			if (m_counterExample.isSet() == false)
			{
				m_counterExample.errState = &state;
				m_counterExample.errEvent = &exitEvent;
				m_counterExample.errMessage = error;
			}			
			
			bOk = false; 
		}
		else if ((exitEvent.getType() == eAnswerEvent) && (trans.toState().isMarked() == false))
		{
			std::wstring error = errorMessage(cAnswerLeavesUnmarkedToUnmarkedMsg, exitEvent.getName(), state.getName(), 
										      trans.toState().getName(), m_interf->getName());
			addError(error);

			//answers are allowed to leave unmarked states but only to marked states
			if (m_counterExample.isSet() == false)
			{
				m_counterExample.errState = &state;
				m_counterExample.errEvent = &exitEvent;
				m_counterExample.errMessage = error;
			}

			bOk = false;
		}
		else if (exitEvent.getType() == eLDataEvent)
		{
			if ((&trans.toState() != &state) && (trans.toState().isMarked() == false))
			{
				std::wstring error = errorMessage(cLDataLeavesUnmarkedToUnmarkedMsg, exitEvent.getName(), 
												  state.getName(), trans.toState().getName(), m_interf->getName());
				addError(error);

				//low data events are allowed to leave unmarked states but only if they are self-looped or
				//they go to a marked state
				if (m_counterExample.isSet() == false)
				{
					m_counterExample.errState = &state;
					m_counterExample.errEvent = &exitEvent;
					m_counterExample.errMessage = error;
				}				

				bOk = false;
			}
		}

	//	m_progress->updateProgress();
	}

	//all exit events checked out
	return bOk;
}

//_________________________________________________________________________________________________

void LdInterfaceCheckAlgo::prepareRun()
{
	m_isLdInterface = false;
	m_counterExample.clear();

	if (m_interf == null)
	{
		throw EX("The algorithm was not given an interface to check");
	}

	if (m_interf->isValid() == false)
	{
		throw EX("The interface is not valid or it has not been verified to be valid.");
	}

	m_interfDes = &m_interf->getSyncDes();

	if (m_interfDes->hasInitialState() == false)
	{
		throw EX("Interface DES has no intitial state");
	}

	if (m_interfDes->getMarkedStateCount() == 0)
	{
		throw EX("Interface DES has no marked states");
	}
}

//_________________________________________________________________________________________________

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

	bool verifOk = true;
	
	prepareRun();

	verifOk = verifyInitialState();
	
	Des::StateIteratorPtr stateIt = m_interfDes->createStateIterator();
	for(stateIt->first(); stateIt->notDone() && verifOk; stateIt->next())
	{
		const DesState& state = stateIt->currentItem();

		if (state.isMarked())
		{
			verifOk = verifyMarkedStateRules(state);
		}
		else
		{
			verifOk = verifyUnmarkedStateRules(state);
		}
	}

	//save the interface consistent property in the checked interface
	m_interf->setInterfConsist(verifOk);

	return m_isLdInterface = verifOk; // = is intentional
}

}
