Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Default is not to use sleep-set to agree with existing tests
authormlaurent <mathieu.laurent@ens-rennes.fr>
Fri, 17 Feb 2023 09:33:36 +0000 (10:33 +0100)
committermlaurent <mathieu.laurent@ens-rennes.fr>
Fri, 17 Feb 2023 09:33:36 +0000 (10:33 +0100)
src/mc/explo/DFSExplorer.cpp
src/mc/explo/DFSExplorer.hpp
src/mc/mc_config.cpp

index fa83449..a3e0c38 100644 (file)
@@ -160,7 +160,7 @@ void DFSExplorer::run()
              state->get_transition()->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) */
-    std::__detail::__unique_ptr_t<simgrid::mc::State> next_state;
+    std::unique_ptr<State> next_state;
 
     /* If we want sleep set reduction, pass the old state to the new state so it can
      * both copy the sleep set and eventually removes things from it locally */
index 9244842..ad79c59 100644 (file)
@@ -83,7 +83,7 @@ public:
 private:
   void check_non_termination(const State* current_state);
   void backtrack();
-  bool sleep_set_reduction_ = true; 
+  bool sleep_set_reduction_;
 
   /** Stack representing the position in the exploration graph */
   std::list<std::unique_ptr<State>> stack_;
index 8920c57..6b6ea8b 100644 (file)
@@ -49,12 +49,8 @@ static simgrid::config::Flag<std::string> cfg_mc_reduction{
     }};
 
 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");
-    }};
+    "model-check/sleep-set", "Whether to enable the use of sleep-set in the reduction algorithm", false,
+    [](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 "