X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/ed06d5e442e2b600bc6093a6dcf9e98ab0cab785..c8c284176e4f5ae35bf26ad48515f4b029866ef2:/src/mc/mc_global.c

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index c66e9c9285..0d4543dd6d 100644
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -24,140 +24,8 @@ XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
                                 "Logging specific to MC (global)");
 
-/* Configuration support */
-e_mc_reduce_t mc_reduce_kind = e_mc_reduce_unset;
-
-int _sg_do_model_check = 0;
-int _sg_mc_checkpoint = 0;
-int _sg_mc_sparse_checkpoint = 0;
-int _sg_mc_soft_dirty = 0;
-char *_sg_mc_property_file = NULL;
-int _sg_mc_timeout = 0;
-int _sg_mc_hash = 0;
-int _sg_mc_max_depth = 1000;
-int _sg_mc_visited = 0;
-char *_sg_mc_dot_output_file = NULL;
-int _sg_mc_comms_determinism = 0;
-int _sg_mc_send_determinism = 0;
-int _sg_mc_safety = 0;
-int _sg_mc_liveness = 0;
-
 int user_max_depth_reached = 0;
 
-void _mc_cfg_cb_reduce(const char *name, int pos)
-{
-  if (_sg_cfg_init_status && !_sg_do_model_check) {
-    xbt_die
-        ("You are specifying a reduction strategy 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.");
-  }
-  char *val = xbt_cfg_get_string(_sg_cfg_set, name);
-  if (!strcasecmp(val, "none")) {
-    mc_reduce_kind = e_mc_reduce_none;
-  } else if (!strcasecmp(val, "dpor")) {
-    mc_reduce_kind = e_mc_reduce_dpor;
-  } else {
-    xbt_die("configuration option %s can only take 'none' or 'dpor' as a value",
-            name);
-  }
-}
-
-void _mc_cfg_cb_checkpoint(const char *name, int pos)
-{
-  if (_sg_cfg_init_status && !_sg_do_model_check) {
-    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.");
-  }
-  _sg_mc_checkpoint = xbt_cfg_get_int(_sg_cfg_set, name);
-}
-
-void _mc_cfg_cb_sparse_checkpoint(const char *name, int pos) {
-  if (_sg_cfg_init_status && !_sg_do_model_check) {
-    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.");
-  }
-  _sg_mc_sparse_checkpoint = xbt_cfg_get_boolean(_sg_cfg_set, name);
-}
-
-void _mc_cfg_cb_soft_dirty(const char *name, int pos) {
-  if (_sg_cfg_init_status && !_sg_do_model_check) {
-    xbt_die("You are specifying a soft dirty 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.");
-  }
-  _sg_mc_soft_dirty = xbt_cfg_get_boolean(_sg_cfg_set, name);
-}
-
-void _mc_cfg_cb_property(const char *name, int pos)
-{
-  if (_sg_cfg_init_status && !_sg_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.");
-  }
-  _sg_mc_property_file = xbt_cfg_get_string(_sg_cfg_set, name);
-}
-
-void _mc_cfg_cb_timeout(const char *name, int pos)
-{
-  if (_sg_cfg_init_status && !_sg_do_model_check) {
-    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.");
-  }
-  _sg_mc_timeout = xbt_cfg_get_boolean(_sg_cfg_set, name);
-}
-
-void _mc_cfg_cb_hash(const char *name, int pos)
-{
-  if (_sg_cfg_init_status && !_sg_do_model_check) {
-    xbt_die
-        ("You are specifying a value to enable/disable the use of global hash to speedup state comparaison, but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
-  }
-  _sg_mc_hash = xbt_cfg_get_boolean(_sg_cfg_set, name);
-}
-
-void _mc_cfg_cb_max_depth(const char *name, int pos)
-{
-  if (_sg_cfg_init_status && !_sg_do_model_check) {
-    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.");
-  }
-  _sg_mc_max_depth = xbt_cfg_get_int(_sg_cfg_set, name);
-}
-
-void _mc_cfg_cb_visited(const char *name, int pos)
-{
-  if (_sg_cfg_init_status && !_sg_do_model_check) {
-    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.");
-  }
-  _sg_mc_visited = xbt_cfg_get_int(_sg_cfg_set, name);
-}
-
-void _mc_cfg_cb_dot_output(const char *name, int pos)
-{
-  if (_sg_cfg_init_status && !_sg_do_model_check) {
-    xbt_die
-        ("You are specifying a file name for a dot output of graph state 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.");
-  }
-  _sg_mc_dot_output_file = xbt_cfg_get_string(_sg_cfg_set, name);
-}
-
-void _mc_cfg_cb_comms_determinism(const char *name, int pos)
-{
-  if (_sg_cfg_init_status && !_sg_do_model_check) {
-    xbt_die
-        ("You are specifying a value to enable/disable the detection of determinism in the communications schemes 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.");
-  }
-  _sg_mc_comms_determinism = xbt_cfg_get_boolean(_sg_cfg_set, name);
-  mc_reduce_kind = e_mc_reduce_none;
-}
-
-void _mc_cfg_cb_send_determinism(const char *name, int pos)
-{
-  if (_sg_cfg_init_status && !_sg_do_model_check) {
-    xbt_die
-        ("You are specifying a value to enable/disable the detection of send-determinism in the communications schemes 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.");
-  }
-  _sg_mc_send_determinism = xbt_cfg_get_boolean(_sg_cfg_set, name);
-  mc_reduce_kind = e_mc_reduce_none;
-}
-
 /* MC global data structures */
 mc_state_t mc_current_state = NULL;
 char mc_replay_mode = FALSE;
@@ -478,7 +346,7 @@ void MC_wait_for_requests(void)
 
   while (!xbt_dynar_is_empty(simix_global->process_to_run)) {
     SIMIX_process_runall();
-    xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
+      xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
       req = &process->simcall;
       if (req->call != SIMCALL_NONE && !MC_request_is_visible(req))
         SIMIX_simcall_enter(req, 0);