47 struct product_state_equal
50 operator()(
const product_state lhs,
51 const product_state rhs)
const
54 return (lhs.st_prop == rhs.st_prop) &&
55 equal(lhs.st_kripke, rhs.st_kripke);
59 struct product_state_hash
62 operator()(
const product_state that)
const noexcept
67 return wang32_hash(that.st_prop) ^ hasher(that.st_kripke);
73 using shared_map = int;
74 using shared_struct = int;
76 static shared_struct* make_shared_structure(shared_map m,
unsigned i)
86 std::atomic<bool>& stop)
87 : sys_(sys), twa_(
twa), tid_(tid), stop_(stop),
91 State, SuccIterator>::value,
92 "error: does not match the kripkecube requirements");
100 sys_.recycle(todo.back().it_kripke, tid_);
108 product_state initial = {sys_.initial(tid_), twa_->get_initial()};
109 if (SPOT_LIKELY(push_state(initial, dfs_number+1, {})))
111 todo.push_back({initial, sys_.succ(initial.st_kripke, tid_),
112 twa_->succ(initial.st_prop)});
115 if (todo.back().it_prop->done())
118 forward_iterators(sys_, twa_, todo.back().it_kripke,
119 todo.back().it_prop,
true, 0);
120 map[initial] = ++dfs_number;
122 while (!todo.empty() && !stop_.load(std::memory_order_relaxed))
126 if (todo.back().it_kripke->done())
128 bool is_init = todo.size() == 1;
129 auto newtop = is_init? todo.back().st: todo[todo.size() -2].st;
130 if (SPOT_LIKELY(pop_state(todo.back().st,
136 sys_.recycle(todo.back().it_kripke, tid_);
139 if (SPOT_UNLIKELY(found_))
151 todo.back().it_kripke->state(),
152 twa_->trans_storage(todo.back().it_prop, tid_).dst
154 auto acc = twa_->trans_data(todo.back().it_prop, tid_).acc_;
155 forward_iterators(sys_, twa_, todo.back().it_kripke,
156 todo.back().it_prop,
false, 0);
157 auto it = map.find(dst);
160 if (SPOT_LIKELY(push_state(dst, dfs_number+1, acc)))
162 map[dst] = ++dfs_number;
163 todo.push_back({dst, sys_.succ(dst.st_kripke, tid_),
164 twa_->succ(dst.st_prop)});
165 forward_iterators(sys_, twa_, todo.back().it_kripke,
166 todo.back().it_prop,
true, 0);
169 else if (SPOT_UNLIKELY(update(todo.back().st,
171 dst, map[dst], acc)))
184 tm_.start(
"DFS thread " + std::to_string(tid_));
190 roots_.push_back({dfsnum, cond, {}});
201 bool pop_state(product_state,
unsigned top_dfsnum,
bool,
202 product_state,
unsigned)
204 if (top_dfsnum == roots_.back().dfsnum)
208 uf_.markdead(top_dfsnum);
210 dfs_ = todo.size() > dfs_ ? todo.size() : dfs_;
217 product_state,
unsigned dst_dfsnum,
220 if (uf_.isdead(dst_dfsnum))
223 while (!uf_.sameset(dst_dfsnum, roots_.back().dfsnum))
225 auto& el = roots_.back();
227 uf_.unite(dst_dfsnum, el.dfsnum);
228 cond |= el.acc | el.ingoing;
230 roots_.back().acc |= cond;
231 found_ = acc_.accepting(roots_.back().acc);
232 if (SPOT_UNLIKELY(found_))
239 bool tst_val =
false;
241 bool exchanged = stop_.compare_exchange_strong(tst_val, new_val);
244 tm_.stop(
"DFS thread " + std::to_string(tid_));
252 unsigned int states()
257 unsigned int transitions()
264 return tm_.timer(
"DFS thread " + std::to_string(tid_)).walltime();
269 return "renault_lpar13";
279 return !found_ ? mc_rvalue::EMPTY : mc_rvalue::NOT_EMPTY;
285 std::string res =
"Prefix:\n";
289 res +=
" " + std::to_string(s.st.st_prop) +
290 +
"*" + sys_.to_string(s.st.st_kripke) +
"\n";
297 const product_state* prod_st;
298 ctrx_element* parent_st;
299 SuccIterator* it_kripke;
300 std::shared_ptr<trans_index> it_prop;
302 std::queue<ctrx_element*> bfs;
304 acc_cond::mark_t acc = {};
306 bfs.push(
new ctrx_element({&todo.back().st,
nullptr,
307 sys_.succ(todo.back().st.st_kripke, tid_),
308 twa_->succ(todo.back().st.st_prop)}));
312 auto* front = bfs.front();
315 while (!front->it_kripke->done())
317 while (!front->it_prop->done())
319 if (twa_->get_cubeset().intersect
320 (twa_->trans_data(front->it_prop, tid_).cube_,
321 front->it_kripke->condition()))
323 const product_state dst = {
324 front->it_kripke->state(),
325 twa_->trans_storage(front->it_prop).dst
329 auto it = map.find(dst);
330 if (it == map.end() ||
331 !uf_.sameset(it->second,
332 map[todo.back().st]))
334 front->it_prop->next();
341 auto mark = twa_->trans_data(front->it_prop,
345 ctrx_element* current = front;
346 while (current !=
nullptr)
350 std::to_string(current->prod_st->st_prop) +
352 sys_. to_string(current->prod_st->st_kripke) +
354 current = current->parent_st;
360 auto* e = bfs.front();
361 sys_.recycle(e->it_kripke, tid_);
365 sys_.recycle(front->it_kripke, tid_);
370 if (twa_->acc().accepting(acc))
375 const product_state* q = &(it->first);
376 ctrx_element* root =
new ctrx_element({
378 sys_.succ(q->st_kripke, tid_),
379 twa_->succ(q->st_prop)
386 const product_state* q = &(it->first);
387 ctrx_element* root =
new ctrx_element({
389 sys_.succ(q->st_kripke, tid_),
390 twa_->succ(q->st_prop)
394 front->it_prop->next();
396 front->it_prop->reset();
397 front->it_kripke->next();
399 sys_.recycle(front->it_kripke, tid_);
412 SuccIterator* it_kripke;
413 std::shared_ptr<trans_index> it_prop;
416 struct root_element {
418 acc_cond::mark_t ingoing;
419 acc_cond::mark_t acc;
422 typedef std::unordered_map<
const product_state, int,
424 product_state_equal> visited_map;
426 kripkecube<State, SuccIterator>& sys_;
428 std::vector<todo_element> todo;
430 unsigned int dfs_number = 0;
431 unsigned int trans_ = 0;
433 std::atomic<bool>& stop_;
435 std::vector<root_element> roots_;
441 bool finisher_ =
false;