sleep sets are not an option in MC. We always need them

It was useful to have it as an option when debugging.

diff --git a/docs/source/Configuring_SimGrid.rst b/docs/source/Configuring_SimGrid.rst
index f873b95..72d4c51 100644 (file)
--- a/docs/source/Configuring_SimGrid.rst
+++ b/docs/source/Configuring_SimGrid.rst
@@ -117,7 +117,6 @@ Existing Configuration Items
 - **model-check/replay:** :ref:`cfg=model-check/replay`
 - **model-check/send-determinism:** :ref:`cfg=model-check/send-determinism`
 - **model-check/setenv:** :ref:`cfg=model-check/setenv`
-- **model-check/sleep-set:** :ref:`cfg=model-check/sleep-set`
 - **model-check/termination:** :ref:`cfg=model-check/termination`
 - **model-check/timeout:** :ref:`cfg=model-check/timeout`
 - **model-check/visited:** :ref:`cfg=model-check/visited`
@@ -731,15 +730,6 @@ DFS exploration.
  - **uniform**: this is a boring random strategy where choices are based on a uniform sampling of possible choices.
    Surprisingly, it gives really really good results.
 
-
-.. _cfg=model-check/sleep-set:
-
-Sleep sets
-..........
-
-The performance of the DPOR algorithm is greatly improved by using sleep sets, but if you want, you can still disable it with
-this option.
-
 .. _cfg=model-check/visited:
 
 Size of Cycle Detection Set (state equality reduction)

diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp
index 0b6fc02..a33cbf1 100644 (file)
--- a/src/mc/api/State.cpp
+++ b/src/mc/api/State.cpp
@@ -73,22 +73,20 @@ State::State(RemoteApp& remote_app, std::shared_ptr<State> parent_state)
                                                             *remote_app.get_remote_process_memory());
 #endif
 
-  /* If we want sleep set reduction, copy the sleep set and eventually removes things from it */
-  if (_sg_mc_sleep_set) {
-    /* 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
-     * it is not explored*/
-    for (const auto& [aid, transition] : parent_state_->get_sleep_set()) {
-      if (not incoming_transition_->depends(transition.get())) {
-        sleep_set_.try_emplace(aid, transition);
-        if (strategy_->actors_to_run_.count(aid) != 0) {
-          XBT_DEBUG("Actor %ld will not be explored, for it is in the sleep set", aid);
-          strategy_->actors_to_run_.at(aid).mark_done();
-        }
-      } else
-        XBT_DEBUG("Transition >>%s<< removed from the sleep set because it was dependent with incoming >>%s<<",
-                  transition->to_string().c_str(), incoming_transition_->to_string().c_str());
-    }
+  /* 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
+   * it is not explored*/
+  for (const auto& [aid, transition] : parent_state_->get_sleep_set()) {
+    if (not incoming_transition_->depends(transition.get())) {
+      sleep_set_.try_emplace(aid, transition);
+      if (strategy_->actors_to_run_.count(aid) != 0) {
+        XBT_DEBUG("Actor %ld will not be explored, for it is in the sleep set", aid);
+        strategy_->actors_to_run_.at(aid).mark_done();
+      }
+    } else
+      XBT_DEBUG("Transition >>%s<< removed from the sleep set because it was dependent with incoming >>%s<<",
+                transition->to_string().c_str(), incoming_transition_->to_string().c_str());
   }
 }
 

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index aa7fbb0..5bf8cd0 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -198,7 +198,7 @@ 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 (const auto& [aid, transition] : state->get_sleep_set())
         XBT_VERB("  <%ld,%s>", aid, transition->to_string().c_str());
@@ -561,14 +561,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)

diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp
index cdba765..bde1a6b 100644 (file)
--- a/src/mc/mc_config.cpp
+++ b/src/mc/mc_config.cpp
@@ -62,10 +62,6 @@ static simgrid::config::Flag<std::string> cfg_mc_reduction{
                 " 'none', 'dpor', 'sdpor', 'odpor', or 'udpor'");
     }};
 
-simgrid::config::Flag<bool> _sg_mc_sleep_set{
-    "model-check/sleep-set", "Whether to enable the use of sleep-set in the reduction algorithm", true,
-    [](bool) { _mc_cfg_cb_check("value to enable/disable the use of sleep-set in the reduction algorithm"); }};
-
 simgrid::config::Flag<std::string> _sg_mc_strategy{
     "model-check/strategy",
     "Specify the the kind of heuristic to use for guided model-checking",

diff --git a/src/mc/mc_config.hpp b/src/mc/mc_config.hpp
index 07d199f..b581155 100644 (file)
--- a/src/mc/mc_config.hpp
+++ b/src/mc/mc_config.hpp
@@ -29,7 +29,6 @@ extern XBT_PRIVATE simgrid::config::Flag<int> _sg_mc_random_seed;
 extern "C" XBT_PUBLIC int _sg_mc_max_visited_states;
 extern XBT_PRIVATE simgrid::config::Flag<std::string> _sg_mc_dot_output_file;
 extern XBT_PRIVATE simgrid::config::Flag<bool> _sg_mc_termination;
-extern XBT_PUBLIC simgrid::config::Flag<bool> _sg_mc_sleep_set;
 extern XBT_PUBLIC simgrid::config::Flag<std::string> _sg_mc_strategy;
 
 #endif