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

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