1 /* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */
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. */
6 #include "src/mc/explo/udpor/History.hpp"
7 #include "src/mc/explo/udpor/Configuration.hpp"
8 #include "src/mc/explo/udpor/UnfoldingEvent.hpp"
12 namespace simgrid::mc::udpor {
14 History::Iterator::Iterator(const EventSet& initial_events, optional_configuration config)
15 : frontier(initial_events), maximal_events(initial_events), configuration(config)
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
23 void History::Iterator::increment()
25 if (not frontier.empty()) {
26 // "Pop" the event at the "front"
27 const UnfoldingEvent* e = *frontier.begin();
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)) {
39 // Mark this event as seen
40 current_history.insert(e);
42 // Perform the expansion with all viable expansions
43 EventSet candidates = e->get_immediate_causes();
45 maximal_events.subtract(candidates);
47 candidates.subtract(current_history);
48 frontier.form_union(candidates);
52 const UnfoldingEvent* const& History::Iterator::dereference() const
54 return *frontier.begin();
57 bool History::Iterator::equal(const Iterator& other) const
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;
65 EventSet History::get_all_events() const
67 auto first = this->begin();
68 const auto last = this->end();
70 for (; first != last; ++first)
73 return first.current_history;
76 EventSet History::get_all_maximal_events() const
78 auto first = this->begin();
79 const auto last = this->end();
81 for (; first != last; ++first)
84 return first.maximal_events;
87 bool History::contains(const UnfoldingEvent* e) const
89 return std::any_of(this->begin(), this->end(), [=](const UnfoldingEvent* e_hist) { return e == e_hist; });
92 EventSet History::get_event_diff_with(const Configuration& config) const
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();
98 for (; first != last; ++first)
101 return first.current_history;
104 } // namespace simgrid::mc::udpor