on_log_state_signal(get_remote_app());
XBT_INFO("DFS exploration ended. %ld unique states visited; %lu backtracks (%lu transition replays, %lu states "
"visited overall)",
- State::get_expanded_states(), backtrack_count_, visited_states_count_,
- Transition::get_replayed_transitions());
+ State::get_expanded_states(), backtrack_count_, Transition::get_replayed_transitions(),
+ visited_states_count_);
Exploration::log_state();
}
if (_sg_mc_sleep_set && XBT_LOG_ISENABLED(mc_dfs, xbt_log_priority_verbose)) {
XBT_VERB("Sleep set actually containing:");
- for (auto& [aid, transition] : state->get_sleep_set())
+ for (const auto& [aid, transition] : state->get_sleep_set())
XBT_VERB(" <%ld,%s>", aid, transition->to_string().c_str());
}
continue;
if (valid != current)
*valid = std::move(*current);
- if (best == end(opened_states_) || prio > best_prio) {
+ if (best == end(opened_states_) || prio < best_prio) {
best_prio = prio;
best = valid;
}
const auto& state = *iter;
state->do_odpor_unwind();
XBT_DEBUG("\tPerformed ODPOR 'clean-up'. Sleep set has:");
- for (auto& [aid, transition] : state->get_sleep_set())
+ for (const auto& [aid, transition] : state->get_sleep_set())
XBT_DEBUG("\t <%ld,%s>", aid, transition->to_string().c_str());
if (!state->has_empty_tree()) {
return state;
} else {
XBT_DEBUG("ODPOR: Ignoring race: `sleep(E')` intersects `WI_[E'](v := notdep(%u, E))`", e);
XBT_DEBUG("Sleep set contains:");
- for (auto& [aid, transition] : prev_state.get_sleep_set())
+ for (const auto& [aid, transition] : prev_state.get_sleep_set())
XBT_DEBUG(" <%ld,%s>", aid, transition->to_string().c_str());
}
}