+ if((visited_num = is_visited_pair(reached_pair, current_pair->num, current_pair->automaton_state, current_pair->atomic_propositions)) != -1){
+
+ 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{
+
+ 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++;
+
+ /* Answer the request */
+ SIMIX_simcall_pre(req, value);
+
+ /* Wait for requests (schedules processes) */
+ MC_wait_for_requests();
+
+ MC_SET_RAW_MEM;
+ prop_values = get_atomic_propositions_values();
+ MC_UNSET_RAW_MEM;
+
+ int new_pair = 0;
+
+ /* 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, 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();
+ next_pair->graph_state = MC_state_new();
+ next_pair->automaton_state = transition_succ->dst;
+ next_pair->atomic_propositions = get_atomic_propositions_values();
+
+ /* 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)){
+ MC_state_interleave_process(next_pair->graph_state, process);
+ }
+ }
+
+ next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
+
+ if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
+ next_pair->search_cycle = 1;
+
+ xbt_fifo_unshift(mc_stack_liveness, next_pair);
+
+ if(mc_stats->expanded_pairs%1000000 == 0)
+ XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
+
+ MC_UNSET_RAW_MEM;
+
+ new_pair = 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){