model-checker : function to compare values of propositional symbols fixed

diff --git a/examples/msg/mc/automaton.c b/examples/msg/mc/automaton.c
index b2e3ae3..8f189a8 100644 (file)
--- a/examples/msg/mc/automaton.c
+++ b/examples/msg/mc/automaton.c
@@ -341,12 +341,18 @@ int automaton_label_transition_compare(xbt_exp_label_t l1, xbt_exp_label_t l2){
 }
 
 
-int propositional_symbols_compare_value(const void *s1, const void *s2){
+int propositional_symbols_compare_value(xbt_dynar_t s1, xbt_dynar_t s2){
 
-  const int *ps1 = s1;
-  const int *ps2 = s2;
-  printf("ps 1 = %d, ps2 = %d", *ps1, *ps2);
+  int *iptr1, *iptr2;
+  unsigned int cursor;
+  unsigned int nb_elem = xbt_dynar_length(s1);
 
-  return (!(*ps1 == *ps2));
+  for(cursor=0;cursor<nb_elem;cursor++){
+    iptr1 = xbt_dynar_get_ptr(s1, cursor);
+    iptr2 = xbt_dynar_get_ptr(s2, cursor);
+    if(*iptr1 != *iptr2)
+      return 1;
+  } 
 
+  return 0;
 }

diff --git a/examples/msg/mc/automaton.h b/examples/msg/mc/automaton.h
index 485f02b..f140ed2 100644 (file)
--- a/examples/msg/mc/automaton.h
+++ b/examples/msg/mc/automaton.h
@@ -103,7 +103,7 @@ XBT_PUBLIC(xbt_state_t) xbt_automaton_get_current_state(xbt_automaton_t a);
 
 XBT_PUBLIC(int) automaton_state_compare(xbt_state_t s1, xbt_state_t s2);
 
-XBT_PUBLIC(int) propositional_symbols_compare_value(const void *s1, const void *s2);
+XBT_PUBLIC(int) propositional_symbols_compare_value(xbt_dynar_t s1, xbt_dynar_t s2);
 
 XBT_PUBLIC(int) automaton_transition_compare(const void *t1, const void *t2);
 

diff --git a/include/xbt/automaton.h b/include/xbt/automaton.h
index 485f02b..f140ed2 100644 (file)
--- a/include/xbt/automaton.h
+++ b/include/xbt/automaton.h
@@ -103,7 +103,7 @@ XBT_PUBLIC(xbt_state_t) xbt_automaton_get_current_state(xbt_automaton_t a);
 
 XBT_PUBLIC(int) automaton_state_compare(xbt_state_t s1, xbt_state_t s2);
 
-XBT_PUBLIC(int) propositional_symbols_compare_value(const void *s1, const void *s2);
+XBT_PUBLIC(int) propositional_symbols_compare_value(xbt_dynar_t s1, xbt_dynar_t s2);
 
 XBT_PUBLIC(int) automaton_transition_compare(const void *t1, const void *t2);
 

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 14b385e..f0b4a60 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -60,6 +60,8 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
 
 int reached(xbt_automaton_t a, mc_snapshot_t s){
 
+  XBT_DEBUG("Test reached");
+
   if(xbt_dynar_is_empty(reached_pairs)){
     return 0;
   }else{
@@ -77,7 +79,7 @@ int reached(xbt_automaton_t a, mc_snapshot_t s){
     xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
       int (*f)() = ps->function;
       int res = (*f)();
-      xbt_dynar_push(pair->prop_ato, &res);
+      xbt_dynar_push_as(pair->prop_ato, int, res);
     }
     
     cursor = 0;
@@ -85,7 +87,7 @@ int reached(xbt_automaton_t a, mc_snapshot_t s){
     //int (*compare_dynar)(const void*, const void*) = &propositional_symbols_compare_value;
     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
       if(automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
-       if(xbt_dynar_compare(pair_test->prop_ato, pair->prop_ato, propositional_symbols_compare_value) == 0){
+       if(propositional_symbols_compare_value(pair_test->prop_ato, pair->prop_ato) == 0){
          if(snapshot_compare(pair_test->system_state, pair->system_state) == 0){
            MC_UNSET_RAW_MEM;
            return 1;
@@ -118,7 +120,7 @@ int set_pair_reached(xbt_automaton_t a, mc_snapshot_t s){
     xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
       int (*f)() = ps->function;
       int res = (*f)();
-      xbt_dynar_push(pair->prop_ato, &res);
+      xbt_dynar_push_as(pair->prop_ato, int, res);
     }
      
     xbt_dynar_push(reached_pairs, &pair); 

diff --git a/src/xbt/automaton.c b/src/xbt/automaton.c
index b2e3ae3..8f189a8 100644 (file)
--- a/src/xbt/automaton.c
+++ b/src/xbt/automaton.c
@@ -341,12 +341,18 @@ int automaton_label_transition_compare(xbt_exp_label_t l1, xbt_exp_label_t l2){
 }
 
 
-int propositional_symbols_compare_value(const void *s1, const void *s2){
+int propositional_symbols_compare_value(xbt_dynar_t s1, xbt_dynar_t s2){
 
-  const int *ps1 = s1;
-  const int *ps2 = s2;
-  printf("ps 1 = %d, ps2 = %d", *ps1, *ps2);
+  int *iptr1, *iptr2;
+  unsigned int cursor;
+  unsigned int nb_elem = xbt_dynar_length(s1);
 
-  return (!(*ps1 == *ps2));
+  for(cursor=0;cursor<nb_elem;cursor++){
+    iptr1 = xbt_dynar_get_ptr(s1, cursor);
+    iptr2 = xbt_dynar_get_ptr(s2, cursor);
+    if(*iptr1 != *iptr2)
+      return 1;
+  } 
 
+  return 0;
 }

diff --git a/src/xbt/mmalloc/mm_legacy.c b/src/xbt/mmalloc/mm_legacy.c
index 6c72b25..ba34bff 100644 (file)
--- a/src/xbt/mmalloc/mm_legacy.c
+++ b/src/xbt/mmalloc/mm_legacy.c
@@ -307,7 +307,7 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){
   block_busy1 = start1 + mdp1->heapinfo[start1].free.size;
   block_busy2 = start2 + mdp2->heapinfo[start2].free.size;
 
-  XBT_DEBUG("Block busy : %Zu - %Zu", block_busy1, block_busy2);
+  //XBT_DEBUG("Block busy : %Zu - %Zu", block_busy1, block_busy2);
 
 
   if(mdp1->heapinfo[start1].free.size != mdp2->heapinfo[start2].free.size){ // <=> check block_busy
@@ -326,12 +326,12 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){
    
       i=block_busy1 ;
 
-      XBT_DEBUG("Next free : %Zu", mdp1->heapinfo[start1].free.next);
+      //XBT_DEBUG("Next free : %Zu", mdp1->heapinfo[start1].free.next);
 
 
       while(i<mdp1->heapinfo[start1].free.next){
 
-       XBT_DEBUG("i (block busy) : %Zu", i);
+       //XBT_DEBUG("i (block busy) : %Zu", i);
 
        if(mdp1->heapinfo[i].busy.type != mdp2->heapinfo[i].busy.type){
          XBT_DEBUG("Different type of busy block");
@@ -347,7 +347,7 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){
              XBT_DEBUG("Different size of a large cluster");
              return 1;
            }else{
-             XBT_DEBUG("Blocks %Zu : %p - %p / Data size : %Zu (%Zu blocks)", i, addr_block1, addr_block2, (mdp->heapinfo[i].busy.info.size * BLOCKSIZE),mdp->heapinfo[i].busy.info.size );    
+             //XBT_DEBUG("Blocks %Zu : %p - %p / Data size : %Zu (%Zu blocks)", i, addr_block1, addr_block2, (mdp->heapinfo[i].busy.info.size * BLOCKSIZE),mdp->heapinfo[i].busy.info.size );  
              if(memcmp(addr_block1, addr_block2, mdp1->heapinfo[i].busy.info.size * BLOCKSIZE) != 0){
                XBT_DEBUG("Different data in block %Zu", i);
                return 1;
@@ -392,14 +392,17 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){
          return 1;
        }else{
 
-         XBT_DEBUG("Index of next busy block : %Zu - %Zu", block_busy1, block_busy2);
-         XBT_DEBUG("Index of next free cluster : %Zu", mdp1->heapinfo[block_free1].free.next);
+         //XBT_DEBUG("Index of next busy block : %Zu - %Zu", block_busy1, block_busy2);
+         //XBT_DEBUG("Index of next free cluster : %Zu", mdp1->heapinfo[block_free1].free.next);
        
          i = block_busy1;
 
          while(i<mdp1->heapinfo[block_free1].free.next){
 
-           XBT_DEBUG("i (block busy) : %Zu", i);
+           //XBT_DEBUG("i (block busy) : %Zu", i);
+
+           if(i==0)
+             i = 1;
 
            if(mdp1->heapinfo[i].busy.type != mdp2->heapinfo[i].busy.type){
              XBT_DEBUG("Different type of busy block");
@@ -415,7 +418,7 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){
                  XBT_DEBUG("Different size of a large cluster");
                  return 1;
                }else{
-                 XBT_DEBUG("Blocks %Zu : %p - %p / Data size : %Zu", i, addr_block1, addr_block2, (mdp->heapinfo[i].busy.info.size * BLOCKSIZE));              
+                 //XBT_DEBUG("Blocks %Zu : %p - %p / Data size : %Zu", i, addr_block1, addr_block2, (mdp->heapinfo[i].busy.info.size * BLOCKSIZE));            
                  //XBT_DEBUG("Size of large cluster %d", mdp->heapinfo[i].busy.info.size);
                  if(memcmp(addr_block1, addr_block2, (mdp1->heapinfo[i].busy.info.size * BLOCKSIZE)) != 0){
                    XBT_DEBUG("Different data in block %Zu", i);
@@ -442,7 +445,9 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){
                i++;
                break;
              }
-           } 
+           }
+
+           
          }
        }