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) {
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",