simgrid::mc::Remote<simgrid::simix::Comm> temp_comm;
mc_model_checker->process().read(temp_comm, comm_addr);
simgrid::simix::Comm* comm =
simgrid::mc::Remote<simgrid::simix::Comm> temp_comm;
mc_model_checker->process().read(temp_comm, comm_addr);
simgrid::simix::Comm* comm =
smx_process_t src_proc = mc_model_checker->process().resolveProcess(
simgrid::mc::remote(comm->src_proc));
smx_process_t src_proc = mc_model_checker->process().resolveProcess(
simgrid::mc::remote(comm->src_proc));
mc_model_checker->process().read(temp_synchro, remote(
static_cast<simgrid::simix::Comm*>(pattern->comm_addr)));
simgrid::simix::Comm* synchro =
mc_model_checker->process().read(temp_synchro, remote(
static_cast<simgrid::simix::Comm*>(pattern->comm_addr)));
simgrid::simix::Comm* synchro =
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));
simgrid::mc::Remote<simgrid::simix::Comm> temp_comm;
mc_model_checker->process().read(temp_comm, remote(
static_cast<simgrid::simix::Comm*>(pattern->comm_addr)));
simgrid::mc::Remote<simgrid::simix::Comm> temp_comm;
mc_model_checker->process().read(temp_comm, remote(
static_cast<simgrid::simix::Comm*>(pattern->comm_addr)));
/* Get an enabled process and insert it in the interleave set of the initial state */
for (auto& p : mc_model_checker->process().simix_processes())
/* Get an enabled process and insert it in the interleave set of the initial state */
for (auto& p : mc_model_checker->process().simix_processes())
std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
/* If comm determinism verification, we cannot stop the exploration if
std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
/* If comm determinism verification, we cannot stop the exploration if
These communications are incomplete and they cannot be analyzed and
compared with the initial pattern. */
bool compare_snapshots = all_communications_are_finished()
These communications are incomplete and they cannot be analyzed and
compared with the initial pattern. */
bool compare_snapshots = all_communications_are_finished()
/* Get enabled processes and insert them in the interleave set of the next state */
for (auto& p : mc_model_checker->process().simix_processes())
/* Get enabled processes and insert them in the interleave set of the next state */
for (auto& p : mc_model_checker->process().simix_processes())
if (dot_output != nullptr)
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
if (dot_output != nullptr)
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",