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. |
The header file of the class BddTrans.
The structure used to represent the transition relation.
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
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