spot 2.12.2
utils.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 <spot/mc/intersect.hh>
22#include <spot/twa/twa.hh>
23#include <spot/twacube_algos/convert.hh>
24
25namespace spot
26{
29 template<typename State, typename SuccIterator,
30 typename StateHash, typename StateEqual>
31 class SPOT_API kripkecube_to_twa
32 {
33 public:
34
36 sys_(sys), dict_(dict)
37 {
38 static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
39 State, SuccIterator>::value,
40 "error: does not match the kripkecube requirements");
41 }
42
44 {
45 visited_.clear();
46 }
47
48 void run()
49 {
50 setup();
51 State initial = sys_.initial(0);
52 if (SPOT_LIKELY(push(initial, dfs_number_+1)))
53 {
54 visited_[initial] = dfs_number_++;
55 todo_.push_back({initial, sys_.succ(initial, 0)});
56 }
57 while (!todo_.empty())
58 {
59 if (todo_.back().it->done())
60 {
61 if (SPOT_LIKELY(pop(todo_.back().s)))
62 {
63 sys_.recycle(todo_.back().it, 0);
64 todo_.pop_back();
65 }
66 }
67 else
68 {
69 ++transitions_;
70 State dst = todo_.back().it->state();
71 auto it = visited_.find(dst);
72 if (it == visited_.end())
73 {
74 if (SPOT_LIKELY(push(dst, dfs_number_+1)))
75 {
76 visited_[dst] = dfs_number_++;
77 todo_.back().it->next();
78 todo_.push_back({dst, sys_.succ(dst, 0)});
79 }
80 }
81 else
82 {
83 edge(visited_[todo_.back().s], visited_[dst]);
84 todo_.back().it->next();
85 }
86 }
87 }
88 finalize();
89 }
90
91 void setup()
92 {
93 auto d = spot::make_bdd_dict();
94 res_ = make_twa_graph(d);
95 names_ = new std::vector<std::string>();
96
97 int i = 0;
98 for (auto ap : sys_.ap())
99 {
100 auto idx = res_->register_ap(ap);
101 reverse_binder_[i++] = idx;
102 }
103 }
104
105 bool push(State s, unsigned i)
106 {
107
108 unsigned st = res_->new_state();
109 names_->push_back(sys_.to_string(s));
110 if (!todo_.empty())
111 {
112 edge(visited_[todo_.back().s], st);
113 }
114
115 SPOT_ASSERT(st+1 == i);
116 return true;
117 }
118
119 bool pop(State)
120 {
121 return true;
122 }
123
124 void edge(unsigned src, unsigned dst)
125 {
126 cubeset cs(sys_.ap().size());
127 bdd cond = cube_to_bdd(todo_.back().it->condition(),
128 cs, reverse_binder_);
129 res_->new_edge(src, dst, cond);
130 }
131
132 void finalize()
133 {
134 res_->purge_unreachable_states();
135 res_->set_named_prop<std::vector<std::string>>("state-names", names_);
136 }
137
138 twa_graph_ptr twa()
139 {
140 return res_;
141 }
142
143 protected:
145 {
146 State s;
147 SuccIterator* it;
148 };
149
150 typedef std::unordered_map<const State, int,
151 StateHash, StateEqual> visited__map;
152
154 std::vector<todo__element> todo_;
155 visited__map visited_;
156 unsigned int dfs_number_ = 0;
157 unsigned int transitions_ = 0;
158 spot::twa_graph_ptr res_;
159 std::vector<std::string>* names_;
160 bdd_dict_ptr dict_;
161 std::unordered_map<int, int> reverse_binder_;
162 };
163
166 template<typename State, typename SuccIterator,
167 typename StateHash, typename StateEqual>
168 class SPOT_API product_to_twa
169 {
170 struct product_state
171 {
172 State st_kripke;
173 unsigned st_prop;
174 };
175
176 struct product_state_equal
177 {
178 bool
179 operator()(const product_state lhs,
180 const product_state rhs) const
181 {
182 StateEqual equal;
183 return (lhs.st_prop == rhs.st_prop) &&
184 equal(lhs.st_kripke, rhs.st_kripke);
185 }
186 };
187
188 struct product_state_hash
189 {
190 size_t
191 operator()(const product_state lhs) const noexcept
192 {
193 StateHash hash;
194 unsigned u = hash(lhs.st_kripke) % (1<<30);
195 u = wang32_hash(lhs.st_prop) ^ u;
196 u = u % (1<<30);
197 return u;
198 }
199 };
200
201 public:
203 twacube_ptr twa):
204 sys_(sys), twa_(twa)
205 {
206 static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
207 State, SuccIterator>::value,
208 "error: does not match the kripkecube requirements");
209 }
210
211 virtual ~product_to_twa()
212 {
213 map.clear();
214 }
215
216 bool run()
217 {
218 setup();
219 product_state initial = {sys_.initial(0), twa_->get_initial()};
220 if (SPOT_LIKELY(push_state(initial, dfs_number_+1, {})))
221 {
222 todo_.push_back({initial, sys_.succ(initial.st_kripke, 0),
223 twa_->succ(initial.st_prop)});
224
225 // Not going further! It's a product with a single state.
226 if (todo_.back().it_prop->done())
227 return false;
228
229 forward_iterators(sys_, twa_, todo_.back().it_kripke,
230 todo_.back().it_prop, true, 0);
231 map[initial] = ++dfs_number_;
232 }
233 while (!todo_.empty())
234 {
235 // Check the kripke is enough since it's the outer loop. More
236 // details in forward_iterators.
237 if (todo_.back().it_kripke->done())
238 {
239 bool is_init = todo_.size() == 1;
240 auto newtop = is_init? todo_.back().st: todo_[todo_.size() -2].st;
241 if (SPOT_LIKELY(pop_state(todo_.back().st,
242 map[todo_.back().st],
243 is_init,
244 newtop,
245 map[newtop])))
246 {
247 sys_.recycle(todo_.back().it_kripke, 0);
248 todo_.pop_back();
249 }
250 }
251 else
252 {
253 ++transitions_;
254 product_state dst = {
255 todo_.back().it_kripke->state(),
256 twa_->trans_storage(todo_.back().it_prop, 0).dst
257 };
258 auto acc = twa_->trans_data(todo_.back().it_prop, 0).acc_;
259 forward_iterators(sys_, twa_, todo_.back().it_kripke,
260 todo_.back().it_prop, false, 0);
261 auto it = map.find(dst);
262 if (it == map.end())
263 {
264 if (SPOT_LIKELY(push_state(dst, dfs_number_+1, acc)))
265 {
266 map[dst] = ++dfs_number_;
267 todo_.push_back({dst, sys_.succ(dst.st_kripke, 0),
268 twa_->succ(dst.st_prop)});
269 forward_iterators(sys_, twa_, todo_.back().it_kripke,
270 todo_.back().it_prop, true, 0);
271 }
272 }
273 else if (SPOT_UNLIKELY(update(todo_.back().st, dfs_number_,
274 dst, map[dst], acc)))
275 return true;
276 }
277 }
278 return false;
279 }
280
281 twa_graph_ptr twa()
282 {
283 res_->purge_unreachable_states();
284 res_->set_named_prop<std::vector<std::string>>("state-names", names_);
285 return res_;
286 }
287
288 void setup()
289 {
290 auto d = spot::make_bdd_dict();
291 res_ = make_twa_graph(d);
292 names_ = new std::vector<std::string>();
293
294 int i = 0;
295 for (auto ap : sys_.ap())
296 {
297 auto idx = res_->register_ap(ap);
298 reverse_binder_[i++] = idx;
299 }
300 }
301
302 bool push_state(product_state s, unsigned i, acc_cond::mark_t)
303 {
304 unsigned st = res_->new_state();
305
306 if (!todo_.empty())
307 {
308 auto c = twa_->get_cubeset()
309 .intersection(twa_->trans_data
310 (todo_.back().it_prop).cube_,
311 todo_.back().it_kripke->condition());
312
313 bdd x = spot::cube_to_bdd(c, twa_->get_cubeset(),
314 reverse_binder_);
315 twa_->get_cubeset().release(c);
316 res_->new_edge(map[todo_.back().st]-1, st, x,
317 twa_->trans_data
318 (todo_.back().it_prop).acc_);
319 }
320
321
322 names_->push_back(sys_.to_string(s.st_kripke) +
323 ('*' + std::to_string(s.st_prop)));
324 SPOT_ASSERT(st+1 == i);
325 return true;
326 }
327
328 bool update(product_state, unsigned src,
329 product_state, unsigned dst,
330 acc_cond::mark_t cond)
331 {
332 auto c = twa_->get_cubeset()
333 .intersection(twa_->trans_data
334 (todo_.back().it_prop).cube_,
335 todo_.back().it_kripke->condition());
336
337 bdd x = spot::cube_to_bdd(c, twa_->get_cubeset(),
338 reverse_binder_);
339 twa_->get_cubeset().release(c);
340 res_->new_edge(src-1, dst-1, x, cond);
341 return false;
342 }
343
344 bool pop_state(product_state, unsigned, bool, product_state, unsigned)
345 {
346 return true;
347 }
348
349 private:
350 struct todo__element
351 {
352 product_state st;
353 SuccIterator* it_kripke;
354 std::shared_ptr<trans_index> it_prop;
355 };
356
357 typedef std::unordered_map<const product_state, int,
358 product_state_hash,
359 product_state_equal> visited_map;
360
362 twacube_ptr twa_;
363 std::vector<todo__element> todo_;
364 visited_map map;
365 unsigned int dfs_number_ = 0;
366 unsigned int transitions_ = 0;
367 spot::twa_graph_ptr res_;
368 std::vector<std::string>* names_;
369 std::unordered_map<int, int> reverse_binder_;
370 };
371}
Definition: cube.hh:68
This class allows to ensure (at compile time) if a given parameter is of type kripkecube....
Definition: kripke.hh:71
convert a (cube) model into a twa. Note that this algorithm cannot be run in parallel but could.
Definition: utils.hh:32
This class is a template representation of a Kripke structure. It is composed of two template paramet...
Definition: kripke.hh:40
convert a (cube) product automaton into a twa Note that this algorithm cannot be run in parallel.
Definition: utils.hh:169
A Transition-based ω-Automaton.
Definition: twa.hh:619
void set_named_prop(std::string s, void *val, std::function< void(void *)> destructor)
Declare a named property.
size_t wang32_hash(size_t key)
Thomas Wang's 32 bit hash function.
Definition: hashfunc.hh:37
@ ap
Atomic proposition.
twa_graph_ptr make_twa_graph(const bdd_dict_ptr &dict)
Build an explicit automaton from all states of aut,.
Definition: twagraph.hh:787
Definition: automata.hh:26
bdd cube_to_bdd(spot::cube cube, const cubeset &cubeset, std::unordered_map< int, int > &reverse_binder)
Transform a cube cube into bdd using the map that bind cube indexes to bdd indexes.
An acceptance mark.
Definition: acc.hh:84

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