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

#include "nusmv/core/enc/enc.h"
#include "nusmv/core/enc/be/BeEnc.h"
#include "nusmv/core/trace/Trace.h"
#include "nusmv/core/bmc/sbmc/sbmcStructs.h"
#include "nusmv/core/utils/utils.h"

Go to the source code of this file.

Defines
#define	sbmc_SNH_text   "%s:%d: Should not happen"
	Tableau function for SBMC package.
#define	sbmc_SNYI_text   "%s:%d: Something not yet implemented\n"
Functions
be_ptr	sbmc_build_InLoop_i (const BeEnc_ptr be_enc, const state_vars_struct *state_vars, array_t *InLoop_array, const unsigned int i_model)
	Build InLoop_i.
be_ptr	sbmc_equal_vectors_formula (const BeEnc_ptr be_enc, lsList vars, const unsigned int i, const unsigned int j)
	Makes the BE formula "\land_{v \in vars} s_i = s_j".
hash_ptr	sbmc_init_LTL_info (const NuSMVEnv_ptr env, SymbLayer_ptr layer, node_ptr ltlspec, lsList state_vars_formula_pd0, lsList state_vars_formula_pdx, lsList state_vars_formula_aux, const int opt_force_state_vars, const int opt_do_virtual_unrolling)
	Associates each subformula node of ltlspec with a sbmc_LTL_info.
void	sbmc_init_state_vector (const BeEnc_ptr be_enc, const node_ptr ltlspec, const hash_ptr info_map, const unsigned int i_real, const node_ptr LastState_var, const be_ptr be_LoopExists)
	Initialize trans_bes[i][d] for each sub-formula.
lsList	sbmc_SimplePaths (const BeEnc_ptr be_enc, const state_vars_struct *state_vars, array_t *InLoop_array, const unsigned int k)
	Build SimplePath_{i,k} for each 0<=i<k.

---

Define Documentation

#define sbmc_SNH_text   "%s:%d: Should not happen"

Tableau function for SBMC package.

Author:

Tommi Junttila, Marco Roveri Tableau function for SBMC package

Todo:

Missing synopsis

Todo:

Missing description

#define sbmc_SNYI_text   "%s:%d: Something not yet implemented\n"

Todo:

Missing synopsis

Todo:

Missing description

---

Function Documentation

be_ptr sbmc_build_InLoop_i	(	const BeEnc_ptr	be_enc,
		const state_vars_struct *	state_vars,
		array_t *	InLoop_array,
		const unsigned int	i_model
	)

Build InLoop_i.

Build InLoop_i stuff Define InLoop_i = (InLoop_{i-1} || l_i)
Returns the BE constraint InLoop_{i-1} => !l_i (or 0 when i=0)

None

be_ptr sbmc_equal_vectors_formula	(	const BeEnc_ptr	be_enc,
		lsList	vars,
		const unsigned int	i,
		const unsigned int	j
	)

Makes the BE formula "\land_{v \in vars} s_i = s_j".

AutomaticStart

Creates the BE for the formula "\land_{v \in vars} s_i = s_j"

None

hash_ptr sbmc_init_LTL_info	(	const NuSMVEnv_ptr	env,
		SymbLayer_ptr	layer,
		node_ptr	ltlspec,
		lsList	state_vars_formula_pd0,
		lsList	state_vars_formula_pdx,
		lsList	state_vars_formula_aux,
		const int	opt_force_state_vars,
		const int	opt_do_virtual_unrolling
	)

Associates each subformula node of ltlspec with a sbmc_LTL_info.

Associates each subformula node of ltlspec with a sbmc_LTL_info. Returns a hash from node_ptr to sbmc_LTL_info*. New state variables named LTL_t'i' can be allocate to 'layer'. The new state vars are inserted in state_vars_formula_??? appropriately.

None

void sbmc_init_state_vector	(	const BeEnc_ptr	be_enc,
		const node_ptr	ltlspec,
		const hash_ptr	info_map,
		const unsigned int	i_real,
		const node_ptr	LastState_var,
		const be_ptr	be_LoopExists
	)

Initialize trans_bes[i][d] for each sub-formula.

Initialize trans_bes[i][d], 0<=d<=pd, to

• the formula [[f]]_i^d for definitionally translated subformulae
• the [[f]]_i^d be variable for variable translated subformulae

None

lsList sbmc_SimplePaths	(	const BeEnc_ptr	be_enc,
		const state_vars_struct *	state_vars,
		array_t *	InLoop_array,
		const unsigned int	k
	)

Build SimplePath_{i,k} for each 0<=i<k.

Build SimplePath_{i,k} for each 0<=i<k

None