X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/2bdd4ab1f667695dbf8aeedfe7d3d940991146cd..9cc0d42f835e6aa5ea5195a346098e74b0376927:/src/mc/CommunicationDeterminismChecker.cpp diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp index 3c0cd08bf2..4588869070 100644 --- a/src/mc/CommunicationDeterminismChecker.cpp +++ b/src/mc/CommunicationDeterminismChecker.cpp @@ -301,30 +301,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 CommunicationDeterminismChecker::getTextualTrace() // override { std::vector 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->req_num, simgrid::mc::RequestType::executed)); } return trace; } @@ -381,7 +373,6 @@ bool all_communications_are_finished() int CommunicationDeterminismChecker::main(void) { - int value; std::unique_ptr visited_state = nullptr; smx_simcall_t req = nullptr; @@ -399,16 +390,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->req_num; + 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 +411,12 @@ 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 */ + simgrid::mc::handle_simcall(req, req_num); /* 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();