00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00038 #ifndef __NUSMV_CORE_TRANS_BDD_CLUSTER_H__
00039 #define __NUSMV_CORE_TRANS_BDD_CLUSTER_H__
00040
00041 #include "nusmv/core/trans/bdd/ClusterOptions.h"
00042 #include "nusmv/core/utils/object.h"
00043 #include "nusmv/core/dd/dd.h"
00044
00070 typedef struct Cluster_TAG* Cluster_ptr;
00071
00079 typedef struct ClusterIwls95_TAG* ClusterIwls95_ptr;
00080
00086 #define CLUSTER(x) \
00087 ((Cluster_ptr) x)
00088
00094 #define CLUSTER_CHECK_INSTANCE(x) \
00095 (nusmv_assert(CLUSTER(x) != CLUSTER(NULL)))
00096
00102 #define CLUSTER_IWLS95(x) \
00103 ((ClusterIwls95_ptr) x)
00104
00110 #define CLUSTER_IWLS95_CHECK_INSTANCE(x) \
00111 (nusmv_assert(CLUSTER_IWLS95(x) != CLUSTER_IWLS95(NULL)))
00112
00113
00114
00115
00116
00117
00118
00127 Cluster_ptr Cluster_create(DDMgr_ptr dd);
00128
00136 boolean
00137 Cluster_is_equal(const Cluster_ptr self, const Cluster_ptr other);
00138
00146 bdd_ptr Cluster_get_trans(const Cluster_ptr self);
00147
00155 void
00156 Cluster_set_trans(Cluster_ptr self, DDMgr_ptr dd, bdd_ptr current);
00157
00167 bdd_ptr
00168 Cluster_get_quantification_state_input(const Cluster_ptr self);
00169
00177 void
00178 Cluster_set_quantification_state_input(Cluster_ptr self,
00179 DDMgr_ptr dd, bdd_ptr new_val);
00180
00188 bdd_ptr
00189 Cluster_get_quantification_state(const Cluster_ptr self);
00190
00198 void
00199 Cluster_set_quantification_state(Cluster_ptr self,
00200 DDMgr_ptr dd, bdd_ptr new_val);
00201
00202
00203
00204
00217 ClusterIwls95_ptr
00218 ClusterIwls95_create(DDMgr_ptr dd,
00219 const ClusterOptions_ptr trans_options,
00220 const double v_c,
00221 const double w_c,
00222 const double x_c,
00223 const double y_c,
00224 const double z_c,
00225 const double min_c,
00226 const double max_c);
00227
00234 double
00235 ClusterIwls95_get_benefit(const ClusterIwls95_ptr self);
00236
00237
00238 #endif