/*	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 "DesIntegrityAlgo.h"
#include "NameValidator.h"
#include "ReachabilityAlgo.h"
#include "DesSubsystem.h"
#include "CommonDefinitions.h"

namespace DESpot
{

const std::wstring DesIntegrityAlgo::cDesIntegCheckAlgo = L"DES Consistency Algorithm";

//error messages
const std::wstring DesIntegrityAlgo::cEmptyStateSpaceErr = L"DES '%ls' has an empty state set";
const std::wstring DesIntegrityAlgo::cNoInitStateErr = L"DES '%ls' does not have an initial state";
const std::wstring DesIntegrityAlgo::cInitStateNotUniqueErr = L"Initial state '%ls' is not unique in DES '%ls'";
const std::wstring DesIntegrityAlgo::cNoMarkedStatesErr = L"Des '%ls' does not have any marked states";
const std::wstring DesIntegrityAlgo::cStateNameNotUniqueErr = L"State name '%ls' is not unique in DES '%ls' ";
const std::wstring DesIntegrityAlgo::cEventNameNotUniqueErr = L"Event name '%ls' is not unique in DES '%ls'";
const std::wstring DesIntegrityAlgo::cInvalidEventTypeErr = L"Invalid event type for event '%ls' in DES '%ls'";
const std::wstring DesIntegrityAlgo::cInvalidTransErr = L"Invalid transition: (%ls; %ls; %ls) in DES '%ls'";
const std::wstring DesIntegrityAlgo::cNonDeterministicDesErr = L"DES '%ls' is non-deterministic";
const std::wstring DesIntegrityAlgo::cUnreachStateErr = L"Unreachable state was found: '%ls' in DES '%ls'";

//warning messages
const std::wstring DesIntegrityAlgo::cInvalidDesNameWarn = L"Invalid des name: %ls";
const std::wstring DesIntegrityAlgo::cInvalidStateNameWarn = L"Invalid state name '%ls' in DES '%ls'";
const std::wstring DesIntegrityAlgo::cEmptyEventSetWarn = L"The event set of DES '%ls' is empty";
const std::wstring DesIntegrityAlgo::cInvalidEventNameWarn = L"Invalid event name '%ls' in DES '%ls'";
const std::wstring DesIntegrityAlgo::cEventNotUsedWarn = L"Event '%ls' not used in DES '%ls'";
const std::wstring DesIntegrityAlgo::cUnknownDesTypeWarn = L"Unknown des type for DES '%ls'";
const std::wstring DesIntegrityAlgo::cNoTransitionWarn = L"Des '%ls' has no transitions";


//_________________________________________________________________________________________________

DesIntegrityAlgo::DesIntegrityAlgo(void) : m_des(null)
{
	m_description = cDesIntegCheckAlgo;
}

//_________________________________________________________________________________________________

DesIntegrityAlgo::DesIntegrityAlgo(UpdateProgressInterface* progress) : m_des(null)
{
	m_description = cDesIntegCheckAlgo;
	provideProgress(progress);
}

//_________________________________________________________________________________________________

DesIntegrityAlgo::DesIntegrityAlgo(const Des* des)
{
	m_description = cDesIntegCheckAlgo;
	setInputDes(des);
}

//_________________________________________________________________________________________________

DesIntegrityAlgo::~DesIntegrityAlgo(void)
{
}

//_________________________________________________________________________________________________

void DesIntegrityAlgo::setInputDes(const Des* des)
{
	m_des = des;

	m_errorList.clear();
	m_warningList.clear();

	addError(cNotCheckedErr);
}

//_________________________________________________________________________________________________

//verifies if the event type is valid in the input DES
bool DesIntegrityAlgo::isEventTypeValid(EventType eventType)
{
	switch(m_des->getType())
	{
		case eInterfaceDes:
			return ((eventType == eAnswerEvent)  || 				
				    (eventType == eRequestEvent) || 
				    (eventType == eLDataEvent));

		case eSubsystemDes:
		{
			bool validType = ((eventType == eDefaultEvent) ||
							 (eventType == eAnswerEvent)  || 				
							 (eventType == eRequestEvent) || 
							 (eventType == eLDataEvent));  
			
			return validType;
		}

		default:
			return true; //by default the type is ignored
	}
}

//_________________________________________________________________________________________________

//verifies the name of DES doesn't contain invalid characters
bool DesIntegrityAlgo::verifyDesName()
{
	bool verifOk = true;
	NameValidator nameValidator(new AlphaNumValidator(new WordSepValidator()));
	if (nameValidator.validate(m_des->getName()) == false)
	{
		addWarning(errorMessage(cInvalidDesNameWarn, m_des->getName()));
		
		verifOk = false;
	}

	//updateProgress();

	return verifOk;
}	

//_________________________________________________________________________________________________

//verifies that DES has at least one state, that each state has a unique name, 
//that DES has only one initial state, that DES has at least one marked state
bool DesIntegrityAlgo::verifyDesStates()
{
	bool verifOk = true;
	


	//verify that DES state space is not empty
	if (m_des->getStateCount() == 0)
	{
		addError(errorMessage(cEmptyStateSpaceErr, m_des->getName()));
		verifOk = false;
	}

	//verify that there is at least one marked state
	if (m_des->getMarkedStateCount() == 0)
	{
		addError(errorMessage(cNoMarkedStatesErr, m_des->getName()));
		verifOk = false;
	}
	
	//verify that DES has an initial state
	if (m_des->hasInitialState() == false)
	{
		addError(errorMessage(cNoInitStateErr, m_des->getName()));
		verifOk = false;
	}

	//verify the validity of each state: unique initial state, valid and unique name
	NameMap nameMap;
	NameValidator nameValidator(new AlphaNumValidator(new WordSepValidator()));
	Des::StateIteratorPtr stateIt = m_des->createStateIterator();
	for(stateIt->first(); stateIt->notDone(); stateIt->next())
	{
		const DesState& crtState = stateIt->currentItem();
		std::wstring    crtStateName = crtState.getName();
		
		//ensure the state name is unique
		if (nameValidator.validate(crtStateName) == false)
		{
			addWarning(errorMessage(cInvalidStateNameWarn, crtStateName, m_des->getName()));
		}
		
		//ensure the initial state is unique
		if (crtState.isInit() && (&crtState != &m_des->getInitialState()))
		{
			addError(errorMessage(cInitStateNotUniqueErr, crtState.getName(), m_des->getName()));
			verifOk = false;			
		}

		//make sure the name is unique
		bool alreadyReported = false;
		if (isNameDuplicated(nameMap, crtStateName, alreadyReported) && (alreadyReported == false))
		{
			//a duplicate name has been found for the first time -> add error
			addError(errorMessage(cStateNameNotUniqueErr, crtStateName, m_des->getName()));
			verifOk = false;
		}
	}


	


	updateProgress();


	//updateProgress();

	return verifOk;
}

//_________________________________________________________________________________________________

//verify that DES has at least one event, that each event name is unique
bool DesIntegrityAlgo::verifyDesEvents()
{
	bool verifOk = true;

	//verify that DES event is not empty
	if (m_des->getEventCount() == 0)
	{
		addWarning(errorMessage(cEmptyEventSetWarn, m_des->getName()));
	}

	//verify each event: name validity, name uniqueness and type
	NameMap nameMap;
	NameValidator nameValidator(new AlphaNumValidator(new WordSepValidator()));
	Des::EventIteratorPtr eventIt = m_des->createEventIterator();
	for(eventIt->first(); eventIt->notDone(); eventIt->next())
	{
		const DesEvent& crtEvent = eventIt->currentItem();
		std::wstring    crtEventName = crtEvent.getName();
		//ensure the state name is unique
		if (nameValidator.validate(crtEventName) == false)
		{
			addWarning(errorMessage(cInvalidEventNameWarn, crtEventName, m_des->getName()));
		}
		
		//make sure the name is unique
		bool alreadyReported = false;
		if (isNameDuplicated(nameMap, crtEventName, alreadyReported) && (alreadyReported == false))
		{
			//a duplicate name has been found for the first time -> add error
			addError(errorMessage(cEventNameNotUniqueErr, crtEventName, m_des->getName()));
			verifOk = false;
		}

		//verify the type
		EventType eventType = crtEvent.getType();
		if (isEventTypeValid(eventType) == false)
		{
			addError(errorMessage(cInvalidEventTypeErr, crtEventName, m_des->getName()));
			verifOk = false;
		}

		//verify that the event is used in a transition
		if (crtEvent.isUsed() == false)
		{
			addWarning(errorMessage(cEventNotUsedWarn, crtEventName, m_des->getName()));
		}
	}

	//updateProgress();

	return verifOk;
}

//_________________________________________________________________________________________________

//verifies that DES has at least one transition there are no incomplete transitions,
//that DES is deterministic
bool DesIntegrityAlgo::verifyTransitions()
{
	bool verifOk = true;
	if (m_des->isNonDeterministic())
	{
		addError(errorMessage(cNonDeterministicDesErr, m_des->getName()));
		verifOk = false;
	}

	if (m_des->getTransCount() == 0)
	{
		addWarning(errorMessage(cNoTransitionWarn, m_des->getName()));
	}

	//identical transitions are not allowed by construction

	//verify if all transitions are valid
	Des::TransIteratorPtr transIt = m_des->createTransIterator(true);
	for(transIt->first(); transIt->notDone(); transIt->next())
	{
		const DesTransition& trans = transIt->currentItem();
		if (trans.isValid() == false)
		{
			addError(errorMessage(cInvalidTransErr, trans.fromState().getName(),
													trans.event().getName(),
													trans.toState().getName(),
													m_des->getName()));
			verifOk = false;
		}
	}

	//updateProgress();

	return verifOk;
}

//_________________________________________________________________________________________________

//verifies that DES is reachable
bool DesIntegrityAlgo::verifyReachable()
{
	bool verifOk = true;

	if (m_des->hasInitialState())
	{
		//the reachability information will be saved in DES. Ensure the reachability algorithm doesn't check for
		//integrity as that would create logical infinite loop
		ReachabilityAlgo reachAlgo(m_des, false);
		if (m_des->checkReachability(reachAlgo) == false)
		{
			ReachabilityAlgo::StateIteratorPtr stateIt = reachAlgo.createUnreachStateIterator();
			for(stateIt->first(); stateIt->notDone(); stateIt->next())
			{
				addError(errorMessage(cUnreachStateErr, stateIt->currentItem()->getName(), m_des->getName()));
			}

			verifOk = false;
		}
	}

	//updateProgress();

	return verifOk;
}

//_________________________________________________________________________________________________

//Runs the algorithm and returns true if DES is consistent
bool DesIntegrityAlgo::verifyIntegrity()
{
	verifyDesName();
	
	verifyDesStates();
	
	verifyDesEvents();

	verifyTransitions();

	verifyReachable();

	return isValid();
}

} //namespace DESpot

