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

#include "nusmv/core/bmc/bmcDump.h"
#include "nusmv/core/utils/utils.h"
#include "nusmv/core/prop/Prop.h"

Go to the source code of this file.

Functions
int	Bmc_SBMCGenSolveLtl (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)
	High-level functionalities interface file for SBMC.

---

Function Documentation

int Bmc_SBMCGenSolveLtl	(	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
	)

High-level functionalities interface file for SBMC.

Author:

Timo Latvala, Marco Roveri High level functionalities to perform Simple Bounded Model Checking for LTL properties.

For further information about this implementation see: T. Latvala, A. Biere, K. Heljanko, and T. Junttila. Simple is Better: Efficient Bounded Model Checking for Past LTL. In: R. Cousot (ed.), Verification, Model Checking, and Abstract Interpretation, 6th International Conference VMCAI 2005, Paris, France, Volume 3385 of LNCS, pp. 380-395, Springer, 2005. Copyright (C) Springer-Verlag.

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

See also:

Bmc_GenSolve_Action