X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/20725839bfdac54bf58497e0c34705ba37f19265..9b00b25919fb4fe7311031c78a13e7ae2055df70:/src/mc/mc_visited.cpp

diff --git a/src/mc/mc_visited.cpp b/src/mc/mc_visited.cpp
index 391f445669..38f0cbf5b6 100644
--- a/src/mc/mc_visited.cpp
+++ b/src/mc/mc_visited.cpp
@@ -42,11 +42,11 @@ static int is_exploration_stack_state(mc_visited_state_t state){
 
 void visited_state_free(mc_visited_state_t state)
 {
-  if (state) {
-    if(!is_exploration_stack_state(state))
-      delete state->system_state;
-    xbt_free(state);
-  }
+  if (!state)
+    return;
+  if(!is_exploration_stack_state(state))
+    delete state->system_state;
+  xbt_free(state);
 }
 
 void visited_state_free_voidp(void *s)
@@ -67,8 +67,8 @@ static mc_visited_state_t visited_state_new()
     process->get_malloc_info());
 
   MC_process_smx_refresh(&mc_model_checker->process());
-  new_state->nb_processes = xbt_dynar_length(
-    mc_model_checker->process().smx_process_infos);
+  new_state->nb_processes =
+    mc_model_checker->process().smx_process_infos.size();
 
   new_state->system_state = simgrid::mc::take_snapshot(mc_stats->expanded_states);
   new_state->num = mc_stats->expanded_states;
@@ -79,18 +79,18 @@ static mc_visited_state_t visited_state_new()
 mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state)
 {
   simgrid::mc::Process* process = &(mc_model_checker->process());
-  mc_visited_pair_t pair = NULL;
+  mc_visited_pair_t pair = nullptr;
   pair = xbt_new0(s_mc_visited_pair_t, 1);
   pair->graph_state = graph_state;
-  if(pair->graph_state->system_state == NULL)
+  if(pair->graph_state->system_state == nullptr)
     pair->graph_state->system_state = simgrid::mc::take_snapshot(pair_num);
   pair->heap_bytes_used = mmalloc_get_bytes_used_remote(
     process->get_heap()->heaplimit,
     process->get_malloc_info());
 
   MC_process_smx_refresh(&mc_model_checker->process());
-  pair->nb_processes = xbt_dynar_length(
-    mc_model_checker->process().smx_process_infos);
+  pair->nb_processes =
+    mc_model_checker->process().smx_process_infos.size();
 
   pair->automaton_state = automaton_state;
   pair->num = pair_num;
@@ -98,7 +98,7 @@ mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automa
   pair->acceptance_removed = 0;
   pair->visited_removed = 0;
   pair->acceptance_pair = 0;
-  pair->atomic_propositions = xbt_dynar_new(sizeof(int), NULL);
+  pair->atomic_propositions = xbt_dynar_new(sizeof(int), nullptr);
   unsigned int cursor = 0;
   int value;
   xbt_dynar_foreach(atomic_propositions, cursor, value)
@@ -120,12 +120,12 @@ static int is_exploration_stack_pair(mc_visited_pair_t pair){
 
 void MC_visited_pair_delete(mc_visited_pair_t p)
 {
-  p->automaton_state = NULL;
+  p->automaton_state = nullptr;
   if( !is_exploration_stack_pair(p))
     MC_state_delete(p->graph_state, 1);
   xbt_dynar_free(&(p->atomic_propositions));
   xbt_free(p);
-  p = NULL;
+  p = nullptr;
 }
 
 /**
@@ -172,16 +172,15 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
       nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
       heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
     }
-    if (nb_processes_test < nb_processes) {
+    if (nb_processes_test < nb_processes)
       start = cursor + 1;
-    } else if (nb_processes_test > nb_processes) {
+    else if (nb_processes_test > nb_processes)
       end = cursor - 1;
-    } else {
-      if (heap_bytes_used_test < heap_bytes_used) {
-        start = cursor + 1;
-      } else if (heap_bytes_used_test > heap_bytes_used) {
-        end = cursor - 1;
-      } else {
+    else if (heap_bytes_used_test < heap_bytes_used)
+      start = cursor + 1;
+    else if (heap_bytes_used_test > heap_bytes_used)
+      end = cursor - 1;
+    else {
         *min = *max = cursor;
         previous_cursor = cursor - 1;
         while (previous_cursor >= 0) {
@@ -216,7 +215,6 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
           next_cursor++;
         }
         return -1;
-      }
     }
   }
   return cursor;
@@ -231,7 +229,7 @@ void replace_state(
   else
     new_state->other_num = state_test->other_num;
 
-  if (dot_output == NULL)
+  if (dot_output == nullptr)
     XBT_DEBUG("State %d already visited ! (equal to state %d)",
       new_state->num, state_test->num);
   else
@@ -242,7 +240,7 @@ void replace_state(
   /* 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_remove_at(visited_states, cursor, nullptr);
   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);
@@ -268,9 +266,8 @@ bool some_dommunications_are_not_finished()
 
 mc_visited_state_t is_visited_state(mc_state_t graph_state)
 {
-
   if (_sg_mc_visited == 0)
-    return NULL;
+    return nullptr;
 
   /* If comm determinism verification, we cannot stop the exploration if some 
      communications are not finished (at least, data are transfered). These communications 
@@ -284,11 +281,9 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
   XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num);
 
   if (xbt_dynar_is_empty(visited_states)) {
-
     xbt_dynar_push(visited_states, &new_state);
-    return NULL;
-
-  } else {
+    return nullptr;
+  }
 
     int min = -1, max = -1, index;
 
@@ -304,11 +299,11 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
          new_state->other_num = state_test->num;
          else
          new_state->other_num = state_test->other_num;
-         if(dot_output == NULL)
+         if(dot_output == nullptr)
          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);
-         xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
+         xbt_dynar_remove_at(visited_states, (min + res) - 1, nullptr);
          xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
          return new_state->other_num;
          } */
@@ -336,21 +331,21 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
 
       // The state has not been visited: insert the state in the dynamic array.
       mc_visited_state_t state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
-      if (state_test->nb_processes < new_state->nb_processes) {
+      if (state_test->nb_processes < new_state->nb_processes)
         xbt_dynar_insert_at(visited_states, index + 1, &new_state);
-      } else {
-        if (state_test->heap_bytes_used < new_state->heap_bytes_used)
-          xbt_dynar_insert_at(visited_states, index + 1, &new_state);
-        else
-          xbt_dynar_insert_at(visited_states, index, &new_state);
-      }
+      else if (state_test->heap_bytes_used < new_state->heap_bytes_used)
+        xbt_dynar_insert_at(visited_states, index + 1, &new_state);
+      else
+        xbt_dynar_insert_at(visited_states, index, &new_state);
 
        XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
 
     }
 
-    // We have reached the maximum number of stored states;
-    if ((ssize_t) xbt_dynar_length(visited_states) > _sg_mc_visited) {
+  if ((ssize_t) xbt_dynar_length(visited_states) <= _sg_mc_visited)
+    return nullptr;
+
+  // We have reached the maximum number of stored states;
 
       XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
 
@@ -360,21 +355,18 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
       unsigned int index2 = 0;
 
       mc_visited_state_t state_test;
-      xbt_dynar_foreach(visited_states, cursor2, state_test){
+      xbt_dynar_foreach(visited_states, cursor2, state_test)
         if (!mc_model_checker->is_important_snapshot(*state_test->system_state)
             && state_test->num < min2) {
           index2 = cursor2;
           min2 = state_test->num;
         }
-      }
 
       // and drop it:
-      xbt_dynar_remove_at(visited_states, index2, NULL);
+      xbt_dynar_remove_at(visited_states, index2, nullptr);
       XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
-    }
 
-    return NULL;
-  }
+    return nullptr;
 }
 
 /**
@@ -385,19 +377,16 @@ int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
   if (_sg_mc_visited == 0)
     return -1;
 
-  mc_visited_pair_t new_visited_pair = NULL;
-
-  if (visited_pair == NULL) {
+  mc_visited_pair_t new_visited_pair = nullptr;
+  if (visited_pair == nullptr)
     new_visited_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
-  } else {
+  else
     new_visited_pair = visited_pair;
-  }
 
   if (xbt_dynar_is_empty(visited_pairs)) {
-
     xbt_dynar_push(visited_pairs, &new_visited_pair);
-
-  } else {
+    return -1;
+  }
 
     int min = -1, max = -1, index;
     //int res;
@@ -414,11 +403,11 @@ int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
          pair->other_num = pair_test->num;
          else
          pair->other_num = pair_test->other_num;
-         if(dot_output == NULL)
+         if(dot_output == nullptr)
          XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
          else
          XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
-         xbt_dynar_remove_at(visited_pairs, (min + res) - 1, NULL);
+         xbt_dynar_remove_at(visited_pairs, (min + res) - 1, nullptr);
          xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
          pair_test->visited_removed = 1;
          if(pair_test->stack_removed && pair_test->visited_removed){
@@ -442,19 +431,16 @@ int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
                 new_visited_pair->other_num = pair_test->num;
               else
                 new_visited_pair->other_num = pair_test->other_num;
-              if (dot_output == NULL)
+              if (dot_output == nullptr)
                 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
               else
                 XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_visited_pair->num, pair_test->num, new_visited_pair->other_num);
               xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
               xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
               pair_test->visited_removed = 1;
-              if (pair_test->acceptance_pair) {
-                if (pair_test->acceptance_removed == 1)
-                  MC_visited_pair_delete(pair_test);
-              } else {
+              if (!pair_test->acceptance_pair
+                  || pair_test->acceptance_removed == 1)
                 MC_visited_pair_delete(pair_test);
-              }
               return new_visited_pair->other_num;
             }
           }
@@ -464,14 +450,12 @@ int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
       xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
     } else {
       pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index, mc_visited_pair_t);
-      if (pair_test->nb_processes < new_visited_pair->nb_processes) {
+      if (pair_test->nb_processes < new_visited_pair->nb_processes)
         xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
-      } else {
-        if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
-          xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
-        else
-          xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
-      }
+      else if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
+        xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
+      else
+        xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
     }
 
     if ((ssize_t) xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
@@ -487,15 +471,9 @@ int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
       }
       xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
       pair_test->visited_removed = 1;
-      if (pair_test->acceptance_pair) {
-        if (pair_test->acceptance_removed)
-          MC_visited_pair_delete(pair_test);
-      } else {
+      if (!pair_test->acceptance_pair || pair_test->acceptance_removed)
         MC_visited_pair_delete(pair_test);
-      }
     }
-
-  }
   return -1;
 }