spot  2.3
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
kripkegraph.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de
3 // Recherche et Développement de 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  SPOT_ASSERT(o);
46 
47  // Do not simply return "other - this", it might not fit in an int.
48  if (o < this)
49  return -1;
50  if (o > this)
51  return 1;
52  return 0;
53  }
54 
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  return const_cast<kripke_graph_state*>(this);
65  }
66 
67  virtual void destroy() const override
68  {
69  }
70 
71  bdd cond() const
72  {
73  return cond_;
74  }
75 
76  void cond(bdd c)
77  {
78  cond_ = c;
79  }
80 
81  private:
82  bdd cond_;
83  };
84 
85  template<class Graph>
86  class SPOT_API kripke_graph_succ_iterator final: public kripke_succ_iterator
87  {
88  private:
89  typedef typename Graph::edge edge;
90  typedef typename Graph::state_data_t state;
91  const Graph* g_;
92  edge t_;
93  edge p_;
94  public:
95  kripke_graph_succ_iterator(const Graph* g,
96  const typename Graph::state_storage_t* s):
97  kripke_succ_iterator(s->cond()),
98  g_(g),
99  t_(s->succ)
100  {
101  }
102 
104  {
105  }
106 
107  void recycle(const typename Graph::state_storage_t* s)
108  {
109  cond_ = s->cond();
110  t_ = s->succ;
111  }
112 
113  virtual bool first() override
114  {
115  p_ = t_;
116  return p_;
117  }
118 
119  virtual bool next() override
120  {
121  p_ = g_->edge_storage(p_).next_succ;
122  return p_;
123  }
124 
125  virtual bool done() const override
126  {
127  return !p_;
128  }
129 
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 
141  class SPOT_API kripke_graph final : public kripke
142  {
143  public:
146  protected:
147  graph_t g_;
148  mutable unsigned init_number_;
149  public:
150  kripke_graph(const bdd_dict_ptr& d)
151  : kripke(d), init_number_(0)
152  {
153  }
154 
155  virtual ~kripke_graph()
156  {
157  get_dict()->unregister_all_my_variables(this);
158  }
159 
160  unsigned num_states() const
161  {
162  return g_.num_states();
163  }
164 
165  unsigned num_edges() const
166  {
167  return g_.num_edges();
168  }
169 
170  void set_init_state(graph_t::state s)
171  {
172  if (SPOT_UNLIKELY(s >= num_states()))
173  throw std::invalid_argument
174  ("set_init_state() called with nonexisiting state");
175  init_number_ = s;
176  }
177 
178  graph_t::state get_init_state_number() const
179  {
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  return init_number_;
184  }
185 
186  virtual const kripke_graph_state* get_init_state() const override
187  {
188  return state_from_number(get_init_state_number());
189  }
190 
194  succ_iter(const spot::state* st) const override
195  {
196  auto s = down_cast<const typename graph_t::state_storage_t*>(st);
197  SPOT_ASSERT(s);
198  SPOT_ASSERT(!s->succ || g_.is_valid_edge(s->succ));
199 
200  if (this->iter_cache_)
201  {
202  auto it =
203  down_cast<kripke_graph_succ_iterator<graph_t>*>(this->iter_cache_);
204  it->recycle(s);
205  this->iter_cache_ = nullptr;
206  return it;
207  }
208  return new kripke_graph_succ_iterator<graph_t>(&g_, s);
209 
210  }
211 
212  graph_t::state
213  state_number(const state* st) const
214  {
215  auto s = down_cast<const typename graph_t::state_storage_t*>(st);
216  SPOT_ASSERT(s);
217  return s - &g_.state_storage(0);
218  }
219 
220  const kripke_graph_state*
221  state_from_number(graph_t::state n) const
222  {
223  return &g_.state_data(n);
224  }
225 
226  kripke_graph_state*
227  state_from_number(graph_t::state n)
228  {
229  return &g_.state_data(n);
230  }
231 
232  std::string format_state(unsigned n) const
233  {
234  std::stringstream ss;
235  ss << n;
236  return ss.str();
237  }
238 
239  virtual std::string format_state(const state* st) const override
240  {
241  return format_state(state_number(st));
242  }
243 
245  virtual bdd state_condition(const state* s) const override
246  {
247  auto gs = down_cast<const kripke_graph_state*>(s);
248  SPOT_ASSERT(gs);
249  return gs->cond();
250  }
251 
252  edge_storage_t& edge_storage(unsigned t)
253  {
254  return g_.edge_storage(t);
255  }
256 
257  const edge_storage_t edge_storage(unsigned t) const
258  {
259  return g_.edge_storage(t);
260  }
261 
262  unsigned new_state(bdd cond)
263  {
264  return g_.new_state(cond);
265  }
266 
267  unsigned new_states(unsigned n, bdd cond)
268  {
269  return g_.new_states(n, cond);
270  }
271 
272  unsigned new_edge(unsigned src, unsigned dst)
273  {
274  return g_.new_edge(src, dst);
275  }
276  };
277 
278  typedef std::shared_ptr<kripke_graph> kripke_graph_ptr;
279 
280  inline kripke_graph_ptr
281  make_kripke_graph(const bdd_dict_ptr& d)
282  {
283  return std::make_shared<kripke_graph>(d);
284  }
285 }
virtual bdd cond() const override
Get the condition on the edge leading to this successor.
Definition: graph.hh:33
virtual kripke_graph_state * clone() const override
Duplicate a state.
Definition: kripkegraph.hh:62
state_storage_t & state_storage(state s)
return a reference to the storage of a state
Definition: graph.hh:700
Kripke Structure.
Definition: kripkegraph.hh:141
virtual kripke_graph_state * dst() const override
Get the destination state of the current edge.
Definition: kripkegraph.hh:130
state_storage_t::data_t & state_data(state s)
return the State_Data associated to a state
Definition: graph.hh:718
Interface for a Kripke structure.
Definition: kripke.hh:90
state new_states(unsigned n, Args &&...args)
Create n new states.
Definition: graph.hh:685
LTL/PSL formula interface.
edge_storage_t & edge_storage(edge s)
return a reference to the storage of an edge
Definition: graph.hh:736
Abstract class for states.
Definition: twa.hh:50
Iterator code for Kripke structure.
Definition: kripke.hh:43
unsigned num_edges() const
The number of edges in the automaton.
Definition: graph.hh:654
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:119
virtual size_t hash() const override
Hash a state.
Definition: kripkegraph.hh:55
Definition: graph.hh:159
virtual void destroy() const override
Release a state.
Definition: kripkegraph.hh:67
virtual bool first() override
Position the iterator on the first successor (if any).
Definition: kripkegraph.hh:113
edge new_edge(state src, state dst, Args &&...args)
Create a new edge.
Definition: graph.hh:773
bool is_valid_edge(edge t) const
Test whether the given edge is valid.
Definition: graph.hh:970
virtual bdd state_condition(const state *s) const override
Get the condition on the state.
Definition: kripkegraph.hh:245
virtual bool done() const override
Check whether the iteration is finished.
Definition: kripkegraph.hh:125
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:194
virtual const kripke_graph_state * get_init_state() const override
Get the initial state of the automaton.
Definition: kripkegraph.hh:186
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:239
state new_state(Args &&...args)
Create a new states.
Definition: graph.hh:671
unsigned num_states() const
The number of states in the automaton.
Definition: graph.hh:646
Definition: kripkegraph.hh:86

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Thu Jan 19 2017 11:08:40 for spot by doxygen 1.8.8