/*************************************************************************
  FILE:  BddHiscSub.cpp
  DESCR: Processing subsystem file(.sub)
  AUTH:  Raoguang Song
  Supervisor: Dr. Ryan Leduc
  DATE:  (C) Jan, 2006
*************************************************************************/
#include "BddHiscSub.h"
#include <string>
#include "BddHiscDES.h"
#include <map>
#include <cassert>
#include <fdd.h>
#include "BddHiscPubfunc.h"
#include "BddHiscErrmsg.h"
#include "BddHiscType.h"
#include "BddHiscProject.h"

using namespace std;


namespace BDDHISC
{
    extern CProject *pPrj;

    /**
     * DESCR:   Constructor
     * PARA:    vsSubFile: subsystem file name with path (.sub)(input)
     *          viSubIndex: subsystem index (high: 0, low: 1,2,...)(input)
     * RETURN:  None
     * ACCESS:  public
     */
    CSub::CSub(const string & vsSubFile, int viSubIndex)
    {
        m_sSubFile = vsSubFile;
        m_sSubName.clear();
        m_iSubIndex = viSubIndex;

        m_iNumofPlants = -1;
        m_iNumofSpecs = -1;
        m_iNumofIntfs = -1;

        //Initialize to false so that the default behaviour would be to not skip any kind of
        //verification on any subsystem.
        m_ExtractionSystemSkipTest = false;

        m_pDESArr = NULL;

        m_SubEventsMap.clear();

        //Initializes MaxCon and MaxUnCon. Notice that one gets initialized to
        // 0 and the other to 0xFFFF so that when events are added, controllable
        // event indices remain odd and uncontrollable indices remain even.
        // (updated to support LD events) --H.I.
        for (int k = H_EVENT; k < NUMBER_OF_EVENTS; k++)
        {
            m_usiMaxCon[k] = 0xFFFF;
            m_usiMaxUnCon[k] = 0x0;
        }
        m_piDESOrderArr = NULL;
        m_piDESPosArr = NULL;

        InitBddFields();
    }

    /**
     * DESCR:   Destructor
     * PARA:    None
     * RETURN:  None
     * ACCESS:  public
     */
    CSub::~CSub()
    {
        if (m_pDESArr != NULL)
        {
            int iNumofDES = this->GetNumofDES();

            for (int i = 0; i < iNumofDES; i++)
            {
                if (m_pDESArr[i] != NULL)
                {
                    if (m_pDESArr[i]->GetDESType() == INTERFACE_DES && m_iSubIndex == 0)
                        continue;
                    else
                    {
                        delete m_pDESArr[i];
                        m_pDESArr[i] = NULL;
                    }
                }
            }
            delete[] m_pDESArr;
            m_pDESArr = NULL;
        }
        delete[] m_piDESOrderArr;
        m_piDESOrderArr = NULL;
        delete[] m_piDESPosArr;
        m_piDESPosArr = NULL;

        ClearBddFields();
    }

    /*
     * DESCR:   Initialize BDD related data members
     * PARA:    None
     * RETURN:  0
     * ACCESS:  protected
     */
    int CSub::InitBddFields()
    {
        m_iNumofBddNormVar = 0;
        m_bddInit = bddtrue;
        m_bddMarking = bddtrue;
        m_bddSuper = bddfalse;

        for (int k = H_EVENT; k < NUMBER_OF_EVENTS; k++)
        {
            m_pbdd_ConTrans[k] = NULL;
            m_pbdd_UnConTrans[k] = NULL;
            m_pbdd_UnConPlantTrans[k] = NULL;

            m_pbdd_ConVar[k] = NULL;
            m_pbdd_ConVarPrim[k] = NULL;

            m_pbdd_UnConVar[k] = NULL;
            m_pbdd_UnConVarPrim[k] = NULL;

            m_pbdd_UnConPlantVar[k] = NULL;
            m_pbdd_UnConPlantVarPrim[k] = NULL;

            m_pbdd_ConPhysicVar[k] = NULL;
            m_pbdd_ConPhysicVarPrim[k] = NULL;

            m_pPair_Con[k] = NULL;
            m_pPair_UnCon[k] = NULL;
            m_pPair_ConPrim[k] = NULL;
            m_pPair_UnConPrim[k] = NULL;
        }
        return 0;
    }

    /*
     * DESCR:   Release memory for BDD related data members
     * PARA:    None
     * RETURN:  0
     * ACCESS:  protected
     */
    int CSub::ClearBddFields()
    {
        for (int k = H_EVENT; k < NUMBER_OF_EVENTS; k++)
        {
            delete[] m_pbdd_ConTrans[k];
            m_pbdd_ConTrans[k] = NULL;

            delete[] m_pbdd_UnConTrans[k];
            m_pbdd_UnConTrans[k] = NULL;

            delete[] m_pbdd_UnConPlantTrans[k];
            m_pbdd_UnConPlantTrans[k] = NULL;

            delete[] m_pbdd_ConVar[k];
            m_pbdd_ConVar[k] = NULL;
            delete[] m_pbdd_UnConVar[k];
            m_pbdd_UnConVar[k] = NULL;

            delete[] m_pbdd_ConVarPrim[k];
            m_pbdd_ConVarPrim[k] = NULL;
            delete[] m_pbdd_UnConVarPrim[k];
            m_pbdd_UnConVarPrim[k] = NULL;

            delete[] m_pbdd_UnConPlantVar[k];
            m_pbdd_UnConPlantVar[k] = NULL;
            delete[] m_pbdd_UnConPlantVarPrim[k];
            m_pbdd_UnConPlantVarPrim[k] = NULL;

            delete[] m_pbdd_ConPhysicVar[k];
            m_pbdd_ConPhysicVar[k] = NULL;
            delete[] m_pbdd_ConPhysicVarPrim[k];
            m_pbdd_ConPhysicVarPrim[k] = NULL;


            if (m_pPair_UnCon[k] != NULL)
            {
                for (int i = 0; i < m_usiMaxUnCon[k]; i += 2)
                {
                    if (m_pPair_UnCon[k][i/2] != NULL)
                    {
                        bdd_freepair(m_pPair_UnCon[k][i/2]);
                        m_pPair_UnCon[k][i/2] = NULL;
                    }
                }
                delete[] m_pPair_UnCon[k];
                m_pPair_UnCon[k] = NULL;
            }

            if (m_pPair_Con[k] != NULL)
            {
                for (int i = 1; i < (unsigned short)(m_usiMaxCon[k] + 1); i += 2)
                {
                    if (m_pPair_Con[k][(i - 1)/2] != NULL)
                    {
                        bdd_freepair(m_pPair_Con[k][(i - 1)/2]);
                        m_pPair_Con[k][(i - 1)/2] = NULL;
                    }
                }
                delete[] m_pPair_Con[k];
                m_pPair_Con[k] = NULL;
            }

            if (m_pPair_UnConPrim[k] != NULL)
            {
                for (int i = 0; i < m_usiMaxUnCon[k]; i += 2)
                {
                    if (m_pPair_UnConPrim[k][i/2] != NULL)
                    {
                        bdd_freepair(m_pPair_UnConPrim[k][i/2]);
                        m_pPair_UnConPrim[k][i/2] = NULL;
                    }
                }
                delete[] m_pPair_UnConPrim[k];
                m_pPair_UnConPrim[k] = NULL;
            }

            if (m_pPair_ConPrim[k] != NULL)
            {
                for (int i = 1; i < (unsigned short)(m_usiMaxCon[k] + 1); i += 2)
                {
                    if (m_pPair_ConPrim[k][(i - 1)/2] != NULL)
                    {
                        bdd_freepair(m_pPair_ConPrim[k][(i - 1)/2]);
                        m_pPair_ConPrim[k][(i - 1)/2] = NULL;
                    }
                }
                delete[] m_pPair_ConPrim[k];
                m_pPair_ConPrim[k] = NULL;
            }

        }
        return 0;
    }

    /*
     * DESCR:   Generate a DES file name with path (*.hsc) from a sub file name
     *          with path (.sub) and a DES file name without path.
     *          ex: vsSubFile = "/home/roger/high.sub", vsDES = "AttchCase.hsc",
     *              will return "/home/roger/AttchCase.hsc"
     * PARA:    vsSubFile: sub file name with path
     *          vsDES: DES file name without path
     * RETURN:  Generated DES file name with path
     * ACCESS:  protected
     */
    string CSub::GetDESFileFromSubFile(const string & vsSubFile,
                            const string &vsDES)
    {
        assert(vsSubFile.length() > 4);
        assert(vsSubFile.substr(vsSubFile.length() - 4) == ".sub");
        assert(vsDES.length() > 0);
        string sDES = vsDES;

        if (sDES.length() > 4)
        {
            if (sDES.substr(sDES.length() - 4) == ".hsc")
            {
                sDES = sDES.substr(0, sDES.length() - 4);
            }
        }
        sDES += ".hsc";

        unsigned int iPos = vsSubFile.find_last_of('/');

        if ( iPos == string::npos)
            return sDES;
        else
            return vsSubFile.substr(0, iPos + 1) + sDES;
    }

    /**
     * DESCR:   Add events to the event Map of this sub. If the event already exists,
     *          return its index; Otherwise generate a new 16 bit unsigned index
     *          and return the index.
     * PARA:    vsEventName:    Event name
     *          vEventSub: Event Sub (H_EVENT/R_EVENT/A_EVENT/L_EVENT/LD_EVENT),
     *          vEventType: Controllable? (CON_EVENT, UNCON_EVENT)
     * RETURN:  >0: event index (odd: controllable  even: uncontrollable)
     *          0:  error
     * ACCESS:  public
     */
    unsigned short CSub::AddSubEvent(const string & vsEventName,
                                         const EVENTSUB vEventSub,
                                         const EVENTTYPE vEventType)
    {
        LOCALEVENTS::const_iterator citer;

        //Checks the map to see if vsEventName exists. If so, it will return a
        // a pointer to that location. If not, it'll return m_SubEventsMap.end() --H.I.
        citer = m_SubEventsMap.find(vsEventName);

        if (citer != m_SubEventsMap.end())  //the event exists, return its index
            return citer->second;
        else  //the event does not exist, generate a new index.
        {
            if (vEventType == CON_EVENT)
            {
                //keeps track of the highest index assigned to an event belonging to
                // a particular type. e.g. m_usiMaxCon[0] would be the highest index
                // assigned to an event of type 0 (high level). 1 = request, 2 = answer, etc... --H.I.
                m_usiMaxCon[vEventSub] += 2;
                m_SubEventsMap[vsEventName] = m_usiMaxCon[vEventSub];
                return m_usiMaxCon[vEventSub];
            }
            else
            {
                m_usiMaxUnCon[vEventSub] += 2;
                m_SubEventsMap[vsEventName] = m_usiMaxUnCon[vEventSub];
                return m_usiMaxUnCon[vEventSub];
            }
        }
        return 0;
    }
} //end of namespace BDDHISC
