model-checker : fix memory leak in ddfs algorithm

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index 832005f..2b2fe9d 100644 (file)
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -725,7 +725,7 @@ static void MC_dump_checkpoint_ignore(mc_snapshot_t snapshot){
 }
 
 
-mc_snapshot_t MC_take_snapshot(){
+mc_snapshot_t MC_take_snapshot(int num_state){
 
   mc_snapshot_t snapshot = xbt_new0(s_mc_snapshot_t, 1);
   snapshot->nb_processes = xbt_swag_size(simix_global->process_list);
@@ -741,7 +741,8 @@ mc_snapshot_t MC_take_snapshot(){
     //MC_get_hash_local(snapshot->hash_local, snapshot->stacks);
   }
 
-  MC_dump_checkpoint_ignore(snapshot);
+  if(num_state > 0)
+    MC_dump_checkpoint_ignore(snapshot);
 
   return snapshot;
 
@@ -756,7 +757,7 @@ void MC_restore_snapshot(mc_snapshot_t snapshot){
 }
 
 mc_snapshot_t SIMIX_pre_mc_snapshot(smx_simcall_t simcall){
-  return MC_take_snapshot();
+  return MC_take_snapshot(1);
 }
 
 void *MC_snapshot(void){

diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c
index 7f2ea63..e7ece50 100644 (file)
--- a/src/mc/mc_compare.c
+++ b/src/mc/mc_compare.c
@@ -337,10 +337,10 @@ int snapshot_compare(void *state1, void *state2){
   int num1, num2;
   
   if(_sg_mc_property_file && _sg_mc_property_file[0] != '\0'){ /* Liveness MC */
-    s1 = ((mc_pair_t)state1)->graph_state->system_state;
-    s2 = ((mc_pair_t)state2)->graph_state->system_state;
-    num1 = ((mc_pair_t)state1)->num;
-    num2 =  ((mc_pair_t)state2)->num;
+    s1 = ((mc_visited_pair_t)state1)->graph_state->system_state;
+    s2 = ((mc_visited_pair_t)state2)->graph_state->system_state;
+    num1 = ((mc_visited_pair_t)state1)->num;
+    num2 =  ((mc_visited_pair_t)state2)->num;
     /* Firstly compare automaton state */
     /*if(xbt_automaton_state_compare(((mc_pair_t)state1)->automaton_state, ((mc_pair_t)state2)->automaton_state) != 0)
       return 1;

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index 643acf8..ebda309 100644 (file)
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -33,7 +33,7 @@ static mc_visited_state_t visited_state_new(){
   new_state = xbt_new0(s_mc_visited_state_t, 1);
   new_state->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
   new_state->nb_processes = xbt_swag_size(simix_global->process_list);
-  new_state->system_state = MC_take_snapshot();
+  new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
   new_state->num = mc_stats->expanded_states;
   new_state->other_num = -1;
 
@@ -276,6 +276,7 @@ void MC_dpor(void)
   mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
   smx_process_t process = NULL;
   xbt_fifo_item_t item = NULL;
+  mc_state_t state_test = NULL;
   int pos;
   int visited_state = -1;
   int enabled = 0;
@@ -287,9 +288,9 @@ void MC_dpor(void)
       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
 
     XBT_DEBUG("**************************************************");
-    XBT_DEBUG("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d)",
+    XBT_DEBUG("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d, first_enabled_state size : %d)",
               xbt_fifo_size(mc_stack_safety), state, state->num,
-              MC_state_interleave_size(state), user_max_depth_reached);
+              MC_state_interleave_size(state), user_max_depth_reached, xbt_dict_size(first_enabled_state));
       
     /* Update statistics */
     mc_stats->visited_states++;
@@ -343,7 +344,7 @@ void MC_dpor(void)
         }
 
         if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
-          next_state->system_state = MC_take_snapshot();
+          next_state->system_state = MC_take_snapshot(next_state->num);
         }
 
         if(dot_output != NULL)
@@ -395,8 +396,6 @@ void MC_dpor(void)
             char *key = bprintf("%lu", process->pid);
             enabled = (int)strtoul(xbt_dict_get_or_null(first_enabled_state, key), 0, 10);
             xbt_free(key);
-            mc_state_t state_test = NULL;
-            xbt_fifo_item_t item = NULL;
             int cursor = xbt_fifo_size(mc_stack_safety);
             xbt_fifo_foreach(mc_stack_safety, item, state_test, mc_state_t){
               if(cursor-- == enabled){ 
@@ -406,7 +405,7 @@ void MC_dpor(void)
                   break;
                 }
               }
-            } 
+            }
           }
         }
 
@@ -504,7 +503,7 @@ void MC_dpor(void)
             MC_UNSET_RAW_MEM;
             MC_replay(mc_stack_safety, -1);
           }
-          XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety));
+          XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack_safety));
           break;
         } else {
           XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1); 

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 2fba00d..4ae023d 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -1875,7 +1875,7 @@ void MC_modelcheck_safety(void)
   MC_SET_RAW_MEM;
   /* Save the initial state */
   initial_state_safety = xbt_new0(s_mc_global_t, 1);
-  initial_state_safety->snapshot = MC_take_snapshot();
+  initial_state_safety->snapshot = MC_take_snapshot(0);
   MC_UNSET_RAW_MEM;
 
   MC_dpor();

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 2007c64..d0303b5 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -36,20 +36,20 @@ static xbt_dynar_t get_atomic_propositions_values(){
   return values;
 }
 
-static int get_search_interval(xbt_dynar_t all_pairs, mc_pair_t pair, int *min, int *max){
+static int get_search_interval(xbt_dynar_t all_pairs, mc_visited_pair_t pair, int *min, int *max){
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
   MC_SET_RAW_MEM;
 
   int cursor = 0, previous_cursor, next_cursor;
-  mc_pair_t pair_test;
+  mc_visited_pair_t pair_test;
   int start = 0;
   int end = xbt_dynar_length(all_pairs) - 1;
   
   while(start <= end){
     cursor = (start + end) / 2;
-    pair_test = (mc_pair_t)xbt_dynar_get_as(all_pairs, cursor, mc_pair_t);
+    pair_test = (mc_visited_pair_t)xbt_dynar_get_as(all_pairs, cursor, mc_visited_pair_t);
     if(pair_test->nb_processes < pair->nb_processes){
       start = cursor + 1;
     }else if(pair_test->nb_processes > pair->nb_processes){
@@ -63,7 +63,7 @@ static int get_search_interval(xbt_dynar_t all_pairs, mc_pair_t pair, int *min,
         *min = *max = cursor;
         previous_cursor = cursor - 1;
         while(previous_cursor >= 0){
-          pair_test = (mc_pair_t)xbt_dynar_get_as(all_pairs, previous_cursor, mc_pair_t);
+          pair_test = (mc_visited_pair_t)xbt_dynar_get_as(all_pairs, previous_cursor, mc_visited_pair_t);
           if(pair_test->nb_processes != pair->nb_processes || pair_test->heap_bytes_used != pair->heap_bytes_used)
             break;
           *min = previous_cursor;
@@ -71,7 +71,7 @@ static int get_search_interval(xbt_dynar_t all_pairs, mc_pair_t pair, int *min,
         }
         next_cursor = cursor + 1;
         while(next_cursor < xbt_dynar_length(all_pairs)){
-          pair_test = (mc_pair_t)xbt_dynar_get_as(all_pairs, next_cursor, mc_pair_t);
+          pair_test = (mc_visited_pair_t)xbt_dynar_get_as(all_pairs, next_cursor, mc_visited_pair_t);
           if(pair_test->nb_processes != pair->nb_processes || pair_test->heap_bytes_used != pair->heap_bytes_used)
             break;
           *max = next_cursor;
@@ -90,35 +90,25 @@ static int get_search_interval(xbt_dynar_t all_pairs, mc_pair_t pair, int *min,
   return cursor;
 }
 
-static int is_reached_acceptance_pair(mc_pair_t pair){
+static mc_visited_pair_t is_reached_acceptance_pair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions){
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
   MC_SET_RAW_MEM;
- 
+  
+  mc_visited_pair_t pair = NULL;
+  pair = MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
+  pair->acceptance_pair = 1;
+  
   if(xbt_dynar_is_empty(acceptance_pairs)){
 
-    if(pair->graph_state->system_state == NULL){
-      pair->graph_state->system_state = MC_take_snapshot();
-      pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
-    }
     xbt_dynar_push(acceptance_pairs, &pair); 
 
-    if(!raw_mem_set)
-      MC_UNSET_RAW_MEM;
-
-    return -1;
-
   }else{
 
-    if(pair->graph_state->system_state == NULL){
-      pair->graph_state->system_state = MC_take_snapshot();
-      pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
-    }
-
     int min = -1, max = -1, index;
     //int res;
-    mc_pair_t pair_test;
+    mc_visited_pair_t pair_test;
     int cursor;
 
     index = get_search_interval(acceptance_pairs, pair, &min, &max);
@@ -132,13 +122,20 @@ static int is_reached_acceptance_pair(mc_pair_t pair){
         }*/
       cursor = min;
       while(cursor <= max){
-        pair_test = (mc_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_pair_t);
+        pair_test = (mc_visited_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_visited_pair_t);
         if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
           if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
             if(snapshot_compare(pair_test, pair) == 0){
+              XBT_INFO("Pair %d already reached (equal to pair %d) !", pair->num, pair_test->num);
+              
+              xbt_fifo_shift(mc_stack_liveness);
+              if(dot_output != NULL)
+                fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, pair_test->num, initial_state_liveness->prev_req);
+
               if(!raw_mem_set)
                 MC_UNSET_RAW_MEM;
-              return pair_test->num;
+
+              return NULL;
             }
           }
         }
@@ -146,7 +143,7 @@ static int is_reached_acceptance_pair(mc_pair_t pair){
       }
       xbt_dynar_insert_at(acceptance_pairs, min, &pair);
     }else{
-      pair_test = (mc_pair_t)xbt_dynar_get_as(acceptance_pairs, index, mc_pair_t);
+      pair_test = (mc_visited_pair_t)xbt_dynar_get_as(acceptance_pairs, index, mc_visited_pair_t);
       if(pair_test->nb_processes < pair->nb_processes){
         xbt_dynar_insert_at(acceptance_pairs, index+1, &pair);
       }else{
@@ -156,119 +153,48 @@ static int is_reached_acceptance_pair(mc_pair_t pair){
           xbt_dynar_insert_at(acceptance_pairs, index, &pair);
       }
     }
-
-    if(!raw_mem_set)
-      MC_UNSET_RAW_MEM;
-    
-    return -1;
-    
-  }
- 
-}
-
-
-static void set_acceptance_pair_reached(mc_pair_t pair){
-
-  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
-
-  MC_SET_RAW_MEM;
-
-  if(xbt_dynar_is_empty(acceptance_pairs)){
-
-     if(pair->graph_state->system_state == NULL){
-       pair->graph_state->system_state = MC_take_snapshot();
-       pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
-     }
-     xbt_dynar_push(acceptance_pairs, &pair); 
-
-  }else{
-
-    if(pair->graph_state->system_state == NULL){
-      pair->graph_state->system_state = MC_take_snapshot();
-      pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
-    }
     
-    size_t current_bytes_used = pair->heap_bytes_used;
-    int current_nb_processes = pair->nb_processes;
-
-    int cursor = 0;
-    int start = 0;
-    int end = xbt_dynar_length(acceptance_pairs) - 1;
-
-    mc_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_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_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(pair_test->nb_processes < pair->nb_processes){
-      xbt_dynar_insert_at(acceptance_pairs, cursor+1, &pair);
-    }else{
-      if(pair_test->heap_bytes_used < pair->heap_bytes_used)
-        xbt_dynar_insert_at(acceptance_pairs, cursor + 1, &pair);
-      else
-        xbt_dynar_insert_at(acceptance_pairs, cursor, &pair);
-    }    
-
   }
 
   if(!raw_mem_set)
     MC_UNSET_RAW_MEM;
-    
+
+  return pair;
+ 
 }
 
-static void remove_acceptance_pair(mc_pair_t pair){
+static void remove_acceptance_pair(int pair_num){
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
+  fprintf(stderr, "Search acceptance pair %d\n", pair_num);
+
   MC_SET_RAW_MEM;
 
   unsigned int cursor = 0;
-  mc_pair_t pair_test;
-  int pair_found = 0;
+  mc_visited_pair_t pair_test = NULL;
 
   xbt_dynar_foreach(acceptance_pairs, cursor, pair_test){
-    if(pair_test->num == pair->num){
-      pair_found = 1;
+    if(pair_test->num == pair_num){
       break;
     }
   }
 
-  if(pair_found)
-    xbt_dynar_remove_at(acceptance_pairs, cursor, NULL);
+  xbt_dynar_remove_at(acceptance_pairs, cursor, &pair_test);
   
-  pair->acceptance_removed = 1;
+  pair_test->acceptance_removed = 1;
 
-  if(pair->stack_removed && pair->acceptance_removed){
-    if(_sg_mc_visited == 0){
-      MC_pair_delete(pair);
-    }else if(pair->visited_removed){
-      MC_pair_delete(pair);
-    }
+  if(_sg_mc_visited == 0){
+    MC_visited_pair_delete(pair_test);
+  }else if(pair_test->visited_removed == 1){
+    MC_visited_pair_delete(pair_test);
   }
 
   if(!raw_mem_set)
     MC_UNSET_RAW_MEM;
 }
 
-static int is_visited_pair(mc_pair_t pair){
+static int is_visited_pair(mc_visited_pair_t pair, int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions){
 
   if(_sg_mc_visited == 0)
     return -1;
@@ -277,28 +203,26 @@ static int is_visited_pair(mc_pair_t pair){
 
   MC_SET_RAW_MEM;
 
-  if(xbt_dynar_is_empty(visited_pairs)){
+  mc_visited_pair_t new_pair = NULL;
 
-    if(pair->graph_state->system_state == NULL)
-      pair->graph_state->system_state = MC_take_snapshot();
-    xbt_dynar_push(visited_pairs, &pair); 
+  if(pair == NULL){
+    new_pair = MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
+  }else{
+    new_pair = pair;
+  }
 
-    if(!raw_mem_set)
-      MC_UNSET_RAW_MEM;
+  if(xbt_dynar_is_empty(visited_pairs)){
 
-    return -1;
+    xbt_dynar_push(visited_pairs, &new_pair); 
 
   }else{
 
-    if(pair->graph_state->system_state == NULL)
-      pair->graph_state->system_state = MC_take_snapshot();
-
     int min = -1, max = -1, index;
     //int res;
-    mc_pair_t pair_test;
+    mc_visited_pair_t pair_test;
     int cursor;
 
-    index = get_search_interval(visited_pairs, pair, &min, &max);
+    index = get_search_interval(visited_pairs, new_pair, &min, &max);
 
     if(min != -1 && max != -1){ // Visited pair with same number of processes and same heap bytes used exists
       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
@@ -330,48 +254,47 @@ static int is_visited_pair(mc_pair_t pair){
         }*/
       cursor = min;
       while(cursor <= max){
-        pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, cursor, mc_pair_t);
-        if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
-          if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){
-            if(snapshot_compare(pair_test, pair) == 0){
-              if(pair_test->other_num == -1)
-                pair->other_num = pair_test->num;
-              else
-                pair->other_num = pair_test->other_num;
-              if(dot_output == NULL)
-                XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
-              else
-                XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
-              xbt_dynar_remove_at(visited_pairs, cursor, NULL);
-              xbt_dynar_insert_at(visited_pairs, cursor, &pair);
-              pair_test->visited_removed = 1;
-              if(pair_test->stack_removed && pair_test->visited_removed){
-                if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
-                  if(pair_test->acceptance_removed){
-                    MC_pair_delete(pair_test);
-                  }
+        pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
+        //if(pair_test->acceptance_pair == 0){ /* Acceptance pair have been already checked before */
+          if(xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) == 0){
+            if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_pair->atomic_propositions) == 0){
+              if(snapshot_compare(pair_test, new_pair) == 0){
+                if(pair_test->other_num == -1)
+                  new_pair->other_num = pair_test->num;
+                else
+                  new_pair->other_num = pair_test->other_num;
+                if(dot_output == NULL)
+                  XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_pair->num, pair_test->num);
+                else
+                  XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_pair->num, pair_test->num, pair->other_num);
+                xbt_dynar_remove_at(visited_pairs, cursor, NULL);
+                xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
+                pair_test->visited_removed = 1;
+                if(pair_test->acceptance_pair){
+                  if(pair_test->acceptance_removed == 1)
+                    MC_visited_pair_delete(pair_test);
                 }else{
-                  MC_pair_delete(pair_test);
+                  MC_visited_pair_delete(pair_test);
                 }
+                if(!raw_mem_set)
+                  MC_UNSET_RAW_MEM;
+                return new_pair->other_num;
               }
-              if(!raw_mem_set)
-                MC_UNSET_RAW_MEM;
-              return pair->other_num;
             }
-          }
+            //}
         }
         cursor++;
       }
-      xbt_dynar_insert_at(visited_pairs, min, &pair);
+      xbt_dynar_insert_at(visited_pairs, min, &new_pair);
     }else{
-      pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, index, mc_pair_t);
-      if(pair_test->nb_processes < pair->nb_processes){
-        xbt_dynar_insert_at(visited_pairs, index+1, &pair);
+      pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, index, mc_visited_pair_t);
+      if(pair_test->nb_processes < new_pair->nb_processes){
+        xbt_dynar_insert_at(visited_pairs, index+1, &new_pair);
       }else{
-        if(pair_test->heap_bytes_used < pair->heap_bytes_used)
-          xbt_dynar_insert_at(visited_pairs, index + 1, &pair);
+        if(pair_test->heap_bytes_used < new_pair->heap_bytes_used)
+          xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
         else
-          xbt_dynar_insert_at(visited_pairs, index, &pair);
+          xbt_dynar_insert_at(visited_pairs, index, &new_pair);
       }
     }
 
@@ -387,17 +310,20 @@ static int is_visited_pair(mc_pair_t pair){
       }
       xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
       pair_test->visited_removed = 1;
-      if(pair_test->stack_removed && pair_test->acceptance_removed && pair_test->visited_removed)
-        MC_pair_delete(pair_test);
-      
+      if(pair_test->acceptance_pair){
+        if(pair_test->acceptance_removed)
+          MC_visited_pair_delete(pair_test);
+      }else{
+        MC_visited_pair_delete(pair_test);
+      }
     }
 
-    if(!raw_mem_set)
-      MC_UNSET_RAW_MEM;
-    
-    return -1;
-
   }
+
+  if(!raw_mem_set)
+    MC_UNSET_RAW_MEM;
+  
+  return -1;
 }
 
 static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l, xbt_dynar_t atomic_propositions_values){
@@ -456,11 +382,11 @@ void MC_ddfs_init(void){
 
   MC_SET_RAW_MEM;
 
-  acceptance_pairs = xbt_dynar_new(sizeof(mc_pair_t), NULL); 
-  visited_pairs = xbt_dynar_new(sizeof(mc_pair_t), NULL); 
+  acceptance_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL); 
+  visited_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL); 
   successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
 
-  initial_state_liveness->snapshot = MC_take_snapshot();
+  initial_state_liveness->snapshot = MC_take_snapshot(0);
   initial_state_liveness->prev_pair = 0;
 
   MC_UNSET_RAW_MEM; 
@@ -497,40 +423,7 @@ void MC_ddfs_init(void){
       if(cursor != 0){
         MC_restore_snapshot(initial_state_liveness->snapshot);
         MC_UNSET_RAW_MEM;
-      }
-      
-
-    }else if(automaton_state->type == 2){ /* Acceptance automaton state */
-      
-      MC_SET_RAW_MEM;
-
-      initial_pair = MC_pair_new();
-      initial_pair->automaton_state = automaton_state;
-      initial_pair->graph_state = MC_state_new();
-      initial_pair->atomic_propositions = get_atomic_propositions_values();
-        
-      /* Get enabled process and insert it in the interleave set of the graph_state */
-      xbt_swag_foreach(process, simix_global->process_list){
-        if(MC_process_is_enabled(process)){
-          MC_state_interleave_process(initial_pair->graph_state, process);
-        }
-      }
-
-      initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state);
-      initial_pair->search_cycle = 1;
-        
-      xbt_fifo_unshift(mc_stack_liveness, initial_pair);
-        
-      MC_UNSET_RAW_MEM;
-
-      set_acceptance_pair_reached(initial_pair);
-  
-      MC_ddfs();
-
-      if(cursor != 0){
-        MC_restore_snapshot(initial_state_liveness->snapshot);
-        MC_UNSET_RAW_MEM;
-      }
+      } 
     }
   }
 
@@ -557,7 +450,7 @@ void MC_ddfs(){
   /* Update current state in buchi automaton */
   _mc_property_automaton->current_state = current_pair->automaton_state;
 
-  XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d, interleave size %d)", xbt_fifo_size(mc_stack_liveness), current_pair->search_cycle, MC_state_interleave_size(current_pair->graph_state));
+  XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d, interleave size %d, pair_num %d)", xbt_fifo_size(mc_stack_liveness), current_pair->search_cycle, MC_state_interleave_size(current_pair->graph_state), current_pair->num);
  
   mc_stats->visited_pairs++;
 
@@ -568,10 +461,12 @@ void MC_ddfs(){
   xbt_automaton_transition_t transition_succ;
   unsigned int cursor = 0;
   int res;
-  int reached_num, visited_num;
+  int visited_num;
 
   mc_pair_t next_pair = NULL;
   xbt_dynar_t prop_values = NULL;
+  int new_pair = 0;
+  mc_visited_pair_t reached_pair = NULL;
   
   if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
 
@@ -580,16 +475,7 @@ void MC_ddfs(){
       if(current_pair->search_cycle){
 
         if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){ 
-          
-          if((reached_num = is_reached_acceptance_pair(current_pair)) != -1){
-        
-            XBT_INFO("Pair %d already reached (equal to pair %d) !", current_pair->num, reached_num);
-            
-            MC_SET_RAW_MEM;
-            xbt_fifo_shift(mc_stack_liveness);
-            if(dot_output != NULL)
-              fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, reached_num, initial_state_liveness->prev_req);
-            MC_UNSET_RAW_MEM;
+          if((reached_pair = is_reached_acceptance_pair(current_pair->num, current_pair->automaton_state, current_pair->atomic_propositions)) == NULL){
 
             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
             XBT_INFO("|             ACCEPTANCE CYCLE            |");
@@ -604,14 +490,13 @@ void MC_ddfs(){
         }
       }
 
-      if((visited_num = is_visited_pair(current_pair)) != -1){
+      if((visited_num = is_visited_pair(reached_pair, current_pair->num, current_pair->automaton_state, current_pair->atomic_propositions)) != -1){
 
         MC_SET_RAW_MEM;
         if(dot_output != NULL)
           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, visited_num, initial_state_liveness->prev_req);
         MC_UNSET_RAW_MEM;
-        
-      
+              
       }else{  
 
         while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
@@ -662,6 +547,9 @@ void MC_ddfs(){
 
             if(res == 1){ // enabled transition in automaton
 
+              if(new_pair)
+                MC_replay_liveness(mc_stack_liveness, 1); 
+
               MC_SET_RAW_MEM;
 
               next_pair = MC_pair_new();
@@ -688,6 +576,8 @@ void MC_ddfs(){
 
               MC_UNSET_RAW_MEM;
 
+              new_pair = 1;
+
               MC_ddfs();
 
             }
@@ -701,6 +591,9 @@ void MC_ddfs(){
             res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
   
             if(res == 2){ // true transition in automaton
+
+              if(new_pair)
+                MC_replay_liveness(mc_stack_liveness, 1); 
             
               MC_SET_RAW_MEM;
             
@@ -728,6 +621,8 @@ void MC_ddfs(){
             
               MC_UNSET_RAW_MEM;
 
+              new_pair = 1;
+
               MC_ddfs();
 
             }
@@ -743,117 +638,6 @@ void MC_ddfs(){
 
       }
  
-    }else{
-
-      mc_stats->executed_transitions++;
-      
-      XBT_DEBUG("No request to execute in this state, search evolution in Büchi Automaton.");
-
-      if(current_pair->search_cycle){
-
-        if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){ 
-          
-          if((reached_num = is_reached_acceptance_pair(current_pair)) != -1){
-        
-            XBT_INFO("Pair %d already reached (equal to pair %d) !", current_pair->num, reached_num);
-            
-            MC_SET_RAW_MEM;
-            xbt_fifo_shift(mc_stack_liveness);
-            MC_UNSET_RAW_MEM;
-
-            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();
-
-          }
-        }
-      }
-
-      if((visited_num = is_visited_pair(current_pair)) != -1){
-
-        XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", current_pair->num, visited_num);
-      
-      }else{            
-        
-        MC_SET_RAW_MEM;
-        prop_values = get_atomic_propositions_values();
-        MC_UNSET_RAW_MEM;
-
-        /* Evaluate enabled transition according to atomic propositions values */
-        cursor= 0;
-        xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
-
-          res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
-
-          if(res == 1){ // enabled transition in automaton
-
-            MC_SET_RAW_MEM;
-
-            next_pair = MC_pair_new();
-            next_pair->graph_state = MC_state_new();
-            next_pair->automaton_state = transition_succ->dst;
-            next_pair->atomic_propositions = get_atomic_propositions_values();
-            next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
-              
-            if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
-              next_pair->search_cycle = 1;
-            
-            xbt_fifo_unshift(mc_stack_liveness, next_pair);
-
-            if(mc_stats->expanded_pairs%1000 == 0)
-              XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
-
-            if(dot_output != NULL)
-              fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", current_pair->num, next_pair->num, "");
-
-            MC_UNSET_RAW_MEM;
-
-            MC_ddfs();
-
-          }
-
-        }
-
-        /* Then, evaluate true transitions (always true, whatever atomic propositions values) */
-        cursor = 0;   
-        xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
-      
-          res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
-  
-          if(res == 2){ // true transition in automaton
-
-            MC_SET_RAW_MEM;
-            
-            next_pair = MC_pair_new();
-            next_pair->graph_state = MC_state_new();
-            next_pair->automaton_state = transition_succ->dst;
-            next_pair->atomic_propositions = get_atomic_propositions_values();
-            next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
-            
-            if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
-              next_pair->search_cycle = 1;
-
-            xbt_fifo_unshift(mc_stack_liveness, next_pair);
-
-            if(mc_stats->expanded_pairs%1000 == 0)
-              XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
-            
-            if(dot_output != NULL)
-              fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", current_pair->num, next_pair->num, "");
-
-            MC_UNSET_RAW_MEM;
-
-            MC_ddfs();
-
-          }
-
-        }
-      }
     }
     
   }else{
@@ -877,15 +661,10 @@ void MC_ddfs(){
   MC_SET_RAW_MEM;
   xbt_dynar_free(&prop_values);
   current_pair = xbt_fifo_shift(mc_stack_liveness);
-  current_pair->stack_removed = 1;
-  if(current_pair->search_cycle){
-    remove_acceptance_pair(current_pair);
-  }else{
-    if(_sg_mc_visited == 0)
-      MC_pair_delete(current_pair);
-    else if(current_pair->visited_removed)
-      MC_pair_delete(current_pair);
+  if(xbt_fifo_size(mc_stack_liveness) != _sg_mc_max_depth -1 && current_pair->requests > 0 && current_pair->search_cycle){
+    remove_acceptance_pair(current_pair->num);
   }
+  MC_pair_delete(current_pair);
 
   MC_UNSET_RAW_MEM;
 

diff --git a/src/mc/mc_pair.c b/src/mc/mc_pair.c
index ca6678b..1056f44 100644 (file)
--- a/src/mc/mc_pair.c
+++ b/src/mc/mc_pair.c
@@ -9,19 +9,43 @@
 mc_pair_t MC_pair_new(){
   mc_pair_t p = NULL;
   p = xbt_new0(s_mc_pair_t, 1);
-  p->nb_processes = xbt_swag_size(simix_global->process_list);
   p->num = ++mc_stats->expanded_pairs;
   p->search_cycle = 0;
-  p->other_num = -1;
   return p;
 }
 
+mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions){
+  mc_visited_pair_t pair = NULL;
+  pair = xbt_new0(s_mc_visited_pair_t, 1);
+  pair->graph_state = MC_state_new();
+  pair->graph_state->system_state = MC_take_snapshot(pair_num);
+  pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
+  pair->nb_processes = xbt_swag_size(simix_global->process_list);
+  pair->automaton_state = automaton_state;
+  pair->num = pair_num;
+  pair->other_num = -1;
+  pair->acceptance_removed = 0;
+  pair->visited_removed = 0;
+  pair->acceptance_pair = 0;
+  pair->atomic_propositions = xbt_dynar_new(sizeof(int), NULL);
+  unsigned int cursor = 0;
+  int value;
+  xbt_dynar_foreach(atomic_propositions, cursor, value)
+    xbt_dynar_push_as(pair->atomic_propositions, int, value);
+  return pair;
+}
+
+void MC_visited_pair_delete(mc_visited_pair_t p){
+  p->automaton_state = NULL;
+  MC_state_delete(p->graph_state);
+  xbt_dynar_free(&(p->atomic_propositions));
+  xbt_free(p);
+  p = NULL;
+}
+
 void MC_pair_delete(mc_pair_t p){
   p->automaton_state = NULL;
   MC_state_delete(p->graph_state);
-  p->stack_removed = 0;
-  p->visited_removed = 0;
-  p->acceptance_removed = 0;
   xbt_dynar_free(&(p->atomic_propositions));
   xbt_free(p);
   p = NULL;

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index f112c7e..9e1db34 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -66,7 +66,7 @@ typedef struct s_mc_checkpoint_ignore_region{
 }s_mc_checkpoint_ignore_region_t, *mc_checkpoint_ignore_region_t;
 
 mc_snapshot_t SIMIX_pre_mc_snapshot(smx_simcall_t simcall);
-mc_snapshot_t MC_take_snapshot(void);
+mc_snapshot_t MC_take_snapshot(int num_state);
 void MC_restore_snapshot(mc_snapshot_t);
 void MC_free_snapshot(mc_snapshot_t);
 
@@ -299,22 +299,31 @@ extern xbt_dynar_t mc_data_bss_comparison_ignore;
 
 typedef struct s_mc_pair{
   int num;
-  int other_num; /* Dot output for */
   int search_cycle;
   mc_state_t graph_state; /* System state included */
   xbt_automaton_state_t automaton_state;
   xbt_dynar_t atomic_propositions;
   int requests;
+}s_mc_pair_t, *mc_pair_t;
+
+typedef struct s_mc_visited_pair{
+  int num;
+  int other_num; /* Dot output for */
+  int acceptance_pair;
+  mc_state_t graph_state; /* System state included */
+  xbt_automaton_state_t automaton_state;
+  xbt_dynar_t atomic_propositions;
   size_t heap_bytes_used;
   int nb_processes;
-  int stack_removed;
-  int visited_removed;
   int acceptance_removed;
-}s_mc_pair_t, *mc_pair_t;
+  int visited_removed;
+}s_mc_visited_pair_t, *mc_visited_pair_t;
 
 mc_pair_t MC_pair_new(void);
 void MC_pair_delete(mc_pair_t);
 void mc_pair_free_voidp(void *p);
+mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions);
+void MC_visited_pair_delete(mc_visited_pair_t p);
 
 void MC_ddfs_init(void);
 void MC_ddfs(void);