/*************************************************************************
  FILE:  BddHiscHighSub.h
  DESCR: Header file for HighSub*.cpp (High-level processing files)
  AUTH:  Raoguang Song
  Supervisor: Dr. Ryan Leduc
  DATE:  (C) Jan, 2006
*************************************************************************/
#ifndef _BddHiscHSUB_H_
#define _BddHiscHSUB_H_
#include <string>
#include "BddHiscSub.h"
#include "BddHiscType.h"
#include <fdd.h>


#include "DesProject.h"
#include "ProjectEvent.h"
#include "DesTypes.h"
//#include "DesFlatProject.h"
#include "DesHierProject.h"
#include "Des.h"

using namespace std;

namespace BDDHISC
{

class CHighSub:public CSub
{
public:
    CHighSub(const string &  vsHighFile, int viSubIndex);
    virtual ~CHighSub();

public:
    virtual int PrintSub(ofstream& fout);
    virtual int PrintSubAll(ofstream & fout);
    virtual string SearchEventName(EVENTSUB EventSub, 
                                            unsigned short usiLocalIndex);
    
    virtual int LoadSub(const DESpot::DesSubsystem& subSys);
    virtual int SynSuper(const HISC_COMPUTEMETHOD computemethod, 
                         HISC_SUPERINFO &superinfo, 
                         const HISC_SAVESUPERTYPE savetype, 
                         const string& savepath);
    virtual int VeriSub(const HISC_TRACETYPE showtrace, 
                        HISC_SUPERINFO & superinfo, 
                        const HISC_SAVEPRODUCTTYPE savetype, 
                        const string& savepath,
			const HISC_TESTTYPE testType);

private:
    virtual int MakeBdd();
    int GenConBad(bdd &bddConBad);
    int VeriConBad(bdd &bddConBad, const bdd &bddReach, string & vsErr);
    int GenP3Bad(bdd &bddP3Bad);
    int VeriP3Bad(bdd &bddP3Bad, const bdd &bddReach, string & vsErr);
    int supcp(bdd & bddP);
    bdd cr(const bdd & bddPStart, const bdd & bddP, const int viEventSub, 
            int & iErr);
    bdd r(const bdd &bddP, int &iErr);
    virtual int InitBddFields();
    virtual int ClearBddFields();
    void BadStateInfo(const bdd& bddBad, const int viErrCode, 
                        const HISC_TRACETYPE showtrace, 
                        const string &vsExtraInfo = "");
    
private:
    //Expanded to support LD Events --H.I.
    int *m_piUArr[4]; //Uncontrollable event index array, 0:Request  1:Answer
    int *m_piCArr[4]; //Controllable event index array, 0:Request  1:Answer
    
    bdd *m_pbdd_IVar;           //Interface normal variables
    bdd *m_pbdd_IVarPrim;       //Interface Prime Variables
    bdd *m_pbdd_UnConATrans;    //transition predicate for answer events
                                //(for interface alone).
    bdd *m_pbdd_ConATrans;      //transition predicate for answer events
                                //(only for interface alone).
    bdd *m_pbdd_UnConLDTrans;   //transition predicate for low data events
                                //(for interface alone).
    bdd *m_pbdd_ConLDTrans;     //transition predicate for low data events
                                //(only for interface alone).
};

} //end of namespace BDDHISC

#endif //_BddHiscHSUB_H_
