#include "xbt/asserts.h"
#include <algorithm>
-#include <stack>
#include <stdexcept>
namespace simgrid::mc::udpor {
std::vector<const UnfoldingEvent*> Configuration::get_topologically_sorted_events() const
{
- // This is essentially an implementation of detecting cycles
- // in a graph with coloring, except it makes a topological
- // ordering out of it
-
- if (events_.empty()) {
- return std::vector<const UnfoldingEvent*>();
- }
-
- std::stack<const UnfoldingEvent*> event_stack;
- std::vector<const UnfoldingEvent*> topological_ordering;
- EventSet unknown_events = events_;
- EventSet temporarily_marked_events;
- EventSet permanently_marked_events;
-
- while (not unknown_events.empty()) {
- EventSet discovered_events;
- event_stack.push(*unknown_events.begin());
-
- while (not event_stack.empty()) {
- const UnfoldingEvent* evt = event_stack.top();
- discovered_events.insert(evt);
-
- if (not temporarily_marked_events.contains(evt)) {
- // If this event hasn't yet been marked, do
- // so now so that if we both see it
- // again in a child we can detect a cycle
- temporarily_marked_events.insert(evt);
-
- EventSet immediate_causes = evt->get_immediate_causes();
- if (!immediate_causes.empty() && immediate_causes.is_subset_of(temporarily_marked_events)) {
- throw std::invalid_argument("Attempted to perform a topological sort on a configuration "
- "whose contents contain a cycle. The configuration (and the graph "
- "connecting all of the events) is an invalid event structure");
- }
- immediate_causes.subtract(discovered_events);
- immediate_causes.subtract(permanently_marked_events);
- std::for_each(immediate_causes.begin(), immediate_causes.end(),
- [&event_stack](const UnfoldingEvent* cause) { event_stack.push(cause); });
- } else {
- unknown_events.remove(evt);
- temporarily_marked_events.remove(evt);
- permanently_marked_events.insert(evt);
-
- // In moving this event to the end of the list,
- // we are saying this events "happens before" other
- // events that are added later.
- topological_ordering.push_back(evt);
-
- // Only now do we remove the event, i.e. once
- // we've processed the same event twice
- event_stack.pop();
- }
- }
- }
- return topological_ordering;
+ return this->events_.get_topological_ordering();
}
std::vector<const UnfoldingEvent*> Configuration::get_topologically_sorted_events_of_reverse_graph() const
{
- // 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.
- auto topological_events = get_topologically_sorted_events();
- std::reverse(topological_events.begin(), topological_events.end());
- return topological_events;
+ return this->events_.get_topological_ordering_of_reverse_graph();
}
EventSet Configuration::get_minimally_reproducible_events() const
#include "src/mc/explo/udpor/EventSet.hpp"
#include "src/mc/explo/udpor/Configuration.hpp"
#include "src/mc/explo/udpor/History.hpp"
+#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
#include <iterator>
+#include <stack>
namespace simgrid::mc::udpor {
return *this == history.get_all_maximal_events();
}
+bool EventSet::is_conflict_free() const
+{
+ return false;
+}
+
+std::vector<const UnfoldingEvent*> EventSet::get_topological_ordering() const
+{
+ // This is essentially an implementation of detecting cycles
+ // in a graph with coloring, except it makes a topological
+ // ordering out of it
+ if (empty()) {
+ return std::vector<const UnfoldingEvent*>();
+ }
+
+ std::stack<const UnfoldingEvent*> event_stack;
+ std::vector<const UnfoldingEvent*> topological_ordering;
+ EventSet unknown_events = *this;
+ EventSet temporarily_marked_events;
+ EventSet permanently_marked_events;
+
+ while (not unknown_events.empty()) {
+ EventSet discovered_events;
+ event_stack.push(*unknown_events.begin());
+
+ while (not event_stack.empty()) {
+ const UnfoldingEvent* evt = event_stack.top();
+ discovered_events.insert(evt);
+
+ if (not temporarily_marked_events.contains(evt)) {
+ // If this event hasn't yet been marked, do
+ // so now so that if we both see it
+ // again in a child we can detect a cycle
+ temporarily_marked_events.insert(evt);
+
+ EventSet immediate_causes = evt->get_immediate_causes();
+ if (!immediate_causes.empty() && immediate_causes.is_subset_of(temporarily_marked_events)) {
+ throw std::invalid_argument("Attempted to perform a topological sort on a configuration "
+ "whose contents contain a cycle. The configuration (and the graph "
+ "connecting all of the events) is an invalid event structure");
+ }
+ immediate_causes.subtract(discovered_events);
+ immediate_causes.subtract(permanently_marked_events);
+ std::for_each(immediate_causes.begin(), immediate_causes.end(),
+ [&event_stack](const UnfoldingEvent* cause) { event_stack.push(cause); });
+ } else {
+ unknown_events.remove(evt);
+ temporarily_marked_events.remove(evt);
+ permanently_marked_events.insert(evt);
+
+ // In moving this event to the end of the list,
+ // we are saying this events "happens before" other
+ // events that are added later.
+ if (this->contains(evt)) {
+ topological_ordering.push_back(evt);
+ }
+
+ // Only now do we remove the event, i.e. once
+ // we've processed the same event twice
+ event_stack.pop();
+ }
+ }
+ }
+ return topological_ordering;
+}
+
+std::vector<const UnfoldingEvent*> EventSet::get_topological_ordering_of_reverse_graph() const
+{
+ // 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.
+ auto topological_events = get_topological_ordering();
+ std::reverse(topological_events.begin(), topological_events.end());
+ return topological_events;
+}
+
} // namespace simgrid::mc::udpor
\ No newline at end of file
* `e'` in `E` such that `e < e'`
*/
bool is_maximal() const;
+
+ /**
+ * @brief Whether or not this set of events is
+ * free of conflicts
+ *
+ * A set of events `E` is said to be _conflict free_
+ * if
+ *
+ * 1. For each event `e` in `E`, there is no event
+ * `e'` in `E` such that `e # e'` where `#` is the
+ * conflict relation over the unfolding from
+ * which the events `E` are derived
+ *
+ * @note: This method makes use only of the causality
+ * tree of the events in the set; i.e. it determines conflicts
+ * based solely on the unfolding and the definition of
+ * conflict in an unfolding. Some clever techniques
+ * exist for computing conflicts with specialized transition
+ * types (only mutexes if I remember correctly) that was
+ * referenced in The Anh Pham's thesis. This would require
+ * keeping track of information *outside* of any given
+ * set and probably doesn't work for all types of transitions
+ * anyway.
+ */
+ bool is_conflict_free() const;
+
+ /**
+ * @brief Orders the events of the set such that
+ * "more recent" events (i.e. those that are farther down in
+ * the event structure's dependency chain) come after those
+ * that appeared "farther in the past"
+ *
+ * @returns a vector `V` with the following property:
+ *
+ * 1. Let i(e) := C -> I map events to their indices in `V`.
+ * For every pair of events e, e' in C, if e < e' then i(e) < i(e')
+ *
+ * Intuitively, events that are closer to the "bottom" of the event
+ * structure appear farther along in the list than those that appear
+ * closer to the "top"
+ */
+ std::vector<const UnfoldingEvent*> get_topological_ordering() const;
+
+ /**
+ * @brief Orders the events of set such that
+ * "more recent" events (i.e. those that are farther down in
+ * the event structure's dependency chain) come before those
+ * that appear "farther in the past"
+ *
+ * @note The events of the event structure are arranged such that
+ * e < e' implies a directed edge from e to e'. However, it is
+ * also useful to be able to traverse the *reverse* graph (for
+ * example when computing the compatibility graph of a configuration),
+ * hence the distinction between "reversed" and the method
+ * "EventSet::get_topological_ordering()"
+ *
+ * @returns a vector `V` with the following property:
+ *
+ * 1. Let i(e) := C -> I map events to their indices in `V`.
+ * For every pair of events e, e' in C, if e < e' then i(e) > i(e')
+ *
+ * Intuitively, events that are closer to the "top" of the event
+ * structure appear farther along in the list than those that appear
+ * closer to the "bottom"
+ */
+ std::vector<const UnfoldingEvent*> get_topological_ordering_of_reverse_graph() const;
};
} // namespace simgrid::mc::udpor
