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

#pragma once

#include <deque>
#include <map>
#include "DesAlgo.h"
#include "DesHierProject.h"
#include "IntPN5_6.h"


#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 InterfImplCheckAlgo : public DesAlgo
	{

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


//----------------data define
	
public:
	int interface_Poistion;
	DesSet m_inDesSet;
public:
	short DesNum;
    short EventNum;
    short StateMaxNum;
    short ***transitionMatrix;

public:
	SourceStateList m_pendingList;
	IntPN6Trie *turpleStorage;
	//  needto know if have already added a state reached by a
	//	request event.
	MeetSynTrie *tuppleReqEvnStorage;
    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:
			InterfImplCheckAlgo(const DesSubsystem& subsystem);
			~InterfImplCheckAlgo(void);

		public:
			virtual bool runAlgo();

			bool isSubsysImplCorrect() const;

		protected:
			virtual void prepareRun();

	public:
		void addInputIntfDes(DesProject::DesIteratorPtr desIterator);
		void addInputSubDes(DesProject::DesIteratorPtr desIterator);
		void addInputDes(const Des* inDes);
		void loadSubSystemInterface(); //--1
		void loadProductDes(); //--2
		void createInitialStateTuple(); //--3

		bool canUseTransition(short in_eventId);
		void fillRequestStateList(short id,SrcStateTuple& in_tuple);

		void reachableCheck();
		int pn6Check();
		int pn5Check();
		void getInterfaceSubsystemName(SrcStateTuple& tuple,std::wstring& intName,std::wstring& subName);


		protected:
			const DesSubsystem& m_subsystem;
			const DesInterface& m_interf;
			bool m_integrity;
			bool m_subsysImplCorrect;

		private:
			static const std::wstring cInterfImplCheckAlgoDesc;
			static const std::wstring cAnsNotImplForHigh;
			static const std::wstring cAnsNotImplForLow;
			static const std::wstring cSemiMarkStateErrorForHigh;	
			static const std::wstring cSemiMarkStateErrorForLow;	
		// added by zain for counter example
			bool ProcessingFirstError;
	};
}
