X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/ba9a4cfeba4eb00e84cd17603fc9654e81445655..e6ca184e99d50d0ee8fe405a83ee5277e2ecfce6:/src/mc/mc_liveness.cpp

diff --git a/src/mc/mc_liveness.cpp b/src/mc/mc_liveness.cpp
index 84e996d784..fbea394d25 100644
--- 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;
   }
@@ -178,10 +172,7 @@ static int MC_modelcheck_liveness_main(void);
 static void MC_pre_modelcheck_liveness(void)
 {
   mc_pair_t initial_pair = nullptr;
-  smx_process_t process;
-
   mc_model_checker->wait_for_requests();
-
   acceptance_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), nullptr);
   if(_sg_mc_visited > 0)
     visited_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), nullptr);
@@ -202,11 +193,9 @@ static void MC_pre_modelcheck_liveness(void)
       initial_pair->depth = 1;
 
       /* Get enabled processes and insert them in the interleave set of the graph_state */
-      MC_EACH_SIMIX_PROCESS(process,
-        if (MC_process_is_enabled(process)) {
-          MC_state_interleave_process(initial_pair->graph_state, process);
-        }
-      );
+      for (auto& p : mc_model_checker->process().simix_processes())
+        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);
       initial_pair->search_cycle = 0;
@@ -218,7 +207,6 @@ static void MC_pre_modelcheck_liveness(void)
 
 static int MC_modelcheck_liveness_main(void)
 {
-  smx_process_t process = nullptr;
   mc_pair_t current_pair = nullptr;
   int value, res, visited_num = -1;
   smx_simcall_t req = nullptr;
@@ -282,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);
 
@@ -301,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();
@@ -324,11 +312,9 @@ static int MC_modelcheck_liveness_main(void)
               next_pair->atomic_propositions = get_atomic_propositions_values();
               next_pair->depth = current_pair->depth + 1;
               /* Get enabled processes and insert them in the interleave set of the next graph_state */
-              MC_EACH_SIMIX_PROCESS(process,
-                if (MC_process_is_enabled(process)) {
-                  MC_state_interleave_process(next_pair->graph_state, process);
-                }
-              );
+              for (auto& p : mc_model_checker->process().simix_processes())
+                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);
 
@@ -402,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;
 }