X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/3ed8cddf1b2849cb3db5139684348bd64d47b09e..69aaa26fa5228c31e55086fa166479732a9cd1b7:/src/mc/checker/CommunicationDeterminismChecker.cpp diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp index 05eede3028..9175947c95 100644 --- a/src/mc/checker/CommunicationDeterminismChecker.cpp +++ b/src/mc/checker/CommunicationDeterminismChecker.cpp @@ -236,8 +236,7 @@ void CommunicationDeterminismChecker::complete_comm_pattern(RemotePtrcomm_addr == comm_addr); }); - if (current_comm_pattern == std::end(incomplete_pattern)) - xbt_die("Corresponding communication not found!"); + xbt_assert(current_comm_pattern != std::end(incomplete_pattern), "Corresponding communication not found!"); update_comm_pattern(*current_comm_pattern, comm_addr); std::unique_ptr comm_pattern(*current_comm_pattern); @@ -313,11 +312,12 @@ void CommunicationDeterminismChecker::prepare() XBT_DEBUG("********* Start communication determinism verification *********"); - /* Get an enabled actor and insert it in the interleave set of the initial state */ - auto actors = api::get().get_actors(); - for (auto& actor : actors) - if (api::get().actor_is_enabled(actor.copy.get_buffer()->get_pid())) - initial_state->mark_todo(actor.copy.get_buffer()); + /* Add all enabled actors to the interleave set of the initial state */ + for (auto& act : api::get().get_actors()) { + auto actor = act.copy.get_buffer(); + if (get_session().actor_is_enabled(actor->get_pid())) + initial_state->mark_todo(actor); + } stack_.push_back(std::move(initial_state)); } @@ -344,7 +344,7 @@ void CommunicationDeterminismChecker::restoreState() return; } - session->restore_initial_state(); + get_session().restore_initial_state(); const unsigned long maxpid = api::get().get_maxpid(); assert(maxpid == incomplete_communications_pattern.size()); @@ -467,11 +467,12 @@ void CommunicationDeterminismChecker::real_run() visited_state = nullptr; if (visited_state == nullptr) { - /* Get enabled actors and insert them in the interleave set of the next state */ - auto actors = api::get().get_actors(); - for (auto& actor : actors) - if (api::get().actor_is_enabled(actor.copy.get_buffer()->get_pid())) - next_state->mark_todo(actor.copy.get_buffer()); + /* Add all enabled actors to the interleave set of the next state */ + for (auto& act : api::get().get_actors()) { + auto actor = act.copy.get_buffer(); + if (get_session().actor_is_enabled(actor->get_pid())) + next_state->mark_todo(actor); + } if (dot_output != nullptr) fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", cur_state->num_, next_state->num_, req_str.c_str()); @@ -526,13 +527,13 @@ void CommunicationDeterminismChecker::real_run() void CommunicationDeterminismChecker::run() { XBT_INFO("Check communication determinism"); - get_session()->take_initial_snapshot(); + get_session().take_initial_snapshot(); this->prepare(); this->real_run(); } -Checker* createCommunicationDeterminismChecker(Session* session) +Checker* create_communication_determinism_checker(Session* session) { return new CommunicationDeterminismChecker(session); }