src/mc/mc_request.c

   1 /* Copyright (c) 2008-2014. The SimGrid Team.
   2  * All rights reserved.                                                     */
   3
   4 /* This program is free software; you can redistribute it and/or modify it
   5  * under the terms of the license (GNU LGPL) which comes with this package. */
   6
   7 #include "mc_request.h"
   8 #include "mc_safety.h"
   9 #include "mc_private.h"
  10
  11 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_request, mc,
  12                                 "Logging specific to MC (request)");
  13
  14 static char *pointer_to_string(void *pointer);
  15 static char *buff_size_to_string(size_t size);
  16
  17 int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2)
  18 {
  19   if (mc_reduce_kind == e_mc_reduce_none)
  20     return TRUE;
  21
  22   if (r1->issuer == r2->issuer)
  23     return FALSE;
  24
  25   /* Wait with timeout transitions are not considered by the independance theorem, thus we consider them as dependant with all other transitions */
  26   if ((r1->call == SIMCALL_COMM_WAIT && simcall_comm_wait__get__timeout(r1) > 0)
  27       || (r2->call == SIMCALL_COMM_WAIT
  28           && simcall_comm_wait__get__timeout(r2) > 0))
  29     return TRUE;
  30
  31   if (r1->call == SIMCALL_COMM_ISEND && r2->call == SIMCALL_COMM_IRECV)
  32     return FALSE;
  33
  34   if (r1->call == SIMCALL_COMM_IRECV && r2->call == SIMCALL_COMM_ISEND)
  35     return FALSE;
  36
  37   if ((r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV)
  38       && r2->call == SIMCALL_COMM_WAIT) {
  39
  40     smx_rdv_t rdv =
  41         r1->call ==
  42         SIMCALL_COMM_ISEND ? simcall_comm_isend__get__rdv(r1) :
  43         simcall_comm_irecv__get__rdv(r1);
  44
  45     // FIXME, remote access to comm object
  46
  47     if (rdv != simcall_comm_wait__get__comm(r2)->comm.rdv_cpy
  48         && simcall_comm_wait__get__timeout(r2) <= 0)
  49       return FALSE;
  50
  51     if ((r1->issuer != simcall_comm_wait__get__comm(r2)->comm.src_proc)
  52         && (r1->issuer != simcall_comm_wait__get__comm(r2)->comm.dst_proc)
  53         && simcall_comm_wait__get__timeout(r2) <= 0)
  54       return FALSE;
  55
  56     if ((r1->call == SIMCALL_COMM_ISEND)
  57         && (simcall_comm_wait__get__comm(r2)->comm.type == SIMIX_COMM_SEND)
  58         && (simcall_comm_wait__get__comm(r2)->comm.src_buff !=
  59             simcall_comm_isend__get__src_buff(r1))
  60         && simcall_comm_wait__get__timeout(r2) <= 0)
  61       return FALSE;
  62
  63     if ((r1->call == SIMCALL_COMM_IRECV)
  64         && (simcall_comm_wait__get__comm(r2)->comm.type == SIMIX_COMM_RECEIVE)
  65         && (simcall_comm_wait__get__comm(r2)->comm.dst_buff !=
  66             simcall_comm_irecv__get__dst_buff(r1))
  67         && simcall_comm_wait__get__timeout(r2) <= 0)
  68       return FALSE;
  69   }
  70
  71   if ((r2->call == SIMCALL_COMM_ISEND || r2->call == SIMCALL_COMM_IRECV)
  72       && r1->call == SIMCALL_COMM_WAIT) {
  73
  74     smx_rdv_t rdv =
  75         r2->call ==
  76         SIMCALL_COMM_ISEND ? simcall_comm_isend__get__rdv(r2) :
  77         simcall_comm_irecv__get__rdv(r2);
  78
  79     if (rdv != simcall_comm_wait__get__comm(r1)->comm.rdv_cpy
  80         && simcall_comm_wait__get__timeout(r1) <= 0)
  81       return FALSE;
  82
  83     if ((r2->issuer != simcall_comm_wait__get__comm(r1)->comm.src_proc)
  84         && (r2->issuer != simcall_comm_wait__get__comm(r1)->comm.dst_proc)
  85         && simcall_comm_wait__get__timeout(r1) <= 0)
  86       return FALSE;
  87
  88     if ((r2->call == SIMCALL_COMM_ISEND)
  89         && (simcall_comm_wait__get__comm(r1)->comm.type == SIMIX_COMM_SEND)
  90         && (simcall_comm_wait__get__comm(r1)->comm.src_buff !=
  91             simcall_comm_isend__get__src_buff(r2))
  92         && simcall_comm_wait__get__timeout(r1) <= 0)
  93       return FALSE;
  94
  95     if ((r2->call == SIMCALL_COMM_IRECV)
  96         && (simcall_comm_wait__get__comm(r1)->comm.type == SIMIX_COMM_RECEIVE)
  97         && (simcall_comm_wait__get__comm(r1)->comm.dst_buff !=
  98             simcall_comm_irecv__get__dst_buff(r2))
  99         && simcall_comm_wait__get__timeout(r1) <= 0)
 100       return FALSE;
 101   }
 102
 103   /* FIXME: the following rule assumes that the result of the
 104    * isend/irecv call is not stored in a buffer used in the
 105    * test call. */
 106   /*if(   (r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV)
 107      &&  r2->call == SIMCALL_COMM_TEST)
 108      return FALSE; */
 109
 110   /* FIXME: the following rule assumes that the result of the
 111    * isend/irecv call is not stored in a buffer used in the
 112    * test call.*/
 113   /*if(   (r2->call == SIMCALL_COMM_ISEND || r2->call == SIMCALL_COMM_IRECV)
 114      && r1->call == SIMCALL_COMM_TEST)
 115      return FALSE; */
 116
 117   if (r1->call == SIMCALL_COMM_ISEND && r2->call == SIMCALL_COMM_ISEND
 118       && simcall_comm_isend__get__rdv(r1) != simcall_comm_isend__get__rdv(r2))
 119     return FALSE;
 120
 121   if (r1->call == SIMCALL_COMM_IRECV && r2->call == SIMCALL_COMM_IRECV
 122       && simcall_comm_irecv__get__rdv(r1) != simcall_comm_irecv__get__rdv(r2))
 123     return FALSE;
 124
 125   if (r1->call == SIMCALL_COMM_WAIT
 126       && (r2->call == SIMCALL_COMM_WAIT || r2->call == SIMCALL_COMM_TEST)
 127       && (simcall_comm_wait__get__comm(r1)->comm.src_proc == NULL
 128           || simcall_comm_wait__get__comm(r1)->comm.dst_proc == NULL))
 129     return FALSE;
 130
 131   if (r2->call == SIMCALL_COMM_WAIT
 132       && (r1->call == SIMCALL_COMM_WAIT || r1->call == SIMCALL_COMM_TEST)
 133       && (simcall_comm_wait__get__comm(r2)->comm.src_proc == NULL
 134           || simcall_comm_wait__get__comm(r2)->comm.dst_proc == NULL))
 135     return FALSE;
 136
 137   if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_WAIT
 138       && simcall_comm_wait__get__comm(r1)->comm.src_buff ==
 139       simcall_comm_wait__get__comm(r2)->comm.src_buff
 140       && simcall_comm_wait__get__comm(r1)->comm.dst_buff ==
 141       simcall_comm_wait__get__comm(r2)->comm.dst_buff)
 142     return FALSE;
 143
 144   if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_WAIT
 145       && simcall_comm_wait__get__comm(r1)->comm.src_buff != NULL
 146       && simcall_comm_wait__get__comm(r1)->comm.dst_buff != NULL
 147       && simcall_comm_wait__get__comm(r2)->comm.src_buff != NULL
 148       && simcall_comm_wait__get__comm(r2)->comm.dst_buff != NULL
 149       && simcall_comm_wait__get__comm(r1)->comm.dst_buff !=
 150       simcall_comm_wait__get__comm(r2)->comm.src_buff
 151       && simcall_comm_wait__get__comm(r1)->comm.dst_buff !=
 152       simcall_comm_wait__get__comm(r2)->comm.dst_buff
 153       && simcall_comm_wait__get__comm(r2)->comm.dst_buff !=
 154       simcall_comm_wait__get__comm(r1)->comm.src_buff)
 155     return FALSE;
 156
 157   if (r1->call == SIMCALL_COMM_TEST &&
 158       (simcall_comm_test__get__comm(r1) == NULL
 159        || simcall_comm_test__get__comm(r1)->comm.src_buff == NULL
 160        || simcall_comm_test__get__comm(r1)->comm.dst_buff == NULL))
 161     return FALSE;
 162
 163   if (r2->call == SIMCALL_COMM_TEST &&
 164       (simcall_comm_test__get__comm(r2) == NULL
 165        || simcall_comm_test__get__comm(r2)->comm.src_buff == NULL
 166        || simcall_comm_test__get__comm(r2)->comm.dst_buff == NULL))
 167     return FALSE;
 168
 169   if (r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT
 170       && simcall_comm_test__get__comm(r1)->comm.src_buff ==
 171       simcall_comm_wait__get__comm(r2)->comm.src_buff
 172       && simcall_comm_test__get__comm(r1)->comm.dst_buff ==
 173       simcall_comm_wait__get__comm(r2)->comm.dst_buff)
 174     return FALSE;
 175
 176   if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST
 177       && simcall_comm_wait__get__comm(r1)->comm.src_buff ==
 178       simcall_comm_test__get__comm(r2)->comm.src_buff
 179       && simcall_comm_wait__get__comm(r1)->comm.dst_buff ==
 180       simcall_comm_test__get__comm(r2)->comm.dst_buff)
 181     return FALSE;
 182
 183   if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST
 184       && simcall_comm_wait__get__comm(r1)->comm.src_buff != NULL
 185       && simcall_comm_wait__get__comm(r1)->comm.dst_buff != NULL
 186       && simcall_comm_test__get__comm(r2)->comm.src_buff != NULL
 187       && simcall_comm_test__get__comm(r2)->comm.dst_buff != NULL
 188       && simcall_comm_wait__get__comm(r1)->comm.dst_buff !=
 189       simcall_comm_test__get__comm(r2)->comm.src_buff
 190       && simcall_comm_wait__get__comm(r1)->comm.dst_buff !=
 191       simcall_comm_test__get__comm(r2)->comm.dst_buff
 192       && simcall_comm_test__get__comm(r2)->comm.dst_buff !=
 193       simcall_comm_wait__get__comm(r1)->comm.src_buff)
 194     return FALSE;
 195
 196   if (r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT
 197       && simcall_comm_test__get__comm(r1)->comm.src_buff != NULL
 198       && simcall_comm_test__get__comm(r1)->comm.dst_buff != NULL
 199       && simcall_comm_wait__get__comm(r2)->comm.src_buff != NULL
 200       && simcall_comm_wait__get__comm(r2)->comm.dst_buff != NULL
 201       && simcall_comm_test__get__comm(r1)->comm.dst_buff !=
 202       simcall_comm_wait__get__comm(r2)->comm.src_buff
 203       && simcall_comm_test__get__comm(r1)->comm.dst_buff !=
 204       simcall_comm_wait__get__comm(r2)->comm.dst_buff
 205       && simcall_comm_wait__get__comm(r2)->comm.dst_buff !=
 206       simcall_comm_test__get__comm(r1)->comm.src_buff)
 207     return FALSE;
 208
 209
 210   return TRUE;
 211 }
 212
 213 static char *pointer_to_string(void *pointer)
 214 {
 215
 216   if (XBT_LOG_ISENABLED(mc_request, xbt_log_priority_verbose))
 217     return bprintf("%p", pointer);
 218
 219   return xbt_strdup("(verbose only)");
 220 }
 221
 222 static char *buff_size_to_string(size_t buff_size)
 223 {
 224
 225   if (XBT_LOG_ISENABLED(mc_request, xbt_log_priority_verbose))
 226     return bprintf("%zu", buff_size);
 227
 228   return xbt_strdup("(verbose only)");
 229 }
 230
 231
 232 char *MC_request_to_string(smx_simcall_t req, int value)
 233 {
 234   char *type = NULL, *args = NULL, *str = NULL, *p = NULL, *bs = NULL;
 235   smx_synchro_t act = NULL;
 236   size_t size = 0;
 237
 238   // FIXME, host_get_name
 239   // FIXME, buffer access (issuer->name, issuer->smx_host)
 240
 241   smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, req);
 242
 243   switch (req->call) {
 244   case SIMCALL_COMM_ISEND:
 245     type = xbt_strdup("iSend");
 246     p = pointer_to_string(simcall_comm_isend__get__src_buff(req));
 247     bs = buff_size_to_string(simcall_comm_isend__get__src_buff_size(req));
 248     if (issuer->smx_host)
 249       args =
 250           bprintf("src=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
 251                   MSG_host_get_name(issuer->smx_host), issuer->name,
 252                   p, bs);
 253     else
 254       args =
 255           bprintf("src=(%lu)%s, buff=%s, size=%s", issuer->pid,
 256                   issuer->name, p, bs);
 257     break;
 258   case SIMCALL_COMM_IRECV:
 259     size =
 260         simcall_comm_irecv__get__dst_buff_size(req) ?
 261         *simcall_comm_irecv__get__dst_buff_size(req) : 0;
 262     type = xbt_strdup("iRecv");
 263     p = pointer_to_string(simcall_comm_irecv__get__dst_buff(req));
 264     bs = buff_size_to_string(size);
 265     if (issuer->smx_host)
 266       args =
 267           bprintf("dst=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
 268                   MSG_host_get_name(issuer->smx_host), issuer->name,
 269                   p, bs);
 270     else
 271       args =
 272           bprintf("dst=(%lu)%s, buff=%s, size=%s", issuer->pid,
 273                   issuer->name, p, bs);
 274     break;
 275   case SIMCALL_COMM_WAIT:
 276     act = simcall_comm_wait__get__comm(req);
 277     if (value == -1) {
 278       type = xbt_strdup("WaitTimeout");
 279       p = pointer_to_string(act);
 280       args = bprintf("comm=%s", p);
 281     } else {
 282       type = xbt_strdup("Wait");
 283       p = pointer_to_string(act);
 284       args = bprintf("comm=%s [(%lu)%s (%s)-> (%lu)%s (%s)]", p,
 285                      act->comm.src_proc ? act->comm.src_proc->pid : 0,
 286                      act->comm.src_proc ? MSG_host_get_name(act->comm.src_proc->
 287                                                             smx_host) : "",
 288                      act->comm.src_proc ? act->comm.src_proc->name : "",
 289                      act->comm.dst_proc ? act->comm.dst_proc->pid : 0,
 290                      act->comm.dst_proc ? MSG_host_get_name(act->comm.dst_proc->
 291                                                             smx_host) : "",
 292                      act->comm.dst_proc ? act->comm.dst_proc->name : "");
 293     }
 294     break;
 295   case SIMCALL_COMM_TEST:
 296     act = simcall_comm_test__get__comm(req);
 297     if (act->comm.src_proc == NULL || act->comm.dst_proc == NULL) {
 298       type = xbt_strdup("Test FALSE");
 299       p = pointer_to_string(act);
 300       args = bprintf("comm=%s", p);
 301     } else {
 302       type = xbt_strdup("Test TRUE");
 303       p = pointer_to_string(act);
 304       args = bprintf("comm=%s [(%lu)%s (%s) -> (%lu)%s (%s)]", p,
 305                      act->comm.src_proc->pid, act->comm.src_proc->name,
 306                      MSG_host_get_name(act->comm.src_proc->smx_host),
 307                      act->comm.dst_proc->pid, act->comm.dst_proc->name,
 308                      MSG_host_get_name(act->comm.dst_proc->smx_host));
 309     }
 310     break;
 311
 312   case SIMCALL_COMM_WAITANY:
 313     type = xbt_strdup("WaitAny");
 314     if (!xbt_dynar_is_empty(simcall_comm_waitany__get__comms(req))) {
 315       p = pointer_to_string(xbt_dynar_get_as
 316                             (simcall_comm_waitany__get__comms(req), value,
 317                              smx_synchro_t));
 318       args =
 319           bprintf("comm=%s (%d of %lu)", p, value + 1,
 320                   xbt_dynar_length(simcall_comm_waitany__get__comms(req)));
 321     } else {
 322       args = bprintf("comm at idx %d", value);
 323     }
 324     break;
 325
 326   case SIMCALL_COMM_TESTANY:
 327     if (value == -1) {
 328       type = xbt_strdup("TestAny FALSE");
 329       args = xbt_strdup("-");
 330     } else {
 331       type = xbt_strdup("TestAny");
 332       args =
 333           bprintf("(%d of %lu)", value + 1,
 334                   xbt_dynar_length(simcall_comm_testany__get__comms(req)));
 335     }
 336     break;
 337
 338   case SIMCALL_MC_SNAPSHOT:
 339     type = xbt_strdup("MC_SNAPSHOT");
 340     args = NULL;
 341     break;
 342
 343   case SIMCALL_MC_COMPARE_SNAPSHOTS:
 344     type = xbt_strdup("MC_COMPARE_SNAPSHOTS");
 345     args = NULL;
 346     break;
 347
 348   case SIMCALL_MC_RANDOM:
 349     type = xbt_strdup("MC_RANDOM");
 350     args = bprintf("%d", value);
 351     break;
 352
 353   default:
 354     THROW_UNIMPLEMENTED;
 355   }
 356
 357   if (args != NULL) {
 358     str =
 359         bprintf("[(%lu)%s (%s)] %s(%s)", issuer->pid,
 360                 MSG_host_get_name(issuer->smx_host), issuer->name,
 361                 type, args);
 362   } else {
 363     str =
 364         bprintf("[(%lu)%s (%s)] %s ", issuer->pid,
 365                 MSG_host_get_name(issuer->smx_host), issuer->name,
 366                 type);
 367   }
 368
 369   xbt_free(args);
 370   xbt_free(type);
 371   xbt_free(p);
 372   xbt_free(bs);
 373   return str;
 374 }
 375
 376 unsigned int MC_request_testany_fail(smx_simcall_t req)
 377 {
 378   unsigned int cursor;
 379   smx_synchro_t action;
 380
 381   xbt_dynar_foreach(simcall_comm_testany__get__comms(req), cursor, action) {
 382     if (action->comm.src_proc && action->comm.dst_proc)
 383       return FALSE;
 384   }
 385
 386   return TRUE;
 387 }
 388
 389 int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx)
 390 {
 391   smx_synchro_t act;
 392
 393   switch (req->call) {
 394
 395   case SIMCALL_COMM_WAIT:
 396     /* FIXME: check also that src and dst processes are not suspended */
 397     act = simcall_comm_wait__get__comm(req);
 398     return (act->comm.src_proc && act->comm.dst_proc);
 399     break;
 400
 401   case SIMCALL_COMM_WAITANY:
 402     act =
 403         xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), idx,
 404                          smx_synchro_t);
 405     return (act->comm.src_proc && act->comm.dst_proc);
 406     break;
 407
 408   case SIMCALL_COMM_TESTANY:
 409     act =
 410         xbt_dynar_get_as(simcall_comm_testany__get__comms(req), idx,
 411                          smx_synchro_t);
 412     return (act->comm.src_proc && act->comm.dst_proc);
 413     break;
 414
 415   default:
 416     return TRUE;
 417   }
 418 }
 419
 420 int MC_process_is_enabled(smx_process_t process)
 421 {
 422   return MC_request_is_enabled(&process->simcall);
 423 }
 424
 425 char *MC_request_get_dot_output(smx_simcall_t req, int value)
 426 {
 427   // TODO, remote access to MSG_host_get_name(issuer->smx_host)
 428
 429   char *str = NULL, *label = NULL;
 430   smx_synchro_t act = NULL;
 431
 432   const smx_process_t issuer = MC_process_get_issuer(&mc_model_checker->process, req);
 433
 434   switch (req->call) {
 435   case SIMCALL_COMM_ISEND:
 436     if (issuer->smx_host)
 437       label =
 438           bprintf("[(%lu)%s] iSend", issuer->pid,
 439                   MSG_host_get_name(issuer->smx_host));
 440     else
 441       label = bprintf("[(%lu)] iSend", issuer->pid);
 442     break;
 443
 444   case SIMCALL_COMM_IRECV:
 445     if (issuer->smx_host)
 446       label =
 447           bprintf("[(%lu)%s] iRecv", issuer->pid,
 448                   MSG_host_get_name(issuer->smx_host));
 449     else
 450       label = bprintf("[(%lu)] iRecv", issuer->pid);
 451     break;
 452
 453   case SIMCALL_COMM_WAIT:
 454     act = simcall_comm_wait__get__comm(req);
 455     if (value == -1) {
 456       if (issuer->smx_host)
 457         label =
 458             bprintf("[(%lu)%s] WaitTimeout", issuer->pid,
 459                     MSG_host_get_name(issuer->smx_host));
 460       else
 461         label = bprintf("[(%lu)] WaitTimeout", issuer->pid);
 462     } else {
 463       if (issuer->smx_host)
 464         label =
 465             bprintf("[(%lu)%s] Wait [(%lu)->(%lu)]", issuer->pid,
 466                     MSG_host_get_name(issuer->smx_host),
 467                     act->comm.src_proc ? act->comm.src_proc->pid : 0,
 468                     act->comm.dst_proc ? act->comm.dst_proc->pid : 0);
 469       else
 470         label =
 471             bprintf("[(%lu)] Wait [(%lu)->(%lu)]", issuer->pid,
 472                     act->comm.src_proc ? act->comm.src_proc->pid : 0,
 473                     act->comm.dst_proc ? act->comm.dst_proc->pid : 0);
 474     }
 475     break;
 476
 477   case SIMCALL_COMM_TEST:
 478     act = simcall_comm_test__get__comm(req);
 479     if (act->comm.src_proc == NULL || act->comm.dst_proc == NULL) {
 480       if (issuer->smx_host)
 481         label =
 482             bprintf("[(%lu)%s] Test FALSE", issuer->pid,
 483                     MSG_host_get_name(issuer->smx_host));
 484       else
 485         label = bprintf("[(%lu)] Test FALSE", issuer->pid);
 486     } else {
 487       if (issuer->smx_host)
 488         label =
 489             bprintf("[(%lu)%s] Test TRUE", issuer->pid,
 490                     MSG_host_get_name(issuer->smx_host));
 491       else
 492         label = bprintf("[(%lu)] Test TRUE", issuer->pid);
 493     }
 494     break;
 495
 496   case SIMCALL_COMM_WAITANY:
 497     if (issuer->smx_host)
 498       label =
 499           bprintf("[(%lu)%s] WaitAny [%d of %lu]", issuer->pid,
 500                   MSG_host_get_name(issuer->smx_host), value + 1,
 501                   xbt_dynar_length(simcall_comm_waitany__get__comms(req)));
 502     else
 503       label =
 504           bprintf("[(%lu)] WaitAny [%d of %lu]", issuer->pid, value + 1,
 505                   xbt_dynar_length(simcall_comm_waitany__get__comms(req)));
 506     break;
 507
 508   case SIMCALL_COMM_TESTANY:
 509     if (value == -1) {
 510       if (issuer->smx_host)
 511         label =
 512             bprintf("[(%lu)%s] TestAny FALSE", issuer->pid,
 513                     MSG_host_get_name(issuer->smx_host));
 514       else
 515         label = bprintf("[(%lu)] TestAny FALSE", issuer->pid);
 516     } else {
 517       if (issuer->smx_host)
 518         label =
 519             bprintf("[(%lu)%s] TestAny TRUE [%d of %lu]", issuer->pid,
 520                     MSG_host_get_name(issuer->smx_host), value + 1,
 521                     xbt_dynar_length(simcall_comm_testany__get__comms(req)));
 522       else
 523         label =
 524             bprintf("[(%lu)] TestAny TRUE [%d of %lu]", issuer->pid,
 525                     value + 1,
 526                     xbt_dynar_length(simcall_comm_testany__get__comms(req)));
 527     }
 528     break;
 529
 530   case SIMCALL_MC_RANDOM:
 531     if (issuer->smx_host)
 532       label =
 533           bprintf("[(%lu)%s] MC_RANDOM (%d)", issuer->pid,
 534                   MSG_host_get_name(issuer->smx_host), value);
 535     else
 536       label = bprintf("[(%lu)] MC_RANDOM (%d)", issuer->pid, value);
 537     break;
 538
 539   case SIMCALL_MC_SNAPSHOT:
 540     if (issuer->smx_host)
 541       label =
 542           bprintf("[(%lu)%s] MC_SNAPSHOT", issuer->pid,
 543                   MSG_host_get_name(issuer->smx_host));
 544     else
 545       label = bprintf("[(%lu)] MC_SNAPSHOT", issuer->pid);
 546     break;
 547
 548   case SIMCALL_MC_COMPARE_SNAPSHOTS:
 549     if (issuer->smx_host)
 550       label =
 551           bprintf("[(%lu)%s] MC_COMPARE_SNAPSHOTS", issuer->pid,
 552                   MSG_host_get_name(issuer->smx_host));
 553     else
 554       label = bprintf("[(%lu)] MC_COMPARE_SNAPSHOTS", issuer->pid);
 555     break;
 556
 557   default:
 558     THROW_UNIMPLEMENTED;
 559   }
 560
 561   str =
 562       bprintf("label = \"%s\", color = %s, fontcolor = %s", label,
 563               colors[issuer->pid - 1], colors[issuer->pid - 1]);
 564   xbt_free(label);
 565   return str;
 566
 567 }