[mc] Move MC_replay_liveness() as a static function of mc_liveness.c

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index e92fcaf..dbd4677 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -223,73 +223,6 @@ void MC_replay(xbt_fifo_t stack)
   XBT_DEBUG("**** End Replay ****");
 }
 
-void MC_replay_liveness(xbt_fifo_t stack)
-{
-  xbt_fifo_item_t item;
-  simgrid::mc::Pair* pair = nullptr;
-  mc_state_t state = nullptr;
-  smx_simcall_t req = nullptr, saved_req = NULL;
-  int value, depth = 1;
-  char *req_str;
-
-  XBT_DEBUG("**** Begin Replay ****");
-
-  /* Intermediate backtracking */
-  if(_sg_mc_checkpoint > 0) {
-    item = xbt_fifo_get_first_item(stack);
-    pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
-    if(pair->graph_state->system_state){
-      simgrid::mc::restore_snapshot(pair->graph_state->system_state);
-      return;
-    }
-  }
-
-  /* Restore the initial state */
-  simgrid::mc::restore_snapshot(initial_global_state->snapshot);
-
-    /* Traverse the stack from the initial state and re-execute the transitions */
-    for (item = xbt_fifo_get_last_item(stack);
-         item != xbt_fifo_get_first_item(stack);
-         item = xbt_fifo_get_prev_item(item)) {
-
-      pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
-
-      state = (mc_state_t) pair->graph_state;
-
-      if (pair->exploration_started) {
-
-        saved_req = MC_state_get_executed_request(state, &value);
-
-        if (saved_req != nullptr) {
-          /* because we got a copy of the executed request, we have to fetch the
-             real one, pointed by the request field of the issuer process */
-          const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
-          req = &issuer->simcall;
-
-          /* Debug information */
-          if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
-            req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
-            XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
-            xbt_free(req_str);
-          }
-
-        }
-
-        simgrid::mc::handle_simcall(req, value);
-        mc_model_checker->wait_for_requests();
-      }
-
-      /* Update statistics */
-      mc_stats->visited_pairs++;
-      mc_stats->executed_transitions++;
-
-      depth++;
-      
-    }
-
-  XBT_DEBUG("**** End Replay ****");
-}
-
 /**
  * \brief Dumps the contents of a model-checker's stack and shows the actual
  *        execution trace

diff --git a/src/mc/mc_liveness.cpp b/src/mc/mc_liveness.cpp
index edf700d..2266c83 100644 (file)
--- a/src/mc/mc_liveness.cpp
+++ b/src/mc/mc_liveness.cpp
@@ -207,6 +207,73 @@ static void MC_pre_modelcheck_liveness(void)
   }
 }
 
+static void MC_replay_liveness(xbt_fifo_t stack)
+{
+  xbt_fifo_item_t item;
+  simgrid::mc::Pair* pair = nullptr;
+  mc_state_t state = nullptr;
+  smx_simcall_t req = nullptr, saved_req = NULL;
+  int value, depth = 1;
+  char *req_str;
+
+  XBT_DEBUG("**** Begin Replay ****");
+
+  /* Intermediate backtracking */
+  if(_sg_mc_checkpoint > 0) {
+    item = xbt_fifo_get_first_item(stack);
+    pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
+    if(pair->graph_state->system_state){
+      simgrid::mc::restore_snapshot(pair->graph_state->system_state);
+      return;
+    }
+  }
+
+  /* Restore the initial state */
+  simgrid::mc::restore_snapshot(initial_global_state->snapshot);
+
+    /* Traverse the stack from the initial state and re-execute the transitions */
+    for (item = xbt_fifo_get_last_item(stack);
+         item != xbt_fifo_get_first_item(stack);
+         item = xbt_fifo_get_prev_item(item)) {
+
+      pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
+
+      state = (mc_state_t) pair->graph_state;
+
+      if (pair->exploration_started) {
+
+        saved_req = MC_state_get_executed_request(state, &value);
+
+        if (saved_req != nullptr) {
+          /* because we got a copy of the executed request, we have to fetch the
+             real one, pointed by the request field of the issuer process */
+          const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
+          req = &issuer->simcall;
+
+          /* Debug information */
+          if (XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)) {
+            req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
+            XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
+            xbt_free(req_str);
+          }
+
+        }
+
+        simgrid::mc::handle_simcall(req, value);
+        mc_model_checker->wait_for_requests();
+      }
+
+      /* Update statistics */
+      mc_stats->visited_pairs++;
+      mc_stats->executed_transitions++;
+
+      depth++;
+
+    }
+
+  XBT_DEBUG("**** End Replay ****");
+}
+
 static int MC_modelcheck_liveness_main(void)
 {
   simgrid::mc::Pair* current_pair = nullptr;

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 869042c..28f1178 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -48,7 +48,6 @@ XBT_PRIVATE extern FILE *dot_output;
 XBT_PRIVATE extern int user_max_depth_reached;
 
 XBT_PRIVATE void MC_replay(xbt_fifo_t stack);
-XBT_PRIVATE void MC_replay_liveness(xbt_fifo_t stack);
 XBT_PRIVATE void MC_show_deadlock(smx_simcall_t req);
 XBT_PRIVATE void MC_show_stack_safety(xbt_fifo_t stack);
 XBT_PRIVATE void MC_dump_stack_safety(xbt_fifo_t stack);