BddTrans Struct Reference

The header file of the class BddTrans. More...

#include <BddTrans.h>

Related Functions
(Note that these are not member functions.)
void	BddTrans_apply_synchronous_product (BddTrans_ptr self, const BddTrans_ptr other)
	Performs the synchronous product between two trans.
BddTrans_ptr	BddTrans_create (DDMgr_ptr dd_manager, const ClusterList_ptr clusters_bdd, bdd_ptr state_vars_cube, bdd_ptr input_vars_cube, bdd_ptr next_state_vars_cube, const TransType trans_type, const ClusterOptions_ptr cl_options)
	Builds the transition relation from a provided cluster list.
bdd_ptr	BddTrans_get_backward_image_state (const BddTrans_ptr self, bdd_ptr s)
	Computes the backward image by existentially quantifying over state variables only.
bdd_ptr	BddTrans_get_backward_image_state_input (const BddTrans_ptr self, bdd_ptr s)
	Computes the backward image by existentially quantifying over both state and input variables.
ClusterList_ptr	BddTrans_get_clusterlist (const BddTrans_ptr self)
	Returns a clusterized BDD representing the whole transition relation.
bdd_ptr	BddTrans_get_forward_image_state (const BddTrans_ptr self, bdd_ptr s)
	Computes the forward image by existentially quantifying over state variables only.
bdd_ptr	BddTrans_get_forward_image_state_input (const BddTrans_ptr self, bdd_ptr s)
	Computes the forward image by existentially quantifying over both state and input variables.
bdd_ptr	BddTrans_get_k_backward_image_state (const BddTrans_ptr self, bdd_ptr s, int k)
	Computes the k backward image by existentially quantifying over state variables only.
bdd_ptr	BddTrans_get_k_backward_image_state_input (const BddTrans_ptr self, bdd_ptr s, int k)
	Computes the k backward image by existentially quantifying over both state and input variables.
bdd_ptr	BddTrans_get_k_forward_image_state (const BddTrans_ptr self, bdd_ptr s, int k)
	Computes the k forward image by existentially quantifying over state variables only.
bdd_ptr	BddTrans_get_k_forward_image_state_input (const BddTrans_ptr self, bdd_ptr s, int k)
	Computes the k forward image by existentially quantifying over both state and input variables.
bdd_ptr	BddTrans_get_monolithic_bdd (const BddTrans_ptr self)
	Returns a monolithic BDD representing the whole transition relation.
void	BddTrans_print_short_info (const BddTrans_ptr self, FILE *file)
	Prints short info associated to a Trans.

---

Detailed Description

The header file of the class BddTrans.

Author:

Roberto Cavada The package trans.bdd implements classes to store and maipulate transition relation in bdd form

The structure used to represent the transition relation.

---

Friends And Related Function Documentation

void BddTrans_apply_synchronous_product	(	BddTrans_ptr	self,
		const BddTrans_ptr	other
	)			[related]

Performs the synchronous product between two trans.

The result goes into self and contained forward and backward cluster lists would be rescheduled. Other will remain unchanged.

self will change

BddTrans_ptr BddTrans_create	(	DDMgr_ptr	dd_manager,
		const ClusterList_ptr	clusters_bdd,
		bdd_ptr	state_vars_cube,
		bdd_ptr	input_vars_cube,
		bdd_ptr	next_state_vars_cube,
		const TransType	trans_type,
		const ClusterOptions_ptr	cl_options
	)			[related]

Builds the transition relation from a provided cluster list.

None of given arguments will become owned by self. You should destroy cl_options by yourself. This is a specialized version of constructor to build BddTrans based on ClusterList

See also:

BddTrans_generic_create

bdd_ptr BddTrans_get_backward_image_state	(	const BddTrans_ptr	self,
		bdd_ptr	s
	)			[related]

Computes the backward image by existentially quantifying over state variables only.

Returned bdd is referenced

bdd_ptr BddTrans_get_backward_image_state_input	(	const BddTrans_ptr	self,
		bdd_ptr	s
	)			[related]

Computes the backward image by existentially quantifying over both state and input variables.

Returned bdd is referenced

ClusterList_ptr BddTrans_get_clusterlist

(

const BddTrans_ptr

self

)

[related]

Returns a clusterized BDD representing the whole transition relation.

Invoker has to free the returned clusterlist

bdd_ptr BddTrans_get_forward_image_state	(	const BddTrans_ptr	self,
		bdd_ptr	s
	)			[related]

Computes the forward image by existentially quantifying over state variables only.

Returned bdd is referenced

self keeps the ownership of the returned instance.

bdd_ptr BddTrans_get_forward_image_state_input	(	const BddTrans_ptr	self,
		bdd_ptr	s
	)			[related]

Computes the forward image by existentially quantifying over both state and input variables.

Returned bdd is referenced

bdd_ptr BddTrans_get_k_backward_image_state	(	const BddTrans_ptr	self,
		bdd_ptr	s,
		int	k
	)			[related]

Computes the k backward image by existentially quantifying over state variables only.

Returned bdd is referenced

bdd_ptr BddTrans_get_k_backward_image_state_input	(	const BddTrans_ptr	self,
		bdd_ptr	s,
		int	k
	)			[related]

Computes the k backward image by existentially quantifying over both state and input variables.

Returned bdd is referenced

bdd_ptr BddTrans_get_k_forward_image_state	(	const BddTrans_ptr	self,
		bdd_ptr	s,
		int	k
	)			[related]

Computes the k forward image by existentially quantifying over state variables only.

Returned bdd is referenced

self keeps the ownership of the returned instance.

bdd_ptr BddTrans_get_k_forward_image_state_input	(	const BddTrans_ptr	self,
		bdd_ptr	s,
		int	k
	)			[related]

Computes the k forward image by existentially quantifying over both state and input variables.

Returned bdd is referenced

bdd_ptr BddTrans_get_monolithic_bdd

(

const BddTrans_ptr

self

)

[related]

Returns a monolithic BDD representing the whole transition relation.

Warning: computation of such BDD may be very time- and memory-consuming.

Invoker has to free the returned BDD.

self will change

void BddTrans_print_short_info	(	const BddTrans_ptr	self,
		FILE *	file
	)			[related]

Prints short info associated to a Trans.

Prints info about the size of each cluster in forward/backward transition relations

---

The documentation for this struct was generated from the following file:

• NuSMV/code/nusmv/core/trans/bdd/BddTrans.h