X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/23a620e6c6df0a9023991f607cb93b71ed8f6065..df842dc41ca05e49bc585f7732df1849de91cac8:/src/mc/mc_dfs.c

diff --git a/src/mc/mc_dfs.c b/src/mc/mc_dfs.c
index 6f7102d6a7..246b21b3a3 100644
--- a/src/mc/mc_dfs.c
+++ b/src/mc/mc_dfs.c
@@ -1,15 +1,13 @@
 #include "private.h"
+#include "unistd.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dfs, mc,
                                 "Logging specific to MC DFS algorithm");
 
-
-extern xbt_fifo_t mc_snapshot_stack; 
-mc_pairs_t mc_reached = NULL;
 xbt_dynar_t initial_pairs = NULL;
 int max_pair = 0;
-xbt_dynar_t list_pairs_reached = NULL;
-extern mc_snapshot_t initial_snapshot;
+xbt_dynar_t visited_pairs;
+xbt_dynar_t reached_pairs;
 
 mc_pairs_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){
   mc_pairs_t p = NULL;
@@ -17,39 +15,113 @@ mc_pairs_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){
   p->system_state = sn;
   p->automaton_state = st;
   p->graph_state = sg;
-  p->visited = 0;
   p->num = max_pair;
   max_pair++;
   return p;
     
 }
 
-void set_pair_visited(mc_pairs_t p){
-  p->visited = 1;
+void set_pair_visited(mc_state_t gs, xbt_state_t as, int sc){
+
+  if(visited(gs, as, sc) == 0){
+    //XBT_DEBUG("New visited pair : graph=%p, automaton=%p", gs, as);
+    MC_SET_RAW_MEM;
+    mc_visited_pairs_t p = NULL;
+    p = xbt_new0(s_mc_visited_pairs_t, 1);
+    p->graph_state = gs;
+    p->automaton_state = as;
+    p->search_cycle = sc;
+    xbt_dynar_push(visited_pairs, &p);  
+    MC_UNSET_RAW_MEM;
+  }
+
+  //XBT_DEBUG("New visited pair , length of visited pairs : %lu", xbt_dynar_length(visited_pairs));
 }
 
-int pair_reached(xbt_dynar_t p, int num_pair){
-  int n;
-  unsigned int cursor = 0;
-  xbt_dynar_foreach(p, cursor, n){
-    if(n == num_pair)
-      return 1;
+int reached(mc_state_t gs, xbt_state_t as ){
+
+  mc_reached_pairs_t rp = NULL;
+  unsigned int c= 0;
+  unsigned int i;
+  int different_process;
+
+  MC_SET_RAW_MEM;
+  xbt_dynar_foreach(reached_pairs, c, rp){
+    if(rp->automaton_state == as){
+      different_process=0;
+      for(i=0; i < gs->max_pid; i++){
+	if(gs->proc_status[i].state != rp->graph_state->proc_status[i].state){
+	  different_process++;
+	}
+      }
+      if(different_process==0){
+	MC_UNSET_RAW_MEM;
+	return 1;
+      }
+    }
   }
+  MC_UNSET_RAW_MEM;
   return 0;
 }
 
-void MC_dfs_init(xbt_automaton_t a){
+void set_pair_reached(mc_state_t gs, xbt_state_t as){
+
+  if(reached(gs, as) == 0){
+    MC_SET_RAW_MEM;
+    mc_reached_pairs_t p = NULL;
+    p = xbt_new0(s_mc_reached_pairs_t, 1);
+    p->graph_state = gs;
+    p->automaton_state = as;
+    xbt_dynar_push(reached_pairs, &p); 
+    //XBT_DEBUG("New reached pair : graph=%p, automaton=%p", gs, as);
+    MC_UNSET_RAW_MEM;
+  }
+
+}
+
+int visited(mc_state_t gs, xbt_state_t as, int sc){
+  unsigned int c = 0;
+  mc_visited_pairs_t p = NULL;
+  unsigned int i;
+  int different_process;
+
+  MC_SET_RAW_MEM;
+  xbt_dynar_foreach(visited_pairs, c, p){
+    if((p->automaton_state == as) && (p->search_cycle == sc)){
+      different_process=0;
+      for(i=0; i < gs->max_pid; i++){
+	if(gs->proc_status[i].state != p->graph_state->proc_status[i].state){
+	  different_process++;
+	}
+      }
+      if(different_process==0){
+	MC_UNSET_RAW_MEM;
+	return 1;
+      }
+    }
+  }
+  MC_UNSET_RAW_MEM;
+  return 0;
+
+}
 
-  mc_pairs_t mc_initial_pair = NULL;
-  mc_state_t initial_graph_state = NULL;
-  smx_process_t process;
+void MC_dfs_init(xbt_automaton_t a){
 
+   XBT_DEBUG("**************************************************");
+   XBT_DEBUG("DFS init");
+   XBT_DEBUG("**************************************************");
+ 
+  mc_pairs_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;
 
-  initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
-  MC_take_snapshot(initial_snapshot);
+  init_snapshot = xbt_new0(s_mc_snapshot_t, 1);
+
   initial_graph_state = MC_state_new();
   xbt_swag_foreach(process, simix_global->process_list){
     if(MC_process_is_enabled(process)){
@@ -57,69 +129,369 @@ void MC_dfs_init(xbt_automaton_t a){
     }
   }
 
-  list_pairs_reached = xbt_dynar_new(sizeof(int), NULL); 
+  visited_pairs = xbt_dynar_new(sizeof(mc_visited_pairs_t), NULL); 
+  reached_pairs = xbt_dynar_new(sizeof(mc_reached_pairs_t), NULL); 
 
-  MC_UNSET_RAW_MEM;
+  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
+  /* 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;
-  xbt_state_t state = NULL;
   unsigned int cursor2 = 0;
+  xbt_state_t state = NULL;
   int res;
-  xbt_transition_t transition_succ = NULL;
-  xbt_dynar_t elses = xbt_dynar_new(sizeof(xbt_transition_t), NULL);
-  int enabled_transition = 0;
+  xbt_transition_t transition_succ;
+  xbt_dynar_t elses = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
+  xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
+  //  int enabled_transition = 0;
+  mc_pairs_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){
 	 
 	  MC_SET_RAW_MEM;
 
-	  mc_initial_pair = new_pair(initial_snapshot, initial_graph_state, transition_succ->dst);
-	  xbt_fifo_unshift(mc_snapshot_stack, mc_initial_pair);
-	  set_pair_visited(mc_initial_pair);
+	  mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
+	  xbt_dynar_push(successors, &mc_initial_pair);
 
-	  MC_UNSET_RAW_MEM;
-
-	  enabled_transition = 1;
+	  //XBT_DEBUG("New initial successor");
 
-	  XBT_DEBUG(" ++++++++++++++++++ new initial pair +++++++++++++++++++");
+	  MC_UNSET_RAW_MEM;
 
-	  MC_dfs(a, 0);
 	}else{
 	  if(res == 2){
-	    xbt_dynar_push(elses,&transition_succ);
+
+	    MC_SET_RAW_MEM;
+	    
+	    mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
+	    xbt_dynar_push(elses, &mc_initial_pair);
+
+	    //XBT_DEBUG("New initial successor");
+
+	    MC_UNSET_RAW_MEM;
 	  }
 	}
       }
     }
   }
 
-  if(enabled_transition == 0){
-    cursor2 = 0;
-    xbt_dynar_foreach(elses, cursor, transition_succ){
-    
+  if(xbt_dynar_length(successors) > 0){
+
+    cursor = 0;
+    xbt_dynar_foreach(successors, cursor, pair_succ){
       MC_SET_RAW_MEM;
 
-      mc_initial_pair = new_pair(initial_snapshot, initial_graph_state, transition_succ->dst);
-      xbt_fifo_unshift(mc_snapshot_stack, mc_initial_pair);
-      set_pair_visited(mc_initial_pair);
+      xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
+
+      XBT_DEBUG("**************************************************");
+      XBT_DEBUG("Initial state=%p ", pair_succ);
+
+      MC_UNSET_RAW_MEM; 
+
+      set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, 0);
+   
+      if(cursor == 0)
+	MC_dfs(a, 0, 0);
+      else
+	MC_dfs(a, 0, 1);
     
-      MC_UNSET_RAW_MEM;
+    } 
+
+  }else{
+
+    if(xbt_dynar_length(elses) > 0){
+      cursor = 0;
+      xbt_dynar_foreach(elses, cursor, pair_succ){
+	MC_SET_RAW_MEM;
+
+	xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
+
+	XBT_DEBUG("**************************************************");
+	XBT_DEBUG("Initial state=%p ", pair_succ);
+
+	MC_UNSET_RAW_MEM;  
+
+	set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, 0);
+
+	if(cursor == 0)
+	  MC_dfs(a, 0, 0);
+	else
+	  MC_dfs(a, 0, 1);
+      } 
+    }else{
+
+      XBT_DEBUG("No initial state !");
+
+      return;
+    }
+  }
+  
+}
+
+
+
+void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){
+
+
+  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;
+  }
+
+
+  //XBT_DEBUG("Lpv length after restore snapshot: %lu", xbt_dynar_length(visited_pairs));
+
+  /* Get current state */
+  mc_pairs_t current_pair = (mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
+
+  XBT_DEBUG("**************************************************");
+  XBT_DEBUG("State : graph=%p, automaton=%p, %u interleave, stack size=%d", current_pair->graph_state, current_pair->automaton_state, MC_state_interleave_size(current_pair->graph_state), xbt_fifo_size(mc_snapshot_stack));
+  //XBT_DEBUG("Restore : %d", restore);
+  
+
+  /* Update statistics */
+  //mc_stats->visited_states++;
+  //set_pair_visited(current_pair->graph_state, current_pair->automaton_state, search_cycle);
+  
+  //sleep(1);
+
+  smx_process_t process = NULL;
+  int value;
+  mc_state_t next_graph_state = NULL;
+  smx_req_t req = NULL;
+  char *req_str;
+
+  mc_pairs_t pair_succ;
+  xbt_transition_t transition_succ;
+  unsigned int cursor;
+  int res;
+  //int enabled_transition = 0;
+
+  xbt_dynar_t elses = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
+  xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pairs_t), NULL); 
+
+  mc_pairs_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){
+
+    //XBT_DEBUG("Current pair : %p (%u interleave)", current_pair, MC_state_interleave_size(current_pair->graph_state)+1);
+    //XBT_DEBUG("Visited pairs : %lu", xbt_dynar_length(visited_pairs));
+
+    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_dfs, xbt_log_priority_debug)){
+      req_str = MC_request_to_string(req, value);
+      XBT_DEBUG("Execute: %s", req_str);
+      xbt_free(req_str);
+    }
+
+    MC_state_set_executed_request(current_pair->graph_state, req, value);
+    //mc_stats->executed_transitions++;
+
+    /* 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_new();
     
-      MC_dfs(a, 0);
+    /* 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);
+      }
     }
+
+    next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
+    MC_take_snapshot(next_snapshot);
+      
+    MC_UNSET_RAW_MEM;
+
+    xbt_dynar_reset(elses);
+    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;
+      next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
+
+      //XBT_DEBUG("Next pair : %p", next_pair);
+	
+      if(res == 1){ // enabled transition in automaton
+	xbt_dynar_push(successors, &next_pair);   
+	//XBT_DEBUG("New Successors length : %lu", xbt_dynar_length(successors));
+      }else{
+	if(res == 2){
+	  xbt_dynar_push(elses, &next_pair);
+	  //XBT_DEBUG("New Elses length : %lu", xbt_dynar_length(elses));
+	}
+      }
+
+      MC_UNSET_RAW_MEM;
+    }
+
+   
+    if((xbt_dynar_length(successors) == 0) && (xbt_dynar_length(elses) == 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;
+	
+    }
+
+    //XBT_DEBUG("Successors length : %lu", xbt_dynar_length(successors));
+    //XBT_DEBUG("Elses length : %lu", xbt_dynar_length(elses));
+
+    if(xbt_dynar_length(successors) >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(visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle) == 0){
+
+	  MC_SET_RAW_MEM;
+	  xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
+	  MC_UNSET_RAW_MEM;
+
+	  set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle);
+	  MC_dfs(a, search_cycle, 0);
+
+	  if((search_cycle == 0) && (pair_succ->automaton_state->type == 1)){
+	    
+	    set_pair_reached(pair_succ->graph_state, pair_succ->automaton_state); 
+	    XBT_DEBUG("Acceptance state : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
+	    MC_dfs(a, 1, 0);
+
+	  }
+	}else{
+	  //XBT_DEBUG("Pair (graph=%p, automaton=%p) already visited !", pair_succ->graph_state, pair_succ->automaton_state );
+	  set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle);
+	}
+	
+      }
+    
+    }else{ 
+
+      cursor = 0;
+      xbt_dynar_foreach(elses, cursor, pair_succ){
+
+	//XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
+	
+	if(visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle) == 0){
+
+	  MC_SET_RAW_MEM;
+	  xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
+	  MC_UNSET_RAW_MEM;
+
+	  set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle);
+	  MC_dfs(a, search_cycle, 0);
+	    
+	  if((search_cycle == 0) && (pair_succ->automaton_state->type == 1)){
+
+	    set_pair_reached(pair_succ->graph_state, pair_succ->automaton_state); 
+	    XBT_DEBUG("Acceptance state : graph state=%p, automaton state=%p",pair_succ->graph_state, pair_succ->automaton_state);
+	    MC_dfs(a, 1, 0);
+
+	  }
+	}else{
+	  //XBT_DEBUG("Pair (graph=%p, automaton=%p) already visited !", pair_succ->graph_state, pair_succ->automaton_state );
+	  /* Different graph_state */
+	  set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle);
+	}
+    
+      }
+
+    }  
+
+    if(MC_state_interleave_size(current_pair->graph_state) > 0){
+      MC_restore_snapshot(current_snapshot);
+      MC_UNSET_RAW_MEM;
+      //XBT_DEBUG("Snapshot restored");
+    }      
+  }
+
+  if((search_cycle == 1) && (reached(current_pair->graph_state, current_pair->automaton_state) == 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);
+    exit(0);
   }
   
+  MC_SET_RAW_MEM;
+  xbt_fifo_shift(mc_snapshot_stack);
+  //XBT_DEBUG("State shifted in snapshot_stack, mc_snapshot_stack size=%d", xbt_fifo_size(mc_snapshot_stack));
+  MC_UNSET_RAW_MEM;
+
+}
+
+void MC_show_snapshot_stack(xbt_fifo_t stack){
+  int value;
+  mc_pairs_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_pairs_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);
+    }
+  }
+}
+
+void MC_dump_snapshot_stack(xbt_fifo_t stack){
+  mc_pairs_t pair;
+
+  MC_SET_RAW_MEM;
+  while ((pair = (mc_pairs_t) xbt_fifo_pop(stack)) != NULL)
+    MC_pair_delete(pair);
+  MC_UNSET_RAW_MEM;
+}
+
+void MC_pair_delete(mc_pairs_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 MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){
   
   switch(l->type){
@@ -237,137 +609,3 @@ int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){
 
   xbt_fifo_shift(stack_automaton_dfs);
   }*/
-
-
-void MC_dfs(xbt_automaton_t a, int search_cycle){
-
-  smx_process_t process = NULL;
-  int value;
-  mc_state_t next_graph_state = NULL;
-  smx_req_t req = NULL;
-  char *req_str;
-
-  xbt_transition_t transition_succ = NULL;
-  xbt_state_t successor = NULL;
-  unsigned int cursor = 0;
-  xbt_dynar_t elses = xbt_dynar_new(sizeof(xbt_transition_t), NULL);
-  int res;
-  int enabled_transition = 0;
-
-  mc_pairs_t next_pair = NULL;
-  mc_snapshot_t next_snapshot = NULL;
-  
-
-  /* Get current state */
-  mc_pairs_t current_pair = (mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
-
-  XBT_DEBUG("**************************************************");
-  XBT_DEBUG("State=%p, %u interleave",current_pair->graph_state,MC_state_interleave_size(current_pair->graph_state));
-  
-  /* Update statistics */
-  mc_stats->visited_states++;
-
-  MC_restore_snapshot(current_pair->system_state);
-  MC_UNSET_RAW_MEM;
-
-  //FIXME : vérifier condition permettant d'avoir tous les successeurs possibles dans le graph
-
-  while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
-    
-    /* Debug information */
-    if(XBT_LOG_ISENABLED(mc_dfs, xbt_log_priority_debug)){
-      req_str = MC_request_to_string(req, value);
-      XBT_DEBUG("Execute: %s", req_str);
-      xbt_free(req_str);
-    }
-
-    MC_state_set_executed_request(current_pair->graph_state, req, value);
-    mc_stats->executed_transitions++;
-
-    /* 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_new();
-    
-    /* Get an 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);
-      }
-    }
-
-    next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
-    MC_take_snapshot(next_snapshot);
-
-    MC_UNSET_RAW_MEM;
-
-    xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
-      successor = transition_succ->dst;
-      res = MC_automaton_evaluate_label(a, transition_succ->label);
-      if(res == 1){ // enabled transition 
-	
-	MC_SET_RAW_MEM;
-	next_pair = new_pair(next_snapshot, next_graph_state, successor);
-     
-	if((search_cycle == 1) && (pair_reached(list_pairs_reached, next_pair->num) == 1)){
-	  printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n");
-	  // afficher chemin menant au cycle d'acceptation
-	  exit(1);
-	}
-	if(next_pair->visited == 0){ // FIXME : tester avec search_cycle ?
-	  xbt_fifo_unshift(mc_snapshot_stack, next_pair);
-	  set_pair_visited(next_pair);
-	  MC_dfs(a, search_cycle);
-	  if((search_cycle == 0) && (next_pair->automaton_state->type == 1)){
-	    xbt_dynar_push(list_pairs_reached, &next_pair->num);
-	    MC_dfs(a, 1);
-	  }
-	}
-
-	MC_UNSET_RAW_MEM;
-	enabled_transition = 1;
-      }else{
-	if(res == 2){
-	  xbt_dynar_push(elses,&transition_succ);
-	}
-      }
-    }
-
-    if(enabled_transition == 0){
-      cursor = 0;
-      xbt_dynar_foreach(elses, cursor, transition_succ){
-	successor = transition_succ->dst;
-	MC_SET_RAW_MEM;
-	next_pair = new_pair(next_snapshot, next_graph_state, successor);
-	
-	if((search_cycle == 1) && (pair_reached(list_pairs_reached, next_pair->num) == 1)){
-	  printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n");
-	  // afficher chemin menant au cycle d'acceptation
-	  exit(1);
-	}
-	if(next_pair->visited == 0){ // FIXME : tester avec search_cycle ?
-	  xbt_fifo_unshift(mc_snapshot_stack, next_pair);
-	  set_pair_visited(next_pair);
-	  MC_dfs(a, search_cycle);
-	  if((search_cycle == 0) && (next_pair->automaton_state->type == 1)){
-	    xbt_dynar_push(list_pairs_reached, &next_pair->num);
-	    MC_dfs(a, 1);
-	  }
-	}
-
-	MC_UNSET_RAW_MEM;
-      }
-    }
-    
-  }
-
-  xbt_fifo_shift(mc_snapshot_stack);
-
-}