X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/4b6daec896cfa8220c801d9c7dcf2af7eedcbff0..403e0e03205591d9b723d0f032fe9b72651066b4:/src/mc/mc_liveness.c

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 9b92e214cb..c693825661 100644
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -5,80 +5,137 @@ 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_fifo_t reached_pairs;
+xbt_dynar_t successors = NULL;
+extern mc_snapshot_t initial_snapshot;
 
-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 snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
 
+  XBT_DEBUG("Compare snapshot");
+  
+  if(s1->num_reg != s2->num_reg){
+    XBT_DEBUG("Different num_reg");
+    return 1;
+  }
 
-int reached(mc_pair_t pair){
-
-  char* hash_reached = malloc(sizeof(char)*160);
-  unsigned int c= 0;
+  int i;
+  int 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){
+      XBT_DEBUG("Different size of region");
+      return 1;
+    }
+    
+    if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
+      XBT_DEBUG("Different start addr of region");
+      return 1;
+    }
+    
+    if(s1->regions[i]->type != s2->regions[i]->type){
+      XBT_DEBUG("Different type of region");
       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)");
+	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 or program");
+    	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(xbt_fifo_size(reached_pairs) == 0){
+
+    return 0;
+
+  }else{
 
-  if(reached(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;
-  }
+    
+    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);
+    }
+
+
+
+    int i=0;
+    xbt_fifo_item_t item = xbt_fifo_get_first_item(reached_pairs);
+    mc_pair_reached_t pair_test = NULL;
+
+    while(i < xbt_fifo_size(reached_pairs)){
+
+      pair_test = (mc_pair_reached_t) xbt_fifo_get_item_content(item);
+      
+      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(s, pair_test->system_state) == 0){
+	    MC_UNSET_RAW_MEM;
+	    return 1;
+	  }
+	}
+      }
+
+      item = xbt_fifo_get_next_item(item);
+      
+      i++;
 
-void MC_show_snapshot_stack(xbt_fifo_t stack){
-  int value;
-  mc_pair_t pair;
-  xbt_fifo_item_t item;
-  smx_req_t req;
-  char *req_str = NULL;
-  
-  for (item = xbt_fifo_get_last_item(stack);
-       (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item)))
-        : (NULL)); item = xbt_fifo_get_prev_item(item)) {
-    req = MC_state_get_executed_request(pair->graph_state, &value);
-    if(req){
-      req_str = MC_request_to_string(req, value);
-      XBT_INFO("%s", req_str);
-      xbt_free(req_str);
     }
+
+    MC_UNSET_RAW_MEM;
+    return 0;
+    
   }
 }
 
-void MC_dump_snapshot_stack(xbt_fifo_t stack){
-  mc_pair_t pair;
+void set_pair_reached(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t sn){
 
+ 
   MC_SET_RAW_MEM;
-  while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
-    MC_pair_delete(pair);
+  
+  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_fifo_unshift(reached_pairs, pair); 
+  
   MC_UNSET_RAW_MEM;
+  
+  
 }
 
 void MC_pair_delete(mc_pair_t pair){
@@ -89,6 +146,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){
@@ -132,66 +190,41 @@ 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, int r){
+  mc_pair_stateless_t p = NULL;
+  p = xbt_new0(s_mc_pair_stateless_t, 1);
+  p->automaton_state = st;
+  p->graph_state = sg;
+  p->requests = r;
+  mc_stats_pair->expanded_pairs++;
+  return p;
 }
 
-
-void MC_vddfs_with_restore_snapshot_init(xbt_automaton_t a){
+void MC_ddfs_stateless_init(xbt_automaton_t a, char *prgm){
 
   XBT_DEBUG("**************************************************");
-  XBT_DEBUG("Double-DFS with visited state and restore snapshot 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)){
@@ -199,94 +232,69 @@ void MC_vddfs_with_restore_snapshot_init(xbt_automaton_t a){
     }
   }
 
-  visited_pairs = xbt_dynar_new(sizeof(char *), NULL); 
-  reached_pairs = xbt_dynar_new(sizeof(char *), NULL); 
+  reached_pairs = xbt_fifo_new(); 
+  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_liveness(initial_snapshot, prgm);
 
   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, MC_state_interleave_size(initial_graph_state));
+      xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
+      MC_UNSET_RAW_MEM;
+      
+      if(cursor != 0){
+	MC_restore_snapshot(initial_snapshot);
+	MC_UNSET_RAW_MEM;
       }
-    }
-  }
 
-  cursor = 0;
+      MC_ddfs_stateless(a, 0, 0, prgm);
 
-  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_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
+	xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
+	MC_UNSET_RAW_MEM;
 
-	mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
-	xbt_dynar_push(successors, &mc_initial_pair);
+	set_pair_reached(a, state, initial_snapshot);
+	
+	if(cursor != 0){
+	  MC_restore_snapshot(initial_snapshot);
+	  MC_UNSET_RAW_MEM;
+	}
+	
+	MC_ddfs_stateless(a, 1, 0, prgm);
 	
-	MC_UNSET_RAW_MEM;
       }
     }
-  }
-
-  cursor = 0;
-  xbt_dynar_foreach(successors, cursor, pair_succ){
-    MC_SET_RAW_MEM;
+  } 
 
-    xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
-    set_pair_visited(pair_succ, 0);
-
-    MC_UNSET_RAW_MEM;
-
-    if(cursor == 0){
-      MC_vddfs_with_restore_snapshot(a, 0, 0);
-    }else{
-      MC_vddfs_with_restore_snapshot(a, 0, 1);
-    }
-  }  
 }
 
 
-void MC_vddfs_with_restore_snapshot(xbt_automaton_t a, int search_cycle, int restore){
+void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *prgm){
 
-  smx_process_t process = NULL;
+  smx_process_t process;
+  mc_pair_stateless_t current_pair = NULL;
+  mc_snapshot_t snapshot = NULL;
 
-
-  if(xbt_fifo_size(mc_snapshot_stack) == 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_snapshot_stack)))->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_snapshot_stack));
-
-  if(restore==1){
+  if(replay == 1){
+    MC_replay_liveness(mc_stack_liveness_stateless, 0);
+    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);
@@ -294,10 +302,16 @@ void MC_vddfs_with_restore_snapshot(xbt_automaton_t a, int search_cycle, int res
     }
   }
 
-  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;
@@ -305,420 +319,299 @@ void MC_vddfs_with_restore_snapshot(xbt_automaton_t a, int search_cycle, int res
   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_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){
+  if(xbt_fifo_size(mc_stack_liveness_stateless) < MAX_DEPTH_LIVENESS){
 
-    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("Execute: %s", req_str);
-      xbt_free(req_str);
-    }
+    if(current_pair->requests > 0){
 
-    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;
+      while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
+   
+	/* 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);
+	}
 
-    next_graph_state = MC_state_pair_new();
+	MC_state_set_executed_request(current_pair->graph_state, req, value);   
     
-    /* 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);
-      }
-    }
+	/* Answer the request */
+	SIMIX_request_pre(req, value);
 
-    next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
-    MC_take_snapshot(next_snapshot);
-      
-    MC_UNSET_RAW_MEM;
+	/* Wait for requests (schedules processes) */
+	MC_wait_for_requests();
 
-    xbt_dynar_reset(successors);
-    
-    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;
 
-      MC_SET_RAW_MEM;
-	
-      if((res == 1) || (res == 2)){ // enabled transition in automaton
-	next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
-	xbt_dynar_push(successors, &next_pair);
-      }
+	/* Create the new expanded graph_state */
+	next_graph_state = MC_state_pair_new();
 
-      MC_UNSET_RAW_MEM;
-    }
+	/* 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);
+	  }
+	}
 
-   
-    if(xbt_dynar_length(successors) == 0){
+	xbt_dynar_reset(successors);
 
-      MC_SET_RAW_MEM;
-      next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state);
-      xbt_dynar_push(successors, &next_pair);
-      MC_UNSET_RAW_MEM;
-	
-    }
+	MC_UNSET_RAW_MEM;
 
 
-    cursor = 0;
-    xbt_dynar_foreach(successors, cursor, pair_succ){
+	cursor= 0;
+	xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 
-      //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
+	  res = MC_automaton_evaluate_label(a, transition_succ->label);
 
-      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_snapshot_stack(mc_snapshot_stack);
-	MC_dump_snapshot_stack(mc_snapshot_stack);
-	MC_print_statistics_pairs(mc_stats_pair);
-	exit(0);
-      }
-	
-      if(visited(pair_succ, search_cycle) == 0){
+	  if(res == 1){ // enabled transition in automaton
+	    MC_SET_RAW_MEM;
+	    next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
+	    xbt_dynar_push(successors, &next_pair);
+	    MC_UNSET_RAW_MEM;
+	  }
 
-	mc_stats_pair->executed_transitions++;
- 
-	MC_SET_RAW_MEM;
-	xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
-	set_pair_visited(pair_succ, search_cycle);
-	MC_UNSET_RAW_MEM;
+	}
 
-	MC_vddfs_with_restore_snapshot(a, search_cycle, 0);
+	cursor = 0;
+   
+	xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
+      
+	  res = MC_automaton_evaluate_label(a, transition_succ->label);
+	
+	  if(res == 2){ // true transition in automaton
+	    MC_SET_RAW_MEM;
+	    next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
+	    xbt_dynar_push(successors, &next_pair);
+	    MC_UNSET_RAW_MEM;
+	  }
 
-	if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
+	}
 
-	  MC_restore_snapshot(current_pair->system_state);
+   
+	if(xbt_dynar_length(successors) == 0){
+	  MC_SET_RAW_MEM;
+	  next_pair = new_pair_stateless(next_graph_state, current_pair->automaton_state, MC_state_interleave_size(next_graph_state));
+	  xbt_dynar_push(successors, &next_pair);
 	  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_with_restore_snapshot(a, 1, 1);
-
 	}
-      }else{
 
-	XBT_DEBUG("Pair already visited !");
+	cursor = 0; 
 
-      }
-    }
-    
-    
-    if(MC_state_interleave_size(current_pair->graph_state) > 0){
-      MC_restore_snapshot(current_snapshot);
-      MC_UNSET_RAW_MEM;
-    }
-  }
+	xbt_dynar_foreach(successors, cursor, pair_succ){
 
-  
-  MC_SET_RAW_MEM;
-  xbt_fifo_shift(mc_snapshot_stack);
-  XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in snapshot_stack", current_pair->graph_state, current_pair->automaton_state);
-  MC_UNSET_RAW_MEM;
+	  if(search_cycle == 1){
 
-}
+	    if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
+		      
+	      MC_SET_RAW_MEM;
+	      snapshot = xbt_new0(s_mc_snapshot_t, 1);
+	      MC_take_snapshot_liveness(snapshot, prgm);
+	      MC_UNSET_RAW_MEM;
 
+	      if(reached(a, pair_succ->automaton_state, snapshot) == 1){
 
+		XBT_DEBUG("Next pair (depth = %d, %d interleave) already reached !", xbt_fifo_size(mc_stack_liveness_stateless) + 1, MC_state_interleave_size(pair_succ->graph_state));
 
-/********************* Double-DFS without visited state *******************/
+		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);
 
+	      }else{
 
-void MC_ddfs_with_restore_snapshot_init(xbt_automaton_t a){
+		XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness_stateless) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
+	      
+		set_pair_reached(a, pair_succ->automaton_state, snapshot); 
 
-  XBT_DEBUG("**************************************************");
-  XBT_DEBUG("Double-DFS without visited state and with restore snapshot init");
-  XBT_DEBUG("**************************************************");
- 
-  mc_pair_t mc_initial_pair;
-  mc_state_t initial_graph_state;
-  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);
+	  }else{
+	  
+	    if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 
-  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);
-    }
-  }
+	      XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness_stateless) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
 
-  reached_pairs = xbt_dynar_new(sizeof(char *), NULL); 
+	      MC_SET_RAW_MEM;
+	      snapshot = xbt_new0(s_mc_snapshot_t, 1);
+	      MC_take_snapshot_liveness(snapshot, prgm);
+	      MC_UNSET_RAW_MEM;
+	    
+	      set_pair_reached(a, pair_succ->automaton_state, snapshot); 
+	      
+	      search_cycle = 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 */
+	  MC_SET_RAW_MEM;
+	  xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
+	  MC_UNSET_RAW_MEM;
 
-  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;
+	  MC_ddfs_stateless(a, search_cycle, 0, prgm);
 
-  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);
+	  /* Restore system before checking others successors */
+	  if(cursor != (xbt_dynar_length(successors) - 1))
+	    MC_replay_liveness(mc_stack_liveness_stateless, 1);
 	
-  	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;
-
 	}
-      }
-    }
-  }
-
-  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;
+	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, 0);
+	}
       }
-    }
-  }
-
-  cursor = 0;
-  xbt_dynar_foreach(successors, cursor, pair_succ){
-    MC_SET_RAW_MEM;
 
-    xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
-
-    MC_UNSET_RAW_MEM;
-
-    if(cursor == 0){
-      MC_ddfs_with_restore_snapshot(a, 0, 0);
-    }else{
-      MC_ddfs_with_restore_snapshot(a, 0, 1);
-    }
-  }  
-}
+ 
+    }else{  /*No request to execute, search evolution in Büchi automaton */
 
+      MC_SET_RAW_MEM;
 
-void MC_ddfs_with_restore_snapshot(xbt_automaton_t a, int search_cycle, int restore){
+      /* Create the new expanded graph_state */
+      next_graph_state = MC_state_pair_new();
 
-  smx_process_t process = NULL;
+      xbt_dynar_reset(successors);
 
+      MC_UNSET_RAW_MEM;
 
-  if(xbt_fifo_size(mc_snapshot_stack) == 0)
-    return;
 
-  if(restore == 1){
-    MC_restore_snapshot(((mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)))->system_state);
-    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);
 
-  /* Get current state */
-  mc_pair_t current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
+	if(res == 1){ // enabled transition in automaton
+	  MC_SET_RAW_MEM;
+	  next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
+	  xbt_dynar_push(successors, &next_pair);
+	  MC_UNSET_RAW_MEM;
+	}
 
-  if(restore==1){
-    xbt_swag_foreach(process, simix_global->process_list){
-      if(MC_process_is_enabled(process)){
-	MC_state_interleave_process(current_pair->graph_state, process);
       }
-    }
-  }
-
-  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));
-  
 
-  mc_stats_pair->visited_pairs++;
-
-  int value;
-  mc_state_t next_graph_state = NULL;
-  smx_req_t req = NULL;
-  char *req_str;
-
-  mc_pair_t pair_succ;
-  xbt_transition_t transition_succ;
-  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;
-  
-  
-  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;
+      cursor = 0;
    
-    
-    /* 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);
-    }
+      xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
+      
+	res = MC_automaton_evaluate_label(a, transition_succ->label);
+	
+	if(res == 2){ // true transition in automaton
+	  MC_SET_RAW_MEM;
+	  next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
+	  xbt_dynar_push(successors, &next_pair);
+	  MC_UNSET_RAW_MEM;
+	}
 
-    MC_state_set_executed_request(current_pair->graph_state, req, value);
+      }
 
-    /* Answer the request */
-    SIMIX_request_pre(req, value);
+   
+      if(xbt_dynar_length(successors) == 0){
+	MC_SET_RAW_MEM;
+	next_pair = new_pair_stateless(next_graph_state, current_pair->automaton_state, MC_state_interleave_size(next_graph_state));
+	xbt_dynar_push(successors, &next_pair);
+	MC_UNSET_RAW_MEM;
+      }
 
-    /* Wait for requests (schedules processes) */
-    MC_wait_for_requests();
+      cursor = 0; 
 
+      xbt_dynar_foreach(successors, cursor, pair_succ){
 
-    /* Create the new expanded graph_state */
-    MC_SET_RAW_MEM;
+	if(search_cycle == 1){
 
-    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);
-      }
-    }
+	  if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
 
-    next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
-    MC_take_snapshot(next_snapshot);
-      
-    MC_UNSET_RAW_MEM;
+	    MC_SET_RAW_MEM;
+	    snapshot = xbt_new0(s_mc_snapshot_t, 1);
+	    MC_take_snapshot_liveness(snapshot, prgm);
+	    MC_UNSET_RAW_MEM;
+	
+	    if(reached(a, pair_succ->automaton_state, snapshot) == 1){
 
-    xbt_dynar_reset(successors);
-    
-    cursor = 0;
-    xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
+	      XBT_DEBUG("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness_stateless) + 1);
 
-      res = MC_automaton_evaluate_label(a, transition_succ->label);
+	      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_SET_RAW_MEM;
-	
-      if((res == 1) || (res == 2)){ // enabled transition in automaton
-	next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
-	xbt_dynar_push(successors, &next_pair);
-      }
+	    }else{
 
-      MC_UNSET_RAW_MEM;
-    }
+	      XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness_stateless) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
+	      
+	      set_pair_reached(a, pair_succ->automaton_state, snapshot); 
 
-   
-    if(xbt_dynar_length(successors) == 0){
+	    }
 
-      MC_SET_RAW_MEM;
-      next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state);
-      xbt_dynar_push(successors, &next_pair);
-      MC_UNSET_RAW_MEM;
-	
-    }
+	  }
 
+	}else{
+	  
+	  if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)) && (xbt_fifo_size(mc_stack_liveness_stateless) < (MAX_DEPTH_LIVENESS - 1))){
 
-    cursor = 0;
-    xbt_dynar_foreach(successors, cursor, pair_succ){
+	    MC_SET_RAW_MEM;
+	    snapshot = xbt_new0(s_mc_snapshot_t, 1);
+	    MC_take_snapshot_liveness(snapshot, prgm);
+	    MC_UNSET_RAW_MEM;
+	    
+	    set_pair_reached(a, pair_succ->automaton_state, snapshot); 
+	    	    
+	    search_cycle = 1;
 
-      //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_snapshot_stack(mc_snapshot_stack);
-	MC_dump_snapshot_stack(mc_snapshot_stack);
-	MC_print_statistics_pairs(mc_stats_pair);
-	exit(0);
-      }
-	
-      mc_stats_pair->executed_transitions++;
- 
-      MC_SET_RAW_MEM;
-      xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
-      MC_UNSET_RAW_MEM;
+	}
 
-      MC_ddfs_with_restore_snapshot(a, search_cycle, 0);
+	MC_SET_RAW_MEM;
+	xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
+	MC_UNSET_RAW_MEM;
 
-      if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
+	MC_ddfs_stateless(a, search_cycle, 0, prgm);
 
-	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_with_restore_snapshot(a, 1, 1);
+	/* Restore system before checking others successors */
+	if(cursor != xbt_dynar_length(successors) - 1)
+	  MC_replay_liveness(mc_stack_liveness_stateless, 1);
 
       }
-    }
-    
-    
-    if(MC_state_interleave_size(current_pair->graph_state) > 0){
-      MC_restore_snapshot(current_snapshot);
-      MC_UNSET_RAW_MEM;
+     
     }
   }
 
+  if(xbt_fifo_size(mc_stack_liveness_stateless) == MAX_DEPTH_LIVENESS ){
+    XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u) shifted in stack, maximum depth reached", current_pair->graph_state, current_pair->automaton_state, search_cycle);
+  }else{
+    XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle);
+  }
+
   
   MC_SET_RAW_MEM;
-  xbt_fifo_shift(mc_snapshot_stack);
-  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);
+  if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
+    xbt_fifo_shift(reached_pairs);
+  }
+  if(snapshot != NULL)
+    MC_free_snapshot(snapshot);
   MC_UNSET_RAW_MEM;
 
+  MC_pair_stateless_delete(current_pair);
+
+  /* FIXME : free memory (pair, snapshot)*/
+
 }