* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/mc/explo/DFSExplorer.hpp"
-#include "src/mc/VisitedState.hpp"
#include "src/mc/mc_config.hpp"
#include "src/mc/mc_exit.hpp"
#include "src/mc/mc_private.hpp"
#include "src/mc/mc_record.hpp"
#include "src/mc/transition/Transition.hpp"
+#if SIMGRID_HAVE_STATEFUL_MC
+#include "src/mc/VisitedState.hpp"
+#endif
+
#include "src/xbt/mmalloc/mmprivate.h"
#include "xbt/log.h"
#include "xbt/string.hpp"
void DFSExplorer::check_non_termination(const State* current_state)
{
-#if SIMGRID_HAVE_MC
+#if SIMGRID_HAVE_STATEFUL_MC
for (auto const& state : stack_) {
if (state->get_system_state()->equals_to(*current_state->get_system_state(),
*get_remote_app().get_remote_process_memory())) {
continue;
}
+#if SIMGRID_HAVE_STATEFUL_MC
// Backtrack if we are revisiting a state we saw previously while applying state-equality reduction
if (visited_state_ != nullptr) {
XBT_DEBUG("State already visited (equal to state %ld), exploration stopped on this path.",
this->backtrack();
continue;
}
+#endif
// Search for the next transition
// next_transition returns a pair<aid_t, double> in case we want to consider multiple state (eg. during backtrack)
if (prev_state->is_actor_enabled(issuer_id)) {
if (not prev_state->is_actor_done(issuer_id)) {
prev_state->consider_one(issuer_id);
- opened_states_.push(std::shared_ptr<State>(tmp_stack.back()));
+ opened_states_.emplace(tmp_stack.back());
} else
XBT_DEBUG("Actor %ld is already in done set: no need to explore it again", issuer_id);
} else {
issuer_id);
// If we ended up marking at least a transition, explore it at some point
if (prev_state->consider_all() > 0)
- opened_states_.push(std::shared_ptr<State>(tmp_stack.back()));
+ opened_states_.emplace(tmp_stack.back());
}
break;
} else {
// Before leaving that state, if the transition we just took can be taken multiple times, we
// need to give it to the opened states
if (stack_.back()->count_todo_multiples() > 0)
- opened_states_.push(std::shared_ptr<State>(stack_.back()));
+ opened_states_.emplace(stack_.back());
if (_sg_mc_termination)
this->check_non_termination(next_state.get());
-#if SIMGRID_HAVE_MC
+#if SIMGRID_HAVE_STATEFUL_MC
/* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */
if (_sg_mc_max_visited_states > 0)
visited_state_ = visited_states_.addVisitedState(next_state->get_num(), next_state.get(), get_remote_app());
dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(), stack_.back()->get_num(),
state->get_transition()->dot_string().c_str());
- } else
+#if SIMGRID_HAVE_STATEFUL_MC
+ } else {
dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(),
visited_state_->original_num_ == -1 ? visited_state_->num_ : visited_state_->original_num_,
state->get_transition()->dot_string().c_str());
+#endif
+ }
}
log_state();
}
return;
}
- std::shared_ptr<State> backtracking_point = opened_states_.top(); // Take the point with smallest distance
- opened_states_.pop();
+ // Take the point with smallest distance
+ auto backtracking_point = opened_states_.extract(begin(opened_states_)).value();
// if the smallest distance corresponded to no enable actor, remove this and let the
// exploration ask again for a backtrack
backtrack_count_++;
XBT_DEBUG("Backtracking to state#%ld", backtracking_point->get_num());
-#if SIMGRID_HAVE_MC
+#if SIMGRID_HAVE_STATEFUL_MC
/* If asked to rollback on a state that has a snapshot, restore it */
if (const auto* system_state = backtracking_point->get_system_state()) {
system_state->restore(*get_remote_app().get_remote_process_memory());
stack_.back()->consider_all();
}
if (stack_.back()->count_todo_multiples() > 1)
- opened_states_.push(std::shared_ptr<State>(stack_.back()));
+ opened_states_.emplace(stack_.back());
}
Exploration* create_dfs_exploration(const std::vector<char*>& args, bool with_dpor)