From: Ehsan Azimi <eazimi@ehsan.irisa.fr>
Date: Fri, 4 Dec 2020 17:18:14 +0000 (+0100)
Subject: mc_api::get_automaton_state() defined. It is called in LivenessChecker::run()
X-Git-Tag: v3.26~13^2~42
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/0d3fb525534744cb1a0f7e0b664dbb3c2791e9cc?hp=46c9742557ba551912d7561aefd807b6acf7440f

mc_api::get_automaton_state() defined. It is called in LivenessChecker::run()
---

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index c47ae66cde..bdebbc26e7 100644
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -320,11 +320,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()) {
diff --git a/src/mc/mc_api.cpp b/src/mc/mc_api.cpp
index 5bda6c5126..34df9cc72f 100644
--- a/src/mc/mc_api.cpp
+++ b/src/mc/mc_api.cpp
@@ -522,5 +522,16 @@ std::vector<int> mc_api::automaton_propositional_symbol_evaluate() const
   return values;
 }
 
+std::vector<xbt_automaton_state_t> mc_api::get_automaton_state() const
+{
+  std::vector<xbt_automaton_state_t> automaton_stack;
+  unsigned int cursor = 0;
+  xbt_automaton_state_t automaton_state;
+  xbt_dynar_foreach (mc::property_automaton->states, cursor, automaton_state)
+    if (automaton_state->type == -1)
+      automaton_stack.push_back(automaton_state);
+  return automaton_stack;
+}
+
 } // namespace mc
 } // namespace simgrid
diff --git a/src/mc/mc_api.hpp b/src/mc/mc_api.hpp
index fc4e15a44c..f6a4526155 100644
--- a/src/mc/mc_api.hpp
+++ b/src/mc/mc_api.hpp
@@ -8,6 +8,7 @@
 #include "src/mc/mc_forward.hpp"
 #include "src/mc/mc_request.hpp"
 #include "src/mc/mc_state.hpp"
+#include "xbt/automaton.hpp"
 #include "xbt/base.h"
 
 namespace simgrid {
@@ -111,6 +112,7 @@ public:
   void automaton_load(const char *file) const;
   #endif
   std::vector<int> automaton_propositional_symbol_evaluate() const;
+  std::vector<xbt_automaton_state_t> get_automaton_state() const;
 };
 
 } // namespace mc