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