Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Start moving classes into the mc/api directory
[simgrid.git] / src / mc / checker / SafetyChecker.cpp
index 17ffc58..5eff438 100644 (file)
@@ -3,10 +3,10 @@
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
+#include "src/mc/checker/SafetyChecker.hpp"
 #include "src/mc/Session.hpp"
-#include "src/mc/Transition.hpp"
 #include "src/mc/VisitedState.hpp"
-#include "src/mc/checker/SafetyChecker.hpp"
+#include "src/mc/api/Transition.hpp"
 #include "src/mc/mc_config.hpp"
 #include "src/mc/mc_exit.hpp"
 #include "src/mc/mc_private.hpp"
@@ -41,7 +41,7 @@ void SafetyChecker::check_non_termination(const State* current_state)
       XBT_INFO("Counter-example execution trace:");
       for (auto const& s : get_textual_trace())
         XBT_INFO("  %s", s.c_str());
-      api::get().dump_record_path();
+      simgrid::mc::dumpRecordPath();
       api::get().log_state();
 
       throw TerminationError();
@@ -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())) {
-          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);
@@ -208,11 +206,9 @@ void SafetyChecker::backtrack()
             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_);
         }
       }
     }