/*************************************************************************
  FILE:  BddHiscDES.cpp
  DESCR: Processing DES file
  AUTH:  Raoguang Song
  Supervisor: Dr. Ryan Leduc
  DATE:  (C) Jan, 2006
*************************************************************************/
#include <QString>

#include "BddHisc.h"

#include "BddHiscDES.h"
#include "BddHiscPubfunc.h"
#include <fstream>
#include <cstdlib>
#include "BddHiscType.h"
#include "BddHiscProject.h"
#include "BddHiscErrmsg.h"
#include <cassert>
#include "BddHiscSub.h"
#include "BddHiscLowSub.h"
#include "BddHiscHighSub.h"

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

// for debug
//#include <iostream>

using namespace std;

namespace BDDHISC
{

extern CProject *pPrj;

/**
 * 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:    None
 * RETURN:  0: sucess  -1: fail
 * ACCESS:  public
 */
int CDES::LoadDES(DESpot::Des& theDes, bool isHigh)
{
    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 + ": "; 
 
      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)
	{
	  pPrj->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())  
	 {
	   pPrj->SetErr(sDESLoc + "Duplicate state names--" + 
			stateName, HISC_BAD_DES_FORMAT);
	   throw -1;
	 }
       else if (stateName[0] == '(')
	 {
	   pPrj->SetErr(sDESLoc + 
			"The first letter of state names can not be (", 
			HISC_BAD_DES_FORMAT);
	   throw -1;
	 }
       else
	 {

       /*  This 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;
#elif defined __APPLE__
                m_StatesMap[stateName] = m_StatesMap.size();
                m_InvStatesMap[m_StatesMap.size() -1] = 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())
	 {
	   pPrj->SetErr(sDESLoc + "Initial state is not defined.", 
			HISC_BAD_DES_FORMAT);
	   throw -1;
	 }

	 //only one initial state allowed
	 if (m_iInitState != -1)  
	   {
	     pPrj->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())
	      {
		pPrj->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)
		  {
		    pPrj->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';
	}
    
        switch(event.getType())
        {
            case DESpot::eDefaultEvent:
                if (isHigh)
                {
                    cEventSub = 'H';
                }

                else
                {
                    if (event.isChildLDEvent())
                    {
                        cEventSub = 'Z';
                    }
                    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:
                if (event.isChildLDEvent())
                {
                    cEventSub = 'Z';
                }
                else
                {
                    cEventSub = 'L';
                }
                break;

            default:
                assert(false); //unknown event type
                break;
            }
    
      // cEventSub, cControllable, eventName                    
      if (cEventSub >= 'a')
	cEventSub -= 32;
      if (cControllable >= 'a')
	cControllable -= 32;
      
      iTmpEventIndex = AddEvent(eventName, cEventSub, 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())
	  {
	    pPrj->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(blocked 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";
	}
      pPrj->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', 'D')(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 cEventSub, 
                    const char cControllable)
{
    string sErr;
        
    int iTmpEventIndex = 0;
    int iTmpLocalEventIndex = 0;
    
    EVENTSUB vConflictEventSub = H_EVENT;
    int viConflictSubIndex = -1;
    
    string sDESLoc = m_pSub->GetSubName() + ": " + m_sDESName + ": ";
    
    //Interface DES
    if (m_DESType == INTERFACE_DES)
    {
        //Modified to add support for Low Data Events --H.I.
        if (cEventSub != 'R' && cEventSub != 'A' && cEventSub != 'D')
        {
            pPrj->SetErr(sDESLoc + "Interface DES can only include request," +
                        " answer or low data events.", HISC_BAD_DES_FORMAT);
            return -1;
        }
    }
    //Controllable or uncontrollable
    if (cControllable != 'Y' && cControllable != 'N')
    {
        pPrj->SetErr(sDESLoc + "Unknown event controllablility type--" +vsEventName,
                        HISC_BAD_DES_FORMAT);
        return -1;
    }

    //already defined in current DES
    if (m_DESEventsMap.find(vsEventName) != m_DESEventsMap.end())
    {
        pPrj->SetErr(sDESLoc + "Duplicate events definition--" + vsEventName, 
            HISC_BAD_DES_FORMAT);
        return -1;
    }
    
    //High sub DES
    if (m_pSub->GetSubIndex() == 0)
    {
        //Modified to add reject child LD events (if found in the high level) --H.I.
        if ((cEventSub == 'L') || (cEventSub == 'Z'))
        {
            pPrj->SetErr(sDESLoc + "High sub DES includes a low sub event--" +
                        vsEventName, HISC_BAD_DES_FORMAT);
            return -1;
        }
        if (cEventSub == 'H')  //high sub event
        {
            //Compute local event index
            iTmpLocalEventIndex = m_pSub->AddSubEvent(vsEventName, 
                                        SubLetterToValue(cEventSub), 
                                        (cControllable == 'Y')? 
                                        CON_EVENT:UNCON_EVENT);

            if ((cControllable == 'Y' && iTmpLocalEventIndex % 2 == 0) ||
               (cControllable == 'N' && iTmpLocalEventIndex % 2 == 1))
            {
                pPrj->SetErr(sDESLoc + "Event " + vsEventName + 
                             " has inconsistent controllability definitions.", 
                    HISC_BAD_DES_FORMAT);
                return -1;
            }

            //Compute global event index
            iTmpEventIndex = pPrj->GenEventIndex(SubLetterToValue(cEventSub), 
                                                m_pSub->GetSubIndex(), 
                                                iTmpLocalEventIndex);
        }
        else  //interface events
        {
            iTmpEventIndex = pPrj->SearchPrjEvent(vsEventName);
            if (iTmpEventIndex < 0)
            {
                pPrj->SetErr(sDESLoc + "Event " + vsEventName + 
                             " is not a valid Request/Answer/Low Data Event.",
                             HISC_BAD_DES_FORMAT);
                return -1;
            }
            else
            {
                int iEventSub = iTmpEventIndex >> 28;
                int iSubIndex = (iTmpEventIndex & 0x0FFF0000) >> 16;
                if ((EVENTSUB)iEventSub != SubLetterToValue(cEventSub))
                {
                    pPrj->SetErr(sDESLoc + "Event " + vsEventName + 
                        " is not a " + SubValueToLetter((EVENTSUB)iEventSub) + 
                        " Event in low-level " + 
                        pPrj->GetSub(iSubIndex)->GetSubName(), 
                        HISC_BAD_DES_FORMAT);
                    return -1;
                }
                else if(!((iTmpEventIndex % 2 == 0 && cControllable == 'N') || 
                        (iTmpEventIndex % 2 == 1 && cControllable == 'Y')))
                {
                    pPrj->SetErr(sDESLoc + "Event " + vsEventName + 
                        " doesn't have same controllable property in low-level " 
                        + pPrj->GetSub(iSubIndex)->GetSubName(), 
                        HISC_BAD_DES_FORMAT);
                    return -1;
                }
                else
                    return iTmpEventIndex;
            }
        }
    }
    else //Low sub DES
    {
        if (cEventSub == 'H')
        {
            pPrj->SetErr(sDESLoc + "Low sub DES includes a high sub event--" +
                vsEventName, HISC_BAD_DES_FORMAT);
            return -1;
        }
        if (m_DESType == INTERFACE_DES || cEventSub == 'L' || cEventSub == 'Z')
        {
            //Compute local event index
            iTmpLocalEventIndex = m_pSub->AddSubEvent(vsEventName, 
                     SubLetterToValue(cEventSub),
                     (cControllable == 'Y')? CON_EVENT:UNCON_EVENT);

            //Controllable event indices are odd (starting from 1)
            //Uncontrollable event indices are even (starting from 0)
            //If this is not the case, then the controllability definitions
            //are inconsistent. --H.I.
            if ((cControllable == 'Y' && iTmpLocalEventIndex % 2 == 0) ||
               (cControllable == 'N' && iTmpLocalEventIndex % 2 == 1))
            {
                pPrj->SetErr(sDESLoc + "Event " + vsEventName + 
                      " has inconsistent controllability definitions.", 
                        HISC_BAD_DES_FORMAT);
                return -1;
            }
            //Compute global event index
            iTmpEventIndex = pPrj->GenEventIndex(SubLetterToValue(cEventSub), 
                                                m_pSub->GetSubIndex(), 
                                                iTmpLocalEventIndex);
        }
        else  //'R', 'A' or 'D' appeared in low level des, must be in interface des
        {
            iTmpEventIndex = pPrj->SearchPrjEvent(vsEventName);
            if (iTmpEventIndex < 0)
            {
                pPrj->SetErr(sDESLoc + "Event " + vsEventName + 
                    " is not a valid valid Request/Answer Event.",
                    HISC_BAD_DES_FORMAT);
                return -1;
            }
            else
            {
                int iEventSub = iTmpEventIndex >> 28;
                int iSubIndex = (iTmpEventIndex & 0x0fff0000) >> 16;
                if (iSubIndex != m_pSub->GetSubIndex())
                {
                    pPrj->SetErr(sDESLoc + "Event " + vsEventName + 
                        " is an invalid Request/Answer/Low Data Event in interface DES.",
                        HISC_BAD_DES_FORMAT);
                    return -1;
                }
                else if ((EVENTSUB)iEventSub != SubLetterToValue(cEventSub))
                {
                    pPrj->SetErr(sDESLoc + "Event " + vsEventName + 
                        " has a different event level in the interface DES.", 
                        HISC_BAD_DES_FORMAT);
                    return -1;
                }
                else if(!((iTmpEventIndex % 2 == 0 && cControllable == 'N') || 
                        (iTmpEventIndex % 2 == 1 && cControllable == 'Y')))
                {
                    pPrj->SetErr(sDESLoc + "Event " + vsEventName + 
                     " has a different controllable property in interface DES.", 
                     HISC_BAD_DES_FORMAT);
                    return -1;
                }
                else
                    return iTmpEventIndex;
            }
        }
    }
    
    //Add Event to pPrj->m_AllEventsMap
    if (pPrj->AddPrjEvent(vsEventName, iTmpEventIndex, 
                    vConflictEventSub, viConflictSubIndex) < 0)
    {
        sErr = "Event conflict--" +  m_pSub->GetSubName() + ":" + 
                this->GetDESName() + ":" + 
                vsEventName + " is also defined in sub " + 
                pPrj->GetSub(viConflictSubIndex)->GetSubName() + " as a " + 
                SubValueToLetter(vConflictEventSub) + " event";
        pPrj->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)
        {
            pPrj->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)
        {
            pPrj->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())
        {
            pPrj->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())
        {
            pPrj->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())
        {
            pPrj->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" << "\t" << 
                    SubValueToLetter((EVENTSUB)(ci->first >> 28)).at(0) << endl;
            else
                fout << ci->second << "\t" << "Y" << "\t" <<
                    SubValueToLetter((EVENTSUB)(ci->first >> 28)).at(0) << 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 BDDHISC
