Add skeleton implementations to ExtensionSetCalculator

diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp
index c760337..2ff083a 100644 (file)
--- a/src/mc/explo/UdporChecker.cpp
+++ b/src/mc/explo/UdporChecker.cpp
@@ -6,6 +6,7 @@
 #include "src/mc/explo/UdporChecker.hpp"
 #include "src/mc/api/State.hpp"
 #include "src/mc/explo/udpor/Comb.hpp"
+#include "src/mc/explo/udpor/ExtensionSetCalculator.hpp"
 #include "src/mc/explo/udpor/History.hpp"
 #include "src/mc/explo/udpor/maximal_subsets_iterator.hpp"
 
@@ -128,15 +129,8 @@ EventSet UdporChecker::compute_exC(const Configuration& C, const State& stateC,
 
   for (const auto& [aid, actor_state] : stateC.get_actors_list()) {
     for (const auto& transition : actor_state.get_enabled_transitions()) {
-      // First check for a specialized function that can compute the extension
-      // set "quickly" based on its type. Otherwise, fall back to computing
-      // the set "by hand"
-      const auto specialized_extension_function = incremental_extension_functions.find(transition->type_);
-      if (specialized_extension_function != incremental_extension_functions.end()) {
-        exC.form_union((specialized_extension_function->second)(C, transition));
-      } else {
-        exC.form_union(this->compute_exC_by_enumeration(C, transition));
-      }
+      EventSet extension = ExtensionSetCalculator::partially_extend(C, unfolding, transition);
+      exC.form_union(extension);
     }
   }
   return exC;

diff --git a/src/mc/explo/udpor/ExtensionSetCalculator.cpp b/src/mc/explo/udpor/ExtensionSetCalculator.cpp
index e69de29..e5b9a18 100644 (file)
--- a/src/mc/explo/udpor/ExtensionSetCalculator.cpp
+++ b/src/mc/explo/udpor/ExtensionSetCalculator.cpp
@@ -0,0 +1,68 @@
+/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved.          */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/mc/explo/udpor/ExtensionSetCalculator.hpp"
+
+#include <functional>
+#include <unordered_map>
+#include <xbt/asserts.h>
+#include <xbt/ex.h>
+
+using namespace simgrid::mc;
+
+namespace simgrid::mc::udpor {
+
+EventSet ExtensionSetCalculator::partially_extend(const Configuration& C, const Unfolding& U,
+                                                  const std::shared_ptr<Transition> action)
+{
+  switch (action->type_) {
+    case Transition::Type::COMM_WAIT: {
+      return partially_extend_CommWait(C, U, std::static_pointer_cast<CommWaitTransition>(std::move(action)));
+    }
+    case Transition::Type::COMM_ASYNC_SEND: {
+      return partially_extend_CommSend(C, U, std::static_pointer_cast<CommSendTransition>(std::move(action)));
+    }
+    case Transition::Type::COMM_ASYNC_RECV: {
+      return partially_extend_CommRecv(C, U, std::static_pointer_cast<CommRecvTransition>(std::move(action)));
+    }
+    default: {
+      xbt_assert(false,
+                 "There is currently no specialized computation for the transition "
+                 "'%s' for computing extension sets in UDPOR, so the model checker cannot "
+                 "determine how to proceed. Please submit a bug report requesting "
+                 "that the transition be supported in SimGrid using UDPOR and consider "
+                 "using the other model-checking algorithms supported by SimGrid instead "
+                 "in the meantime",
+                 action->to_string().c_str());
+      DIE_IMPOSSIBLE;
+    }
+  }
+}
+
+EventSet ExtensionSetCalculator::partially_extend_CommSend(const Configuration& C, const Unfolding& U,
+                                                           const std::shared_ptr<CommSendTransition> action)
+{
+  return EventSet();
+}
+
+EventSet ExtensionSetCalculator::partially_extend_CommRecv(const Configuration& C, const Unfolding& U,
+                                                           const std::shared_ptr<CommRecvTransition> action)
+{
+  return EventSet();
+}
+
+EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration&, const Unfolding& U,
+                                                           std::shared_ptr<CommWaitTransition>)
+{
+  return EventSet();
+}
+
+EventSet ExtensionSetCalculator::partially_extend_CommTest(const Configuration&, const Unfolding& U,
+                                                           std::shared_ptr<CommTestTransition>)
+{
+  return EventSet();
+}
+
+} // namespace simgrid::mc::udpor
\ No newline at end of file

diff --git a/src/mc/explo/udpor/ExtensionSetCalculator.hpp b/src/mc/explo/udpor/ExtensionSetCalculator.hpp
index 7a71285..95d06fe 100644 (file)
--- a/src/mc/explo/udpor/ExtensionSetCalculator.hpp
+++ b/src/mc/explo/udpor/ExtensionSetCalculator.hpp
@@ -3,9 +3,10 @@
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
-#ifndef SIMGRID_MC_UDPOR_EVENT_SET_HPP
-#define SIMGRID_MC_UDPOR_EVENT_SET_HPP
+#ifndef SIMGRID_MC_UDPOR_EVENTSETCALCULATOR_HPP
+#define SIMGRID_MC_UDPOR_EVENTSETCALCULATOR_HPP
 
+#include "src/mc/explo/udpor/EventSet.hpp"
 #include "src/mc/explo/udpor/udpor_forward.hpp"
 #include "src/mc/transition/Transition.hpp"
 #include "src/mc/transition/TransitionActorJoin.hpp"
@@ -15,6 +16,8 @@
 #include "src/mc/transition/TransitionRandom.hpp"
 #include "src/mc/transition/TransitionSynchro.hpp"
 
+#include <memory>
+
 namespace simgrid::mc::udpor {
 
 /**
@@ -22,13 +25,17 @@ namespace simgrid::mc::udpor {
  */
 struct ExtensionSetCalculator final {
 private:
-  static EventSet partially_extend_CommSend(const Configuration&, std::shared_ptr<CommSendTransition>);
-  static EventSet partially_extend_CommReceive(const Configuration&, std::shared_ptr<CommReceiveTransition>);
-  static EventSet partially_extend_CommWait(const Configuration&, std::shared_ptr<CommWaitTransition>);
-  static EventSet partially_extend_CommTest(const Configuration&, std::shared_ptr<CommTestTransition>);
+  static EventSet partially_extend_CommSend(const Configuration&, const Unfolding&,
+                                            std::shared_ptr<CommSendTransition>);
+  static EventSet partially_extend_CommRecv(const Configuration&, const Unfolding&,
+                                            std::shared_ptr<CommRecvTransition>);
+  static EventSet partially_extend_CommWait(const Configuration&, const Unfolding&,
+                                            std::shared_ptr<CommWaitTransition>);
+  static EventSet partially_extend_CommTest(const Configuration&, const Unfolding&,
+                                            std::shared_ptr<CommTestTransition>);
 
 public:
-  static EventSet partially_extend(const Configuration&, const Unfolding&, const std::shared_ptr<Transition> action);
+  static EventSet partially_extend(const Configuration&, const Unfolding&, const std::shared_ptr<Transition>);
 };
 
 } // namespace simgrid::mc::udpor