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

#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"
#include "nusmv/core/prop/PropDb.h"

Go to the source code of this file.

Functions
int	Bmc_Gen_check_psl_property (NuSMVEnv_ptr env, Prop_ptr prop, boolean dump_prob, boolean inc_sat, boolean single_prob, int k, int rel_loop)
	Top-level function for bmc of PSL properties.
be_ptr	Bmc_Gen_InvarBaseStep (const BeFsm_ptr be_fsm, const node_ptr wff)
	Returns the base step of the invariant construction.
be_ptr	Bmc_Gen_InvarInductStep (const BeFsm_ptr be_fsm, const node_ptr wff)
	Returns the induction step of the invariant construction.
be_ptr	Bmc_Gen_InvarProblem (const BeFsm_ptr be_fsm, const node_ptr wff)
	Public interface of the Generation module.
be_ptr	Bmc_Gen_LtlProblem (const BeFsm_ptr be_fsm, const node_ptr ltl_wff, const int k, const int l)
	Returns the LTL problem at length k with loopback l (single loop, no loop and all loopbacks are allowed).
be_ptr	Bmc_Gen_UnrollingFragment (const BeFsm_ptr self, const int i)
	Generates i-th fragment of BMC unrolling.

---

Function Documentation

int Bmc_Gen_check_psl_property	(	NuSMVEnv_ptr	env,
		Prop_ptr	prop,
		boolean	dump_prob,
		boolean	inc_sat,
		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.
• 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

be_ptr Bmc_Gen_InvarBaseStep	(	const BeFsm_ptr	be_fsm,
		const node_ptr	wff
	)

Returns the base step of the invariant construction.

Returns I0 -> P0, where I0 is the init and invar at time 0, and P0 is the given formula at time 0

See also:

Bmc_Gen_InvarInductStep

be_ptr Bmc_Gen_InvarInductStep	(	const BeFsm_ptr	be_fsm,
		const node_ptr	wff
	)

Returns the induction step of the invariant construction.

Returns (P0 and R01) -> P1, where P0 is the formula at time 0, R01 is the transition (without init) from time 0 to 1, and P1 is the formula at time 1

See also:

Bmc_Gen_InvarBaseStep

be_ptr Bmc_Gen_InvarProblem	(	const BeFsm_ptr	be_fsm,
		const node_ptr	wff
	)

Public interface of the Generation module.

Author:

Roberto Cavada

Todo:

: Missing description

AutomaticStart

Builds and returns the invariant problem of the given propositional formula Builds the negation of (I0 imp P0) and ((P0 and R01) imp P1) that must be unsatisfiable.

See also:

Bmc_Gen_InvarBaseStep, Bmc_Gen_InvarInductStep

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

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

be_ptr Bmc_Gen_UnrollingFragment	(	const BeFsm_ptr	self,
		const int	i
	)

Generates i-th fragment of BMC unrolling.

None