[mc] Rename RecordTraceElement as Transition and use it to represent a transition

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

diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp
index ea3ab38..d2438e4 100644 (file)
--- a/src/mc/CommunicationDeterminismChecker.cpp
+++ b/src/mc/CommunicationDeterminismChecker.cpp
@@ -22,6 +22,7 @@
 #include "src/mc/CommunicationDeterminismChecker.hpp"
 #include "src/mc/mc_exit.h"
 #include "src/mc/VisitedState.hpp"
+#include "src/mc/Transition.hpp"
 
 using simgrid::mc::remote;
 
@@ -96,8 +97,10 @@ static void update_comm_pattern(simgrid::mc::PatternCommunication* comm_pattern,
   s_smx_synchro_t comm;
   mc_model_checker->process().read(&comm, remote(comm_addr));
 
-  smx_process_t src_proc = MC_smx_resolve_process(comm.comm.src_proc);
-  smx_process_t dst_proc = MC_smx_resolve_process(comm.comm.dst_proc);
+  smx_process_t src_proc = mc_model_checker->process().resolveProcess(
+    simgrid::mc::remote(comm.comm.src_proc));
+  smx_process_t dst_proc = mc_model_checker->process().resolveProcess(
+    simgrid::mc::remote(comm.comm.dst_proc));
   comm_pattern->src_proc = src_proc->pid;
   comm_pattern->dst_proc = dst_proc->pid;
   comm_pattern->src_host = MC_smx_process_get_host_name(src_proc);
@@ -189,7 +192,8 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type
     char* remote_name = mc_model_checker->process().read<char*>(
       (std::uint64_t)(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name));
     pattern->rdv = mc_model_checker->process().read_string(remote_name);
-    pattern->src_proc = MC_smx_resolve_process(synchro.comm.src_proc)->pid;
+    pattern->src_proc = mc_model_checker->process().resolveProcess(
+      simgrid::mc::remote(synchro.comm.src_proc))->pid;
     pattern->src_host = MC_smx_process_get_host_name(issuer);
 
     struct s_smpi_mpi_request mpi_request =
@@ -235,7 +239,8 @@ void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type
     mc_model_checker->process().read(&remote_name,
       remote(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name));
     pattern->rdv = mc_model_checker->process().read_string(remote_name);
-    pattern->dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc)->pid;
+    pattern->dst_proc = mc_model_checker->process().resolveProcess(
+      simgrid::mc::remote(synchro.comm.dst_proc))->pid;
     pattern->dst_host = MC_smx_process_get_host_name(issuer);
   } else
     xbt_die("Unexpected call_type %i", (int) call_type);
@@ -301,30 +306,22 @@ CommunicationDeterminismChecker::~CommunicationDeterminismChecker()
 
 }
 
-// TODO, deduplicate with SafetyChecker
 RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
 {
   RecordTrace res;
-  for (auto const& state : stack_) {
-    int value = 0;
-    smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
-    const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
-    const int pid = issuer->pid;
-    res.push_back(RecordTraceElement(pid, value));
-  }
+  for (auto const& state : stack_)
+    res.push_back(state->getRecordElement());
   return res;
 }
 
-// TODO, deduplicate with SafetyChecker
 std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // override
 {
   std::vector<std::string> trace;
   for (auto const& state : stack_) {
-    int value;
-    smx_simcall_t req = MC_state_get_executed_request(state.get(), &value);
+    smx_simcall_t req = &state->executed_req;
     if (req)
       trace.push_back(simgrid::mc::request_to_string(
-        req, value, simgrid::mc::RequestType::executed));
+        req, state->transition.argument, simgrid::mc::RequestType::executed));
   }
   return trace;
 }
@@ -360,7 +357,7 @@ void CommunicationDeterminismChecker::prepare()
   /* Get an enabled process and insert it in the interleave set of the initial state */
   for (auto& p : mc_model_checker->process().simix_processes())
     if (simgrid::mc::process_is_enabled(&p.copy))
-      MC_state_interleave_process(initial_state.get(), &p.copy);
+      initial_state->interleave(&p.copy);
 
   stack_.push_back(std::move(initial_state));
 }
@@ -381,7 +378,6 @@ bool all_communications_are_finished()
 
 int CommunicationDeterminismChecker::main(void)
 {
-  int value;
   std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
   smx_simcall_t req = nullptr;
 
@@ -399,16 +395,18 @@ int CommunicationDeterminismChecker::main(void)
     mc_stats->visited_states++;
 
     if (stack_.size() <= (std::size_t) _sg_mc_max_depth
-        && (req = MC_state_get_request(state, &value))
+        && (req = MC_state_get_request(state)) != nullptr
         && (visited_state == nullptr)) {
 
+      int req_num = state->transition.argument;
+
       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());
 
       std::string req_str;
       if (dot_output != nullptr)
-        req_str = simgrid::mc::request_get_dot_output(req, value);
+        req_str = simgrid::mc::request_get_dot_output(req, req_num);
 
       mc_stats->executed_transitions++;
 
@@ -418,12 +416,13 @@ int CommunicationDeterminismChecker::main(void)
         call = MC_get_call_type(req);
 
       /* Answer the request */
-      simgrid::mc::handle_simcall(req, value);    /* After this call req is no longer useful */
+      mc_model_checker->handle_simcall(state->transition);
+      /* After this call req is no longer useful */
 
       if(!initial_global_state->initial_communications_pattern_done)
-        MC_handle_comm_pattern(call, req, value, initial_communications_pattern, 0);
+        MC_handle_comm_pattern(call, req, req_num, initial_communications_pattern, 0);
       else
-        MC_handle_comm_pattern(call, req, value, nullptr, 0);
+        MC_handle_comm_pattern(call, req, req_num, nullptr, 0);
 
       /* Wait for requests (schedules processes) */
       mc_model_checker->wait_for_requests();
@@ -445,7 +444,7 @@ int CommunicationDeterminismChecker::main(void)
         /* Get enabled processes and insert them in the interleave set of the next state */
         for (auto& p : mc_model_checker->process().simix_processes())
           if (simgrid::mc::process_is_enabled(&p.copy))
-            MC_state_interleave_process(next_state.get(), &p.copy);
+            next_state->interleave(&p.copy);
 
         if (dot_output != nullptr)
           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",