src/mc/explo/udpor/EventSet.cpp

   1 /* Copyright (c) 2008-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 #include "src/mc/explo/udpor/EventSet.hpp"
   7 #include "src/mc/explo/udpor/Configuration.hpp"
   8 #include "src/mc/explo/udpor/History.hpp"
   9
  10 #include <iterator>
  11
  12 namespace simgrid::mc::udpor {
  13
  14 EventSet::EventSet(Configuration&& config) : EventSet(std::move(config.get_events())) {}
  15
  16 void EventSet::remove(UnfoldingEvent* e)
  17 {
  18   this->events_.erase(e);
  19 }
  20
  21 void EventSet::subtract(const EventSet& other)
  22 {
  23   this->events_ = std::move(subtracting(other).events_);
  24 }
  25
  26 void EventSet::subtract(const Configuration& config)
  27 {
  28   subtract(config.get_events());
  29 }
  30
  31 EventSet EventSet::subtracting(const EventSet& other) const
  32 {
  33   std::unordered_set<UnfoldingEvent*> result = this->events_;
  34
  35   for (UnfoldingEvent* e : other.events_)
  36     result.erase(e);
  37
  38   return EventSet(std::move(result));
  39 }
  40
  41 EventSet EventSet::subtracting(const Configuration& config) const
  42 {
  43   return subtracting(config.get_events());
  44 }
  45
  46 EventSet EventSet::subtracting(UnfoldingEvent* e) const
  47 {
  48   auto result = this->events_;
  49   result.erase(e);
  50   return EventSet(std::move(result));
  51 }
  52
  53 void EventSet::insert(UnfoldingEvent* e)
  54 {
  55   this->events_.insert(e);
  56 }
  57
  58 void EventSet::form_union(const EventSet& other)
  59 {
  60   this->events_ = std::move(make_union(other).events_);
  61 }
  62
  63 void EventSet::form_union(const Configuration& config)
  64 {
  65   form_union(config.get_events());
  66 }
  67
  68 EventSet EventSet::make_union(UnfoldingEvent* e) const
  69 {
  70   auto result = this->events_;
  71   result.insert(e);
  72   return EventSet(std::move(result));
  73 }
  74
  75 EventSet EventSet::make_union(const EventSet& other) const
  76 {
  77   std::unordered_set<UnfoldingEvent*> result = this->events_;
  78
  79   for (UnfoldingEvent* e : other.events_)
  80     result.insert(e);
  81
  82   return EventSet(std::move(result));
  83 }
  84
  85 EventSet EventSet::make_union(const Configuration& config) const
  86 {
  87   return make_union(config.get_events());
  88 }
  89
  90 size_t EventSet::size() const
  91 {
  92   return this->events_.size();
  93 }
  94
  95 bool EventSet::empty() const
  96 {
  97   return this->events_.empty();
  98 }
  99
 100 bool EventSet::contains(UnfoldingEvent* e) const
 101 {
 102   return this->events_.find(e) != this->events_.end();
 103 }
 104
 105 bool EventSet::is_subset_of(const EventSet& other) const
 106 {
 107   // If there is some element not contained in `other`, then
 108   // the set difference will contain that element and the
 109   // result won't be empty
 110   return subtracting(other).empty();
 111 }
 112
 113 bool EventSet::is_valid_configuration() const
 114 {
 115   /// @invariant: A collection of events `E` is a configuration
 116   /// if and only if following while following the history of
 117   /// each event `e` of `E`you remain in `E`. In other words, you
 118   /// only see events from set `E`
 119   ///
 120   /// The proof is based on the definition of a configuration
 121   /// which requires that all
 122   const History history(*this);
 123   return this->contains(history);
 124 }
 125
 126 bool EventSet::contains(const History& history) const
 127 {
 128   return std::all_of(history.begin(), history.end(), [=](UnfoldingEvent* e) { return this->contains(e); });
 129 }
 130
 131 bool EventSet::is_maximal_event_set() const
 132 {
 133   const History history(*this);
 134   return *this == history.get_all_maximal_events();
 135 }
 136
 137 } // namespace simgrid::mc::udpor