Adding test for SURF concurrency feature

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

diff --git a/src/mc/mc_visited.cpp b/src/mc/mc_visited.cpp
index 761c306..459db40 100644 (file)
--- a/src/mc/mc_visited.cpp
+++ b/src/mc/mc_visited.cpp
@@ -7,12 +7,12 @@
 #include <unistd.h>
 #include <sys/wait.h>
 
-#include "mc_comm_pattern.h"
-#include "mc_safety.h"
-#include "mc_liveness.h"
-#include "mc_private.h"
-#include "mc/Process.hpp"
-#include "mc_smx.h"
+#include "src/mc/mc_comm_pattern.h"
+#include "src/mc/mc_safety.h"
+#include "src/mc/mc_liveness.h"
+#include "src/mc/mc_private.h"
+#include "src/mc/Process.hpp"
+#include "src/mc/mc_smx.h"
 
 extern "C" {
 
@@ -242,6 +242,20 @@ void replace_state(
     state_test->num, new_state->num);
 }
 
+static
+bool some_dommunications_are_not_finished()
+{
+  for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
+    xbt_dynar_t pattern = xbt_dynar_get_as(
+      incomplete_communications_pattern, current_process, xbt_dynar_t);
+    if (!xbt_dynar_is_empty(pattern)) {
+      XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
+      return true;
+    }
+  }
+  return false;
+}
+
 /**
  * \brief Checks whether a given state has already been visited by the algorithm.
  */
@@ -255,16 +269,8 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
   /* If comm determinism verification, we cannot stop the exploration if some 
      communications are not finished (at least, data are transfered). These communications 
      are incomplete and they cannot be analyzed and compared with the initial pattern. */
-  int partial_comm = 0;
-  if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
-    for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
-      if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))){
-        XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
-        partial_comm = 1;
-        break;
-      }
-    }
-  }
+  int partial_comm = (_sg_mc_comms_determinism || _sg_mc_send_determinism) &&
+    some_dommunications_are_not_finished();
 
   mc_visited_state_t new_state = visited_state_new();
   graph_state->system_state = new_state->system_state;
@@ -349,7 +355,8 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
 
       mc_visited_state_t state_test;
       xbt_dynar_foreach(visited_states, cursor2, state_test){
-        if (!MC_important_snapshot(state_test->system_state) && state_test->num < min2) {
+        if (!mc_model_checker->is_important_snapshot(*state_test->system_state)
+            && state_test->num < min2) {
           index2 = cursor2;
           min2 = state_test->num;
         }
@@ -466,7 +473,7 @@ int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
       unsigned int cursor2 = 0;
       unsigned int index2 = 0;
       xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
-        if (!MC_important_snapshot(pair_test->graph_state->system_state)
+        if (!mc_model_checker->is_important_snapshot(*pair_test->graph_state->system_state)
             && pair_test->num < min2) {
           index2 = cursor2;
           min2 = pair_test->num;