From: Martin Quinson Date: Thu, 27 Apr 2023 23:25:04 +0000 (+0200) Subject: Factorize more code between DFSExplo and LivenessExplo, and UDPOR X-Git-Tag: v3.34~135 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/76fd6cc1330945172740464411a0b2f1170dcb2a Factorize more code between DFSExplo and LivenessExplo, and UDPOR --- diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index 0130455d79..63765f80cf 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -71,19 +71,9 @@ RecordTrace DFSExplorer::get_record_trace() // override RecordTrace res; for (auto const& transition : stack_.back()->get_recipe()) res.push_back(transition); - res.push_back(stack_.back()->get_transition_out().get()); - return res; -} - -std::vector DFSExplorer::get_textual_trace() // override -{ - std::vector trace; - for (auto const& transition : stack_.back()->get_recipe()) { - trace.push_back(xbt::string_printf("%ld: %s", transition->aid_, transition->to_string().c_str())); - } if (const auto trans = stack_.back()->get_transition_out(); trans != nullptr) - trace.push_back(xbt::string_printf("%ld: %s", trans->aid_, trans->to_string().c_str())); - return trace; + res.push_back(stack_.back()->get_transition_out().get()); + return res; } void DFSExplorer::restore_stack(std::shared_ptr state) diff --git a/src/mc/explo/DFSExplorer.hpp b/src/mc/explo/DFSExplorer.hpp index 6510cfe220..27194a8b46 100644 --- a/src/mc/explo/DFSExplorer.hpp +++ b/src/mc/explo/DFSExplorer.hpp @@ -46,7 +46,6 @@ public: explicit DFSExplorer(const std::vector& args, bool with_dpor, bool need_memory_info = false); void run() override; RecordTrace get_record_trace() override; - std::vector get_textual_trace() override; void log_state() override; /** Called once when the exploration starts */ diff --git a/src/mc/explo/Exploration.cpp b/src/mc/explo/Exploration.cpp index 7a77588d61..8bf01108a3 100644 --- a/src/mc/explo/Exploration.cpp +++ b/src/mc/explo/Exploration.cpp @@ -8,6 +8,7 @@ #include "src/mc/mc_environ.h" #include "src/mc/mc_exit.hpp" #include "src/mc/mc_private.hpp" +#include "xbt/string.hpp" #if SIMGRID_HAVE_STATEFUL_MC #include "src/mc/sosp/RemoteProcessMemory.hpp" @@ -81,6 +82,15 @@ static const char* signal_name(int status) return strsignal(WTERMSIG(status)); } } + +std::vector Exploration::get_textual_trace() +{ + std::vector trace; + for (auto const& transition : get_record_trace()) + trace.push_back(xbt::string_printf("%ld: %s", transition->aid_, transition->to_string().c_str())); + return trace; +} + XBT_ATTRIB_NORETURN void Exploration::report_crash(int status) { XBT_INFO("**************************"); diff --git a/src/mc/explo/Exploration.hpp b/src/mc/explo/Exploration.hpp index a164bf0a8f..824adcd3f7 100644 --- a/src/mc/explo/Exploration.hpp +++ b/src/mc/explo/Exploration.hpp @@ -55,13 +55,11 @@ public: * to get and display information about the current state of the * model-checking algorithm: */ - /** Show the current trace/stack - * - * Could this be handled in the Session/ModelChecker instead? */ + /** Retrieve the current stack to build an execution trace */ virtual RecordTrace get_record_trace() = 0; /** Generate a textual execution trace of the simulated application */ - virtual std::vector get_textual_trace() = 0; + std::vector get_textual_trace(); /** Log additional information about the state of the model-checker */ virtual void log_state(); diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp index e254683fa6..3d60ef96e4 100644 --- a/src/mc/explo/LivenessChecker.cpp +++ b/src/mc/explo/LivenessChecker.cpp @@ -258,7 +258,8 @@ RecordTrace LivenessChecker::get_record_trace() // override { RecordTrace res; for (std::shared_ptr const& pair : exploration_stack_) - res.push_back(pair->app_state_->get_transition_out().get()); + if (pair->app_state_->get_transition_out() != nullptr) + res.push_back(pair->app_state_->get_transition_out().get()); return res; } @@ -285,16 +286,6 @@ void LivenessChecker::show_acceptance_cycle(std::size_t depth) XBT_INFO("Counter-example depth: %zu", depth); } -std::vector LivenessChecker::get_textual_trace() // override -{ - std::vector trace; - for (std::shared_ptr const& pair : exploration_stack_) - if (pair->app_state_->get_transition_out() != nullptr) - trace.push_back(pair->app_state_->get_transition_out()->to_string()); - - return trace; -} - std::shared_ptr LivenessChecker::create_pair(const Pair* current_pair, xbt_automaton_state_t state, std::shared_ptr> propositions) { diff --git a/src/mc/explo/LivenessChecker.hpp b/src/mc/explo/LivenessChecker.hpp index 532f6395a8..baed48eb0f 100644 --- a/src/mc/explo/LivenessChecker.hpp +++ b/src/mc/explo/LivenessChecker.hpp @@ -56,7 +56,6 @@ public: void run() override; RecordTrace get_record_trace() override; - std::vector get_textual_trace() override; void log_state() override; private: diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp index 6d913b2b96..e367890ea9 100644 --- a/src/mc/explo/UdporChecker.cpp +++ b/src/mc/explo/UdporChecker.cpp @@ -325,16 +325,6 @@ RecordTrace UdporChecker::get_record_trace() return res; } -std::vector UdporChecker::get_textual_trace() -{ - std::vector trace; - for (auto const& state : state_stack) { - const auto t = state->get_transition_out(); - trace.push_back(xbt::string_printf("%ld: %s", t->aid_, t->to_string().c_str())); - } - return trace; -} - } // namespace simgrid::mc::udpor namespace simgrid::mc { diff --git a/src/mc/explo/UdporChecker.hpp b/src/mc/explo/UdporChecker.hpp index 6706d2bc6b..0e23ab0a24 100644 --- a/src/mc/explo/UdporChecker.hpp +++ b/src/mc/explo/UdporChecker.hpp @@ -38,7 +38,6 @@ public: void run() override; RecordTrace get_record_trace() override; - std::vector get_textual_trace() override; std::unique_ptr get_current_state() { return std::make_unique(get_remote_app()); } private: diff --git a/src/mc/mc_record.cpp b/src/mc/mc_record.cpp index f63910724a..63d9fc0680 100644 --- a/src/mc/mc_record.cpp +++ b/src/mc/mc_record.cpp @@ -51,7 +51,7 @@ void RecordTrace::replay() const const auto& actor_list = engine->get_actor_list(); if (actor_list.empty()) { XBT_INFO("The replay of the trace is complete. The application is terminating."); - } else if (std::none_of(begin(actor_list), end(actor_list), + } else if (std::none_of(std::begin(actor_list), std::end(actor_list), [](const auto& kv) { return mc::actor_is_enabled(kv.second); })) { XBT_INFO("The replay of the trace is complete. DEADLOCK detected."); engine->display_all_actor_status(); diff --git a/src/mc/mc_record.hpp b/src/mc/mc_record.hpp index 2958780644..753ffafa9f 100644 --- a/src/mc/mc_record.hpp +++ b/src/mc/mc_record.hpp @@ -36,6 +36,8 @@ public: std::string to_string() const; void push_back(Transition* t) { transitions_.push_back(t); } + std::vector::const_iterator begin() const { return transitions_.begin(); } + std::vector::const_iterator end() const { return transitions_.end(); } /** Replay all transitions of a trace */ void replay() const;