safety: give some basic logging at verbose level already

[simgrid.git] / src / mc / checker / SafetyChecker.cpp

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index 796bed5..df92ccd 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -31,17 +31,10 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
 namespace simgrid {
 namespace mc {
 
-static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
-{
-  simgrid::mc::Snapshot* s1 = state1->system_state.get();
-  simgrid::mc::Snapshot* s2 = state2->system_state.get();
-  return snapshot_compare(s1, s2);
-}
-
 void SafetyChecker::check_non_termination(simgrid::mc::State* current_state)
 {
   for (auto state = stack_.rbegin(); state != stack_.rend(); ++state)
-    if (snapshot_compare(state->get(), current_state) == 0) {
+    if (snapshot_equal((*state)->system_state.get(), current_state->system_state.get())) {
       XBT_INFO("Non-progressive cycle: state %d -> state %d", (*state)->num, current_state->num);
       XBT_INFO("******************************************");
       XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
@@ -96,8 +89,8 @@ void SafetyChecker::run()
     simgrid::mc::State* state = stack_.back().get();
 
     XBT_DEBUG("**************************************************");
-    XBT_DEBUG("Exploration depth=%zu (state=%p, num %d)(%zu interleave)", stack_.size(), state, state->num,
-              state->interleaveSize());
+    XBT_VERB("Exploration depth=%zu (state=%p, num %d)(%zu interleave)", stack_.size(), state, state->num,
+             state->interleaveSize());
 
     mc_model_checker->visited_states++;
 
@@ -161,7 +154,7 @@ void SafetyChecker::run()
 
       /* Get an enabled process and insert it in the interleave set of the next state */
       for (auto& remoteActor : mc_model_checker->process().actors()) {
-        auto actor = remoteActor.copy.getBuffer();
+        auto actor = remoteActor.copy.get_buffer();
         if (simgrid::mc::actor_is_enabled(actor)) {
           next_state->addInterleavingSet(actor);
           if (reductionMode_ == simgrid::mc::ReductionMode::dpor)
@@ -315,8 +308,8 @@ SafetyChecker::SafetyChecker(Session& s) : Checker(s)
 
   /* Get an enabled actor and insert it in the interleave set of the initial state */
   for (auto& actor : mc_model_checker->process().actors())
-    if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
-      initial_state->addInterleavingSet(actor.copy.getBuffer());
+    if (simgrid::mc::actor_is_enabled(actor.copy.get_buffer())) {
+      initial_state->addInterleavingSet(actor.copy.get_buffer());
       if (reductionMode_ != simgrid::mc::ReductionMode::none)
         break;
     }