[mc] Delegate some part of Session::logState() to Checker::logState()

This separates the Checker-specific code from the generic/shared code.
The session should not need to know about every existing Checker.

diff --git a/examples/smpi/mc/only_send_deterministic.tesh b/examples/smpi/mc/only_send_deterministic.tesh
index 97b804e..10cdd9a 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_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
+> [0.000000] [mc_comm_determinism/INFO] ******************************************************
+> [0.000000] [mc_comm_determinism/INFO] **** Only-send-deterministic communication pattern ****
+> [0.000000] [mc_comm_determinism/INFO] ******************************************************
+> [0.000000] [mc_comm_determinism/INFO] The recv communications pattern of the process 0 is different! Different source for communication #2
+> [0.000000] [mc_comm_determinism/INFO] Expanded states = 520
+> [0.000000] [mc_comm_determinism/INFO] Visited states = 1476
+> [0.000000] [mc_comm_determinism/INFO] Executed transitions = 1312
+> [0.000000] [mc_comm_determinism/INFO] Send-deterministic : Yes
+> [0.000000] [mc_comm_determinism/INFO] Recv-deterministic : No

diff --git a/src/mc/Checker.cpp b/src/mc/Checker.cpp
index 1fefd9d..6ae0aae 100644 (file)
--- a/src/mc/Checker.cpp
+++ b/src/mc/Checker.cpp
@@ -37,5 +37,10 @@ std::vector<std::string> Checker::getTextualTrace()
   return {};
 }
 
+// virtual
+void Checker::logState()
+{
+}
+
 }
 }

diff --git a/src/mc/Checker.hpp b/src/mc/Checker.hpp
index 8f7e0cc..58fa3d6 100644 (file)
--- a/src/mc/Checker.hpp
+++ b/src/mc/Checker.hpp
@@ -48,6 +48,7 @@ public:
    */
   virtual RecordTrace getRecordTrace();
   virtual std::vector<std::string> getTextualTrace();
+  virtual void logState();
 
 protected:
   Session& getSession() { return *session_; }

diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp
index 57a8ee8..e5b383d 100644 (file)
--- a/src/mc/CommunicationDeterminismChecker.cpp
+++ b/src/mc/CommunicationDeterminismChecker.cpp
@@ -326,6 +326,35 @@ std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // o
   return trace;
 }
 
+void CommunicationDeterminismChecker::logState() // override
+{
+  Checker::logState();
+  if (_sg_mc_comms_determinism &&
+      !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(_sg_mc_comms_determinism &&
+      !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);
+  }
+  XBT_INFO("Expanded states = %lu", mc_stats->expanded_states);
+  XBT_INFO("Visited states = %lu", mc_stats->visited_states);
+  XBT_INFO("Executed transitions = %lu", mc_stats->executed_transitions);
+  if (simgrid::mc::initial_global_state != nullptr)
+    XBT_INFO("Send-deterministic : %s",
+      !simgrid::mc::initial_global_state->send_deterministic ? "No" : "Yes");
+  if (simgrid::mc::initial_global_state != nullptr && _sg_mc_comms_determinism)
+    XBT_INFO("Recv-deterministic : %s",
+      !simgrid::mc::initial_global_state->recv_deterministic ? "No" : "Yes");
+}
+
 void CommunicationDeterminismChecker::prepare()
 {
 

diff --git a/src/mc/CommunicationDeterminismChecker.hpp b/src/mc/CommunicationDeterminismChecker.hpp
index bd30d04..291d98e 100644 (file)
--- a/src/mc/CommunicationDeterminismChecker.hpp
+++ b/src/mc/CommunicationDeterminismChecker.hpp
@@ -29,6 +29,7 @@ public:
 private:
   void prepare();
   int main();
+  void logState() override;
 private:
   /** Stack representing the position in the exploration graph */
   std::list<std::unique_ptr<simgrid::mc::State>> stack_;

diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp
index 39f6bdb..15a0a73 100644 (file)
--- a/src/mc/LivenessChecker.cpp
+++ b/src/mc/LivenessChecker.cpp
@@ -301,6 +301,14 @@ RecordTrace LivenessChecker::getRecordTrace() // override
   return res;
 }
 
+void LivenessChecker::logState() // override
+{
+  Checker::logState();
+  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);
+}
+
 void LivenessChecker::showAcceptanceCycle(std::size_t depth)
 {
   XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");

diff --git a/src/mc/LivenessChecker.hpp b/src/mc/LivenessChecker.hpp
index 7ce79ce..2c482ad 100644 (file)
--- a/src/mc/LivenessChecker.hpp
+++ b/src/mc/LivenessChecker.hpp
@@ -68,6 +68,7 @@ public:
   int run() override;
   RecordTrace getRecordTrace() override;
   std::vector<std::string> getTextualTrace() override;
+  void logState() override;
 private:
   int main();
   void prepare();

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index 28cfb9b..b51d39a 100644 (file)
--- a/src/mc/SafetyChecker.cpp
+++ b/src/mc/SafetyChecker.cpp
@@ -87,6 +87,14 @@ std::vector<std::string> SafetyChecker::getTextualTrace() // override
   return trace;
 }
 
+void SafetyChecker::logState() // override
+{
+  Checker::logState();
+  XBT_INFO("Expanded states = %lu", mc_stats->expanded_states);
+  XBT_INFO("Visited states = %lu", mc_stats->visited_states);
+  XBT_INFO("Executed transitions = %lu", mc_stats->executed_transitions);
+}
+
 int SafetyChecker::run()
 {
   this->init();

diff --git a/src/mc/SafetyChecker.hpp b/src/mc/SafetyChecker.hpp
index 8d237ce..a9662be 100644 (file)
--- a/src/mc/SafetyChecker.hpp
+++ b/src/mc/SafetyChecker.hpp
@@ -27,6 +27,7 @@ public:
   int run() override;
   RecordTrace getRecordTrace() override;
   std::vector<std::string> getTextualTrace() override;
+  void logState() override;
 private:
   // Temp
   void init();

diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp
index e600b30..1bb2878 100644 (file)
--- a/src/mc/Session.cpp
+++ b/src/mc/Session.cpp
@@ -18,6 +18,7 @@
 #include "src/mc/Session.hpp"
 #include "src/mc/mc_state.h"
 #include "src/mc/mc_private.h"
+#include "src/mc/Checker.hpp"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_Session, mc, "Model-checker session");
 
@@ -106,42 +107,12 @@ void Session::execute(Transition const& transition)
 
 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);
-    }
-  }
+  mc_model_checker->getChecker()->logState();
 
-  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);