/*	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
*/

#include "InterfImplCheckAlgo.h"
namespace DESpot
{

const std::wstring InterfImplCheckAlgo::cInterfImplCheckAlgoDesc = L"Subsys I-Consist Check Algo";

const std::wstring InterfImplCheckAlgo::cAnsNotImplForHigh = L"State '%ls' in high-level subsystem '%ls' was reached by request event '%ls'.  \
Answer event '%ls' possible in state '%ls' of interface '%ls', but there exists no path to allow '%ls' in low-level via low-level events.";
const std::wstring InterfImplCheckAlgo::cAnsNotImplForLow = L"State '%ls' in low-level subsystem '%ls' was reached by request event '%ls'.  \
Answer event '%ls' possible in state '%ls' of interface '%ls', but there exists no path to allow '%ls' in low-level via low-level events.";

const std::wstring InterfImplCheckAlgo::cSemiMarkStateErrorForHigh = L"The high-level subsystem '%ls' cannot reach a marked state from state '%ls' via low-level events, \
															   while interface '%ls' is in state '%ls'";
const std::wstring InterfImplCheckAlgo::cSemiMarkStateErrorForLow = L"The low-level subsystem '%ls' cannot reach a marked state from state '%ls' via low-level events, \
															   while interface '%ls' is in state '%ls'";

//_________________________________________________________________________________________________

InterfImplCheckAlgo::InterfImplCheckAlgo(const DesSubsystem& subsystem) : 
                m_subsystem(subsystem),
                m_interf(subsystem.getInterface()),
                m_subsysImplCorrect(false),
				interface_Poistion(-1),
				ispn6right(false),ispn5right(true)

{
	
	m_description = cInterfImplCheckAlgoDesc;
	m_integrity=false;
	ProcessingFirstError=false;
	tranMap = NULL;
	turpleStorage = NULL;
	m_pendinglist= NULL;
	m_requestList=NULL;
	tuppleReqEvnStorage = NULL;
}





//_________________________________________________________________________________________________

InterfImplCheckAlgo::~InterfImplCheckAlgo(void)
{

		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;
		}
		if(tuppleReqEvnStorage!=NULL)
		{
			delete tuppleReqEvnStorage;
			tuppleReqEvnStorage=NULL;
		}

}

//_________________________________________________________________________________________________

bool InterfImplCheckAlgo::isSubsysImplCorrect() const
{
	return m_subsysImplCorrect;
}

//_________________________________________________________________________________________________

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

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

void InterfImplCheckAlgo::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 InterfImplCheckAlgo::loadSubSystemInterface() //--1
	{
      addInputIntfDes(m_interf.createDesIterator());
	  addInputSubDes(m_subsystem.createDesIterator());

	}
void InterfImplCheckAlgo::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);
	//load for States reached by Req Events lookup
	tuppleReqEvnStorage = new MeetSynTrie(m_inDesSet);
	//+add
	m_pendinglist=new PendingVector(DesNum,500);
	m_requestList=new PendingVector(DesNum,200);
	}

void InterfImplCheckAlgo::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 InterfImplCheckAlgo::canUseTransition(short in_eventId)
	{
		return tranMap->isLowEvent(in_eventId);// only care about the reverse transition of the lowevent
	}



void InterfImplCheckAlgo::fillRequestStateList(short id,SrcStateTuple& in_tuple)
	{
		if(tranMap->isRequestEvent(id)==true)
		{
		  // marked state as seen so only add once
		  tuppleReqEvnStorage->insert(&in_tuple);
		  request_event_list.push_back(id);
		  m_requestList->PushPending(in_tuple);
		}
	}

void InterfImplCheckAlgo::prepareRun()
{
     
		loadSubSystemInterface();
		loadProductDes();
		createInitialStateTuple();
		m_subsysImplCorrect=true;
}

//_________________________________________________________________________________________________



void InterfImplCheckAlgo::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);
		   
		   // need to always add states reached by request
		   // events, but only once
		   if(tuppleReqEvnStorage->search(&temptuple)==false) {
		     fillRequestStateList(i,temptuple);
		   }

		   if(turpleStorage->search(&temptuple,m_id,useEvent)==false)
		     {
		       //add for pn6
		       turpleStorage->insert(&temptuple,m_id,useEvent,interface_Poistion);
		       m_pendinglist->PushPending(temptuple);
		     }
		 }
	     }
	 }
     }
   turpleStorage->destoryMemory();
   // don't need tuppleReqEvnStorage so del
   delete tuppleReqEvnStorage;
   tuppleReqEvnStorage=NULL;
}


int InterfImplCheckAlgo::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;
				if(this->isfirsterror) ProcessingFirstError=true;
				getInterfaceSubsystemName(temp,interface_name,subsystem_name);
				if(m_subsystem.isRoot())
			addError(errorMessage(cSemiMarkStateErrorForHigh, m_subsystem.getName(),subsystem_name, m_interf.getName(), interface_name));
				else
			addError(errorMessage(cSemiMarkStateErrorForLow, 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 InterfImplCheckAlgo::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();
					if(this->isfirsterror)
					ProcessingFirstError=true;
				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();
					if(m_subsystem.isRoot())
			        addError(errorMessage(cAnsNotImplForHigh, subsystem_name, m_subsystem.getName(),request_event_name,
										                answer_event_name, interface_name, m_interf.getName(),  
													    answer_event_name)); 
					else
						 addError(errorMessage(cAnsNotImplForLow, 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 InterfImplCheckAlgo::getInterfaceSubsystemName(SrcStateTuple& tuple,std::wstring& intName,std::wstring& subName)
	{
		std::wstringstream intstream;
		std::wstringstream substream;
		intstream<<L"(";
		substream<<L"(";

		//create state name for interface
		for(int i=0;i<=interface_Poistion;i++)
		{
		  const Des*  blockingDes = m_inDesSet[i];

		  if (i > 0)
		    {
		      intstream<< L", ";
		    }

		  intstream<<blockingDes->getName() << L"/";
		  intstream<<blockingDes->getState(tuple[i]).getName();	
		  if(ProcessingFirstError)
		  this->CE_tuplemap[blockingDes->getName()]=tuple[i];
		}

		intstream << L")";
		intName=intstream.str();

		// create state name for subsystem
		for(int j=interface_Poistion;j<DesNum;j++)
		{
		  const Des*  blockingDes = m_inDesSet[j];

		  if (j > interface_Poistion)
		    {
		      substream<< L", ";
		    }

		  substream<<blockingDes->getName() << L"/";
		  substream<<blockingDes->getState(tuple[j]).getName();

		  // for counter example
		  if(ProcessingFirstError)		  
		  this->CE_tuplemap[blockingDes->getName()]=tuple[j];	
		}

		
		if(ProcessingFirstError)
		{		
		this->setIFailureType(IntrfImplAlgo);
		this->setErrorSubSystemName(m_subsystem.getName());
		this->ErrorSubSystem = &m_subsystem;
		ProcessingFirstError=false;
		this->isfirsterror=false;
		this->IsFirstErrorSubSystem=false;
		}
		
		substream<< L")";
		subName=substream.str();
    }

bool InterfImplCheckAlgo::runAlgo()
{

   m_integrity = m_subsystem.getValidProp() == eIntegYes && m_interf.getValidProp() == eIntegYes ? true : false;

	if ( m_integrity == false)
	{
		throw EX("Either project is not valid, or integrity \
has not yet been checked.");
		 return false;
	}

		reachableCheck();

		pn5Check();
		m_subsysImplCorrect&=ispn5right;
		if(m_subsysImplCorrect==false)
		{
			return false;
		}

		pn6Check();
        m_subsysImplCorrect&=ispn6right;
		if(m_subsysImplCorrect==false)
		{
			return false;
		}
        return true;
}

}
