Remove StateManager

The StateManager class was created to wrap
some of the functionality used in tiny_simgrid,
but it turns out that this functionality isn't
actually needed. States are managed entirely
by the UdporChecker/UDPOR in what is
effectively a stack, and it doesn't make sense
for events to talk about states when states
are associated with configurations

diff --git a/MANIFEST.in b/MANIFEST.in
index 0863de7..1decdf0 100644 (file)
--- a/MANIFEST.in
+++ b/MANIFEST.in
@@ -2216,8 +2216,6 @@ include src/mc/explo/udpor/Configuration.hpp
 include src/mc/explo/udpor/Configuration.cpp
 include src/mc/explo/udpor/EventSet.cpp
 include src/mc/explo/udpor/EventSet.hpp
-include src/mc/explo/udpor/StateManager.cpp
-include src/mc/explo/udpor/StateManager.hpp
 include src/mc/explo/udpor/UnfoldingEvent.cpp
 include src/mc/explo/udpor/UnfoldingEvent.hpp
 include src/mc/explo/udpor/Unfolding.cpp

diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp
index da236e2..fdd3680 100644 (file)
--- a/src/mc/explo/UdporChecker.cpp
+++ b/src/mc/explo/UdporChecker.cpp
@@ -4,6 +4,7 @@
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "src/mc/explo/UdporChecker.hpp"
+#include "src/mc/api/State.hpp"
 #include <xbt/asserts.h>
 #include <xbt/log.h>
 

diff --git a/src/mc/explo/UdporChecker.hpp b/src/mc/explo/UdporChecker.hpp
index cc1604a..e63802b 100644 (file)
--- a/src/mc/explo/UdporChecker.hpp
+++ b/src/mc/explo/UdporChecker.hpp
@@ -10,7 +10,6 @@
 #include "src/mc/explo/Exploration.hpp"
 #include "src/mc/explo/udpor/Configuration.hpp"
 #include "src/mc/explo/udpor/EventSet.hpp"
-#include "src/mc/explo/udpor/StateManager.hpp"
 #include "src/mc/explo/udpor/Unfolding.hpp"
 #include "src/mc/explo/udpor/UnfoldingEvent.hpp"
 #include "src/mc/mc_record.hpp"
@@ -74,12 +73,6 @@ private:
    */
   EventSet G;
 
-  /**
-   * Maintains the mapping between handles referenced by events in
-   * the current state of the unfolding
-   */
-  StateManager state_manager_;
-
   /**
    * @brief UDPOR's current "view" of the program it is exploring
    */

diff --git a/src/mc/explo/udpor/StateManager.cpp b/src/mc/explo/udpor/StateManager.cpp
deleted file mode 100644 (file)
index 81792ce..0000000
--- a/src/mc/explo/udpor/StateManager.cpp
+++ /dev/null
@@ -1,38 +0,0 @@
-/* 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/StateManager.hpp"
-#include "xbt/asserts.h"
-
-namespace simgrid::mc::udpor {
-
-StateManager::Handle StateManager::record_state(std::unique_ptr<State> state)
-{
-  if (state.get() == nullptr) {
-    throw std::invalid_argument("Expected a newly-allocated State but got NULL instead");
-  }
-
-  const auto integer_handle = this->current_handle_;
-  this->state_map_.insert({integer_handle, std::move(state)});
-
-  this->current_handle_++;
-  xbt_assert(integer_handle <= this->current_handle_, "Too many states were vended out during exploration via UDPOR.\n"
-                                                      "It's suprising you didn't run out of memory elsewhere first...\n"
-                                                      "Please report this as a bug along with the very large program");
-
-  return integer_handle;
-}
-
-std::optional<std::reference_wrapper<State>> StateManager::get_state(StateManager::Handle handle)
-{
-  auto state = this->state_map_.find(handle);
-  if (state == this->state_map_.end()) {
-    return std::nullopt;
-  }
-  auto& state_ref = *state->second.get();
-  return std::optional<std::reference_wrapper<State>>{state_ref};
-}
-
-} // namespace simgrid::mc::udpor

diff --git a/src/mc/explo/udpor/StateManager.hpp b/src/mc/explo/udpor/StateManager.hpp
deleted file mode 100644 (file)
index f02b976..0000000
--- a/src/mc/explo/udpor/StateManager.hpp
+++ /dev/null
@@ -1,29 +0,0 @@
-/* Copyright (c) 2007-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. */
-
-#ifndef SIMGRID_MC_UDPOR_GLOBAL_HPP
-#define SIMGRID_MC_UDPOR_GLOBAL_HPP
-
-#include "src/mc/api/State.hpp"
-#include "src/mc/explo/udpor/udpor_forward.hpp"
-
-#include <optional>
-
-namespace simgrid::mc::udpor {
-
-class StateManager {
-private:
-  using Handle = StateHandle;
-
-  Handle current_handle_ = 1ul;
-  std::unordered_map<Handle, std::unique_ptr<State>> state_map_;
-
-public:
-  Handle record_state(std::unique_ptr<State>);
-  std::optional<std::reference_wrapper<State>> get_state(Handle);
-};
-
-} // namespace simgrid::mc::udpor
-#endif

diff --git a/src/mc/explo/udpor/udpor_forward.hpp b/src/mc/explo/udpor/udpor_forward.hpp
index ab28a5a..c8b12c0 100644 (file)
--- a/src/mc/explo/udpor/udpor_forward.hpp
+++ b/src/mc/explo/udpor/udpor_forward.hpp
@@ -16,7 +16,6 @@ namespace simgrid::mc::udpor {
 class EventSet;
 class UnfoldingEvent;
 class Configuration;
-class StateManager;
 class Unfolding;
 using StateHandle = unsigned long long;
 

diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake
index 0746dc4..054bc13 100644 (file)
--- a/tools/cmake/DefinePackages.cmake
+++ b/tools/cmake/DefinePackages.cmake
@@ -529,8 +529,6 @@ set(MC_SRC
   src/mc/explo/udpor/Configuration.cpp
   src/mc/explo/udpor/EventSet.cpp
   src/mc/explo/udpor/EventSet.hpp
-  src/mc/explo/udpor/StateManager.cpp
-  src/mc/explo/udpor/StateManager.hpp
   src/mc/explo/udpor/UnfoldingEvent.cpp
   src/mc/explo/udpor/UnfoldingEvent.hpp
   src/mc/explo/udpor/Unfolding.cpp