Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
CommunicationDeterminismChecker::log_state() uses APIs of mc_api
[simgrid.git] / src / mc / checker / CommunicationDeterminismChecker.cpp
index f652d1f2a9a08bb8827f643472c660e1a2e9d0ef..baae6c8e65bffbf0a150bf49345ca5f028d33d99 100644 (file)
@@ -321,8 +321,8 @@ void CommunicationDeterminismChecker::log_state() // override
     }
   }
   XBT_INFO("Expanded states = %lu", expanded_states_count_);
-  XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
-  XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
+  XBT_INFO("Visited states = %lu", mcapi::get().mc_get_visited_states());
+  XBT_INFO("Executed transitions = %lu", mcapi::get().mc_get_executed_trans());
   XBT_INFO("Send-deterministic : %s", this->send_deterministic ? "Yes" : "No");
   if (_sg_mc_comms_determinism)
     XBT_INFO("Recv-deterministic : %s", this->recv_deterministic ? "Yes" : "No");
@@ -351,7 +351,8 @@ void CommunicationDeterminismChecker::prepare()
 
 static inline bool all_communications_are_finished()
 {
-  for (size_t current_actor = 1; current_actor < mcapi::get().get_maxpid(); current_actor++) {
+  auto maxpid = mcapi::get().get_maxpid();
+  for (size_t current_actor = 1; current_actor < maxpid; current_actor++) {
     if (not incomplete_communications_pattern[current_actor].empty()) {
       XBT_DEBUG("Some communications are not finished, cannot stop the exploration! State not visited.");
       return false;
@@ -371,9 +372,9 @@ void CommunicationDeterminismChecker::restoreState()
   }
 
   /* Restore the initial state */
-  mc::session->restore_initial_state();
+  mcapi::get().s_restore_initial_state();
 
-  unsigned n = MC_smx_get_maxpid();
+  unsigned n = mcapi::get().get_maxpid();
   assert(n == incomplete_communications_pattern.size());
   assert(n == initial_communications_pattern.size());
   for (unsigned j=0; j < n ; j++) {
@@ -393,18 +394,18 @@ void CommunicationDeterminismChecker::restoreState()
     /* because we got a copy of the executed request, we have to fetch the
        real one, pointed by the request field of the issuer process */
 
-    const smx_actor_t issuer = MC_smx_simcall_get_issuer(saved_req);
+    const smx_actor_t issuer = mcapi::get().mc_smx_simcall_get_issuer(saved_req);
     smx_simcall_t req        = &issuer->simcall_;
 
     /* TODO : handle test and testany simcalls */
     e_mc_call_type_t call = MC_get_call_type(req);
-    mc_model_checker->handle_simcall(state->transition_);
+    mcapi::get().handle_simcall(state->transition_);
     MC_handle_comm_pattern(call, req, req_num, 1);
-    mc_model_checker->wait_for_requests();
+    mcapi::get().mc_wait_for_requests();
 
     /* Update statistics */
-    mc_model_checker->visited_states++;
-    mc_model_checker->executed_transitions++;
+    mcapi::get().mc_inc_visited_states();
+    mcapi::get().mc_inc_executed_trans();
   }
 }