From: Marion Guthmuller Date: Thu, 19 Sep 2013 13:22:08 +0000 (+0200) Subject: model-checker : --cfg=model-check/checkpoint is an int, not a boolean X-Git-Tag: v3_9_90~104^2~37 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/9bfb3e8563dcd70af5abdd1f96f20ac825d815dd model-checker : --cfg=model-check/checkpoint is an int, not a boolean --- diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index cbd6cc8b87..613cf30324 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -53,7 +53,7 @@ void _mc_cfg_cb_checkpoint(const char *name, int pos) { if (_sg_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."); } - _sg_mc_checkpoint = xbt_cfg_get_boolean(_sg_cfg_set, name); + _sg_mc_checkpoint = xbt_cfg_get_int(_sg_cfg_set, name); } void _mc_cfg_cb_property(const char *name, int pos) { if (_sg_init_status && !_sg_do_model_check) { diff --git a/src/simgrid/sg_config.c b/src/simgrid/sg_config.c index f61b9e392b..596e2616cc 100644 --- a/src/simgrid/sg_config.c +++ b/src/simgrid/sg_config.c @@ -567,13 +567,12 @@ void sg_config_init(int *argc, char **argv) xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check", default_value); /* do stateful model-checking */ - default_value = (char*)"off"; xbt_cfg_register(&_sg_cfg_set, "model-check/checkpoint", - "Specify the amount of steps between checkpoints during stateful model-checking (default: off => stateless verification). " + "Specify the amount of steps between checkpoints during stateful model-checking (default: 0 => stateless verification). " "If value=on, one checkpoint is saved for each step => faster verification, but huge memory consumption; higher values are good compromises between speed and memory consumption.", - xbt_cfgelm_boolean, NULL, 0, 1, + xbt_cfgelm_int, NULL, 0, 1, _mc_cfg_cb_checkpoint, NULL); - xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/checkpoint", default_value); + xbt_cfg_setdefault_int(_sg_cfg_set, "model-check/checkpoint", 0); /* do liveness model-checking */ xbt_cfg_register(&_sg_cfg_set, "model-check/property",