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

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.8.13