adding option for sleep set

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 0e5dd64..ccd0fea 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -307,6 +307,8 @@ DFSExplorer::DFSExplorer(const std::vector<char*>& args, bool with_dpor) : Explo
   else
     reduction_mode_ = ReductionMode::none;
 
+  sleep_set_reduction_ = _sg_mc_sleep_set;
+  
   if (_sg_mc_termination) {
     if (with_dpor) {
       XBT_INFO("Check non progressive cycles (turning DPOR off)");

diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp
index 1a6af99..8920c57 100644 (file)
--- a/src/mc/mc_config.cpp
+++ b/src/mc/mc_config.cpp
@@ -48,6 +48,14 @@ static simgrid::config::Flag<std::string> cfg_mc_reduction{
         xbt_die("configuration option 'model-check/reduction' can only take 'none' or 'dpor' as a value");
     }};
 
+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<int> _sg_mc_checkpoint{
     "model-check/checkpoint", "Specify the amount of steps between checkpoints during stateful model-checking "
                               "(default: 0 => stateless verification). If value=1, one checkpoint is saved for each "

diff --git a/src/mc/mc_config.hpp b/src/mc/mc_config.hpp
index 1f91c22..eaf2e20 100644 (file)
--- a/src/mc/mc_config.hpp
+++ b/src/mc/mc_config.hpp
@@ -25,5 +25,6 @@ extern XBT_PRIVATE simgrid::config::Flag<int> _sg_mc_max_depth;
 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;
 
 #endif