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();
}
continue;
}
- if (_sg_mc_sleep_set && XBT_LOG_ISENABLED(mc_dfs, xbt_log_priority_verbose)) {
+ if (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());
}
/* Actually answer the request: let's execute the selected request (MCed does one step) */
- const auto executed_transition = state->execute_next(next, get_remote_app());
+ auto executed_transition = state->execute_next(next, get_remote_app());
on_transition_execute_signal(state->get_transition_out().get(), get_remote_app());
// If there are processes to interleave and the maximum depth has not been
continue;
} else if (prev_state->get_transition_out()->depends(state->get_transition_out().get())) {
XBT_VERB("Dependent Transitions:");
- XBT_VERB(" %s (state=%ld)", prev_state->get_transition_out()->to_string().c_str(), prev_state->get_num());
- XBT_VERB(" %s (state=%ld)", state->get_transition_out()->to_string().c_str(), state->get_num());
+ XBT_VERB(" #%ld %s (state=%ld)", prev_state->get_transition_out()->aid_,
+ prev_state->get_transition_out()->to_string().c_str(), prev_state->get_num());
+ XBT_VERB(" #%ld %s (state=%ld)", state->get_transition_out()->aid_,
+ state->get_transition_out()->to_string().c_str(), state->get_num());
if (prev_state->is_actor_enabled(issuer_id)) {
if (not prev_state->is_actor_done(issuer_id)) {
break;
} else {
XBT_VERB("INDEPENDENT Transitions:");
- XBT_VERB(" %s (state=%ld)", prev_state->get_transition_out()->to_string().c_str(), prev_state->get_num());
- XBT_VERB(" %s (state=%ld)", state->get_transition_out()->to_string().c_str(), state->get_num());
+ XBT_VERB(" #%ld %s (state=%ld)", prev_state->get_transition_out()->aid_,
+ prev_state->get_transition_out()->to_string().c_str(), prev_state->get_num());
+ XBT_VERB(" #%ld %s (state=%ld)", state->get_transition_out()->aid_,
+ state->get_transition_out()->to_string().c_str(), state->get_num());
}
tmp_stack.pop_back();
}
for (const auto e_race : execution_seq_.get_reversible_races_of(next_E_p)) {
State* prev_state = stack_[e_race].get();
const auto choices = execution_seq_.get_missing_source_set_actors_from(e_race, prev_state->get_backtrack_set());
- if (!choices.empty()) {
+ if (not choices.empty()) {
// NOTE: To incorporate the idea of attempting to select the "best"
// backtrack point into SDPOR, instead of selecting the `first` initial,
// we should instead compute all choices and decide which is best
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()) {
+ if (not state->has_empty_tree()) {
return state;
}
}
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()) {
- const auto result = prev_state.insert_into_wakeup_tree(v.value(), execution_seq_.get_prefix_before(e));
- switch (result) {
+ 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`:",
} 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());
}
}
}
if (stack_.back()->count_todo_multiples() > 1)
opened_states_.emplace_back(stack_.back());
-
- if (mode == ReductionMode::odpor && !_sg_mc_sleep_set) {
- // ODPOR requires the use of sleep sets; SDPOR
- // "likes" using sleep sets but it is not strictly
- // required
- XBT_INFO("Forcing the use of sleep sets for use with ODPOR");
- _sg_mc_sleep_set = true;
- }
}
Exploration* create_dfs_exploration(const std::vector<char*>& args, ReductionMode mode)
