Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Merge branch 'master' into 'master'
[simgrid.git] / src / mc / checker / SafetyChecker.cpp
index f827c1f..c08ecaa 100644 (file)
@@ -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_);
         }
       }
     }