#include "src/mc/mc_exit.hpp"
#include "src/mc/mc_private.hpp"
#include "src/mc/mc_record.hpp"
+#include "src/mc/remote/mc_protocol.h"
#include "src/mc/transition/Transition.hpp"
+#include "xbt/asserts.h"
#include "xbt/log.h"
#include "xbt/string.hpp"
#include "xbt/sysdep.h"
const aid_t next = reduction_mode_ == ReductionMode::odpor ? state->next_odpor_transition()
: std::get<0>(state->next_transition_guided());
- if (next < 0) {
- // If there is no more transition in the current state ), backtrace
- XBT_VERB("%lu actors remain, but none of them need to be interleaved (depth %zu).", state->get_actor_count(),
- stack_.size() + 1);
-
- if (state->get_actor_count() == 0) {
- get_remote_app().finalize_app();
- XBT_VERB("Execution came to an end at %s (state: %ld, depth: %zu)", get_record_trace().to_string().c_str(),
- state->get_num(), stack_.size());
+ if (next < 0 || not state->is_actor_enabled(next)) {
+ if (next >= 0) { // Actor is not enabled, then
+ XBT_DEBUG(
+ "Reduction %s wants to execute a disabled transition %s. If it's ODPOR, ReversibleRace is suboptimal.",
+ to_c_str(reduction_mode_), state->get_actors_list().at(next).get_transition()->to_string(true).c_str());
+ if (reduction_mode_ == ReductionMode::odpor) {
+ // 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());
+ } else {
+ xbt_assert(false, "Only ODPOR should be confident enought in itself to try executing a disabled transition");
+ }
}
-
- this->backtrack();
- continue;
- }
- if (not state->is_actor_enabled(next)) {
- // if ODPOR picked an actor that is not enabled -- ReversibleRace is an overapproximation
- xbt_assert(reduction_mode_ == ReductionMode::odpor,
- "Only ODPOR should be fool enough to try to execute a disabled transition");
- XBT_VERB("Preventing ODPOR exploration from executing a disabled transition. The reversibility of the race "
- "must have been overapproximated");
-
- 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 --
+ // ReversibleRace is an overapproximation), backtrace
XBT_VERB("%lu actors remain, but none of them need to be interleaved (depth %zu).", state->get_actor_count(),
stack_.size() + 1);
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;
}
// Search how to restore the backtracking point
std::deque<Transition*> replay_recipe;
- for (auto* s = backtracking_point.get(); s != nullptr; s = s->get_parent_state().get()) {
+ for (const auto* s = backtracking_point.get(); s != nullptr; s = s->get_parent_state().get()) {
if (s->get_transition_in() != nullptr) // The root has no transition_in
replay_recipe.push_front(s->get_transition_in().get());
}