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

  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;    
        m_ALFChkFail = 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; 
      }

    ~SD_ChkInfo(void)
      {

      }
};

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