X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/b2b401f886e6e1c849e1dcd5b70a7133ba4859f9..6988d9960f1104aaac5371c51c0d79daf1a13b68:/src/mc/mc_liveness.c?ds=sidebyside

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index eee93052c2..9771381e78 100644
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -5,52 +5,132 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
                                 "Logging specific to algorithms for liveness properties verification");
 
 xbt_dynar_t initial_pairs = NULL;
-int max_pair = 0;
 xbt_dynar_t reached_pairs;
+xbt_dynar_t successors = NULL;
 extern mc_snapshot_t initial_snapshot;
 
+/* Global variables for stateless algorithm */
+mc_snapshot_t snapshot = NULL;
+
+/* Global variables for stateful algorithm */
+mc_snapshot_t next_snapshot = NULL;
+mc_snapshot_t current_snapshot = NULL;
+
+
 mc_pair_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){
   mc_pair_t p = NULL;
   p = xbt_new0(s_mc_pair_t, 1);
   p->system_state = sn;
   p->automaton_state = st;
   p->graph_state = sg;
-  p->num = max_pair;
-  max_pair++;
   mc_stats_pair->expanded_pairs++;
   return p;
     
 }
 
-int reached(mc_pair_t pair){
+int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
+  
+  if(s1->num_reg != s2->num_reg)
+    return 1;
 
-  char* hash_reached = malloc(sizeof(char)*160);
-  unsigned int c= 0;
+  int i, errors=0;
 
-  MC_SET_RAW_MEM;
-  char *hash = malloc(sizeof(char)*160);
-  xbt_sha((char *)&pair, hash);
-  xbt_dynar_foreach(reached_pairs, c, hash_reached){
-    if(strcmp(hash, hash_reached) == 0){
-      MC_UNSET_RAW_MEM;
+  for(i=0 ; i< s1->num_reg ; i++){
+    
+    if(s1->regions[i]->size != s2->regions[i]->size)
+      return 1;
+    
+    if(s1->regions[i]->start_addr != s2->regions[i]->start_addr)
+      return 1;
+    
+    if(s1->regions[i]->type != s2->regions[i]->type)
       return 1;
+
+    if(s1->regions[i]->type == 0){ 
+      if(mmalloc_compare_heap(s1->regions[i]->start_addr, s2->regions[i]->start_addr)){
+	XBT_DEBUG("Different heap (mmalloc_compare)");
+	sleep(1);
+	errors++; 
+      }
+    }else{
+      if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
+    	XBT_DEBUG("Different memcmp for data in libsimgrid");
+	sleep(1);
+    	errors++;
+      }
     }
+    
+    
   }
-  
-  MC_UNSET_RAW_MEM;
-  return 0;
+
+  return (errors>0);
+
 }
 
-void set_pair_reached(mc_pair_t pair){
+int reached(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t s){
+
 
-  if(reached(pair) == 0){
+  if(xbt_dynar_is_empty(reached_pairs)){
+    return 0;
+  }else{
     MC_SET_RAW_MEM;
-    char *hash = malloc(sizeof(char)*160) ;
-    xbt_sha((char *)&pair, hash);
-    xbt_dynar_push(reached_pairs, &hash); 
+    
+    xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
+
+    /* Get values of propositional symbols */
+    unsigned int cursor = 0;
+    xbt_propositional_symbol_t ps = NULL;
+    xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
+      int (*f)() = ps->function;
+      int res = (*f)();
+      xbt_dynar_push_as(prop_ato, int, res);
+    }
+    
+    cursor = 0;
+    mc_pair_reached_t pair_test;
+
+    xbt_dynar_foreach(reached_pairs, cursor, pair_test){
+      if(automaton_state_compare(pair_test->automaton_state, st) == 0){
+	if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
+	  if(snapshot_compare(pair_test->system_state, s) == 0){
+	    MC_UNSET_RAW_MEM;
+	    return 1;
+	  }
+	}
+      }
+    }
+
     MC_UNSET_RAW_MEM;
+    return 0;
+    
   }
+}
+
+void set_pair_reached(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t sn){
 
+ 
+  MC_SET_RAW_MEM;
+  
+  mc_pair_reached_t pair = NULL;
+  pair = xbt_new0(s_mc_pair_reached_t, 1);
+  pair->automaton_state = st;
+  pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
+  pair->system_state = sn;
+  
+  /* Get values of propositional symbols */
+  unsigned int cursor = 0;
+  xbt_propositional_symbol_t ps = NULL;
+  xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
+    int (*f)() = ps->function;
+    int res = (*f)();
+    xbt_dynar_push_as(pair->prop_ato, int, res);
+  }
+  
+  xbt_dynar_push(reached_pairs, &pair); 
+  
+  MC_UNSET_RAW_MEM;
+  
+  
 }
 
 void MC_pair_delete(mc_pair_t pair){
@@ -61,6 +141,7 @@ void MC_pair_delete(mc_pair_t pair){
 }
 
 
+
 int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){
   
   switch(l->type){
@@ -104,66 +185,42 @@ int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){
 
 
 
-/******************************* DFS with visited state *******************************/
 
-xbt_dynar_t visited_pairs;
 
-void set_pair_visited(mc_pair_t pair, int sc){
-
-  MC_SET_RAW_MEM;
-  mc_visited_pair_t p = NULL;
-  p = xbt_new0(s_mc_visited_pair_t, 1);
-  p->pair = pair;
-  p->search_cycle = sc;
-  char *hash = malloc(sizeof(char)*160);
-  xbt_sha((char *)&p, hash);
-  xbt_dynar_push(visited_pairs, &hash); 
-  MC_UNSET_RAW_MEM;	
+/********************* Double-DFS stateless *******************/
 
+void MC_pair_stateless_delete(mc_pair_stateless_t pair){
+  xbt_free(pair->graph_state->proc_status);
+  xbt_free(pair->graph_state);
+  //xbt_free(pair->automaton_state); -> FIXME : à implémenter
+  xbt_free(pair);
 }
 
-int visited(mc_pair_t pair, int sc){
-
-  char* hash_visited = malloc(sizeof(char)*160);
-  unsigned int c= 0;
-
-  MC_SET_RAW_MEM;
-  mc_visited_pair_t p = NULL;
-  p = xbt_new0(s_mc_visited_pair_t, 1);
-  p->pair = pair;
-  p->search_cycle = sc;
-  char *hash = malloc(sizeof(char)*160);
-  xbt_sha((char *)&p, hash);
-  xbt_dynar_foreach(visited_pairs, c, hash_visited){
-    if(strcmp(hash, hash_visited) == 0){
-      MC_UNSET_RAW_MEM;
-      return 1;
-    }
-  }
-  
-  MC_UNSET_RAW_MEM;
-  return 0;
-
+mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st){
+  mc_pair_stateless_t p = NULL;
+  p = xbt_new0(s_mc_pair_stateless_t, 1);
+  p->automaton_state = st;
+  p->graph_state = sg;
+  mc_stats_pair->expanded_pairs++;
+  return p;
 }
 
 
-void MC_vddfs_stateful_init(xbt_automaton_t a){
+
+void MC_ddfs_stateless_init(xbt_automaton_t a){
 
   XBT_DEBUG("**************************************************");
-  XBT_DEBUG("Double-DFS stateful with visited state init");
+  XBT_DEBUG("Double-DFS stateless init");
   XBT_DEBUG("**************************************************");
  
-  mc_pair_t mc_initial_pair;
-  mc_state_t initial_graph_state;
+  mc_pair_stateless_t mc_initial_pair = NULL;
+  mc_state_t initial_graph_state = NULL;
   smx_process_t process; 
-  mc_snapshot_t init_snapshot;
  
   MC_wait_for_requests();
 
   MC_SET_RAW_MEM;
 
-  init_snapshot = xbt_new0(s_mc_snapshot_t, 1);
-
   initial_graph_state = MC_state_pair_new();
   xbt_swag_foreach(process, simix_global->process_list){
     if(MC_process_is_enabled(process)){
@@ -171,94 +228,66 @@ void MC_vddfs_stateful_init(xbt_automaton_t a){
     }
   }
 
-  visited_pairs = xbt_dynar_new(sizeof(char *), NULL); 
-  reached_pairs = xbt_dynar_new(sizeof(char *), NULL); 
+  reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL); 
+  successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
+  snapshot = xbt_new0(s_mc_snapshot_t, 1);
 
-  MC_take_snapshot(init_snapshot);
+  initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
+  MC_take_snapshot(initial_snapshot);
 
   MC_UNSET_RAW_MEM; 
 
-  /* regarder dans l'automate toutes les transitions activables grâce à l'état initial du système 
-    -> donnera les états initiaux de la propriété consistants avec l'état initial du système */
-
   unsigned int cursor = 0;
-  unsigned int cursor2 = 0;
-  xbt_state_t state = NULL;
-  int res;
-  xbt_transition_t transition_succ;
-  xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
-  mc_pair_t pair_succ;
+  xbt_state_t state;
 
   xbt_dynar_foreach(a->states, cursor, state){
     if(state->type == -1){
-      xbt_dynar_foreach(state->out, cursor2, transition_succ){
-  	res = MC_automaton_evaluate_label(a, transition_succ->label);
-	
-  	if((res == 1) || (res == 2)){
-	 
-  	  MC_SET_RAW_MEM;
-
-  	  mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
-  	  xbt_dynar_push(successors, &mc_initial_pair);
-
-  	  MC_UNSET_RAW_MEM;
-
-	}
+      
+      MC_SET_RAW_MEM;
+      mc_initial_pair = new_pair_stateless(initial_graph_state, state);
+      xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
+      MC_UNSET_RAW_MEM;
+      
+      if(cursor == 0){
+	MC_ddfs_stateless(a, 0, 0);
+      }else{
+	MC_restore_snapshot(initial_snapshot);
+	MC_UNSET_RAW_MEM;
+	MC_ddfs_stateless(a, 0, 0);
       }
-    }
-  }
-
-  cursor = 0;
-
-  if(xbt_dynar_length(successors) == 0){
-    xbt_dynar_foreach(a->states, cursor, state){
-      if(state->type == -1){
+    }else{
+      if(state->type == 2){
+      
 	MC_SET_RAW_MEM;
-
-	mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
-	xbt_dynar_push(successors, &mc_initial_pair);
-	
+	mc_initial_pair = new_pair_stateless(initial_graph_state, state);
+	xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
 	MC_UNSET_RAW_MEM;
+	
+	if(cursor == 0){
+	  MC_ddfs_stateless(a, 1, 0);
+	}else{
+	  MC_restore_snapshot(initial_snapshot);
+	  MC_UNSET_RAW_MEM;
+	  MC_ddfs_stateless(a, 1, 0);
+	}
       }
     }
-  }
-
-  cursor = 0;
-  xbt_dynar_foreach(successors, cursor, pair_succ){
-    MC_SET_RAW_MEM;
-
-    xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
-    set_pair_visited(pair_succ, 0);
-
-    MC_UNSET_RAW_MEM;
+  } 
 
-    if(cursor == 0){
-      MC_vddfs_stateful(a, 0, 0);
-    }else{
-      MC_vddfs_stateful(a, 0, 1);
-    }
-  }  
 }
 
 
-void MC_vddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
-
-  smx_process_t process = NULL;
+void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){
 
+  smx_process_t process;
+  mc_pair_stateless_t current_pair = NULL;
 
-  if(xbt_fifo_size(mc_stack_liveness_stateful) == 0)
+  if(xbt_fifo_size(mc_stack_liveness_stateless) == 0)
     return;
 
-  if(restore == 1){
-    MC_restore_snapshot(((mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)))->system_state);
-    MC_UNSET_RAW_MEM;
-  }
-
-
-  /* Get current state */
-  mc_pair_t current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
-
-  if(restore==1){
+  if(replay == 1){
+    MC_replay_liveness(mc_stack_liveness_stateless);
+    current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
     xbt_swag_foreach(process, simix_global->process_list){
       if(MC_process_is_enabled(process)){
 	MC_state_interleave_process(current_pair->graph_state, process);
@@ -266,10 +295,17 @@ void MC_vddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
     }
   }
 
-  XBT_DEBUG("************************************************** ( search_cycle = %d )", search_cycle);
-  XBT_DEBUG("Pair : 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));
-  
+  /* Get current pair */
+  current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
 
+  /* Update current state in buchi automaton */
+  a->current_state = current_pair->automaton_state;
+
+ 
+  XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateless), search_cycle);
+  XBT_DEBUG("Pair : 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));
+ 
+  
   mc_stats_pair->visited_pairs++;
 
   int value;
@@ -277,26 +313,16 @@ void MC_vddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
   smx_req_t req = NULL;
   char *req_str;
 
-  mc_pair_t pair_succ;
   xbt_transition_t transition_succ;
-  unsigned int cursor;
+  unsigned int cursor = 0;
   int res;
 
-  xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
+  mc_pair_stateless_t next_pair = NULL;
+  mc_pair_stateless_t pair_succ;
+  //mc_snapshot_t next_snapshot = NULL;
 
-  mc_pair_t next_pair;
-  mc_snapshot_t next_snapshot;
-  mc_snapshot_t current_snapshot;
-  
-  
   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
-
-    MC_SET_RAW_MEM;
-    current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
-    MC_take_snapshot(current_snapshot);
-    MC_UNSET_RAW_MEM;
    
-    
     /* Debug information */
     if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
       req_str = MC_request_to_string(req, value);
@@ -304,8 +330,10 @@ void MC_vddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
       xbt_free(req_str);
     }
 
-    MC_state_set_executed_request(current_pair->graph_state, req, value);
+    //sleep(1);
 
+    MC_state_set_executed_request(current_pair->graph_state, req, value);   
+    
     /* Answer the request */
     SIMIX_request_pre(req, value);
 
@@ -313,11 +341,11 @@ void MC_vddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
     MC_wait_for_requests();
 
 
-    /* Create the new expanded graph_state */
     MC_SET_RAW_MEM;
 
+    /* Create the new expanded graph_state */
     next_graph_state = MC_state_pair_new();
-    
+
     /* Get enabled process and insert it in the interleave set of the next graph_state */
     xbt_swag_foreach(process, simix_global->process_list){
       if(MC_process_is_enabled(process)){
@@ -325,106 +353,127 @@ void MC_vddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
       }
     }
 
-    next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
-    MC_take_snapshot(next_snapshot);
-      
+    xbt_dynar_reset(successors);
+
     MC_UNSET_RAW_MEM;
 
-    xbt_dynar_reset(successors);
-    
-    cursor = 0;
+
+    cursor= 0;
     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 
       res = MC_automaton_evaluate_label(a, transition_succ->label);
 
-      MC_SET_RAW_MEM;
+      if(res == 1){ // enabled transition in automaton
+	MC_SET_RAW_MEM;
+	next_pair = new_pair_stateless(next_graph_state, transition_succ->dst);
+	xbt_dynar_push(successors, &next_pair);
+	MC_UNSET_RAW_MEM;
+      }
+
+    }
+
+    cursor = 0;
+   
+    xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
+      
+      res = MC_automaton_evaluate_label(a, transition_succ->label);
 	
-      if((res == 1) || (res == 2)){ // enabled transition in automaton
-	next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
+      if(res == 2){ // true transition in automaton
+	MC_SET_RAW_MEM;
+	next_pair = new_pair_stateless(next_graph_state, transition_succ->dst);
 	xbt_dynar_push(successors, &next_pair);
+	MC_UNSET_RAW_MEM;
       }
 
-      MC_UNSET_RAW_MEM;
     }
 
    
     if(xbt_dynar_length(successors) == 0){
-
       MC_SET_RAW_MEM;
-      next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state);
+      next_pair = new_pair_stateless(next_graph_state, current_pair->automaton_state);
       xbt_dynar_push(successors, &next_pair);
       MC_UNSET_RAW_MEM;
-	
     }
 
+    cursor = 0; 
 
-    cursor = 0;
     xbt_dynar_foreach(successors, cursor, pair_succ){
 
-      //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
-
-      if((search_cycle == 1) && (reached(pair_succ) == 1)){
-	XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
-	XBT_INFO("|             ACCEPTANCE CYCLE            |");
-	XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
-	XBT_INFO("Counter-example that violates formula :");
-	MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
-	MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful);
-	MC_print_statistics_pairs(mc_stats_pair);
-	exit(0);
-      }
-	
-      if(visited(pair_succ, search_cycle) == 0){
+     
 
-	mc_stats_pair->executed_transitions++;
- 
+      if((search_cycle == 1) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)) ){
+	
+	XBT_DEBUG("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness_stateless) + 1);
+	
 	MC_SET_RAW_MEM;
-	xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
-	set_pair_visited(pair_succ, search_cycle);
+	MC_take_snapshot(snapshot);
 	MC_UNSET_RAW_MEM;
 
-	MC_vddfs_stateful(a, search_cycle, 0);
+	if(reached(a, pair_succ->automaton_state, snapshot) == 1){
+	  XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
+	  XBT_INFO("|             ACCEPTANCE CYCLE            |");
+	  XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
+	  XBT_INFO("Counter-example that violates formula :");
+	  MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
+	  MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
+	  MC_print_statistics_pairs(mc_stats_pair);
+	  exit(1);
+	}
+      }
+      
+      int interleave = MC_state_interleave_size(pair_succ->graph_state);
 
-	if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
+      if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)) && ( interleave > 0)){
+	XBT_DEBUG("Take snapshot of acceptance pair (depth = %d)", xbt_fifo_size(mc_stack_liveness_stateless) + 1 );
+	MC_SET_RAW_MEM;
+	MC_take_snapshot(snapshot);
+	MC_UNSET_RAW_MEM;
+      }
 
-	  MC_restore_snapshot(current_pair->system_state);
-	  MC_UNSET_RAW_MEM;
- 
-	  xbt_swag_foreach(process, simix_global->process_list){
-	    if(MC_process_is_enabled(process)){
-	      MC_state_interleave_process(current_pair->graph_state, process);
-	    }
-	  }
-	    
-	  set_pair_reached(current_pair);
-	  XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
-	  MC_vddfs_stateful(a, 1, 1);
+      MC_SET_RAW_MEM;
+      xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
+      MC_UNSET_RAW_MEM;
+      
+      MC_ddfs_stateless(a, search_cycle, 0);
 
-	}
-      }else{
+      /* If pair_succ is the last state of the execution (0 interleave), no acceptance cycle possible */
+      if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)) && ( interleave > 0)){
+       
+	XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
 
-	XBT_DEBUG("Pair already visited !");
+		
+	set_pair_reached(a, pair_succ->automaton_state, snapshot);
+
+	
+	/* Pair shifted from stack when first MC_ddfs finished and returned at this point */
+	MC_SET_RAW_MEM;
+	xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
+	MC_UNSET_RAW_MEM;
+      
+	MC_ddfs_stateless(a, 1, 1);
 
+	/* No acceptance cycle with this acceptance pair, we remove it from the list reached_pairs */
+	MC_SET_RAW_MEM;
+	xbt_dynar_pop(reached_pairs, NULL);
+	MC_UNSET_RAW_MEM;
+	  
       }
     }
-    
-    
+
     if(MC_state_interleave_size(current_pair->graph_state) > 0){
-      MC_restore_snapshot(current_snapshot);
-      MC_UNSET_RAW_MEM;
-    }
+      XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateless));
+      MC_replay_liveness(mc_stack_liveness_stateless);
+    }    
+   
   }
-
   
   MC_SET_RAW_MEM;
-  xbt_fifo_shift(mc_stack_liveness_stateful);
-  XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in snapshot_stack", current_pair->graph_state, current_pair->automaton_state);
+  xbt_fifo_shift(mc_stack_liveness_stateless);
+  XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle);
   MC_UNSET_RAW_MEM;
 
 }
 
-
-
 /********************* Double-DFS stateful without visited state *******************/
 
 
@@ -443,8 +492,6 @@ void MC_ddfs_stateful_init(xbt_automaton_t a){
 
   MC_SET_RAW_MEM;
 
-  init_snapshot = xbt_new0(s_mc_snapshot_t, 1);
-
   initial_graph_state = MC_state_pair_new();
   xbt_swag_foreach(process, simix_global->process_list){
     if(MC_process_is_enabled(process)){
@@ -452,102 +499,84 @@ void MC_ddfs_stateful_init(xbt_automaton_t a){
     }
   }
 
-  reached_pairs = xbt_dynar_new(sizeof(char *), NULL); 
-
+  reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL); 
+  successors = xbt_dynar_new(sizeof(mc_pair_t), NULL); 
+  current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
+  next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
+  
+  init_snapshot = xbt_new0(s_mc_snapshot_t, 1);
   MC_take_snapshot(init_snapshot);
 
   MC_UNSET_RAW_MEM; 
 
-  /* regarder dans l'automate toutes les transitions activables grâce à l'état initial du système 
-    -> donnera les états initiaux de la propriété consistants avec l'état initial du système */
-
   unsigned int cursor = 0;
-  unsigned int cursor2 = 0;
   xbt_state_t state = NULL;
-  int res;
-  xbt_transition_t transition_succ;
-  xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
-  mc_pair_t pair_succ;
 
   xbt_dynar_foreach(a->states, cursor, state){
     if(state->type == -1){
-      xbt_dynar_foreach(state->out, cursor2, transition_succ){
-  	res = MC_automaton_evaluate_label(a, transition_succ->label);
-	
-  	if((res == 1) || (res == 2)){
+    
+      MC_SET_RAW_MEM;
+      mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state);
+      xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair);
+      MC_UNSET_RAW_MEM;
+
+      if(cursor == 0){
+	MC_ddfs_stateful(a, 0, 0);
+      }else{
+	MC_restore_snapshot(init_snapshot);
+	MC_UNSET_RAW_MEM;
+	MC_ddfs_stateful(a, 0, 0);
+      }
+    }else{
+       if(state->type == 2){
+    
+	 MC_SET_RAW_MEM;
+	 mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state);
+	 xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair);
+	 MC_UNSET_RAW_MEM;
 	 
-  	  MC_SET_RAW_MEM;
+	 if(cursor == 0){
+	   MC_ddfs_stateful(a, 1, 0);
+	 }else{
+	   MC_restore_snapshot(init_snapshot);
+	   MC_UNSET_RAW_MEM;
+	   MC_ddfs_stateful(a, 1, 0);
+	 }
+       }
+    }
+  } 
+}
 
-  	  mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
-  	  xbt_dynar_push(successors, &mc_initial_pair);
 
-  	  MC_UNSET_RAW_MEM;
-
-	}
-      }
-    }
-  }
-
-  cursor = 0;
-
-  if(xbt_dynar_length(successors) == 0){
-    xbt_dynar_foreach(a->states, cursor, state){
-      if(state->type == -1){
-	MC_SET_RAW_MEM;
-
-	mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
-	xbt_dynar_push(successors, &mc_initial_pair);
-	
-	MC_UNSET_RAW_MEM;
-      }
-    }
-  }
-
-  cursor = 0;
-  xbt_dynar_foreach(successors, cursor, pair_succ){
-    MC_SET_RAW_MEM;
-
-    xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
-
-    MC_UNSET_RAW_MEM;
-
-    if(cursor == 0){
-      MC_ddfs_stateful(a, 0, 0);
-    }else{
-      MC_ddfs_stateful(a, 0, 1);
-    }
-  }  
-}
-
-
-void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
+void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
 
   smx_process_t process = NULL;
-
+  mc_pair_t current_pair = NULL;
 
   if(xbt_fifo_size(mc_stack_liveness_stateful) == 0)
     return;
 
   if(restore == 1){
-    MC_restore_snapshot(((mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)))->system_state);
-    MC_UNSET_RAW_MEM;
-  }
-
-
-  /* Get current state */
-  mc_pair_t current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
-
-  if(restore==1){
+    current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
+    MC_restore_snapshot(current_pair->system_state);
     xbt_swag_foreach(process, simix_global->process_list){
       if(MC_process_is_enabled(process)){
 	MC_state_interleave_process(current_pair->graph_state, process);
       }
     }
+    MC_UNSET_RAW_MEM;
   }
 
-  XBT_DEBUG("************************************************** ( search_cycle = %d )", search_cycle);
+  /* Get current state */
+  current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
+
+
+  XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateful), search_cycle);
   XBT_DEBUG("Pair : 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));
+
+  a->current_state = current_pair->automaton_state;
   
+  //sleep(1);
 
   mc_stats_pair->visited_pairs++;
 
@@ -561,24 +590,18 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
   unsigned int cursor;
   int res;
 
-  xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
-
-  mc_pair_t next_pair;
-  mc_snapshot_t next_snapshot;
-  mc_snapshot_t current_snapshot;
-  
+  mc_pair_t next_pair = NULL;
   
   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 
     MC_SET_RAW_MEM;
-    current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
     MC_take_snapshot(current_snapshot);
     MC_UNSET_RAW_MEM;
-   
-    
+     
     /* Debug information */
     if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
       req_str = MC_request_to_string(req, value);
+      XBT_DEBUG("Pair : 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));
       XBT_DEBUG("Execute: %s", req_str);
       xbt_free(req_str);
     }
@@ -604,26 +627,40 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
       }
     }
 
-    next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
     MC_take_snapshot(next_snapshot);
-      
-    MC_UNSET_RAW_MEM;
 
     xbt_dynar_reset(successors);
+
+    MC_UNSET_RAW_MEM;
+
     
     cursor = 0;
     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 
       res = MC_automaton_evaluate_label(a, transition_succ->label);
+	
+      if(res == 1){ // enabled transition in automaton
+	MC_SET_RAW_MEM;
+	next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
+	xbt_dynar_push(successors, &next_pair);
+	MC_UNSET_RAW_MEM;
+      }
 
-      MC_SET_RAW_MEM;
+    }
+
+    cursor = 0;
+    xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
+
+      res = MC_automaton_evaluate_label(a, transition_succ->label);
 	
-      if((res == 1) || (res == 2)){ // enabled transition in automaton
+      if(res == 2){ // transition always enabled in automaton
+	MC_SET_RAW_MEM;
 	next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
 	xbt_dynar_push(successors, &next_pair);
+	MC_UNSET_RAW_MEM;
       }
 
-      MC_UNSET_RAW_MEM;
+     
     }
 
    
@@ -636,351 +673,62 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
 	
     }
 
-
     cursor = 0;
     xbt_dynar_foreach(successors, cursor, pair_succ){
 
-      //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
-
-      if((search_cycle == 1) && (reached(pair_succ) == 1)){
-	XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
-	XBT_INFO("|             ACCEPTANCE CYCLE            |");
-	XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
-	XBT_INFO("Counter-example that violates formula :");
-	MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
-	MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful);
-	MC_print_statistics_pairs(mc_stats_pair);
-	exit(0);
+      if((search_cycle == 1) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
+	
+	if(reached(a, pair_succ->automaton_state, next_snapshot) == 1){
+	  XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
+	  XBT_INFO("|             ACCEPTANCE CYCLE            |");
+	  XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
+	  XBT_INFO("Counter-example that violates formula :");
+	  MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
+	  MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful);
+	  MC_print_statistics_pairs(mc_stats_pair);
+	  exit(1);
+	}
       }
 	
-      mc_stats_pair->executed_transitions++;
  
       MC_SET_RAW_MEM;
       xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
       MC_UNSET_RAW_MEM;
 
       MC_ddfs_stateful(a, search_cycle, 0);
-
-      if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
-
-	MC_restore_snapshot(current_pair->system_state);
-	MC_UNSET_RAW_MEM;
- 
-	xbt_swag_foreach(process, simix_global->process_list){
-	  if(MC_process_is_enabled(process)){
-	    MC_state_interleave_process(current_pair->graph_state, process);
-	  }
-	}
-	    
-	set_pair_reached(current_pair);
-	XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
-	MC_ddfs_stateful(a, 1, 1);
-
-      }
-    }
     
     
-    if(MC_state_interleave_size(current_pair->graph_state) > 0){
-      MC_restore_snapshot(current_snapshot);
-      MC_UNSET_RAW_MEM;
-    }
-  }
-
-  
-  MC_SET_RAW_MEM;
-  xbt_fifo_shift(mc_stack_liveness_stateful);
-  XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in snapshot_stack", current_pair->graph_state, current_pair->automaton_state);
-  MC_UNSET_RAW_MEM;
-
-}
-
-
-
-/********************* Double-DFS stateless *******************/
-
-void MC_pair_stateless_delete(mc_pair_stateless_t pair){
-  xbt_free(pair->graph_state->proc_status);
-  xbt_free(pair->graph_state);
-  //xbt_free(pair->automaton_state); -> FIXME : à implémenter
-  xbt_free(pair);
-}
+      if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 
-mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st){
-  mc_pair_stateless_t p = NULL;
-  p = xbt_new0(s_mc_pair_stateless_t, 1);
-  p->automaton_state = st;
-  p->graph_state = sg;
-  mc_stats_pair->expanded_pairs++;
-  return p;
-}
-
-
-int reached_stateless(mc_pair_stateless_t pair){
-
-  char* hash_reached = malloc(sizeof(char)*160);
-  unsigned int c= 0;
-
-  MC_SET_RAW_MEM;
-  char *hash = malloc(sizeof(char)*160);
-  xbt_sha((char *)&pair, hash);
-  xbt_dynar_foreach(reached_pairs, c, hash_reached){
-    if(strcmp(hash, hash_reached) == 0){
-      MC_UNSET_RAW_MEM;
-      return 1;
-    }
-  }
-  
-  MC_UNSET_RAW_MEM;
-  return 0;
-}
-
-void set_pair_stateless_reached(mc_pair_stateless_t pair){
-
-  if(reached_stateless(pair) == 0){
-    MC_SET_RAW_MEM;
-    char *hash = malloc(sizeof(char)*160) ;
-    xbt_sha((char *)&pair, hash);
-    xbt_dynar_push(reached_pairs, &hash); 
-    MC_UNSET_RAW_MEM;
-  }
-
-}
-
-
-void MC_ddfs_stateless_init(xbt_automaton_t a){
-
-  XBT_DEBUG("**************************************************");
-  XBT_DEBUG("Double-DFS stateless init");
-  XBT_DEBUG("**************************************************");
- 
-  mc_pair_stateless_t mc_initial_pair;
-  mc_state_t initial_graph_state;
-  smx_process_t process; 
- 
-  MC_wait_for_requests();
-
-  MC_SET_RAW_MEM;
-
-  initial_graph_state = MC_state_pair_new();
-  xbt_swag_foreach(process, simix_global->process_list){
-    if(MC_process_is_enabled(process)){
-      MC_state_interleave_process(initial_graph_state, process);
-    }
-  }
-
-  reached_pairs = xbt_dynar_new(sizeof(char *), NULL); 
-
-  MC_UNSET_RAW_MEM; 
-
-  /* regarder dans l'automate toutes les transitions activables grâce à l'état initial du système 
-    -> donnera les états initiaux de la propriété consistants avec l'état initial du système */
-
-  unsigned int cursor = 0;
-  unsigned int cursor2 = 0;
-  xbt_state_t state = NULL;
-  int res;
-  xbt_transition_t transition_succ;
-  xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
-  mc_pair_stateless_t pair_succ;
-
-  xbt_dynar_foreach(a->states, cursor, state){
-    if(state->type == -1){
-      xbt_dynar_foreach(state->out, cursor2, transition_succ){
-  	res = MC_automaton_evaluate_label(a, transition_succ->label);
+	XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
+	set_pair_reached(a, pair_succ->automaton_state, next_snapshot);
 	
-  	if((res == 1) || (res == 2)){
-	 
-  	  MC_SET_RAW_MEM;
-
-  	  mc_initial_pair = new_pair_stateless(initial_graph_state, transition_succ->dst);
-  	  xbt_dynar_push(successors, &mc_initial_pair);
-
-  	  MC_UNSET_RAW_MEM;
-
-	}
-      }
-    }
-  }
-
-  cursor = 0;
-
-  if(xbt_dynar_length(successors) == 0){
-    xbt_dynar_foreach(a->states, cursor, state){
-      if(state->type == -1){
 	MC_SET_RAW_MEM;
-
-	mc_initial_pair = new_pair_stateless(initial_graph_state, transition_succ->dst);
-	xbt_dynar_push(successors, &mc_initial_pair);
-	
+	xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
 	MC_UNSET_RAW_MEM;
-      }
-    }
-  }
-
-  cursor = 0;
-  xbt_dynar_foreach(successors, cursor, pair_succ){
-    MC_SET_RAW_MEM;
-
-    xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
-
-    /* Save the initial state */
-    initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
-    MC_take_snapshot(initial_snapshot);
-
-    MC_UNSET_RAW_MEM;
-
-    if(cursor == 0){
-      MC_ddfs_stateless(a, 0, 0);
-    }else{
-      MC_ddfs_stateless(a, 0, 1);
-    }
-  }  
-}
-
-
-void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){
-
- smx_process_t process = NULL;
-
-
-  if(xbt_fifo_size(mc_stack_liveness_stateless) == 0)
-    return;
-
-  /* Get current state */
-  mc_pair_stateless_t current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
-
-  XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateless), search_cycle);
-  XBT_DEBUG("Pair : 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));
-  
-
-  mc_stats_pair->visited_pairs++;
-
-  int value;
-  mc_state_t next_graph_state = NULL;
-  smx_req_t req = NULL;
-  char *req_str;
-
-  mc_pair_stateless_t pair_succ;
-  xbt_transition_t transition_succ;
-  unsigned int cursor;
-  int res;
-
-  xbt_dynar_t successors;
-
-  mc_pair_stateless_t next_pair;  
-  
-  while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
-
-    //XBT_DEBUG("Interleave size %u", MC_state_interleave_size(current_pair->graph_state));
-
-    /* Debug information */
-    if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
-      req_str = MC_request_to_string(req, value);
-      XBT_DEBUG("Execute: %s", req_str);
-      xbt_free(req_str);
-    }
-
-    //sleep(1);
-
-    MC_state_set_executed_request(current_pair->graph_state, req, value);   
-    
-    /* Answer the request */
-    SIMIX_request_pre(req, value);
-
-    /* Wait for requests (schedules processes) */
-    MC_wait_for_requests();
-
-
-    /* Create the new expanded graph_state */
-    MC_SET_RAW_MEM;
-
-    next_graph_state = MC_state_pair_new();
-    
-    /* Get enabled process and insert it in the interleave set of the next graph_state */
-    xbt_swag_foreach(process, simix_global->process_list){
-      if(MC_process_is_enabled(process)){
-	MC_state_interleave_process(next_graph_state, process);
-      }
-    }
-
-    successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
-      
-    MC_UNSET_RAW_MEM;
-
-    //xbt_dynar_reset(successors);
-    
-    cursor = 0;
-   
-    xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
+	
+	MC_ddfs_stateful(a, 1, 1);
 
-      res = MC_automaton_evaluate_label(a, transition_succ->label);
 
-      MC_SET_RAW_MEM;
-	
-      if((res == 1) || (res == 2)){ // enabled transition in automaton
-	next_pair = new_pair_stateless(next_graph_state, transition_succ->dst);
-	xbt_dynar_push(successors, &next_pair);
+	MC_SET_RAW_MEM;
+	xbt_dynar_pop(reached_pairs, NULL);
+	MC_UNSET_RAW_MEM;
       }
 
-      MC_UNSET_RAW_MEM;
     }
 
-   
-    if(xbt_dynar_length(successors) == 0){
-
-      MC_SET_RAW_MEM;
-      next_pair = new_pair_stateless(next_graph_state, current_pair->automaton_state);
-      xbt_dynar_push(successors, &next_pair);
+    if(MC_state_interleave_size(current_pair->graph_state) > 0){
+      XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateful));
+      MC_restore_snapshot(current_snapshot);
       MC_UNSET_RAW_MEM;
-	
     }
 
-    cursor = 0;
-
-    xbt_dynar_foreach(successors, cursor, pair_succ){
-
-      if((search_cycle == 1) && (reached_stateless(pair_succ) == 1)){
-	XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
-	XBT_INFO("|             ACCEPTANCE CYCLE            |");
-	XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
-	XBT_INFO("Counter-example that violates formula :");
-	MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
-	MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
-	MC_print_statistics_pairs(mc_stats_pair);
-	exit(0);
-      }
-	
-      mc_stats_pair->executed_transitions++;
- 
-      MC_SET_RAW_MEM;
-      xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
-      MC_UNSET_RAW_MEM;
-
-      
-
-      MC_ddfs_stateless(a, search_cycle, 0);
-
-      if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
-
-	set_pair_stateless_reached(current_pair);
-	XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
-	MC_replay_liveness(mc_stack_liveness_stateless);
-	MC_ddfs_stateless(a, 1, 1);
-
-      }
-    }
-    
-    if(MC_state_interleave_size(current_pair->graph_state) > 0){
-      XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateless));
-      MC_replay_liveness(mc_stack_liveness_stateless);
-    }
   }
 
   
   MC_SET_RAW_MEM;
-  xbt_fifo_shift(mc_stack_liveness_stateless);
+  xbt_fifo_shift(mc_stack_liveness_stateful);
   XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in stack", current_pair->graph_state, current_pair->automaton_state);
   MC_UNSET_RAW_MEM;
 
 }
-