namespace simgrid::mc::udpor {
-History::Iterator& History::Iterator::operator++()
+History::Iterator::Iterator(const EventSet& initial_events, optional_configuration config)
+ : frontier(initial_events), maximal_events(initial_events), configuration(config)
+{
+ // NOTE: Only events in the initial set of events can ever hope to have
+ // a chance at being a maximal event, since all other events in
+ // the search are generate by looking at dependencies of these events
+ // and all subsequent events that are added by the iterator
+}
+
+void History::Iterator::increment()
{
if (not frontier.empty()) {
// "Pop" the event at the "front"
- UnfoldingEvent* e = *frontier.begin();
+ const UnfoldingEvent* e = *frontier.begin();
frontier.remove(e);
- // If we've seen this event before, skip it
-
// If there is a configuration and if the
// event is in it, skip it: the event and
// all of its immediate causes do not need to
// be searched since the configuration contains
// them (configuration invariant)
if (configuration.has_value() && configuration->get().contains(e)) {
- return *this;
+ return;
}
// Mark this event as seen
// Perform the expansion with all viable expansions
EventSet candidates = e->get_immediate_causes();
- candidates.subtract(current_history);
- frontier.form_union(std::move(candidates));
+ maximal_events.subtract(candidates);
+
+ candidates.subtract(current_history);
+ frontier.form_union(candidates);
}
- return *this;
+}
+
+const UnfoldingEvent* const& History::Iterator::dereference() const
+{
+ return *frontier.begin();
+}
+
+bool History::Iterator::equal(const Iterator& other) const
+{
+ // If what the iterator sees next is the same, we consider them
+ // to be the same iterator. This way, once the iterator has completed
+ // its search, it will be "equal" to an iterator searching nothing
+ return this->frontier == other.frontier;
}
EventSet History::get_all_events() const
return first.current_history;
}
-bool History::contains(UnfoldingEvent* e) const
+EventSet History::get_all_maximal_events() const
{
- return std::any_of(this->begin(), this->end(), [=](UnfoldingEvent* e_hist) { return e == e_hist; });
+ auto first = this->begin();
+ const auto last = this->end();
+
+ for (; first != last; ++first)
+ ;
+
+ return first.maximal_events;
+}
+
+bool History::contains(const UnfoldingEvent* e) const
+{
+ return std::any_of(this->begin(), this->end(), [=](const UnfoldingEvent* e_hist) { return e == e_hist; });
}
EventSet History::get_event_diff_with(const Configuration& config) const
{
- // auto wrapped_config = std::optional<std::reference_wrapper<Configuration>>(config);
- // auto first = Iterator(events_, wrapped_config);
- // const auto last = this->end();
+ auto wrapped_config = std::optional<std::reference_wrapper<const Configuration>>{config};
+ auto first = Iterator(events_, wrapped_config);
+ const auto last = this->end();
- // for (; first != last; ++first)
- // ;
+ for (; first != last; ++first)
+ ;
- // return first.current_history;
- // TODO: Implement this
- return EventSet();
+ return first.current_history;
}
} // namespace simgrid::mc::udpor
