/*************************************************************************
  FILE:  BddHisc.cpp
  DESCR: Implementation for C/C++ interface for the HISC synthesis and 
         verifcation package
  AUTH:  Raoguang Song
  Supervisor: Dr. Ryan Leduc
  DATE:  (C) Jan, 2006
*************************************************************************/
#include "BddHisc.h"
#include "BddHiscProject.h"
#include <string>
#include <fstream>
#include "BddHiscErrmsg.h"
#include <cassert>
#include "BddHiscSub.h"
#include "BddHiscLowSub.h"
#include "BddHiscHighSub.h"
#ifdef _WIN32
#include <winsock.h>
#include<time.h>
#include <sys/types.h>
#else
#include <sys/time.h>
#endif
#include <cstring>

#include "DesProject.h"


using namespace std;


namespace BDDHISC
{

CProject *pPrj = NULL;

/**
 * DESCR:   Initialize the HISC enviorment
 * PARA:    None
 * RETURN:  0: sucess  < 0: fail
 * */
int init_hisc()
{
    pPrj = new CProject();
    if (pPrj == NULL)
        return HISC_NOT_ENOUGH_MEMORY;
    return 0;
}

/**
 * DESCR:  Load a HISC project
 * PARA:   prjfile: HISC project file name (input)
 *         errmsg: returned errmsg (output)
 * RETURN: 0: sucess  < 0: fail
 * */
int load_prj(DESpot::DesProject& DESpotProj,  char *errmsg)
{

    int iRet = 0;
    
    assert(errmsg != NULL);
    
    pPrj->InitPrj();    
    pPrj->LoadPrj(DESpotProj);
    
    strcpy(errmsg, pPrj->GetErrMsg());
    iRet = pPrj->GetErrCode();
    if (pPrj->GetErrCode() < 0)
    {
        if (pPrj->GetErrCode() > HISC_WARN_BLOCKEVENTS) //error happened
            pPrj->ClearPrj();
        //else only a warning 
    }
    return iRet;
}

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

    pPrj->ClearPrj();
    pPrj->InitPrj();

    strcpy(errmsg, pPrj->GetErrMsg());
    iRet = pPrj->GetErrCode();
    if (pPrj->GetErrCode() < 0)
    {
        pPrj->ClearPrj();
    }
    return iRet;
}

/**
 * DESCR:  clear the HISC enviorment
 * PARA:   none
 * RETURN: 0
 * */
int close_hisc()
{
    delete pPrj;
    pPrj = 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(const char *filename, char *errmsg)
{
    int iRet = 0;
    assert(filename != NULL);
    assert(errmsg != NULL);

    pPrj->PrintPrjAll(filename);

    strcpy(errmsg, pPrj->GetErrMsg());
    iRet = pPrj->GetErrCode();
    
    pPrj->ClearErr();
    
    return iRet;
}

/**
 * DESCR:   Synthesize a supervisor for a specified low level
 * PARA:    computemethod: computemethod,synthesize on reachable states or 
 *                         on coreachable states (input).
 *          subname: low level name ("all!" means all the low levels) (input).
 *          errmsg:  returned errmsg (output)
 *          pinfo:   returned supervisor info (output)
 *          pnextlow: next low level sub index(initially,it must be 0, mainly 
 *                    used for "all!")(input)
 *          savetype:  how to save the supervisors (input)
 *          savepath:  where to save the supervisors(input)
 * RETURN:  0: successsful < 0: error happened (See errmsg.h)
 * */ 
int syn_lowsuper(HISC_COMPUTEMETHOD computemethod,  
                    char *subname, 
                    char *errmsg,                      
                    HISC_SUPERINFO *pinfo, 
                    int* pnextlow,                     
                    const HISC_SAVESUPERTYPE savetype, 
                    const char *savepath)
{
    int iRet = 0;
    
    assert(subname != NULL);
    assert(errmsg != NULL);
    assert(pinfo != NULL);
    assert(pnextlow != NULL);
    assert(*pnextlow >= 0);
    assert((savetype == HISC_SAVESUPER_NONE) || savepath != NULL); 
    
    string sSubName = subname;
    
    if (sSubName == "all!" || *pnextlow > 0)
    {
        (*pnextlow)++;
        if (*pnextlow <= pPrj->GetNumofLows())
        {
            sSubName = pPrj->GetSub(*pnextlow)->GetSubName();
            strcpy(subname, sSubName.data());
        }
        
        if (*pnextlow == pPrj->GetNumofLows())
            *pnextlow = -1;
    }

    int i = 0;
    for (i = 0; i < pPrj->GetNumofLows(); i++)
    {
        if (pPrj->GetSub(i + 1)->GetSubName() == sSubName)
            break;
    }
    if (i < pPrj->GetNumofLows())
    {
        string sSavePath;
        if (savetype != HISC_SAVESUPER_NONE)
            sSavePath = savepath;

        time_t tstart;
        time(&tstart);

        if (pPrj->GetSub(i + 1)->SynSuper(computemethod, *pinfo, savetype, 
            sSavePath) < 0)
        {
            strcpy(errmsg, pPrj->GetErrMsg());
            iRet = pPrj->GetErrCode();
            pPrj->ClearErr();
        }
        
        time_t tend;
        time(&tend);
        pinfo->time = tend - tstart;
        
    }
    else
    {
        string sErr = "Unable to find the low-level ";
        sErr += sSubName;

        strcpy(errmsg, sErr.data());
        iRet = HISC_NONEXISTED_LEVEL_NAME;
    }
    return iRet;
}

/**
 * DESCR:   synthesize high level supervisor
 * PARA:    computemethod: synthesize on reachable states or on coreachable 
 *                          states (input)
 *          errmsg: returned errmsg (output)
 *          pinfo: returned supervisor infomation(output)
 *          savetype: how to save the supervisors (input)
 *          savepath: where to save the supervisor (input)
 * RETURN: 0: successsful < 0: error happened (See errmsg.h)
 */
int syn_highsuper(HISC_COMPUTEMETHOD computemethod, 
                    char *errmsg,                    
                    HISC_SUPERINFO *pinfo,           
                    const HISC_SAVESUPERTYPE savetype,
                    const char *savepath)
{
    assert(errmsg != NULL);
    assert(pinfo != NULL);
    assert((savetype == HISC_SAVESUPER_NONE) || savepath != NULL); 

    int iRet = 0;
    
    string sSavePath;
    if (savetype != HISC_SAVESUPER_NONE)
        sSavePath = savepath;
    
    time_t tstart;
    time(&tstart);

    pPrj->GetSub(0)->SynSuper(computemethod, *pinfo, savetype, sSavePath);
    strcpy(errmsg, pPrj->GetErrMsg());
    iRet = pPrj->GetErrCode();
    pPrj->ClearErr();

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

    return iRet;
}

/**
 * DESCR:   verify high level
 * PARA:    showtrace: show a trace to the bad state (not implemented)(input)
 *          errmsg: returned errmsg (output)
 *          pinfo: returned system infomation (output)
 *          saveproduct: whether to save the syn-product (input)
 *          savepath: where to save the syn-product (input)
 *          testType: specifies which tests should be run on high-level
 * RETURN:  successsful < 0: error happened (See errmsg.h)
 * */ 
int verify_high(
            HISC_TRACETYPE showtrace,               
            char *errmsg,                           
            HISC_SUPERINFO *pinfo,                  
            const HISC_SAVEPRODUCTTYPE saveproduct, 
            const char *savepath,
			const HISC_TESTTYPE testType,
	    	string &highName,			Hisc_ChkInfo& checkInfo){
    assert(errmsg != NULL);
    assert(pinfo != NULL);
    assert((saveproduct == HISC_NOTSAVEPRODUCT) || savepath != NULL); 

    // return name of the high-level
    highName = (pPrj->GetSub(0))->GetSubName();

    int iRet = 0;
    
    string sSavePath;
    if (saveproduct != HISC_NOTSAVEPRODUCT)
        sSavePath = savepath;
    
    time_t tstart;
    time(&tstart);

    if (pPrj->GetSub(0)->VeriSub(showtrace, *pinfo, saveproduct,
    sSavePath, testType,checkInfo) < 0)
    {
        strcpy(errmsg, pPrj->GetErrMsg());
        iRet = pPrj->GetErrCode();
    }
    pPrj->ClearErr();

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

    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)
 *          testType: specifies which tests should be run on low-level
 * RETURN: 0: successsful < 0: error happened (See errmsg.h)
 * */ 
int verify_low(
        HISC_TRACETYPE showtrace, 
        char *subname,            
        char *errmsg,             
        HISC_SUPERINFO *pinfo,    
        int* pnextlow,            
        const HISC_SAVEPRODUCTTYPE saveproduct, 
        const char *savepath, 
	const HISC_TESTTYPE testType, Hisc_ChkInfo& checkInfo)
{
    assert(subname != NULL);
    assert(errmsg != NULL);
    assert(pinfo != NULL);
    assert(pnextlow != NULL);
    assert(*pnextlow >= 0);
    assert((saveproduct == HISC_NOTSAVEPRODUCT) || savepath != NULL); 

    int iRet = 0;
    
    string sSubName = subname;
    
    if (sSubName == "all!" || *pnextlow > 0)
    {
        (*pnextlow)++;
        if (*pnextlow <= pPrj->GetNumofLows())
        {
            sSubName = pPrj->GetSub(*pnextlow)->GetSubName();
            strcpy(subname, sSubName.data());
        }
        
        if (*pnextlow == pPrj->GetNumofLows())
            *pnextlow = -1;
    }

    int i = 0;
    for (i = 0; i < pPrj->GetNumofLows(); i++)
    {
        if (pPrj->GetSub(i + 1)->GetSubName() == sSubName)
            break;
    }
    
    if (i < pPrj->GetNumofLows())
    {
        string sSavePath;
        if (saveproduct != HISC_NOTSAVEPRODUCT)
            sSavePath = savepath;
            
        time_t tstart;
        time(&tstart);

        if (pPrj->GetSub(i + 1)->VeriSub(showtrace, *pinfo, saveproduct, 
					 sSavePath, testType,checkInfo) < 0)
        {
            strcpy(errmsg, pPrj->GetErrMsg());
            iRet = pPrj->GetErrCode();
	    std::cout << "error code is " << iRet << ".\n";
            pPrj->ClearErr();
        }

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

    }
    else
    {
        string sErr = "Unable to find the low-level ";
        sErr += sSubName;
        strcpy(errmsg, sErr.data());
        iRet = HISC_NONEXISTED_LEVEL_NAME;
    }
    return iRet;
}



} //end of namespace BDDHISC
