BddFsmCache Struct Reference

Private interface for package bdd_fsm. More...

#include <bddInt.h>

Data Structures
struct	BddFsmReachable_TAG
Data Fields
DDMgr_ptr	dd
BddStates	deadlock_states
BddStates	fair_states
BddStatesInputs	fair_states_inputs
unsigned int *	family_counter
BddStatesInputs	legal_state_input
BddStatesInputs	monolithic_trans
BddStates	not_successor_states
struct BddFsmCache::BddFsmReachable_TAG	reachable
BddStates	revfair_states
BddStatesInputs	revfair_states_inputs
BddStates	successor_states
Related Functions
(Note that these are not member functions.)
void	BddFsmCache_copy_reachables (BddFsmCache_ptr self, const BddFsmCache_ptr other)
	Copies reachable states information within other into self.
BddFsmCache_ptr	BddFsmCache_create (DDMgr_ptr dd)
	Class contructor.
void	BddFsmCache_destroy (BddFsmCache_ptr self)
	Class destructor.
BddFsmCache_ptr	BddFsmCache_hard_copy (const BddFsmCache_ptr self)
	Class copy constructor.
void	BddFsmCache_reset_not_reusable_fields_after_product (BddFsmCache_ptr self)
	Resets any field in the cache that must be recalculated.
void	BddFsmCache_set_reachable_states (BddFsmCache_ptr self, BddStates reachable)
	Fills cache structure with reachable states information.
void	BddFsmCache_set_reachables (BddFsmCache_ptr self, node_ptr layers_list, const int diameter, boolean completed)
	Fills cache structure with reachable states information.
BddFsmCache_ptr	BddFsmCache_soft_copy (const BddFsmCache_ptr self)
	Family soft copier.

Detailed Description

Private interface for package bdd_fsm.

Author:: Roberto Cavada

Todo:: : Missing description

Todo:: Missing synopsis

Todo:: Missing description

Friends And Related Function Documentation

void BddFsmCache_copy_reachables	(	BddFsmCache_ptr	self,
		const BddFsmCache_ptr	other
	)			`[related]`

Copies reachable states information within other into self.

This method is used when copying reachable states information between to FSMs

BddFsmCache_ptr BddFsmCache_create ( DDMgr_ptr dd ) [related]

Class contructor.

void BddFsmCache_destroy ( BddFsmCache_ptr self ) [related]

Class destructor.

BddFsmCache_ptr BddFsmCache_hard_copy ( const BddFsmCache_ptr self ) [related]

Class copy constructor.

Hardly copy the instance, by creating a new, separate family

See also:: BddFsmCache_soft_copy

void BddFsmCache_reset_not_reusable_fields_after_product ( BddFsmCache_ptr self ) [related]

Resets any field in the cache that must be recalculated.

This is called when syncronous product is carried out. In particular LTL BDD-based model checking, after having applied the product between the original fsm and the fsm coming from the tableau contruction, needs to disable the cache sharing and to recalculate fair states and other fields, since the fsm changed. All fsm's fields that need to be recalculated after the syncronous product must be reset by this method.

See also:: BddFsm_apply_synchronous_product

void BddFsmCache_set_reachable_states	(	BddFsmCache_ptr	self,
		BddStates	reachable
	)			`[related]`

Fills cache structure with reachable states information.

Fills cache structure with reachable states information. The given BDD is supposed to represent the whole set of reachable states of the Bdd FSM. It should NOT contain other informations (such as onion rings ecc)

void BddFsmCache_set_reachables	(	BddFsmCache_ptr	self,
		node_ptr	layers_list,
		const int	diameter,
		boolean	completed
	)			`[related]`

Fills cache structure with reachable states information.

Given list layers_list must be reversed, from last layer to the layer corresponding to initial state. Given list layers_list will be destroyed.

given list layers_list will be destroyed, cache changes

BddFsmCache_ptr BddFsmCache_soft_copy ( const BddFsmCache_ptr self ) [related]

Family soft copier.

Returns the same instance, but the family counter is increased, in order to handle sharing of the instance. The destructor will actually destroy this instance only when the last family member will be destroyed