src/mc/explo/udpor/History.cpp

   1 /* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved.          */
   2
   3 /* This program is free software; you can redistribute it and/or modify it
   4  * under the terms of the license (GNU LGPL) which comes with this package. */
   5
   6 #include "src/mc/explo/udpor/History.hpp"
   7 #include "src/mc/explo/udpor/Configuration.hpp"
   8 #include "src/mc/explo/udpor/UnfoldingEvent.hpp"
   9
  10 #include <stack>
  11
  12 namespace simgrid::mc::udpor {
  13
  14 History::Iterator::Iterator(const EventSet& initial_events, optional_configuration config)
  15     : frontier(initial_events), maximal_events(initial_events), configuration(config)
  16 {
  17   // NOTE: Only events in the initial set of events can ever hope to have
  18   // a chance at being a maximal event, since all other events in
  19   // the search are generate by looking at dependencies of these events
  20   // and all subsequent events that are added by the iterator
  21 }
  22
  23 void History::Iterator::increment()
  24 {
  25   if (not frontier.empty()) {
  26     // "Pop" the event at the "front"
  27     const UnfoldingEvent* e = *frontier.begin();
  28     frontier.remove(e);
  29
  30     // If there is a configuration and if the
  31     // event is in it, skip it: the event and
  32     // all of its immediate causes do not need to
  33     // be searched since the configuration contains
  34     // them (configuration invariant)
  35     if (configuration.has_value() && configuration->get().contains(e)) {
  36       return;
  37     }
  38
  39     // Mark this event as seen
  40     current_history.insert(e);
  41
  42     // Perform the expansion with all viable expansions
  43     EventSet candidates = e->get_immediate_causes();
  44
  45     maximal_events.subtract(candidates);
  46
  47     candidates.subtract(current_history);
  48     frontier.form_union(candidates);
  49   }
  50 }
  51
  52 const UnfoldingEvent* const& History::Iterator::dereference() const
  53 {
  54   return *frontier.begin();
  55 }
  56
  57 bool History::Iterator::equal(const Iterator& other) const
  58 {
  59   // If what the iterator sees next is the same, we consider them
  60   // to be the same iterator. This way, once the iterator has completed
  61   // its search, it will be "equal" to an iterator searching nothing
  62   return this->frontier == other.frontier;
  63 }
  64
  65 EventSet History::get_all_events() const
  66 {
  67   auto first      = this->begin();
  68   const auto last = this->end();
  69
  70   for (; first != last; ++first)
  71     ;
  72
  73   return first.current_history;
  74 }
  75
  76 EventSet History::get_all_maximal_events() const
  77 {
  78   auto first      = this->begin();
  79   const auto last = this->end();
  80
  81   for (; first != last; ++first)
  82     ;
  83
  84   return first.maximal_events;
  85 }
  86
  87 bool History::contains(const UnfoldingEvent* e) const
  88 {
  89   return std::any_of(this->begin(), this->end(), [=](const UnfoldingEvent* e_hist) { return e == e_hist; });
  90 }
  91
  92 EventSet History::get_event_diff_with(const Configuration& config) const
  93 {
  94   auto wrapped_config = std::optional<std::reference_wrapper<const Configuration>>{config};
  95   auto first          = Iterator(events_, wrapped_config);
  96   const auto last     = this->end();
  97
  98   for (; first != last; ++first)
  99     ;
 100
 101   return first.current_history;
 102 }
 103
 104 } // namespace simgrid::mc::udpor