xbt_cfgelm_int, 1, 1, _mc_cfg_cb_checkpoint, NULL);
xbt_cfg_setdefault_int(_sg_cfg_set, "model-check/checkpoint", 0);
+ /* do stateful model-checking */
+ xbt_cfg_register(&_sg_cfg_set, "model-check/sparse-checkpoint",
+ "Use sparse per-page snapshots.",
+ xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_sparse_checkpoint, NULL);
+ xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/sparse-checkpoint", "no");
+
+ /* do stateful model-checking */
+ xbt_cfg_register(&_sg_cfg_set, "model-check/soft-dirty",
+ "Use sparse per-page snapshots.",
+ xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_soft_dirty, NULL);
+ xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/soft-dirty", "yes");
+
/* do liveness model-checking */
xbt_cfg_register(&_sg_cfg_set, "model-check/property",
"Specify the name of the file containing the property. It must be the result of the ltl2ba program.",