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   auto begin() const { return this->events_.begin(); }
  22   auto end() const { return this->events_.end(); }
  23
  24   bool contains(UnfoldingEvent* e) const { return this->events_.contains(e); }
  25   const EventSet& get_events() const { return this->events_; }
  26   const EventSet& get_maximal_events() const { return this->max_events_; }
  27   UnfoldingEvent* get_latest_event() const { return this->newest_event; }
  28
  29   void add_event(UnfoldingEvent*);
  30
  31 private:
  32   /**
  33    * @brief The most recent event added to the configuration
  34    */
  35   UnfoldingEvent* newest_event = nullptr;
  36
  37   /**
  38    * @brief The events which make up this configuration
  39    *
  40    * @invariant For each event `e` in `events_`, the set of
  41    * dependencies of `e` is also contained in `events_`
  42    *
  43    * TODO: UDPOR enforces this invariant, but perhaps we should
  44    * too?
  45    */
  46   EventSet events_;
  47
  48   /**
  49    * The <-maxmimal events of the configuration. These are
  50    * dynamically adjusted as events are added to the configuration
  51    *
  52    * @invariant Each event that is part of this set is
  53    *
  54    * 1. a <-maxmimal event of the configuration, in the sense that
  55    * there is no event in the configuration that is "greater" than it.
  56    * In UDPOR terminology, each event does not "cause" another event
  57    *
  58    * 2. contained in the set of events `events_` which comprise
  59    * the configuration
  60    */
  61   EventSet max_events_;
  62
  63 private:
  64   void recompute_maxmimal_events(UnfoldingEvent* new_event);
  65 };
  66
  67 } // namespace simgrid::mc::udpor
  68 #endif