double clock = MSG_get_clock(); /* this "call" is free thanks to inlining */
sprintf(full_name, "%s:%s", MSG_process_get_name(MSG_process_self()),
double clock = MSG_get_clock(); /* this "call" is free thanks to inlining */
sprintf(full_name, "%s:%s", MSG_process_get_name(MSG_process_self()),