From f01650f24121782b62c9ddca5bacb4e5867a8230 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Tue, 7 Nov 2023 23:25:46 +0100 Subject: [PATCH] Add an assert that the checker don't try to exec disabled transitions It's too bad this assert actually fails sometimes with ODPOR :) --- src/mc/remote/AppSide.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp index 84769a1dc9..aabac0027a 100644 --- a/src/mc/remote/AppSide.cpp +++ b/src/mc/remote/AppSide.cpp @@ -89,6 +89,8 @@ void AppSide::handle_simcall_execute(const s_mc_message_simcall_execute_t* messa { kernel::actor::ActorImpl* actor = kernel::EngineImpl::get_instance()->get_actor_by_pid(message->aid_); xbt_assert(actor != nullptr, "Invalid pid %ld", message->aid_); + xbt_assert(actor->simcall_.observer_ == nullptr || actor->simcall_.observer_->is_enabled(), + "Please, model-checker, don't execute disabled transitions."); // The client may send some messages to the server while processing the transition actor->simcall_handle(message->times_considered_); -- 2.20.1