/*	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 <sstream>
#include "NameValidator.h"
#include "DesTypes.h"

namespace DESpot
{

class DesState
{
	//Types_____________________________
	public:
		//#pragma region DesState Typedefs
		typedef unsigned char Props;
		typedef unsigned long long Index;
		typedef unsigned long long Count;
		//#pragma endregion

		//#pragma region DesState::ID Class Definition
		class ID
		{
		    private:
				Index m_id;

			public:
				ID()
				{
					m_id = 0;
				}
				
				ID(const Index& id)
				{
					m_id = id;
				}
				
				ID(const ID& stateId)
				{
					m_id = stateId.m_id;
				}

				ID& operator = (const ID& stateId) 
				{
					if (this != &stateId)
					{
						m_id = stateId.m_id;
					}
					return *this; 
				}

				operator Index() const
				{
					return m_id;
				}

				Index id() const
				{
					return m_id;
				}

				
				bool operator == (const ID& other)
				{
					return m_id == other.m_id;
				}

				bool operator != (const ID& other)
				{
					return m_id != other.m_id;
				}

				bool isValid() const
				{
					return m_id != (Index)(-1);
				}



		};

		//#pragma endregion

		//members
		//data
	private:
		
		//wont be useful
///////////////////////////////////////////////////////////////////
        std::wstring   m_name; // the name of the state
		std::wstring   m_alias;//wont be necessary
///////////////////////////////////////////////////////////////////
        
		Props     m_props;  //the proposition of the state, used to store the rechability mainly
		const ID  m_id;
		static NameValidator m_nameValidator;

	//constants
	private:
		static const Props cInitFlagMask;			
		static const Props cMarkFlagMask;			
		static const Props cReachSetFlagMask;			
		static const Props cReachableFlagMask;			
		static const Props cDefaultStateProps;	


      //functions
	public:
		DesState(void);
		DesState(DesState::ID stateId);
		DesState(DesState::ID stateId, const DesState& otherState);
		DesState(const DesState& otherState); //copy constructor
		
		virtual ~DesState(void);
                //operator overloading,
		//copying
		DesState& operator= (const DesState& otherState);

		//comparing 
		bool operator == (const DesState& otherState) const
		{
			return ((m_id == otherState.m_id) && 
				   (m_name == otherState.m_name) &&
				   (m_alias == otherState.m_alias) &&
				   (m_props == otherState.m_props));
		}

		bool operator != (const DesState& otherState) const
		{
			return !(*this == otherState);
		}

        public:
            
			
			
			
		
			// set and get the name alias and properties, might not be necessary
/////////////////////////////////////////////////////////////////////////////////////////////////////////////////
                //name
		std::wstring getName(void) const
		{
                        return m_name; // the name of the state
		}
		
		void setName(const std::wstring& newName)
		{
			if (m_nameValidator.validate(newName))
			{
				m_name = newName;
			}
			else
			{
				std::wstring message = L"Invalid state name (";
				message += newName;
				message += L"). Use an alpha-numeric string (a-z;A-Z;0-9;.-_)";
				throw message;
			}
		}
		void setIDasName()
		{
		    std::wstringstream s;
            s<<m_id.id();
	        m_name=s.str();
		}


                // alias
		std::wstring getAlias(void) const
		{
			return (m_alias.empty() == false) ? m_alias : m_name;
		}
		
		void setAlias(const std::wstring& newAlias)
		{
			if (m_nameValidator.validate(newAlias))
			{
				m_alias = newAlias;
			}
			else
			{
				std::wstring message = L"Invalid state alias (";
				message += newAlias;
				message += L"). Use an alpha-numeric string (a-z;A-Z;0-9;.-_)";
				throw message;
			}
		}

/////////////////////////////////////////////////////////////////////////////////////////////////////////








                //props
		Props  getProps(void) const
		{
			return m_props;
		}
		
		void setProps(const Props& newProps)
		{
			m_props = newProps;
		}
                //initial state

		bool isInit(void) const
		{
			return (m_props & cInitFlagMask) != 0;
		}

		void setInit(bool isInit = true)
		{
			if (isInit)
			{
				setProps(m_props | cInitFlagMask);
			}
			else
			{
				setProps(m_props & ~cInitFlagMask);
			}
		}

		void toggleInit()
		{
			setInit(!isInit());
		}

                //marked state
		bool isMarked(void) const
		{
			return (m_props & cMarkFlagMask) != 0;
		}
		void setMarked(bool isMarked = true)
		{
			if (isMarked)
			{
				setProps(m_props | cMarkFlagMask);
			}
			else
			{
				setProps(m_props & ~cMarkFlagMask);
			}
		}
		void toggleMarked()
		{
			setMarked(!isMarked());
		}

                //reachablility

                //get the current state's reachabililty
		ReachableProp getReachState() const
		{
                    //the reachability was not set
			if ((m_props & cReachSetFlagMask) == 0)
			{
				return eReachableNotVerified;
			}
			else 
			{
				//Reachabiliyty was set so check to see if the state is reachable or not
				if ((m_props & cReachableFlagMask) != 0)
				{
					return eReachableYes;
				}
				else
				{
					return eReachableNo;
				}
			}
		}

		void setReachabilityState(ReachableProp reachState)
		{
			switch(reachState)
			{
				case eReachableYes:
					//set the ReachSet and the Reachable flags
					setProps(m_props | cReachSetFlagMask);					
					setProps(m_props | cReachableFlagMask);					
					break;

				case eReachableNo:
					//set the ReachSet flag to 1 and the Reachable flag to zero
					setProps(m_props | cReachSetFlagMask);					
					setProps(m_props & ~cReachableFlagMask);
					break;

				case eReachableNotVerified:
					//make sure the ReachSet flag is zero (not set)
					setProps(m_props & ~cReachSetFlagMask);					

					//reset the Reachable flag so that we at least do not assume the state is reachable by mistake when
					//in fact it is unknown
					setProps(m_props & ~cReachableFlagMask);
					break;

				default:
					assert(false);
			}
		}
		
		bool isReachKnown() const
		{
			return (m_props & cReachSetFlagMask) != 0;
		}
		
		bool isReachable(void) const
		{
			if ((m_props & cReachSetFlagMask) == 0)
			{
				//the reachability was never set so it is unknown
				assert(false);
				throw EX("Reachability has not been set. Cannot tell if the state is reachable or not");
			}

			return ((m_props & cReachSetFlagMask) != 0) && ((m_props & cReachableFlagMask) != 0);
		}

		void setReachable(bool isReachable = true)
		{			
			if (isReachable)
			{
				setProps(m_props | cReachableFlagMask);
			}
			else
			{
				setProps(m_props & ~cReachableFlagMask);
			}

			//mark the flag that signifies that the reachability was set
			setProps(m_props | cReachSetFlagMask);
		}

		void toggleReachable()
		{
			setReachable(!isReachable());
		}

		const ID getId() const
		{
			return m_id;
		}

		//reset the fields of the state to their initial values. This makes it possible
		//to reuse state as templates
		void reset();
		void resetAlias();

		
};

} //end of namespace DESpot
