Merge branch 'master' of https://framagit.org/simgrid/simgrid

diff --combined src/mc/api/State.cpp
index 866a1d0,fd60a3c..aff9d5c
--- 1/src/mc/api/State.cpp
--- 2/src/mc/api/State.cpp
+++ b/src/mc/api/State.cpp
@@@ -25,6 -25,7 +25,6 @@@ State::State(RemoteApp& remote_app) : n
  {
    XBT_VERB("Creating a guide for the state");
  
 -  
    if (_sg_mc_strategy == "none")
      strategy_ = std::make_shared<BasicStrategy>();
    else if (_sg_mc_strategy == "max_match_comm")
@@@ -32,19 -33,13 +32,12 @@@
    else if (_sg_mc_strategy == "min_match_comm")
      strategy_ = std::make_shared<MinMatchComm>();
    else if (_sg_mc_strategy == "uniform") {
 -    xbt::random::set_mersenne_seed(_sg_mc_random_seed);  
 +    xbt::random::set_mersenne_seed(_sg_mc_random_seed);
      strategy_ = std::make_shared<UniformStrategy>();
 -  }
 -  else
 +  } else
      THROW_IMPOSSIBLE;
  
    remote_app.get_actors_status(strategy_->actors_to_run_);
- 
- #if SIMGRID_HAVE_STATEFUL_MC
-   /* Stateful model checking */
-   if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination)
-     system_state_ = std::make_shared<simgrid::mc::Snapshot>(num_, remote_app.get_page_store(),
-                                                             *remote_app.get_remote_process_memory());
- #endif
  }
  
  State::State(RemoteApp& remote_app, std::shared_ptr<State> parent_state)
@@@ -56,7 -51,7 +49,7 @@@
      strategy_ = std::make_shared<MaxMatchComm>();
    else if (_sg_mc_strategy == "min_match_comm")
      strategy_ = std::make_shared<MinMatchComm>();
 -  else if (_sg_mc_strategy == "uniform") 
 +  else if (_sg_mc_strategy == "uniform")
      strategy_ = std::make_shared<UniformStrategy>();
    else
      THROW_IMPOSSIBLE;
@@@ -64,12 -59,6 +57,6 @@@
  
    remote_app.get_actors_status(strategy_->actors_to_run_);
  
- #if SIMGRID_HAVE_STATEFUL_MC /* Stateful model checking */
-   if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination)
-     system_state_ = std::make_shared<simgrid::mc::Snapshot>(num_, remote_app.get_page_store(),
-                                                             *remote_app.get_remote_process_memory());
- #endif
- 
    /* Copy the sleep set and eventually removes things from it: */
    /* For each actor in the previous sleep set, keep it if it is not dependent with current transition.
     * And if we kept it and the actor is enabled in this state, mark the actor as already done, so that
@@@ -212,9 -201,6 +199,9 @@@ void State::seed_wakeup_tree_if_needed(
  {
    // TODO: It would be better not to have such a flag.
    if (has_initialized_wakeup_tree) {
 +    XBT_DEBUG("Reached a node with the following initialized WuT:");
 +    XBT_DEBUG("\n%s", wakeup_tree_.string_of_whole_tree().c_str());
 +
      return;
    }
    // TODO: Note that the next action taken by the actor may be updated
@@@ -240,11 -226,6 +227,11 @@@
  
  void State::sprout_tree_from_parent_state()
  {
 +
 +    XBT_DEBUG("Initializing Wut with parent one:");
 +    XBT_DEBUG("\n%s", parent_state_->wakeup_tree_.string_of_whole_tree().c_str());
 +
 +    
    xbt_assert(parent_state_ != nullptr, "Attempting to construct a wakeup tree for the root state "
                                         "(or what appears to be, rather for state without a parent defined)");
    const auto min_process_node = parent_state_->wakeup_tree_.get_min_single_process_node();
@@@ -252,14 -233,18 +239,18 @@@
                                             "parent with an empty wakeup tree. This indicates either that ODPOR "
                                             "actor selection in State.cpp is incorrect, or that the code "
                                             "deciding when to make subtrees in ODPOR is incorrect");
-   xbt_assert((get_transition_in()->aid_ == min_process_node.value()->get_actor()) &&
-                  (get_transition_in()->type_ == min_process_node.value()->get_action()->type_),
-              "We tried to make a subtree from a parent state who claimed to have executed `%s` on actor %ld "
-              "but whose wakeup tree indicates it should have executed `%s` on actor %ld. This indicates "
-              "that exploration is not following ODPOR. Are you sure you're choosing actors "
-              "to schedule from the wakeup tree?",
-              get_transition_in()->to_string(false).c_str(), get_transition_in()->aid_,
-              min_process_node.value()->get_action()->to_string(false).c_str(), min_process_node.value()->get_actor());
+   if (not(get_transition_in()->aid_ == min_process_node.value()->get_actor() &&
+           get_transition_in()->type_ == min_process_node.value()->get_action()->type_)) {
+     XBT_ERROR("We tried to make a subtree from a parent state who claimed to have executed `%s` on actor %ld "
+               "but whose wakeup tree indicates it should have executed `%s` on actor %ld. This indicates "
+               "that exploration is not following ODPOR. Are you sure you're choosing actors "
+               "to schedule from the wakeup tree? Trace so far:",
+               get_transition_in()->to_string(false).c_str(), get_transition_in()->aid_,
+               min_process_node.value()->get_action()->to_string(false).c_str(), min_process_node.value()->get_actor());
+     for (auto elm : Exploration::get_instance()->get_textual_trace())
+       XBT_ERROR("%s", elm.c_str());
+     xbt_abort();
+   }
    this->wakeup_tree_ = odpor::WakeupTree::make_subtree_rooted_at(min_process_node.value());
  }
  

diff --combined src/mc/api/State.hpp
index f10d7bd,ca77b51..de11f78
--- 1/src/mc/api/State.hpp
--- 2/src/mc/api/State.hpp
+++ b/src/mc/api/State.hpp
@@@ -13,10 -13,6 +13,6 @@@
  #include "src/mc/explo/odpor/WakeupTree.hpp"
  #include "src/mc/transition/Transition.hpp"
  
- #if SIMGRID_HAVE_STATEFUL_MC
- #include "src/mc/sosp/Snapshot.hpp"
- #endif
- 
  namespace simgrid::mc {
  
  /* A node in the exploration graph (kind-of) */
@@@ -32,9 -28,6 +28,6 @@@ class XBT_PRIVATE State : public xbt::E
    /** Sequential state ID (used for debugging) */
    long num_ = 0;
  
-   /** Snapshot of system state (if needed) */
-   std::shared_ptr<Snapshot> system_state_;
- 
    /** Unique parent of this state. Required both for sleep set computation
        and for guided model-checking */
    std::shared_ptr<State> parent_state_ = nullptr;
@@@ -98,9 -91,6 +91,6 @@@ public
    unsigned long get_actor_count() const { return strategy_->actors_to_run_.size(); }
    bool is_actor_enabled(aid_t actor) const { return strategy_->actors_to_run_.at(actor).is_enabled(); }
  
-   Snapshot* get_system_state() const { return system_state_.get(); }
-   void set_system_state(std::shared_ptr<Snapshot> state) { system_state_ = std::move(state); }
- 
    /**
     * @brief Computes the backtrack set for this state
     * according to its definition in SimGrid.
@@@ -154,9 -144,7 +144,9 @@@
     */
    void remove_subtree_using_current_out_transition();
    bool has_empty_tree() const { return this->wakeup_tree_.empty(); }
 +  std::string string_of_wut() const { return this->wakeup_tree_.string_of_whole_tree(); }
  
 +  
    /**
     * @brief
     */

diff --combined src/mc/explo/DFSExplorer.cpp
index b23ce48,ffa682f..f82d8da
--- 1/src/mc/explo/DFSExplorer.cpp
--- 2/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@@ -10,11 -10,6 +10,6 @@@
  #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"
  #include "xbt/sysdep.h"
@@@ -44,30 -39,6 +39,6 @@@ xbt::signal<void(Transition*, RemoteApp
  
  xbt::signal<void(RemoteApp&)> DFSExplorer::on_log_state_signal;
  
- void DFSExplorer::check_non_termination(const State* current_state)
- {
- #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())) {
-       XBT_INFO("Non-progressive cycle: state %ld -> state %ld", state->get_num(), current_state->get_num());
-       XBT_INFO("******************************************");
-       XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
-       XBT_INFO("******************************************");
-       XBT_INFO("Counter-example execution trace:");
-       for (auto const& s : get_textual_trace())
-         XBT_INFO("  %s", s.c_str());
-       XBT_INFO("You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with "
-                "--cfg=model-check/replay:'%s'",
-                get_record_trace().to_string().c_str());
-       log_state();
- 
-       throw McError(ExitStatus::NON_TERMINATION);
-     }
-   }
- #endif
- }
- 
  RecordTrace DFSExplorer::get_record_trace() // override
  {
    RecordTrace res;
@@@ -113,7 -84,7 +84,7 @@@ void DFSExplorer::log_state() // overri
    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();
  }
  
@@@ -152,18 -123,6 +123,6 @@@ void DFSExplorer::run(
        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.",
-                 visited_state_->original_num_ == -1 ? visited_state_->num_ : visited_state_->original_num_);
- 
-       visited_state_ = nullptr;
-       this->backtrack();
-       continue;
-     }
- #endif
- 
      if (reduction_mode_ == ReductionMode::odpor) {
        // In the case of ODPOR, the wakeup tree for this
        // state may be empty if we're exploring new territory
@@@ -210,7 -169,7 +169,7 @@@
  
      // If there are processes to interleave and the maximum depth has not been
      // reached then perform one step of the exploration algorithm.
 -    XBT_VERB("Execute %ld: %.60s (stack depth: %zu, state: %ld, %zu interleaves)", state->get_transition_out()->aid_,
 +    XBT_VERB("Execute %ld: %.150s (stack depth: %zu, state: %ld, %zu interleaves)", state->get_transition_out()->aid_,
               state->get_transition_out()->to_string().c_str(), stack_.size(), state->get_num(), state->count_todo());
  
      /* Create the new expanded state (copy the state of MCed into our MCer data) */
@@@ -253,8 -212,10 +212,10 @@@
            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)) {
@@@ -273,8 -234,10 +234,10 @@@
            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();
        }
@@@ -324,36 -287,18 +287,18 @@@
      if (stack_.back()->count_todo_multiples() > 0)
        opened_states_.emplace_back(stack_.back());
  
-     if (_sg_mc_termination)
-       this->check_non_termination(next_state.get());
- 
- #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());
- #endif
- 
      stack_.emplace_back(std::move(next_state));
  
      /* If this is a new state (or if we don't care about state-equality reduction) */
-     if (visited_state_ == nullptr) {
-       /* Get an enabled process and insert it in the interleave set of the next state */
-       if (reduction_mode_ == ReductionMode::dpor)
-         stack_.back()->consider_best(); // Take only one transition if DPOR: others may be considered later if required
-       else {
-         stack_.back()->consider_all();
-       }
- 
-       dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(), stack_.back()->get_num(),
-                  state->get_transition_out()->dot_string().c_str());
- #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_out()->dot_string().c_str());
- #endif
+     /* Get an enabled process and insert it in the interleave set of the next state */
+     if (reduction_mode_ == ReductionMode::dpor)
+       stack_.back()->consider_best(); // Take only one transition if DPOR: others may be considered later if required
+     else {
+       stack_.back()->consider_all();
      }
+ 
+     dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(), stack_.back()->get_num(),
+                state->get_transition_out()->dot_string().c_str());
    }
    log_state();
  }
@@@ -402,8 -347,6 +347,8 @@@ std::shared_ptr<State> DFSExplorer::nex
      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()) {
 +      XBT_DEBUG("\t    found the following non-empty WuT:\n"
 +                "%s", state->string_of_wut().c_str());
        return state;
      }
    }
@@@ -432,12 -375,9 +377,12 @@@ void DFSExplorer::backtrack(
          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: {
@@@ -486,41 -426,16 +431,16 @@@
    backtrack_count_++;
    XBT_DEBUG("Backtracking to state#%ld", backtracking_point->get_num());
  
- #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());
-     on_restore_system_state_signal(backtracking_point.get(), get_remote_app());
-     this->restore_stack(backtracking_point);
-     return;
-   }
- #endif
- 
    // Search how to restore the backtracking point
-   State* init_state = nullptr;
    std::deque<Transition*> replay_recipe;
    for (auto* s = backtracking_point.get(); s != nullptr; s = s->get_parent_state().get()) {
- #if SIMGRID_HAVE_STATEFUL_MC
-     if (s->get_system_state() != nullptr) { // Found a state that I can restore
-       init_state = s;
-       break;
-     }
- #endif
      if (s->get_transition_in() != nullptr) // The root has no transition_in
        replay_recipe.push_front(s->get_transition_in().get());
    }
  
-   // Restore the init_state, if any
-   if (init_state != nullptr) {
- #if SIMGRID_HAVE_STATEFUL_MC
-     const auto* system_state = init_state->get_system_state();
-     system_state->restore(*get_remote_app().get_remote_process_memory());
-     on_restore_system_state_signal(init_state, get_remote_app());
- #endif
-   } else { // Restore the initial state if no intermediate state was found
-     get_remote_app().restore_initial_state();
-     on_restore_initial_state_signal(get_remote_app());
-   }
+   // Restore the initial state if no intermediate state was found
+   get_remote_app().restore_initial_state();
+   on_restore_initial_state_signal(get_remote_app());
  
    /* if no snapshot, we need to restore the initial state and replay the transitions */
    /* Traverse the stack from the state at position start and re-execute the transitions */
@@@ -532,23 -447,9 +452,9 @@@
    this->restore_stack(backtracking_point);
  }
  
- DFSExplorer::DFSExplorer(const std::vector<char*>& args, ReductionMode mode, bool need_memory_info)
-     : Exploration(args, need_memory_info || _sg_mc_termination
- #if SIMGRID_HAVE_STATEFUL_MC
-                             || _sg_mc_checkpoint > 0
- #endif
-                   )
-     , reduction_mode_(mode)
+ DFSExplorer::DFSExplorer(const std::vector<char*>& args, ReductionMode mode) : Exploration(args), reduction_mode_(mode)
  {
-   if (_sg_mc_termination) {
-     if (mode != ReductionMode::none) {
-       XBT_INFO("Check non progressive cycles (turning DPOR off)");
-       reduction_mode_ = ReductionMode::none;
-     } else {
-       XBT_INFO("Check non progressive cycles");
-     }
-   } else
-     XBT_INFO("Start a DFS exploration. Reduction is: %s.", to_c_str(reduction_mode_));
+   XBT_INFO("Start a DFS exploration. Reduction is: %s.", to_c_str(reduction_mode_));
  
    auto initial_state = std::make_shared<State>(get_remote_app());
  

diff --combined src/mc/transition/TransitionSynchro.cpp
index 21ea4ec,5e7ded2..bd57886
--- 1/src/mc/transition/TransitionSynchro.cpp
--- 2/src/mc/transition/TransitionSynchro.cpp
+++ b/src/mc/transition/TransitionSynchro.cpp
@@@ -32,7 -32,7 +32,7 @@@ bool BarrierTransition::depends(const T
    // Actions executed by the same actor are always dependent
    if (o->aid_ == aid_)
      return true;
-   
+ 
    if (const auto* other = dynamic_cast<const BarrierTransition*>(o)) {
      if (bar_ != other->bar_)
        return false;
@@@ -128,7 -128,7 +128,11 @@@ bool SemaphoreTransition::depends(cons
    // Actions executed by the same actor are always dependent
    if (o->aid_ == aid_)
      return true;
++<<<<<<< HEAD
 +  
++=======
+ 
++>>>>>>> dfafe652e9ae62c35cd0fc084b117fc987b3e8dc
    if (const auto* other = dynamic_cast<const SemaphoreTransition*>(o)) {
      if (sem_ != other->sem_)
        return false;