/*************************************************************************
  FILE:  BddSdLowSub.cpp
  DESCR: Reading low-level DES files and initialze all the BDDs
  AUTH:  Raoguang Song, Yu Wang
  DATE:  (C) Jan, 2006, 2009
*************************************************************************/
#include "BddSdSub.h"
#include "BddSdLowSub.h"
#include <string>
#include "BddSdDES.h"
#include "BddSdErrmsg.h"
#include "BddSdType.h"
#include "BddSdPubfunc.h"
#include <cassert>
#include <fstream>
#include <cstdlib>


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

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

// for debug
//  #include <iostream>


using namespace std;

namespace BDDSD
{

extern CSub *pSub;

/**
 * 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):
CSub(vsLowFile)
{
    InitBddFields();
}

/**
 * DESCR:   Destructor
 * PARA:    None
 * RETURN:  None
 * ACCESS:  public
 */
CLowSub::~CLowSub()
{
    // do nothing for now.
}

/*
 * DESCR:   Initialize BDD related data members (only those in LowSub.h)
 * PARA:    None
 * RETURN:  0
 * ACCESS:  private
 */
int CLowSub::InitBddFields()
{
    return 0;
}

/*
 * DESCR:   Release memory for BDD related data members(only those in Lowsub.h)
 * PARA:    None
 * RETURN:  0
 * ACCESS:  private
 */
int CLowSub::ClearBddFields()
{
    return 0;
}

/**
 * DESCR:   Load a flat project
 * PARA:    None
 * RETURN:  0 sucess <0 fail;
 * ACCESS:  public
 */
  int CLowSub::LoadSub(DESpot::DesProject& DESpotProj, bool isTimed)
{
  //    ifstream fin;
    int iRet = 0;
    CDES *pDES = NULL;

  if (!DESpotProj.isValid()) 
    {
      close_hisc();
       throw EX("Project integrity test must pass before running BDD algorithms.");
    }

  //  this must never be called for a non flat project.
  // If I extend this later to include HISC as flat projects, this
  // test can be removed
  /*
  if(!(DESpotProj.getType() == DESpot::eFlatProject))
    {
      close_hisc();
      throw EX("Can only run BddSd algorithms on flat projects.");
    }
  */

  // need to add here a check that all DES contain a controllable
  // event with name "tick" and alias "t" if we are dealing with a
  // timed system.
  
  {

    if (isTimed) {

      DESpot::DesSubsystem::DesIteratorPtr PdesIt = DESpotProj.createDesIterator();
      std::wstring tName = L"tick";
      std::wstring tAlias = L"t";
      bool fndEvent = false;


      for(PdesIt->first(); PdesIt->notDone(); PdesIt->next())
	{
	  DESpot::Des& des = PdesIt->currentItem();
	  const DESpot::DesEvent* event;
	  fndEvent = false;

	  if (des.findEvent(tName,event))
	    {
	      std::wstring tmpAlias = event->getAlias();
	      if ((tAlias == tmpAlias) && (event->isControllable()))
		{
		  fndEvent = true;
		}
	    } 

	  if (!fndEvent)
	    {
	      close_hisc();
	      std::wstring message = L"BddSd requires that every DES\
 contain a controllable event named \"tick\" with alias\
 \"t\". DES \"";
	      message += des.getName();
	      message += L"\" does not.";
	      throw message;
	    }

      }
    }
  }



  try
    {
      
      // set project name 
      QString TmpString = QString::fromStdWString(DESpotProj.getName());
      m_sSubName = TmpString.toStdString();

      // are these variables needed anymore?
      //        char scBuf[MAX_LINE_LENGTH];
      //       string sLine;
      //        int iField = -1; //0: SYSTEM 1:PLANT 2:SPEC
      //       char *scFieldArr[] = {"SYSTEM", "PLANT", "SPEC"};
      string sDESFile;

      //  int iTmp = 0;

      int numPlants = 0;
      int numSups = 0;

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

      m_iNumofPlants = numPlants;

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

      m_iNumofSpecs = numSups;

      //Check number of Plants and apply for memory space
      if (m_iNumofPlants + m_iNumofSpecs <= 0)
	{
	  pSub->SetErr(m_sSubName +
		       ": Must have at least one DES.",
		       HISC_BAD_LOW_FORMAT);
	  throw -1;
	}

      if (m_iNumofPlants < 0 || m_iNumofSpecs < 0)
	{
	  pSub->SetErr(m_sSubName +
		       ": Must have at least one plant and one spec DES.",
		       HISC_BAD_LOW_FORMAT);
	  throw -1;
	}

      m_pDESArr = new CDES *[this->GetNumofDES()];

      if(m_pDESArr == NULL) throw -1;

      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 plant components
      int iNumofPlants = 0;

      {
	DESpot::DesSubsystem::DesIteratorPtr desIt = DESpotProj.createDesIterator(DESpot::ePlantDes);
	for(desIt->first(); desIt->notDone(); desIt->next())
	  {
	    DESpot::Des& des = desIt->currentItem();
	    QString DESName = QString::fromStdWString(des.getName());

	    //	    std::cout <<  "Plant DES named: "<< DESName.toStdString() << ".\n";

	    // sDESFile not used with DESpot 
	    sDESFile = DESName.toStdString();
	    pDES = new CDES(this, sDESFile, PLANT_DES);
	    // need to modify des load  to take a DESpot DES 
	    if (pDES == NULL || pDES->LoadDES(des) < 0)
	      throw -1;   //here LoadDES() will generate the err msg.
	    else
	      {
		iNumofPlants++;
		m_pDESArr[iNumofPlants - 1] = pDES;

		for (EVENTS::const_iterator ci = pDES->m_DESEventsMap.begin(); ci != pDES->m_DESEventsMap.end(); ++ci)
		  {
		    m_SubPlantEvents.insert(ci->second);
		  }

		pDES = NULL;

	      }
	  }
      }


      // Process specs
      int iNumofSpecs = 0;
      
      {
	DESpot::DesSubsystem::DesIteratorPtr desIt =  DESpotProj.createDesIterator(DESpot::eSupervisorDes);
	for(desIt->first(); desIt->notDone(); desIt->next())
	  {
	    DESpot::Des& des = desIt->currentItem();
	    QString DESName = QString::fromStdWString(des.getName());

	    //	    std::cout <<  "Sup DES named: "<< DESName.toStdString() << ".\n";

	    // sDESFile not used with DESpot 
	    sDESFile = DESName.toStdString();
	    pDES = new CDES(this, sDESFile, SPEC_DES);
	    if (pDES == NULL || pDES->LoadDES(des) < 0)
	      throw -1;   //here LoadDES() will generate the err msg.
	    else
	      {
		iNumofSpecs++;
		m_pDESArr[m_iNumofPlants + iNumofSpecs - 1] = pDES;
		
		for (EVENTS::const_iterator ci = pDES->m_DESEventsMap.begin(); ci != pDES->m_DESEventsMap.end(); ++ci)
		  {
		    m_SubSupervisorEvents.insert(ci->second);
		  }

		pDES = NULL;
	      }
	  }
      }
      
      this->DESReorder();

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

/*
 * DESCR:   Initialize BDD data memebers
 * PARA:    None
 * RETURN:  0: sucess -1: fail
 * ACCESS:  private
 */
int CLowSub::MakeBdd()
{
    const char * DEBUG = "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)
        {
            VERBOSE(1) { PRINT_DEBUG << "Name of DES " << i << ": " << m_pDESArr[i/2]->GetDESName() << endl; }

            piDomainArr[0] = m_pDESArr[i/2]->GetNumofStates();
            piDomainArr[1] = piDomainArr[0];

            VERBOSE(1) { PRINT_DEBUG << "piDomainArr[0] (# of states): " << piDomainArr[0] << endl; }
            VERBOSE(1) { PRINT_DEBUG << "piDomainArr[1] (# of states): " << piDomainArr[1] << endl; }

            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());
        }

        //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;
        }

        //Compute transitions predicate
            if (m_usiMaxCon != 0xFFFF)
            {
                m_pbdd_ConTrans = new bdd[(m_usiMaxCon + 1) / 2];
                m_pbdd_ConVar = new bdd[(m_usiMaxCon + 1) / 2];
                m_pbdd_ConPlantTrans =  new bdd[(m_usiMaxCon + 1) / 2];
                m_pbdd_ConSupTrans =    new bdd[(m_usiMaxCon + 1) / 2];

                m_pbdd_ConVarPrim =
                                new bdd[(m_usiMaxCon + 1) / 2];
                m_pbdd_ConPhysicVar =
                                new bdd[(m_usiMaxCon + 1) / 2];
                m_pbdd_ConSupVar =
                                new bdd[(m_usiMaxCon + 1) / 2];
                m_pbdd_ConPhysicVarPrim =
                                new bdd[(m_usiMaxCon + 1) / 2];
                m_pbdd_ConSupVarPrim =
                                new bdd[(m_usiMaxCon + 1) / 2];

                m_pPair_Con = new bddPair *[(m_usiMaxCon + 1) / 2];
                for (int iPair = 0; iPair < (m_usiMaxCon + 1) / 2; iPair++)
                {
                    m_pPair_Con[iPair] = NULL;
                }

                m_pPair_ConPrim = new bddPair *[(m_usiMaxCon + 1) / 2];
                for (int iPair = 0; iPair < (m_usiMaxCon + 1) / 2; iPair++)
                {
                    m_pPair_ConPrim[iPair] = NULL;
                }
            }
            if (m_usiMaxUnCon != 0)
            {
                m_pbdd_UnConTrans = new bdd[m_usiMaxUnCon/2];

                m_pbdd_UnConVar = new bdd[m_usiMaxUnCon/2];
                m_pbdd_UnConPlantTrans =
                                        new bdd[m_usiMaxUnCon/2];
                m_pbdd_UnConSupTrans =
                                        new bdd[m_usiMaxUnCon/2];

                m_pbdd_UnConVarPrim = new bdd[m_usiMaxUnCon/2];
                m_pbdd_UnConPlantVar = new bdd[m_usiMaxUnCon/2];
                m_pbdd_UnConSupVar = new bdd[m_usiMaxUnCon/2];

                m_pbdd_UnConPlantVarPrim =
                                        new bdd[m_usiMaxUnCon/2];
                m_pbdd_UnConSupVarPrim =
                                        new bdd[m_usiMaxUnCon/2];

                m_pPair_UnCon = new bddPair *[m_usiMaxUnCon/2];
                for (int iPair = 0; iPair < m_usiMaxUnCon/2; iPair++)
                {
                    m_pPair_UnCon[iPair] = NULL;
                }
                m_pPair_UnConPrim = new bddPair *[m_usiMaxUnCon/2];
                for (int iPair = 0; iPair < m_usiMaxUnCon/2; iPair++)
                {
                    m_pPair_UnConPrim[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 iIndex = (ciTmp->first & 0x0000FFFF) / 2 - 1;

                    if (m_pbdd_UnConVar[iIndex] == bddfalse)
                    {
                        m_pbdd_UnConTrans[iIndex] = bddtrue;
                        m_pbdd_UnConVar[iIndex] = bddtrue;
                        m_pbdd_UnConVarPrim[iIndex] = bddtrue;
                    }

                    m_pbdd_UnConTrans[iIndex] &= ciTmp->second;
                    m_pbdd_UnConVar[iIndex] &= fdd_ithset(i * 2);
                    m_pbdd_UnConVarPrim[iIndex] &= fdd_ithset(i * 2 + 1);

                    //compute uncontrollable plant vars and varprimes
                    if (m_pDESArr[i]->GetDESType() == PLANT_DES)
                    {
                        if (m_pbdd_UnConPlantVar[iIndex] == bddfalse)
                        {
                            m_pbdd_UnConPlantTrans[iIndex] = bddtrue;
                            m_pbdd_UnConPlantVar[iIndex] = bddtrue;
                            m_pbdd_UnConPlantVarPrim[iIndex] = bddtrue;
                        }

                        m_pbdd_UnConPlantTrans[iIndex] &= ciTmp->second;
                        m_pbdd_UnConPlantVar[iIndex] &= fdd_ithset(i * 2);
                        m_pbdd_UnConPlantVarPrim[iIndex] &= fdd_ithset(i * 2 + 1);
                    }
                    else if (m_pDESArr[i]->GetDESType() == SPEC_DES)
                    {
                        if (m_pbdd_UnConSupVar[iIndex] == bddfalse)
                        {
                            m_pbdd_UnConSupTrans[iIndex] = bddtrue;
                            m_pbdd_UnConSupVar[iIndex] = bddtrue;
                            m_pbdd_UnConSupVarPrim[iIndex] = bddtrue;
                        }

                        m_pbdd_UnConSupTrans[iIndex] &= ciTmp->second;
                        m_pbdd_UnConSupVar[iIndex] &= fdd_ithset(i * 2);
                        m_pbdd_UnConSupVarPrim[iIndex] &= fdd_ithset(i * 2 + 1);
                    }
                }
                else  //controllable
                {
                    int iIndex = ((ciTmp->first & 0x0000FFFF) - 1)/ 2;

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

                    //compute controllable physical plant vars and varprimes
                    if (m_pDESArr[i]->GetDESType() == PLANT_DES)
                    {
                        if (m_pbdd_ConPhysicVar[iIndex] == bddfalse)
                        {
                            m_pbdd_ConPlantTrans[iIndex] = bddtrue;
                            m_pbdd_ConPhysicVar[iIndex] = bddtrue;
                            m_pbdd_ConPhysicVarPrim[iIndex]= bddtrue;
                        }

                        m_pbdd_ConPlantTrans[iIndex] &= ciTmp->second;
                        m_pbdd_ConPhysicVar[iIndex] &= fdd_ithset(i * 2);
                        m_pbdd_ConPhysicVarPrim[iIndex] &= fdd_ithset(i * 2 + 1);
                    }
                    else if (m_pDESArr[i]->GetDESType() == SPEC_DES)
                    {
                        if (m_pbdd_ConSupVar[iIndex] == bddfalse)
                        {
                            m_pbdd_ConSupTrans[iIndex] = bddtrue;
                            m_pbdd_ConSupVar[iIndex] = bddtrue;
                            m_pbdd_ConSupVarPrim[iIndex]= bddtrue;
                        }

                        m_pbdd_ConSupTrans[iIndex] &= ciTmp->second;
                        m_pbdd_ConSupVar[iIndex] &= fdd_ithset(i * 2);
                        m_pbdd_ConSupVarPrim[iIndex] &= fdd_ithset(i * 2 + 1);
                    }
                }
            }
        }

        // Add self loops of any event to plant (sup) trans predicate if the event
        // does not exist in the plants (sups), but exists in the sups (plants).
        int sig = 0;
        for (int iIndex = 0; iIndex < (m_usiMaxCon + 1) / 2; iIndex++)
        {
            sig = (iIndex * 2) + 1;
            if ((m_SubSupervisorEvents.find(sig) == m_SubSupervisorEvents.end())
                && (m_SubPlantEvents.find(sig) != m_SubPlantEvents.end()))
            {
                m_pbdd_ConSupTrans[iIndex] = bddtrue;
            }
            else if ((m_SubSupervisorEvents.find(sig) != m_SubSupervisorEvents.end())
                && (m_SubPlantEvents.find(sig) == m_SubPlantEvents.end()))
            {
                m_pbdd_ConPlantTrans[iIndex] = bddtrue;
            }
        }

        for (int iIndex = 0; iIndex < (m_usiMaxUnCon / 2); iIndex++)
        {
            sig = (iIndex + 1) * 2;
            if ((m_SubSupervisorEvents.find(sig) == m_SubSupervisorEvents.end())
                && (m_SubPlantEvents.find(sig) != m_SubPlantEvents.end()))
            {
                m_pbdd_UnConSupTrans[iIndex] = bddtrue;
            }
            else if ((m_SubSupervisorEvents.find(sig) != m_SubSupervisorEvents.end())
                && (m_SubPlantEvents.find(sig) == m_SubPlantEvents.end()))
            {
                m_pbdd_UnConPlantTrans[iIndex] = bddtrue;
            }
        }

        //compute m_pPair_UnCon, m_pPair_Con
        for (int j = 0; j < m_usiMaxUnCon; j += 2)
        {
            m_pPair_UnCon[j/2] = bdd_newpair();
            SetBddPairs(m_pPair_UnCon[j/2], m_pbdd_UnConVar[j/2],
                            m_pbdd_UnConVarPrim[j/2]);
            m_pPair_UnConPrim[j/2] = bdd_newpair();
            SetBddPairs(m_pPair_UnConPrim[j/2],
                                m_pbdd_UnConVarPrim[j/2],
                                m_pbdd_UnConVar[j/2]);
        }
        for (int j = 1; j < (unsigned short)(m_usiMaxCon + 1); j += 2)
        {
            m_pPair_Con[(j - 1) / 2] = bdd_newpair();
            SetBddPairs(m_pPair_Con[(j - 1) / 2],
                                m_pbdd_ConVar[(j - 1) / 2],
                                m_pbdd_ConVarPrim[(j - 1) / 2]);
            m_pPair_ConPrim[(j - 1) / 2] = bdd_newpair();
            SetBddPairs(m_pPair_ConPrim[(j - 1) / 2],
                                m_pbdd_ConVarPrim[(j - 1) / 2],
                                m_pbdd_ConVar[(j - 1) / 2]);
        }
    }
    catch(...)
    {
        string sErr;
        sErr = "Error happens when initializing low level ";
        sErr += " BDD!";
        pSub->SetErr(sErr, HISC_SYSTEM_INITBDD);
        return -1;
    }
    return 0;
}

} //end of namespace BDDSD
