MC: display the 100 first transitions when we reach the depth-limit

diff --git a/src/mc/api/strategy/BasicStrategy.hpp b/src/mc/api/strategy/BasicStrategy.hpp
index fd28633..de0fe65 100644 (file)
--- a/src/mc/api/strategy/BasicStrategy.hpp
+++ b/src/mc/api/strategy/BasicStrategy.hpp
@@ -7,13 +7,17 @@
 #define SIMGRID_MC_BASICSTRATEGY_HPP
 
 #include "Strategy.hpp"
+#include "src/mc/explo/Exploration.hpp"
+
+XBT_LOG_EXTERNAL_CATEGORY(mc_dfs);
 
 namespace simgrid::mc {
 
 /** Basic MC guiding class which corresponds to no guide. When asked for different states
  *  it will follow a depth first search politics to minize the number of opened states. */
 class BasicStrategy : public Strategy {
-    int depth_ = _sg_mc_max_depth; // Arbitrary starting point. next_transition must return a positiv value to work with threshold in DFSExplorer
+  int depth_ = _sg_mc_max_depth; // Arbitrary starting point. next_transition must return a positive value to work with
+                                 // threshold in DFSExplorer
 
 public:
   void copy_from(const Strategy* strategy) override
@@ -21,7 +25,16 @@ public:
     const auto* cast_strategy = dynamic_cast<BasicStrategy const*>(strategy);
     xbt_assert(cast_strategy != nullptr);
     depth_ = cast_strategy->depth_ - 1;
-    xbt_assert(depth_ > 0, "The exploration reached a depth greater than %d. We will stop here to prevent weird interaction with DFSExplorer. If you want to change that behaviour, you should augment the size of the search by using --cfg=model-check/max-depth:", _sg_mc_max_depth.get());
+    if (depth_ <= 0) {
+      XBT_CERROR(mc_dfs,
+                 "The exploration reached a depth greater than %d. Change the depth limit with "
+                 "--cfg=model-check/max-depth. Here are the 100 first trace elements",
+                 _sg_mc_max_depth.get());
+      auto trace = Exploration::get_instance()->get_textual_trace(100);
+      for (auto elm : trace)
+        XBT_CERROR(mc_dfs, "  %s", elm.c_str());
+      xbt_die("Aborting now.");
+    }
   }
   BasicStrategy()                     = default;
   ~BasicStrategy() override           = default;

diff --git a/src/mc/explo/Exploration.cpp b/src/mc/explo/Exploration.cpp
index 3c8e650..d219abd 100644 (file)
--- a/src/mc/explo/Exploration.cpp
+++ b/src/mc/explo/Exploration.cpp
@@ -83,7 +83,7 @@ static const char* signal_name(int status)
   }
 }
 
-std::vector<std::string> Exploration::get_textual_trace()
+std::vector<std::string> Exploration::get_textual_trace(int max_elements)
 {
   std::vector<std::string> trace;
   for (auto const& transition : get_record_trace()) {
@@ -93,6 +93,9 @@ std::vector<std::string> Exploration::get_textual_trace()
                                          transition->to_string().c_str()));
     else
       trace.push_back(xbt::string_printf("Actor %ld in simcall %s", transition->aid_, transition->to_string().c_str()));
+    max_elements--;
+    if (max_elements == 0)
+      break;
   }
   return trace;
 }

diff --git a/src/mc/explo/Exploration.hpp b/src/mc/explo/Exploration.hpp
index 64114d4..571ed19 100644 (file)
--- a/src/mc/explo/Exploration.hpp
+++ b/src/mc/explo/Exploration.hpp
@@ -60,7 +60,7 @@ public:
   virtual RecordTrace get_record_trace() = 0;
 
   /** Generate a textual execution trace of the simulated application */
-  std::vector<std::string> get_textual_trace();
+  std::vector<std::string> get_textual_trace(int max_elements = -1);
 
   /** Log additional information about the state of the model-checker */
   virtual void log_state();