/*	Author: Zain Ajaz
	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
	2012 - 2013

*/

#include "CounterExampleAlgo.h"
#include<assert.h>
namespace DESpot{

	StateInfoTree tree(100000);
	
	CounterExampleAlgo::CounterExampleAlgo():MAXEventSeqLength(80),ModifiedLength(MAXEventSeqLength),ProcessedLevel(0)
	{
	}

	 
	CounterExampleAlgo::~CounterExampleAlgo()
	{
		if(tranMap!=null)
		{
			delete tranMap;
			tranMap=null;
		}
		if(FoundList!=null)
		{
			delete FoundList;
			FoundList=null;
		}
		if(main_pendinglist!=null)
		{
			delete main_pendinglist;
			main_pendinglist=null;
		}
		if(!(m_FinalState.empty()))
			this->m_FinalState.clear();
		
		
	}
	//=======================================================================================

	void CounterExampleAlgo::addInputDes(DesProject::DesIteratorPtr desIterator)
	{
	for(desIterator->first(); desIterator->notDone(); desIterator->next())
	{
		addInputDes(&desIterator->currentItem());
	}
	}
	void CounterExampleAlgo::addInputDes(const Des* inDes)
	{
	//Make sure the same Des is not added twice
	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 CounterExampleAlgo::SetFinalState(CEStateTuple & tuple)
	{
		m_FinalState=tuple;
	}

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

       //load turpleStorage
		FoundList=new AlgoTrie(m_inDesSet);		
		main_pendinglist=new PendingQueue(DesNum);
		
	}

	
	void CounterExampleAlgo::createInitialStateTuple() //--2
	{
		CEStateTuple 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;
			
		}

	    
        FoundList->insert(&tuple);       
		TempSTN=tree.AllocateNode();
		TempSTN->prev=NULL;
		TempSTN->Event=0;
		main_pendinglist->Enque(tuple,Level=0,TempSTN);
		Is_FinalState(tuple);
	}
	

	void CounterExampleAlgo::Is_FinalState(CEStateTuple& tuple)
	{	for(short i=0;i<tuple.size();i++)
		{
			if(tuple[i] != m_FinalState[i])
			{m_isFinalState= false;
			return;
			}
		}
	
	m_isFinalState= true;
	}
	bool CounterExampleAlgo::ModifyEvSeqLength()
	{bool OK=false;
			if(Level==MAXEventSeqLength)
			  {
				 ModifiedLength = QInputDialog::getInteger(NULL, "DESpot","Maximum length of 80 events for counter example was reached.\nPlease enter a new length.\n(Note: the new length should be greater than 80.)", 85, 81, 1000, 2, &OK);
				 ProcessedLevel=Level;	
				 if(!OK) return false;
			  }
			  else 
			  if(Level==ModifiedLength)
			  {	
				  QString msg("Modified length of %1 events for counter example was reached.\nPlease enter a new length.\n(Note: the new length should be greater than %1.)");
				  msg=msg.arg(ModifiedLength);
				  ModifiedLength = QInputDialog::getInteger(NULL, "DESpot",msg, (ModifiedLength+2), (ModifiedLength+1), 1000, 2, &OK);
				 ProcessedLevel=Level;	
				 if(!OK) return false;				  
			  }
		  
	return true;
}

	void CounterExampleAlgo::createEvLookupTab()
{
	
	
	for(m_eventIt->first(); m_eventIt->isDone() == false; m_eventIt->next())
	{
		ProjectEvent& ev = m_eventIt->currentItem();
		m_EvlookupTab.insert(QString::fromStdWString(ev.getName()),&ev);
	}

	;
}

	void CounterExampleAlgo::CreateCntrExmp(StateInfoNode *Final)
	{ 
		ProjectEventSet temp;
		long i=0,j=1;
		createEvLookupTab();
		while(Final->prev)
		{	
			DesEventRef=tranMap->getEvent((short)Final->Event);
			wstring EventName= DesEventRef->getName();
			QString ProjEvName=QString::fromStdWString(EventName);
			ProjEvRef = m_EvlookupTab.value(ProjEvName.arg(ProjEvName));
			temp.insert((unsigned long)i,ProjEvRef);
			i++;
			//m_CEEventSet.insert(Level,ProjEvRef);
			Final=Final->prev;
		}
		i--;
		
		while(i>=0)
		{ //projectEventSet.values(key);
			m_CEEventSet.insert((unsigned long)j,temp.value((unsigned long)i));
			j++;
			i--;
		}		
	}

	ProjectEventSet CounterExampleAlgo::GetCounterExample()
	{
		return m_CEEventSet;
	}

	void CounterExampleAlgo::prepareRun()
	{
		if (m_inDesSet.size() < 2)
		{
		throw EX("The MEET algorithm requires at least two input DES.");
		}
	
	loadProductDes();
    createInitialStateTuple();
	
	}

	bool CounterExampleAlgo::runAlgo()
	{
	prepareRun();
	//for testing
	//m_FinalState[3]=-1;
	bool flag=false;	
	while(m_isFinalState==false)
	 {	
		  runonce=true;
		  CEStateTuple crtSrcStateTuple(DesNum);
		  if(!(main_pendinglist->itemCount() < 0))
		  {
			TempSTN=main_pendinglist->Deque(crtSrcStateTuple,Level); 
				if(Level==MAXEventSeqLength && Level !=ProcessedLevel)
				{
					if(!ModifyEvSeqLength())
					return false;
				}
				else if(Level>MAXEventSeqLength && Level==ModifiedLength && Level!= ProcessedLevel)
				{
					if(!ModifyEvSeqLength())
					return false;
				}
		  }
		  else
		  {
			   QMessageBox ErrorMsg;
			   ErrorMsg.setWindowTitle("DESpot");
			   QPushButton *OK = ErrorMsg.addButton("OK", QMessageBox::AcceptRole);
			   ErrorMsg.setIcon(QMessageBox::Critical);
			   ErrorMsg.setText("The error state provided by the algorithm could not be found, please inform the DESpot developers.");
			   ErrorMsg.exec();
			   return false;
		  }

		  
		 
		  for(short i=1;i<EventNum;i++)
		  { 
			  CEStateTuple 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;// ignores the rest of the states in the tuple and jumps to the next event
				  } 				

				  if(j==DesNum-1)
				  {  // Last state in the tuple					 
					  if(FoundList->search(&temptuple)==false)
					  {
						  FoundList->insert(&temptuple);					 
						  NextNode = tree.AllocateNode();
						  NextNode->Event = i;
						  NextNode->prev = TempSTN;
						  main_pendinglist->Enque(temptuple,(Level+1),NextNode);
						  Is_FinalState(temptuple);
						  if(m_isFinalState)
						  {
							  flag=true;
							  break;
						  }
					  }
					  
				  }

			  }
			  if(flag)  break;
		  }		  
	 }
	
		if(runonce==true)
		CreateCntrExmp(NextNode);    	
			 
	return true;
	}

	
}
