From f81d3fa9690297fe0953c37d368201702b6c9bbb Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Tue, 17 Jun 2014 14:42:38 +0200 Subject: [PATCH 1/1] [mc] Add option --cfg=model-check/sparse-checkpoint:yes to enable per page snapshot --- src/mc/mc_global.c | 2 +- src/simgrid/sg_config.c | 6 ++++++ 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index e909cc6042..b22364d7c5 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -73,7 +73,7 @@ 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."); } - _sg_mc_sparse_checkpoint = xbt_cfg_get_int(_sg_cfg_set, name); + _sg_mc_sparse_checkpoint = xbt_cfg_get_boolean(_sg_cfg_set, name); } void _mc_cfg_cb_property(const char *name, int pos) diff --git a/src/simgrid/sg_config.c b/src/simgrid/sg_config.c index 8e456dcc29..d9dea55c65 100644 --- a/src/simgrid/sg_config.c +++ b/src/simgrid/sg_config.c @@ -602,6 +602,12 @@ void sg_config_init(int *argc, char **argv) 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 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.", -- 2.20.1