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){
+ XBT_DEBUG("Compare with state %d", pair_test->num);
if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
if(raw_mem_set)
MC_SET_RAW_MEM;
break;
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){
+ XBT_DEBUG("Compare with state %d", pair_test->num);
if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
if(raw_mem_set)
MC_SET_RAW_MEM;
break;
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){
+ XBT_DEBUG("Compare with state %d", pair_test->num);
if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
if(raw_mem_set)
MC_SET_RAW_MEM;
size_t bytes_used_test;
int nb_processes_test;
int same_processes_and_bytes_not_found = 1;
- int result;
while(start <= end && same_processes_and_bytes_not_found){
cursor = (start + end) / 2;
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){
if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
+ if(pair_test->other_num == -1)
+ pair->other_num = pair_test->num;
+ else
+ pair->other_num = pair_test->other_num;
+ if(dot_output == NULL)
+ XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
+ else
+ XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
xbt_dynar_remove_at(visited_pairs, cursor, NULL);
xbt_dynar_insert_at(visited_pairs, cursor, &pair);
pair_test->visited_removed = 1;
- result = pair_test->num;
if(pair_test->stack_removed && pair_test->visited_removed){
if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
if(pair_test->acceptance_removed){
MC_SET_RAW_MEM;
else
MC_UNSET_RAW_MEM;
- return result;
+ return pair->other_num;
}
}
}
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){
if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
+ if(pair_test->other_num == -1)
+ pair->other_num = pair_test->num;
+ else
+ pair->other_num = pair_test->other_num;
+ if(dot_output == NULL)
+ XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
+ else
+ XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
xbt_dynar_remove_at(visited_pairs, previous_cursor, NULL);
xbt_dynar_insert_at(visited_pairs, previous_cursor, &pair);
pair_test->visited_removed = 1;
- result = pair_test->num;
if(pair_test->stack_removed && pair_test->visited_removed){
if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
if(pair_test->acceptance_removed){
MC_SET_RAW_MEM;
else
MC_UNSET_RAW_MEM;
- return result;
+ return pair->other_num;
}
}
}
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){
if(snapshot_compare(pair->graph_state->system_state, pair_test->graph_state->system_state) == 0){
+ if(pair_test->other_num == -1)
+ pair->other_num = pair_test->num;
+ else
+ pair->other_num = pair_test->other_num;
+ if(dot_output == NULL)
+ XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
+ else
+ XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
xbt_dynar_remove_at(visited_pairs, next_cursor, NULL);
xbt_dynar_insert_at(visited_pairs, next_cursor, &pair);
pair_test->visited_removed = 1;
- result = pair_test->num;
if(pair_test->stack_removed && pair_test->visited_removed){
if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
if(pair_test->acceptance_removed){
MC_SET_RAW_MEM;
else
MC_UNSET_RAW_MEM;
- return result;
+ return pair->other_num;
}
}
}
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;
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_value = NULL;
+ xbt_dynar_t prop_values = NULL;
if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
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("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
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++;
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();
MC_UNSET_RAW_MEM;
- new_pair = 1;
-
MC_ddfs();
}
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;
MC_UNSET_RAW_MEM;
- new_pair = 1;
-
MC_ddfs();
}
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();
if(mc_stats->expanded_pairs%1000 == 0)
XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
- MC_UNSET_RAW_MEM;
+ if(dot_output != NULL)
+ fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", current_pair->num, next_pair->num, "");
- new_pair = 1;
+ MC_UNSET_RAW_MEM;
MC_ddfs();
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();
if(mc_stats->expanded_pairs%1000 == 0)
XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
- MC_UNSET_RAW_MEM;
+ if(dot_output != NULL)
+ fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", current_pair->num, next_pair->num, "");
- new_pair = 1;
+ MC_UNSET_RAW_MEM;
MC_ddfs();
MC_SET_RAW_MEM;
- if(prop_values != NULL)
- xbt_dynar_free(&prop_values);
+ 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)
else if(current_pair->visited_removed)
MC_pair_delete(current_pair);
}
+
MC_UNSET_RAW_MEM;
}