X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/c6189d1b7b02cda083791afc98f7e632100424d5..c12f31e0bf110c61b506ef20c1d4de6b2cd2db87:/src/mc/mc_liveness.c

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 778c88e9ba..424929e3e7 100644
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -1,4 +1,4 @@
-/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved.            */
+/* Copyright (c) 2011-2013 Da SimGrid Team. All rights reserved.            */
 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
@@ -10,399 +10,425 @@
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
                                 "Logging specific to algorithms for liveness properties verification");
 
-xbt_dynar_t reached_pairs;
+/********* Global variables *********/
+
+xbt_dynar_t acceptance_pairs;
 xbt_dynar_t visited_pairs;
 xbt_dynar_t successors;
 
-int create_dump(int pair)
-{
-   // Try to enable core dumps
-  struct rlimit core_limit;
-  core_limit.rlim_cur = RLIM_INFINITY;
-  core_limit.rlim_max = RLIM_INFINITY;
-  
-  if(setrlimit(RLIMIT_CORE, &core_limit) < 0)
-    fprintf(stderr, "setrlimit: %s\nWarning: core dumps may be truncated or non-existant\n", strerror(errno));
-  
-  int status;
-  switch(fork()){
-  case 0:
-    // We are the child process -- run the actual program
-    xbt_abort();
-    break;
-    
-  case -1:
-    // An error occurred, shouldn't happen
-    perror("fork");
-    return -1;
-    
-  default:
-    // We are the parent process -- wait for the child process to exit
-    if(wait(&status) < 0)
-      perror("wait");
-    if(WIFSIGNALED(status) && WCOREDUMP(status)){
-      char *core_name = malloc(20);
-      sprintf(core_name,"core_%d", pair); 
-      rename("core", core_name);
-      free(core_name);
-    }
-  }
-
-  return 0;
-}
-
-void MC_print_comparison_times_statistics(mc_comparison_times_t ct){
-
-  XBT_DEBUG("Comparisons done : %d", ct->nb_comparisons);
-  
-  double total, min, max;
-  unsigned int cursor;
-  
-  if(xbt_dynar_length(ct->chunks_used_comparison_times) > 0){
-    cursor = 0;
-    total = 0.0;
-    max = 0.0;
-    min = xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double);
-    while(cursor < xbt_dynar_length(ct->chunks_used_comparison_times) - 1){
-      total += xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double);
-      if(xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double) > max)
-        max = xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double);
-      if(xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double) < min)
-        min = xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double);
-      cursor++;
-    }
-    XBT_DEBUG("Chunks used comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->chunks_used_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->chunks_used_comparison_times), max, min);
-  }
-
-  if(xbt_dynar_length(ct->stacks_sizes_comparison_times) > 0){
-    cursor = 0;
-    total = 0.0;
-    max = 0.0;
-    min = xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double);
-    while(cursor < xbt_dynar_length(ct->stacks_sizes_comparison_times) - 1){
-      total += xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double);
-      if(xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double) > max)
-        max = xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double);
-      if(xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double) < min)
-        min = xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double);
-      cursor++;
-    }
-    XBT_DEBUG("Stacks sizes comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->stacks_sizes_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->stacks_sizes_comparison_times), max, min);
-  }
-
-  if(xbt_dynar_length(ct->program_data_segment_comparison_times) > 0){
-    cursor = 0;
-    total = 0.0;
-    max = 0.0;
-    min = xbt_dynar_get_as(ct->program_data_segment_comparison_times, cursor, double);
-    while(cursor < xbt_dynar_length(ct->program_data_segment_comparison_times) - 1){
-      total += xbt_dynar_get_as(ct->program_data_segment_comparison_times, cursor, double);
-      if(xbt_dynar_get_as(ct->program_data_segment_comparison_times, cursor, double) > max)
-        max = xbt_dynar_get_as(ct->program_data_segment_comparison_times, cursor, double);
-      if(xbt_dynar_get_as(ct->program_data_segment_comparison_times, cursor, double) < min)
-        min = xbt_dynar_get_as(ct->program_data_segment_comparison_times, cursor, double);
-      cursor++;
-    }
-    XBT_DEBUG("Program data/bss segments comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->program_data_segment_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->program_data_segment_comparison_times), max, min);
-  }
-
-  if(xbt_dynar_length(ct->libsimgrid_data_segment_comparison_times) > 0){
-    cursor = 0;
-    total = 0.0;
-    max = 0.0;
-    min = xbt_dynar_get_as(ct->libsimgrid_data_segment_comparison_times, cursor, double);
-    while(cursor < xbt_dynar_length(ct->libsimgrid_data_segment_comparison_times) - 1){
-      total += xbt_dynar_get_as(ct->libsimgrid_data_segment_comparison_times, cursor, double);
-      if(xbt_dynar_get_as(ct->libsimgrid_data_segment_comparison_times, cursor, double) > max)
-        max = xbt_dynar_get_as(ct->libsimgrid_data_segment_comparison_times, cursor, double);
-      if(xbt_dynar_get_as(ct->libsimgrid_data_segment_comparison_times, cursor, double) < min)
-        min = xbt_dynar_get_as(ct->libsimgrid_data_segment_comparison_times, cursor, double);
-      cursor++;
-    }
-    XBT_DEBUG("Libsimgrid data/bss segments comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->libsimgrid_data_segment_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->libsimgrid_data_segment_comparison_times), max, min);
-  }
-
-  if(xbt_dynar_length(ct->heap_comparison_times) > 0){
-    cursor = 0;
-    total = 0.0;
-    max = 0.0;
-    min = xbt_dynar_get_as(ct->heap_comparison_times, cursor, double);
-    while(cursor < xbt_dynar_length(ct->heap_comparison_times) - 1){
-      total += xbt_dynar_get_as(ct->heap_comparison_times, cursor, double);
-      if(xbt_dynar_get_as(ct->heap_comparison_times, cursor, double) > max)
-        max = xbt_dynar_get_as(ct->heap_comparison_times, cursor, double);
-      if(xbt_dynar_get_as(ct->heap_comparison_times, cursor, double) < min)
-        min = xbt_dynar_get_as(ct->heap_comparison_times, cursor, double);
-      cursor++;
-    }
-    XBT_DEBUG("Heap comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->heap_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->heap_comparison_times), max, min);
-  }
-
-  if(xbt_dynar_length(ct->stacks_comparison_times) > 0){
-    cursor = 0;
-    total = 0.0;
-    max = 0.0;
-    min = xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double);
-    while(cursor < xbt_dynar_length(ct->stacks_comparison_times) - 1){
-      total += xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double);
-      if(xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double) > max)
-        max = xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double);
-      if(xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double) < min)
-        min = xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double);
-      cursor++;
-    }
-    XBT_DEBUG("Stacks comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->stacks_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->stacks_comparison_times), max, min);
-  }
-
-  if(xbt_dynar_length(ct->snapshot_comparison_times) > 0){
-    cursor = 0;
-    total = 0.0;
-    max = 0.0;
-    min = xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double);
-    while(cursor < xbt_dynar_length(ct->snapshot_comparison_times) - 1){
-      total += xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double);
-      if(xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double) > max)
-        max = xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double);
-      if(xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double) < min)
-        min = xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double);
-      cursor++;
-    }
-    XBT_DEBUG("Snapshot comparison (Whole funnel) -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->snapshot_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->snapshot_comparison_times), max, min);
-  }
-
-}
-
-mc_comparison_times_t new_comparison_times(){
-  mc_comparison_times_t ct = NULL;
-  ct = xbt_new0(s_mc_comparison_times_t, 1);
-  ct->nb_comparisons = 0;
-  ct->snapshot_comparison_times = xbt_dynar_new(sizeof(double), NULL);
-  ct->chunks_used_comparison_times = xbt_dynar_new(sizeof(double), NULL);
-  ct->stacks_sizes_comparison_times = xbt_dynar_new(sizeof(double), NULL);
-  ct->program_data_segment_comparison_times = xbt_dynar_new(sizeof(double), NULL);
-  ct->libsimgrid_data_segment_comparison_times = xbt_dynar_new(sizeof(double), NULL);
-  ct->heap_comparison_times = xbt_dynar_new(sizeof(double), NULL);
-  ct->stacks_comparison_times = xbt_dynar_new(sizeof(double), NULL);
-  return ct;
-}
 
-int reached(xbt_state_t st){
+/********* Static functions *********/
 
-  raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+static mc_acceptance_pair_t acceptance_pair_new(int num, xbt_automaton_state_t as){
 
-  MC_SET_RAW_MEM;
-
-  mc_pair_reached_t new_pair = NULL;
-  new_pair = xbt_new0(s_mc_pair_reached_t, 1);
-  new_pair->nb = xbt_dynar_length(reached_pairs) + 1;
-  new_pair->automaton_state = st;
+  mc_acceptance_pair_t new_pair = NULL;
+  new_pair = xbt_new0(s_mc_acceptance_pair_t, 1);
+  new_pair->num = num;
+  new_pair->automaton_state = as;
   new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
-  new_pair->comparison_times = new_comparison_times();
-  new_pair->system_state = MC_take_snapshot_liveness();  
+  new_pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
+  new_pair->nb_processes = xbt_swag_size(simix_global->process_list);
+  new_pair->system_state = MC_take_snapshot();  
   
   /* Get values of propositional symbols */
   int res;
   int_f_void_t f;
   unsigned int cursor = 0;
-  xbt_propositional_symbol_t ps = NULL;
+  xbt_automaton_propositional_symbol_t ps = NULL;
   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
     f = (int_f_void_t)ps->function;
-    res = (*f)();
+    res = f();
     xbt_dynar_push_as(new_pair->prop_ato, int, res);
   }
-  
+
+  return new_pair;
+
+}
+
+static int is_reached_acceptance_pair(int num, xbt_automaton_state_t as){
+
+  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+  MC_SET_RAW_MEM;
+  mc_acceptance_pair_t new_pair = acceptance_pair_new(num, as);  
   MC_UNSET_RAW_MEM;
   
-  if(xbt_dynar_is_empty(reached_pairs)/* || !compare*/){
+  if(xbt_dynar_is_empty(acceptance_pairs)){
 
     MC_SET_RAW_MEM;
-    /* New pair reached */
-    xbt_dynar_push(reached_pairs, &new_pair); 
+    xbt_dynar_push(acceptance_pairs, &new_pair); 
     MC_UNSET_RAW_MEM;
 
     if(raw_mem_set)
       MC_SET_RAW_MEM;
- 
-    return 0;
+
+    return -1;
 
   }else{
 
     MC_SET_RAW_MEM;
     
-    cursor = 0;
-    mc_pair_reached_t pair_test = NULL;
-     
-    xbt_dynar_foreach(reached_pairs, cursor, pair_test){
-      if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug))
-        XBT_DEBUG("****** Pair reached #%d ******", pair_test->nb);
-      if(automaton_state_compare(pair_test->automaton_state, st) == 0){
-        if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
-          if(snapshot_compare(new_pair->system_state, pair_test->system_state, new_pair->comparison_times, pair_test->comparison_times) == 0){
-            
-            if(raw_mem_set)
-              MC_SET_RAW_MEM;
-            else
-              MC_UNSET_RAW_MEM;
-            
-            return 1;
-          }       
-        }else{
-          XBT_INFO("Different values of propositional symbols");
+    size_t current_bytes_used = new_pair->heap_bytes_used;
+    int current_nb_processes = new_pair->nb_processes;
+
+    unsigned int cursor = 0;
+    int previous_cursor = 0, next_cursor = 0;
+    int start = 0;
+    int end = xbt_dynar_length(acceptance_pairs) - 1;
+
+    mc_acceptance_pair_t pair_test = NULL;
+    size_t bytes_used_test;
+    int nb_processes_test;
+    int same_processes_and_bytes_not_found = 1;
+
+    while(start <= end && same_processes_and_bytes_not_found){
+      cursor = (start + end) / 2;
+      pair_test = (mc_acceptance_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_acceptance_pair_t);
+      bytes_used_test = pair_test->heap_bytes_used;
+      nb_processes_test = pair_test->nb_processes;
+      if(nb_processes_test < current_nb_processes)
+        start = cursor + 1;
+      if(nb_processes_test > current_nb_processes)
+        end = cursor - 1; 
+      if(nb_processes_test == current_nb_processes){
+        if(bytes_used_test < current_bytes_used)
+          start = cursor + 1;
+        if(bytes_used_test > current_bytes_used)
+          end = cursor - 1;
+        if(bytes_used_test == current_bytes_used){
+          same_processes_and_bytes_not_found = 0;
+          if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){
+            if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
+              if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
+                if(raw_mem_set)
+                  MC_SET_RAW_MEM;
+                else
+                  MC_UNSET_RAW_MEM;
+                return pair_test->num;
+              }
+            }
+          }
+          /* Search another pair with same number of bytes used in std_heap */
+          previous_cursor = cursor - 1;
+          while(previous_cursor >= 0){
+            pair_test = (mc_acceptance_pair_t)xbt_dynar_get_as(acceptance_pairs, previous_cursor, mc_acceptance_pair_t);
+            bytes_used_test = pair_test->system_state->heap_bytes_used;
+            if(bytes_used_test != current_bytes_used)
+              break;
+            if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){
+              if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){  
+                if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
+                  if(raw_mem_set)
+                    MC_SET_RAW_MEM;
+                  else
+                    MC_UNSET_RAW_MEM;
+                  return pair_test->num;
+                }
+              }
+            }
+            previous_cursor--;
+          }
+          next_cursor = cursor + 1;
+          while(next_cursor < xbt_dynar_length(acceptance_pairs)){
+            pair_test = (mc_acceptance_pair_t)xbt_dynar_get_as(acceptance_pairs, next_cursor, mc_acceptance_pair_t);
+            bytes_used_test = pair_test->system_state->heap_bytes_used;
+            if(bytes_used_test != current_bytes_used)
+              break;
+            if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){
+              if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
+                if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
+                  if(raw_mem_set)
+                    MC_SET_RAW_MEM;
+                  else
+                    MC_UNSET_RAW_MEM;
+                  return pair_test->num;
+                }
+              }
+            }
+            next_cursor++;
+          }
         }
-      }else{
-        XBT_INFO("Different automaton state");
-      }
-      if(pair_test->comparison_times != NULL && XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
-        XBT_DEBUG("*** Comparison times statistics ***");
-        MC_print_comparison_times_statistics(pair_test->comparison_times);
       }
     }
 
-    /* New pair reached */
-    xbt_dynar_push(reached_pairs, &new_pair); 
+    pair_test = (mc_acceptance_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_acceptance_pair_t);
+    bytes_used_test = pair_test->heap_bytes_used;
+
+    if(bytes_used_test < current_bytes_used)
+      xbt_dynar_insert_at(acceptance_pairs, cursor + 1, &new_pair);
+    else
+      xbt_dynar_insert_at(acceptance_pairs, cursor, &new_pair);
     
     MC_UNSET_RAW_MEM;
 
     if(raw_mem_set)
       MC_SET_RAW_MEM;
- 
-    compare = 0;
     
-    return 0;
+    return -1;
     
   }
+ 
 }
 
 
-void set_pair_reached(xbt_state_t st){
+static void set_acceptance_pair_reached(int num, xbt_automaton_state_t as){
 
-  raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
  
   MC_SET_RAW_MEM;
+  mc_acceptance_pair_t new_pair = acceptance_pair_new(num, as);
+  MC_UNSET_RAW_MEM;
 
-  mc_pair_reached_t pair = NULL;
-  pair = xbt_new0(s_mc_pair_reached_t, 1);
-  pair->nb = xbt_dynar_length(reached_pairs) + 1;
-  pair->automaton_state = st;
-  pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
-  pair->comparison_times = new_comparison_times();
-  pair->system_state = MC_take_snapshot_liveness();
+  if(xbt_dynar_is_empty(acceptance_pairs)){
 
-  /* Get values of propositional symbols */
-  unsigned int cursor = 0;
-  xbt_propositional_symbol_t ps = NULL;
-  int res;
-  int_f_void_t f;
+     MC_SET_RAW_MEM;
+     xbt_dynar_push(acceptance_pairs, &new_pair); 
+     MC_UNSET_RAW_MEM;
 
-  xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
-    f = (int_f_void_t)ps->function;
-    res = (*f)();
-    xbt_dynar_push_as(pair->prop_ato, int, res);
-  }
+  }else{
 
-  xbt_dynar_push(reached_pairs, &pair); 
-  
-  MC_UNSET_RAW_MEM;
+    MC_SET_RAW_MEM;
+    
+    size_t current_bytes_used = new_pair->heap_bytes_used;
+    int current_nb_processes = new_pair->nb_processes;
+
+    unsigned int cursor = 0;
+    int start = 0;
+    int end = xbt_dynar_length(acceptance_pairs) - 1;
+
+    mc_acceptance_pair_t pair_test = NULL;
+    size_t bytes_used_test = 0;
+    int nb_processes_test;
+
+    while(start <= end){
+      cursor = (start + end) / 2;
+      pair_test = (mc_acceptance_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_acceptance_pair_t);
+      bytes_used_test = pair_test->heap_bytes_used;
+      nb_processes_test = pair_test->nb_processes;
+      if(nb_processes_test < current_nb_processes)
+        start = cursor + 1;
+      if(nb_processes_test > current_nb_processes)
+        end = cursor - 1; 
+      if(nb_processes_test == current_nb_processes){
+        if(bytes_used_test < current_bytes_used)
+          start = cursor + 1;
+        if(bytes_used_test > current_bytes_used)
+          end = cursor - 1;
+        if(bytes_used_test == current_bytes_used)
+          break;
+      }
+    }
+
+    if(bytes_used_test < current_bytes_used)
+      xbt_dynar_insert_at(acceptance_pairs, cursor + 1, &new_pair);
+    else
+      xbt_dynar_insert_at(acceptance_pairs, cursor, &new_pair);
+    
+    MC_UNSET_RAW_MEM;
+    
+  }
 
   if(raw_mem_set)
     MC_SET_RAW_MEM;
     
 }
 
-int visited(xbt_state_t st){
+static void remove_acceptance_pair(int num_pair){
 
-  if(_surf_mc_stateful == 0)
-    return 0;
+  unsigned int cursor = 0;
+  mc_acceptance_pair_t current_pair;
 
-  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+  xbt_dynar_foreach(acceptance_pairs, cursor, current_pair){
+    if(current_pair->num == num_pair)
+      break;
+  }
+  
+  xbt_dynar_remove_at(acceptance_pairs, cursor, NULL);
 
-  MC_SET_RAW_MEM;
+}
 
-  mc_pair_visited_t new_pair = NULL;
-  new_pair = xbt_new0(s_mc_pair_visited_t, 1);
-  new_pair->automaton_state = st;
+static mc_visited_pair_t visited_pair_new(int num, xbt_automaton_state_t as){
+
+  mc_visited_pair_t new_pair = NULL;
+  new_pair = xbt_new0(s_mc_visited_pair_t, 1);
+  new_pair->automaton_state = as;
+  new_pair->num = num;
   new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
-  new_pair->system_state = MC_take_snapshot_liveness();  
+  new_pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
+  new_pair->nb_processes = xbt_swag_size(simix_global->process_list);
+  new_pair->system_state = MC_take_snapshot();  
   
   /* Get values of propositional symbols */
   int res;
   int_f_void_t f;
   unsigned int cursor = 0;
-  xbt_propositional_symbol_t ps = NULL;
+  xbt_automaton_propositional_symbol_t ps = NULL;
   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
     f = (int_f_void_t)ps->function;
-    res = (*f)();
+    res = f();
     xbt_dynar_push_as(new_pair->prop_ato, int, res);
   }
-  
+
+  return new_pair;
+
+}
+
+static int is_visited_pair(int num, xbt_automaton_state_t as){
+
+  if(_sg_mc_visited == 0)
+    return -1;
+
+  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+  MC_SET_RAW_MEM;
+  mc_visited_pair_t new_pair = visited_pair_new(num, as);
   MC_UNSET_RAW_MEM;
-  
+
   if(xbt_dynar_is_empty(visited_pairs)){
 
     MC_SET_RAW_MEM;
-    /* New pair visited */
     xbt_dynar_push(visited_pairs, &new_pair); 
     MC_UNSET_RAW_MEM;
 
     if(raw_mem_set)
       MC_SET_RAW_MEM;
- 
-    return 0;
+
+    return -1;
 
   }else{
 
     MC_SET_RAW_MEM;
     
-    cursor = 0;
-    mc_pair_visited_t pair_test = NULL;
-     
-    xbt_dynar_foreach(visited_pairs, cursor, pair_test){
-      if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug))
-        XBT_DEBUG("****** Pair visited #%d ******", cursor + 1);
-      if(automaton_state_compare(pair_test->automaton_state, st) == 0){
-        if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
-          if(snapshot_compare(new_pair->system_state, pair_test->system_state, NULL, NULL) == 0){
-            if(raw_mem_set)
-              MC_SET_RAW_MEM;
-            else
-              MC_UNSET_RAW_MEM;
-            
-            return 1;
-          }   
-        }else{
-          XBT_INFO("Different values of propositional symbols");
+    size_t current_bytes_used = new_pair->heap_bytes_used;
+    int current_nb_processes = new_pair->nb_processes;
+
+    unsigned int cursor = 0;
+    int previous_cursor = 0, next_cursor = 0;
+    int start = 0;
+    int end = xbt_dynar_length(visited_pairs) - 1;
+
+    mc_visited_pair_t pair_test = NULL;
+    size_t bytes_used_test;
+    int nb_processes_test;
+    int same_processes_and_bytes_not_found = 1;
+
+    while(start <= end && same_processes_and_bytes_not_found){
+      cursor = (start + end) / 2;
+      pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
+      bytes_used_test = pair_test->heap_bytes_used;
+      nb_processes_test = pair_test->nb_processes;
+      if(nb_processes_test < current_nb_processes)
+        start = cursor + 1;
+      if(nb_processes_test > current_nb_processes)
+        end = cursor - 1; 
+      if(nb_processes_test == current_nb_processes){
+        if(bytes_used_test < current_bytes_used)
+          start = cursor + 1;
+        if(bytes_used_test > current_bytes_used)
+          end = cursor - 1;
+        if(bytes_used_test == current_bytes_used){
+          same_processes_and_bytes_not_found = 0;
+          if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){
+            if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
+              if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
+                xbt_dynar_remove_at(visited_pairs, cursor, NULL);
+                xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
+                XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_pair->num, pair_test->num);
+                if(raw_mem_set)
+                  MC_SET_RAW_MEM;
+                else
+                  MC_UNSET_RAW_MEM;
+                return pair_test->num;
+              }
+            }
+          }
+          /* Search another pair with same number of bytes used in std_heap */
+          previous_cursor = cursor - 1;
+          while(previous_cursor >= 0){
+            pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, previous_cursor, mc_visited_pair_t);
+            bytes_used_test = pair_test->system_state->heap_bytes_used;
+            if(bytes_used_test != current_bytes_used)
+              break;
+            if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){
+              if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){  
+                if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
+                  xbt_dynar_remove_at(visited_pairs, previous_cursor, NULL);
+                  xbt_dynar_insert_at(visited_pairs, previous_cursor, &new_pair);
+                  XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_pair->num, pair_test->num);
+                  if(raw_mem_set)
+                    MC_SET_RAW_MEM;
+                  else
+                    MC_UNSET_RAW_MEM;
+                  return pair_test->num;
+                }
+              }
+            }
+            previous_cursor--;
+          }
+          next_cursor = cursor + 1;
+          while(next_cursor < xbt_dynar_length(visited_pairs)){
+            pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, next_cursor, mc_visited_pair_t);
+            bytes_used_test = pair_test->system_state->heap_bytes_used;
+            if(bytes_used_test != current_bytes_used)
+              break;
+            if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){
+              if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
+                if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
+                  xbt_dynar_remove_at(visited_pairs, next_cursor, NULL);
+                  xbt_dynar_insert_at(visited_pairs, next_cursor, &new_pair);
+                  XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_pair->num, pair_test->num);
+                  if(raw_mem_set)
+                    MC_SET_RAW_MEM;
+                  else
+                    MC_UNSET_RAW_MEM;
+                  return pair_test->num;
+                }
+              }
+            }
+            next_cursor++;
+          }
         }
-      }else{
-        XBT_INFO("Different automaton state");
       }
     }
 
-    if(xbt_dynar_length(visited_pairs) == _surf_mc_stateful){
-      xbt_dynar_remove_at(visited_pairs, 0, NULL);
+    pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
+    bytes_used_test = pair_test->heap_bytes_used;
+
+    if(bytes_used_test < current_bytes_used)
+      xbt_dynar_insert_at(visited_pairs, cursor + 1, &new_pair);
+    else
+      xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
+
+    if(xbt_dynar_length(visited_pairs) > _sg_mc_visited){
+      int min = mc_stats->expanded_states;
+      unsigned int cursor2 = 0;
+      unsigned int index = 0;
+      xbt_dynar_foreach(visited_pairs, cursor2, pair_test){
+        if(pair_test->num < min){
+          index = cursor2;
+          min = pair_test->num;
+        }
+      }
+      xbt_dynar_remove_at(visited_pairs, index, NULL);
     }
 
-    /* New pair visited */
-    xbt_dynar_push(visited_pairs, &new_pair); 
+    /*cursor = 0;
+    xbt_dynar_foreach(visited_pairs, cursor, pair_test){
+      fprintf(stderr, "Visited pair %d, nb_processes %d and heap_bytes_used %zu\n", pair_test->num, pair_test->nb_processes, pair_test->heap_bytes_used);
+      }*/
     
     MC_UNSET_RAW_MEM;
 
     if(raw_mem_set)
       MC_SET_RAW_MEM;
     
-    return 0;
+    return -1;
     
   }
+ 
 }
 
-void MC_pair_delete(mc_pair_t pair){
-  xbt_free(pair->graph_state->proc_status);
-  xbt_free(pair->graph_state);
-  xbt_free(pair);
-}
-
-
-
-int MC_automaton_evaluate_label(xbt_exp_label_t l){
+static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l){
   
   switch(l->type){
   case 0 : {
@@ -421,12 +447,12 @@ int MC_automaton_evaluate_label(xbt_exp_label_t l){
   }
   case 3 : { 
     unsigned int cursor = 0;
-    xbt_propositional_symbol_t p = NULL;
+    xbt_automaton_propositional_symbol_t p = NULL;
     int_f_void_t f;
     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
       if(strcmp(p->pred, l->u.predicat) == 0){
         f = (int_f_void_t)p->function;
-        return (*f)();
+        return f();
       }
     }
     return -1;
@@ -440,64 +466,45 @@ int MC_automaton_evaluate_label(xbt_exp_label_t l){
 }
 
 
-/********************* Double-DFS stateless *******************/
+/********* Free functions *********/
 
-void pair_visited_free(mc_pair_visited_t pair){
+static void visited_pair_free(mc_visited_pair_t pair){
   if(pair){
-    pair->automaton_state = NULL;
     xbt_dynar_free(&(pair->prop_ato));
     MC_free_snapshot(pair->system_state);
     xbt_free(pair);
   }
 }
 
-void pair_visited_free_voidp(void *p){
-  pair_visited_free((mc_pair_visited_t) * (void **) p);
-}
-
-void pair_stateless_free(mc_pair_stateless_t pair){
-  xbt_free(pair->graph_state->system_state);
-  xbt_free(pair->graph_state->proc_status);
-  xbt_free(pair->graph_state);
-  xbt_free(pair);
+static void visited_pair_free_voidp(void *p){
+  visited_pair_free((mc_visited_pair_t) * (void **) p);
 }
 
-void pair_stateless_free_voidp(void *p){
-  pair_stateless_free((mc_pair_stateless_t) * (void **) p);
-}
-
-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 pair_reached_free(mc_pair_reached_t pair){
+static void acceptance_pair_free(mc_acceptance_pair_t pair){
   if(pair){
-    pair->automaton_state = NULL;
     xbt_dynar_free(&(pair->prop_ato));
     MC_free_snapshot(pair->system_state);
     xbt_free(pair);
   }
 }
 
-void pair_reached_free_voidp(void *p){
-  pair_reached_free((mc_pair_reached_t) * (void **) p);
+static void acceptance_pair_free_voidp(void *p){
+  acceptance_pair_free((mc_acceptance_pair_t) * (void **) p);
 }
 
+
+/********* DDFS Algorithm *********/
+
+
 void MC_ddfs_init(void){
 
-  raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+  initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
-  XBT_INFO("**************************************************");
-  XBT_INFO("Double-DFS init");
-  XBT_INFO("**************************************************");
+  XBT_DEBUG("**************************************************");
+  XBT_DEBUG("Double-DFS init");
+  XBT_DEBUG("**************************************************");
 
-  mc_pair_stateless_t mc_initial_pair = NULL;
+  mc_pair_t mc_initial_pair = NULL;
   mc_state_t initial_graph_state = NULL;
   smx_process_t process; 
 
@@ -506,52 +513,52 @@ void MC_ddfs_init(void){
 
   MC_SET_RAW_MEM;
 
-  initial_graph_state = MC_state_pair_new();
+  initial_graph_state = MC_state_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(mc_pair_reached_t), pair_reached_free_voidp);
-  visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), pair_visited_free_voidp);
-  successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
+  acceptance_pairs = xbt_dynar_new(sizeof(mc_acceptance_pair_t), acceptance_pair_free_voidp);
+  visited_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), visited_pair_free_voidp);
+  successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
 
   /* Save the initial state */
-  initial_state_liveness->initial_snapshot = MC_take_snapshot_liveness();
+  initial_state_liveness->snapshot = MC_take_snapshot();
 
   MC_UNSET_RAW_MEM; 
   
   unsigned int cursor = 0;
-  xbt_state_t state;
+  xbt_automaton_state_t automaton_state;
 
-  xbt_dynar_foreach(_mc_property_automaton->states, cursor, state){
-    if(state->type == -1){
+  xbt_dynar_foreach(_mc_property_automaton->states, cursor, automaton_state){
+    if(automaton_state->type == -1){
       
       MC_SET_RAW_MEM;
-      mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
+      mc_initial_pair = MC_pair_new(initial_graph_state, automaton_state, MC_state_interleave_size(initial_graph_state));
       xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
       MC_UNSET_RAW_MEM;
       
       if(cursor != 0){
-        MC_restore_snapshot(initial_state_liveness->initial_snapshot);
+        MC_restore_snapshot(initial_state_liveness->snapshot);
         MC_UNSET_RAW_MEM;
       }
 
       MC_ddfs(0);
 
     }else{
-      if(state->type == 2){
+      if(automaton_state->type == 2){
       
         MC_SET_RAW_MEM;
-        mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
+        mc_initial_pair = MC_pair_new(initial_graph_state, automaton_state, MC_state_interleave_size(initial_graph_state));
         xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
         MC_UNSET_RAW_MEM;
 
-        set_pair_reached(state);
+        set_acceptance_pair_reached(mc_initial_pair->num, automaton_state);
 
         if(cursor != 0){
-          MC_restore_snapshot(initial_state_liveness->initial_snapshot);
+          MC_restore_snapshot(initial_state_liveness->snapshot);
           MC_UNSET_RAW_MEM;
         }
   
@@ -561,7 +568,7 @@ void MC_ddfs_init(void){
     }
   }
 
-  if(raw_mem_set)
+  if(initial_state_liveness->raw_mem_set)
     MC_SET_RAW_MEM;
   else
     MC_UNSET_RAW_MEM;
@@ -572,17 +579,15 @@ void MC_ddfs_init(void){
 
 void MC_ddfs(int search_cycle){
 
-  raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
-
   smx_process_t process;
-  mc_pair_stateless_t current_pair = NULL;
+  mc_pair_t current_pair = NULL;
 
   if(xbt_fifo_size(mc_stack_liveness) == 0)
     return;
 
 
   /* Get current pair */
-  current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
+  current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
 
   /* Update current state in buchi automaton */
   _mc_property_automaton->current_state = current_pair->automaton_state;
@@ -590,26 +595,24 @@ void MC_ddfs(int search_cycle){
  
   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
  
-  mc_stats_pair->visited_pairs++;
-
-  //sleep(1);
+  mc_stats->visited_pairs++;
 
   int value;
   mc_state_t next_graph_state = NULL;
   smx_simcall_t req = NULL;
   char *req_str;
 
-  xbt_transition_t transition_succ;
+  xbt_automaton_transition_t transition_succ;
   unsigned int cursor = 0;
   int res;
+  int reached_num;
 
-  mc_pair_stateless_t next_pair = NULL;
-  mc_pair_stateless_t pair_succ;
+  mc_pair_t next_pair = NULL;
+  mc_pair_t pair_succ;
 
-  mc_pair_stateless_t remove_pair;
-  mc_pair_reached_t remove_pair_reached;
+  mc_pair_t pair_to_remove;
   
-  if(xbt_fifo_size(mc_stack_liveness) < _surf_mc_max_depth){
+  if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
 
     if(current_pair->requests > 0){
 
@@ -617,11 +620,14 @@ void MC_ddfs(int search_cycle){
    
         /* Debug information */
        
-        req_str = MC_request_to_string(req, value);
-        XBT_DEBUG("Execute: %s", req_str);
-        xbt_free(req_str);
+        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);
+        }
 
-        MC_state_set_executed_request(current_pair->graph_state, req, value);   
+        MC_state_set_executed_request(current_pair->graph_state, req, value);  
+        mc_stats->executed_transitions++;
 
         /* Answer the request */
         SIMIX_simcall_pre(req, value);
@@ -632,10 +638,9 @@ void MC_ddfs(int search_cycle){
         MC_SET_RAW_MEM;
 
         /* Create the new expanded graph_state */
-        next_graph_state = MC_state_pair_new();
+        next_graph_state = MC_state_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)){
             XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call); 
@@ -660,7 +665,7 @@ void MC_ddfs(int search_cycle){
 
           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));
+            next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
             xbt_dynar_push(successors, &next_pair);
             MC_UNSET_RAW_MEM;
           }
@@ -675,7 +680,7 @@ void MC_ddfs(int search_cycle){
   
           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));
+            next_pair = MC_pair_new(next_graph_state, transition_succ->dst,  MC_state_interleave_size(next_graph_state));
             xbt_dynar_push(successors, &next_pair);
             MC_UNSET_RAW_MEM;
           }
@@ -690,9 +695,9 @@ void MC_ddfs(int search_cycle){
 
             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
           
-              if(reached(pair_succ->automaton_state)){
+              if((reached_num = is_reached_acceptance_pair(pair_succ->num, pair_succ->automaton_state)) != -1){
         
-                XBT_INFO("Next pair (depth = %d, %u interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state));
+                XBT_INFO("Next pair (depth = %d, %u interleave) already reached (equal to state %d) !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state), reached_num);
 
                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
@@ -700,12 +705,12 @@ void MC_ddfs(int search_cycle){
                 XBT_INFO("Counter-example that violates formula :");
                 MC_show_stack_liveness(mc_stack_liveness);
                 MC_dump_stack_liveness(mc_stack_liveness);
-                MC_print_statistics_pairs(mc_stats_pair);
+                MC_print_statistics(mc_stats);
                 xbt_abort();
 
               }else{
 
-                if(visited(pair_succ->automaton_state)){
+                if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
 
                   XBT_DEBUG("Next pair already visited !");
                   break;
@@ -714,7 +719,7 @@ void MC_ddfs(int search_cycle){
 
                   XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 
-                  XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+                  XBT_DEBUG("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
 
                   MC_SET_RAW_MEM;
                   xbt_fifo_unshift(mc_stack_liveness, pair_succ);
@@ -728,7 +733,7 @@ void MC_ddfs(int search_cycle){
 
             }else{
 
-              if(visited(pair_succ->automaton_state)){
+              if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
 
                 XBT_DEBUG("Next pair already visited !");
                 break;
@@ -746,7 +751,7 @@ void MC_ddfs(int search_cycle){
 
           }else{
 
-            if(visited(pair_succ->automaton_state)){
+            if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
 
               XBT_DEBUG("Next pair already visited !");
               break;
@@ -757,11 +762,11 @@ void MC_ddfs(int search_cycle){
 
                 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
       
-                set_pair_reached(pair_succ->automaton_state); 
+                set_acceptance_pair_reached(pair_succ->num, pair_succ->automaton_state); 
 
                 search_cycle = 1;
 
-                XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+                XBT_DEBUG("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
 
               }
 
@@ -789,13 +794,15 @@ void MC_ddfs(int search_cycle){
 
  
     }else{
+
+      mc_stats->executed_transitions++;
       
       XBT_DEBUG("No more request to execute in this state, search evolution in Büchi Automaton.");
 
       MC_SET_RAW_MEM;
 
       /* Create the new expanded graph_state */
-      next_graph_state = MC_state_pair_new();
+      next_graph_state = MC_state_new();
 
       xbt_dynar_reset(successors);
 
@@ -809,7 +816,7 @@ void MC_ddfs(int search_cycle){
 
         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));
+          next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
           xbt_dynar_push(successors, &next_pair);
           MC_UNSET_RAW_MEM;
         }
@@ -824,7 +831,7 @@ void MC_ddfs(int search_cycle){
   
         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));
+          next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
           xbt_dynar_push(successors, &next_pair);
           MC_UNSET_RAW_MEM;
         }
@@ -839,9 +846,9 @@ void MC_ddfs(int search_cycle){
 
           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
 
-            if(reached(pair_succ->automaton_state)){
+            if((reached_num = is_reached_acceptance_pair(pair_succ->num, pair_succ->automaton_state)) != -1){
            
-              XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
+              XBT_INFO("Next pair (depth = %d) already reached (equal to state %d)!", xbt_fifo_size(mc_stack_liveness) + 1, reached_num);
         
               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
               XBT_INFO("|             ACCEPTANCE CYCLE            |");
@@ -849,51 +856,78 @@ void MC_ddfs(int search_cycle){
               XBT_INFO("Counter-example that violates formula :");
               MC_show_stack_liveness(mc_stack_liveness);
               MC_dump_stack_liveness(mc_stack_liveness);
-              MC_print_statistics_pairs(mc_stats_pair);
-              exit(0);
+              MC_print_statistics(mc_stats);
+              xbt_abort();
 
             }else{
 
-              XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
+              if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
+                
+                XBT_DEBUG("Next pair already visited !");
+                break;
+                
+              }else{
+
+                XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
         
-              XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+                XBT_INFO("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
 
-              MC_SET_RAW_MEM;
-              xbt_fifo_unshift(mc_stack_liveness, pair_succ);
-              MC_UNSET_RAW_MEM;
+                MC_SET_RAW_MEM;
+                xbt_fifo_unshift(mc_stack_liveness, pair_succ);
+                MC_UNSET_RAW_MEM;
         
-              MC_ddfs(search_cycle);
+                MC_ddfs(search_cycle);
+              
+              }
 
             }
 
           }else{
+            
+            if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
+              
+              XBT_DEBUG("Next pair already visited !");
+              break;
+              
+            }else{
 
-            MC_SET_RAW_MEM;
-            xbt_fifo_unshift(mc_stack_liveness, pair_succ);
-            MC_UNSET_RAW_MEM;
+              MC_SET_RAW_MEM;
+              xbt_fifo_unshift(mc_stack_liveness, pair_succ);
+              MC_UNSET_RAW_MEM;
             
-            MC_ddfs(search_cycle);
+              MC_ddfs(search_cycle);
+
+            }
             
           }
       
 
         }else{
       
-          if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
+          if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
 
-            set_pair_reached(pair_succ->automaton_state);
+            XBT_DEBUG("Next pair already visited !");
+            break;
+            
+          }else{
+
+            if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
+
+              set_acceptance_pair_reached(pair_succ->num, pair_succ->automaton_state);
          
-            search_cycle = 1;
+              search_cycle = 1;
 
-            XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+              XBT_INFO("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
 
-          }
+            }
 
-          MC_SET_RAW_MEM;
-          xbt_fifo_unshift(mc_stack_liveness, pair_succ);
-          MC_UNSET_RAW_MEM;
+            MC_SET_RAW_MEM;
+            xbt_fifo_unshift(mc_stack_liveness, pair_succ);
+            MC_UNSET_RAW_MEM;
           
-          MC_ddfs(search_cycle);
+            MC_ddfs(search_cycle);
+          
+          }
           
         }
 
@@ -907,11 +941,15 @@ void MC_ddfs(int search_cycle){
     
   }else{
     
-    XBT_DEBUG("Max depth reached");
-
+    XBT_WARN("/!\\ Max depth reached ! /!\\ ");
+    if(MC_state_interleave_size(current_pair->graph_state) > 0){
+      XBT_WARN("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ "); 
+      XBT_WARN("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
+    }
+    
   }
 
-  if(xbt_fifo_size(mc_stack_liveness) == _surf_mc_max_depth ){
+  if(xbt_fifo_size(mc_stack_liveness) == _sg_mc_max_depth ){
     XBT_DEBUG("Pair (depth = %d) shifted in stack, maximum depth reached", xbt_fifo_size(mc_stack_liveness) );
   }else{
     XBT_DEBUG("Pair (depth = %d) shifted in stack", xbt_fifo_size(mc_stack_liveness) );
@@ -919,17 +957,12 @@ void MC_ddfs(int search_cycle){
 
   
   MC_SET_RAW_MEM;
-  remove_pair = xbt_fifo_shift(mc_stack_liveness);
-  xbt_fifo_remove(mc_stack_liveness, remove_pair);
-  remove_pair = NULL;
+  pair_to_remove = xbt_fifo_shift(mc_stack_liveness);
+  xbt_fifo_remove(mc_stack_liveness, pair_to_remove);
+  pair_to_remove = NULL;
   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
-    remove_pair_reached = xbt_dynar_pop_as(reached_pairs, mc_pair_reached_t);
-    pair_reached_free(remove_pair_reached);
-    remove_pair_reached = NULL;
+    remove_acceptance_pair(current_pair->num);
   }
   MC_UNSET_RAW_MEM;
 
-  if(raw_mem_set)
-    MC_SET_RAW_MEM;
-
 }