/*	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 "CoreachabilityAlgo.h"

namespace DESpot
{
	class NonBlockingAlgo : public CoreachabilityAlgo
	{
		public:
			NonBlockingAlgo(bool runIncremental = false);
			NonBlockingAlgo(Des* inDes, bool runIncremental = false);
			
			virtual ~NonBlockingAlgo(void);

		public:
			//runs the algorithm and returns true if the the DES is non-blocking
			virtual bool runAlgo();//++

			//Returns true if all states in DES are coreachable
			bool isNonBlocking() const;

			//overrides the result of the non-blocking algorithm
			void overrideNonBlocking(bool nonBlocking);
			
			
			//Returns the number of blocking states
			DesState::Count getBlockingStateCount();

			//Returns an iterator that allows the user to iterate through the non-coreachable states
			StateIteratorPtr createBlockingStateIterator();

			const ErrorList& getErrorList();

			int getErrorCount() const;

		protected:
			//Prepares the informaiton necessary for the algorithm to run
			virtual void prepareRun();

			//checks to see if a state was found blocking by the algorithm
			bool foundNonBlocking(const DesState& state);

			//returns true if the algorithm found the state. It is equivalent to foundBlocking but it is overriden
			//so the basic algorithm uses the right information
			virtual bool found(const DesState& state);

		private:
			static const std::wstring cNonBlockAlgoDesc;
			static const std::wstring cBlockStateErr;
	};

} //end of namespace DESpot

