BddTrans.c
Routines related to Transition Relation in Bdd form
Cluster.c
Routines related to clusters of transition relation.
ClusterList.c
Routines related to list of transition clusters.
ClusterOptions.c
Routines related to "ClusterOptions" class.

BddTrans.c

Routines related to Transition Relation in Bdd form

By: Roberto Cavada

This file contains the definition of the "BddTrans" class definition

BddTrans_create()
Builds the transition relation
BddTrans_apply_synchronous_product()
Performs the synchronous product between two trans
BddTrans_get_backward()
Returns backward transition relation.
BddTrans_get_forward()
Returns forward transition relation.
BddTrans_get_forward_image_state()
Computes the forward image by existentially quantifying over state variables only.
BddTrans_get_forward_image_state_input()
Computes the forward image by existentially quantifying over both state and input variables.
BddTrans_get_backward_image_state()
Computes the backward image by existentially quantifying over state variables only.
BddTrans_get_backward_image_state_input()
Computes the backward image by existentially quantifying over both state and input variables.
BddTrans_get_k_forward_image_state()
Computes the k forward image by existentially quantifying over state variables only.
BddTrans_get_k_forward_image_state_input()
Computes the k forward image by existentially quantifying over both state and input variables.
BddTrans_get_k_backward_image_state()
Computes the k backward image by existentially quantifying over state variables only.
BddTrans_get_k_backward_image_state_input()
Computes the k backward image by existentially quantifying over both state and input variables.
BddTrans_print_short_info()
Prints short info associated to a Trans
bdd_trans_copy()
Copy constructor
bdd_trans_debug_partitioned()
Checks the equality between given Monolithic and Partitioned transition relations.

Cluster.c

Routines related to clusters of transition relation.

By: Roberto Cavada

This file conains the definition of Cluster and all derived classes

Cluster_create()
The "Cluster" class constructor.
Cluster_is_equal()
Checks if two clusters are equal
Cluster_get_trans()
Retrives the clusterized transition relation of the self .
Cluster_set_trans()
Sets the transition relation inside the cluster
Cluster_get_quantification_state_input()
Returns a pointer to the list of variables (both state and input vars) to be quantified.
Cluster_set_quantification_state_input()
Sets the list of variables (both state and input vars) to be quantified inside the cluster.
Cluster_get_quantification_state()
Returns a pointer to the list of variables (state vars only) to be quantified
Cluster_set_quantification_state()
Sets the list of variables (state vars only) to be quantified inside the cluster
ClusterIwls95_create()
"ClusterIwls95" Class constructor.
ClusterIwls95_get_benefit()
Returns the value of the "benifit" variable.
cluster_init()
Initializes the cluster with default values.
cluster_deinit()
Deinitializes the cluster.
cluster_finalize()
Finalize a cluster.
cluster_copy()
Copies the given cluster.
cluster_copy_aux()
It helps to copy the given cluster.
cluster_iwls95_init()
Initializes Iwls95 cluster.
cluster_iwls95_deinit()
Deinitialized Iwls95 cluster.
cluster_iwls95_finalize()
Finalize iwls95 cluster.
cluster_iwls95_copy()
Copies iwls95 cluster.
cluster_iwls95_copy_aux()
It helps to copy iwls95 cluster.

ClusterList.c

Routines related to list of transition clusters.

By: Roberto Cavada

This file contains ClusterList class and modules related to it.

()
Number of allowed clusters whose BDD size is below the partitioning threshold while using affinity.
ClusterList_create()
Class ClusterList Constructor.
ClusterList_destroy()
ClusterList Class dectructor.
ClusterList_copy()
Returns a copy of the "self".
ClusterList_reverse()
Reverses the list of clusters.
ClusterList_remove_cluster()
Deletes every occurrence of the given cluster from the self.
ClusterList_apply_monolithic()
It returns a monolithic transition cluster corresponding to the cluster list of the "self".
ClusterList_apply_threshold()
It returns a threshold based cluster list corresponding to the cluster list of the "self".
ClusterList_length()
Returns the number of the clusters stored in "self".
ClusterList_prepend_cluster()
Prepends given cluster to the list
ClusterList_append_cluster()
Appends given cluster to the list
ClusterList_begin()
Returns an Iterator to iterate the self.
ClusterList_get_cluster()
Returns the cluster kept at the position given by the iterator
ClusterList_set_cluster()
Sets the cluster of the "self" at the position given by iterator "iter" to cluster "cluster".
ClusterList_build_schedule()
It builds the quantification schedule of the variables inside the clusters of the "self".
ClusterList_get_image_state()
Computes the image of the given bdd "s" using the clusters of the "self" while quantifying state vars only.
ClusterList_get_image_state_input()
Computes the image of the given bdd "s" using the clusters of the "self" while quantifying both state and input vars.
ClusterList_get_k_image_state()
Computes the k image of the given bdd "s" using the clusters of the "self" while quantifying state vars only.
ClusterList_get_k_image_state_input()
Computes the k image of the given bdd "s" using the clusters of the "self" while quantifying both state and input vars.
ClusterList_get_monolithic_bdd()
Returns the monolithic bdd corresponding to the "self".
ClusterList_get_clusters_cube()
Computes the cube of the set of support of all the clusters
ClusterList_apply_iwls95_partition()
Orders the clusters according to the IWLS95 algo. to perform image computation.
ClusterList_apply_synchronous_product()
Performs the synchronous product between two cluster lists
ClusterList_print_short_info()
Prints size of each cluster of the "self"
ClusterListIterator_next()
Use to iterate a list
ClusterListIterator_is_end()
Use to check if iterator is at the end of list
ClusterList_check_equality()
Returns true if two clusters list are logically equivalent
ClusterList_check_schedule()
Check the schedule for self. Call after you applied the schedule
()
Computes the image from a given set of states "s".
()
Use to compute the k image from a given set of states "s".
cluster_list_iwls95_order()
It orders a copy of the "self" according to the IWLS95 algorithm and returns the copy.
cluster_list_apply_iwls95_info()
It applies iwls95 info passed as parameters to a copy of the "self" and returns it.
cluster_list_get_supp_Q_Ci()
Computes the set Supp_Q_Ci.
clusterlist_build_schedule_recur()
Helps to compute the quantification schedule
cluster_list_destroy_weak()
private function to weakly destroy the "self"
cluster_list_copy()
Dups a given list of clusters, copying clusters depending on the value in weak_copy
cluster_list_apply_threshold()
Forms the clusters of relations based on BDD size heuristic
cluster_list_apply_threshold_affinity()
OPTIMIZED affinity clustering
clusterlist_affinity_move_clusters()
Copy over threshold clusters in result list or in support list & heap.
()
Compute the Affinity of two BDD clusters.
compute_bdd_affinity()
Compute the Affinity of two BDD clusters.
support_list_entry_create()
Allocates an af_support_list_entry
af_support_pair_create()
Allocates a pair
support_list_heap_add()
Add a new entry in support list and new pairs in heap.
support_list_del()
Delete a cluster in support list.

ClusterOptions.c

Routines related to "ClusterOptions" class.

By: Roberto Cavada

This file contains class "ClusterOptions" which stores various options available for Clusters like threshold, affinity, preorder and options related to Iwls95 algo.

ClusterOptions_create()
"ClusterOptions" class constructor.
ClusterOptions_destroy()
ClusterOption class destructor.
ClusterOptions_get_threshold()
Returns the threshold field.
ClusterOptions_is_affinity()
Checks whether Affinity is enabled.
ClusterOptions_clusters_appended()
Returns true if clusters must be appended, false if clusters must be prepended
ClusterOptions_is_iwls95_preorder()
Checks whether preordering is enabled.
ClusterOptions_get_cluster_size()
Returns the cluster_size field.
ClusterOptions_get_w1()
Retrieves the parameter w1.
ClusterOptions_get_w2()
Retrieves the parameter w2.
ClusterOptions_get_w3()
Retrieves the parameter w3.
ClusterOptions_get_w4()
Retrieves the parameter w4.
ClusterOptions_print()
Prints all the cluster options inside the specified file.

Last updated on 2011/04/06 21h:12