One reference to the global singleton mc_model_checker that I'd like to kill

diff --git a/src/mc/VisitedState.cpp b/src/mc/VisitedState.cpp
index e8fde38..e067dfb 100644 (file)
--- a/src/mc/VisitedState.cpp
+++ b/src/mc/VisitedState.cpp
@@ -18,10 +18,9 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_VisitedState, mc, "Logging specific to state
 namespace simgrid::mc {
 
 /** @brief Save the current state */
-VisitedState::VisitedState(unsigned long state_number, unsigned int actor_count)
-    : actor_count_(actor_count), num_(state_number)
+VisitedState::VisitedState(unsigned long state_number, unsigned int actor_count, std::size_t heap_bytes_used)
+    : heap_bytes_used_(heap_bytes_used), actor_count_(actor_count), num_(state_number)
 {
-  this->heap_bytes_used_ = mc_model_checker->get_remote_process().get_remote_heap_bytes();
   this->system_state_    = std::make_shared<simgrid::mc::Snapshot>(state_number);
 }
 
@@ -40,10 +39,12 @@ void VisitedStates::prune()
 }
 
 /** @brief Checks whether a given state has already been visited by the algorithm. */
-std::unique_ptr<simgrid::mc::VisitedState> VisitedStates::addVisitedState(unsigned long state_number,
-                                                                          simgrid::mc::State* graph_state)
+std::unique_ptr<simgrid::mc::VisitedState>
+VisitedStates::addVisitedState(unsigned long state_number, simgrid::mc::State* graph_state, std::size_t heap_bytes_used)
 {
-  auto new_state = std::make_unique<simgrid::mc::VisitedState>(state_number, graph_state->get_actor_count());
+  auto new_state =
+      std::make_unique<simgrid::mc::VisitedState>(state_number, graph_state->get_actor_count(), heap_bytes_used);
+
   graph_state->set_system_state(new_state->system_state_);
   XBT_DEBUG("Snapshot %p of visited state %ld (exploration stack state %ld)", new_state->system_state_.get(),
             new_state->num_, graph_state->get_num());

diff --git a/src/mc/VisitedState.hpp b/src/mc/VisitedState.hpp
index b9cb789..e3de838 100644 (file)
--- a/src/mc/VisitedState.hpp
+++ b/src/mc/VisitedState.hpp
@@ -22,15 +22,15 @@ public:
   long num_;               // unique id of that state in the storage of all stored IDs
   long original_num_ = -1; // num field of the VisitedState to which I was declared equal to (used for dot_output)
 
-  explicit VisitedState(unsigned long state_number, unsigned int actor_count);
+  explicit VisitedState(unsigned long state_number, unsigned int actor_count, std::size_t heap_bytes_used);
 };
 
 class XBT_PRIVATE VisitedStates {
   std::vector<std::unique_ptr<simgrid::mc::VisitedState>> states_;
 public:
   void clear() { states_.clear(); }
-  std::unique_ptr<simgrid::mc::VisitedState> addVisitedState(unsigned long state_number,
-                                                             simgrid::mc::State* graph_state);
+  std::unique_ptr<simgrid::mc::VisitedState>
+  addVisitedState(unsigned long state_number, simgrid::mc::State* graph_state, std::size_t heap_bytes_used);
 
 private:
   void prune();

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index d9eb85d..e2f4fe3 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -178,7 +178,8 @@ void DFSExplorer::run()
 
     /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */
     if (_sg_mc_max_visited_states > 0)
-      visited_state_ = visited_states_.addVisitedState(next_state->get_num(), next_state.get());
+      visited_state_ = visited_states_.addVisitedState(next_state->get_num(), next_state.get(),
+                                                       get_remote_app().get_remote_process().get_remote_heap_bytes());
 
     /* If this is a new state (or if we don't care about state-equality reduction) */
     if (visited_state_ == nullptr) {