state.hh 8.66 KB
 Alexandre Duret-Lutz committed Jan 17, 2013 1 2 3 ``````// -*- coding: utf-8 -*- // Copyright (C) 2009, 2011, 2013 Laboratoire de Recherche et // Développement de l'Epita (LRDE). `````` Guillaume Sadegh committed Jan 24, 2010 4 ``````// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 `````` Alexandre Duret-Lutz committed Jan 17, 2013 5 ``````// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université `````` Guillaume Sadegh committed Oct 01, 2009 6 ``````// Pierre et Marie Curie. `````` Alexandre Duret-Lutz committed Nov 21, 2003 7 8 9 10 11 ``````// // This file is part of Spot, a model checking library. // // Spot is free software; you can redistribute it and/or modify it // under the terms of the GNU General Public License as published by `````` Alexandre Duret-Lutz committed Oct 12, 2012 12 ``````// the Free Software Foundation; either version 3 of the License, or `````` Alexandre Duret-Lutz committed Nov 21, 2003 13 14 15 16 17 18 19 20 ``````// (at your option) any later version. // // Spot 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 General Public // License for more details. // // You should have received a copy of the GNU General Public License `````` Alexandre Duret-Lutz committed Oct 12, 2012 21 ``````// along with this program. If not, see . `````` Alexandre Duret-Lutz committed Nov 21, 2003 22 `````` `````` Alexandre Duret-Lutz committed May 26, 2003 23 24 25 ``````#ifndef SPOT_TGBA_STATE_HH # define SPOT_TGBA_STATE_HH `````` Alexandre Duret-Lutz committed Jul 29, 2013 26 ``````#include "misc/common.hh" `````` Alexandre Duret-Lutz committed Aug 29, 2003 27 ``````#include `````` Alexandre Duret-Lutz committed May 27, 2003 28 ``````#include `````` Alexandre Duret-Lutz committed Sep 10, 2003 29 ``````#include `````` Alexandre Duret-Lutz committed Sep 30, 2003 30 ``````#include `````` Alexandre Duret-Lutz committed Feb 12, 2014 31 ``````#include `````` Alexandre Duret-Lutz committed Mar 31, 2011 32 ``````#include "misc/casts.hh" `````` Alexandre Duret-Lutz committed Aug 23, 2013 33 ``````#include "misc/hash.hh" `````` Alexandre Duret-Lutz committed May 27, 2003 34 `````` `````` Alexandre Duret-Lutz committed May 26, 2003 35 36 ``````namespace spot { `````` Alexandre Duret-Lutz committed May 27, 2003 37 `````` `````` Alexandre Duret-Lutz committed Nov 16, 2004 38 `````` /// \ingroup tgba_essentials `````` Alexandre Duret-Lutz committed Jun 08, 2013 39 `````` /// \brief Abstract class for states. `````` Alexandre Duret-Lutz committed Jul 29, 2013 40 `````` class SPOT_API state `````` Alexandre Duret-Lutz committed May 26, 2003 41 42 `````` { public: `````` Alexandre Duret-Lutz committed May 27, 2003 43 44 45 46 47 48 49 50 51 52 53 `````` /// \brief Compares two states (that come from the same automaton). /// /// This method returns an integer less than, equal to, or greater /// than zero if \a this is found, respectively, to be less than, equal /// to, or greater than \a other according to some implicit total order. /// /// This method should not be called to compare states from /// different automata. /// /// \sa spot::state_ptr_less_than virtual int compare(const state* other) const = 0; `````` Alexandre Duret-Lutz committed May 27, 2003 54 `````` `````` Alexandre Duret-Lutz committed Aug 29, 2003 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 `````` /// \brief Hash a state. /// /// This method returns an integer that can be used as a /// hash value for this state. /// /// Note that the hash value is guaranteed to be unique for all /// equal states (in compare()'s sense) for only has long has one /// of these states exists. So it's OK to use a spot::state as a /// key in a \c hash_map because the mere use of the state as a /// key in the hash will ensure the state continues to exist. /// /// However if you create the state, get its hash key, delete the /// state, recreate the same state, and get its hash key, you may /// obtain two different hash keys if the same state were not /// already used elsewhere. In practice this weird situation can /// occur only when the state is BDD-encoded, because BDD numbers /// (used to build the hash value) can be reused for other /// formulas. That probably doesn't matter, since the hash value /// is meant to be used in a \c hash_map, but it had to be noted. virtual size_t hash() const = 0; `````` Alexandre Duret-Lutz committed Jun 16, 2003 76 77 78 `````` /// Duplicate a state. virtual state* clone() const = 0; `````` Alexandre Duret-Lutz committed Jan 27, 2011 79 80 81 82 83 `````` /// \brief Release a state. /// /// Methods from the tgba or tgba_succ_iterator always return a /// new state that you should deallocate with this function. /// Before Spot 0.7, you had to "delete" your state directly. `````` Alexandre Duret-Lutz committed Jan 17, 2013 84 85 86 87 `````` /// Starting with Spot 0.7, you should update your code to use /// this function instead. destroy() usually call delete, except /// in subclasses that destroy() to allow better memory management /// (e.g., no memory allocation for explicit automata). `````` Alexandre Duret-Lutz committed Jan 27, 2011 88 89 90 91 92 `````` virtual void destroy() const { delete this; } `````` Alexandre Duret-Lutz committed Mar 30, 2011 93 `````` protected: `````` Alexandre Duret-Lutz committed Jan 27, 2011 94 95 `````` /// \brief Destructor. /// `````` Alexandre Duret-Lutz committed Jan 17, 2013 96 `````` /// Note that client code should call `````` Alexandre Duret-Lutz committed Jan 27, 2011 97 `````` /// s->destroy(); instead of delete s;. `````` Alexandre Duret-Lutz committed May 26, 2003 98 99 100 101 `````` virtual ~state() { } }; `````` Alexandre Duret-Lutz committed May 27, 2003 102 `````` `````` Alexandre Duret-Lutz committed Nov 16, 2004 103 `````` /// \ingroup tgba_essentials `````` Alexandre Duret-Lutz committed Jun 08, 2013 104 `````` /// \brief Strict Weak Ordering for \c state*. `````` Alexandre Duret-Lutz committed May 27, 2003 105 106 107 108 109 110 111 112 113 114 `````` /// /// This is meant to be used as a comparison functor for /// STL \c map whose key are of type \c state*. /// /// For instance here is how one could declare /// a map of \c state*. /// \code /// // Remember how many times each state has been visited. /// std::map seen; /// \endcode `````` Alexandre Duret-Lutz committed Jul 09, 2004 115 `````` struct state_ptr_less_than: `````` Alexandre Duret-Lutz committed Sep 30, 2003 116 `````` public std::binary_function `````` Alexandre Duret-Lutz committed May 27, 2003 117 118 `````` { bool `````` Alexandre Duret-Lutz committed Jul 08, 2003 119 `````` operator()(const state* left, const state* right) const `````` Alexandre Duret-Lutz committed May 27, 2003 120 `````` { `````` Alexandre Duret-Lutz committed Aug 25, 2003 121 `````` assert(left); `````` Alexandre Duret-Lutz committed May 27, 2003 122 123 124 125 `````` return left->compare(right) < 0; } }; `````` Alexandre Duret-Lutz committed Nov 16, 2004 126 `````` /// \ingroup tgba_essentials `````` Alexandre Duret-Lutz committed Jun 08, 2013 127 `````` /// \brief An Equivalence Relation for \c state*. `````` Alexandre Duret-Lutz committed Aug 29, 2003 128 129 `````` /// /// This is meant to be used as a comparison functor for `````` Alexandre Duret-Lutz committed Feb 12, 2014 130 `````` /// an \c unordered_map whose key are of type \c state*. `````` Alexandre Duret-Lutz committed Aug 29, 2003 131 132 133 134 135 `````` /// /// For instance here is how one could declare /// a map of \c state*. /// \code /// // Remember how many times each state has been visited. `````` Alexandre Duret-Lutz committed Feb 12, 2014 136 `````` /// std::unordered_map seen; /// \endcode `````` Alexandre Duret-Lutz committed Jul 09, 2004 139 `````` struct state_ptr_equal: `````` Alexandre Duret-Lutz committed Sep 30, 2003 140 `````` public std::binary_function `````` Alexandre Duret-Lutz committed Aug 29, 2003 141 142 143 144 145 146 147 148 149 `````` { bool operator()(const state* left, const state* right) const { assert(left); return 0 == left->compare(right); } }; `````` Alexandre Duret-Lutz committed Nov 16, 2004 150 `````` /// \ingroup tgba_essentials `````` Alexandre Duret-Lutz committed Nov 17, 2004 151 `````` /// \ingroup hash_funcs `````` Alexandre Duret-Lutz committed Jun 08, 2013 152 `````` /// \brief Hash Function for \c state*. `````` Alexandre Duret-Lutz committed Aug 29, 2003 153 154 `````` /// /// This is meant to be used as a hash functor for `````` Alexandre Duret-Lutz committed Feb 12, 2014 155 `````` /// an \c unordered_map whose key are of type \c state*. `````` Alexandre Duret-Lutz committed Aug 29, 2003 156 157 158 159 160 `````` /// /// For instance here is how one could declare /// a map of \c state*. /// \code /// // Remember how many times each state has been visited. `````` Alexandre Duret-Lutz committed Feb 12, 2014 161 `````` /// std::unordered_map seen; /// \endcode `````` Alexandre Duret-Lutz committed Jul 09, 2004 164 `````` struct state_ptr_hash: `````` Alexandre Duret-Lutz committed Sep 30, 2003 165 `````` public std::unary_function `````` Alexandre Duret-Lutz committed Aug 29, 2003 166 167 168 169 170 171 172 173 174 `````` { size_t operator()(const state* that) const { assert(that); return that->hash(); } }; `````` Alexandre Duret-Lutz committed Feb 12, 2014 175 176 `````` typedef std::unordered_set state_set; `````` Alexandre Duret-Lutz committed Aug 23, 2013 177 178 `````` `````` Guillaume Sadegh committed Oct 01, 2009 179 180 181 `````` // Functions related to shared_ptr. ////////////////////////////////////////////////// `````` Alexandre Duret-Lutz committed Feb 12, 2014 182 `````` typedef std::shared_ptr shared_state; `````` Guillaume Sadegh committed Oct 01, 2009 183 `````` `````` Alexandre Duret-Lutz committed Jan 27, 2011 184 185 `````` inline void shared_state_deleter(state* s) { s->destroy(); } `````` Alexandre Duret-Lutz committed Jun 08, 2013 186 `````` /// \ingroup tgba_essentials `````` Guillaume Sadegh committed Oct 01, 2009 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 `````` /// \brief Strict Weak Ordering for \c shared_state /// (shared_ptr). /// /// This is meant to be used as a comparison functor for /// STL \c map whose key are of type \c shared_state. /// /// For instance here is how one could declare /// a map of \c shared_state. /// \code /// // Remember how many times each state has been visited. /// std::map seen; /// \endcode struct state_shared_ptr_less_than: public std::binary_function { bool operator()(shared_state left, shared_state right) const { assert(left); return left->compare(right.get()) < 0; } }; `````` Alexandre Duret-Lutz committed Jun 08, 2013 212 `````` /// \ingroup tgba_essentials `````` Guillaume Sadegh committed Oct 01, 2009 213 214 215 216 `````` /// \brief An Equivalence Relation for \c shared_state /// (shared_ptr). /// /// This is meant to be used as a comparison functor for `````` Alexandre Duret-Lutz committed Feb 12, 2014 217 `````` /// un \c unordered_map whose key are of type \c shared_state. `````` Guillaume Sadegh committed Oct 01, 2009 218 219 220 221 222 `````` /// /// For instance here is how one could declare /// a map of \c shared_state /// \code /// // Remember how many times each state has been visited. `````` Alexandre Duret-Lutz committed Feb 12, 2014 223 224 225 `````` /// std::unordered_map seen; `````` Guillaume Sadegh committed Oct 01, 2009 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 `````` /// \endcode struct state_shared_ptr_equal: public std::binary_function { bool operator()(shared_state left, shared_state right) const { assert(left); return 0 == left->compare(right.get()); } }; /// \ingroup tgba_essentials /// \ingroup hash_funcs `````` Alexandre Duret-Lutz committed Jun 08, 2013 242 `````` /// \brief Hash Function for \c shared_state (shared_ptr). `````` Guillaume Sadegh committed Oct 01, 2009 243 244 `````` /// /// This is meant to be used as a hash functor for `````` Alexandre Duret-Lutz committed Feb 12, 2014 245 `````` /// an \c unordered_map whose key are of type `````` Guillaume Sadegh committed Oct 01, 2009 246 247 248 249 250 251 `````` /// \c shared_state. /// /// For instance here is how one could declare /// a map of \c shared_state. /// \code /// // Remember how many times each state has been visited. `````` Alexandre Duret-Lutz committed Feb 12, 2014 252 253 254 `````` /// std::unordered_map seen; `````` Guillaume Sadegh committed Oct 01, 2009 255 256 257 258 259 260 261 262 263 264 265 266 `````` /// \endcode struct state_shared_ptr_hash: public std::unary_function { size_t operator()(shared_state that) const { assert(that); return that->hash(); } }; `````` Alexandre Duret-Lutz committed Feb 12, 2014 267 268 269 `````` typedef std::unordered_set shared_state_set; `````` Alexandre Duret-Lutz committed Aug 23, 2013 270 `````` `````` Alexandre Duret-Lutz committed May 26, 2003 271 272 273 ``````} #endif // SPOT_TGBA_STATE_HH``````