NuSMV/code/nusmv/core/fsm/bdd/FairnessList.h
Go to the documentation of this file.00001 /* --------------------------------------------------------------------------- 00002 00003 00004 This file is part of the ``fsm.bdd'' 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 00044 #ifndef __NUSMV_CORE_FSM_BDD_FAIRNESS_LIST_H__ 00045 #define __NUSMV_CORE_FSM_BDD_FAIRNESS_LIST_H__ 00046 00047 #include "nusmv/core/fsm/bdd/bdd.h" 00048 #include "nusmv/core/utils/object.h" /* for object inheritance support */ 00049 #include "nusmv/core/utils/utils.h" 00050 #include "nusmv/core/node/node.h" 00051 #include "nusmv/core/dd/dd.h" 00052 00053 /* ---------------------------------------------------------------------- */ 00054 /* Base type, derives from Object */ 00055 00062 typedef struct FairnessList_TAG* FairnessList_ptr; 00063 00069 #define FAIRNESS_LIST(x) \ 00070 ((FairnessList_ptr) x) 00071 00077 #define FAIRNESS_LIST_CHECK_INSTANCE(self) \ 00078 (nusmv_assert( FAIRNESS_LIST(self) != FAIRNESS_LIST(NULL) )) 00079 /* ---------------------------------------------------------------------- */ 00080 00081 00082 00083 /* ---------------------------------------------------------------------- */ 00084 /* Iterator for the list */ 00085 00091 typedef node_ptr FairnessListIterator_ptr; 00092 /* ---------------------------------------------------------------------- */ 00093 00094 00095 00096 /* ---------------------------------------------------------------------- */ 00097 /* Derives from FairnessList */ 00098 00105 typedef struct JusticeList_TAG* JusticeList_ptr; 00106 00112 #define JUSTICE_LIST(x) \ 00113 ((JusticeList_ptr) x) 00114 00120 #define JUSTICE_LIST_CHECK_INSTANCE(self) \ 00121 (nusmv_assert( JUSTICE_LIST(self) != JUSTICE_LIST(NULL) )) 00122 /* ---------------------------------------------------------------------- */ 00123 00124 00125 /* ---------------------------------------------------------------------- */ 00126 /* Derives from FairnessList */ 00127 00134 typedef struct CompassionList_TAG* CompassionList_ptr; 00135 00141 #define COMPASSION_LIST(x) \ 00142 ((CompassionList_ptr) x) 00143 00149 #define COMPASSION_LIST_CHECK_INSTANCE(self) \ 00150 (nusmv_assert( COMPASSION_LIST(self) != COMPASSION_LIST(NULL) )) 00151 /* ---------------------------------------------------------------------- */ 00152 00153 00154 00155 /* ---------------------------------------------------------------------- */ 00156 /* Public methods: */ 00157 /* ---------------------------------------------------------------------- */ 00158 00165 FairnessList_ptr FairnessList_create(DDMgr_ptr dd_manager); 00166 00173 boolean FairnessList_is_empty(const FairnessList_ptr self); 00174 00181 FairnessListIterator_ptr 00182 FairnessList_begin(const FairnessList_ptr self); 00183 00190 boolean 00191 FairnessListIterator_is_end(const FairnessListIterator_ptr self); 00192 00199 FairnessListIterator_ptr 00200 FairnessListIterator_next(const FairnessListIterator_ptr self); 00201 00202 00203 /* Justice */ 00204 00211 JusticeList_ptr JusticeList_create(DDMgr_ptr dd_manager); 00212 00219 BddStates 00220 JusticeList_get_p(const JusticeList_ptr self, 00221 const FairnessListIterator_ptr iter); 00222 00230 void JusticeList_append_p(JusticeList_ptr self, BddStates p); 00231 00241 void 00242 JusticeList_apply_synchronous_product(JusticeList_ptr self, 00243 const JusticeList_ptr other); 00244 00245 /* Compassion */ 00246 00253 CompassionList_ptr CompassionList_create(DDMgr_ptr dd_manager); 00254 00261 BddStates 00262 CompassionList_get_p(const CompassionList_ptr self, 00263 const FairnessListIterator_ptr iter); 00264 00271 BddStates 00272 CompassionList_get_q(const CompassionList_ptr self, 00273 const FairnessListIterator_ptr iter); 00274 00282 void CompassionList_append_p_q(CompassionList_ptr self, 00283 BddStates p, BddStates q); 00284 00294 void 00295 CompassionList_apply_synchronous_product(CompassionList_ptr self, 00296 const CompassionList_ptr other); 00297 00298 #endif /* __NUSMV_CORE_FSM_BDD_FAIRNESS_LIST_H__ */
