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>
36 template<
typename State,
typename SuccIterator,
37 typename StateHash,
typename StateEqual>
49 std::atomic<bool> blue;
50 std::atomic<bool> red;
64 state_hasher(
const product_state&)
67 state_hasher() =
default;
69 brick::hash::hash128_t
70 hash(
const product_state& lhs)
const
74 unsigned u = hash(lhs.st_kripke) % (1<<30);
80 bool equal(
const product_state& lhs,
81 const product_state& rhs)
const
84 return (lhs.st_prop == rhs.st_prop)
85 && equal(lhs.st_kripke, rhs.st_kripke);
92 SuccIterator* it_kripke;
93 std::shared_ptr<trans_index> it_prop;
100 using shared_map = brick::hashset::FastConcurrent <product_state,
104 static shared_struct* make_shared_structure(
shared_map m,
unsigned i)
110 shared_map& map, shared_struct* ,
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)),
119 State, SuccIterator>::value,
120 "error: does not match the kripkecube requirements");
121 SPOT_ASSERT(nb_th_ > tid);
124 virtual ~swarmed_cndfs()
126 while (!todo_blue_.empty())
128 sys_.recycle(todo_blue_.back().it_kripke, tid_);
129 todo_blue_.pop_back();
131 while (!todo_red_.empty())
133 sys_.recycle(todo_red_.back().it_kripke, tid_);
134 todo_red_.pop_back();
147 tm_.start(
"DFS thread " + std::to_string(tid_));
150 std::pair<bool, product_state>
151 push_blue(product_state s,
bool from_accepting)
153 cndfs_colors* c = (cndfs_colors*) p_colors_.allocate();
156 for (
unsigned i = 0; i < nb_th_; ++i)
158 c->l[i].cyan =
false;
159 c->l[i].is_in_Rp =
false;
165 auto it = map_.insert(s);
172 p_colors_.deallocate(c);
173 bool blue = ((*it)).colors->blue.load();
174 bool cyan = ((*it)).colors->l[tid_].cyan;
180 ((*it)).colors->l[tid_].cyan =
true;
182 todo_blue_.push_back({*it,
183 sys_.succ(((*it)).st_kripke, tid_),
184 twa_->succ(((*it)).st_prop),
189 std::pair<bool, product_state>
190 push_red(product_state s,
bool ignore_cyan)
193 auto it = map_.insert(s);
194 SPOT_ASSERT(!it.isnew());
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)
202 ((*it)).colors->l[tid_].is_in_Rp =
true;
205 todo_red_.push_back({*it,
206 sys_.succ(((*it)).st_kripke, tid_),
207 twa_->succ(((*it)).st_prop),
215 dfs_ = todo_blue_.size() > dfs_ ? todo_blue_.size() : dfs_;
217 todo_blue_.back().st.colors->l[tid_].cyan =
false;
218 sys_.recycle(todo_blue_.back().it_kripke, tid_);
219 todo_blue_.pop_back();
226 dfs_ = todo_blue_.size() + todo_red_.size() > dfs_ ?
227 todo_blue_.size() + todo_red_.size() : dfs_;
230 sys_.recycle(todo_red_.back().it_kripke, tid_);
231 todo_red_.pop_back();
237 bool tst_val =
false;
239 bool exchanged = stop_.compare_exchange_strong(tst_val, new_val);
242 tm_.stop(
"DFS thread " + std::to_string(tid_));
255 unsigned transitions()
262 return tm_.timer(
"DFS thread " + std::to_string(tid_)).walltime();
282 SPOT_ASSERT(!is_empty_);
284 auto state_equal = [equal](product_state a, product_state b)
286 return a.st_prop == b.st_prop
287 && equal(a.st_kripke, b.st_kripke);
290 std::string res =
"Prefix:\n";
292 auto it = todo_blue_.begin();
293 while (it != todo_blue_.end())
295 if (state_equal(((*it)).st, cycle_start_))
297 res +=
" " + std::to_string(((*it)).st.st_prop)
298 +
"*" + sys_.to_string(((*it)).st.st_kripke) +
"\n";
303 while (it != todo_blue_.end())
305 res +=
" " + std::to_string(((*it)).st.st_prop)
306 +
"*" + sys_.to_string(((*it)).st.st_kripke) +
"\n";
310 if (!todo_red_.empty())
312 it = todo_red_.begin() + 1;
313 while (it != todo_red_.end())
315 res +=
" " + std::to_string(((*it)).st.st_prop)
316 +
"*" + sys_.to_string(((*it)).st.st_kripke) +
"\n";
320 res +=
" " + std::to_string(cycle_start_.st_prop)
321 +
"*" + sys_.to_string(cycle_start_.st_kripke) +
"\n";
329 product_state initial = {sys_.initial(tid_),
332 if (!push_blue(initial,
false).first)
336 if (todo_blue_.back().it_prop->done())
339 forward_iterators(sys_, twa_, todo_blue_.back().it_kripke,
340 todo_blue_.back().it_prop,
true, tid_);
342 while (!todo_blue_.empty() && !stop_.load(std::memory_order_relaxed))
344 auto current = todo_blue_.back();
346 if (!current.it_kripke->done())
350 current.it_kripke->state(),
351 twa_->trans_storage(current.it_prop, tid_).dst,
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_);
359 auto tmp = push_blue(s, acc);
361 forward_iterators(sys_, twa_, todo_blue_.back().it_kripke,
362 todo_blue_.back().it_prop,
true, tid_);
368 if (tmp.second.colors->l[tid_].cyan)
376 SPOT_ASSERT(tmp.second.colors->blue);
386 current.st.colors->blue.store(
true);
389 if (current.from_accepting)
391 red_dfs(todo_blue_.back().st);
404 for (product_state& s: Rp_acc_)
406 while (s.colors->red.load() && !stop_.load())
411 for (product_state& s: Rp_)
413 s.colors->red.store(
true);
414 s.colors->l[tid_].is_in_Rp =
false;
421 void red_dfs(product_state initial)
423 auto init_push = push_red(initial,
true);
424 SPOT_ASSERT(init_push.second.colors->blue);
426 if (!init_push.first)
429 forward_iterators(sys_, twa_, todo_red_.back().it_kripke,
430 todo_red_.back().it_prop,
true, tid_);
432 while (!todo_red_.empty() && !stop_.load(std::memory_order_relaxed))
434 auto current = todo_red_.back();
436 if (!current.it_kripke->done())
440 current.it_kripke->state(),
441 twa_->trans_storage(current.it_prop, tid_).dst,
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_);
448 auto res = push_red(s,
false);
451 forward_iterators(sys_, twa_, todo_red_.back().it_kripke,
452 todo_red_.back().it_prop,
true, tid_);
454 SPOT_ASSERT(res.second.colors->blue);
462 for (
auto& st: Rp_acc_)
464 if (st.colors == res.second.colors)
471 Rp_acc_.push_back(Rp_.back());
476 if (res.second.colors->l[tid_].cyan)
481 if (init_push.second.colors == res.second.colors && !acc)
488 else if (acc && res.second.colors->l[tid_].is_in_Rp)
490 auto it = map_.insert(s);
491 Rp_acc_.push_back(*it);
502 kripkecube<State, SuccIterator>& sys_;
504 std::vector<todo_element> todo_blue_;
505 std::vector<todo_element> todo_red_;
506 unsigned transitions_ = 0;
510 unsigned states_ = 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;
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
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
@ NOT_EMPTY
The product is not empty.
@ EMPTY
The product is empty.