[mc] Move things in simgrid::mc

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

diff --git a/src/mc/mc_liveness.cpp b/src/mc/mc_liveness.cpp
index d184f90..fbea394 100644 (file)
--- a/src/mc/mc_liveness.cpp
+++ b/src/mc/mc_liveness.cpp
@@ -57,11 +57,9 @@ static mc_visited_pair_t is_reached_acceptance_pair(mc_pair_t pair)
   new_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
   new_pair->acceptance_pair = 1;
 
-  if (xbt_dynar_is_empty(acceptance_pairs)) {
-
+  if (xbt_dynar_is_empty(acceptance_pairs))
     xbt_dynar_push(acceptance_pairs, &new_pair);
-
-  } else {
+  else {
 
     int min = -1, max = -1, index;
     //int res;
@@ -99,14 +97,12 @@ static mc_visited_pair_t is_reached_acceptance_pair(mc_pair_t pair)
       xbt_dynar_insert_at(acceptance_pairs, min, &new_pair);
     } else {
       pair_test = (mc_visited_pair_t) xbt_dynar_get_as(acceptance_pairs, index, mc_visited_pair_t);
-      if (pair_test->nb_processes < new_pair->nb_processes) {
+      if (pair_test->nb_processes < new_pair->nb_processes)
         xbt_dynar_insert_at(acceptance_pairs, index + 1, &new_pair);
-      } else {
-        if (pair_test->heap_bytes_used < new_pair->heap_bytes_used)
-          xbt_dynar_insert_at(acceptance_pairs, index + 1, &new_pair);
-        else
-          xbt_dynar_insert_at(acceptance_pairs, index, &new_pair);
-      }
+      else if (pair_test->heap_bytes_used < new_pair->heap_bytes_used)
+        xbt_dynar_insert_at(acceptance_pairs, index + 1, &new_pair);
+      else
+        xbt_dynar_insert_at(acceptance_pairs, index, &new_pair);
     }
   }
   return new_pair;
@@ -118,12 +114,11 @@ static void remove_acceptance_pair(int pair_num)
   mc_visited_pair_t pair_test = nullptr;
   int pair_found = 0;
 
-  xbt_dynar_foreach(acceptance_pairs, cursor, pair_test) {
+  xbt_dynar_foreach(acceptance_pairs, cursor, pair_test)
     if (pair_test->num == pair_num) {
        pair_found = 1;
       break;
     }
-  }
 
   if(pair_found == 1) {
     xbt_dynar_remove_at(acceptance_pairs, cursor, &pair_test);
@@ -165,9 +160,8 @@ static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l,
       }
       return -1;
     }
-  case 4:{
-      return 2;
-    }
+  case 4:
+    return 2;
   default:
     return -1;
   }
@@ -200,7 +194,7 @@ static void MC_pre_modelcheck_liveness(void)
 
       /* Get enabled processes and insert them in the interleave set of the graph_state */
       for (auto& p : mc_model_checker->process().simix_processes())
-        if (MC_process_is_enabled(&p.copy))
+        if (simgrid::mc::process_is_enabled(&p.copy))
           MC_state_interleave_process(initial_pair->graph_state, &p.copy);
 
       initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state);
@@ -276,13 +270,13 @@ static int MC_modelcheck_liveness_main(void)
              xbt_free(initial_global_state->prev_req);
            }
            initial_global_state->prev_pair = current_pair->num;
-           initial_global_state->prev_req = MC_request_get_dot_output(req, value);
+           initial_global_state->prev_req = simgrid::mc::request_get_dot_output(req, value);
            if (current_pair->search_cycle)
              fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
            fflush(dot_output);
          }
 
-         char* req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX); 
+         char* req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
          XBT_DEBUG("Execute: %s", req_str);
          xbt_free(req_str);
 
@@ -295,7 +289,7 @@ static int MC_modelcheck_liveness_main(void)
            mc_stats->visited_pairs++;
 
          /* Answer the request */
-         MC_simcall_handle(req, value);
+         simgrid::mc::handle_simcall(req, value);
          
          /* Wait for requests (schedules processes) */
          mc_model_checker->wait_for_requests();
@@ -319,7 +313,7 @@ static int MC_modelcheck_liveness_main(void)
               next_pair->depth = current_pair->depth + 1;
               /* Get enabled processes and insert them in the interleave set of the next graph_state */
               for (auto& p : mc_model_checker->process().simix_processes())
-                if (MC_process_is_enabled(&p.copy))
+                if (simgrid::mc::process_is_enabled(&p.copy))
                   MC_state_interleave_process(next_pair->graph_state, &p.copy);
 
               next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
@@ -394,7 +388,7 @@ int MC_modelcheck_liveness(void)
   int res = MC_modelcheck_liveness_main();
 
   /* We're done */
-  xbt_free(mc_time);
+  simgrid::mc::processes_time.clear();
 
   return res;
 }