X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/473ec27e22fce9c0e968524b05e174ef440e21bb..947e36b8b2d9cd9dbdd44170d4cc4b034f4f7a99:/src/mc/LivenessChecker.hpp

diff --git a/src/mc/LivenessChecker.hpp b/src/mc/LivenessChecker.hpp
index 0390a4c8f8..f12c0b3be1 100644
--- a/src/mc/LivenessChecker.hpp
+++ b/src/mc/LivenessChecker.hpp
@@ -29,8 +29,6 @@ SG_END_DECL()
 namespace simgrid {
 namespace mc {
 
-extern XBT_PRIVATE xbt_automaton_t property_automaton;
-
 struct XBT_PRIVATE Pair {
   int num = 0;
   bool search_cycle = false;
@@ -51,7 +49,6 @@ struct XBT_PRIVATE Pair {
 struct XBT_PRIVATE VisitedPair {
   int num = 0;
   int other_num = 0; /* Dot output for */
-  int acceptance_pair = 0;
   std::shared_ptr<simgrid::mc::State> graph_state = nullptr; /* System state included */
   xbt_automaton_state_t automaton_state = nullptr;
   std::vector<int> atomic_propositions;
@@ -82,9 +79,13 @@ private:
   void showAcceptanceCycle(std::size_t depth);
   void replay();
   void removeAcceptancePair(int pair_num);
+  void purgeVisitedPairs();
+  void backtrack();
+  std::shared_ptr<Pair> newPair(Pair* pair, xbt_automaton_state_t state);
 public:
+  // A stack of (application_state, automaton_state) pairs for DFS exploration:
+  std::list<std::shared_ptr<Pair>> explorationStack_;
   std::list<std::shared_ptr<VisitedPair>> acceptancePairs_;
-  std::list<Pair*> livenessStack_;
   std::list<std::shared_ptr<VisitedPair>> visitedPairs_;
 };