[mc] Factorisation in mc_visited.cpp

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

diff --git a/src/mc/mc_visited.cpp b/src/mc/mc_visited.cpp
index edcfcff..e3ebc85 100644 (file)
--- a/src/mc/mc_visited.cpp
+++ b/src/mc/mc_visited.cpp
@@ -11,7 +11,7 @@
 #include "mc_safety.h"
 #include "mc_liveness.h"
 #include "mc_private.h"
-#include "mc_process.h"
+#include "mc/Process.hpp"
 #include "mc_smx.h"
 
 extern "C" {
@@ -60,13 +60,9 @@ static mc_visited_state_t visited_state_new()
     process->get_heap()->heaplimit,
     process->get_malloc_info());
 
-  if (mc_model_checker->process().is_self()) {
-    new_state->nb_processes = xbt_swag_size(simix_global->process_list);
-  } else {
-    MC_process_smx_refresh(&mc_model_checker->process());
-    new_state->nb_processes = xbt_dynar_length(
-      mc_model_checker->process().smx_process_infos);
-  }
+  MC_process_smx_refresh(&mc_model_checker->process());
+  new_state->nb_processes = xbt_dynar_length(
+    mc_model_checker->process().smx_process_infos);
 
   new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
   new_state->num = mc_stats->expanded_states;
@@ -85,13 +81,11 @@ mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automa
   pair->heap_bytes_used = mmalloc_get_bytes_used_remote(
     process->get_heap()->heaplimit,
     process->get_malloc_info());
-  if (mc_model_checker->process().is_self()) {
-    pair->nb_processes = xbt_swag_size(simix_global->process_list);
-  } else {
-    MC_process_smx_refresh(&mc_model_checker->process());
-    pair->nb_processes = xbt_dynar_length(
-      mc_model_checker->process().smx_process_infos);
-  }
+
+  MC_process_smx_refresh(&mc_model_checker->process());
+  pair->nb_processes = xbt_dynar_length(
+    mc_model_checker->process().smx_process_infos);
+
   pair->automaton_state = automaton_state;
   pair->num = pair_num;
   pair->other_num = -1;
@@ -222,6 +216,31 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
   return cursor;
 }
 
+static
+void replace_state(
+  mc_visited_state_t state_test, mc_visited_state_t new_state, int cursor)
+{
+  if (state_test->other_num == -1)
+    new_state->other_num = state_test->num;
+  else
+    new_state->other_num = state_test->other_num;
+
+  if (dot_output == NULL)
+    XBT_DEBUG("State %d already visited ! (equal to state %d)",
+      new_state->num, state_test->num);
+  else
+    XBT_DEBUG(
+      "State %d already visited ! (equal to state %d (state %d in dot_output))",
+      new_state->num, state_test->num, new_state->other_num);
+
+  /* Replace the old state with the new one (with a bigger num)
+     (when the max number of visited states is reached,  the oldest
+     one is removed according to its number (= with the min number) */
+  xbt_dynar_remove_at(visited_states, cursor, NULL);
+  xbt_dynar_insert_at(visited_states, cursor, &new_state);
+  XBT_DEBUG("Replace visited state %d with the new visited state %d",
+    state_test->num, new_state->num);
+}
 
 /**
  * \brief Checks whether a given state has already been visited by the algorithm.
@@ -297,22 +316,7 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
           if (snapshot_compare(state_test, new_state) == 0) {
             // The state has been visited:
 
-            if (state_test->other_num == -1)
-              new_state->other_num = state_test->num;
-            else
-              new_state->other_num = state_test->other_num;
-            if (dot_output == NULL)
-              XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
-            else
-              XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num);
-
-            /* Replace the old state with the new one (with a bigger num) 
-               (when the max number of visited states is reached,  the oldest 
-               one is removed according to its number (= with the min number) */
-            xbt_dynar_remove_at(visited_states, cursor, NULL);
-            xbt_dynar_insert_at(visited_states, cursor, &new_state);
-            XBT_DEBUG("Replace visited state %d with the new visited state %d", state_test->num, new_state->num);
-
+            replace_state(state_test, new_state, cursor);
             return state_test;
           }
           cursor++;
@@ -349,7 +353,7 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
       unsigned int cursor2 = 0;
       unsigned int index2 = 0;
       xbt_dynar_foreach(visited_states, cursor2, state_test){
-        if (state_test->num < min2) {
+        if (!MC_important_snapshot(state_test->system_state) && state_test->num < min2) {
           index2 = cursor2;
           min2 = state_test->num;
         }
@@ -466,7 +470,8 @@ 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 (pair_test->num < min2) {
+        if (!MC_important_snapshot(pair_test->graph_state->system_state)
+            && pair_test->num < min2) {
           index2 = cursor2;
           min2 = pair_test->num;
         }