X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/7ebd6d64a6382e0dad15e4d63cd4f84d94d8312f..09477e8696995c466837f459085024435f23d34b:/src/mc/SafetyChecker.cpp

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index 25abd4bb1c..02d1304483 100644
--- a/src/mc/SafetyChecker.cpp
+++ b/src/mc/SafetyChecker.cpp
@@ -10,9 +10,6 @@
 #include <list>
 
 #include <xbt/log.h>
-#include <xbt/dynar.h>
-#include <xbt/dynar.hpp>
-#include <xbt/fifo.h>
 #include <xbt/sysdep.h>
 
 #include "src/mc/mc_state.h"
@@ -54,7 +51,7 @@ static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* stat
   return snapshot_compare(num1, s1, num2, s2);
 }
 
-bool SafetyChecker::checkNonDeterminism(simgrid::mc::State* current_state)
+bool SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
 {
   for (auto i = stack_.rbegin(); i != stack_.rend(); ++i)
     if (snapshot_compare(i->get(), current_state) == 0){
@@ -109,17 +106,18 @@ int SafetyChecker::run()
 
     XBT_DEBUG("**************************************************");
     XBT_DEBUG(
-      "Exploration depth=%zi (state=%p, num %d)(%u interleave, user_max_depth %d)",
+      "Exploration depth=%zi (state=%p, num %d)(%u interleave)",
       stack_.size(), state, state->num,
-      MC_state_interleave_size(state), user_max_depth_reached);
+      MC_state_interleave_size(state));
 
     /* Update statistics */
     mc_stats->visited_states++;
 
     /* If there are processes to interleave and the maximum depth has not been reached
        then perform one step of the exploration algorithm */
-    if (stack_.size() <= (std::size_t) _sg_mc_max_depth && !user_max_depth_reached
-        && (req = MC_state_get_request(state, &value)) && visited_state == nullptr) {
+    if (stack_.size() <= (std::size_t) _sg_mc_max_depth
+        && (req = MC_state_get_request(state, &value))
+        && visited_state == nullptr) {
 
       char* req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
       XBT_DEBUG("Execute: %s", req_str);
@@ -142,7 +140,7 @@ int SafetyChecker::run()
       std::unique_ptr<simgrid::mc::State> next_state =
         std::unique_ptr<simgrid::mc::State>(MC_state_new());
 
-      if (_sg_mc_termination && this->checkNonDeterminism(next_state.get())){
+      if (_sg_mc_termination && this->checkNonTermination(next_state.get())) {
           MC_show_non_termination();
           return SIMGRID_MC_EXIT_NON_TERMINATION;
       }
@@ -175,12 +173,9 @@ int SafetyChecker::run()
     } else {
 
       if (stack_.size() > (std::size_t) _sg_mc_max_depth
-          || user_max_depth_reached
           || visited_state != nullptr) {
 
-        if (user_max_depth_reached && visited_state == nullptr)
-          XBT_DEBUG("User max depth reached !");
-        else if (visited_state == nullptr)
+        if (visited_state == nullptr)
           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
         else
           XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);
@@ -329,6 +324,11 @@ SafetyChecker::SafetyChecker(Session& session) : Checker(session)
 SafetyChecker::~SafetyChecker()
 {
 }
+
+Checker* createSafetyChecker(Session& session)
+{
+  return new SafetyChecker(session);
+}
   
 }
 }