[mc] Remove user_max_depth which back up MC_cut() for now

This variables is not set since the cross-process mode anyway.

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index 389f638..02d1304 100644 (file)
--- a/src/mc/SafetyChecker.cpp
+++ b/src/mc/SafetyChecker.cpp
@@ -106,17 +106,18 @@ int SafetyChecker::run()
 
     XBT_DEBUG("**************************************************");
     XBT_DEBUG(
-      "Exploration depth=%zi (state=%p, num %d)(%u interleave, user_max_depth %d)",
+      "Exploration depth=%zi (state=%p, num %d)(%u interleave)",
       stack_.size(), state, state->num,
-      MC_state_interleave_size(state), user_max_depth_reached);
+      MC_state_interleave_size(state));
 
     /* Update statistics */
     mc_stats->visited_states++;
 
     /* If there are processes to interleave and the maximum depth has not been reached
        then perform one step of the exploration algorithm */
-    if (stack_.size() <= (std::size_t) _sg_mc_max_depth && !user_max_depth_reached
-        && (req = MC_state_get_request(state, &value)) && visited_state == nullptr) {
+    if (stack_.size() <= (std::size_t) _sg_mc_max_depth
+        && (req = MC_state_get_request(state, &value))
+        && visited_state == nullptr) {
 
       char* req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
       XBT_DEBUG("Execute: %s", req_str);
@@ -172,12 +173,9 @@ int SafetyChecker::run()
     } else {
 
       if (stack_.size() > (std::size_t) _sg_mc_max_depth
-          || user_max_depth_reached
           || visited_state != nullptr) {
 
-        if (user_max_depth_reached && visited_state == nullptr)
-          XBT_DEBUG("User max depth reached !");
-        else if (visited_state == nullptr)
+        if (visited_state == nullptr)
           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
         else
           XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);

diff --git a/src/mc/mc_client_api.cpp b/src/mc/mc_client_api.cpp
index cb8a785..d3fdc26 100644 (file)
--- a/src/mc/mc_client_api.cpp
+++ b/src/mc/mc_client_api.cpp
@@ -35,7 +35,6 @@ void MC_assert(int prop)
 void MC_cut(void)
 {
   // FIXME, We want to do this in the model-checker:
-  // user_max_depth_reached = 1;
   xbt_die("MC_cut() not implemented");
 }
 

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index cf23f62..ad03c3f 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -54,7 +54,6 @@ std::vector<double> processes_time;
 }
 
 #if HAVE_MC
-int user_max_depth_reached = 0;
 
 /* MC global data structures */
 simgrid::mc::State* mc_current_state = nullptr;

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 064926f..99da4d5 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -63,8 +63,6 @@ XBT_PRIVATE void MC_init_dot_output();
 
 XBT_PRIVATE extern FILE *dot_output;
 
-XBT_PRIVATE extern int user_max_depth_reached;
-
 XBT_PRIVATE void MC_show_deadlock(void);
 
 /****************************** Statistics ************************************/