Another use of mc_model_checker disapears. In Snapshot.equals.

I guess that this could be done in a better way, as noted in the
comment.

diff --git a/src/mc/VisitedState.cpp b/src/mc/VisitedState.cpp
index b974d01..a52b8fc 100644 (file)
--- a/src/mc/VisitedState.cpp
+++ b/src/mc/VisitedState.cpp
@@ -58,7 +58,8 @@ VisitedStates::addVisitedState(unsigned long state_number, simgrid::mc::State* g
 
   for (auto i = range_begin; i != range_end; ++i) {
     auto& visited_state = *i;
-    if (*visited_state->system_state_.get() == *new_state->system_state_.get()) {
+    if (visited_state->system_state_->equals_to(*new_state->system_state_.get(),
+                                                remote_app.get_remote_process_memory())) {
       // The state has been visited:
 
       std::unique_ptr<simgrid::mc::VisitedState> old_state = std::move(visited_state);

diff --git a/src/mc/compare.cpp b/src/mc/compare.cpp
index 71fac79..9fe8072 100644 (file)
--- a/src/mc/compare.cpp
+++ b/src/mc/compare.cpp
@@ -1206,13 +1206,19 @@ static bool local_variables_differ(const simgrid::mc::RemoteProcessMemory& proce
 }
 
 namespace simgrid::mc {
-
-bool Snapshot::operator==(const Snapshot& other)
+bool Snapshot::equals_to(const Snapshot& other, RemoteProcessMemory& memory)
 {
-  // TODO, make this a field of ModelChecker or something similar
-  static StateComparator state_comparator;
+  /* TODO: the memory parameter should be eventually removed. It seems to be there because each snapshot lacks some sort
+    of metadata. That's OK for now (letting appart the fact that we cannot have a nice operator== because we need that
+    extra parameter), but it will fall short when we want to have parallel explorations, with more than one
+    RemoteProcess. At the very least, snapshots will need to know the remote process they are corresponding to, and more
+    probably they will need to embeed all their metadata to let the remoteprocesses die before the end of the
+    exploration. */
+
+  /* TODO: This method should moved to Snapshot.cpp, but it needs the StateComparator that is declared locally to this
+   * file only. */
 
-  RemoteProcessMemory& memory = mc_model_checker->get_remote_process_memory();
+  static StateComparator state_comparator; // TODO, make this a field of a persistant state object
 
   if (hash_ != other.hash_) {
     XBT_VERB("(%ld - %ld) Different hash: 0x%" PRIx64 "--0x%" PRIx64, this->num_state_, other.num_state_, this->hash_,

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 13488a0..9839611 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -42,7 +42,8 @@ xbt::signal<void(RemoteApp&)> DFSExplorer::on_log_state_signal;
 void DFSExplorer::check_non_termination(const State* current_state)
 {
   for (auto const& state : stack_) {
-    if (*state->get_system_state() == *current_state->get_system_state()) {
+    if (state->get_system_state()->equals_to(*current_state->get_system_state(),
+                                             get_remote_app().get_remote_process_memory())) {
       XBT_INFO("Non-progressive cycle: state %ld -> state %ld", state->get_num(), current_state->get_num());
       XBT_INFO("******************************************");
       XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");

diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp
index 60857d8..2ce38b8 100644 (file)
--- a/src/mc/explo/LivenessChecker.cpp
+++ b/src/mc/explo/LivenessChecker.cpp
@@ -74,7 +74,8 @@ std::shared_ptr<VisitedPair> LivenessChecker::insert_acceptance_pair(simgrid::mc
       std::shared_ptr<simgrid::mc::VisitedPair> const& pair_test = *i;
       if (xbt_automaton_state_compare(pair_test->prop_state_, new_pair->prop_state_) != 0 ||
           *(pair_test->atomic_propositions) != *(new_pair->atomic_propositions) ||
-          (*pair_test->app_state_->get_system_state() != *new_pair->app_state_->get_system_state()))
+          (not pair_test->app_state_->get_system_state()->equals_to(*new_pair->app_state_->get_system_state(),
+                                                                    get_remote_app().get_remote_process_memory())))
         continue;
       XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
       exploration_stack_.pop_back();
@@ -151,7 +152,8 @@ int LivenessChecker::insert_visited_pair(std::shared_ptr<VisitedPair> visited_pa
     const VisitedPair* pair_test = i->get();
     if (xbt_automaton_state_compare(pair_test->prop_state_, visited_pair->prop_state_) != 0 ||
         *(pair_test->atomic_propositions) != *(visited_pair->atomic_propositions) ||
-        (*pair_test->app_state_->get_system_state() != *visited_pair->app_state_->get_system_state()))
+        (not pair_test->app_state_->get_system_state()->equals_to(*visited_pair->app_state_->get_system_state(),
+                                                                  get_remote_app().get_remote_process_memory())))
       continue;
     if (pair_test->other_num == -1)
       visited_pair->other_num = pair_test->num;

diff --git a/src/mc/sosp/Snapshot.hpp b/src/mc/sosp/Snapshot.hpp
index 6066335..d584bdf 100644 (file)
--- a/src/mc/sosp/Snapshot.hpp
+++ b/src/mc/sosp/Snapshot.hpp
@@ -77,8 +77,7 @@ public:
   Region* get_region(const void* addr, Region* hinted_region) const;
   void restore(RemoteProcessMemory& memory) const;
 
-  bool operator==(const Snapshot& other);
-  bool operator!=(const Snapshot& other) { return not(*this == other); }
+  bool equals_to(const Snapshot& other, RemoteProcessMemory& memory);
 
   // To be private
   long num_state_;