spot  2.4.3
kripkegraph.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2011-2017 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  virtual ~kripke_graph_state() noexcept
39  {
40  }
41 
42  virtual int compare(const spot::state* other) const override
43  {
44  auto o = down_cast<const kripke_graph_state*>(other);
45 
46  // Do not simply return "other - this", it might not fit in an int.
47  if (o < this)
48  return -1;
49  if (o > this)
50  return 1;
51  return 0;
52  }
53 
54  virtual size_t hash() const override
55  {
56  return
57  reinterpret_cast<const char*>(this) - static_cast<const char*>(nullptr);
58  }
59 
60  virtual kripke_graph_state*
61  clone() const override
62  {
63  return const_cast<kripke_graph_state*>(this);
64  }
65 
66  virtual void destroy() const override
67  {
68  }
69 
70  bdd cond() const
71  {
72  return cond_;
73  }
74 
75  void cond(bdd c)
76  {
77  cond_ = c;
78  }
79 
80  private:
81  bdd cond_;
82  };
83 
84  template<class Graph>
85  class SPOT_API kripke_graph_succ_iterator final: public kripke_succ_iterator
86  {
87  private:
88  typedef typename Graph::edge edge;
89  typedef typename Graph::state_data_t state;
90  const Graph* g_;
91  edge t_;
92  edge p_;
93  public:
94  kripke_graph_succ_iterator(const Graph* g,
95  const typename Graph::state_storage_t* s):
96  kripke_succ_iterator(s->cond()),
97  g_(g),
98  t_(s->succ)
99  {
100  }
101 
103  {
104  }
105 
106  void recycle(const typename Graph::state_storage_t* s)
107  {
108  cond_ = s->cond();
109  t_ = s->succ;
110  }
111 
112  virtual bool first() override
113  {
114  p_ = t_;
115  return p_;
116  }
117 
118  virtual bool next() override
119  {
120  p_ = g_->edge_storage(p_).next_succ;
121  return p_;
122  }
123 
124  virtual bool done() const override
125  {
126  return !p_;
127  }
128 
129  virtual kripke_graph_state* dst() const override
130  {
131  SPOT_ASSERT(!done());
132  return const_cast<kripke_graph_state*>
133  (&g_->state_data(g_->edge_storage(p_).dst));
134  }
135  };
136 
137 
140  class SPOT_API kripke_graph final : public kripke
141  {
142  public:
145  protected:
146  graph_t g_;
147  mutable unsigned init_number_;
148  public:
149  kripke_graph(const bdd_dict_ptr& d)
150  : kripke(d), init_number_(0)
151  {
152  }
153 
154  virtual ~kripke_graph()
155  {
156  get_dict()->unregister_all_my_variables(this);
157  }
158 
159  unsigned num_states() const
160  {
161  return g_.num_states();
162  }
163 
164  unsigned num_edges() const
165  {
166  return g_.num_edges();
167  }
168 
169  void set_init_state(graph_t::state s)
170  {
171  if (SPOT_UNLIKELY(s >= num_states()))
172  throw std::invalid_argument
173  ("set_init_state() called with nonexisiting state");
174  init_number_ = s;
175  }
176 
177  graph_t::state get_init_state_number() const
178  {
179  // If the kripke has no state, it has no initial state.
180  if (num_states() == 0)
181  throw std::runtime_error("kripke has no state at all");
182  return init_number_;
183  }
184 
185  virtual const kripke_graph_state* get_init_state() const override
186  {
187  return state_from_number(get_init_state_number());
188  }
189 
193  succ_iter(const spot::state* st) const override
194  {
195  auto s = down_cast<const typename graph_t::state_storage_t*>(st);
196  SPOT_ASSERT(!s->succ || g_.is_valid_edge(s->succ));
197 
198  if (this->iter_cache_)
199  {
200  auto it =
201  down_cast<kripke_graph_succ_iterator<graph_t>*>(this->iter_cache_);
202  it->recycle(s);
203  this->iter_cache_ = nullptr;
204  return it;
205  }
206  return new kripke_graph_succ_iterator<graph_t>(&g_, s);
207 
208  }
209 
210  graph_t::state
211  state_number(const state* st) const
212  {
213  auto s = down_cast<const typename graph_t::state_storage_t*>(st);
214  return s - &g_.state_storage(0);
215  }
216 
217  const kripke_graph_state*
218  state_from_number(graph_t::state n) const
219  {
220  return &g_.state_data(n);
221  }
222 
224  state_from_number(graph_t::state n)
225  {
226  return &g_.state_data(n);
227  }
228 
229  std::string format_state(unsigned n) const
230  {
231  std::stringstream ss;
232  ss << n;
233  return ss.str();
234  }
235 
236  virtual std::string format_state(const state* st) const override
237  {
238  return format_state(state_number(st));
239  }
240 
242  virtual bdd state_condition(const state* s) const override
243  {
244  auto gs = down_cast<const kripke_graph_state*>(s);
245  return gs->cond();
246  }
247 
248  edge_storage_t& edge_storage(unsigned t)
249  {
250  return g_.edge_storage(t);
251  }
252 
253  const edge_storage_t edge_storage(unsigned t) const
254  {
255  return g_.edge_storage(t);
256  }
257 
258  unsigned new_state(bdd cond)
259  {
260  return g_.new_state(cond);
261  }
262 
263  unsigned new_states(unsigned n, bdd cond)
264  {
265  return g_.new_states(n, cond);
266  }
267 
268  unsigned new_edge(unsigned src, unsigned dst)
269  {
270  return g_.new_edge(src, dst);
271  }
272  };
273 
274  typedef std::shared_ptr<kripke_graph> kripke_graph_ptr;
275 
276  inline kripke_graph_ptr
277  make_kripke_graph(const bdd_dict_ptr& d)
278  {
279  return std::make_shared<kripke_graph>(d);
280  }
281 }
state new_states(unsigned n, Args &&... args)
Create n new states.
Definition: graph.hh:697
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:61
Kripke Structure.
Definition: kripkegraph.hh:140
virtual kripke_graph_state * dst() const override
Get the destination state of the current edge.
Definition: kripkegraph.hh:129
Interface for a Kripke structure.
Definition: kripke.hh:90
state new_state(Args &&... args)
Create a new states.
Definition: graph.hh:683
LTL/PSL formula interface.
Abstract class for states.
Definition: twa.hh:50
Iterator code for Kripke structure.
Definition: kripke.hh:43
Definition: graph.hh:184
Concrete class for kripke_graph states.
Definition: kripkegraph.hh:30
virtual bool next() override
Jump to the next successor (if any).
Definition: kripkegraph.hh:118
edge_storage_t & edge_storage(edge s)
return a reference to the storage of an edge
Definition: graph.hh:748
edge new_edge(state src, state dst, Args &&... args)
Create a new edge.
Definition: graph.hh:785
state_storage_t::data_t & state_data(state s)
return the State_Data associated to a state
Definition: graph.hh:730
virtual size_t hash() const override
Hash a state.
Definition: kripkegraph.hh:54
Definition: graph.hh:159
state_storage_t & state_storage(state s)
return a reference to the storage of a state
Definition: graph.hh:712
virtual void destroy() const override
Release a state.
Definition: kripkegraph.hh:66
virtual bool first() override
Position the iterator on the first successor (if any).
Definition: kripkegraph.hh:112
unsigned num_states() const
The number of states in the automaton.
Definition: graph.hh:646
unsigned num_edges() const
The number of edges in the automaton.
Definition: graph.hh:654
bool is_valid_edge(edge t) const
Test whether the given edge is valid.
Definition: graph.hh:982
virtual bdd state_condition(const state *s) const override
Get the condition on the state.
Definition: kripkegraph.hh:242
virtual bool done() const override
Check whether the iteration is finished.
Definition: kripkegraph.hh:124
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:193
virtual const kripke_graph_state * get_init_state() const override
Get the initial state of the automaton.
Definition: kripkegraph.hh:185
virtual int compare(const spot::state *other) const override
Compares two states (that come from the same automaton).
Definition: kripkegraph.hh:42
virtual std::string format_state(const state *st) const override
Format the state as a string for printing.
Definition: kripkegraph.hh:236
Definition: kripkegraph.hh:85

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Tue Dec 19 2017 09:22:58 for spot by doxygen 1.8.13