NuSMV/code/nusmv/core/trans/bdd/Cluster.h

Go to the documentation of this file.

/* ---------------------------------------------------------------------------


  This file is part of the ``trans.bdd'' package of NuSMV version 2. 
  Copyright (C) 2003 by FBK-irst. 

  NuSMV version 2 is free software; you can redistribute it and/or 
  modify it under the terms of the GNU Lesser General Public 
  License as published by the Free Software Foundation; either 
  version 2 of the License, or (at your option) any later version.

  NuSMV version 2 is distributed in the hope that it will be useful, 
  but WITHOUT ANY WARRANTY; without even the implied warranty of 
  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU 
  Lesser General Public License for more details.

  You should have received a copy of the GNU Lesser General Public 
  License along with this library; if not, write to the Free Software 
  Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307  USA.

  For more information on NuSMV see <http://nusmv.fbk.eu>
  or email to <nusmv-users@fbk.eu>.
  Please report bugs to <nusmv-users@fbk.eu>.

  To contact the NuSMV development board, email to <nusmv@fbk.eu>. 

-----------------------------------------------------------------------------*/

#ifndef __NUSMV_CORE_TRANS_BDD_CLUSTER_H__
#define __NUSMV_CORE_TRANS_BDD_CLUSTER_H__

#include "nusmv/core/trans/bdd/ClusterOptions.h"
#include "nusmv/core/utils/object.h" 
#include "nusmv/core/dd/dd.h"

typedef struct Cluster_TAG*  Cluster_ptr;

typedef struct ClusterIwls95_TAG*  ClusterIwls95_ptr;

#define CLUSTER(x)    \
          ((Cluster_ptr) x)

#define CLUSTER_CHECK_INSTANCE(x)  \
          (nusmv_assert(CLUSTER(x) != CLUSTER(NULL)))

#define CLUSTER_IWLS95(x)    \
          ((ClusterIwls95_ptr) x)

#define CLUSTER_IWLS95_CHECK_INSTANCE(x)  \
          (nusmv_assert(CLUSTER_IWLS95(x) != CLUSTER_IWLS95(NULL)))



/* ---------------------------------------------------------------------- */
/*    Public interface                                                    */
/* ---------------------------------------------------------------------- */

Cluster_ptr Cluster_create(DDMgr_ptr dd);

boolean 
Cluster_is_equal(const Cluster_ptr self, const Cluster_ptr other);

bdd_ptr Cluster_get_trans(const Cluster_ptr self);

void 
Cluster_set_trans(Cluster_ptr self, DDMgr_ptr dd, bdd_ptr current);

bdd_ptr 
Cluster_get_quantification_state_input(const Cluster_ptr self);

void 
Cluster_set_quantification_state_input(Cluster_ptr self, 
                                       DDMgr_ptr dd, bdd_ptr new_val);

bdd_ptr 
Cluster_get_quantification_state(const Cluster_ptr self);

void 
Cluster_set_quantification_state(Cluster_ptr self, 
                                 DDMgr_ptr dd, bdd_ptr new_val);


/* ClusterIwls95 inherits from Cluster: */

ClusterIwls95_ptr 
ClusterIwls95_create(DDMgr_ptr dd, 
                     const ClusterOptions_ptr trans_options, 
                     const double v_c, 
                     const double w_c, 
                     const double x_c, 
                     const double y_c, 
                     const double z_c, 
                     const double min_c, 
                     const double max_c);

double 
ClusterIwls95_get_benefit(const ClusterIwls95_ptr self);


#endif /* __NUSMV_CORE_TRANS_BDD_CLUSTER_H__ */

---