spot  2.7.1
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:
156  protected:
157  graph_t g_;
158  mutable unsigned init_number_;
159  public:
160  kripke_graph(const bdd_dict_ptr& d)
161  : kripke(d), init_number_(0)
162  {
163  }
164 
165  virtual ~kripke_graph()
166  {
167  get_dict()->unregister_all_my_variables(this);
168  }
169 
170  unsigned num_states() const
171  {
172  return g_.num_states();
173  }
174 
175  unsigned num_edges() const
176  {
177  return g_.num_edges();
178  }
179 
180  void set_init_state(graph_t::state s)
181  {
182  if (SPOT_UNLIKELY(s >= num_states()))
183  throw std::invalid_argument
184  ("set_init_state() called with nonexisiting state");
185  init_number_ = s;
186  }
187 
188  graph_t::state get_init_state_number() const
189  {
190  // If the kripke has no state, it has no initial state.
191  if (num_states() == 0)
192  throw std::runtime_error("kripke has no state at all");
193  return init_number_;
194  }
195 
196  virtual const kripke_graph_state* get_init_state() const override
197  {
198  return state_from_number(get_init_state_number());
199  }
200 
204  succ_iter(const spot::state* st) const override
205  {
206  auto s = down_cast<const typename graph_t::state_storage_t*>(st);
207  SPOT_ASSERT(!s->succ || g_.is_valid_edge(s->succ));
208 
209  if (this->iter_cache_)
210  {
211  auto it =
212  down_cast<kripke_graph_succ_iterator<graph_t>*>(this->iter_cache_);
213  it->recycle(s);
214  this->iter_cache_ = nullptr;
215  return it;
216  }
217  return new kripke_graph_succ_iterator<graph_t>(&g_, s);
218 
219  }
220 
221  graph_t::state
222  state_number(const state* st) const
223  {
224  auto s = down_cast<const typename graph_t::state_storage_t*>(st);
225  return s - &g_.state_storage(0);
226  }
227 
228  const kripke_graph_state*
229  state_from_number(graph_t::state n) const
230  {
231  return &g_.state_data(n);
232  }
233 
235  state_from_number(graph_t::state n)
236  {
237  return &g_.state_data(n);
238  }
239 
240  std::string format_state(unsigned n) const
241  {
242  auto named = get_named_prop<std::vector<std::string>>("state-names");
243  if (named && n < named->size())
244  return (*named)[n];
245 
246  return std::to_string(n);
247  }
248 
249  virtual std::string format_state(const state* st) const override
250  {
251  return format_state(state_number(st));
252  }
253 
255  virtual bdd state_condition(const state* s) const override
256  {
257  auto gs = down_cast<const kripke_graph_state*>(s);
258  return gs->cond();
259  }
260 
261  edge_storage_t& edge_storage(unsigned t)
262  {
263  return g_.edge_storage(t);
264  }
265 
266  const edge_storage_t edge_storage(unsigned t) const
267  {
268  return g_.edge_storage(t);
269  }
270 
271  unsigned new_state(bdd cond)
272  {
273  return g_.new_state(cond);
274  }
275 
276  unsigned new_states(unsigned n, bdd cond)
277  {
278  return g_.new_states(n, cond);
279  }
280 
281  unsigned new_edge(unsigned src, unsigned dst)
282  {
283  return g_.new_edge(src, dst);
284  }
285  };
286 
287  typedef std::shared_ptr<kripke_graph> kripke_graph_ptr;
288 
289  inline kripke_graph_ptr
290  make_kripke_graph(const bdd_dict_ptr& d)
291  {
292  return std::make_shared<kripke_graph>(d);
293  }
294 }
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
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
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
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
virtual bdd state_condition(const state *s) const override
Get the condition on the state.
Definition: kripkegraph.hh:255
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:204
virtual const kripke_graph_state * get_init_state() const override
Get the initial state of the automaton.
Definition: kripkegraph.hh:196
virtual int compare(const spot::state *other) const override
Compares two states (that come from the same automaton).
Definition: kripkegraph.hh:53
virtual std::string format_state(const state *st) const override
Format the state as a string for printing.
Definition: kripkegraph.hh:249
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