[mc] Let the Checker give us the current trace

[simgrid.git] / src / mc / SafetyChecker.cpp

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index e1b87d3..2c9ca22 100644 (file)
--- a/src/mc/SafetyChecker.cpp
+++ b/src/mc/SafetyChecker.cpp
@@ -39,7 +39,8 @@ static void MC_show_non_termination(void)
   XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
   XBT_INFO("******************************************");
   XBT_INFO("Counter-example execution trace:");
-  MC_dump_stack_safety(mc_stack);
+  for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
+    XBT_INFO("%s", s.c_str());
   MC_print_statistics(mc_stats);
 }
 
@@ -66,6 +67,44 @@ static int is_exploration_stack_state(mc_state_t current_state){
   return 0;
 }
 
+RecordTrace SafetyChecker::getRecordTrace() // override
+{
+  RecordTrace res;
+
+  xbt_fifo_item_t start = xbt_fifo_get_last_item(mc_stack);
+  for (xbt_fifo_item_t item = start; item; item = xbt_fifo_get_prev_item(item)) {
+
+    // Find (pid, value):
+    mc_state_t state = (mc_state_t) xbt_fifo_get_item_content(item);
+    int value = 0;
+    smx_simcall_t saved_req = MC_state_get_executed_request(state, &value);
+    const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
+    const int pid = issuer->pid;
+
+    res.push_back(RecordTraceElement(pid, value));
+  }
+
+  return std::move(res);
+}
+
+std::vector<std::string> SafetyChecker::getTextualTrace() // override
+{
+  std::vector<std::string> trace;
+  for (xbt_fifo_item_t item = xbt_fifo_get_last_item(mc_stack);
+       item; item = xbt_fifo_get_prev_item(item)) {
+    mc_state_t state = (mc_state_t)xbt_fifo_get_item_content(item);
+    int value;
+    smx_simcall_t req = MC_state_get_executed_request(state, &value);
+    if (req) {
+      char* req_str = simgrid::mc::request_to_string(
+        req, value, simgrid::mc::RequestType::executed);
+      trace.push_back(req_str);
+      xbt_free(req_str);
+    }
+  }
+  return std::move(trace);
+}
+
 int SafetyChecker::run()
 {
   this->init();