#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");
return topological_events;
}
+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 G;
+}
+
} // namespace simgrid::mc::udpor
