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

#include "nusmv/core/bmc/bmcDump.h"
#include "nusmv/core/bmc/bmc.h"
#include "nusmv/core/fsm/be/BeFsm.h"
#include "nusmv/core/fsm/sexp/SexpFsm.h"
#include "nusmv/core/trace/Trace.h"
#include "nusmv/core/utils/utils.h"
#include "nusmv/core/prop/Prop.h"

Go to the source code of this file.

Enumerations
enum	bmc_invar_closure_strategy { BMC_INVAR_BACKWARD_CLOSURE, BMC_INVAR_FORWARD_CLOSURE }
	BMC invariant checking closure strategies. More...
enum	Bmc_result { BMC_TRUE, BMC_FALSE, BMC_UNKNOWN, BMC_ERROR }
	High-level functionalities interface file. More...
Functions
Bmc_result	Bmc_een_sorensson_algorithm (const NuSMVEnv_ptr env, BeFsm_ptr be_fsm, BoolSexpFsm_ptr bool_fsm, node_ptr binvarspec, int max_k, const Bmc_DumpType dump_type, const char *dump_fname_template, Prop_ptr pp, Prop_ptr oldprop, boolean print_steps, boolean use_extra_step, Trace_ptr *trace)
	Solve and INVARSPEC problems by using Een/Sorensson method non-incrementally.
Bmc_result	Bmc_een_sorensson_algorithm_without_dump (const NuSMVEnv_ptr env, BeFsm_ptr be_fsm, BoolSexpFsm_ptr bool_fsm, node_ptr binvarspec, int max_k, boolean use_extra_step, Trace_ptr *trace)
	Solve and INVARSPEC problems by using Een/Sorensson method non-incrementally and without dumping the problem.
int	Bmc_GenSolveInvar (NuSMVEnv_ptr env, Prop_ptr invarprop, const boolean must_solve, const Bmc_DumpType dump_type, const char *dump_fname_template)
	Generates DIMACS version and/or solve and INVARSPEC problems.
int	Bmc_GenSolveInvar_EenSorensson (NuSMVEnv_ptr env, Prop_ptr invarprop, const int max_k, const Bmc_DumpType dump_type, const char *dump_fname_template, boolean use_extra_step)
	Solve and INVARSPEC problems by using Een/Sorensson method non-incrementally.
int	Bmc_GenSolveInvarDual (NuSMVEnv_ptr env, Prop_ptr invarprop, const int max_k, bmc_invar_closure_strategy strategy)
	Solve an INVARSPEC problems wiht algorithm Dual.
int	Bmc_GenSolveInvarFalsification (NuSMVEnv_ptr env, Prop_ptr invarprop, const int max_k, int step_k)
	Solve an INVARSPEC problems wiht algorithm Fasification.
int	Bmc_GenSolveInvarZigzag (NuSMVEnv_ptr env, Prop_ptr invarprop, const int max_k)
	Solve an INVARSPEC problems with algorithm ZigZag.
int	Bmc_GenSolveLtl (NuSMVEnv_ptr env, Prop_ptr ltlprop, const int k, const int relative_loop, const boolean must_inc_length, const boolean must_solve, const Bmc_DumpType dump_type, const char *dump_fname_template)
	Given a LTL property generates and solve the problems for all Ki (k_min<=i<=k_max). If bIncreaseK is 0 then k_min==k_max==k and only one problem is generated. If bIncreaseK is 1 then k_min == 0 and k_max == k. Each problem Ki takes into account of all possible loops from k_min to Ki if loopback is '*' (BMC_ALL_LOOPS). Also see the Bmc_GenSolve_Action possible values. Returns 1 if solver could not be created, 0 if everything went smooth.
int	Bmc_GenSolveLtlInc (NuSMVEnv_ptr env, Prop_ptr ltlprop, const int k, const int relative_loop, const boolean must_inc_length)
	Solves LTL problem the same way as the original Bmc_GenSolveLtl but just adds BE representing the path incrementaly.
Bmc_result	Bmc_induction_algorithm (const NuSMVEnv_ptr env, BeFsm_ptr be_fsm, node_ptr binvarspec, Trace_ptr *trace_index, NodeList_ptr symbols)
	Apply Induction algorithm on th given FSM to check the given NNFd invarspec.

---

Enumeration Type Documentation

enum bmc_invar_closure_strategy

BMC invariant checking closure strategies.

optional

See also:

optional

Enumerator:

BMC_INVAR_BACKWARD_CLOSURE
BMC_INVAR_FORWARD_CLOSURE

enum Bmc_result

High-level functionalities interface file.

Author:

Roberto Cavada High level functionalities allow to perform Bounded Model Checking for LTL properties and invariants, as well as simulations.

Todo:

Missing synopsis

Todo:

Missing description

Enumerator:

BMC_TRUE
BMC_FALSE
BMC_UNKNOWN
BMC_ERROR

---

Function Documentation

Bmc_result Bmc_een_sorensson_algorithm	(	const NuSMVEnv_ptr	env,
		BeFsm_ptr	be_fsm,
		BoolSexpFsm_ptr	bool_fsm,
		node_ptr	binvarspec,
		int	max_k,
		const Bmc_DumpType	dump_type,
		const char *	dump_fname_template,
		Prop_ptr	pp,
		Prop_ptr	oldprop,
		boolean	print_steps,
		boolean	use_extra_step,
		Trace_ptr *	trace
	)

Solve and INVARSPEC problems by using Een/Sorensson method non-incrementally.

Returns a Bmc_result according to the result of the checking

See also:

Bmc_GenSolvePbs

Bmc_result Bmc_een_sorensson_algorithm_without_dump	(	const NuSMVEnv_ptr	env,
		BeFsm_ptr	be_fsm,
		BoolSexpFsm_ptr	bool_fsm,
		node_ptr	binvarspec,
		int	max_k,
		boolean	use_extra_step,
		Trace_ptr *	trace
	)

Solve and INVARSPEC problems by using Een/Sorensson method non-incrementally and without dumping the problem.

Returns a Bmc_result according to the result of the checking

See also:

Bmc_GenSolvePbs

int Bmc_GenSolveInvar	(	NuSMVEnv_ptr	env,
		Prop_ptr	invarprop,
		const boolean	must_solve,
		const Bmc_DumpType	dump_type,
		const char *	dump_fname_template
	)

Generates DIMACS version and/or solve and INVARSPEC problems.

Returns 1 if solver could not be created, 0 if everything went smooth

See also:

Bmc_GenSolvePbs

int Bmc_GenSolveInvar_EenSorensson	(	NuSMVEnv_ptr	env,
		Prop_ptr	invarprop,
		const int	max_k,
		const Bmc_DumpType	dump_type,
		const char *	dump_fname_template,
		boolean	use_extra_step
	)

Solve and INVARSPEC problems by using Een/Sorensson method non-incrementally.

Returns 1 if solver could not be created, 0 if everything went smooth

See also:

Bmc_GenSolvePbs

int Bmc_GenSolveInvarDual	(	NuSMVEnv_ptr	env,
		Prop_ptr	invarprop,
		const int	max_k,
		bmc_invar_closure_strategy	strategy
	)

Solve an INVARSPEC problems wiht algorithm Dual.

The function tries to solve the problem with not more then max_k transitions. If the problem is not solved after max_k transition then the function returns 0.

If the no_closure flag is true, only the \"base\" encoding is used

int Bmc_GenSolveInvarFalsification	(	NuSMVEnv_ptr	env,
		Prop_ptr	invarprop,
		const int	max_k,
		int	step_k
	)

Solve an INVARSPEC problems wiht algorithm Fasification.

The function tries to solve the problem with not more then max_k transitions. If the problem is not solved after max_k transition then the function returns 0.

int Bmc_GenSolveInvarZigzag	(	NuSMVEnv_ptr	env,
		Prop_ptr	invarprop,
		const int	max_k
	)

Solve an INVARSPEC problems with algorithm ZigZag.

The function will run not more then max_k transitions, then if the problem is not proved the function just returns 0

int Bmc_GenSolveLtl	(	NuSMVEnv_ptr	env,
		Prop_ptr	ltlprop,
		const int	k,
		const int	relative_loop,
		const boolean	must_inc_length,
		const boolean	must_solve,
		const Bmc_DumpType	dump_type,
		const char *	dump_fname_template
	)

Given a LTL property generates and solve the problems for all Ki (k_min<=i<=k_max). If bIncreaseK is 0 then k_min==k_max==k and only one problem is generated. If bIncreaseK is 1 then k_min == 0 and k_max == k. Each problem Ki takes into account of all possible loops from k_min to Ki if loopback is '*' (BMC_ALL_LOOPS).
Also see the Bmc_GenSolve_Action possible values. Returns 1 if solver could not be created, 0 if everything went smooth.

Returns 1 if solver could not be created, 0 if everything went smooth

See also:

Bmc_GenSolve_Action

int Bmc_GenSolveLtlInc	(	NuSMVEnv_ptr	env,
		Prop_ptr	ltlprop,
		const int	k,
		const int	relative_loop,
		const boolean	must_inc_length
	)

Solves LTL problem the same way as the original Bmc_GenSolveLtl but just adds BE representing the path incrementaly.

See also:

Bmc_GenSolve_Action

Bmc_result Bmc_induction_algorithm	(	const NuSMVEnv_ptr	env,
		BeFsm_ptr	be_fsm,
		node_ptr	binvarspec,
		Trace_ptr *	trace_index,
		NodeList_ptr	symbols
	)

Apply Induction algorithm on th given FSM to check the given NNFd invarspec.

Returns BMC_TRUE if the property is true, BMC_UNKNOWN if the induction failed, if the induction fails and the counter example option is activated, then a trace is registered in the global trace manager and its index is stored in trace_index parameter.