+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;
+
+ auto visited_pairs = simgrid::xbt::range<simgrid::mc::VisitedPair*>(simgrid::mc::visited_pairs);
+
+ auto range = std::equal_range(visited_pairs.begin(), visited_pairs.end(),
+ new_visited_pair, simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
+
+ for (auto i = range.first; i != range.second; ++i) {
+ simgrid::mc::VisitedPair* pair_test = *i;
+ std::size_t cursor = i - visited_pairs.begin();
+ 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(simgrid::mc::visited_pairs, cursor, &pair_test);
+ xbt_dynar_insert_at(simgrid::mc::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;
+ }
+ }
+ }
+ }
+
+ xbt_dynar_insert_at(simgrid::mc::visited_pairs, range.first - visited_pairs.begin(), &new_visited_pair);
+
+ if ((ssize_t) visited_pairs.size() > _sg_mc_visited) {
+ int min2 = mc_stats->expanded_pairs;
+ unsigned int index2 = 0;
+ for (std::size_t i = 0; i != (std::size_t) visited_pairs.size(); ++i) {
+ simgrid::mc::VisitedPair* pair_test = visited_pairs[i];
+ if (!mc_model_checker->is_important_snapshot(*pair_test->graph_state->system_state)
+ && pair_test->num < min2) {
+ index2 = i;
+ min2 = pair_test->num;
+ }
+ }
+ simgrid::mc::VisitedPair* pair_test = nullptr;
+ xbt_dynar_remove_at(simgrid::mc::visited_pairs, index2, &pair_test);
+ pair_test->visited_removed = 1;
+ if (!pair_test->acceptance_pair || pair_test->acceptance_removed)
+ delete pair_test;
+ }
+
+ return -1;
+}
+