X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/b8dc7c0693d2606e9cb9f21bcced90a5174bd503..cdf6a962eb4e88efbed3df9c41343adabcf09e6c:/src/mc/checker/SafetyChecker.cpp diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp index f827c1f8dc..c08ecaa23b 100644 --- a/src/mc/checker/SafetyChecker.cpp +++ b/src/mc/checker/SafetyChecker.cpp @@ -81,7 +81,7 @@ void SafetyChecker::run() { /* This function runs the DFS algorithm the state space. * We do so iteratively instead of recursively, dealing with the call stack manually. - * This allows to explore the call stack at wish. */ + * This allows one to explore the call stack at will. */ while (not stack_.empty()) { @@ -113,7 +113,7 @@ void SafetyChecker::run() // Search an enabled transition in the current state; backtrack if the interleave set is empty // get_request also sets state.transition to be the one corresponding to the returned req - smx_simcall_t req = MC_state_get_request(state); + smx_simcall_t req = MC_state_choose_request(state); // req is now the transition of the process that was selected to be executed if (req == nullptr) { @@ -229,15 +229,16 @@ void SafetyChecker::backtrack() } else if (req->issuer_ == prev_state->internal_req.issuer_) { - XBT_DEBUG("Simcall %d and %d with same issuer", req->call_, prev_state->internal_req.call_); + XBT_DEBUG("Simcall %s and %s with same issuer", SIMIX_simcall_name(req->call_), + SIMIX_simcall_name(prev_state->internal_req.call_)); break; } else { const smx_actor_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req); - XBT_DEBUG("Simcall %d, process %ld (state %d) and simcall %d, process %ld (state %d) are independent", - req->call_, issuer->get_pid(), state->num_, prev_state->internal_req.call_, - previous_issuer->get_pid(), prev_state->num_); + XBT_DEBUG("Simcall %s, process %ld (state %d) and simcall %s, process %ld (state %d) are independent", + SIMIX_simcall_name(req->call_), issuer->get_pid(), state->num_, + SIMIX_simcall_name(prev_state->internal_req.call_), previous_issuer->get_pid(), prev_state->num_); } } }