Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : --cfg=model-check/checkpoint is an int, not a boolean
authorMarion Guthmuller <marion.guthmuller@loria.fr>
Thu, 19 Sep 2013 13:22:08 +0000 (15:22 +0200)
committerMarion Guthmuller <marion.guthmuller@loria.fr>
Sat, 21 Sep 2013 20:50:29 +0000 (22:50 +0200)
src/mc/mc_global.c
src/simgrid/sg_config.c

index cbd6cc8..613cf30 100644 (file)
@@ -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) {
index f61b9e3..596e261 100644 (file)
@@ -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",