From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Sun, 13 Jan 2013 16:05:03 +0000 (+0100)
Subject: model-checker : add nb_processes in snapshot
X-Git-Tag: v3_9_rc1~86^2~14
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/614a9d1249ea6287562890365fc68f261776df79

model-checker : add nb_processes in snapshot
---

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index eda45c202c..d9522fd5dd 100644
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -144,6 +144,7 @@ mc_snapshot_t MC_take_snapshot()
   MC_SET_RAW_MEM;
 
   mc_snapshot_t snapshot = xbt_new0(s_mc_snapshot_t, 1);
+  snapshot->nb_processes = xbt_swag_size(simix_global->process_list);
 
   unsigned int i = 0;
   s_map_region_t reg;
diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c
index 0e038ca554..d0c54f16e0 100644
--- a/src/mc/mc_compare.c
+++ b/src/mc/mc_compare.c
@@ -170,39 +170,6 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c
       
   int errors = 0, i = 0;
 
-  if(s1->num_reg != s2->num_reg){
-    if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose)){
-      XBT_VERB("Different num_reg (s1 = %u, s2 = %u)", s1->num_reg, s2->num_reg);
-    }
-    if(!raw_mem)
-      MC_UNSET_RAW_MEM;
-    return 1;
-  }
-
-  int heap_index = 0, data_libsimgrid_index = 0, data_program_index = 0;
-
-  /* Get index of regions */
-  while(i < s1->num_reg){
-    switch(s1->regions[i]->type){
-    case 0:
-      heap_index = i;
-      i++;
-      break;
-    case 1:
-      data_libsimgrid_index = i;
-      i++;
-      while( i < s1->num_reg && s1->regions[i]->type == 1)
-        i++;
-      break;
-    case 2:
-      data_program_index = i;
-      i++;
-      while( i < s1->num_reg && s1->regions[i]->type == 2)
-        i++;
-      break;
-    }
-  }
-
   if(ct1 != NULL)
     ct1->nb_comparisons++;
   if(ct2 != NULL)
@@ -216,6 +183,35 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c
   if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug))
     xbt_os_timer_start(timer);
 
+  /* Compare number of processes */
+  if(s1->nb_processes != s2->nb_processes){
+     if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+       xbt_os_timer_stop(timer);
+       if(ct1 != NULL)
+         xbt_dynar_push_as(ct1->chunks_used_comparison_times, double, xbt_os_timer_elapsed(timer));
+       if(ct2 != NULL)
+         xbt_dynar_push_as(ct2->chunks_used_comparison_times, double, xbt_os_timer_elapsed(timer));
+       XBT_DEBUG("Different number of processes : %d - %d", s1->nb_processes, s2->nb_processes);
+       errors++;
+     }else{
+        if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose))
+          XBT_VERB("Different number of processes : %d - %d", s1->nb_processes, s2->nb_processes);
+     
+        xbt_os_timer_free(timer);
+        xbt_os_timer_stop(global_timer);
+        if(ct1 != NULL)
+          xbt_dynar_push_as(ct1->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer));
+        if(ct2 != NULL)
+          xbt_dynar_push_as(ct2->snapshot_comparison_times, double, xbt_os_timer_elapsed(global_timer));
+        xbt_os_timer_free(global_timer);
+
+        if(!raw_mem)
+          MC_UNSET_RAW_MEM;
+
+        return 1;
+     }
+  }
+
   /* Compare number of blocks/fragments used in each heap */
 
   if(s1->heap_chunks_used != s2->heap_chunks_used){
@@ -301,6 +297,30 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c
     xbt_os_timer_start(timer);
   }
 
+  int heap_index = 0, data_libsimgrid_index = 0, data_program_index = 0;
+  
+  /* Get index of regions */
+  while(i < s1->num_reg){
+    switch(s1->regions[i]->type){
+    case 0:
+      heap_index = i;
+      i++;
+      break;
+    case 1:
+      data_libsimgrid_index = i;
+      i++;
+      while( i < s1->num_reg && s1->regions[i]->type == 1)
+        i++;
+      break;
+    case 2:
+      data_program_index = i;
+      i++;
+      while( i < s1->num_reg && s1->regions[i]->type == 2)
+        i++;
+      break;
+    }
+  }
+
   /* Compare binary global variables */
 
   is_diff = compare_global_variables(s1->regions[data_program_index]->type, s1->regions[data_program_index]->data, s2->regions[data_program_index]->data);
diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 2424c4385d..bddc9f7c0d 100644
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -36,6 +36,7 @@ typedef struct s_mc_snapshot{
   size_t heap_chunks_used;
   mc_mem_region_t *regions;
   xbt_dynar_t stacks;
+  int nb_processes;
 } s_mc_snapshot_t, *mc_snapshot_t;
 
 typedef struct s_mc_snapshot_stack{