/*	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
	modified by xu han
*/

#pragma once

#include "ReachabilityAlgo.h"

namespace DESpot
{
	class CoreachabilityAlgo :	public ReachabilityAlgo
	{
		public:
			CoreachabilityAlgo();
			CoreachabilityAlgo(Des* inDes);

			virtual ~CoreachabilityAlgo(void);

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

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

			//Returns the number of non-coreachable states
			DesState::Count getNonCoreachStateCount();

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

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

			//create a transition iterator for inverse transitions entering the given state. 
			//using DES's inverse transition function
			virtual Des::TransIteratorPtr  createTransIterator(const DesState& state);//++

			//marks the given state as coreachable. 
			 virtual void setCoreachable(const DesState& state);//++

			//return true if the algorithm has found the state to be reachable
			virtual bool foundCoreachable(const DesState& state);//++

		private:
			static const std::wstring cCoreachAlgoDesc;
			static const std::wstring cCoreachNoMarkedStatesError;
	};
} // end of namespace DESpot
