model-checker : order reached_pairs by number of processes and heap bytes used

diff --git a/examples/msg/mc/bugged1_liveness.tesh b/examples/msg/mc/bugged1_liveness.tesh
index b083c7c..b0f05b3 100644 (file)
--- a/examples/msg/mc/bugged1_liveness.tesh
+++ b/examples/msg/mc/bugged1_liveness.tesh
@@ -39,7 +39,6 @@ $ ${bindir:=.}/bugged1_liveness --cfg=model-check:1 --cfg=contexts/factory:ucont
 > [0.000000] [mc_global/INFO] [(3)client] iSend (src=client, buff=(verbose only), size=(verbose only))
 > [0.000000] [mc_global/INFO] [(1)coordinator] Wait (comm=(verbose only) [(3)client -> (1)coordinator])
 > [0.000000] [mc_global/INFO] [(1)coordinator] iSend (src=coordinator, buff=(verbose only), size=(verbose only))
 > [0.000000] [mc_global/INFO] [(3)client] iSend (src=client, buff=(verbose only), size=(verbose only))
 > [0.000000] [mc_global/INFO] [(1)coordinator] Wait (comm=(verbose only) [(3)client -> (1)coordinator])
 > [0.000000] [mc_global/INFO] [(1)coordinator] iSend (src=coordinator, buff=(verbose only), size=(verbose only))

-> [0.000000] [mc_global/INFO] Expanded states = 22
-> [0.000000] [mc_global/INFO] Visited states = 21
+> [0.000000] [mc_global/INFO] Expanded pairs = 23
+> [0.000000] [mc_global/INFO] Visited pairs = 21

 > [0.000000] [mc_global/INFO] Executed transitions = 21
 > [0.000000] [mc_global/INFO] Executed transitions = 21

-> [0.000000] [mc_global/INFO] Expanded / Visited = 0.954545

diff --git a/examples/msg/mc/chord/chord_neverjoin.tesh b/examples/msg/mc/chord/chord_neverjoin.tesh
index 2688128..b458c9c 100644 (file)
--- a/examples/msg/mc/chord/chord_neverjoin.tesh
+++ b/examples/msg/mc/chord/chord_neverjoin.tesh
@@ -25,7 +25,6 @@ $ ${bindir:=.}/chord_liveness --cfg=model-check:1 --cfg=contexts/factory:ucontex
 > [0.000000] [mc_global/INFO] [(1)node] Wait (comm=(verbose only) [(3)node -> (1)node])
 > [0.000000] [mc_global/INFO] [(1)node] iRecv (dst=node, buff=(verbose only), size=(verbose only))
 > [0.000000] [mc_global/INFO] [(1)node] Test FALSE (comm=(verbose only))
 > [0.000000] [mc_global/INFO] [(1)node] Wait (comm=(verbose only) [(3)node -> (1)node])
 > [0.000000] [mc_global/INFO] [(1)node] iRecv (dst=node, buff=(verbose only), size=(verbose only))
 > [0.000000] [mc_global/INFO] [(1)node] Test FALSE (comm=(verbose only))

-> [0.000000] [mc_global/INFO] Expanded states = 11
-> [0.000000] [mc_global/INFO] Visited states = 10
+> [0.000000] [mc_global/INFO] Expanded pairs = 14
+> [0.000000] [mc_global/INFO] Visited pairs = 10

 > [0.000000] [mc_global/INFO] Executed transitions = 10
 > [0.000000] [mc_global/INFO] Executed transitions = 10

-> [0.000000] [mc_global/INFO] Expanded / Visited = 0.909091

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 970ef80..947fc55 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -527,7 +527,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
       depth++;
     
       /* Update statistics */
       depth++;
     
       /* Update statistics */

-      mc_stats->visited_states++;
+      mc_stats->visited_pairs++;

       mc_stats->executed_transitions++;
 
       item = xbt_fifo_get_prev_item(item);
       mc_stats->executed_transitions++;
 
       item = xbt_fifo_get_prev_item(item);


@@ -570,7 +570,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
       depth++;
     
       /* Update statistics */
       depth++;
     
       /* Update statistics */

-      mc_stats->visited_states++;
+      mc_stats->visited_pairs++;

       mc_stats->executed_transitions++;
     }
   }  
       mc_stats->executed_transitions++;
     }
   }  


@@ -692,14 +692,14 @@ void MC_dump_stack_liveness(xbt_fifo_t stack){
 
 void MC_print_statistics(mc_stats_t stats)
 {
 
 void MC_print_statistics(mc_stats_t stats)
 {

-  //XBT_INFO("State space size ~= %lu", stats->state_size);
-  XBT_INFO("Expanded states = %lu", stats->expanded_states);
-  XBT_INFO("Visited states = %lu", stats->visited_states);
+  if(stats->expanded_pairs == 0){
+    XBT_INFO("Expanded states = %lu", stats->expanded_states);
+    XBT_INFO("Visited states = %lu", stats->visited_states);
+  }else{
+    XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
+    XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
+  }

   XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
   XBT_INFO("Executed transitions = %lu", stats->executed_transitions);

-  XBT_INFO("Expanded / Visited = %lf",
-           (double) stats->visited_states / stats->expanded_states);
-  /*XBT_INFO("Exploration coverage = %lf",
-    (double)stats->expanded_states / stats->state_size); */

 }
 
 void MC_assert(int prop)
 }
 
 void MC_assert(int prop)

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index f19a670..7d07e0d 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -19,17 +19,15 @@ xbt_dynar_t successors;
 
 /********* Static functions *********/
 
 
 /********* Static functions *********/
 

-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;
+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);
 
   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->num = num;
+  new_pair->automaton_state = as;

   new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
   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 */
   new_pair->system_state = MC_take_snapshot();  
   
   /* Get values of propositional symbols */


@@ -42,105 +40,219 @@ static int is_reached_acceptance_pair(xbt_automaton_state_t st){
     res = f();
     xbt_dynar_push_as(new_pair->prop_ato, int, res);
   }
     res = f();
     xbt_dynar_push_as(new_pair->prop_ato, int, res);
   }

-  
+
+  return new_pair;
+
+}
+
+static int is_reached_acceptance_pair(int num, xbt_automaton_state_t as){
+
+  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+  MC_SET_RAW_MEM;
+  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;
   MC_UNSET_RAW_MEM;
   
   if(xbt_dynar_is_empty(acceptance_pairs)){
 
     MC_SET_RAW_MEM;

-    /* New acceptance pair */

     xbt_dynar_push(acceptance_pairs, &new_pair); 
     MC_UNSET_RAW_MEM;
 
     if(raw_mem_set)
       MC_SET_RAW_MEM;
     xbt_dynar_push(acceptance_pairs, &new_pair); 
     MC_UNSET_RAW_MEM;
 
     if(raw_mem_set)
       MC_SET_RAW_MEM;

- 
-    return 0;
+
+    return -1;

 
   }else{
 
     MC_SET_RAW_MEM;
     
 
   }else{
 
     MC_SET_RAW_MEM;
     

-    cursor = 0;
+    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;
     mc_acceptance_pair_t pair_test = NULL;

-     
-    xbt_dynar_foreach(acceptance_pairs, cursor, pair_test){
-      if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug))
-        XBT_DEBUG("****** Pair reached #%d ******", pair_test->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)
-              MC_SET_RAW_MEM;
-            else
-              MC_UNSET_RAW_MEM;
-            
-            return 1;
+    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++;

           }
           }

-        }else{
-          XBT_DEBUG("Different values of propositional symbols");

         }
         }

-      }else{
-        XBT_DEBUG("Different automaton state");

       }
     }
 
       }
     }
 

-    /* New acceptance pair */
-    xbt_dynar_push(acceptance_pairs, &new_pair); 
+    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;
+
+    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;
     
     MC_UNSET_RAW_MEM;
 
     if(raw_mem_set)
       MC_SET_RAW_MEM;

- 
-    compare = 0;

     
     

-    return 0;
+    return -1;

     
   }
     
   }

+ 

 }
 
 
 }
 
 

-static void set_acceptance_pair_reached(xbt_automaton_state_t st){
+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;
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
  
   MC_SET_RAW_MEM;

+  mc_acceptance_pair_t new_pair = acceptance_pair_new(num, as);
+  MC_UNSET_RAW_MEM;

 
 

-  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();
+  if(xbt_dynar_is_empty(acceptance_pairs)){

 
 

-  /* Get values of propositional symbols */
-  unsigned int cursor = 0;
-  xbt_automaton_propositional_symbol_t ps = NULL;
-  int res;
-  int_f_void_t f;
+     MC_SET_RAW_MEM;
+     xbt_dynar_push(acceptance_pairs, &new_pair); 
+     MC_UNSET_RAW_MEM;

 
 

-  xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
-    f = (int_f_void_t)ps->function;
-    res = f();
-    xbt_dynar_push_as(pair->prop_ato, int, res);
-  }
+  }else{

 
 

-  xbt_dynar_push(acceptance_pairs, &pair); 
-  
-  MC_UNSET_RAW_MEM;
+    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;
+    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;
+    
+  }

 
   if(raw_mem_set)
     MC_SET_RAW_MEM;
     
 }
 
 
   if(raw_mem_set)
     MC_SET_RAW_MEM;
     
 }
 

-static mc_visited_pair_t visited_pair_new(xbt_automaton_state_t as){
+static void remove_acceptance_pair(int num_pair){
+
+  unsigned int cursor = 0;
+  mc_acceptance_pair_t current_pair;
+
+  xbt_dynar_foreach(acceptance_pairs, cursor, current_pair){
+    if(current_pair->num == num_pair)
+      break;
+  }
+  
+  xbt_dynar_remove_at(acceptance_pairs, cursor, NULL);
+
+}
+
+static mc_visited_pair_t visited_pair_new(int num, xbt_automaton_state_t as){

 
   mc_visited_pair_t new_pair = NULL;
   new_pair = xbt_new0(s_mc_visited_pair_t, 1);
   new_pair->automaton_state = as;
 
   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->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);


@@ -161,7 +273,7 @@ static mc_visited_pair_t visited_pair_new(xbt_automaton_state_t as){
 
 }
 
 
 }
 

-static int is_visited_pair(xbt_automaton_state_t as){
+static int is_visited_pair(int num, xbt_automaton_state_t as){

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


@@ -169,7 +281,7 @@ static int is_visited_pair(xbt_automaton_state_t as){
   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_visited_pair_t new_pair = visited_pair_new(as);
+  mc_visited_pair_t new_pair = visited_pair_new(num, as);

   MC_UNSET_RAW_MEM;
 
   if(xbt_dynar_is_empty(visited_pairs)){
   MC_UNSET_RAW_MEM;
 
   if(xbt_dynar_is_empty(visited_pairs)){


@@ -443,7 +555,7 @@ void MC_ddfs_init(void){
         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_acceptance_pair_reached(automaton_state);
+        set_acceptance_pair_reached(mc_initial_pair->num, automaton_state);

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


@@ -483,7 +595,7 @@ 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->visited_states++;
+  mc_stats->visited_pairs++;

 
   int value;
   mc_state_t next_graph_state = NULL;
 
   int value;
   mc_state_t next_graph_state = NULL;


@@ -498,7 +610,6 @@ void MC_ddfs(int search_cycle){
   mc_pair_t pair_succ;
 
   mc_pair_t pair_to_remove;
   mc_pair_t pair_succ;
 
   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){
 


@@ -583,7 +694,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(is_reached_acceptance_pair(pair_succ->automaton_state)){
+              if(is_reached_acceptance_pair(pair_succ->num, pair_succ->automaton_state) != -1){

         
                 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));
 


@@ -598,7 +709,7 @@ void MC_ddfs(int search_cycle){
 
               }else{
 
 
               }else{
 

-                if(is_visited_pair(pair_succ->automaton_state) != -1){
+                if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){

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


@@ -621,7 +732,7 @@ void MC_ddfs(int search_cycle){
 
             }else{
 
 
             }else{
 

-              if(is_visited_pair(pair_succ->automaton_state) != -1){
+              if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){

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


@@ -639,7 +750,7 @@ void MC_ddfs(int search_cycle){
 
           }else{
 
 
           }else{
 

-            if(is_visited_pair(pair_succ->automaton_state) != -1){
+            if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){

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


@@ -650,7 +761,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);
       

-                set_acceptance_pair_reached(pair_succ->automaton_state); 
+                set_acceptance_pair_reached(pair_succ->num, pair_succ->automaton_state); 

 
                 search_cycle = 1;
 
 
                 search_cycle = 1;
 


@@ -734,7 +845,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(is_reached_acceptance_pair(pair_succ->automaton_state)){
+            if(is_reached_acceptance_pair(pair_succ->num, pair_succ->automaton_state) != -1){

            
               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);
         


@@ -749,7 +860,7 @@ void MC_ddfs(int search_cycle){
 
             }else{
 
 
             }else{
 

-              if(is_visited_pair(pair_succ->automaton_state) != -1){
+              if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){

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


@@ -772,7 +883,7 @@ void MC_ddfs(int search_cycle){
 
           }else{
             
 
           }else{
             

-            if(is_visited_pair(pair_succ->automaton_state) != -1){
+            if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){

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


@@ -792,7 +903,7 @@ void MC_ddfs(int search_cycle){
 
         }else{
       
 
         }else{
       

-          if(is_visited_pair(pair_succ->automaton_state) != -1){
+          if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){

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


@@ -801,7 +912,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))){
 

-              set_acceptance_pair_reached(pair_succ->automaton_state);
+              set_acceptance_pair_reached(pair_succ->num, pair_succ->automaton_state);

          
               search_cycle = 1;
 
          
               search_cycle = 1;
 


@@ -849,9 +960,7 @@ void MC_ddfs(int search_cycle){
   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)){
   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)){

-    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;
+    remove_acceptance_pair(current_pair->num);

   }
   MC_UNSET_RAW_MEM;
 
   }
   MC_UNSET_RAW_MEM;
 

diff --git a/src/mc/mc_pair.c b/src/mc/mc_pair.c
index 9e8ff3e..bd686f9 100644 (file)
--- a/src/mc/mc_pair.c
+++ b/src/mc/mc_pair.c
@@ -12,6 +12,7 @@ mc_pair_t MC_pair_new(mc_state_t gs, xbt_automaton_state_t as, int r){
   p->graph_state = gs;
   p->system_state = NULL;
   p->requests = r;
   p->graph_state = gs;
   p->system_state = NULL;
   p->requests = r;

+  p->num = ++mc_stats->expanded_pairs;

   return p;
 }
 
   return p;
 }
 

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 15deac2..4839b41 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -140,7 +140,9 @@ void MC_state_remove_interleave_process(mc_state_t state, smx_process_t process)
 typedef struct mc_stats {
   unsigned long state_size;
   unsigned long visited_states;
 typedef struct mc_stats {
   unsigned long state_size;
   unsigned long visited_states;

+  unsigned long visited_pairs;

   unsigned long expanded_states;
   unsigned long expanded_states;

+  unsigned long expanded_pairs;

   unsigned long executed_transitions;
 } s_mc_stats_t, *mc_stats_t;
 
   unsigned long executed_transitions;
 } s_mc_stats_t, *mc_stats_t;
 


@@ -285,6 +287,7 @@ typedef struct s_mc_pair{
   mc_state_t graph_state;
   xbt_automaton_state_t automaton_state;
   int requests;
   mc_state_t graph_state;
   xbt_automaton_state_t automaton_state;
   int requests;

+  int num;

 }s_mc_pair_t, *mc_pair_t;
 
 typedef struct s_mc_acceptance_pair{
 }s_mc_pair_t, *mc_pair_t;
 
 typedef struct s_mc_acceptance_pair{


@@ -292,6 +295,8 @@ typedef struct s_mc_acceptance_pair{
   xbt_automaton_state_t automaton_state;
   xbt_dynar_t prop_ato;
   mc_snapshot_t system_state;
   xbt_automaton_state_t automaton_state;
   xbt_dynar_t prop_ato;
   mc_snapshot_t system_state;

+  size_t heap_bytes_used;
+  int nb_processes;

 }s_mc_acceptance_pair_t, *mc_acceptance_pair_t;
 
 typedef struct s_mc_visited_pair{
 }s_mc_acceptance_pair_t, *mc_acceptance_pair_t;
 
 typedef struct s_mc_visited_pair{