X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/3a54b6d1aef3110883b46f912b3a4eeb5c9fb087..5be8607beafe19c7821ded74305548a35dfeb111:/src/mc/mc_liveness.c

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index ac9b74d62e..362e331a89 100644
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -19,17 +19,15 @@ xbt_dynar_t successors;
 
 /********* Static functions *********/
 
-static int is_reached_acceptance_pair(xbt_automaton_state_t st){
-
-  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
-
-  MC_SET_RAW_MEM;
+static mc_acceptance_pair_t acceptance_pair_new(int num, xbt_automaton_state_t as){
 
   mc_acceptance_pair_t new_pair = NULL;
   new_pair = xbt_new0(s_mc_acceptance_pair_t, 1);
-  new_pair->num = xbt_dynar_length(acceptance_pairs) + 1;
-  new_pair->automaton_state = st;
+  new_pair->num = num;
+  new_pair->automaton_state = as;
   new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
+  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 */
@@ -42,113 +40,222 @@ static int is_reached_acceptance_pair(xbt_automaton_state_t st){
     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(acceptance_pairs)){
 
     MC_SET_RAW_MEM;
-    /* New acceptance 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;
+    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;
-     
-    xbt_dynar_foreach(acceptance_pairs, cursor, pair_test){
-      if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug))
-        XBT_DEBUG("****** Pair reached #%d ******", pair_test->num);
-      if(xbt_automaton_state_compare(pair_test->automaton_state, st) == 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 1;
+    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_DEBUG("Different values of propositional symbols");
         }
-      }else{
-        XBT_DEBUG("Different automaton state");
       }
     }
 
-    /* New acceptance pair */
-    xbt_dynar_push(acceptance_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;
     
   }
+ 
 }
 
 
-static void set_acceptance_pair_reached(xbt_automaton_state_t st){
+static void set_acceptance_pair_reached(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;
 
-  mc_acceptance_pair_t pair = NULL;
-  pair = xbt_new0(s_mc_acceptance_pair_t, 1);
-  pair->num = xbt_dynar_length(acceptance_pairs) + 1;
-  pair->automaton_state = st;
-  pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
-  pair->system_state = MC_take_snapshot();
+  if(xbt_dynar_is_empty(acceptance_pairs)){
 
-  /* Get values of propositional symbols */
-  unsigned int cursor = 0;
-  xbt_automaton_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(acceptance_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;
     
 }
 
-static int is_visited_pair(xbt_automaton_state_t st){
+static void remove_acceptance_pair(int num_pair){
 
-  if(_sg_mc_visited == 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;
+}
+
+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 = st;
+  new_pair->automaton_state = as;
+  new_pair->num = num;
   new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
+  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 */
@@ -161,64 +268,164 @@ static int is_visited_pair(xbt_automaton_state_t st){
     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;
+    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;
-     
-    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(xbt_automaton_state_compare(pair_test->automaton_state, st) == 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 1;
-          }   
-        }else{
-          XBT_DEBUG("Different values of propositional symbols");
+    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_DEBUG("Different automaton state");
       }
     }
 
-    if(xbt_dynar_length(visited_pairs) == _sg_mc_visited){
-      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;
     
   }
+ 
 }
 
 static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l){
@@ -348,7 +555,7 @@ void MC_ddfs_init(void){
         xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
         MC_UNSET_RAW_MEM;
 
-        set_acceptance_pair_reached(automaton_state);
+        set_acceptance_pair_reached(mc_initial_pair->num, automaton_state);
 
         if(cursor != 0){
           MC_restore_snapshot(initial_state_liveness->snapshot);
@@ -388,7 +595,7 @@ void MC_ddfs(int search_cycle){
  
   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
  
-  mc_stats->visited_states++;
+  mc_stats->visited_pairs++;
 
   int value;
   mc_state_t next_graph_state = NULL;
@@ -403,7 +610,6 @@ void MC_ddfs(int search_cycle){
   mc_pair_t pair_succ;
 
   mc_pair_t pair_to_remove;
-  mc_acceptance_pair_t acceptance_pair_to_remove;
   
   if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
 
@@ -419,7 +625,8 @@ void MC_ddfs(int search_cycle){
           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);
@@ -487,7 +694,7 @@ void MC_ddfs(int search_cycle){
 
             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
           
-              if(is_reached_acceptance_pair(pair_succ->automaton_state)){
+              if(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));
 
@@ -502,7 +709,7 @@ void MC_ddfs(int search_cycle){
 
               }else{
 
-                if(is_visited_pair(pair_succ->automaton_state)){
+                if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
 
                   XBT_DEBUG("Next pair already visited !");
                   break;
@@ -525,7 +732,7 @@ void MC_ddfs(int search_cycle){
 
             }else{
 
-              if(is_visited_pair(pair_succ->automaton_state)){
+              if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
 
                 XBT_DEBUG("Next pair already visited !");
                 break;
@@ -543,7 +750,7 @@ void MC_ddfs(int search_cycle){
 
           }else{
 
-            if(is_visited_pair(pair_succ->automaton_state)){
+            if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
 
               XBT_DEBUG("Next pair already visited !");
               break;
@@ -554,7 +761,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);
       
-                set_acceptance_pair_reached(pair_succ->automaton_state); 
+                set_acceptance_pair_reached(pair_succ->num, pair_succ->automaton_state); 
 
                 search_cycle = 1;
 
@@ -586,6 +793,8 @@ 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.");
 
@@ -636,7 +845,7 @@ void MC_ddfs(int search_cycle){
 
           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
 
-            if(is_reached_acceptance_pair(pair_succ->automaton_state)){
+            if(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);
         
@@ -651,7 +860,7 @@ void MC_ddfs(int search_cycle){
 
             }else{
 
-              if(is_visited_pair(pair_succ->automaton_state)){
+              if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
                 
                 XBT_DEBUG("Next pair already visited !");
                 break;
@@ -674,7 +883,7 @@ void MC_ddfs(int search_cycle){
 
           }else{
             
-            if(is_visited_pair(pair_succ->automaton_state)){
+            if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
               
               XBT_DEBUG("Next pair already visited !");
               break;
@@ -694,7 +903,7 @@ void MC_ddfs(int search_cycle){
 
         }else{
       
-          if(is_visited_pair(pair_succ->automaton_state)){
+          if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
 
             XBT_DEBUG("Next pair already visited !");
             break;
@@ -703,7 +912,7 @@ void MC_ddfs(int search_cycle){
 
             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 
-              set_acceptance_pair_reached(pair_succ->automaton_state);
+              set_acceptance_pair_reached(pair_succ->num, pair_succ->automaton_state);
          
               search_cycle = 1;
 
@@ -751,9 +960,7 @@ void MC_ddfs(int search_cycle){
   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)){
-    acceptance_pair_to_remove = xbt_dynar_pop_as(acceptance_pairs, mc_acceptance_pair_t);
-    acceptance_pair_free(acceptance_pair_to_remove);
-    acceptance_pair_to_remove = NULL;
+    remove_acceptance_pair(current_pair->num);
   }
   MC_UNSET_RAW_MEM;