+ // Now, we are in the client app, no need for remote memory reading.
+ smx_simcall_t req = &actor->simcall;
+
+ if (req->transition != nullptr)
+ return req->transition->fireable();
+
+ switch (req->call) {
+ case SIMCALL_NONE:
+ return false;
+
+ case SIMCALL_COMM_WAIT: {
+ /* FIXME: check also that src and dst processes are not suspended */
+ simgrid::kernel::activity::CommImpl* act =
+ static_cast<simgrid::kernel::activity::CommImpl*>(simcall_comm_wait__getraw__comm(req));
+
+ if (act->src_timeout_ || act->dst_timeout_) {
+ /* If it has a timeout it will be always be enabled (regardless of who declared the timeout),
+ * because even if the communication is not ready, it can timeout and won't block. */
+ if (_sg_mc_timeout == 1)
+ return true;
+ }
+ /* On the other hand if it hasn't a timeout, check if the comm is ready.*/
+ else if (act->detached() && act->src_actor_ == nullptr &&
+ act->type_ == simgrid::kernel::activity::CommImpl::Type::READY)
+ return (act->dst_actor_ != nullptr);
+ return (act->src_actor_ && act->dst_actor_);
+ }
+
+ case SIMCALL_COMM_WAITANY: {
+ simgrid::kernel::activity::CommImpl** comms = simcall_comm_waitany__get__comms(req);
+ size_t count = simcall_comm_waitany__get__count(req);
+ for (unsigned int index = 0; index < count; ++index) {
+ auto* comm = comms[index];
+ if (comm->src_actor_ && comm->dst_actor_)
+ return true;
+ }
+ return false;
+ }
+
+ case SIMCALL_MUTEX_LOCK: {
+ smx_mutex_t mutex = simcall_mutex_lock__get__mutex(req);
+
+ if (mutex->owner_ == nullptr)
+ return true;
+ return mutex->owner_->get_pid() == req->issuer->get_pid();
+ }
+
+ case SIMCALL_SEM_ACQUIRE: {
+ static int warned = 0;
+ if (not warned)
+ XBT_INFO("Using semaphore in model-checked code is still experimental. Use at your own risk");
+ warned = 1;
+ return true;
+ }
+
+ case SIMCALL_COND_WAIT: {
+ static int warned = 0;
+ if (not warned)
+ XBT_INFO("Using condition variables in model-checked code is still experimental. Use at your own risk");
+ warned = 1;
+ return true;
+ }
+
+ default:
+ /* The rest of the requests are always enabled */
+ return true;
+ }