X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/371649bf05bfba5c4b81a68c44fde1bce924d295..7f06482332409f552ac19d126fa69520ade79fcb:/src/mc/mc_liveness.c diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index fb04b4bbc7..561d3653b9 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -83,14 +83,14 @@ static int is_reached_acceptance_pair(mc_pair_t pair){ nb_processes_test = pair_test->nb_processes; if(nb_processes_test < current_nb_processes) start = cursor + 1; - if(nb_processes_test > current_nb_processes) + else if(nb_processes_test > current_nb_processes) end = cursor - 1; - if(nb_processes_test == current_nb_processes){ + else if(nb_processes_test == current_nb_processes){ if(bytes_used_test < current_bytes_used) start = cursor + 1; - if(bytes_used_test > current_bytes_used) + else if(bytes_used_test > current_bytes_used) end = cursor - 1; - if(bytes_used_test == current_bytes_used){ + else if(bytes_used_test == current_bytes_used){ same_processes_and_bytes_not_found = 0; if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){ if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){ @@ -310,14 +310,14 @@ static int is_visited_pair(mc_pair_t pair){ nb_processes_test = pair_test->nb_processes; if(nb_processes_test < current_nb_processes) start = cursor + 1; - if(nb_processes_test > current_nb_processes) + else if(nb_processes_test > current_nb_processes) end = cursor - 1; - if(nb_processes_test == current_nb_processes){ + else if(nb_processes_test == current_nb_processes){ if(bytes_used_test < current_bytes_used) start = cursor + 1; - if(bytes_used_test > current_bytes_used) + else if(bytes_used_test > current_bytes_used) end = cursor - 1; - if(bytes_used_test == current_bytes_used){ + else if(bytes_used_test == current_bytes_used){ same_processes_and_bytes_not_found = 0; if(xbt_automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){ if(xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, pair->atomic_propositions) == 0){ @@ -448,32 +448,29 @@ static int is_visited_pair(mc_pair_t pair){ } -static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l){ +static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l, xbt_dynar_t atomic_propositions_values){ switch(l->type){ case 0 : { - 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); + int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp, atomic_propositions_values); + int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp, atomic_propositions_values); return (left_res || right_res); } case 1 : { - 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); + int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp, atomic_propositions_values); + int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp, atomic_propositions_values); return (left_res && right_res); } case 2 : { - int res = MC_automaton_evaluate_label(l->u.exp_not); + int res = MC_automaton_evaluate_label(l->u.exp_not, atomic_propositions_values); return (!res); } case 3 : { unsigned int cursor = 0; xbt_automaton_propositional_symbol_t p = NULL; - int_f_void_t f; xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){ - if(strcmp(p->pred, l->u.predicat) == 0){ - f = (int_f_void_t)p->function; - return f(); - } + if(strcmp(p->pred, l->u.predicat) == 0) + return (int)xbt_dynar_get_as(atomic_propositions_values, cursor, int); } return -1; } @@ -509,6 +506,7 @@ void MC_ddfs_init(void){ successors = xbt_dynar_new(sizeof(mc_pair_t), NULL); initial_state_liveness->snapshot = MC_take_snapshot(); + initial_state_liveness->prev_pair = 0; MC_UNSET_RAW_MEM; @@ -539,12 +537,13 @@ void MC_ddfs_init(void){ MC_UNSET_RAW_MEM; + MC_ddfs(); + if(cursor != 0){ MC_restore_snapshot(initial_state_liveness->snapshot); MC_UNSET_RAW_MEM; } - - MC_ddfs(); + }else if(automaton_state->type == 2){ /* Acceptance automaton state */ @@ -570,13 +569,13 @@ void MC_ddfs_init(void){ MC_UNSET_RAW_MEM; set_acceptance_pair_reached(initial_pair); + + MC_ddfs(); if(cursor != 0){ MC_restore_snapshot(initial_state_liveness->snapshot); MC_UNSET_RAW_MEM; } - - MC_ddfs(); } } @@ -615,8 +614,10 @@ void MC_ddfs(){ unsigned int cursor = 0; int res; int reached_num, visited_num; + int new_pair = 0; mc_pair_t next_pair = NULL; + xbt_dynar_t prop_values = NULL; if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){ @@ -632,6 +633,8 @@ void MC_ddfs(){ MC_SET_RAW_MEM; xbt_fifo_shift(mc_stack_liveness); + if(dot_output != NULL) + fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, reached_num, initial_state_liveness->prev_req); MC_UNSET_RAW_MEM; XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); @@ -650,18 +653,41 @@ void MC_ddfs(){ if((visited_num = is_visited_pair(current_pair)) != -1){ XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", current_pair->num, visited_num); + + MC_SET_RAW_MEM; + if(dot_output != NULL) + fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, visited_num, initial_state_liveness->prev_req); + MC_UNSET_RAW_MEM; + - }else{ + }else{ while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){ - + + MC_SET_RAW_MEM; + if(dot_output != NULL){ + if(initial_state_liveness->prev_pair != 0 && initial_state_liveness->prev_pair != current_pair->num){ + fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, current_pair->num, initial_state_liveness->prev_req); + xbt_free(initial_state_liveness->prev_req); + } + initial_state_liveness->prev_pair = current_pair->num; + } + MC_UNSET_RAW_MEM; + /* Debug information */ - if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ req_str = MC_request_to_string(req, value); XBT_DEBUG("Execute: %s", req_str); xbt_free(req_str); } + + MC_SET_RAW_MEM; + if(dot_output != NULL){ + initial_state_liveness->prev_req = MC_request_get_dot_output(req, value); + if(current_pair->search_cycle) + fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num); + } + MC_UNSET_RAW_MEM; MC_state_set_executed_request(current_pair->graph_state, req, value); mc_stats->executed_transitions++; @@ -671,15 +697,22 @@ void MC_ddfs(){ /* Wait for requests (schedules processes) */ MC_wait_for_requests(); - + + MC_SET_RAW_MEM; + prop_values = get_atomic_propositions_values(); + MC_UNSET_RAW_MEM; + /* Evaluate enabled transition according to atomic propositions values */ cursor= 0; xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ - res = MC_automaton_evaluate_label(transition_succ->label); + res = MC_automaton_evaluate_label(transition_succ->label, prop_values); if(res == 1){ // enabled transition in automaton + if(new_pair) + MC_replay_liveness(mc_stack_liveness, 1); + MC_SET_RAW_MEM; next_pair = MC_pair_new(); @@ -706,23 +739,24 @@ void MC_ddfs(){ MC_UNSET_RAW_MEM; - MC_ddfs(); + new_pair = 1; - MC_replay_liveness(mc_stack_liveness, 1); + MC_ddfs(); } - - } /* Then, evaluate true transitions (always true, whatever atomic propositions values) */ cursor = 0; xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ - res = MC_automaton_evaluate_label(transition_succ->label); + res = MC_automaton_evaluate_label(transition_succ->label, prop_values); if(res == 2){ // true transition in automaton + + if(new_pair) + MC_replay_liveness(mc_stack_liveness, 1); MC_SET_RAW_MEM; @@ -750,9 +784,10 @@ void MC_ddfs(){ MC_UNSET_RAW_MEM; + new_pair = 1; + MC_ddfs(); - MC_replay_liveness(mc_stack_liveness, 1); } } @@ -802,15 +837,22 @@ void MC_ddfs(){ XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", current_pair->num, visited_num); }else{ + + MC_SET_RAW_MEM; + prop_values = get_atomic_propositions_values(); + MC_UNSET_RAW_MEM; /* Evaluate enabled transition according to atomic propositions values */ cursor= 0; xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ - res = MC_automaton_evaluate_label(transition_succ->label); + res = MC_automaton_evaluate_label(transition_succ->label, prop_values); if(res == 1){ // enabled transition in automaton + if(new_pair) + MC_replay_liveness(mc_stack_liveness, 1); + MC_SET_RAW_MEM; next_pair = MC_pair_new(); @@ -827,26 +869,30 @@ void MC_ddfs(){ if(mc_stats->expanded_pairs%1000 == 0) XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs); + if(dot_output != NULL) + fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", current_pair->num, next_pair->num, ""); + MC_UNSET_RAW_MEM; - MC_ddfs(); + new_pair = 1; - MC_replay_liveness(mc_stack_liveness, 1); + MC_ddfs(); } - - } /* Then, evaluate true transitions (always true, whatever atomic propositions values) */ cursor = 0; xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ - res = MC_automaton_evaluate_label(transition_succ->label); + res = MC_automaton_evaluate_label(transition_succ->label, prop_values); if(res == 2){ // true transition in automaton - + + if(new_pair) + MC_replay_liveness(mc_stack_liveness, 1); + MC_SET_RAW_MEM; next_pair = MC_pair_new(); @@ -863,20 +909,18 @@ void MC_ddfs(){ if(mc_stats->expanded_pairs%1000 == 0) XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs); + if(dot_output != NULL) + fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", current_pair->num, next_pair->num, ""); + MC_UNSET_RAW_MEM; + new_pair = 1; + MC_ddfs(); - MC_replay_liveness(mc_stack_liveness, 1); } } - - if(MC_state_interleave_size(current_pair->graph_state) > 0){ - XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness)); - MC_replay_liveness(mc_stack_liveness, 0); - } - } } @@ -899,9 +943,10 @@ void MC_ddfs(){ MC_SET_RAW_MEM; + xbt_dynar_free(&prop_values); current_pair = xbt_fifo_shift(mc_stack_liveness); current_pair->stack_removed = 1; - if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){ + if(current_pair->search_cycle){ remove_acceptance_pair(current_pair); }else{ if(_sg_mc_visited == 0)