X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/573b5f83d54c3137fbedd6597bbef9ed3d4645fc..cf0a1a77c65746b1a40b858228bedf7a0eb63f7f:/src/mc/explo/udpor/Configuration.hpp diff --git a/src/mc/explo/udpor/Configuration.hpp b/src/mc/explo/udpor/Configuration.hpp index 2e22036b50..619871eac2 100644 --- a/src/mc/explo/udpor/Configuration.hpp +++ b/src/mc/explo/udpor/Configuration.hpp @@ -9,6 +9,8 @@ #include "src/mc/explo/udpor/EventSet.hpp" #include "src/mc/explo/udpor/udpor_forward.hpp" +#include + namespace simgrid::mc::udpor { class Configuration { @@ -18,42 +20,133 @@ public: Configuration& operator=(Configuration const&) = default; Configuration(Configuration&&) = default; + explicit Configuration(const UnfoldingEvent* event); + explicit Configuration(const EventSet& events); + explicit Configuration(const History& history); + explicit Configuration(std::initializer_list 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(const UnfoldingEvent* e) const { return this->events_.contains(e); } const EventSet& get_events() const { return this->events_; } - const EventSet& get_maximal_events() const { return this->max_events_; } - UnfoldingEvent* get_latest_event() const { return this->newest_event; } + const UnfoldingEvent* get_latest_event() const { return this->newest_event; } - void add_event(UnfoldingEvent*); + /** + * @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. + * + * @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. + * + * @throws an invalid argument exception is raised should the event + * be missing one of its dependencies + * + * @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) + */ + void add_event(const UnfoldingEvent* e); -private: /** - * @brief The most recent event added to the configuration + * @brief Whether or not the given event can be added to + * this configuration while keeping the set of events causally closed + * and conflict-free */ - UnfoldingEvent* newest_event = nullptr; + bool is_compatible_with(const UnfoldingEvent* e) const; /** - * @brief The events which make up this configuration + * @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 */ - EventSet events_; + bool is_compatible_with(const History& history) const; + + std::optional compute_alternative_to(const EventSet& D, const Unfolding& U) const; + std::optional compute_k_partial_alternative_to(const EventSet& D, const Unfolding& U, size_t k) const; /** - * The <-maxmimal events of the configuration. These are - * dynamically adjusted as events are added to the configuration + * @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" * - * @invariant: Each event that is part of this set is + * @returns a vector `V` with the following property: * - * 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 + * 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') * - * 2. contained in the set of events `events_` which comprise - * the configuration + * 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" */ - EventSet max_events_; + std::vector 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 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: - void recompute_maxmimal_events(UnfoldingEvent* new_event); + /** + * @brief The most recent event added to the configuration + */ + const UnfoldingEvent* newest_event = nullptr; + + /** + * @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