Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : cleanups in comments
[simgrid.git] / src / mc / mc_global.c
index 4dfb227..72b9532 100644 (file)
@@ -37,7 +37,6 @@ void _mc_cfg_cb_reduce(const char *name, int pos) {
   } else {
     xbt_die("configuration option %s can only take 'none' or 'dpor' as a value",name);
   }
-  xbt_cfg_set_int(_surf_cfg_set,"model-check",1);
 }
 
 void _mc_cfg_cb_checkpoint(const char *name, int pos) {
@@ -45,14 +44,12 @@ void _mc_cfg_cb_checkpoint(const char *name, int pos) {
     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.");
   }
   _surf_mc_checkpoint = xbt_cfg_get_int(_surf_cfg_set, name);
-  xbt_cfg_set_int(_surf_cfg_set,"model-check",1);
 }
 void _mc_cfg_cb_property(const char *name, int pos) {
   if (_surf_init_status && !_surf_do_model_check) {
     xbt_die("You are specifying a property 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.");
   }
   _surf_mc_property_file= xbt_cfg_get_string(_surf_cfg_set, name);
-  xbt_cfg_set_int(_surf_cfg_set,"model-check",1);
 }
 
 void _mc_cfg_cb_timeout(const char *name, int pos) {
@@ -60,7 +57,6 @@ void _mc_cfg_cb_timeout(const char *name, int pos) {
     xbt_die("You are specifying a value to enable/disable timeout for wait requests 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.");
   }
   _surf_mc_timeout= xbt_cfg_get_int(_surf_cfg_set, name);
-  xbt_cfg_set_int(_surf_cfg_set,"model-check",1);
 }
 
 void _mc_cfg_cb_max_depth(const char *name, int pos) {
@@ -68,15 +64,13 @@ void _mc_cfg_cb_max_depth(const char *name, int pos) {
     xbt_die("You are specifying a max depth 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.");
   }
   _surf_mc_max_depth= xbt_cfg_get_int(_surf_cfg_set, name);
-  xbt_cfg_set_int(_surf_cfg_set,"model-check",1);
 }
 
-void _mc_cfg_cb_stateful(const char *name, int pos) {
+void _mc_cfg_cb_visited(const char *name, int pos) {
   if (_surf_init_status && !_surf_do_model_check) {
-    xbt_die("You are trying to change stateful mode 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.");
+    xbt_die("You are specifying a number of stored visited states 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.");
   }
-  _surf_mc_stateful= xbt_cfg_get_int(_surf_cfg_set, name);
-  xbt_cfg_set_int(_surf_cfg_set,"model-check",1);
+  _surf_mc_visited= xbt_cfg_get_int(_surf_cfg_set, name);
 }
 
 
@@ -221,7 +215,7 @@ void MC_modelcheck_safety(void)
 
   MC_UNSET_RAW_MEM;
 
-  if(_surf_mc_stateful > 0){
+  if(_surf_mc_visited > 0){
     MC_init();
   }else{
     MC_init_memory_map_info();
@@ -235,7 +229,6 @@ void MC_modelcheck_safety(void)
   /* Save the initial state */
   initial_state_safety = xbt_new0(s_mc_global_t, 1);
   initial_state_safety->snapshot = MC_take_snapshot();
-  //MC_take_snapshot(initial_snapshot);
   MC_UNSET_RAW_MEM;
 
   if(raw_mem_set)