X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/63c087da496454d29883c48e7eec52a392c28ad2..1d254b22ecb6119e7d2c37daee60316a70999242:/src/mc/mc_liveness.c

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 173c46a4e4..4d7c048ec0 100644
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -14,6 +14,7 @@
 #include "mc_liveness.h"
 #include "mc_private.h"
 #include "mc_record.h"
+#include "mc_smx.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
                                 "Logging specific to algorithms for liveness properties verification");
@@ -27,30 +28,22 @@ xbt_parmap_t parmap;
 
 static xbt_dynar_t get_atomic_propositions_values()
 {
-  int res;
-  int_f_void_t f;
   unsigned int cursor = 0;
   xbt_automaton_propositional_symbol_t ps = NULL;
   xbt_dynar_t values = xbt_dynar_new(sizeof(int), NULL);
-
   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps) {
-    f = (int_f_void_t) ps->function;
-    res = f();
+    int res = xbt_automaton_propositional_symbol_evaluate(ps);
     xbt_dynar_push_as(values, int, res);
   }
 
   return values;
 }
 
-
-static mc_visited_pair_t is_reached_acceptance_pair(mc_pair_t pair){
-
-  int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
-  MC_SET_MC_HEAP;
+static mc_visited_pair_t is_reached_acceptance_pair(mc_pair_t pair) {
+  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 
   mc_visited_pair_t new_pair = NULL;
-  new_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state->system_state);
+  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)) {
@@ -87,10 +80,7 @@ static mc_visited_pair_t is_reached_acceptance_pair(mc_pair_t pair){
                 xbt_fifo_shift(mc_stack);
                 if (dot_output != NULL)
                   fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, pair_test->num, initial_global_state->prev_req);
-
-                if (!raw_mem_set)
-                  MC_SET_STD_HEAP;
-
+                mmalloc_set_current_heap(heap);
                 return NULL;
               }
             }
@@ -112,19 +102,13 @@ static mc_visited_pair_t is_reached_acceptance_pair(mc_pair_t pair){
     }
 
   }
-
-  if (!raw_mem_set)
-    MC_SET_STD_HEAP;
-
+  mmalloc_set_current_heap(heap);
   return new_pair;
-
 }
 
-static void remove_acceptance_pair(int pair_num) {
-
-  int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
-  MC_SET_MC_HEAP;
+static void remove_acceptance_pair(int pair_num)
+{
+  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 
   unsigned int cursor = 0;
   mc_visited_pair_t pair_test = NULL;
@@ -147,8 +131,7 @@ static void remove_acceptance_pair(int pair_num) {
 
   }
 
-  if (!raw_mem_set)
-    MC_SET_STD_HEAP;
+  mmalloc_set_current_heap(heap);
 }
 
 
@@ -175,7 +158,7 @@ static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l,
       unsigned int cursor = 0;
       xbt_automaton_propositional_symbol_t p = NULL;
       xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p) {
-        if (strcmp(p->pred, l->u.predicat) == 0)
+        if (strcmp(xbt_automaton_propositional_symbol_get_name(p), l->u.predicat) == 0)
           return (int) xbt_dynar_get_as(atomic_propositions_values, cursor, int);
       }
       return -1;
@@ -219,11 +202,11 @@ void MC_pre_modelcheck_liveness(void) {
       initial_pair->depth = 1;
 
       /* Get enabled processes and insert them in the interleave set of the graph_state */
-      xbt_swag_foreach(process, simix_global->process_list) {
+      MC_EACH_SIMIX_PROCESS(process,
         if (MC_process_is_enabled(process)) {
           MC_state_interleave_process(initial_pair->graph_state, process);
         }
-      }
+      );
 
       initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state);
       initial_pair->search_cycle = 0;
@@ -238,12 +221,10 @@ void MC_pre_modelcheck_liveness(void) {
 
   if (initial_global_state->raw_mem_set)
     MC_SET_MC_HEAP;
-
-
 }
 
-void MC_modelcheck_liveness() {
-
+void MC_modelcheck_liveness()
+{
   smx_process_t process = NULL;
   mc_pair_t current_pair = NULL;
   int value, res, visited_num = -1;
@@ -331,7 +312,7 @@ void MC_modelcheck_liveness() {
            mc_stats->visited_pairs++;
 
          /* Answer the request */
-         SIMIX_simcall_handle(req, value);
+         MC_simcall_handle(req, value);
          
          /* Wait for requests (schedules processes) */
          MC_wait_for_requests();
@@ -356,11 +337,11 @@ void MC_modelcheck_liveness() {
               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 */
-              xbt_swag_foreach(process, simix_global->process_list) {
+              MC_EACH_SIMIX_PROCESS(process,
                 if (MC_process_is_enabled(process)) {
                   MC_state_interleave_process(next_pair->graph_state, process);
                 }
-              }
+              );
 
               next_pair->requests = MC_state_interleave_size(next_pair->graph_state);