A few calls to mc_model_checker less by passing more parameters

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

diff --git a/src/mc/explo/udpor/UnfoldingEvent.cpp b/src/mc/explo/udpor/UnfoldingEvent.cpp
index 50c1e22..b62ef1a 100644 (file)
--- a/src/mc/explo/udpor/UnfoldingEvent.cpp
+++ b/src/mc/explo/udpor/UnfoldingEvent.cpp
@@ -67,12 +67,10 @@ bool UnfoldingEvent::conflicts_with(const UnfoldingEvent* other) const
   const EventSet unique_to_me    = my_history.subtracting(other_history);
   const EventSet unique_to_other = other_history.subtracting(my_history);
 
-  const bool conflicts_with_me = std::any_of(unique_to_me.begin(), unique_to_me.end(), [&](const UnfoldingEvent* e) {
-    return e->has_dependent_transition_with(other);
-  });
-  const bool conflicts_with_other =
-      std::any_of(unique_to_other.begin(), unique_to_other.end(),
-                  [&](const UnfoldingEvent* e) { return e->has_dependent_transition_with(this); });
+  const bool conflicts_with_me    = std::any_of(unique_to_me.begin(), unique_to_me.end(),
+                                                [&](const UnfoldingEvent* e) { return e->is_dependent_with(other); });
+  const bool conflicts_with_other = std::any_of(unique_to_other.begin(), unique_to_other.end(),
+                                                [&](const UnfoldingEvent* e) { return e->is_dependent_with(this); });
   return conflicts_with_me or conflicts_with_other;
 }
 
@@ -85,7 +83,36 @@ bool UnfoldingEvent::conflicts_with(const Configuration& config) const
   // if they are not related)
   const EventSet potential_conflicts = config.get_events().subtracting(get_history());
   return std::any_of(potential_conflicts.cbegin(), potential_conflicts.cend(),
-                     [&](const UnfoldingEvent* e) { return this->has_dependent_transition_with(e); });
+                     [&](const UnfoldingEvent* e) { return this->is_dependent_with(e); });
+}
+
+bool UnfoldingEvent::immediately_conflicts_with(const UnfoldingEvent* other) const
+{
+  // They have to be in conflict at a minimum
+  if (not conflicts_with(other)) {
+    return false;
+  }
+
+  auto combined_events = History(EventSet{this, other}).get_all_events();
+
+  // See the definition of immediate conflicts in the original paper on UDPOR
+  {
+    combined_events.remove(this);
+    if (not combined_events.is_valid_configuration()) {
+      return false;
+    }
+    combined_events.insert(this);
+  }
+
+  {
+    combined_events.remove(other);
+    if (not combined_events.is_valid_configuration()) {
+      return false;
+    }
+    combined_events.insert(other);
+  }
+
+  return true;
 }
 
 bool UnfoldingEvent::is_dependent_with(const Transition* t) const
@@ -93,7 +120,7 @@ bool UnfoldingEvent::is_dependent_with(const Transition* t) const
   return associated_transition->depends(t);
 }
 
-bool UnfoldingEvent::has_dependent_transition_with(const UnfoldingEvent* other) const
+bool UnfoldingEvent::is_dependent_with(const UnfoldingEvent* other) const
 {
   return is_dependent_with(other->associated_transition.get());
 }