/*************************************************************************
  FILE:  BddSd.cpp
  DESCR: C/C++ interface for the verification of Sampled-Data algorithms
  AUTH:  Raoguang Song, Yu Wang
  DATE:  (C) Jan, 2006, 2009
*************************************************************************/
#include "BddSd.h"
#include <string>
#include <fstream>
#include "BddSdErrmsg.h"
#include <cassert>
#include "BddSdSub.h"
#include "BddSdLowSub.h"
#ifdef _WIN32
#include <winsock.h>
#include<time.h>
#include <sys/types.h>
#else
#include <sys/time.h>
#endif
#include "BddSdPubfunc.h"

#include "DesProject.h"


using namespace std;

namespace BDDSD
{

#define MAX_PATH2 256

CSub *pSub = NULL;

/**
 * DESCR:  Load a HISC project
 * PARA:   DESpotProj:  DESpot flat project
 *         errmsg: returned errmsg (output)
 * RETURN: 0: sucess  < 0: fail
 * */
  int load_prj(DESpot::DesProject& DESpotProj, string & errmsg, bool isTimed)
{
    int iRet = 0;


    char prjfile[MAX_PATH2];

    // prjfile is no longer used, so just creating default string
    prjfile[0] = 'a';
    prjfile[1] = '\0';

    pSub = new CLowSub(prjfile);

    iRet = pSub->LoadSub(DESpotProj, isTimed);

    errmsg = pSub->GetErrMsg();
    if (pSub->GetErrCode() < 0)
    {
        if (pSub->GetErrCode() > HISC_WARN_BLOCKEVENTS) //error happened
        {
            delete pSub;
            pSub = NULL;
        }
        //else only a warning
    }
    return iRet;
}

/**
 * DESCR:   close opened HISC project
 * PARA:    errmsg: returned errmsg (output)
 * RETURN:  0: sucess  < 0: fail
 * */
int close_prj(string & errmsg)
{
    int iRet = 0;

    if (NULL != pSub)
    {
        errmsg = pSub->GetErrMsg();
        iRet = pSub->GetErrCode();
        if (pSub->GetErrCode() < 0)
        {
            delete pSub;
            pSub = NULL;
        }
    }
    return iRet;
}

/**
 * DESCR:  clear the HISC enviorment
 * PARA:   none
 * RETURN: 0
 * */
int close_hisc()
{
    if (pSub != NULL)
    {
        delete pSub;
        pSub = NULL;
    }
    return 0;
}

/**
 * DESCR:   Save the project in the memory to a text file, just for verifying
 *          the loaded project.
 * PARA:    filename: where to save the text file (input)
 *          errmsg: returned errmsg (output)
 * RETURN:  0: sucess  < 0: fail
 * */
int print_prj(string filename, string & errmsg)
{
    int iRet = 0;
    assert(!filename.empty());
    assert(!errmsg.empty());

    ofstream fout;
    try
    {
        fout.open(filename.data());
        if (!fout)
            throw -1;

        if (pSub->PrintSubAll(fout) < 0)
            throw -1;
        fout.close();
    }
    catch(...)
    {
        if (fout.is_open())
            fout.close();
        pSub->SetErr(filename + ":Unable to create the print file.",
                HISC_BAD_PRINT_FILE);
        return -1;
    }

    return 0;

    errmsg = pSub->GetErrMsg();

    iRet = pSub->GetErrCode();

    pSub->ClearErr();

    return iRet;
}

/**
 * DESCR:   verify low level
 * PARA:    showtrace: show a trace to the bad state (not implemented) (input)
 *          subname: low level name ("all" means all the low levels) (input)
 *          errmsg: returned errmsg (output)
 *          pinfo: returned system infomation (output)
 *          pnextlow: next low level sub index(initially,it must be 0, mainly
 *                    used for "all") (input)
 *          saveproduct: whether to save syn-product (input)
 *          savepath: where to save syn-product (input)
 * RETURN: 0: successsful < 0: error happened (See errmsg.h)
 * */
int verify_low(
        HISC_TRACETYPE showtrace,
        string & errmsg,
        HISC_SUPERINFO *pinfo,
	SD_TESTTYPE testType,SD_ChkInfo& checkInfo)
{
    assert(pinfo != NULL);

    int iRet = 0;

        time_t tstart;
        time(&tstart);

        if (pSub->VeriSub(showtrace, *pinfo, testType,checkInfo) < 0)
        {
            errmsg = pSub->GetErrMsg();
            iRet = pSub->GetErrCode();
            pSub->ClearErr();
        }

        time_t tend;
        time(&tend);
        pinfo->time = tend - tstart;

    return iRet;
}

} //end of namespace BDDSD
