Commit 29aab0b3 authored by Thibault Allançon's avatar Thibault Allançon

WIP: try to add complete deadlock algo

parent 08b8492d
Pipeline #19258 failed with stage
in 17 minutes and 4 seconds
...@@ -117,13 +117,19 @@ namespace spot ...@@ -117,13 +117,19 @@ namespace spot
auto elem = todo_.back(); auto elem = todo_.back();
deadlock_ = elem.current_tr == transitions_; deadlock_ = elem.current_tr == transitions_;
if (SPOT_UNLIKELY(deadlock_)) //if (SPOT_UNLIKELY(deadlock_))
return; // return;
map_.erase(elem.st, brick_state_hasher()); map_.erase(elem.st, brick_state_hasher());
bloom_filter_.insert(state_hash_(elem.st.st)); bloom_filter_.insert(state_hash_(elem.st.st));
//sys_.recycle(elem.it, tid_);
//delete elem.it; auto& it = elem.it;
while (!it->done())
{
delete[] it->state();
it->next();
}
delete it;
todo_.pop_back(); todo_.pop_back();
} }
...@@ -137,7 +143,13 @@ namespace spot ...@@ -137,7 +143,13 @@ namespace spot
{ {
while (!todo_.empty()) while (!todo_.empty())
{ {
delete todo_.back().it; auto& it = todo_.back().it;
while (!it->done())
{
delete[] it->state();
it->next();
}
delete it;
todo_.pop_back(); todo_.pop_back();
} }
} }
...@@ -157,46 +169,34 @@ namespace spot ...@@ -157,46 +169,34 @@ namespace spot
setup(); setup();
deadlock_state initial{sys_.initial(tid_)}; deadlock_state initial{sys_.initial(tid_)};
auto it = sys_.succ(initial.st, tid_); auto it = sys_.succ(initial.st, tid_);
while (!it->done()) if (SPOT_LIKELY(push(initial)))
todo_.push_back({initial, it, transitions_});
while (!todo_.empty() && !stop_.load(std::memory_order_relaxed))
{
if (todo_.back().it->done())
{ {
std::cout << "LA\n"; pop();
delete[] it->state(); if (deadlock_)
it-> next(); break;
} }
delete it; else
delete[] initial.st; // FIXME sys.dealloc(sys.st) {
finalize(); ++transitions_;
State dst = todo_.back().it->state();
deadlock_state next{dst};
// if (SPOT_LIKELY(push(initial))) if (SPOT_LIKELY(push(next)))
// { todo_.push_back({next, sys_.succ(dst, tid_), transitions_});
// todo_.push_back({initial, sys_.succ(initial.st, tid_), transitions_}); else
// } delete[] todo_.back().it->state();
// while (!todo_.empty() && !stop_.load(std::memory_order_relaxed))
// {
// if (todo_.back().it->done())
// {
// pop();
// if (deadlock_)
// break;
// }
// else
// {
// ++transitions_;
// State dst = todo_.back().it->state();
// deadlock_state next{dst};
// if (SPOT_LIKELY(push(next)))
// {
// todo_.back().it->next();
// todo_.push_back({next, sys_.succ(dst, tid_), transitions_});
// }
// else
// {
// todo_.back().it->next();
// }
// }
// }
todo_.back().it->next();
}
}
delete[] initial.st;
finalize();
} }
bool has_deadlock() bool has_deadlock()
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment