/*************************************************************************
  FILE:  BddHiscLowSub.cpp
  DESCR: Reading low-level DES files and initialze all the BDDs
  AUTH:  Raoguang Song
  Supervisor: Dr. Ryan Leduc
  DATE:  (C) Jan, 2006
*************************************************************************/
#include "BddHiscSub.h"
#include "BddHiscLowSub.h"
#include <string>
#include "BddHiscDES.h"
#include "BddHiscErrmsg.h"
#include "BddHiscType.h"
#include "BddHiscPubfunc.h"
#include "BddHiscProject.h"
#include <cassert>
#include <fstream>
#include <cstdlib>

#include "BddHisc.h"
#include <QString>

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


using namespace std;


namespace BDDHISC
{

extern CProject *pPrj;

/**
 * DESCR:   Constructor
 * PARA:    vsLowFile: subsystem file name with path (.sub)(input)
 *          viSubIndex: subsystem index (high: 0, low: 1,2,...)(input)
 * RETURN:  None
 * ACCESS:  public
 */
CLowSub::CLowSub(const string & vsLowFile, int viSubIndex):
CSub(vsLowFile, viSubIndex)
{
    m_iNumofIntfs = 1;  //Number of Interface DES, defined in CSub
    InitBddFields();
}

/**
 * DESCR:   Destructor
 * PARA:    None
 * RETURN:  None
 * ACCESS:  public
 */
CLowSub::~CLowSub()                                                                              
{
    ClearBddFields();
}

/*
 * DESCR:   Initialize BDD related data members (only those in LowSub.h)
 * PARA:    None
 * RETURN:  0
 * ACCESS:  private
 */
int CLowSub::InitBddFields()
{
    m_pbdd_RTrans[0] = NULL;
    m_pbdd_ATrans[0] = NULL;
    m_pbdd_RTrans[1] = NULL;
    m_pbdd_ATrans[1] = NULL;
    m_pbdd_LDTrans[0] = NULL;
    m_pbdd_LDTrans[1] = NULL;
    m_pbdd_CLDTrans[0] = NULL;
    m_pbdd_CLDTrans[1] = NULL;
    m_bddIVar = bddfalse;
    m_bddIVarPrim = bddfalse;
    m_bddIntfInit = bddfalse;
    m_bddIntfMarking = bddfalse;
    return 0;   
}

/*
 * DESCR:   Release memory for BDD related data members(only those in Lowsub.h)
 * PARA:    None
 * RETURN:  0
 * ACCESS:  private
 */
int CLowSub::ClearBddFields()
{
    for (int m = 0; m < 2; m++)
    {
        delete[] m_pbdd_RTrans[m];
        m_pbdd_RTrans[m] = NULL;
        delete[] m_pbdd_ATrans[m];
        m_pbdd_ATrans[m] = NULL;
        delete[] m_pbdd_LDTrans[m];
        m_pbdd_LDTrans[m] = NULL;
        delete[] m_pbdd_CLDTrans[m];
        m_pbdd_CLDTrans[m] = NULL;
    }
    return 0;
}

/**
 * DESCR:   Load a low-level
 * PARA:    subSys: a DESpot type subsystem
 * RETURN:  0 success <0 fail;
 * ACCESS:  public
 */
int CLowSub::LoadSub(const DESpot::DesSubsystem& subSys)
{
    int iRet = 0;
    CDES *pDES = NULL;
    string sDESFile;
    bool temp_skip_test;


    // can I remove this try?
    try
    {
      // set name of subsystem
      QString lowName = QString::fromStdWString(subSys.getName());
      // remove spaces from name
     /* while (lowName.contains(" "))
	{
	  lowName.remove(' ');
	}*/
       m_sSubName = lowName.toStdString();

       //Set local subsystem's test skip value to match that which was passed in to despot
       temp_skip_test = subSys.extractionSystemSkipTest();
       setExtractionSystemSkipTest(temp_skip_test);

       int numPlants = 0;
       int numSups = 0;

       // count number of plants
       {
	 DESpot::DesSubsystem::DesIteratorPtr desIt = subSys.createDesIterator(DESpot::ePlantDes);
	 for(desIt->first(); desIt->notDone(); desIt->next())
	   {
	     numPlants++;
	   }
       }

       m_iNumofPlants = numPlants;

       // count number of Sups
       {
	 DESpot::DesSubsystem::DesIteratorPtr desIt = subSys.createDesIterator(DESpot::eSupervisorDes);
	 for(desIt->first(); desIt->notDone(); desIt->next())
	   {
	     numSups++;
	   }
       }

       m_iNumofSpecs = numSups;
 
       m_pDESArr = new CDES *[this->GetNumofDES()];
       for (int i = 0; i < this->GetNumofDES(); i++)
	 m_pDESArr[i] = NULL;

       //Initialize m_piDESOrderArr
       m_piDESOrderArr = new int[this->GetNumofDES()];
       for (int i = 0; i < this->GetNumofDES(); i++)
	 m_piDESOrderArr[i] = i;
       //Initialize m_piDESPosArr
       m_piDESPosArr = new int[this->GetNumofDES()];
       for (int i = 0; i < this->GetNumofDES(); i++)
	 m_piDESPosArr[i] = i;
   



       // process interface
       if (subSys.implementsInterface())
	 {
	   const DESpot::DesInterface& interf = subSys.getInterface();

	   int numIntfDes = 0;
	   {
	     //  count number of intf DES

	      DESpot::DesInterface::DesIteratorPtr desIt = interf.createDesIterator();
	     for(desIt->first(); desIt->notDone(); desIt->next())
	       {
		 numIntfDes++;
	       }
	   }

	   if ( numIntfDes >1) 
	     {
	       // BDDhisc only allows one intf des, so we need to
	       // first sync them together.
	       DESpot::Des& intfDes = interf.getSyncDes();
	       QString intfDESName = QString::fromStdWString(intfDes.getName());
	       // sDESFile not used with DESpot 
	       sDESFile = intfDESName.toStdString();
	       pDES = new CDES(this, sDESFile, INTERFACE_DES);
	       if (pDES->LoadDES(intfDes, false) < 0)
		 throw -1;   //here LoadDES() will generate the err msg.
	       else
		 {
		   m_pDESArr[0] = pDES;
		   pDES = NULL;
		 }
	     }
	   else
	     {
	       // loop through interface des. bddhisc only allows one.
	        DESpot::DesInterface::DesIteratorPtr desIt = interf.createDesIterator();
	       for(desIt->first(); desIt->notDone(); desIt->next())
		 {
		   DESpot::Des& intfDes = desIt->currentItem();
		   QString intfDESName = QString::fromStdWString(intfDes.getName()) + ".hsc";
		   // sDESFile not used with DESpot 
		   sDESFile = intfDESName.toStdString();
		   pDES = new CDES(this, sDESFile, INTERFACE_DES);
		   if (pDES->LoadDES(intfDes, false) < 0)
		     throw -1;   //here LoadDES() will generate the err msg.
		   else
		     {
		       m_pDESArr[0] = pDES;
		       pDES = NULL;
		     }
		 }
	     }
	 }
       else
	 {
	   close_hisc();
	   std::wstring message = L"Low-level \"";
	   message += lowName.toStdWString();
	   message += L"\" does not implement an interface.";
	   throw message;
	 }


       // process plant components
       int iNumofPlants = 0;

       {
	 DESpot::DesSubsystem::DesIteratorPtr desIt = subSys.createDesIterator(DESpot::ePlantDes);
	 for(desIt->first(); desIt->notDone(); desIt->next())
	   {
	     DESpot::Des& des = desIt->currentItem();
	     QString lowDESName = QString::fromStdWString(des.getName());
	     // sDESFile not used with DESpot 
	     sDESFile = lowDESName.toStdString();
	     pDES = new CDES(this, sDESFile, PLANT_DES);
	     if (pDES->LoadDES(des, false) < 0)
	       throw -1;   //here LoadDES() will generate the err msg.
	     else
	       {
		 iNumofPlants++;
		 m_pDESArr[iNumofPlants] = pDES;
		 pDES = NULL;
	       }
	   }
       }


       // Process specs
        int iNumofSpecs = 0;

       {
	 DESpot::DesSubsystem::DesIteratorPtr desIt = subSys.createDesIterator(DESpot::eSupervisorDes);
	 for(desIt->first(); desIt->notDone(); desIt->next())
	   {
	     DESpot::Des& des = desIt->currentItem();
	     QString lowDESName = QString::fromStdWString(des.getName());
	     // sDESFile not used with DESpot 
	     sDESFile = lowDESName.toStdString();
	     pDES = new CDES(this, sDESFile, SPEC_DES);
	     if (pDES->LoadDES(des, false) < 0)
	       throw -1;   //here LoadDES() will generate the err msg.
	     else
	       {
		 iNumofSpecs++;
		 m_pDESArr[m_iNumofPlants + iNumofSpecs] = pDES;
		 pDES = NULL;
	       }
	   }
       }

    
	//  don't delete the next line.
        this->DESReorder();


    }
    catch (int iError)
    {
        if (pDES != NULL)
        {
            delete pDES;
            pDES = NULL;
        }
        iRet = iError;
    }
    return iRet;
}

/*
 * DESCR:   Initialize BDD data members
 * PARA:    None
 * RETURN:  0: sucess -1: fail
 * ACCESS:  private
 */
int CLowSub::MakeBdd()
{
    try
    {
        //Initialize the bdd node table and cache size.
        long long lNumofStates = 1;
        
        for (int i = 0; i < this->GetNumofDES(); i++)
        {
            lNumofStates *= m_pDESArr[i]->GetNumofStates();
            if (lNumofStates >= MAX_INT)
                break;
        }
        if (lNumofStates <= 10000)
            bdd_init(1000, 100);
        else if (lNumofStates <= 1000000)
            bdd_init(10000, 1000);
        else if (lNumofStates <= 10000000)
            bdd_init(100000, 10000);
        else
        {
            bdd_init(2000000, 1000000);
            bdd_setmaxincrease(1000000);
        }
        
        giNumofBddNodes = 0;
        bdd_gbc_hook(my_bdd_gbchandler);
        
        //define domain variables
        int *piDomainArr = new int[2];
        for (int i = 0; i < 2 * this->GetNumofDES(); i += 2)
        {
            piDomainArr[0] = m_pDESArr[i/2]->GetNumofStates();
            piDomainArr[1] = piDomainArr[0];
            fdd_extdomain(piDomainArr, 2);
        }
        delete[] piDomainArr;
        piDomainArr = NULL;
        
        //compute the number of bdd variables (only for normal variables)
        m_iNumofBddNormVar = 0;
        for (int i = 0; i < 2 * (this->GetNumofDES()); i = i + 2)
            m_iNumofBddNormVar += fdd_varnum(i);
        
        //compute initial state predicate
        for (int i = 0; i < this->GetNumofDES(); i++)
        {
            m_bddInit &= fdd_ithvar(i * 2, m_pDESArr[i]->GetInitState());
            if (m_pDESArr[i]->GetDESType() == INTERFACE_DES)
                m_bddIntfInit = fdd_ithvar(i * 2, m_pDESArr[i]->GetInitState());
        }

        //set the first level block
        int iNumofBddVar = 0;
        int iVarNum = 0;
        bdd bddBlock = bddtrue;
        for (int i = 0; i < 2 * (this->GetNumofDES()); i += 2)
        {
            iVarNum = fdd_varnum(i);
            bddBlock = bddtrue;
            
            for (int j = 0; j < 2 * iVarNum; j++)
            {
                bddBlock &= bdd_ithvar(iNumofBddVar + j);
            }
            bdd_addvarblock(bddBlock, BDD_REORDER_FREE);
            iNumofBddVar += 2 * iVarNum;
        }

        //compute marking states predicate
        bdd bddTmp = bddfalse;
        for (int i = 0; i < this->GetNumofDES(); i++)
        {
            bddTmp = bddfalse;
            MARKINGLIST::const_iterator ci = 
                 (m_pDESArr[i]->GetMarkingList()).begin();
                 
            for (int j = 0; j < m_pDESArr[i]->GetNumofMarkingStates(); j++)
            {
                bddTmp |= fdd_ithvar(i * 2, *ci);
                ++ci;
            }
            m_bddMarking &= bddTmp;

            if (m_pDESArr[i]->GetDESType() == INTERFACE_DES)
                m_bddIntfMarking = bddTmp;
        }
        
        //Initialize interface transitions predicates
        if (m_usiMaxUnCon[R_EVENT] > 0)
            m_pbdd_RTrans[0] = new bdd[m_usiMaxUnCon[R_EVENT] / 2];
        if (m_usiMaxUnCon[A_EVENT] > 0)
            m_pbdd_ATrans[0] = new bdd[m_usiMaxUnCon[A_EVENT]/2];
        if (m_usiMaxUnCon[LD_EVENT] > 0)
            m_pbdd_LDTrans[0] = new bdd[m_usiMaxUnCon[LD_EVENT]/2];
        if (m_usiMaxUnCon[CHILD_LD_EVENT] > 0)
            m_pbdd_CLDTrans[0] = new bdd[m_usiMaxUnCon[CHILD_LD_EVENT]/2];

        if ((unsigned short)(m_usiMaxCon[R_EVENT] + 1) > 0)
            m_pbdd_RTrans[1] = new bdd[(m_usiMaxCon[R_EVENT] + 1)/2];
        if ((unsigned short)(m_usiMaxCon[A_EVENT] + 1) > 0)
            m_pbdd_ATrans[1] = new bdd[(m_usiMaxCon[A_EVENT] + 1)/2];
        if ((unsigned short)(m_usiMaxCon[LD_EVENT] + 1) > 0)
            m_pbdd_LDTrans[1] = new bdd[(m_usiMaxCon[LD_EVENT] + 1)/2];
        if ((unsigned short)(m_usiMaxCon[CHILD_LD_EVENT] + 1) > 0)
            m_pbdd_CLDTrans[1] = new bdd[(m_usiMaxCon[CHILD_LD_EVENT] + 1)/2];

        //Compute transitions predicate
        //k starts at 1 s.t. we do not make bdd's for high level events (k==0)
        for (int k = R_EVENT; k < NUMBER_OF_EVENTS; k++)
        {
            if (m_usiMaxCon[k] != 0xFFFF)
            {
                m_pbdd_ConTrans[k] = new bdd[m_usiMaxCon[k] / 2 + 1];
                m_pbdd_ConVar[k] = new bdd[m_usiMaxCon[k] / 2 + 1];
                m_pbdd_ConVarPrim[k] = 
                                new bdd[m_usiMaxCon[k] / 2 + 1];
                m_pbdd_ConPhysicVar[k] = 
                                new bdd[m_usiMaxCon[k] / 2 + 1];
                m_pbdd_ConPhysicVarPrim[k] = 
                                new bdd[m_usiMaxCon[k] / 2 + 1];
                m_pPair_Con[k] = new bddPair *[m_usiMaxCon[k] / 2 + 1];
                for (int iPair = 0; iPair < m_usiMaxCon[k] / 2 + 1; iPair++)
                    m_pPair_Con[k][iPair] = NULL;
                m_pPair_ConPrim[k] = new bddPair *[m_usiMaxCon[k] / 2 + 1];
                for (int iPair = 0; iPair < m_usiMaxCon[k] / 2 + 1; iPair++)
                    m_pPair_ConPrim[k][iPair] = NULL;
            }
            if (m_usiMaxUnCon[k] != 0)
            {
                m_pbdd_UnConTrans[k] = new bdd[m_usiMaxUnCon[k]/2];
                m_pbdd_UnConVar[k] = new bdd[m_usiMaxUnCon[k]/2];
                m_pbdd_UnConPlantTrans[k] = 
                                        new bdd[m_usiMaxUnCon[k]/2];
                m_pbdd_UnConVarPrim[k] = new bdd[m_usiMaxUnCon[k]/2];
                m_pbdd_UnConPlantVar[k] = new bdd[m_usiMaxUnCon[k]/2];
                m_pbdd_UnConPlantVarPrim[k] = 
                                        new bdd[m_usiMaxUnCon[k]/2];
                m_pPair_UnCon[k] = new bddPair *[m_usiMaxUnCon[k]/2];
                for (int iPair = 0; iPair < m_usiMaxUnCon[k]/2; iPair++)
                    m_pPair_UnCon[k][iPair] = NULL;
                m_pPair_UnConPrim[k] = new bddPair *[m_usiMaxUnCon[k]/2];
                for (int iPair = 0; iPair < m_usiMaxUnCon[k]/2; iPair++)
                    m_pPair_UnConPrim[k][iPair] = NULL;
            }
        }
        
        map<int, bdd> bddTmpTransMap;  //<event_index, transitions>
        for (int i = 0; i < this->GetNumofDES(); i++)
        {
            //before compute transition predicate for each DES, clear it.
            bddTmpTransMap.clear();
            for (int j = 0; j < m_pDESArr[i]->GetNumofEvents(); j++)
            {
                bddTmpTransMap[(m_pDESArr[i]->GetEventsArr())[j]] = bddfalse;
            }
            
            //compute transition predicate for each DES
            for (int j = 0; j < m_pDESArr[i]->GetNumofStates(); j++)
            {
                TRANS::const_iterator ci = 
                                    (*(m_pDESArr[i]->GetTrans() + j)).begin();
                for (; ci != (*(m_pDESArr[i]->GetTrans() + j)).end(); ++ci)
                {
                    bddTmpTransMap[ci->first] |= fdd_ithvar(i * 2, j) &
                        fdd_ithvar(i * 2 + 1, ci->second);
                }
            }

            //combine the current DES transition predicate to 
            //subsystem transition predicate
            map<int, bdd>::const_iterator ciTmp = bddTmpTransMap.begin();
            for (; ciTmp != bddTmpTransMap.end(); ++ciTmp)
            {
                if (ciTmp->first % 2 == 0)  //uncontrollable, start from 2
                {
                    int iEventSub = ciTmp->first >> 28;

                    //uncontrollable event indices are always going to be even
                    int iIndex = (ciTmp->first & 0x0000FFFF) / 2 - 1;
                    
                    if (m_pbdd_UnConVar[iEventSub][iIndex] == bddfalse)
                    {
                        m_pbdd_UnConTrans[iEventSub][iIndex] = bddtrue;
                        m_pbdd_UnConVar[iEventSub][iIndex] = bddtrue;
                        m_pbdd_UnConVarPrim[iEventSub][iIndex] = bddtrue;
                    }
                    
                    m_pbdd_UnConTrans[iEventSub][iIndex] &= ciTmp->second; 
                    m_pbdd_UnConVar[iEventSub][iIndex] &= fdd_ithset(i * 2);
                    m_pbdd_UnConVarPrim[iEventSub][iIndex] &= 
                                                    fdd_ithset(i * 2 + 1);
                    
                    //compute uncontrollable plant vars and varprimes
                    if (m_pDESArr[i]->GetDESType() == PLANT_DES)
                    {
                        if (m_pbdd_UnConPlantVar[iEventSub][iIndex] == bddfalse)
                        {
                            m_pbdd_UnConPlantTrans[iEventSub][iIndex] = bddtrue;
                            m_pbdd_UnConPlantVar[iEventSub][iIndex] = bddtrue;
                            m_pbdd_UnConPlantVarPrim[iEventSub][iIndex] = 
                                                                        bddtrue;
                        }
                        m_pbdd_UnConPlantTrans[iEventSub][iIndex] &= 
                                                                ciTmp->second; 
                        m_pbdd_UnConPlantVar[iEventSub][iIndex] &= 
                                                            fdd_ithset(i * 2);
                        m_pbdd_UnConPlantVarPrim[iEventSub][iIndex] &= 
                                                        fdd_ithset(i * 2 + 1);
                    }

                    //compute interface Transitions
                    if (m_pDESArr[i]->GetDESType() == INTERFACE_DES)
                    {
                        if ((EVENTSUB)iEventSub == R_EVENT)
                            m_pbdd_RTrans[0][iIndex] = ciTmp->second;
                        else if ((EVENTSUB)iEventSub == A_EVENT)
                            m_pbdd_ATrans[0][iIndex] = ciTmp->second;
                        else if ((EVENTSUB)iEventSub == CHILD_LD_EVENT)
                            m_pbdd_CLDTrans[0][iIndex] = ciTmp->second;
                        else
                            m_pbdd_LDTrans[0][iIndex] = ciTmp->second;
                    }
                }
                else  //controllable
                {
                    int iEventSub = ciTmp->first >> 28;

                    //controllable event indices are always going to be odd
                    int iIndex = ((ciTmp->first & 0x0000FFFF) - 1)/ 2;

                    if (m_pbdd_ConVar[iEventSub][iIndex] == bddfalse)
                    {
                        m_pbdd_ConTrans[iEventSub][iIndex] = bddtrue; 
                        m_pbdd_ConVar[iEventSub][iIndex] = bddtrue;
                        m_pbdd_ConVarPrim[iEventSub][iIndex] = bddtrue;
                    }
                    m_pbdd_ConTrans[iEventSub][iIndex] &= ciTmp->second; 
                    m_pbdd_ConVar[iEventSub][iIndex] &= fdd_ithset(i * 2);
                    m_pbdd_ConVarPrim[iEventSub][iIndex] &= 
                                                        fdd_ithset(i * 2 + 1);

                    //compute controllable physical plant vars and varprimes
                    if (m_pDESArr[i]->GetDESType() == PLANT_DES)
                    {
                        if (m_pbdd_ConPhysicVar[iEventSub][iIndex] == bddfalse)
                        {
                            m_pbdd_ConPhysicVar[iEventSub][iIndex] = bddtrue;
                            m_pbdd_ConPhysicVarPrim[iEventSub][iIndex]= bddtrue;
                        }
                        m_pbdd_ConPhysicVar[iEventSub][iIndex] &= 
                                                            fdd_ithset(i * 2);
                        m_pbdd_ConPhysicVarPrim[iEventSub][iIndex] &= 
                                                        fdd_ithset(i * 2 + 1);
                    }

                    //compute interface Transitions
                    //Modified to include LD and child LD events -- H.I. 2014
                    if (m_pDESArr[i]->GetDESType() == INTERFACE_DES)
                    {
                        if ((EVENTSUB)iEventSub == R_EVENT)
                            m_pbdd_RTrans[1][iIndex] = ciTmp->second;
                        else if ((EVENTSUB)iEventSub == A_EVENT)
                            m_pbdd_ATrans[1][iIndex] = ciTmp->second;
                        else if ((EVENTSUB)iEventSub == CHILD_LD_EVENT)
                            m_pbdd_CLDTrans[1][iIndex] = ciTmp->second;
                        else
                            m_pbdd_LDTrans[1][iIndex] = ciTmp->second;
                     }
                }
            }
            if (m_pDESArr[i]->GetDESType() == INTERFACE_DES)
            {
                m_bddIVar = fdd_ithset(i * 2);
                m_bddIVarPrim = fdd_ithset(i * 2 + 1);
            }
        }
        
        //compute m_pPair_UnCon, m_pPair_Con
        for (int k = R_EVENT; k < NUMBER_OF_EVENTS; k++)
        {       
            for (int j = 0; j < m_usiMaxUnCon[k]; j += 2)
            {
                m_pPair_UnCon[k][j/2] = bdd_newpair();
                SetBddPairs(m_pPair_UnCon[k][j/2], m_pbdd_UnConVar[k][j/2], 
                                m_pbdd_UnConVarPrim[k][j/2]); 
                m_pPair_UnConPrim[k][j/2] = bdd_newpair();
                SetBddPairs(m_pPair_UnConPrim[k][j/2], 
                                m_pbdd_UnConVarPrim[k][j/2], 
                                m_pbdd_UnConVar[k][j/2]); 
            }
            for (int j = 1; j < (unsigned short)(m_usiMaxCon[k] + 1); j += 2) 
            {
                m_pPair_Con[k][(j - 1) / 2] = bdd_newpair();
                SetBddPairs(m_pPair_Con[k][(j - 1) / 2], 
                                m_pbdd_ConVar[k][(j - 1) / 2], 
                                m_pbdd_ConVarPrim[k][(j - 1) / 2]); 
                m_pPair_ConPrim[k][(j - 1) / 2] = bdd_newpair();
                SetBddPairs(m_pPair_ConPrim[k][(j - 1) / 2], 
                                m_pbdd_ConVarPrim[k][(j - 1) / 2], 
                                m_pbdd_ConVar[k][(j - 1) / 2]); 
            }
        }
    }
    catch(...)
    {
        string sErr;
        sErr = "Error happens when initializing low-level ";
        sErr += this->GetSubIndex();
        sErr += " BDD!";
        pPrj->SetErr(sErr, HISC_SYSTEM_INITBDD);
        return -1;
    }
    return 0;
}


} //end of namespace BDDHISC
