A few calls to mc_model_checker less by passing more parameters

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

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index aea0570..8475395 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -117,7 +117,7 @@ void DFSExplorer::run()
       continue;
     }
 
-    // Backtrack if we are revisiting a state we saw previously
+    // Backtrack if we are revisiting a state we saw previously while applying state-equality reduction
     if (visited_state_ != nullptr) {
       XBT_DEBUG("State already visited (equal to state %ld), exploration stopped on this path.",
                 visited_state_->original_num_ == -1 ? visited_state_->num_ : visited_state_->original_num_);
@@ -152,7 +152,7 @@ void DFSExplorer::run()
     }
 
     /* Actually answer the request: let's execute the selected request (MCed does one step) */
-    state->execute_next(next);
+    state->execute_next(next, get_remote_app());
     on_transition_execute_signal(state->get_transition(), get_remote_app());
 
     // If there are processes to interleave and the maximum depth has not been
@@ -163,12 +163,7 @@ void DFSExplorer::run()
     /* Create the new expanded state (copy the state of MCed into our MCer data) */
     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 */
-    if (_sg_mc_sleep_set)
-      next_state = std::make_unique<State>(get_remote_app(), state);
-    else
-      next_state = std::make_unique<State>(get_remote_app());
+    next_state = std::make_unique<State>(get_remote_app(), state);
 
     on_state_creation_signal(next_state.get(), get_remote_app());