/**
* ODPOR Race Detection Procedure:
*
- * For each reversible race in the current execution, we
- * note if there are any continuations `C` equivalent to that which
- * would reverse the race that have already either a) been searched by ODPOR or
- * b) been *noted* to be searched by the wakeup tree at the
- * appropriate reversal point, either as `C` directly or
- * an as equivalent to `C` ("eventually looks like C", viz. the `~_E`
- * relation)
+ * For each reversible race in the current execution, we note if there are any continuations `C` equivalent to that
+ * which would reverse the race that have already either a) been searched by ODPOR or b) been *noted* to be searched
+ * by the wakeup tree at the appropriate reversal point, either as `C` directly or an as equivalent to `C`
+ * ("eventually looks like C", viz. the `~_E` relation)
*/
for (auto e_prime = static_cast<odpor::Execution::EventHandle>(0); e_prime <= last_event.value(); ++e_prime) {
- for (const auto e : execution_seq_.get_reversible_races_of(e_prime)) {
+ XBT_DEBUG("ODPOR: Now considering all possible race with `%u`", e_prime);
+ for (const auto e : execution_seq_.get_reversible_races_of(e_prime)) {
XBT_DEBUG("ODPOR: Reversible race detected between events `%u` and `%u`", e, e_prime);
State& prev_state = *stack_[e];
if (const auto v = execution_seq_.get_odpor_extension_from(e, e_prime, prev_state); v.has_value()) {
