include src/mc/explo/udpor/UnfoldingEvent.hpp
include src/mc/explo/udpor/UnfoldingEvent_test.cpp
include src/mc/explo/udpor/Unfolding_test.cpp
+include src/mc/explo/udpor/maximal_subsets_iterator.cpp
+include src/mc/explo/udpor/maximal_subsets_iterator.hpp
include src/mc/explo/udpor/udpor_forward.hpp
include src/mc/inspect/DwarfExpression.cpp
include src/mc/inspect/DwarfExpression.hpp
// TODO: Add verbose logging about which event is being explored
- UnfoldingEvent* e = select_next_unfolding_event(A, enC);
+ const UnfoldingEvent* e = select_next_unfolding_event(A, enC);
xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n"
"UDPOR guarantees that an event will be chosen at each point in\n"
"the search, yet no events were actually chosen\n"
//
// ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} +
// U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at K }
- UnfoldingEvent* e_cur = C.get_latest_event();
- EventSet exC = prev_exC;
+ const UnfoldingEvent* e_cur = C.get_latest_event();
+ EventSet exC = prev_exC;
exC.remove(e_cur);
for (const auto& [aid, actor_state] : stateC.get_actors_list()) {
return next_state;
}
-UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
+const UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
{
if (!enC.empty()) {
return *(enC.begin());
* by the UDPOR algorithm to select new events to search. See the original
* paper [1] for more details
*/
- UnfoldingEvent* select_next_unfolding_event(const EventSet& A, const EventSet& enC);
+ const UnfoldingEvent* select_next_unfolding_event(const EventSet& A, const EventSet& enC);
/**
* @brief Computes the sets `ex(C)` and `en(C)` of the given configuration
namespace simgrid::mc::udpor {
-Configuration::Configuration(std::initializer_list<UnfoldingEvent*> events) : Configuration(EventSet(std::move(events)))
+Configuration::Configuration(std::initializer_list<const UnfoldingEvent*> events)
+ : Configuration(EventSet(std::move(events)))
{
}
}
}
-void Configuration::add_event(UnfoldingEvent* e)
+void Configuration::add_event(const UnfoldingEvent* e)
{
if (e == nullptr) {
throw std::invalid_argument("Expected a nonnull `UnfoldingEvent*` but received NULL instead");
}
}
-std::vector<UnfoldingEvent*> Configuration::get_topologically_sorted_events() const
+std::vector<const UnfoldingEvent*> Configuration::get_topologically_sorted_events() const
{
if (events_.empty()) {
- return std::vector<UnfoldingEvent*>();
+ return std::vector<const UnfoldingEvent*>();
}
- std::stack<UnfoldingEvent*> event_stack;
- std::vector<UnfoldingEvent*> topological_ordering;
+ std::stack<const UnfoldingEvent*> event_stack;
+ std::vector<const UnfoldingEvent*> topological_ordering;
EventSet unknown_events = events_;
EventSet temporarily_marked_events;
EventSet permanently_marked_events;
event_stack.push(*unknown_events.begin());
while (not event_stack.empty()) {
- UnfoldingEvent* evt = event_stack.top();
+ const UnfoldingEvent* evt = event_stack.top();
discovered_events.insert(evt);
if (not temporarily_marked_events.contains(evt)) {
return topological_ordering;
}
-std::vector<UnfoldingEvent*> Configuration::get_topologically_sorted_events_of_reverse_graph() const
+std::vector<const UnfoldingEvent*> Configuration::get_topologically_sorted_events_of_reverse_graph() const
{
// The method exploits the property that
// a topological sorting S^R of the reverse graph G^R
#include "src/mc/explo/udpor/EventSet.hpp"
#include "src/mc/explo/udpor/udpor_forward.hpp"
+#include <boost/iterator/iterator_facade.hpp>
#include <functional>
#include <initializer_list>
+#include <optional>
#include <vector>
namespace simgrid::mc::udpor {
Configuration(Configuration&&) = default;
explicit Configuration(const EventSet& events);
- explicit Configuration(std::initializer_list<UnfoldingEvent*> events);
+ explicit Configuration(std::initializer_list<const UnfoldingEvent*> events);
auto begin() const { return this->events_.begin(); }
auto end() const { return this->events_.end(); }
- 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
* 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 Orders the events of the configuration such that
* structure appear farther along in the list than those that appear
* closer to the "top"
*/
- std::vector<UnfoldingEvent*> get_topologically_sorted_events() const;
+ std::vector<const UnfoldingEvent*> get_topologically_sorted_events() const;
/**
* @brief Orders the events of the configuration such that
* structure appear farther along in the list than those that appear
* closer to the "bottom"
*/
- std::vector<UnfoldingEvent*> get_topologically_sorted_events_of_reverse_graph() const;
+ std::vector<const UnfoldingEvent*> get_topologically_sorted_events_of_reverse_graph() 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
#include "src/mc/explo/udpor/EventSet.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 <unordered_map>
using namespace simgrid::mc::udpor;
SECTION("Topological ordering for entire set")
{
Configuration C{&e1, &e2, &e3, &e4};
- REQUIRE(C.get_topologically_sorted_events() == std::vector<UnfoldingEvent*>{&e1, &e2, &e3, &e4});
- REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<UnfoldingEvent*>{&e4, &e3, &e2, &e1});
+ REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3, &e4});
+ REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() ==
+ std::vector<const UnfoldingEvent*>{&e4, &e3, &e2, &e1});
}
SECTION("Topological ordering for subsets")
SECTION("No elements")
{
Configuration C;
- REQUIRE(C.get_topologically_sorted_events() == std::vector<UnfoldingEvent*>{});
- REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<UnfoldingEvent*>{});
+ REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{});
+ REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<const UnfoldingEvent*>{});
}
SECTION("e1 only")
{
Configuration C{&e1};
- REQUIRE(C.get_topologically_sorted_events() == std::vector<UnfoldingEvent*>{&e1});
- REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<UnfoldingEvent*>{&e1});
+ REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1});
+ REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<const UnfoldingEvent*>{&e1});
}
SECTION("e1 and e2 only")
{
Configuration C{&e1, &e2};
- REQUIRE(C.get_topologically_sorted_events() == std::vector<UnfoldingEvent*>{&e1, &e2});
- REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<UnfoldingEvent*>{&e2, &e1});
+ REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2});
+ REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<const UnfoldingEvent*>{&e2, &e1});
}
SECTION("e1, e2, and e3 only")
{
Configuration C{&e1, &e2, &e3};
- REQUIRE(C.get_topologically_sorted_events() == std::vector<UnfoldingEvent*>{&e1, &e2, &e3});
- REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<UnfoldingEvent*>{&e3, &e2, &e1});
+ REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3});
+ REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() ==
+ std::vector<const UnfoldingEvent*>{&e3, &e2, &e1});
}
}
}
SECTION("No elements")
{
Configuration C;
- REQUIRE(C.get_topologically_sorted_events() == std::vector<UnfoldingEvent*>{});
- REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<UnfoldingEvent*>{});
+ REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{});
+ REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<const UnfoldingEvent*>{});
}
SECTION("e1 only")
{
Configuration C{&e1};
- REQUIRE(C.get_topologically_sorted_events() == std::vector<UnfoldingEvent*>{&e1});
- REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<UnfoldingEvent*>{&e1});
+ REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1});
+ REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<const UnfoldingEvent*>{&e1});
}
SECTION("e1 and e2 only")
{
Configuration C{&e1, &e2};
- REQUIRE(C.get_topologically_sorted_events() == std::vector<UnfoldingEvent*>{&e1, &e2});
- REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<UnfoldingEvent*>{&e2, &e1});
+ REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2});
+ REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<const UnfoldingEvent*>{&e2, &e1});
}
SECTION("e1, e2, and e3 only")
{
Configuration C{&e1, &e2, &e3};
- REQUIRE(C.get_topologically_sorted_events() == std::vector<UnfoldingEvent*>{&e1, &e2, &e3});
- REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<UnfoldingEvent*>{&e3, &e2, &e1});
+ REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3});
+ REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() ==
+ std::vector<const UnfoldingEvent*>{&e3, &e2, &e1});
}
SECTION("e1, e2, e3, and e6 only")
{
Configuration C{&e1, &e2, &e3, &e6};
- REQUIRE(C.get_topologically_sorted_events() == std::vector<UnfoldingEvent*>{&e1, &e2, &e3, &e6});
- REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<UnfoldingEvent*>{&e6, &e3, &e2, &e1});
+ REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3, &e6});
+ REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() ==
+ std::vector<const UnfoldingEvent*>{&e6, &e3, &e2, &e1});
}
SECTION("e1, e2, e3, and e4 only")
{
Configuration C{&e1, &e2, &e3, &e4};
- REQUIRE(C.get_topologically_sorted_events() == std::vector<UnfoldingEvent*>{&e1, &e2, &e3, &e4});
- REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<UnfoldingEvent*>{&e4, &e3, &e2, &e1});
+ REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3, &e4});
+ REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() ==
+ std::vector<const UnfoldingEvent*>{&e4, &e3, &e2, &e1});
}
SECTION("e1, e2, e3, e4, and e5 only")
{
Configuration C{&e1, &e2, &e3, &e4, &e5};
- REQUIRE(C.get_topologically_sorted_events() == std::vector<UnfoldingEvent*>{&e1, &e2, &e3, &e4, &e5});
+ REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3, &e4, &e5});
REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() ==
- std::vector<UnfoldingEvent*>{&e5, &e4, &e3, &e2, &e1});
+ std::vector<const UnfoldingEvent*>{&e5, &e4, &e3, &e2, &e1});
}
SECTION("e1, e2, e3, e4 and e6 only")
// In this case, e4 and e6 are interchangeable. Hence, we have to check
// if the sorting gives us *any* of the combinations
Configuration C{&e1, &e2, &e3, &e4, &e6};
- REQUIRE((C.get_topologically_sorted_events() == std::vector<UnfoldingEvent*>{&e1, &e2, &e3, &e4, &e6} ||
- C.get_topologically_sorted_events() == std::vector<UnfoldingEvent*>{&e1, &e2, &e3, &e6, &e4}));
+ REQUIRE((C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3, &e4, &e6} ||
+ C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3, &e6, &e4}));
REQUIRE((C.get_topologically_sorted_events_of_reverse_graph() ==
- std::vector<UnfoldingEvent*>{&e6, &e4, &e3, &e2, &e1} ||
+ std::vector<const UnfoldingEvent*>{&e6, &e4, &e3, &e2, &e1} ||
C.get_topologically_sorted_events_of_reverse_graph() ==
- std::vector<UnfoldingEvent*>{&e4, &e6, &e3, &e2, &e1}));
+ std::vector<const UnfoldingEvent*>{&e4, &e6, &e3, &e2, &e1}));
}
SECTION("Topological ordering for entire set")
// In this case, e4/e5 are both interchangeable with e6. Hence, again we have to check
// if the sorting gives us *any* of the combinations
Configuration C{&e1, &e2, &e3, &e4, &e5, &e6};
- REQUIRE((C.get_topologically_sorted_events() == std::vector<UnfoldingEvent*>{&e1, &e2, &e3, &e4, &e5, &e6} ||
- C.get_topologically_sorted_events() == std::vector<UnfoldingEvent*>{&e1, &e2, &e3, &e4, &e6, &e5} ||
- C.get_topologically_sorted_events() == std::vector<UnfoldingEvent*>{&e1, &e2, &e3, &e6, &e4, &e5}));
+ REQUIRE(
+ (C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3, &e4, &e5, &e6} ||
+ C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3, &e4, &e6, &e5} ||
+ C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3, &e6, &e4, &e5}));
REQUIRE((C.get_topologically_sorted_events_of_reverse_graph() ==
- std::vector<UnfoldingEvent*>{&e6, &e5, &e4, &e3, &e2, &e1} ||
+ std::vector<const UnfoldingEvent*>{&e6, &e5, &e4, &e3, &e2, &e1} ||
C.get_topologically_sorted_events_of_reverse_graph() ==
- std::vector<UnfoldingEvent*>{&e5, &e6, &e4, &e3, &e2, &e1} ||
+ std::vector<const UnfoldingEvent*>{&e5, &e6, &e4, &e3, &e2, &e1} ||
C.get_topologically_sorted_events_of_reverse_graph() ==
- std::vector<UnfoldingEvent*>{&e5, &e4, &e6, &e3, &e2, &e1}));
+ std::vector<const UnfoldingEvent*>{&e5, &e4, &e6, &e3, &e2, &e1}));
}
}
}
EventSet events_seen;
const auto ordered_events = C.get_topologically_sorted_events();
- std::for_each(ordered_events.begin(), ordered_events.end(), [&events_seen](UnfoldingEvent* e) {
+ std::for_each(ordered_events.begin(), ordered_events.end(), [&events_seen](const UnfoldingEvent* e) {
History history(e);
for (auto* e_hist : history) {
// In this demo, we want to make sure that
EventSet events_seen;
const auto ordered_events = C.get_topologically_sorted_events_of_reverse_graph();
- std::for_each(ordered_events.begin(), ordered_events.end(), [&events_seen](UnfoldingEvent* e) {
+ std::for_each(ordered_events.begin(), ordered_events.end(), [&events_seen](const UnfoldingEvent* e) {
History history(e);
for (auto* e_hist : history) {
events_seen.insert(e);
});
}
+
+ SECTION("Test that the topological ordering contains only the events of the configuration")
+ {
+ const EventSet events_seen = C.get_events();
+
+ SECTION("Forward direction")
+ {
+ auto ordered_events = C.get_topologically_sorted_events();
+ const EventSet ordered_event_set = EventSet(std::move(ordered_events));
+ REQUIRE(events_seen == ordered_event_set);
+ }
+
+ SECTION("Reverse direction")
+ {
+ auto ordered_events = C.get_topologically_sorted_events_of_reverse_graph();
+ const EventSet ordered_event_set = EventSet(std::move(ordered_events));
+ REQUIRE(events_seen == ordered_event_set);
+ }
+ }
+}
+
+TEST_CASE("simgrid::mc::udpor::maximal_subsets_iterator: Basic Testing of Maximal Subsets")
+{
+ // The following tests concern the given event structure:
+ // e1
+ // / /
+ // e2 e5
+ // / /
+ // e3 e6
+ // / / /
+ // e4 e7 e8
+ UnfoldingEvent e1;
+ UnfoldingEvent e2{&e1};
+ UnfoldingEvent e3{&e2};
+ UnfoldingEvent e4{&e3};
+ UnfoldingEvent e5{&e1};
+ UnfoldingEvent e6{&e5};
+ UnfoldingEvent e7{&e6};
+ UnfoldingEvent e8{&e6};
+
+ SECTION("Iteration over an empty configuration yields only the empty set")
+ {
+ Configuration C;
+ maximal_subsets_iterator first(C);
+ maximal_subsets_iterator last;
+
+ REQUIRE(*first == EventSet());
+ ++first;
+ REQUIRE(first == last);
+ }
+
+ SECTION("Check counts of maximal event sets discovered")
+ {
+ std::unordered_map<int, int> maximal_subset_counts;
+
+ Configuration C{&e1, &e2, &e3, &e4, &e5, &e6, &e7, &e8};
+ maximal_subsets_iterator first(C);
+ maximal_subsets_iterator last;
+
+ for (; first != last; ++first) {
+ maximal_subset_counts[(*first).size()]++;
+ }
+
+ // First, ensure that there are only sets of size 0, 1, 2, and 3
+ CHECK(maximal_subset_counts.size() == 4);
+
+ // The empty set should appear only once
+ REQUIRE(maximal_subset_counts[0] == 1);
+
+ // 8 is the number of nodes in the graph
+ REQUIRE(maximal_subset_counts[1] == 8);
+
+ // 13 = 3 * 4 (each of the left branch can combine with one in the right branch) + 1 (e7 + e8)
+ REQUIRE(maximal_subset_counts[2] == 13);
+
+ // e7 + e8 must be included, so that means we can combine from the left branch
+ REQUIRE(maximal_subset_counts[3] == 3);
+ }
+
+ SECTION("Check counts of maximal event sets discovered with a filter")
+ {
+ std::unordered_map<int, int> maximal_subset_counts;
+
+ Configuration C{&e1, &e2, &e3, &e4, &e5, &e6, &e7, &e8};
+
+ SECTION("Filter with events part of initial maximal set")
+ {
+ EventSet interesting_bunch{&e2, &e4, &e7, &e8};
+
+ maximal_subsets_iterator first(C, [&](const UnfoldingEvent* e) { return interesting_bunch.contains(e); });
+ maximal_subsets_iterator last;
+
+ for (; first != last; ++first) {
+ const auto& event_set = *first;
+ // Only events in `interesting_bunch` can appear: thus no set
+ // should include anything else other than `interesting_bunch`
+ REQUIRE(event_set.is_subset_of(interesting_bunch));
+ REQUIRE(event_set.is_maximal_event_set());
+ maximal_subset_counts[event_set.size()]++;
+ }
+
+ // The empty set should (still) appear only once
+ REQUIRE(maximal_subset_counts[0] == 1);
+
+ // 4 is the number of nodes in the `interesting_bunch`
+ REQUIRE(maximal_subset_counts[1] == 4);
+
+ // 5 = 2 * 2 (each of the left branch can combine with one in the right branch) + 1 (e7 + e8)
+ REQUIRE(maximal_subset_counts[2] == 5);
+
+ // e7 + e8 must be included, so that means we can combine from the left branch (only e2 and e4)
+ REQUIRE(maximal_subset_counts[3] == 2);
+
+ // There are no subsets of size 4 (or higher, but that
+ // is tested by asserting each maximal set traversed is a subset)
+ REQUIRE(maximal_subset_counts[4] == 0);
+ }
+
+ SECTION("Filter with interesting subset not initially part of the maximal set")
+ {
+ EventSet interesting_bunch{&e3, &e5, &e6};
+
+ maximal_subsets_iterator first(C, [&](const UnfoldingEvent* e) { return interesting_bunch.contains(e); });
+ maximal_subsets_iterator last;
+
+ for (; first != last; ++first) {
+ const auto& event_set = *first;
+ // Only events in `interesting_bunch` can appear: thus no set
+ // should include anything else other than `interesting_bunch`
+ REQUIRE(event_set.is_subset_of(interesting_bunch));
+ REQUIRE(event_set.is_maximal_event_set());
+ maximal_subset_counts[event_set.size()]++;
+ }
+
+ // The empty set should (still) appear only once
+ REQUIRE(maximal_subset_counts[0] == 1);
+
+ // 3 is the number of nodes in the `interesting_bunch`
+ REQUIRE(maximal_subset_counts[1] == 3);
+
+ // 2 = e3, e5 and e3, e6
+ REQUIRE(maximal_subset_counts[2] == 2);
+
+ // There are no subsets of size 3 (or higher, but that
+ // is tested by asserting each maximal set traversed is a subset)
+ REQUIRE(maximal_subset_counts[3] == 0);
+ }
+ }
+}
+
+TEST_CASE("simgrid::mc::udpor::maximal_subsets_iterator: Stress Test for Maximal Subsets Iteration")
+{
+ // The following tests concern the given event structure:
+ // e1
+ // / /
+ // e2 e3
+ // / / / /
+ // +------* e4 *e5 e6 e7
+ // | / /// / /
+ // | e8 e9 e10
+ // | / / /\ /
+ // | e11 e12 e13 e14 e15
+ // | / / / / / /
+ // +-> e16 e17 e18
+ UnfoldingEvent e1;
+ UnfoldingEvent e2{&e1};
+ UnfoldingEvent e3{&e1};
+ UnfoldingEvent e4{&e2};
+ UnfoldingEvent e5{&e2};
+ UnfoldingEvent e6{&e3};
+ UnfoldingEvent e7{&e3};
+ UnfoldingEvent e8{&e4};
+ UnfoldingEvent e9{&e4, &e5, &e6};
+ UnfoldingEvent e10{&e6, &e7};
+ UnfoldingEvent e11{&e8};
+ UnfoldingEvent e12{&e8};
+ UnfoldingEvent e13{&e9};
+ UnfoldingEvent e14{&e9};
+ UnfoldingEvent e15{&e10};
+ UnfoldingEvent e16{&e5, &e11};
+ UnfoldingEvent e17{&e12, &e13, &e14};
+ UnfoldingEvent e18{&e14, &e15};
+ Configuration C{&e1, &e2, &e3, &e4, &e5, &e6, &e7, &e8, &e9, &e10, &e11, &e12, &e13, &e14, &e15, &e16, &e17, &e18};
+
+ SECTION("Every subset iterated over is maximal")
+ {
+ maximal_subsets_iterator first(C);
+ maximal_subsets_iterator last;
+
+ // Make sure we actually have something to iterate over
+ REQUIRE(first != last);
+
+ for (; first != last; ++first) {
+ REQUIRE((*first).size() <= C.get_events().size());
+ REQUIRE((*first).is_maximal_event_set());
+ }
+ }
}
\ No newline at end of file
EventSet::EventSet(Configuration&& config) : EventSet(config.get_events()) {}
-void EventSet::remove(UnfoldingEvent* e)
+void EventSet::remove(const UnfoldingEvent* e)
{
this->events_.erase(e);
}
EventSet EventSet::subtracting(const EventSet& other) const
{
- std::unordered_set<UnfoldingEvent*> result = this->events_;
+ std::unordered_set<const UnfoldingEvent*> result = this->events_;
- for (UnfoldingEvent* e : other.events_)
+ for (const UnfoldingEvent* e : other.events_)
result.erase(e);
return EventSet(std::move(result));
return subtracting(config.get_events());
}
-EventSet EventSet::subtracting(UnfoldingEvent* e) const
+EventSet EventSet::subtracting(const UnfoldingEvent* e) const
{
auto result = this->events_;
result.erase(e);
return EventSet(std::move(result));
}
-void EventSet::insert(UnfoldingEvent* e)
+void EventSet::insert(const UnfoldingEvent* e)
{
this->events_.insert(e);
}
form_union(config.get_events());
}
-EventSet EventSet::make_union(UnfoldingEvent* e) const
+EventSet EventSet::make_union(const UnfoldingEvent* e) const
{
auto result = this->events_;
result.insert(e);
EventSet EventSet::make_union(const EventSet& other) const
{
- std::unordered_set<UnfoldingEvent*> result = this->events_;
+ std::unordered_set<const UnfoldingEvent*> result = this->events_;
- for (UnfoldingEvent* e : other.events_)
+ for (const UnfoldingEvent* e : other.events_)
result.insert(e);
return EventSet(std::move(result));
return this->events_.empty();
}
-bool EventSet::contains(UnfoldingEvent* e) const
+bool EventSet::contains(const UnfoldingEvent* e) const
{
return this->events_.find(e) != this->events_.end();
}
{
/// @invariant: A collection of events `E` is a configuration
/// if and only if following while following the history of
- /// each event `e` of `E`you remain in `E`. In other words, you
+ /// each event `e` of `E` you remain in `E`. In other words, you
/// only see events from set `E`
///
- /// The proof is based on the definition of a configuration
- /// which requires that all
+ /// The simple proof is based on the definition of a configuration
+ /// which requires that all events have their history contained
+ /// in the set
const History history(*this);
return this->contains(history);
}
bool EventSet::contains(const History& history) const
{
- return std::all_of(history.begin(), history.end(), [=](UnfoldingEvent* e) { return this->contains(e); });
+ return std::all_of(history.begin(), history.end(), [=](const UnfoldingEvent* e) { return this->contains(e); });
}
bool EventSet::is_maximal_event_set() const
#include <cstddef>
#include <initializer_list>
#include <unordered_set>
+#include <vector>
namespace simgrid::mc::udpor {
class EventSet {
private:
- std::unordered_set<UnfoldingEvent*> events_;
+ std::unordered_set<const UnfoldingEvent*> events_;
public:
EventSet() = default;
EventSet& operator=(EventSet&&) = default;
EventSet(EventSet&&) = default;
explicit EventSet(Configuration&& config);
- explicit EventSet(std::unordered_set<UnfoldingEvent*>&& raw_events) : events_(raw_events) {}
- explicit EventSet(std::initializer_list<UnfoldingEvent*> event_list) : events_(std::move(event_list)) {}
+ explicit EventSet(std::vector<const UnfoldingEvent*>&& raw_events) : events_(raw_events.begin(), raw_events.end()) {}
+ explicit EventSet(std::unordered_set<const UnfoldingEvent*>&& raw_events) : events_(raw_events) {}
+ explicit EventSet(std::initializer_list<const UnfoldingEvent*> event_list) : events_(std::move(event_list)) {}
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(); }
- void remove(UnfoldingEvent*);
+ void remove(const UnfoldingEvent*);
void subtract(const EventSet&);
void subtract(const Configuration&);
- EventSet subtracting(UnfoldingEvent*) const;
+ EventSet subtracting(const UnfoldingEvent*) const;
EventSet subtracting(const EventSet&) const;
EventSet subtracting(const Configuration&) const;
- void insert(UnfoldingEvent*);
+ void insert(const UnfoldingEvent*);
void form_union(const EventSet&);
void form_union(const Configuration&);
- EventSet make_union(UnfoldingEvent*) const;
+ EventSet make_union(const UnfoldingEvent*) const;
EventSet make_union(const EventSet&) const;
EventSet make_union(const Configuration&) const;
size_t size() const;
bool empty() const;
- bool contains(UnfoldingEvent*) const;
+ bool contains(const UnfoldingEvent*) const;
bool contains(const History&) const;
bool is_subset_of(const EventSet&) const;
* @brief Whether or not this set of events is
* a *maximal event set*, i.e. whether each element
* of the set causes none of the others
+ *
+ * A set of events `E` is said to be _maximal_ if
+ * it is causally-free. Formally,
+ *
+ * 1. For each event `e` in `E`, there is no event
+ * `e'` in `E` such that `e < e'`
*/
bool is_maximal_event_set() const;
};
// and all subsequent events that are added by the iterator
}
-History::Iterator& History::Iterator::operator++()
+void History::Iterator::increment()
{
if (not frontier.empty()) {
// "Pop" the event at the "front"
- UnfoldingEvent* e = *frontier.begin();
+ const UnfoldingEvent* e = *frontier.begin();
frontier.remove(e);
// If there is a configuration and if the
// be searched since the configuration contains
// them (configuration invariant)
if (configuration.has_value() && configuration->get().contains(e)) {
- return *this;
+ return;
}
// Mark this event as seen
candidates.subtract(current_history);
frontier.form_union(candidates);
}
- return *this;
+}
+
+const UnfoldingEvent* const& History::Iterator::dereference() const
+{
+ return *frontier.begin();
+}
+
+bool History::Iterator::equal(const Iterator& other) const
+{
+ // If what the iterator sees next is the same, we consider them
+ // to be the same iterator. This way, once the iterator has completed
+ // its search, it will be "equal" to an iterator searching nothing
+ return this->frontier == other.frontier;
}
EventSet History::get_all_events() const
#include "src/mc/explo/udpor/EventSet.hpp"
#include "src/mc/explo/udpor/udpor_forward.hpp"
+#include <boost/iterator/iterator_facade.hpp>
#include <functional>
#include <optional>
History& operator=(History const&) = default;
History(History&&) = default;
- explicit History(UnfoldingEvent* e) : events_({e}) {}
explicit History(EventSet event_set = EventSet()) : events_(std::move(event_set)) {}
+ explicit History(const UnfoldingEvent* e) : events_({e}) {}
auto begin() const { return Iterator(events_); }
auto end() const { return Iterator(EventSet()); }
/**
* @brief An iterator which traverses the history of a set of events
*/
- struct Iterator {
+ struct Iterator : boost::iterator_facade<Iterator, const UnfoldingEvent* const, boost::forward_traversal_tag> {
public:
- Iterator& operator++();
- auto operator->() const { return frontier.begin().operator->(); }
- auto operator*() const { return *frontier.begin(); }
-
- // If what the iterator sees next is the same, we consider them
- // to be the same iterator. This way, once the iterator has completed
- // its search, it will be "equal" to an iterator searching nothing
- bool operator==(const Iterator& other) const { return this->frontier == other.frontier; }
- bool operator!=(const Iterator& other) const { return not(this->operator==(other)); }
-
- using iterator_category = std::forward_iterator_tag;
- using difference_type = int; // # of steps between
- using value_type = UnfoldingEvent*;
- using pointer = value_type*;
- using reference = value_type&;
using optional_configuration = std::optional<std::reference_wrapper<const Configuration>>;
-
Iterator(const EventSet& initial_events, optional_configuration config = std::nullopt);
private:
EventSet current_history = EventSet();
/// @brief What the iterator currently believes
+ // to be the set of maximal events
EventSet maximal_events;
optional_configuration configuration;
+
+ // boost::iterator_facade<...> interface to implement
+ void increment();
+ bool equal(const Iterator& other) const;
+
+ const UnfoldingEvent* const& dereference() const;
+
+ // Allows boost::iterator_facade<...> to function properly
+ friend class boost::iterator_core_access;
+
+ // Allow the `History` class to use some of the
+ // computation of the iterator
friend History;
};
};
* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
+#include "src/mc/explo/udpor/History.hpp"
namespace simgrid::mc::udpor {
-UnfoldingEvent::UnfoldingEvent(std::initializer_list<UnfoldingEvent*> init_list)
+UnfoldingEvent::UnfoldingEvent(std::initializer_list<const UnfoldingEvent*> init_list)
: UnfoldingEvent(EventSet(std::move(init_list)))
{
}
return this->immediate_causes == other.immediate_causes;
}
+EventSet UnfoldingEvent::get_history() const
+{
+ return History(this).get_all_events();
+}
+
} // namespace simgrid::mc::udpor
class UnfoldingEvent {
public:
- explicit UnfoldingEvent(std::initializer_list<UnfoldingEvent*> init_list);
+ explicit UnfoldingEvent(std::initializer_list<const UnfoldingEvent*> init_list);
UnfoldingEvent(EventSet immediate_causes = EventSet(),
std::shared_ptr<Transition> transition = std::make_unique<Transition>());
--- /dev/null
+#include "src/mc/explo/udpor/maximal_subsets_iterator.hpp"
+#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
+#include "xbt/asserts.h"
+
+#include <algorithm>
+
+namespace simgrid::mc::udpor {
+
+maximal_subsets_iterator::maximal_subsets_iterator(const Configuration& config,
+ std::optional<node_filter_function> filter)
+ : config({config}), current_maximal_set({EventSet()})
+{
+ const auto candidate_ordering = config.get_topologically_sorted_events_of_reverse_graph();
+ if (filter.has_value()) {
+ // Only store the events in the ordering that "matter" to us
+ std::copy_if(std::move_iterator(candidate_ordering.begin()), std::move_iterator(candidate_ordering.end()),
+ std::back_inserter(topological_ordering), filter.value());
+ } else {
+ topological_ordering = std::move(candidate_ordering);
+ }
+}
+
+void maximal_subsets_iterator::increment()
+{
+ if (current_maximal_set == std::nullopt) {
+ return;
+ }
+
+ if (topological_ordering.empty()) {
+ // Stop immediately if there's nothing to search
+ current_maximal_set = std::nullopt;
+ return;
+ }
+
+ const auto next_event_ref = [&]() {
+ if (!has_started_searching) {
+ has_started_searching = true;
+ return bookkeeper.find_next_candidate_event(topological_ordering.begin(), topological_ordering.end());
+ } else {
+ return continue_traversal_of_maximal_events_tree();
+ }
+ }();
+
+ if (next_event_ref == topological_ordering.end()) {
+ current_maximal_set = std::nullopt;
+ return;
+ }
+
+ // We found some other event `e'` which is not in causally related with anything
+ // that currently exists in `current_maximal_set`, so add it in
+ add_element_to_current_maximal_set(*next_event_ref);
+ backtrack_points.push(next_event_ref);
+}
+
+maximal_subsets_iterator::topological_order_position
+maximal_subsets_iterator::continue_traversal_of_maximal_events_tree()
+{
+ // Nothing needs to be done if there isn't anyone to search for...
+ if (backtrack_points.empty()) {
+ return topological_ordering.end();
+ }
+
+ // 1. First, check if we can keep expanding from the
+ // maximal set that we currently have
+ {
+ // This is an iterator which points to the latest event `e` that
+ // was added to what is currently the maximal set
+ const auto latest_event_ref = backtrack_points.top();
+
+ // Look for the next event to test with what we currently
+ // have based on the conflicts we've already kept track of.
+ //
+ // NOTE: We only need to search FROM `e` and not
+ // from the beginning of the topological sort. The fact that the
+ // set is topologically ordered ensures that removing `e`
+ // will not change whether or not to now allow someone before `e`
+ // in the ordering (otherwise, they would have to be in `e`'s history
+ // and therefore would come after `e`)
+ const auto next_event_ref = bookkeeper.find_next_candidate_event(latest_event_ref, topological_ordering.end());
+
+ // If we can expand from what we currently have, we can stop
+ if (next_event_ref != topological_ordering.end()) {
+ return next_event_ref;
+ }
+ }
+
+ // Otherwise, we backtrack: we repeatedly pop off events that we know we
+ // are finished with
+ while (not backtrack_points.empty()) {
+ // Note: it is important to remove the element FIRST before performing
+ // the search, as removal may enable dependencies of `e` to be selected
+ const auto latest_event_ref = backtrack_points.top();
+ remove_element_from_current_maximal_set(*latest_event_ref);
+ backtrack_points.pop();
+
+ // We begin the search AFTER the event we popped: we only want
+ // to consider those events that could be added AFTER `e` and
+ // not `e` itself again
+ const auto next_event_ref = bookkeeper.find_next_candidate_event(latest_event_ref + 1, topological_ordering.end());
+ if (next_event_ref != topological_ordering.end()) {
+ return next_event_ref;
+ }
+ }
+ return topological_ordering.end();
+}
+
+bool maximal_subsets_iterator::bookkeeper::is_candidate_event(const UnfoldingEvent* e) const
+{
+ if (const auto e_count = event_counts.find(e); e_count != event_counts.end()) {
+ return e_count->second == 0;
+ }
+ return true;
+}
+
+void maximal_subsets_iterator::add_element_to_current_maximal_set(const UnfoldingEvent* e)
+{
+ xbt_assert(current_maximal_set.has_value(), "Attempting to add an event to the maximal set "
+ "when iteration has completed. This indicates that "
+ "the termination condition for the iterator is broken");
+ current_maximal_set.value().insert(e);
+ bookkeeper.mark_included_in_maximal_set(e);
+}
+
+void maximal_subsets_iterator::remove_element_from_current_maximal_set(const UnfoldingEvent* e)
+{
+ xbt_assert(current_maximal_set.has_value(), "Attempting to remove an event to the maximal set "
+ "when iteration has completed. This indicates that "
+ "the termination condition for the iterator is broken");
+ current_maximal_set.value().remove(e);
+ bookkeeper.mark_removed_from_maximal_set(e);
+}
+
+maximal_subsets_iterator::topological_order_position
+maximal_subsets_iterator::bookkeeper::find_next_candidate_event(topological_order_position first,
+ topological_order_position last) const
+{
+ return std::find_if(first, last, [&](const UnfoldingEvent* e) { return is_candidate_event(e); });
+}
+
+void maximal_subsets_iterator::bookkeeper::mark_included_in_maximal_set(const UnfoldingEvent* e)
+{
+ const auto e_history = e->get_history();
+ for (const auto e_hist : e_history) {
+ event_counts[e_hist]++;
+ }
+}
+
+void maximal_subsets_iterator::bookkeeper::mark_removed_from_maximal_set(const UnfoldingEvent* e)
+{
+ const auto e_history = e->get_history();
+ for (const auto e_hist : e_history) {
+ xbt_assert(event_counts.find(e_hist) != event_counts.end(),
+ "Invariant Violation: Attempted to remove an event which was not previously added");
+ xbt_assert(event_counts[e_hist] > 0, "Invariant Violation: An event `e` had a count of `0` at this point "
+ "of the bookkeeping, which means that it is a candidate maximal event. "
+ "Yet some event that `e'` which contains `e` in its history was removed "
+ "first. This incidates that the topological sorting of events of the "
+ "configuration has failed and should be investigated first");
+ event_counts[e_hist]--;
+ }
+}
+
+} // namespace simgrid::mc::udpor
\ No newline at end of file
--- /dev/null
+/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef SIMGRID_MC_UDPOR_MAXIMAL_SUBSETS_ITERATOR_HPP
+#define SIMGRID_MC_UDPOR_MAXIMAL_SUBSETS_ITERATOR_HPP
+
+#include "src/mc/explo/udpor/Configuration.hpp"
+
+#include <boost/iterator/iterator_facade.hpp>
+#include <optional>
+#include <stack>
+#include <unordered_map>
+
+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
+ *
+ * This iterator traverses all possible sets of maximal events that
+ * can be formed from a configuration, 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
+ * whose identity is not "exploitable" (i.e. one whose type information cannot
+ * help us narrow down our search).
+ */
+struct maximal_subsets_iterator
+ : public boost::iterator_facade<maximal_subsets_iterator, const EventSet, boost::forward_traversal_tag> {
+public:
+ // A function which answers the question "do I need to consider maximal sets
+ // that contain this node?"
+ using node_filter_function = std::function<bool(const UnfoldingEvent*)>;
+ using topological_order_position = std::vector<const UnfoldingEvent*>::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<node_filter_function> filter);
+
+private:
+ const std::optional<std::reference_wrapper<const Configuration>> config;
+ std::vector<const UnfoldingEvent*> 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<EventSet> current_maximal_set = std::nullopt;
+ std::stack<topological_order_position> backtrack_points = std::stack<topological_order_position>();
+
+ /**
+ * @brief A small class which provides functionality for managing
+ * the "counts" as the iterator proceeds forward in time
+ *
+ * As an instance of the `maximal_subsets_iterator` traverses
+ * the configuration, it keeps track of how many events
+ * further down in the causality tree have been signaled as in-conflict
+ * with events that are its current maximal event set (i.e.
+ * its `current_maximal_set`)
+ */
+ 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,
+ topological_order_position last) const;
+
+ private:
+ std::unordered_map<const UnfoldingEvent*, unsigned> event_counts;
+
+ /// @brief Whether or not the given event, according to the
+ /// bookkeeping that has been done thus far, can be added to the
+ /// current candidate maximal set
+ bool is_candidate_event(const UnfoldingEvent*) const;
+
+ } bookkeeper;
+
+ void add_element_to_current_maximal_set(const UnfoldingEvent*);
+ void remove_element_from_current_maximal_set(const UnfoldingEvent*);
+
+ /**
+ * @brief Moves to the next node in the topological ordering
+ * by continuing the search in the tree of maximal event sets
+ * from where we currently believe we are in the tree
+ *
+ * At each stage of the iteration, the iterator points to
+ * a maximal event set that can be thought of as `R` + `A`:
+ *
+ * | R | A
+ * +--------+
+ *
+ * where `R` is some set of events and `A` is another event.
+ *
+ * The iterator first tries expansion from `R` + `A`. If it finds
+ * node `B` to expand, this means that there is a node in the tree of
+ * maximal event sets of `C` (the configuration traversed) such that
+ * `R` + `A` + `B` needs to be checked.
+ *
+ * If no such node is found, then the iterator must check `R` +
+ * some other node AFTER `A`. The new set of possibilities potentially
+ * includes some of `A`'s dependencies, so their counts are decremented
+ * prior to searching.
+ *
+ * @note: This method is a mutating method: it manipulates the
+ * iterator such that the iterator refers to the next maximal
+ * set sans the element returned. The `increment()` function performs
+ * the rest of the work needed to actually complete the transition
+ *
+ * @returns an iterator poiting to the event that should next
+ * be added to the set of maximal events if such an event exists,
+ * or to the end of the topological ordering if no such event exists
+ */
+ topological_order_position continue_traversal_of_maximal_events_tree();
+
+ // boost::iterator_facade<...> interface to implement
+ void increment();
+ bool equal(const maximal_subsets_iterator& other) const { return current_maximal_set == other.current_maximal_set; }
+ const EventSet& dereference() const
+ {
+ static const EventSet empty_set = EventSet();
+ if (current_maximal_set.has_value()) {
+ return current_maximal_set.value();
+ }
+ return empty_set;
+ }
+
+ // Allows boost::iterator_facade<...> to function properly
+ friend class boost::iterator_core_access;
+};
+
+} // namespace simgrid::mc::udpor
+#endif
src/mc/explo/udpor/EventSet.hpp
src/mc/explo/udpor/History.cpp
src/mc/explo/udpor/History.hpp
+ src/mc/explo/udpor/maximal_subsets_iterator.cpp
+ src/mc/explo/udpor/maximal_subsets_iterator.hpp
src/mc/explo/udpor/UnfoldingEvent.cpp
src/mc/explo/udpor/UnfoldingEvent.hpp
src/mc/explo/udpor/Unfolding.cpp
