model-checker : use new variable _sg_mc_liveness instead of _sg_mc_property_file

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

diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c
index 819ccaa..69176ea 100644 (file)
--- a/src/mc/mc_compare.c
+++ b/src/mc/mc_compare.c
@@ -237,7 +237,6 @@ static int compare_areas_with_type(void *area1, void *area2,
   case DW_TAG_structure_type:
   case DW_TAG_class_type:
     xbt_dynar_foreach(type->members, cursor, member) {
-      XBT_DEBUG("Compare member %s", member->name);
       void *member1 =
           mc_member_snapshot_resolve(area1, type, member, snapshot1);
       void *member2 =
@@ -375,9 +374,6 @@ static int compare_local_variables(mc_snapshot_t snapshot1,
       offset1 = (char *) current_var1->address - (char *) std_heap;
       offset2 = (char *) current_var2->address - (char *) std_heap;
       // TODO, fix current_varX->subprogram->name to include name if DW_TAG_inlined_subprogram
-      XBT_DEBUG("Compare local variable %s of frame %s",
-                current_var1->subprogram->name, current_var1->subprogram->name);
-
 
       if (current_var1->region == 1) {
         dw_type_t subtype = current_var1->type;
@@ -418,17 +414,12 @@ int snapshot_compare(void *state1, void *state2)
   mc_snapshot_t s1, s2;
   int num1, num2;
 
-  if (_sg_mc_property_file && _sg_mc_property_file[0] != '\0') {        /* Liveness MC */
+  if (_sg_mc_liveness) {        /* Liveness MC */
     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;
-       if(xbt_automaton_propositional_symbols_compare_value(((mc_pair_t)state1)->atomic_propositions, ((mc_pair_t)state2)->atomic_propositions) != 0)
-       return 1; */
-  } else {                      /* Safety MC */
+  } else {                      /* Safety or comm determinism MC */
     s1 = ((mc_visited_state_t) state1)->system_state;
     s2 = ((mc_visited_state_t) state2)->system_state;
     num1 = ((mc_visited_state_t) state1)->num;
@@ -461,11 +452,18 @@ int snapshot_compare(void *state1, void *state2)
     }
   }
 
+  /* Compare enabled processes */
+  unsigned int cursor;
+  int pid;
+  xbt_dynar_foreach(s1->enabled_processes, cursor, pid){
+    if(!xbt_dynar_member(s2->enabled_processes, &pid))
+      XBT_VERB("(%d - %d) Different enabled processes", num1, num2);
+  }
+
   int i = 0;
   size_t size_used1, size_used2;
   int is_diff = 0;
 
-
   /* Compare size of stacks */
   while (i < xbt_dynar_length(s1->stacks)) {
     size_used1 = s1->stack_sizes[i];
@@ -531,7 +529,7 @@ int snapshot_compare(void *state1, void *state2)
 #endif
 
   /* Stacks comparison */
-  unsigned int cursor = 0;
+  cursor = 0;
   int diff_local = 0;
 #ifdef MC_DEBUG
   is_diff = 0;