#include "src/mc/explo/udpor/EventSet.hpp"
#include "src/mc/explo/udpor/udpor_forward.hpp"
-#include <initializer_list>
+#include <optional>
namespace simgrid::mc::udpor {
Configuration& operator=(Configuration const&) = default;
Configuration(Configuration&&) = default;
- Configuration(EventSet events);
- Configuration(std::initializer_list<UnfoldingEvent*> events);
+ explicit Configuration(const UnfoldingEvent* event);
+ explicit Configuration(const EventSet& events);
+ explicit Configuration(const History& history);
+ explicit Configuration(std::initializer_list<const UnfoldingEvent*> events);
auto begin() const { return this->events_.begin(); }
auto end() const { return this->events_.end(); }
+ auto cbegin() const { return this->events_.cbegin(); }
+ auto cend() const { return this->events_.cend(); }
- bool contains(UnfoldingEvent* e) const { return this->events_.contains(e); }
+ bool contains(const UnfoldingEvent* e) const { return this->events_.contains(e); }
const EventSet& get_events() const { return this->events_; }
- UnfoldingEvent* get_latest_event() const { return this->newest_event; }
+ const UnfoldingEvent* get_latest_event() const { return this->newest_event; }
/**
* @brief Insert a new event into the configuration
* we shouldn't focus so much on this (let alone the additional benefit of the
* assertions)
*/
- void add_event(UnfoldingEvent* e);
+ void add_event(const UnfoldingEvent* e);
+
+ /**
+ * @brief Whether or not the given event can be added to
+ * this configuration while keeping the set of events causally closed
+ * and conflict-free
+ */
+ bool is_compatible_with(const UnfoldingEvent* e) const;
+
+ /**
+ * @brief Whether or not the events in the given history can be added to
+ * this configuration while keeping the set of events causally closed
+ * and conflict-free
+ */
+ bool is_compatible_with(const History& history) const;
+
+ std::optional<Configuration> compute_alternative_to(const EventSet& D, const Unfolding& U) const;
+ std::optional<Configuration> compute_k_partial_alternative_to(const EventSet& D, const Unfolding& U, size_t k) const;
+
+ /**
+ * @brief Orders the events of the configuration such that
+ * "more recent" events (i.e. those that are farther down in
+ * the event structure's dependency chain) come after those
+ * that appeared "farther in the past"
+ *
+ * @returns a vector `V` with the following property:
+ *
+ * 1. Let i(e) := C -> I map events to their indices in `V`.
+ * For every pair of events e, e' in C, if e < e' then i(e) < i(e')
+ *
+ * Intuitively, events that are closer to the "bottom" of the event
+ * structure appear farther along in the list than those that appear
+ * closer to the "top"
+ */
+ std::vector<const UnfoldingEvent*> get_topologically_sorted_events() const;
+
+ /**
+ * @brief Orders the events of the configuration such that
+ * "more recent" events (i.e. those that are farther down in
+ * the event structure's dependency chain) come before those
+ * that appear "farther in the past"
+ *
+ * @note The events of the event structure are arranged such that
+ * e < e' implies a directed edge from e to e'. However, it is
+ * also useful to be able to traverse the *reverse* graph (for
+ * example when computing the compatibility graph of a configuration),
+ * hence the distinction between "reversed" and the method
+ * "Configuration::get_topologically_sorted_events()"
+ *
+ * @returns a vector `V` with the following property:
+ *
+ * 1. Let i(e) := C -> I map events to their indices in `V`.
+ * For every pair of events e, e' in C, if e < e' then i(e) > i(e')
+ *
+ * Intuitively, events that are closer to the "top" of the event
+ * structure appear farther along in the list than those that appear
+ * closer to the "bottom"
+ */
+ std::vector<const UnfoldingEvent*> get_topologically_sorted_events_of_reverse_graph() const;
+
+ /**
+ * @brief Computes the smallest set of events whose collective histories
+ * capture all events of this configuration
+ *
+ * @invariant The set of all events in the collective histories
+ * of the events returned by this method is equal to the set of events
+ * in this configuration
+ *
+ * @returns the smallest set of events whose events generates
+ * this configuration (denoted `config(E)`)
+ */
+ EventSet get_minimally_reproducible_events() const;
private:
/**
* @brief The most recent event added to the configuration
*/
- UnfoldingEvent* newest_event = nullptr;
+ const UnfoldingEvent* newest_event = nullptr;
/**
* @brief The events which make up this configuration
