model-checker : minor fix

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

diff --git a/src/simgrid/sg_config.c b/src/simgrid/sg_config.c
index 5b8a406..7a1ceb4 100644 (file)
--- a/src/simgrid/sg_config.c
+++ b/src/simgrid/sg_config.c
@@ -55,6 +55,9 @@ static void sg_config_cmd_line(int *argc, char **argv)
 
       xbt_cfg_set_parse(_sg_cfg_set, opt);
       XBT_DEBUG("Did apply '%s' as config setting", opt);
+    } else if (!strcmp(argv[i], "--version")) {
+      printf("%s\n", SIMGRID_VERSION_STRING);
+      shall_exit = 1;
     } else if (!strcmp(argv[i], "--cfg-help") || !strcmp(argv[i], "--help")) {
       printf
           ("Description of the configuration accepted by this simulator:\n");
@@ -71,6 +74,8 @@ static void sg_config_cmd_line(int *argc, char **argv)
 #endif
 "\n"
 "You can also use --help-logs and --help-log-categories to see the details of logging output.\n"
+"\n"
+"You can also use --version to get SimGrid version information.\n"
 "\n"
         );
       shall_exit = 1;
@@ -559,7 +564,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);
 
@@ -569,6 +574,12 @@ 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 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");
+
     /* 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)",
@@ -611,12 +622,12 @@ void sg_config_init(int *argc, char **argv)
             "Context factory to use in SIMIX. Possible values: thread");
     const char *dflt_ctx_fact = "thread";
 #ifdef CONTEXT_UCONTEXT
-    strcat(description, ", ucontext");
     dflt_ctx_fact = "ucontext";
+    strcat(strcat(description, ", "), dflt_ctx_fact);
 #endif
 #ifdef HAVE_RAWCTX
-    strcat(description, ", raw");
     dflt_ctx_fact = "raw";
+    strcat(strcat(description, ", "), dflt_ctx_fact);
 #endif
     strcat(description, ".");
     xbt_cfg_register(&_sg_cfg_set, "contexts/factory", description,
@@ -628,6 +639,8 @@ void sg_config_init(int *argc, char **argv)
                      "Stack size of contexts in Kib",
                      xbt_cfgelm_int, 1, 1, _sg_cfg_cb_context_stack_size, NULL);
     xbt_cfg_setdefault_int(_sg_cfg_set, "contexts/stack_size", 128);
+    /* No, it was not set yet (the above setdefault() changed this to 1). */
+    smx_context_stack_size_was_set = 0;
 
     /* number of parallel threads for user processes */
     xbt_cfg_register(&_sg_cfg_set, "contexts/nthreads",
@@ -696,7 +709,7 @@ void sg_config_init(int *argc, char **argv)
     xbt_cfg_setdefault_boolean(_sg_cfg_set, "smpi/use_shared_malloc", "yes");
 
     xbt_cfg_register(&_sg_cfg_set, "smpi/cpu_threshold",
-                     "Minimal computation time (in seconds) not discarded.",
+                     "Minimal computation time (in seconds) not discarded, or -1 for infinity.",
                      xbt_cfgelm_double, 1, 1, NULL, NULL);
     xbt_cfg_setdefault_double(_sg_cfg_set, "smpi/cpu_threshold", 1e-6);