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

#include <time.h>
#include <limits.h>
#include <stdio.h>
#include "nusmv/core/enc/be/BeEnc.h"
#include "nusmv/core/fsm/FsmBuilder.h"
#include "nusmv/core/compile/compile.h"
#include "nusmv/core/be/be.h"
#include "nusmv/core/trace/Trace.h"
#include "nusmv/core/trace/TraceMgr.h"
#include "nusmv/core/dd/dd.h"
#include "nusmv/core/opt/opt.h"
#include "nusmv/core/node/node.h"
#include "nusmv/core/utils/utils.h"

Go to the source code of this file.

Defines
#define	BMC_BEXP_OUTPUT_LB   1
#define	BMC_BEXP_OUTPUT_SMV   0
#define	BMC_DUMP_FILENAME_MAXLEN   4096
	The private interfaces for the bmc package.
#define	BMC_NO_PROPERTY_INDEX   -1
#define	DEFAULT_BMC_FORCE_PLTL_TABLEAU   0
#define	DEFAULT_BMC_INC_INVAR_ALG   "dual"
#define	DEFAULT_BMC_INVAR_ALG   "classic"
#define	DEFAULT_BMC_OPTIMIZED_TABLEAU   1
#define	DEFAULT_BMC_PB_LENGTH   10
#define	DEFAULT_BMC_PB_LOOP   Bmc_Utils_GetAllLoopbacksString()
#define	DEFAULT_DIMACS_FILENAME   "@f_k@k_l@l_n@n"
#define	DEFAULT_INVAR_DIMACS_FILENAME   "@f_invar_n@n"
#define	ST_BMC_CONV_BEXPR2BE_HASH   "bcbh"
#define	ST_BMC_TABLEAU_LTL_HASH   "btlh"
Functions
Trace_ptr	Bmc_create_trace_from_cnf_model (const BeEnc_ptr be_enc, const NodeList_ptr symbols, const char *desc, const TraceType type, const Slist_ptr cnf_model, int k)
	Creates a trace out of a cnf model.
Trace_ptr	Bmc_fill_trace_from_cnf_model (const BeEnc_ptr be_enc, const Slist_ptr cnf_model, int k, Trace_ptr trace)
	Fills the given trace out of a cnf model.
be_ptr	Bmc_GetTestTableau (const BeEnc_ptr be_enc, const node_ptr ltl_wff, const int k, const int l)
Trace_ptr	bmc_simulate_get_curr_sim_trace (const NuSMVEnv_ptr env)
int	bmc_simulate_get_curr_sim_trace_index (const NuSMVEnv_ptr env)
void	bmc_simulate_set_curr_sim_trace (const NuSMVEnv_ptr env, Trace_ptr trace, int idx)
hash_ptr	Bmc_Tableau_get_handled_hash (SymbTable_ptr symb_table, char *hash_str)
	Call SymbTable_get_handled_hash_ptr with proper arguments.
node_ptr	bmc_tableau_memoization_get_key (NodeMgr_ptr nodemgr, node_ptr wff, int time, int k, int l)
	Creates the key for ltl_tableau_hash.
void	bmc_tableau_memoization_insert (hash_ptr, node_ptr key, be_ptr be)
	Insertion function for ltl_tableau_hash.
be_ptr	bmc_tableau_memoization_lookup (hash_ptr, node_ptr key)
	Lookup function for ltl_tableau_hash.
be_ptr	bmc_tableauGetEventuallyAtTime (const BeEnc_ptr be_enc, const node_ptr ltl_wff, const int intime, const int k, const int l)
	Resolves the future operator, and builds a conjunctive expression of tableaus, by iterating intime up to k in a different manner depending on the [l, k] interval form.
be_ptr	bmc_tableauGetGloballyAtTime (const BeEnc_ptr be_enc, const node_ptr ltl_wff, const int intime, const int k, const int l)
	As bmc_tableauGetEventuallyAtTime, but builds a conjunctioned expression in order to be able to assure a global constraint.
be_ptr	bmc_tableauGetNextAtTime (const BeEnc_ptr be_enc, const node_ptr ltl_wff, const int time, const int k, const int l)
	Resolves the NEXT operator, building the tableau for its argument.
be_ptr	bmc_tableauGetReleasesAtTime (const BeEnc_ptr be_enc, const node_ptr p, const node_ptr q, const int time, const int k, const int l)
	Builds an expression which evaluates the release operator.
be_ptr	bmc_tableauGetUntilAtTime (const BeEnc_ptr be_enc, const node_ptr p, const node_ptr q, const int time, const int k, const int l)
	Builds an expression which evaluates the until operator.
be_ptr	Bmc_TableauPLTL_GetAllTimeTableau (const BeEnc_ptr be_enc, const node_ptr pltl_wff, const int k)
	Builds the conjunction of the tableaux for a PLTL formula computed on every time instant along a (k,l)-loop.
be_ptr	Bmc_TableauPLTL_GetTableau (const BeEnc_ptr be_enc, const node_ptr pltl_wff, const int k, const int l)
	Builds the tableau for a PLTL formula.
void	Bmc_TestReset (void)
	Call this function to reset the test sub-package (into the reset command for example).
int	Bmc_TestTableau (NuSMVEnv_ptr env, int argc, char **argv)
void	bmc_trace_utils_append_input_state (Trace_ptr trace, BeEnc_ptr be_enc, const Slist_ptr cnf_model)
	Appends a _complete_ (i,S') pair to existing trace.
void	bmc_trace_utils_complete_trace (Trace_ptr trace, const BoolEnc_ptr bool_enc)
	Populates trace with valid defaults assignments.
lsList	Bmc_Utils_get_vars_list_for_uniqueness (BeEnc_ptr be_enc, Prop_ptr invarprop)
	Creates a list of BE variables that are intended to be used by the routine that makes the state unique in invariant checking.
lsList	Bmc_Utils_get_vars_list_for_uniqueness_fsm (BeEnc_ptr be_enc, SexpFsm_ptr bool_fsm)
	Creates a list of BE variables that are intended to be used by the routine that makes the state unique in invariant checking.
be_ptr	BmcInt_Tableau_GetAtTime (const BeEnc_ptr be_enc, const node_ptr ltl_wff, const int time, const int k, const int l)
	Given a wff expressed in ltl builds the model-independent tableau at 'time' of a path formula bounded by [k, l].
boolean	isPureFuture (const node_ptr pltl_wff)
	Checks wether a formula contains only future operators.
Variables
cmp_struct_ptr	cmps
FsmBuilder_ptr	global_fsm_builder
TraceMgr_ptr	global_trace_manager

---

Define Documentation

#define BMC_BEXP_OUTPUT_LB   1

Todo:

Missing synopsis

Todo:

Missing description

#define BMC_BEXP_OUTPUT_SMV   0

Todo:

Missing synopsis

Todo:

Missing description

#define BMC_DUMP_FILENAME_MAXLEN   4096

The private interfaces for the bmc package.

Author:

Roberto Cavada

Todo:

: Missing description

Todo:

Missing synopsis

Todo:

Missing description

#define BMC_NO_PROPERTY_INDEX   -1

Todo:

Missing synopsis

Todo:

Missing description

#define DEFAULT_BMC_FORCE_PLTL_TABLEAU   0

Todo:

Missing synopsis

Todo:

Missing description

#define DEFAULT_BMC_INC_INVAR_ALG   "dual"

Todo:

Missing synopsis

Todo:

Missing description

#define DEFAULT_BMC_INVAR_ALG   "classic"

Todo:

Missing synopsis

Todo:

Missing description

#define DEFAULT_BMC_OPTIMIZED_TABLEAU   1

Todo:

Missing synopsis

Todo:

Missing description

#define DEFAULT_BMC_PB_LENGTH   10

Todo:

Missing synopsis

Todo:

Missing description

#define DEFAULT_BMC_PB_LOOP   Bmc_Utils_GetAllLoopbacksString()

Todo:

Missing synopsis

Todo:

Missing description

#define DEFAULT_DIMACS_FILENAME   "@f_k@k_l@l_n@n"

Todo:

Missing synopsis

Todo:

Missing description

#define DEFAULT_INVAR_DIMACS_FILENAME   "@f_invar_n@n"

Todo:

Missing synopsis

Todo:

Missing description

#define ST_BMC_CONV_BEXPR2BE_HASH   "bcbh"

Todo:

Missing synopsis

Todo:

Missing description

#define ST_BMC_TABLEAU_LTL_HASH   "btlh"

Todo:

Missing synopsis

Todo:

Missing description

---

Function Documentation

Trace_ptr Bmc_create_trace_from_cnf_model	(	const BeEnc_ptr	be_enc,
		const NodeList_ptr	symbols,
		const char *	desc,
		const TraceType	type,
		const Slist_ptr	cnf_model,
		int	k
	)

Creates a trace out of a cnf model.

Creates a complete, k steps long trace in the language of \"symbols\" out a cnf model from a sat solver. The returned trace is non-volatile.

For more control over the built trace, please see Bmc_fill_trace_from_cnf_model

none

See also:

Trace_create, Mc_create_trace_from_bdd_input_list, Bmc_fill_trace_from_cnf_model

Trace_ptr Bmc_fill_trace_from_cnf_model	(	const BeEnc_ptr	be_enc,
		const Slist_ptr	cnf_model,
		int	k,
		Trace_ptr	trace
	)

Fills the given trace out of a cnf model.

Fills the trace. The trace will be a complete, k steps long trace in the language of \"symbols\" out a cnf model from a sat solver.

none

See also:

Trace_create, Mc_fill_trace_from_bdd_input_list

be_ptr Bmc_GetTestTableau	(	const BeEnc_ptr	be_enc,
		const node_ptr	ltl_wff,
		const int	k,
		const int	l
	)

Trace_ptr bmc_simulate_get_curr_sim_trace

(

const NuSMVEnv_ptr

env

)

int bmc_simulate_get_curr_sim_trace_index

(

const NuSMVEnv_ptr

env

)

void bmc_simulate_set_curr_sim_trace	(	const NuSMVEnv_ptr	env,
		Trace_ptr	trace,
		int	idx
	)

hash_ptr Bmc_Tableau_get_handled_hash	(	SymbTable_ptr	symb_table,
		char *	hash_str
	)

Call SymbTable_get_handled_hash_ptr with proper arguments.

node_ptr bmc_tableau_memoization_get_key	(	NodeMgr_ptr	nodemgr,
		node_ptr	wff,
		int	time,
		int	k,
		int	l
	)

Creates the key for ltl_tableau_hash.

AutomaticStart

void bmc_tableau_memoization_insert	(	hash_ptr	,
		node_ptr	key,
		be_ptr	be
	)

Insertion function for ltl_tableau_hash.

be_ptr bmc_tableau_memoization_lookup	(	hash_ptr	,
		node_ptr	key
	)

Lookup function for ltl_tableau_hash.

be_ptr bmc_tableauGetEventuallyAtTime	(	const BeEnc_ptr	be_enc,
		const node_ptr	ltl_wff,
		const int	intime,
		const int	k,
		const int	l
	)

Resolves the future operator, and builds a conjunctive expression of tableaus, by iterating intime up to k in a different manner depending on the [l, k] interval form.

ltl_wff is the 'p' part in 'F p'. If intime<=k is out of [l, k] or if there is no loop, iterates from intime to k, otherwise iterates from l to k

be_ptr bmc_tableauGetGloballyAtTime	(	const BeEnc_ptr	be_enc,
		const node_ptr	ltl_wff,
		const int	intime,
		const int	k,
		const int	l
	)

As bmc_tableauGetEventuallyAtTime, but builds a conjunctioned expression in order to be able to assure a global constraint.

ltl_wff is the 'p' part in 'G p'

See also:

bmc_tableauGetEventuallyAtTime

be_ptr bmc_tableauGetNextAtTime	(	const BeEnc_ptr	be_enc,
		const node_ptr	ltl_wff,
		const int	time,
		const int	k,
		const int	l
	)

Resolves the NEXT operator, building the tableau for its argument.

Returns a falsity constants if the next operator leads out of [l, k] and there is no loop

be_ptr bmc_tableauGetReleasesAtTime	(	const BeEnc_ptr	be_enc,
		const node_ptr	p,
		const node_ptr	q,
		const int	time,
		const int	k,
		const int	l
	)

Builds an expression which evaluates the release operator.

Carries out the steps number to be performed, depending on l,k and time, then calls bmc_tableauGetReleasesAtTime_aux

See also:

bmc_tableauGetReleasesAtTime_aux

be_ptr bmc_tableauGetUntilAtTime	(	const BeEnc_ptr	be_enc,
		const node_ptr	p,
		const node_ptr	q,
		const int	time,
		const int	k,
		const int	l
	)

Builds an expression which evaluates the until operator.

Carries out the steps number to be performed, depending on l,k and time, then calls bmc_tableauGetUntilAtTime_aux

See also:

bmc_tableauGetUntilAtTime_aux

be_ptr Bmc_TableauPLTL_GetAllTimeTableau	(	const BeEnc_ptr	be_enc,
		const node_ptr	pltl_wff,
		const int	k
	)

Builds the conjunction of the tableaux for a PLTL formula computed on every time instant along a (k,l)-loop.

This function is a special case of "evaluateOn", thus it computes its answer by calling "evaluateOn" with some specifc arguments. The only use of this function is in constructing optimized tableaux for those depth-one formulas where "RELEASES" is the unique operator.

See also:

evaluateOn

be_ptr Bmc_TableauPLTL_GetTableau	(	const BeEnc_ptr	be_enc,
		const node_ptr	pltl_wff,
		const int	k,
		const int	l
	)

Builds the tableau for a PLTL formula.

Builds both the bounded-tableau and the loop-tableau for a PLTL formula "pltl_wff" (depending on the value of l). The time the tableau refers to is (implicitly) time zero.

See also:

getTableauAtTime

void Bmc_TestReset

(

void

)

Call this function to reset the test sub-package (into the reset command for example).

int Bmc_TestTableau	(	NuSMVEnv_ptr	env,
		int	argc,
		char **	argv
	)

Command:

_bmc_test_tableau: Generates a random formula to logically test the equivalent tableau

Command arguments: [-h] | [-n property_index] | [[ -d max_depth] [-c max_conns] [-o operator]]

Use this hidden command to generate random formulae and to test the equivalent tableau. The first time this command is called in the current NuSMV session it creates a new smv file with a model and generates a random ltl spec to test tableau. The following times it is called it appends a new formula to the file. The generated model contains the same number of non-deterministic variables the currently model loaded into NuSMV contains.
You cannot call this command if the bmc_loopback is set to '*' (all loops).

The test is possibly broken if the model contains frozen variables

Command:

check_pslspec_bmc_inc: Performs fair PSL model checking using incremental BMC.

Command arguments: [-h] [-m | -o output-file] [-n number | -p "psl-expr [IN context]" | -P "name"] [-1] [-k bmc_length] [-l loopback]\

Performs fair PSL model checking using incremental BMC.

A psl-expr to be checked can be specified at command line using option -p. Alternatively, option -n can be used for checking a particular formula in the property database. If neither -n nor -p are used, all the PSLSPEC formulas in the database are checked.

Command options:

-m

Pipes the output generated by the command in processing SPECs to the program specified by the PAGER shell variable if defined, else through the UNIX command "more".

-o output-file

Writes the output generated by the command in processing PSLSPECs to the file output-file.

-p "psl-expr [IN context]"

A PSL formula to be checked. context is the module instance name which the variables in ctl-expr must be evaluated in.

-n number

Checks the PSL property with index number in the property database.

-P name

Checks the PSL property named name in the property database.

-1 Generates and solves a single problem instead of iterating through 0 and bmc_length.

-k bmc_length

bmc_length is the maximum problem bound must be reached if the option -1 is not specified. If -1 is specified, bmc_length is the exact length of the problem to be generated. Only natural number are valid values for this option. If no value is given the environment variable bmc_length is considered instead.

-l loopback

loopback value may be:

• a natural number in (0, bmc_length-1). Positive sign ('+') can be also used as prefix of the number. Any invalid combination of length and loopback will be skipped during the generation/solving process.
  
• a negative number in (-1, -bmc_length). In this case loopback is considered a value relative to bmc_length. Any invalid combination of length and loopback will be skipped during the generation/solving process.
  
• the symbol 'X', which means "no loopback"
  
• the symbol '*', which means "all possible loopback from zero to <i>bmc_length-1</i>"

void bmc_trace_utils_append_input_state	(	Trace_ptr	trace,
		BeEnc_ptr	be_enc,
		const Slist_ptr	cnf_model
	)

Appends a _complete_ (i,S') pair to existing trace.

This is a private service of BmcStepWise_Simulation

void bmc_trace_utils_complete_trace	(	Trace_ptr	trace,
		const BoolEnc_ptr	bool_enc
	)

Populates trace with valid defaults assignments.

Populates trace with valid defaults assignments.

The trace can be safely considered complete when this function returns. Existing assignments will not be affected.

Trace is populated with default values

lsList Bmc_Utils_get_vars_list_for_uniqueness	(	BeEnc_ptr	be_enc,
		Prop_ptr	invarprop
	)

Creates a list of BE variables that are intended to be used by the routine that makes the state unique in invariant checking.

If coi is enabled, than the returned list will contain only those boolean state variable the given property actually depends on. Otherwise the full set of state boolean vars will occur in the list. Frozen variables are not required, since they do not change from state to state, thus, cannot make a state distinguishable from other states.

Returned list must be destroyed by the called.

lsList Bmc_Utils_get_vars_list_for_uniqueness_fsm	(	BeEnc_ptr	be_enc,
		SexpFsm_ptr	bool_fsm
	)

Creates a list of BE variables that are intended to be used by the routine that makes the state unique in invariant checking.

If coi is enabled, than the returned list will contain only those boolean state variable the given property actually depends on. Otherwise the full set of state boolean vars will occur in the list. Frozen variables are not required, since they do not change from state to state, thus, cannot make a state distinguishable from other states.

Returned list must be destroyed by the called.

be_ptr BmcInt_Tableau_GetAtTime	(	const BeEnc_ptr	be_enc,
		const node_ptr	ltl_wff,
		const int	time,
		const int	k,
		const int	l
	)

Given a wff expressed in ltl builds the model-independent tableau at 'time' of a path formula bounded by [k, l].

This function is the entry point of a mutual recursive calling stack. All logical connectives are resolved, excepted for NOT, which closes the recursive calling stack. Also variables and falsity/truth constants close the recursion.

See also:

bmc_tableauGetNextAtTime, bmc_tableauGetGloballyAtTime, bmc_tableauGetEventuallyAtTime, bmc_tableauGetUntilAtTime, bmc_tableauGetReleasesAtTime

boolean isPureFuture

(

const node_ptr

pltl_wff

)

Checks wether a formula contains only future operators.

---

Variable Documentation

cmp_struct_ptr cmps

FsmBuilder_ptr global_fsm_builder

TraceMgr_ptr global_trace_manager