model-checker : add nb_processes in snapshot

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index eda45c2..d9522fd 100644 (file)
--- 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);
   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;
 
   unsigned int i = 0;
   s_map_region_t reg;

diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c
index 0e038ca..d0c54f1 100644 (file)
--- 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;
 
       
   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)
   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);
 
   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){
   /* 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);
   }
 
     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);
   /* 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 2424c43..bddc9f7 100644 (file)
--- 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;
   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{
 } s_mc_snapshot_t, *mc_snapshot_t;
 
 typedef struct s_mc_snapshot_stack{