Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Prepare to debug the depends
authorMartin Quinson <martin.quinson@ens-rennes.fr>
Fri, 11 Feb 2022 10:28:26 +0000 (11:28 +0100)
committerMartin Quinson <martin.quinson@ens-rennes.fr>
Fri, 11 Feb 2022 11:28:18 +0000 (12:28 +0100)
src/mc/Transition.cpp
src/mc/checker/SafetyChecker.cpp

index 29a4196..28779c3 100644 (file)
@@ -55,9 +55,8 @@ CommWaitTransition::CommWaitTransition(aid_t issuer, int times_considered, char*
 }
 std::string CommWaitTransition::to_string(bool verbose)
 {
 }
 std::string CommWaitTransition::to_string(bool verbose)
 {
-  textual_ = Transition::to_string(verbose);
-  textual_ += xbt::string_printf("%ld: WaitComm(from %ld to %ld, mbox=%u, %s", aid_, sender_, receiver_, mbox_,
-                                 (timeout_ ? "timeout" : "no timeout"));
+  textual_ = xbt::string_printf("%ld: WaitComm(from %ld to %ld, mbox=%u, %s", aid_, sender_, receiver_, mbox_,
+                                (timeout_ ? "timeout" : "no timeout"));
   if (verbose) {
     textual_ += ", src_buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_);
     textual_ += ", dst_buff=" + xbt::string_printf("%p", dst_buff_);
   if (verbose) {
     textual_ += ", src_buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_);
     textual_ += ", dst_buff=" + xbt::string_printf("%p", dst_buff_);
@@ -99,7 +98,7 @@ CommRecvTransition::CommRecvTransition(aid_t issuer, int times_considered, char*
 }
 std::string CommRecvTransition::to_string(bool verbose)
 {
 }
 std::string CommRecvTransition::to_string(bool verbose)
 {
-  textual_ = xbt::string_printf("%ld: Recv(mbox=%u", aid_, mbox_);
+  textual_ = xbt::string_printf("%ld: iRecv(mbox=%u", aid_, mbox_);
   if (verbose)
     textual_ += ", buff=" + xbt::string_printf("%p", dst_buff_);
   textual_ += ")";
   if (verbose)
     textual_ += ", buff=" + xbt::string_printf("%p", dst_buff_);
   textual_ += ")";
@@ -149,7 +148,7 @@ CommSendTransition::CommSendTransition(aid_t issuer, int times_considered, char*
 }
 std::string CommSendTransition::to_string(bool verbose = false)
 {
 }
 std::string CommSendTransition::to_string(bool verbose = false)
 {
-  textual_ = xbt::string_printf("%ld: Send(mbox=%u", aid_, mbox_);
+  textual_ = xbt::string_printf("%ld: iSend(mbox=%u", aid_, mbox_);
   if (verbose)
     textual_ += ", buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_);
   textual_ += ")";
   if (verbose)
     textual_ += ", buff=" + xbt::string_printf("%p", src_buff_) + ", size=" + std::to_string(size_);
   textual_ += ")";
index 17ffc58..4d2cc15 100644 (file)
@@ -196,11 +196,9 @@ void SafetyChecker::backtrack()
                     prev_state->get_transition()->to_cstring(), issuer_id);
           break;
         } else if (prev_state->get_transition()->depends(state->get_transition())) {
                     prev_state->get_transition()->to_cstring(), issuer_id);
           break;
         } else if (prev_state->get_transition()->depends(state->get_transition())) {
-          if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
-            XBT_DEBUG("Dependent Transitions:");
-            XBT_DEBUG("  %s (state=%ld)", prev_state->get_transition()->to_cstring(), prev_state->num_);
-            XBT_DEBUG("  %s (state=%ld)", state->get_transition()->to_cstring(), state->num_);
-          }
+          XBT_VERB("Dependent Transitions:");
+          XBT_VERB("  %s (state=%ld)", prev_state->get_transition()->to_cstring(), prev_state->num_);
+          XBT_VERB("  %s (state=%ld)", state->get_transition()->to_cstring(), state->num_);
 
           if (not prev_state->actor_states_[issuer_id].is_done())
             prev_state->mark_todo(issuer_id);
 
           if (not prev_state->actor_states_[issuer_id].is_done())
             prev_state->mark_todo(issuer_id);
@@ -208,11 +206,9 @@ void SafetyChecker::backtrack()
             XBT_DEBUG("Actor %ld is in done set", issuer_id);
           break;
         } else {
             XBT_DEBUG("Actor %ld is in done set", issuer_id);
           break;
         } else {
-          if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
-            XBT_DEBUG("INDEPENDENT Transitions:");
-            XBT_DEBUG("  %s (state=%ld)", prev_state->get_transition()->to_cstring(), prev_state->num_);
-            XBT_DEBUG("  %s (state=%ld)", state->get_transition()->to_cstring(), state->num_);
-          }
+          XBT_VERB("INDEPENDENT Transitions:");
+          XBT_VERB("  %s (state=%ld)", prev_state->get_transition()->to_cstring(), prev_state->num_);
+          XBT_VERB("  %s (state=%ld)", state->get_transition()->to_cstring(), state->num_);
         }
       }
     }
         }
       }
     }