/*************************************************************************
  FILE:  BddSdLowSub.h
  DESCR: Header file for BddSdLowSub*.cpp (Low-level processing files)
  AUTH:  Raoguang Song, Yu Wang
  DATE:  (C) 2006, 2008
*************************************************************************/
#ifndef _BDDSDLSUB_H_
#define _BDDSDLSUB_H_


#include <string>
#include <map>
#include <stack>
#include "BddSdType.h"
#include "BddSdSub.h"
#include "fdd.h"

#include "BddHiscMain.h"

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



using namespace std;

namespace BDDSD
{

class CDES;
//class Hisc_ChkInfo;
class CLowSub : public CSub
{
public:
    CLowSub(const string & vsLowFile);
    virtual ~CLowSub();

    virtual int PrintSub(ofstream& fout);
    virtual int PrintSubAll(ofstream & fout);
    virtual string SearchEventName(unsigned short usiLocalIndex);

    virtual int LoadSub(DESpot::DesProject& DESpotProj, bool isTimed);
    virtual int VeriSub(const HISC_TRACETYPE showtrace,
                        HISC_SUPERINFO & superinfo,
			SD_TESTTYPE testType,SD_ChkInfo& checkInfo);

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 GenBalemiBad(bdd &bddBalemiBad);
    int VeriBalemiBad(bdd &bddBalemiBad, const bdd &bddReach, string & vsErr);

    int VeriALF(bdd &bddALFBad, bdd bddReach, string & vsErr);
    int VeriProperTimedBehavior(bdd &bddPTBBad, bdd bddReach, string & vsErr);

    int CheckSDControllability(bdd & bddSDBad, const bdd & bddreach, string & vsErr);
    int AnalyseSampledState(bdd & bddSSBad, const bdd & bddreach, const bdd & bddSS,
        list< list<bdd> > & list_NerFail, bdd & bddSF, stack<bdd> & stack_bddSP, string & vsErr);

    int CheckTimedControllability(const EVENTSET & eventsDis, const EVENTSET & eventsPoss);
    int CheckTimedControllability(bdd & bddTCBad, const bdd & bddreach);

    bool RecheckNerodeCells(bdd & bddNCBad, const bdd & bddreach, list< list<bdd> > & list_NerFail);
    bool RecheckNerodeCell(bdd & bddNCBad, const bdd & bddreach, const list<bdd> & Zeqv, list< pair<bdd, bdd> > & listVisited);

    int DetermineNextState(bdd & bddLBBad, const EVENTSET & eventsPoss, const bdd & bddZ, const bdd & bddreach,
        const int & intB, int & intNextFreeLabel, map<int, bdd> & B_map, stack<int> & B_p,
        bdd & bddSF, stack<bdd> & stack_bddSP,
        map<int, EVENTSET> & B_occu, map<int, bdd> & B_conc, string & vsErr);

    void CheckNerodeCells(map<int, bdd> & B_conc, map<int, EVENTSET> & B_occu,
        list< list<bdd> > & list_NerFail);

    int CheckSDiv(bdd & bddSDivBad, const bdd & bddReach);

    EVENTSET GetTransitionEvents(const bdd & bddleave, const bdd & bddenter);

    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, 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, SD_ChkInfo& checkInfo,const string &vsExtraInfo = "");
};

} //end of namespace BDDSD

#endif //_BDDSDLSUB_H_
