X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/60b66b6d708b68fe8338e1a3e0bc8d298b1260ee..45c3a73f3553c8d365f61eaa8445f038db9bdb8f:/src/mc/explo/udpor/maximal_subsets_iterator.hpp diff --git a/src/mc/explo/udpor/maximal_subsets_iterator.hpp b/src/mc/explo/udpor/maximal_subsets_iterator.hpp index aeaebab88f..2c3c07f941 100644 --- a/src/mc/explo/udpor/maximal_subsets_iterator.hpp +++ b/src/mc/explo/udpor/maximal_subsets_iterator.hpp @@ -7,8 +7,10 @@ #define SIMGRID_MC_UDPOR_MAXIMAL_SUBSETS_ITERATOR_HPP #include "src/mc/explo/udpor/Configuration.hpp" +#include "src/xbt/utils/iter/iterator_wrapping.hpp" #include +#include #include #include #include @@ -17,10 +19,11 @@ namespace simgrid::mc::udpor { /** * @brief An iterator over the tree of sets of (non-empty) maximal events that - * can be generated from a given configuration + * can be generated from a given set of events * * This iterator traverses all possible sets of maximal events that - * can be formed from a configuration, each of which satisfy a predicate. + * can be formed from some subset of events of an unfolding, + * each of which satisfy a predicate. * * Iteration over the maximal events of a configuration is an important * step in computing the extension set of a configuration for an action @@ -35,29 +38,27 @@ public: using node_filter_function = std::function; using topological_order_position = std::vector::const_iterator; - maximal_subsets_iterator() = default; - explicit maximal_subsets_iterator(const Configuration& config) : maximal_subsets_iterator(config, std::nullopt) {} - - maximal_subsets_iterator(const Configuration& config, std::optional filter) - : config({config}) - , topological_ordering(config.get_topologically_sorted_events_of_reverse_graph()) - , filter_function(filter) - , current_maximal_set({EventSet()}) + maximal_subsets_iterator() = default; + explicit maximal_subsets_iterator(const Configuration& config, + std::optional filter = std::nullopt, + std::optional maximum_subset_size = std::nullopt) + : maximal_subsets_iterator(config.get_events(), filter, maximum_subset_size) { } + explicit maximal_subsets_iterator(const EventSet& events, std::optional filter = std::nullopt, + std::optional maximum_subset_size = std::nullopt); private: - const std::optional> config; - const std::vector topological_ordering; - const std::optional filter_function = std::nullopt; + std::vector topological_ordering; // The boolean is a bit of an annoyance, but it works. Effectively, // there's no way to distinguish between "we're starting the search // after the empty set" and "we've finished the search" since the resulting // maximal set and backtracking point stack will both be empty in both cases - bool has_started_searching = false; - std::optional current_maximal_set = std::nullopt; - std::stack backtrack_points; + bool has_started_searching = false; + std::optional maximum_subset_size = std::nullopt; + std::optional current_maximal_set = std::nullopt; + std::stack> backtrack_points; /** * @brief A small class which provides functionality for managing @@ -69,9 +70,10 @@ private: * with events that are its current maximal event set (i.e. * its `current_maximal_set`) */ - struct bookkeeper { + struct Bookkeeper { public: using topological_order_position = maximal_subsets_iterator::topological_order_position; + void mark_included_in_maximal_set(const UnfoldingEvent*); void mark_removed_from_maximal_set(const UnfoldingEvent*); topological_order_position find_next_candidate_event(topological_order_position first, @@ -84,8 +86,8 @@ private: /// bookkeeping that has been done thus far, can be added to the /// current candidate maximal set bool is_candidate_event(const UnfoldingEvent*) const; - - } bookkeeper; + }; + Bookkeeper bookkeeper; void add_element_to_current_maximal_set(const UnfoldingEvent*); void remove_element_from_current_maximal_set(const UnfoldingEvent*); @@ -124,9 +126,12 @@ private: */ topological_order_position continue_traversal_of_maximal_events_tree(); - /// @brief Whether or not we should even consider cases where the given - /// event `e` is included in the maximal configurations - bool should_consider_event(const UnfoldingEvent*) const; + /** + * @brief: Whether or not the current maximal set can + * grow based on the size limit imposed on the maximal + * sets that can be produced + */ + bool can_grow_maximal_set() const; // boost::iterator_facade<...> interface to implement void increment(); @@ -144,5 +149,8 @@ private: friend class boost::iterator_core_access; }; +template +using maximal_subsets_iterator_wrapper = simgrid::xbt::iterator_wrapping; + } // namespace simgrid::mc::udpor #endif