NuSMV Developers Manual: NuSMV/code/nusmv/core/fsm/bdd/bddInt.h Source File

00001 /* ---------------------------------------------------------------------------
00002 
00003 
00004   This file is part of the ``bdd_fsm'' package of NuSMV version 2. 
00005   Copyright (C) 2003 by FBK-irst. 
00006 
00007   NuSMV version 2 is free software; you can redistribute it and/or 
00008   modify it under the terms of the GNU Lesser General Public 
00009   License as published by the Free Software Foundation; either 
00010   version 2 of the License, or (at your option) any later version.
00011 
00012   NuSMV version 2 is distributed in the hope that it will be useful, 
00013   but WITHOUT ANY WARRANTY; without even the implied warranty of 
00014   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU 
00015   Lesser General Public License for more details.
00016 
00017   You should have received a copy of the GNU Lesser General Public 
00018   License along with this library; if not, write to the Free Software 
00019   Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307  USA.
00020 
00021   For more information on NuSMV see <http://nusmv.fbk.eu>
00022   or email to <nusmv-users@fbk.eu>.
00023   Please report bugs to <nusmv-users@fbk.eu>.
00024 
00025   To contact the NuSMV development board, email to <nusmv@fbk.eu>. 
00026 
00027 -----------------------------------------------------------------------------*/
00028 
00039 #ifndef __NUSMV_CORE_FSM_BDD_BDD_INT_H__
00040 #define __NUSMV_CORE_FSM_BDD_BDD_INT_H__
00041 
00042 #include "nusmv/core/dd/dd.h"
00043 #include "nusmv/core/opt/opt.h"
00044 
00045 /* members are public from within the bdd fsm */
00046 typedef struct BddFsmCache_TAG 
00047 {
00048   /* for sharing families (i.e. compatible instances): */
00049   unsigned int* family_counter;
00050   
00051   /* dd manager */
00052   DDMgr_ptr dd;
00053   
00054   /* cached values */
00055   BddStates  fair_states;
00056   BddStatesInputs fair_states_inputs;
00057   BddStates  revfair_states;
00058   BddStatesInputs revfair_states_inputs;
00059 
00060   /* interface to this structure is private */
00061   struct BddFsmReachable_TAG
00062   {
00063     boolean computed;
00064     BddStates* layers;   /* array of bdds */
00065     int diameter;
00066     BddStates reachable_states; /* Used to hold the bdd representing the
00067                                    whole set of reachable states of the
00068                                    BddFsm.  These may be computed for
00069                                    example by Guided Reachability */
00070   } reachable;
00071 
00072   BddStates successor_states;
00073   BddStates not_successor_states;
00074   BddStates deadlock_states;
00075   BddStatesInputs legal_state_input; 
00076   BddStatesInputs monolithic_trans;
00077 
00078 } BddFsmCache;
00079 
00086 typedef struct BddFsmCache_TAG* BddFsmCache_ptr;
00087 
00093 #define BDD_FSM_CACHE(x) \
00094          ( (BddFsmCache_ptr) x )
00095 
00101 #define BDD_FSM_CACHE_CHECK_INSTANCE(x) \
00102          ( nusmv_assert(BDD_FSM_CACHE(x) != BDD_FSM_CACHE(NULL)) )
00103 
00109 #define CACHE_SET(member, value) \
00110          (self->cache->member = value)
00111 
00117 #define CACHE_GET(member) \
00118          (self->cache->member)
00119 
00125 #define CACHE_SET_BDD(member, value) \
00126          (self->cache->member = bdd_dup(value))
00127 
00133 #define CACHE_GET_BDD(member) \
00134          (bdd_dup(self->cache->member))
00135 
00141 #define CACHE_IS_EQUAL(member, value) \
00142          (self->cache->member == value)
00143 
00150 BddFsmCache_ptr BddFsmCache_create(DDMgr_ptr dd);
00151 
00158 void BddFsmCache_destroy(BddFsmCache_ptr self);
00159 
00168 BddFsmCache_ptr 
00169 BddFsmCache_hard_copy(const BddFsmCache_ptr self);
00170 
00181 BddFsmCache_ptr 
00182 BddFsmCache_soft_copy(const BddFsmCache_ptr self);
00183 
00191 void 
00192 BddFsmCache_copy_reachables(BddFsmCache_ptr self, 
00193                             const BddFsmCache_ptr other);
00194 
00205 void BddFsmCache_set_reachable_states(BddFsmCache_ptr self,
00206                                              BddStates reachable);
00207 
00219 void BddFsmCache_set_reachables(BddFsmCache_ptr self, 
00220                                        node_ptr   layers_list, 
00221                                        const int  diameter,
00222                                        boolean completed);
00223 
00238 void 
00239 BddFsmCache_reset_not_reusable_fields_after_product(BddFsmCache_ptr self);
00240 
00241 #endif /* __NUSMV_CORE_FSM_BDD_BDD_INT_H__ */