/*************************************************************************
  FILE:  BddSdMain.cpp
  DESCR: Main entrance point for the Sampled-data algorithms.
  AUTH:  Raoguang Song, Yu Wang
  DATE:  (C) Jan, 2006, 2008
*************************************************************************/
#include "BddSdMain.h"
#include "BddSdType.h"
#include "BddSd.h"
#include "BddSdPubfunc.h"
#include "CounterExampleAlgo.h"
#include <iostream>
#include <cstdio>
#include <cstdlib>
#include <string>
#ifdef _WIN32
#include <winsock.h>
#else
#include <termios.h>
#include <unistd.h>
#endif

using namespace std;

namespace BDDSD
{

#define MAX_PATHlng 256
#define MAX_ERRMSG_LENGTH 4096

  // This function defined later in file.
  int BddSDCheckProp(DESpot::DesProject& DESpotProj, SD_TESTTYPE testType,
		       SD_ChkInfo& checkInfo); 

/**
 * DESCR:   Checks the entire project for all bddsd properties
 * PARA:    DESpotProj: an HISC project in DESpot format
 *          SD_ChkInfo: contains output messages and success flags
 * RETURN:  error code 
 * ACCESS:  public
 */
int BddSdCheckSDAll(DESpot::DesProject& DESpotProj, SD_ChkInfo&
checkInfo)
{

  int iret = 0;
  SD_TESTTYPE testType = SD_DOALL;

  iret = BddSDCheckProp(DESpotProj, testType, checkInfo);

  return iret;

}

/**
 * DESCR:   Checks the entire project for nonblocking
 * PARA:    DESpotProj: an HISC project in DESpot format
 *          SD_ChkInfo: contains output messages and success flags
 * RETURN:  error code 
 * ACCESS:  public
 */
int BddSdCheckNB(DESpot::DesProject& DESpotProj, SD_ChkInfo&
checkInfo)
{

  int iret = 0;
  SD_TESTTYPE testType = SD_DONONBLK;

  iret = BddSDCheckProp(DESpotProj, testType, checkInfo);

  return iret;

}


/**
 * DESCR:   Checks the entire project for untimed controllability
 * PARA:    DESpotProj: an HISC project in DESpot format
 *          SD_ChkInfo: contains output messages and success flags
 * RETURN:  error code 
 * ACCESS:  public
 */
int BddSdCheckCtrl(DESpot::DesProject& DESpotProj, SD_ChkInfo&
checkInfo)
{

  int iret = 0;
  SD_TESTTYPE testType = SD_DOCONT;

  iret = BddSDCheckProp(DESpotProj, testType, checkInfo);

  return iret;

}

/**
 * DESCR:   Checks the entire project for SD controllability
 * PARA:    DESpotProj: an HISC project in DESpot format
 *          SD_ChkInfo: contains output messages and success flags
 * RETURN:  error code 
 * ACCESS:  public
 */
int BddSdCheckSDCtrl(DESpot::DesProject& DESpotProj, SD_ChkInfo&
checkInfo)
{

  // note: at moment S-singular behavior is also checked
  int iret = 0;
  SD_TESTTYPE testType = SD_DOSDCONT;

  iret = BddSDCheckProp(DESpotProj, testType, checkInfo);

  return iret;

}

/**
 * DESCR:   Checks the entire project for proper time behavior
 * PARA:    DESpotProj: an HISC project in DESpot format
 *          SD_ChkInfo: contains output messages and success flags
 * RETURN:  error code 
 * ACCESS:  public
 */
int BddSdCheckPTB(DESpot::DesProject& DESpotProj, SD_ChkInfo&
checkInfo)
{

  int iret = 0;
  SD_TESTTYPE testType = SD_DOPTB;

  iret = BddSDCheckProp(DESpotProj, testType, checkInfo);

  return iret;

}

/**
 * DESCR:   Checks the entire project for S-singular behavior
 * PARA:    DESpotProj: an HISC project in DESpot format
 *          SD_ChkInfo: contains output messages and success flags
 * RETURN:  error code 
 * ACCESS:  public
 */
int BddSdCheckSSingP(DESpot::DesProject& DESpotProj, SD_ChkInfo&
checkInfo)
{

  // note: at moment this is integrated as part of SD cont check
  int iret = 0;
  SD_TESTTYPE testType = SD_DOSSPROHIBB;

  iret = BddSDCheckProp(DESpotProj, testType, checkInfo);

  return iret;

}

/**
 * DESCR:   Checks the entire project for Plant completeness
 * PARA:    DESpotProj: an HISC project in DESpot format
 *          SD_ChkInfo: contains output messages and success flags
 * RETURN:  error code 
 * ACCESS:  public
 */
int BddSdCheckPCmplt(DESpot::DesProject& DESpotProj, SD_ChkInfo&
checkInfo)
{

  // note: at moment this is integrated as part of SD cont check
  int iret = 0;
  SD_TESTTYPE testType = SD_DOPCOMPL;

  iret = BddSDCheckProp(DESpotProj, testType, checkInfo);

  return iret;

}

/**
 * DESCR:   Checks the entire project for activity loop free
 * PARA:    DESpotProj: an HISC project in DESpot format
 *          SD_ChkInfo: contains output messages and success flags
 * RETURN:  error code 
 * ACCESS:  public
 */
int BddSdCheckALF(DESpot::DesProject& DESpotProj, SD_ChkInfo&
checkInfo)
{

  // note: at moment this is integrated as part of SD cont check
  int iret = 0;
  SD_TESTTYPE testType = SD_DOALF;

  iret = BddSDCheckProp(DESpotProj, testType, checkInfo);

  return iret;

}

/**
 * DESCR:   Checks the entire project for nonblocking and untimed
 *          controllability 
 * PARA:    DESpotProj: an HISC project in DESpot format
 *          SD_ChkInfo: contains output messages and success flags
 * RETURN:  error code 
 * ACCESS:  public
 */
int BddSdCheckNBCtrl(DESpot::DesProject& DESpotProj, SD_ChkInfo&
checkInfo)
{

  // note: at moment this is integrated as part of SD cont check
  int iret = 0;
  SD_TESTTYPE testType = SD_DONBandCONT;

  iret = BddSDCheckProp(DESpotProj, testType, checkInfo);

  return iret;

}

/**
 * DESCR:   Checks the entire project for timed
 *          controllability 
 * PARA:    DESpotProj: an HISC project in DESpot format
 *          SD_ChkInfo: contains output messages and success flags
 * RETURN:  error code 
 * ACCESS:  public
 */

/*  This feature not implemented yet

int BddSdCheckTCtrl(DESpot::DesProject& DESpotProj, SD_ChkInfo&
checkInfo)
{

  // note: at moment this is integrated as part of SD cont check
  int iret = 0;
  SD_TESTTYPE testType = SD_DOTDESCONT;

  iret = BddSDCheckProp(DESpotProj, testType, checkInfo);

  return iret;

}

*/

/**
 * DESCR:   Checks the entire project for timed
 *          controllability  and nonblocking
 * PARA:    DESpotProj: an HISC project in DESpot format
 *          SD_ChkInfo: contains output messages and success flags
 * RETURN:  error code 
 * ACCESS:  public
 */

/*  This feature not implemented yet

int BddSdCheckTCtrl(DESpot::DesProject& DESpotProj, SD_ChkInfo&
checkInfo)
{

  // note: at moment this is integrated as part of SD cont check
  int iret = 0;
  SD_TESTTYPE testType = SD_DONBandTDESCONT;

  iret = BddSDCheckProp(DESpotProj, testType, checkInfo);

  return iret;

}

*/




/**
 * DESCR:   Checks the entire project for check  specified in 
 *          param testType, using BddSd
 * PARA:    DESpotProj: an HISC project in DESpot format
 *          testType: specifies what sort of checks to do
 *          SD_ChkInfo: contains output messages and success flags
 * RETURN:  error code 
 * ACCESS:  public
 */

 int BddSDCheckProp(DESpot::DesProject& DESpotProj, SD_TESTTYPE testType,
		       SD_ChkInfo& checkInfo)
 {

  int iret = 0;
  string errmsg;
  //DESpot::CounterExampleAlgo::isfirsterror=true;
  
  
  bool isTimed = true;

  // all tests types after SD_DONBandCONT are timed tests.
  if (testType <= SD_DONBandCONT) 
    {
      isTimed = false;
    }

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

  if (iret < 0)
    {
      cout << errmsg << endl;
      cout << "Press any key to continue...";
      iret = 0;
      errmsg[0] = '\0';
    }
  
  HISC_SUPERINFO superinfo;
  HISC_TRACETYPE tracetype = HISC_NO_TRACE;
  int computetime = 0;


  iVerbLevel = 0;

  superinfo.statesize = -1;
  superinfo.nodesize = -1;
  superinfo.time = 0;

  iret = verify_low(tracetype, errmsg, &superinfo, testType,checkInfo);
  cout   << endl << "Return value from verify option is: ("<< iret << ") "  << endl;

  // Probably won't need next line
  //QString ProjName = QString::fromStdWString(DESpotProj.getName());

  checkInfo.m_succStr += "State size: ";
  if (superinfo.statesize >= 0)
    {
      checkInfo.m_succStr += QString::number(superinfo.statesize) + ". <br>";
    }
  else
    {
      checkInfo.m_succStr += "-1. <br>";
    }

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


  //output to console
  if (iret == 0)
    cout << "This system 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 << endl ;

  // computetime is not currently being used.
  computetime += superinfo.time;

  if (iret < 0)
    {
      //verification has failed

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

      // how do we detect when only S-singular prohibitable behavior
      //      has failed?  Hamid figure out?

      // Hamid: do errors HISC_INTERNAL_ERR_SUBEVENT  and
      // HISC_VERI_LOW_ZERO_LB  represent SD cont failed or some other
      // sort of error?  

      // I think HISC_VERI_LOW_ZERO_LB  may represent S-Singular
      // prohib - test this!  Hamid? know if so?

      // for now, I am going to assume they imply sd cont fails
      // need to test this though

      switch(iret)
	{
	case HISC_VERI_LOW_PCOMPLT:  // plant completeness
	  testFailed = true;
	  checkInfo.m_PCompltChkFail = true;
	  break;
	case HISC_VERI_LOW_UNCON:  //cont fails
	  testFailed = true;
	  checkInfo.m_CtrlChkFail = true;
	  checkInfo.m_SDCtrlChkFail = true;
	  break;
	case HISC_VERI_LOW_TDESUNCON:  //timed cont fails
	  testFailed = true;
	  //	  checkInfo.m_TDESCtrlChkFail = true;
	  checkInfo.m_SDCtrlChkFail = true;
	  break;
	case HISC_VERI_LOW_ALF:  //ALF failed
	  testFailed = true;
	  checkInfo.m_ALFChkFail = true;
	  break;
	case HISC_VERI_LOW_BLOCKING:  //nonblocking failed
	  testFailed = true;
	  checkInfo.m_NBChkFail = true;
	  break;
	case HISC_VERI_LOW_PTB:  //PTB failed
	  testFailed = true;
	  checkInfo.m_PropTimedBChkFail= true;
	  break;
	case HISC_VERI_LOW_SD_II: //  SD cont pnt II failed
	  testFailed = true;
	  checkInfo.m_SDCtrlChkFail = true; 
	  break; 
	case HISC_VERI_LOW_SD_III_1: // SD cont pnt III.1 failed 
	  testFailed = true;
	  checkInfo.m_SDCtrlChkFail = true; 
	  break;
	case HISC_VERI_LOW_SD_III_2: // SD cont pnt III.2 failed 
	  testFailed = true;
	  checkInfo.m_SDCtrlChkFail = true; 
	  break;
	case HISC_VERI_LOW_SD_IV: // SD cont pnt IV failed 
	  testFailed = true;
	  checkInfo.m_SDCtrlChkFail = true; 
	  break;
	  //	case HISC_INTERNAL_ERR_SUBEVENT: 
          // does this actuall imply SD cont failed?
	  // testFailed = true;
	  // checkInfo.m_SDCtrlChkFail = true; 
	  // break;
	case HISC_VERI_LOW_ZERO_LB: 
          // I think this implies S-Singular prohib?
	  testFailed = true;
	  checkInfo.m_SSingPhibBChkFail = true; 
	  break;
	default:
	  testFailed = false;
	  break;
	}

      if (testFailed) 
	{
	  checkInfo.m_chkPassed = false;
	  QString tmpErr = QString::fromStdString(errmsg);
	  
	  //error prossing here
	  
	  // 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);
	    }
	  
	  

	  // do I need this step?  Test.
	  checkInfo.m_errStr += "Verification failed.<br><br>";
	  checkInfo.m_errStr += tmpErr; 
	  
	  // closing things up.
	  int  tmp;
	  tmp = close_prj(errmsg);
	  close_hisc();
	  return iret;
	}
      else
	{
	  QString theMessage = "Verification failed.\n\n";
	  theMessage += QString::fromStdString(errmsg);
	  // closing things up.
	  iret = close_prj(errmsg);
	  close_hisc();
	  throw theMessage.toStdWString();
	}
    }
  
  //  cout << "Total computing time:" << computetime << " seconds."
  //     << endl;y

  // closing things up.
  iret = close_prj(errmsg);
  close_hisc();

  checkInfo.m_chkPassed = true;
  
  return 0;

 }




  // this function no longer used


  /*
 * DESCR:   Main entry function for BddSd
 * PARA:    DESpotProj: a flat project in DESpot format
 * RETURN:  error code 
 * ACCESS:  public
 */ 

  /*
int BddSdMain(DESpot::DesProject& DESpotProj)
{

  int iret = 0;
  string errmsg;
  
  // gets passed in later on 
  SD_TESTTYPE testType = SD_DOALL;

  
  // in future, this will depend on the algorithm to be checked
  bool isTimed = true;
  
  //    iret = load_prj(prjfile, errmsg);
  iret = load_prj(DESpotProj, errmsg, isTimed);
  if ((iret < 0) && (iret > -10000))
    {
      QString theMessage =QString::fromStdString(errmsg);
      iret = close_prj(errmsg);
      close_hisc();
      throw theMessage.toStdWString();
    }

  if (iret < 0)
    {
      cout << errmsg << endl;
      cout << "Press any key to continue...";
      iret = 0;
      errmsg[0] = '\0';
    }
  
  HISC_SUPERINFO superinfo;
  HISC_TRACETYPE tracetype = HISC_NO_TRACE;
  int computetime = 0;


  iVerbLevel = 0;

  superinfo.statesize = -1;
  superinfo.nodesize = -1;
  superinfo.time = 0;

  iret = verify_low(tracetype, errmsg, &superinfo, testType);
  cout   << endl << "Return value from verify option is: ("<< iret << ") "  << endl;

  if (iret == 0)
    cout << "This system 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 << endl ;

  // computetime is not currently being used.
  computetime += superinfo.time;

  if (iret < 0)
    {
      cout << errmsg << endl;
      iret = 0;
      errmsg[0] = '\0';
    }
  
  //  cout << "Total computing time:" << computetime << " seconds."
  //     << endl;y

  // closing things up.
  iret = close_prj(errmsg);
  close_hisc();
  
  return 0;
}

  */


/*  It should now be possible to delete the following code.

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] = 'F';
        allowed_choice[5] = 'f';
        allowed_choice[6] = 'l';
        allowed_choice[7] = 'L';
        numofchoice = 8;
        cout << "  L - Low Level verification                     " << 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_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 BDDSD
