22#include <spot/twa/acc.hh>
23#include <spot/mc/unionfind.hh>
24#include <spot/mc/intersect.hh>
25#include <spot/mc/mc.hh>
26#include <spot/misc/timer.hh>
27#include <spot/twacube/twacube.hh>
28#include <spot/twacube/fwd.hh>
37 template<
typename State,
typename SuccIterator,
38 typename StateHash,
typename StateEqual>
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";
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;
This class allows to ensure (at compile time) if a given parameter is of type kripkecube....
Definition: kripke.hh:71
This class is a template representation of a Kripke structure. It is composed of two template paramet...
Definition: kripke.hh:40
This class implements the sequential emptiness check as presented in "Three SCC-based Emptiness Check...
Definition: lpar13.hh:40
bool update(product_state, unsigned, product_state, unsigned dst_dfsnum, acc_cond::mark_t cond)
This method is called for every closing, back, or forward edge. Return true if a counterexample has b...
Definition: lpar13.hh:216
bool pop_state(product_state, unsigned top_dfsnum, bool, product_state, unsigned)
This method is called to notify the emptiness checks that a state will be popped. If the method retur...
Definition: lpar13.hh:201
A map of timer, where each timer has a name.
Definition: timer.hh:225
A Transition-based ω-Automaton.
Definition: twa.hh:619
const acc_cond & acc() const
The acceptance condition of the automaton.
Definition: twa.hh:812
size_t wang32_hash(size_t key)
Thomas Wang's 32 bit hash function.
Definition: hashfunc.hh:37
Definition: automata.hh:26
mc_rvalue
Definition: mc.hh:43
@ NOT_EMPTY
The product is not empty.
@ EMPTY
The product is empty.
An acceptance mark.
Definition: acc.hh:84