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

#include "nusmv/core/bmc/bmc.h"
#include "nusmv/core/bmc/sbmc/sbmcBmcInc.h"
#include "nusmv/core/bmc/sbmc/sbmcBmc.h"
#include "nusmv/core/be/be.h"
#include "nusmv/core/fsm/be/BeFsm.h"
#include "nusmv/core/utils/utils.h"
#include "nusmv/core/node/node.h"

Go to the source code of this file.

Functions

be_ptr Bmc_Gen_SBMCProblem (const BeFsm_ptr be_fsm, const node_ptr ltl_wff, const int k, const int l)
 Public interface of the SBMC Generation module.
int Sbmc_Gen_check_psl_property (NuSMVEnv_ptr env, Prop_ptr prop, boolean dump_prob, boolean inc_sat, boolean do_completeness_check, boolean do_virtual_unrolling, boolean single_prob, int k, int rel_loop)
 Top-level function for bmc of PSL properties.

Function Documentation

be_ptr Bmc_Gen_SBMCProblem ( const BeFsm_ptr  be_fsm,
const node_ptr  ltl_wff,
const int  k,
const int  l 
)

Public interface of the SBMC Generation module.

Author:
Timo Latvala, Marco Roveri
Todo:
: Missing description

AutomaticStart

Returns the LTL problem at length k with loopback l (single loop, no loop and all loopbacks are allowed)

int Sbmc_Gen_check_psl_property ( NuSMVEnv_ptr  env,
Prop_ptr  prop,
boolean  dump_prob,
boolean  inc_sat,
boolean  do_completeness_check,
boolean  do_virtual_unrolling,
boolean  single_prob,
int  k,
int  rel_loop 
)

Top-level function for bmc of PSL properties.

The parameters are:

  • prop is the PSL property to be checked
  • dump_prob is true if the problem must be dumped as DIMACS file (default filename from system corresponding variable)
  • inc_sat is true if incremental sat must be used. If there is no support for inc sat, an internal error will occur.
  • is_single_prob is true if k must be not incremented from 0 to k_max (single problem)
  • k and rel_loop are the bmc parameters.

None

 All Data Structures Files Functions Variables Typedefs Enumerations Enumerator Defines

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