Merge branch 'udpor-phase4' into 'master'

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

diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp
index 8f1ecb22d92708862647fbbf1d07d9428d2844b2..c0929f102f2426d4fc55c822c38368b2fc3662ab 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. */
@@ -19,12 +19,13 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc, "Logging specific to algorithms
 namespace simgrid::mc {
 
 VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t prop_state,
-                         std::shared_ptr<const std::vector<int>> atomic_propositions, std::shared_ptr<State> app_state)
+                         std::shared_ptr<const std::vector<int>> atomic_propositions, std::shared_ptr<State> app_state,
+                         RemoteApp& remote_app)
     : num(pair_num), prop_state_(prop_state)
 {
   this->app_state_ = std::move(app_state);
   if (not this->app_state_->get_system_state())
-    this->app_state_->set_system_state(std::make_shared<Snapshot>(pair_num));
+    this->app_state_->set_system_state(std::make_shared<Snapshot>(pair_num, remote_app.get_page_store()));
   this->heap_bytes_used     = mc_model_checker->get_remote_process().get_remote_heap_bytes();
   this->actor_count_        = app_state_->get_actor_count();
   this->other_num           = -1;
@@ -59,8 +60,8 @@ std::shared_ptr<const std::vector<int>> LivenessChecker::get_proposition_values(
 
 std::shared_ptr<VisitedPair> LivenessChecker::insert_acceptance_pair(simgrid::mc::Pair* pair)
 {
-  auto new_pair =
-      std::make_shared<VisitedPair>(pair->num, pair->prop_state_, pair->atomic_propositions, pair->app_state_);
+  auto new_pair = std::make_shared<VisitedPair>(pair->num, pair->prop_state_, pair->atomic_propositions,
+                                                pair->app_state_, get_remote_app());
 
   auto [res_begin,
         res_end] = boost::range::equal_range(acceptance_pairs_, new_pair.get(), [](auto const& a, auto const& b) {
@@ -76,8 +77,7 @@ std::shared_ptr<VisitedPair> LivenessChecker::insert_acceptance_pair(simgrid::mc
         continue;
       XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
       exploration_stack_.pop_back();
-      mc_model_checker->dot_output("\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, pair_test->num,
-                                   this->previous_request_.c_str());
+      dot_output("\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, pair_test->num, this->previous_request_.c_str());
       return nullptr;
     }
 
@@ -138,8 +138,8 @@ int LivenessChecker::insert_visited_pair(std::shared_ptr<VisitedPair> visited_pa
     return -1;
 
   if (visited_pair == nullptr)
-    visited_pair =
-        std::make_shared<VisitedPair>(pair->num, pair->prop_state_, pair->atomic_propositions, pair->app_state_);
+    visited_pair = std::make_shared<VisitedPair>(pair->num, pair->prop_state_, pair->atomic_propositions,
+                                                 pair->app_state_, get_remote_app());
 
   auto [range_begin,
         range_end] = boost::range::equal_range(visited_pairs_, visited_pair.get(), [](auto const& a, auto const& b) {
@@ -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);
 }
@@ -387,9 +389,7 @@ void LivenessChecker::run()
     if (not current_pair->exploration_started) {
       int visited_num = this->insert_visited_pair(reached_pair, current_pair.get());
       if (visited_num != -1) {
-        mc_model_checker->dot_output("\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, visited_num,
-                                     this->previous_request_.c_str());
-        mc_model_checker->dot_output_flush();
+        dot_output("\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, visited_num, this->previous_request_.c_str());
 
         XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num);
         current_pair->requests = 0;
@@ -403,15 +403,13 @@ void LivenessChecker::run()
 
     /* Update the dot output */
     if (this->previous_pair_ != 0 && this->previous_pair_ != current_pair->num) {
-      mc_model_checker->dot_output("\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, current_pair->num,
-                                   this->previous_request_.c_str());
+      dot_output("\"%d\" -> \"%d\" [%s];\n", this->previous_pair_, current_pair->num, this->previous_request_.c_str());
       this->previous_request_.clear();
     }
     this->previous_pair_    = current_pair->num;
     this->previous_request_ = current_pair->app_state_->get_transition()->dot_string();
     if (current_pair->search_cycle)
-      mc_model_checker->dot_output("%d [shape=doublecircle];\n", current_pair->num);
-    mc_model_checker->dot_output_flush();
+      dot_output("%d [shape=doublecircle];\n", current_pair->num);
 
     if (not current_pair->exploration_started)
       visited_pairs_count_++;