untangle a tiny bit checker algo and enabled actor

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

diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp
index f606492..94ef188 100644 (file)
--- a/src/mc/mc_state.cpp
+++ b/src/mc/mc_state.cpp
@@ -10,14 +10,14 @@
 #include "xbt/log.h"
 #include "xbt/sysdep.h"
 
-#include "src/simix/smx_private.h"
-#include "src/mc/mc_state.h"
-#include "src/mc/mc_request.h"
+#include "src/mc/Transition.hpp"
+#include "src/mc/mc_comm_pattern.hpp"
 #include "src/mc/mc_private.h"
-#include "src/mc/mc_comm_pattern.h"
+#include "src/mc/mc_request.h"
 #include "src/mc/mc_smx.h"
+#include "src/mc/mc_state.h"
 #include "src/mc/mc_xbt.hpp"
-#include "src/mc/Transition.hpp"
+#include "src/simix/smx_private.h"
 
 using simgrid::mc::remote;
 
@@ -80,8 +80,6 @@ static inline smx_simcall_t MC_state_get_request_for_process(
   state->transition.argument           = -1;
   state->executed_req.call             = SIMCALL_NONE;
 
-  if (not procstate->isTodo())
-    return nullptr; // Not considered by the checker algorithm
   if (not simgrid::mc::actor_is_enabled(actor))
     return nullptr; // Not executable in the application
 
@@ -225,6 +223,10 @@ static inline smx_simcall_t MC_state_get_request_for_process(
 smx_simcall_t MC_state_get_request(simgrid::mc::State* state)
 {
   for (auto& actor : mc_model_checker->process().actors()) {
+    /* Only consider the actors that were marked as interleaving by the checker algorithm */
+    if (not state->actorStates[actor.copy.getBuffer()->pid].isTodo())
+      continue;
+
     smx_simcall_t res = MC_state_get_request_for_process(state, actor.copy.getBuffer());
     if (res)
       return res;