/*************************************************************************
  FILE:  BddSdDES.cpp
  DESCR: Processing DES file
  AUTH:  Raoguang Song, Yu Wang
  DATE:  (C) Jan, 2006, 2009
*************************************************************************/
#include "BddSdDES.h"
#include "BddSdPubfunc.h"
#include <fstream>
#include <cstdlib>
#include "BddSdType.h"
#include "BddSdErrmsg.h"
#include <cassert>
#include "BddSdSub.h"
#include "BddSdLowSub.h"

#include "Des.h"
#include "DesTypes.h"
#include "DesStatePool.h"
#include "DesEventPool.h"
#include "DesTransitionFunction.h"

// for debug
//#include <iostream>

using namespace std;

namespace BDDSD
{

extern CSub *pSub;

/**
 * DESCR:   Constructor
 * PARA:    vpSub:  which subsystem this DES belongs to (input)
 *          vsDESFile:  DES file name with path (input)
 *          vDESType:   DES Type (inpute)
 * RETURN: none
 * ACCESS: public
 */
CDES::CDES(CSub *vpSub, const string &vsDESFile, const DESTYPE vDESType)
{
    m_pSub = vpSub;
    m_sDESFile = vsDESFile;
    m_sDESName.clear();
    m_DESType = vDESType;
    m_iNumofStates = 0;
    m_iInitState = -1;

    m_MarkingList.clear();
    m_StatesMap.clear();
    m_InvStatesMap.clear();
    m_DESEventsMap.clear();
    m_UnusedEvents.clear();
    m_InvDESEventsMap.clear();

    m_piEventsArr = NULL;
    m_pTransArr = NULL;
}

/**
 * DESCR:   Destructor
 * PARA:    None
 * RETURN:  None
 * ACCESS:  public
 */
CDES::~CDES()
{
    delete[] m_pTransArr;
    m_pTransArr = NULL;

    delete[] m_piEventsArr;
    m_piEventsArr = NULL;
}

/**
 * DESCR:   Loading DES file
 * PARA:    theDES - a DESpot DES
 * RETURN:  0: sucess  -1: fail
 * ACCESS:  public
 */
int CDES::LoadDES(DESpot::Des& theDes)
{

  int iRet = 0;
  string sErr;
    
  int i = 0;
    
  string sSubName = m_pSub->GetSubName();
    
  try
    {
      
      QString theDESName = QString::fromStdWString(theDes.getName());
      m_sDESName = theDESName.toStdString();

      // for debug
      //     cout  << "proc DES: "<< m_sDESName << ".\n";


      //      string sDESLoc = sSubName + ":" + m_sDESName + ": "; 
      string sDESLoc = sSubName + ":" + m_sDESName + " : ";

      int numStates = 0;
      // count the number of states
      {
	DESpot::Des::StateIteratorPtr stateIt = theDes.createStateIterator();
	for(stateIt->first(); stateIt->isDone() == false; stateIt->next())
	  {
	    numStates++;
	  }
      }

      if (numStates <= 0 || numStates  > MAX_STATES_IN_ONE_COMPONENT_DES)
	{
          pSub->SetErr(sDESLoc + "Too few or too many states", HISC_BAD_DES_FORMAT);
	  throw -1;
	}
      
      //initialize the number of states
      m_iNumofStates = numStates;
                        
      //initialize the transition arrary
      m_pTransArr = new TRANS[m_iNumofStates];

      // output state names
      {
	DESpot::Des::StateIteratorPtr stateIt = theDes.createStateIterator();
	for(stateIt->first(); stateIt->isDone() == false; stateIt->next())
	  {
	    const DESpot::DesState& state = stateIt->currentItem();
	    QString theName = QString::fromStdWString(state.getName());
	    string stateName = theName.toStdString();
	    
	    if (m_StatesMap.find(stateName) != m_StatesMap.end())  
	      {
		pSub->SetErr(sDESLoc + "Duplicate state names--" + 
			     stateName, HISC_BAD_DES_FORMAT);
		throw -1;
	      }
	    else if (stateName[0] == '(')
	      {
		pSub->SetErr(sDESLoc + 
			     "The first letter of state names can not be (", 
			     HISC_BAD_DES_FORMAT);
		throw -1;
	      }
	    else
	      {

		/*  This is odd.  Under Linux, if m_StatesMap.size() then
		    "m_StatesMap[stateName] = m_StatesMap.size() - 1;"
		    seems to store 0!   Maybe it preincrements for the state
		    being added?
		*/
#ifdef _WIN32
		m_StatesMap[stateName] = m_StatesMap.size();
		m_InvStatesMap[m_StatesMap.size()] = stateName;
#else
		m_StatesMap[stateName] = m_StatesMap.size() - 1;
		m_InvStatesMap[m_StatesMap.size() - 1] = stateName;
#endif
	      }
	    
	  }
      }

      // specify initial state
      if (theDes.hasInitialState())
	{
	  const DESpot::DesState& initState = theDes.getInitialState();
	  QString theName = QString::fromStdWString(initState.getName());
	  string stateName = theName.toStdString();
	  
	  //Initial state name must be valid
	  if (m_StatesMap.find(stateName) == m_StatesMap.end())
	    {
	      pSub->SetErr(sDESLoc + "Initial state is not defined.", 
			   HISC_BAD_DES_FORMAT);
	      throw -1;
	    }

	  //only one initial state allowed
	  if (m_iInitState != -1)  
	    {
	      pSub->SetErr(sDESLoc + "More than one initial states.", 
			   HISC_BAD_DES_FORMAT);
	      throw -1;
	    }
                    
	  m_iInitState = m_StatesMap[stateName];
	}
      else
	{
	  assert(false);  // des has no initial state
	}

      
      // process marking states
      int iTmpStateIndex = 0;

      {
	DESpot::Des::StateIteratorPtr stateIt = theDes.createStateIterator();
	for(stateIt->first(); stateIt->isDone() == false; stateIt->next())
	  {
	    const DESpot::DesState& state = stateIt->currentItem();
	    if (state.isMarked())
	      {
		QString theName = QString::fromStdWString(state.getName());
		string stateName = theName.toStdString();

		if (m_StatesMap.find(stateName) == m_StatesMap.end())
		  {
		    pSub->SetErr(sDESLoc + "Marking states do not exist.", 
				 HISC_BAD_DES_FORMAT);
		    throw -1;
		  }
		
		iTmpStateIndex = m_StatesMap[stateName];
	    
		for (MARKINGLIST::const_iterator ci = m_MarkingList.begin();
		     ci != m_MarkingList.end(); ci++)
		  {
		    if (*ci == iTmpStateIndex)
		      {
			pSub->SetErr(sDESLoc + "Duplicate marking states.", 
				     HISC_BAD_DES_FORMAT);
			throw -1;
		      }
		  }
		
		m_MarkingList.push_back(iTmpStateIndex);
	      }
	  }
      }

      
      //process events
      char cEventSub = '\0';
      char cControllable = 'N';
      int iTmpEventIndex = 0;

      DESpot::Des::EventIteratorPtr eventIt = theDes.createEventIterator();
      for(eventIt->first(); eventIt->isDone() == false; eventIt->next())
	{
	  const DESpot::DesEvent& event = eventIt->currentItem();
    
	  cControllable = 'N';
	  cEventSub = '\0';
	  QString theName = QString::fromStdWString(event.getName());
	  string eventName = theName.toStdString();

	  if (event.isControllable())
	    {
	      cControllable = 'Y';
	    }
    
	  cEventSub = 'L';
	  
	  /*  for bddsd, it ignores this
	      switch(event.getType())
	      {
	      case DESpot::eDefaultEvent:
	      if (isHigh) 
	      {
	      cEventSub = 'H';
	      }
	      else 
	      {
	      cEventSub = 'L';
	      }
	      break;
	      case DESpot::eAnswerEvent:
	      cEventSub = 'A';
	      break;
	      case DESpot::eRequestEvent:
	      cEventSub = 'R';
	      break;
	      case DESpot::eLDataEvent:
	      cEventSub = 'D';
	      break;
	      case DESpot::eHighLevelEvent:
	      cEventSub = 'H';
	      break;
	      case DESpot::eLowLevelEvent:
	      cEventSub = 'L';
	      break;
	      default:
	      assert(false); //unknown event type
	      break;
	      }
	  */

    
	  // cEventSub, cControllable, eventName
	  
	  if (cEventSub >= 'a')
	    cEventSub -= 32;
	  if (cControllable >= 'a')
	    cControllable -= 32;
	  
	  // bddsd doesn't use cEventSub
	  //      iTmpEventIndex = AddEvent(eventName, cEventSub, cControllable);
	  iTmpEventIndex = AddEvent(eventName, cControllable);
	  if (iTmpEventIndex < 0)
	    throw -1;   //Errmsg generated by AddEvent
	  
	  m_DESEventsMap[eventName] = iTmpEventIndex;
	  m_UnusedEvents[eventName] = iTmpEventIndex;
	  m_InvDESEventsMap[iTmpEventIndex] = eventName; 
	  
	}		 	    
      
      // process transitions
      string sExitState;
      int iExitState = -1;

      {
	DESpot::Des::StateIteratorPtr stateIt = theDes.createStateIterator();
	for(stateIt->first(); stateIt->isDone() == false; stateIt->next())
	  {
	    const DESpot::DesState& state = stateIt->currentItem();
	    QString theName = QString::fromStdWString(state.getName());
	    sExitState = theName.toStdString();
	    
	    if (m_StatesMap.find(sExitState) == m_StatesMap.end())
	      {
		pSub->SetErr(sDESLoc + "Exiting state:" + sExitState + 
			     " in transitions does not exist",
			     HISC_BAD_DES_FORMAT);
		throw -1;
	      }
	    iExitState = m_StatesMap[sExitState];
	

	    DESpot::Des::TransIteratorPtr transIt = theDes.createTransIterator(false);   //false - include global self-loops

	    for(transIt->first(); !transIt->isDone(); transIt->next())
	      {
		const DESpot::DesTransition& trans = transIt->currentItem();
		const DESpot::DesState& fromState = trans.fromState();
		const DESpot::DesState& toState = trans.toState();
		const DESpot::DesEvent& event=  trans.event();
		
		if (state != fromState)
		  {
		    continue;
		  }

		QString transInfo = "(" + QString::fromStdWString(event.getName()) + "\t" +  QString::fromStdWString(toState.getName()) + ")";
		string theTrans = transInfo.toStdString();

		if (AddTrans(theTrans, sExitState, iExitState) < 0)
		  throw -1;
		
	      }
	  }
      }
      

      //Add event indices into m_piEventsArr;
      m_piEventsArr = new int[m_DESEventsMap.size()];
      i = 0;
      for (EVENTS::const_iterator ci = m_DESEventsMap.begin();
	   ci != m_DESEventsMap.end(); ++ci)
	{
	  m_piEventsArr[i] = ci->second;
	  ++i;
	}
      qsort(m_piEventsArr, m_DESEventsMap.size(), sizeof(int), CompareInt);
      
      //unused events
      if (m_UnusedEvents.size() > 0)
	{
	  string sWarn;
	  sWarn = "\nWarning: ";
	  sWarn += sDESLoc + "blocks events:\n";
	  for (EVENTS::const_iterator ci = m_UnusedEvents.begin();
	       ci != m_UnusedEvents.end(); ++ci)
	    {
	      sWarn += ci->first;
	      sWarn += "\n";
	    }
	  pSub->SetErr(sWarn, HISC_WARN_BLOCKEVENTS);
	}
      
    }
  catch (int iError)
    {
      iRet = iError;
    }
  return iRet;
}

/*
 * DESCR:   Add an event to CSub event map and CProject event map
 *          For CSub event map: If exists, return local index;
 *                              Otherwise create a new one.
 *          For CProject event map: If exists, must have same global index;
 *                                  Otherwise the event sets are not disjoint
 * PARA:    vsEventName: Event name(input)
 *          cEventSub: Event type ('H", 'L', 'R', 'A')(input)
 *          cControllable: Controllable? ('Y', 'N')(input)
 * RETURN:  >0 global event index
 *          <0 the event sets are not disjoint.
 * ACCESS:  Private
 */
int CDES::AddEvent(const string & vsEventName, const char cControllable)
{
    string sErr;

    int iTmpEventIndex = 0;
    int iTmpLocalEventIndex = 0;

    string sDESLoc = m_pSub->GetSubName() + ": " + m_sDESName + ": ";

    //Controllable or uncontrollable
    if (cControllable != 'Y' && cControllable != 'N')
    {
        pSub->SetErr(sDESLoc + "Unknown event controllable type--" +vsEventName,
                        HISC_BAD_DES_FORMAT);
        return -1;
    }

    //already defined in current DES
    if (m_DESEventsMap.find(vsEventName) != m_DESEventsMap.end())
    {
        pSub->SetErr(sDESLoc + "Duplicate events definition--" + vsEventName,
            HISC_BAD_DES_FORMAT);
        return -1;
    }

    //Compute local event index
    iTmpLocalEventIndex = m_pSub->AddSubEvent(vsEventName,
             (cControllable == 'Y')? CON_EVENT:UNCON_EVENT);

    if ((cControllable == 'Y' && iTmpLocalEventIndex % 2 == 0) ||
       (cControllable == 'N' && iTmpLocalEventIndex % 2 == 1))
    {
        pSub->SetErr(sDESLoc + "Event " + vsEventName +
              " has inconsistent controllability definitions.",
                HISC_BAD_DES_FORMAT);
        return -1;
    }
    //Compute global event index
    iTmpEventIndex = pSub->GenEventIndex(iTmpLocalEventIndex);

    //Add Event to pSub->m_AllEventsMap
    if (pSub->AddPrjEvent(vsEventName, iTmpEventIndex) < 0)
    {
        sErr = "Event conflict--" +  m_pSub->GetSubName() + ":" +
                this->GetDESName() + ":" +
                vsEventName + " is also defined in sub " + " event";
        pSub->SetErr(sErr, HISC_BAD_DES_FORMAT);
        iTmpEventIndex = -1;
    }

    return iTmpEventIndex;
}

/*
 * DESCR:   Add a transition to the m_pTransArr of the current DES.
 * PARA:    vsLine: a text line in [Transition] field(input)
 *          vsExitState: source state name of the transition(input)
 *          viExitState: source state index of the transition(input)
 * RETURN:  0: success -1: fail
 * ACCESS:  private
 */
int CDES::AddTrans(const string & vsLine,
                    const string & vsExitState,
                    const int viExitState)
{
    string sTrans = vsLine;

    string sEnterState;
    int iEnterStateIndex;

    string sTransEvent;
    int iTransEventIndex;

    unsigned long iSepLoc = string::npos;
    string sErrMsg;

    string sDESLoc = m_pSub->GetSubName() + ": " + m_sDESName + ": ";


    try
    {
        if (viExitState == -1)
        {
            pSub->SetErr(sDESLoc + "No existing state for transitions",
                                        HISC_BAD_DES_FORMAT);
            throw -1;
        }

        //remove '(' and ')'
        sTrans = sTrans.substr(1);
        sTrans = sTrans.substr(0, sTrans.length() - 1);
        sTrans = str_trim(sTrans);

        //find sepration character '\t' or ' '
        iSepLoc = sTrans.find_last_of('\t');
        if (iSepLoc == string::npos)
            iSepLoc = sTrans.find_last_of(' ');

        if (iSepLoc == string::npos)
        {
            pSub->SetErr(sDESLoc +
                        "No event or entering state for transition. (" +
                        sTrans + ")", HISC_BAD_DES_FORMAT);
            throw -1;
        }
        else
        {
            sEnterState = str_trim(sTrans.substr(iSepLoc + 1));
            sTransEvent = str_trim(sTrans.substr(0, iSepLoc));
        }

        //Check event in transitions
        if (m_DESEventsMap.find(sTransEvent) == m_DESEventsMap.end())
        {
            pSub->SetErr(sDESLoc + "Event " + sTransEvent +
                    " in transitions does not exist.",
                    HISC_BAD_DES_FORMAT);
            throw -1;
        }
        iTransEventIndex = m_DESEventsMap[sTransEvent];
        m_UnusedEvents.erase(sTransEvent);

        //Check entering state
        if (m_StatesMap.find(sEnterState) == m_StatesMap.end())
        {
            pSub->SetErr(sDESLoc + "State " + sEnterState +
                    " in transitions does not exist.",
                    HISC_BAD_DES_FORMAT);
            throw -1;
        }
        iEnterStateIndex = m_StatesMap[sEnterState];

        //Check determinacy
        if (m_pTransArr[viExitState].find(iTransEventIndex) !=
            m_pTransArr[viExitState].end())
        {
            pSub->SetErr(sDESLoc + "ExitState:" + vsExitState +
                    " has nondeterministic transitions on event " + sTransEvent,
                    HISC_BAD_DES_FORMAT);
            throw -1;
        }
        m_pTransArr[viExitState][iTransEventIndex] = iEnterStateIndex;
    }
    catch(int)
    {
        return -1;
    }

    return 0;
}

/*
 * DESCR:   Print this DES in memory to a file (for checking)
 * PARA:    fout: file stream(input)
 * RETURN:  0: success -1: fail
 * ACCESS:  public
 */
int CDES::PrintDES(ofstream & fout)
{
    try
    {
        int i = 0;

        fout << endl << "#-------DES: " << m_sDESName << " ---------" << endl;
        fout << "[States]" << endl;
        fout << m_iNumofStates << endl;

        for (INVSTATES::const_iterator ci = m_InvStatesMap.begin();
             ci != m_InvStatesMap.end(); ++ci)
        {
            fout << ci->second << endl;
        }

        fout << endl;
        fout << "[InitState]" << endl;
#ifdef _WIN32
        fout << m_InvStatesMap[m_iInitState + 1] << endl;
#else
        fout << m_InvStatesMap[m_iInitState] << endl;
#endif

        fout << endl;
        fout << "[MarkingStates]" << endl;
        for (MARKINGLIST::const_iterator ci = m_MarkingList.begin();
             ci != m_MarkingList.end(); ++ci)
        {
#ifdef _WIN32
	  fout << m_InvStatesMap[(*ci) +1] << endl;
#else
            fout << m_InvStatesMap[*ci] << endl;
#endif
        }

        fout << endl;
        fout << "[Events]" << endl;
        for (INVEVENTS::const_iterator ci = m_InvDESEventsMap.begin();
             ci != m_InvDESEventsMap.end(); ++ci)
        {
            if (ci->first % 2 == 0)  //uncontrollable
                fout << ci->second << "\t" << "N" << "\tL" << endl;
            else
                fout << ci->second << "\t" << "Y" << "\tL" << endl;
        }

        fout << endl;
        fout << "[Transitions]" << endl;
        if (m_pTransArr != NULL)
        {
            for (i = 0; i < m_iNumofStates; i++)
            {
#ifdef _WIN32
                fout << m_InvStatesMap[i + 1] << endl;
#else
                fout << m_InvStatesMap[i] << endl;
#endif

                for (TRANS::const_iterator ci = (m_pTransArr[i]).begin();
                     ci != (m_pTransArr[i]).end(); ++ci)
                {
#ifdef _WIN32
                    fout << "(" << m_InvDESEventsMap[ci->first] << " "
			 << m_InvStatesMap[(ci->second) + 1] << ")" << endl;
#else
                    fout << "(" << m_InvDESEventsMap[ci->first] << " "
                        << m_InvStatesMap[ci->second] << ")" << endl;
#endif
               }
            }
        }

        fout << "################################################" << endl;
    }
    catch(...)
    {
        return -1;
    }
    return 0;
}

} //end of namespace BDDSD
