#include "src/mc/explo/udpor/EventSet.hpp"
#include "src/mc/explo/udpor/udpor_forward.hpp"
-namespace simgrid::mc::udpor {
+#include <optional>
-using StateHandle = uint64_t;
+namespace simgrid::mc::udpor {
class Configuration {
public:
Configuration& operator=(Configuration const&) = default;
Configuration(Configuration&&) = default;
- inline auto begin() const { return this->events_.begin(); }
- inline auto end() const { return this->events_.end(); }
- inline const EventSet& get_events() const { return this->events_; }
- inline const EventSet& get_maximal_events() const { return this->max_events_; }
+ explicit Configuration(const UnfoldingEvent* event);
+ explicit Configuration(const EventSet& events);
+ explicit Configuration(const History& history);
+ explicit Configuration(std::initializer_list<const UnfoldingEvent*> events);
- void add_event(UnfoldingEvent*);
- UnfoldingEvent* get_latest_event() const;
+ 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(); }
-private:
- /**
- * @brief The most recent event added to the configuration
- */
- UnfoldingEvent* newest_event = nullptr;
- EventSet events_;
+ bool contains(const UnfoldingEvent* e) const { return this->events_.contains(e); }
+ const EventSet& get_events() const { return this->events_; }
+ const UnfoldingEvent* get_latest_event() const { return this->newest_event; }
/**
- * The <-maxmimal events of the configuration. These are
- * dynamically adjusted as events are added to the configuration
+ * @brief Insert a new event into the configuration
+ *
+ * When the newly added event is inserted into the configuration,
+ * an assertion is made to ensure that the configuration remains
+ * valid, i.e. that the newly added event's dependencies are contained
+ * within the configuration.
*
- * @invariant: Each event that is part of this set is
+ * @param e the event to add to the configuration. If the event is
+ * already a part of the configuration, calling this method has no
+ * effect.
*
- * 1. a <-maxmimal event of the configuration, in the sense that
- * there is no event in the configuration that is "greater" than it.
- * In UDPOR terminology, each event does not "cause" another event
+ * @throws an invalid argument exception is raised should the event
+ * be missing one of its dependencies
*
- * 2. contained in the set of events `events_` which comprise
- * the configuration
+ * @note: UDPOR technically enforces the invariant that all newly-added events
+ * will ensure that the configuration is valid. We perform extra checks to ensure
+ * that UDPOR is implemented as expected. There is a performance penalty that
+ * should be noted: checking for maximality requires ensuring that all events in the
+ * configuration have their dependencies containes within the configuration, which
+ * essentially means performing a BFS/DFS over the configuration using a History object.
+ * However, since the slowest part of UDPOR involves enumerating all
+ * subsets of maximal events and computing k-partial alternatives (the
+ * latter definitively an NP-hard problem when optimal), Amdahl's law suggests
+ * we shouldn't focus so much on this (let alone the additional benefit of the
+ * assertions)
*/
- EventSet max_events_;
-
-private:
- void recompute_maxmimal_events(UnfoldingEvent* new_event);
-};
-
-class UnfoldingEvent {
-public:
- UnfoldingEvent(unsigned int nb_events, std::string const& trans_tag, EventSet const& immediate_causes,
- StateHandle sid);
- UnfoldingEvent(unsigned int nb_events, std::string const& trans_tag, EventSet const& immediate_causes);
- UnfoldingEvent(const UnfoldingEvent&) = default;
- UnfoldingEvent& operator=(UnfoldingEvent const&) = default;
- UnfoldingEvent(UnfoldingEvent&&) = default;
+ void add_event(const UnfoldingEvent* e);
- EventSet get_history() const;
- bool in_history(const UnfoldingEvent* otherEvent) const;
-
- bool conflicts_with(const UnfoldingEvent* otherEvent) const;
- bool conflicts_with(const Configuration& config) const;
- bool immediately_conflicts_with(const UnfoldingEvent* otherEvt) const;
+ /**
+ * @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;
- bool operator==(const UnfoldingEvent&) const { return false; };
+ /**
+ * @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;
- inline StateHandle get_state_id() const { return state_id; }
- inline void set_state_id(StateHandle sid) { state_id = sid; }
+ 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;
-private:
- int id = -1;
+ /**
+ * @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 The "immediate" causes of this event.
+ * @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()"
*
- * An event `e` is an immediate cause of an event `e'` if
+ * @returns a vector `V` with the following property:
*
- * 1. e < e'
- * 2. There is no event `e''` in E such that
- * `e < e''` and `e'' < e'`
+ * 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, an immediate cause "happened right before"
- * this event was executed. It is sufficient to store
- * only the immediate causes of any event `e`, as any indirect
- * causes of that event would either be an indirect cause
- * or an immediate cause of the immediate causes of `e`, and
- * so on.
+ * 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"
*/
- EventSet immediate_causes;
- StateHandle state_id = 0ul;
-};
+ std::vector<const UnfoldingEvent*> get_topologically_sorted_events_of_reverse_graph() const;
-class StateManager {
-private:
- using Handle = StateHandle;
+ /**
+ * @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;
- Handle current_handle_ = 1ul;
- std::unordered_map<Handle, std::unique_ptr<State>> state_map_;
+private:
+ /**
+ * @brief The most recent event added to the configuration
+ */
+ const UnfoldingEvent* newest_event = nullptr;
-public:
- Handle record_state(std::unique_ptr<State>);
- std::optional<std::reference_wrapper<State>> get_state(Handle);
+ /**
+ * @brief The events which make up this configuration
+ *
+ * @invariant For each event `e` in `events_`, the set of
+ * dependencies of `e` is also contained in `events_`
+ */
+ EventSet events_;
};
} // namespace simgrid::mc::udpor
