X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/8c6bbb14f44b8daed5ea43d80880c6bf2155118b..76fd6cc1330945172740464411a0b2f1170dcb2a:/src/mc/mc_base.cpp diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp index 64a2ae63a7..6e4ecf107b 100644 --- a/src/mc/mc_base.cpp +++ b/src/mc/mc_base.cpp @@ -8,14 +8,13 @@ #include "src/kernel/activity/CommImpl.hpp" #include "src/kernel/activity/MutexImpl.hpp" #include "src/kernel/actor/SimcallObserver.hpp" + #include "src/mc/mc.h" +#include "src/mc/mc_config.hpp" #include "src/mc/mc_replay.hpp" -#if SIMGRID_HAVE_MC -#include "src/mc/ModelChecker.hpp" -#include "src/mc/api/RemoteApp.hpp" -#include "src/mc/remote/AppSide.hpp" -#include "src/mc/remote/RemoteProcess.hpp" +#if SIMGRID_HAVE_STATEFUL_MC +#include "src/mc/sosp/RemoteProcessMemory.hpp" #endif XBT_LOG_NEW_DEFAULT_CATEGORY(mc, "All MC categories"); @@ -52,9 +51,8 @@ void execute_actors() */ bool actor_is_enabled(kernel::actor::ActorImpl* actor) { -#if SIMGRID_HAVE_MC - xbt_assert(mc_model_checker == nullptr, "This should be called from the client side"); -#endif + xbt_assert(get_model_checking_mode() != ModelCheckingMode::CHECKER_SIDE, + "This should be called from the client side"); // Now, we are in the client app, no need for remote memory reading. kernel::actor::Simcall* req = &actor->simcall_; @@ -74,9 +72,9 @@ bool actor_is_enabled(kernel::actor::ActorImpl* actor) */ bool request_is_visible(const kernel::actor::Simcall* req) { -#if SIMGRID_HAVE_MC - xbt_assert(mc_model_checker == nullptr, "This should be called from the client side"); -#endif + xbt_assert(get_model_checking_mode() != ModelCheckingMode::CHECKER_SIDE, + "This should be called from the client side"); + if (req->observer_ == nullptr) return false; return req->observer_->is_visible();