From: Maxwell Pirtle Date: Wed, 8 Mar 2023 08:13:15 +0000 (+0100) Subject: Add conflict detection to EventSet X-Git-Tag: v3.34~350^2~10 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/dbbec1b6c52dca870aae22b10d0a5869838bf360 Add conflict detection to EventSet Detecting whether or not a collection of events are in conflict important for computing en(C) and for K-partial alternatives. We simply follow the definition of conflicts. More esoteric methods may exist that are faster, but for now let's keep it simple: we can always add those in later incrementally --- diff --git a/src/mc/explo/udpor/Configuration.cpp b/src/mc/explo/udpor/Configuration.cpp index f4ee2e1a5a..a1b7924edb 100644 --- a/src/mc/explo/udpor/Configuration.cpp +++ b/src/mc/explo/udpor/Configuration.cpp @@ -75,7 +75,7 @@ EventSet Configuration::get_minimally_reproducible_events() const // topological ordering that appear in `S` EventSet minimally_reproducible_events = EventSet(); - for (const auto& maximal_set : maximal_subsets_iterator_wrapper(*this)) { + for (const auto& maximal_set : maximal_subsets_iterator_wrapper(*this)) { if (maximal_set.size() > minimally_reproducible_events.size()) { minimally_reproducible_events = maximal_set; } else { diff --git a/src/mc/explo/udpor/EventSet.cpp b/src/mc/explo/udpor/EventSet.cpp index 33442cd16d..2cdb6fbed3 100644 --- a/src/mc/explo/udpor/EventSet.cpp +++ b/src/mc/explo/udpor/EventSet.cpp @@ -7,9 +7,10 @@ #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 #include +#include namespace simgrid::mc::udpor { @@ -133,13 +134,23 @@ bool EventSet::contains(const History& history) const bool EventSet::is_maximal() const { + // A set of events is maximal if no event from + // the original set is ruled out when traversing + // the history of the events const History history(*this); return *this == history.get_all_maximal_events(); } bool EventSet::is_conflict_free() const { - return false; + const auto begin = maximal_subsets_iterator(*this, std::nullopt, {2}); + const auto end = maximal_subsets_iterator(); + return std::none_of(begin, end, [](const EventSet event_pair) { + const auto events = std::move(event_pair).move_into_vector(); + const UnfoldingEvent* e1 = events[0]; + const UnfoldingEvent* e2 = events[1]; + return e1->conflicts_with(e2); + }); } std::vector EventSet::get_topological_ordering() const @@ -213,4 +224,16 @@ std::vector EventSet::get_topological_ordering_of_reverse return topological_events; } +std::vector EventSet::move_into_vector() const&& +{ + std::vector contents; + contents.reserve(size()); + + for (auto&& event : *this) { + contents.push_back(event); + } + + return contents; +} + } // namespace simgrid::mc::udpor \ No newline at end of file diff --git a/src/mc/explo/udpor/EventSet.hpp b/src/mc/explo/udpor/EventSet.hpp index 31bd7a9927..e49e1dbfef 100644 --- a/src/mc/explo/udpor/EventSet.hpp +++ b/src/mc/explo/udpor/EventSet.hpp @@ -142,6 +142,11 @@ public: * closer to the "bottom" */ std::vector get_topological_ordering_of_reverse_graph() const; + + /** + * @brief Moves the event set into a list + */ + std::vector move_into_vector() const&&; }; } // namespace simgrid::mc::udpor diff --git a/src/mc/explo/udpor/UnfoldingEvent.cpp b/src/mc/explo/udpor/UnfoldingEvent.cpp index 88f4b82dc7..9dffa8354b 100644 --- a/src/mc/explo/udpor/UnfoldingEvent.cpp +++ b/src/mc/explo/udpor/UnfoldingEvent.cpp @@ -40,4 +40,43 @@ EventSet UnfoldingEvent::get_history() const return History(this).get_all_events(); } +bool UnfoldingEvent::related_to(const UnfoldingEvent* other) const +{ + return EventSet({this, other}).is_maximal(); +} + +bool UnfoldingEvent::in_history_of(const UnfoldingEvent* other) const +{ + return History(other).contains(this); +} + +bool UnfoldingEvent::conflicts_with(const UnfoldingEvent* other) const +{ + // Events that have a causal relation never are in conflict + // in an unfolding structure. Two events in conflict must + // not be contained in each other's histories + if (related_to(other)) { + return false; + } + + const EventSet my_history = get_history(); + const EventSet other_history = other->get_history(); + const EventSet unique_to_me = my_history.subtracting(other_history); + const EventSet unique_to_other = other_history.subtracting(my_history); + + for (const auto e_me : unique_to_me) { + for (const auto e_other : unique_to_other) { + if (e_me->has_conflicting_transition_with(e_other)) { + return true; + } + } + } + return false; +} + +bool UnfoldingEvent::has_conflicting_transition_with(const UnfoldingEvent* other) const +{ + return associated_transition->depends(other->associated_transition.get()); +} + } // namespace simgrid::mc::udpor diff --git a/src/mc/explo/udpor/UnfoldingEvent.hpp b/src/mc/explo/udpor/UnfoldingEvent.hpp index f19c41eb68..e6c4662681 100644 --- a/src/mc/explo/udpor/UnfoldingEvent.hpp +++ b/src/mc/explo/udpor/UnfoldingEvent.hpp @@ -27,11 +27,13 @@ public: UnfoldingEvent(UnfoldingEvent&&) = default; EventSet get_history() const; - bool in_history_of(const UnfoldingEvent* otherEvent) const; + bool in_history_of(const UnfoldingEvent* other) const; + bool related_to(const UnfoldingEvent* other) const; - bool conflicts_with(const UnfoldingEvent* otherEvent) const; + bool conflicts_with(const UnfoldingEvent* other) const; bool conflicts_with(const Configuration& config) const; - bool immediately_conflicts_with(const UnfoldingEvent* otherEvt) const; + bool immediately_conflicts_with(const UnfoldingEvent* other) const; + bool has_conflicting_transition_with(const UnfoldingEvent* other) const; const EventSet& get_immediate_causes() const { return this->immediate_causes; } Transition* get_transition() const { return this->associated_transition.get(); } diff --git a/src/mc/explo/udpor/maximal_subsets_iterator.hpp b/src/mc/explo/udpor/maximal_subsets_iterator.hpp index c36d04a02c..7d0ab46565 100644 --- a/src/mc/explo/udpor/maximal_subsets_iterator.hpp +++ b/src/mc/explo/udpor/maximal_subsets_iterator.hpp @@ -148,8 +148,8 @@ private: friend class boost::iterator_core_access; }; -using maximal_subsets_iterator_wrapper = - simgrid::xbt::iterator_wrapping; +template +using maximal_subsets_iterator_wrapper = simgrid::xbt::iterator_wrapping; } // namespace simgrid::mc::udpor #endif