mcapi.get_actors() is called in LivenessChecker::create_pair()

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

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index 07a6bb0e7ff84998cddc458922b40dd8d9c7fc44..b14a94de6d51a4c031b9c3bcfd5d5261d019ac5f 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -75,11 +75,7 @@ Pair::Pair(unsigned long expanded_pairs) : num(expanded_pairs)
 
 std::shared_ptr<const std::vector<int>> LivenessChecker::get_proposition_values() const
 {
-  std::vector<int> values;
-  unsigned int cursor = 0;
-  xbt_automaton_propositional_symbol_t ps = nullptr;
-  xbt_dynar_foreach (mc::property_automaton->propositional_symbols, cursor, ps)
-    values.push_back(xbt_automaton_propositional_symbol_evaluate(ps));
+  auto values = mcapi::get().automaton_propositional_symbol_evaluate();  
   return std::make_shared<const std::vector<int>>(std::move(values));
 }
 
@@ -274,8 +270,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)
       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 */
@@ -311,10 +308,10 @@ void LivenessChecker::backtrack()
 void LivenessChecker::run()
 {
   XBT_INFO("Check the liveness property %s", _sg_mc_property_file.get().c_str());
-  MC_automaton_load(_sg_mc_property_file.get().c_str());
+  mcapi::get().automaton_load(_sg_mc_property_file.get().c_str());
 
   XBT_DEBUG("Starting the liveness algorithm");
-  mc::session->initialize();
+  mcapi::get().session_initialize();
 
   /* Initialize */
   this->previous_pair_ = 0;