X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/c7df79fb2ff6e105b83092e142fbe74214fd3b75..ab8e2fe95944fb998edd6e95d1022a05175c4f92:/src/mc/mc_global.cpp

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index 187a69b442..38609f9644 100644
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -13,6 +13,10 @@
 
 #include <vector>
 
+#include <xbt/dynar.h>
+#include <xbt/automaton.h>
+#include <xbt/swag.h>
+
 #include "mc_base.h"
 
 #include "mc/mc.h"
@@ -31,10 +35,10 @@
 #include "src/mc/mc_request.h"
 #include "src/mc/mc_safety.h"
 #include "src/mc/mc_snapshot.h"
-#include "src/mc/LivenessChecker.hpp"
 #include "src/mc/mc_private.h"
 #include "src/mc/mc_unw.h"
 #include "src/mc/mc_smx.h"
+#include "src/mc/Checker.hpp"
 #endif
 
 #include "src/mc/mc_record.h"
@@ -54,14 +58,12 @@ 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;
 char mc_replay_mode = false;
 
 mc_stats_t mc_stats = nullptr;
-xbt_fifo_t mc_stack = nullptr;
 
 /* Liveness */
 
@@ -110,27 +112,23 @@ void MC_run()
   simgrid::mc::processes_time.clear();
 }
 
+namespace simgrid {
+namespace mc {
+
 /**
  * \brief Re-executes from the state at position start all the transitions indicated by
  *        a given model-checker stack.
  * \param stack The stack with the transitions to execute.
  * \param start Start index to begin the re-execution.
  */
-void MC_replay(xbt_fifo_t stack)
+void replay(std::list<std::unique_ptr<simgrid::mc::State>> const& stack)
 {
-  int value, count = 1;
-  char *req_str;
-  smx_simcall_t req = nullptr, saved_req = NULL;
-  xbt_fifo_item_t item, start_item;
-  simgrid::mc::State* state;
-  
   XBT_DEBUG("**** Begin Replay ****");
 
   /* Intermediate backtracking */
   if(_sg_mc_checkpoint > 0 || _sg_mc_termination || _sg_mc_visited > 0) {
-    start_item = xbt_fifo_get_first_item(stack);
-    state = (simgrid::mc::State*)xbt_fifo_get_item_content(start_item);
-    if(state->system_state){
+    simgrid::mc::State* state = stack.back().get();
+    if (state->system_state) {
       simgrid::mc::restore_snapshot(state->system_state);
       if(_sg_mc_comms_determinism || _sg_mc_send_determinism) 
         MC_restore_communications_pattern(state);
@@ -144,8 +142,6 @@ void MC_replay(xbt_fifo_t stack)
   /* At the moment of taking the snapshot the raw heap was set, so restoring
    * it will set it back again, we have to unset it to continue  */
 
-  start_item = xbt_fifo_get_last_item(stack);
-
   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
     // int n = xbt_dynar_length(incomplete_communications_pattern);
     unsigned n = MC_smx_get_maxpid();
@@ -153,31 +149,32 @@ void MC_replay(xbt_fifo_t stack)
     assert(n == xbt_dynar_length(initial_communications_pattern));
     for (unsigned j=0; j < n ; j++) {
       xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t));
-      xbt_dynar_get_as(initial_communications_pattern, j, mc_list_comm_pattern_t)->index_comm = 0;
+      xbt_dynar_get_as(initial_communications_pattern, j, simgrid::mc::PatternCommunicationList*)->index_comm = 0;
     }
   }
 
+  int count = 1;
+
   /* Traverse the stack from the state at position start and re-execute the transitions */
-  for (item = start_item;
-       item != xbt_fifo_get_first_item(stack);
-       item = xbt_fifo_get_prev_item(item)) {
+  for (std::unique_ptr<simgrid::mc::State> const& state : stack) {
+    if (state == stack.back())
+      break;
 
-    state = (simgrid::mc::State*) xbt_fifo_get_item_content(item);
-    saved_req = MC_state_get_executed_request(state, &value);
+    int value;
+    smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
     
     if (saved_req) {
       /* 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;
+      smx_simcall_t 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: %s (%p)", req_str, state);
-        xbt_free(req_str);
-      }
+      XBT_DEBUG("Replay: %s (%p)",
+        simgrid::mc::request_to_string(
+          req, value, simgrid::mc::RequestType::simix).c_str(),
+        state.get());
 
       /* TODO : handle test and testany simcalls */
       e_mc_call_type_t call = MC_CALL_TYPE_NONE;
@@ -203,6 +200,9 @@ void MC_replay(xbt_fifo_t stack)
   XBT_DEBUG("**** End Replay ****");
 }
 
+}
+}
+
 void MC_show_deadlock(void)
 {
   XBT_INFO("**************************");