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 84769a1..aabac00 100644 (file)
--- 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_);