/*	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 "DesFlatProject.h"
#include "FlatProjIntegrityAlgo.h"
#include "MultiNonBlockingAlgo.h"
#include "MultiCtrlAlgo.h"
#include "CounterExampleAlgo_FlatCntr.h"
#include "CounterExampleAlgo_FlatNB.h"
#include "DummyProjCreation.h"
#include "DesProject.h"

namespace DESpot
{
	class FlatProjectPropCheck : public DesAlgo
	{
		public:
			FlatProjectPropCheck(DesFlatProject& project, bool runIncremental = true);
			virtual ~FlatProjectPropCheck(void);

		public:
			void checkIntegrity(bool checkInteg = true);
			bool integrityChecked() const;
			FlatProjIntegrityAlgo& integAlgo();

			void checkNonBlock(bool checkNonBlock = true);
			bool nonBlockChecked() const;
			MultiNonBlockingAlgo& nonBlockAlgo();

			void checkCtrl(bool checkCtrl = true);
			bool ctrlChecked();
			MultiCtrlAlgo& ctrlAlgo();

			bool runSuccessful() const;

		public:
			virtual bool runAlgo();

		protected:
			virtual void prepareRun();


		private:
			DesFlatProject& m_project;

			bool m_checkInteg;
			FlatProjIntegrityAlgo m_integAlgo;
			
			bool m_checkNonBlock;
			MultiNonBlockingAlgo m_nonBlockAlgo;			
			bool m_checkCtrl;
			MultiCtrlAlgo m_ctrlAlgo;

			bool m_runSuccessful;

			static const std::wstring cFlatProjectPropCheckAlgoDesc;
	};

} //end of namespace DESpot


