It is not useless: model-checking is enabled when we use the simgrid-mc wrapper.
\section options_modelchecking Configuring the Model-Checking
-To enable the experimental SimGrid model-checking support the program should
-be executed with the command line argument
+To enable the SimGrid model-checking support the program should
+be executed using the simgrid-mc wrapper:
\verbatim
---cfg=model-check:1
+simgrid-mc ./my_program
\endverbatim
Safety properties are expressed as assertions using the function
--cfg=model-check/property:<filename>
\endverbatim
-Of course, specifying a liveness property enables the model-checking
-so that you don't have to give <tt>--cfg=model-check:1</tt> in
-addition.
-
\subsection options_modelchecking_steps Going for stateful verification
By default, the system is backtracked to its initial state to explore
--cfg=model-check/checkpoint:1
\endverbatim
-Of course, specifying this option enables the model-checking so that
-you don't have to give <tt>--cfg=model-check:1</tt> in addition.
-
\subsection options_modelchecking_reduction Specifying the kind of reduction
The main issue when using the model-checking is the state space
* dpor: Apply Dynamic Partial Ordering Reduction. Only valid if you
verify local safety properties.
-Of course, specifying a reduction technique enables the model-checking
-so that you don't have to give <tt>--cfg=model-check:1</tt> in
-addition.
-
\subsection options_modelchecking_visited model-check/visited, Cycle detection
In order to detect cycles, the model-checker needs to check if a new explored
! expect return 1
! timeout 20
-$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1 --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=contexts/stack_size:256
+$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=contexts/stack_size:256
> [ 0.000000] (0:@) Check a safety property
> [ 0.000000] (2:client@HostB) Sent!
> [ 0.000000] (3:client@HostC) Sent!
! expect return 2
! timeout 20
-$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack_size:256 --cfg=model-check/property:promela_bugged1_liveness
+$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack_size:256 --cfg=model-check/property:promela_bugged1_liveness
> [ 0.000000] (0:@) Check the liveness property promela_bugged1_liveness
> [ 0.000000] (2:client@Boivin) Ask the request
> [ 0.000000] (3:client@Fafard) Ask the request
! expect return 2
! timeout 60
-$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack_size:256 --cfg=model-check/sparse-checkpoint:yes --cfg=model-check/property:promela_bugged1_liveness
+$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack_size:256 --cfg=model-check/sparse-checkpoint:yes --cfg=model-check/property:promela_bugged1_liveness
> [ 0.000000] (0:@) Check the liveness property promela_bugged1_liveness
> [ 0.000000] (2:client@Boivin) Ask the request
> [ 0.000000] (3:client@Fafard) Ask the request
timeout 30s ${bindir:=.}/bugged1_liveness_cleaner_$state \
${srcdir:=.}/../../platforms/platform.xml \
${srcdir:=.}/deploy_bugged1_liveness.xml \
- --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" \
+ "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" \
--cfg=contexts/factory:ucontext \
--cfg=contexts/stack_size:256
assert 'test $? = 134'
! expect return 2
! timeout 90
-$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack_size:256 --cfg=model-check/property:promela_bugged1_liveness
+$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack_size:256 --cfg=model-check/property:promela_bugged1_liveness
> [ 0.000000] (0:@) Check the liveness property promela_bugged1_liveness
> [ 0.000000] (2:client@Boivin) Ask the request
> [ 0.000000] (3:client@Fafard) Ask the request
! expect return 2
! timeout 90
-$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack_size:256 --cfg=model-check/sparse-checkpoint:yes --cfg=model-check/property:promela_bugged1_liveness
+$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack_size:256 --cfg=model-check/sparse-checkpoint:yes --cfg=model-check/property:promela_bugged1_liveness
> [ 0.000000] (0:@) Check the liveness property promela_bugged1_liveness
> [ 0.000000] (2:client@Boivin) Ask the request
> [ 0.000000] (3:client@Fafard) Ask the request
! expect return 1
! timeout 20
-$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged2 --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=contexts/stack_size:256
+$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged2 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=contexts/stack_size:256
> [ 0.000000] (0:@) Check a safety property
> [ 0.000000] (2:client@HostB) Send 1!
> [ 0.000000] (3:client@HostC) Send 2!
#! ./tesh
-$ ${bindir:=.}/centralized --cfg=model-check:1
+$ ${bindir:=.}/centralized
> [Fafard:client:(2) 0.000000] [centralized/INFO] Ask the request
> [Boivin:client:(3) 0.000000] [centralized/INFO] Ask the request
> [TeX:client:(4) 0.000000] [centralized/INFO] Ask the request
/******************************************************************************/
/* Run :
- /usr/bin/time -f "clock:%e user:%U sys:%S swapped:%W exitval:%x max:%Mk" "$@" ../../../smpi_script/bin/smpirun -hostfile hostfile_bugged1_liveness -platform ../../platforms/cluster.xml --cfg=model-check:1 --cfg=contexts/factory:ucontext --cfg=model-check/reduction:none --cfg=model-check/property:promela_bugged1_liveness --cfg=smpi/send_is_detached_thres:0 --cfg=contexts/stack_size:128 --cfg=model-check/visited:100000 --cfg=model-check/max_depth:100000 ./bugged1_liveness */
+ /usr/bin/time -f "clock:%e user:%U sys:%S swapped:%W exitval:%x max:%Mk" "$@" ../../../smpi_script/bin/smpirun -hostfile hostfile_bugged1_liveness -platform ../../platforms/cluster.xml --cfg=contexts/factory:ucontext --cfg=model-check/reduction:none --cfg=model-check/property:promela_bugged1_liveness --cfg=smpi/send_is_detached_thres:0 --cfg=contexts/stack_size:128 --cfg=model-check/visited:100000 --cfg=model-check/max_depth:100000 ./bugged1_liveness */
#include <stdio.h>
#include <mpi.h>
#! ./tesh
! timeout 60
-$ ../../../smpi_script/bin/smpirun -wrapper ${bindir:=.}/../../../bin/simgrid-mc -hostfile ${srcdir:=.}/hostfile_non_deterministic -platform ${srcdir:=.}/../../platforms/cluster.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 --cfg=model-check/communications_determinism:1 --cfg=smpi/send_is_detached_thres:0 --cfg=smpi/running_power:1e9 ./smpi_non_deterministic
+$ ../../../smpi_script/bin/smpirun -wrapper ${bindir:=.}/../../../bin/simgrid-mc -hostfile ${srcdir:=.}/hostfile_non_deterministic -platform ${srcdir:=.}/../../platforms/cluster.xml --log=xbt_cfg.thresh:warning --cfg=model-check/communications_determinism:1 --cfg=smpi/send_is_detached_thres:0 --cfg=smpi/running_power:1e9 ./smpi_non_deterministic
> [0.000000] [mc_global/INFO] Check communication determinism
> [0.000000] [mc_comm_determinism/INFO] The communications pattern of the process 1 is different! (Different communication : 1)
> [0.000000] [mc_comm_determinism/INFO] ****************************************************
-/* ../../../smpi_script/bin/smpirun -hostfile hostfile_send_deterministic -platform ../../platforms/cluster.xml -np 3 --cfg=model-check:1 --cfg=smpi/send_is_detached_thres:0 gdb\ --args\ ./send_deterministic */
+/* ../../../smpi_script/bin/smpirun -hostfile hostfile_send_deterministic -platform ../../platforms/cluster.xml -np 3 --cfg=smpi/send_is_detached_thres:0 gdb\ --args\ ./send_deterministic */
/* Copyright (c) 2009-2015. The SimGrid Team.
* All rights reserved. */
#! ./tesh
! timeout 60
-$ ../../../smpi_script/bin/smpirun -wrapper "${bindir:=.}/../../../bin/simgrid-mc" --log=xbt_cfg.thresh:warning -hostfile ${srcdir:=.}/hostfile_only_send_deterministic -platform ${srcdir:=.}/../../platforms/cluster.xml --cfg=model-check:1 --cfg=model-check/communications_determinism:1 --cfg=smpi/send_is_detached_thres:0 --cfg=smpi/running_power:1e9 ./smpi_only_send_deterministic
+$ ../../../smpi_script/bin/smpirun -wrapper "${bindir:=.}/../../../bin/simgrid-mc" --log=xbt_cfg.thresh:warning -hostfile ${srcdir:=.}/hostfile_only_send_deterministic -platform ${srcdir:=.}/../../platforms/cluster.xml --cfg=model-check/communications_determinism:1 --cfg=smpi/send_is_detached_thres:0 --cfg=smpi/running_power:1e9 ./smpi_only_send_deterministic
> [0.000000] [mc_comm_determinism/INFO] Check communication determinism
> [0.000000] [mc_global/INFO] ******************************************************
> [0.000000] [mc_global/INFO] **** Only-send-deterministic communication pattern ****
{
if (_sg_cfg_init_status && !(_sg_do_model_check || MC_record_path)) {
xbt_die
- ("You are specifying a value to enable/disable timeout for wait requests after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+ ("You are specifying a value to enable/disable timeout for wait requests after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
}
_sg_mc_timeout = xbt_cfg_get_boolean(_sg_cfg_set, name);
}
{
if (_sg_cfg_init_status && !_sg_do_model_check) {
xbt_die
- ("You are specifying a reduction strategy after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+ ("You are specifying a reduction strategy after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
}
char *val = xbt_cfg_get_string(_sg_cfg_set, name);
if (!strcasecmp(val, "none")) {
{
if (_sg_cfg_init_status && !_sg_do_model_check) {
xbt_die
- ("You are specifying a checkpointing value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+ ("You are specifying a checkpointing value after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
}
_sg_mc_checkpoint = xbt_cfg_get_int(_sg_cfg_set, name);
}
void _mc_cfg_cb_sparse_checkpoint(const char *name, int pos) {
if (_sg_cfg_init_status && !_sg_do_model_check) {
- xbt_die("You are specifying a checkpointing value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+ xbt_die("You are specifying a checkpointing value after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
}
_sg_mc_sparse_checkpoint = xbt_cfg_get_boolean(_sg_cfg_set, name);
}
{
if (_sg_cfg_init_status && !_sg_do_model_check) {
xbt_die
- ("You are specifying a property after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+ ("You are specifying a property after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
}
_sg_mc_property_file = xbt_cfg_get_string(_sg_cfg_set, name);
}
{
if (_sg_cfg_init_status && !_sg_do_model_check) {
xbt_die
- ("You are specifying a value to enable/disable the use of global hash to speedup state comparaison, but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+ ("You are specifying a value to enable/disable the use of global hash to speedup state comparaison, but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
}
_sg_mc_hash = xbt_cfg_get_boolean(_sg_cfg_set, name);
}
{
if (_sg_cfg_init_status && !_sg_do_model_check) {
xbt_die
- ("You are specifying a value to enable/disable the use of FD snapshoting, but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+ ("You are specifying a value to enable/disable the use of FD snapshoting, but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
}
_sg_mc_snapshot_fds = xbt_cfg_get_boolean(_sg_cfg_set, name);
}
{
if (_sg_cfg_init_status && !_sg_do_model_check) {
xbt_die
- ("You are specifying a max depth value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+ ("You are specifying a max depth value after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
}
_sg_mc_max_depth = xbt_cfg_get_int(_sg_cfg_set, name);
}
{
if (_sg_cfg_init_status && !_sg_do_model_check) {
xbt_die
- ("You are specifying a number of stored visited states after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+ ("You are specifying a number of stored visited states after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
}
_sg_mc_visited = xbt_cfg_get_int(_sg_cfg_set, name);
}
{
if (_sg_cfg_init_status && !_sg_do_model_check) {
xbt_die
- ("You are specifying a file name for a dot output of graph state after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+ ("You are specifying a file name for a dot output of graph state after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
}
_sg_mc_dot_output_file = xbt_cfg_get_string(_sg_cfg_set, name);
}
{
if (_sg_cfg_init_status && !_sg_do_model_check) {
xbt_die
- ("You are specifying a value to enable/disable the detection of determinism in the communications schemes after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+ ("You are specifying a value to enable/disable the detection of determinism in the communications schemes after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
}
_sg_mc_comms_determinism = xbt_cfg_get_boolean(_sg_cfg_set, name);
}
{
if (_sg_cfg_init_status && !_sg_do_model_check) {
xbt_die
- ("You are specifying a value to enable/disable the detection of send-determinism in the communications schemes after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+ ("You are specifying a value to enable/disable the detection of send-determinism in the communications schemes after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
}
_sg_mc_send_determinism = xbt_cfg_get_boolean(_sg_cfg_set, name);
}
{
if (_sg_cfg_init_status && !_sg_do_model_check) {
xbt_die
- ("You are specifying a value to enable/disable the detection of non progressive cycles after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+ ("You are specifying a value to enable/disable the detection of non progressive cycles after the initialization (through MSG_config?), but model-checking was not activated at config time (through bu the program was not runned under the model-checker (with simgrid-mc)). This won't work, sorry.");
}
_sg_mc_termination = xbt_cfg_get_boolean(_sg_cfg_set, name);
}
int main(int argc, char** argv)
{
+ _sg_do_model_check = 1;
+
// We need to keep the original parameters in order to pass them to the
// model-checked process:
int argc_copy = argc;
MC_record_path = xbt_cfg_get_string(_sg_cfg_set, name);
}
-static void _sg_cfg_cb_model_check(const char *name, int pos)
-{
-#ifdef HAVE_MC
- _sg_do_model_check = xbt_cfg_get_boolean(_sg_cfg_set, name);
-#else
- if (xbt_cfg_get_boolean(_sg_cfg_set, name)) {
- xbt_die("You tried to activate the model-checking from the command line, but it was not compiled in. Change your settings in cmake, recompile and try again");
- }
-#endif
-}
-
static void _sg_cfg_cb_model_check_record(const char *name, int pos)
{
#ifdef HAVE_MC
xbt_cfgelm_string, 0, 1, _sg_cfg_cb_model_check_replay, NULL);
#ifdef HAVE_MC
- /* do model-checking */
- xbt_cfg_register(&_sg_cfg_set, "model-check",
- "Verify the system through model-checking instead of simulating it (EXPERIMENTAL)",
- xbt_cfgelm_boolean, 1, 1, _sg_cfg_cb_model_check, NULL);
- xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check", "no");
-
/* do model-checking-record */
xbt_cfg_register(&_sg_cfg_set, "model-check/record",
"Record the model-checking paths",
#include "mc/mc_protocol.h"
#include "mc/mc_client.h"
#endif
+
+#ifdef HAVE_MC
+#include <stdlib.h>
+#include "mc/mc_protocol.h"
+#endif
+
#include "mc/mc_record.h"
#ifdef HAVE_SMPI
*/
void SIMIX_global_init(int *argc, char **argv)
{
+#ifdef HAVE_MC
+ _sg_do_model_check = getenv(MC_ENV_VARIABLE) != NULL;
+#endif
+
s_smx_process_t proc;
if (!simix_global) {
#!/usr/bin/env tesh
! expect return 1
! output ignore
-$ ${bindir:=.}/../../bin/simgrid-mc ${bindir:=.}/mutex_handling --cfg=model-check:1 ../../examples/platforms/platform.xml mutex_handling.xml
+$ ${bindir:=.}/../../bin/simgrid-mc ${bindir:=.}/mutex_handling ../../examples/platforms/platform.xml mutex_handling.xml
#!/usr/bin/env tesh
! expect return 1
! output ignore
-$ ${bindir:=.}/../../bin/simgrid-mc ${bindir:=.}/no_mutex_handling --cfg=model-check:1 ../../examples/platforms/platform.xml mutex_handling.xml
+$ ${bindir:=.}/../../bin/simgrid-mc ${bindir:=.}/no_mutex_handling ../../examples/platforms/platform.xml mutex_handling.xml
#!/usr/bin/env tesh
! expect return 1
-$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random_bug ${srcdir:=.}/../../../examples/platforms/small_platform.xml ${srcdir:=.}/random_bug.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=model-check:1 --cfg=model-check/record:1
+$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random_bug ${srcdir:=.}/../../../examples/platforms/small_platform.xml ${srcdir:=.}/random_bug.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=model-check/record:1
> [ 0.000000] (0:@) Check a safety property
> [ 0.000000] (0:@) **************************
> [ 0.000000] (0:@) *** PROPERTY NOT VALID ***
! expect return 3
! output display
-$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml -np 3 --log=xbt_cfg.thresh:warning --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/any_src-can-deadlock10 --log=smpi_coll.thresh:error
+$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml -np 3 --log=xbt_cfg.thresh:warning --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/any_src-can-deadlock10 --log=smpi_coll.thresh:error
> [0.000000] [mc_safety/INFO] Check a safety property
> (0) is alive on Tremblay
> (1) is alive on Jupiter
! expect return 3
! output display
-$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml -np 3 --log=xbt_cfg.thresh:warning --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/any_src-can-deadlock4 --log=smpi_coll.thresh:error
+$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml -np 3 --log=xbt_cfg.thresh:warning --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/any_src-can-deadlock4 --log=smpi_coll.thresh:error
> [0.000000] [mc_safety/INFO] Check a safety property
> (0) is alive on Tremblay
> (1) is alive on Jupiter
! expect return 3
! output display
-$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --log=xbt_cfg.thresh:warning --cfg=smpi/coll_selector:mpich ${bindir:=.}/any_src-can-deadlock5 --log=smpi_coll.thresh:error
+$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml -np 3 --cfg=smpi/running_power:1e9 --log=xbt_cfg.thresh:warning --cfg=smpi/coll_selector:mpich ${bindir:=.}/any_src-can-deadlock5 --log=smpi_coll.thresh:error
> [0.000000] [mc_safety/INFO] Check a safety property
> (0) is alive on Tremblay
> (1) is alive on Jupiter
! expect return 3
! output display
-$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/any_src-can-deadlock6 --log=smpi_coll.thresh:error
+$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/any_src-can-deadlock6 --log=smpi_coll.thresh:error
> [0.000000] [mc_safety/INFO] Check a safety property
> (0) is alive on Tremblay
> (1) is alive on Jupiter
! expect return 3
! output display
-$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/any_src-wait-deadlock --log=smpi_coll.thresh:error
+$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/any_src-wait-deadlock --log=smpi_coll.thresh:error
> [0.000000] [mc_safety/INFO] Check a safety property
> (0) is alive on Tremblay
> (1) is alive on Jupiter
! expect return 3
! output display
-$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/any_src-waitall-deadlock2 --log=smpi_coll.thresh:error
+$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/any_src-waitall-deadlock2 --log=smpi_coll.thresh:error
> [0.000000] [mc_safety/INFO] Check a safety property
> (0) is alive on Tremblay
> (1) is alive on Jupiter
! expect return 3
! output display
-$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/any_src-waitall-deadlock3 --log=smpi_coll.thresh:error
+$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/any_src-waitall-deadlock3 --log=smpi_coll.thresh:error
> [0.000000] [mc_safety/INFO] Check a safety property
> (0) is alive on Tremblay
> (1) is alive on Jupiter
! expect return 3
! output display
-$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/any_src-waitany-deadlock --log=smpi_coll.thresh:error
+$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/any_src-waitany-deadlock --log=smpi_coll.thresh:error
> [0.000000] [mc_safety/INFO] Check a safety property
> (0) is alive on Tremblay
> (1) is alive on Jupiter
! expect return 3
! output display
-$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/any_src-waitany-deadlock2 --log=smpi_coll.thresh:error
+$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/any_src-waitany-deadlock2 --log=smpi_coll.thresh:error
> [0.000000] [mc_safety/INFO] Check a safety property
> (0) is alive on Tremblay
> (1) is alive on Jupiter
! expect return 3
! output display
-$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" --log=xbt_cfg.thresh:warning -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/basic-deadlock-comm_create --log=smpi_coll.thresh:error
+$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" --log=xbt_cfg.thresh:warning -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml -np 3 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/basic-deadlock-comm_create --log=smpi_coll.thresh:error
> [0.000000] [mc_safety/INFO] Check a safety property
> (0) is alive on Tremblay
> (1) is alive on Jupiter
! expect return 3
! output display
-$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/basic-deadlock-comm_dup --log=smpi_coll.thresh:error
+$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/basic-deadlock-comm_dup --log=smpi_coll.thresh:error
> [0.000000] [mc_safety/INFO] Check a safety property
> (0) is alive on Tremblay
> (1) is alive on Jupiter
! expect return 3
! output display
-$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/basic-deadlock-comm_split --log=smpi_coll.thresh:error
+$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/basic-deadlock-comm_split --log=smpi_coll.thresh:error
> [0.000000] [mc_safety/INFO] Check a safety property
> (0) is alive on Tremblay
> (1) is alive on Jupiter
! expect return 3
! output display
-$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/basic-deadlock --log=smpi_coll.thresh:error
+$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/basic-deadlock --log=smpi_coll.thresh:error
> [0.000000] [mc_safety/INFO] Check a safety property
> (0) is alive on Tremblay
> (1) is alive on Jupiter
! expect return 3
! output display
-$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/bcast-deadlock --log=smpi_coll.thresh:error
+$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/bcast-deadlock --log=smpi_coll.thresh:error
> [0.000000] [mc_safety/INFO] Check a safety property
> (0) is alive on Tremblay
> (1) is alive on Jupiter
! expect return 3
! output display
-$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/collective-misorder-allreduce --log=smpi_coll.thresh:error
+$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/collective-misorder-allreduce --log=smpi_coll.thresh:error
> [0.000000] [mc_safety/INFO] Check a safety property
> (0) is alive on Tremblay
> (1) is alive on Jupiter
! expect return 3
! output display
-$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/collective-misorder --log=smpi_coll.thresh:error
+$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/collective-misorder --log=smpi_coll.thresh:error
> [0.000000] [mc_safety/INFO] Check a safety property
> (0) is alive on Tremblay
> (1) is alive on Jupiter
! expect return 3
! output display
-$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/complex-deadlock --log=smpi_coll.thresh:error
+$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/complex-deadlock --log=smpi_coll.thresh:error
> [0.000000] [mc_safety/INFO] Check a safety property
> (0) is alive on Tremblay
> (1) is alive on Jupiter
! expect return 3
! output display
-$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/deadlock-config --log=smpi_coll.thresh:error
+$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/deadlock-config --log=smpi_coll.thresh:error
> [0.000000] [mc_safety/INFO] Check a safety property
> WARNING: This test depends on the MPI's eager limit. Set it appropriately.
> Initializing (0 of 3)
! expect return 3
! output display
-$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/finalize-deadlock --log=smpi_coll.thresh:error
+$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/finalize-deadlock --log=smpi_coll.thresh:error
> [0.000000] [mc_safety/INFO] Check a safety property
> (0) is alive on Tremblay
> (1) is alive on Jupiter
! expect return 3
! output display
-$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/irecv-deadlock --log=smpi_coll.thresh:error
+$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/irecv-deadlock --log=smpi_coll.thresh:error
> [0.000000] [mc_safety/INFO] Check a safety property
> (0) is alive on Tremblay
> (1) is alive on Jupiter
! timeout 5
! expect return 0
! output display
-$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/no-error --log=smpi_coll.thresh:error
+$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/no-error --log=smpi_coll.thresh:error
> [0.000000] [mc_safety/INFO] Check a safety property
> (0) is alive on Tremblay
> (1) is alive on Jupiter
! timeout 5
! expect return 0
! output display
-$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/no-error2 --log=smpi_coll.thresh:error
+$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/no-error2 --log=smpi_coll.thresh:error
> [0.000000] [mc_safety/INFO] Check a safety property
> (0) is alive on Tremblay
> (1) is alive on Jupiter
! timeout 5
! expect return 0
! output display
-$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/no-error3-any_src --log=smpi_coll.thresh:error
+$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/no-error3-any_src --log=smpi_coll.thresh:error
> [0.000000] [mc_safety/INFO] Check a safety property
> (0) is alive on Tremblay
> (1) is alive on Jupiter
! timeout 5
! expect return 0
! output display
-$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/no-error3 --log=smpi_coll.thresh:error
+$ ${bindir:=.}/../../../../bin/smpirun -wrapper "${bindir:=.}/../../../../bin/simgrid-mc" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/no-error3 --log=smpi_coll.thresh:error
> [0.000000] [mc_safety/INFO] Check a safety property
> (0) is alive on Tremblay
> (1) is alive on Jupiter
