/*************************************************************************
  FILE:  BddHiscMain.h
  DESCR: Header file for main.cpp
  AUTH:  Raoguang Song
  Supervisor: DR. Ryan Leduc
  DATE:  (C) Jan, 2006
*************************************************************************/
#pragma once

#include  <QString>
#include "BddHisc.h"
#include "DesProject.h"
#include <map>


namespace BDDHISC
{

using namespace std;

/**
 * A class for storing information for an HISC Check
 * */
class Hisc_ChkInfo
{
  public:
    bool m_chkPassed;   /* was check successful? */
    QString m_headerStr;  /* header info for successful test announce */
    QString m_succStr;  /* body of message successful test announce */
    QString m_errStr;  /* error info when test fails */
    // next used only for CheckAll
    bool m_iConsisChkFail;   /* was check successful? */ 
    bool m_LDNBChkFail;   /* was check successful? */ 
    bool m_LDCtrlChkFail;   /* was check successful? */ 

	// Added by zain for counter example
	public:
		map<std::string,std::wstring> CE_tuplemap;
		typedef std::vector<short> CounterExampleStateTuple;
		enum IConstSubAlgos
			{
				AnsAcptAlgo,
				ReqAcptAlgo,
				IntrfImplAlgo
			};
	protected:
		bool isfirsterror;
		//CounterExampleStateTuple* FirstErrorTuple;
		std::wstring ErrorSubSystemName;	
		IConstSubAlgos FailureType;
	public: 

		inline void setErrorFlag(){isfirsterror=false;}
		inline bool getErrorFlag(){return isfirsterror;}
	
		//inline CounterExampleStateTuple* getErrorTuple(){return FirstErrorTuple;}
		//void setErrorTuple(int size,CounterExampleStateTuple in_tuple);		

		inline std::wstring getErrorSubsystemName(){return ErrorSubSystemName;}
		inline void setErrorSubSystemName(std::wstring in_name){ErrorSubSystemName=in_name;}

		inline IConstSubAlgos getIFailureType(){return FailureType;}
		inline void setIFailureType(IConstSubAlgos in_type){FailureType=in_type;}

		

  public:
    Hisc_ChkInfo(void)
      {
	m_chkPassed = true;
	m_headerStr = "";
	m_succStr = "";
	m_errStr = "";
	m_iConsisChkFail = false;
	m_LDNBChkFail = false;
	m_LDCtrlChkFail = false;
	isfirsterror=true;
	//FirstErrorTuple=NULL;
   
      }

    Hisc_ChkInfo(QString headerInfo)
      {
	m_chkPassed = true;
	m_headerStr = headerInfo;
	m_succStr = "";
	m_errStr = "";
	  // the next three lines were just added.  Need to test that
    // they are alright there
    m_iConsisChkFail = false;
    m_LDNBChkFail = false;
	m_LDCtrlChkFail = false;
	isfirsterror=true;
	//FirstErrorTuple=NULL;
      }

    ~Hisc_ChkInfo(void)
      {
		  
		  if(!this->CE_tuplemap.empty())
			CE_tuplemap.clear();
      }
};



/**
 * A class for storing information for lw nonblocking check
 * */
 class Hisc_LWNBChkInfo  : public Hisc_ChkInfo
{

  public:
    Hisc_LWNBChkInfo(void)
      {
      }

     Hisc_LWNBChkInfo(QString headerInfo): Hisc_ChkInfo(headerInfo)
      {
      }

    ~Hisc_LWNBChkInfo(void)
      {
      }
};

/**
 * A class for storing information for susbsystem lw nonblocking check
 * */
 class Hisc_SubLWNBChkInfo  : public Hisc_ChkInfo
{
  public:
    QString m_subsystName;   /* DESpot subsystem Name */

  public:
    Hisc_SubLWNBChkInfo(void)
      {
	m_subsystName = "";
      }

 Hisc_SubLWNBChkInfo(QString headerInfo, QString subName): 
    Hisc_ChkInfo(headerInfo),
      m_subsystName(subName)
      {
      }

    ~Hisc_SubLWNBChkInfo(void)
      {
      }
};



/**
 * A class for storing information for lw cont check
 * */
class Hisc_LWContChkInfo  : public Hisc_ChkInfo
{
  public:
    Hisc_LWContChkInfo(void)
      {
      }

    Hisc_LWContChkInfo(QString headerInfo): Hisc_ChkInfo(headerInfo)
      {
      }

    ~Hisc_LWContChkInfo(void)
      {
      }
};

/**
 * A class for storing information for subsystem lw cont check
 * */
class Hisc_SubLWContChkInfo  : public Hisc_ChkInfo
{
  public:
    QString m_subsystName;   /* DESpot subsystem Name */

  public:
    Hisc_SubLWContChkInfo(void)
      {
	m_subsystName = "";
      }

    Hisc_SubLWContChkInfo(QString headerInfo, QString subName): 
    Hisc_ChkInfo(headerInfo),
      m_subsystName(subName)
      {
      }

    ~Hisc_SubLWContChkInfo(void)
      {
      }
};


/**
 * A class for storing information for I consist check
 * */
class Hisc_IConsisChkInfo  : public Hisc_ChkInfo
{
  public:
    Hisc_IConsisChkInfo(void)
      {
      }

    Hisc_IConsisChkInfo(QString headerInfo): Hisc_ChkInfo(headerInfo)
      {
      }

    ~Hisc_IConsisChkInfo(void)
      {
      }
};

/**
 * A class for storing information for subsystem I consist check
 * */
class Hisc_SubIConsisChkInfo  : public Hisc_ChkInfo
{
  public:
    QString m_subsystName;   /* DESpot subsystem Name */

  public:
    Hisc_SubIConsisChkInfo(void)
      {
	m_subsystName = "";
      }

    Hisc_SubIConsisChkInfo(QString headerInfo, QString subName): 
    Hisc_ChkInfo(headerInfo),
      m_subsystName(subName)
      {
      }

    ~Hisc_SubIConsisChkInfo(void)
      {
      }
};


/**
 * A class for storing information for LD intf check
 * */
class Hisc_LDIntfChkInfo : public Hisc_ChkInfo
{
  public:
    QString m_theIntfName;   /* DESpot interface Name */

  public:
    Hisc_LDIntfChkInfo(void)
      {
	m_theIntfName = "";
      }

 Hisc_LDIntfChkInfo(QString headerInfo, QString intfName): 
    Hisc_ChkInfo(headerInfo),
      m_theIntfName(intfName)
      {
      }

    ~Hisc_LDIntfChkInfo(void)
      {
      }
};


/**
 * A class for storing information for lw synthesis
 * */
 class Hisc_LWSynthChkInfo  : public Hisc_ChkInfo
{

  public:
    Hisc_LWSynthChkInfo(void)
      {
      }

     Hisc_LWSynthChkInfo(QString headerInfo): Hisc_ChkInfo(headerInfo)
      {
      }

    ~Hisc_LWSynthChkInfo(void)
      {
      }
};

/**
 * A class for storing information for susbsystem lw synthesis
 * */
 class Hisc_SubLWSynthChkInfo  : public Hisc_ChkInfo
{
  public:
    QString m_subsystName;   /* DESpot subsystem Name */

  public:
    Hisc_SubLWSynthChkInfo(void)
      {
	m_subsystName = "";
      }

 Hisc_SubLWSynthChkInfo(QString headerInfo, QString subName): 
    Hisc_ChkInfo(headerInfo),
      m_subsystName(subName)
      {
      }

    ~Hisc_SubLWSynthChkInfo(void)
      {
      }
};





  int getchoice(bool bPrjLoaded, const char *scPrjFile);
  char getkeystroke(char *allowed_choices, int len);
  int getchoice_savesup();
  int getchoice_saveproduct();
  int getchoice_tracetype();
  int BddHiscMain(DESpot::DesProject& DESpotProj);
  int BddHiscCheckHISCAll(DESpot::DesProject& DESpotProj,
			  Hisc_ChkInfo& checkInfo); 
  int BddHiscCheckLWNonBlk(DESpot::DesProject& DESpotProj, QString
			 SubsName, bool isHigh, Hisc_ChkInfo& checkInfo); 
  int BddHiscCheckLWCtrl(DESpot::DesProject& DESpotProj, QString
			 SubsName, bool isHigh, Hisc_ChkInfo& checkInfo); 
  int BddHiscCheckIConsist(DESpot::DesProject& DESpotProj, QString
			SubsName, bool isHigh, Hisc_ChkInfo& checkInfo); 
  int BddHiscCheckIntf(DESpot::DesProject& DESpotProj, QString
			SubsName, bool isHigh, Hisc_ChkInfo& checkInfo); 
  int BddHiscLWSynth(DESpot::DesProject& DESpotProj, char OutFileType,
		       QString filePath, QString SubsName, bool isHigh, Hisc_ChkInfo& checkInfo);
  int BddHiscCheckProp(DESpot::DesProject& DESpotProj, QString
		       SubsName, bool isHigh, HISC_TESTTYPE testType,
		       Hisc_ChkInfo& checkInfo);


  //  the following classes will be used for selecting the right method
  //  based on the class passed to it.



} //end of namespace BDDHISC
