model-checker : cleanups

[simgrid.git] / src / mc / mc_liveness.c

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 06265cb..ac9b74d 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -1,4 +1,4 @@
-/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved.            */
+/* Copyright (c) 2011-2013 Da SimGrid Team. All rights reserved.            */

 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */


@@ -10,56 +10,24 @@
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
                                 "Logging specific to algorithms for liveness properties verification");
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
                                 "Logging specific to algorithms for liveness properties verification");
 

-xbt_dynar_t reached_pairs;
+/********* Global variables *********/
+
+xbt_dynar_t acceptance_pairs;

 xbt_dynar_t visited_pairs;
 xbt_dynar_t successors;
 
 xbt_dynar_t visited_pairs;
 xbt_dynar_t successors;
 

-int create_dump(int pair)
-{
-   // Try to enable core dumps
-  struct rlimit core_limit;
-  core_limit.rlim_cur = RLIM_INFINITY;
-  core_limit.rlim_max = RLIM_INFINITY;
-  
-  if(setrlimit(RLIMIT_CORE, &core_limit) < 0)
-    fprintf(stderr, "setrlimit: %s\nWarning: core dumps may be truncated or non-existant\n", strerror(errno));
-  
-  int status;
-  switch(fork()){
-  case 0:
-    // We are the child process -- run the actual program
-    xbt_abort();
-    break;
-    
-  case -1:
-    // An error occurred, shouldn't happen
-    perror("fork");
-    return -1;
-    
-  default:
-    // We are the parent process -- wait for the child process to exit
-    if(wait(&status) < 0)
-      perror("wait");
-    if(WIFSIGNALED(status) && WCOREDUMP(status)){
-      char *core_name = xbt_malloc(20);
-      sprintf(core_name,"core_%d", pair); 
-      rename("core", core_name);
-      free(core_name);
-    }
-  }

 
 

-  return 0;
-}
+/********* Static functions *********/

 
 

-int reached(xbt_state_t st){
+static int is_reached_acceptance_pair(xbt_automaton_state_t st){

 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
   MC_SET_RAW_MEM;
 
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
   MC_SET_RAW_MEM;
 

-  mc_pair_reached_t new_pair = NULL;
-  new_pair = xbt_new0(s_mc_pair_reached_t, 1);
-  new_pair->nb = xbt_dynar_length(reached_pairs) + 1;
+  mc_acceptance_pair_t new_pair = NULL;
+  new_pair = xbt_new0(s_mc_acceptance_pair_t, 1);
+  new_pair->num = xbt_dynar_length(acceptance_pairs) + 1;

   new_pair->automaton_state = st;
   new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
   new_pair->system_state = MC_take_snapshot();  
   new_pair->automaton_state = st;
   new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
   new_pair->system_state = MC_take_snapshot();  


@@ -68,7 +36,7 @@ int reached(xbt_state_t st){
   int res;
   int_f_void_t f;
   unsigned int cursor = 0;
   int res;
   int_f_void_t f;
   unsigned int cursor = 0;

-  xbt_propositional_symbol_t ps = NULL;
+  xbt_automaton_propositional_symbol_t ps = NULL;

   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
     f = (int_f_void_t)ps->function;
     res = f();
   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
     f = (int_f_void_t)ps->function;
     res = f();


@@ -77,11 +45,11 @@ int reached(xbt_state_t st){
   
   MC_UNSET_RAW_MEM;
   
   
   MC_UNSET_RAW_MEM;
   

-  if(xbt_dynar_is_empty(reached_pairs)/* || !compare*/){
+  if(xbt_dynar_is_empty(acceptance_pairs)){

 
     MC_SET_RAW_MEM;
 
     MC_SET_RAW_MEM;

-    /* New pair reached */
-    xbt_dynar_push(reached_pairs, &new_pair); 
+    /* New acceptance pair */
+    xbt_dynar_push(acceptance_pairs, &new_pair); 

     MC_UNSET_RAW_MEM;
 
     if(raw_mem_set)
     MC_UNSET_RAW_MEM;
 
     if(raw_mem_set)


@@ -94,13 +62,13 @@ int reached(xbt_state_t st){
     MC_SET_RAW_MEM;
     
     cursor = 0;
     MC_SET_RAW_MEM;
     
     cursor = 0;

-    mc_pair_reached_t pair_test = NULL;
+    mc_acceptance_pair_t pair_test = NULL;

      
      

-    xbt_dynar_foreach(reached_pairs, cursor, pair_test){
+    xbt_dynar_foreach(acceptance_pairs, cursor, pair_test){

       if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug))
       if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug))

-        XBT_DEBUG("****** Pair reached #%d ******", pair_test->nb);
-      if(automaton_state_compare(pair_test->automaton_state, st) == 0){
-        if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
+        XBT_DEBUG("****** Pair reached #%d ******", pair_test->num);
+      if(xbt_automaton_state_compare(pair_test->automaton_state, st) == 0){
+        if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){

           if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
             
             if(raw_mem_set)
           if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
             
             if(raw_mem_set)


@@ -118,8 +86,8 @@ int reached(xbt_state_t st){
       }
     }
 
       }
     }
 

-    /* New pair reached */
-    xbt_dynar_push(reached_pairs, &new_pair); 
+    /* New acceptance pair */
+    xbt_dynar_push(acceptance_pairs, &new_pair); 

     
     MC_UNSET_RAW_MEM;
 
     
     MC_UNSET_RAW_MEM;
 


@@ -134,22 +102,22 @@ int reached(xbt_state_t st){
 }
 
 
 }
 
 

-void set_pair_reached(xbt_state_t st){
+static void set_acceptance_pair_reached(xbt_automaton_state_t st){

 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
  
   MC_SET_RAW_MEM;
 
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
  
   MC_SET_RAW_MEM;
 

-  mc_pair_reached_t pair = NULL;
-  pair = xbt_new0(s_mc_pair_reached_t, 1);
-  pair->nb = xbt_dynar_length(reached_pairs) + 1;
+  mc_acceptance_pair_t pair = NULL;
+  pair = xbt_new0(s_mc_acceptance_pair_t, 1);
+  pair->num = xbt_dynar_length(acceptance_pairs) + 1;

   pair->automaton_state = st;
   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
   pair->system_state = MC_take_snapshot();
 
   /* Get values of propositional symbols */
   unsigned int cursor = 0;
   pair->automaton_state = st;
   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
   pair->system_state = MC_take_snapshot();
 
   /* Get values of propositional symbols */
   unsigned int cursor = 0;

-  xbt_propositional_symbol_t ps = NULL;
+  xbt_automaton_propositional_symbol_t ps = NULL;

   int res;
   int_f_void_t f;
 
   int res;
   int_f_void_t f;
 


@@ -159,7 +127,7 @@ void set_pair_reached(xbt_state_t st){
     xbt_dynar_push_as(pair->prop_ato, int, res);
   }
 
     xbt_dynar_push_as(pair->prop_ato, int, res);
   }
 

-  xbt_dynar_push(reached_pairs, &pair); 
+  xbt_dynar_push(acceptance_pairs, &pair); 

   
   MC_UNSET_RAW_MEM;
 
   
   MC_UNSET_RAW_MEM;
 


@@ -168,7 +136,7 @@ void set_pair_reached(xbt_state_t st){
     
 }
 
     
 }
 

-int visited(xbt_state_t st){
+static int is_visited_pair(xbt_automaton_state_t st){

 
   if(_sg_mc_visited == 0)
     return 0;
 
   if(_sg_mc_visited == 0)
     return 0;


@@ -177,8 +145,8 @@ int visited(xbt_state_t st){
 
   MC_SET_RAW_MEM;
 
 
   MC_SET_RAW_MEM;
 

-  mc_pair_visited_t new_pair = NULL;
-  new_pair = xbt_new0(s_mc_pair_visited_t, 1);
+  mc_visited_pair_t new_pair = NULL;
+  new_pair = xbt_new0(s_mc_visited_pair_t, 1);

   new_pair->automaton_state = st;
   new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
   new_pair->system_state = MC_take_snapshot();  
   new_pair->automaton_state = st;
   new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
   new_pair->system_state = MC_take_snapshot();  


@@ -187,7 +155,7 @@ int visited(xbt_state_t st){
   int res;
   int_f_void_t f;
   unsigned int cursor = 0;
   int res;
   int_f_void_t f;
   unsigned int cursor = 0;

-  xbt_propositional_symbol_t ps = NULL;
+  xbt_automaton_propositional_symbol_t ps = NULL;

   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
     f = (int_f_void_t)ps->function;
     res = f();
   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
     f = (int_f_void_t)ps->function;
     res = f();


@@ -213,13 +181,13 @@ int visited(xbt_state_t st){
     MC_SET_RAW_MEM;
     
     cursor = 0;
     MC_SET_RAW_MEM;
     
     cursor = 0;

-    mc_pair_visited_t pair_test = NULL;
+    mc_visited_pair_t pair_test = NULL;

      
     xbt_dynar_foreach(visited_pairs, cursor, pair_test){
       if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug))
         XBT_DEBUG("****** Pair visited #%d ******", cursor + 1);
      
     xbt_dynar_foreach(visited_pairs, cursor, pair_test){
       if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug))
         XBT_DEBUG("****** Pair visited #%d ******", cursor + 1);

-      if(automaton_state_compare(pair_test->automaton_state, st) == 0){
-        if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
+      if(xbt_automaton_state_compare(pair_test->automaton_state, st) == 0){
+        if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){

           if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
             if(raw_mem_set)
               MC_SET_RAW_MEM;
           if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
             if(raw_mem_set)
               MC_SET_RAW_MEM;


@@ -253,15 +221,7 @@ int visited(xbt_state_t st){
   }
 }
 
   }
 }
 

-void MC_pair_delete(mc_pair_t pair){
-  xbt_free(pair->graph_state->proc_status);
-  xbt_free(pair->graph_state);
-  xbt_free(pair);
-}
-
-
-
-int MC_automaton_evaluate_label(xbt_exp_label_t l){
+static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l){

   
   switch(l->type){
   case 0 : {
   
   switch(l->type){
   case 0 : {


@@ -280,7 +240,7 @@ int MC_automaton_evaluate_label(xbt_exp_label_t l){
   }
   case 3 : { 
     unsigned int cursor = 0;
   }
   case 3 : { 
     unsigned int cursor = 0;

-    xbt_propositional_symbol_t p = NULL;
+    xbt_automaton_propositional_symbol_t p = NULL;

     int_f_void_t f;
     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
       if(strcmp(p->pred, l->u.predicat) == 0){
     int_f_void_t f;
     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
       if(strcmp(p->pred, l->u.predicat) == 0){


@@ -299,9 +259,9 @@ int MC_automaton_evaluate_label(xbt_exp_label_t l){
 }
 
 
 }
 
 

-/********************* Double-DFS stateless *******************/
+/********* Free functions *********/

 
 

-void pair_visited_free(mc_pair_visited_t pair){
+static void visited_pair_free(mc_visited_pair_t pair){

   if(pair){
     xbt_dynar_free(&(pair->prop_ato));
     MC_free_snapshot(pair->system_state);
   if(pair){
     xbt_dynar_free(&(pair->prop_ato));
     MC_free_snapshot(pair->system_state);


@@ -309,32 +269,11 @@ void pair_visited_free(mc_pair_visited_t pair){
   }
 }
 
   }
 }
 

-void pair_visited_free_voidp(void *p){
-  pair_visited_free((mc_pair_visited_t) * (void **) p);
+static void visited_pair_free_voidp(void *p){
+  visited_pair_free((mc_visited_pair_t) * (void **) p);

 }
 
 }
 

-void pair_stateless_free(mc_pair_stateless_t pair){
-  xbt_free(pair->graph_state->system_state);
-  xbt_free(pair->graph_state->proc_status);
-  xbt_free(pair->graph_state);
-  xbt_free(pair);
-}
-
-void pair_stateless_free_voidp(void *p){
-  pair_stateless_free((mc_pair_stateless_t) * (void **) p);
-}
-
-mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
-  mc_pair_stateless_t p = NULL;
-  p = xbt_new0(s_mc_pair_stateless_t, 1);
-  p->automaton_state = st;
-  p->graph_state = sg;
-  p->requests = r;
-  mc_stats_pair->expanded_pairs++;
-  return p;
-}
-
-void pair_reached_free(mc_pair_reached_t pair){
+static void acceptance_pair_free(mc_acceptance_pair_t pair){

   if(pair){
     xbt_dynar_free(&(pair->prop_ato));
     MC_free_snapshot(pair->system_state);
   if(pair){
     xbt_dynar_free(&(pair->prop_ato));
     MC_free_snapshot(pair->system_state);


@@ -342,10 +281,14 @@ void pair_reached_free(mc_pair_reached_t pair){
   }
 }
 
   }
 }
 

-void pair_reached_free_voidp(void *p){
-  pair_reached_free((mc_pair_reached_t) * (void **) p);
+static void acceptance_pair_free_voidp(void *p){
+  acceptance_pair_free((mc_acceptance_pair_t) * (void **) p);

 }
 
 }
 

+
+/********* DDFS Algorithm *********/
+
+

 void MC_ddfs_init(void){
 
   initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 void MC_ddfs_init(void){
 
   initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);


@@ -354,7 +297,7 @@ void MC_ddfs_init(void){
   XBT_DEBUG("Double-DFS init");
   XBT_DEBUG("**************************************************");
 
   XBT_DEBUG("Double-DFS init");
   XBT_DEBUG("**************************************************");
 

-  mc_pair_stateless_t mc_initial_pair = NULL;
+  mc_pair_t mc_initial_pair = NULL;

   mc_state_t initial_graph_state = NULL;
   smx_process_t process; 
 
   mc_state_t initial_graph_state = NULL;
   smx_process_t process; 
 


@@ -363,16 +306,16 @@ void MC_ddfs_init(void){
 
   MC_SET_RAW_MEM;
 
 
   MC_SET_RAW_MEM;
 

-  initial_graph_state = MC_state_pair_new();
+  initial_graph_state = MC_state_new();

   xbt_swag_foreach(process, simix_global->process_list){
     if(MC_process_is_enabled(process)){
       MC_state_interleave_process(initial_graph_state, process);
     }
   }
 
   xbt_swag_foreach(process, simix_global->process_list){
     if(MC_process_is_enabled(process)){
       MC_state_interleave_process(initial_graph_state, process);
     }
   }
 

-  reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), pair_reached_free_voidp);
-  visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), pair_visited_free_voidp);
-  successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
+  acceptance_pairs = xbt_dynar_new(sizeof(mc_acceptance_pair_t), acceptance_pair_free_voidp);
+  visited_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), visited_pair_free_voidp);
+  successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);

 
   /* Save the initial state */
   initial_state_liveness->snapshot = MC_take_snapshot();
 
   /* Save the initial state */
   initial_state_liveness->snapshot = MC_take_snapshot();


@@ -380,13 +323,13 @@ void MC_ddfs_init(void){
   MC_UNSET_RAW_MEM; 
   
   unsigned int cursor = 0;
   MC_UNSET_RAW_MEM; 
   
   unsigned int cursor = 0;

-  xbt_state_t state;
+  xbt_automaton_state_t automaton_state;

 
 

-  xbt_dynar_foreach(_mc_property_automaton->states, cursor, state){
-    if(state->type == -1){
+  xbt_dynar_foreach(_mc_property_automaton->states, cursor, automaton_state){
+    if(automaton_state->type == -1){

       
       MC_SET_RAW_MEM;
       
       MC_SET_RAW_MEM;

-      mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
+      mc_initial_pair = MC_pair_new(initial_graph_state, automaton_state, MC_state_interleave_size(initial_graph_state));

       xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
       MC_UNSET_RAW_MEM;
       
       xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
       MC_UNSET_RAW_MEM;
       


@@ -398,14 +341,14 @@ void MC_ddfs_init(void){
       MC_ddfs(0);
 
     }else{
       MC_ddfs(0);
 
     }else{

-      if(state->type == 2){
+      if(automaton_state->type == 2){

       
         MC_SET_RAW_MEM;
       
         MC_SET_RAW_MEM;

-        mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
+        mc_initial_pair = MC_pair_new(initial_graph_state, automaton_state, MC_state_interleave_size(initial_graph_state));

         xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
         MC_UNSET_RAW_MEM;
 
         xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
         MC_UNSET_RAW_MEM;
 

-        set_pair_reached(state);
+        set_acceptance_pair_reached(automaton_state);

 
         if(cursor != 0){
           MC_restore_snapshot(initial_state_liveness->snapshot);
 
         if(cursor != 0){
           MC_restore_snapshot(initial_state_liveness->snapshot);


@@ -429,17 +372,15 @@ void MC_ddfs_init(void){
 
 void MC_ddfs(int search_cycle){
 
 
 void MC_ddfs(int search_cycle){
 

-  //initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
-

   smx_process_t process;
   smx_process_t process;

-  mc_pair_stateless_t current_pair = NULL;
+  mc_pair_t current_pair = NULL;

 
   if(xbt_fifo_size(mc_stack_liveness) == 0)
     return;
 
 
   /* Get current pair */
 
   if(xbt_fifo_size(mc_stack_liveness) == 0)
     return;
 
 
   /* Get current pair */

-  current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
+  current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));

 
   /* Update current state in buchi automaton */
   _mc_property_automaton->current_state = current_pair->automaton_state;
 
   /* Update current state in buchi automaton */
   _mc_property_automaton->current_state = current_pair->automaton_state;


@@ -447,24 +388,22 @@ void MC_ddfs(int search_cycle){
  
   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
  
  
   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
  

-  mc_stats_pair->visited_pairs++;
-
-  //sleep(1);
+  mc_stats->visited_states++;

 
   int value;
   mc_state_t next_graph_state = NULL;
   smx_simcall_t req = NULL;
   char *req_str;
 
 
   int value;
   mc_state_t next_graph_state = NULL;
   smx_simcall_t req = NULL;
   char *req_str;
 

-  xbt_transition_t transition_succ;
+  xbt_automaton_transition_t transition_succ;

   unsigned int cursor = 0;
   int res;
 
   unsigned int cursor = 0;
   int res;
 

-  mc_pair_stateless_t next_pair = NULL;
-  mc_pair_stateless_t pair_succ;
+  mc_pair_t next_pair = NULL;
+  mc_pair_t pair_succ;

 
 

-  mc_pair_stateless_t remove_pair;
-  mc_pair_reached_t remove_pair_reached;
+  mc_pair_t pair_to_remove;
+  mc_acceptance_pair_t acceptance_pair_to_remove;

   
   if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
 
   
   if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
 


@@ -491,7 +430,7 @@ void MC_ddfs(int search_cycle){
         MC_SET_RAW_MEM;
 
         /* Create the new expanded graph_state */
         MC_SET_RAW_MEM;
 
         /* Create the new expanded graph_state */

-        next_graph_state = MC_state_pair_new();
+        next_graph_state = MC_state_new();

 
         /* Get enabled process and insert it in the interleave set of the next graph_state */
         xbt_swag_foreach(process, simix_global->process_list){
 
         /* Get enabled process and insert it in the interleave set of the next graph_state */
         xbt_swag_foreach(process, simix_global->process_list){


@@ -518,7 +457,7 @@ void MC_ddfs(int search_cycle){
 
           if(res == 1){ // enabled transition in automaton
             MC_SET_RAW_MEM;
 
           if(res == 1){ // enabled transition in automaton
             MC_SET_RAW_MEM;

-            next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
+            next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));

             xbt_dynar_push(successors, &next_pair);
             MC_UNSET_RAW_MEM;
           }
             xbt_dynar_push(successors, &next_pair);
             MC_UNSET_RAW_MEM;
           }


@@ -533,7 +472,7 @@ void MC_ddfs(int search_cycle){
   
           if(res == 2){ // true transition in automaton
             MC_SET_RAW_MEM;
   
           if(res == 2){ // true transition in automaton
             MC_SET_RAW_MEM;

-            next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
+            next_pair = MC_pair_new(next_graph_state, transition_succ->dst,  MC_state_interleave_size(next_graph_state));

             xbt_dynar_push(successors, &next_pair);
             MC_UNSET_RAW_MEM;
           }
             xbt_dynar_push(successors, &next_pair);
             MC_UNSET_RAW_MEM;
           }


@@ -548,7 +487,7 @@ void MC_ddfs(int search_cycle){
 
             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
           
 
             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
           

-              if(reached(pair_succ->automaton_state)){
+              if(is_reached_acceptance_pair(pair_succ->automaton_state)){

         
                 XBT_INFO("Next pair (depth = %d, %u interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state));
 
         
                 XBT_INFO("Next pair (depth = %d, %u interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state));
 


@@ -558,12 +497,12 @@ void MC_ddfs(int search_cycle){
                 XBT_INFO("Counter-example that violates formula :");
                 MC_show_stack_liveness(mc_stack_liveness);
                 MC_dump_stack_liveness(mc_stack_liveness);
                 XBT_INFO("Counter-example that violates formula :");
                 MC_show_stack_liveness(mc_stack_liveness);
                 MC_dump_stack_liveness(mc_stack_liveness);

-                MC_print_statistics_pairs(mc_stats_pair);
+                MC_print_statistics(mc_stats);

                 xbt_abort();
 
               }else{
 
                 xbt_abort();
 
               }else{
 

-                if(visited(pair_succ->automaton_state)){
+                if(is_visited_pair(pair_succ->automaton_state)){

 
                   XBT_DEBUG("Next pair already visited !");
                   break;
 
                   XBT_DEBUG("Next pair already visited !");
                   break;


@@ -572,7 +511,7 @@ void MC_ddfs(int search_cycle){
 
                   XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 
 
                   XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 

-                  XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+                  XBT_DEBUG("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));

 
                   MC_SET_RAW_MEM;
                   xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 
                   MC_SET_RAW_MEM;
                   xbt_fifo_unshift(mc_stack_liveness, pair_succ);


@@ -586,7 +525,7 @@ void MC_ddfs(int search_cycle){
 
             }else{
 
 
             }else{
 

-              if(visited(pair_succ->automaton_state)){
+              if(is_visited_pair(pair_succ->automaton_state)){

 
                 XBT_DEBUG("Next pair already visited !");
                 break;
 
                 XBT_DEBUG("Next pair already visited !");
                 break;


@@ -604,7 +543,7 @@ void MC_ddfs(int search_cycle){
 
           }else{
 
 
           }else{
 

-            if(visited(pair_succ->automaton_state)){
+            if(is_visited_pair(pair_succ->automaton_state)){

 
               XBT_DEBUG("Next pair already visited !");
               break;
 
               XBT_DEBUG("Next pair already visited !");
               break;


@@ -615,11 +554,11 @@ void MC_ddfs(int search_cycle){
 
                 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
       
 
                 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
       

-                set_pair_reached(pair_succ->automaton_state); 
+                set_acceptance_pair_reached(pair_succ->automaton_state); 

 
                 search_cycle = 1;
 
 
                 search_cycle = 1;
 

-                XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+                XBT_DEBUG("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));

 
               }
 
 
               }
 


@@ -653,7 +592,7 @@ void MC_ddfs(int search_cycle){
       MC_SET_RAW_MEM;
 
       /* Create the new expanded graph_state */
       MC_SET_RAW_MEM;
 
       /* Create the new expanded graph_state */

-      next_graph_state = MC_state_pair_new();
+      next_graph_state = MC_state_new();

 
       xbt_dynar_reset(successors);
 
 
       xbt_dynar_reset(successors);
 


@@ -667,7 +606,7 @@ void MC_ddfs(int search_cycle){
 
         if(res == 1){ // enabled transition in automaton
           MC_SET_RAW_MEM;
 
         if(res == 1){ // enabled transition in automaton
           MC_SET_RAW_MEM;

-          next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
+          next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));

           xbt_dynar_push(successors, &next_pair);
           MC_UNSET_RAW_MEM;
         }
           xbt_dynar_push(successors, &next_pair);
           MC_UNSET_RAW_MEM;
         }


@@ -682,7 +621,7 @@ void MC_ddfs(int search_cycle){
   
         if(res == 2){ // true transition in automaton
           MC_SET_RAW_MEM;
   
         if(res == 2){ // true transition in automaton
           MC_SET_RAW_MEM;

-          next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
+          next_pair = MC_pair_new(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));

           xbt_dynar_push(successors, &next_pair);
           MC_UNSET_RAW_MEM;
         }
           xbt_dynar_push(successors, &next_pair);
           MC_UNSET_RAW_MEM;
         }


@@ -697,7 +636,7 @@ void MC_ddfs(int search_cycle){
 
           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
 
 
           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ 
 

-            if(reached(pair_succ->automaton_state)){
+            if(is_reached_acceptance_pair(pair_succ->automaton_state)){

            
               XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
         
            
               XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
         


@@ -707,12 +646,12 @@ void MC_ddfs(int search_cycle){
               XBT_INFO("Counter-example that violates formula :");
               MC_show_stack_liveness(mc_stack_liveness);
               MC_dump_stack_liveness(mc_stack_liveness);
               XBT_INFO("Counter-example that violates formula :");
               MC_show_stack_liveness(mc_stack_liveness);
               MC_dump_stack_liveness(mc_stack_liveness);

-              MC_print_statistics_pairs(mc_stats_pair);
+              MC_print_statistics(mc_stats);

               xbt_abort();
 
             }else{
 
               xbt_abort();
 
             }else{
 

-              if(visited(pair_succ->automaton_state)){
+              if(is_visited_pair(pair_succ->automaton_state)){

                 
                 XBT_DEBUG("Next pair already visited !");
                 break;
                 
                 XBT_DEBUG("Next pair already visited !");
                 break;


@@ -721,7 +660,7 @@ void MC_ddfs(int search_cycle){
 
                 XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
         
 
                 XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
         

-                XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+                XBT_INFO("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));

 
                 MC_SET_RAW_MEM;
                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 
                 MC_SET_RAW_MEM;
                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);


@@ -735,7 +674,7 @@ void MC_ddfs(int search_cycle){
 
           }else{
             
 
           }else{
             

-            if(visited(pair_succ->automaton_state)){
+            if(is_visited_pair(pair_succ->automaton_state)){

               
               XBT_DEBUG("Next pair already visited !");
               break;
               
               XBT_DEBUG("Next pair already visited !");
               break;


@@ -755,7 +694,7 @@ void MC_ddfs(int search_cycle){
 
         }else{
       
 
         }else{
       

-          if(visited(pair_succ->automaton_state)){
+          if(is_visited_pair(pair_succ->automaton_state)){

 
             XBT_DEBUG("Next pair already visited !");
             break;
 
             XBT_DEBUG("Next pair already visited !");
             break;


@@ -764,11 +703,11 @@ void MC_ddfs(int search_cycle){
 
             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 
 
             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 

-              set_pair_reached(pair_succ->automaton_state);
+              set_acceptance_pair_reached(pair_succ->automaton_state);

          
               search_cycle = 1;
 
          
               search_cycle = 1;
 

-              XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+              XBT_INFO("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));

 
             }
 
 
             }
 


@@ -793,7 +732,7 @@ void MC_ddfs(int search_cycle){
   }else{
     
     XBT_WARN("/!\\ Max depth reached ! /!\\ ");
   }else{
     
     XBT_WARN("/!\\ Max depth reached ! /!\\ ");

-    if(current_pair->requests > 0){
+    if(MC_state_interleave_size(current_pair->graph_state) > 0){

       XBT_WARN("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ "); 
       XBT_WARN("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
     }
       XBT_WARN("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ "); 
       XBT_WARN("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
     }


@@ -808,17 +747,14 @@ void MC_ddfs(int search_cycle){
 
   
   MC_SET_RAW_MEM;
 
   
   MC_SET_RAW_MEM;

-  remove_pair = xbt_fifo_shift(mc_stack_liveness);
-  xbt_fifo_remove(mc_stack_liveness, remove_pair);
-  remove_pair = NULL;
+  pair_to_remove = xbt_fifo_shift(mc_stack_liveness);
+  xbt_fifo_remove(mc_stack_liveness, pair_to_remove);
+  pair_to_remove = NULL;

   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){

-    remove_pair_reached = xbt_dynar_pop_as(reached_pairs, mc_pair_reached_t);
-    pair_reached_free(remove_pair_reached);
-    remove_pair_reached = NULL;
+    acceptance_pair_to_remove = xbt_dynar_pop_as(acceptance_pairs, mc_acceptance_pair_t);
+    acceptance_pair_free(acceptance_pair_to_remove);
+    acceptance_pair_to_remove = NULL;

   }
   MC_UNSET_RAW_MEM;
 
   }
   MC_UNSET_RAW_MEM;
 

-  /*if(initial_state_liveness->raw_mem_set)
-    MC_SET_RAW_MEM;*/
-

 }
 }