- /*
- FIXME: this function is not setting model-check to it's default value because
- internally it calls to variable->cb_set that in this case is the function
- _surf_cfg_cb_model_check which sets it's value to 1 (instead of the default value 0)
- xbt_cfg_set_int(_surf_cfg_set, "model-check", default_value_int); */
+ /* do liveness model-checking */
+ default_value = xbt_strdup("");
+ xbt_cfg_register(&_surf_cfg_set, "model-check/property",
+ "Specify the name of the file containing the property. It must be the result of the ltl2ba program.",
+ xbt_cfgelm_string, &default_value, 0, 1,
+ _mc_cfg_cb_property, NULL);
+
+ /* Specify the kind of model-checking reduction */
+ default_value = xbt_strdup("unset");
+ xbt_cfg_register(&_surf_cfg_set, "model-check/reduction",
+ "Specify the kind of exploration reduction (either none or DPOR)",
+ xbt_cfgelm_string, &default_value, 0, 1,
+ _mc_cfg_cb_reduce, NULL);
+#endif