spot 2.11.4.dev
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
27namespace 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 reinterpret_cast<size_t>(this);
68 }
69
70 virtual kripke_graph_state*
71 clone() const override
72 {
73 return const_cast<kripke_graph_state*>(this);
74 }
75
76 virtual void destroy() const override
77 {
78 }
79
80 bdd cond() const
81 {
82 return cond_;
83 }
84
85 void cond(bdd c)
86 {
87 cond_ = c;
88 }
89
90 private:
91 bdd cond_;
92 };
93
94 template<class Graph>
96 {
97 private:
98 typedef typename Graph::edge edge;
99 typedef typename Graph::state_data_t state;
100 const Graph* g_;
101 edge t_;
102 edge p_;
103 public:
104 kripke_graph_succ_iterator(const Graph* g,
105 const typename Graph::state_storage_t* s):
106 kripke_succ_iterator(s->cond()),
107 g_(g),
108 t_(s->succ)
109 {
110 }
111
113 {
114 }
115
116 void recycle(const typename Graph::state_storage_t* s)
117 {
118 cond_ = s->cond();
119 t_ = s->succ;
120 }
121
122 virtual bool first() override
123 {
124 p_ = t_;
125 return p_;
126 }
127
128 virtual bool next() override
129 {
130 p_ = g_->edge_storage(p_).next_succ;
131 return p_;
132 }
133
134 virtual bool done() const override
135 {
136 return !p_;
137 }
138
139 virtual kripke_graph_state* dst() const override
140 {
141 SPOT_ASSERT(!done());
142 return const_cast<kripke_graph_state*>
143 (&g_->state_data(g_->edge_storage(p_).dst));
144 }
145 };
146
147
150 class SPOT_API kripke_graph final : public kripke
151 {
152 public:
154 // We avoid using graph_t::edge_storage_t because graph_t is not
155 // instantiated in the SWIG bindings, and SWIG would therefore
156 // handle graph_t::edge_storage_t as an abstract type.
157 typedef internal::edge_storage<unsigned, unsigned, unsigned,
159 <void, true>>
161 static_assert(std::is_same<typename graph_t::edge_storage_t,
162 edge_storage_t>::value, "type mismatch");
163
164 typedef internal::distate_storage<unsigned,
167 static_assert(std::is_same<typename graph_t::state_storage_t,
168 state_storage_t>::value, "type mismatch");
169 typedef std::vector<state_storage_t> state_vector;
170
171 // We avoid using graph_t::state for the very same reason.
172 typedef unsigned state_num;
173 static_assert(std::is_same<typename graph_t::state, state_num>::value,
174 "type mismatch");
175
176 protected:
177 graph_t g_;
178 mutable unsigned init_number_;
179 public:
180 kripke_graph(const bdd_dict_ptr& d)
181 : kripke(d), init_number_(0)
182 {
183 }
184
185 virtual ~kripke_graph()
186 {
187 get_dict()->unregister_all_my_variables(this);
188 }
189
190 unsigned num_states() const
191 {
192 return g_.num_states();
193 }
194
195 unsigned num_edges() const
196 {
197 return g_.num_edges();
198 }
199
200 void set_init_state(state_num s)
201 {
202 if (SPOT_UNLIKELY(s >= num_states()))
203 throw std::invalid_argument
204 ("set_init_state() called with nonexisiting state");
205 init_number_ = s;
206 }
207
208 state_num get_init_state_number() const
209 {
210 // If the kripke has no state, it has no initial state.
211 if (num_states() == 0)
212 throw std::runtime_error("kripke has no state at all");
213 return init_number_;
214 }
215
216 virtual const kripke_graph_state* get_init_state() const override
217 {
218 return state_from_number(get_init_state_number());
219 }
220
224 succ_iter(const spot::state* st) const override
225 {
226 auto s = down_cast<const typename graph_t::state_storage_t*>(st);
227 SPOT_ASSERT(!s->succ || g_.is_valid_edge(s->succ));
228
229 if (this->iter_cache_)
230 {
231 auto it =
232 down_cast<kripke_graph_succ_iterator<graph_t>*>(this->iter_cache_);
233 it->recycle(s);
234 this->iter_cache_ = nullptr;
235 return it;
236 }
237 return new kripke_graph_succ_iterator<graph_t>(&g_, s);
238
239 }
240
241 state_num
242 state_number(const state* st) const
243 {
244 auto s = down_cast<const typename graph_t::state_storage_t*>(st);
245 return s - &g_.state_storage(0);
246 }
247
248 const kripke_graph_state*
249 state_from_number(state_num n) const
250 {
251 return &g_.state_data(n);
252 }
253
254 kripke_graph_state*
255 state_from_number(state_num n)
256 {
257 return &g_.state_data(n);
258 }
259
260 std::string format_state(unsigned n) const
261 {
262 auto named = get_named_prop<std::vector<std::string>>("state-names");
263 if (named && n < named->size())
264 return (*named)[n];
265
266 return std::to_string(n);
267 }
268
269 virtual std::string format_state(const state* st) const override
270 {
271 return format_state(state_number(st));
272 }
273
275 virtual bdd state_condition(const state* s) const override
276 {
277 auto gs = down_cast<const kripke_graph_state*>(s);
278 return gs->cond();
279 }
280
281 edge_storage_t& edge_storage(unsigned t)
282 {
283 return g_.edge_storage(t);
284 }
285
286 const edge_storage_t edge_storage(unsigned t) const
287 {
288 return g_.edge_storage(t);
289 }
290
291 unsigned new_state(bdd cond)
292 {
293 return g_.new_state(cond);
294 }
295
296 unsigned new_states(unsigned n, bdd cond)
297 {
298 return g_.new_states(n, cond);
299 }
300
301 unsigned new_edge(unsigned src, unsigned dst)
302 {
303 return g_.new_edge(src, dst);
304 }
305
306
307#ifndef SWIG
308 const state_vector& states() const
309 {
310 return g_.states();
311 }
312#endif
313
314 state_vector& states()
315 {
316 return g_.states();
317 }
318
319#ifndef SWIG
320 internal::all_trans<const graph_t>
321 edges() const noexcept
322 {
323 return g_.edges();
324 }
325#endif
326
327 internal::all_trans<graph_t>
328 edges() noexcept
329 {
330 return g_.edges();
331 }
332
333#ifndef SWIG
334 internal::state_out<const graph_t>
335 out(unsigned src) const
336 {
337 return g_.out(src);
338 }
339#endif
340
341 internal::state_out<graph_t>
342 out(unsigned src)
343 {
344 return g_.out(src);
345 }
346
347 };
348
349 typedef std::shared_ptr<kripke_graph> kripke_graph_ptr;
350
351 inline kripke_graph_ptr
352 make_kripke_graph(const bdd_dict_ptr& d)
353 {
354 return std::make_shared<kripke_graph>(d);
355 }
356}
unsigned num_states() const
The number of states in the automaton.
Definition: graph.hh:649
state new_states(unsigned n, Args &&... args)
Create n new states.
Definition: graph.hh:688
state new_state(Args &&... args)
Create a new states.
Definition: graph.hh:674
bool is_valid_edge(edge t) const
Test whether the given edge is valid.
Definition: graph.hh:988
internal::state_out< digraph > out(state src)
Return a fake container with all edges leaving src.
Definition: graph.hh:893
state_storage_t::data_t & state_data(state s)
return the State_Data associated to a state
Definition: graph.hh:721
edge_storage_t & edge_storage(edge s)
return a reference to the storage of an edge
Definition: graph.hh:739
const state_vector & states() const
Return the vector of states.
Definition: graph.hh:937
internal::all_trans< const digraph > edges() const
Return a fake container with all edges (exluding erased edges)
Definition: graph.hh:952
unsigned num_edges() const
The number of edges in the automaton.
Definition: graph.hh:657
state_storage_t & state_storage(state s)
return a reference to the storage of a state
Definition: graph.hh:703
edge new_edge(state src, state dst, Args &&... args)
Create a new edge.
Definition: graph.hh:776
Definition: kripkegraph.hh:96
virtual bool first() override
Position the iterator on the first successor (if any).
Definition: kripkegraph.hh:122
virtual bool done() const override
Check whether the iteration is finished.
Definition: kripkegraph.hh:134
virtual bool next() override
Jump to the next successor (if any).
Definition: kripkegraph.hh:128
virtual kripke_graph_state * dst() const override
Get the destination state of the current edge.
Definition: kripkegraph.hh:139
Kripke Structure.
Definition: kripkegraph.hh:151
virtual std::string format_state(const state *st) const override
Format the state as a string for printing.
Definition: kripkegraph.hh:269
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:224
virtual bdd state_condition(const state *s) const override
Get the condition on the state.
Definition: kripkegraph.hh:275
virtual const kripke_graph_state * get_init_state() const override
Get the initial state of the automaton.
Definition: kripkegraph.hh:216
Iterator code for Kripke structure.
Definition: kripke.hh:131
virtual bdd cond() const override
Get the condition on the edge leading to this successor.
Interface for a Kripke structure.
Definition: kripke.hh:178
Abstract class for states.
Definition: twa.hh:51
LTL/PSL formula interface.
Definition: automata.hh:27
Definition: graph.hh:66
Definition: graph.hh:163
Definition: graph.hh:188
Concrete class for kripke_graph states.
Definition: kripkegraph.hh:31
virtual size_t hash() const override
Hash a state.
Definition: kripkegraph.hh:65
virtual kripke_graph_state * clone() const override
Duplicate a state.
Definition: kripkegraph.hh:71
virtual void destroy() const override
Release a state.
Definition: kripkegraph.hh:76
virtual int compare(const spot::state *other) const override
Compares two states (that come from the same automaton).
Definition: kripkegraph.hh:53

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