X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/f456852dd160e1f60f58e2a3ef37a0e688993fe0..d6eb772e45cc853fc204bb5aebeb411cdfa7c929:/src/mc/explo/udpor/Configuration.hpp diff --git a/src/mc/explo/udpor/Configuration.hpp b/src/mc/explo/udpor/Configuration.hpp index ead739e407..619871eac2 100644 --- a/src/mc/explo/udpor/Configuration.hpp +++ b/src/mc/explo/udpor/Configuration.hpp @@ -6,13 +6,10 @@ #ifndef SIMGRID_MC_UDPOR_CONFIGURATION_HPP #define SIMGRID_MC_UDPOR_CONFIGURATION_HPP -#include "src/mc/explo/udpor/CompatibilityGraph.hpp" #include "src/mc/explo/udpor/EventSet.hpp" #include "src/mc/explo/udpor/udpor_forward.hpp" -#include -#include -#include +#include namespace simgrid::mc::udpor { @@ -23,15 +20,19 @@ public: Configuration& operator=(Configuration const&) = default; Configuration(Configuration&&) = default; + explicit Configuration(const UnfoldingEvent* event); explicit Configuration(const EventSet& events); - explicit Configuration(std::initializer_list 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(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 @@ -60,7 +61,24 @@ public: * 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 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; /** * @brief Orders the events of the configuration such that @@ -77,7 +95,7 @@ public: * structure appear farther along in the list than those that appear * closer to the "top" */ - std::vector get_topologically_sorted_events() const; + std::vector get_topologically_sorted_events() const; /** * @brief Orders the events of the configuration such that @@ -101,26 +119,26 @@ public: * 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; + std::vector get_topologically_sorted_events_of_reverse_graph() const; /** - * @brief Construct a new compatibility graph from the events of the - * configuration whose associated transitions are dependent with the - * given action + * @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 * - * @param pred whether or not to even consider the unfolding event in any - * compatibility nodes of the resulting graph - * @returns a new compatibility graph that defines possible maximal subsets - * of events of C that satisfy the predicate `pred` + * @returns the smallest set of events whose events generates + * this configuration (denoted `config(E)`) */ - std::unique_ptr - make_compatibility_graph_filtered_on(std::function pred) const; + 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