X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/5a9c70d5dfe11c9c7660b795b00f49b4170da968..071699dbbcb6ebfc659f27ae4b83bc74f6dfa9cb:/src/mc/mc_global.c

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 68d6453533..2738d46e43 100644
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -106,7 +106,7 @@ void MC_init_liveness_stateful(xbt_automaton_t a){
 
   /* Initialize statistics */
   mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1);
-  mc_stats = xbt_new0(s_mc_stats_t, 1);
+  //mc_stats = xbt_new0(s_mc_stats_t, 1);
 
   XBT_DEBUG("Creating snapshot_stack");
 
@@ -116,7 +116,6 @@ void MC_init_liveness_stateful(xbt_automaton_t a){
 
   MC_UNSET_RAW_MEM;
 
-  //MC_vddfs_stateful_init(a);
   MC_ddfs_stateful_init(a);
   //MC_dpor2_init(a);
   //MC_dpor3_init(a);
@@ -136,7 +135,7 @@ void MC_init_liveness_stateless(xbt_automaton_t a){
   /* Initialize statistics */
   mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1);
 
-  XBT_DEBUG("Creating snapshot_stack");
+  XBT_DEBUG("Creating stack");
 
  /* Create exploration stack */
   mc_stack_liveness_stateless = xbt_fifo_new();
@@ -144,6 +143,8 @@ void MC_init_liveness_stateless(xbt_automaton_t a){
   MC_UNSET_RAW_MEM;
 
   MC_ddfs_stateless_init(a);
+
+  
 }
 
 
@@ -174,7 +175,7 @@ void MC_modelcheck_liveness_stateless(xbt_automaton_t a){
 void MC_exit_liveness(void)
 {
   MC_print_statistics_pairs(mc_stats_pair);
-  xbt_free(mc_time);
+  //xbt_free(mc_time);
   MC_memory_exit();
 }
 
@@ -281,6 +282,57 @@ void MC_replay(xbt_fifo_t stack)
   XBT_DEBUG("**** End Replay ****");
 }
 
+void MC_replay_liveness(xbt_fifo_t stack)
+{
+  int value;
+  char *req_str;
+  smx_req_t req = NULL, saved_req = NULL;
+  xbt_fifo_item_t item;
+  mc_state_t state;
+  mc_pair_stateless_t pair;
+
+  XBT_DEBUG("**** Begin Replay ****");
+
+  /* Restore the initial state */
+  MC_restore_snapshot(initial_snapshot);
+  /* 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  */
+  MC_UNSET_RAW_MEM;
+
+  /* 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 = (mc_pair_stateless_t) xbt_fifo_get_item_content(item);
+    state = (mc_state_t) pair->graph_state;
+    saved_req = MC_state_get_executed_request(state, &value);
+    //XBT_DEBUG("SavedReq->call %u", saved_req->call);
+   
+    if(saved_req != NULL){
+      /* 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 */
+      req = &saved_req->issuer->request;
+      //XBT_DEBUG("Req->call %u", req->call);
+
+      /* Debug information */
+      if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
+        req_str = MC_request_to_string(req, value);
+        XBT_DEBUG("Replay: %s (%p)", req_str, state);
+        xbt_free(req_str);
+      }
+    }
+         
+    SIMIX_request_pre(req, value);
+    MC_wait_for_requests();
+         
+    /* Update statistics */
+    mc_stats_pair->visited_pairs++;
+  }
+  XBT_DEBUG("**** End Replay ****");
+}
+
+
 /**
  * \brief Dumps the contents of a model-checker's stack and shows the actual
  *        execution trace