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/EventSet.hpp"
  10 #include "src/mc/explo/udpor/udpor_forward.hpp"
  11
  12 namespace simgrid::mc::udpor {
  13
  14 class Configuration {
  15 public:
  16   Configuration()                                = default;
  17   Configuration(const Configuration&)            = default;
  18   Configuration& operator=(Configuration const&) = default;
  19   Configuration(Configuration&&)                 = default;
  20
  21   Configuration(EventSet events) : events_(events) {}
  22   Configuration(EventSet&& events) : events_(events) {}
  23
  24   auto begin() const { return this->events_.begin(); }
  25   auto end() const { return this->events_.end(); }
  26
  27   bool contains(UnfoldingEvent* e) const { return this->events_.contains(e); }
  28   const EventSet& get_events() const { return this->events_; }
  29   UnfoldingEvent* get_latest_event() const { return this->newest_event; }
  30
  31   /**
  32    * @brief Insert a new event into the configuration
  33    *
  34    * When the newly added event is inserted into the configuration,
  35    * an assertion is made to ensure that the configuration remains
  36    * valid, i.e. that the newly added event's dependencies are contained
  37    * within the configuration.
  38    *
  39    * @throws an invalid argument exception is raised should the event
  40    * be missing one of its dependencies
  41    *
  42    * @note: UDPOR technically enforces the invariant that all newly-added events
  43    * will ensure that the configuration is valid. We perform extra checks to ensure
  44    * that UDPOR is implemented as expected. There is a performance penalty that
  45    * should be noted: checking for maximality requires ensuring that all events in the
  46    * configuration have their dependencies containes within the configuration, which
  47    * essentially means performing a BFS/DFS over the configuration using a History object.
  48    * However, since the slowest part of UDPOR involves enumerating all
  49    * subsets of maximal events and computing k-partial alternatives (the
  50    * latter definitively an NP-hard problem when optimal), Amdahl's law suggests
  51    * we shouldn't focus so much on this (let alone the additional benefit of the
  52    * assertions)
  53    */
  54   void add_event(UnfoldingEvent*);
  55
  56 private:
  57   /**
  58    * @brief The most recent event added to the configuration
  59    */
  60   UnfoldingEvent* newest_event = nullptr;
  61
  62   /**
  63    * @brief The events which make up this configuration
  64    *
  65    * @invariant For each event `e` in `events_`, the set of
  66    * dependencies of `e` is also contained in `events_`
  67    */
  68   EventSet events_;
  69 };
  70
  71 } // namespace simgrid::mc::udpor
  72 #endif