mc_api::automaton_propositional_symbol_evaluate() is used in LivenessChecker::get_pro...

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index 9377785..274b520 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));
 }
 

diff --git a/src/mc/mc_api.cpp b/src/mc/mc_api.cpp
index cbf5bbc..f838048 100644 (file)
--- a/src/mc/mc_api.cpp
+++ b/src/mc/mc_api.cpp
@@ -507,6 +507,16 @@ void mc_api::automaton_load(const char *file) const
 }
 #endif
 
+std::vector<int> mc_api::automaton_propositional_symbol_evaluate() const  
+{
+  unsigned int cursor = 0;
+  std::vector<int> values;    
+  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));
+  return values;
+}
+
 void mc_api::log_state() const
 {
   session->log_state();

diff --git a/src/mc/mc_api.hpp b/src/mc/mc_api.hpp
index 8446162..fc4e15a 100644 (file)
--- a/src/mc/mc_api.hpp
+++ b/src/mc/mc_api.hpp
@@ -106,10 +106,11 @@ public:
   void s_close() const;
   void execute(Transition const& transition) const;
 
-  // Global APIs
+  // AUTOMATION APIs
   #if SIMGRID_HAVE_MC
   void automaton_load(const char *file) const;
   #endif
+  std::vector<int> automaton_propositional_symbol_evaluate() const;
 };
 
 } // namespace mc