/*	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 "DesAlgo.h"
#include "DesHierProject.h"
#include "HierProjIntegrityAlgo.h"
#include "IConsistAlgo.h"
#include "LwNonBlockingAlgo.h"
#include "LwCtrlAlgo.h"
#include "CounterExampleAlgo_IntfImpAlgo.h"

namespace DESpot
{

	class HierProjectPropCheck   : public DesAlgo
	{
		public:
			HierProjectPropCheck(DesHierProject& project, bool runIncremental = true);
			virtual ~HierProjectPropCheck(void);
		
		public:
			void checkIntegrity(bool checkInteg = true);
			bool integrityChecked() const;
			HierProjIntegrityAlgo& integAlgo();

			void checkInterfConsist(bool checkIConsist = true);
			bool iConsistChecked() const;
			IConsistAlgo& interfConsistAlgo();

			void checkLwNonBlock(bool checkLwNonBlock = true);
			bool lwNonBlockChecked() const;
			LwNonBlockingAlgo& levelWiseNonBlockAlgo();

			void checkLwCtrl(bool checkLwCtrl = true);
			bool lwCtrlChecked();
			LwCtrlAlgo& levelWiseCtrlAlgo();

			bool runSuccessful() const;
		
		public:
			virtual bool runAlgo();

		protected:
			virtual void prepareRun();

		private:
			DesHierProject& m_project;

			bool m_checkInteg;
			HierProjIntegrityAlgo m_integAlgo;
			
			bool m_checkIConsist;
			IConsistAlgo m_iConsAlgo;
			
			bool m_checkLwNonBlock;
			LwNonBlockingAlgo m_lwNonBlockAlgo;
			
			bool m_checkLwCtrl;
			LwCtrlAlgo m_lwCtrlAlgo;

			bool m_runSuccessful;

			static const std::wstring cHierProjectPropCheckAlgoDesc;
	};

} //end of namespace DESpot


