/*************************************************************************
  FILE:  BddHisc.h
  DESCR: C/C++ interface for the HISC synthesis and verifcation package
  AUTH:  Raoguang Song
  Supervisor: Dr. Ryan Leduc
  DATE:  (C) Jan, 2006
*************************************************************************/

#include <string>
#include "DesProject.h"

#ifndef _BDDHISC_H_
#define _BDDHISC_H_

namespace BDDHISC
{

/**
 * DESCR:   Initialize the HISC enviorment
 * PARA:    None
 * RETURN:  0: sucess  < 0: fail
 * */
int init_hisc();  

/**
 * 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,  char *errmsg);

/**
 * DESCR:   close opened HISC project
 * PARA:    errmsg: returned errmsg (output)
 * RETURN:  0: sucess  < 0: fail
 * */
int close_prj(char *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(const char *filename, char *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;


/**
 * HISC_SAVESUPER_NONE: Not to save the synthesized supervisor
 * HISC_SAVESUPER_BDD: Save synthesized BDD control predicates
 * HISC_SAVESUPER_AUTOMATA: Save synthesized automata-based supervisor
 * HISC_SAVESUPER_BOTH: Save both
 * */
enum HISC_SAVESUPERTYPE {HISC_SAVESUPER_NONE = 0, HISC_SAVESUPER_BDD = 1, 
    HISC_SAVESUPER_AUTOMATA = 2, HISC_SAVESUPER_BOTH = 3};
    
/**
 * 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 save the syn-product for a verified subsystem or not
 * */
enum HISC_SAVEPRODUCTTYPE{HISC_NOTSAVEPRODUCT = 0, HISC_SAVEPRODUCT = 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. HISC_DOLWNONBLK = do
 * lw nonblock check, HISC_DOLWCONT = do lw cont check, HISC_DOALL =
 * check all thrre conditions, HISC_DOINTFCHK = just check interafce defn
 * */
 enum HISC_TESTTYPE{HISC_DOLWNONBLK = 0, HISC_DOLWCONT=1,
                    HISC_DOICONSIS=2, HISC_DOALL=3, HISC_DOINTFCHK=4};


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

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

/**
 * 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)
 * RETURN:  successsful < 0: error happened (See errmsg.h)
 * */ 
 class Hisc_ChkInfo;
int verify_high(
            HISC_TRACETYPE showtrace,               
            char *errmsg,                           
            HISC_SUPERINFO *pinfo,                  
            const HISC_SAVEPRODUCTTYPE saveproduct, 
            const char *savepath,
            const HISC_TESTTYPE testType,
	    std::string &highName,
	    Hisc_ChkInfo& checkInfo);

/**
 * 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, 
        char *subname,            
        char *errmsg,             
        HISC_SUPERINFO *pinfo,    
        int* pnextlow,            
        const HISC_SAVEPRODUCTTYPE saveproduct, 
        const char *savepath,
	const HISC_TESTTYPE testType, Hisc_ChkInfo& checkInfo);                  




} //end of namespace BDDHISC


#endif 

