-
BddTrans_apply_synchronous_product()
- Performs the synchronous product between two trans
-
BddTrans_create()
- Builds the transition relation from a provided
cluster list.
-
BddTrans_get_backward_image_state_input()
- Computes the backward 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_forward_image_state_input()
- Computes the forward image by existentially quantifying
over both state and input variables.
-
BddTrans_get_forward_image_state()
- Computes the forward 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_get_k_backward_image_state()
- Computes the k backward 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_forward_image_state()
- Computes the k forward image by existentially quantifying
over state variables only.
-
BddTrans_get_monolithic_bdd()
- Returns a monolithic BDD representing the whole
transition relation.
-
BddTrans_print_short_info()
- Prints short info associated to a Trans
-
ClusterIwls95_create()
- "ClusterIwls95" Class constructor.
-
ClusterIwls95_get_benefit()
- Returns the value of the "benifit" variable.
-
ClusterListIterator_is_end()
- Use to check if iterator is at the end of list
-
ClusterListIterator_next()
- Use to iterate a list
-
ClusterList_append_cluster()
- Appends given cluster to the list
-
ClusterList_apply_iwls95_partition()
- Orders the clusters according to the IWLS95 algo. to
perform image computation.
-
ClusterList_apply_monolithic()
- It returns a monolithic transition cluster corresponding
to the cluster list of the "self".
-
ClusterList_apply_synchronous_product()
- Performs the synchronous product between two cluster lists
-
ClusterList_apply_threshold()
- It returns a threshold based cluster list corresponding
to the cluster list of the "self".
-
ClusterList_begin()
- Returns an Iterator to iterate the self.
-
ClusterList_build_schedule()
- It builds the quantification schedule of the variables
inside the clusters of the "self".
-
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
-
ClusterList_copy()
- Returns a copy of the "self".
-
ClusterList_create()
- Class ClusterList Constructor.
-
ClusterList_destroy()
- ClusterList Class dectructor.
-
ClusterList_get_clusters_cube()
- Computes the cube of the set of support of all the clusters
-
ClusterList_get_cluster()
- Returns the cluster kept at the position given by the
iterator
-
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_image_state()
- Computes the 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_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_monolithic_bdd()
- Returns the monolithic bdd corresponding to the "self".
-
ClusterList_length()
- Returns the number of the clusters stored in "self".
-
ClusterList_prepend_cluster()
- Prepends given cluster to the list
-
ClusterList_print_short_info()
- Prints size of each cluster of the "self"
-
ClusterList_remove_cluster()
- Deletes every occurrence of the given cluster from the
self.
-
ClusterList_reverse()
- Reverses the list of clusters.
-
ClusterList_set_cluster()
- Sets the cluster of the "self" at the position given by
iterator "iter" to cluster "cluster".
-
ClusterOptions_clusters_appended()
- Returns true if clusters must be appended, false if
clusters must be prepended
-
ClusterOptions_create()
- "ClusterOptions" class constructor.
-
ClusterOptions_destroy()
- ClusterOption class destructor.
-
ClusterOptions_get_cluster_size()
- Returns the cluster_size field.
-
ClusterOptions_get_threshold()
- Returns the threshold 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_is_affinity()
- Checks whether Affinity is enabled.
-
ClusterOptions_is_iwls95_preorder()
- Checks whether preordering is enabled.
-
ClusterOptions_print()
- Prints all the cluster options inside the specified file.
-
Cluster_create()
- The "Cluster" class constructor.
-
Cluster_get_quantification_state_input()
- Returns a pointer to the list of variables (both state
and input vars) to be quantified.
-
Cluster_get_quantification_state()
- Returns a pointer to the list of variables (state vars
only) to be quantified
-
Cluster_get_trans()
- Retrives the clusterized transition relation of the self
.
-
Cluster_is_equal()
- Checks if two clusters are equal
-
Cluster_set_quantification_state_input()
- Sets the list of variables (both state and input vars) to
be quantified inside the cluster.
-
Cluster_set_quantification_state()
- Sets the list of variables (state vars only) to be
quantified inside the cluster
-
Cluster_set_trans()
- Sets the transition relation inside the cluster
-
af_support_pair_create()
- Allocates a pair
-
bdd_trans_clusterlist_compute_image()
- Implementation of 'compute_image' parameter of
BddTrans_generic_create having 'transition' of type ClusterBasedTrans_ptr
-
bdd_trans_clusterlist_compute_k_image()
- Implementation of 'compute_k_image' parameter of
BddTrans_generic_create having 'transition' of type ClusterBasedTrans_ptr
-
bdd_trans_clusterlist_copy()
- Implementation of 'copy' parameter of
BddTrans_generic_create having 'transition' of type ClusterBasedTrans_ptr
-
bdd_trans_clusterlist_destroy()
- Implementation of 'destroy' parameter of
BddTrans_generic_create having 'transition' of type ClusterBasedTrans_ptr
-
bdd_trans_clusterlist_get_monolithic_bdd()
- Implementation of 'get_monolithic_bdd' parameter of
BddTrans_generic_create having 'transition' of type ClusterBasedTrans_ptr
-
bdd_trans_clusterlist_print_short_info()
- Implementation of 'print_short_info' parameter of
BddTrans_generic_create having 'transition' of type ClusterBasedTrans_ptr
-
bdd_trans_clusterlist_synchronous_product()
- Implementation of 'synchronous_product' parameter of
BddTrans_generic_create having 'transition' of type ClusterBasedTrans_ptr
-
bdd_trans_copy()
- Copy constructor
-
bdd_trans_debug_partitioned()
- Checks the equality between given Monolithic and
Partitioned transition relations.
-
cluster_copy_aux()
- It helps to copy the given cluster.
-
cluster_copy()
- Copies the given cluster.
-
cluster_deinit()
- Deinitializes the cluster.
-
cluster_finalize()
- Finalize a cluster.
-
cluster_init()
- Initializes the cluster with default values.
-
cluster_iwls95_copy_aux()
- It helps to copy iwls95 cluster.
-
cluster_iwls95_copy()
- Copies iwls95 cluster.
-
cluster_iwls95_deinit()
- Deinitialized Iwls95 cluster.
-
cluster_iwls95_finalize()
- Finalize iwls95 cluster.
-
cluster_iwls95_init()
- Initializes Iwls95 cluster.
-
cluster_list_apply_iwls95_info()
- It applies iwls95 info passed as parameters to a copy of
the "self" and returns it.
-
cluster_list_apply_threshold_affinity()
- OPTIMIZED affinity clustering
-
cluster_list_apply_threshold()
- Forms the clusters of relations based on BDD
size heuristic
-
cluster_list_copy()
- Dups a given list of clusters, copying clusters
depending on the value in weak_copy
-
cluster_list_destroy_weak()
- private function to weakly destroy the "self"
-
cluster_list_get_supp_Q_Ci()
- Computes the set Supp_Q_Ci.
-
cluster_list_iwls95_order()
- It orders a copy of the "self" according to the IWLS95
algorithm and returns the copy.
-
clusterlist_affinity_move_clusters()
- Copy over threshold clusters in result list or in support
list & heap.
-
clusterlist_build_schedule_recur()
- Helps to compute the quantification schedule
-
compute_bdd_affinity()
- Compute the Affinity of two BDD clusters.
-
support_list_del()
- Delete a cluster in support list.
-
support_list_entry_create()
- Allocates an af_support_list_entry
-
support_list_heap_add()
- Add a new entry in support list and new pairs in heap.
-
()
- Builds the transition relation
-
()
- Compute the Affinity of two BDD clusters.
-
()
- Computes the image from a given set of states
"s".
-
()
- Number of allowed clusters whose BDD size is below the
partitioning threshold while using affinity.
-
()
- Use to compute the k image from a given set of states
"s".
Last updated on 2012/11/18 14h:37