}
-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;
}
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);
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);
int reached(xbt_automaton_t a, mc_snapshot_t s){
+ XBT_DEBUG("Test reached");
+
if(xbt_dynar_is_empty(reached_pairs)){
return 0;
}else{
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;
//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;
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);
}
-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;
}
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
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");
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;
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");
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);
i++;
break;
}
- }
+ }
+
+
}
}