[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 b45c70c..2266c83 100644 (file)
--- a/src/mc/mc_liveness.cpp
+++ b/src/mc/mc_liveness.cpp
@@ -13,7 +13,6 @@
 #include <xbt/dynar.h>
 #include <xbt/fifo.h>
 #include <xbt/log.h>
-#include <xbt/parmap.h>
 #include <xbt/sysdep.h>
 
 #include "src/mc/mc_request.h"
@@ -21,22 +20,17 @@
 #include "src/mc/mc_private.h"
 #include "src/mc/mc_record.h"
 #include "src/mc/mc_smx.h"
-#include "src/mc/mc_client.h"
+#include "src/mc/Client.hpp"
 #include "src/mc/mc_replay.h"
 #include "src/mc/mc_safety.h"
 #include "src/mc/mc_exit.h"
 
-extern "C" {
-
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
                                 "Logging specific to algorithms for liveness properties verification");
 
-}
-
 /********* Global variables *********/
 
 xbt_dynar_t acceptance_pairs;
-xbt_parmap_t parmap;
 
 /********* Static functions *********/
 
@@ -213,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;
@@ -379,8 +440,6 @@ static int MC_modelcheck_liveness_main(void)
 
 int modelcheck_liveness(void)
 {
-  if (mc_reduce_kind == e_mc_reduce_unset)
-    mc_reduce_kind = e_mc_reduce_none;
   XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
   MC_automaton_load(_sg_mc_property_file);
   mc_model_checker->wait_for_requests();