- case SIMCALL_NONE:
- return false;
-
- case SIMCALL_SEM_ACQUIRE:
- xbt_die("Don't use semaphores in model-checked code, it's not supported yet");
- case SIMCALL_COND_WAIT:
- xbt_die("Don't use condition variables in model-checked code, it's not supported yet");
-
- case SIMCALL_COMM_WAIT:
- {
- /* FIXME: check also that src and dst processes are not suspended */
- simgrid::kernel::activity::Comm *act =
- static_cast<simgrid::kernel::activity::Comm*>(simcall_comm_wait__get__comm(req));
-
-#if HAVE_MC
- // Fetch from MCed memory:
- // HACK, type puning
- if (mc_model_checker != nullptr) {
- simgrid::mc::Remote<simgrid::kernel::activity::Comm> temp_comm;
- mc_model_checker->process().read(temp_comm, remote(act));
- act = static_cast<simgrid::kernel::activity::Comm*>(temp_comm.getBuffer());
+ 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_proc == nullptr && act->type == SIMIX_COMM_READY)
+ return (act->dst_proc != nullptr);
+ return (act->src_proc && act->dst_proc);