src/mc/explo/udpor/Configuration.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_CONFIGURATION_HPP
   7 #define SIMGRID_MC_UDPOR_CONFIGURATION_HPP
   8
   9 #include "src/mc/explo/udpor/CompatibilityGraph.hpp"
  10 #include "src/mc/explo/udpor/EventSet.hpp"
  11 #include "src/mc/explo/udpor/udpor_forward.hpp"
  12
  13 #include <functional>
  14 #include <initializer_list>
  15 #include <vector>
  16
  17 namespace simgrid::mc::udpor {
  18
  19 class Configuration {
  20 public:
  21   Configuration()                                = default;
  22   Configuration(const Configuration&)            = default;
  23   Configuration& operator=(Configuration const&) = default;
  24   Configuration(Configuration&&)                 = default;
  25
  26   explicit Configuration(const EventSet& events);
  27   explicit Configuration(std::initializer_list<UnfoldingEvent*> events);
  28
  29   auto begin() const { return this->events_.begin(); }
  30   auto end() const { return this->events_.end(); }
  31
  32   bool contains(UnfoldingEvent* e) const { return this->events_.contains(e); }
  33   const EventSet& get_events() const { return this->events_; }
  34   UnfoldingEvent* get_latest_event() const { return this->newest_event; }
  35
  36   /**
  37    * @brief Insert a new event into the configuration
  38    *
  39    * When the newly added event is inserted into the configuration,
  40    * an assertion is made to ensure that the configuration remains
  41    * valid, i.e. that the newly added event's dependencies are contained
  42    * within the configuration.
  43    *
  44    * @param e the event to add to the configuration. If the event is
  45    * already a part of the configuration, calling this method has no
  46    * effect.
  47    *
  48    * @throws an invalid argument exception is raised should the event
  49    * be missing one of its dependencies
  50    *
  51    * @note: UDPOR technically enforces the invariant that all newly-added events
  52    * will ensure that the configuration is valid. We perform extra checks to ensure
  53    * that UDPOR is implemented as expected. There is a performance penalty that
  54    * should be noted: checking for maximality requires ensuring that all events in the
  55    * configuration have their dependencies containes within the configuration, which
  56    * essentially means performing a BFS/DFS over the configuration using a History object.
  57    * However, since the slowest part of UDPOR involves enumerating all
  58    * subsets of maximal events and computing k-partial alternatives (the
  59    * latter definitively an NP-hard problem when optimal), Amdahl's law suggests
  60    * we shouldn't focus so much on this (let alone the additional benefit of the
  61    * assertions)
  62    */
  63   void add_event(UnfoldingEvent* e);
  64
  65   /**
  66    * @brief Orders the events of the configuration such that
  67    * "more recent" events (i.e. those that are farther down in
  68    * the event structure's dependency chain) come after those
  69    * that appeared "farther in the past"
  70    *
  71    * @returns a vector `V` with the following property:
  72    *
  73    * 1. Let i(e) := C -> I map events to their indices in `V`.
  74    * For every pair of events e, e' in C, if e < e' then i(e) < i(e')
  75    *
  76    * Intuitively, events that are closer to the "bottom" of the event
  77    * structure appear farther along in the list than those that appear
  78    * closer to the "top"
  79    */
  80   std::vector<UnfoldingEvent*> get_topologically_sorted_events() const;
  81
  82   /**
  83    * @brief Orders the events of the configuration such that
  84    * "more recent" events (i.e. those that are farther down in
  85    * the event structure's dependency chain) come before those
  86    * that appear "farther in the past"
  87    *
  88    * @note The events of the event structure are arranged such that
  89    * e < e' implies a directed edge from e to e'. However, it is
  90    * also useful to be able to traverse the *reverse* graph (for
  91    * example when computing the compatibility graph of a configuration),
  92    * hence the distinction between "reversed" and the method
  93    * "Configuration::get_topologically_sorted_events()"
  94    *
  95    * @returns a vector `V` with the following property:
  96    *
  97    * 1. Let i(e) := C -> I map events to their indices in `V`.
  98    * For every pair of events e, e' in C, if e < e' then i(e) > i(e')
  99    *
 100    * Intuitively, events that are closer to the "top" of the event
 101    * structure appear farther along in the list than those that appear
 102    * closer to the "bottom"
 103    */
 104   std::vector<UnfoldingEvent*> get_topologically_sorted_events_of_reverse_graph() const;
 105
 106   /**
 107    * @brief Construct a new compatibility graph from the events of the
 108    * configuration whose associated transitions are dependent with the
 109    * given action
 110    *
 111    * @param pred whether or not to even consider the unfolding event in any
 112    * compatibility nodes of the resulting graph
 113    * @returns a new compatibility graph that defines possible maximal subsets
 114    * of events of C that satisfy the predicate `pred`
 115    */
 116   std::unique_ptr<CompatibilityGraph>
 117   make_compatibility_graph_filtered_on(std::function<bool(const UnfoldingEvent*)> pred) const;
 118
 119 private:
 120   /**
 121    * @brief The most recent event added to the configuration
 122    */
 123   UnfoldingEvent* newest_event = nullptr;
 124
 125   /**
 126    * @brief The events which make up this configuration
 127    *
 128    * @invariant For each event `e` in `events_`, the set of
 129    * dependencies of `e` is also contained in `events_`
 130    */
 131   EventSet events_;
 132 };
 133
 134 } // namespace simgrid::mc::udpor
 135 #endif