Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Merge branch 'master' of https://framagit.org/simgrid/simgrid
authormlaurent <mathieu.laurent@ens-rennes.fr>
Mon, 20 Mar 2023 15:52:48 +0000 (16:52 +0100)
committermlaurent <mathieu.laurent@ens-rennes.fr>
Mon, 20 Mar 2023 15:52:48 +0000 (16:52 +0100)
1  2 
src/mc/explo/DFSExplorer.cpp
tools/cmake/DefinePackages.cmake

@@@ -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);
  
      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_++;
      }
@@@ -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