Add iterator files to xbt/utils

[simgrid.git] / src / mc / explo / LivenessChecker.cpp

diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp
index 26fb2a8de3e219960bc404901270a822421eb9b0..7466bce11c20255344dac99a5203c3579327a70d 100644 (file)
--- a/src/mc/explo/LivenessChecker.cpp
+++ b/src/mc/explo/LivenessChecker.cpp
@@ -1,4 +1,4 @@
-/* Copyright (c) 2011-2022. The SimGrid Team. All rights reserved.          */
+/* Copyright (c) 2011-2023. The SimGrid Team. All rights reserved.          */
 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
@@ -180,13 +180,12 @@ void LivenessChecker::purge_visited_pairs()
 LivenessChecker::LivenessChecker(const std::vector<char*>& args) : Exploration(args) {}
 LivenessChecker::~LivenessChecker()
 {
-  if (property_automaton_ != nullptr)
-    xbt_automaton_free(property_automaton_);
+  xbt_automaton_free(property_automaton_);
 }
 
 xbt_automaton_t LivenessChecker::property_automaton_ = nullptr;
 
-void LivenessChecker::automaton_load(const char* file)
+void LivenessChecker::automaton_load(const char* file) const
 {
   if (property_automaton_ == nullptr)
     property_automaton_ = xbt_automaton_new();
@@ -242,7 +241,8 @@ xbt_automaton_state_t LivenessChecker::get_automaton_transition_dst(xbt_dynar_t
   const xbt_automaton_transition* transition = xbt_dynar_get_as(dynar, index, xbt_automaton_transition_t);
   return transition->dst;
 }
-void LivenessChecker::automaton_register_symbol(RemoteProcess& remote_process, const char* name, RemotePtr<int> address)
+void LivenessChecker::automaton_register_symbol(RemoteProcess const& remote_process, const char* name,
+                                                RemotePtr<int> address)
 {
   if (property_automaton_ == nullptr)
     property_automaton_ = xbt_automaton_new();
@@ -275,7 +275,9 @@ void LivenessChecker::show_acceptance_cycle(std::size_t depth)
   XBT_INFO("Counter-example that violates formula:");
   for (auto const& s : this->get_textual_trace())
     XBT_INFO("  %s", s.c_str());
-  XBT_INFO("Path = %s", get_record_trace().to_string().c_str());
+  XBT_INFO("You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with "
+           "--cfg=model-check/replay:'%s'",
+           get_record_trace().to_string().c_str());
   log_state();
   XBT_INFO("Counter-example depth: %zu", depth);
 }