/*************************************************************************
  FILE:  BddSd.h
  DESCR: C/C++ interface for the verification of Sampled-Data algorithms
  AUTH:  Raoguang Song, Yu Wang 
  DATE:  (C) Jan, 2006, 2009
*************************************************************************/

#ifndef _BDDSD_H_
#define _BDDSD_H_



#include <string>

#include "DesProject.h"

namespace BDDSD
{

/**
 * DESCR:   Clear the HISC enviorment
 * PARA:    None
 * RETURN:  0
 * */
int close_hisc();

/**
 * 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, std::string & errmsg, bool isTimed);

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

/**
 * 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(std::string filename, std::string & errmsg);

/**
 * A structure for storing computing result information
 * */
typedef struct Hisc_SuperInfo
{
    double statesize;   /*state size*/
    int nodesize;       /*bdd node size*/
    int time;           /*computing time (seconds)*/
}HISC_SUPERINFO;

/**
 * To show a path from the initial state to one bad state or not
 * Currently HISC_SHOW_TRACE is only for telling if a blocking state is
 * deadlock or livelock
 * */
enum HISC_TRACETYPE {HISC_NO_TRACE = 0, HISC_SHOW_TRACE = 1};

/**
 * To synthesize on reachable statespace or not
 * */
enum HISC_COMPUTEMETHOD{HISC_ONCOREACHABLE = 0, HISC_ONREACHABLE = 1};


/**
 * To specify what type of operation to perform. SD_DONONBLK = do a
 * nonblocking test, SD_DOCONT = do an untimed controllability test, 
 * SD_DONBandCONT = do a nonblocking and untimed controllability test,
 * SD_DOSDCONT = do an SD controllability test, SD_DOPTB = do a proper
 * time behavior test on the plant, SD_DOSSPROHIBB = do an S-singular
 * prohibitable behavior test, SD_DOPCOMPL = do a plant completeness
 * test, SD_DOALF = do an ALF test, SD_DOTDESCONT = do a TDES
 * controllability test, SD_DONBandTDESCONT= do a nonblocking and
 * TDES controllability test, SD_DOALL = do all of the above
 * tests
 * */
 enum SD_TESTTYPE{SD_DONONBLK = 0, SD_DOCONT=1,  SD_DONBandCONT=2,
                    SD_DOSDCONT=3, SD_DOPTB=4, SD_DOSSPROHIBB=5,
		  SD_DOPCOMPL=6, SD_DOALF=7, SD_DOTDESCONT=8,
		  SD_DONBandTDESCONT=9, SD_DOALL=10};


/**
 * 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,
        std::string & errmsg,
        HISC_SUPERINFO *pinfo,
	SD_TESTTYPE testType,SD_ChkInfo& checkInfo);

} //end of namespace BDDSD

#endif  // _BDDSD_H_

