+static void MC_replay_liveness(xbt_fifo_t stack)
+{
+ xbt_fifo_item_t item;
+ simgrid::mc::Pair* pair = nullptr;
+ mc_state_t state = nullptr;
+ smx_simcall_t req = nullptr, saved_req = NULL;
+ int value, depth = 1;
+ char *req_str;
+
+ XBT_DEBUG("**** Begin Replay ****");
+
+ /* Intermediate backtracking */
+ if(_sg_mc_checkpoint > 0) {
+ item = xbt_fifo_get_first_item(stack);
+ pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
+ if(pair->graph_state->system_state){
+ simgrid::mc::restore_snapshot(pair->graph_state->system_state);
+ return;
+ }
+ }
+
+ /* Restore the initial state */
+ simgrid::mc::restore_snapshot(initial_global_state->snapshot);
+
+ /* Traverse the stack from the initial state and re-execute the transitions */
+ for (item = xbt_fifo_get_last_item(stack);
+ item != xbt_fifo_get_first_item(stack);
+ item = xbt_fifo_get_prev_item(item)) {
+
+ pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
+
+ state = (mc_state_t) pair->graph_state;
+
+ if (pair->exploration_started) {
+
+ saved_req = MC_state_get_executed_request(state, &value);
+
+ if (saved_req != nullptr) {
+ /* because we got a copy of the executed request, we have to fetch the
+ real one, pointed by the request field of the issuer process */
+ const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
+ req = &issuer->simcall;
+
+ /* Debug information */
+ if (XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)) {
+ req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
+ XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
+ xbt_free(req_str);
+ }
+
+ }
+
+ simgrid::mc::handle_simcall(req, value);
+ mc_model_checker->wait_for_requests();
+ }
+
+ /* Update statistics */
+ mc_stats->visited_pairs++;
+ mc_stats->executed_transitions++;
+
+ depth++;
+
+ }
+
+ XBT_DEBUG("**** End Replay ****");
+}
+
+/**
+ * \brief Checks whether a given pair has already been visited by the algorithm.
+ */
+static
+int is_visited_pair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair)
+{
+ if (_sg_mc_visited == 0)
+ return -1;
+
+ simgrid::mc::VisitedPair* new_visited_pair = nullptr;
+ if (visited_pair == nullptr)
+ new_visited_pair = new simgrid::mc::VisitedPair(
+ pair->num, pair->automaton_state, pair->atomic_propositions.get(),
+ pair->graph_state);
+ else
+ new_visited_pair = visited_pair;
+
+ if (xbt_dynar_is_empty(visited_pairs)) {
+ xbt_dynar_push(visited_pairs, &new_visited_pair);
+ return -1;
+ }
+
+ int min = -1, max = -1, index;
+ //int res;
+ simgrid::mc::VisitedPair* pair_test;
+ int cursor;
+
+ index = get_search_interval(
+ (simgrid::mc::VisitedPair**) xbt_dynar_get_ptr(visited_pairs, 0),
+ xbt_dynar_length(visited_pairs), new_visited_pair, &min, &max);
+
+ if (min != -1 && max != -1) { // Visited pair with same number of processes and same heap bytes used exists
+ cursor = min;
+ while (cursor <= max) {
+ pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(visited_pairs, cursor, simgrid::mc::VisitedPair*);
+ if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
+ if (xbt_automaton_propositional_symbols_compare_value(
+ pair_test->atomic_propositions.get(),
+ new_visited_pair->atomic_propositions.get()) == 0) {
+ if (snapshot_compare(pair_test, new_visited_pair) == 0) {
+ if (pair_test->other_num == -1)
+ new_visited_pair->other_num = pair_test->num;
+ else
+ new_visited_pair->other_num = pair_test->other_num;
+ if (dot_output == nullptr)
+ XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
+ else
+ XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_visited_pair->num, pair_test->num, new_visited_pair->other_num);
+ xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
+ xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
+ pair_test->visited_removed = 1;
+ if (!pair_test->acceptance_pair
+ || pair_test->acceptance_removed == 1)
+ delete pair_test;
+ return new_visited_pair->other_num;
+ }
+ }
+ }
+ cursor++;
+ }
+ xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
+ } else {
+ xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
+ }
+
+ if ((ssize_t) xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
+ int min2 = mc_stats->expanded_pairs;
+ unsigned int cursor2 = 0;
+ unsigned int index2 = 0;
+ xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
+ if (!mc_model_checker->is_important_snapshot(*pair_test->graph_state->system_state)
+ && pair_test->num < min2) {
+ index2 = cursor2;
+ min2 = pair_test->num;
+ }
+ }
+ xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
+ pair_test->visited_removed = 1;
+ if (!pair_test->acceptance_pair || pair_test->acceptance_removed)
+ delete pair_test;
+ }
+ return -1;
+}
+