Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : use separate configuration flags for comm determinism and send determ...
[simgrid.git] / src / simgrid / sg_config.c
index 4886b39..dafa406 100644 (file)
@@ -574,12 +574,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 determinism model-checking */
-        xbt_cfg_register(&_sg_cfg_set, "model-check/communications_determinism",
+    /* 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)",