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 void maximal_subsets_iterator::increment()
  10 {
  11   if (current_maximal_set = std::nullopt) {
  12     return;
  13   }
  14
  15   const auto next_event_ref = continue_traversal_of_maximal_events_tree();
  16   if (next_event_ref == topological_ordering.end()) {
  17     current_maximal_set = std::nullopt;
  18     return;
  19   }
  20
  21   // We found some other event `e'` which is not in causally related with anything
  22   // that currently exists in `current_maximal_set`. Add it in
  23   add_element_to_current_maximal_set(*next_event_ref);
  24   backtrack_points.push(next_event_ref);
  25 }
  26
  27 maximal_subsets_iterator::topological_order_position
  28 maximal_subsets_iterator::continue_traversal_of_maximal_events_tree()
  29 {
  30   while (not backtrack_points.empty()) {
  31     // This is an iterator which points to the latest event `e` that
  32     // was added to what is currently the maximal set
  33     const auto latest_event_ref = backtrack_points.top();
  34
  35     // Look for the next event to test with what we currently
  36     // have based on the conflicts we've already kept track of.
  37     //
  38     // NOTE: We only need to search FROM `e` and not
  39     // from the beginning of the topological sort. The fact that the
  40     // set is topologically ordered ensures that removing `e`
  41     // will not change whether or not to now allow someone before `e`
  42     // in the ordering (otherwise, they would have to be in `e`'s history
  43     // and therefore would come after `e`)
  44     auto next_event_ref = bookkeeper.find_next_candidate_event(latest_event_ref, topological_ordering.end());
  45
  46     // If we found some event, we can stop
  47     if (next_event_ref != topological_ordering.end() and should_consider_event(*next_event_ref)) {
  48       return next_event_ref;
  49     } else {
  50       // Otherwise, if we can't find another event to add after `e` that
  51       // we need to consider, we retry after first removing the latest event.
  52       // This effectively tests "check now with all combinations that3
  53       // exclude the latest event".
  54       //
  55       // Note: it is important to remove the element FIRST before performing
  56       // the second search, as removal may enable dependencies of `e` to be selected
  57       remove_element_from_current_maximal_set(*latest_event_ref);
  58       backtrack_points.pop();
  59
  60       // We begin the search AFTER the event we popped: we only want
  61       // to consider those events that could be added AFTER `e` and
  62       // not `e` itself again
  63       next_event_ref = bookkeeper.find_next_candidate_event(latest_event_ref + 1, topological_ordering.end());
  64
  65       // If we finally found some event AFTER removal, we can stop
  66       if (next_event_ref != topological_ordering.end() and should_consider_event(*next_event_ref)) {
  67         return next_event_ref;
  68       }
  69     }
  70   }
  71   return topological_ordering.end();
  72 }
  73
  74 bool maximal_subsets_iterator::should_consider_event(const UnfoldingEvent* e) const
  75 {
  76   if (filter_function.has_value()) {
  77     return filter_function.value()(e);
  78   }
  79   return true; // If nobody specified a filter, we default to considering the event
  80 }
  81
  82 bool maximal_subsets_iterator::bookkeeper::is_candidate_event(const UnfoldingEvent* e) const
  83 {
  84   if (const auto e_count = event_counts.find(e); e_count != event_counts.end()) {
  85     return e_count->second == 0;
  86   }
  87   return true;
  88 }
  89
  90 void maximal_subsets_iterator::add_element_to_current_maximal_set(const UnfoldingEvent* e)
  91 {
  92   xbt_assert(current_maximal_set.has_value(), "Attempting to add an event to the maximal set "
  93                                               "when iteration has completed. This indicates that "
  94                                               "the termination condition for the iterator is broken");
  95   current_maximal_set.value().insert(e);
  96   bookkeeper.mark_included_in_maximal_set(e);
  97 }
  98
  99 void maximal_subsets_iterator::remove_element_from_current_maximal_set(const UnfoldingEvent* e)
 100 {
 101   xbt_assert(current_maximal_set.has_value(), "Attempting to remove an event to the maximal set "
 102                                               "when iteration has completed. This indicates that "
 103                                               "the termination condition for the iterator is broken");
 104   current_maximal_set.value().remove(e);
 105   bookkeeper.mark_removed_from_maximal_set(e);
 106 }
 107
 108 maximal_subsets_iterator::topological_order_position
 109 maximal_subsets_iterator::bookkeeper::find_next_candidate_event(topological_order_position first,
 110                                                                 topological_order_position last) const
 111 {
 112   return std::find_if(first, last, [&](const UnfoldingEvent* e) { return is_candidate_event(e); });
 113 }
 114
 115 void maximal_subsets_iterator::bookkeeper::mark_included_in_maximal_set(const UnfoldingEvent* e)
 116 {
 117   const auto e_history = e->get_history();
 118   for (const auto e_hist : e_history) {
 119     event_counts[e_hist]++;
 120   }
 121 }
 122
 123 void maximal_subsets_iterator::bookkeeper::mark_removed_from_maximal_set(const UnfoldingEvent* e)
 124 {
 125   const auto e_history = e->get_history();
 126   for (const auto e_hist : e_history) {
 127     xbt_assert(event_counts.find(e_hist) != event_counts.end(),
 128                "Invariant Violation: Attempted to remove an event which was not previously added");
 129     xbt_assert(event_counts[e_hist] > 0, "Invariant Violation: An event `e` had a count of `0` at this point "
 130                                          "of the bookkeeping, which means that it is a candidate maximal event. "
 131                                          "Yet some event that `e'` which contains `e` in its history was removed "
 132                                          "first. This incidates that the topological sorting of events of the "
 133                                          "configuration has failed and should be investigated first");
 134     event_counts[e_hist]--;
 135   }
 136 }
 137
 138 } // namespace simgrid::mc::udpor