+ case SIMCALL_COMM_IRECV:
+ if (issuer->smx_host)
+ label =
+ bprintf("[(%lu)%s] iRecv", issuer->pid,
+ MC_smx_process_get_host_name(issuer));
+ else
+ label = bprintf("[(%lu)] iRecv", issuer->pid);
+ break;
+
+ case SIMCALL_COMM_WAIT: {
+ if (value == -1) {
+ if (issuer->smx_host)
+ label =
+ bprintf("[(%lu)%s] WaitTimeout", issuer->pid,
+ MC_smx_process_get_host_name(issuer));
+ else
+ label = bprintf("[(%lu)] WaitTimeout", issuer->pid);
+ } else {
+ smx_synchro_t remote_act = simcall_comm_wait__get__comm(req);
+ s_smx_synchro_t synchro;
+ MC_process_read_simple(&mc_model_checker->process, &synchro,
+ remote_act, sizeof(synchro));
+
+ smx_process_t src_proc = MC_smx_resolve_process(synchro.comm.src_proc);
+ smx_process_t dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc);
+ if (issuer->smx_host)
+ label =
+ bprintf("[(%lu)%s] Wait [(%lu)->(%lu)]", issuer->pid,
+ MC_smx_process_get_host_name(issuer),
+ src_proc ? src_proc->pid : 0,
+ dst_proc ? dst_proc->pid : 0);
+ else
+ label =
+ bprintf("[(%lu)] Wait [(%lu)->(%lu)]", issuer->pid,
+ src_proc ? src_proc->pid : 0,
+ dst_proc ? dst_proc->pid : 0);
+ }
+ break;
+ }
+
+ case SIMCALL_COMM_TEST: {
+ smx_synchro_t remote_act = simcall_comm_test__get__comm(req);
+ s_smx_synchro_t synchro;
+ MC_process_read_simple(&mc_model_checker->process, &synchro,
+ remote_act, sizeof(synchro));
+ if (synchro.comm.src_proc == NULL || synchro.comm.dst_proc == NULL) {
+ if (issuer->smx_host)
+ label =
+ bprintf("[(%lu)%s] Test FALSE", issuer->pid,
+ MC_smx_process_get_host_name(issuer));
+ else
+ label = bprintf("[(%lu)] Test FALSE", issuer->pid);
+ } else {
+ if (issuer->smx_host)
+ label =
+ bprintf("[(%lu)%s] Test TRUE", issuer->pid,
+ MC_smx_process_get_host_name(issuer));
+ else
+ label = bprintf("[(%lu)] Test TRUE", issuer->pid);
+ }