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

[simgrid.git] / src / mc / mc_liveness.cpp

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;