NuSMV/code/nusmv/core/bmc/bmc.h File Reference

#include "nusmv/core/bmc/bmcBmc.h"
#include "nusmv/core/bmc/bmcPkg.h"
#include "nusmv/core/bmc/bmcGen.h"
#include "nusmv/core/bmc/bmcDump.h"
#include "nusmv/core/bmc/bmcTableau.h"
#include "nusmv/core/bmc/bmcModel.h"
#include "nusmv/core/bmc/bmcConv.h"
#include "nusmv/core/bmc/bmcCheck.h"
#include "nusmv/core/bmc/bmcUtils.h"

Go to the source code of this file.

Defines

#define BMC_DIMACS_FILENAME   "bmc_dimacs_filename"
#define BMC_FORCE_PLTL_TABLEAU   "bmc_force_pltl_tableau"
#define BMC_HAS_TO_SOLVE   true
#define BMC_INC_INVAR_ALG_DUAL   "dual"
#define BMC_INC_INVAR_ALG_FALSIFICATION   "falsification"
#define BMC_INC_INVAR_ALG_INTERP_SEQ   "interp_seq"
#define BMC_INC_INVAR_ALG_INTERPOLANTS   "interpolants"
#define BMC_INC_INVAR_ALG_ZIGZAG   "zigzag"
#define BMC_INVAR_ALG   "bmc_invar_alg"
#define BMC_INVAR_ALG_CLASSIC   "classic"
 The names for INVAR solving algorithms (incremental and non-incremental).
#define BMC_INVAR_ALG_EEN_SORENSSON   "een-sorensson"
#define BMC_INVAR_ALG_FALSIFICATION   "falsification"
#define BMC_INVAR_BACKWARD   "backward"
 The names for INVAR closure strategies.
#define BMC_INVAR_DIMACS_FILENAME   "bmc_invar_dimacs_filename"
#define BMC_INVAR_FORWARD   "forward"
#define BMC_MODE   "bmc_mode"
#define BMC_OPT_INITIALIZED   "__bmc_opt_initialized__"
 The header file for the bmc package.
#define BMC_OPTIMIZED_TABLEAU   "bmc_optimized_tableau"
#define BMC_PB_LENGTH   "bmc_length"
#define BMC_PB_LOOP   "bmc_loopback"
#define BMC_SBMC_CACHE_OPT   "bmc_sbmc_cache_opt"
#define BMC_SBMC_GF_FG_OPT   "bmc_sbmc_gf_fg_opt"
#define BMC_SBMC_IL_OPT   "bmc_sbmc_il_opt"
#define BMC_WATCHDOG_NAME   "bmc_watchdog"
 Name of the watchdog timer used in the bmc algorithm.

Enumerations

enum  bmc_invar_algorithm {
  ALG_UNDEFINED, ALG_CLASSIC, ALG_EEN_SORENSSON, ALG_FALSIFICATION,
  ALG_DUAL, ALG_ZIGZAG, ALG_INTERP_SEQ, ALG_INTERPOLANTS
}
 

BMC invariant checking algorithms.

More...

Functions

char * get_bmc_dimacs_filename (OptsHandler_ptr)
const char * get_bmc_invar_alg (OptsHandler_ptr)
char * get_bmc_invar_dimacs_filename (OptsHandler_ptr)
int get_bmc_pb_length (OptsHandler_ptr)
const char * get_bmc_pb_loop (OptsHandler_ptr)
boolean opt_bmc_force_pltl_tableau (OptsHandler_ptr)
boolean opt_bmc_mode (OptsHandler_ptr)
boolean opt_bmc_optimized_tableau (OptsHandler_ptr)
boolean opt_bmc_sbmc_cache (OptsHandler_ptr opt)
boolean opt_bmc_sbmc_gf_fg_opt (OptsHandler_ptr opt)
boolean opt_bmc_sbmc_il_opt (OptsHandler_ptr opt)
void set_bmc_dimacs_filename (OptsHandler_ptr, char *)
void set_bmc_force_pltl_tableau (OptsHandler_ptr)
void set_bmc_invar_alg (OptsHandler_ptr opt, const char *loop)
void set_bmc_invar_dimacs_filename (OptsHandler_ptr, char *)
void set_bmc_mode (OptsHandler_ptr)
void set_bmc_optimized_tableau (OptsHandler_ptr)
void set_bmc_pb_length (OptsHandler_ptr opt, const int k)
void set_bmc_pb_loop (OptsHandler_ptr opt, const char *loop)
void set_bmc_sbmc_cache (OptsHandler_ptr opt)
void set_bmc_sbmc_gf_fg_opt (OptsHandler_ptr opt)
void set_bmc_sbmc_il_opt (OptsHandler_ptr opt)
void unset_bmc_force_pltl_tableau (OptsHandler_ptr)
void unset_bmc_mode (OptsHandler_ptr)
void unset_bmc_optimized_tableau (OptsHandler_ptr)
void unset_bmc_sbmc_cache (OptsHandler_ptr opt)
void unset_bmc_sbmc_gf_fg_opt (OptsHandler_ptr opt)
void unset_bmc_sbmc_il_opt (OptsHandler_ptr opt)

Define Documentation

#define BMC_DIMACS_FILENAME   "bmc_dimacs_filename"
Todo:
Missing synopsis
Todo:
Missing description
#define BMC_FORCE_PLTL_TABLEAU   "bmc_force_pltl_tableau"
Todo:
Missing synopsis
Todo:
Missing description
#define BMC_HAS_TO_SOLVE   true
Todo:
Missing synopsis
Todo:
Missing description
#define BMC_INC_INVAR_ALG_DUAL   "dual"
Todo:
Missing synopsis
Todo:
Missing description
#define BMC_INC_INVAR_ALG_FALSIFICATION   "falsification"
Todo:
Missing synopsis
Todo:
Missing description
#define BMC_INC_INVAR_ALG_INTERP_SEQ   "interp_seq"
Todo:
Missing synopsis
Todo:
Missing description
#define BMC_INC_INVAR_ALG_INTERPOLANTS   "interpolants"
Todo:
Missing synopsis
Todo:
Missing description
#define BMC_INC_INVAR_ALG_ZIGZAG   "zigzag"
Todo:
Missing synopsis
Todo:
Missing description
#define BMC_INVAR_ALG   "bmc_invar_alg"
Todo:
Missing synopsis
Todo:
Missing description
#define BMC_INVAR_ALG_CLASSIC   "classic"

The names for INVAR solving algorithms (incremental and non-incremental).

#define BMC_INVAR_ALG_EEN_SORENSSON   "een-sorensson"
Todo:
Missing synopsis
Todo:
Missing description
#define BMC_INVAR_ALG_FALSIFICATION   "falsification"
Todo:
Missing synopsis
Todo:
Missing description
#define BMC_INVAR_BACKWARD   "backward"

The names for INVAR closure strategies.

Currently this applies to DUAL algorithm only

#define BMC_INVAR_DIMACS_FILENAME   "bmc_invar_dimacs_filename"
Todo:
Missing synopsis
Todo:
Missing description
#define BMC_INVAR_FORWARD   "forward"
Todo:
Missing synopsis
Todo:
Missing description
#define BMC_MODE   "bmc_mode"
Todo:
Missing synopsis
Todo:
Missing description
#define BMC_OPT_INITIALIZED   "__bmc_opt_initialized__"

The header file for the bmc package.

Author:
Roberto Cavada
Todo:
: Missing description
Todo:
Missing synopsis
Todo:
Missing description
#define BMC_OPTIMIZED_TABLEAU   "bmc_optimized_tableau"
Todo:
Missing synopsis
Todo:
Missing description
#define BMC_PB_LENGTH   "bmc_length"
Todo:
Missing synopsis
Todo:
Missing description
#define BMC_PB_LOOP   "bmc_loopback"
Todo:
Missing synopsis
Todo:
Missing description
#define BMC_SBMC_CACHE_OPT   "bmc_sbmc_cache_opt"
Todo:
Missing synopsis
Todo:
Missing description
#define BMC_SBMC_GF_FG_OPT   "bmc_sbmc_gf_fg_opt"
Todo:
Missing synopsis
Todo:
Missing description
#define BMC_SBMC_IL_OPT   "bmc_sbmc_il_opt"
Todo:
Missing synopsis
Todo:
Missing description
#define BMC_WATCHDOG_NAME   "bmc_watchdog"

Name of the watchdog timer used in the bmc algorithm.

Name of the watchdog timer used in the bmc algorithm


Enumeration Type Documentation

BMC invariant checking algorithms.

optional

See also:
optional
Enumerator:
ALG_UNDEFINED 
ALG_CLASSIC 
ALG_EEN_SORENSSON 
ALG_FALSIFICATION 
ALG_DUAL 
ALG_ZIGZAG 
ALG_INTERP_SEQ 
ALG_INTERPOLANTS 

Function Documentation

char* get_bmc_dimacs_filename ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
const char* get_bmc_invar_alg ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
char* get_bmc_invar_dimacs_filename ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
int get_bmc_pb_length ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
const char* get_bmc_pb_loop ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_bmc_force_pltl_tableau ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_bmc_mode ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_bmc_optimized_tableau ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_bmc_sbmc_cache ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_bmc_sbmc_gf_fg_opt ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
boolean opt_bmc_sbmc_il_opt ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_bmc_dimacs_filename ( OptsHandler_ptr  ,
char *   
)
Todo:
Missing synopsis
Todo:
Missing description
void set_bmc_force_pltl_tableau ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_bmc_invar_alg ( OptsHandler_ptr  opt,
const char *  loop 
)
Todo:
Missing synopsis
Todo:
Missing description
void set_bmc_invar_dimacs_filename ( OptsHandler_ptr  ,
char *   
)
Todo:
Missing synopsis
Todo:
Missing description
void set_bmc_mode ( OptsHandler_ptr   ) 

AutomaticStart

Todo:
Missing synopsis
Todo:
Missing description
void set_bmc_optimized_tableau ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_bmc_pb_length ( OptsHandler_ptr  opt,
const int  k 
)
Todo:
Missing synopsis
Todo:
Missing description
void set_bmc_pb_loop ( OptsHandler_ptr  opt,
const char *  loop 
)
Todo:
Missing synopsis
Todo:
Missing description
void set_bmc_sbmc_cache ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_bmc_sbmc_gf_fg_opt ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void set_bmc_sbmc_il_opt ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_bmc_force_pltl_tableau ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_bmc_mode ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_bmc_optimized_tableau ( OptsHandler_ptr   ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_bmc_sbmc_cache ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_bmc_sbmc_gf_fg_opt ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
void unset_bmc_sbmc_il_opt ( OptsHandler_ptr  opt  ) 
Todo:
Missing synopsis
Todo:
Missing description
 All Data Structures Files Functions Variables Typedefs Enumerations Enumerator Defines

Generated on 14 Oct 2015 for NuSMV Developers Manual by  doxygen 1.6.1