Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
git checkout hypervisor
[simgrid.git] / src / mc / mc_liveness.c
index f01ccb9..424929e 100644 (file)
-#include "private.h"
-#include "unistd.h"
+/* Copyright (c) 2011-2013 Da SimGrid Team. All rights reserved.            */
 
-XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dfs, mc,
-                                "Logging specific to MC DFS algorithm");
+/* 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. */
 
-xbt_dynar_t initial_pairs = NULL;
-int max_pair = 0;
+#include "mc_private.h"
+#include <unistd.h>
+#include <sys/wait.h>
+
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
+                                "Logging specific to algorithms for liveness properties verification");
+
+/********* Global variables *********/
+
+xbt_dynar_t acceptance_pairs;
 xbt_dynar_t visited_pairs;
-xbt_dynar_t reached_pairs;
-
-mc_pairs_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){
-  mc_pairs_t p = NULL;
-  p = xbt_new0(s_mc_pairs_t, 1);
-  p->system_state = sn;
-   p->automaton_state = st;
-  p->graph_state = sg;
-  p->num = max_pair;
-  max_pair++;
-  return p;
-    
+xbt_dynar_t successors;
+
+
+/********* Static functions *********/
+
+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 = 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 */
+  int res;
+  int_f_void_t f;
+  unsigned int cursor = 0;
+  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();
+    xbt_dynar_push_as(new_pair->prop_ato, int, res);
+  }
+
+  return new_pair;
+
 }
 
-void set_pair_visited(mc_state_t gs, xbt_state_t as, int sc){
+static int is_reached_acceptance_pair(int num, xbt_automaton_state_t as){
+
+  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
-  //XBT_DEBUG("New visited pair : graph=%p, automaton=%p", gs, as);
   MC_SET_RAW_MEM;
-  mc_visited_pairs_t p = NULL;
-  p = xbt_new0(s_mc_visited_pairs_t, 1);
-  p->graph_state = gs;
-  p->automaton_state = as;
-  p->search_cycle = sc;
-  xbt_dynar_push(visited_pairs, &p); 
-  //XBT_DEBUG("New visited pair , length of visited pairs : %lu", xbt_dynar_length(visited_pairs));
+  mc_acceptance_pair_t new_pair = acceptance_pair_new(num, as);  
   MC_UNSET_RAW_MEM;
+  
+  if(xbt_dynar_is_empty(acceptance_pairs)){
 
-  //XBT_DEBUG("New visited pair , length of visited pairs : %lu", xbt_dynar_length(visited_pairs));
-}
+    MC_SET_RAW_MEM;
+    xbt_dynar_push(acceptance_pairs, &new_pair); 
+    MC_UNSET_RAW_MEM;
 
-int reached(mc_state_t gs, xbt_state_t as ){
+    if(raw_mem_set)
+      MC_SET_RAW_MEM;
 
-  mc_reached_pairs_t rp = NULL;
-  unsigned int c= 0;
-  unsigned int i;
-  int different_process;
+    return -1;
 
-  MC_SET_RAW_MEM;
-  xbt_dynar_foreach(reached_pairs, c, rp){
-    if(rp->automaton_state == as){
-      different_process=0;
-      for(i=0; i < gs->max_pid; i++){
-       if(gs->proc_status[i].state != rp->graph_state->proc_status[i].state){
-         different_process++;
-       }
-      }
-      if(different_process==0){
-       MC_UNSET_RAW_MEM;
-       XBT_DEBUG("Pair (graph=%p, automaton=%p(%s)) already reached (graph=%p)!", gs, as, as->id, rp->graph_state);
-       return 1;
+  }else{
+
+    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 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++;
+          }
+        }
       }
-      /* XBT_DEBUG("Pair (graph=%p, automaton=%p(%s)) already reached !", gs, as, as->id); */
-      /* return 1; */
     }
-  }
-  MC_UNSET_RAW_MEM;
-  return 0;
-}
 
-void set_pair_reached(mc_state_t gs, xbt_state_t as){
+    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;
 
-  //XBT_DEBUG("Set pair (graph=%p, automaton=%p) reached ", gs, as);
-  //if(reached(gs, as) == 0){
-    MC_SET_RAW_MEM;
-    mc_reached_pairs_t p = NULL;
-    p = xbt_new0(s_mc_reached_pairs_t, 1);
-    p->graph_state = gs;
-    p->automaton_state = as;
-    xbt_dynar_push(reached_pairs, &p); 
-    XBT_DEBUG("New reached pair : graph=%p, automaton=%p(%s)", gs, as, as->id);
+    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;
+    
+    return -1;
+    
+  }
 }
 
-int visited(mc_state_t gs, xbt_state_t as, int sc){
-  unsigned int c = 0;
-  mc_visited_pairs_t p = NULL;
-  unsigned int i;
-  int different_process;
 
-  //XBT_DEBUG("Visited pair length : %lu", xbt_dynar_length(visited_pairs));
+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;
-  xbt_dynar_foreach(visited_pairs, c, p){
-    //XBT_DEBUG("Test pair visited");
-    //sleep(1);
-    if((p->automaton_state == as) && (p->search_cycle == sc)){
-      different_process=0;
-      for(i=0; i < gs->max_pid; i++){
-       if(gs->proc_status[i].state != p->graph_state->proc_status[i].state){
-         different_process++;
-       }
-      }
-      if(different_process==0){
-       MC_UNSET_RAW_MEM;
-       return 1;
+  mc_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;
+     xbt_dynar_push(acceptance_pairs, &new_pair); 
+     MC_UNSET_RAW_MEM;
+
+  }else{
+
+    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;
+    
   }
-  MC_UNSET_RAW_MEM;
-  return 0;
 
+  if(raw_mem_set)
+    MC_SET_RAW_MEM;
+    
 }
 
-void MC_dfs_init(xbt_automaton_t a){
+static void remove_acceptance_pair(int num_pair){
 
-   XBT_DEBUG("**************************************************");
-   XBT_DEBUG("DFS init");
-   XBT_DEBUG("**************************************************");
-  mc_pairs_t mc_initial_pair;
-  mc_state_t initial_graph_state;
-  smx_process_t process; 
-  mc_snapshot_t init_snapshot;
-  MC_wait_for_requests();
+  unsigned int cursor = 0;
+  mc_acceptance_pair_t current_pair;
 
-  MC_SET_RAW_MEM;
+  xbt_dynar_foreach(acceptance_pairs, cursor, current_pair){
+    if(current_pair->num == num_pair)
+      break;
+  }
+  
+  xbt_dynar_remove_at(acceptance_pairs, cursor, NULL);
 
-  init_snapshot = xbt_new0(s_mc_snapshot_t, 1);
+}
 
-  initial_graph_state = MC_state_pair_new();
-  xbt_swag_foreach(process, simix_global->process_list){
-    if(MC_process_is_enabled(process)){
-      MC_state_interleave_process(initial_graph_state, process);
-    }
-  }
+static mc_visited_pair_t visited_pair_new(int num, xbt_automaton_state_t as){
 
-  visited_pairs = xbt_dynar_new(sizeof(mc_visited_pairs_t), NULL); 
-  reached_pairs = xbt_dynar_new(sizeof(mc_reached_pairs_t), NULL); 
+  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->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_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();
+    xbt_dynar_push_as(new_pair->prop_ato, int, res);
+  }
 
-  MC_take_snapshot(init_snapshot);
+  return new_pair;
 
-  MC_UNSET_RAW_MEM; 
+}
 
-  /* unsigned int cursor = 0; */
-  /* xbt_state_t state = NULL; */
-  /* int nb_init_state = 0; */
+static int is_visited_pair(int num, xbt_automaton_state_t as){
 
-  /* xbt_dynar_foreach(a->states, cursor, state){ */
-  /*   if(state->type == -1){ */
+  if(_sg_mc_visited == 0)
+    return -1;
 
-  /*     MC_SET_RAW_MEM; */
-  /*     mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state); */
+  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
-  /*     xbt_fifo_unshift(mc_snapshot_stack, mc_initial_pair); */
+  MC_SET_RAW_MEM;
+  mc_visited_pair_t new_pair = visited_pair_new(num, as);
+  MC_UNSET_RAW_MEM;
 
-  /*     XBT_DEBUG("**************************************************"); */
-  /*     XBT_DEBUG("Initial state=%p ", mc_initial_pair); */
+  if(xbt_dynar_is_empty(visited_pairs)){
 
-  /*     MC_UNSET_RAW_MEM; */
+    MC_SET_RAW_MEM;
+    xbt_dynar_push(visited_pairs, &new_pair); 
+    MC_UNSET_RAW_MEM;
 
-  /*     set_pair_visited(mc_initial_pair->graph_state, mc_initial_pair->automaton_state, 0); */
-      
-  /*     if(nb_init_state == 0) */
-  /*   MC_dfs(a, 0, 0); */
-  /*     else */
-  /*   MC_dfs(a, 0, 1); */
-      
-  /*     nb_init_state++; */
-  /*   } */
-  /* } */
+    if(raw_mem_set)
+      MC_SET_RAW_MEM;
 
-  /* regarder dans l'automate toutes les transitions activables grâce à l'état initial du système 
-    -> donnera les états initiaux de la propriété consistants avec l'état initial du système */
+    return -1;
 
-  unsigned int cursor = 0;
-  unsigned int cursor2 = 0;
-  xbt_state_t state = NULL;
-  int res;
-  xbt_transition_t transition_succ;
-  xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
-  xbt_dynar_t elses = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
-  mc_pairs_t pair_succ;
-
-  xbt_dynar_foreach(a->states, cursor, state){
-    if(state->type == -1){
-      xbt_dynar_foreach(state->out, cursor2, transition_succ){
-       res = MC_automaton_evaluate_label(a, transition_succ->label);
-       
-       if(res == 1){
-        
-         MC_SET_RAW_MEM;
-
-         mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
-         xbt_dynar_push(successors, &mc_initial_pair);
-
-         MC_UNSET_RAW_MEM;
-
-       }else{
-         if(res == 2){
-        
-           MC_SET_RAW_MEM;
-
-           mc_initial_pair = new_pair(init_snapshot, initial_graph_state, transition_succ->dst);
-           xbt_dynar_push(elses, &mc_initial_pair);
-
-           MC_UNSET_RAW_MEM;
-         }
-       }
-      }
-    }
-  }
+  }else{
 
-  cursor = 0;
-  xbt_dynar_foreach(successors, cursor, pair_succ){
     MC_SET_RAW_MEM;
+    
+    size_t current_bytes_used = new_pair->heap_bytes_used;
+    int current_nb_processes = new_pair->nb_processes;
 
-    xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
+    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++;
+          }
+        }
+      }
+    }
 
-    XBT_DEBUG("**************************************************");
-    XBT_DEBUG("Initial pair=%p (graph=%p, automaton=%p(%s)) ", pair_succ, pair_succ->graph_state, pair_succ->automaton_state,pair_succ->automaton_state->id );
+    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);
+    }
 
+    /*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;
 
-    set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, 0);
+    if(raw_mem_set)
+      MC_SET_RAW_MEM;
+    
+    return -1;
+    
+  }
+}
 
-    if(cursor == 0){
-      MC_dfs(a, 0, 0);
-    }else{
-      MC_dfs(a, 0, 1);
+static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l){
+  
+  switch(l->type){
+  case 0 : {
+    int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
+    int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
+    return (left_res || right_res);
+  }
+  case 1 : {
+    int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
+    int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
+    return (left_res && right_res);
+  }
+  case 2 : {
+    int res = MC_automaton_evaluate_label(l->u.exp_not);
+    return (!res);
+  }
+  case 3 : { 
+    unsigned int cursor = 0;
+    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 -1;
   }
+  case 4 : {
+    return 2;
+  }
+  default : 
+    return -1;
+  }
+}
 
-  cursor = 0;
-  xbt_dynar_foreach(elses, cursor, pair_succ){
-    MC_SET_RAW_MEM;
-
-    xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
 
-    XBT_DEBUG("**************************************************");
-    XBT_DEBUG("Initial pair=%p (graph=%p, automaton=%p(%s)) ", pair_succ, pair_succ->graph_state, pair_succ->automaton_state,pair_succ->automaton_state->id );
+/********* Free functions *********/
 
-    MC_UNSET_RAW_MEM;
+static void visited_pair_free(mc_visited_pair_t pair){
+  if(pair){
+    xbt_dynar_free(&(pair->prop_ato));
+    MC_free_snapshot(pair->system_state);
+    xbt_free(pair);
+  }
+}
 
-    set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, 0);
+static void visited_pair_free_voidp(void *p){
+  visited_pair_free((mc_visited_pair_t) * (void **) p);
+}
 
-    if((xbt_dynar_length(successors) == 0) && (cursor == 0)){
-      MC_dfs(a, 0, 0);
-    }else{
-      MC_dfs(a, 0, 1);
-    }
+static void acceptance_pair_free(mc_acceptance_pair_t pair){
+  if(pair){
+    xbt_dynar_free(&(pair->prop_ato));
+    MC_free_snapshot(pair->system_state);
+    xbt_free(pair);
   }
-  
 }
 
+static void acceptance_pair_free_voidp(void *p){
+  acceptance_pair_free((mc_acceptance_pair_t) * (void **) p);
+}
 
-void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){
 
-  smx_process_t process = NULL;
+/********* DDFS Algorithm *********/
 
 
-  if(xbt_fifo_size(mc_snapshot_stack) == 0)
-    return;
+void MC_ddfs_init(void){
 
-  if(restore == 1){
-    MC_restore_snapshot(((mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)))->system_state);
-    MC_UNSET_RAW_MEM;
-  }
+  initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
-  //XBT_DEBUG("Lpv length after restore snapshot: %lu", xbt_dynar_length(visited_pairs));
+  XBT_DEBUG("**************************************************");
+  XBT_DEBUG("Double-DFS init");
+  XBT_DEBUG("**************************************************");
 
-  /* Get current state */
-  mc_pairs_t current_pair = (mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
+  mc_pair_t mc_initial_pair = NULL;
+  mc_state_t initial_graph_state = NULL;
+  smx_process_t process; 
 
-  if(restore==1){
-    xbt_swag_foreach(process, simix_global->process_list){
-      if(MC_process_is_enabled(process)){
-       //XBT_DEBUG("Pid : %lu", process->pid);
-       MC_state_interleave_process(current_pair->graph_state, process);
-      }
+  MC_wait_for_requests();
+
+  MC_SET_RAW_MEM;
+
+  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);
     }
   }
 
-  XBT_DEBUG("************************************************** ( search_cycle = %d )", search_cycle);
-  XBT_DEBUG("State : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id,MC_state_interleave_size(current_pair->graph_state));
-  //XBT_DEBUG("Restore : %d", restore);
-  
-  //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+  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();
+
+  MC_UNSET_RAW_MEM; 
   
-  //sleep(1);
+  unsigned int cursor = 0;
+  xbt_automaton_state_t automaton_state;
 
-  mc_stats_pair->visited_pairs++;
+  xbt_dynar_foreach(_mc_property_automaton->states, cursor, automaton_state){
+    if(automaton_state->type == -1){
+      
+      MC_SET_RAW_MEM;
+      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->snapshot);
+        MC_UNSET_RAW_MEM;
+      }
 
-  int value;
-  mc_state_t next_graph_state = NULL;
-  smx_req_t req = NULL;
-  char *req_str;
+      MC_ddfs(0);
 
-  mc_pairs_t pair_succ;
-  xbt_transition_t transition_succ;
-  unsigned int cursor;
-  int res;
-  //int enabled_transition = 0;
+    }else{
+      if(automaton_state->type == 2){
+      
+        MC_SET_RAW_MEM;
+        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;
 
-  xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
-  xbt_dynar_t elses = xbt_dynar_new(sizeof(mc_pairs_t), NULL);
+        set_acceptance_pair_reached(mc_initial_pair->num, automaton_state);
 
-  mc_pairs_t next_pair;
-  mc_snapshot_t next_snapshot;
-  mc_snapshot_t current_snapshot;
+        if(cursor != 0){
+          MC_restore_snapshot(initial_state_liveness->snapshot);
+          MC_UNSET_RAW_MEM;
+        }
   
+        MC_ddfs(1);
   
-  while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
+      }
+    }
+  }
 
+  if(initial_state_liveness->raw_mem_set)
     MC_SET_RAW_MEM;
-    current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
-    MC_take_snapshot(current_snapshot);
+  else
     MC_UNSET_RAW_MEM;
-   
-    
-    /* Debug information */
-    if(XBT_LOG_ISENABLED(mc_dfs, xbt_log_priority_debug)){
-      req_str = MC_request_to_string(req, value);
-      XBT_DEBUG("Execute: %s", req_str);
-      xbt_free(req_str);
-    }
+  
 
-    MC_state_set_executed_request(current_pair->graph_state, req, value);
+}
 
-    /* Answer the request */
-    SIMIX_request_pre(req, value);
 
-    /* Wait for requests (schedules processes) */
-    MC_wait_for_requests();
+void MC_ddfs(int search_cycle){
 
+  smx_process_t process;
+  mc_pair_t current_pair = NULL;
 
-    /* Create the new expanded graph_state */
-    MC_SET_RAW_MEM;
+  if(xbt_fifo_size(mc_stack_liveness) == 0)
+    return;
 
-    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("Pid : %lu", process->pid);
-       MC_state_interleave_process(next_graph_state, process);
-      }
-    }
 
-    next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
-    MC_take_snapshot(next_snapshot);
-      
-    MC_UNSET_RAW_MEM;
+  /* Get current pair */
+  current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
 
-    xbt_dynar_reset(successors);
-    xbt_dynar_reset(elses);
-    
-    cursor = 0;
-    xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
-
-      res = MC_automaton_evaluate_label(a, transition_succ->label);
+  /* Update current state in buchi automaton */
+  _mc_property_automaton->current_state = current_pair->automaton_state;
 
-      MC_SET_RAW_MEM;
-      next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
-
-      //XBT_DEBUG("Next pair : %p", next_pair);
-       
-      if(res == 1){ // enabled transition in automaton
-       xbt_dynar_push(successors, &next_pair);
-       mc_stats_pair->expanded_pairs++;
-      }else{
-       if(res == 2){ // enabled transition in automaton
-         xbt_dynar_push(elses, &next_pair);
-         mc_stats_pair->expanded_pairs++;
-       }
-      }
+  XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
+  mc_stats->visited_pairs++;
 
-      MC_UNSET_RAW_MEM;
-    }
+  int value;
+  mc_state_t next_graph_state = NULL;
+  smx_simcall_t req = NULL;
+  char *req_str;
 
-   
-    if(xbt_dynar_length(successors) == 0){
+  xbt_automaton_transition_t transition_succ;
+  unsigned int cursor = 0;
+  int res;
+  int reached_num;
 
-      MC_SET_RAW_MEM;
-      next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state);
-      xbt_dynar_push(successors, &next_pair);
-      mc_stats_pair->expanded_pairs++;
-      MC_UNSET_RAW_MEM;
-       
-    }
+  mc_pair_t next_pair = NULL;
+  mc_pair_t pair_succ;
 
+  mc_pair_t pair_to_remove;
+  
+  if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
 
-    cursor = 0;
-    xbt_dynar_foreach(successors, cursor, pair_succ){
+    if(current_pair->requests > 0){
 
-      //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
+      while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
+   
+        /* Debug information */
+       
+        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);
+        }
 
-      if((search_cycle == 1) && (reached(pair_succ->graph_state, pair_succ->automaton_state) == 1)){
-       XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
-       XBT_INFO("|             ACCEPTANCE CYCLE            |");
-       XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
-       XBT_INFO("Counter-example that violates formula :");
-       MC_show_snapshot_stack(mc_snapshot_stack);
-       MC_dump_snapshot_stack(mc_snapshot_stack);
-       MC_print_statistics_pairs(mc_stats_pair);
-       exit(0);
-      }
-       
-      if(visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle) == 0){
+        MC_state_set_executed_request(current_pair->graph_state, req, value);  
+        mc_stats->executed_transitions++;
 
-       //XBT_DEBUG("Unvisited pair !");
+        /* Answer the request */
+        SIMIX_simcall_pre(req, value);
 
-       mc_stats_pair->executed_transitions++;
-       MC_SET_RAW_MEM;
-       xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
-       MC_UNSET_RAW_MEM;
+        /* Wait for requests (schedules processes) */
+        MC_wait_for_requests();
 
-       set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle);
-       MC_dfs(a, search_cycle, 0);
+        MC_SET_RAW_MEM;
 
-       if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
+        /* Create the new expanded graph_state */
+        next_graph_state = MC_state_new();
 
-         MC_restore_snapshot(current_pair->system_state);
-         MC_UNSET_RAW_MEM;
-         xbt_swag_foreach(process, simix_global->process_list){
-           if(MC_process_is_enabled(process)){
-             //XBT_DEBUG("Pid : %lu", process->pid);
-             MC_state_interleave_process(current_pair->graph_state, process);
-           }
-         }
-           
-         set_pair_reached(current_pair->graph_state, current_pair->automaton_state);
-         XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
-         MC_dfs(a, 1, 1);
-
-       }
-      }
-    }
+        /* 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); 
+          }
+        }
 
-    cursor = 0;
-    xbt_dynar_foreach(elses, cursor, pair_succ){
+        xbt_swag_foreach(process, simix_global->process_list){
+          if(MC_process_is_enabled(process)){
+            MC_state_interleave_process(next_graph_state, process);
+          }
+        }
 
-      //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
+        xbt_dynar_reset(successors);
 
-      if((search_cycle == 1) && (reached(pair_succ->graph_state, pair_succ->automaton_state) == 1)){
-       XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
-       XBT_INFO("|             ACCEPTANCE CYCLE            |");
-       XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
-       XBT_INFO("Counter-example that violates formula :");
-       MC_show_snapshot_stack(mc_snapshot_stack);
-       MC_dump_snapshot_stack(mc_snapshot_stack);
-       MC_print_statistics_pairs(mc_stats_pair);
-       exit(0);
-      }
-       
-      if(visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle) == 0){
+        MC_UNSET_RAW_MEM;
 
-       //XBT_DEBUG("Unvisited pair !");
 
-       mc_stats_pair->executed_transitions++;
-       MC_SET_RAW_MEM;
-       xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
-       MC_UNSET_RAW_MEM;
+        cursor= 0;
+        xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 
-       set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle);
-       MC_dfs(a, search_cycle, 0);
+          res = MC_automaton_evaluate_label(transition_succ->label);
 
-       if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
+          if(res == 1){ // enabled transition in automaton
+            MC_SET_RAW_MEM;
+            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;
+          }
 
-         MC_restore_snapshot(current_pair->system_state);
-         MC_UNSET_RAW_MEM;
-         xbt_swag_foreach(process, simix_global->process_list){
-           if(MC_process_is_enabled(process)){
-             //XBT_DEBUG("Pid : %lu", process->pid);
-             MC_state_interleave_process(current_pair->graph_state, process);
-           }
-         }
-           
-         set_pair_reached(current_pair->graph_state, current_pair->automaton_state);
-         XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
-         MC_dfs(a, 1, 1);
-
-       }
-      }
-    }
-    
-    
-    if(MC_state_interleave_size(current_pair->graph_state) > 0){
-      MC_restore_snapshot(current_snapshot);
-      MC_UNSET_RAW_MEM;
-      //XBT_DEBUG("Snapshot restored");
-    }
-  }
+        }
 
+        cursor = 0;
+   
+        xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
+      
+          res = MC_automaton_evaluate_label(transition_succ->label);
   
-  MC_SET_RAW_MEM;
-  //remove_pair_reached(current_pair->graph_state);
-  xbt_fifo_shift(mc_snapshot_stack);
-  XBT_DEBUG("State (graph=%p, automaton =%p) shifted in snapshot_stack", current_pair->graph_state, current_pair->automaton_state);
-  MC_UNSET_RAW_MEM;
+          if(res == 2){ // true transition in automaton
+            MC_SET_RAW_MEM;
+            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;
+          }
 
-}
+        }
 
-void MC_show_snapshot_stack(xbt_fifo_t stack){
-  int value;
-  mc_pairs_t pair;
-  xbt_fifo_item_t item;
-  smx_req_t req;
-  char *req_str = NULL;
+        cursor = 0; 
   
-  for (item = xbt_fifo_get_last_item(stack);
-       (item ? (pair = (mc_pairs_t) (xbt_fifo_get_item_content(item)))
-        : (NULL)); item = xbt_fifo_get_prev_item(item)) {
-    req = MC_state_get_executed_request(pair->graph_state, &value);
-    if(req){
-      req_str = MC_request_to_string(req, value);
-      XBT_INFO("%s", req_str);
-      xbt_free(req_str);
-    }
-  }
-}
+        xbt_dynar_foreach(successors, cursor, pair_succ){
 
-void MC_dump_snapshot_stack(xbt_fifo_t stack){
-  mc_pairs_t pair;
+          if(search_cycle == 1){
 
-  MC_SET_RAW_MEM;
-  while ((pair = (mc_pairs_t) xbt_fifo_pop(stack)) != NULL)
-    MC_pair_delete(pair);
-  MC_UNSET_RAW_MEM;
-}
+            if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
+          
+              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 (equal to state %d) !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state), reached_num);
 
-void MC_pair_delete(mc_pairs_t pair){
-  xbt_free(pair->graph_state->proc_status);
-  xbt_free(pair->graph_state);
-  //xbt_free(pair->automaton_state); -> FIXME : à implémenter
-  xbt_free(pair);
-}
+                XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
+                XBT_INFO("|             ACCEPTANCE CYCLE            |");
+                XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
+                XBT_INFO("Counter-example that violates formula :");
+                MC_show_stack_liveness(mc_stack_liveness);
+                MC_dump_stack_liveness(mc_stack_liveness);
+                MC_print_statistics(mc_stats);
+                xbt_abort();
 
+              }else{
 
-int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){
-  
-  switch(l->type){
-  case 0 : {
-    int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
-    int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
-    return (left_res || right_res);
-    break;
-  }
-  case 1 : {
-    int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
-    int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
-    return (left_res && right_res);
-    break;
-  }
-  case 2 : {
-    int res = MC_automaton_evaluate_label(a, l->u.exp_not);
-    return (!res);
-    break;
-  }
-  case 3 : { 
-    unsigned int cursor = 0;
-    xbt_propositional_symbol_t p = NULL;
-    xbt_dynar_foreach(a->propositional_symbols, cursor, p){
-      if(strcmp(p->pred, l->u.predicat) == 0){
-       int (*f)() = p->function;
-       return (*f)();
-      }
-    }
-    return -1;
-    break;
-  }
-  case 4 : {
-    return 2;
-    break;
-  }
-  default : 
-    return -1;
-  }
-}
+                if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
 
-/*void MC_dfs(xbt_automaton_t a, int search_cycle){
+                  XBT_DEBUG("Next pair already visited !");
+                  break;
+            
+                }else{
 
-  xbt_state_t current_state = (xbt_state_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(stack_automaton_dfs));
-  xbt_transition_t transition_succ = NULL;
-  xbt_state_t successor = NULL;
-  unsigned int cursor = 0;
-  xbt_dynar_t elses = xbt_dynar_new(sizeof(xbt_transition_t), NULL);
-  int res;
+                  XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 
-  //printf("++ current state : %s\n", current_state->id);
-
-  xbt_dynar_foreach(current_state->out, cursor, transition_succ){
-    successor = transition_succ->dst; 
-    res = MC_automaton_evaluate_label(a, transition_succ->label);
-    //printf("-- state : %s, transition_label : %d, res = %d\n", successor->id, transition_succ->label->type, res);
-    if(res == 1){
-      if(search_cycle == 1 && reached_dfs != NULL){
-       if(strcmp(reached_dfs->id, successor->id) == 0){
-         xbt_dynar_push(state_automaton_visited_dfs, &successor); 
-         printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n");
-         printf("Visited states : \n");
-         unsigned int cursor2 = 0;
-         xbt_state_t visited_state = NULL;
-         xbt_dynar_foreach(state_automaton_visited_dfs, cursor2, visited_state){
-           printf("State : %s\n", visited_state->id);
-         }
-         exit(1);
-       }
-      }
-      if(successor->visited == 0){
-       successor->visited = 1;
-       xbt_fifo_unshift(stack_automaton_dfs, successor);
-       xbt_dynar_push(state_automaton_visited_dfs, &successor);      
-       MC_dfs(a, search_cycle);
-       if(search_cycle == 0 && successor->type == 1){
-         reached_dfs = successor;
-         MC_dfs(a, 1);
-       }
-      }
-    }else{
-      if(res == 2){
-       xbt_dynar_push(elses,&transition_succ);
-      }
-    }
-  }
-  
-  cursor = 0;
-  xbt_dynar_foreach(elses, cursor, transition_succ){
-   successor = transition_succ->dst; 
-   if(search_cycle == 1 && reached_dfs != NULL){
-     if(strcmp(reached_dfs->id, successor->id) == 0){
-       xbt_dynar_push(state_automaton_visited_dfs, &successor); 
-       printf("\n-*-*-*-*-*-*- ACCEPTANCE CYCLE -*-*-*-*-*-*-\n");
-       printf("Visited states : \n");
-       unsigned int cursor2 = 0;
-       xbt_state_t visited_state = NULL;
-       xbt_dynar_foreach(state_automaton_visited_dfs, cursor2, visited_state){
-        printf("State : %s\n", visited_state->id);
-       }
-       exit(1);
-     }
-   }
-   if(successor->visited == 0){
-     successor->visited = 1;
-     xbt_fifo_unshift(stack_automaton_dfs, successor);
-     xbt_dynar_push(state_automaton_visited_dfs, &successor);      
-     MC_dfs(a, search_cycle);
-     if(search_cycle == 0 && successor->type == 1){
-       reached_dfs = successor;
-       MC_dfs(a, 1);
-     }
-   }
-  }
+                  XBT_DEBUG("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_ddfs(search_cycle);
+                
+                }
 
-  xbt_fifo_shift(stack_automaton_dfs);
-  }*/
+              }
 
+            }else{
 
-/* void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){ */
+              if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
 
+                XBT_DEBUG("Next pair already visited !");
+                break;
+                
+              }else{
 
-/*   if(xbt_fifo_size(mc_snapshot_stack) == 0) */
-/*     return; */
+                MC_SET_RAW_MEM;
+                xbt_fifo_unshift(mc_stack_liveness, pair_succ);
+                MC_UNSET_RAW_MEM;
+                
+                MC_ddfs(search_cycle);
+              }
+               
+            }
 
-/*   if(restore == 1){ */
-/*     MC_restore_snapshot(((mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)))->system_state); */
-/*     MC_UNSET_RAW_MEM; */
-/*   } */
+          }else{
 
+            if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
 
-/*   //XBT_DEBUG("Lpv length after restore snapshot: %lu", xbt_dynar_length(visited_pairs)); */
+              XBT_DEBUG("Next pair already visited !");
+              break;
+            
+            }else{
+    
+              if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 
-/*   /\* Get current state *\/ */
-/*   mc_pairs_t current_pair = (mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)); */
+                XBT_DEBUG("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->num, pair_succ->automaton_state); 
 
-/*   XBT_DEBUG("************************************************** ( search_cycle = %d )", search_cycle); */
-/*   XBT_DEBUG("State : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id,MC_state_interleave_size(current_pair->graph_state)); */
-  
-/*   //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); */
-  
-/*   //sleep(1); */
-
-/*   smx_process_t process = NULL; */
-/*   int value; */
-/*   mc_state_t next_graph_state = NULL; */
-/*   smx_req_t req = NULL; */
-/*   char *req_str; */
-
-/*   mc_pairs_t pair_succ; */
-/*   xbt_transition_t transition_succ; */
-/*   unsigned int cursor; */
-/*   int res; */
-/*   //int enabled_transition = 0; */
-
-/*   xbt_dynar_t elses = xbt_dynar_new(sizeof(mc_pairs_t), NULL); */
-/*   xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pairs_t), NULL);  */
-/*   xbt_dynar_reset(all_successors); */
-
-/*   mc_pairs_t next_pair; */
-/*   mc_snapshot_t next_snapshot; */
-/*   mc_snapshot_t current_snapshot; */
-  
-/*   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){ */
+                search_cycle = 1;
 
-/*     //XBT_DEBUG("Current pair : %p (%u interleave)", current_pair, MC_state_interleave_size(current_pair->graph_state)+1); */
-/*     //XBT_DEBUG("Visited pairs : %lu", xbt_dynar_length(visited_pairs)); */
+                XBT_DEBUG("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
 
-/*     MC_SET_RAW_MEM; */
-/*     current_snapshot = xbt_new0(s_mc_snapshot_t, 1); */
-/*     MC_take_snapshot(current_snapshot); */
-/*     MC_UNSET_RAW_MEM; */
-   
-    
-/*     /\* Debug information *\/ */
-/*     if(XBT_LOG_ISENABLED(mc_dfs, xbt_log_priority_debug)){ */
-/*       req_str = MC_request_to_string(req, value); */
-/*       XBT_DEBUG("Execute: %s", req_str); */
-/*       xbt_free(req_str); */
-/*     } */
+              }
 
-/*     MC_state_set_executed_request(current_pair->graph_state, req, value); */
-/*     //mc_stats->executed_transitions++; */
+              MC_SET_RAW_MEM;
+              xbt_fifo_unshift(mc_stack_liveness, pair_succ);
+              MC_UNSET_RAW_MEM;
+            
+              MC_ddfs(search_cycle);
 
-/*     /\* Answer the request *\/ */
-/*     SIMIX_request_pre(req, value);  */
+            }
+           
+          }
 
-/*     /\* Wait for requests (schedules processes) *\/ */
-/*     MC_wait_for_requests(); */
+          /* 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_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
+          MC_replay_liveness(mc_stack_liveness, 0);
+        }
+      }
 
-/*     /\* Create the new expanded graph_state *\/ */
-/*     MC_SET_RAW_MEM; */
+    }else{
 
-/*     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)){ */
-/*     MC_state_interleave_process(next_graph_state, process); */
-/*       } */
-/*     } */
-
-/*     next_snapshot = xbt_new0(s_mc_snapshot_t, 1); */
-/*     MC_take_snapshot(next_snapshot); */
+      mc_stats->executed_transitions++;
       
-/*     MC_UNSET_RAW_MEM; */
+      XBT_DEBUG("No more request to execute in this state, search evolution in Büchi Automaton.");
 
-/*     xbt_dynar_reset(elses); */
-/*     xbt_dynar_reset(successors); */
-    
-/*     cursor = 0; */
-/*     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ */
+      MC_SET_RAW_MEM;
 
-/*       res = MC_automaton_evaluate_label(a, transition_succ->label); */
+      /* Create the new expanded graph_state */
+      next_graph_state = MC_state_new();
 
-/*       MC_SET_RAW_MEM; */
-/*       next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst); */
+      xbt_dynar_reset(successors);
 
-/*       //XBT_DEBUG("Next pair : %p", next_pair); */
-       
-/*       if(res == 1){ // enabled transition in automaton */
-/*     xbt_dynar_push(successors, &next_pair);    */
-/*     //XBT_DEBUG("New Successors length : %lu", xbt_dynar_length(successors)); */
-/*       }else{ */
-/*     if(res == 2){ */
-/*       xbt_dynar_push(elses, &next_pair); */
-/*       //XBT_DEBUG("New Elses length : %lu", xbt_dynar_length(elses)); */
-/*     } */
-/*       } */
+      MC_UNSET_RAW_MEM;
 
-/*       MC_UNSET_RAW_MEM; */
-/*     } */
 
-   
-/*     if((xbt_dynar_length(successors) == 0) && (xbt_dynar_length(elses) == 0) ){ */
+      cursor= 0;
+      xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 
-/*       MC_SET_RAW_MEM; */
-/*       next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state); */
-/*       xbt_dynar_push(successors, &next_pair); */
-/*       MC_UNSET_RAW_MEM; */
-       
-/*     } */
+        res = MC_automaton_evaluate_label(transition_succ->label);
 
-/*     //XBT_DEBUG("Successors length : %lu", xbt_dynar_length(successors)); */
-/*     //XBT_DEBUG("Elses length : %lu", xbt_dynar_length(elses)); */
+        if(res == 1){ // enabled transition in automaton
+          MC_SET_RAW_MEM;
+          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;
+        }
 
-/*     if(xbt_dynar_length(successors) > 0){ */
+      }
+
+      cursor = 0;
+   
+      xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
+      
+        res = MC_automaton_evaluate_label(transition_succ->label);
+  
+        if(res == 2){ // true transition in automaton
+          MC_SET_RAW_MEM;
+          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;
+        }
 
-/*       cursor = 0; */
-/*       xbt_dynar_foreach(successors, cursor, pair_succ){ */
-/*     MC_SET_RAW_MEM; */
-/*     xbt_dynar_push(all_successors, &pair_succ); */
-/*     MC_UNSET_RAW_MEM; */
-/*       } */
+      }
 
-/*     }else{  */
+      cursor = 0; 
+     
+      xbt_dynar_foreach(successors, cursor, pair_succ){
+
+        if(search_cycle == 1){
+
+          if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
+
+            if((reached_num = is_reached_acceptance_pair(pair_succ->num, pair_succ->automaton_state)) != -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            |");
+              XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
+              XBT_INFO("Counter-example that violates formula :");
+              MC_show_stack_liveness(mc_stack_liveness);
+              MC_dump_stack_liveness(mc_stack_liveness);
+              MC_print_statistics(mc_stats);
+              xbt_abort();
+
+            }else{
+
+              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("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_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_ddfs(search_cycle);
+
+            }
+            
+          }
+      
 
-/*       cursor = 0; */
-/*       xbt_dynar_foreach(elses, cursor, pair_succ){ */
-/*     MC_SET_RAW_MEM; */
-/*     xbt_dynar_push(all_successors, &pair_succ); */
-/*     MC_UNSET_RAW_MEM; */
-/*       } */
+        }else{
+      
+          if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
 
-/*     }  */
+            XBT_DEBUG("Next pair already visited !");
+            break;
+            
+          }else{
 
-/*     MC_restore_snapshot(current_snapshot); */
-/*     MC_UNSET_RAW_MEM; */
-     
-/*   }    */
+            if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 
-/*   //XBT_DEBUG("All successors : %lu", xbt_dynar_length(all_successors)); */
+              set_acceptance_pair_reached(pair_succ->num, pair_succ->automaton_state);
+         
+              search_cycle = 1;
 
-/*   cursor = 0; */
+              XBT_INFO("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));
 
-/*   xbt_dynar_foreach(all_successors, cursor, pair_succ){ */
+            }
 
-/*     if((search_cycle == 1) && (reached(pair_succ->graph_state, pair_succ->automaton_state) == 1)){ */
-/*       XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); */
-/*       XBT_INFO("|             ACCEPTANCE CYCLE            |"); */
-/*       XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); */
-/*       XBT_INFO("Counter-example that violates formula :"); */
-/*       MC_show_snapshot_stack(mc_snapshot_stack); */
-/*       MC_dump_snapshot_stack(mc_snapshot_stack); */
-/*       exit(0); */
-/*     } */
-       
-/*     if(visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle) == 0){ */
+            MC_SET_RAW_MEM;
+            xbt_fifo_unshift(mc_stack_liveness, pair_succ);
+            MC_UNSET_RAW_MEM;
+          
+            MC_ddfs(search_cycle);
+          
+          }
+          
+        }
 
-/*       //XBT_DEBUG("New pair in stack"); */
-/*       MC_SET_RAW_MEM; */
-/*       xbt_fifo_unshift(mc_snapshot_stack, pair_succ); */
-/*       MC_UNSET_RAW_MEM; */
+        /* Restore system before checking others successors */
+        if(cursor != xbt_dynar_length(successors) - 1)
+          MC_replay_liveness(mc_stack_liveness, 1);
 
-/*       set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle); */
-/*       MC_dfs(a, search_cycle, 1); */
+      }           
 
-/*       if((search_cycle == 0) && (pair_succ->automaton_state->type == 1)){ */
-           
-/*     set_pair_reached(pair_succ->graph_state, pair_succ->automaton_state);  */
-/*     XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); */
-/*     MC_dfs(a, 1, 1); */
+    }
+    
+  }else{
+    
+    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) == _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) );
+  }
 
-/*   } */
   
-/*   MC_SET_RAW_MEM; */
-/*   //remove_pair_reached(current_pair->graph_state); */
-/*   xbt_fifo_shift(mc_snapshot_stack); */
-/*   XBT_DEBUG("State (graph=%p, automaton =%p) shifted in snapshot_stack", current_pair->graph_state, current_pair->automaton_state); */
-/*   MC_UNSET_RAW_MEM; */
+  MC_SET_RAW_MEM;
+  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_acceptance_pair(current_pair->num);
+  }
+  MC_UNSET_RAW_MEM;
 
-/* } */
+}