[mc] Move MC_print_statistics() as Session::logState()

diff --git a/examples/smpi/mc/only_send_deterministic.tesh b/examples/smpi/mc/only_send_deterministic.tesh
index c7993f4..97b804e 100644 (file)
--- a/examples/smpi/mc/only_send_deterministic.tesh
+++ b/examples/smpi/mc/only_send_deterministic.tesh
@@ -3,12 +3,12 @@
 ! timeout 60
 $ ../../../smpi_script/bin/smpirun -wrapper "${bindir:=.}/../../../bin/simgrid-mc" --log=xbt_cfg.thresh:warning -hostfile ${srcdir:=.}/hostfile_only_send_deterministic  -platform ${srcdir:=.}/../../platforms/cluster.xml --cfg=model-check/communications_determinism:1 --cfg=smpi/send_is_detached_thresh:0 --cfg=smpi/running_power:1e9 ./smpi_only_send_deterministic
 > [0.000000] [mc_comm_determinism/INFO] Check communication determinism
-> [0.000000] [mc_global/INFO] ******************************************************
-> [0.000000] [mc_global/INFO] **** Only-send-deterministic communication pattern ****
-> [0.000000] [mc_global/INFO] ******************************************************
-> [0.000000] [mc_global/INFO] The recv communications pattern of the process 0 is different! Different source for communication #2
-> [0.000000] [mc_global/INFO] Expanded states = 520
-> [0.000000] [mc_global/INFO] Visited states = 1476
-> [0.000000] [mc_global/INFO] Executed transitions = 1312
-> [0.000000] [mc_global/INFO] Send-deterministic : Yes
-> [0.000000] [mc_global/INFO] Recv-deterministic : No
+> [0.000000] [mc_Session/INFO] ******************************************************
+> [0.000000] [mc_Session/INFO] **** Only-send-deterministic communication pattern ****
+> [0.000000] [mc_Session/INFO] ******************************************************
+> [0.000000] [mc_Session/INFO] The recv communications pattern of the process 0 is different! Different source for communication #2
+> [0.000000] [mc_Session/INFO] Expanded states = 520
+> [0.000000] [mc_Session/INFO] Visited states = 1476
+> [0.000000] [mc_Session/INFO] Executed transitions = 1312
+> [0.000000] [mc_Session/INFO] Send-deterministic : Yes
+> [0.000000] [mc_Session/INFO] Recv-deterministic : No

diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp
index 2b20a33..57a8ee8 100644 (file)
--- a/src/mc/CommunicationDeterminismChecker.cpp
+++ b/src/mc/CommunicationDeterminismChecker.cpp
@@ -144,7 +144,7 @@ static void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunic
         XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
         xbt_free(simgrid::mc::initial_global_state->send_diff);
         simgrid::mc::initial_global_state->send_diff = nullptr;
-        MC_print_statistics(mc_stats);
+        simgrid::mc::session->logState();
         mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
       }else if(_sg_mc_comms_determinism
           && (!simgrid::mc::initial_global_state->send_deterministic
@@ -158,7 +158,7 @@ static void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunic
         simgrid::mc::initial_global_state->send_diff = nullptr;
         xbt_free(simgrid::mc::initial_global_state->recv_diff);
         simgrid::mc::initial_global_state->recv_diff = nullptr;
-        MC_print_statistics(mc_stats);
+        simgrid::mc::session->logState();
         mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
       }
     }
@@ -503,7 +503,7 @@ int CommunicationDeterminismChecker::main(void)
     }
   }
 
-  MC_print_statistics(mc_stats);
+  simgrid::mc::session->logState();
   return SIMGRID_MC_EXIT_SUCCESS;
 }
 

diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp
index 537dd9b..39f6bdb 100644 (file)
--- a/src/mc/LivenessChecker.cpp
+++ b/src/mc/LivenessChecker.cpp
@@ -310,7 +310,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);
 }
 
@@ -422,7 +422,7 @@ int LivenessChecker::main(void)
   }
 
   XBT_INFO("No property violation found.");
-  MC_print_statistics(mc_stats);
+  simgrid::mc::session->logState();
   return SIMGRID_MC_EXIT_SUCCESS;
 }
 

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index d565169..28cfb9b 100644 (file)
--- a/src/mc/SafetyChecker.cpp
+++ b/src/mc/SafetyChecker.cpp
@@ -43,7 +43,7 @@ static void MC_show_non_termination(void)
   XBT_INFO("Counter-example execution trace:");
   for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
     XBT_INFO("%s", s.c_str());
-  MC_print_statistics(mc_stats);
+  simgrid::mc::session->logState();
 }
 
 static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
@@ -165,7 +165,7 @@ int SafetyChecker::run()
   }
 
   XBT_INFO("No property violation found.");
-  MC_print_statistics(mc_stats);
+  simgrid::mc::session->logState();
   initial_global_state = nullptr;
   return SIMGRID_MC_EXIT_SUCCESS;
 }

diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp
index 842fa3c..e600b30 100644 (file)
--- a/src/mc/Session.cpp
+++ b/src/mc/Session.cpp
@@ -9,11 +9,15 @@
 
 #include <functional>
 
+#include <xbt/log.h>
 #include <xbt/system_error.hpp>
 #include <simgrid/sg_config.h>
 #include <simgrid/modelchecker.h>
+#include <mc/mc.h>
 
 #include "src/mc/Session.hpp"
+#include "src/mc/mc_state.h"
+#include "src/mc/mc_private.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_Session, mc, "Model-checker session");
 
@@ -100,6 +104,50 @@ void Session::execute(Transition const& transition)
   modelChecker_->wait_for_requests();
 }
 
+void Session::logState()
+{
+  if(_sg_mc_comms_determinism) {
+    if (!simgrid::mc::initial_global_state->recv_deterministic &&
+        simgrid::mc::initial_global_state->send_deterministic){
+      XBT_INFO("******************************************************");
+      XBT_INFO("**** Only-send-deterministic communication pattern ****");
+      XBT_INFO("******************************************************");
+      XBT_INFO("%s", simgrid::mc::initial_global_state->recv_diff);
+    }else if(!simgrid::mc::initial_global_state->send_deterministic &&
+        simgrid::mc::initial_global_state->recv_deterministic) {
+      XBT_INFO("******************************************************");
+      XBT_INFO("**** Only-recv-deterministic communication pattern ****");
+      XBT_INFO("******************************************************");
+      XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
+    }
+  }
+
+  if (mc_stats->expanded_pairs == 0) {
+    XBT_INFO("Expanded states = %lu", mc_stats->expanded_states);
+    XBT_INFO("Visited states = %lu", mc_stats->visited_states);
+  } else {
+    XBT_INFO("Expanded pairs = %lu", mc_stats->expanded_pairs);
+    XBT_INFO("Visited pairs = %lu", mc_stats->visited_pairs);
+  }
+  XBT_INFO("Executed transitions = %lu", mc_stats->executed_transitions);
+  if ((_sg_mc_dot_output_file != nullptr) && (_sg_mc_dot_output_file[0] != '\0')) {
+    fprintf(dot_output, "}\n");
+    fclose(dot_output);
+  }
+  if (simgrid::mc::initial_global_state != nullptr
+      && (_sg_mc_comms_determinism || _sg_mc_send_determinism)) {
+    XBT_INFO("Send-deterministic : %s",
+      !simgrid::mc::initial_global_state->send_deterministic ? "No" : "Yes");
+    if (_sg_mc_comms_determinism)
+      XBT_INFO("Recv-deterministic : %s",
+        !simgrid::mc::initial_global_state->recv_deterministic ? "No" : "Yes");
+  }
+  if (getenv("SIMGRID_MC_SYSTEM_STATISTICS")){
+    int ret=system("free");
+    if(ret!=0)XBT_WARN("system call did not return 0, but %d",ret);
+  }
+}
+
 // static
 Session* Session::fork(std::function<void(void)> code)
 {

diff --git a/src/mc/Session.hpp b/src/mc/Session.hpp
index 23e3eaa..dd2e031 100644 (file)
--- a/src/mc/Session.hpp
+++ b/src/mc/Session.hpp
@@ -51,6 +51,7 @@ public:
 
 public:
   void execute(Transition const& transition);
+  void logState();
 
 public: // static constructors
 

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index 5ad3660..630adb9 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -208,51 +208,7 @@ void MC_show_deadlock(void)
   XBT_INFO("Counter-example execution trace:");
   for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
     XBT_INFO("%s", s.c_str());
-  MC_print_statistics(mc_stats);
-}
-
-void MC_print_statistics(mc_stats_t stats)
-{
-  if(_sg_mc_comms_determinism) {
-    if (!simgrid::mc::initial_global_state->recv_deterministic &&
-        simgrid::mc::initial_global_state->send_deterministic){
-      XBT_INFO("******************************************************");
-      XBT_INFO("**** Only-send-deterministic communication pattern ****");
-      XBT_INFO("******************************************************");
-      XBT_INFO("%s", simgrid::mc::initial_global_state->recv_diff);
-    }else if(!simgrid::mc::initial_global_state->send_deterministic &&
-        simgrid::mc::initial_global_state->recv_deterministic) {
-      XBT_INFO("******************************************************");
-      XBT_INFO("**** Only-recv-deterministic communication pattern ****");
-      XBT_INFO("******************************************************");
-      XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
-    }
-  }
-
-  if (stats->expanded_pairs == 0) {
-    XBT_INFO("Expanded states = %lu", stats->expanded_states);
-    XBT_INFO("Visited states = %lu", stats->visited_states);
-  } else {
-    XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
-    XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
-  }
-  XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
-  if ((_sg_mc_dot_output_file != nullptr) && (_sg_mc_dot_output_file[0] != '\0')) {
-    fprintf(dot_output, "}\n");
-    fclose(dot_output);
-  }
-  if (simgrid::mc::initial_global_state != nullptr
-      && (_sg_mc_comms_determinism || _sg_mc_send_determinism)) {
-    XBT_INFO("Send-deterministic : %s",
-      !simgrid::mc::initial_global_state->send_deterministic ? "No" : "Yes");
-    if (_sg_mc_comms_determinism)
-      XBT_INFO("Recv-deterministic : %s",
-        !simgrid::mc::initial_global_state->recv_deterministic ? "No" : "Yes");
-  }
-  if (getenv("SIMGRID_MC_SYSTEM_STATISTICS")){
-    int ret=system("free");
-    if(ret!=0)XBT_WARN("system call did not return 0, but %d",ret);
-  }
+  simgrid::mc::session->logState();
 }
 
 void MC_automaton_load(const char *file)
@@ -341,7 +297,7 @@ void MC_report_assertion_error(void)
   simgrid::mc::dumpRecordPath();
   for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
     XBT_INFO("%s", s.c_str());
-  MC_print_statistics(mc_stats);
+  simgrid::mc::session->logState();
 }
 
 void MC_report_crash(int status)
@@ -361,7 +317,7 @@ void MC_report_crash(int status)
   simgrid::mc::dumpRecordPath();
   for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
     XBT_INFO("%s", s.c_str());
-  MC_print_statistics(mc_stats);
+  simgrid::mc::session->logState();
   XBT_INFO("Stack trace:");
   mc_model_checker->process().dumpStack();
 }

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index ceaf9c1..143aac7 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -77,8 +77,6 @@ typedef struct mc_stats {
 
 XBT_PRIVATE extern mc_stats_t mc_stats;
 
-XBT_PRIVATE void MC_print_statistics(mc_stats_t stats);
-
 /********************************** Snapshot comparison **********************************/
 
 //#define MC_DEBUG 1