mc_api::set_property_automaton(), it is called in run()

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index 97d14fb..77e28d2 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -328,7 +328,7 @@ void LivenessChecker::run()
     std::shared_ptr<Pair> current_pair = exploration_stack_.back();
 
     /* Update current state in buchi automaton */
-    mc::property_automaton->current_state = current_pair->automaton_state;
+    mcapi::get().set_property_automaton(current_pair->automaton_state);
 
     XBT_DEBUG(
         "********************* ( Depth = %d, search_cycle = %d, interleave size = %zu, pair_num = %d, requests = %d)",

diff --git a/src/mc/mc_api.cpp b/src/mc/mc_api.cpp
index c94007f..42f2a6e 100644 (file)
--- a/src/mc/mc_api.cpp
+++ b/src/mc/mc_api.cpp
@@ -544,5 +544,10 @@ int mc_api::compare_automaton_exp_lable(const xbt_automaton_exp_label* l, std::v
   return -1;
 }
 
+void mc_api::set_property_automaton(xbt_automaton_state_t const& automaton_state) const
+{
+  mc::property_automaton->current_state = automaton_state;
+}
+
 } // namespace mc
 } // namespace simgrid

diff --git a/src/mc/mc_api.hpp b/src/mc/mc_api.hpp
index e4ecaea..c8488ef 100644 (file)
--- a/src/mc/mc_api.hpp
+++ b/src/mc/mc_api.hpp
@@ -114,6 +114,7 @@ public:
   std::vector<int> automaton_propositional_symbol_evaluate() const;
   std::vector<xbt_automaton_state_t> get_automaton_state() const;
   int compare_automaton_exp_lable(const xbt_automaton_exp_label* l, std::vector<int> const& values) const;
+  void set_property_automaton(xbt_automaton_state_t const& automaton_state) const;
 };
 
 } // namespace mc