[mc] Move visitedState as a field of SafetyChecker

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

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index 25abd4b..68d89d7 100644 (file)
--- 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){
@@ -100,7 +97,6 @@ int SafetyChecker::run()
 
   int value;
   smx_simcall_t req = nullptr;
-  std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
 
   while (!stack_.empty()) {
 
@@ -109,17 +105,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)) != nullptr
+        && visitedState_ == nullptr) {
 
       char* req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
       XBT_DEBUG("Execute: %s", req_str);
@@ -142,13 +139,13 @@ 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;
       }
 
       if (_sg_mc_visited == 0
-          || (visited_state = visitedStates_.addVisitedState(next_state.get(), true)) == nullptr) {
+          || (visitedState_ = visitedStates_.addVisitedState(next_state.get(), true)) == nullptr) {
 
         /* Get an enabled process and insert it in the interleave set of the next state */
         for (auto& p : mc_model_checker->process().simix_processes())
@@ -162,7 +159,7 @@ int SafetyChecker::run()
           std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
 
       } else if (dot_output != nullptr)
-        std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
+        std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num, req_str);
 
       stack_.push_back(std::move(next_state));
 
@@ -175,16 +172,13 @@ 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)
+          || visitedState_ != nullptr) {
+        if (visitedState_ == 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);
-
+          XBT_DEBUG("State already visited (equal to state %d),"
+            " exploration stopped on this path.",
+            visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num);
       } else
         XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
           stack_.size() + 1);
@@ -193,7 +187,7 @@ int SafetyChecker::run()
       XBT_DEBUG("Delete state %d at depth %zi", state->num, stack_.size());
       stack_.pop_back();
 
-      visited_state = nullptr;
+      visitedState_ = nullptr;
 
       /* Check for deadlocks */
       if (mc_model_checker->checkDeadlock()) {
@@ -329,6 +323,11 @@ SafetyChecker::SafetyChecker(Session& session) : Checker(session)
 SafetyChecker::~SafetyChecker()
 {
 }
+
+Checker* createSafetyChecker(Session& session)
+{
+  return new SafetyChecker(session);
+}
   
 }
 }