#pragma once

#include <string>
#include <sstream>
#include <QMessageBox>
#include <set>
#include <map>
#include <vector>
#include "DesProject.h"
#include "Des.h"
#include "DesInterface.h"
#include "DesSubsystem.h"
#include "ProductTransitionMap.h"
#include "TireStorage.h"
#include "PendingStructure.h"

namespace DESpot
{



class IntPN5_6
{
	//--------------typedefine--------------------
public:
	typedef std::vector<const Des*> DesSet;
	typedef DesSet::iterator DesSetIt;
	typedef DesSet::const_iterator DesSetCIt;
    //---algo use-----
	typedef std::set<int> MarkedStateSet;
	typedef MarkedStateSet MarkedStateSetIt;
	typedef std::vector<short> SrcStateTuple; 
	typedef std::deque<SrcStateTuple*> SourceStateList;
	typedef std::deque<int> NonblockCheckList;
	typedef std::set<int> BlockedStateList;
	typedef std::set<int> SemiMarkedStateSet;
	typedef std::set<int>::iterator SemiMarkedStateSetIt;

	typedef std::deque<short> RequestEventList;


	//pn5 use
	typedef std::set<short> AnswerEventList;
	typedef std::set<short>::iterator AnswerEventListIt;


public:
	int interface_Poistion;
	DesSet m_inDesSet;
	const DesSubsystem& m_subsystem;
	const DesInterface& m_interf;

public:
	short DesNum;
    short EventNum;
    short StateMaxNum;
    short ***transitionMatrix;

public:
	SourceStateList m_pendingList;
	IntPN6Trie *turpleStorage;
    ProductTransitionMap *tranMap;
    // new add
	NonblockCheckList m_nonblocklist;
    int nonblocknumber;
    bool *markchecker;
	bool ispn6right;
	bool ispn5right;

	PendingVector* m_pendinglist;
	PendingVector* m_requestList;
	RequestEventList request_event_list;
	


	


public:
	IntPN5_6(const DesInterface& in_interf,const DesSubsystem& in_subsystem):interface_Poistion(-1),m_interf(in_interf),m_subsystem(in_subsystem),ispn6right(false),ispn5right(true)
	{

	}
	~IntPN5_6()
	{
		if(tranMap!=NULL)
		{
			delete tranMap;
			tranMap=NULL;
		}
		if(turpleStorage!=NULL)
		{
			delete turpleStorage;
			turpleStorage=NULL;
		}
		if(m_pendinglist!=NULL)
		{
			delete m_pendinglist;
			m_pendinglist=NULL;
		}
		if(m_requestList!=NULL)
		{
			delete m_requestList;
			m_requestList=NULL;
		}
	}
	

	
	void addInputIntfDes(DesProject::DesIteratorPtr desIterator)
	{
		for(desIterator->first(); desIterator->notDone(); desIterator->next())
		{
			addInputDes(&desIterator->currentItem());
			interface_Poistion++;
		}
	}

	void addInputSubDes(DesProject::DesIteratorPtr desIterator)
	{
		for(desIterator->first(); desIterator->notDone(); desIterator->next())
		{
			addInputDes(&desIterator->currentItem());
			
		}
	}

	void addInputDes(const Des* inDes)
	{
		for (unsigned int iDes = 0; iDes < m_inDesSet.size(); ++iDes)
		{
			if (inDes == m_inDesSet[iDes])
			{
				throw EX("A DES with the same name already exists in the list of input DES. Cannot add.")
			}
		}
		m_inDesSet.push_back(inDes);
	}








    void loadSubSystemInterface() //--1
	{
      addInputIntfDes(m_interf.createDesIterator());
	  addInputSubDes(m_subsystem.createDesIterator());

	}
	void loadProductDes() //--2
	{
		//load ProductTransitionMap
		tranMap= new ProductTransitionMap (m_inDesSet);
        DesNum=tranMap->getDesNum();
		EventNum=tranMap->getEventNum();
        StateMaxNum=tranMap->getStateMaxNum();
        transitionMatrix=tranMap->getTransitionMatrix();

       //load turpleStorage
		turpleStorage=new IntPN6Trie(m_inDesSet);
		//+add
		m_pendinglist=new PendingVector(DesNum,500);
		m_requestList=new PendingVector(DesNum,200);
	}

	void createInitialStateTuple() //--3
	{
		SrcStateTuple tuple(DesNum);
		for(short i=0;i<DesNum;i++)
		{
           
			const unsigned long long itmp=m_inDesSet[i]->getInitialState().getId().id();
            unsigned long long tmp=itmp;
			tuple[i]=(short)tmp;
		}

	   //put into finishlist
        turpleStorage->insert(&tuple,interface_Poistion);
		m_pendinglist->PushPending(tuple);
	}

    bool canUseTransition(short in_eventId)
	{
		return tranMap->isLowEvent(in_eventId);// only care about the reverse transition of the lowevent
	}



	void fillRequestStateList(short id,SrcStateTuple& in_tuple)
	{
		if(tranMap->isRequestEvent(id)==true)
		{
			request_event_list.push_back(id);
			m_requestList->PushPending(in_tuple);
		}
	}
    void prepareRun()
	{

		loadSubSystemInterface();
        loadProductDes();
		createInitialStateTuple();
	}

	void reachableCheck()
	{
		prepareRun();
		
     //----------------------1:check and fill table only care about the lowevent for PN6 and fill the request state list for PN5---------------------
		while(m_pendinglist->isEmpty()==false)
		{
			SrcStateTuple crtSrcStateTuple(DesNum);
			m_pendinglist->PopPending(crtSrcStateTuple);
		    int m_id=turpleStorage->getStateId(&crtSrcStateTuple);
		    for(short i=1;i<EventNum;i++)
			{
				SrcStateTuple temptuple(DesNum);
			    for(short j=0;j<DesNum;j++)
			    {
					short from_state=crtSrcStateTuple[j];
				    short to_state=transitionMatrix[j][i][from_state];
					if(to_state!=-1)
				    {
						temptuple[j]=to_state;
				    }
					else
				    {
					    break;
				    }
				    if(j==DesNum-1)
				    {  // at end of the entry; the whole tuple is finished
					    bool useEvent=canUseTransition(i);
					    if(turpleStorage->search(&temptuple,m_id,useEvent)==false)
					    {
							//add for pn6
						    turpleStorage->insert(&temptuple,m_id,useEvent,interface_Poistion);
							m_pendinglist->PushPending(temptuple);
							//add for pn5
							fillRequestStateList(i,temptuple);
					    }
				    }
				}
			}
		}
		turpleStorage->destoryMemory();
	}


	int pn6Check()
	{
	     //---------2:verify the pn6 valid-----------------
       //precheck--Got lucky: point 6 was sucessful by default - there are no semi marked states


		if(turpleStorage->semi_set.empty()==true)
		{
			ispn6right=true;
			turpleStorage->destoryAllState();
			turpleStorage->destoryAllStateList();
			if(m_pendinglist!=NULL)
			{
				delete m_pendinglist;
				m_pendinglist=NULL;
			}
			return 0;
		}
		int state_count=turpleStorage->getStateCount();
	    markchecker=new bool[state_count];
	    for(int i=0;i<state_count;i++)
		{
			markchecker[i]=false;
	    }
	    while(turpleStorage->m_queue.empty()==false)
	    {
			int mark_id=turpleStorage->m_queue.front();
		    turpleStorage->m_queue.pop_front();
		    nonblocknumber++;
		    markchecker[mark_id]=true;
		    m_nonblocklist.push_back(mark_id);
	    }

		SemiMarkedStateSet& s_set=turpleStorage->semi_set;
	    int state_id;
	    State *pend_state;
	    while(m_nonblocklist.empty()==false)
		{
			state_id=m_nonblocklist.front();
		    m_nonblocklist.pop_front();
		    pend_state=turpleStorage->getState(state_id);

		    for(int i=0;i<=pend_state->returnUpperBound();i++)
		    {
				int temp_id=pend_state->getValue(i);
			    if(markchecker[temp_id]==false)
				{
					nonblocknumber++;
				    markchecker[temp_id]=true;
				    m_nonblocklist.push_back(temp_id);
					
					if(s_set.empty()==true)
				    {
						ispn6right=true;
					    turpleStorage->destoryAllState();
			            turpleStorage->destoryAllStateList();
						if(m_pendinglist!=NULL)
						{
							delete m_pendinglist;
				            m_pendinglist=NULL;
						}
					    return 0;
					}
				    else
					{
					    SemiMarkedStateSetIt it=s_set.find(temp_id);
				        if(it!=s_set.end())
					    {
							s_set.erase(it);
						    if(s_set.empty()==true)
						    {
								ispn6right=true;
							    turpleStorage->destoryAllState();
			                    turpleStorage->destoryAllStateList();
								if(m_pendinglist!=NULL)
								{
									delete m_pendinglist;
				                    m_pendinglist=NULL;
			                    }
							    return 0;
							}
						}
					}
				}
			}
			
			if(nonblocknumber==state_count)
		    {
			    break;
			}
		}



      if(ispn6right==false)
	  {
		  for(SemiMarkedStateSetIt it=s_set.begin();it!=s_set.end();it++)
		  {
			  	SrcStateTuple temp(DesNum);
				m_pendinglist->GetTurple(*it,temp);
				std::wstring interface_name;
				std::wstring subsystem_name;
				getInterfaceSubsystemName(temp,interface_name,subsystem_name);
		//	addError(errorMessage(cSemiMarkStateError, m_subsystem.getName(),subsystem_name, m_interf.getName(), interface_name));
		  }
	  }



		turpleStorage->destoryAllState();
	    turpleStorage->destoryAllStateList();
		if(m_pendinglist!=NULL)
		{
				delete m_pendinglist;
				m_pendinglist=NULL;
		}
	    return 0;
	}
	
	












    int pn5Check()
	{

		while(m_requestList->isEmpty()==false)
		{
			//step1: get the reqest event state from the pending list
			SrcStateTuple reqtemp(DesNum);
		    m_requestList->PopPending(reqtemp);
			short request_event_id=request_event_list.front();
			request_event_list.pop_front();

			//step2: fill the answer event list
			AnswerEventList answer_event_list;
		    for(short i=1;i<EventNum;i++)
			{
			    for(short j=0;j<=interface_Poistion;j++)
				{

					short from_state=reqtemp[j];
				    short to_state=transitionMatrix[j][i][from_state];
					if(to_state==-1)
				    {
						break;
				    }
				    if(j==interface_Poistion)
				    {  //fill this answer event into the list
						if(tranMap->isAnswerEvent(i)==true)
						{
							answer_event_list.insert(i);
						}

				    }
				}
			}
            //step3: process the event
			//create the pendinglist and fill the first entry
			PendingList temp_pendinglist(DesNum,100);
			temp_pendinglist.PushPending(reqtemp);
			//create the trie and fill insert the first entry
			AlgoTrie temp_trie(m_inDesSet);
			temp_trie.insert(&reqtemp);
			while(temp_pendinglist.isEmpty()==false&&answer_event_list.empty()==false)
			{
				SrcStateTuple crtSrcStateTuple(DesNum);
				temp_pendinglist.PopPending(crtSrcStateTuple);
			    for(short i=1;i<EventNum;i++)
				{
					SrcStateTuple temptuple(DesNum);
			        for(short j=0;j<DesNum;j++)
					{
						short from_state=crtSrcStateTuple[j];
				        short to_state=transitionMatrix[j][i][from_state];
					    if(to_state!=-1)
						{
							temptuple[j]=to_state;
						}
					    else
				        {
					        break;
				        }
				        if(j==DesNum-1)
				        {  // at end of the entry; the whole tuple is finished
							if(tranMap->isAnswerEvent(i)==true)
							{
								AnswerEventListIt it=answer_event_list.find(i);
								if(it!=answer_event_list.end())
								{
									answer_event_list.erase(it);
								}
							}
							if(temp_trie.search(&temptuple)==false&&tranMap->isLowEvent(i)==true)
							{
								temp_trie.insert(&temptuple);
								temp_pendinglist.PushPending(temptuple);
							}
					    }
					}
				}
			}

			//step4: report error
			if(answer_event_list.empty()==false)
			{
				ispn5right=false;
			    std::wstring interface_name;
				std::wstring subsystem_name;
				std::wstring request_event_name=tranMap->getEvent(request_event_id)->getName();
				getInterfaceSubsystemName(reqtemp,interface_name,subsystem_name);
				for(AnswerEventListIt it=answer_event_list.begin();it!=answer_event_list.end();it++)
				{
					std::wstring answer_event_name=tranMap->getEvent(*it)->getName();
			       // addError(errorMessage(cAnsNotImpl, subsystem_name, m_subsystem.getName(),request_event_name,
										                // answer_event_name, interface_name, m_interf.getName(),  
														// answer_event_name)); 
				}
				if(m_requestList!=null)
				{
					delete m_requestList;
					m_requestList=null;
				}
				return 0;
			}

		}
		ispn5right=true;
				if(m_requestList!=null)
				{
					delete m_requestList;
					m_requestList=null;
				}
		return 0;

	}




	void getInterfaceSubsystemName(SrcStateTuple& tuple,std::wstring& intName,std::wstring& subName)
	{
		std::wstringstream intstream;
		std::wstringstream substream;
		intstream<<"Interface";
		substream<<"Subsystem";
		for(int i=0;i<=interface_Poistion;i++)
		{
			intstream<<m_inDesSet[i]->getState(tuple[i]).getName();
			intstream<<"-";
		}
		intName=intstream.str();
		for(int j=interface_Poistion;j<DesNum;j++)
		{
			substream<<m_inDesSet[j]->getState(tuple[j]).getName();
			substream<<"-";
		}
		subName=substream.str();
    }


	
	void runAlgo()
	{
		reachableCheck();
		pn5Check();
		pn6Check();

		if(ispn6right==true&&ispn5right==true)
		{
			std::string k="pn6 pn5 true";
	        QMessageBox::information(NULL,"t",k.c_str());
		}
		else
		{
			std::string k="false";
	        QMessageBox::information(NULL,"t",k.c_str());
		}

	}



 



};
}