spot  2.2.1
 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 (num_states() == 0)
181  const_cast<graph_t&>(g_).new_state();
182  return init_number_;
183  }
184 
185  virtual const kripke_graph_state* get_init_state() const override
186  {
187  if (num_states() == 0)
188  const_cast<graph_t&>(g_).new_state();
189  return state_from_number(init_number_);
190  }
191 
195  succ_iter(const spot::state* st) const override
196  {
197  auto s = down_cast<const typename graph_t::state_storage_t*>(st);
198  SPOT_ASSERT(s);
199  SPOT_ASSERT(!s->succ || g_.is_valid_edge(s->succ));
200 
201  if (this->iter_cache_)
202  {
203  auto it =
204  down_cast<kripke_graph_succ_iterator<graph_t>*>(this->iter_cache_);
205  it->recycle(s);
206  this->iter_cache_ = nullptr;
207  return it;
208  }
209  return new kripke_graph_succ_iterator<graph_t>(&g_, s);
210 
211  }
212 
213  graph_t::state
214  state_number(const state* st) const
215  {
216  auto s = down_cast<const typename graph_t::state_storage_t*>(st);
217  SPOT_ASSERT(s);
218  return s - &g_.state_storage(0);
219  }
220 
221  const kripke_graph_state*
222  state_from_number(graph_t::state n) const
223  {
224  return &g_.state_data(n);
225  }
226 
227  kripke_graph_state*
228  state_from_number(graph_t::state n)
229  {
230  return &g_.state_data(n);
231  }
232 
233  std::string format_state(unsigned n) const
234  {
235  std::stringstream ss;
236  ss << n;
237  return ss.str();
238  }
239 
240  virtual std::string format_state(const state* st) const override
241  {
242  return format_state(state_number(st));
243  }
244 
246  virtual bdd state_condition(const state* s) const override
247  {
248  auto gs = down_cast<const kripke_graph_state*>(s);
249  SPOT_ASSERT(gs);
250  return gs->cond();
251  }
252 
253  edge_storage_t& edge_storage(unsigned t)
254  {
255  return g_.edge_storage(t);
256  }
257 
258  const edge_storage_t edge_storage(unsigned t) const
259  {
260  return g_.edge_storage(t);
261  }
262 
263  unsigned new_state(bdd cond)
264  {
265  return g_.new_state(cond);
266  }
267 
268  unsigned new_states(unsigned n, bdd cond)
269  {
270  return g_.new_states(n, cond);
271  }
272 
273  unsigned new_edge(unsigned src, unsigned dst)
274  {
275  return g_.new_edge(src, dst);
276  }
277  };
278 
279  typedef std::shared_ptr<kripke_graph> kripke_graph_ptr;
280 
281  inline kripke_graph_ptr
282  make_kripke_graph(const bdd_dict_ptr& d)
283  {
284  return std::make_shared<kripke_graph>(d);
285  }
286 }
virtual bdd cond() const override
Get the condition on the edge leading to this successor.
Definition: graph.hh:32
unsigned num_edges() const
The number of edges in the automaton.
Definition: graph.hh:639
virtual kripke_graph_state * clone() const override
Duplicate a state.
Definition: kripkegraph.hh:62
edge_storage_t & edge_storage(edge s)
return a reference to the storage of an edge
Definition: graph.hh:715
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 new_state(Args &&...args)
Create a new states.
Definition: graph.hh:650
Interface for a Kripke structure.
Definition: kripke.hh:90
unsigned num_states() const
The number of states in the automaton.
Definition: graph.hh:631
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:119
virtual size_t hash() const override
Hash a state.
Definition: kripkegraph.hh:55
Definition: graph.hh:158
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
state new_states(unsigned n, Args &&...args)
Create n new states.
Definition: graph.hh:664
virtual bdd state_condition(const state *s) const override
Get the condition on the state.
Definition: kripkegraph.hh:246
virtual bool done() const override
Check whether the iteration is finished.
Definition: kripkegraph.hh:125
bool is_valid_edge(edge t) const
Test whether the given edge is valid.
Definition: graph.hh:879
edge new_edge(state src, out_state dst, Args &&...args)
Create a new edge.
Definition: graph.hh:752
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:195
virtual const kripke_graph_state * get_init_state() const override
Get the initial state of the automaton.
Definition: kripkegraph.hh:185
state_storage_t & state_storage(state s)
return a reference to the storage of a state
Definition: graph.hh:679
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:240
state_storage_t::data_t & state_data(state s)
return the State_Data associated to a state
Definition: graph.hh:697
Definition: kripkegraph.hh:86

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Mon Nov 21 2016 08:26:36 for spot by doxygen 1.8.8