Merge branch 'mc' into mc++

[simgrid.git] / src / simgrid / sg_config.c

diff --git a/src/simgrid/sg_config.c b/src/simgrid/sg_config.c
index 6deb481af343d396abdcabdbbcae31ca2bd55ded..4ebfb8ee45c6ca236991ca779310d1769114a524 100644 (file)
--- a/src/simgrid/sg_config.c
+++ b/src/simgrid/sg_config.c
@@ -67,6 +67,7 @@ static void sg_config_cmd_line(int *argc, char **argv)
 "Each of these configurations can be used by adding\n"
 "    --cfg=<option name>:<option value>\n"
 "to the command line.\n"
+"\n"
 "You can also use --help-models to see the details of all models known by this simulator.\n"
 #ifdef HAVE_TRACING
 "\n"
@@ -579,7 +580,7 @@ void sg_config_init(int *argc, char **argv)
     /* do stateful model-checking */
     xbt_cfg_register(&_sg_cfg_set, "model-check/checkpoint",
                      "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.",
+                     "If value=1, 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_int, 0, 1, _mc_cfg_cb_checkpoint, NULL);
     xbt_cfg_setdefault_int(_sg_cfg_set, "model-check/checkpoint", 0);
 
@@ -589,6 +590,18 @@ void sg_config_init(int *argc, char **argv)
                      xbt_cfgelm_string, 0, 1, _mc_cfg_cb_property, NULL);
     xbt_cfg_setdefault_string(_sg_cfg_set, "model-check/property", "");
 
+    /* do communications determinism model-checking */
+    xbt_cfg_register(&_sg_cfg_set, "model-check/communications_determinism",
+                     "Enable/disable the detection of determinism in the communications schemes",
+                     xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_comms_determinism, NULL);
+    xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/communications_determinism", "no");
+
+    /* do send determinism model-checking */
+    xbt_cfg_register(&_sg_cfg_set, "model-check/send_determinism",
+                     "Enable/disable the detection of send-determinism in the communications schemes",
+                     xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_send_determinism, NULL);
+    xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/send_determinism", "no");
+
     /* Specify the kind of model-checking reduction */
     xbt_cfg_register(&_sg_cfg_set, "model-check/reduction",
                      "Specify the kind of exploration reduction (either none or DPOR)",
@@ -601,6 +614,12 @@ void sg_config_init(int *argc, char **argv)
                      xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_timeout, NULL);
     xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/timeout", "no");
 
+    /* Enable/disable global hash computation with model-checking */
+    xbt_cfg_register(&_sg_cfg_set, "model-check/hash",
+                     "Enable/Disable state hash for state comparison",
+                     xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_hash, NULL);
+    xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/hash", "no");
+
     /* Set max depth exploration */
     xbt_cfg_register(&_sg_cfg_set, "model-check/max_depth",
                      "Specify the max depth of exploration (default : 1000)",