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

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 722d6ee111..8067a737c0 100644
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -11,29 +11,9 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
                                 "Logging specific to algorithms for liveness properties verification");
 
 xbt_dynar_t reached_pairs;
-xbt_dynar_t reached_pairs_hash;
 xbt_dynar_t visited_pairs;
-xbt_dynar_t visited_pairs_hash;
 xbt_dynar_t successors;
 
-xbt_dynar_t hosts_table;
-
-
-/* fast implementation of djb2 algorithm */
-unsigned int hash_region(char *str, int str_len){
-
-  int c;
-  register unsigned int hash = 5381;
-
-  while (str_len--) {
-    c = *str++;
-    hash = ((hash << 5) + hash) + c;    /* hash * 33 + c */
-  }
-
-  return hash;
-
-}
-
 int create_dump(int pair)
 {
    // Try to enable core dumps
@@ -48,7 +28,7 @@ int create_dump(int pair)
   switch(fork()){
   case 0:
     // We are the child process -- run the actual program
-    abort();
+    xbt_abort();
     break;
     
   case -1:
@@ -61,7 +41,7 @@ int create_dump(int pair)
     if(wait(&status) < 0)
       perror("wait");
     if(WIFSIGNALED(status) && WCOREDUMP(status)){
-      char *core_name = malloc(20);
+      char *core_name = xbt_malloc(20);
       sprintf(core_name,"core_%d", pair); 
       rename("core", core_name);
       free(core_name);
@@ -73,70 +53,80 @@ int create_dump(int pair)
 
 int reached(xbt_state_t st){
 
-  raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+  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;
+  new_pair->automaton_state = st;
+  new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
+  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_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
+    f = (int_f_void_t)ps->function;
+    res = (*f)();
+    xbt_dynar_push_as(new_pair->prop_ato, int, res);
+  }
+  
+  MC_UNSET_RAW_MEM;
+  
+  if(xbt_dynar_is_empty(reached_pairs)/* || !compare*/){
 
-  if(xbt_dynar_is_empty(reached_pairs)){
+    MC_SET_RAW_MEM;
+    /* New pair reached */
+    xbt_dynar_push(reached_pairs, &new_pair); 
+    MC_UNSET_RAW_MEM;
 
+    if(raw_mem_set)
+      MC_SET_RAW_MEM;
+ 
     return 0;
 
   }else{
 
     MC_SET_RAW_MEM;
-
-    mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
-    MC_take_snapshot_liveness(sn);    
     
-    xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
-    int res;
-    int_f_void_t f;
-
-    /* Get values of propositional symbols */
-    unsigned int cursor = 0;
-    xbt_propositional_symbol_t ps = NULL;
-    xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
-      f = (int_f_void_t)ps->function;
-      res = (*f)();
-      xbt_dynar_push_as(prop_ato, int, res);
-    }
-
     cursor = 0;
     mc_pair_reached_t pair_test = NULL;
      
     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
-      XBT_INFO("Pair reached #%d", pair_test->nb);
+      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, prop_ato) == 0){
-          if(snapshot_compare(pair_test->system_state, sn) == 0){
-     
-            MC_free_snapshot(sn);
-            xbt_dynar_reset(prop_ato);
-            xbt_free(prop_ato);
-            MC_UNSET_RAW_MEM;
-
+        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) == 0){
+            
             if(raw_mem_set)
               MC_SET_RAW_MEM;
             else
               MC_UNSET_RAW_MEM;
             
             return 1;
-          }       
+          }
         }else{
-          XBT_INFO("Different values of propositional symbols");
+          XBT_DEBUG("Different values of propositional symbols");
         }
       }else{
-        XBT_INFO("Different automaton state");
+        XBT_DEBUG("Different automaton state");
       }
     }
 
-    MC_free_snapshot(sn);
-    xbt_dynar_reset(prop_ato);
-    xbt_free(prop_ato);
+    /* New pair reached */
+    xbt_dynar_push(reached_pairs, &new_pair); 
+    
     MC_UNSET_RAW_MEM;
 
     if(raw_mem_set)
       MC_SET_RAW_MEM;
-    else
-      MC_UNSET_RAW_MEM;
+ 
+    compare = 0;
     
     return 0;
     
@@ -146,7 +136,7 @@ int reached(xbt_state_t st){
 
 void set_pair_reached(xbt_state_t st){
 
-  raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
  
   MC_SET_RAW_MEM;
 
@@ -155,9 +145,7 @@ void set_pair_reached(xbt_state_t st){
   pair->nb = xbt_dynar_length(reached_pairs) + 1;
   pair->automaton_state = st;
   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
-  pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
-  //pair->rdv_points = xbt_dict_new();  
-  MC_take_snapshot_liveness(pair->system_state);
+  pair->system_state = MC_take_snapshot();
 
   /* Get values of propositional symbols */
   unsigned int cursor = 0;
@@ -172,415 +160,99 @@ void set_pair_reached(xbt_state_t st){
   }
 
   xbt_dynar_push(reached_pairs, &pair); 
-
-  create_dump(xbt_dynar_length(reached_pairs));
   
   MC_UNSET_RAW_MEM;
 
   if(raw_mem_set)
     MC_SET_RAW_MEM;
-  else
-    MC_UNSET_RAW_MEM;
     
 }
 
+int visited(xbt_state_t st){
 
-int reached_hash(xbt_state_t st){
-
-  raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
-
-  if(xbt_dynar_is_empty(reached_pairs_hash)){
-
-    return 0;
-
-  }else{
-
-    MC_SET_RAW_MEM;
-
-    mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
-    MC_take_snapshot_liveness(sn);
-
-    int j;
-    unsigned int hash_regions[sn->num_reg];
-    for(j=0; j<sn->num_reg; j++){
-      hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
-    }
-
-
-    /* Get values of propositional symbols */
-    xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
-    unsigned int cursor = 0;
-    xbt_propositional_symbol_t ps = NULL;
-    int res;
-    int_f_void_t f;
-
-    xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
-      f = (int_f_void_t)ps->function;
-      res = (*f)();
-      xbt_dynar_push_as(prop_ato, int, res);
-    }
-
-    mc_pair_reached_hash_t pair_test = NULL;
-
-    int region_diff = 0;
-
-    cursor = 0;
-
-    xbt_dynar_foreach(reached_pairs_hash, cursor, pair_test){
-
-      if(automaton_state_compare(pair_test->automaton_state, st) == 0){
-        if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
-          for(j=0 ; j< sn->num_reg ; j++){
-            if(hash_regions[j] != pair_test->hash_regions[j]){
-              region_diff++;
-            }
-          }
-          if(region_diff == 0){
-            MC_free_snapshot(sn);
-            xbt_dynar_reset(prop_ato);
-            xbt_free(prop_ato);
-            MC_UNSET_RAW_MEM;
-
-            if(raw_mem_set)
-              MC_SET_RAW_MEM;
-            else
-              MC_UNSET_RAW_MEM;
-            
-            return 1;
-          }else{
-            XBT_INFO("Different snapshot");
-          }
-        }else{
-          XBT_INFO("Different values of propositional symbols");
-        }
-      }else{
-        XBT_INFO("Different automaton state");
-      }
-
-      region_diff = 0;
-    }
-    
-    MC_free_snapshot(sn);
-    xbt_dynar_reset(prop_ato);
-    xbt_free(prop_ato);
-    MC_UNSET_RAW_MEM;
-
-    if(raw_mem_set)
-      MC_SET_RAW_MEM;
-    else
-      MC_UNSET_RAW_MEM;
-    
+  if(_sg_mc_visited == 0)
     return 0;
-    
-  }
-}
 
-void set_pair_reached_hash(xbt_state_t st){
+  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
-  raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
- 
   MC_SET_RAW_MEM;
 
-  mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
-  MC_take_snapshot_liveness(sn);
- 
-  mc_pair_reached_hash_t pair = NULL;
-  pair = xbt_new0(s_mc_pair_reached_hash_t, 1);
-  pair->automaton_state = st;
-  pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
-  pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
-  
-  int i;
-
-  for(i=0 ; i< sn->num_reg ; i++){
-    pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
-  }
+  mc_pair_visited_t new_pair = NULL;
+  new_pair = xbt_new0(s_mc_pair_visited_t, 1);
+  new_pair->automaton_state = st;
+  new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
+  new_pair->system_state = MC_take_snapshot();  
   
   /* Get values of propositional symbols */
-  unsigned int cursor = 0;
-  xbt_propositional_symbol_t ps = NULL;
   int res;
   int_f_void_t f;
-
+  unsigned int cursor = 0;
+  xbt_propositional_symbol_t ps = NULL;
   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);
+    xbt_dynar_push_as(new_pair->prop_ato, int, res);
   }
   
-  xbt_dynar_push(reached_pairs_hash, &pair);
-
-  MC_free_snapshot(sn);
-  
   MC_UNSET_RAW_MEM;
+  
+  if(xbt_dynar_is_empty(visited_pairs)){
 
-  if(raw_mem_set)
     MC_SET_RAW_MEM;
-  else
+    /* New pair visited */
+    xbt_dynar_push(visited_pairs, &new_pair); 
     MC_UNSET_RAW_MEM;
-      
-}
-
-
-int visited(xbt_state_t st, int sc){
-
-  raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
-
-  if(xbt_dynar_is_empty(visited_pairs)){
 
+    if(raw_mem_set)
+      MC_SET_RAW_MEM;
+ 
     return 0;
 
   }else{
 
     MC_SET_RAW_MEM;
-
-    mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
-    MC_take_snapshot_liveness(sn);
-
-    xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
-
-    /* Get values of propositional symbols */
-    unsigned int cursor = 0;
-    xbt_propositional_symbol_t ps = NULL;
-    int res;
-    int_f_void_t f;
-
-    xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
-      f = (int_f_void_t)ps->function;
-      res = (*f)();
-      xbt_dynar_push_as(prop_ato, int, res);
-    }
-
+    
     cursor = 0;
     mc_pair_visited_t pair_test = NULL;
-
+     
     xbt_dynar_foreach(visited_pairs, cursor, pair_test){
-      if(pair_test->search_cycle == sc) {
-        if(automaton_state_compare(pair_test->automaton_state, st) == 0){
-          if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
-            if(snapshot_compare(pair_test->system_state, sn) == 0){
-      
-              MC_free_snapshot(sn);
-              xbt_dynar_reset(prop_ato);
-              xbt_free(prop_ato);
+      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) == 0){
+            if(raw_mem_set)
+              MC_SET_RAW_MEM;
+            else
               MC_UNSET_RAW_MEM;
-    
-              if(raw_mem_set)
-                MC_SET_RAW_MEM;
-              else
-                MC_UNSET_RAW_MEM;
-              
-              return 1;
-  
-            }else{
-              XBT_INFO("Different snapshot");
-            }
-          }else{
-            XBT_INFO("Different values of propositional symbols"); 
-          }
+            
+            return 1;
+          }   
         }else{
-          XBT_INFO("Different automaton state");
+          XBT_DEBUG("Different values of propositional symbols");
         }
       }else{
-        XBT_INFO("Different value of search_cycle");
+        XBT_DEBUG("Different automaton state");
       }
     }
 
-
-    MC_free_snapshot(sn);
-    xbt_dynar_reset(prop_ato);
-    xbt_free(prop_ato);
-    MC_UNSET_RAW_MEM;
-
-    if(raw_mem_set)
-      MC_SET_RAW_MEM;
-    else
-      MC_UNSET_RAW_MEM;
-    
-    return 0;
-    
-  }
-}
-
-
-int visited_hash(xbt_state_t st, int sc){
-
-  raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
-
-  if(xbt_dynar_is_empty(visited_pairs_hash)){
-
-    return 0;
-
-  }else{
-
-    MC_SET_RAW_MEM;
-
-    mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
-    MC_take_snapshot_liveness(sn);
-
-    int j;
-    unsigned int hash_regions[sn->num_reg];
-    for(j=0; j<sn->num_reg; j++){
-      hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
+    if(xbt_dynar_length(visited_pairs) == _sg_mc_visited){
+      xbt_dynar_remove_at(visited_pairs, 0, NULL);
     }
 
+    /* New pair visited */
+    xbt_dynar_push(visited_pairs, &new_pair); 
     
-    /* Get values of propositional symbols */
-    xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
-    unsigned int cursor = 0;
-    xbt_propositional_symbol_t ps = NULL;
-    int res;
-    int_f_void_t f;
-
-    xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
-      f = (int_f_void_t)ps->function;
-      res = (*f)();
-      xbt_dynar_push_as(prop_ato, int, res);
-    }
-
-    mc_pair_visited_hash_t pair_test = NULL;
-
-    int region_diff = 0;
-    cursor = 0;
-
-    xbt_dynar_foreach(visited_pairs_hash, cursor, pair_test){
-  
-      if(pair_test->search_cycle == sc) {
-        if(automaton_state_compare(pair_test->automaton_state, st) == 0){
-          if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
-            for(j=0 ; j< sn->num_reg ; j++){
-              if(hash_regions[j] != pair_test->hash_regions[j]){
-                region_diff++;
-              }
-            }
-            if(region_diff == 0){
-              MC_free_snapshot(sn);
-              xbt_dynar_reset(prop_ato);
-              xbt_free(prop_ato);
-              MC_UNSET_RAW_MEM;
-              
-              if(raw_mem_set)
-                MC_SET_RAW_MEM;
-              else
-                MC_UNSET_RAW_MEM;
-  
-              return 1;
-            }else{
-              //XBT_INFO("Different snapshot");
-            }
-          }else{
-            //XBT_INFO("Different values of propositional symbols"); 
-          }
-        }else{
-          //XBT_INFO("Different automaton state");
-        }
-      }else{
-        //XBT_INFO("Different value of search_cycle");
-      }
-      
-      region_diff = 0;
-    }
-    
-    MC_free_snapshot(sn);
-    xbt_dynar_reset(prop_ato);
-    xbt_free(prop_ato);
     MC_UNSET_RAW_MEM;
-  
+
     if(raw_mem_set)
       MC_SET_RAW_MEM;
-    else
-      MC_UNSET_RAW_MEM;
-  
+    
     return 0;
     
   }
 }
 
-void set_pair_visited_hash(xbt_state_t st, int sc){
-
-  raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
- 
-  MC_SET_RAW_MEM;
-
-  mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
-  MC_take_snapshot_liveness(sn);
- 
-  mc_pair_visited_hash_t pair = NULL;
-  pair = xbt_new0(s_mc_pair_visited_hash_t, 1);
-  pair->automaton_state = st;
-  pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
-  pair->search_cycle = sc;
-  pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
-  
-  int i;
-
-  for(i=0 ; i< sn->num_reg ; i++){
-    pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
-  }
-  
-  /* Get values of propositional symbols */
-  unsigned int cursor = 0;
-  xbt_propositional_symbol_t ps = NULL;
-  int res;
-  int_f_void_t f;
-
-  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);
-  }
-  
-  xbt_dynar_push(visited_pairs_hash, &pair);
-
-  MC_free_snapshot(sn);
-  
-  MC_UNSET_RAW_MEM;
-    
-  if(raw_mem_set)
-    MC_SET_RAW_MEM;
-  else
-    MC_UNSET_RAW_MEM;
-  
-}
-
-void set_pair_visited(xbt_state_t st, int sc){
-
-  raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
- 
-  MC_SET_RAW_MEM;
- 
-  mc_pair_visited_t pair = NULL;
-  pair = xbt_new0(s_mc_pair_visited_t, 1);
-  pair->automaton_state = st;
-  pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
-  pair->search_cycle = sc;
-  pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
-  MC_take_snapshot_liveness(pair->system_state);
-
-
-  /* Get values of propositional symbols */
-  unsigned int cursor = 0;
-  xbt_propositional_symbol_t ps = NULL;
-  int res;
-  int_f_void_t f;
-
-  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);
-  }
-  
-  xbt_dynar_push(visited_pairs, &pair);
-  
-  MC_UNSET_RAW_MEM;
-  
-  if(raw_mem_set)
-    MC_SET_RAW_MEM;
-  else
-    MC_UNSET_RAW_MEM;
-  
-}
-
 void MC_pair_delete(mc_pair_t pair){
   xbt_free(pair->graph_state->proc_status);
   xbt_free(pair->graph_state);
@@ -629,12 +301,30 @@ int MC_automaton_evaluate_label(xbt_exp_label_t l){
 
 /********************* Double-DFS stateless *******************/
 
-void MC_pair_stateless_delete(mc_pair_stateless_t pair){
+void pair_visited_free(mc_pair_visited_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);
 }
 
+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);
@@ -645,13 +335,26 @@ mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
   return p;
 }
 
+void pair_reached_free(mc_pair_reached_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);
+}
+
 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_state_t initial_graph_state = NULL;
@@ -669,18 +372,15 @@ void MC_ddfs_init(void){
     }
   }
 
-  reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
-  //reached_pairs_hash = xbt_dynar_new(sizeof(mc_pair_reached_hash_t), NULL);
-  //visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), NULL);
-  //visited_pairs_hash = xbt_dynar_new(sizeof(mc_pair_visited_hash_t), NULL);
+  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);
 
   /* Save the initial state */
-  initial_snapshot_liveness = xbt_new0(s_mc_snapshot_t, 1);
-  MC_take_snapshot_liveness(initial_snapshot_liveness);
+  initial_state_liveness->snapshot = MC_take_snapshot();
 
   MC_UNSET_RAW_MEM; 
-
+  
   unsigned int cursor = 0;
   xbt_state_t state;
 
@@ -693,7 +393,7 @@ void MC_ddfs_init(void){
       MC_UNSET_RAW_MEM;
       
       if(cursor != 0){
-        MC_restore_snapshot(initial_snapshot_liveness);
+        MC_restore_snapshot(initial_state_liveness->snapshot);
         MC_UNSET_RAW_MEM;
       }
 
@@ -708,10 +408,9 @@ void MC_ddfs_init(void){
         MC_UNSET_RAW_MEM;
 
         set_pair_reached(state);
-        //set_pair_reached_hash(state);
 
         if(cursor != 0){
-          MC_restore_snapshot(initial_snapshot_liveness);
+          MC_restore_snapshot(initial_state_liveness->snapshot);
           MC_UNSET_RAW_MEM;
         }
   
@@ -721,7 +420,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;
@@ -732,7 +431,7 @@ void MC_ddfs_init(void){
 
 void MC_ddfs(int search_cycle){
 
-  raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+  //initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
   smx_process_t process;
   mc_pair_stateless_t current_pair = NULL;
@@ -748,7 +447,7 @@ void MC_ddfs(int search_cycle){
   _mc_property_automaton->current_state = current_pair->automaton_state;
 
  
-  XBT_INFO("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
+  XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
  
   mc_stats_pair->visited_pairs++;
 
@@ -765,14 +464,11 @@ void MC_ddfs(int search_cycle){
 
   mc_pair_stateless_t next_pair = NULL;
   mc_pair_stateless_t pair_succ;
-  
-  if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){
 
-    //set_pair_visited(current_pair->automaton_state, search_cycle);
-    //set_pair_visited_hash(current_pair->automaton_state, search_cycle);
-
-    //XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs));
-    //XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs_hash));
+  mc_pair_stateless_t remove_pair;
+  mc_pair_reached_t remove_pair_reached;
+  
+  if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
 
     if(current_pair->requests > 0){
 
@@ -781,7 +477,7 @@ void MC_ddfs(int search_cycle){
         /* Debug information */
        
         req_str = MC_request_to_string(req, value);
-        XBT_INFO("Execute: %s", req_str);
+        XBT_DEBUG("Execute: %s", req_str);
         xbt_free(req_str);
 
         MC_state_set_executed_request(current_pair->graph_state, req, value);   
@@ -792,13 +488,18 @@ void MC_ddfs(int search_cycle){
         /* Wait for requests (schedules processes) */
         MC_wait_for_requests();
 
-
         MC_SET_RAW_MEM;
 
         /* Create the new expanded graph_state */
         next_graph_state = MC_state_pair_new();
 
         /* Get enabled process and insert it in the interleave set of the next graph_state */
+        xbt_swag_foreach(process, simix_global->process_list){
+          if(MC_process_is_enabled(process)){
+            XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call); 
+          }
+        }
+
         xbt_swag_foreach(process, simix_global->process_list){
           if(MC_process_is_enabled(process)){
             MC_state_interleave_process(next_graph_state, process);
@@ -848,7 +549,6 @@ 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_hash(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));
 
@@ -859,94 +559,96 @@ void MC_ddfs(int search_cycle){
                 MC_show_stack_liveness(mc_stack_liveness);
                 MC_dump_stack_liveness(mc_stack_liveness);
                 MC_print_statistics_pairs(mc_stats_pair);
-                exit(0);
+                xbt_abort();
 
               }else{
 
-                XBT_INFO("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
-        
-                set_pair_reached(pair_succ->automaton_state);
-                //set_pair_reached_hash(pair_succ->automaton_state);
+                if(visited(pair_succ->automaton_state)){
 
-                XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
-                //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
+                  XBT_DEBUG("Next pair already visited !");
+                  break;
+            
+                }else{
 
-                MC_SET_RAW_MEM;
-                xbt_fifo_unshift(mc_stack_liveness, pair_succ);
-                MC_UNSET_RAW_MEM;
+                  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));
+
+                  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(!visited_hash(pair_succ->automaton_state, search_cycle)){
-                //if(!visited(pair_succ->automaton_state, search_cycle)){
-    
+              if(visited(pair_succ->automaton_state)){
+
+                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_ddfs(search_cycle);
-    
-                /*}else{
-
-                XBT_INFO("Next pair already visited ! ");
-
-                }*/
-        
+              }
+               
             }
 
           }else{
+
+            if(visited(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))){
+              if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 
-              XBT_INFO("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
+                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_pair_reached_hash(pair_succ->automaton_state);
+                set_pair_reached(pair_succ->automaton_state); 
 
-              search_cycle = 1;
+                search_cycle = 1;
 
-              XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
-              //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
+                XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 
-            }
+              }
 
-            //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
-              //if(!visited(pair_succ->automaton_state, search_cycle)){
-        
               MC_SET_RAW_MEM;
               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
               MC_UNSET_RAW_MEM;
-        
+            
               MC_ddfs(search_cycle);
-        
-              /*}else{
-
-              XBT_INFO("Next pair already visited ! ");
-
-              }*/
 
+            }
+           
           }
 
-   
           /* Restore system before checking others successors */
           if(cursor != (xbt_dynar_length(successors) - 1))
             MC_replay_liveness(mc_stack_liveness, 1);
-  
-    
+            
         }
 
         if(MC_state_interleave_size(current_pair->graph_state) > 0){
-          XBT_INFO("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
+          XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
           MC_replay_liveness(mc_stack_liveness, 0);
         }
       }
 
  
-    }else{  /*No request to execute, search evolution in Büchi automaton */
+    }else{
+      
+      XBT_DEBUG("No more request to execute in this state, search evolution in Büchi Automaton.");
 
       MC_SET_RAW_MEM;
 
@@ -996,8 +698,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(reached_hash(pair_succ->automaton_state)){
-
+           
               XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
         
               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
@@ -1007,17 +708,13 @@ void MC_ddfs(int search_cycle){
               MC_show_stack_liveness(mc_stack_liveness);
               MC_dump_stack_liveness(mc_stack_liveness);
               MC_print_statistics_pairs(mc_stats_pair);
-              exit(0);
+              xbt_abort();
 
             }else{
 
-              XBT_INFO("Next pair (depth = %d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
+              XBT_INFO("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_pair_reached_hash(pair_succ->automaton_state);
-    
               XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
-              //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
 
               MC_SET_RAW_MEM;
               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
@@ -1029,20 +726,12 @@ void MC_ddfs(int search_cycle){
 
           }else{
 
-            //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
-              //if(!visited(pair_succ->automaton_state, search_cycle)){
-
-              MC_SET_RAW_MEM;
-              xbt_fifo_unshift(mc_stack_liveness, pair_succ);
-              MC_UNSET_RAW_MEM;
-        
-              MC_ddfs(search_cycle);
-        
-              /*}else{
-
-              XBT_INFO("Next pair already visited ! ");
-
-              }*/
+            MC_SET_RAW_MEM;
+            xbt_fifo_unshift(mc_stack_liveness, pair_succ);
+            MC_UNSET_RAW_MEM;
+            
+            MC_ddfs(search_cycle);
+            
           }
       
 
@@ -1051,65 +740,58 @@ 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_pair_reached_hash(pair_succ->automaton_state);
-            
+         
             search_cycle = 1;
 
             XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
-            //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
 
           }
 
-          //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
-            //if(!visited(pair_succ->automaton_state, search_cycle)){
-
-            MC_SET_RAW_MEM;
-            xbt_fifo_unshift(mc_stack_liveness, pair_succ);
-            MC_UNSET_RAW_MEM;
-      
-            MC_ddfs(search_cycle);
-      
-            /*}else{
-
-            XBT_INFO("Next pair already visited ! ");
-
-            }*/
-
+          MC_SET_RAW_MEM;
+          xbt_fifo_unshift(mc_stack_liveness, pair_succ);
+          MC_UNSET_RAW_MEM;
+          
+          MC_ddfs(search_cycle);
+          
         }
 
         /* Restore system before checking others successors */
         if(cursor != xbt_dynar_length(successors) - 1)
           MC_replay_liveness(mc_stack_liveness, 1);
 
-   
-      }
-           
+      }           
+
     }
     
   }else{
     
-    XBT_INFO("Max depth reached");
-
+    XBT_WARN("/!\\ Max depth reached ! /!\\ ");
+    if(current_pair->requests > 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) == MAX_DEPTH_LIVENESS ){
-    XBT_INFO("Pair (graph=%p, automaton =%p, search_cycle = %d, depth = %d) shifted in stack, maximum depth reached", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) );
+  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_INFO("Pair (graph=%p, automaton =%p, search_cycle = %d, depth = %d) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) );
+    XBT_DEBUG("Pair (depth = %d) shifted in stack", xbt_fifo_size(mc_stack_liveness) );
   }
 
   
   MC_SET_RAW_MEM;
-  xbt_fifo_shift(mc_stack_liveness);
+  remove_pair = xbt_fifo_shift(mc_stack_liveness);
+  xbt_fifo_remove(mc_stack_liveness, remove_pair);
+  remove_pair = NULL;
   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
-    xbt_dynar_pop(reached_pairs, NULL);
-    //xbt_dynar_pop(reached_pairs_hash, NULL);
+    remove_pair_reached = xbt_dynar_pop_as(reached_pairs, mc_pair_reached_t);
+    pair_reached_free(remove_pair_reached);
+    remove_pair_reached = NULL;
   }
   MC_UNSET_RAW_MEM;
 
-  if(raw_mem_set)
-    MC_SET_RAW_MEM;
-  else
-    MC_UNSET_RAW_MEM;
+  /*if(initial_state_liveness->raw_mem_set)
+    MC_SET_RAW_MEM;*/
 
 }