Fix MANIFEST.in etc.

[simgrid.git] / src / mc / explo / DFSExplorer.cpp

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 4ed3f68..2c72764 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -144,7 +144,7 @@ void DFSExplorer::run()
         XBT_ERROR("/!\\ Max depth of %d reached! THIS **WILL** BREAK the reduction, which is not sound "
                   "when stopping at a fixed depth /!\\",
                   _sg_mc_max_depth.get());
-        XBT_ERROR("/!\\ If bad things happen, disable dpor with --cfg=model-check/reduction:none /!\\");
+        XBT_ERROR("/!\\ If bad things happen, disable the reduction with --cfg=model-check/reduction:none /!\\");
       } else {
         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
       }
@@ -293,20 +293,23 @@ void DFSExplorer::run()
        * 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/OPDPOR execution "
-                 "even though one was just added");
+      xbt_assert(execution_seq_.get_latest_event_handle().has_value(), "No events are contained in the SDPOR execution "
+                                                                       "even though one was just added");
 
       const auto next_E_p = execution_seq_.get_latest_event_handle().value();
-      for (const auto racing_event_handle : execution_seq_.get_reversible_races_of(next_E_p)) {
-        const std::shared_ptr<State> prev_state = stack_[racing_event_handle];
-        // 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
-        if (const auto q =
-                execution_seq_.get_first_sdpor_initial_from(racing_event_handle, prev_state->get_backtrack_set());
-            q.has_value()) {
-          prev_state->consider_one(q.value());
+      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()) {
+          // 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);
           opened_states_.emplace_back(std::move(prev_state));
         }
       }
@@ -395,6 +398,9 @@ std::shared_ptr<State> DFSExplorer::next_odpor_state()
   for (auto iter = stack_.rbegin(); iter != stack_.rend(); ++iter) {
     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())
+      XBT_DEBUG("\t  <%ld,%s>", aid, transition->to_string().c_str());
     if (!state->has_empty_tree()) {
       return state;
     }
@@ -448,6 +454,9 @@ 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())
+            XBT_DEBUG("  <%ld,%s>", aid, transition->to_string().c_str());
         }
       }
     }
@@ -552,6 +561,14 @@ 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)