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

diff --combined src/mc/api/State.cpp
index aff9d5c,afd8904..b5929f3
--- 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,9 -33,10 +32,9 @@@
    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_);
@@@ -49,7 -51,7 +49,7 @@@ State::State(RemoteApp& remote_app, std
      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;
@@@ -199,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
@@@ -212,9 -211,8 +212,8 @@@
      // Find an enabled transition to pick
      for (const auto& [_, actor] : get_actors_list()) {
        if (actor.is_enabled()) {
-         // For each variant of the transition, we want
-         // to insert the action into the tree. This ensures
-         // that all variants are searched
+         // For each variant of the transition that is enabled, we want to insert the action into the tree.
+         // This ensures that all variants are searched
          for (unsigned times = 0; times < actor.get_max_considered(); ++times) {
            wakeup_tree_.insert(prior, odpor::PartialExecution{actor.get_transition(times)});
          }
@@@ -227,11 -225,6 +226,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();

diff --combined src/mc/explo/DFSExplorer.cpp
index 6fe0b46,978cdfd..033c525
--- 1/src/mc/explo/DFSExplorer.cpp
--- 2/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@@ -65,12 -65,9 +65,9 @@@ void DFSExplorer::restore_stack(std::sh
    }
    XBT_DEBUG("Replaced stack by %s", get_record_trace().to_string().c_str());
    if (reduction_mode_ == ReductionMode::sdpor || reduction_mode_ == ReductionMode::odpor) {
-     // NOTE: The outgoing transition for the top-most
-     // state of the  stack refers to that which was taken
-     // as part of the last trace explored by the algorithm.
-     // Thus, only the sequence of transitions leading up to,
-     // but not including, the last state must be included
-     // when reconstructing the Exploration for SDPOR.
+     // NOTE: The outgoing transition for the top-most state of the  stack refers to that which was taken
+     // as part of the last trace explored by the algorithm. Thus, only the sequence of transitions leading up to,
+     // but not including, the last state must be included when reconstructing the Exploration for SDPOR.
      for (auto iter = std::next(stack_.begin()); iter != stack_.end(); ++iter) {
        execution_seq_.push_transition((*iter)->get_transition_in());
      }
@@@ -84,7 -81,7 +81,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();
  }
  
@@@ -124,16 -121,12 +121,12 @@@ void DFSExplorer::run(
      }
  
      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
-       // (rather than following the partial execution of a
-       // wakeup tree). This corresponds to lines 9 to 13 of
+       // In the case of ODPOR, the wakeup tree for this state may be empty if we're exploring new territory
+       // (rather than following the partial execution of a wakeup tree). This corresponds to lines 9 to 13 of
        // the ODPOR pseudocode
        //
-       // INVARIANT: The execution sequence should be consistent
-       // with the state when seeding the tree. If the sequence
-       // gets out of sync with the state, selection will not
-       // work as we intend
+       // INVARIANT: The execution sequence should be consistent with the state when seeding the tree. If the sequence
+       // gets out of sync with the state, selection will not work as we intend
        state->seed_wakeup_tree_if_needed(execution_seq_);
      }
  
@@@ -163,13 -156,16 +156,16 @@@
          XBT_VERB("  <%ld,%s>", aid, transition->to_string().c_str());
      }
  
+     auto todo = state->get_actors_list().at(next).get_transition();
+     XBT_DEBUG("wanna execute %ld: %.60s", next, todo->to_string().c_str());
+ 
      /* Actually answer the request: let's execute the selected request (MCed does one step) */
      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
      // reached then perform one step of the exploration algorithm.
-     XBT_VERB("Execute %ld: %.150s (stack depth: %zu, state: %ld, %zu interleaves)", state->get_transition_out()->aid_,
+     XBT_VERB("Executed %ld: %.60s (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) */
@@@ -177,13 -173,10 +173,10 @@@
      on_state_creation_signal(next_state.get(), get_remote_app());
  
      if (reduction_mode_ == ReductionMode::odpor) {
-       // With ODPOR, after taking a step forward, we must
-       // assign a copy of that subtree to the next state.
+       // With ODPOR, after taking a step forward, we must assign a copy of that subtree to the next state.
        //
-       // NOTE: We only add actions to the sleep set AFTER
-       // we've regenerated states. We must perform the search
-       // fully down a single path before we consider adding
-       // any elements to the sleep set according to the pseudocode
+       // NOTE: We only add actions to the sleep set AFTER we've regenerated states. We must perform the search
+       // fully down a single path before we consider adding any elements to the sleep set according to the pseudocode
        next_state->sprout_tree_from_parent_state();
      } else {
        /* Sleep set procedure:
@@@ -245,15 -238,13 +238,13 @@@
        /**
         * SDPOR Source Set Procedure:
         *
-        * Find "reversible races" in the current execution `E` with respect
-        * to the latest action `p`. For each such race, determine one thread
-        * not contained in the backtrack set at the "race point" `r` which
-        * "represents" the trace formed by first executing everything after
-        * `r` that doesn't depend on it (`v := notdep(r, E)`) and then `p` to
+        * Find "reversible races" in the current execution `E` with respect to the latest action `p`. For each such race,
+        * determine one thread not contained in the backtrack set at the "race point" `r` which "represents" the trace
+        * formed by first executing everything after `r` that doesn't depend on it (`v := notdep(r, E)`) and then `p` to
         * flip the race.
         *
-        * The intuition is that some subsequence of `v` may enable `p`, so
-        * we want to be sure that search "in that direction"
+        * The intuition is that some subsequence of `v` may enable `p`, so we want to be sure that search "in that
+        * direction"
         */
        execution_seq_.push_transition(std::move(executed_transition));
        xbt_assert(execution_seq_.get_latest_event_handle().has_value(), "No events are contained in the SDPOR execution "
@@@ -264,12 -255,10 +255,10 @@@
          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 (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
+           // 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
            //
-           // Here, we choose the actor with the lowest ID to ensure
-           // we get deterministic results
+           // Here, we choose the actor with the lowest ID to ensure we get deterministic results
            const auto q =
                std::min_element(choices.begin(), choices.end(), [](const aid_t a1, const aid_t a2) { return a1 < a2; });
            prev_state->consider_one(*q);
@@@ -277,8 -266,7 +266,7 @@@
          }
        }
      } else if (reduction_mode_ == ReductionMode::odpor) {
-       // In the case of ODPOR, we simply observe the transition that was executed
-       // until we've reached a maximal trace
+       // In the case of ODPOR, we simply observe the transition that was executed until we've reached a maximal trace
        execution_seq_.push_transition(std::move(executed_transition));
      }
  
@@@ -347,8 -335,6 +335,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;
      }
    }
@@@ -362,28 -348,21 +350,25 @@@ void DFSExplorer::backtrack(
      /**
       * ODPOR Race Detection Procedure:
       *
-      * For each reversible race in the current execution, we
-      * note if there are any continuations `C` equivalent to that which
-      * would reverse the race that have already either a) been searched by ODPOR or
-      * b) been *noted* to be searched by the wakeup tree at the
-      * appropriate reversal point, either as `C` directly or
-      * an as equivalent to `C` ("eventually looks like C", viz. the `~_E`
-      * relation)
+      * For each reversible race in the current execution, we note if there are any continuations `C` equivalent to that
+      * which would reverse the race that have already either a) been searched by ODPOR or b) been *noted* to be searched
+      * by the wakeup tree at the appropriate reversal point, either as `C` directly or an as equivalent to `C`
+      * ("eventually looks like C", viz. the `~_E` relation)
       */
      for (auto e_prime = static_cast<odpor::Execution::EventHandle>(0); e_prime <= last_event.value(); ++e_prime) {
 -      for (const auto e : execution_seq_.get_reversible_races_of(e_prime)) {
 +      XBT_DEBUG("ODPOR: Now considering all possible race with `%u`", e_prime);
 +      for (const auto e : execution_seq_.get_reversible_races_of(e_prime)) {
          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()) {
            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: {

diff --combined src/mc/explo/odpor/ReversibleRaceCalculator.cpp
index f6007c2,d671e93..9b8f614
--- 1/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
--- 2/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
+++ b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
@@@ -5,24 -5,16 +5,26 @@@
  
  #include "src/mc/explo/odpor/ReversibleRaceCalculator.hpp"
  #include "src/mc/explo/odpor/Execution.hpp"
+ #include "src/mc/transition/Transition.hpp"
+ #include "src/mc/transition/TransitionSynchro.hpp"
  
  #include <functional>
  #include <unordered_map>
  #include <xbt/asserts.h>
  #include <xbt/ex.h>
  
 +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_odpor_reversible_race, mc_dfs, "ODPOR exploration algorithm of the model-checker");
 +
  namespace simgrid::mc::odpor {
  
 +/**
 +   The reversible race detector should only be used if we already have the assumption
 +   e1 <* e2 (see Source set: a foundation for ODPOR). In particular this means that :
 +   - e1 -->_E e2
 +   - proc(e1) != proc(e2)
 +   - there is no event e3 s.t. e1 --> e3 --> e2
 +*/
 +
  bool ReversibleRaceCalculator::is_race_reversible(const Execution& E, Execution::EventHandle e1,
                                                    Execution::EventHandle e2)
  {
@@@ -151,12 -143,8 +153,12 @@@ bool ReversibleRaceCalculator::is_race_
  bool ReversibleRaceCalculator::is_race_reversible_MutexWait(const Execution& E, Execution::EventHandle e1,
                                                              const Transition* /*e2*/)
  {
 -  // TODO: Get the semantics correct here
 +  // The only possibilities for e1 to satisfy the pre-condition are :
 +    // - MUTEX_ASYNC_LOCK
 +
 +  
    const auto e1_action = E.get_transition_for_handle(e1)->type_;
 +  xbt_assert(e1_action == Transition::Type::MUTEX_UNLOCK);
    return e1_action != Transition::Type::MUTEX_ASYNC_LOCK && e1_action != Transition::Type::MUTEX_UNLOCK;
  }
  
@@@ -174,15 -162,15 +176,15 @@@ bool ReversibleRaceCalculator::is_race_
    return true;
  }
  
- bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution&, Execution::EventHandle /*e1*/,
+ bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution& E, Execution::EventHandle e1,
                                                            const Transition* /*e2*/)
  {
-   // TODO: Get the semantics correct here
-     // Certainement qu'il suffit de considérer les SemUnlock. ⋀ a priori,
-     // il doit même suffir de considérer le cas où leur capacity après execution est <=1
-     // ces cas disent qu'avant éxecution la capacity était de 0. Donc aucune chance de pouvoir
-     // wait avant le unlock.
-   return false;
+   // Reversible with everynbody but unlock which creates a free token
+   const auto e1_transition = E.get_transition_for_handle(e1);
+   if (e1_transition->type_ == Transition::Type::SEM_UNLOCK &&
+       static_cast<const SemaphoreTransition*>(e1_transition)->get_capacity() <= 1)
+     return false;
+   return true;
  }
  
  bool ReversibleRaceCalculator::is_race_reversible_ObjectAccess(const Execution&, Execution::EventHandle /*e1*/,