Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
cosmetics
[simgrid.git] / src / mc / checker / CommunicationDeterminismChecker.cpp
index 741e7ad..e899990 100644 (file)
@@ -13,7 +13,6 @@
 #include "src/mc/Transition.hpp"
 #include "src/mc/VisitedState.hpp"
 #include "src/mc/checker/CommunicationDeterminismChecker.hpp"
-#include "src/mc/mc_comm_pattern.h"
 #include "src/mc/mc_exit.h"
 #include "src/mc/mc_private.h"
 #include "src/mc/mc_record.h"
@@ -513,9 +512,9 @@ void CommunicationDeterminismChecker::main(void)
       bool compare_snapshots = all_communications_are_finished()
         && this->initial_communications_pattern_done;
 
-      if (_sg_mc_visited == 0
-          || (visited_state = visitedStates_.addVisitedState(
-            expandedStatesCount_, next_state.get(), compare_snapshots)) == nullptr) {
+      if (_sg_mc_max_visited_states == 0 ||
+          (visited_state = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), compare_snapshots)) ==
+              nullptr) {
 
         /* Get enabled actors and insert them in the interleave set of the next state */
         for (auto& actor : mc_model_checker->process().actors())
@@ -527,8 +526,8 @@ void CommunicationDeterminismChecker::main(void)
             state->num,  next_state->num, req_str.c_str());
 
       } else if (dot_output != nullptr)
-        fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
-          state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str.c_str());
+        fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
+                visited_state->original_num == -1 ? visited_state->num : visited_state->original_num, req_str.c_str());
 
       stack_.push_back(std::move(next_state));
 
@@ -537,7 +536,8 @@ void CommunicationDeterminismChecker::main(void)
       if (stack_.size() > (std::size_t) _sg_mc_max_depth)
         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
       else if (visited_state != nullptr)
-        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.",
+            visited_state->original_num == -1 ? visited_state->num : visited_state->original_num);
       else
         XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
           stack_.size());