NuSMV/code/nusmv/core/trans/bdd/ClusterList.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_LIST_H__
#define __NUSMV_CORE_TRANS_BDD_CLUSTER_LIST_H__

#include "nusmv/core/trans/bdd/Cluster.h"
#include "nusmv/core/dd/dd.h"
#include "nusmv/core/node/node.h"

typedef struct ClusterList_TAG* ClusterList_ptr;

typedef node_ptr ClusterListIterator_ptr;

#define CLUSTER_LIST(x)  \
        ((ClusterList_ptr) x)

#define CLUSTER_LIST_CHECK_INSTANCE(x)  \
        (nusmv_assert(CLUSTER_LIST(x) != CLUSTER_LIST(NULL)))

#define CLUSTER_LIST_ITERATOR(x) \
        ((ClusterListIterator_ptr) x)

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

/*
   This define controls the way a cluster is put into the cluster list
   If this macro is not defined, clusters will be appended instead of
   being prepended.
*/
/*#define CLUSTER_LIST_PREPEND_CLUSTER*/
#undef CLUSTER_LIST_PREPEND_CLUSTER

/*
   This decides how the affinity among two BDDs is computed. If this
   symbol is defined, then affinity is the ratio between the number of
   shared variables and the number of the union of all variables
   (intersection/union) as as suggested by Moon, Hachtel, Somenzi in
   BBT paper. Otherwise a variation to the previous one is used: this
   is possibly more expensive than the previous one.
*/

#define MHS_AFFINITY_DEFINITION

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

ClusterList_ptr ClusterList_create(DDMgr_ptr dd);

void ClusterList_destroy(ClusterList_ptr self);

ClusterList_ptr ClusterList_copy(const ClusterList_ptr self);

ClusterListIterator_ptr
ClusterList_begin(const ClusterList_ptr self);

DDMgr_ptr
ClusterList_get_dd_manager(const ClusterList_ptr self);

Cluster_ptr
ClusterList_get_cluster(const ClusterList_ptr self,
                        const ClusterListIterator_ptr iter);

void ClusterList_set_cluster(ClusterList_ptr self,
                                    const ClusterListIterator_ptr iter,
                                    Cluster_ptr cluster);

int ClusterList_length(const ClusterList_ptr self);

void
ClusterList_prepend_cluster(ClusterList_ptr self, Cluster_ptr cluster);

void
ClusterList_append_cluster(ClusterList_ptr self, Cluster_ptr cluster);

ClusterListIterator_ptr
ClusterListIterator_next(const ClusterListIterator_ptr self);

boolean
ClusterListIterator_is_end(const ClusterListIterator_ptr self);

void ClusterList_reverse(ClusterList_ptr self);

int
ClusterList_remove_cluster(ClusterList_ptr self, Cluster_ptr cluster);

ClusterList_ptr
ClusterList_apply_monolithic(const ClusterList_ptr self);

ClusterList_ptr
ClusterList_apply_threshold(const ClusterList_ptr self,
                            const ClusterOptions_ptr cl_options);

ClusterList_ptr
ClusterList_apply_iwls95_partition(const ClusterList_ptr self,
                                   bdd_ptr state_vars_cube,
                                   bdd_ptr input_vars_cube,
                                   bdd_ptr next_state_vars_cube,
                                   const ClusterOptions_ptr cl_options);

void
ClusterList_apply_synchronous_product(ClusterList_ptr self,
                                      const ClusterList_ptr other);

bdd_ptr
ClusterList_get_monolithic_bdd(const ClusterList_ptr self);

bdd_ptr
ClusterList_get_clusters_cube(const ClusterList_ptr self);

void
ClusterList_build_schedule(ClusterList_ptr self,
                           bdd_ptr state_vars_cube,
                           bdd_ptr input_vars_cube);

bdd_ptr
ClusterList_get_image_state(const ClusterList_ptr self, bdd_ptr s);

bdd_ptr
ClusterList_get_image_state_input(const ClusterList_ptr self, bdd_ptr s);

bdd_ptr
ClusterList_get_k_image_state(const ClusterList_ptr self, bdd_ptr s, int k);

bdd_ptr
ClusterList_get_k_image_state_input(const ClusterList_ptr self, bdd_ptr s, int k);

void
ClusterList_print_short_info(const ClusterList_ptr self, FILE* file);

boolean ClusterList_check_equality(const ClusterList_ptr self,
                                          const ClusterList_ptr other);

boolean ClusterList_check_schedule(const ClusterList_ptr self);


#endif /* __NUSMV_CORE_TRANS_BDD_CLUSTER_LIST_H__ */

---