From: Martin Quinson <martin.quinson@ens-rennes.fr>
Date: Tue, 7 Nov 2023 22:25:46 +0000 (+0100)
Subject: Add an assert that the checker don't try to exec disabled transitions
X-Git-Tag: v3.35~87^2~2
X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/f01650f24121782b62c9ddca5bacb4e5867a8230

Add an assert that the checker don't try to exec disabled transitions

It's too bad this assert actually fails sometimes with ODPOR :)
---

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_);