From f88cea0e25ce1a9212c14b414322b882e796d72c Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Tue, 25 Oct 2011 16:44:25 +0200 Subject: [PATCH] model-checker : function to compare values of propositional symbols fixed --- examples/msg/mc/automaton.c | 16 +++++++++++----- examples/msg/mc/automaton.h | 2 +- include/xbt/automaton.h | 2 +- src/mc/mc_liveness.c | 8 +++++--- src/xbt/automaton.c | 16 +++++++++++----- src/xbt/mmalloc/mm_legacy.c | 23 ++++++++++++++--------- 6 files changed, 43 insertions(+), 24 deletions(-) diff --git a/examples/msg/mc/automaton.c b/examples/msg/mc/automaton.c index b2e3ae3305..8f189a8cf0 100644 --- 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;cursorpropositional_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 b2e3ae3305..8f189a8cf0 100644 --- 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;cursorheapinfo[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(iheapinfo[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(iheapinfo[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; } - } + } + + } } -- 2.20.1