kripkegraph.hh 6.43 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de
// Recherche et Développement de l'Epita (LRDE)
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
//
// 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
// the Free Software Foundation; either version 3 of the License, or
// (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
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

#pragma once

#include <iosfwd>
23
24
25
#include <spot/kripke/kripke.hh>
#include <spot/graph/graph.hh>
#include <spot/tl/formula.hh>
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41

namespace spot
{
  /// \brief Concrete class for kripke_graph states.
  struct SPOT_API kripke_graph_state: public spot::state
  {
  public:
    kripke_graph_state(bdd cond = bddfalse) noexcept
      : cond_(cond)
    {
    }

    virtual ~kripke_graph_state() noexcept
    {
    }

42
    virtual int compare(const spot::state* other) const override
43
44
    {
      auto o = down_cast<const kripke_graph_state*>(other);
45
      SPOT_ASSERT(o);
46
47
48

      // Do not simply return "other - this", it might not fit in an int.
      if (o < this)
49
        return -1;
50
      if (o > this)
51
        return 1;
52
53
54
      return 0;
    }

55
    virtual size_t hash() const override
56
57
    {
      return
58
        reinterpret_cast<const char*>(this) - static_cast<const char*>(nullptr);
59
60
61
    }

    virtual kripke_graph_state*
62
    clone() const override
63
64
65
66
    {
      return const_cast<kripke_graph_state*>(this);
    }

67
    virtual void destroy() const override
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
    {
    }

    bdd cond() const
    {
      return cond_;
    }

    void cond(bdd c)
    {
      cond_ = c;
    }

  private:
    bdd cond_;
  };

  template<class Graph>
  class SPOT_API kripke_graph_succ_iterator final: public kripke_succ_iterator
  {
  private:
    typedef typename Graph::edge edge;
    typedef typename Graph::state_data_t state;
    const Graph* g_;
    edge t_;
    edge p_;
  public:
    kripke_graph_succ_iterator(const Graph* g,
96
                               const typename Graph::state_storage_t* s):
97
98
99
100
101
102
103
104
105
106
      kripke_succ_iterator(s->cond()),
      g_(g),
      t_(s->succ)
    {
    }

    ~kripke_graph_succ_iterator()
    {
    }

107
    void recycle(const typename Graph::state_storage_t* s)
108
109
110
111
112
    {
      cond_ = s->cond();
      t_ = s->succ;
    }

113
    virtual bool first() override
114
115
116
117
118
    {
      p_ = t_;
      return p_;
    }

119
    virtual bool next() override
120
121
122
123
124
    {
      p_ = g_->edge_storage(p_).next_succ;
      return p_;
    }

125
    virtual bool done() const override
126
127
128
129
    {
      return !p_;
    }

130
    virtual kripke_graph_state* dst() const override
131
    {
132
      SPOT_ASSERT(!done());
133
      return const_cast<kripke_graph_state*>
134
        (&g_->state_data(g_->edge_storage(p_).dst));
135
136
137
138
139
140
    }
  };


  /// \class kripke_graph
  /// \brief Kripke Structure.
141
  class SPOT_API kripke_graph final : public kripke
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
  {
  public:
    typedef digraph<kripke_graph_state, void> graph_t;
    typedef graph_t::edge_storage_t edge_storage_t;
  protected:
    graph_t g_;
    mutable unsigned init_number_;
  public:
    kripke_graph(const bdd_dict_ptr& d)
      : kripke(d), init_number_(0)
    {
    }

    virtual ~kripke_graph()
    {
      get_dict()->unregister_all_my_variables(this);
    }

    unsigned num_states() const
    {
      return g_.num_states();
    }

    unsigned num_edges() const
    {
      return g_.num_edges();
    }

    void set_init_state(graph_t::state s)
    {
172
173
174
      if (SPOT_UNLIKELY(s >= num_states()))
        throw std::invalid_argument
          ("set_init_state() called with nonexisiting state");
175
176
177
178
179
      init_number_ = s;
    }

    graph_t::state get_init_state_number() const
    {
180
      // If the kripke has no state, it has no initial state.
181
      if (num_states() == 0)
182
        throw std::runtime_error("kripke has no state at all");
183
184
185
      return init_number_;
    }

186
    virtual const kripke_graph_state* get_init_state() const override
187
    {
188
      return state_from_number(get_init_state_number());
189
190
191
192
193
    }

    /// \brief Allow to get an iterator on the state we passed in
    /// parameter.
    virtual kripke_graph_succ_iterator<graph_t>*
194
    succ_iter(const spot::state* st) const override
195
196
    {
      auto s = down_cast<const typename graph_t::state_storage_t*>(st);
197
198
      SPOT_ASSERT(s);
      SPOT_ASSERT(!s->succ || g_.is_valid_edge(s->succ));
199
200

      if (this->iter_cache_)
201
202
203
204
205
206
207
        {
          auto it =
            down_cast<kripke_graph_succ_iterator<graph_t>*>(this->iter_cache_);
          it->recycle(s);
          this->iter_cache_ = nullptr;
          return it;
        }
208
209
210
211
212
213
214
215
      return new kripke_graph_succ_iterator<graph_t>(&g_, s);

    }

    graph_t::state
    state_number(const state* st) const
    {
      auto s = down_cast<const typename graph_t::state_storage_t*>(st);
216
      SPOT_ASSERT(s);
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
      return s - &g_.state_storage(0);
    }

    const kripke_graph_state*
    state_from_number(graph_t::state n) const
    {
      return &g_.state_data(n);
    }

    kripke_graph_state*
    state_from_number(graph_t::state n)
    {
      return &g_.state_data(n);
    }

    std::string format_state(unsigned n) const
    {
      std::stringstream ss;
      ss << n;
      return ss.str();
    }

239
    virtual std::string format_state(const state* st) const override
240
241
242
243
244
    {
      return format_state(state_number(st));
    }

    /// \brief Get the condition on the state
245
    virtual bdd state_condition(const state* s) const override
246
    {
247
248
249
      auto gs = down_cast<const kripke_graph_state*>(s);
      SPOT_ASSERT(gs);
      return gs->cond();
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
    }

    edge_storage_t& edge_storage(unsigned t)
    {
      return g_.edge_storage(t);
    }

    const edge_storage_t edge_storage(unsigned t) const
    {
      return g_.edge_storage(t);
    }

    unsigned new_state(bdd cond)
    {
      return g_.new_state(cond);
    }

    unsigned new_states(unsigned n, bdd cond)
    {
      return g_.new_states(n, cond);
    }

    unsigned new_edge(unsigned src, unsigned dst)
    {
      return g_.new_edge(src, dst);
    }
  };

  typedef std::shared_ptr<kripke_graph> kripke_graph_ptr;

  inline kripke_graph_ptr
  make_kripke_graph(const bdd_dict_ptr& d)
  {
    return std::make_shared<kripke_graph>(d);
  }
}