XBT_INFO("DFS exploration ended. %ld unique states visited; %lu backtracks (%lu transition replays, %lu states "
"visited overall)",
State::get_expanded_states(), backtrack_count_, Transition::get_replayed_transitions(),
- visited_states_count_);
+ visited_states_count_);
Exploration::log_state();
}
const aid_t next = reduction_mode_ == ReductionMode::odpor ? state->next_odpor_transition()
: std::get<0>(state->next_transition_guided());
+
if (next < 0 || not state->is_actor_enabled(next)) {
if (next >= 0) { // Actor is not enabled, then
XBT_INFO("Reduction %s wants to execute a disabled transition %s. If it's ODPOR, ReversibleRace is suboptimal.",
XBT_INFO("Current trace:");
for (auto elm : get_textual_trace())
XBT_ERROR("%s", elm.c_str());
+ // Remove the disabled transition from the wakeup tree so that ODPOR doesn't try it again
+ state->remove_subtree_at_aid(next);
+ state->add_sleep_set(state->get_actors_list().at(next).get_transition());
}
}
// If there is no more transition in the current state (or if ODPOR picked an actor that is not enabled --
XBT_DEBUG("\tPerformed ODPOR 'clean-up'. Sleep set has:");
for (const auto& [aid, transition] : state->get_sleep_set())
XBT_DEBUG("\t <%ld,%s>", aid, transition->to_string().c_str());
- if (not state->has_empty_tree()) {
- return state;
- }
}
return nullptr;
}
* ("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) {
+ 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()) {
switch (prev_state.insert_into_wakeup_tree(v.value(), execution_seq_.get_prefix_before(e))) {
case odpor::WakeupTree::InsertionResult::root: {
- XBT_DEBUG("ODPOR: Reversible race with `%u` unaccounted for in the wakeup tree for "
- "the execution prior to event `%u`:",
- e_prime, e);
+ XBT_DEBUG("ODPOR: Reversible race with `%u`(%ld: %.20s) unaccounted for in the wakeup tree for "
+ "the execution prior to event `%u`(%ld: %.20s):",
+ e_prime, stack_[e_prime]->get_transition_out()->aid_,
+ stack_[e_prime]->get_transition_out()->to_string(true).c_str(), e,
+ prev_state.get_transition_out()->aid_,
+ prev_state.get_transition_out()->to_string(true).c_str());
break;
}
case odpor::WakeupTree::InsertionResult::interior_node: {