/*	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
*/

#pragma once

#include "IntegrityAlgo.h"
#include "Des.h"

namespace DESpot
{
	class DesIntegrityAlgo: public IntegrityAlgo
	{
		public:
			DesIntegrityAlgo();
			DesIntegrityAlgo(UpdateProgressInterface* progress);
			DesIntegrityAlgo(const Des* des);
			virtual ~DesIntegrityAlgo(void);
			
			void setInputDes(const Des* des);
	
		//Verification methods: return true if the verification was succesfull and they
		//output warnings and errors in m_warnList and m_errList. Note a verification is
		//successful even if there are warnings
		//protected:
			//Overridable called from the "run" method of the base implementation of the algorithm
			virtual bool verifyIntegrity();

			//verifies the name of DES doesn't contain invalid characters
			virtual bool verifyDesName();
			
			//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
			virtual bool verifyDesStates();
			
			//verify that DES has at least one event, that each event name is unique
			virtual bool verifyDesEvents();

			//verifies that DES has at least one transition there are no incomplete transitions,
			//that DES is deterministic
			virtual bool verifyTransitions();

			//verifies that DES is reachable
			virtual bool verifyReachable();

		//Other implementation methods
		protected:
			//verifies if the event type is valid in the input DES
			bool isEventTypeValid(EventType eventType);

		protected:
			//The des being checked
			const Des* m_des;

		private:
			static const std::wstring cDesIntegCheckAlgo;

			//error messages
			static const std::wstring cEmptyStateSpaceErr;
			static const std::wstring cNoInitStateErr;
			static const std::wstring cInitStateNotUniqueErr;
			static const std::wstring cNoMarkedStatesErr;
			static const std::wstring cStateNameNotUniqueErr; 
			static const std::wstring cEventNameNotUniqueErr; 
			static const std::wstring cInvalidEventTypeErr; 
			static const std::wstring cInvalidTransErr;
			static const std::wstring cNonDeterministicDesErr;
			static const std::wstring cUnreachStateErr;

			//warning messages
			static const std::wstring cInvalidDesNameWarn;
			static const std::wstring cInvalidStateNameWarn; 
			static const std::wstring cEmptyEventSetWarn;
			static const std::wstring cInvalidEventNameWarn;
			static const std::wstring cEventNotUsedWarn;
			static const std::wstring cUnknownDesTypeWarn;
			static const std::wstring cNoTransitionWarn;
	};

} // end of namespace DESpot
