X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/c0066756813cabe50a74ef326ec88eb71984556a..716c8e0b373bed43c35af2b35514f0b7a69b08a5:/src/mc/explo/DFSExplorer.cpp

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index f21297cb7d..451920da63 100644
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -112,8 +112,8 @@ void DFSExplorer::log_state() // override
   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();
 }
 
@@ -198,14 +198,14 @@ void DFSExplorer::run()
       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
@@ -300,10 +300,13 @@ void DFSExplorer::run()
       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
+          //
+          // 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);
@@ -369,7 +372,7 @@ std::shared_ptr<State> DFSExplorer::best_opened_state()
       continue;
     if (valid != current)
       *valid = std::move(*current);
-    if (best == end(opened_states_) || prio > best_prio) {
+    if (best == end(opened_states_) || prio < best_prio) {
       best_prio = prio;
       best      = valid;
     }
@@ -396,9 +399,9 @@ std::shared_ptr<State> DFSExplorer::next_odpor_state()
     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;
     }
   }
@@ -425,8 +428,7 @@ void DFSExplorer::backtrack()
         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`:",
@@ -452,7 +454,7 @@ void DFSExplorer::backtrack()
         } 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());
         }
       }
@@ -558,14 +560,6 @@ DFSExplorer::DFSExplorer(const std::vector<char*>& args, ReductionMode mode, boo
   }
   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)