#include "src/mc/explo/udpor/EventSet.hpp"
#include "src/mc/explo/udpor/udpor_forward.hpp"
+#include <boost/iterator/iterator_facade.hpp>
#include <functional>
+#include <initializer_list>
#include <optional>
namespace simgrid::mc::udpor {
History& operator=(History const&) = default;
History(History&&) = default;
- explicit History(UnfoldingEvent* e) : events_({e}) {}
+ explicit History(const UnfoldingEvent* e) : events_({e}) {}
explicit History(EventSet event_set = EventSet()) : events_(std::move(event_set)) {}
+ explicit History(std::initializer_list<const UnfoldingEvent*> list) : events_(std::move(list)) {}
auto begin() const { return Iterator(events_); }
auto end() const { return Iterator(EventSet()); }
* @param e the event to check
* @returns whether or not `e` is contained in the collection
*/
- bool contains(UnfoldingEvent* e) const;
+ bool contains(const UnfoldingEvent* e) const;
/**
* @brief Computes all events in the history described by this instance
* dependency graph for all events in this history
*/
EventSet get_all_events() const;
+
+ /**
+ * @brief Computes all events in the history described by this instance
+ * which are maximal (intuitively, those events which cause no others
+ * or are the "most recent")
+ */
+ EventSet get_all_maximal_events() const;
+
+ /**
+ * @brief Computes the set of events that are not contained
+ * in the given configuration
+ *
+ * A configuration is a causally-closed, conflict-free set
+ * of events. Thus, you can determine which events lie outside
+ * of a configuration during the search more efficiently: the moment
+ * you discover an event contained in the configuration, you
+ * do not need to search that event or any of its ancestors as
+ * they will all be contained in the configuration
+ */
EventSet get_event_diff_with(const Configuration& config) const;
private:
/**
* @brief An iterator which traverses the history of a set of events
*/
- struct Iterator {
+ struct Iterator : boost::iterator_facade<Iterator, const UnfoldingEvent* const, boost::forward_traversal_tag> {
+ public:
+ using optional_configuration = std::optional<std::reference_wrapper<const Configuration>>;
+ Iterator(const EventSet& initial_events, optional_configuration config = std::nullopt);
+
private:
+ /// @brief Points in the graph from where to continue the search
EventSet frontier;
+
+ /// @brief What the iterator currently believes to be the
+ /// entire history of the events in the graph it traverses
EventSet current_history = EventSet();
- std::optional<std::reference_wrapper<Configuration>> configuration;
- friend History;
+ /// @brief What the iterator currently believes
+ // to be the set of maximal events
+ EventSet maximal_events;
+ optional_configuration configuration;
- public:
- Iterator(const EventSet& initial_events, std::optional<std::reference_wrapper<Configuration>> config = std::nullopt)
- : frontier(initial_events), configuration(config)
- {
- }
-
- Iterator& operator++();
- auto operator->() { return frontier.begin().operator->(); }
- auto operator*() const { return *frontier.begin(); }
-
- // 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
- bool operator==(const Iterator& other) { return this->frontier == other.frontier; }
- bool operator!=(const Iterator& other) { return not(this->operator==(other)); }
-
- using iterator_category = std::forward_iterator_tag;
- using difference_type = int; // # of steps between
- using value_type = UnfoldingEvent*;
- using pointer = value_type*;
- using reference = value_type&;
+ // boost::iterator_facade<...> interface to implement
+ void increment();
+ bool equal(const Iterator& other) const;
+
+ const UnfoldingEvent* const& dereference() const;
+
+ // Allows boost::iterator_facade<...> to function properly
+ friend class boost::iterator_core_access;
+
+ // Allow the `History` class to use some of the
+ // computation of the iterator
+ friend History;
};
};
