From 061e670ff8857e59d3901377c45ca6565c778018 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Thu, 9 Nov 2023 00:01:46 +0100 Subject: [PATCH] Spit a message when ODPOR is not optimal --- src/mc/explo/DFSExplorer.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index 0fb95fd182..a7c9dcf021 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -8,8 +8,10 @@ #include "src/mc/mc_exit.hpp" #include "src/mc/mc_private.hpp" #include "src/mc/mc_record.hpp" +#include "src/mc/remote/mc_protocol.h" #include "src/mc/transition/Transition.hpp" +#include "xbt/asserts.h" #include "xbt/log.h" #include "xbt/string.hpp" #include "xbt/sysdep.h" @@ -137,6 +139,16 @@ void DFSExplorer::run() : std::get<0>(state->next_transition_guided()); if (next < 0 || not state->is_actor_enabled(next)) { + if (next >= 0) { // Actor is not enabled, then + XBT_INFO("Reduction %s wants to execute a disabled transition %s. If it's ODPOR, ReversibleRace is suboptimal.", + to_c_str(reduction_mode_), + state->get_actors_list().at(next).get_transition()->to_string(true).c_str()); + if (reduction_mode_ == ReductionMode::odpor) { + XBT_INFO("Current trace:"); + for (auto elm : get_textual_trace()) + XBT_ERROR("%s", elm.c_str()); + } + } // If there is no more transition in the current state (or if ODPOR picked an actor that is not enabled -- // ReversibleRace is an overapproximation), backtrace XBT_VERB("%lu actors remain, but none of them need to be interleaved (depth %zu).", state->get_actor_count(), -- 2.20.1