From 753ea77ea991c7e407d6731839d5f7dbcc24f7e2 Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Mon, 20 Feb 2023 13:54:05 +0100 Subject: [PATCH] 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 --- MANIFEST.in | 2 -- src/mc/explo/UdporChecker.cpp | 1 + src/mc/explo/UdporChecker.hpp | 7 ----- src/mc/explo/udpor/StateManager.cpp | 38 ---------------------------- src/mc/explo/udpor/StateManager.hpp | 29 --------------------- src/mc/explo/udpor/udpor_forward.hpp | 1 - tools/cmake/DefinePackages.cmake | 2 -- 7 files changed, 1 insertion(+), 79 deletions(-) delete mode 100644 src/mc/explo/udpor/StateManager.cpp delete mode 100644 src/mc/explo/udpor/StateManager.hpp diff --git a/MANIFEST.in b/MANIFEST.in index 0863de72a5..1decdf051d 100644 --- 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 da236e29c8..fdd3680134 100644 --- 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 #include diff --git a/src/mc/explo/UdporChecker.hpp b/src/mc/explo/UdporChecker.hpp index cc1604ab35..e63802bb38 100644 --- 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 index 81792ce985..0000000000 --- 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) -{ - 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> 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>{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 index f02b9763f9..0000000000 --- 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 - -namespace simgrid::mc::udpor { - -class StateManager { -private: - using Handle = StateHandle; - - Handle current_handle_ = 1ul; - std::unordered_map> state_map_; - -public: - Handle record_state(std::unique_ptr); - std::optional> 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 ab28a5a970..c8b12c05ff 100644 --- 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 0746dc418e..054bc132ec 100644 --- 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 -- 2.20.1