X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/1f3dc5fab0ccdb98c1c77fdb2f96f662ea3e45a2..41982e805766505052bbfc0f887ab4f9f1be560a:/src/mc/mc_liveness.c diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index d6ff58b114..6e0bb8c52d 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -5,7 +5,6 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, "Logging specific to algorithms for liveness properties verification"); xbt_dynar_t initial_pairs = NULL; -int max_pair = 0; xbt_dynar_t reached_pairs; extern mc_snapshot_t initial_snapshot; @@ -15,42 +14,90 @@ mc_pair_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){ p->system_state = sn; p->automaton_state = st; p->graph_state = sg; - p->num = max_pair; - max_pair++; mc_stats_pair->expanded_pairs++; return p; } -int reached(mc_pair_t pair){ +int reached(xbt_automaton_t a){ - 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){ - MC_UNSET_RAW_MEM; - return 1; + if(xbt_dynar_is_empty(reached_pairs)){ + return 0; + }else{ + MC_SET_RAW_MEM; + + mc_pair_reached_t pair = NULL; + pair = xbt_new0(s_mc_pair_reached_t, 1); + pair->automaton_state = a->current_state; + pair->prop_ato = xbt_dynar_new(sizeof(int), NULL); + + /* Get values of propositional symbols */ + unsigned int cursor = 0; + xbt_propositional_symbol_t ps = NULL; + xbt_dynar_foreach(a->propositional_symbols, cursor, ps){ + int (*f)() = ps->function; + int res = (*f)(); + xbt_dynar_push(pair->prop_ato, &res); + } + + cursor = 0; + mc_pair_reached_t pair_test; + //int size = xbt_dynar_length(pair->prop_ato); + //int i, d1, d2; + + xbt_dynar_foreach(reached_pairs, cursor, pair_test){ + /*if(memcmp(pair_test->automaton_state, pair->automaton_state, sizeof(xbt_state_t)) == 0){ + for(i=0; i< size; i++){ + d1 = xbt_dynar_get_as(pair->prop_ato, i, int); + d2 = xbt_dynar_get_as(pair_test->prop_ato, i, int); + if(d1 == d2){ + MC_UNSET_RAW_MEM; + return 1; + } + } + }*/ + + if(memcmp(pair_test, pair, sizeof(mc_pair_reached_t)) == 0){ + MC_UNSET_RAW_MEM; + return 1; + } } + + MC_UNSET_RAW_MEM; + return 0; + } - - MC_UNSET_RAW_MEM; - return 0; } -void set_pair_reached(mc_pair_t pair){ +int set_pair_reached(xbt_automaton_t a){ + + if(reached(a) == 0){ - 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); + + mc_pair_reached_t pair = NULL; + pair = xbt_new0(s_mc_pair_reached_t, 1); + pair->automaton_state = a->current_state; + pair->prop_ato = xbt_dynar_new(sizeof(int), NULL); + + /* Get values of propositional symbols */ + unsigned int cursor = 0; + xbt_propositional_symbol_t ps = NULL; + 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(reached_pairs, &pair); + MC_UNSET_RAW_MEM; + + return 1; + } + return 0; } void MC_pair_delete(mc_pair_t pair){ @@ -115,8 +162,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 +171,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; - } @@ -172,7 +214,7 @@ void MC_vddfs_stateful_init(xbt_automaton_t a){ } visited_pairs = xbt_dynar_new(sizeof(char *), NULL); - reached_pairs = xbt_dynar_new(sizeof(char *), NULL); + reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL); MC_take_snapshot(init_snapshot); @@ -234,7 +276,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); @@ -245,6 +287,7 @@ void MC_vddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateful), 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)); + a->current_state = current_pair->automaton_state; mc_stats_pair->visited_pairs++; @@ -253,16 +296,21 @@ 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 = NULL; + mc_snapshot_t next_snapshot = NULL; + mc_snapshot_t current_snapshot = NULL; + mc_pair_t pair_succ = NULL; - mc_pair_t next_pair; - mc_snapshot_t next_snapshot; - mc_snapshot_t current_snapshot; + MC_SET_RAW_MEM; + successors = xbt_dynar_new(sizeof(mc_pair_t), NULL); + MC_UNSET_RAW_MEM; while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){ @@ -300,42 +348,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); + + 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,11 +397,16 @@ 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)){ + if((search_cycle == 1) && (reached(a) == 1)){ XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); XBT_INFO("| ACCEPTANCE CYCLE |"); XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); @@ -367,37 +416,38 @@ 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++; + set_pair_visited(pair_succ, search_cycle); + 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); + XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); + int res = set_pair_reached(a); + + 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); - xbt_dynar_pop(reached_pairs, NULL); + + if(res){ + MC_SET_RAW_MEM; + xbt_dynar_pop(reached_pairs, NULL); + MC_UNSET_RAW_MEM; + } } @@ -407,6 +457,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); @@ -454,7 +505,7 @@ void MC_ddfs_stateful_init(xbt_automaton_t a){ } } - reached_pairs = xbt_dynar_new(sizeof(char *), NULL); + reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL); MC_take_snapshot(init_snapshot); @@ -502,31 +553,31 @@ void MC_ddfs_stateful_init(xbt_automaton_t a){ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ smx_process_t process = NULL; - + mc_pair_t current_pair = NULL; if(xbt_fifo_size(mc_stack_liveness_stateful) == 0) return; if(restore == 1){ - MC_restore_snapshot(((mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)))->system_state); - 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)); - - if(restore==1){ + current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)); + MC_restore_snapshot(current_pair->system_state); xbt_swag_foreach(process, simix_global->process_list){ if(MC_process_is_enabled(process)){ MC_state_interleave_process(current_pair->graph_state, process); } } + MC_UNSET_RAW_MEM; } + /* Get current state */ + current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)); + + XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateful), 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)); + a->current_state = current_pair->automaton_state; + mc_stats_pair->visited_pairs++; int value; @@ -539,14 +590,16 @@ 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 = 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; //sleep(1); - + MC_SET_RAW_MEM; + successors = xbt_dynar_new(sizeof(mc_pair_t), NULL); + MC_UNSET_RAW_MEM; while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){ @@ -559,7 +612,7 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ /* Debug information */ if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ req_str = MC_request_to_string(req, value); - XBT_DEBUG("%u Execute: %s", search_cycle, req_str); + XBT_DEBUG("Execute: %s", req_str); xbt_free(req_str); } @@ -586,39 +639,39 @@ 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); - - MC_UNSET_RAW_MEM; xbt_dynar_reset(successors); + + 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){ // enabled transition in automaton + 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){ // transition always enabled in automaton + 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; + } @@ -638,7 +691,7 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){ //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state); - if((search_cycle == 1) && (reached(pair_succ) == 1)){ + if((search_cycle == 1) && (reached(a) == 1)){ XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); XBT_INFO("| ACCEPTANCE CYCLE |"); XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); @@ -658,26 +711,28 @@ 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); + int res = set_pair_reached(a); + 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); - xbt_dynar_pop(reached_pairs, NULL); + if(res){ + MC_SET_RAW_MEM; + xbt_dynar_pop(reached_pairs, NULL); + MC_UNSET_RAW_MEM; + } } } + if(MC_state_interleave_size(current_pair->graph_state) > 0){ + XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateful)); MC_restore_snapshot(current_snapshot); MC_UNSET_RAW_MEM; } @@ -713,38 +768,6 @@ 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){ - MC_UNSET_RAW_MEM; - return 1; - } - } - - 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); - xbt_dynar_push(reached_pairs, &hash); - MC_UNSET_RAW_MEM; - } - -} - void MC_ddfs_stateless_init(xbt_automaton_t a){ @@ -752,14 +775,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)){ @@ -767,97 +789,15 @@ void MC_ddfs_stateless_init(xbt_automaton_t a){ } } - reached_pairs = xbt_dynar_new(sizeof(char *), NULL); + reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL); - MC_UNSET_RAW_MEM; + initial_snapshot = xbt_new0(s_mc_snapshot_t, 1); + MC_take_snapshot(initial_snapshot); - /* 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 */ + MC_UNSET_RAW_MEM; 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){ @@ -865,10 +805,6 @@ void MC_ddfs_stateless_init(xbt_automaton_t a){ MC_SET_RAW_MEM; mc_initial_pair = new_pair_stateless(initial_graph_state, state); xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair); - - initial_snapshot = xbt_new0(s_mc_snapshot_t, 1); - MC_take_snapshot(initial_snapshot); - MC_UNSET_RAW_MEM; if(cursor == 0){ @@ -884,10 +820,6 @@ void MC_ddfs_stateless_init(xbt_automaton_t a){ MC_SET_RAW_MEM; mc_initial_pair = new_pair_stateless(initial_graph_state, state); xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair); - - initial_snapshot = xbt_new0(s_mc_snapshot_t, 1); - MC_take_snapshot(initial_snapshot); - MC_UNSET_RAW_MEM; if(cursor == 0){ @@ -906,22 +838,31 @@ 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)); + /* Update current state in automaton */ + a->current_state = current_pair->automaton_state; + 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)); + mc_stats_pair->visited_pairs++; @@ -930,20 +871,21 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ 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)); /* Debug information */ if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ @@ -963,11 +905,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,60 +917,56 @@ 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){ - if((search_cycle == 1) && (reached_stateless(pair_succ) == 1)){ + if((search_cycle == 1) && (reached(a) == 1)){ XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); XBT_INFO("| ACCEPTANCE CYCLE |"); XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); @@ -1039,30 +977,29 @@ 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 %p : graph=%p, automaton=%p(%s)", pair_succ, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); + int res = set_pair_reached(a); - 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); - - xbt_dynar_pop(reached_pairs, NULL); + + if(res){ + MC_SET_RAW_MEM; + xbt_dynar_pop(reached_pairs, NULL); + MC_UNSET_RAW_MEM; + } } } @@ -1072,7 +1009,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);