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

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 06265cb6e0..ac9b74d62e 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,56 +10,24 @@
 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 = xbt_malloc(20);
-      sprintf(core_name,"core_%d", pair); 
-      rename("core", core_name);
-      free(core_name);
-    }
-  }
 
-  return 0;
-}
+/********* Static functions *********/
 
-int reached(xbt_state_t st){
+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;
 
-  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;
+  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->prop_ato = xbt_dynar_new(sizeof(int), NULL);
   new_pair->system_state = MC_take_snapshot();  
@@ -68,7 +36,7 @@ int reached(xbt_state_t st){
   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();
@@ -77,11 +45,11 @@ int reached(xbt_state_t st){
   
   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); 
+    /* New acceptance pair */
+    xbt_dynar_push(acceptance_pairs, &new_pair); 
     MC_UNSET_RAW_MEM;
 
     if(raw_mem_set)
@@ -94,13 +62,13 @@ int reached(xbt_state_t st){
     MC_SET_RAW_MEM;
     
     cursor = 0;
-    mc_pair_reached_t pair_test = NULL;
+    mc_acceptance_pair_t pair_test = NULL;
      
-    xbt_dynar_foreach(reached_pairs, cursor, pair_test){
+    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->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){
+        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)
@@ -118,8 +86,8 @@ int reached(xbt_state_t st){
       }
     }
 
-    /* New pair reached */
-    xbt_dynar_push(reached_pairs, &new_pair); 
+    /* New acceptance pair */
+    xbt_dynar_push(acceptance_pairs, &new_pair); 
     
     MC_UNSET_RAW_MEM;
 
@@ -134,22 +102,22 @@ int reached(xbt_state_t st){
 }
 
 
-void set_pair_reached(xbt_state_t st){
+static void set_acceptance_pair_reached(xbt_automaton_state_t st){
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
  
   MC_SET_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;
+  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();
 
   /* Get values of propositional symbols */
   unsigned int cursor = 0;
-  xbt_propositional_symbol_t ps = NULL;
+  xbt_automaton_propositional_symbol_t ps = NULL;
   int res;
   int_f_void_t f;
 
@@ -159,7 +127,7 @@ void set_pair_reached(xbt_state_t st){
     xbt_dynar_push_as(pair->prop_ato, int, res);
   }
 
-  xbt_dynar_push(reached_pairs, &pair); 
+  xbt_dynar_push(acceptance_pairs, &pair); 
   
   MC_UNSET_RAW_MEM;
 
@@ -168,7 +136,7 @@ void set_pair_reached(xbt_state_t st){
     
 }
 
-int visited(xbt_state_t st){
+static int is_visited_pair(xbt_automaton_state_t st){
 
   if(_sg_mc_visited == 0)
     return 0;
@@ -177,8 +145,8 @@ int visited(xbt_state_t st){
 
   MC_SET_RAW_MEM;
 
-  mc_pair_visited_t new_pair = NULL;
-  new_pair = xbt_new0(s_mc_pair_visited_t, 1);
+  mc_visited_pair_t new_pair = NULL;
+  new_pair = xbt_new0(s_mc_visited_pair_t, 1);
   new_pair->automaton_state = st;
   new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
   new_pair->system_state = MC_take_snapshot();  
@@ -187,7 +155,7 @@ int visited(xbt_state_t st){
   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();
@@ -213,13 +181,13 @@ int visited(xbt_state_t st){
     MC_SET_RAW_MEM;
     
     cursor = 0;
-    mc_pair_visited_t pair_test = NULL;
+    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(automaton_state_compare(pair_test->automaton_state, st) == 0){
-        if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
+      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;
@@ -253,15 +221,7 @@ int visited(xbt_state_t st){
   }
 }
 
-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 : {
@@ -280,7 +240,7 @@ 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){
@@ -299,9 +259,9 @@ 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){
     xbt_dynar_free(&(pair->prop_ato));
     MC_free_snapshot(pair->system_state);
@@ -309,32 +269,11 @@ void pair_visited_free(mc_pair_visited_t pair){
   }
 }
 
-void pair_visited_free_voidp(void *p){
-  pair_visited_free((mc_pair_visited_t) * (void **) p);
+static void visited_pair_free_voidp(void *p){
+  visited_pair_free((mc_visited_pair_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);
-}
-
-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){
     xbt_dynar_free(&(pair->prop_ato));
     MC_free_snapshot(pair->system_state);
@@ -342,10 +281,14 @@ void pair_reached_free(mc_pair_reached_t 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){
 
   initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
@@ -354,7 +297,7 @@ void MC_ddfs_init(void){
   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; 
 
@@ -363,16 +306,16 @@ 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->snapshot = MC_take_snapshot();
@@ -380,13 +323,13 @@ void MC_ddfs_init(void){
   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;
       
@@ -398,14 +341,14 @@ void MC_ddfs_init(void){
       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(automaton_state);
 
         if(cursor != 0){
           MC_restore_snapshot(initial_state_liveness->snapshot);
@@ -429,17 +372,15 @@ void MC_ddfs_init(void){
 
 void MC_ddfs(int search_cycle){
 
-  //initial_state_liveness->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;
@@ -447,24 +388,22 @@ 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_states++;
 
   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;
 
-  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;
+  mc_acceptance_pair_t acceptance_pair_to_remove;
   
   if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
 
@@ -491,7 +430,7 @@ 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){
@@ -518,7 +457,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;
           }
@@ -533,7 +472,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;
           }
@@ -548,7 +487,7 @@ 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(is_reached_acceptance_pair(pair_succ->automaton_state)){
         
                 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));
 
@@ -558,12 +497,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->automaton_state)){
 
                   XBT_DEBUG("Next pair already visited !");
                   break;
@@ -572,7 +511,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);
@@ -586,7 +525,7 @@ void MC_ddfs(int search_cycle){
 
             }else{
 
-              if(visited(pair_succ->automaton_state)){
+              if(is_visited_pair(pair_succ->automaton_state)){
 
                 XBT_DEBUG("Next pair already visited !");
                 break;
@@ -604,7 +543,7 @@ void MC_ddfs(int search_cycle){
 
           }else{
 
-            if(visited(pair_succ->automaton_state)){
+            if(is_visited_pair(pair_succ->automaton_state)){
 
               XBT_DEBUG("Next pair already visited !");
               break;
@@ -615,11 +554,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->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));
 
               }
 
@@ -653,7 +592,7 @@ 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();
 
       xbt_dynar_reset(successors);
 
@@ -667,7 +606,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;
         }
@@ -682,7 +621,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;
         }
@@ -697,7 +636,7 @@ 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(is_reached_acceptance_pair(pair_succ->automaton_state)){
            
               XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
         
@@ -707,12 +646,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->automaton_state)){
                 
                 XBT_DEBUG("Next pair already visited !");
                 break;
@@ -721,7 +660,7 @@ void MC_ddfs(int search_cycle){
 
                 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);
@@ -735,7 +674,7 @@ void MC_ddfs(int search_cycle){
 
           }else{
             
-            if(visited(pair_succ->automaton_state)){
+            if(is_visited_pair(pair_succ->automaton_state)){
               
               XBT_DEBUG("Next pair already visited !");
               break;
@@ -755,7 +694,7 @@ void MC_ddfs(int search_cycle){
 
         }else{
       
-          if(visited(pair_succ->automaton_state)){
+          if(is_visited_pair(pair_succ->automaton_state)){
 
             XBT_DEBUG("Next pair already visited !");
             break;
@@ -764,11 +703,11 @@ void MC_ddfs(int search_cycle){
 
             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 
-              set_pair_reached(pair_succ->automaton_state);
+              set_acceptance_pair_reached(pair_succ->automaton_state);
          
               search_cycle = 1;
 
-              XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+              XBT_INFO("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
 
             }
 
@@ -793,7 +732,7 @@ void MC_ddfs(int search_cycle){
   }else{
     
     XBT_WARN("/!\\ Max depth reached ! /!\\ ");
-    if(current_pair->requests > 0){
+    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.");
     }
@@ -808,17 +747,14 @@ 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;
+    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;
   }
   MC_UNSET_RAW_MEM;
 
-  /*if(initial_state_liveness->raw_mem_set)
-    MC_SET_RAW_MEM;*/
-
 }