#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;
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);
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 =
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);
}
-// TODO, deduplicate with SafetyChecker
RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
{
RecordTrace res;
return res;
}
-// TODO, deduplicate with SafetyChecker
std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // override
{
std::vector<std::string> trace;
smx_simcall_t req = &state->executed_req;
if (req)
trace.push_back(simgrid::mc::request_to_string(
- req, state->req_num, simgrid::mc::RequestType::executed));
+ req, state->transition.argument, simgrid::mc::RequestType::executed));
}
return trace;
}
&& (req = MC_state_get_request(state)) != nullptr
&& (visited_state == nullptr)) {
- int req_num = state->req_num;
+ int req_num = state->transition.argument;
XBT_DEBUG("Execute: %s",
simgrid::mc::request_to_string(
call = MC_get_call_type(req);
/* Answer the request */
- simgrid::mc::handle_simcall(req, req_num); /* 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, req_num, initial_communications_pattern, 0);