further reduce the amount of call sites for RemoteProcess::actors()

diff --git a/src/mc/VisitedState.cpp b/src/mc/VisitedState.cpp
index 5ad4043..5e45f71 100644 (file)
--- a/src/mc/VisitedState.cpp
+++ b/src/mc/VisitedState.cpp
@@ -17,10 +17,10 @@ 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) : num(state_number)
+VisitedState::VisitedState(unsigned long state_number, unsigned int actor_count)
+    : actor_count_(actor_count), num(state_number)
 {
   this->heap_bytes_used = Api::get().get_remote_heap_bytes();
-  this->actors_count    = mc_model_checker->get_remote_process().actors().size();
   this->system_state = std::make_shared<simgrid::mc::Snapshot>(state_number);
 }
 
@@ -42,7 +42,7 @@ void VisitedStates::prune()
 std::unique_ptr<simgrid::mc::VisitedState>
 VisitedStates::addVisitedState(unsigned long state_number, simgrid::mc::State* graph_state, bool compare_snapshots)
 {
-  auto new_state             = std::make_unique<simgrid::mc::VisitedState>(state_number);
+  auto new_state = std::make_unique<simgrid::mc::VisitedState>(state_number, graph_state->get_actor_count());
   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 33f3d1a..50ef93f 100644 (file)
--- a/src/mc/VisitedState.hpp
+++ b/src/mc/VisitedState.hpp
@@ -18,11 +18,11 @@ class XBT_PRIVATE VisitedState {
 public:
   std::shared_ptr<simgrid::mc::Snapshot> system_state = nullptr;
   std::size_t heap_bytes_used = 0;
-  int actors_count            = 0;
-  long num                                            = 0; // unique id of that state in the storage of all stored IDs
+  int actor_count_;
+  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);
+  explicit VisitedState(unsigned long state_number, unsigned int actor_count);
 };
 
 class XBT_PRIVATE VisitedStates {

diff --git a/src/mc/api.hpp b/src/mc/api.hpp
index c30d999..2a9d250 100644 (file)
--- a/src/mc/api.hpp
+++ b/src/mc/api.hpp
@@ -36,7 +36,7 @@ private:
   struct DerefAndCompareByActorsCountAndUsedHeap {
     template <class X, class Y> bool operator()(X const& a, Y const& b) const
     {
-      return std::make_pair(a->actors_count, a->heap_bytes_used) < std::make_pair(b->actors_count, b->heap_bytes_used);
+      return std::make_pair(a->actor_count_, a->heap_bytes_used) < std::make_pair(b->actor_count_, b->heap_bytes_used);
     }
   };
 

diff --git a/src/mc/compare.cpp b/src/mc/compare.cpp
index 6b7ffe1..a59f4c7 100644 (file)
--- a/src/mc/compare.cpp
+++ b/src/mc/compare.cpp
@@ -1188,11 +1188,7 @@ bool snapshot_equal(const Snapshot* s1, const Snapshot* s2)
   }
   XBT_VERB("(%ld - %ld) Same hash: 0x%" PRIx64, s1->num_state_, s2->num_state_, s1->hash_);
 
-  /* Compare enabled processes */
-  if (s1->enabled_processes_ != s2->enabled_processes_) {
-    XBT_VERB("(%ld - %ld) Different amount of enabled processes", s1->num_state_, s2->num_state_);
-    return false;
-  }
+  /* TODO: re-enable the quick filter of counting enabled processes in each snapshots */
 
   /* Compare size of stacks */
   for (unsigned long i = 0; i < s1->stacks_.size(); i++) {

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 76825fa..d7e0f1e 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -126,10 +126,10 @@ void DFSExplorer::run()
     int next = state->next_transition();
 
     if (next < 0) { // If there is no more transition in the current state, backtrack.
-      XBT_DEBUG("There remains %zu actors, but none to interleave (depth %zu).",
-                mc_model_checker->get_remote_process().actors().size(), stack_.size() + 1);
+      XBT_DEBUG("There remains %d actors, but none to interleave (depth %zu).", state->get_actor_count(),
+                stack_.size() + 1);
 
-      if (mc_model_checker->get_remote_process().actors().empty()) {
+      if (state->get_actor_count() == 0) {
         mc_model_checker->finalize_app();
         XBT_VERB("Execution came to an end at %s (state: %ld, depth: %zu)", get_record_trace().to_string().c_str(),
                  state->get_num(), stack_.size());

diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp
index 64d9f36..cc418c5 100644 (file)
--- a/src/mc/explo/LivenessChecker.cpp
+++ b/src/mc/explo/LivenessChecker.cpp
@@ -27,7 +27,7 @@ VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state,
   if (not this->graph_state->get_system_state())
     this->graph_state->set_system_state(std::make_shared<Snapshot>(pair_num));
   this->heap_bytes_used     = Api::get().get_remote_heap_bytes();
-  this->actors_count        = mc_model_checker->get_remote_process().actors().size();
+  this->actor_count_        = mc_model_checker->get_remote_process().actors().size();
   this->other_num           = -1;
   this->atomic_propositions = std::move(atomic_propositions);
 }

diff --git a/src/mc/explo/LivenessChecker.hpp b/src/mc/explo/LivenessChecker.hpp
index 31aa65c..a783d46 100644 (file)
--- a/src/mc/explo/LivenessChecker.hpp
+++ b/src/mc/explo/LivenessChecker.hpp
@@ -42,7 +42,7 @@ public:
   xbt_automaton_state_t automaton_state;
   std::shared_ptr<const std::vector<int>> atomic_propositions;
   std::size_t heap_bytes_used = 0;
-  int actors_count            = 0;
+  int actor_count_;
 
   VisitedPair(int pair_num, xbt_automaton_state_t automaton_state,
               std::shared_ptr<const std::vector<int>> atomic_propositions, std::shared_ptr<State> graph_state);

diff --git a/src/mc/sosp/Snapshot.cpp b/src/mc/sosp/Snapshot.cpp
index 6b07c1f..bf91e7c 100644 (file)
--- a/src/mc/sosp/Snapshot.cpp
+++ b/src/mc/sosp/Snapshot.cpp
@@ -203,9 +203,6 @@ Snapshot::Snapshot(long num_state, RemoteProcess* process) : AddressSpace(proces
 {
   XBT_DEBUG("Taking snapshot %ld", num_state);
 
-  for (auto const& p : process->actors())
-    enabled_processes_.insert(p.copy.get_buffer()->get_pid());
-
   snapshot_handle_ignore(this);
 
   /* Save the std heap and the writable mapped pages of libsimgrid and binary */

diff --git a/src/mc/sosp/Snapshot.hpp b/src/mc/sosp/Snapshot.hpp
index 412c7b9..dec7ffe 100644 (file)
--- a/src/mc/sosp/Snapshot.hpp
+++ b/src/mc/sosp/Snapshot.hpp
@@ -78,7 +78,6 @@ public:
   long num_state_;
   std::size_t heap_bytes_used_ = 0;
   std::vector<std::unique_ptr<Region>> snapshot_regions_;
-  std::set<pid_t> enabled_processes_;
   std::vector<std::size_t> stack_sizes_;
   std::vector<s_mc_snapshot_stack_t> stacks_;
   std::vector<simgrid::mc::IgnoredHeapRegion> to_ignore_;