From: mlaurent <mathieu.laurent@ens-rennes.fr>
Date: Mon, 20 Mar 2023 15:52:48 +0000 (+0100)
Subject: Merge branch 'master' of https://framagit.org/simgrid/simgrid
X-Git-Tag: v3.34~240^2~13
X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/41966a6d30f870c0c7cc5ad5e64c0263e63970a8?hp=-c

Merge branch 'master' of https://framagit.org/simgrid/simgrid
---

41966a6d30f870c0c7cc5ad5e64c0263e63970a8
diff --combined src/mc/explo/DFSExplorer.cpp
index e61a25013a,98396111b1..c58d581120
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@@ -42,7 -42,8 +42,8 @@@ xbt::signal<void(RemoteApp&)> DFSExplor
  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 ***");
@@@ -173,7 -174,7 +174,7 @@@ void DFSExplorer::run(
      XBT_DEBUG("Marking Transition >>%s<< of process %ld done and adding it to the sleep set",
                state->get_transition()->to_string().c_str(), state->get_transition()->aid_);
      state->add_sleep_set(state->get_transition()); // Actors are marked done when they are considerd in ActorState
 -    
 +
      /* DPOR persistent set procedure:
       * for each new transition considered, check if it depends on any other previous transition executed before it
       * on another process. If there exists one, find the more recent, and add its process to the interleave set.
@@@ -259,6 -260,7 +260,6 @@@ void DFSExplorer::backtrack(
  
      stack_.pop_back();
  
 -
      if (state->count_todo() == 0) { // Empty interleaving set: exploration at this level is over
        XBT_DEBUG("Delete state %ld at depth %zu", state->get_num(), stack_.size() + 1);
  
@@@ -288,7 -290,7 +289,7 @@@
      for (std::unique_ptr<State> const& state : stack_) {
        if (state == stack_.back()) /* If we are arrived on the target state, don't replay the outgoing transition */
          break;
-       state->get_transition()->replay();
+       state->get_transition()->replay(get_remote_app());
        on_transition_replay_signal(state->get_transition(), get_remote_app());
        visited_states_count_++;
      }
diff --combined tools/cmake/DefinePackages.cmake
index be3a5561a1,6ed5d73c04..528ed022ba
--- a/tools/cmake/DefinePackages.cmake
+++ b/tools/cmake/DefinePackages.cmake
@@@ -598,26 -598,23 +598,27 @@@ set(MC_SR
    src/mc/transition/TransitionSynchro.cpp
    src/mc/transition/TransitionSynchro.hpp
  
-   src/mc/AddressSpace.hpp
-   src/mc/ModelChecker.cpp
-   src/mc/ModelChecker.hpp
-   src/mc/VisitedState.cpp
-   src/mc/VisitedState.hpp
+   src/mc/api/guide/BasicGuide.hpp
+   src/mc/api/guide/GuidedState.hpp
    src/mc/api/ActorState.hpp
    src/mc/api/State.cpp
    src/mc/api/State.hpp
    src/mc/api/RemoteApp.cpp
    src/mc/api/RemoteApp.hpp
+ 
+   src/mc/AddressSpace.hpp
+   src/mc/VisitedState.cpp
+   src/mc/VisitedState.hpp
    src/mc/compare.cpp
    src/mc/mc_exit.hpp
    src/mc/mc_forward.hpp
    src/mc/mc_private.hpp
    src/mc/mc_record.cpp
  
 +  src/mc/api/guide/BasicGuide.hpp
 +  src/mc/api/guide/GuidedState.hpp
 +  src/mc/api/guide/WaitGuide.hpp
 +  
    src/xbt/mmalloc/mm_interface.c
    )
  
@@@ -1054,6 -1051,7 +1055,7 @@@ set(CMAKE_SOURCE_FILE
    tools/cmake/Modules/FindNS3.cmake
    tools/cmake/Modules/FindPAPI.cmake
    tools/cmake/Modules/FindValgrind.cmake
+   tools/cmake/Modules/nlohmann_jsonConfig.cmake
    tools/cmake/Modules/pybind11Config.cmake
    tools/cmake/Option.cmake
    tools/cmake/Tests.cmake