state.hh 8.66 KB
Newer Older
1
2
3
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2011, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
Guillaume Sadegh's avatar
Guillaume Sadegh committed
4
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6
5
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
6
// Pierre et Marie Curie.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
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
12
// the Free Software Foundation; either version 3 of the License, or
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
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
21
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
22

23
24
25
#ifndef SPOT_TGBA_STATE_HH
# define SPOT_TGBA_STATE_HH

26
#include "misc/common.hh"
27
#include <cstddef>
28
#include <bdd.h>
29
#include <cassert>
30
#include <functional>
31
#include <memory>
32
#include "misc/casts.hh"
33
#include "misc/hash.hh"
34

35
36
namespace spot
{
37

38
  /// \ingroup tgba_essentials
39
  /// \brief Abstract class for states.
40
  class SPOT_API state
41
42
  {
  public:
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;
54

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;

76
77
78
    /// Duplicate a state.
    virtual state* clone() const = 0;

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.
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).
88
89
90
91
92
    virtual void destroy() const
    {
      delete this;
    }

93
  protected:
94
95
    /// \brief Destructor.
    ///
96
    /// Note that client code should call
97
    /// <code>s->destroy();</code> instead of <code>delete s;</code>.
98
99
100
101
    virtual ~state()
    {
    }
  };
102

103
  /// \ingroup tgba_essentials
104
  /// \brief Strict Weak Ordering for \c state*.
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<spot::state*, int, spot::state_ptr_less_than> seen;
  /// \endcode
115
  struct state_ptr_less_than:
116
    public std::binary_function<const state*, const state*, bool>
117
118
  {
    bool
Alexandre Duret-Lutz's avatar
spacing    
Alexandre Duret-Lutz committed
119
    operator()(const state* left, const state* right) const
120
    {
121
      assert(left);
122
123
124
125
      return left->compare(right) < 0;
    }
  };

126
  /// \ingroup tgba_essentials
127
  /// \brief An Equivalence Relation for \c state*.
128
129
  ///
  /// This is meant to be used as a comparison functor for
130
  /// an \c unordered_map whose key are of type \c state*.
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.
136
  ///   std::unordered_map<spot::state*, int, spot::state_ptr_hash,
137
138
  ///                                    spot::state_ptr_equal> seen;
  /// \endcode
139
  struct state_ptr_equal:
140
    public std::binary_function<const state*, const state*, bool>
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);
    }
  };

150
  /// \ingroup tgba_essentials
151
  /// \ingroup hash_funcs
152
  /// \brief Hash Function for \c state*.
153
154
  ///
  /// This is meant to be used as a hash functor for
155
  /// an \c unordered_map whose key are of type \c state*.
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.
161
  ///   std::unordered_map<spot::state*, int, spot::state_ptr_hash,
162
163
  ///                                    spot::state_ptr_equal> seen;
  /// \endcode
164
  struct state_ptr_hash:
165
    public std::unary_function<const state*, size_t>
166
167
168
169
170
171
172
173
174
  {
    size_t
    operator()(const state* that) const
    {
      assert(that);
      return that->hash();
    }
  };

175
176
  typedef std::unordered_set<const state*,
			     state_ptr_hash, state_ptr_equal> state_set;
177
178


179
180
181
  // Functions related to shared_ptr.
  //////////////////////////////////////////////////

182
  typedef std::shared_ptr<const state> shared_state;
183

184
185
  inline void shared_state_deleter(state* s) { s->destroy(); }

186
  /// \ingroup tgba_essentials
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<const state*>).
  ///
  /// 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<shared_state, int, spot::state_shared_ptr_less_than> seen;
  /// \endcode
  struct state_shared_ptr_less_than:
    public std::binary_function<shared_state,
                                shared_state, bool>
  {
    bool
    operator()(shared_state left,
               shared_state right) const
    {
      assert(left);
      return left->compare(right.get()) < 0;
    }
  };

212
  /// \ingroup tgba_essentials
213
214
215
216
  /// \brief An Equivalence Relation for \c shared_state
  /// (shared_ptr<const state*>).
  ///
  /// This is meant to be used as a comparison functor for
217
  /// un \c unordered_map whose key are of type \c shared_state.
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.
223
224
225
  ///   std::unordered_map<shared_state, int,
  ///                      state_shared_ptr_hash,
  ///                      state_shared_ptr_equal> seen;
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<shared_state,
                                shared_state, bool>
  {
    bool
    operator()(shared_state left,
               shared_state right) const
    {
      assert(left);
      return 0 == left->compare(right.get());
    }
  };

  /// \ingroup tgba_essentials
  /// \ingroup hash_funcs
242
  /// \brief Hash Function for \c shared_state (shared_ptr<const state*>).
243
244
  ///
  /// This is meant to be used as a hash functor for
245
  /// an \c unordered_map whose key are of type
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.
252
253
254
  ///   std::unordered_map<shared_state, int,
  ///                      state_shared_ptr_hash,
  ///                      state_shared_ptr_equal> seen;
255
256
257
258
259
260
261
262
263
264
265
266
  /// \endcode
  struct state_shared_ptr_hash:
    public std::unary_function<shared_state, size_t>
  {
    size_t
    operator()(shared_state that) const
    {
      assert(that);
      return that->hash();
    }
  };

267
268
269
  typedef std::unordered_set<shared_state,
			     state_shared_ptr_hash,
			     state_shared_ptr_equal> shared_state_set;
270

271
272
273
}

#endif // SPOT_TGBA_STATE_HH