spot 2.12.2
kripkegraph.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) by the Spot authors, see the AUTHORS file for details.
3//
4// This file is part of Spot, a model checking library.
5//
6// Spot is free software; you can redistribute it and/or modify it
7// under the terms of the GNU General Public License as published by
8// the Free Software Foundation; either version 3 of the License, or
9// (at your option) any later version.
10//
11// Spot is distributed in the hope that it will be useful, but WITHOUT
12// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
13// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
14// License for more details.
15//
16// You should have received a copy of the GNU General Public License
17// along with this program. If not, see <http://www.gnu.org/licenses/>.
18
19#pragma once
20
21#include <iosfwd>
22#include <spot/kripke/kripke.hh>
23#include <spot/graph/graph.hh>
24#include <spot/tl/formula.hh>
25
26namespace spot
27{
29 struct SPOT_API kripke_graph_state: public spot::state
30 {
31 public:
32 kripke_graph_state(bdd cond = bddfalse) noexcept
33 : cond_(cond)
34 {
35 }
36
37 kripke_graph_state(const kripke_graph_state& other) noexcept
38 : cond_(other.cond_)
39 {
40 }
41
42 kripke_graph_state& operator=(const kripke_graph_state& other) noexcept
43 {
44 cond_ = other.cond_;
45 return *this;
46 }
47
48 virtual ~kripke_graph_state() noexcept
49 {
50 }
51
52 virtual int compare(const spot::state* other) const override
53 {
54 auto o = down_cast<const kripke_graph_state*>(other);
55
56 // Do not simply return "other - this", it might not fit in an int.
57 if (o < this)
58 return -1;
59 if (o > this)
60 return 1;
61 return 0;
62 }
63
64 virtual size_t hash() const override
65 {
66 return reinterpret_cast<size_t>(this);
67 }
68
69 virtual kripke_graph_state*
70 clone() const override
71 {
72 return const_cast<kripke_graph_state*>(this);
73 }
74
75 virtual void destroy() const override
76 {
77 }
78
79 bdd cond() const
80 {
81 return cond_;
82 }
83
84 void cond(bdd c)
85 {
86 cond_ = c;
87 }
88
89 private:
90 bdd cond_;
91 };
92
93 template<class Graph>
95 {
96 private:
97 typedef typename Graph::edge edge;
98 typedef typename Graph::state_data_t state;
99 const Graph* g_;
100 edge t_;
101 edge p_;
102 public:
103 kripke_graph_succ_iterator(const Graph* g,
104 const typename Graph::state_storage_t* s):
105 kripke_succ_iterator(s->cond()),
106 g_(g),
107 t_(s->succ)
108 {
109 }
110
112 {
113 }
114
115 void recycle(const typename Graph::state_storage_t* s)
116 {
117 cond_ = s->cond();
118 t_ = s->succ;
119 }
120
121 virtual bool first() override
122 {
123 p_ = t_;
124 return p_;
125 }
126
127 virtual bool next() override
128 {
129 p_ = g_->edge_storage(p_).next_succ;
130 return p_;
131 }
132
133 virtual bool done() const override
134 {
135 return !p_;
136 }
137
138 virtual kripke_graph_state* dst() const override
139 {
140 SPOT_ASSERT(!done());
141 return const_cast<kripke_graph_state*>
142 (&g_->state_data(g_->edge_storage(p_).dst));
143 }
144 };
145
146
149 class SPOT_API kripke_graph final : public kripke
150 {
151 public:
153 // We avoid using graph_t::edge_storage_t because graph_t is not
154 // instantiated in the SWIG bindings, and SWIG would therefore
155 // handle graph_t::edge_storage_t as an abstract type.
156 typedef internal::edge_storage<unsigned, unsigned, unsigned,
158 <void, true>>
160 static_assert(std::is_same<typename graph_t::edge_storage_t,
161 edge_storage_t>::value, "type mismatch");
162
163 typedef internal::distate_storage<unsigned,
166 static_assert(std::is_same<typename graph_t::state_storage_t,
167 state_storage_t>::value, "type mismatch");
168 typedef std::vector<state_storage_t> state_vector;
169
170 // We avoid using graph_t::state for the very same reason.
171 typedef unsigned state_num;
172 static_assert(std::is_same<typename graph_t::state, state_num>::value,
173 "type mismatch");
174
175 protected:
176 graph_t g_;
177 mutable unsigned init_number_;
178 public:
179 kripke_graph(const bdd_dict_ptr& d)
180 : kripke(d), init_number_(0)
181 {
182 }
183
184 virtual ~kripke_graph()
185 {
186 get_dict()->unregister_all_my_variables(this);
187 }
188
189 unsigned num_states() const
190 {
191 return g_.num_states();
192 }
193
194 unsigned num_edges() const
195 {
196 return g_.num_edges();
197 }
198
199 void set_init_state(state_num s)
200 {
201 if (SPOT_UNLIKELY(s >= num_states()))
202 throw std::invalid_argument
203 ("set_init_state() called with nonexisiting state");
204 init_number_ = s;
205 }
206
207 state_num get_init_state_number() const
208 {
209 // If the kripke has no state, it has no initial state.
210 if (num_states() == 0)
211 throw std::runtime_error("kripke has no state at all");
212 return init_number_;
213 }
214
215 virtual const kripke_graph_state* get_init_state() const override
216 {
217 return state_from_number(get_init_state_number());
218 }
219
223 succ_iter(const spot::state* st) const override
224 {
225 auto s = down_cast<const typename graph_t::state_storage_t*>(st);
226 SPOT_ASSERT(!s->succ || g_.is_valid_edge(s->succ));
227
228 if (this->iter_cache_)
229 {
230 auto it =
231 down_cast<kripke_graph_succ_iterator<graph_t>*>(this->iter_cache_);
232 it->recycle(s);
233 this->iter_cache_ = nullptr;
234 return it;
235 }
236 return new kripke_graph_succ_iterator<graph_t>(&g_, s);
237
238 }
239
240 state_num
241 state_number(const state* st) const
242 {
243 auto s = down_cast<const typename graph_t::state_storage_t*>(st);
244 return s - &g_.state_storage(0);
245 }
246
247 const kripke_graph_state*
248 state_from_number(state_num n) const
249 {
250 return &g_.state_data(n);
251 }
252
253 kripke_graph_state*
254 state_from_number(state_num n)
255 {
256 return &g_.state_data(n);
257 }
258
259 std::string format_state(unsigned n) const
260 {
261 auto named = get_named_prop<std::vector<std::string>>("state-names");
262 if (named && n < named->size())
263 return (*named)[n];
264
265 return std::to_string(n);
266 }
267
268 virtual std::string format_state(const state* st) const override
269 {
270 return format_state(state_number(st));
271 }
272
274 virtual bdd state_condition(const state* s) const override
275 {
276 auto gs = down_cast<const kripke_graph_state*>(s);
277 return gs->cond();
278 }
279
280 edge_storage_t& edge_storage(unsigned t)
281 {
282 return g_.edge_storage(t);
283 }
284
285 const edge_storage_t edge_storage(unsigned t) const
286 {
287 return g_.edge_storage(t);
288 }
289
290 unsigned new_state(bdd cond)
291 {
292 return g_.new_state(cond);
293 }
294
295 unsigned new_states(unsigned n, bdd cond)
296 {
297 return g_.new_states(n, cond);
298 }
299
300 unsigned new_edge(unsigned src, unsigned dst)
301 {
302 return g_.new_edge(src, dst);
303 }
304
305
306#ifndef SWIG
307 const state_vector& states() const
308 {
309 return g_.states();
310 }
311#endif
312
313 state_vector& states()
314 {
315 return g_.states();
316 }
317
318#ifndef SWIG
319 internal::all_trans<const graph_t>
320 edges() const noexcept
321 {
322 return g_.edges();
323 }
324#endif
325
326 internal::all_trans<graph_t>
327 edges() noexcept
328 {
329 return g_.edges();
330 }
331
332#ifndef SWIG
333 internal::state_out<const graph_t>
334 out(unsigned src) const
335 {
336 return g_.out(src);
337 }
338#endif
339
340 internal::state_out<graph_t>
341 out(unsigned src)
342 {
343 return g_.out(src);
344 }
345
346 };
347
348 typedef std::shared_ptr<kripke_graph> kripke_graph_ptr;
349
350 inline kripke_graph_ptr
351 make_kripke_graph(const bdd_dict_ptr& d)
352 {
353 return std::make_shared<kripke_graph>(d);
354 }
355}
unsigned num_states() const
The number of states in the automaton.
Definition: graph.hh:657
state new_states(unsigned n, Args &&... args)
Create n new states.
Definition: graph.hh:696
state new_state(Args &&... args)
Create a new states.
Definition: graph.hh:682
bool is_valid_edge(edge t) const
Test whether the given edge is valid.
Definition: graph.hh:996
internal::state_out< digraph > out(state src)
Return a fake container with all edges leaving src.
Definition: graph.hh:901
state_storage_t::data_t & state_data(state s)
return the State_Data associated to a state
Definition: graph.hh:729
edge_storage_t & edge_storage(edge s)
return a reference to the storage of an edge
Definition: graph.hh:747
const state_vector & states() const
Return the vector of states.
Definition: graph.hh:945
internal::all_trans< const digraph > edges() const
Return a fake container with all edges (excluding erased edges)
Definition: graph.hh:960
unsigned num_edges() const
The number of edges in the automaton.
Definition: graph.hh:665
state_storage_t & state_storage(state s)
return a reference to the storage of a state
Definition: graph.hh:711
edge new_edge(state src, state dst, Args &&... args)
Create a new edge.
Definition: graph.hh:784
Definition: kripkegraph.hh:95
virtual bool first() override
Position the iterator on the first successor (if any).
Definition: kripkegraph.hh:121
virtual bool done() const override
Check whether the iteration is finished.
Definition: kripkegraph.hh:133
virtual bool next() override
Jump to the next successor (if any).
Definition: kripkegraph.hh:127
virtual kripke_graph_state * dst() const override
Get the destination state of the current edge.
Definition: kripkegraph.hh:138
Kripke Structure.
Definition: kripkegraph.hh:150
virtual std::string format_state(const state *st) const override
Format the state as a string for printing.
Definition: kripkegraph.hh:268
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:223
virtual bdd state_condition(const state *s) const override
Get the condition on the state.
Definition: kripkegraph.hh:274
virtual const kripke_graph_state * get_init_state() const override
Get the initial state of the automaton.
Definition: kripkegraph.hh:215
Iterator code for Kripke structure.
Definition: kripke.hh:130
virtual bdd cond() const override
Get the condition on the edge leading to this successor.
Interface for a Kripke structure.
Definition: kripke.hh:177
Abstract class for states.
Definition: twa.hh:47
LTL/PSL formula interface.
Definition: automata.hh:26
Definition: graph.hh:65
Definition: graph.hh:162
Definition: graph.hh:187
Concrete class for kripke_graph states.
Definition: kripkegraph.hh:30
virtual size_t hash() const override
Hash a state.
Definition: kripkegraph.hh:64
virtual kripke_graph_state * clone() const override
Duplicate a state.
Definition: kripkegraph.hh:70
virtual void destroy() const override
Release a state.
Definition: kripkegraph.hh:75
virtual int compare(const spot::state *other) const override
Compares two states (that come from the same automaton).
Definition: kripkegraph.hh:52

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