#include "src/mc/mc_private.h"
#include "src/mc/mc_record.h"
#include "src/mc/mc_request.h"
#include "src/mc/mc_private.h"
#include "src/mc/mc_record.h"
#include "src/mc/mc_request.h"
#include "src/mc/mc_smx.h"
#include "src/mc/mc_state.h"
#include "src/mc/remote/Client.hpp"
#include "src/mc/mc_smx.h"
#include "src/mc/mc_state.h"
#include "src/mc/remote/Client.hpp"
smx_actor_t src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->src_proc));
smx_actor_t dst_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->dst_proc));
smx_actor_t src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->src_proc));
smx_actor_t dst_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->dst_proc));
if (call_type == MC_CALL_TYPE_SEND) {
/* Create comm pattern */
pattern->type = simgrid::mc::PatternCommunicationType::send;
if (call_type == MC_CALL_TYPE_SEND) {
/* Create comm pattern */
pattern->type = simgrid::mc::PatternCommunicationType::send;
- remote(static_cast<simgrid::kernel::activity::Comm*>(pattern->comm_addr)));
- simgrid::kernel::activity::Comm* synchro = static_cast<simgrid::kernel::activity::Comm*>(temp_synchro.getBuffer());
+ remote(static_cast<simgrid::kernel::activity::CommImpl*>(pattern->comm_addr)));
+ simgrid::kernel::activity::CommImpl* synchro =
+ static_cast<simgrid::kernel::activity::CommImpl*>(temp_synchro.getBuffer());
char* remote_name = mc_model_checker->process().read<char*>(
(std::uint64_t)(synchro->mbox ? &synchro->mbox->name_ : &synchro->mbox_cpy->name_));
char* remote_name = mc_model_checker->process().read<char*>(
(std::uint64_t)(synchro->mbox ? &synchro->mbox->name_ : &synchro->mbox_cpy->name_));
}
} else if (call_type == MC_CALL_TYPE_RECV) {
pattern->type = simgrid::mc::PatternCommunicationType::receive;
}
} else if (call_type == MC_CALL_TYPE_RECV) {
pattern->type = simgrid::mc::PatternCommunicationType::receive;
simgrid::smpi::Request mpi_request;
mc_model_checker->process().read(&mpi_request,
remote((simgrid::smpi::Request*)simcall_comm_irecv__get__data(request)));
pattern->tag = mpi_request.tag();
simgrid::smpi::Request mpi_request;
mc_model_checker->process().read(&mpi_request,
remote((simgrid::smpi::Request*)simcall_comm_irecv__get__data(request)));
pattern->tag = mpi_request.tag();
- remote(static_cast<simgrid::kernel::activity::Comm*>(pattern->comm_addr)));
- simgrid::kernel::activity::Comm* comm = temp_comm.getBuffer();
+ remote(static_cast<simgrid::kernel::activity::CommImpl*>(pattern->comm_addr)));
+ simgrid::kernel::activity::CommImpl* comm = temp_comm.getBuffer();
- xbt_dynar_t list, simgrid::mc::RemotePtr<simgrid::kernel::activity::Comm> comm_addr, unsigned int issuer,
+ xbt_dynar_t list, simgrid::mc::RemotePtr<simgrid::kernel::activity::CommImpl> comm_addr, unsigned int issuer,
/* Get an enabled actor and insert it in the interleave set of the initial state */
for (auto& actor : mc_model_checker->process().actors())
if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer()))
/* Get an enabled actor and insert it in the interleave set of the initial state */
for (auto& actor : mc_model_checker->process().actors())
if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer()))
/* Get enabled actors and insert them in the interleave set of the next state */
for (auto& actor : mc_model_checker->process().actors())
if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer()))
/* Get enabled actors and insert them in the interleave set of the next state */
for (auto& actor : mc_model_checker->process().actors())
if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer()))
if (dot_output != nullptr)
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
if (dot_output != nullptr)
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",