From 5e6bdb0664f53d8b1534cb4f907cfe8e98911d95 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Wed, 4 May 2011 16:07:05 +0200 Subject: [PATCH] model-check : show stack for acceptance cycle --- examples/msg/mc/example_automaton.c | 7 ++- src/mc/mc_dfs.c | 98 +++++++++++++++++++---------- src/mc/private.h | 2 + 3 files changed, 70 insertions(+), 37 deletions(-) diff --git a/examples/msg/mc/example_automaton.c b/examples/msg/mc/example_automaton.c index 74ba1e8c76..a4c9572cfa 100644 --- a/examples/msg/mc/example_automaton.c +++ b/examples/msg/mc/example_automaton.c @@ -6,7 +6,7 @@ #include "y.tab.c" -#define N 3 +#define N 5 XBT_LOG_NEW_DEFAULT_CATEGORY(example, "Example with automaton"); @@ -40,8 +40,8 @@ int server(int argc, char *argv[]) } MSG_task_receive(&task, "mymailbox"); count++; - r++; - r=r%2; + r=(r+1)%4; + } MC_assert(atoi(MSG_task_get_name(task)) == 3); @@ -59,6 +59,7 @@ int client(int argc, char *argv[]) MSG_task_send(task, "mymailbox"); XBT_INFO("Sent!"); + r=(r+1)%4; return 0; } diff --git a/src/mc/mc_dfs.c b/src/mc/mc_dfs.c index 55a10f3888..514417ad4d 100644 --- a/src/mc/mc_dfs.c +++ b/src/mc/mc_dfs.c @@ -24,7 +24,7 @@ mc_pairs_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){ void set_pair_visited(mc_state_t gs, xbt_state_t as, int sc){ if(visited(gs, as, sc) == 0){ - XBT_DEBUG("New visited pair : graph=%p, automaton=%p", gs, as); + //XBT_DEBUG("New visited pair : graph=%p, automaton=%p", gs, as); MC_SET_RAW_MEM; mc_visited_pairs_t p = NULL; p = xbt_new0(s_mc_visited_pairs_t, 1); @@ -41,13 +41,23 @@ void set_pair_visited(mc_state_t gs, xbt_state_t as, int sc){ int reached(mc_state_t gs, xbt_state_t as ){ mc_reached_pairs_t rp = NULL; - unsigned int cursor = 0; - + unsigned int c= 0; + unsigned int i; + int different_process; + MC_SET_RAW_MEM; - xbt_dynar_foreach(reached_pairs, cursor, rp){ - if((rp->graph_state == gs) &&(rp->automaton_state == as)){ - MC_UNSET_RAW_MEM; - return 1; + xbt_dynar_foreach(reached_pairs, c, rp){ + if(rp->automaton_state == as){ + different_process=0; + for(i=0; i < gs->max_pid; i++){ + if(gs->proc_status[i].state != rp->graph_state->proc_status[i].state){ + different_process++; + } + } + if(different_process==0){ + MC_UNSET_RAW_MEM; + return 1; + } } } MC_UNSET_RAW_MEM; @@ -63,7 +73,7 @@ void set_pair_reached(mc_state_t gs, xbt_state_t as){ p->graph_state = gs; p->automaton_state = as; xbt_dynar_push(reached_pairs, &p); - XBT_DEBUG("New reached pair : graph=%p, automaton=%p", gs, as); + //XBT_DEBUG("New reached pair : graph=%p, automaton=%p", gs, as); MC_UNSET_RAW_MEM; } @@ -246,7 +256,7 @@ void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){ mc_pairs_t current_pair = (mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)); XBT_DEBUG("**************************************************"); - XBT_DEBUG("State=%p, %u interleave, mc_snapshot_stack size=%d", current_pair, MC_state_interleave_size(current_pair->graph_state), xbt_fifo_size(mc_snapshot_stack)); + XBT_DEBUG("State : graph=%p, automaton=%p, %u interleave, stack size=%d", current_pair->graph_state, current_pair->automaton_state, MC_state_interleave_size(current_pair->graph_state), xbt_fifo_size(mc_snapshot_stack)); //XBT_DEBUG("Restore : %d", restore); @@ -277,7 +287,7 @@ void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){ while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){ - XBT_DEBUG("Current pair : %p (%u interleave)", current_pair, MC_state_interleave_size(current_pair->graph_state)+1); + //XBT_DEBUG("Current pair : %p (%u interleave)", current_pair, MC_state_interleave_size(current_pair->graph_state)+1); //XBT_DEBUG("Visited pairs : %lu", xbt_dynar_length(visited_pairs)); MC_SET_RAW_MEM; @@ -335,11 +345,11 @@ void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){ if(res == 1){ // enabled transition in automaton xbt_dynar_push(successors, &next_pair); - XBT_DEBUG("New Successors length : %lu", xbt_dynar_length(successors)); + //XBT_DEBUG("New Successors length : %lu", xbt_dynar_length(successors)); }else{ if(res == 2){ xbt_dynar_push(elses, &next_pair); - XBT_DEBUG("New Elses length : %lu", xbt_dynar_length(elses)); + //XBT_DEBUG("New Elses length : %lu", xbt_dynar_length(elses)); } } @@ -373,24 +383,23 @@ void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){ MC_UNSET_RAW_MEM; set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle); - MC_dfs(a, search_cycle, 0); if((search_cycle == 0) && (pair_succ->automaton_state->type == 1)){ - mc_pairs_t first_item = (mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)); - if((first_item->graph_state != pair_succ->graph_state) || (first_item->automaton_state != pair_succ->automaton_state) ){ - MC_SET_RAW_MEM; - xbt_fifo_unshift(mc_snapshot_stack, pair_succ); - MC_UNSET_RAW_MEM; - } + /* mc_pairs_t first_item = (mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)); */ + /* if((first_item->graph_state != pair_succ->graph_state) || (first_item->automaton_state != pair_succ->automaton_state) ){ */ + /* MC_SET_RAW_MEM; */ + /* xbt_fifo_unshift(mc_snapshot_stack, pair_succ); */ + /* MC_UNSET_RAW_MEM; */ + /* } */ set_pair_reached(pair_succ->graph_state, pair_succ->automaton_state); XBT_DEBUG("Acceptance state : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state); MC_dfs(a, 1, 0); } }else{ - XBT_DEBUG("Pair (graph=%p, automaton=%p) already visited !", pair_succ->graph_state, pair_succ->automaton_state ); + //XBT_DEBUG("Pair (graph=%p, automaton=%p) already visited !", pair_succ->graph_state, pair_succ->automaton_state ); set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle); } @@ -414,19 +423,14 @@ void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){ if((search_cycle == 0) && (pair_succ->automaton_state->type == 1)){ - mc_pairs_t first_item = (mc_pairs_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)); - if((first_item->graph_state != pair_succ->graph_state) || (first_item->automaton_state != pair_succ->automaton_state)){ - MC_SET_RAW_MEM; - xbt_fifo_unshift(mc_snapshot_stack, pair_succ); - MC_UNSET_RAW_MEM; - } - set_pair_reached(pair_succ->graph_state, pair_succ->automaton_state); XBT_DEBUG("Acceptance state : graph state=%p, automaton state=%p",pair_succ->graph_state, pair_succ->automaton_state); MC_dfs(a, 1, 0); + } }else{ - XBT_DEBUG("Pair (graph=%p, automaton=%p) already visited !", pair_succ->graph_state, pair_succ->automaton_state ); + //XBT_DEBUG("Pair (graph=%p, automaton=%p) already visited !", pair_succ->graph_state, pair_succ->automaton_state ); + /* Different graph_state */ set_pair_visited(pair_succ->graph_state, pair_succ->automaton_state, search_cycle); } @@ -437,23 +441,49 @@ void MC_dfs(xbt_automaton_t a, int search_cycle, int restore){ if(MC_state_interleave_size(current_pair->graph_state) > 0){ MC_restore_snapshot(current_snapshot); MC_UNSET_RAW_MEM; - XBT_DEBUG("Snapshot restored"); + //XBT_DEBUG("Snapshot restored"); } } if((search_cycle == 1) && (reached(current_pair->graph_state, current_pair->automaton_state) == 1)){ - XBT_DEBUG("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); - XBT_DEBUG("| ACCEPTANCE CYCLE |"); - XBT_DEBUG("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); - // afficher chemin menant au cycle d'acceptation + XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); + XBT_INFO("| ACCEPTANCE CYCLE |"); + XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); + XBT_INFO("Counter-example that violates formula :"); + MC_show_snapshot_stack(mc_snapshot_stack); + MC_dump_snapshot_stack(mc_snapshot_stack); exit(0); } MC_SET_RAW_MEM; xbt_fifo_shift(mc_snapshot_stack); - XBT_DEBUG("State shifted in snapshot_stack, mc_snapshot_stack size=%d", xbt_fifo_size(mc_snapshot_stack)); + //XBT_DEBUG("State shifted in snapshot_stack, mc_snapshot_stack size=%d", xbt_fifo_size(mc_snapshot_stack)); MC_UNSET_RAW_MEM; + +} + +void MC_show_snapshot_stack(xbt_fifo_t stack){ + int value; + mc_pairs_t pair; + xbt_fifo_item_t item; + smx_req_t req; + char *req_str = NULL; + + for (item = xbt_fifo_get_last_item(stack); + (item ? (pair = (mc_pairs_t) (xbt_fifo_get_item_content(item))) + : (NULL)); item = xbt_fifo_get_prev_item(item)) { + req = MC_state_get_executed_request(pair->graph_state, &value); + if(req){ + req_str = MC_request_to_string(req, value); + XBT_INFO("%s", req_str); + xbt_free(req_str); + } + } +} + +void MC_dump_snapshot_stack(xbt_fifo_t stack){ + } diff --git a/src/mc/private.h b/src/mc/private.h index e98ed9ad5e..0c151dd4c6 100644 --- a/src/mc/private.h +++ b/src/mc/private.h @@ -199,5 +199,7 @@ void set_pair_visited(mc_state_t gs, xbt_state_t as, int search_cycle); int visited(mc_state_t gs, xbt_state_t as, int search_cycle); int reached(mc_state_t gs, xbt_state_t as); void set_pair_reached(mc_state_t gs, xbt_state_t as); +void MC_show_snapshot_stack(xbt_fifo_t stack); +void MC_dump_snapshot_stack(xbt_fifo_t stack); #endif -- 2.20.1