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

*/

#pragma once
#include "CounterExampleAlgo_BDDLwNB.h"
#include <string>
namespace DESpot
{
	
	 CounterExampleAlgo_BDDLwNB::CounterExampleAlgo_BDDLwNB(const DesHierProject* Project,
															DesProject::EventIteratorPtr eventIt,
															BDDHISC::Hisc_ChkInfo& checkInfo)
	 														
	{
	m_eventIt=eventIt;
	tranMap=NULL;
	FoundList=NULL;
	main_pendinglist=NULL;
	Level=0;
	m_isFinalState=false;
	runonce=false;
	//testing
	//std::wstring fakesubsys = (L"fake name");
	//const DesSubsystem& m_subsystem=Project->getSubsystem(fakesubsys);
	const DesSubsystem& m_subsystem=Project->getSubsystem(checkInfo.getErrorSubsystemName());

	if(m_subsystem.getLevel() == 0)
	{
		// for high level Subsystem
		int i=0;
		this->m_FinalState.resize(checkInfo.CE_tuplemap.size());
		bool StateFound=false;
		DesSubsystem::DesIteratorPtr desIT=m_subsystem.createDesIterator();
			for(desIT->first(); desIT->notDone(); desIT->next(),i++)
			{
				QString tempName = QString::fromStdWString(desIT->currentItem().getName());
				std::string DesName=tempName.toStdString();
				addInputDes(&desIT->currentItem());
				DESpot::Des::StateIteratorPtr stateitr = desIT->currentItem().createStateIterator();
				StateFound=false;
				if(checkInfo.CE_tuplemap.find(DesName)==checkInfo.CE_tuplemap.end())
				{
					QString Terr ="Fatal Error: The error tuple provided by the algorithm did not have an entry for the DES \"%1\". Please inform DESpot developers.";
					QString DesNameErr=Terr.arg(QString::fromStdString(DesName));
					QMessageBox::critical(NULL, "DESpot",DesNameErr);	
				}
					for(stateitr->first();stateitr->notDone();stateitr->next())
					{	
						if(stateitr->currentItem().getName() == checkInfo.CE_tuplemap[DesName])
						{
							m_FinalState[i]=stateitr->currentItem().getId();
							StateFound=true;
							break;

						}
						
					}
					if(!StateFound)
						{
							QString tempError = "The current state name \"%1\" was not found in the statepool of \"%2\" DES. Please inform the DESpot developers";
							QString Statename = QString::fromStdWString(checkInfo.CE_tuplemap[DesName]);
							QString DESName	= QString::fromStdString(DesName);
							QString StateLookupError=tempError.arg(Statename,DESName);							
							QMessageBox::critical(NULL, "DESpot",StateLookupError);	
						}

			}	
		DesHierProject::InterfIteratorPtr interfIt = Project->createInterfIterator();
		for(interfIt->first(); interfIt->notDone(); interfIt->next())
		{
			const DesInterface& interf = interfIt->currentItem();
			DesSubsystem::DesIteratorPtr IntrfDesIT = interf.createDesIterator();
			for(IntrfDesIT->first(); IntrfDesIT->notDone(); IntrfDesIT->next(),i++)
			{
				QString tempName2 = QString::fromStdWString(IntrfDesIT->currentItem().getName());
				std::string DesName=tempName2.toStdString();
				addInputDes(&IntrfDesIT->currentItem());
				DESpot::Des::StateIteratorPtr stateitr = IntrfDesIT->currentItem().createStateIterator();
				StateFound=false;
				if(checkInfo.CE_tuplemap.find(DesName)==checkInfo.CE_tuplemap.end())
				{
					QString Terr ="Fatal Error: The error tuple provided by the algorithm did not have an entry for the DES \"%1\". Please inform DESpot developers.";
					QString DesNameErr=Terr.arg(QString::fromStdString(DesName));
					QMessageBox::critical(NULL, "DESpot",DesNameErr);	
				}
					for(stateitr->first();stateitr->notDone();stateitr->next())
					{	
						if(stateitr->currentItem().getName() == checkInfo.CE_tuplemap[DesName])
						{
							m_FinalState[i]=stateitr->currentItem().getId();
							StateFound=true;
							break;
						}						

					}
					if(!StateFound)
						{
							QString tempError = "The current state name \"%1\" was not found in the statepool of \"%2\" DES. Please inform the DESpot developers";
							QString Statename = QString::fromStdWString(checkInfo.CE_tuplemap[DesName]);
							QString DESName	= QString::fromStdString(DesName);
							QString StateLookupError=tempError.arg(Statename,DESName);							
							QMessageBox::critical(NULL, "DESpot",StateLookupError);	
						}
			}
		}		
	}

	else if(m_subsystem.getLevel() > 0)
	{	
		// for Low level Subsystem	
		int i=0;
		this->m_FinalState.resize(checkInfo.CE_tuplemap.size());
		bool StateFound=false;
		DesSubsystem::DesIteratorPtr desIT=m_subsystem.createDesIterator();
			for(desIT->first(); desIT->notDone(); desIT->next(),i++)
			{
				QString tempName = QString::fromStdWString(desIT->currentItem().getName());
				std::string DesName=tempName.toStdString();
				addInputDes(&desIT->currentItem());
				DESpot::Des::StateIteratorPtr stateitr = desIT->currentItem().createStateIterator();
				StateFound=false;
				if(checkInfo.CE_tuplemap.find(DesName)==checkInfo.CE_tuplemap.end())
				{
					QString Terr ="Fatal Error: The error tuple provided by the algorithm did not have an entry for the DES \"%1\". Please inform DESpot developers.";
					QString DesNameErr=Terr.arg(QString::fromStdString(DesName));
					QMessageBox::critical(NULL, "DESpot",DesNameErr);	
				}
					for(stateitr->first();stateitr->notDone();stateitr->next())
					{	
						if(stateitr->currentItem().getName() == checkInfo.CE_tuplemap[DesName])
						{
							m_FinalState[i]=stateitr->currentItem().getId();
							StateFound=true;
							break;
						}
						
					}
					if(!StateFound)
						{
							QString tempError = "The current state name \"%1\" was not found in the statepool of \"%2\" DES. Please inform the DESpot developers";
							QString Statename = QString::fromStdWString(checkInfo.CE_tuplemap[DesName]);
							QString DESName	= QString::fromStdString(DesName);
							QString StateLookupError=tempError.arg(Statename,DESName);							
							QMessageBox::critical(NULL, "DESpot",StateLookupError);	
						}
			}			
		DesSubsystem::DesIteratorPtr IntrfDesIT = m_subsystem.getInterface().createDesIterator();
			for(IntrfDesIT->first(); IntrfDesIT->notDone(); IntrfDesIT->next(),i++)
			{
				QString tempName2 = QString::fromStdWString(IntrfDesIT->currentItem().getName());
				std::string DesName=tempName2.toStdString();
				addInputDes(&IntrfDesIT->currentItem());
				DESpot::Des::StateIteratorPtr stateitr = IntrfDesIT->currentItem().createStateIterator();
				StateFound=false;
				if(checkInfo.CE_tuplemap.find(DesName)==checkInfo.CE_tuplemap.end())
				{
					QString Terr ="Fatal Error: The error tuple provided by the algorithm did not have an entry for the DES \"%1\". Please inform DESpot developers.";
					QString DesNameErr=Terr.arg(QString::fromStdString(DesName));
					QMessageBox::critical(NULL, "DESpot",DesNameErr);	
				}
					for(stateitr->first();stateitr->notDone();stateitr->next())
					{	
						if(stateitr->currentItem().getName() == checkInfo.CE_tuplemap[DesName])
						{
							m_FinalState[i]=stateitr->currentItem().getId();
							StateFound=true;
							break;
						}
						
					}
					if(!StateFound)
						{
							QString tempError = "The current state name \"%1\" was not found in the statepool of \"%2\" DES. Please inform the DESpot developers";
							QString Statename = QString::fromStdWString(checkInfo.CE_tuplemap[DesName]);
							QString DESName	= QString::fromStdString(DesName);
							QString StateLookupError=tempError.arg(Statename,DESName);							
							QMessageBox::critical(NULL, "DESpot",StateLookupError);	
						}

			}
	}

	}

	
	 CounterExampleAlgo_BDDLwNB::~CounterExampleAlgo_BDDLwNB()
	{//base distructor will be invoked automatically and will free the resources
	}
}