[mc] Move liveness stats out of mc_stats into LivenessChecker

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

diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp
index 80cffd3..e5613cd 100644 (file)
--- a/src/mc/LivenessChecker.cpp
+++ b/src/mc/LivenessChecker.cpp
@@ -29,6 +29,8 @@
 #include "src/mc/mc_replay.h"
 #include "src/mc/mc_safety.h"
 #include "src/mc/mc_exit.h"
+#include "src/mc/Transition.hpp"
+#include "src/mc/Session.hpp"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
                                 "Logging specific to algorithms for liveness properties verification");
@@ -92,7 +94,7 @@ static bool evaluate_label(
   }
 }
 
-Pair::Pair() : num(++mc_stats->expanded_pairs)
+Pair::Pair(unsigned long expanded_pairs) : num(expanded_pairs)
 {}
 
 Pair::~Pair() {}
@@ -157,7 +159,6 @@ void LivenessChecker::removeAcceptancePair(int pair_num)
 
 void LivenessChecker::prepare(void)
 {
-  mc_model_checker->wait_for_requests();
   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
   initial_global_state->prev_pair = 0;
 
@@ -199,7 +200,7 @@ void LivenessChecker::replay()
 
     if (pair->exploration_started) {
 
-      int value = state->req_num;
+      int req_num = state->transition.argument;
       smx_simcall_t saved_req = &state->executed_req;
 
       smx_simcall_t req = nullptr;
@@ -214,16 +215,15 @@ void LivenessChecker::replay()
         XBT_DEBUG("Replay (depth = %d) : %s (%p)",
           depth,
           simgrid::mc::request_to_string(
-            req, value, simgrid::mc::RequestType::simix).c_str(),
+            req, req_num, simgrid::mc::RequestType::simix).c_str(),
           state.get());
       }
 
-      simgrid::mc::handle_simcall(req, value);
-      mc_model_checker->wait_for_requests();
+      this->getSession().execute(state->transition);
     }
 
     /* Update statistics */
-    mc_stats->visited_pairs++;
+    visitedPairsCount_++;
     mc_stats->executed_transitions++;
 
     depth++;
@@ -297,10 +297,18 @@ RecordTrace LivenessChecker::getRecordTrace() // override
 {
   RecordTrace res;
   for (std::shared_ptr<Pair> const& pair : explorationStack_)
-    res.push_back(pair->graph_state->getRecordElement());
+    res.push_back(pair->graph_state->getTransition());
   return res;
 }
 
+void LivenessChecker::logState() // override
+{
+  Checker::logState();
+  XBT_INFO("Expanded pairs = %lu", expandedPairsCount_);
+  XBT_INFO("Visited pairs = %lu", visitedPairsCount_);
+  XBT_INFO("Executed transitions = %lu", mc_stats->executed_transitions);
+}
+
 void LivenessChecker::showAcceptanceCycle(std::size_t depth)
 {
   XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
@@ -310,7 +318,7 @@ void LivenessChecker::showAcceptanceCycle(std::size_t depth)
   simgrid::mc::dumpRecordPath();
   for (auto& s : this->getTextualTrace())
     XBT_INFO("%s", s.c_str());
-  MC_print_statistics(mc_stats);
+  simgrid::mc::session->logState();
   XBT_INFO("Counter-example depth : %zd", depth);
 }
 
@@ -318,11 +326,11 @@ std::vector<std::string> LivenessChecker::getTextualTrace() // override
 {
   std::vector<std::string> trace;
   for (std::shared_ptr<Pair> const& pair : explorationStack_) {
-    int value = pair->graph_state->req_num;
+    int req_num = pair->graph_state->transition.argument;
     smx_simcall_t req = &pair->graph_state->executed_req;
     if (req && req->call != SIMCALL_NONE)
       trace.push_back(simgrid::mc::request_to_string(
-        req, value, simgrid::mc::RequestType::executed));
+        req, req_num, simgrid::mc::RequestType::executed));
   }
   return trace;
 }
@@ -370,8 +378,8 @@ int LivenessChecker::main(void)
       continue;
     }
 
-    int value;
-    smx_simcall_t req = MC_state_get_request(current_pair->graph_state.get(), &value);
+    smx_simcall_t req = MC_state_get_request(current_pair->graph_state.get());
+    int req_num = current_pair->graph_state->transition.argument;
 
     if (dot_output != nullptr) {
       if (initial_global_state->prev_pair != 0 && initial_global_state->prev_pair != current_pair->num) {
@@ -381,7 +389,7 @@ int LivenessChecker::main(void)
         initial_global_state->prev_req.clear();
       }
       initial_global_state->prev_pair = current_pair->num;
-      initial_global_state->prev_req = simgrid::mc::request_get_dot_output(req, value);
+      initial_global_state->prev_req = simgrid::mc::request_get_dot_output(req, req_num);
       if (current_pair->search_cycle)
         fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
       fflush(dot_output);
@@ -389,15 +397,15 @@ int LivenessChecker::main(void)
 
     XBT_DEBUG("Execute: %s",
       simgrid::mc::request_to_string(
-        req, value, simgrid::mc::RequestType::simix).c_str());
+        req, req_num, simgrid::mc::RequestType::simix).c_str());
 
     /* Update mc_stats */
     mc_stats->executed_transitions++;
     if (!current_pair->exploration_started)
-      mc_stats->visited_pairs++;
+      visitedPairsCount_++;
 
     /* Answer the request */
-    simgrid::mc::handle_simcall(req, value);
+    mc_model_checker->handle_simcall(current_pair->graph_state->transition);
 
     /* Wait for requests (schedules processes) */
     mc_model_checker->wait_for_requests();
@@ -422,13 +430,13 @@ int LivenessChecker::main(void)
   }
 
   XBT_INFO("No property violation found.");
-  MC_print_statistics(mc_stats);
+  simgrid::mc::session->logState();
   return SIMGRID_MC_EXIT_SUCCESS;
 }
 
 std::shared_ptr<Pair> LivenessChecker::newPair(Pair* current_pair, xbt_automaton_state_t state, std::shared_ptr<const std::vector<int>> propositions)
 {
-  std::shared_ptr<Pair> next_pair = std::make_shared<Pair>();
+  std::shared_ptr<Pair> next_pair = std::make_shared<Pair>(++expandedPairsCount_);
   next_pair->automaton_state = state;
   next_pair->graph_state = std::shared_ptr<simgrid::mc::State>(MC_state_new());
   next_pair->atomic_propositions = std::move(propositions);