model-checker : new function MC_diff to display all informations about a system state

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

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 8ff2144..b562fa2 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -52,7 +52,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
     case 0:
       if(s1->regions[i]->size != s2->regions[i]->size){
        if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
-         XBT_DEBUG("Different size of heap (s1 = %Zu, s2 = %Zu)", s1->regions[i]->size, s2->regions[i]->size);
+         XBT_DEBUG("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
          errors++;
        }else{
          return 1;
@@ -78,7 +78,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
     case 1 :
       if(s1->regions[i]->size != s2->regions[i]->size){
        if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
-         XBT_DEBUG("Different size of libsimgrid (s1 = %Zu, s2 = %Zu)", s1->regions[i]->size, s2->regions[i]->size);
+         XBT_DEBUG("Different size of libsimgrid (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
          errors++;
        }else{
          return 1;
@@ -104,7 +104,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
       /*case 2:
       if(s1->regions[i]->size != s2->regions[i]->size){
        if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
-         XBT_DEBUG("Different size of program (s1 = %Zu, s2 = %Zu)", s1->regions[i]->size, s2->regions[i]->size);
+         XBT_DEBUG("Different size of program (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
          errors++;
        }else{
          return 1;
@@ -130,7 +130,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
     case 3:
       if(s1->regions[i]->size != s2->regions[i]->size){
        if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
-         XBT_DEBUG("Different size of stack (s1 = %Zu, s2 = %Zu)", s1->regions[i]->size, s2->regions[i]->size);
+         XBT_DEBUG("Different size of stack (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
          errors++;
        }else{
          return 1;
@@ -207,8 +207,14 @@ int reached(xbt_state_t st){
            xbt_free(prop_ato);
            MC_UNSET_RAW_MEM;
            return 1;
+         }else{
+           XBT_DEBUG("Different snapshot");
          }
+       }else{
+         XBT_DEBUG("Different values of propositional symbols");
        }
+      }else{
+       XBT_DEBUG("Different automaton state");
       }
     }
 
@@ -306,11 +312,16 @@ int reached_hash(xbt_state_t st){
            xbt_free(prop_ato);
            MC_UNSET_RAW_MEM;
            return 1;
+         }else{
+           XBT_DEBUG("Different snapshot");
          }
+       }else{
+         XBT_DEBUG("Different values of propositional symbols");
        }
+      }else{
+       XBT_DEBUG("Different automaton state");
       }
-      
-     
+
       region_diff = 0;
     }
     
@@ -407,9 +418,17 @@ int visited(xbt_state_t st, int sc){
                
              return 1;
        
+           }else{
+             XBT_DEBUG("Different snapshot");
            }
+         }else{
+           XBT_DEBUG("Different values of propositional symbols"); 
          }
+       }else{
+         XBT_DEBUG("Different automaton state");
        }
+      }else{
+       XBT_DEBUG("Different value of search_cycle");
       }
     }
 
@@ -479,11 +498,19 @@ int visited_hash(xbt_state_t st, int sc){
              xbt_free(prop_ato);
              MC_UNSET_RAW_MEM;
              return 1;
+           }else{
+             XBT_DEBUG("Different snapshot");
            }
+         }else{
+           XBT_DEBUG("Different values of propositional symbols"); 
          }
+       }else{
+         XBT_DEBUG("Different automaton state");
        }
+      }else{
+       XBT_DEBUG("Different value of search_cycle");
       }
-     
+      
       region_diff = 0;
     }
     
@@ -616,6 +643,7 @@ int MC_automaton_evaluate_label(xbt_exp_label_t l){
   }
   default : 
     return -1;
+    break;
   }
 }