X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/67ccc3846b39d92013765366e197a59a76068422..c9e3badfcca0d44e112171cefd237ed3f0ae01ca:/src/mc/checker/CommunicationDeterminismChecker.cpp diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp index ec9ff9e955..4fedf30dda 100644 --- a/src/mc/checker/CommunicationDeterminismChecker.cpp +++ b/src/mc/checker/CommunicationDeterminismChecker.cpp @@ -10,23 +10,22 @@ #include #include -#include "src/mc/mc_state.h" -#include "src/mc/mc_comm_pattern.h" -#include "src/mc/mc_request.h" -#include "src/mc/mc_safety.h" -#include "src/mc/mc_private.h" -#include "src/mc/mc_record.h" -#include "src/mc/mc_smx.h" -#include "src/mc/Client.hpp" -#include "src/mc/checker/CommunicationDeterminismChecker.hpp" -#include "src/mc/mc_exit.h" -#include "src/mc/VisitedState.hpp" #include "src/mc/Transition.hpp" +#include "src/mc/VisitedState.hpp" +#include "src/mc/checker/CommunicationDeterminismChecker.hpp" +#include "src/mc/mc_exit.hpp" +#include "src/mc/mc_private.hpp" +#include "src/mc/mc_record.hpp" +#include "src/mc/mc_request.hpp" +#include "src/mc/mc_smx.hpp" +#include "src/mc/mc_state.hpp" +#include "src/mc/remote/Client.hpp" + +#include "smpi_request.hpp" using simgrid::mc::remote; -XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc, - "Logging specific to MC communication determinism detection"); +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc, "Logging specific to MC communication determinism detection"); /********** Global variables **********/ @@ -35,7 +34,8 @@ xbt_dynar_t incomplete_communications_pattern; /********** Static functions ***********/ -static e_mc_comm_pattern_difference_t compare_comm_pattern(simgrid::mc::PatternCommunication* comm1, simgrid::mc::PatternCommunication* comm2) +static e_mc_comm_pattern_difference_t compare_comm_pattern(simgrid::mc::PatternCommunication* comm1, + simgrid::mc::PatternCommunication* comm2) { if(comm1->type != comm2->type) return TYPE_DIFF; @@ -54,8 +54,11 @@ static e_mc_comm_pattern_difference_t compare_comm_pattern(simgrid::mc::PatternC return NONE_DIFF; } -static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, simgrid::mc::PatternCommunication* comm, unsigned int cursor) { - char *type, *res; +static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, + simgrid::mc::PatternCommunication* comm, unsigned int cursor) +{ + char* type; + char* res; if (comm->type == simgrid::mc::PatternCommunicationType::send) type = bprintf("The send communications pattern of the process %d is different!", process - 1); @@ -64,25 +67,25 @@ static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int p switch(diff) { case TYPE_DIFF: - res = bprintf("%s Different type for communication #%d", type, cursor); + res = bprintf("%s Different type for communication #%u", type, cursor); break; case RDV_DIFF: - res = bprintf("%s Different rdv for communication #%d", type, cursor); + res = bprintf("%s Different rdv for communication #%u", type, cursor); break; case TAG_DIFF: - res = bprintf("%s Different tag for communication #%d", type, cursor); + res = bprintf("%s Different tag for communication #%u", type, cursor); break; case SRC_PROC_DIFF: - res = bprintf("%s Different source for communication #%d", type, cursor); + res = bprintf("%s Different source for communication #%u", type, cursor); break; case DST_PROC_DIFF: - res = bprintf("%s Different destination for communication #%d", type, cursor); + res = bprintf("%s Different destination for communication #%u", type, cursor); break; case DATA_SIZE_DIFF: - res = bprintf("%s\n Different data size for communication #%d", type, cursor); + res = bprintf("%s\n Different data size for communication #%u", type, cursor); break; case DATA_DIFF: - res = bprintf("%s\n Different data for communication #%d", type, cursor); + res = bprintf("%s\n Different data for communication #%u", type, cursor); break; default: res = nullptr; @@ -92,14 +95,13 @@ static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int p return res; } -static void update_comm_pattern( - simgrid::mc::PatternCommunication* comm_pattern, - simgrid::mc::RemotePtr comm_addr) +static void update_comm_pattern(simgrid::mc::PatternCommunication* comm_pattern, + simgrid::mc::RemotePtr comm_addr) { // HACK, type punning - simgrid::mc::Remote temp_comm; + simgrid::mc::Remote temp_comm; mc_model_checker->process().read(temp_comm, comm_addr); - simgrid::kernel::activity::Comm* comm = temp_comm.getBuffer(); + simgrid::kernel::activity::CommImpl* comm = temp_comm.getBuffer(); 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)); @@ -109,27 +111,24 @@ static void update_comm_pattern( comm_pattern->dst_host = MC_smx_actor_get_host_name(dst_proc); if (comm_pattern->data.size() == 0 && comm->src_buff != nullptr) { size_t buff_size; - mc_model_checker->process().read( - &buff_size, remote(comm->dst_buff_size)); + mc_model_checker->process().read(&buff_size, remote(comm->dst_buff_size)); comm_pattern->data.resize(buff_size); - mc_model_checker->process().read_bytes( - comm_pattern->data.data(), comm_pattern->data.size(), - remote(comm->src_buff)); + mc_model_checker->process().read_bytes(comm_pattern->data.data(), comm_pattern->data.size(), + remote(comm->src_buff)); } } namespace simgrid { namespace mc { -void CommunicationDeterminismChecker::deterministic_comm_pattern( - int process, simgrid::mc::PatternCommunication* comm, int backtracking) +void CommunicationDeterminismChecker::deterministic_comm_pattern(int process, simgrid::mc::PatternCommunication* comm, + int backtracking) { simgrid::mc::PatternCommunicationList* list = xbt_dynar_get_as(initial_communications_pattern, process, simgrid::mc::PatternCommunicationList*); - if(!backtracking){ - e_mc_comm_pattern_difference_t diff = - compare_comm_pattern(list->list[list->index_comm].get(), comm); + if (not backtracking) { + e_mc_comm_pattern_difference_t diff = compare_comm_pattern(list->list[list->index_comm].get(), comm); if (diff != NONE_DIFF) { if (comm->type == simgrid::mc::PatternCommunicationType::send) { @@ -143,7 +142,7 @@ void CommunicationDeterminismChecker::deterministic_comm_pattern( xbt_free(this->recv_diff); this->recv_diff = print_determinism_result(diff, process, comm, list->index_comm + 1); } - if(_sg_mc_send_determinism && !this->send_deterministic){ + if (_sg_mc_send_determinism && not this->send_deterministic) { XBT_INFO("*********************************************************"); XBT_INFO("***** Non-send-deterministic communications pattern *****"); XBT_INFO("*********************************************************"); @@ -152,8 +151,7 @@ void CommunicationDeterminismChecker::deterministic_comm_pattern( this->send_diff = nullptr; simgrid::mc::session->logState(); mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM); - }else if(_sg_mc_comms_determinism - && (!this->send_deterministic && !this->recv_deterministic)) { + } else if (_sg_mc_comms_determinism && (not this->send_deterministic && not this->recv_deterministic)) { XBT_INFO("****************************************************"); XBT_INFO("***** Non-deterministic communications pattern *****"); XBT_INFO("****************************************************"); @@ -172,99 +170,90 @@ void CommunicationDeterminismChecker::deterministic_comm_pattern( /********** Non Static functions ***********/ -void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking) +void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, + e_mc_call_type_t call_type, int backtracking) { const smx_actor_t issuer = MC_smx_simcall_get_issuer(request); - simgrid::mc::PatternCommunicationList* initial_pattern = xbt_dynar_get_as( - initial_communications_pattern, issuer->pid, simgrid::mc::PatternCommunicationList*); - xbt_dynar_t incomplete_pattern = xbt_dynar_get_as( - incomplete_communications_pattern, issuer->pid, xbt_dynar_t); + simgrid::mc::PatternCommunicationList* initial_pattern = + xbt_dynar_get_as(initial_communications_pattern, issuer->pid, simgrid::mc::PatternCommunicationList*); + xbt_dynar_t incomplete_pattern = xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t); std::unique_ptr pattern = - std::unique_ptr( - new simgrid::mc::PatternCommunication()); - pattern->index = - initial_pattern->index_comm + xbt_dynar_length(incomplete_pattern); + std::unique_ptr(new simgrid::mc::PatternCommunication()); + pattern->index = initial_pattern->index_comm + xbt_dynar_length(incomplete_pattern); if (call_type == MC_CALL_TYPE_SEND) { /* Create comm pattern */ pattern->type = simgrid::mc::PatternCommunicationType::send; - pattern->comm_addr = simcall_comm_isend__get__result(request); + pattern->comm_addr = static_cast(simcall_comm_isend__getraw__result(request)); - simgrid::mc::Remote temp_synchro; - mc_model_checker->process().read(temp_synchro, remote( - static_cast(pattern->comm_addr))); - simgrid::kernel::activity::Comm* synchro = - static_cast(temp_synchro.getBuffer()); + simgrid::mc::Remote temp_synchro; + mc_model_checker->process().read(temp_synchro, + remote(static_cast(pattern->comm_addr))); + simgrid::kernel::activity::CommImpl* synchro = + static_cast(temp_synchro.getBuffer()); char* remote_name = mc_model_checker->process().read( - (std::uint64_t)(synchro->mbox ? &synchro->mbox->name : &synchro->mbox_cpy->name)); - pattern->rdv = mc_model_checker->process().read_string(remote_name); + RemotePtr((uint64_t)(synchro->mbox ? &synchro->mbox->name_ : &synchro->mbox_cpy->name_))); + pattern->rdv = mc_model_checker->process().read_string(RemotePtr(remote_name)); pattern->src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(synchro->src_proc))->pid; pattern->src_host = MC_smx_actor_get_host_name(issuer); - struct s_smpi_mpi_request mpi_request = - mc_model_checker->process().read( - (std::uint64_t) simcall_comm_isend__get__data(request)); - pattern->tag = mpi_request.tag; + simgrid::smpi::Request mpi_request = mc_model_checker->process().read( + RemotePtr((std::uint64_t)simcall_comm_isend__get__data(request))); + pattern->tag = mpi_request.tag(); - if (synchro->src_buff != nullptr){ + if (synchro->src_buff != nullptr) { pattern->data.resize(synchro->src_buff_size); - mc_model_checker->process().read_bytes( - pattern->data.data(), pattern->data.size(), - remote(synchro->src_buff)); + mc_model_checker->process().read_bytes(pattern->data.data(), pattern->data.size(), remote(synchro->src_buff)); } - if(mpi_request.detached){ - if (!this->initial_communications_pattern_done) { + if(mpi_request.detached()){ + if (not this->initial_communications_pattern_done) { /* Store comm pattern */ - simgrid::mc::PatternCommunicationList* list = xbt_dynar_get_as( - initial_communications_pattern, pattern->src_proc, - simgrid::mc::PatternCommunicationList*); + simgrid::mc::PatternCommunicationList* list = + xbt_dynar_get_as(initial_communications_pattern, pattern->src_proc, simgrid::mc::PatternCommunicationList*); list->list.push_back(std::move(pattern)); } else { /* Evaluate comm determinism */ this->deterministic_comm_pattern(pattern->src_proc, pattern.get(), backtracking); - xbt_dynar_get_as( - initial_communications_pattern, pattern->src_proc, simgrid::mc::PatternCommunicationList* - )->index_comm++; + xbt_dynar_get_as(initial_communications_pattern, pattern->src_proc, simgrid::mc::PatternCommunicationList*) + ->index_comm++; } return; } } else if (call_type == MC_CALL_TYPE_RECV) { pattern->type = simgrid::mc::PatternCommunicationType::receive; - pattern->comm_addr = simcall_comm_irecv__get__result(request); + pattern->comm_addr = static_cast(simcall_comm_irecv__getraw__result(request)); - struct s_smpi_mpi_request mpi_request; - mc_model_checker->process().read( - &mpi_request, remote((struct s_smpi_mpi_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(); - simgrid::mc::Remote temp_comm; - mc_model_checker->process().read(temp_comm, remote( - static_cast(pattern->comm_addr))); - simgrid::kernel::activity::Comm* comm = temp_comm.getBuffer(); + simgrid::mc::Remote temp_comm; + mc_model_checker->process().read(temp_comm, + remote(static_cast(pattern->comm_addr))); + simgrid::kernel::activity::CommImpl* comm = temp_comm.getBuffer(); char* remote_name; - mc_model_checker->process().read(&remote_name, - remote(comm->mbox ? &comm->mbox->name : &comm->mbox_cpy->name)); - pattern->rdv = mc_model_checker->process().read_string(remote_name); + mc_model_checker->process().read( + &remote_name, remote(comm->mbox ? &simgrid::xbt::string::to_string_data(comm->mbox->name_).data + : &simgrid::xbt::string::to_string_data(comm->mbox_cpy->name_).data)); + pattern->rdv = mc_model_checker->process().read_string(RemotePtr(remote_name)); pattern->dst_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->dst_proc))->pid; pattern->dst_host = MC_smx_actor_get_host_name(issuer); } else xbt_die("Unexpected call_type %i", (int) call_type); - XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", - pattern.get(), issuer->pid); - xbt_dynar_t dynar = - xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t); + XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", pattern.get(), issuer->pid); + xbt_dynar_t dynar = xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t); simgrid::mc::PatternCommunication* pattern2 = pattern.release(); xbt_dynar_push(dynar, &pattern2); } - void CommunicationDeterminismChecker::complete_comm_pattern( - xbt_dynar_t list, simgrid::mc::RemotePtr comm_addr, - unsigned int issuer, int backtracking) + xbt_dynar_t list, simgrid::mc::RemotePtr comm_addr, unsigned int issuer, + int backtracking) { simgrid::mc::PatternCommunication* current_comm_pattern; unsigned int cursor = 0; @@ -277,21 +266,19 @@ void CommunicationDeterminismChecker::complete_comm_pattern( update_comm_pattern(current_comm_pattern, comm_addr); completed = 1; simgrid::mc::PatternCommunication* temp; - xbt_dynar_remove_at( - xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), - cursor, &temp); + xbt_dynar_remove_at(xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, &temp); comm_pattern = std::unique_ptr(temp); XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", issuer, cursor); break; } - if(!completed) + if (not completed) xbt_die("Corresponding communication not found!"); - simgrid::mc::PatternCommunicationList* pattern = xbt_dynar_get_as( - initial_communications_pattern, issuer, simgrid::mc::PatternCommunicationList*); + simgrid::mc::PatternCommunicationList* pattern = + xbt_dynar_get_as(initial_communications_pattern, issuer, simgrid::mc::PatternCommunicationList*); - if (!this->initial_communications_pattern_done) + if (not this->initial_communications_pattern_done) /* Store comm pattern */ pattern->list.push_back(std::move(comm_pattern)); else { @@ -301,10 +288,8 @@ void CommunicationDeterminismChecker::complete_comm_pattern( } } -CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& session) - : Checker(session) +CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& session) : Checker(session) { - } CommunicationDeterminismChecker::~CommunicationDeterminismChecker() = default; @@ -323,25 +308,20 @@ std::vector CommunicationDeterminismChecker::getTextualTrace() // o for (auto const& state : stack_) { smx_simcall_t req = &state->executed_req; if (req) - trace.push_back(simgrid::mc::request_to_string( - req, state->transition.argument, simgrid::mc::RequestType::executed)); + trace.push_back( + simgrid::mc::request_to_string(req, state->transition.argument, simgrid::mc::RequestType::executed)); } return trace; } void CommunicationDeterminismChecker::logState() // override { - Checker::logState(); - if (_sg_mc_comms_determinism && - !this->recv_deterministic && - this->send_deterministic) { + if (_sg_mc_comms_determinism && not this->recv_deterministic && this->send_deterministic) { XBT_INFO("******************************************************"); XBT_INFO("**** Only-send-deterministic communication pattern ****"); XBT_INFO("******************************************************"); XBT_INFO("%s", this->recv_diff); - } else if(_sg_mc_comms_determinism && - !this->send_deterministic && - this->recv_deterministic) { + } else if (_sg_mc_comms_determinism && not this->send_deterministic && this->recv_deterministic) { XBT_INFO("******************************************************"); XBT_INFO("**** Only-recv-deterministic communication pattern ****"); XBT_INFO("******************************************************"); @@ -350,10 +330,9 @@ void CommunicationDeterminismChecker::logState() // override XBT_INFO("Expanded states = %lu", expandedStatesCount_); XBT_INFO("Visited states = %lu", mc_model_checker->visited_states); XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions); - XBT_INFO("Send-deterministic : %s", !this->send_deterministic ? "No" : "Yes"); + XBT_INFO("Send-deterministic : %s", not this->send_deterministic ? "No" : "Yes"); if (_sg_mc_comms_determinism) - XBT_INFO("Recv-deterministic : %s", - !this->recv_deterministic ? "No" : "Yes"); + XBT_INFO("Recv-deterministic : %s", not this->recv_deterministic ? "No" : "Yes"); } void CommunicationDeterminismChecker::prepare() @@ -382,18 +361,17 @@ void CommunicationDeterminismChecker::prepare() /* 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())) - initial_state->interleave(actor.copy.getBuffer()); + initial_state->addInterleavingSet(actor.copy.getBuffer()); stack_.push_back(std::move(initial_state)); } -static inline -bool all_communications_are_finished() +static inline bool all_communications_are_finished() { for (size_t current_actor = 1; current_actor < MC_smx_get_maxpid(); current_actor++) { xbt_dynar_t pattern = xbt_dynar_get_as(incomplete_communications_pattern, current_actor, xbt_dynar_t); - if (!xbt_dynar_is_empty(pattern)) { - XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited."); + if (not xbt_dynar_is_empty(pattern)) { + XBT_DEBUG("Some communications are not finished, cannot stop the exploration! State not visited."); return false; } } @@ -403,19 +381,16 @@ bool all_communications_are_finished() void CommunicationDeterminismChecker::restoreState() { /* Intermediate backtracking */ - { - simgrid::mc::State* state = stack_.back().get(); - if (state->system_state) { - simgrid::mc::restore_snapshot(state->system_state); - MC_restore_communications_pattern(state); - return; - } + simgrid::mc::State* state = stack_.back().get(); + if (state->system_state) { + simgrid::mc::restore_snapshot(state->system_state); + MC_restore_communications_pattern(state); + return; } /* Restore the initial state */ simgrid::mc::session->restoreInitialState(); - // int n = xbt_dynar_length(incomplete_communications_pattern); unsigned n = MC_smx_get_maxpid(); assert(n == xbt_dynar_length(incomplete_communications_pattern)); assert(n == xbt_dynar_length(initial_communications_pattern)); @@ -451,33 +426,32 @@ void CommunicationDeterminismChecker::restoreState() } } -void CommunicationDeterminismChecker::main(void) +void CommunicationDeterminismChecker::main() { std::unique_ptr visited_state = nullptr; smx_simcall_t req = nullptr; - while (!stack_.empty()) { - + while (not stack_.empty()) { /* Get current state */ simgrid::mc::State* state = stack_.back().get(); XBT_DEBUG("**************************************************"); - XBT_DEBUG("Exploration depth = %zi (state = %d, interleaved processes = %zd)", - stack_.size(), state->num, + XBT_DEBUG("Exploration depth = %zu (state = %d, interleaved processes = %zu)", stack_.size(), state->num, state->interleaveSize()); /* Update statistics */ mc_model_checker->visited_states++; - if (stack_.size() <= (std::size_t) _sg_mc_max_depth - && (req = MC_state_get_request(state)) != nullptr - && (visited_state == nullptr)) { + if (stack_.size() <= (std::size_t)_sg_mc_max_depth) + req = MC_state_get_request(state); + else + req = nullptr; + + if (req != nullptr && visited_state == nullptr) { int req_num = state->transition.argument; - XBT_DEBUG("Execute: %s", - simgrid::mc::request_to_string( - req, req_num, simgrid::mc::RequestType::simix).c_str()); + XBT_DEBUG("Execute: %s", simgrid::mc::request_to_string(req, req_num, simgrid::mc::RequestType::simix).c_str()); std::string req_str; if (dot_output != nullptr) @@ -494,7 +468,7 @@ void CommunicationDeterminismChecker::main(void) mc_model_checker->handle_simcall(state->transition); /* After this call req is no longer useful */ - if (!this->initial_communications_pattern_done) + if (not this->initial_communications_pattern_done) MC_handle_comm_pattern(call, req, req_num, initial_communications_pattern, 0); else MC_handle_comm_pattern(call, req, req_num, nullptr, 0); @@ -506,48 +480,48 @@ void CommunicationDeterminismChecker::main(void) std::unique_ptr next_state = std::unique_ptr(new simgrid::mc::State(++expandedStatesCount_)); - /* If comm determinism verification, we cannot stop the exploration if - some communications are not finished (at least, data are transferred). - These communications are incomplete and they cannot be analyzed and - compared with the initial pattern. */ - bool compare_snapshots = all_communications_are_finished() - && this->initial_communications_pattern_done; + /* If comm determinism verification, we cannot stop the exploration if some communications are not finished (at + * least, data are transferred). These communications are incomplete and they cannot be analyzed and compared + * with the initial pattern. */ + bool compare_snapshots = all_communications_are_finished() && this->initial_communications_pattern_done; + + if (_sg_mc_max_visited_states != 0) + visited_state = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), compare_snapshots); + else + visited_state = nullptr; - if (_sg_mc_visited == 0 - || (visited_state = visitedStates_.addVisitedState( - expandedStatesCount_, next_state.get(), compare_snapshots)) == nullptr) { + if (visited_state == nullptr) { /* 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())) - next_state->interleave(actor.copy.getBuffer()); + next_state->addInterleavingSet(actor.copy.getBuffer()); if (dot_output != nullptr) fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str.c_str()); } else if (dot_output != nullptr) - fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", - state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str.c_str()); + fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, + visited_state->original_num == -1 ? visited_state->num : visited_state->original_num, req_str.c_str()); stack_.push_back(std::move(next_state)); } else { if (stack_.size() > (std::size_t) _sg_mc_max_depth) - XBT_WARN("/!\\ Max depth reached ! /!\\ "); + XBT_WARN("/!\\ Max depth reached! /!\\ "); else if (visited_state != nullptr) - XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num); + XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", + visited_state->original_num == -1 ? visited_state->num : visited_state->original_num); else - XBT_DEBUG("There are no more processes to interleave. (depth %zi)", - stack_.size()); + XBT_DEBUG("There are no more processes to interleave. (depth %zu)", stack_.size()); - if (!this->initial_communications_pattern_done) + if (not this->initial_communications_pattern_done) this->initial_communications_pattern_done = 1; /* Trash the current state, no longer needed */ - XBT_DEBUG("Delete state %d at depth %zi", - state->num, stack_.size()); + XBT_DEBUG("Delete state %d at depth %zu", state->num, stack_.size()); stack_.pop_back(); visited_state = nullptr; @@ -555,28 +529,24 @@ void CommunicationDeterminismChecker::main(void) /* Check for deadlocks */ if (mc_model_checker->checkDeadlock()) { MC_show_deadlock(); - throw new simgrid::mc::DeadlockError(); + throw simgrid::mc::DeadlockError(); } - while (!stack_.empty()) { + while (not stack_.empty()) { std::unique_ptr state = std::move(stack_.back()); stack_.pop_back(); - if (state->interleaveSize() - && stack_.size() < (std::size_t) _sg_mc_max_depth) { + if (state->interleaveSize() && stack_.size() < (std::size_t)_sg_mc_max_depth) { /* We found a back-tracking point, let's loop */ - XBT_DEBUG("Back-tracking to state %d at depth %zi", - state->num, stack_.size() + 1); + XBT_DEBUG("Back-tracking to state %d at depth %zu", state->num, stack_.size() + 1); stack_.push_back(std::move(state)); this->restoreState(); - XBT_DEBUG("Back-tracking to state %d at depth %zi done", - stack_.back()->num, stack_.size()); + XBT_DEBUG("Back-tracking to state %d at depth %zu done", stack_.back()->num, stack_.size()); break; } else { - XBT_DEBUG("Delete state %d at depth %zi", - state->num, stack_.size() + 1); + XBT_DEBUG("Delete state %d at depth %zu", state->num, stack_.size() + 1); } } }