{
/// @invariant: A collection of events `E` is a configuration
/// if and only if following while following the history of
- /// each event `e` of `E`you remain in `E`. In other words, you
+ /// each event `e` of `E` you remain in `E`. In other words, you
/// only see events from set `E`
///
- /// The proof is based on the definition of a configuration
- /// which requires that all
+ /// The simple proof is based on the definition of a configuration
+ /// which requires that all events have their history contained
+ /// in the set
const History history(*this);
return this->contains(history);
}
// and all subsequent events that are added by the iterator
}
-History::Iterator& History::Iterator::operator++()
+void History::Iterator::increment()
{
if (not frontier.empty()) {
// "Pop" the event at the "front"
// 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
candidates.subtract(current_history);
frontier.form_union(candidates);
}
- return *this;
+}
+
+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
#include "src/mc/explo/udpor/EventSet.hpp"
#include "src/mc/explo/udpor/udpor_forward.hpp"
+#include <boost/iterator/iterator_facade.hpp>
#include <functional>
#include <optional>
/**
* @brief An iterator which traverses the history of a set of events
*/
- struct Iterator {
+ struct Iterator : boost::iterator_facade<Iterator, UnfoldingEvent* const, boost::forward_traversal_tag> {
public:
- Iterator& operator++();
- auto operator->() const { 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) const { return this->frontier == other.frontier; }
- bool operator!=(const Iterator& other) const { 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&;
using optional_configuration = std::optional<std::reference_wrapper<const Configuration>>;
-
Iterator(const EventSet& initial_events, optional_configuration config = std::nullopt);
private:
EventSet current_history = EventSet();
/// @brief What the iterator currently believes
+ // to be the set of maximal events
EventSet maximal_events;
optional_configuration configuration;
+
+ // boost::iterator_facade<...> interface to implement
+ void increment();
+ bool equal(const Iterator& other) 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;
};
};
