spot  2.12.2
kripkegraph.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) by the Spot authors, see the AUTHORS file for details.
3 //
4 // This file is part of Spot, a model checking library.
5 //
6 // Spot is free software; you can redistribute it and/or modify it
7 // under the terms of the GNU General Public License as published by
8 // the Free Software Foundation; either version 3 of the License, or
9 // (at your option) any later version.
10 //
11 // Spot is distributed in the hope that it will be useful, but WITHOUT
12 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
13 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
14 // License for more details.
15 //
16 // You should have received a copy of the GNU General Public License
17 // along with this program. If not, see <http://www.gnu.org/licenses/>.
18 
19 #pragma once
20 
21 #include <iosfwd>
22 #include <spot/kripke/kripke.hh>
23 #include <spot/graph/graph.hh>
24 #include <spot/tl/formula.hh>
25 
26 namespace spot
27 {
29  struct SPOT_API kripke_graph_state: public spot::state
30  {
31  public:
32  kripke_graph_state(bdd cond = bddfalse) noexcept
33  : cond_(cond)
34  {
35  }
36 
37  kripke_graph_state(const kripke_graph_state& other) noexcept
38  : cond_(other.cond_)
39  {
40  }
41 
42  kripke_graph_state& operator=(const kripke_graph_state& other) noexcept
43  {
44  cond_ = other.cond_;
45  return *this;
46  }
47 
48  virtual ~kripke_graph_state() noexcept
49  {
50  }
51 
52  virtual int compare(const spot::state* other) const override
53  {
54  auto o = down_cast<const kripke_graph_state*>(other);
55 
56  // Do not simply return "other - this", it might not fit in an int.
57  if (o < this)
58  return -1;
59  if (o > this)
60  return 1;
61  return 0;
62  }
63 
64  virtual size_t hash() const override
65  {
66  return reinterpret_cast<size_t>(this);
67  }
68 
69  virtual kripke_graph_state*
70  clone() const override
71  {
72  return const_cast<kripke_graph_state*>(this);
73  }
74 
75  virtual void destroy() const override
76  {
77  }
78 
79  bdd cond() const
80  {
81  return cond_;
82  }
83 
84  void cond(bdd c)
85  {
86  cond_ = c;
87  }
88 
89  private:
90  bdd cond_;
91  };
92 
93  template<class Graph>
94  class SPOT_API kripke_graph_succ_iterator final: public kripke_succ_iterator
95  {
96  private:
97  typedef typename Graph::edge edge;
98  typedef typename Graph::state_data_t state;
99  const Graph* g_;
100  edge t_;
101  edge p_;
102  public:
103  kripke_graph_succ_iterator(const Graph* g,
104  const typename Graph::state_storage_t* s):
105  kripke_succ_iterator(s->cond()),
106  g_(g),
107  t_(s->succ)
108  {
109  }
110 
112  {
113  }
114 
115  void recycle(const typename Graph::state_storage_t* s)
116  {
117  cond_ = s->cond();
118  t_ = s->succ;
119  }
120 
121  virtual bool first() override
122  {
123  p_ = t_;
124  return p_;
125  }
126 
127  virtual bool next() override
128  {
129  p_ = g_->edge_storage(p_).next_succ;
130  return p_;
131  }
132 
133  virtual bool done() const override
134  {
135  return !p_;
136  }
137 
138  virtual kripke_graph_state* dst() const override
139  {
140  SPOT_ASSERT(!done());
141  return const_cast<kripke_graph_state*>
142  (&g_->state_data(g_->edge_storage(p_).dst));
143  }
144  };
145 
146 
149  class SPOT_API kripke_graph final : public kripke
150  {
151  public:
153  // We avoid using graph_t::edge_storage_t because graph_t is not
154  // instantiated in the SWIG bindings, and SWIG would therefore
155  // handle graph_t::edge_storage_t as an abstract type.
156  typedef internal::edge_storage<unsigned, unsigned, unsigned,
158  <void, true>>
160  static_assert(std::is_same<typename graph_t::edge_storage_t,
161  edge_storage_t>::value, "type mismatch");
162 
163  typedef internal::distate_storage<unsigned,
166  static_assert(std::is_same<typename graph_t::state_storage_t,
167  state_storage_t>::value, "type mismatch");
168  typedef std::vector<state_storage_t> state_vector;
169 
170  // We avoid using graph_t::state for the very same reason.
171  typedef unsigned state_num;
172  static_assert(std::is_same<typename graph_t::state, state_num>::value,
173  "type mismatch");
174 
175  protected:
176  graph_t g_;
177  mutable unsigned init_number_;
178  public:
179  kripke_graph(const bdd_dict_ptr& d)
180  : kripke(d), init_number_(0)
181  {
182  }
183 
184  virtual ~kripke_graph()
185  {
186  get_dict()->unregister_all_my_variables(this);
187  }
188 
189  unsigned num_states() const
190  {
191  return g_.num_states();
192  }
193 
194  unsigned num_edges() const
195  {
196  return g_.num_edges();
197  }
198 
199  void set_init_state(state_num s)
200  {
201  if (SPOT_UNLIKELY(s >= num_states()))
202  throw std::invalid_argument
203  ("set_init_state() called with nonexisiting state");
204  init_number_ = s;
205  }
206 
207  state_num get_init_state_number() const
208  {
209  // If the kripke has no state, it has no initial state.
210  if (num_states() == 0)
211  throw std::runtime_error("kripke has no state at all");
212  return init_number_;
213  }
214 
215  virtual const kripke_graph_state* get_init_state() const override
216  {
217  return state_from_number(get_init_state_number());
218  }
219 
223  succ_iter(const spot::state* st) const override
224  {
225  auto s = down_cast<const typename graph_t::state_storage_t*>(st);
226  SPOT_ASSERT(!s->succ || g_.is_valid_edge(s->succ));
227 
228  if (this->iter_cache_)
229  {
230  auto it =
231  down_cast<kripke_graph_succ_iterator<graph_t>*>(this->iter_cache_);
232  it->recycle(s);
233  this->iter_cache_ = nullptr;
234  return it;
235  }
236  return new kripke_graph_succ_iterator<graph_t>(&g_, s);
237 
238  }
239 
240  state_num
241  state_number(const state* st) const
242  {
243  auto s = down_cast<const typename graph_t::state_storage_t*>(st);
244  return s - &g_.state_storage(0);
245  }
246 
247  const kripke_graph_state*
248  state_from_number(state_num n) const
249  {
250  return &g_.state_data(n);
251  }
252 
253  kripke_graph_state*
254  state_from_number(state_num n)
255  {
256  return &g_.state_data(n);
257  }
258 
259  std::string format_state(unsigned n) const
260  {
261  auto named = get_named_prop<std::vector<std::string>>("state-names");
262  if (named && n < named->size())
263  return (*named)[n];
264 
265  return std::to_string(n);
266  }
267 
268  virtual std::string format_state(const state* st) const override
269  {
270  return format_state(state_number(st));
271  }
272 
274  virtual bdd state_condition(const state* s) const override
275  {
276  auto gs = down_cast<const kripke_graph_state*>(s);
277  return gs->cond();
278  }
279 
280  edge_storage_t& edge_storage(unsigned t)
281  {
282  return g_.edge_storage(t);
283  }
284 
285  const edge_storage_t edge_storage(unsigned t) const
286  {
287  return g_.edge_storage(t);
288  }
289 
290  unsigned new_state(bdd cond)
291  {
292  return g_.new_state(cond);
293  }
294 
295  unsigned new_states(unsigned n, bdd cond)
296  {
297  return g_.new_states(n, cond);
298  }
299 
300  unsigned new_edge(unsigned src, unsigned dst)
301  {
302  return g_.new_edge(src, dst);
303  }
304 
305 
306 #ifndef SWIG
307  const state_vector& states() const
308  {
309  return g_.states();
310  }
311 #endif
312 
313  state_vector& states()
314  {
315  return g_.states();
316  }
317 
318 #ifndef SWIG
319  internal::all_trans<const graph_t>
320  edges() const noexcept
321  {
322  return g_.edges();
323  }
324 #endif
325 
326  internal::all_trans<graph_t>
327  edges() noexcept
328  {
329  return g_.edges();
330  }
331 
332 #ifndef SWIG
333  internal::state_out<const graph_t>
334  out(unsigned src) const
335  {
336  return g_.out(src);
337  }
338 #endif
339 
340  internal::state_out<graph_t>
341  out(unsigned src)
342  {
343  return g_.out(src);
344  }
345 
346  };
347 
348  typedef std::shared_ptr<kripke_graph> kripke_graph_ptr;
349 
350  inline kripke_graph_ptr
351  make_kripke_graph(const bdd_dict_ptr& d)
352  {
353  return std::make_shared<kripke_graph>(d);
354  }
355 }
unsigned num_states() const
The number of states in the automaton.
Definition: graph.hh:657
const state_vector & states() const
Return the vector of states.
Definition: graph.hh:945
state new_states(unsigned n, Args &&... args)
Create n new states.
Definition: graph.hh:696
state new_state(Args &&... args)
Create a new states.
Definition: graph.hh:682
bool is_valid_edge(edge t) const
Test whether the given edge is valid.
Definition: graph.hh:996
edge_storage_t & edge_storage(edge s)
return a reference to the storage of an edge
Definition: graph.hh:747
internal::state_out< digraph > out(state src)
Return a fake container with all edges leaving src.
Definition: graph.hh:901
state_storage_t & state_storage(state s)
return a reference to the storage of a state
Definition: graph.hh:711
unsigned num_edges() const
The number of edges in the automaton.
Definition: graph.hh:665
state_storage_t::data_t & state_data(state s)
return the State_Data associated to a state
Definition: graph.hh:729
edge new_edge(state src, state dst, Args &&... args)
Create a new edge.
Definition: graph.hh:784
internal::all_trans< const digraph > edges() const
Return a fake container with all edges (excluding erased edges)
Definition: graph.hh:960
Definition: kripkegraph.hh:95
virtual bool first() override
Position the iterator on the first successor (if any).
Definition: kripkegraph.hh:121
virtual bool done() const override
Check whether the iteration is finished.
Definition: kripkegraph.hh:133
virtual bool next() override
Jump to the next successor (if any).
Definition: kripkegraph.hh:127
virtual kripke_graph_state * dst() const override
Get the destination state of the current edge.
Definition: kripkegraph.hh:138
Kripke Structure.
Definition: kripkegraph.hh:150
virtual kripke_graph_succ_iterator< graph_t > * succ_iter(const spot::state *st) const override
Allow to get an iterator on the state we passed in parameter.
Definition: kripkegraph.hh:223
virtual std::string format_state(const state *st) const override
Format the state as a string for printing.
Definition: kripkegraph.hh:268
virtual const kripke_graph_state * get_init_state() const override
Get the initial state of the automaton.
Definition: kripkegraph.hh:215
virtual bdd state_condition(const state *s) const override
Get the condition on the state.
Definition: kripkegraph.hh:274
Iterator code for Kripke structure.
Definition: kripke.hh:130
virtual bdd cond() const override
Get the condition on the edge leading to this successor.
Interface for a Kripke structure.
Definition: kripke.hh:177
Abstract class for states.
Definition: twa.hh:47
LTL/PSL formula interface.
Definition: automata.hh:26
Definition: graph.hh:65
Definition: graph.hh:162
Definition: graph.hh:187
Concrete class for kripke_graph states.
Definition: kripkegraph.hh:30
virtual size_t hash() const override
Hash a state.
Definition: kripkegraph.hh:64
virtual kripke_graph_state * clone() const override
Duplicate a state.
Definition: kripkegraph.hh:70
virtual void destroy() const override
Release a state.
Definition: kripkegraph.hh:75
virtual int compare(const spot::state *other) const override
Compares two states (that come from the same automaton).
Definition: kripkegraph.hh:52

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.1