/*	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 <deque>
#include <vector>
#include <map>
#include "ControllabilityAlgo.h"
#include "Des.h"
#include "DesState.h"
#include "DesEvent.h"
#include "EventTranslator.h"

namespace DESpot
{
	class CtrlStdAlgo : public ControllabilityAlgo
	{
		//Types___________________________________________________________
		public:
			struct ClosedState
			{				
				const DesState* plantState;
				
				//the state in the supervisor
				const DesState* supState;	

				ClosedState()
				{
					plantState = null;
					supState = null;
				}

				ClosedState(const DesState* plantState, const DesState* supState)
				{
					this->plantState = plantState;
					this->supState = supState;
				}

				void set(const DesState* plantState, const DesState* supState)
				{
					this->plantState = plantState;
					this->supState = supState;
				}

				void clear()
				{
					plantState = null;
					supState = null;
				}
			};

						
			struct ParentInfo
			{
				//The parent of a closed state (null for the initial state)
				ClosedState parentState;

				//the event in the plant DES that led to the closed loop state
				const DesEvent* exitEvent; 

				ParentInfo()
				{
					exitEvent = null;
				}

				ParentInfo(const ClosedState& parentState, const DesEvent* exitEvent)
				{
					this->exitEvent = exitEvent;
					this->parentState = parentState;
				}

				void set(const DesEvent* exitEvent, const DesState* plantState, const DesState* supState)
				{
					this->exitEvent = exitEvent;
					this->parentState.set(plantState, supState);
				}

				void clear()
				{
					exitEvent = null;
					parentState.clear();
				}
			};			

			struct CtrlBehaviour : ClosedState
			{
				const DesEvent* event;

				CtrlBehaviour()
				{
					event = null;
				}

				CtrlBehaviour(ClosedState& state, const DesEvent* event)
				{
					this->event = event;
					this->plantState = state.plantState;
					this->supState = state.supState;
				}

				void set(const DesState* plantState, const DesState* supState, const DesEvent* event)
				{
					this->event = event;
					ClosedState::set(plantState, supState);
				}

				void clear()
				{
					event = null;
					ClosedState::clear();
				}
			};

			typedef std::list<CtrlBehaviour> CounterExample;
			typedef CounterExample::const_iterator BehavIt;

		//Initialization___________________________________________________________
		public:
			CtrlStdAlgo(void);
			CtrlStdAlgo(Des* plantDes, Des* supDes);
			virtual ~CtrlStdAlgo(void);

			void setPlantDes(Des* plantDes);
			void setSupervisorDes(Des* supDes);

		//Operations ___________________________________________________________
		public:
			//Runs the algorithm and return true if the supervisor is controllable for the plant
			virtual bool runAlgo();
		
			//If the supervisor is not controllable for the plant (isControllable() == false) this method
			//provides the counter example: the state of the plant, the state of the DES and the uncontrollable event 
			//being blocked by the supervisor 
			const CtrlBehaviour& getUnctrlBehaviour();

			//Returns a detailed counter example in the form of a trace of (plant-state, sup-state, event) tuples that
			//lead to the uncontrolled behaviour
			const CounterExample& getCounterExample();

		//Implementation methods___________________________________________________________
		protected:
			//prepare the algorithm to run by initializing the different structures most importantly
			//the pending queue. The algorithm starts with the initial state of the plant and supervisor
			virtual void prepareRun();

			//creates a transition iterator out of the given plant state in the plant DES
			virtual Des::TransIteratorPtr createTransIterator(const DesState* plantState);

			//retrives a pending closed loop state out of the pending queue
			ClosedState popPending();
			
			//adds the given state to the pending state for futher processing
			void pushPending(ClosedState& state, const DesEvent* leadEvent = null, const ClosedState& parentState = ClosedState());

			//returns true if the givve closed loop has been found before
			virtual bool found(ClosedState& state);

			//marks the given state as found
			void markFound(ClosedState& state, const DesEvent* leadEvent, const ClosedState& parentState);

			//Obtain the behaviour the lead to the given state
			CtrlBehaviour getPreviousBehaviour(ClosedState& state);
		
		//Data____________________________________________________________________________
		protected:
			//The plant DES
			Des* m_plantDes;
			
			//The supervisor DES for the plant DES - m_plantDes
			Des* m_supDes;

			//The list of pending closed loop behaviours that we need to still analyze
			std::deque<ClosedState> m_pendStates;

			//The structure of found closed loop states: a jagged array: a vector of plant states
			//where the index is the ID of the plant state. For each plant state, the structure stores
			//a vector of supervisor states that were paired with the plants state. This structure insures
			//optimal memory but not optimal speed since the supervisor states are in an array. 
			typedef std::map<DesState::ID, ParentInfo> ClosedStateFindMap;
			typedef ClosedStateFindMap::iterator ClosedStateIt;
			std::vector< std::map<DesState::ID, ParentInfo> > m_foundStates;

			//Translates  plant events into supervisor events based on the name of the events
			EventTranslator m_eventTransl;

			//The uncontrolled behaviour information set when the supervisor is not controllable which tells which
			//uncontrollable event in the plant was blocked by the supervisor and in what supervisor and plant states
			CtrlBehaviour m_unctrlBehaviour;

			//Detailed counter-example trace that shows how system gets to the uncontrolled behaviour
			CounterExample m_counterExample;

		//Constants________________________________________________________________________
		private:
			static const std::wstring cCtrlAlgoDesc;
	};

} //end of namespace DESpot
