include src/mc/explo/udpor/History.cpp
include src/mc/explo/udpor/History.hpp
include src/mc/explo/udpor/History_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/Unfolding.cpp
include src/mc/explo/udpor/Unfolding.hpp
include src/mc/explo/udpor/UnfoldingEvent.cpp
events_seen.insert(e);
});
}
+
+ SECTION("Test that the topological ordering contains only the events of the configuration") {}
}
\ No newline at end of file
* 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 {
return this->immediate_causes == other.immediate_causes;
}
+EventSet UnfoldingEvent::get_history()
+{
+ return History(this).get_all_events();
+}
+
} // namespace simgrid::mc::udpor
UnfoldingEvent& operator=(UnfoldingEvent const&) = default;
UnfoldingEvent(UnfoldingEvent&&) = default;
- EventSet get_history() const;
+ EventSet get_history();
bool in_history_of(const UnfoldingEvent* otherEvent) const;
bool conflicts_with(const UnfoldingEvent* otherEvent) const;
--- /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 {
+
+void maximal_subsets_iterator::increment()
+{
+ // Until we discover otherwise, we default to being done
+ auto next_event_ref = topological_ordering.end();
+
+ while (not backtrack_points.empty()) {
+ // 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`)
+ next_event_ref = bookkeeper.find_next_event(latest_event_ref, topological_ordering.end());
+
+ // If we can't find another event to add after `e`,
+ // then we retry after first removing the latest event.
+ // This effectively tests "check now with all combinations that
+ // exclude the latest event".
+ //
+ // Note: it is important to remove the element FIRST before performing
+ // the second search, as removal may enable dependencies of `e` to be selected
+ if (next_event_ref == topological_ordering.end()) {
+ 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
+ next_event_ref = bookkeeper.find_next_event(latest_event_ref + 1, topological_ordering.end());
+
+ // If we finally found some event, we can stop
+ if (next_event_ref != topological_ordering.end()) {
+ break;
+ }
+ }
+ }
+
+ // If after all of the backtracking we still have no luck, we've finished
+ if (next_event_ref == topological_ordering.end()) {
+ return;
+ }
+
+ // Otherwise we found some other event `e'` which is not in conflict with anything
+ // that currently exists in `current_maximal_set`. Add it in and perform
+ // some more bookkeeping
+ UnfoldingEvent* next_event = *next_event_ref;
+ add_element_to_current_maximal_set(next_event);
+ backtrack_points.push(next_event_ref);
+}
+
+void maximal_subsets_iterator::add_element_to_current_maximal_set(UnfoldingEvent* e)
+{
+ current_maximal_set.insert(e);
+ bookkeeper.mark_included_in_maximal_set(e);
+}
+
+void maximal_subsets_iterator::remove_element_from_current_maximal_set(UnfoldingEvent* e)
+{
+ current_maximal_set.remove(e);
+ bookkeeper.mark_removed_from_maximal_set(e);
+}
+
+maximal_subsets_iterator::topological_order_position
+maximal_subsets_iterator::bookkeeper::find_next_event(topological_order_position first,
+ topological_order_position last) const
+{
+ return std::find_if(first, last, [&](UnfoldingEvent* e) { return is_candidate_event(e); });
+}
+
+bool maximal_subsets_iterator::bookkeeper::is_candidate_event(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::bookkeeper::mark_included_in_maximal_set(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(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 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*)>;
+
+ maximal_subsets_iterator();
+ maximal_subsets_iterator(const Configuration& config)
+ : maximal_subsets_iterator(
+ config, [](const UnfoldingEvent*) constexpr { return true; })
+ {
+ }
+
+ maximal_subsets_iterator(const Configuration& config, node_filter_function filter)
+ : config({config})
+ , topological_ordering(config.get_topologically_sorted_events_of_reverse_graph())
+ , filter(filter)
+ {
+ // The idea here is that initially, no work has been done; but we want
+ // it to be the case that the iterator points at the very first
+ // element in the list. Effectively, we want to take the first step
+ if (not topological_ordering.empty()) {
+ auto earliest_element_iter = topological_ordering.begin();
+ // add_element_to_current_maximal_set(*earliest_element_iter);
+ backtrack_points.push(earliest_element_iter);
+ }
+ }
+
+private:
+ using topological_order_position = std::vector<UnfoldingEvent*>::const_iterator;
+ const std::optional<std::reference_wrapper<const Configuration>> config;
+ const std::vector<UnfoldingEvent*> topological_ordering;
+ const std::optional<node_filter_function> filter;
+
+ EventSet current_maximal_set = EventSet();
+ std::stack<topological_order_position> backtrack_points;
+
+ /**
+ * @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 {
+ private:
+ using topological_order_position = maximal_subsets_iterator::topological_order_position;
+ std::unordered_map<UnfoldingEvent*, unsigned> event_counts;
+
+ bool is_candidate_event(UnfoldingEvent*) const;
+
+ public:
+ void mark_included_in_maximal_set(UnfoldingEvent*);
+ void mark_removed_from_maximal_set(UnfoldingEvent*);
+
+ topological_order_position find_next_event(topological_order_position first, topological_order_position last) const;
+ } bookkeeper;
+
+ void add_element_to_current_maximal_set(UnfoldingEvent*);
+ void remove_element_from_current_maximal_set(UnfoldingEvent*);
+
+ // 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 { return current_maximal_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
