#include "src/mc/explo/udpor/Configuration.hpp"
#include "src/mc/explo/udpor/History.hpp"
#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
+#include "xbt/asserts.h"
#include <algorithm>
#include <stack>
{
}
-Configuration::Configuration(EventSet events) : events_(events)
+Configuration::Configuration(const EventSet& events) : events_(events)
{
if (!events_.is_valid_configuration()) {
throw std::invalid_argument("The events do not form a valid configuration");
}
}
-std::vector<UnfoldingEvent*> Configuration::get_topogolically_sorted_events_of_reverse_graph() const
+std::vector<UnfoldingEvent*> Configuration::get_topologically_sorted_events() const
{
if (events_.empty()) {
return std::vector<UnfoldingEvent*>();
// detect a cycle and if we see it again here
// we can detect that the node is re-processed
temporarily_marked_events.insert(evt);
- } else {
+ 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);
+ const EventSet undiscovered_causes = std::move(immediate_causes);
+
+ for (const auto cause : undiscovered_causes) {
+ event_stack.push(cause);
+ }
+ } else {
// Mark this event as:
// 1. discovered across all DFSs performed
- // 2. part of the topological search
+ // 2. permanently marked
+ // 3. part of the topological search
+ 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 again
event_stack.pop();
}
+ }
+ }
+ return topological_ordering;
+}
- const EventSet immediate_causes = evt->get_immediate_causes();
- if (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");
- }
- const EventSet undiscovered_causes = std::move(immediate_causes).subtracting(discovered_events);
+std::vector<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
+ // 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;
+}
- for (const auto cause : undiscovered_causes) {
- event_stack.push(cause);
+std::unique_ptr<CompatibilityGraph>
+Configuration::make_compatibility_graph_filtered_on(std::function<bool(UnfoldingEvent*)> pred) const
+{
+ auto G = std::make_unique<CompatibilityGraph>();
+
+ struct UnfoldingEventSearchData {
+ int immediate_children_count = 0;
+ CompatibilityGraphNode* potential_placement = nullptr;
+ std::unordered_set<CompatibilityGraphNode*> conflicts = std::unordered_set<CompatibilityGraphNode*>();
+ };
+ std::unordered_map<UnfoldingEvent*, UnfoldingEventSearchData> search_data;
+
+ for (auto* e : get_topologically_sorted_events_of_reverse_graph()) {
+
+ // 1. Figure out where to place `e` in `G`
+
+ // Determine which nodes in the graph are in conflict
+ // with this event. These nodes would have been added by child
+ // events while iterating over the topological ordering of the reverse graph
+
+ const auto e_search_data_loc = search_data.find(e);
+ const bool e_has_no_search_data = e_search_data_loc == search_data.end();
+ const auto e_search_data = e_has_no_search_data ? UnfoldingEventSearchData() : std::move(e_search_data_loc->second);
+
+ const auto& e_conflicts = e_search_data.conflicts;
+ const auto& e_potential_placement = e_search_data.potential_placement;
+ const auto e_child_count = e_search_data.immediate_children_count;
+
+ CompatibilityGraphNode* e_placement = nullptr;
+
+ // The justification is as follows:
+ //
+ // e_has_no_search_data:
+ // If nobody told us about a placement, we must either be a leaf event
+ // OR be the cause of an event that itself has more than one cause.
+ //
+ // child_count >= 2:
+ // If there are two or more events that this event causes,
+ // then we certainly must be part of a different compatibility
+ // graph node since
+ const bool new_placement_required = e_has_no_search_data || e_child_count >= 2;
+
+ if (new_placement_required) {
+ auto new_graph_node = std::make_unique<CompatibilityGraphNode>(e_conflicts, EventSet({e}));
+ e_placement = new_graph_node.get();
+ G->insert(std::move(new_graph_node));
+ } else {
+ xbt_assert(e_child_count == 1, "An event was informed by an immediate child of placement in "
+ "the same compatibility graph node, yet the child did not inform "
+ "the parent about its precense");
+ // A child event told us this node can be in the
+ // same compatibility node in the graph G. Add ourselves now
+ e_placement = e_potential_placement;
+ e_placement->add_event(e);
+ }
+
+ // 2. Update the children of `e`
+
+ const EventSet& e_immediate_causes = e->get_immediate_causes();
+ if (e_immediate_causes.size() == 1) {
+ // If there is only a single ancestor, then it MAY BE in
+ // the same "chain" of events as us. Note that the ancestor must
+ // also have only a single child (see the note on `new_placement_required`)
+ UnfoldingEvent* only_ancestor = *e_immediate_causes.begin();
+ search_data[only_ancestor].potential_placement = e_placement;
+ }
+
+ // Our ancestors conflict with everyone `e` does else PLUS `e` itself
+ auto parent_conflicts = std::move(e_conflicts);
+ parent_conflicts.insert(e_placement);
+ for (auto* cause : e_immediate_causes) {
+ search_data[cause].immediate_children_count += 1;
+
+ for (auto parent_conflict : parent_conflicts) {
+ search_data[cause].conflicts.insert(parent_conflict);
}
}
+
+ // This event will only ever be seen once in the
+ // topological ordering. Hence, its resources do not
+ // need to be kept around
+ search_data.erase(e);
}
- return topological_ordering;
+ return G;
}
} // namespace simgrid::mc::udpor
