- 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, 1);
-
- MC_SET_MC_HEAP;
-
- 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, next_pair);
-
- if (mc_stats->expanded_pairs % 1000000 == 0)
- XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
-
- MC_SET_STD_HEAP;
-
- new_pair = 1;
-
- MC_modelcheck_liveness();
-
- }
-
- }
-
- /* 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,
- prop_values);
-
- if (res == 2) { // true transition in automaton
-
- if (new_pair)
- MC_replay_liveness(mc_stack, 1);
-
- MC_SET_MC_HEAP;
-
+ XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num);
+ MC_SET_MC_HEAP;
+ current_pair->requests = 0;
+ MC_SET_STD_HEAP;
+ goto backtracking;
+
+ }else{
+
+ 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);
+ 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 */