/*************************************************************************
  FILE:  BddHiscSub.h
  DESCR: Header file for Sub*.cpp (subsystem processing file)
  AUTH:  Raoguang Song
  Supervisor: Dr. Ryan Leduc
  DATE:  (C) Jan, 2006
*************************************************************************/
#ifndef _BddHiscSUB_H_
#define _BddHiscSUB_H_

#include <string>
#include <map>
#include "BddHiscType.h"
#include "BddHiscDES.h"
#include <fstream>
#include <fdd.h>
#include "BddHisc.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 CSub
    {
    public: //public methods
        CSub(const string &  vsSubFile, int viSubIndex);
        virtual ~CSub();
        virtual unsigned short AddSubEvent(const string & vsEventName,
                                           const EVENTSUB vEventSub,
                                           const EVENTTYPE vEventType);
        virtual int PrintSub(ofstream & fout) = 0;
        virtual int PrintSubAll(ofstream& fout) = 0;
        virtual string SearchEventName(EVENTSUB k,unsigned short usiLocalIndex) = 0;

        virtual int LoadSub(const DESpot::DesSubsystem& subSys) = 0;
        virtual int SynSuper(const HISC_COMPUTEMETHOD computemethod,
                             HISC_SUPERINFO &superinfo,
                             const HISC_SAVESUPERTYPE savetype,
                             const string& savepath) = 0;
        virtual int VeriSub(const HISC_TRACETYPE showtrace,
                            HISC_SUPERINFO & superinfo,
                            const HISC_SAVEPRODUCTTYPE savetype,
                            const string& savepath,
                            const HISC_TESTTYPE testType,Hisc_ChkInfo& checkInfo) = 0;

    public:  //access methods
        virtual string GetSubName() const {return m_sSubName;};
        virtual int GetSubIndex() const {return m_iSubIndex;};
        virtual int GetNumofDES() const
                    {return m_iNumofPlants + m_iNumofSpecs + m_iNumofIntfs;};
        virtual unsigned short GetMaxUnCon(EVENTSUB EventSub)
                    {return m_usiMaxUnCon[EventSub];};
        virtual unsigned short GetMaxCon(EVENTSUB EventSub)
                    {return m_usiMaxCon[EventSub];};
        //Functions imported from DesSubsystem.h to test and set a boolean that determines
        //whether we skip NB/Controllability verification for a given subsystem.
        //Done to support extending Despot to support multi-level systems
        bool extractionSystemSkipTest() const
                            {
                                return (m_ExtractionSystemSkipTest == true);
                            };
        void setExtractionSystemSkipTest(bool extractionSystemSkipTestFlag)
                            {
                                m_ExtractionSystemSkipTest = extractionSystemSkipTestFlag;
                            };

    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();
        bool m_ExtractionSystemSkipTest;    //Whether or not to skip Controllability/NB Verification for a subsys

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

        int DESReorder();

        //SaveSuper related methods
        int SaveSuper(const bdd & bddReach, const HISC_SAVESUPERTYPE savetype,
                        const string & savepath);
        int PrintStateSet(ofstream & fout, const bdd & bddStateSet,
                            STATES & statesMap, int viSetFlag);
        int PrintEvents(ofstream & fout);
        int PrintTextTrans(ofstream & fout, bdd & bddController,
                             EVENTSUB EventSub, unsigned short usiLocalIndex,
                             const bdd & bddReach, string sEventName,
                             STATES & statesMap);
        bdd SimplifyController(const bdd & bddController, EVENTSUB EventSub,
                                const unsigned short usiIndex);

    protected:  //fields
        string m_sSubFile;   //this subsytem file name(".sub") with path.
        string m_sSubName;   //This subsystem name
        int m_iSubIndex;      //This subsystem index (High: 0 Low: 1,2,...)

        int m_iNumofPlants;   //Number of Plant DES
        int m_iNumofSpecs;    //Number of Specification DES
        int m_iNumofIntfs;    //Number of Interface 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)
        LOCALEVENTS m_SubEventsMap; //save all the events map in this subsytems
                                    //(name(key), local index(16 bits))
                                    //just for compute local event index.
        unsigned short m_usiMaxCon[6]; //Max index of controllable events (1,3,...) (expanded to LD events --H.I.)
        unsigned short m_usiMaxUnCon[6];//Max index of uncontrollable events(2,4,..) (expanded to LD events --H.I.)

        /*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 int 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
        //4: Low data events --H.I.
        //5: Child low data events --H.I. 2014
        //////////////////////////////////////////////////////////////////
        //Transition predicates
        bdd *m_pbdd_ConTrans[6];
        bdd *m_pbdd_UnConTrans[6];
        bdd *m_pbdd_UnConPlantTrans[6];
        //variable(DES index) set for transition predicates
        bdd *m_pbdd_ConVar[6];
        bdd *m_pbdd_ConVarPrim[6];
        bdd *m_pbdd_UnConVar[6];
        bdd *m_pbdd_UnConVarPrim[6];
        //plant part variables
        bdd *m_pbdd_UnConPlantVar[6];
        bdd *m_pbdd_UnConPlantVarPrim[6];
        bdd *m_pbdd_ConPhysicVar[6];   //for simplifying controller (note: physical)
        bdd *m_pbdd_ConPhysicVarPrim[6];//for simplifying controller (note:physical)
        //variable pairs(normal-prime)
        bddPair **m_pPair_Con[6];
        bddPair **m_pPair_UnCon[6];
        bddPair **m_pPair_ConPrim[6];
        bddPair **m_pPair_UnConPrim[6];
    };
} //end of namespace BDDHISC

#endif //_BddHiscSUB_H_
