/*************************************************************************
  FILE:  BddSdTmp.h
  DESCR: customized data types
  AUTH:  Raoguang Song, Yu Wang
  DATE:  (C) Jan, 2006, 2008
*************************************************************************/
#ifndef _BDDSDCHKINFO_H_
#define _BDDSDCHKINFO_H_

#include  <QString>

using namespace std;

namespace BDDSD
{


/*
 * A class for storing information for an SD Check
 * For an SD check that does all TDES properties below, then they will
 * use just this CLASS, not one of the derived classes.
 */

class SD_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 multi-property checks
    bool m_NBChkFail;   // was check successful? 
    bool m_CtrlChkFail;   // was check successful? 
    bool m_TDESCtrlChkFail;   // was check successful? 
    bool m_SDCtrlChkFail;   // was check successful? 
    bool m_PropTimedBChkFail;   // was check successful? 
    bool m_SSingPhibBChkFail;   // was check successful? 
    bool m_PCompltChkFail;   // was check successful? 
    bool m_ALFChkFail;   // was check successful? 

	// Added by zain for counter example
		map<std::string,std::wstring> CE_tuplemap;
		typedef std::vector<short> CounterExampleStateTuple;
		enum IConstSubAlgos
			{
				AnsAcptAlgo,
				ReqAcptAlgo,
				IntrfImplAlgo
			};
	protected:
		bool isfirsterror;		
		std::wstring ErrorSubSystemName;	
		IConstSubAlgos FailureType;
		bool CEgenerated;
	public: 
		inline void setErrorFlag(){isfirsterror=false;}
		inline bool getErrorFlag(){return isfirsterror;}	
		
		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;}

		inline void setErrorAlgoFlag(bool in_flag){CEgenerated=in_flag;}
		inline bool getErrorAlgoFlag(){return CEgenerated;}

  public:
    SD_ChkInfo(void)
      {
	m_chkPassed = true;
	m_headerStr = "";
	m_succStr = "";
	m_errStr = "";
	m_NBChkFail = false;   
	m_CtrlChkFail = false;    
	m_TDESCtrlChkFail = false;  
        m_SDCtrlChkFail = false;   
        m_PropTimedBChkFail = false;    
        m_SSingPhibBChkFail = false;   
        m_PCompltChkFail = false;    
        isfirsterror=true;
		//FirstErrorTuple=NULL;
		m_ALFChkFail = false;    
		 CEgenerated=false;

      }

    SD_ChkInfo(QString headerInfo)
      {
	m_chkPassed = true;
	m_headerStr = headerInfo;
	m_succStr = "";
	m_errStr = "";
	m_NBChkFail = false;   
	m_CtrlChkFail = false;    
	m_TDESCtrlChkFail = false;  
        m_SDCtrlChkFail = false;   
        m_PropTimedBChkFail = false;    
        m_SSingPhibBChkFail = false;   
        m_PCompltChkFail = false;    
        m_ALFChkFail = false;
		isfirsterror=true;
		//FirstErrorTuple=NULL;
		CEgenerated=false;
      }

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

//  the following classes are to allow an overloaded to distinguish a
//  test type based upon the class that is passed into it.


/**
 * A class for storing information for nonblocking check
 * */
 class SD_NBChkInfo  : public SD_ChkInfo
{

  public:
    SD_NBChkInfo(void)
      {
      }

     SD_NBChkInfo(QString headerInfo): SD_ChkInfo(headerInfo)
      {
      }

    ~SD_NBChkInfo(void)
      {
      }
};

/**
 * A class for storing information for untimed controllability check
 * */
 class SD_CtrlChkInfo  : public SD_ChkInfo
{

  public:
    SD_CtrlChkInfo(void)
      {
      }

     SD_CtrlChkInfo(QString headerInfo): SD_ChkInfo(headerInfo)
      {
      }

    ~SD_CtrlChkInfo(void)
      {
      }
};

/**
 * A class for storing information for TDES controllability check
 * */
 class SD_TCtrlChkInfo  : public SD_ChkInfo
{

  public:
    SD_TCtrlChkInfo(void)
      {
      }

     SD_TCtrlChkInfo(QString headerInfo): SD_ChkInfo(headerInfo)
      {
      }

    ~SD_TCtrlChkInfo(void)
      {
      }
};

/**
 * A class for storing information for SD controllability check
 * */
 class SD_SDCtrlChkInfo  : public SD_ChkInfo
{

  public:
    SD_SDCtrlChkInfo(void)
      {
      }

     SD_SDCtrlChkInfo(QString headerInfo): SD_ChkInfo(headerInfo)
      {
      }

    ~SD_SDCtrlChkInfo(void)
      {
      }
};

/**
 * A class for storing information for Proper timed behavior check
 * */
 class SD_PTBChkInfo  : public SD_ChkInfo
{

  public:
    SD_PTBChkInfo(void)
      {
      }

     SD_PTBChkInfo(QString headerInfo): SD_ChkInfo(headerInfo)
      {
      }

    ~SD_PTBChkInfo(void)
      {
      }
};

/**
 * A class for storing information for S-singular prohibitable behavior check
 * */
 class SD_SSingPChkInfo  : public SD_ChkInfo
{

  public:
    SD_SSingPChkInfo(void)
      {
      }

     SD_SSingPChkInfo(QString headerInfo): SD_ChkInfo(headerInfo)
      {
      }

    ~SD_SSingPChkInfo(void)
      {
      }
};



/**
 * A class for storing information for Plant completeness check
 * */
 class SD_PCmpltChkInfo  : public SD_ChkInfo
{

  public:
    SD_PCmpltChkInfo(void)
      {
      }

     SD_PCmpltChkInfo(QString headerInfo): SD_ChkInfo(headerInfo)
      {
      }

    ~SD_PCmpltChkInfo(void)
      {
      }
};

/**
 * A class for storing information for Activity Loop Free check
 * */
 class SD_ALFChkInfo  : public SD_ChkInfo
{

  public:
    SD_ALFChkInfo(void)
      {
      }

     SD_ALFChkInfo(QString headerInfo): SD_ChkInfo(headerInfo)
      {
      }

    ~SD_ALFChkInfo(void)
      {
      }
};


} //end of namespace BDDSD

#endif //_BDDSDCHKINFO_H_
