From 716dbb41c51b7420cc95ef7c43609d09720d5142 Mon Sep 17 00:00:00 2001
From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Fri, 24 Jun 2011 14:24:47 +0200
Subject: [PATCH 1/1] model-checker : dfs with good restore snapshot

---
 src/mc/mc_liveness.c | 35 +++++++++++++++++++++++++++++------
 src/mc/private.h     |  2 +-
 2 files changed, 30 insertions(+), 7 deletions(-)

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 626abebb51..980d7a4e1b 100644
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -273,14 +273,21 @@ void MC_dfs_init(xbt_automaton_t a){
 
     MC_UNSET_RAW_MEM;
 
-    MC_dfs(a,0);
-
+    if(cursor == 0){
+      MC_dfs(a, 0, 0);
+    }else{
+      MC_dfs(a, 0, 1);
+    }
   }
 
+ 
+
+ 
+  
 }
 
 
-void MC_dfs(xbt_automaton_t a, int search_cycle){
+void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){
 
   smx_process_t process = NULL;
 
@@ -288,11 +295,23 @@ void MC_dfs(xbt_automaton_t a, int search_cycle){
   if(xbt_fifo_size(mc_snapshot_stack) == 0)
     return;
 
- 
+  if(restore == 1){
+    MC_restore_snapshot(((mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)))->system_state);
+    MC_UNSET_RAW_MEM;
+  }
+
 
   /* Get current state */
   mc_pairs_t current_pair = (mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
 
+  /*if(restore==1){
+    xbt_swag_foreach(process, simix_global->process_list){
+      if(MC_process_is_enabled(process)){
+	//XBT_DEBUG("Pid : %lu", process->pid);
+	MC_state_interleave_process(current_pair->graph_state, process);
+      }
+    }
+    }*/
 
   XBT_DEBUG("************************************************** ( search_cycle = %d )", search_cycle);
   XBT_DEBUG("State : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id,MC_state_interleave_size(current_pair->graph_state));
@@ -414,7 +433,7 @@ void MC_dfs(xbt_automaton_t a, int search_cycle){
 	set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle);
 	MC_UNSET_RAW_MEM;
 
-	MC_dfs(a, search_cycle);
+	MC_dfs(a, search_cycle, 0);
 
 	if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
 
@@ -430,9 +449,13 @@ void MC_dfs(xbt_automaton_t a, int search_cycle){
 	    
 	  set_pair_reached(current_pair->graph_state, current_pair->automaton_state);
 	  XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
-	  MC_dfs(a, 1);
+	  MC_dfs(a, 1, 1);
 
 	}
+      }else{
+
+	XBT_DEBUG("Pair already visited !");
+
       }
     }
     
diff --git a/src/mc/private.h b/src/mc/private.h
index 8fa81adafd..0431ced999 100644
--- a/src/mc/private.h
+++ b/src/mc/private.h
@@ -211,7 +211,7 @@ typedef struct s_mc_reached_pairs{
 extern xbt_fifo_t mc_snapshot_stack;
 
 void MC_dfs_init(xbt_automaton_t a);
-void MC_dfs(xbt_automaton_t automaton, int search_cycle);
+void MC_dfs(xbt_automaton_t automaton, int search_cycle, int restore);
 int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l);
 mc_pairs_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st);
 void set_pair_visited(mc_state_t gs, xbt_state_t as, int search_cycle);
-- 
2.20.1