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

#include "nusmv/core/fsm/be/BeFsm.h"
#include "nusmv/core/be/be.h"
#include "nusmv/core/node/node.h"
#include "nusmv/core/utils/utils.h"

Go to the source code of this file.

Functions
lsList	sbmc_dependent (const BeEnc_ptr be_enc, const node_ptr bltlspec, const int k, const state_vars_struct *state_vars, array_t *InLoop_array, const be_ptr be_LoopExists, const hash_ptr info_map)
	required
lsList	sbmc_formula_dependent (const BeEnc_ptr be_enc, const node_ptr ltlspec, const unsigned int k_model, const hash_ptr info_map)
	Create the formula specific k-dependent constraints.
lsList	sbmc_unroll_base (const BeEnc_ptr be_enc, const node_ptr ltlspec, const hash_ptr info_map, const be_ptr be_LoopExists, const int do_optimization)
	Public interface for Incremental SBMC tableau-related functionalities.
lsList	sbmc_unroll_invariant (const BeEnc_ptr be_enc, const node_ptr bltlspec, const int previous_k, const int new_k, const state_vars_struct *state_vars, array_t *InLoop_array, const hash_ptr info_map, const be_ptr be_LoopExists, const int opt_do_optimization)
	Unroll future and past fragment from previous_k+1 upto and including new_k.
lsList	sbmc_unroll_invariant_f (const BeEnc_ptr be_enc, const node_ptr ltlspec, const unsigned int i_model, const hash_ptr info_map, const be_ptr be_InLoop_i, const be_ptr be_l_i, const be_ptr be_LastState_i, const be_ptr be_LoopExists, const int do_optimization)
	Create the k-invariant constraints for propositional and future temporal operators at time i.
lsList	sbmc_unroll_invariant_p (const BeEnc_ptr be_enc, const node_ptr ltlspec, const unsigned int i_model, const hash_ptr info_map, const be_ptr be_InLoop_i, const be_ptr be_l_i, const int do_optimization)
	Create the k-invariant constraints at time i.
lsList	sbmc_unroll_invariant_propositional (const BeEnc_ptr be_enc, const node_ptr ltlspec, const unsigned int i_model, const hash_ptr info_map, const be_ptr be_InLoop_i, const be_ptr be_l_i, const int do_optimization)
	Create the k-invariant constraints for propositional operators at time i.

---

Function Documentation

lsList sbmc_dependent	(	const BeEnc_ptr	be_enc,
		const node_ptr	bltlspec,
		const int	k,
		const state_vars_struct *	state_vars,
		array_t *	InLoop_array,
		const be_ptr	be_LoopExists,
		const hash_ptr	info_map
	)

required

Creates several constraints:

• Create the constraint l_{k+1} <=> FALSE
• Create the constraint s_E = s_k
• Create the constraint LoopExists <=> InLoop_k
• Create the formula specific k-dependent constraints

None

lsList sbmc_formula_dependent	(	const BeEnc_ptr	be_enc,
		const node_ptr	ltlspec,
		const unsigned int	k_model,
		const hash_ptr	info_map
	)

Create the formula specific k-dependent constraints.

Create the formula specific k-dependent constraints. Return a list of be_ptrs for the created constraints.

None

lsList sbmc_unroll_base	(	const BeEnc_ptr	be_enc,
		const node_ptr	ltlspec,
		const hash_ptr	info_map,
		const be_ptr	be_LoopExists,
		const int	do_optimization
	)

Public interface for Incremental SBMC tableau-related functionalities.

Author:

Tommi Juntilla, Marco Roveri

Todo:

: Missing description

AutomaticStart

Creates the BASE constraints. Create the BASE constraints.
Return a list of be_ptr for the created constraints.
Create the following constraints:

• !LoopExists => ([[f]]_L^d == FALSE)
• LoopExists => ([[Ff]]_E^pd(Gf) => <<Ff>>_E)
• LoopExists => ([[Gf]]_E^pd(Gf) <= <<Gf>>_E)
• LoopExists => ([[fUg]]_E^pd(Gf) => <<Fg>>_E)
• LoopExists => ([[fRg]]_E^pd(Gf) <= <<Gg>>_E)

If do_optimization is true, then create the following constraints:

• [[p]]_E^d <=> p_E
• [[TRUE]]_E^0 <=> TRUE
• [[FALSE]]_E^0 <=> FALSE
• [[f | g]]_E^d <=> [[f]]_E^d | [[g]]_E^d
• [[f & g]]_E^d <=> [[f]]_E^d & [[g]]_E^d
• [[!f]]_E^d <=> ![[f]]_E^d
• [[Ff]]_E^d <=> [[f]]_E^d | [[Ff]]_L^min(d+1,pd(f))
• [[Ff]]_E^d+1 => [[Ff]]_E^d
• <<Ff>>_E => [[Ff]]_E^pd(Ff)
• [[Gf]]_E^d <=> [[f]]_E^d & [[Gf]]_L^min(d+1,pd(f))
• [[Gf]]_E^d => [[Gf]]_E^d+1
• [[Gf]]_E^pd(Gf) => <<Gf>>_E
• [[fUg]]_E^d <=> [[g]]_E^d | ([[f]]_E^d & [[fUg]]_L^min(d+1,pd(fUg)))
• [[fRg]]_E^d <=> [[g]]_E^d & ([[f]]_E^d | [[fRg]]_L^min(d+1,pd(fUg)))
• [[Xf]]_E^d <=> [[f]]_L^min(d+1,pd(f))
• [[Hf]]_E^d+1 => [[Hf]]_E^d
• [[Of]]_E^d => [[Of]]_E^d+1

None

lsList sbmc_unroll_invariant	(	const BeEnc_ptr	be_enc,
		const node_ptr	bltlspec,
		const int	previous_k,
		const int	new_k,
		const state_vars_struct *	state_vars,
		array_t *	InLoop_array,
		const hash_ptr	info_map,
		const be_ptr	be_LoopExists,
		const int	opt_do_optimization
	)

Unroll future and past fragment from previous_k+1 upto and including new_k.

Unroll future and past fragment from previous_k+1 upto and including new_k. Return a list of constraints.

None

lsList sbmc_unroll_invariant_f	(	const BeEnc_ptr	be_enc,
		const node_ptr	ltlspec,
		const unsigned int	i_model,
		const hash_ptr	info_map,
		const be_ptr	be_InLoop_i,
		const be_ptr	be_l_i,
		const be_ptr	be_LastState_i,
		const be_ptr	be_LoopExists,
		const int	do_optimization
	)

Create the k-invariant constraints for propositional and future temporal operators at time i.

Create the k-invariant constraints for propositional and future temporal operators at time i. Return a list of be_ptrs for the created constraints.

None

lsList sbmc_unroll_invariant_p	(	const BeEnc_ptr	be_enc,
		const node_ptr	ltlspec,
		const unsigned int	i_model,
		const hash_ptr	info_map,
		const be_ptr	be_InLoop_i,
		const be_ptr	be_l_i,
		const int	do_optimization
	)

Create the k-invariant constraints at time i.

Create the k-invariant constraints at time i. Return a list of be_ptrs for the created constraints.

None

lsList sbmc_unroll_invariant_propositional	(	const BeEnc_ptr	be_enc,
		const node_ptr	ltlspec,
		const unsigned int	i_model,
		const hash_ptr	info_map,
		const be_ptr	be_InLoop_i,
		const be_ptr	be_l_i,
		const int	do_optimization
	)

Create the k-invariant constraints for propositional operators at time i.

Create the k-invariant constraints for propositional operators at time i. Return a list of be_ptrs for the created constraints.

None