From f9bc1eb9da233212a26b57efa214e1224fd03677 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Thu, 1 Dec 2011 15:56:38 +0100 Subject: [PATCH] model-checker : args prgm and automaton changed in global variables --- src/mc/mc_checkpoint.c | 8 +-- src/mc/mc_global.c | 7 +- src/mc/mc_liveness.c | 149 +++++++++++++++++++++++++---------------- src/mc/private.h | 21 +++--- 4 files changed, 114 insertions(+), 71 deletions(-) diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c index 0181c4dc3a..acdafa7fb7 100644 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@ -112,7 +112,7 @@ void MC_take_snapshot(mc_snapshot_t snapshot) } -void MC_take_snapshot_liveness(mc_snapshot_t snapshot, char *prgm) +void MC_take_snapshot_liveness(mc_snapshot_t snapshot) { unsigned int i = 0; s_map_region reg; @@ -138,7 +138,7 @@ void MC_take_snapshot_liveness(mc_snapshot_t snapshot, char *prgm) if (!memcmp(basename(maps->regions[i].pathname), "libsimgrid", 10)){ MC_snapshot_add_region(snapshot, 1, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); } else { - if (!memcmp(basename(maps->regions[i].pathname), basename(prgm), strlen(basename(prgm)))){ + if (!memcmp(basename(maps->regions[i].pathname), basename(prog_name), strlen(basename(prog_name)))){ MC_snapshot_add_region(snapshot, 2, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); } /*else { if (!memcmp(maps->regions[i].pathname, "[stack]", 7)){ @@ -154,7 +154,7 @@ void MC_take_snapshot_liveness(mc_snapshot_t snapshot, char *prgm) /* FIXME: free the memory map */ } -void MC_take_snapshot_to_restore_liveness(mc_snapshot_t snapshot, char *prgm) +void MC_take_snapshot_to_restore_liveness(mc_snapshot_t snapshot) { unsigned int i = 0; s_map_region reg; @@ -180,7 +180,7 @@ void MC_take_snapshot_to_restore_liveness(mc_snapshot_t snapshot, char *prgm) if (!memcmp(basename(maps->regions[i].pathname), "libsimgrid", 10)){ MC_snapshot_add_region(snapshot, 1, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); } else { - if (!memcmp(basename(maps->regions[i].pathname), basename(prgm), strlen(basename(prgm)))){ + if (!memcmp(basename(maps->regions[i].pathname), basename(prog_name), strlen(basename(prog_name)))){ MC_snapshot_add_region(snapshot, 2, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); } } diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 128e06d118..e093b3d1a9 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -32,6 +32,8 @@ mc_stats_pair_t mc_stats_pair = NULL; xbt_fifo_t mc_stack_liveness_stateless = NULL; mc_snapshot_t initial_snapshot_liveness = NULL; +xbt_automaton_t automaton; +char *prog_name; /** * \brief Initialize the model-checker data structures @@ -143,7 +145,10 @@ void MC_init_liveness_stateless(xbt_automaton_t a, char *prgm){ MC_UNSET_RAW_MEM; - MC_ddfs_stateless_init(a, prgm); + automaton = a; + prog_name = strdup(prgm); + + MC_ddfs_stateless_init(); } diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index 7d5eb8a86a..518ef2c5ac 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -97,7 +97,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ } -int reached(xbt_automaton_t a, xbt_state_t st, char *prgm){ +int reached(xbt_state_t st){ if(xbt_fifo_size(reached_pairs) == 0){ @@ -115,14 +115,14 @@ int reached(xbt_automaton_t a, xbt_state_t st, char *prgm){ /* Get values of propositional symbols */ unsigned int cursor = 0; xbt_propositional_symbol_t ps = NULL; - xbt_dynar_foreach(a->propositional_symbols, cursor, ps){ + xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){ f = ps->function; res = (*f)(); xbt_dynar_push_as(prop_ato, int, res); } mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1); - MC_take_snapshot_liveness(sn, prgm); + MC_take_snapshot_liveness(sn); int i=0; xbt_fifo_item_t item = xbt_fifo_get_first_item(reached_pairs); @@ -163,7 +163,7 @@ int reached(xbt_automaton_t a, xbt_state_t st, char *prgm){ } } -void set_pair_reached(xbt_automaton_t a, xbt_state_t st, char *prgm){ +void set_pair_reached(xbt_state_t st){ MC_SET_RAW_MEM; @@ -173,7 +173,7 @@ void set_pair_reached(xbt_automaton_t a, xbt_state_t st, char *prgm){ pair->automaton_state = st; pair->prop_ato = xbt_dynar_new(sizeof(int), NULL); pair->system_state = xbt_new0(s_mc_snapshot_t, 1); - MC_take_snapshot_liveness(pair->system_state, prgm); + MC_take_snapshot_liveness(pair->system_state); /* Get values of propositional symbols */ unsigned int cursor = 0; @@ -181,7 +181,7 @@ void set_pair_reached(xbt_automaton_t a, xbt_state_t st, char *prgm){ int res; int (*f)(); - xbt_dynar_foreach(a->propositional_symbols, cursor, ps){ + xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){ f = ps->function; res = (*f)(); xbt_dynar_push_as(pair->prop_ato, int, res); @@ -194,7 +194,7 @@ void set_pair_reached(xbt_automaton_t a, xbt_state_t st, char *prgm){ } -int visited(xbt_automaton_t a, xbt_state_t st, int sc, char *prgm){ +int visited(xbt_state_t st, int sc){ if(xbt_fifo_size(visited_pairs) == 0){ @@ -213,14 +213,14 @@ int visited(xbt_automaton_t a, xbt_state_t st, int sc, char *prgm){ int res; int (*f)(); - xbt_dynar_foreach(a->propositional_symbols, cursor, ps){ + xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){ f = ps->function; res = (*f)(); xbt_dynar_push_as(prop_ato, int, res); } mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1); - MC_take_snapshot_liveness(sn, prgm); + MC_take_snapshot_liveness(sn); int i=0; xbt_fifo_item_t item = xbt_fifo_get_first_item(visited_pairs); @@ -263,7 +263,7 @@ int visited(xbt_automaton_t a, xbt_state_t st, int sc, char *prgm){ } } -void set_pair_visited(xbt_automaton_t a, xbt_state_t st, int sc, char *prgm){ +void set_pair_visited(xbt_state_t st, int sc){ MC_SET_RAW_MEM; @@ -273,7 +273,7 @@ void set_pair_visited(xbt_automaton_t a, xbt_state_t st, int sc, char *prgm){ pair->automaton_state = st; pair->prop_ato = xbt_dynar_new(sizeof(int), NULL); pair->system_state = xbt_new0(s_mc_snapshot_t, 1); - MC_take_snapshot_liveness(pair->system_state, prgm); + MC_take_snapshot_liveness(pair->system_state); pair->search_cycle = sc; /* Get values of propositional symbols */ @@ -282,7 +282,7 @@ void set_pair_visited(xbt_automaton_t a, xbt_state_t st, int sc, char *prgm){ int res; int (*f)(); - xbt_dynar_foreach(a->propositional_symbols, cursor, ps){ + xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){ f = ps->function; res = (*f)(); xbt_dynar_push_as(pair->prop_ato, int, res); @@ -303,30 +303,30 @@ void MC_pair_delete(mc_pair_t pair){ -int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){ +int MC_automaton_evaluate_label(xbt_exp_label_t l){ switch(l->type){ case 0 : { - int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp); - int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp); + int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp); + int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp); return (left_res || right_res); break; } case 1 : { - int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp); - int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp); + int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp); + int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp); return (left_res && right_res); break; } case 2 : { - int res = MC_automaton_evaluate_label(a, l->u.exp_not); + int res = MC_automaton_evaluate_label(l->u.exp_not); return (!res); break; } case 3 : { unsigned int cursor = 0; xbt_propositional_symbol_t p = NULL; - xbt_dynar_foreach(a->propositional_symbols, cursor, p){ + xbt_dynar_foreach(automaton->propositional_symbols, cursor, p){ if(strcmp(p->pred, l->u.predicat) == 0){ int (*f)() = p->function; return (*f)(); @@ -366,7 +366,7 @@ mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){ return p; } -void MC_ddfs_stateless_init(xbt_automaton_t a, char *prgm){ +void MC_ddfs_stateless_init(){ XBT_DEBUG("**************************************************"); XBT_DEBUG("Double-DFS stateless init"); @@ -393,14 +393,14 @@ void MC_ddfs_stateless_init(xbt_automaton_t a, char *prgm){ /* Save the initial state */ initial_snapshot_liveness = xbt_new0(s_mc_snapshot_t, 1); - MC_take_snapshot_to_restore_liveness(initial_snapshot_liveness, prgm); + MC_take_snapshot_to_restore_liveness(initial_snapshot_liveness); MC_UNSET_RAW_MEM; unsigned int cursor = 0; xbt_state_t state; - xbt_dynar_foreach(a->states, cursor, state){ + xbt_dynar_foreach(automaton->states, cursor, state){ if(state->type == -1){ MC_SET_RAW_MEM; @@ -413,7 +413,7 @@ void MC_ddfs_stateless_init(xbt_automaton_t a, char *prgm){ MC_UNSET_RAW_MEM; } - MC_ddfs_stateless(a, 0, 0, prgm); + MC_ddfs_stateless(0); }else{ if(state->type == 2){ @@ -423,14 +423,14 @@ void MC_ddfs_stateless_init(xbt_automaton_t a, char *prgm){ xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair); MC_UNSET_RAW_MEM; - set_pair_reached(a, state, prgm); + set_pair_reached(state); if(cursor != 0){ MC_restore_snapshot(initial_snapshot_liveness); MC_UNSET_RAW_MEM; } - MC_ddfs_stateless(a, 1, 0, prgm); + MC_ddfs_stateless(1); } } @@ -439,7 +439,7 @@ void MC_ddfs_stateless_init(xbt_automaton_t a, char *prgm){ } -void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *prgm){ +void MC_ddfs_stateless(int search_cycle){ smx_process_t process; mc_pair_stateless_t current_pair = NULL; @@ -447,21 +447,12 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr if(xbt_fifo_size(mc_stack_liveness_stateless) == 0) return; - if(replay == 1){ - MC_replay_liveness(mc_stack_liveness_stateless, 0); - current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless)); - xbt_swag_foreach(process, simix_global->process_list){ - if(MC_process_is_enabled(process)){ - MC_state_interleave_process(current_pair->graph_state, process); - } - } - } /* Get current pair */ current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless)); /* Update current state in buchi automaton */ - a->current_state = current_pair->automaton_state; + automaton->current_state = current_pair->automaton_state; XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateless), search_cycle); @@ -485,9 +476,9 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr if(xbt_fifo_size(mc_stack_liveness_stateless) < MAX_DEPTH_LIVENESS){ - set_pair_visited(a, current_pair->automaton_state, search_cycle, prgm); + set_pair_visited(current_pair->automaton_state, search_cycle); - //XBT_DEBUG("Visited pairs : %d", xbt_fifo_size(visited_pairs)); + XBT_DEBUG("Visited pairs : %d", xbt_fifo_size(visited_pairs)); if(current_pair->requests > 0){ @@ -529,7 +520,7 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr cursor= 0; xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ - res = MC_automaton_evaluate_label(a, transition_succ->label); + res = MC_automaton_evaluate_label(transition_succ->label); if(res == 1){ // enabled transition in automaton MC_SET_RAW_MEM; @@ -544,7 +535,7 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ - res = MC_automaton_evaluate_label(a, transition_succ->label); + res = MC_automaton_evaluate_label(transition_succ->label); if(res == 2){ // true transition in automaton MC_SET_RAW_MEM; @@ -559,13 +550,13 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr xbt_dynar_foreach(successors, cursor, pair_succ){ - if(!visited(a, pair_succ->automaton_state, search_cycle, prgm)){ + if(!visited(pair_succ->automaton_state, search_cycle)){ if(search_cycle == 1){ if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ - if(reached(a, pair_succ->automaton_state, prgm) == 1){ + if(reached(pair_succ->automaton_state) == 1){ XBT_DEBUG("Next pair (depth = %d, %d interleave) already reached !", xbt_fifo_size(mc_stack_liveness_stateless) + 1, MC_state_interleave_size(pair_succ->graph_state)); @@ -582,9 +573,9 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness_stateless) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); - set_pair_reached(a, pair_succ->automaton_state, prgm); + set_pair_reached(pair_succ->automaton_state); - //XBT_DEBUG("Reached pairs : %d", xbt_fifo_size(reached_pairs)); + XBT_DEBUG("Reached pairs : %d", xbt_fifo_size(reached_pairs)); } @@ -596,11 +587,11 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness_stateless) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); - set_pair_reached(a, pair_succ->automaton_state, prgm); + set_pair_reached(pair_succ->automaton_state); search_cycle = 1; - //XBT_DEBUG("Reached pairs : %d", xbt_fifo_size(reached_pairs)); + XBT_DEBUG("Reached pairs : %d", xbt_fifo_size(reached_pairs)); } @@ -610,7 +601,7 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ); MC_UNSET_RAW_MEM; - MC_ddfs_stateless(a, search_cycle, 0, prgm); + MC_ddfs_stateless(search_cycle); /* Restore system before checking others successors */ if(cursor != (xbt_dynar_length(successors) - 1)) @@ -619,6 +610,28 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr }else{ XBT_DEBUG("Next pair already visited"); + + if(search_cycle == 1){ + + if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ + + if(reached(pair_succ->automaton_state) == 1){ + + XBT_DEBUG("Next pair (depth = %d, %d interleave) already reached !", xbt_fifo_size(mc_stack_liveness_stateless) + 1, MC_state_interleave_size(pair_succ->graph_state)); + + XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); + XBT_INFO("| ACCEPTANCE CYCLE |"); + XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); + XBT_INFO("Counter-example that violates formula :"); + MC_show_stack_liveness_stateless(mc_stack_liveness_stateless); + MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless); + MC_print_statistics_pairs(mc_stats_pair); + exit(0); + + } + + } + } } } @@ -645,7 +658,7 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr cursor= 0; xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ - res = MC_automaton_evaluate_label(a, transition_succ->label); + res = MC_automaton_evaluate_label(transition_succ->label); if(res == 1){ // enabled transition in automaton MC_SET_RAW_MEM; @@ -660,7 +673,7 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ - res = MC_automaton_evaluate_label(a, transition_succ->label); + res = MC_automaton_evaluate_label(transition_succ->label); if(res == 2){ // true transition in automaton MC_SET_RAW_MEM; @@ -675,13 +688,13 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr xbt_dynar_foreach(successors, cursor, pair_succ){ - if(!visited(a, pair_succ->automaton_state, search_cycle, prgm)){ + if(!visited(pair_succ->automaton_state, search_cycle)){ if(search_cycle == 1){ if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ - if(reached(a, pair_succ->automaton_state, prgm) == 1){ + if(reached(pair_succ->automaton_state) == 1){ XBT_DEBUG("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness_stateless) + 1); @@ -698,9 +711,9 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness_stateless) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); - set_pair_reached(a, pair_succ->automaton_state, prgm); + set_pair_reached(pair_succ->automaton_state); - //XBT_DEBUG("Reached pairs : %d", xbt_fifo_size(reached_pairs)); + XBT_DEBUG("Reached pairs : %d", xbt_fifo_size(reached_pairs)); } @@ -710,11 +723,11 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)) && (xbt_fifo_size(mc_stack_liveness_stateless) < (MAX_DEPTH_LIVENESS - 1))){ - set_pair_reached(a, pair_succ->automaton_state, prgm); + set_pair_reached(pair_succ->automaton_state); search_cycle = 1; - //XBT_DEBUG("Reached pairs : %d", xbt_fifo_size(reached_pairs)); + XBT_DEBUG("Reached pairs : %d", xbt_fifo_size(reached_pairs)); } @@ -724,7 +737,7 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ); MC_UNSET_RAW_MEM; - MC_ddfs_stateless(a, search_cycle, 0, prgm); + MC_ddfs_stateless(search_cycle); /* Restore system before checking others successors */ if(cursor != xbt_dynar_length(successors) - 1) @@ -733,7 +746,29 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *pr }else{ XBT_DEBUG("Next pair already visited"); - + + if(search_cycle == 1){ + + if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ + + if(reached(pair_succ->automaton_state) == 1){ + + XBT_DEBUG("Next pair (depth = %d, %d interleave) already reached !", xbt_fifo_size(mc_stack_liveness_stateless) + 1, MC_state_interleave_size(pair_succ->graph_state)); + + XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); + XBT_INFO("| ACCEPTANCE CYCLE |"); + XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); + XBT_INFO("Counter-example that violates formula :"); + MC_show_stack_liveness_stateless(mc_stack_liveness_stateless); + MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless); + MC_print_statistics_pairs(mc_stats_pair); + exit(0); + + } + + } + + } } } diff --git a/src/mc/private.h b/src/mc/private.h index 0ee74139ef..415a8bca59 100644 --- a/src/mc/private.h +++ b/src/mc/private.h @@ -35,9 +35,11 @@ typedef struct s_mc_snapshot{ mc_mem_region_t *regions; } s_mc_snapshot_t, *mc_snapshot_t; +extern char *prog_name; + void MC_take_snapshot(mc_snapshot_t); -void MC_take_snapshot_liveness(mc_snapshot_t s, char *prgm); -void MC_take_snapshot_to_restore_liveness(mc_snapshot_t s, char *prgm); +void MC_take_snapshot_liveness(mc_snapshot_t s); +void MC_take_snapshot_to_restore_liveness(mc_snapshot_t s); void MC_restore_snapshot(mc_snapshot_t); void MC_free_snapshot(mc_snapshot_t); @@ -227,19 +229,19 @@ typedef struct s_mc_pair_visited{ int search_cycle; }s_mc_pair_visited_t, *mc_pair_visited_t; -int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l); +int MC_automaton_evaluate_label(xbt_exp_label_t l); mc_pair_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st); -int reached(xbt_automaton_t a, xbt_state_t st, char *prgm); -void set_pair_reached(xbt_automaton_t a, xbt_state_t st, char *prgm); +int reached(xbt_state_t st); +void set_pair_reached(xbt_state_t st); int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2); void MC_show_stack_liveness_stateful(xbt_fifo_t stack); void MC_dump_stack_liveness_stateful(xbt_fifo_t stack); void MC_pair_delete(mc_pair_t pair); void MC_exit_liveness(void); mc_state_t MC_state_pair_new(void); -int visited(xbt_automaton_t a, xbt_state_t st, int search_cycle, char *prgm); -void set_pair_visited(xbt_automaton_t a, xbt_state_t st, int search_cycle, char *prgm); +int visited(xbt_state_t st, int search_cycle); +void set_pair_visited(xbt_state_t st, int search_cycle); /* **** Double-DFS stateful without visited state **** */ @@ -258,10 +260,11 @@ typedef struct s_mc_pair_stateless{ extern xbt_fifo_t mc_stack_liveness_stateless; extern mc_snapshot_t initial_snapshot_liveness; +extern xbt_automaton_t automaton; mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r); -void MC_ddfs_stateless_init(xbt_automaton_t a, char *prgm); -void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *prgm); +void MC_ddfs_stateless_init(); +void MC_ddfs_stateless(int search_cycle); void MC_show_stack_liveness_stateless(xbt_fifo_t stack); void MC_dump_stack_liveness_stateless(xbt_fifo_t stack); void MC_pair_stateless_delete(mc_pair_stateless_t pair); -- 2.20.1