mc_api::compare_automaton_exp_lable() defined. It's called in evaluate_label()

[simgrid.git] / src / mc / checker / LivenessChecker.cpp

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index 274b520..97d14fb 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -54,12 +54,9 @@ static bool evaluate_label(const xbt_automaton_exp_label* l, std::vector<int> co
   case xbt_automaton_exp_label::AUT_NOT:
     return not evaluate_label(l->u.exp_not, values);
   case xbt_automaton_exp_label::AUT_PREDICAT:{
-      unsigned int cursor = 0;
-      xbt_automaton_propositional_symbol_t p = nullptr;
-      xbt_dynar_foreach(simgrid::mc::property_automaton->propositional_symbols, cursor, p) {
-        if (std::strcmp(xbt_automaton_propositional_symbol_get_name(p), l->u.predicat) == 0)
-          return values[cursor] != 0;
-      }
+      auto cursor = mcapi::get().compare_automaton_exp_lable(l, values);
+      if(cursor >= 0)
+        return values[cursor] != 0;
       xbt_die("Missing predicate");
       break;
     }
@@ -270,8 +267,9 @@ std::shared_ptr<Pair> LivenessChecker::create_pair(const Pair* current_pair, xbt
   else
     next_pair->depth = 1;
   /* Get enabled actors and insert them in the interleave set of the next graph_state */
-  for (auto& actor : mc_model_checker->get_remote_simulation().actors())
-    if (mc::actor_is_enabled(actor.copy.get_buffer()))
+  auto actors = mcapi::get().get_actors();
+  for (auto& actor : actors)
+    if (mcapi::get().actor_is_enabled(actor.copy.get_buffer()->get_pid()))
       next_pair->graph_state->add_interleaving_set(actor.copy.get_buffer());
   next_pair->requests = next_pair->graph_state->interleave_size();
   /* FIXME : get search_cycle value for each accepting state */
@@ -319,11 +317,11 @@ void LivenessChecker::run()
 
   // For each initial state of the property automaton, push a
   // (application_state, automaton_state) pair to the exploration stack:
-  unsigned int cursor = 0;
-  xbt_automaton_state_t automaton_state;
-  xbt_dynar_foreach (mc::property_automaton->states, cursor, automaton_state)
+  auto automaton_stack = mcapi::get().get_automaton_state();
+  std::for_each(automaton_stack.begin(), automaton_stack.end(), [&](xbt_automaton_state_t const& automaton_state) {
     if (automaton_state->type == -1)
       exploration_stack_.push_back(this->create_pair(nullptr, automaton_state, propos));
+  });
 
   /* Actually run the double DFS search for counter-examples */
   while (not exploration_stack_.empty()) {