src/mc/explo/udpor/CompatibilityGraph.hpp

   1 /* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved.          */
   2
   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. */
   5
   6 #ifndef SIMGRID_MC_UDPOR_COMPATIBILITY_GRAPH_HPP
   7 #define SIMGRID_MC_UDPOR_COMPATIBILITY_GRAPH_HPP
   8
   9 #include "src/mc/explo/udpor/CompatibilityGraphNode.hpp"
  10 #include "src/mc/explo/udpor/udpor_forward.hpp"
  11
  12 #include <memory>
  13 #include <unordered_map>
  14
  15 namespace simgrid::mc::udpor {
  16
  17 /**
  18  * @brief A graph which describes the causal-conflicts between groups of
  19  * events from an unfolding
  20  *
  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.
  28  *
  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.
  33  *
  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.
  45  */
  46 class CompatibilityGraph {
  47 private:
  48   std::unordered_map<CompatibilityGraphNode*, std::unique_ptr<CompatibilityGraphNode>> nodes;
  49
  50 public:
  51   CompatibilityGraph()                                = default;
  52   CompatibilityGraph& operator=(CompatibilityGraph&&) = default;
  53   CompatibilityGraph(CompatibilityGraph&&)            = default;
  54
  55   auto begin() const { return this->nodes.begin(); }
  56   auto end() const { return this->nodes.end(); }
  57
  58   void remove(CompatibilityGraphNode* e);
  59   void insert(std::unique_ptr<CompatibilityGraphNode> e);
  60
  61   size_t size() const { return this->nodes.size(); }
  62   bool empty() const { return this->nodes.empty(); }
  63 };
  64
  65 } // namespace simgrid::mc::udpor
  66 #endif