Factorize more code between DFSExplo and LivenessExplo, and UDPOR

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 0130455..63765f8 100644 (file)
--- 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<std::string> DFSExplorer::get_textual_trace() // override
-{
-  std::vector<std::string> 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> state)

diff --git a/src/mc/explo/DFSExplorer.hpp b/src/mc/explo/DFSExplorer.hpp
index 6510cfe..27194a8 100644 (file)
--- a/src/mc/explo/DFSExplorer.hpp
+++ b/src/mc/explo/DFSExplorer.hpp
@@ -46,7 +46,6 @@ public:
   explicit DFSExplorer(const std::vector<char*>& args, bool with_dpor, bool need_memory_info = false);
   void run() override;
   RecordTrace get_record_trace() override;
-  std::vector<std::string> 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 7a77588..8bf0110 100644 (file)
--- 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<std::string> Exploration::get_textual_trace()
+{
+  std::vector<std::string> 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 a164bf0..824adcd 100644 (file)
--- 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<std::string> get_textual_trace() = 0;
+  std::vector<std::string> 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 e254683..3d60ef9 100644 (file)
--- 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<Pair> 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<std::string> LivenessChecker::get_textual_trace() // override
-{
-  std::vector<std::string> trace;
-  for (std::shared_ptr<Pair> 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<Pair> LivenessChecker::create_pair(const Pair* current_pair, xbt_automaton_state_t state,
                                                    std::shared_ptr<const std::vector<int>> propositions)
 {

diff --git a/src/mc/explo/LivenessChecker.hpp b/src/mc/explo/LivenessChecker.hpp
index 532f639..baed48e 100644 (file)
--- 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<std::string> get_textual_trace() override;
   void log_state() override;
 
 private:

diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp
index 6d913b2..e367890 100644 (file)
--- 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<std::string> UdporChecker::get_textual_trace()
-{
-  std::vector<std::string> 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 6706d2b..0e23ab0 100644 (file)
--- 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<std::string> get_textual_trace() override;
   std::unique_ptr<State> get_current_state() { return std::make_unique<State>(get_remote_app()); }
 
 private:

diff --git a/src/mc/mc_record.cpp b/src/mc/mc_record.cpp
index f639107..63d9fc0 100644 (file)
--- 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 2958780..753ffaf 100644 (file)
--- 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<Transition*>::const_iterator begin() const { return transitions_.begin(); }
+  std::vector<Transition*>::const_iterator end() const { return transitions_.end(); }
 
   /** Replay all transitions of a trace */
   void replay() const;