X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/29d98d1ceb682fbc4c734a92353be4b0bcd5d17b..7a3a100990355eb757dc81106b5aac6daed0b8e1:/src/mc/checker/SafetyChecker.cpp

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index 4256b56a26..391a1aa5b1 100644
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -1,5 +1,4 @@
-/* Copyright (c) 2016. The SimGrid Team.
- * All rights reserved.                                                     */
+/* Copyright (c) 2016-2017. The SimGrid Team. All rights reserved.          */
 
 /* 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. */
@@ -18,11 +17,11 @@
 #include "src/mc/Transition.hpp"
 #include "src/mc/VisitedState.hpp"
 #include "src/mc/checker/SafetyChecker.hpp"
-#include "src/mc/mc_exit.h"
-#include "src/mc/mc_private.h"
-#include "src/mc/mc_record.h"
-#include "src/mc/mc_request.h"
-#include "src/mc/mc_smx.h"
+#include "src/mc/mc_exit.hpp"
+#include "src/mc/mc_private.hpp"
+#include "src/mc/mc_record.hpp"
+#include "src/mc/mc_request.hpp"
+#include "src/mc/mc_smx.hpp"
 
 #include "src/xbt/mmalloc/mmprivate.h"
 
@@ -49,7 +48,7 @@ void SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
       XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
       XBT_INFO("******************************************");
       XBT_INFO("Counter-example execution trace:");
-      for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
+      for (auto const& s : mc_model_checker->getChecker()->getTextualTrace())
         XBT_INFO("%s", s.c_str());
       simgrid::mc::session->logState();
 
@@ -80,7 +79,6 @@ std::vector<std::string> SafetyChecker::getTextualTrace() // override
 
 void SafetyChecker::logState() // override
 {
-  Checker::logState();
   XBT_INFO("Expanded states = %lu", expandedStatesCount_);
   XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
   XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
@@ -98,8 +96,8 @@ void SafetyChecker::run()
     simgrid::mc::State* state = stack_.back().get();
 
     XBT_DEBUG("**************************************************");
-    XBT_DEBUG("Exploration depth=%zi (state=%p, num %d)(%zu interleave)",
-      stack_.size(), state, state->num, state->interleaveSize());
+    XBT_DEBUG("Exploration depth=%zu (state=%p, num %d)(%zu interleave)", stack_.size(), state, state->num,
+              state->interleaveSize());
 
     mc_model_checker->visited_states++;
 
@@ -126,7 +124,7 @@ void SafetyChecker::run()
     // req is now the transition of the process that was selected to be executed
 
     if (req == nullptr) {
-      XBT_DEBUG("There are no more processes to interleave. (depth %zi)", stack_.size() + 1);
+      XBT_DEBUG("There are no more processes to interleave. (depth %zu)", stack_.size() + 1);
 
       this->backtrack();
       continue;
@@ -247,7 +245,7 @@ void SafetyChecker::backtrack()
         } else {
 
           const smx_actor_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
-          XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independent",
+          XBT_DEBUG("Simcall %d, process %ld (state %d) and simcall %d, process %ld (state %d) are independent",
                     req->call, issuer->pid, state->num,
                     prev_state->internal_req.call,
                     previous_issuer->pid,
@@ -260,15 +258,13 @@ void SafetyChecker::backtrack()
     if (state->interleaveSize()
         && stack_.size() < (std::size_t) _sg_mc_max_depth) {
       /* We found a back-tracking point, let's loop */
-      XBT_DEBUG("Back-tracking to state %d at depth %zi", state->num, stack_.size() + 1);
+      XBT_DEBUG("Back-tracking to state %d at depth %zu", state->num, stack_.size() + 1);
       stack_.push_back(std::move(state));
       this->restoreState();
-      XBT_DEBUG("Back-tracking to state %d at depth %zi done",
-        stack_.back()->num, stack_.size());
+      XBT_DEBUG("Back-tracking to state %d at depth %zu done", stack_.back()->num, stack_.size());
       break;
     } else {
-      XBT_DEBUG("Delete state %d at depth %zi",
-        state->num, stack_.size() + 1);
+      XBT_DEBUG("Delete state %d at depth %zu", state->num, stack_.size() + 1);
     }
   }
 }
@@ -335,6 +331,6 @@ Checker* createSafetyChecker(Session& session)
 {
   return new SafetyChecker(session);
 }
-  
+
 }
 }