+ req = MC_state_get_request(current_pair->graph_state, &value);
+
+ if (dot_output != NULL) {
+ MC_SET_MC_HEAP;
+ if (initial_global_state->prev_pair != 0 && initial_global_state->prev_pair != current_pair->num) {
+ fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, current_pair->num, initial_global_state->prev_req);
+ xbt_free(initial_global_state->prev_req);
+ }
+ initial_global_state->prev_pair = current_pair->num;
+ initial_global_state->prev_req = MC_request_get_dot_output(req, value);
+ if (current_pair->search_cycle)
+ fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
+ fflush(dot_output);
+ MC_SET_STD_HEAP;
+ }
+
+ char* req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX);
+ XBT_DEBUG("Execute: %s", req_str);
+ xbt_free(req_str);
+
+ /* Set request as executed */
+ MC_state_set_executed_request(current_pair->graph_state, req, value);
+
+ /* Update mc_stats */
+ mc_stats->executed_transitions++;
+ if(current_pair->exploration_started == 0)
+ mc_stats->visited_pairs++;
+
+ /* Answer the request */
+ MC_simcall_handle(req, value);
+
+ /* Wait for requests (schedules processes) */
+ MC_wait_for_requests();
+
+ MC_SET_MC_HEAP;
+
+ current_pair->requests--;
+ current_pair->exploration_started = 1;
+
+ /* Get values of atomic propositions (variables used in the property formula) */
+ prop_values = get_atomic_propositions_values();
+
+ /* Evaluate enabled/true transitions in automaton according to atomic propositions values and create new pairs */
+ cursor = xbt_dynar_length(current_pair->automaton_state->out) - 1;
+ while (cursor >= 0) {
+ transition_succ = (xbt_automaton_transition_t)xbt_dynar_get_as(current_pair->automaton_state->out, cursor, xbt_automaton_transition_t);
+ res = MC_automaton_evaluate_label(transition_succ->label, prop_values);
+ if (res == 1 || res == 2) { /* 1 = True transition (always enabled), 2 = enabled transition according to atomic prop values */
+ 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();
+ next_pair->depth = current_pair->depth + 1;
+ /* Get enabled processes and insert them in the interleave set of the next graph_state */
+ MC_EACH_SIMIX_PROCESS(process,
+ if (MC_process_is_enabled(process)) {
+ MC_state_interleave_process(next_pair->graph_state, process);