/*	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 <map>
#include "DesAlgo.h"
#include "DesHierProject.h"
#include "SubsysReqAcceptAlgo.h"
#include "InterfImplCheckAlgo.h"

namespace DESpot
{
	

	class LowSubsysIConsistAlgo : public DesAlgo
	{
		public:
			LowSubsysIConsistAlgo(const DesSubsystem& subsystem);
			virtual ~LowSubsysIConsistAlgo(void);

		public:
			virtual bool runAlgo();

			bool isSubsysInterfConsist() const;

			const DesSubsystem& getInputSubsystem() const;

		protected:
			virtual void prepareRun();

			//Step4: verify that all requests enabled by the interface are accepted by the subsystem
			virtual bool verifySubsysAcceptsRequests();

			//Step 5 and 6: verify that the subsystem implements the interface correctly: all answers possible
			//in the interface are implemented as such and all interface commands end in marked states in the low level
			virtual bool verifySubsysImplementation();

		protected:
			const DesSubsystem& m_subsystem;

			SubsysReqAcceptAlgo m_subsysReqAcceptAlgo;
			InterfImplCheckAlgo m_subsysInterfImplCheckAlgo;		

	private:
			static const std::wstring cLowSubsysIConsistAlgoDesc;
			//added by zain for counter example
			DesHierProject* m_project;
	public:
			inline void set_proj(DesHierProject* in_proj){m_project=in_proj;}
			inline DesHierProject* get_proj(){return m_project;}
	};
}

