X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/37628abb1a6de84ea9ddee484632b6a9d6245c96..0a82e90d4cfdd7e27e1b946d22aff74a5abdda99:/src/mc/CommunicationDeterminismChecker.cpp?ds=sidebyside

diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp
index 57a8ee8d34..c6f1270ba2 100644
--- 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", expandedStatesCount_);
+  XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
+  XBT_INFO("Executed transitions = %lu", mc_model_checker->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()
 {
 
@@ -347,7 +376,7 @@ void CommunicationDeterminismChecker::prepare()
   }
 
   std::unique_ptr<simgrid::mc::State> initial_state =
-    std::unique_ptr<simgrid::mc::State>(MC_state_new());
+    std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
 
   XBT_DEBUG("********* Start communication determinism verification *********");
 
@@ -389,7 +418,7 @@ int CommunicationDeterminismChecker::main(void)
               state->interleaveSize());
 
     /* Update statistics */
-    mc_stats->visited_states++;
+    mc_model_checker->visited_states++;
 
     if (stack_.size() <= (std::size_t) _sg_mc_max_depth
         && (req = MC_state_get_request(state)) != nullptr
@@ -405,7 +434,7 @@ int CommunicationDeterminismChecker::main(void)
       if (dot_output != nullptr)
         req_str = simgrid::mc::request_get_dot_output(req, req_num);
 
-      mc_stats->executed_transitions++;
+      mc_model_checker->executed_transitions++;
 
       /* TODO : handle test and testany simcalls */
       e_mc_call_type_t call = MC_CALL_TYPE_NONE;
@@ -426,7 +455,7 @@ int CommunicationDeterminismChecker::main(void)
 
       /* Create the new expanded state */
       std::unique_ptr<simgrid::mc::State> next_state =
-        std::unique_ptr<simgrid::mc::State>(MC_state_new());
+        std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
 
       /* If comm determinism verification, we cannot stop the exploration if
          some communications are not finished (at least, data are transfered).
@@ -436,7 +465,8 @@ int CommunicationDeterminismChecker::main(void)
         && initial_global_state->initial_communications_pattern_done;
 
       if (_sg_mc_visited == 0
-          || (visited_state = visitedStates_.addVisitedState(next_state.get(), compare_snapshots)) == nullptr) {
+          || (visited_state = visitedStates_.addVisitedState(
+            expandedStatesCount_, next_state.get(), compare_snapshots)) == nullptr) {
 
         /* Get enabled processes and insert them in the interleave set of the next state */
         for (auto& p : mc_model_checker->process().simix_processes())
@@ -510,12 +540,11 @@ int CommunicationDeterminismChecker::main(void)
 int CommunicationDeterminismChecker::run()
 {
   XBT_INFO("Check communication determinism");
-  mc_model_checker->wait_for_requests();
+  simgrid::mc::session->initialize();
 
   this->prepare();
 
   initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
-  initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
   initial_global_state->initial_communications_pattern_done = 0;
   initial_global_state->recv_deterministic = 1;
   initial_global_state->send_deterministic = 1;