NuSMV/code/nusmv/core/trans/bdd/BddTrans.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_BDD_TRANS_H__
#define __NUSMV_CORE_TRANS_BDD_BDD_TRANS_H__

#include "nusmv/core/trans/generic/GenericTrans.h"

#include "nusmv/core/trans/bdd/ClusterList.h"
#include "nusmv/core/trans/bdd/ClusterOptions.h"

#include "nusmv/core/dd/dd.h"

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

typedef struct BddTrans_TAG* BddTrans_ptr;

#define BDD_TRANS(x)  \
        ((BddTrans_ptr) x)

#define BDD_TRANS_CHECK_INSTANCE(x)  \
        (nusmv_assert(BDD_TRANS(x) != BDD_TRANS(NULL)))


typedef enum TransImageKind_TAG {
  TRANS_IMAGE_FORWARD_STATE = 0,
  TRANS_IMAGE_FORWARD_STATE_INPUT = 1,
  TRANS_IMAGE_BACKWARD_STATE = 2,
  TRANS_IMAGE_BACKWARD_STATE_INPUT = 3
} TransImageKind;



/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

#define TRANS_IMAGE_IS_FORWARD(kind) (!((kind) >> 1))

#define TRANS_IMAGE_IS_STATE_ONLY(kind) (!((kind) & 1))

/* ---------------------------------------------------------------------- */
/* Enable this to auto-check trans after creation                         */
#if 0
# define TRANS_DEBUG_THRESHOLD
#endif
/* ---------------------------------------------------------------------- */

/*---------------------------------------------------------------------------*/
/* Function prototypes                                                       */
/*---------------------------------------------------------------------------*/

BddTrans_ptr
BddTrans_create(DDMgr_ptr dd_manager,
                const ClusterList_ptr clusters_bdd,
                bdd_ptr state_vars_cube,
                bdd_ptr input_vars_cube,
                bdd_ptr next_state_vars_cube,
                const TransType trans_type,
                const ClusterOptions_ptr cl_options);

BddTrans_ptr
BddTrans_generic_create(
                        const NuSMVEnv_ptr env,
                        const TransType trans_type,
                        void* transition,
                        void* (*copy)(void* tranistion),
                        void  (*destroy)(void* tranistion),
                        bdd_ptr (*compute_image)(void* tranistion,
                                                 bdd_ptr bdd, TransImageKind kind),
                        bdd_ptr (*compute_k_image)(void* tranistion,
                                                   bdd_ptr bdd, int k,
                                                   TransImageKind kind),
                        bdd_ptr (*get_monolithic_bdd)(void* tranistion),
                        void (*synchronous_product)(void* tranistion1,
                                                    void* const transition2),
                        void (*print_short_info)(void* tranistion, FILE* file),
                        ClusterList_ptr (*trans_get_clusterlist)(void* transition));

void
BddTrans_apply_synchronous_product(BddTrans_ptr self,
                                   const BddTrans_ptr other);

bdd_ptr
BddTrans_get_monolithic_bdd(const BddTrans_ptr self);

ClusterList_ptr
BddTrans_get_clusterlist(const BddTrans_ptr self);

bdd_ptr
BddTrans_get_forward_image_state(const BddTrans_ptr self, bdd_ptr s);

bdd_ptr
BddTrans_get_forward_image_state_input(const BddTrans_ptr self,
                                       bdd_ptr s);

bdd_ptr
BddTrans_get_backward_image_state(const BddTrans_ptr self, bdd_ptr s);

bdd_ptr
BddTrans_get_backward_image_state_input(const BddTrans_ptr self,
                                        bdd_ptr s);

bdd_ptr
BddTrans_get_k_forward_image_state(const BddTrans_ptr self,
                                   bdd_ptr s, int k);

bdd_ptr
BddTrans_get_k_forward_image_state_input(const BddTrans_ptr self,
                                         bdd_ptr s, int k);

bdd_ptr
BddTrans_get_k_backward_image_state(const BddTrans_ptr self,
                                    bdd_ptr s, int k);

bdd_ptr
BddTrans_get_k_backward_image_state_input(const BddTrans_ptr self,
                                            bdd_ptr s, int k);

void BddTrans_print_short_info(const BddTrans_ptr self,
                                      FILE* file);



#endif /* __NUSMV_CORE_TRANS_BDD_BDD_TRANS_H__ */

---