/*************************************************************************
  FILE:  BddSdSub.h
  DESCR: Header file for BddSdSub*.cpp (subsystem processing file)
  AUTH:  Raoguang Song, Yu Wang
  DATE:  (C) Jan, 2006, 2009
*************************************************************************/
#ifndef _BDDSDSUB_H_
#define _BDDSDSUB_H_

#include <string>
#include <map>
#include "BddSd.h"
#include "BddSdType.h"
#include "BddSdDES.h"
#include <fstream>
#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 BDDSD
{

class CSub
{
public: //public methods
    CSub(const string &  vsSubFile);
    virtual ~CSub();
    virtual unsigned short AddSubEvent(const string & vsEventName,
                                       const EVENTTYPE vEventType);
    virtual int PrintSub(ofstream & fout) = 0;
    virtual int PrintSubAll(ofstream& fout) = 0;
    virtual string SearchEventName(unsigned short usiLocalIndex) = 0;

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

    void SetErr(const string & vsErrMsg, const int viErrCode);

    int GenEventIndex(const unsigned short vusiLocalEventIndex);
    int SearchPrjEvent(const string & vsEventName);
    int SearchSubEvent(const string & vsEventName);
    INVEVENTS & GetInvAllEventsMap() {return m_InvAllEventsMap;};

    string GetErrMsg() const {return m_sErrMsg;};
    int GetErrCode() const {return m_iErrCode;};
    void ClearErr();

    int AddPrjEvent(const string & vsEventName, const int viEventIndex);

private:
    string m_sErrMsg; //Error msg during processing this project
    int m_iErrCode; //Error code during processing this project

public:  //access methods
    virtual string GetSubName() const {return m_sSubName;};

    virtual int GetNumofDES() const
                {return m_iNumofPlants + m_iNumofSpecs;};
    virtual unsigned short GetMaxUnCon()
                {return m_usiMaxUnCon;};
    virtual unsigned short GetMaxCon()
                {return m_usiMaxCon;};

private: //DES reorder related memebers
    int ** m_piCrossMatrix;
    int DESReorder_Sift();
    double TotalCross_Sift(double dOldCross, double dSwapCross,
                            int iCur, int iFlag);
    double cross(int i, int j);
    int DESReorder_Force();
    void UpdatePos();
    void InsertDES(int iCur, int iPos);
    double TotalCross_Force();
    double Force(int i);
    int InitialDESOrder();

protected:  //protected methods
    virtual string GetDESFileFromSubFile(const string & vsSubFile,
                    const string &vsDES);
    virtual int MakeBdd() = 0;
    virtual int InitBddFields();
    virtual int ClearBddFields();

    int DESReorder();

    int PrintStateSet(const bdd & bddStateSet, int viSetFlag);
    void PrintStateSet2(const bdd & bddStateSet);
    bdd GetOneState(const bdd & bddStates);
    int CountStates(const bdd & bddStateSet);

    int PrintEvents(ofstream & fout);
    int PrintTextTrans(ofstream & fout, bdd & bddController,
                         unsigned short usiLocalIndex,
                         const bdd & bddReach, string sEventName,
                         STATES & statesMap);
    bdd SimplifyController(const bdd & bddController, const unsigned short usiIndex);

protected:  //fields
    string m_sSubFile;   //this subsytem file name(".sub") with path.
    string m_sSubName;   //This subsystem name

    int m_iNumofPlants;   //Number of Plant DES
    int m_iNumofSpecs;    //Number of Specification DES
                          //(High: all interface DES; Low: 1)

    CDES **m_pDESArr;     //DES Array for all the DES in high or low levels.
                          //(High: including all interface DES,
                          //Low: only including 1 DES for this subsystem)

    EVENTSET m_SubPlantEvents;
    EVENTSET m_SubSupervisorEvents;

    LOCALEVENTS m_SubEventsMap; //save all the events map in this subsytems
                                //(name(key), local index(16 bits))
                                //just for compute local event index.
    LOCALINVEVENTS m_InvSubEventsMap;

    EVENTS m_AllEventsMap; //The map containing all the events in this project
                           //(Event Name (key), Event global index)
    INVEVENTS m_InvAllEventsMap; //The map containing all the events in this
                                //project (Event global index (key), Event Name)

    unsigned short m_usiMaxCon; //Max index of controllable events (1,3,...)
    unsigned short m_usiMaxUnCon;//Max index of uncontrollable events(2,4,..)

    /*BDD needed fields*/
    int m_iNumofBddNormVar; //Num of BDD normal variables in the sub.
    int *m_piDESOrderArr; //DES indices organized as clusters.
    int *m_piDESPosArr; //DES positions in the m_piDESOrderArr

    bdd m_bddInit;  //Initial state predicate
    bdd m_bddMarking;  //Marking states predicate
    bdd m_bddSuper; //The generated supervisor

    //////////////////////////////////////////////////////////////////
    //Transition predicates and its variable sets, variable pairs.
    //0: High level events
    //1: Request events
    //2: Answer events
    //3: Low level events
    //////////////////////////////////////////////////////////////////
    //Transition predicates
    bdd *m_pbdd_ConTrans;
    bdd *m_pbdd_ConPlantTrans;
    bdd *m_pbdd_ConSupTrans;
    bdd *m_pbdd_UnConTrans;
    bdd *m_pbdd_UnConPlantTrans;
    bdd *m_pbdd_UnConSupTrans;

    //variable(DES index) set for transition predicates
    bdd *m_pbdd_ConVar;
    bdd *m_pbdd_ConVarPrim;
    bdd *m_pbdd_UnConVar;
    bdd *m_pbdd_UnConVarPrim;
    //plant part variables
    bdd *m_pbdd_UnConPlantVar;
    bdd *m_pbdd_UnConPlantVarPrim;
    bdd *m_pbdd_ConPhysicVar;   //for simplifying controller (note: physical)
    bdd *m_pbdd_ConPhysicVarPrim;//for simplifying controller (note:physical)
    //supervisor part variables
    bdd *m_pbdd_UnConSupVar;
    bdd *m_pbdd_UnConSupVarPrim;
    bdd *m_pbdd_ConSupVar;   //for simplifying controller (note: physical)
    bdd *m_pbdd_ConSupVarPrim;//for simplifying controller (note:physical)
    //variable pairs(normal-prime)
    bddPair **m_pPair_Con;
    bddPair **m_pPair_UnCon;
    bddPair **m_pPair_ConPrim;
    bddPair **m_pPair_UnConPrim;
};

} //end of namespace BDDSD

#endif //_BDDSDSUB_H_
