/*************************************************************************
  FILE:  BddHiscMain.cpp
  DESCR: Main entrance point for the bddhisc HISC verification and
  synthesis algorithms. 
  AUTH:  Raoguang Song
  Supervisor: Dr. Ryan Leduc
  DATE:  (C) Jan, 2006
*************************************************************************/
#include "BddHiscMain.h"
#include <iostream>
#include <cstdio>
#include <string>
#include "BddHisc.h"
#include "BddHiscErrmsg.h"
#include "CounterExampleAlgo.h"
#ifdef _WIN32
#include <winsock.h>
#else
#include <termios.h>
#include <unistd.h>
#endif

#include <QString>

#include "DesProject.h"

using namespace std;


namespace BDDHISC
{


#define MAX_PATHLng 512
#define MAX_ERRMSG_LENGTH 4096



  // This function defined later in file.
  int BddHiscCheckProp(DESpot::DesProject& DESpotProj, QString
		       SubsName, bool isHigh, HISC_TESTTYPE testType,
		       Hisc_ChkInfo& checkInfo);  




/**
 * DESCR:   Checks the entire project for LD Intf Con, LD lw-
 *          nonblocking, LD lw- cont using BddHisc
 * PARA:    DESpotProj: an HISC project in DESpot format
 *          succOutputMsg: successful output string
 * RETURN:  error code 
 * ACCESS:  public
 */


  int BddHiscCheckHISCAll(DESpot::DesProject& DESpotProj, Hisc_ChkInfo& checkInfo) 
{

  int iret = 0;

  HISC_TESTTYPE testType = HISC_DOALL;

  // set to process all susbsytems
  QString SubsName =  "all!";
  // isHigh will be ignored
  bool isHigh = false;


  iret = BddHiscCheckProp(DESpotProj, SubsName, isHigh, testType,
         checkInfo);

  return iret;
    
}



/**
 * DESCR:   Checks the entire project for  LD lw- nonblocking, 
 *          using BddHisc
 * PARA:    DESpotProj: an HISC project in DESpot format
 *          SubsName: name of subsystem - ignored if high-level.
 *                    If set to "all!", then process all subsystems         
 *          isHigh:  true if subsystem is high-level - ignored if
 *                   processing all subsystems
 *          succOutputMsg: successful output string
 * RETURN:  error code 
 * ACCESS:  public
 */

  int BddHiscCheckLWNonBlk(DESpot::DesProject& DESpotProj, QString
			 SubsName, bool isHigh, Hisc_ChkInfo& checkInfo)
{

  int iret = 0;
  HISC_TESTTYPE testType = HISC_DOLWNONBLK;

  iret = BddHiscCheckProp(DESpotProj, SubsName, isHigh, testType, checkInfo);
  return iret;
    
}

/**
 * DESCR:   Checks the entire project for  LD lw- cont, 
 *          using BddHisc
 * PARA:    DESpotProj: an HISC project in DESpot format
 *          SubsName: name of subsystem - ignored if high-level.
 *                    If set to "all!", then process all subsystems         
 *          isHigh:  true if subsystem is high-level - ignored if
 *                   processing all subsystems
 *          succOutputMsg: successful output string
 * RETURN:  error code 
 * ACCESS:  public
 */

  int BddHiscCheckLWCtrl(DESpot::DesProject& DESpotProj, QString
			 SubsName, bool isHigh, Hisc_ChkInfo& checkInfo)
{

  int iret = 0;
  HISC_TESTTYPE testType = HISC_DOLWCONT;

  iret = BddHiscCheckProp(DESpotProj, SubsName, isHigh, testType, checkInfo);
  return iret;
    
}


/**
 * DESCR:   Checks the entire project for  LD lw- Intf Con, 
 *          using BddHisc
 * PARA:    DESpotProj: an HISC project in DESpot format
 *          SubsName: name of subsystem - ignored if high-level.
 *                    If set to "all!", then process all subsystems         
 *          isHigh:  true if subsystem is high-level - ignored if
 *                   processing all subsystems
 *          succOutputMsg: successful output string
 * RETURN:  error code 
 * ACCESS:  public
 */

  int BddHiscCheckIConsist(DESpot::DesProject& DESpotProj, QString
			 SubsName, bool isHigh, Hisc_ChkInfo& checkInfo)
{

  int iret = 0;
  HISC_TESTTYPE testType = HISC_DOICONSIS;

  iret = BddHiscCheckProp(DESpotProj, SubsName, isHigh, testType, checkInfo);
  return iret;
    
}


/**
 * DESCR:   Check that indicated interafce is an ld interface, 
 *          using BddHisc
 * PARA:    DESpotProj: an HISC project in DESpot format
 *          SubsName: name of subsystem - ignored if high-level.       
 *          isHigh:  true if subsystem is high-level - ignored if
 *                   processing all subsystems
 *          succOutputMsg: successful output string
 * RETURN:  error code 
 * ACCESS:  public
 */

  int BddHiscCheckIntf(DESpot::DesProject& DESpotProj, QString
			 SubsName, bool isHigh, Hisc_ChkInfo& checkInfo)
{

  int iret = 0;
  HISC_TESTTYPE testType = HISC_DOINTFCHK;

  iret = BddHiscCheckProp(DESpotProj, SubsName, isHigh, testType, checkInfo);
  return iret;
    
}


/**
 * DESCR:   Checks the entire project for check  specified in 
 *          param testType, using BddHisc
 * PARA:    DESpotProj: an HISC project in DESpot format
 *          SubsName: name of subsystem - ignored if high-level.
 *                    If set to "all!", then process all subsystems         
 *          isHigh:  true if subsystem is high-level - ignored if
 *                   processing all subsystems
 *          testType: specifies what sort of checks to do
 *          succOutputMsg: successful output string
 * RETURN:  error code 
 * ACCESS:  public
 */

  int BddHiscCheckProp(DESpot::DesProject& DESpotProj, QString
			 SubsName, bool isHigh, HISC_TESTTYPE
			 testType, Hisc_ChkInfo& checkInfo)
{

  char errmsg[MAX_ERRMSG_LENGTH];

  int iret = 0;
  char subname[MAX_PATHLng];
  //DESpot::CounterExampleAlgo::isfirsterror=true;
  //DESpot::CounterExampleAlgo::IsFirstErrorSubSystem=true;
    
  char savepath[MAX_PATHLng]; 
  savepath[0] = '\0';
  HISC_SUPERINFO superinfo;
  HISC_SAVEPRODUCTTYPE saveproducttype;
  HISC_TRACETYPE tracetype;
  
  
  init_hisc();

  iret = load_prj(DESpotProj,  errmsg);
  if ((iret < 0) && (iret > -10000))
    {
	  close_hisc();
	  QString theMessage =QString::fromStdString(errmsg);
	  throw theMessage.toStdWString();
    }


    if (iret < 0)
      {
	cout << errmsg << endl;
	iret = 0;
	errmsg[0] = '\0';
      }

    // set to not save sync prod.
    saveproducttype = HISC_NOTSAVEPRODUCT ;

    // set to not show the blocking type
    tracetype = HISC_NO_TRACE;

    bool doAll = false;
    string tmpString2 =   SubsName.toStdString();

    // If name set to "all!", then this is a full project verification. Note:
    // won't conflict with actual name of a  DESpot subsystem as "!" is
    // a forbidden character 
    if (tmpString2 == "all!")
      {
	doAll = true;
      }

    int computetime = 0;

    if (!isHigh  || doAll) {
      // Verify low-level subsystem(s) 

      // set output file path
      if (SubsName.length() < MAX_PATHLng)
	{
	  strcpy(subname, tmpString2.data());
	}
      else
	{
	  close_hisc();
	  QString theMessage = "BddHisc error: name of low-level \
subsystem '" + SubsName + "' too long.\n";
	  throw theMessage.toStdWString();
	}

      // using depot output which is html based - <ul> <li> </ul>
      // create a bulleted list in html
      checkInfo.m_succStr += "<ul>  ";

    int nextlow = 0;
    do
      {
	superinfo.statesize = -1;
	superinfo.nodesize = -1;
	superinfo.time = 0;
                    
	iret = verify_low(tracetype, subname, errmsg, &superinfo, 
			  &nextlow, saveproducttype, savepath, testType, checkInfo);
	//  construct output string to use if verification is successful.
	checkInfo.m_succStr +=  "<li> Low-level: '" + QString::fromStdString(subname) + "'.  State size: ";
	if (superinfo.statesize >= 0)
	  {
	    checkInfo.m_succStr += QString::number(superinfo.statesize) + ".  ";
	  }
	else
	  {
	    checkInfo.m_succStr += "-1.  ";
	  }

	checkInfo.m_succStr += "Computing time: " + QString::number(superinfo.time) + " second(s).";

	// output to console
	cout << "Low-level Name: " << subname << endl;
	if (iret == 0)
	  cout << "This low-level has been verified succesfully!" 
	       << endl;
	if (superinfo.statesize >= 0)
	  cout << "State size of the synchronous product: " << 
	    superinfo.statesize << endl;
	if (superinfo.nodesize >= 0)
	  cout << "Number of bdd nodes to store" << 
	    " the synchronous product: " << superinfo.nodesize 
	       << endl; 
	cout << "Computing time: " << superinfo.time << 
	  " second(s)." << endl;
	computetime += superinfo.time;



	if (iret < 0)
	  {
	    // verification for this low-level failed
	    close_hisc();
	    // output error message to console
	    cout << errmsg << endl;

	    // need to determine if a test failed as opposed to a
	    // structural error such as not enough memory
            bool testFailed = false;

	    switch(iret)
	      {
	      case HISC_BAD_INTERFACE:
		testFailed = true;
		checkInfo.m_iConsisChkFail = true;
		break;
	      case HISC_VERI_LOW_UNCON:
		testFailed = true;
		checkInfo.m_LDCtrlChkFail = true;
		break;
	      case HISC_VERI_LOW_P4FAILED:
		testFailed = true;
		checkInfo.m_iConsisChkFail = true;
		break;
	      case HISC_VERI_LOW_BLOCKING:
		testFailed = true;
		checkInfo.m_LDNBChkFail = true;
		break;
	      case HISC_VERI_LOW_P6FAILED:
		testFailed = true;
		checkInfo.m_iConsisChkFail = true;
		break;
	      case HISC_VERI_LOW_P5FAILED:
		testFailed = true;
		checkInfo.m_iConsisChkFail = true;
		break;
	      default:
		testFailed = false;
		break;
	      }

	    if (testFailed) 
	      {
		checkInfo.m_chkPassed = false;
		QString tmpErr = QString::fromStdString(errmsg);
		
		// need to replace "\n" with <br>
		int index = tmpErr.indexOf("\n",0, Qt::CaseInsensitive);
		while (index != -1)
		  {
		    tmpErr = tmpErr.replace (index, 1, "<br>");
		    index = tmpErr.indexOf("\n",index+4, Qt::CaseInsensitive);
		  }
		

		checkInfo.m_errStr += "Verification of low-level '" +
		  QString::fromStdString(subname) + "' failed.<br><br>";
		checkInfo.m_errStr += tmpErr; 
		return iret;
	      }
	    else
	      {
	      QString theMessage = "Verification of low-level '" +
		  QString::fromStdString(subname) + "' failed.\n\n";
	      theMessage += QString::fromStdString(errmsg);
	      throw theMessage.toStdWString();
	      }
	  }
      } while (nextlow > 0);
    checkInfo.m_succStr += "</ul> ";
    }
    
    //process high-level if needed
    if (isHigh  || doAll) 
      {

	// verify high-level
	superinfo.statesize = -1;
	superinfo.nodesize = -1;
	superinfo.time = 0;

	// get name of high-level
	string highName = "";

	iret = verify_high(tracetype, errmsg, &superinfo, 
			   saveproducttype, savepath, testType, highName,checkInfo);
	checkInfo.m_succStr +=  "<ul> <li> High-level '" +
		  QString::fromStdString(highName) + "'  state size: ";
	if (superinfo.statesize >= 0)
	  {
	    checkInfo.m_succStr += QString::number(superinfo.statesize) + ".  ";
	  }
	else
	  {
	    checkInfo.m_succStr += "-1.  ";
	  }

	checkInfo.m_succStr += "Computing time: " + QString::number(superinfo.time) +" second(s).</ul> ";
	computetime += superinfo.time;
	checkInfo.m_succStr += "Total computing time for project: " +
	QString::number(computetime) + " second(s).";

	//output to console
	if (iret == 0)
	  cout << "The high-level has been verified succesfully!" 
	       << endl;
	if (superinfo.statesize >= 0)
	  cout << "State size of the synchronous product: " 
	       << superinfo.statesize << endl;
	if (superinfo.nodesize >= 0)
	  cout << "Number of bdd nodes to store" << 
	    " the synchronous product: " << superinfo.nodesize << endl; 
	cout << "Computing time: " << superinfo.time 
	     << " second(s)." << endl;

	cout << "Total computing time for project:" << computetime << " second(s)."  << endl;

	if (iret < 0)
	  {
	    // verification of high-level failed
	    close_hisc();
	    // output error message to console
	    cout << errmsg << endl;
	
	    // need to determine if a test failed as opposed to a
	    // structural error such as not enough memory
            bool testFailed = false;

	    switch(iret)
	      {
	      case HISC_VERI_HIGH_UNCON:
		testFailed = true;
		checkInfo.m_LDCtrlChkFail = true;
		break;
	      case HISC_VERI_HIGH_P3FAILED:
		testFailed = true;
		checkInfo.m_iConsisChkFail = true;
		break;
	      case HISC_VERI_HIGH_BLOCKING:
		testFailed = true;
		checkInfo.m_LDNBChkFail = true;
		break;
	      default:
		testFailed = false;
		break;
	      }

	    if (testFailed) 
	      {
		checkInfo.m_chkPassed = false;
		QString tmpErr = QString::fromStdString(errmsg);
				
		// need to replace "\n" with <br>
		int index = tmpErr.indexOf("\n",0, Qt::CaseInsensitive);
		while (index != -1)
		  {
		    tmpErr = tmpErr.replace (index, 1,	"<br>");
		    index = tmpErr.indexOf("\n",index+4, Qt::CaseInsensitive);
		  }

		checkInfo.m_errStr += "Verification of high-level failed. <br> <br>";
		checkInfo.m_errStr += tmpErr;
		return iret;
	      }
	    else
	      {
	      QString theMessage = "Verification of high-level failed.\n\n";
	      theMessage += QString::fromStdString(errmsg);
	      throw theMessage.toStdWString();
	      }
	  }
      }

    //if got this far, then verification is successful.

    close_hisc();
    checkInfo.m_chkPassed = true;

    return iret;
    
}




/**
 * DESCR:   Performs HISC level-wise synthesis for subsystem 
 *           using BddHisc
 * PARA:    DESpotProj: an HISC project in DESpot format
 *          OutFileType: 'b'  means ouput synthesis to BDD file
 *          format, 'd' to synchronous product, and 'o' to both.
 *          filePath:  directory to save files into.
 *          SubsName: name of subsystem - ignored if high-level.
 *                   If set to "all!", then process all subsystems         
 *          isHigh:  true if subsystem is high-levell - ignored if
 *                   processing all subsystems
 *          succOutputMsg: successful output string
 * RETURN:  error code 
 * ACCESS:  public
 */

  int BddHiscLWSynth(DESpot::DesProject& DESpotProj, char OutFileType,
		       QString filePath, QString SubsName, bool isHigh, Hisc_ChkInfo& checkInfo)
{

  char errmsg[MAX_ERRMSG_LENGTH];

  int iret = 0;
  char subname[MAX_PATHLng];
    
  char savepath[MAX_PATHLng]; 
  savepath[0] = '\0';
  HISC_SUPERINFO superinfo;
  HISC_SAVESUPERTYPE savesupertype;

  //  checkInfo.m_succStr += "Level-wise synthesis complete.\n\n";
  

  
  init_hisc();

  iret = load_prj(DESpotProj,  errmsg);
  if ((iret < 0) && (iret > -10000))
    {
	  close_hisc();
	  QString theMessage =QString::fromStdString(errmsg);
	  throw theMessage.toStdWString();
    }


    if (iret < 0)
      {
	cout << errmsg << endl;
	iret = 0;
	errmsg[0] = '\0';
      }

    // set file type for saving supervisors
    switch(OutFileType)
      {
      case 'b':
	savesupertype = HISC_SAVESUPER_BDD;
	break;
      case 'd':
	savesupertype = HISC_SAVESUPER_AUTOMATA;
	break;
      case 'o':
	savesupertype = HISC_SAVESUPER_BOTH;
	break;
      default:
	savesupertype = HISC_SAVESUPER_BDD;
	assert(false); //unknown file type
	break;
      }

    string tmpString =  filePath.toStdString();

    // set output file path
    if (filePath.length() < MAX_PATHLng)
      {
	strcpy(savepath, tmpString.data());
      }
    else
      {
	close_hisc();
	    QString theMessage = "BddHisc error: path name to save supervisors is too long.\n" ;
	    throw theMessage.toStdWString();
      }

    int computetime = 0;

    bool doAll = false;
    string tmpString2 =   SubsName.toStdString();

    // If name set to "all!", then this is a full project synhtesis. Note:
    // won't conflict with actual name of a  DESpot subsystem as "!" is
    // a forbidden character 
    if (tmpString2 == "all!")
      {
	doAll = true;
      }

    if (!isHigh  || doAll) {
      // synthesize supervisor for the low-level subsystem 

      // set output file path
      if (SubsName.length() < MAX_PATHLng)
	{
	  strcpy(subname, tmpString2.data());
	}
      else
	{
	  close_hisc();
	  QString theMessage = "BddHisc error: name of low-level \
subsystem \"" + SubsName + "\" too long.\n";
	  throw theMessage.toStdWString();
	}


      int nextlow = 0;
      do
	{
	  superinfo.statesize = -1;
	  superinfo.nodesize = -1;
	  superinfo.time = 0;
                    
	  iret = syn_lowsuper(HISC_ONREACHABLE, subname, errmsg, 
			      &superinfo, &nextlow, savesupertype, savepath);

	  //  construct output string to use if verification is successful.
	  checkInfo.m_succStr +=  "- Low-level: " + QString::fromStdString(subname) + 
	    ".  State size: ";
	  if (superinfo.statesize >= 0)
	    {
	      checkInfo.m_succStr += QString::number(superinfo.statesize) + ".  ";
	    }
	  else
	    {
	      checkInfo.m_succStr += "-1.  ";
	    }

	  checkInfo.m_succStr += "Computing time: " + QString::number(superinfo.time) + " second(s).\n";

	  // output to console
	  cout << "Low-level Name: " << subname << endl;
	  if (iret == 0)
	    cout << "Synthesis successful for this low-level!" 
		 << endl;
	  if (superinfo.statesize >= 0)
	    cout << "State size of the synchronous product: " << 
	      superinfo.statesize << endl;
	  if (superinfo.nodesize >= 0)
	    cout << "Number of bdd nodes to store" << 
	      " the synchronous product: " << superinfo.nodesize 
		 << endl; 
	  cout << "Computing time: " << superinfo.time << 
	    " second(s)." << endl;
	  computetime += superinfo.time;

	  if (iret < 0)
	    {
	      // synthesis for this low-level failed
	      close_hisc();
	      // output error message to console
	      cout << errmsg << endl;

	      QString theMessage = "Synthesis of low-level \"" +
		QString::fromStdString(subname) + "\" failed.\n\n";
	      theMessage += QString::fromStdString(errmsg);
	      throw theMessage.toStdWString();
	    }
	} while (nextlow > 0);
    }



    //process high-level if needed
    if (isHigh  || doAll) 
      {
	
	// synthesize supervisor for high-level
	superinfo.statesize = -1;
	superinfo.nodesize = -1;
	superinfo.time = 0;
	
	iret = syn_highsuper(HISC_ONREACHABLE, errmsg, &superinfo, 
			     savesupertype, savepath);
	
	checkInfo.m_succStr +=  "- High-level state size: ";
	if (superinfo.statesize >= 0)
	  {
	    checkInfo.m_succStr += QString::number(superinfo.statesize) + ".  ";
	  }
	else
	  {
	    checkInfo.m_succStr += "-1.  ";
	  }
	
	checkInfo.m_succStr += "Computing time: " + QString::number(superinfo.time) +" second(s).\n\n";
	computetime += superinfo.time;
	checkInfo.m_succStr += "Total computing time for project: " +
	QString::number(computetime) + " second(s).\n";

	//output to console
	if (iret == 0)
	  cout << "High-level synthesis succesfull!" 
	       << endl;
	if (superinfo.statesize >= 0)
	  cout << "State size of the synchronous product: " 
	       << superinfo.statesize << endl;
	if (superinfo.nodesize >= 0)
	  cout << "Number of bdd nodes to store" << 
	    " the synchronous product: " << superinfo.nodesize << endl; 
	cout << "Computing time: " << superinfo.time 
	     << " second(s)." << endl;

	cout << "Total computing time for project:" << computetime << " second(s)."  << endl;

	if (iret < 0)
	  {
	    // synthesis for high-level failed
	    close_hisc();
	    // output error message to console
	    cout << errmsg << endl;
	
	    QString theMessage = "Synthesis of high-level failed.\n\n";
	    theMessage += QString::fromStdString(errmsg);
	    throw theMessage.toStdWString();
	  }
      }

    //if got this far, then synthesis was successful.

    QString tmpErr = checkInfo.m_succStr;
    
    // need to replace "\n" with <br>
    int index = tmpErr.indexOf("\n",0, Qt::CaseInsensitive);
    while (index != -1)
      {
	tmpErr = tmpErr.replace (index, 1,	"<br>");
	index = tmpErr.indexOf("\n",index+4, Qt::CaseInsensitive);
      }

    checkInfo.m_succStr = tmpErr;
    
    close_hisc();
    
    return iret;
    
}
/*
// Added by zain for counter example
void  Hisc_ChkInfo::setErrorTuple(int size,CounterExampleStateTuple in_tuple)
{
	FirstErrorTuple= new CounterExampleStateTuple(size);
	*FirstErrorTuple=in_tuple;
}
*/

// should now be able to remove remaining functions


/*


 * DESCR:   Main entry function for BddHisc
 * PARA:    DESpotProj: an HISC project in DESpot format
 * RETURN:  error code 
 * ACCESS:  public
 

  int BddHiscMain(DESpot::DesProject& DESpotProj)
{
    bool bPrjLoaded = false;
    char ch = '\0';
    char prjfile[MAX_PATHLng];
    char errmsg[MAX_ERRMSG_LENGTH];
    prjfile[0] = '\0';
    int iret = 0;
    char prjoutputfile[MAX_PATHLng];
    char subname[MAX_PATHLng];
    
    int nextlow = 0;
    char savepath[MAX_PATHLng]; 
    savepath[0] = '\0';
    HISC_SUPERINFO superinfo;
    HISC_SAVESUPERTYPE savesupertype;
    HISC_SAVEPRODUCTTYPE saveproducttype;
    HISC_TRACETYPE tracetype;
    int computetime = 0;
    HISC_TESTTYPE testType = HISC_DOALL;
    
    init_hisc();

    //    iret = load_prj(prjfile, errmsg);
    iret = load_prj(DESpotProj,  errmsg);
    if (iret < 0)
      {
	if (iret > -10000) //error
	  bPrjLoaded = false;
	else
	  bPrjLoaded = true; //waring
      }
    else
      bPrjLoaded = true;

    if (iret < 0)
      {
	cout << errmsg << endl;
	cout << "Press any key to continue...";
	iret = 0;
	errmsg[0] = '\0';
	getkeystroke(NULL, 0);
      }

    
    while (ch != 'q' && ch != 'Q')
    {
        ch = getchoice(bPrjLoaded, prjfile);
        switch (ch)
        {
            case 'q':
            case 'Q':
                break;
            //Load a project
            case 'P':
            case 'p':
                cout << "Project name:";
                cin.getline(prjfile, MAX_PATHLng);
                iret = load_prj(DESpotProj,  errmsg);
                if (iret < 0)
                {
                    if (iret > -10000) //error
                        bPrjLoaded = false;
                    else
                        bPrjLoaded = true; //waring
                }
                else
                    bPrjLoaded = true;
                break;
            //close the current project
            case 'c':
            case 'C':
                iret = close_prj(errmsg);
                bPrjLoaded = false;
                prjfile[0] = '\0';
                break;
            //File the current project
            case 'f':
            case 'F':
                cout << "file name:";
                cin.getline(prjoutputfile, MAX_PATHLng);
                iret = print_prj(prjoutputfile, errmsg);
                break;
            //Low Level synthesis
            case 'o':
            case 'O':
                cout << "low-level name:";
                cin.getline(subname, MAX_PATHLng);
                cout << "Save the supervisor? (0:none  1:bdd-based " << 
                     "2:automata-based  3:both)" << endl;
                cout << "Warning: choose 2 or 3 may generate huge file."<< endl;
                cout << "Your choice:";
                savesupertype = (HISC_SAVESUPERTYPE)getchoice_savesup();
                if (savesupertype != HISC_SAVESUPER_NONE)
                {
                    cout << "Path to save the supervisor:";
                    cin.getline(savepath, MAX_PATHLng);
                }
                
                nextlow = 0;
                computetime = 0;
                do
                {
                    superinfo.statesize = -1;
                    superinfo.nodesize = -1;
                    superinfo.time = 0;
                    iret = syn_lowsuper(HISC_ONREACHABLE, subname, errmsg, 
                                        &superinfo, &nextlow, 
                                        savesupertype, savepath);
                    cout << "Low-Level Name: " << subname << endl;
                    if (iret == 0)
                    {
                        cout << "Supervisor state size: " << 
                                            superinfo.statesize << endl;
                        cout << "Number of bdd nodes to store the supervisor: " 
                                            << superinfo.nodesize << endl; 
                        cout << "Computing time:" << superinfo.time << 
                                            " seconds." << endl;
                        computetime += superinfo.time;
                    }
                    else
                    {
                        cout << errmsg << endl;
                        cout << "Press any key to continue...";
                        iret = 0;
                        errmsg[0] = '\0';
                        getkeystroke(NULL, 0);
                    }
                } while (nextlow > 0);
                
                cout << "Total computing time:" << computetime << 
                            " seconds." << endl;

                break;
            //Low Level verification
            case 'l':
            case 'L':
                cout << "low level name:";
                cin.getline(subname, MAX_PATHLng);
                cout << "Save the synchronous product" << 
                        "(may generate huge file)(Y/N)? ";
                saveproducttype = (HISC_SAVEPRODUCTTYPE)getchoice_saveproduct();
                if (saveproducttype != HISC_NOTSAVEPRODUCT)
                {
                    cout << "Path to save the synchronous product:";
                    cin.getline(savepath, MAX_PATHLng);
                }

                cout << "Show the blocking type(may take long time)(Y/N)?";
                tracetype = (HISC_TRACETYPE)getchoice_tracetype();

                nextlow = 0;
                computetime = 0;
                do
                {
                    superinfo.statesize = -1;
                    superinfo.nodesize = -1;
                    superinfo.time = 0;
                    
                    iret = verify_low(tracetype, subname, errmsg, &superinfo, 
				      &nextlow, saveproducttype,
				      savepath, testType);
                    cout << "Low Level Name: " << subname << endl;
                    if (iret == 0)
                        cout << "This low level has been verified succesfully!" 
                             << endl;
                    if (superinfo.statesize >= 0)
                        cout << "State size of the synchronous product: " << 
                                superinfo.statesize << endl;
                    if (superinfo.nodesize >= 0)
                        cout << "Number of bdd nodes to store" << 
                            " the synchronous product: " << superinfo.nodesize 
                            << endl; 
                    cout << "Computing time: " << superinfo.time << 
                            " seconds." << endl;
                    computetime += superinfo.time;
                    if (iret < 0)
                    {
                        cout << errmsg << endl;
                        cout << "Press any key to continue...";
                        iret = 0;
                        errmsg[0] = '\0';
                        getkeystroke(NULL, 0);
                    }
                } while (nextlow > 0);

                cout << "Total computing time:" << computetime << " seconds." 
                        << endl;

                break;
            //High Level synthesis
            case 'i':
            case 'I':
                cout << "Save the supervisor? (0:none  1:bdd-based  " << 
                        "2:automata-based  3:both)" << endl;
                cout << "Warning: choose 2 or 3 may generate huge file." <<endl;
                cout << "Your choice:";
                savesupertype = (HISC_SAVESUPERTYPE)getchoice_savesup();
                if (savesupertype != HISC_SAVESUPER_NONE)
                {
                    cout << "Path to save the supervisor:";
                    cin.getline(savepath, MAX_PATHLng);
                }

                superinfo.statesize = -1;
                superinfo.nodesize = -1;
                superinfo.time = 0;
                iret = syn_highsuper(HISC_ONREACHABLE, errmsg, &superinfo, 
                                    savesupertype, savepath);
                if (iret == 0)
                {
                    cout << "Supervisor state size: " << 
                            superinfo.statesize << endl;
                    cout << "Number of bdd nodes to store the supervisor: " << 
                            superinfo.nodesize << endl; 
                    cout << "Computing time:" << superinfo.time << 
                            " seconds." << endl;
                }
                break;
            //High Level verification
            case 'h':
            case 'H':
                cout << "Save the synchronous product" << 
                        "(may generate huge file)(Y/N)? ";
                saveproducttype = (HISC_SAVEPRODUCTTYPE)getchoice_saveproduct();
                if (saveproducttype != HISC_NOTSAVEPRODUCT)
                {
                    cout << "Path to save the synchronous product:";
                    cin.getline(savepath, MAX_PATHLng);
                }

                cout << "Show the blocking type(may take long time)(Y/N)?";
                tracetype = (HISC_TRACETYPE)getchoice_tracetype();

                superinfo.statesize = -1;
                superinfo.nodesize = -1;
                superinfo.time = 0;
                
                iret = verify_high(tracetype, errmsg, &superinfo, 
                        saveproducttype, savepath, testType);
                if (iret == 0)
                    cout << "The high level has been verified succesfully!" 
                         << endl;
                if (superinfo.statesize >= 0)
                    cout << "State size of the synchronous product: " 
                        << superinfo.statesize << endl;
                if (superinfo.nodesize >= 0)
                    cout << "Number of bdd nodes to store" << 
                    " the synchronous product: " << superinfo.nodesize << endl; 
                cout << "Computing time: " << superinfo.time 
                    << " seconds." << endl;
                break;
        }
        if (iret < 0)
        {
            cout << errmsg << endl;
            cout << "Press any key to continue...";
            iret = 0;
            errmsg[0] = '\0';
            getkeystroke(NULL, 0);
        }
    }
    
    close_hisc();
    
    return 0;


}



int getchoice(bool bPrjLoaded, const char *prjfile)
{
    char allowed_choice[50];
    int numofchoice = 0;
    
    cout << endl << endl << endl << endl << endl;
    cout << "*************************************************" << endl;
    cout << "  Bdd-based HISC Synthesis and Verification Tool " << endl;
    cout << "*************************************************" << endl;
    if (!bPrjLoaded)
    {
        allowed_choice[0] = 'p';
        allowed_choice[1] = 'P';
        allowed_choice[2] = 'q';
        allowed_choice[3] = 'Q'; 
        numofchoice = 4;
        cout << "  P - Load a HISC project                        " << endl;
    }
    else
    {
        allowed_choice[0] = 'c';
        allowed_choice[1] = 'C';
        allowed_choice[2] = 'q';
        allowed_choice[3] = 'Q';
        allowed_choice[4] = 'h';
        allowed_choice[5] = 'H';
        allowed_choice[6] = 'i';
        allowed_choice[7] = 'I'; 
        allowed_choice[8] = 'F';
        allowed_choice[9] = 'f'; 
        allowed_choice[10] = 'O';
        allowed_choice[11] = 'o'; 
        allowed_choice[12] = 'l';
        allowed_choice[13] = 'L'; 
        numofchoice = 14;
        cout << "  H - High level verification                    " << endl;
        cout << "  I - High level synthesis                       " << endl;
        cout << "  L - Low Level verification                     " << endl;
        cout << "  O - Low Level synthesis                        " << endl;
        cout << "  F - File the current project                   " << endl;
        cout << "  C - Close the current project                  " << endl;
    }
    cout << "  Q - Quit                                       " << endl;
    cout << "*************************************************" << endl;
    if (bPrjLoaded)
    {
        cout << "Current Project: " << prjfile << endl;
    }
    cout << endl;
    cout << "Procedure desired:";
    return getkeystroke(allowed_choice, numofchoice);
}

char getkeystroke(char *allowed_choices, int len)
{
    char choice;
    struct termios initial_settings, new_settings;
    
    //cin.ignore(255, '\n');
    tcgetattr(fileno(stdin), &initial_settings);
    new_settings = initial_settings;
    new_settings.c_lflag &= ~ICANON;
    //new_settings.c_lflag &= ~ECHO;
    new_settings.c_cc[VMIN] = 1;
    new_settings.c_cc[VTIME] = 0;
    new_settings.c_lflag &= ~ISIG;
    
    tcsetattr(fileno(stdin), TCSANOW, &new_settings);
    if (len > 0)
    {
        do {
            choice = fgetc(stdin);
            int i;
            for (i = 0; i < len; i++)
            {
                if (choice == allowed_choices[i])
                    break;
            }
            if (i == len)
                choice = '\n';
        } while (choice == '\n' || choice == '\r');
    }
    else
        choice = fgetc(stdin);
    
    tcsetattr(fileno(stdin),TCSANOW, &initial_settings);
    cout << endl;
    return choice;
}

int getchoice_savesup()
{
    char allowed_choice[50];
    int numofchoice = 0;
    char choice;
    
    allowed_choice[0] = '0';
    allowed_choice[1] = '1';
    allowed_choice[2] = '2';
    allowed_choice[3] = '3';
    numofchoice = 4;
    choice = getkeystroke(allowed_choice, numofchoice);
    return choice - '0';
}

int getchoice_saveproduct()
{
    char allowed_choice[50];
    int numofchoice = 0;
    char choice;
    
    allowed_choice[0] = 'Y';
    allowed_choice[1] = 'y';
    allowed_choice[2] = 'N';
    allowed_choice[3] = 'n';
    numofchoice = 4;
    choice = getkeystroke(allowed_choice, numofchoice);
    
    if (choice == 'Y' || choice == 'y')
        return 1;
    else
        return 0;
}

int getchoice_tracetype()
{
    char allowed_choice[50];
    int numofchoice = 0;
    char choice;
    
    allowed_choice[0] = 'Y';
    allowed_choice[1] = 'y';
    allowed_choice[2] = 'N';
    allowed_choice[3] = 'n';
    numofchoice = 4;
    choice = getkeystroke(allowed_choice, numofchoice);
    
    if (choice == 'Y' || choice == 'y')
        return 1;
    else
        return 0;
}

*/

} //end of namespace BDDHISC
