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 <cstddef>
  12 #include <initializer_list>
  13 #include <unordered_set>
  14 #include <vector>
  15
  16 namespace simgrid::mc::udpor {
  17
  18 class EventSet {
  19 private:
  20   std::unordered_set<const UnfoldingEvent*> events_;
  21
  22 public:
  23   EventSet()                           = default;
  24   EventSet(const EventSet&)            = default;
  25   EventSet& operator=(const EventSet&) = default;
  26   EventSet& operator=(EventSet&&)      = default;
  27   EventSet(EventSet&&)                 = default;
  28   explicit EventSet(Configuration&& config);
  29   explicit EventSet(std::vector<const UnfoldingEvent*>&& raw_events) : events_(raw_events.begin(), raw_events.end()) {}
  30   explicit EventSet(std::unordered_set<const UnfoldingEvent*>&& raw_events) : events_(raw_events) {}
  31   explicit EventSet(std::initializer_list<const UnfoldingEvent*> event_list) : events_(std::move(event_list)) {}
  32
  33   auto begin() const { return this->events_.begin(); }
  34   auto end() const { return this->events_.end(); }
  35   auto cbegin() const { return this->events_.cbegin(); }
  36   auto cend() const { return this->events_.cend(); }
  37
  38   void remove(const UnfoldingEvent*);
  39   void subtract(const EventSet&);
  40   void subtract(const Configuration&);
  41   EventSet subtracting(const UnfoldingEvent*) const;
  42   EventSet subtracting(const EventSet&) const;
  43   EventSet subtracting(const Configuration&) const;
  44
  45   void insert(const UnfoldingEvent*);
  46   void form_union(const EventSet&);
  47   void form_union(const Configuration&);
  48   EventSet make_union(const UnfoldingEvent*) const;
  49   EventSet make_union(const EventSet&) const;
  50   EventSet make_union(const Configuration&) const;
  51
  52   size_t size() const;
  53   bool empty() const;
  54   bool contains(const UnfoldingEvent*) const;
  55   bool contains(const History&) const;
  56   bool is_subset_of(const EventSet&) const;
  57
  58   bool operator==(const EventSet& other) const { return this->events_ == other.events_; }
  59   bool operator!=(const EventSet& other) const { return this->events_ != other.events_; }
  60
  61   /**
  62    * @brief Whether or not this set of events could
  63    * represent a configuration
  64    */
  65   bool is_valid_configuration() const;
  66
  67   /**
  68    * @brief Whether or not this set of events is
  69    * a *maximal event set*, i.e. whether each element
  70    * of the set causes none of the others
  71    *
  72    * A set of events `E` is said to be _maximal_ if
  73    * it is causally-free. Formally,
  74    *
  75    * 1. For each event `e` in `E`, there is no event
  76    * `e'` in `E` such that `e < e'`
  77    */
  78   bool is_maximal_event_set() const;
  79 };
  80
  81 } // namespace simgrid::mc::udpor
  82 #endif