[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 f79c6b98bf42763cf67a0b40f9d189bd65fde99b..62a4f5c17737fe323537efeb45bff41a5f69d607 100644 (file)
--- a/src/mc/SafetyChecker.cpp
+++ b/src/mc/SafetyChecker.cpp
@@ -132,7 +132,6 @@ int SafetyChecker::run()
     if (dot_output != nullptr)
       req_str = simgrid::mc::request_get_dot_output(req, value);
 
-    MC_state_set_executed_request(state, req, value);
     mc_stats->executed_transitions++;
 
     // TODO, bundle both operations in a single message
@@ -157,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;
         }
@@ -239,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);
 
@@ -310,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;
     }