From: Maxwell Pirtle Date: Fri, 3 Mar 2023 12:34:02 +0000 (+0100) Subject: Add computation for minimally reproducible sets X-Git-Tag: v3.34~362^2~6 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/d60b44af675a79ff27e2b1ddbcbe0d9885905d2b Add computation for minimally reproducible sets A minimally reproducible set of a configuration is simply the smallest set of events whose collective histories joint together cover every event in the configuration. Effecively, it is the maximal set of C whose history equals C. The computation builds upon the maximal_subsets_iterator introduced in a prior phase and exploits all of the work that already went into computing the subsets --- diff --git a/src/mc/explo/udpor/Configuration.cpp b/src/mc/explo/udpor/Configuration.cpp index 70f4659f0b..7f242d780b 100644 --- a/src/mc/explo/udpor/Configuration.cpp +++ b/src/mc/explo/udpor/Configuration.cpp @@ -6,6 +6,7 @@ #include "src/mc/explo/udpor/Configuration.hpp" #include "src/mc/explo/udpor/History.hpp" #include "src/mc/explo/udpor/UnfoldingEvent.hpp" +#include "src/mc/explo/udpor/maximal_subsets_iterator.hpp" #include "xbt/asserts.h" #include @@ -88,10 +89,6 @@ std::vector Configuration::get_topologically_sorted_event event_stack.push(cause); } } else { - // Mark this event as: - // 1. discovered across all DFSs performed - // 2. permanently marked - // 3. part of the topological search unknown_events.remove(evt); temporarily_marked_events.remove(evt); permanently_marked_events.insert(evt); @@ -102,7 +99,7 @@ std::vector Configuration::get_topologically_sorted_event topological_ordering.push_back(evt); // Only now do we remove the event, i.e. once - // we've processed the same event again + // we've processed the same event twice event_stack.pop(); } } @@ -112,7 +109,7 @@ std::vector Configuration::get_topologically_sorted_event std::vector Configuration::get_topologically_sorted_events_of_reverse_graph() const { - // The method exploits the property that + // The implementation exploits the property that // a topological sorting S^R of the reverse graph G^R // of some graph G is simply the reverse of any // topological sorting S of G. @@ -121,4 +118,35 @@ std::vector Configuration::get_topologically_sorted_event return topological_events; } +EventSet Configuration::get_minimally_reproducible_events() const +{ + // The implementation exploits the following observations: + // + // To select the smallest reproducible set of events, we want + // to pick events that "knock out" a lot of others. Furthermore, + // we need to ensure that the events furthest down in the + // causality graph are also selected. If you combine these ideas, + // you're basically left with traversing the set of maximal + // subsets of C! And we have an iterator for that already! + // + // The next observation is that the moment we don't increase in size + // the current maximal set (or decrease the number of events), + // we know that the prior set `S` covered the entire history of C and + // was maximal. Subsequent sets will miss events earlier in the + // topological ordering that appear in `S` + EventSet minimally_reproducible_events = EventSet(); + + for (const auto& maximal_set : maximal_subsets_iterator_wrapper(*this)) { + if (maximal_set.size() > minimally_reproducible_events.size()) { + minimally_reproducible_events = maximal_set; + } else { + // The moment we see the iterator generate a set of size + // that is not monotonically increasing, we can stop: + // the set prior was the minimally-reproducible one + return minimally_reproducible_events; + } + } + return minimally_reproducible_events; +} + } // namespace simgrid::mc::udpor diff --git a/src/mc/explo/udpor/Configuration.hpp b/src/mc/explo/udpor/Configuration.hpp index a820a41f91..6dbc953dcb 100644 --- a/src/mc/explo/udpor/Configuration.hpp +++ b/src/mc/explo/udpor/Configuration.hpp @@ -104,6 +104,19 @@ public: */ 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: /** * @brief The most recent event added to the configuration diff --git a/src/mc/explo/udpor/maximal_subsets_iterator.hpp b/src/mc/explo/udpor/maximal_subsets_iterator.hpp index be8e86c10e..33c364eee4 100644 --- a/src/mc/explo/udpor/maximal_subsets_iterator.hpp +++ b/src/mc/explo/udpor/maximal_subsets_iterator.hpp @@ -132,5 +132,37 @@ private: friend class boost::iterator_core_access; }; +/** + * @brief A collection whose contents consist of + * the maximal event sets of some configuration + * + * @note You should treat this class as a small + * wrapper that is more convenient and readable + * than creating iterators directly, and thus should + * not e.g. store instanca + */ +class maximal_subsets_iterator_wrapper { +public: + using node_filter_function = maximal_subsets_iterator::node_filter_function; + + maximal_subsets_iterator_wrapper(const maximal_subsets_iterator_wrapper&) = delete; + maximal_subsets_iterator_wrapper& operator=(const maximal_subsets_iterator_wrapper&) = delete; + maximal_subsets_iterator_wrapper(const maximal_subsets_iterator_wrapper&&) = delete; + maximal_subsets_iterator_wrapper& operator=(const maximal_subsets_iterator_wrapper&&) = delete; + + explicit maximal_subsets_iterator_wrapper(const Configuration& config) : config(config) {} + maximal_subsets_iterator_wrapper(const Configuration& config, node_filter_function filter) + : config(config), filter({filter}) + { + } + + auto begin() const { return maximal_subsets_iterator(config, filter); } + auto end() const { return maximal_subsets_iterator(); } + +private: + const Configuration& config; + std::optional filter = std::nullopt; +}; + } // namespace simgrid::mc::udpor #endif