- MC_LOG_REQUEST(mc_liveness, req, value);
-
- MC_SET_MC_HEAP;
- if (dot_output != NULL) {
- 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);
- }
- MC_SET_STD_HEAP;
-
- MC_state_set_executed_request(current_pair->graph_state, req, value);
- mc_stats->executed_transitions++;
-
- /* Answer the request */
- SIMIX_simcall_handle(req, value);
-
- /* Wait for requests (schedules processes) */
- MC_wait_for_requests();
-
- MC_SET_MC_HEAP;
- prop_values = get_atomic_propositions_values();
- MC_SET_STD_HEAP;
-
- 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;
-
+ 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 */