/*************************************************************************
  FILE:  BddHiscLowSub.h
  DESCR: Header file for LowSub*.cpp (Low-level processing files)
  AUTH:  Raoguang Song
  Supervisor: Dr. Ryan Leduc
  DATE:  (C) Jan, 2006
*************************************************************************/
#ifndef _BddHiscLSUB_H_
#define _BddHiscLSUB_H_
#include <string>
#include <map>
#include "BddHiscType.h"
#include "BddHiscSub.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 CDES;

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

public:
    virtual int PrintSub(ofstream& fout); 
    virtual int PrintSubAll(ofstream & fout); 
    virtual string SearchEventName(EVENTSUB k, 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,
						Hisc_ChkInfo& checkInfo);
    CDES *GetIntfDES();
    
private:
    virtual int MakeBdd();  
    virtual int InitBddFields(); 
    virtual int ClearBddFields(); 
    int CheckIntf();
    int SynPartSuper(const HISC_COMPUTEMETHOD computemethod, 
                                        bdd & bddReach, bdd & bddBad);
    int GenConBad(bdd &bddConBad);
    int VeriConBad(bdd &bddConBad, const bdd &bddReach, string & vsErr);
    int GenP4Bad(bdd &bddP4Bad);
    int VeriP4Bad(bdd &bddP4Bad, 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);
    bdd p5(const bdd& bddP, int &iErr);
    bdd p6(const bdd& bddP, int &iErr);
    void BadStateInfo(const bdd& bddBad, const int viErrCode, 
            const HISC_TRACETYPE showtrace,Hisc_ChkInfo&  checkInfo, const string &vsExtraInfo = "");
	bdd intf_r(const bdd &bddP, int &iErr);
    
private: 
    bdd *m_pbdd_RTrans[2]; //Request event transition predicate in the intf
                            //0: uncon 1: con
    bdd *m_pbdd_ATrans[2];  //Answer event transition predicate in the intf
                            //0: uncon 1: con
    bdd *m_pbdd_LDTrans[2]; //Low data event transition predicate in the intf
                            //0: uncon 1: con
    bdd *m_pbdd_CLDTrans[2]; //Child Low data event transition predicate in the intf
                            //0: uncon 1: con

    bdd m_bddIVar; //normal interface variables
    bdd m_bddIVarPrim; //prime interface variables
    bdd m_bddIntfInit; //Initial state in the intface DES
    bdd m_bddIntfMarking; //Marker states in the interface DES
};


} //end of namespace BDDHISC

#endif //_BddHiscLSUB_H_
