X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/35b406733ae5c5b8463d3712a09b430d8585ce6d..57970bcf4905da230f47be5c0f9a37128cca29f4:/src/mc/checker/SafetyChecker.cpp

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index 643c734c5b..4256b56a26 100644
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -22,10 +22,7 @@
 #include "src/mc/mc_private.h"
 #include "src/mc/mc_record.h"
 #include "src/mc/mc_request.h"
-#include "src/mc/mc_safety.h"
 #include "src/mc/mc_smx.h"
-#include "src/mc/mc_state.h"
-#include "src/mc/remote/Client.hpp"
 
 #include "src/xbt/mmalloc/mmprivate.h"
 
@@ -95,7 +92,7 @@ void SafetyChecker::run()
    * We do so iteratively instead of recursively, dealing with the call stack manually.
    * This allows to explore the call stack at wish. */
 
-  while (!stack_.empty()) {
+  while (not stack_.empty()) {
 
     /* Get current state */
     simgrid::mc::State* state = stack_.back().get();
@@ -165,12 +162,14 @@ void SafetyChecker::run()
     if (visitedState_ == nullptr) {
 
       /* Get an enabled process and insert it in the interleave set of the next state */
-      for (auto& actor : mc_model_checker->process().actors())
-        if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
-          next_state->interleave(actor.copy.getBuffer());
+      for (auto& remoteActor : mc_model_checker->process().actors()) {
+        auto actor = remoteActor.copy.getBuffer();
+        if (simgrid::mc::actor_is_enabled(actor)) {
+          next_state->addInterleavingSet(actor);
           if (reductionMode_ == simgrid::mc::ReductionMode::dpor)
-            break;
+            break; // With DPOR, we take the first enabled transition
         }
+      }
 
       if (dot_output != nullptr)
         std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
@@ -205,7 +204,7 @@ void SafetyChecker::backtrack()
      executed before it. If it does then add it to the interleave set of the
      state that executed that previous request. */
 
-  while (!stack_.empty()) {
+  while (not stack_.empty()) {
     std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
     stack_.pop_back();
     if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
@@ -233,8 +232,8 @@ void SafetyChecker::backtrack()
               state->num);
           }
 
-          if (!prev_state->actorStates[issuer->pid].isDone())
-            prev_state->interleave(issuer);
+          if (not prev_state->actorStates[issuer->pid].isDone())
+            prev_state->addInterleavingSet(issuer);
           else
             XBT_DEBUG("Process %p is in done set", req->issuer);
 
@@ -324,7 +323,7 @@ SafetyChecker::SafetyChecker(Session& session) : Checker(session)
   /* Get an enabled actor and insert it in the interleave set of the initial state */
   for (auto& actor : mc_model_checker->process().actors())
     if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
-      initial_state->interleave(actor.copy.getBuffer());
+      initial_state->addInterleavingSet(actor.copy.getBuffer());
       if (reductionMode_ != simgrid::mc::ReductionMode::none)
         break;
     }
@@ -332,10 +331,6 @@ SafetyChecker::SafetyChecker(Session& session) : Checker(session)
   stack_.push_back(std::move(initial_state));
 }
 
-SafetyChecker::~SafetyChecker()
-{
-}
-
 Checker* createSafetyChecker(Session& session)
 {
   return new SafetyChecker(session);