From 12e01354e36033d37625d9675769d18058f7c1e7 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Mon, 17 Jul 2017 08:09:01 +0200 Subject: [PATCH] untangle a tiny bit checker algo and enabled actor --- src/mc/mc_state.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp index f37e793654..94ef18847c 100644 --- a/src/mc/mc_state.cpp +++ b/src/mc/mc_state.cpp @@ -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; -- 2.20.1