#pragma once

#include <vector>
#include <map>
#include "Des.h"
#include "DesState.h"
#include "DesEvent.h"
#include "DesAlgo.h"
#include <string>
#include <iostream>
#include <QMessageBox>
#include <sstream>
#include <set>
#include "ProductTransitionMap.h"
#include "TireStorage.h"
#include <deque>
#include "PendingStructure.h"
#include "NonBlockingAlgo.h"
#include "DesTypes.h"
#include "CounterExampleAlgo.h"

namespace DESpot
{	
	
	class Des;

	class MultiNonBlockingAlgo :public DesAlgo
	{
       //--------------type  define-----------------------

	public:
		//for regular syn
		typedef std::vector<const Des*> DesSet;
		typedef DesSet::iterator DesSetIt;
	    typedef std::vector<short> SrcStateTuple; 
	    typedef std::deque<SrcStateTuple*> SourceStateList;
        // for nonblocking--- new add
	    typedef std::deque<int> NonblockCheckList;
	    typedef std::set<int> BlockedStateList;

		typedef std::list<std::wstring> ErrorList;
	    typedef ErrorList::iterator ErrorListIt;
		


         //-----------------data define------------------------------
		public:
		DesSet m_inDesSet;
		bool m_checkDesIntegrity;
	public:
		static const std::wstring cMultiNonBlockingAlgoDesc;
		static const std::wstring cMultiNonBlockingAlgoErr;
	public:
	    short DesNum;
        short EventNum;
        short StateMaxNum;
        short ***transitionMatrix;
	    SourceStateList m_pendingList;
	    NonblockTrie *turpleStorage;
        ProductTransitionMap *tranMap;
		PendingVector *main_pendinglist;
		
		
	//-----for nonblocking algo
		bool *markchecker;
	public:
		NonblockCheckList m_nonblocklist;
        int nonblocknumber;
		BlockedStateList m_blockstatelist;
		bool isnonblocked;
		ErrorList m_inErrorList;


     //--------------function define----------------------------
	public:
		MultiNonBlockingAlgo(bool checkIntegrity = true);
		virtual ~MultiNonBlockingAlgo(void);
	public:
		void addInputDes(const Des* inDes);
	public:
		virtual bool runAlgo();
	public:
		virtual void prepareRun();
	public:
		void overrideNonBlocking(bool nonBlocking);
		void loadProductDes();
		void createInitialStateTuple();
		void fillErrorList(SrcStateTuple &in_tuple);
		//void pushPending(SrcStateTuple* tuple);
		//std::vector<short>* popPending();
		//void pendinglistClear();
		//bool ispendingEmpty();
      // nonblocking operation
		void reachableCheck();
		int nonblockingCheck();
		void BlockedStateCheck();
		virtual const ErrorList& getErrorList();
		virtual bool canUseTransition(short in_eventId);
		bool isNonBlocking() const;
		int getDesNum();
		NonBlockingAlgo m_non_algo;
		bool m_integrity;
		void setIntegrity(bool in_m_integrity);

	};
}   //End of namespace DESpot
