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 ***");
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.
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_++;
}
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
)
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