1 /* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */
3 /* This program is free software; you can redistribute it and/or modify it
4 * under the terms of the license (GNU LGPL) which comes with this package. */
6 #ifndef SIMGRID_MC_UDPOR_COMPATIBILITY_GRAPH_HPP
7 #define SIMGRID_MC_UDPOR_COMPATIBILITY_GRAPH_HPP
9 #include "src/mc/explo/udpor/CompatibilityGraphNode.hpp"
10 #include "src/mc/explo/udpor/udpor_forward.hpp"
13 #include <unordered_map>
15 namespace simgrid::mc::udpor {
18 * @brief A graph which describes the causal-conflicts between groups of
19 * events from an unfolding
21 * A compatibility graph conceptually describes how causal "strands" of an
22 * event structure are related to one another. Each node in the graph
23 * represents a set of events from which only a single event could be selected
24 * if creating a new subset of the events of an unfolding which is *causally-free*.
25 * We say a set of events is *causally free* if and only if that set of events is a
26 * maximal set of events (i.e., the two conditions are equivalent). We write
27 * E(_node_) to denote the set of events associated with that node.
29 * The edges of the graph describe which "strands" are in causal conflict with one
30 * another. That is, if (u, v) is an edge of compatibility graph G, then at
31 * most one event from the set S(u) ∪ S(v) could be selected in a causally-free
32 * subset of events of an unfolding.
34 * An important property of a compatibility graph G is that the cliques of
35 * its complement graph G' (recall that the complement G' of a graph G is the
36 * graph which has an edge (u,v) whenever G lacks an edge (u,v))
37 * determine all possible combinations of events which are maximal events;
38 * i.e., a clique of size `k` in G' is such that all maximal event sets
39 * with events chosen from the union of all events mapped to each node in the
40 * clique can be formed. Thus, the problem of determining sets of maximal
41 * events of a configuration is equivalent to finding all possible cliques
42 * of the compatibility graph. While this is an NP-complete problem in
43 * general, it is still a (potentially major) refinement over checking
44 * all possible subsets of events of the configuration directly.
46 class CompatibilityGraph {
48 std::unordered_map<CompatibilityGraphNode*, std::unique_ptr<CompatibilityGraphNode>> nodes;
51 CompatibilityGraph() = default;
52 CompatibilityGraph& operator=(CompatibilityGraph&&) = default;
53 CompatibilityGraph(CompatibilityGraph&&) = default;
55 auto begin() const { return this->nodes.begin(); }
56 auto end() const { return this->nodes.end(); }
58 void remove(CompatibilityGraphNode* e);
59 void insert(std::unique_ptr<CompatibilityGraphNode> e);
61 size_t size() const { return this->nodes.size(); }
62 bool empty() const { return this->nodes.empty(); }
65 } // namespace simgrid::mc::udpor