#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. |
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.
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:
None