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:
 All Data Structures Files Functions Variables Typedefs Enumerations Enumerator Defines

Generated on 14 Oct 2015 for NuSMV Developers Manual by  doxygen 1.6.1