[mc] Remote support for MC_deadlock_check() using MC_MESSAGE_DEADLOCK_CHECK IPC message

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

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 173c46a..ec50dad 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -27,30 +27,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 +79,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 +101,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 +130,7 @@ static void remove_acceptance_pair(int pair_num) {
 
   }
 
-  if (!raw_mem_set)
-    MC_SET_STD_HEAP;
+  mmalloc_set_current_heap(heap);
 }
 
 
@@ -175,7 +157,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;
@@ -238,12 +220,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;