src/mc/explo/udpor/History.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_HISTORY_HPP
   7 #define SIMGRID_MC_UDPOR_HISTORY_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 /**
  15  * @brief Conceptually describes the local configuration(s) of
  16  * an event or a collection of events, encoding the history of
  17  * the events without needing to actually fully compute all of
  18  * the events contained in the history
  19  *
  20  * When you create an instance of `History`, you are effectively
  21  * making a "lazy" configuration whose elements are the set of
  22  * causes of a given event (if the `History` constists of a single
  23  * event) or the union of all causes of all events (if the
  24  * `History` consists of a set of events).
  25  *
  26  * Using a `History` object to represent the history of a set of
  27  * events is more efficient (and reads more easily) than first
  28  * computing the entire history of each of the events separately
  29  * and combining the results. The former can take advantage of the
  30  * fact that the histories of a set of events overlap greatly, and
  31  * thus only a single BFS/DFS search over the event structure needs
  32  * to be performed instead of many isolated searches for each event.
  33  *
  34  * The same observation also allows you to compute the difference between
  35  * a configuration and a history of a set of events. This is used
  36  * in UDPOR, for example, when determing the difference J / C and
  37  * when using K-partial alternatives (which computes J as the union
  38  * of histories of events)
  39  */
  40 class History {
  41 private:
  42   /**
  43    * @brief The events whose history this instance describes
  44    */
  45   EventSet events_;
  46
  47 public:
  48   History()                          = default;
  49   History(const History&)            = default;
  50   History& operator=(History const&) = default;
  51   History(History&&)                 = default;
  52
  53   explicit History(UnfoldingEvent* e) : events_({e}) {}
  54   explicit History(EventSet event_set) : events_(std::move(event_set)) {}
  55
  56   /**
  57    * @brief Whether or not the given event is contained in the history
  58    *
  59    * @note If you only need to determine whether a few events are contained
  60    * in a history, prefer this method. If, however, you wish to repeatedly
  61    * determine over time (e.g. over the course of a computation) whether
  62    * some event is part of the history, it may be better to first compute
  63    * all events (see `History::get_all_events()`) and reuse this set
  64    *
  65    * @param e the event to check
  66    * @returns whether or not `e` is contained in the collection
  67    */
  68   bool contains(UnfoldingEvent* e) const;
  69
  70   /**
  71    * @brief Computes all events in the history described by this instance
  72    *
  73    * Sometimes, it is useful to compute the entire set of events that
  74    * comprise the history of some event `e` of some set of events `E`.
  75    * This method performs that computation.
  76    *
  77    * @returns the set of all causal dependencies of all events this
  78    * history represents. Equivalently, the method returns the full
  79    * dependency graph for all events in this history
  80    */
  81   EventSet get_all_events() const;
  82
  83   EventSet get_event_diff_with(const EventSet& event_set) const;
  84   EventSet get_event_diff_with(const Configuration& config) const;
  85 };
  86
  87 } // namespace simgrid::mc::udpor
  88 #endif