From ca2459a5a9672bb1764ee4a95e59c01c82dcea78 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Fri, 9 Sep 2011 17:52:13 +0200 Subject: [PATCH] model-checker : empty pair for stateless ddfs fixed --- src/mc/mc_liveness.c | 381 ++++++++++++++++++------------------------- 1 file changed, 156 insertions(+), 225 deletions(-) diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index d6ff58b114..2ea1786d8e 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -24,30 +24,30 @@ mc_pair_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){ int reached(mc_pair_t pair){ - char* hash_reached = malloc(sizeof(char)*160); - unsigned int c= 0; - - MC_SET_RAW_MEM; - char *hash = malloc(sizeof(char)*160); - xbt_sha((char *)&pair, hash); - xbt_dynar_foreach(reached_pairs, c, hash_reached){ - if(strcmp(hash, hash_reached) == 0){ + if(xbt_dynar_is_empty(reached_pairs)){ + return 0; + }else{ + MC_SET_RAW_MEM; + char hash[41]; + xbt_sha((const char *)&pair, hash); + if(xbt_dynar_member(reached_pairs, hash)){ MC_UNSET_RAW_MEM; return 1; + }else{ + MC_UNSET_RAW_MEM; + return 0; } } - - MC_UNSET_RAW_MEM; - return 0; + } void set_pair_reached(mc_pair_t pair){ if(reached(pair) == 0){ MC_SET_RAW_MEM; - char *hash = malloc(sizeof(char)*160) ; - xbt_sha((char *)&pair, hash); - xbt_dynar_push(reached_pairs, &hash); + char hash[41]; + xbt_sha((const char *)&pair, hash); + xbt_dynar_push(reached_pairs, &hash); MC_UNSET_RAW_MEM; } @@ -115,8 +115,8 @@ void set_pair_visited(mc_pair_t pair, int sc){ p = xbt_new0(s_mc_visited_pair_t, 1); p->pair = pair; p->search_cycle = sc; - char *hash = malloc(sizeof(char)*160); - xbt_sha((char *)&p, hash); + char hash[41]; + xbt_sha((const char *)&p, hash); xbt_dynar_push(visited_pairs, &hash); MC_UNSET_RAW_MEM; @@ -124,26 +124,21 @@ void set_pair_visited(mc_pair_t pair, int sc){ int visited(mc_pair_t pair, int sc){ - char* hash_visited = malloc(sizeof(char)*160); - unsigned int c= 0; - MC_SET_RAW_MEM; + mc_visited_pair_t p = NULL; p = xbt_new0(s_mc_visited_pair_t, 1); p->pair = pair; p->search_cycle = sc; - char *hash = malloc(sizeof(char)*160); - xbt_sha((char *)&p, hash); - xbt_dynar_foreach(visited_pairs, c, hash_visited){ - if(strcmp(hash, hash_visited) == 0){ - MC_UNSET_RAW_MEM; - return 1; - } + char hash[41]; + xbt_sha((const char *)&p, hash); + if(xbt_dynar_member(visited_pairs, hash)){ + MC_UNSET_RAW_MEM; + return 1; + }else{ + MC_UNSET_RAW_MEM; + return 0; } - - MC_UNSET_RAW_MEM; - return 0; - } @@ -234,7 +229,7 @@ void MC_vddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ /* Get current state */ mc_pair_t current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)); - if(restore==1){ + if(restore == 1){ xbt_swag_foreach(process, simix_global->process_list){ if(MC_process_is_enabled(process)){ MC_state_interleave_process(current_pair->graph_state, process); @@ -253,16 +248,17 @@ void MC_vddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ smx_req_t req = NULL; char *req_str; - mc_pair_t pair_succ; + xbt_transition_t transition_succ; unsigned int cursor; int res; - xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_t), NULL); + xbt_dynar_t successors = NULL; - mc_pair_t next_pair; - mc_snapshot_t next_snapshot; - mc_snapshot_t current_snapshot; + mc_pair_t next_pair = NULL; + mc_snapshot_t next_snapshot = NULL; + mc_snapshot_t current_snapshot = NULL; + mc_pair_t pair_succ = NULL;; while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){ @@ -300,42 +296,38 @@ void MC_vddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ MC_state_interleave_process(next_graph_state, process); } } - + next_snapshot = xbt_new0(s_mc_snapshot_t, 1); MC_take_snapshot(next_snapshot); - - MC_UNSET_RAW_MEM; - xbt_dynar_reset(successors); + successors = xbt_dynar_new(sizeof(mc_pair_t), NULL); + + MC_UNSET_RAW_MEM; cursor = 0; xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ res = MC_automaton_evaluate_label(a, transition_succ->label); - - MC_SET_RAW_MEM; if(res == 1){ + MC_SET_RAW_MEM; next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst); xbt_dynar_push(successors, &next_pair); - } - - MC_UNSET_RAW_MEM; + MC_UNSET_RAW_MEM; + } } cursor = 0; xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ res = MC_automaton_evaluate_label(a, transition_succ->label); - - MC_SET_RAW_MEM; if(res == 2){ + MC_SET_RAW_MEM; next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst); xbt_dynar_push(successors, &next_pair); + MC_UNSET_RAW_MEM; } - - MC_UNSET_RAW_MEM; } @@ -353,9 +345,14 @@ void MC_vddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ //XBT_DEBUG("Successors length %lu", xbt_dynar_length(successors)); cursor = 0; + xbt_dynar_foreach(successors, cursor, pair_succ){ - //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state); + XBT_DEBUG("Search reached pair %p : graph=%p, automaton=%p", pair_succ, pair_succ->graph_state, pair_succ->automaton_state); + char hash[41]; + XBT_DEBUG("Const char pair %s", (const char *)&pair_succ); + xbt_sha((const char *)&pair_succ, hash); + XBT_DEBUG("Hash pair_succ %s", hash); if((search_cycle == 1) && (reached(pair_succ) == 1)){ XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); @@ -367,37 +364,36 @@ void MC_vddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ MC_print_statistics_pairs(mc_stats_pair); exit(0); } + + XBT_DEBUG("Search visited pair %p : graph %p, automaton %p", pair_succ, pair_succ->graph_state, pair_succ->automaton_state); if(visited(pair_succ, search_cycle) == 0){ - mc_stats_pair->executed_transitions++; + //mc_stats_pair->executed_transitions++; MC_SET_RAW_MEM; xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ); set_pair_visited(pair_succ, search_cycle); - //XBT_DEBUG("New pair (graph=%p, automaton=%p) in stack", pair_succ->graph_state, pair_succ->automaton_state); MC_UNSET_RAW_MEM; MC_vddfs_stateful(a, search_cycle, 0); //XBT_DEBUG("Pair (graph=%p, automaton=%p) expanded", pair_succ->graph_state, pair_succ->automaton_state); - if((search_cycle == 0) && ((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2))){ + if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){ - MC_restore_snapshot(current_pair->system_state); + set_pair_reached(pair_succ); + XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); + + MC_SET_RAW_MEM; + xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ); MC_UNSET_RAW_MEM; - - xbt_swag_foreach(process, simix_global->process_list){ - if(MC_process_is_enabled(process)){ - MC_state_interleave_process(current_pair->graph_state, process); - } - } - - - set_pair_reached(current_pair); - XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id); + MC_vddfs_stateful(a, 1, 1); + + //MC_SET_RAW_MEM; xbt_dynar_pop(reached_pairs, NULL); + //MC_UNSET_RAW_MEM; } @@ -407,6 +403,7 @@ void MC_vddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ } } + if(MC_state_interleave_size(current_pair->graph_state) > 0){ MC_restore_snapshot(current_snapshot); @@ -512,7 +509,6 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ MC_UNSET_RAW_MEM; } - /* Get current state */ mc_pair_t current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)); @@ -539,7 +535,7 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ unsigned int cursor; int res; - xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_t), NULL); + xbt_dynar_t successors; mc_pair_t next_pair; mc_snapshot_t next_snapshot; @@ -587,9 +583,11 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ next_snapshot = xbt_new0(s_mc_snapshot_t, 1); MC_take_snapshot(next_snapshot); + successors = xbt_dynar_new(sizeof(mc_pair_t), NULL); + MC_UNSET_RAW_MEM; - xbt_dynar_reset(successors); + //xbt_dynar_reset(successors); cursor = 0; xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ @@ -658,25 +656,24 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ MC_ddfs_stateful(a, search_cycle, 0); - if((search_cycle == 0) && ((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2))){ + if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){ - MC_restore_snapshot(current_pair->system_state); + set_pair_reached(pair_succ); + XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); + + MC_SET_RAW_MEM; + xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ); MC_UNSET_RAW_MEM; - - xbt_swag_foreach(process, simix_global->process_list){ - if(MC_process_is_enabled(process)){ - MC_state_interleave_process(current_pair->graph_state, process); - } - } - - set_pair_reached(current_pair); - XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id); + MC_ddfs_stateful(a, 1, 1); + //MC_SET_RAW_MEM; xbt_dynar_pop(reached_pairs, NULL); + //MC_UNSET_RAW_MEM; } } + if(MC_state_interleave_size(current_pair->graph_state) > 0){ MC_restore_snapshot(current_snapshot); MC_UNSET_RAW_MEM; @@ -715,33 +712,38 @@ mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st){ int reached_stateless(mc_pair_stateless_t pair){ - char* hash_reached = malloc(sizeof(char)*160); - unsigned int c= 0; - - MC_SET_RAW_MEM; - char *hash = malloc(sizeof(char)*160); - xbt_sha((char *)&pair, hash); - xbt_dynar_foreach(reached_pairs, c, hash_reached){ - if(strcmp(hash, hash_reached) == 0){ + if(xbt_dynar_is_empty(reached_pairs)){ + return 0; + }else{ + MC_SET_RAW_MEM; + + char hash[41] =""; + xbt_sha((const char*)&pair, hash); + XBT_DEBUG("Hash : %s", hash); + if(xbt_dynar_member(reached_pairs, hash)){ + XBT_DEBUG("Pair already reached"); MC_UNSET_RAW_MEM; return 1; + }else{ + MC_UNSET_RAW_MEM; + return 0; } } - - MC_UNSET_RAW_MEM; - return 0; } void set_pair_stateless_reached(mc_pair_stateless_t pair){ - if(reached_stateless(pair) == 0){ - - MC_SET_RAW_MEM; - char *hash = malloc(sizeof(char)*160) ; - xbt_sha((char *)&pair, hash); + //MC_SET_RAW_MEM; + char hash[41] = ""; + xbt_sha((const char*)&pair, hash); + XBT_DEBUG("Hash to pushed %s", hash); + if(strcmp(hash, "da39a3ee5e6b4b0d3255bfef95601890afd80709") == 0){ + XBT_DEBUG("Error in hash, pair empty !"); + sleep(4); + } + xbt_dynar_push(reached_pairs, &hash); - MC_UNSET_RAW_MEM; - } + //MC_UNSET_RAW_MEM; } @@ -752,14 +754,13 @@ void MC_ddfs_stateless_init(xbt_automaton_t a){ XBT_DEBUG("Double-DFS stateless init"); XBT_DEBUG("**************************************************"); - mc_pair_stateless_t mc_initial_pair; - mc_state_t initial_graph_state; + mc_pair_stateless_t mc_initial_pair = NULL; + mc_state_t initial_graph_state = NULL; smx_process_t process; MC_wait_for_requests(); MC_SET_RAW_MEM; - initial_graph_state = MC_state_pair_new(); xbt_swag_foreach(process, simix_global->process_list){ if(MC_process_is_enabled(process)){ @@ -768,96 +769,10 @@ void MC_ddfs_stateless_init(xbt_automaton_t a){ } reached_pairs = xbt_dynar_new(sizeof(char *), NULL); - MC_UNSET_RAW_MEM; - /* regarder dans l'automate toutes les transitions activables grâce à l'état initial du système - -> donnera les états initiaux de la propriété consistants avec l'état initial du système */ - unsigned int cursor = 0; - //unsigned int cursor2 = 0; - xbt_state_t state = NULL; - //int res; - //xbt_transition_t transition_succ; - //xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL); - //xbt_dynar_t elses = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL); - //mc_pair_stateless_t pair_succ; - - /*xbt_dynar_foreach(a->states, cursor, state){ - if(state->type == -1){ - xbt_dynar_foreach(state->out, cursor2, transition_succ){ - res = MC_automaton_evaluate_label(a, transition_succ->label); - - if(res == 1){ - - MC_SET_RAW_MEM; - - mc_initial_pair = new_pair_stateless(initial_graph_state, transition_succ->dst); - xbt_dynar_push(successors, &mc_initial_pair); - - MC_UNSET_RAW_MEM; - - } - } - } - } - - cursor = 0; - cursor2 = 0; - - xbt_dynar_foreach(a->states, cursor, state){ - if(state->type == -1){ - xbt_dynar_foreach(state->out, cursor2, transition_succ){ - res = MC_automaton_evaluate_label(a, transition_succ->label); - - if(res == 2){ - - MC_SET_RAW_MEM; - - mc_initial_pair = new_pair_stateless(initial_graph_state, transition_succ->dst); - xbt_dynar_push(successors, &mc_initial_pair); - - MC_UNSET_RAW_MEM; - - } - } - } - } - - - cursor = 0; - - if((xbt_dynar_length(successors) == 0) && (xbt_dynar_length(elses) == 0)){ - xbt_dynar_foreach(a->states, cursor, state){ - if(state->type == -1){ - MC_SET_RAW_MEM; - - mc_initial_pair = new_pair_stateless(initial_graph_state, transition_succ->dst); - xbt_dynar_push(successors, &mc_initial_pair); - - MC_UNSET_RAW_MEM; - } - } - } - - - cursor = 0; - xbt_dynar_foreach(successors, cursor, pair_succ){ - MC_SET_RAW_MEM; - - xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ); - - initial_snapshot = xbt_new0(s_mc_snapshot_t, 1); - MC_take_snapshot(initial_snapshot); - - MC_UNSET_RAW_MEM; - - if(cursor == 0){ - MC_ddfs_stateless(a, 0, 0); - }else{ - MC_ddfs_stateless(a, 0, 1); - } - } */ + xbt_state_t state; xbt_dynar_foreach(a->states, cursor, state){ if(state->type == -1){ @@ -906,41 +821,62 @@ void MC_ddfs_stateless_init(xbt_automaton_t a){ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ - smx_process_t process = NULL; + smx_process_t process; + mc_pair_stateless_t current_pair = NULL; if(xbt_fifo_size(mc_stack_liveness_stateless) == 0) return; if(replay == 1){ MC_replay_liveness(mc_stack_liveness_stateless); + 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); + } + } } - //XBT_DEBUG("Stack size before restore %u", xbt_fifo_size(mc_stack_liveness_stateless)); - /* Get current state */ - mc_pair_stateless_t current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless)); - + current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless)); + XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateless), search_cycle); XBT_DEBUG("Pair : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id,MC_state_interleave_size(current_pair->graph_state)); + + //sleep(1); mc_stats_pair->visited_pairs++; + /*if(MC_state_interleave_size(current_pair->graph_state) == 0 && (current_pair->automaton_state->type == 1)){ + xbt_fifo_shift(mc_stack_liveness_stateless); + 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); + }*/ + int value; mc_state_t next_graph_state = NULL; smx_req_t req = NULL; char *req_str; - mc_pair_stateless_t pair_succ; xbt_transition_t transition_succ; - unsigned int cursor; + unsigned int cursor = 0; int res; - xbt_dynar_t successors; - - mc_pair_stateless_t next_pair; - //mc_snapshot_t current_snap; - + mc_pair_stateless_t next_pair = NULL; + mc_pair_stateless_t pair_succ; + + xbt_dynar_t successors = NULL; + MC_SET_RAW_MEM; + successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL); + MC_UNSET_RAW_MEM; + while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){ //XBT_DEBUG("Interleave size %u", MC_state_interleave_size(current_pair->graph_state)); @@ -963,11 +899,11 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ MC_wait_for_requests(); - /* Create the new expanded graph_state */ MC_SET_RAW_MEM; + /* Create the new expanded graph_state */ next_graph_state = MC_state_pair_new(); - + /* Get enabled process and insert it in the interleave set of the next graph_state */ xbt_swag_foreach(process, simix_global->process_list){ if(MC_process_is_enabled(process)){ @@ -975,55 +911,51 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ } } - successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL); + xbt_dynar_reset(successors); MC_UNSET_RAW_MEM; - //xbt_dynar_reset(successors); - cursor = 0; - + + cursor= 0; xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ res = MC_automaton_evaluate_label(a, transition_succ->label); - MC_SET_RAW_MEM; - if(res == 1){ // enabled transition in automaton + MC_SET_RAW_MEM; next_pair = new_pair_stateless(next_graph_state, transition_succ->dst); xbt_dynar_push(successors, &next_pair); + MC_UNSET_RAW_MEM; } - MC_UNSET_RAW_MEM; } cursor = 0; xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ - + res = MC_automaton_evaluate_label(a, transition_succ->label); - - MC_SET_RAW_MEM; if(res == 2){ // enabled transition in automaton + MC_SET_RAW_MEM; next_pair = new_pair_stateless(next_graph_state, transition_succ->dst); xbt_dynar_push(successors, &next_pair); + MC_UNSET_RAW_MEM; } - MC_UNSET_RAW_MEM; } if(xbt_dynar_length(successors) == 0){ - MC_SET_RAW_MEM; next_pair = new_pair_stateless(next_graph_state, current_pair->automaton_state); xbt_dynar_push(successors, &next_pair); MC_UNSET_RAW_MEM; - } cursor = 0; + //XBT_DEBUG("Successors length %lu", xbt_dynar_length(successors)); xbt_dynar_foreach(successors, cursor, pair_succ){ @@ -1039,30 +971,30 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ exit(0); } - mc_stats_pair->executed_transitions++; - MC_SET_RAW_MEM; xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ); MC_UNSET_RAW_MEM; MC_ddfs_stateless(a, search_cycle, 0); + + //XBT_DEBUG("Stack size %u", xbt_fifo_size(mc_stack_liveness_stateless)); - if((search_cycle == 0) && ((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2))){ + if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){ - /*xbt_swag_foreach(process, simix_global->process_list){ - if(MC_process_is_enabled(process)){ - MC_state_interleave_process(current_pair->graph_state, process); - } - }*/ + XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); + set_pair_stateless_reached(pair_succ); - set_pair_stateless_reached(current_pair); - XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id); + MC_SET_RAW_MEM; + xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ); + MC_UNSET_RAW_MEM; MC_ddfs_stateless(a, 1, 1); - + + MC_SET_RAW_MEM; xbt_dynar_pop(reached_pairs, NULL); + MC_UNSET_RAW_MEM; } } @@ -1072,7 +1004,6 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ } } - MC_SET_RAW_MEM; xbt_fifo_shift(mc_stack_liveness_stateless); -- 2.20.1