Add method to check if an EventSet is a config

[simgrid.git] / src / mc / explo / udpor / EventSet.cpp

diff --git a/src/mc/explo/udpor/EventSet.cpp b/src/mc/explo/udpor/EventSet.cpp
index 57aeeb975acacc9fea1c245d75fe9a6cd5da3f38..681a27290972996311cfb3ab0f732421a9b6ea5b 100644 (file)
--- a/src/mc/explo/udpor/EventSet.cpp
+++ b/src/mc/explo/udpor/EventSet.cpp
@@ -4,10 +4,10 @@
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "src/mc/explo/udpor/EventSet.hpp"
+#include "src/mc/explo/udpor/Configuration.hpp"
+#include "src/mc/explo/udpor/History.hpp"
 
-#include <algorithm>
 #include <iterator>
-#include <set>
 
 namespace simgrid::mc::udpor {
 
@@ -21,14 +21,26 @@ void EventSet::subtract(const EventSet& other)
   this->events_ = std::move(subtracting(other).events_);
 }
 
+void EventSet::subtract(const Configuration& config)
+{
+  subtract(config.get_events());
+}
+
 EventSet EventSet::subtracting(const EventSet& other) const
 {
-  std::set<UnfoldingEvent*> result;
-  std::set_difference(this->events_.begin(), this->events_.end(), other.events_.begin(), other.events_.end(),
-                      std::inserter(result, result.end()));
+  std::unordered_set<UnfoldingEvent*> result = this->events_;
+
+  for (UnfoldingEvent* e : other.events_)
+    result.erase(e);
+
   return EventSet(std::move(result));
 }
 
+EventSet EventSet::subtracting(const Configuration& config) const
+{
+  return subtracting(config.get_events());
+}
+
 EventSet EventSet::subtracting(UnfoldingEvent* e) const
 {
   auto result = this->events_;
@@ -38,7 +50,6 @@ EventSet EventSet::subtracting(UnfoldingEvent* e) const
 
 void EventSet::insert(UnfoldingEvent* e)
 {
-  // TODO: Potentially react if the event is already inserted
   this->events_.insert(e);
 }
 
@@ -47,6 +58,11 @@ void EventSet::form_union(const EventSet& other)
   this->events_ = std::move(make_union(other).events_);
 }
 
+void EventSet::form_union(const Configuration& config)
+{
+  form_union(config.get_events());
+}
+
 EventSet EventSet::make_union(UnfoldingEvent* e) const
 {
   auto result = this->events_;
@@ -56,12 +72,19 @@ EventSet EventSet::make_union(UnfoldingEvent* e) const
 
 EventSet EventSet::make_union(const EventSet& other) const
 {
-  std::set<UnfoldingEvent*> result;
-  std::set_union(this->events_.begin(), this->events_.end(), other.events_.begin(), other.events_.end(),
-                 std::inserter(result, result.end()));
+  std::unordered_set<UnfoldingEvent*> result = this->events_;
+
+  for (UnfoldingEvent* e : other.events_)
+    result.insert(e);
+
   return EventSet(std::move(result));
 }
 
+EventSet EventSet::make_union(const Configuration& config) const
+{
+  return make_union(config.get_events());
+}
+
 size_t EventSet::size() const
 {
   return this->events_.size();
@@ -85,4 +108,17 @@ bool EventSet::is_subset_of(const EventSet& other) const
   return subtracting(other).empty();
 }
 
+bool EventSet::is_valid_configuration() const
+{
+  /// @invariant: A collection of events `E` is a configuration
+  /// if and only if following while following the history of
+  /// each event `e` of `E`you remain in `E`. In other words, you
+  /// only see events from set `E`
+  ///
+  /// The proof is based on the definition of a configuration
+  /// which requires that all
+  const History history(*this);
+  return std::all_of(history.begin(), history.end(), [=](UnfoldingEvent* e) { return this->contains(e); });
+}
+
 } // namespace simgrid::mc::udpor
\ No newline at end of file