[mc] Simplify/unify the interleeaving/exploration logic

[simgrid.git] / src / mc / SafetyChecker.cpp

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index e7c62e8a3f5c6809ca4cad654aa4f68b5cef928a..62a4f5c17737fe323537efeb45bff41a5f69d607 100644 (file)
--- a/src/mc/SafetyChecker.cpp
+++ b/src/mc/SafetyChecker.cpp
@@ -156,7 +156,7 @@ int SafetyChecker::run()
       /* Get an enabled process and insert it in the interleave set of the next state */
       for (auto& p : mc_model_checker->process().simix_processes())
         if (simgrid::mc::process_is_enabled(&p.copy)) {
-          MC_state_interleave_process(next_state.get(), &p.copy);
+          next_state->interleave(&p.copy);
           if (reductionMode_ != simgrid::mc::ReductionMode::none)
             break;
         }
@@ -238,8 +238,8 @@ int SafetyChecker::backtrack()
               state->num);
           }
 
-          if (!prev_state->processStates[issuer->pid].done())
-            MC_state_interleave_process(prev_state, issuer);
+          if (!prev_state->processStates[issuer->pid].isDone())
+            prev_state->interleave(issuer);
           else
             XBT_DEBUG("Process %p is in done set", req->issuer);
 
@@ -309,7 +309,7 @@ void SafetyChecker::init()
   /* Get an enabled process and insert it in the interleave set of the initial state */
   for (auto& p : mc_model_checker->process().simix_processes())
     if (simgrid::mc::process_is_enabled(&p.copy)) {
-      MC_state_interleave_process(initial_state.get(), &p.copy);
+      initial_state->interleave(&p.copy);
       if (reductionMode_ != simgrid::mc::ReductionMode::none)
         break;
     }