src/mc/explo/udpor/maximal_subsets_iterator.cpp

   1 #include "src/mc/explo/udpor/maximal_subsets_iterator.hpp"
   2 #include "src/mc/explo/udpor/UnfoldingEvent.hpp"
   3 #include "xbt/asserts.h"
   4
   5 #include <algorithm>
   6
   7 namespace simgrid::mc::udpor {
   8
   9 maximal_subsets_iterator::maximal_subsets_iterator(const EventSet& events, std::optional<node_filter_function> filter,
  10                                                    std::optional<size_t> maximum_subset_size)
  11     : maximum_subset_size(maximum_subset_size), current_maximal_set({EventSet()})
  12 {
  13   const auto candidate_ordering = events.get_topological_ordering_of_reverse_graph();
  14   if (filter.has_value()) {
  15     // Only store the events in the ordering that "matter" to us
  16     std::copy_if(std::move_iterator(candidate_ordering.begin()), std::move_iterator(candidate_ordering.end()),
  17                  std::back_inserter(topological_ordering), filter.value());
  18   } else {
  19     topological_ordering = std::move(candidate_ordering);
  20   }
  21 }
  22
  23 void maximal_subsets_iterator::increment()
  24 {
  25   // Termination condition
  26   if (current_maximal_set == std::nullopt) {
  27     return;
  28   }
  29
  30   // Stop immediately if there's nothing to search
  31   if (topological_ordering.empty()) {
  32     current_maximal_set = std::nullopt;
  33     return;
  34   }
  35
  36   const auto next_event_ref = [&]() {
  37     if (!has_started_searching) {
  38       has_started_searching = true;
  39       return bookkeeper.find_next_candidate_event(topological_ordering.begin(), topological_ordering.end());
  40     } else {
  41       return continue_traversal_of_maximal_events_tree();
  42     }
  43   }();
  44
  45   // Out of events: we've finished
  46   if (next_event_ref == topological_ordering.end()) {
  47     current_maximal_set = std::nullopt;
  48     return;
  49   }
  50
  51   // We found some other event `e'` which is not in causally related with anything
  52   // that currently exists in `current_maximal_set`, so add it in
  53   add_element_to_current_maximal_set(*next_event_ref);
  54   backtrack_points.push(next_event_ref);
  55 }
  56
  57 maximal_subsets_iterator::topological_order_position
  58 maximal_subsets_iterator::continue_traversal_of_maximal_events_tree()
  59 {
  60   // Nothing needs to be done if there isn't anyone to search for...
  61   if (backtrack_points.empty()) {
  62     return topological_ordering.end();
  63   }
  64
  65   xbt_assert(current_maximal_set.has_value(), "Traversal continued even after the termination condition "
  66                                               "was met. Please verify that the termination condition "
  67                                               "of the iterator has not been modified");
  68
  69   // 1. First, check if we can keep expanding from the
  70   // maximal set that we currently have
  71   if (can_grow_maximal_set()) {
  72     // This is an iterator which points to the latest event `e` that
  73     // was added to what is currently the maximal set
  74     const auto latest_event_ref = backtrack_points.top();
  75
  76     // Look for the next event to test with what we currently
  77     // have based on the conflicts we've already kept track of.
  78     //
  79     // NOTE: We only need to search FROM `e` and not
  80     // from the beginning of the topological sort. The fact that the
  81     // set is topologically ordered ensures that removing `e`
  82     // will not change whether or not to now allow someone before `e`
  83     // in the ordering (otherwise, they would have to be in `e`'s history
  84     // and therefore would come after `e`)
  85     const auto next_event_ref = bookkeeper.find_next_candidate_event(latest_event_ref, topological_ordering.end());
  86
  87     // If we can expand from what we currently have, we can stop
  88     if (next_event_ref != topological_ordering.end()) {
  89       return next_event_ref;
  90     }
  91   }
  92
  93   // Otherwise, we backtrack: we repeatedly pop off events that we know we
  94   // are finished with
  95   while (not backtrack_points.empty()) {
  96     // Note: it is important to remove the element FIRST before performing
  97     // the search, as removal may enable dependencies of `e` to be selected
  98     const auto latest_event_ref = backtrack_points.top();
  99     remove_element_from_current_maximal_set(*latest_event_ref);
 100     backtrack_points.pop();
 101
 102     // We begin the search AFTER the event we popped: we only want
 103     // to consider those events that could be added AFTER `e` and
 104     // not `e` itself again
 105     const auto next_event_ref = bookkeeper.find_next_candidate_event(latest_event_ref + 1, topological_ordering.end());
 106     if (next_event_ref != topological_ordering.end()) {
 107       return next_event_ref;
 108     }
 109   }
 110   return topological_ordering.end();
 111 }
 112
 113 bool maximal_subsets_iterator::bookkeeper::is_candidate_event(const UnfoldingEvent* e) const
 114 {
 115   if (const auto e_count = event_counts.find(e); e_count != event_counts.end()) {
 116     return e_count->second == 0;
 117   }
 118   return true;
 119 }
 120
 121 void maximal_subsets_iterator::add_element_to_current_maximal_set(const UnfoldingEvent* e)
 122 {
 123   xbt_assert(can_grow_maximal_set(), "Attempting to add an event to the maximal set "
 124                                      "when doing so would increase the size past the "
 125                                      "prescribed limit. This indicates that detecting when "
 126                                      "to stop growing the maximal set when continuing the "
 127                                      "search is broken");
 128   xbt_assert(current_maximal_set.has_value(), "Attempting to add an event to the maximal set "
 129                                               "when iteration has completed. This indicates that "
 130                                               "the termination condition for the iterator is broken");
 131   current_maximal_set.value().insert(e);
 132   bookkeeper.mark_included_in_maximal_set(e);
 133 }
 134
 135 void maximal_subsets_iterator::remove_element_from_current_maximal_set(const UnfoldingEvent* e)
 136 {
 137   xbt_assert(current_maximal_set.has_value(), "Attempting to remove an event to the maximal set "
 138                                               "when iteration has completed. This indicates that "
 139                                               "the termination condition for the iterator is broken");
 140   current_maximal_set.value().remove(e);
 141   bookkeeper.mark_removed_from_maximal_set(e);
 142 }
 143
 144 bool maximal_subsets_iterator::can_grow_maximal_set() const
 145 {
 146   if (not current_maximal_set.has_value()) {
 147     return true;
 148   }
 149   if (maximum_subset_size.has_value()) {
 150     return current_maximal_set.value().size() < maximum_subset_size.value();
 151   }
 152   return true;
 153 }
 154
 155 maximal_subsets_iterator::topological_order_position
 156 maximal_subsets_iterator::bookkeeper::find_next_candidate_event(topological_order_position first,
 157                                                                 topological_order_position last) const
 158 {
 159   return std::find_if(first, last, [&](const UnfoldingEvent* e) { return is_candidate_event(e); });
 160 }
 161
 162 void maximal_subsets_iterator::bookkeeper::mark_included_in_maximal_set(const UnfoldingEvent* e)
 163 {
 164   const auto e_history = e->get_history();
 165   for (const auto e_hist : e_history) {
 166     event_counts[e_hist]++;
 167   }
 168 }
 169
 170 void maximal_subsets_iterator::bookkeeper::mark_removed_from_maximal_set(const UnfoldingEvent* e)
 171 {
 172   const auto e_history = e->get_history();
 173   for (const auto e_hist : e_history) {
 174     xbt_assert(event_counts.find(e_hist) != event_counts.end(),
 175                "Invariant Violation: Attempted to remove an event which was not previously added");
 176     xbt_assert(event_counts[e_hist] > 0, "Invariant Violation: An event `e` had a count of `0` at this point "
 177                                          "of the bookkeeping, which means that it is a candidate maximal event. "
 178                                          "Yet some event that `e'` which contains `e` in its history was removed "
 179                                          "first. This incidates that the topological sorting of events of the "
 180                                          "configuration has failed and should be investigated first");
 181     event_counts[e_hist]--;
 182   }
 183 }
 184
 185 } // namespace simgrid::mc::udpor