/*	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 <map>
#include <deque>
#include <vector>
#include <string>
#include <iostream>
#include <QMessageBox>
#include <sstream>
#include "DesAlgo.h"
#include "DesState.h"
#include "DesEvent.h"
#include "DesProject.h"
#include "TireStorage.h"
#include "ProductTransitionMap.h"
#include "SimRoot.h"
#include "CntrExmpPendingQueue.h"
#include "SimConfig.h"
#include "DesFlatProject.h"
#include "DesHierProject.h"
#include "DesSubsystem.h"
#include "BddHiscMain.h"
#include "qmessagebox.h"
#include "ui_FlatProjectEditor.h"
#include <qmessagebox.h>
#include <qinputdialog.h>

namespace DESpot
{
	
	class CounterExampleAlgo		
		
	{
	//--------------type  define-----------------------	
	public:
		typedef std::vector<const Des*> DesSet;
		typedef DesSet::iterator DesSetIt;
		typedef DesSet::const_iterator DesSetCIt;
	    typedef std::vector<short> CEStateTuple; 
	    typedef std::deque<StateTuple*> SourceStateList;
		typedef map<std::wstring,short> CntrExmpTupleMap;
		enum IConstSubAlgos
			{
				AnsAcptAlgo,
				ReqAcptAlgo,
				IntrfImplAlgo
			};		

	//-----------------data define------------------------------	
	protected:
		DesSet m_inDesSet;
		bool m_checkDesIntegrity;
	    short DesNum;
        short EventNum;
        short StateMaxNum;
        short ***transitionMatrix;
	    SourceStateList m_pendingList;
	    AlgoTrie *FoundList;

		DesProject::EventIteratorPtr m_eventIt;
		QMap<QString,ProjectEvent*> m_EvlookupTab;
		ProjectEventSet m_CEEventSet;
		ProjectEvent *ProjEvRef;
		DesEvent* DesEventRef;
        ProductTransitionMap *tranMap;
		PendingQueue *main_pendinglist;
		
		StateInfoNode* TempSTN;
		StateInfoNode* NextNode;
		
		unsigned long Level;
		const unsigned long MAXEventSeqLength;
		unsigned long long ModifiedLength;
		unsigned long long ProcessedLevel;
	
		bool m_isFinalState;
		CEStateTuple m_FinalState;		
		bool runonce;
		

	//--------------function define----------------------------
	protected:
		CounterExampleAlgo();	
		~CounterExampleAlgo();
	public:
		void addInputDes(const Des* inDes);
		void addInputDes(DesProject::DesIteratorPtr desIterator);	
		bool runAlgo();	
		void prepareRun();	
		void loadProductDes();
		void createInitialStateTuple();
		void Is_FinalState(CEStateTuple& tuple);
		void SetFinalState(CEStateTuple& tuple);
		void CreateCntrExmp(StateInfoNode *);
		void createEvLookupTab();
		bool ModifyEvSeqLength();		
		ProjectEventSet GetCounterExample();			
	};
	
}//end of namespace