/*	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 <string>
#include "DesAlgo.h"

namespace DESpot
{
	class DesInterface;
	class Des;
	class DesState;
	class DesEvent;

	class LdInterfaceCheckAlgo : public DesAlgo
	{
		public:
			struct CounterExample
			{
				const DesState* errState;
				const DesEvent* errEvent;
				std::wstring    errMessage;

				CounterExample()
				{
					errState = null;
					errEvent = null;
				}

				void clear()
				{
					errState = null;
					errEvent = null;
					errMessage.clear();
				}

				bool isSet()
				{
					return (((errState != null) || (errEvent != null)) && (errMessage.empty() == false));
				}
			};
		
		public:
			LdInterfaceCheckAlgo();
			LdInterfaceCheckAlgo(const DesInterface& interf);
			virtual ~LdInterfaceCheckAlgo(void);

			void setInputInterface(const DesInterface& interf);
			const DesInterface* getInputInterface();

		public:
			virtual bool runAlgo();

			//retruns true if the input interface is an Ld-interface
			bool isLdInterface();

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

		protected:
			virtual void prepareRun();

			//Rule 1: - verifies that the initial state is marked
			virtual bool verifyInitialState();
			
			//Rule 2: - verifies the all exit events of a marked state are either requests or low-data goint to marked states
			virtual bool verifyMarkedStateRules(const DesState& state);
			
			//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
			virtual bool verifyUnmarkedStateRules(const DesState& state);

		protected:
			const DesInterface* m_interf;
			const Des*			m_interfDes;

			bool m_isLdInterface;
			
			CounterExample m_counterExample;

		protected:
			static const std::wstring cLdInterfaceAlgoDesc;
			static const std::wstring cInitStateNotMarkedMsg;
			static const std::wstring cAnswerLeavesMarkedStateMsg;
			static const std::wstring cLDataLeavesMarkedToUnmarkedMsg;
			static const std::wstring cReqLeavesUnmarkedStateMsg;
			static const std::wstring cAnswerLeavesUnmarkedToUnmarkedMsg;
			static const std::wstring cLDataLeavesUnmarkedToUnmarkedMsg;
	};
}
