model-checker : fix sort of acceptance pairs

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

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 2b3e32e..e62c1f6 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -203,10 +203,15 @@ static void set_acceptance_pair_reached(mc_pair_t pair){
       }
     }
 
-    if(bytes_used_test < current_bytes_used)
-      xbt_dynar_insert_at(acceptance_pairs, cursor + 1, &pair);
-    else
-      xbt_dynar_insert_at(acceptance_pairs, cursor, &pair);    
+    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)
@@ -321,13 +326,13 @@ static int is_visited_pair(mc_pair_t pair){
     }
 
     if(xbt_dynar_length(visited_pairs) > _sg_mc_visited){
-      int min = mc_stats->expanded_states;
+      int min2 = mc_stats->expanded_pairs;
       unsigned int cursor2 = 0;
       unsigned int index2 = 0;
       xbt_dynar_foreach(visited_pairs, cursor2, pair_test){
-        if(pair_test->num < min){
-          index = cursor2;
-          min = pair_test->num;
+        if(pair_test->num < min2){
+          index2 = cursor2;
+          min2 = pair_test->num;
         }
       }
       xbt_dynar_remove_at(visited_pairs, index2, &pair_test);