spot 2.11.6.dev
Loading...
Searching...
No Matches
cndfs.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2015-2020, 2022 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 <atomic>
23#include <thread>
24#include <vector>
25
26#include <spot/bricks/brick-hashset>
27#include <spot/kripke/kripke.hh>
28#include <spot/misc/common.hh>
29#include <spot/misc/fixpool.hh>
30#include <spot/misc/timer.hh>
31#include <spot/twacube/twacube.hh>
32#include <spot/mc/mc.hh>
33
34namespace spot
35{
36 template<typename State, typename SuccIterator,
37 typename StateHash, typename StateEqual>
38 class SPOT_API swarmed_cndfs
39 {
40 struct local_colors
41 {
42 bool cyan;
43 bool is_in_Rp;
44 };
45
47 struct cndfs_colors
48 {
49 std::atomic<bool> blue;
50 std::atomic<bool> red;
51 local_colors l[1];
52 };
53
54 struct product_state
55 {
56 State st_kripke;
57 unsigned st_prop;
58 cndfs_colors* colors;
59 };
60
62 struct state_hasher
63 {
64 state_hasher(const product_state&)
65 { }
66
67 state_hasher() = default;
68
69 brick::hash::hash128_t
70 hash(const product_state& lhs) const
71 {
72 StateHash hash;
73 // Not modulo 31 according to brick::hashset specifications.
74 unsigned u = hash(lhs.st_kripke) % (1<<30);
75 u = wang32_hash(lhs.st_prop) ^ u;
76 u = u % (1<<30);
77 return {u, u};
78 }
79
80 bool equal(const product_state& lhs,
81 const product_state& rhs) const
82 {
83 StateEqual equal;
84 return (lhs.st_prop == rhs.st_prop)
85 && equal(lhs.st_kripke, rhs.st_kripke);
86 }
87 };
88
89 struct todo_element
90 {
91 product_state st;
92 SuccIterator* it_kripke;
93 std::shared_ptr<trans_index> it_prop;
94 bool from_accepting;
95 };
96
97 public:
98
100 using shared_map = brick::hashset::FastConcurrent <product_state,
101 state_hasher>;
102 using shared_struct = shared_map;
103
104 static shared_struct* make_shared_structure(shared_map m, unsigned i)
105 {
106 return nullptr; // Useless here.
107 }
108
110 shared_map& map, shared_struct* /* useless here*/,
111 unsigned tid, std::atomic<bool>& stop):
112 sys_(sys), twa_(twa), tid_(tid), map_(map),
113 nb_th_(std::thread::hardware_concurrency()),
114 p_colors_(sizeof(cndfs_colors) +
115 sizeof(local_colors)*(std::thread::hardware_concurrency() - 1)),
116 stop_(stop)
117 {
118 static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
119 State, SuccIterator>::value,
120 "error: does not match the kripkecube requirements");
121 SPOT_ASSERT(nb_th_ > tid);
122 }
123
124 virtual ~swarmed_cndfs()
125 {
126 while (!todo_blue_.empty())
127 {
128 sys_.recycle(todo_blue_.back().it_kripke, tid_);
129 todo_blue_.pop_back();
130 }
131 while (!todo_red_.empty())
132 {
133 sys_.recycle(todo_red_.back().it_kripke, tid_);
134 todo_red_.pop_back();
135 }
136 }
137
138 void run()
139 {
140 setup();
141 blue_dfs();
142 finalize();
143 }
144
145 void setup()
146 {
147 tm_.start("DFS thread " + std::to_string(tid_));
148 }
149
150 std::pair<bool, product_state>
151 push_blue(product_state s, bool from_accepting)
152 {
153 cndfs_colors* c = (cndfs_colors*) p_colors_.allocate();
154 c->red = false;
155 c->blue = false;
156 for (unsigned i = 0; i < nb_th_; ++i)
157 {
158 c->l[i].cyan = false;
159 c->l[i].is_in_Rp = false;
160 }
161
162 s.colors = c;
163
164 // Try to insert the new state in the shared map.
165 auto it = map_.insert(s);
166 bool b = it.isnew();
167
168 // Insertion failed, delete element
169 // FIXME Should we add a local cache to avoid useless allocations?
170 if (!b)
171 {
172 p_colors_.deallocate(c);
173 bool blue = ((*it)).colors->blue.load();
174 bool cyan = ((*it)).colors->l[tid_].cyan;
175 if (blue || cyan)
176 return {false, *it};
177 }
178
179 // Mark state as visited.
180 ((*it)).colors->l[tid_].cyan = true;
181 ++states_;
182 todo_blue_.push_back({*it,
183 sys_.succ(((*it)).st_kripke, tid_),
184 twa_->succ(((*it)).st_prop),
185 from_accepting});
186 return {true, *it};
187 }
188
189 std::pair<bool, product_state>
190 push_red(product_state s, bool ignore_cyan)
191 {
192 // Try to insert the new state in the shared map.
193 auto it = map_.insert(s);
194 SPOT_ASSERT(!it.isnew()); // should never be new in a red DFS
195 bool red = ((*it)).colors->red.load();
196 bool cyan = ((*it)).colors->l[tid_].cyan;
197 bool in_Rp = ((*it)).colors->l[tid_].is_in_Rp;
198 if (red || (cyan && !ignore_cyan) || in_Rp)
199 return {false, *it}; // couldn't insert
200
201 // Mark state as visited.
202 ((*it)).colors->l[tid_].is_in_Rp = true;
203 Rp_.push_back(*it);
204 ++states_;
205 todo_red_.push_back({*it,
206 sys_.succ(((*it)).st_kripke, tid_),
207 twa_->succ(((*it)).st_prop),
208 false});
209 return {true, *it};
210 }
211
212 bool pop_blue()
213 {
214 // Track maximum dfs size
215 dfs_ = todo_blue_.size() > dfs_ ? todo_blue_.size() : dfs_;
216
217 todo_blue_.back().st.colors->l[tid_].cyan = false;
218 sys_.recycle(todo_blue_.back().it_kripke, tid_);
219 todo_blue_.pop_back();
220 return true;
221 }
222
223 bool pop_red()
224 {
225 // Track maximum dfs size
226 dfs_ = todo_blue_.size() + todo_red_.size() > dfs_ ?
227 todo_blue_.size() + todo_red_.size() : dfs_;
228
229
230 sys_.recycle(todo_red_.back().it_kripke, tid_);
231 todo_red_.pop_back();
232 return true;
233 }
234
235 void finalize()
236 {
237 bool tst_val = false;
238 bool new_val = true;
239 bool exchanged = stop_.compare_exchange_strong(tst_val, new_val);
240 if (exchanged)
241 finisher_ = true;
242 tm_.stop("DFS thread " + std::to_string(tid_));
243 }
244
245 bool finisher()
246 {
247 return finisher_;
248 }
249
250 unsigned states()
251 {
252 return states_;
253 }
254
255 unsigned transitions()
256 {
257 return transitions_;
258 }
259
260 unsigned walltime()
261 {
262 return tm_.timer("DFS thread " + std::to_string(tid_)).walltime();
263 }
264
265 std::string name()
266 {
267 return "cndfs";
268 }
269
270 int sccs()
271 {
272 return -1;
273 }
274
275 mc_rvalue result()
276 {
277 return is_empty_ ? mc_rvalue::EMPTY : mc_rvalue::NOT_EMPTY;
278 }
279
280 std::string trace()
281 {
282 SPOT_ASSERT(!is_empty_);
283 StateEqual equal;
284 auto state_equal = [equal](product_state a, product_state b)
285 {
286 return a.st_prop == b.st_prop
287 && equal(a.st_kripke, b.st_kripke);
288 };
289
290 std::string res = "Prefix:\n";
291
292 auto it = todo_blue_.begin();
293 while (it != todo_blue_.end())
294 {
295 if (state_equal(((*it)).st, cycle_start_))
296 break;
297 res += " " + std::to_string(((*it)).st.st_prop)
298 + "*" + sys_.to_string(((*it)).st.st_kripke) + "\n";
299 ++it;
300 }
301
302 res += "Cycle:\n";
303 while (it != todo_blue_.end())
304 {
305 res += " " + std::to_string(((*it)).st.st_prop)
306 + "*" + sys_.to_string(((*it)).st.st_kripke) + "\n";
307 ++it;
308 }
309
310 if (!todo_red_.empty())
311 {
312 it = todo_red_.begin() + 1; // skip first element, also in blue
313 while (it != todo_red_.end())
314 {
315 res += " " + std::to_string(((*it)).st.st_prop)
316 + "*" + sys_.to_string(((*it)).st.st_kripke) + "\n";
317 ++it;
318 }
319 }
320 res += " " + std::to_string(cycle_start_.st_prop)
321 + "*" + sys_.to_string(cycle_start_.st_kripke) + "\n";
322
323 return res;
324 }
325
326 private:
327 void blue_dfs()
328 {
329 product_state initial = {sys_.initial(tid_),
330 twa_->get_initial(),
331 nullptr};
332 if (!push_blue(initial, false).first)
333 return;
334
335 // Property automaton has only one state
336 if (todo_blue_.back().it_prop->done())
337 return;
338
339 forward_iterators(sys_, twa_, todo_blue_.back().it_kripke,
340 todo_blue_.back().it_prop, true, tid_);
341
342 while (!todo_blue_.empty() && !stop_.load(std::memory_order_relaxed))
343 {
344 auto current = todo_blue_.back();
345
346 if (!current.it_kripke->done())
347 {
348 ++transitions_;
349 product_state s = {
350 current.it_kripke->state(),
351 twa_->trans_storage(current.it_prop, tid_).dst,
352 nullptr
353 };
354
355 bool acc = (bool) twa_->trans_storage(current.it_prop, tid_).acc_;
356 forward_iterators(sys_, twa_, todo_blue_.back().it_kripke,
357 todo_blue_.back().it_prop, false, tid_);
358
359 auto tmp = push_blue(s, acc);
360 if (tmp.first)
361 forward_iterators(sys_, twa_, todo_blue_.back().it_kripke,
362 todo_blue_.back().it_prop, true, tid_);
363 else if (acc)
364 {
365 // The state cyan and we can reach it throught an
366 // accepting transition, a accepting cycle has been
367 // found without launching a red dfs
368 if (tmp.second.colors->l[tid_].cyan)
369 {
370 cycle_start_ = s;
371 is_empty_ = false;
372 stop_.store(true);
373 return;
374 }
375
376 SPOT_ASSERT(tmp.second.colors->blue);
377
378 red_dfs(s);
379 if (!is_empty_)
380 return;
381 post_red_dfs();
382 }
383 }
384 else
385 {
386 current.st.colors->blue.store(true);
387
388 // backtracked an accepting transition; launch red DFS
389 if (current.from_accepting)
390 {
391 red_dfs(todo_blue_.back().st);
392 if (!is_empty_)
393 return;
394 post_red_dfs();
395 }
396
397 pop_blue();
398 }
399 }
400 }
401
402 void post_red_dfs()
403 {
404 for (product_state& s: Rp_acc_)
405 {
406 while (s.colors->red.load() && !stop_.load())
407 {
408 // await
409 }
410 }
411 for (product_state& s: Rp_)
412 {
413 s.colors->red.store(true);
414 s.colors->l[tid_].is_in_Rp = false; // empty Rp
415 }
416
417 Rp_.clear();
418 Rp_acc_.clear();
419 }
420
421 void red_dfs(product_state initial)
422 {
423 auto init_push = push_red(initial, true);
424 SPOT_ASSERT(init_push.second.colors->blue);
425
426 if (!init_push.first)
427 return;
428
429 forward_iterators(sys_, twa_, todo_red_.back().it_kripke,
430 todo_red_.back().it_prop, true, tid_);
431
432 while (!todo_red_.empty() && !stop_.load(std::memory_order_relaxed))
433 {
434 auto current = todo_red_.back();
435
436 if (!current.it_kripke->done())
437 {
438 ++transitions_;
439 product_state s = {
440 current.it_kripke->state(),
441 twa_->trans_storage(current.it_prop, tid_).dst,
442 nullptr
443 };
444 bool acc = (bool) twa_->trans_storage(current.it_prop, tid_).acc_;
445 forward_iterators(sys_, twa_, todo_red_.back().it_kripke,
446 todo_red_.back().it_prop, false, tid_);
447
448 auto res = push_red(s, false);
449 if (res.first) // could push properly
450 {
451 forward_iterators(sys_, twa_, todo_red_.back().it_kripke,
452 todo_red_.back().it_prop, true, tid_);
453
454 SPOT_ASSERT(res.second.colors->blue);
455
456 // The transition is accepting, we want to keep
457 // track of this state
458 if (acc)
459 {
460 // Do not insert twice a state
461 bool found = false;
462 for (auto& st: Rp_acc_)
463 {
464 if (st.colors == res.second.colors)
465 {
466 found = true;
467 break;
468 }
469 }
470 if (!found)
471 Rp_acc_.push_back(Rp_.back());
472 }
473 }
474 else
475 {
476 if (res.second.colors->l[tid_].cyan)
477 {
478 // color pointers are unique to each element,
479 // comparing them is equivalent (but faster) to comparing
480 // st_kripke and st_prop individually.
481 if (init_push.second.colors == res.second.colors && !acc)
482 continue;
483 is_empty_ = false;
484 cycle_start_ = s;
485 stop_.store(true);
486 return;
487 }
488 else if (acc && res.second.colors->l[tid_].is_in_Rp)
489 {
490 auto it = map_.insert(s);
491 Rp_acc_.push_back(*it);
492 }
493 }
494 }
495 else
496 {
497 pop_red();
498 }
499 }
500 }
501
502 kripkecube<State, SuccIterator>& sys_;
503 twacube_ptr twa_;
504 std::vector<todo_element> todo_blue_;
505 std::vector<todo_element> todo_red_;
506 unsigned transitions_ = 0;
507 unsigned tid_;
508 shared_map map_;
509 spot::timer_map tm_;
510 unsigned states_ = 0;
511 unsigned dfs_ = 0;
512 unsigned nb_th_ = 0;
513 fixed_size_pool<pool_type::Unsafe> p_colors_;
514 bool is_empty_ = true;
515 std::atomic<bool>& stop_;
516 std::vector<product_state> Rp_;
517 std::vector<product_state> Rp_acc_;
518 product_state cycle_start_;
519 bool finisher_ = false;
520 };
521}
This class allows to ensure (at compile time) if a given parameter is of type kripkecube....
Definition kripke.hh:72
This class is a template representation of a Kripke structure. It is composed of two template paramet...
Definition kripke.hh:41
Definition cndfs.hh:39
brick::hashset::FastConcurrent< product_state, state_hasher > shared_map
<
Definition cndfs.hh:101
A map of timer, where each timer has a name.
Definition timer.hh:229
A Transition-based ω-Automaton.
Definition twa.hh:623
size_t wang32_hash(size_t key)
Thomas Wang's 32 bit hash function.
Definition hashfunc.hh:41
Definition automata.hh:27
mc_rvalue
Definition mc.hh:44

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