src/mc/explo/udpor/EventSet.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_EVENT_SET_HPP
   7 #define SIMGRID_MC_UDPOR_EVENT_SET_HPP
   8
   9 #include "src/mc/explo/udpor/udpor_forward.hpp"
  10
  11 #include <algorithm>
  12 #include <cstddef>
  13 #include <initializer_list>
  14 #include <unordered_set>
  15 #include <vector>
  16 #include <xbt/asserts.h>
  17
  18 namespace simgrid::mc::udpor {
  19
  20 class EventSet {
  21 private:
  22   std::unordered_set<const UnfoldingEvent*> events_;
  23
  24 public:
  25   EventSet()                           = default;
  26   EventSet(const EventSet&)            = default;
  27   EventSet& operator=(const EventSet&) = default;
  28   EventSet& operator=(EventSet&&)      = default;
  29   EventSet(EventSet&&)                 = default;
  30   explicit EventSet(Configuration&& config);
  31   explicit EventSet(std::vector<const UnfoldingEvent*>&& raw_events) : events_(raw_events.begin(), raw_events.end())
  32   {
  33     xbt_assert(std::none_of(events_.begin(), events_.end(), [](const auto* e) { return e == nullptr; }), "Oh no");
  34   }
  35   explicit EventSet(std::unordered_set<const UnfoldingEvent*>&& raw_events) : events_(raw_events)
  36   {
  37     xbt_assert(std::none_of(events_.begin(), events_.end(), [](const auto* e) { return e == nullptr; }), "Oh no");
  38   }
  39   explicit EventSet(std::initializer_list<const UnfoldingEvent*> event_list) : events_(std::move(event_list))
  40   {
  41     xbt_assert(std::none_of(events_.begin(), events_.end(), [](const auto* e) { return e == nullptr; }), "Oh no");
  42   }
  43
  44   auto begin() const { return this->events_.begin(); }
  45   auto end() const { return this->events_.end(); }
  46   auto cbegin() const { return this->events_.cbegin(); }
  47   auto cend() const { return this->events_.cend(); }
  48
  49   void remove(const UnfoldingEvent*);
  50   void subtract(const EventSet&);
  51   void subtract(const Configuration&);
  52   EventSet subtracting(const UnfoldingEvent*) const;
  53   EventSet subtracting(const EventSet&) const;
  54   EventSet subtracting(const Configuration&) const;
  55
  56   void insert(const UnfoldingEvent*);
  57   void form_union(const EventSet&);
  58   void form_union(const Configuration&);
  59   EventSet make_union(const UnfoldingEvent*) const;
  60   EventSet make_union(const EventSet&) const;
  61   EventSet make_union(const Configuration&) const;
  62   EventSet get_local_config() const;
  63
  64   size_t size() const;
  65   bool empty() const;
  66   bool contains(const UnfoldingEvent*) const;
  67   bool contains(const History&) const;
  68   bool intersects(const EventSet&) const;
  69   bool intersects(const History&) const;
  70   bool is_subset_of(const EventSet&) const;
  71
  72   bool operator==(const EventSet& other) const { return this->events_ == other.events_; }
  73   bool operator!=(const EventSet& other) const { return this->events_ != other.events_; }
  74   std::string to_string() const;
  75
  76   /**
  77    * @brief Whether or not this set of events could
  78    * represent a configuration
  79    */
  80   bool is_valid_configuration() const;
  81
  82   /**
  83    * @brief Whether or not this set of events is
  84    * a *maximal event set*, i.e. whether each element
  85    * of the set causes none of the others
  86    *
  87    * A set of events `E` is said to be _maximal_ if
  88    * it is causally-free. Formally,
  89    *
  90    * 1. For each event `e` in `E`, there is no event
  91    * `e'` in `E` such that `e < e'`
  92    */
  93   bool is_maximal() const;
  94
  95   /**
  96    * @brief Whether or not this set of events is
  97    * free of conflicts
  98    *
  99    * A set of events `E` is said to be _conflict free_
 100    * if
 101    *
 102    * 1. For each event `e` in `E`, there is no event
 103    * `e'` in `E` such that `e # e'` where `#` is the
 104    * conflict relation over the unfolding from
 105    * which the events `E` are derived
 106    *
 107    * @note: This method makes use only of the causality
 108    * tree of the events in the set; i.e. it determines conflicts
 109    * based solely on the unfolding and the definition of
 110    * conflict in an unfolding. Some clever techniques
 111    * exist for computing conflicts with specialized transition
 112    * types (only mutexes if I remember correctly) that was
 113    * referenced in The Anh Pham's thesis. This would require
 114    * keeping track of information *outside* of any given
 115    * set and probably doesn't work for all types of transitions
 116    * anyway.
 117    */
 118   bool is_conflict_free() const;
 119
 120   /**
 121    * @brief Produces the largest subset of this
 122    * set of events which is maximal
 123    */
 124   EventSet get_largest_maximal_subset() const;
 125
 126   /**
 127    * @brief Orders the events of the set such that
 128    * "more recent" events (i.e. those that are farther down in
 129    * the event structure's dependency chain) come after those
 130    * that appeared "farther in the past"
 131    *
 132    * @returns a vector `V` with the following property:
 133    *
 134    * 1. Let i(e) := C -> I map events to their indices in `V`.
 135    * For every pair of events e, e' in C, if e < e' then i(e) < i(e')
 136    *
 137    * Intuitively, events that are closer to the "bottom" of the event
 138    * structure appear farther along in the list than those that appear
 139    * closer to the "top"
 140    */
 141   std::vector<const UnfoldingEvent*> get_topological_ordering() const;
 142
 143   /**
 144    * @brief Orders the events of set such that
 145    * "more recent" events (i.e. those that are farther down in
 146    * the event structure's dependency chain) come before those
 147    * that appear "farther in the past"
 148    *
 149    * @note The events of the event structure are arranged such that
 150    * e < e' implies a directed edge from e to e'. However, it is
 151    * also useful to be able to traverse the *reverse* graph (for
 152    * example when computing the compatibility graph of a configuration),
 153    * hence the distinction between "reversed" and the method
 154    * "EventSet::get_topological_ordering()"
 155    *
 156    * @returns a vector `V` with the following property:
 157    *
 158    * 1. Let i(e) := C -> I map events to their indices in `V`.
 159    * For every pair of events e, e' in C, if e < e' then i(e) > i(e')
 160    *
 161    * Intuitively, events that are closer to the "top" of the event
 162    * structure appear farther along in the list than those that appear
 163    * closer to the "bottom"
 164    */
 165   std::vector<const UnfoldingEvent*> get_topological_ordering_of_reverse_graph() const;
 166
 167   /**
 168    * @brief Moves the event set into a list
 169    */
 170   std::vector<const UnfoldingEvent*> move_into_vector() const&&;
 171
 172   using iterator       = decltype(events_)::iterator;
 173   using const_iterator = decltype(events_)::const_iterator;
 174   using value_type     = decltype(events_)::value_type;
 175 };
 176
 177 } // namespace simgrid::mc::udpor
 178 #endif