From a88428006c545383c30052e5606b3f8e895bd9d8 Mon Sep 17 00:00:00 2001 From: Arnaud Giersch Date: Sat, 4 Mar 2023 10:35:59 +0100 Subject: [PATCH] Walking the stack in the forward direction gives the same result, but makes the code simpler. --- src/mc/explo/DFSExplorer.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index 2739857961..05b607b850 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -41,9 +41,9 @@ xbt::signal DFSExplorer::on_log_state_signal; void DFSExplorer::check_non_termination(const State* current_state) { - for (auto state = stack_.rbegin(); state != stack_.rend(); ++state) - if (*(*state)->get_system_state() == *current_state->get_system_state()) { - XBT_INFO("Non-progressive cycle: state %ld -> state %ld", (*state)->get_num(), current_state->get_num()); + for (auto const& state : stack_) { + if (*state->get_system_state() == *current_state->get_system_state()) { + 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_INFO("******************************************"); @@ -57,6 +57,7 @@ void DFSExplorer::check_non_termination(const State* current_state) throw TerminationError(); } + } } RecordTrace DFSExplorer::get_record_trace() // override -- 2.20.1