cosmetics

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

diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp
index 03a2f4f..e899990 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.cpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.cpp
@@ -10,18 +10,17 @@
 #include <xbt/log.h>
 #include <xbt/sysdep.h>
 
-#include "src/mc/mc_state.h"
-#include "src/mc/mc_comm_pattern.h"
-#include "src/mc/mc_request.h"
-#include "src/mc/mc_safety.h"
+#include "src/mc/Transition.hpp"
+#include "src/mc/VisitedState.hpp"
+#include "src/mc/checker/CommunicationDeterminismChecker.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_safety.h"
 #include "src/mc/mc_smx.h"
-#include "src/mc/Client.hpp"
-#include "src/mc/checker/CommunicationDeterminismChecker.hpp"
-#include "src/mc/mc_exit.h"
-#include "src/mc/VisitedState.hpp"
-#include "src/mc/Transition.hpp"
+#include "src/mc/mc_state.h"
+#include "src/mc/remote/Client.hpp"
 
 using simgrid::mc::remote;
 
@@ -307,10 +306,7 @@ CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& sessio
 
 }
 
-CommunicationDeterminismChecker::~CommunicationDeterminismChecker()
-{
-
-}
+CommunicationDeterminismChecker::~CommunicationDeterminismChecker() = default;
 
 RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
 {
@@ -361,20 +357,18 @@ void CommunicationDeterminismChecker::logState() // override
 
 void CommunicationDeterminismChecker::prepare()
 {
-
-  int i;
   const int maxpid = MC_smx_get_maxpid();
 
   // Create initial_communications_pattern elements:
   initial_communications_pattern = simgrid::xbt::newDeleteDynar<simgrid::mc::PatternCommunicationList*>();
-  for (i=0; i < maxpid; i++){
+  for (int i = 0; i < maxpid; i++) {
     simgrid::mc::PatternCommunicationList* process_list_pattern = new simgrid::mc::PatternCommunicationList();
     xbt_dynar_insert_at(initial_communications_pattern, i, &process_list_pattern);
   }
 
   // Create incomplete_communications_pattern elements:
   incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
-  for (i=0; i < maxpid; i++){
+  for (int i = 0; i < maxpid; i++) {
     xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(simgrid::mc::PatternCommunication*), nullptr);
     xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
   }
@@ -518,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())
@@ -532,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));
 
@@ -542,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());
@@ -597,12 +592,6 @@ void CommunicationDeterminismChecker::run()
 
   this->prepare();
 
-  this->initial_communications_pattern_done = 0;
-  this->recv_deterministic = 1;
-  this->send_deterministic = 1;
-  this->recv_diff = nullptr;
-  this->send_diff = nullptr;
-
   this->main();
 }