/*	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"
#include "TemplateNameParser.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::cInvalidTemplateDesNameWarn = L"Invalid template des name: '%ls'";
const std::wstring DesIntegrityAlgo::cInvalidStateNameWarn = L"Invalid state name '%ls' in DES '%ls'";
const std::wstring DesIntegrityAlgo::cInvalidTemplateStateNameWarn = L"Invalid template 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::cInvalidTemplateEventNameWarn = L"Invalid template 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";

const std::wstring DesIntegrityAlgo::cInvalidEventVariableErr = L"The variables in event name '%ls' is not consistent with the variables in DES name '%ls'.";
const std::wstring DesIntegrityAlgo::cInvalidStateVariableErr = L"The variables in state name '%ls' is not consistent with the variables in DES name '%ls'.";
const std::wstring DesIntegrityAlgo::cInvalidStateNameErr = L"Invalid state name '%ls' in DES '%ls'";
const std::wstring DesIntegrityAlgo::cInvalidEventNameErr = L"Invalid event name '%ls' in DES '%ls'";


//_________________________________________________________________________________________________

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 eInterfaceTemplateDes:
		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()));
	TemplateNameParser* temp_nameValidator=new TemplateNameParser(m_des->getName());
	if (temp_nameValidator->isTemplateName()==false&&m_des->isTemplate()==true)
	{
		addWarning(errorMessage(cInvalidTemplateDesNameWarn,m_des->getName()));
		verifOk = false;
	}
	if (nameValidator.validate(m_des->getName()) == false && m_des->isTemplate()==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();
		TemplateNameParser* temp_nameValidator=new TemplateNameParser(crtState.getName());
		if(m_des->isTemplate()&&temp_nameValidator->isTemplateName()&&(!CompareNameVariables(m_des->getName(),crtState.getName())))
		{
			addError(errorMessage(cInvalidStateVariableErr, crtStateName, m_des->getName()));
		}

		if(m_des->isTemplate()==false&&temp_nameValidator->isTemplateName())
		{
			addError(errorMessage(cInvalidStateNameErr,crtStateName, m_des->getName()));
		}
		//ensure the state name is unique
		else if (nameValidator.validate(crtStateName) == false&&m_des->isTemplate()==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();
		TemplateNameParser* temp_nameValidator=new TemplateNameParser(crtEvent.getName());
		if(m_des->isTemplate()&&temp_nameValidator->isTemplateName()&&(!CompareNameVariables(m_des->getName(),crtEvent.getName())))
		{
			addError(errorMessage(cInvalidEventVariableErr, crtEventName, m_des->getName()));
		}

		if(m_des->isTemplate()==false&&temp_nameValidator->isTemplateName())
		{
			addError(errorMessage(cInvalidEventNameErr,crtEventName, m_des->getName()));
		}
		//ensure the state name is unique
		else if (nameValidator.validate(crtEventName) == false&& m_des->isTemplate()==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();
}


bool DesIntegrityAlgo::CompareNameVariables(const std::wstring name1,const std::wstring name2)
{
	int flag=0;
    //std::vector<std::wstring> variable;
	TemplateNameParser::TemplateParameter* par1= TemplateNameParser::getVariablesFromName(name1);
	TemplateNameParser::TemplateParameter* par2= TemplateNameParser::getVariablesFromName(name2);
	TemplateNameParser::TemplateParameterItr itr1=par1->begin();
	TemplateNameParser::TemplateParameterItr itr2=par2->begin();
	while(itr1!=par1->end())
	{
		while(itr2!=par2->end())
		{
			if(itr1->first!=itr2->first)
			{
				itr2++;
			}
			else
			{
				flag=1;
                break;
			}
		}
		if(flag==0)
		{
			return false;
		}
		
		itr1++;
		itr2=par2->begin();
		flag=0;
	}
	return true;
		
}


} //namespace DESpot

