Merge lp:~tapaal-ltl/verifypn/resumable-suc-generator into lp:~tapaal-ltl/verifypn/ltl_model_checker

[Simon Virenfeldt]

Merge branch resumable_suc_generator

[lp:~tapaal-ltl/verifypn/resumable-suc-generator]

262. By Simon Virenfeldt on 2020-11-09

Removed some commented code lines

263. By Simon Virenfeldt on 2020-11-09

Merge remote

[Simon Virenfeldt (simwir)]

review: Approve

=== modified file 'CMakeLists.txt'
--- CMakeLists.txt	2020-10-19 11:13:27 +0000
+++ CMakeLists.txt	2020-11-09 13:59:57 +0000
@@ -29,7 +29,7 @@
 endif()
 
 if (CMAKE_BUILD_TYPE MATCHES Debug)
-    #add_compile_definitions(PRINTF_DEBUG)
+    add_compile_definitions(PRINTF_DEBUG)
 endif()
 
 if (VERIFYPN_Static)
@@ -59,7 +59,7 @@
 endif ()
 
 set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -Wall -pedantic-errors -O3 -DNDEBUG")
-set(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS_DEBUG} -O0 -fno-omit-frame-pointer -fsanitize=address ")
+set(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS_DEBUG} -O0 -fno-omit-frame-pointer")
 set(CMAKE_EXE_LINKER_FLAGS_RELEASE "${CMAKE_EXE_LINKER_FLAGS_RELEASE} -O3 -DNDEBUG")
 if (VERIFYPN_Static AND NOT APPLE)
     set(CMAKE_EXE_LINKER_FLAGS_RELEASE "${CMAKE_EXE_LINKER_FLAGS_RELEASE} -static")
 
=== modified file 'include/LTL/BuchiSuccessorGenerator.h'
--- include/LTL/BuchiSuccessorGenerator.h	2020-10-05 10:15:17 +0000
+++ include/LTL/BuchiSuccessorGenerator.h	2020-11-09 13:59:57 +0000
@@ -18,7 +18,7 @@
 namespace LTL {
     class BuchiSuccessorGenerator {
     public:
-        BuchiSuccessorGenerator(Structures::BuchiAutomaton automaton)
+        explicit BuchiSuccessorGenerator(Structures::BuchiAutomaton automaton)
                 : aut(std::move(automaton)) {
         }
 
@@ -31,7 +31,7 @@
         bool next(size_t &state, bdd &cond) {
             if (!succ->done()) {
                 state = aut.buchi->state_number(succ->dst());
-#ifdef PRINTF_DEBUG
+#ifdef _PRINTF_DEBUG
                 std::cerr << "buchi state " << state << std::endl;
 #endif
                 cond = succ->cond();
 
=== modified file 'include/LTL/LTL_algorithm/ModelChecker.h'
--- include/LTL/LTL_algorithm/ModelChecker.h	2020-10-16 11:34:00 +0000
+++ include/LTL/LTL_algorithm/ModelChecker.h	2020-11-09 13:59:57 +0000
@@ -20,6 +20,8 @@
         std::unique_ptr<ProductSuccessorGenerator> successorGenerator;
         const PetriEngine::PetriNet &net;
         PetriEngine::PQL::Condition_ptr formula;
+
+        size_t _discovered = 0;
     };
 }
 
 
=== modified file 'include/LTL/LTL_algorithm/NestedDepthFirstSearch.h'
--- include/LTL/LTL_algorithm/NestedDepthFirstSearch.h	2020-10-05 10:15:17 +0000
+++ include/LTL/LTL_algorithm/NestedDepthFirstSearch.h	2020-11-09 13:59:57 +0000
@@ -12,6 +12,7 @@
 #include "LTL/Structures/ProductStateFactory.h"
 
 #include <ptrie/ptrie_stable.h>
+#include <unordered_set>
 
 using namespace PetriEngine;
 
@@ -20,7 +21,7 @@
     public:
         NestedDepthFirstSearch(const PetriNet &net, PetriEngine::PQL::Condition_ptr ptr)
                 : ModelChecker(net, ptr), factory{net, successorGenerator->initial_buchi_state()},
-                  mark1(net, 0, (int)net.numberOfPlaces() + 1), mark2(net, 0, (int)net.numberOfPlaces() + 1) {}
+                states(net, 0, (int)net.numberOfPlaces() + 1) {}
 
         bool isSatisfied() override;
 
@@ -28,9 +29,14 @@
         using State = LTL::Structures::ProductState;
 
         Structures::ProductStateFactory factory;
-        PetriEngine::Structures::StateSet mark1;
-        PetriEngine::Structures::StateSet mark2;
+        PetriEngine::Structures::StateSet states;
+        std::set<size_t> mark1;
+        std::set<size_t> mark2;
 
+        struct StackEntry {
+            size_t id;
+            successor_info sucinfo;
+        };
 
         State *seed;
         bool violation = false;
 
=== modified file 'include/LTL/LTL_algorithm/TarjanModelChecker.h'
--- include/LTL/LTL_algorithm/TarjanModelChecker.h	2020-10-19 12:35:11 +0000
+++ include/LTL/LTL_algorithm/TarjanModelChecker.h	2020-11-09 13:59:57 +0000
@@ -18,10 +18,11 @@
 
 namespace LTL {
 
+    template <bool SaveTrace>
     class TarjanModelChecker : public ModelChecker {
     public:
         TarjanModelChecker(const PetriEngine::PetriNet &net, const Condition_ptr &cond)
-                : ModelChecker(net, cond), successorGenerator(net, cond), factory(net, successorGenerator.initial_buchi_state()),
+                : ModelChecker(net, cond), factory(net, successorGenerator->initial_buchi_state()),
                   seen(net, 0, (int) net.numberOfPlaces() + 1) {
             chash.fill(std::numeric_limits<idx_t>::max());
         }
@@ -31,45 +32,46 @@
     private:
         using State = LTL::Structures::ProductState;
         using idx_t = size_t;
+        static constexpr idx_t HashSz = 4096;
 
-        LTL::ProductSuccessorGenerator successorGenerator;
         LTL::Structures::ProductStateFactory factory;
 
         PetriEngine::Structures::StateSet seen;
         std::unordered_set<idx_t> store;
-        //PetriEngine::Structures::StateSet store;
 
-        static constexpr idx_t HashSz = 4096;
         std::array<idx_t, HashSz> chash;
-        inline idx_t hash_search(idx_t stateid) {
-            idx_t idx = chash[hash(stateid)];
-            while (idx != stateid && idx != std::numeric_limits<idx_t>::max()) {
-                idx = cstack[idx].next;
-            }
-            return idx;
-        }
 
-        inline idx_t hash(idx_t id) {
+        static inline idx_t hash(idx_t id) {
             return id % HashSz;
         }
 
-        struct CStack {
+        struct PlainCEntry {
             size_t lowlink;
             size_t stateid;
             size_t next = std::numeric_limits<idx_t>::max();
 
-            CStack(size_t lowlink, size_t stateid, size_t next) : lowlink(lowlink), stateid(stateid), next(next) {}
-        };
-
-        struct DStack {
+            PlainCEntry(size_t lowlink, size_t stateid, size_t next) : lowlink(lowlink), stateid(stateid), next(next) {}
+        };
+
+        struct TracableCEntry : PlainCEntry {
+            idx_t lowsource = std::numeric_limits<size_t>::max();
+            uint32_t sourcetrans;
+
+            TracableCEntry(size_t lowlink, size_t stateid, size_t next) : PlainCEntry(lowlink, stateid, next) {}
+        };
+
+        using CEntry = std::conditional_t<SaveTrace,
+            TracableCEntry,
+            PlainCEntry>;
+
+        struct DEntry {
             size_t pos;
-            uint32_t nexttrans = -1;
-            std::optional<std::vector<size_t>> neighbors;
+            successor_info sucinfo;
         };
 
 
-        std::vector<CStack> cstack;
-        std::stack<DStack> dstack;
+        std::vector<CEntry> cstack;
+        std::stack<DEntry> dstack;
         std::stack<idx_t> astack;
         bool violation = false;
 
@@ -79,8 +81,10 @@
 
         void update(idx_t to);
 
-        bool nexttrans(State &state, DStack &delem);
+        bool nexttrans(State &state, State& parent, DEntry &delem);
     };
+extern template class TarjanModelChecker<true>;
+extern template class TarjanModelChecker<false>;
 }
 
 #endif //VERIFYPN_TARJANMODELCHECKER_H
 
=== modified file 'include/LTL/ProductSuccessorGenerator.h'
--- include/LTL/ProductSuccessorGenerator.h	2020-10-16 11:20:30 +0000
+++ include/LTL/ProductSuccessorGenerator.h	2020-11-09 13:59:57 +0000
@@ -11,13 +11,63 @@
 #include "LTL/BuchiSuccessorGenerator.h"
 #include "LTL/LTLToBuchi.h"
 
+
 namespace LTL {
+    /**
+     * type holding sufficient information to resume successor generation for a state from a given point.
+     */
+    struct successor_info {
+        uint32_t pcounter;
+        uint32_t tcounter;
+        size_t buchi_state;
+        size_t last_state;
+
+        friend bool operator==(const successor_info &lhs, const successor_info &rhs) {
+            return lhs.pcounter == rhs.pcounter &&
+                   lhs.tcounter == rhs.tcounter &&
+                   lhs.buchi_state == rhs.buchi_state &&
+                   lhs.last_state == rhs.last_state;
+        }
+
+        friend bool operator!=(const successor_info &lhs, const successor_info &rhs) {
+            return !(rhs == lhs);
+        }
+
+        inline bool has_pcounter() const {
+            return pcounter != NoPCounter;
+        }
+
+        inline bool has_tcounter() const {
+            return tcounter != NoTCounter;
+        }
+
+        inline bool has_buchistate() const {
+            return buchi_state != NoBuchiState;
+        }
+
+        inline bool has_prev_state() const {
+            return last_state != NoLastState;
+        }
+
+        static constexpr auto NoPCounter = 0;
+        static constexpr auto NoTCounter = std::numeric_limits<uint32_t>::max();
+        static constexpr auto NoBuchiState = std::numeric_limits<size_t>::max();
+        static constexpr auto NoLastState = std::numeric_limits<size_t>::max();
+    };
+
+    constexpr successor_info initial_suc_info{
+            successor_info::NoPCounter,
+            successor_info::NoTCounter,
+            successor_info::NoBuchiState,
+            successor_info::NoLastState
+    };
+
     class ProductSuccessorGenerator : public PetriEngine::SuccessorGenerator {
     public:
+
         ProductSuccessorGenerator(const PetriEngine::PetriNet &net,
-                                  const PetriEngine::PQL::Condition_ptr& cond)
-                                  : PetriEngine::SuccessorGenerator(net), buchi(makeBuchiAutomaton(cond))
-        {}
+                                  const PetriEngine::PQL::Condition_ptr &cond)
+                : PetriEngine::SuccessorGenerator(net), buchi(makeBuchiAutomaton(cond)) {}
 
         [[nodiscard]] size_t initial_buchi_state() const { return buchi.initial_state_number(); };
 
@@ -43,8 +93,21 @@
             }
         }
 
-    protected:
-        bool next(LTL::Structures::ProductState &write, uint32_t &tindex);
+        /**
+         * prepare a state for successor generation, starting from specific point in iteration
+         * @param state the source state to generate successors from
+         * @param sucinfo the point in the iteration to start from, as returned by `next`.
+         */
+        void prepare(const LTL::Structures::ProductState *state, const successor_info &sucinfo);
+
+        /**
+         * compute the next successor from the last state that was sent to `prepare`.
+         * @param[out] state the state to write
+         * @param[out] sucinfo checkpoint information from which iteration can later be resumed.
+         * @return `true` if a successor was successfully generated, `false` otherwise.
+         * @warning do not use the same State for both prepare and next, this will cause wildly incorrect behaviour!
+         */
+        bool next(Structures::ProductState &state, successor_info &sucinfo);
 
     private:
         BuchiSuccessorGenerator buchi;
 
=== modified file 'include/LTL/Structures/ProductState.h'
--- include/LTL/Structures/ProductState.h	2020-10-16 11:20:30 +0000
+++ include/LTL/Structures/ProductState.h	2020-11-09 13:59:57 +0000
@@ -48,6 +48,8 @@
                    getBuchiState() == rhs.getBuchiState();*/
         }
 
+        size_t size() const { return buchi_state_idx + 1; }
+
         bool operator!=(const ProductState &rhs) const {
             return !(rhs == *this);
         }
 
=== modified file 'include/PetriEngine/PQL/Expressions.h'
--- include/PetriEngine/PQL/Expressions.h	2020-09-23 12:26:04 +0000
+++ include/PetriEngine/PQL/Expressions.h	2020-11-09 13:59:57 +0000
@@ -533,7 +533,7 @@
                 // TODO implement
                 assert(false); std::cerr << "TODO implement" << std::endl; exit(0);
             }
-            bool containsNext() const override { return true; }
+            bool containsNext() const override { return _cond->containsNext(); }
             virtual bool isLoopSensitive() const override { return true; }
             void visit(Visitor&) const override;
         private:
@@ -569,7 +569,7 @@
                 // TODO implement
                 assert(false); std::cerr << "TODO implement" << std::endl; exit(0);
             }
-            bool containsNext() const override { return true; }
+            bool containsNext() const override { return _cond->containsNext(); }
             virtual bool isLoopSensitive() const override { return true; }
             void visit(Visitor&) const override;
         private:
 
=== modified file 'include/PetriEngine/SuccessorGenerator.h'
--- include/PetriEngine/SuccessorGenerator.h	2020-10-16 11:20:30 +0000
+++ include/PetriEngine/SuccessorGenerator.h	2020-11-09 13:59:57 +0000
@@ -60,16 +60,20 @@
      */
     void producePostset(Structures::State& write, uint32_t t);
 
+    size_t last_transition() const { return _suc_tcounter == std::numeric_limits<uint32_t>::max() ? std::numeric_limits<uint32_t>::max() : _suc_tcounter - 1; }
+
 protected:
     const PetriNet& _net;
 
     bool next(Structures::State &write, uint32_t &tindex);
 
     const Structures::State* _parent;
-private:
+
     uint32_t _suc_pcounter;
     uint32_t _suc_tcounter;
 
+private:
+
     friend class ReducingSuccessorGenerator;
 
 };
 
=== modified file 'src/LTL/LTL_algorithm/LTLToBuchi.cpp'
--- src/LTL/LTL_algorithm/LTLToBuchi.cpp	2020-10-16 11:20:30 +0000
+++ src/LTL/LTL_algorithm/LTLToBuchi.cpp	2020-11-09 13:59:57 +0000
@@ -29,8 +29,6 @@
 
         void _accept(const PetriEngine::PQL::OrCondition *element) override;
 
-        //void _accept(const PetriEngine::PQL::CompareConjunction *element) override;
-
         void _accept(const PetriEngine::PQL::LessThanCondition *element) override;
 
         void _accept(const PetriEngine::PQL::LessThanOrEqualCondition *element) override;
@@ -63,7 +61,7 @@
 
     public:
 
-        FormulaToSpotSyntax(std::ostream &os = std::cout)
+        explicit FormulaToSpotSyntax(std::ostream &os = std::cout)
                 : PetriEngine::PQL::QueryPrinter(os) {}
 
         auto begin() const {
@@ -147,88 +145,76 @@
 
     void FormulaToSpotSyntax::_accept(const PetriEngine::PQL::LiteralExpr *element) {
         assert(false);
-        std::cerr << "LiteralExpr should not be visited by Spot serialiezr" << std::endl;
+        std::cerr << "LiteralExpr should not be visited by Spot serializer" << std::endl;
         exit(1);
         //make_atomic_prop(element->shared_from_this());
     }
 
     void FormulaToSpotSyntax::_accept(const PetriEngine::PQL::PlusExpr *element) {
         assert(false);
-        std::cerr << "PlusExpr should not be visited by Spot serialiezr" << std::endl;
+        std::cerr << "PlusExpr should not be visited by Spot serializer" << std::endl;
         exit(1);
         //make_atomic_prop(element->shared_from_this());
     }
 
     void FormulaToSpotSyntax::_accept(const PetriEngine::PQL::MultiplyExpr *element) {
         assert(false);
-        std::cerr << "MultiplyExpr should not be visited by Spot serialiezr" << std::endl;
+        std::cerr << "MultiplyExpr should not be visited by Spot serializer" << std::endl;
         exit(1);
         //make_atomic_prop(element->shared_from_this());
     }
 
     void FormulaToSpotSyntax::_accept(const PetriEngine::PQL::MinusExpr *element) {
         assert(false);
-        std::cerr << "MinusExpr should not be visited by Spot serialiezr" << std::endl;
+        std::cerr << "MinusExpr should not be visited by Spot serializer" << std::endl;
         exit(1);
         //make_atomic_prop(element->shared_from_this());
     }
 
     void FormulaToSpotSyntax::_accept(const PetriEngine::PQL::SubtractExpr *element) {
         assert(false);
-        std::cerr << "LiteralExpr should not be visited by Spot serialiezr" << std::endl;
+        std::cerr << "LiteralExpr should not be visited by Spot serializer" << std::endl;
         exit(1);
         //make_atomic_prop(element->shared_from_this());
     }
 
     void FormulaToSpotSyntax::_accept(const PetriEngine::PQL::IdentifierExpr *element) {
         assert(false);
-        std::cerr << "IdentifierExpr should not be visited by Spot serialiezr" << std::endl;
+        std::cerr << "IdentifierExpr should not be visited by Spot serializer" << std::endl;
         exit(1);
         //make_atomic_prop(element->shared_from_this());
     }
 
-
-    std::string toSpotFormat(const QueryItem &query) {
-        std::stringstream ss;
-        toSpotFormat(query, ss);
-        return ss.str();
-    }
-
-    void toSpotFormat(const QueryItem &query, std::ostream &os) {
-        FormulaToSpotSyntax spotConverter{os};
-        // FIXME nasty hack for top-level query, should be fixed elsewhere (e.g. asLTL)
-        auto top_quant = dynamic_cast<SimpleQuantifierCondition *>(query.query.get());
-        (*top_quant)[0]->visit(spotConverter);
-    }
-
     BuchiSuccessorGenerator makeBuchiAutomaton(const Condition_ptr &query) {
         std::stringstream ss;
         FormulaToSpotSyntax spotConverter{ss};
         query->visit(spotConverter);
-
         const std::string spotFormula = "!(" + ss.str() + ")";
 #ifdef PRINTF_DEBUG
         std::cerr << "ORIG FORMULA: \n  " << ss.str() << std::endl;
         std::cerr << "SPOT FORMULA: \n  " << spotFormula << std::endl;
 #endif
         spot::formula formula = spot::parse_formula(spotFormula);
-        spot::bdd_dict_ptr bdd = spot::make_bdd_dict();
-        auto translator = spot::translator(bdd);
-        translator.set_pref(spot::postprocessor::Complete
-                            | spot::postprocessor::SBAcc);
+        spot::translator translator;
+        translator.set_type(spot::postprocessor::BA);
+        translator.set_pref(spot::postprocessor::Complete);
         spot::twa_graph_ptr automaton = translator.run(formula);
 #ifdef PRINTF_DEBUG
         automaton->get_graph().dump_storage(std::cerr);
         spot::print_dot(std::cerr, automaton);
-        bdd->dump(std::cerr);
 #endif
         std::unordered_map<int, AtomicProposition> ap_map;
+        // bind PQL expressions to the atomic proposition IDs used by spot.
+        // the resulting map can be indexed using variables mentioned on edges of the created Büchi automaton.
         for (const auto &apinfo : spotConverter) {
             int varnum = automaton->register_ap(apinfo.text);
             ap_map[varnum] = apinfo;
         }
+#ifdef PRINTF_DEBUG
+        automaton->get_dict()->dump(std::cerr);
+#endif
 
-        return BuchiSuccessorGenerator{Structures::BuchiAutomaton{automaton, ap_map}};
+        return BuchiSuccessorGenerator{Structures::BuchiAutomaton{std::move(automaton), std::move(ap_map)}};
     }
 
-}
 \ No newline at end of file
+}
 
=== modified file 'src/LTL/LTL_algorithm/NestedDepthFirstSearch.cpp'
--- src/LTL/LTL_algorithm/NestedDepthFirstSearch.cpp	2020-10-19 12:35:11 +0000
+++ src/LTL/LTL_algorithm/NestedDepthFirstSearch.cpp	2020-11-09 13:59:57 +0000
@@ -20,100 +20,106 @@
 
     bool NestedDepthFirstSearch::isSatisfied() {
         dfs();
+#ifdef _PRINTF_DEBUG
+        std::cout << "discovered " << _discovered << " states." << std::endl;
+        std::cout << "mark1 size: " << mark1.size() << "\tmark2 size: " << mark2.size() << std::endl;
+#endif
         return !violation;
     }
 
     void NestedDepthFirstSearch::dfs() {
         std::stack<size_t> call_stack;
-
-        PetriEngine::Structures::StateSet states{net,0, (int)net.numberOfPlaces() + 1};
-        PetriEngine::Structures::DFSQueue todo{&states};
+        std::stack<StackEntry> todo;
 
         State working = factory.newState();
-        PQL::DistanceContext ctx{&net, working.marking()};
         State curState = factory.newState();
+
         {
             std::vector<State> initial_states;
             successorGenerator->makeInitialState(initial_states);
             for (auto &state : initial_states) {
                 auto res = states.add(state);
                 assert(res.first);
-                todo.push(res.second, ctx, formula);
+                todo.push(StackEntry{res.second, initial_suc_info});
+                _discovered++;
             }
         }
 
-        while (todo.top(curState)) {
-
-            if (!call_stack.empty() && states.lookup(curState).second == call_stack.top()) {
+        while (!todo.empty()) {
+            auto &top = todo.top();
+            states.decode(curState, top.id);
+            successorGenerator->prepare(&curState, top.sucinfo);
+            if (top.sucinfo.has_prev_state()) {
+                states.decode(working, top.sucinfo.last_state);
+            }
+            if (!successorGenerator->next(working, top.sucinfo)) {
+                // no successor
+                todo.pop();
                 if (successorGenerator->isAccepting(curState)) {
                     seed = &curState;
                     ndfs(curState);
-                    if (violation)
-                        return;
+                    if (violation) return;
                 }
-                todo.pop(curState);
-                call_stack.pop();
             } else {
-                call_stack.push(states.add(curState).second);
-                if (!mark1.add(curState).first) {
-                    continue;
-                }
-                successorGenerator->prepare(&curState);
-#ifdef PRINTF_DEBUG
-                std::cerr << "curState:\n";
-                dump_state(curState);
-#endif
-                while (successorGenerator->next(working)) {
-#ifdef PRINTF_DEBUG
-                    std::cerr << "working:\n";
-                    dump_state(working);
-#endif
-                    auto r = states.add(working);
-                    todo.push(r.second, ctx, formula);
+#ifdef PRINTF_DEBUG
+                dump_state(working);
+#endif
+                auto[_, stateid] = states.add(working);
+                auto[it, is_new] = mark1.insert(stateid);
+                top.sucinfo.last_state = stateid;
+                if (is_new) {
+                    _discovered++;
+                    todo.push(StackEntry{stateid, initial_suc_info});
                 }
             }
         }
     }
 
 
-    void NestedDepthFirstSearch::ndfs(State& state) {
-        PetriEngine::Structures::StateSet states{net, 0, (int)net.numberOfPlaces() + 1};
-        PetriEngine::Structures::DFSQueue todo{&states};
+    void NestedDepthFirstSearch::ndfs(State &state) {
+#ifdef PRINTF_DEBUG
+        std::cerr << "ENTERING NDFS" << std::endl;
+#endif
+        std::stack<StackEntry> todo;
 
         State working = factory.newState();
         State curState = factory.newState();
 
-        PQL::DistanceContext ctx{&net, state.marking()};
-
-        todo.push(states.add(state).second, ctx, formula);
-
-        while (todo.pop(curState)) {
-            if (!mark2.add(curState).first) {
-                continue;
+        todo.push(StackEntry{states.add(state).second, initial_suc_info});
+
+        while (!todo.empty()) {
+            auto &top = todo.top();
+            states.decode(curState, top.id);
+            successorGenerator->prepare(&curState, top.sucinfo);
+            if (top.sucinfo.has_prev_state()) {
+                states.decode(working, top.sucinfo.last_state);
             }
-
-            successorGenerator->prepare(&curState);
-#ifdef PRINTF_DEBUG
-            std::cerr << "curState:\n";
-            dump_state(curState);
-#endif
-            while (successorGenerator->next(working)) {
-#ifdef PRINTF_DEBUG
-                std::cerr << "working:\n";
+            if (!successorGenerator->next(working, top.sucinfo)) {
+                todo.pop();
+            } else {
+#ifdef PRINTF_DEBUG
                 dump_state(working);
 #endif
                 if (working == *seed) {
-#ifdef PRINTF_DEBUG
+#ifdef _PRINTF_DEBUG
                     std::cerr << "seed:\n  "; dump_state(*seed);
                     std::cerr << "working:\n  "; dump_state(working);
 #endif
                     violation = true;
                     return;
                 }
-                auto r = states.add(working);
-                todo.push(r.second, ctx, formula);
+                auto[_, stateid] = states.add(working);
+                auto[it, is_new] = mark2.insert(stateid);
+                top.sucinfo.last_state = stateid;
+                if (is_new) {
+                    _discovered++;
+                    todo.push(StackEntry{stateid, initial_suc_info});
+                }
+
             }
         }
-
+#ifdef PRINTF_DEBUG
+        std::cerr << "LEAVING NDFS" << std::endl;
+#endif
     }
 }
 \ No newline at end of file
 
=== modified file 'src/LTL/LTL_algorithm/ProductSuccessorGenerator.cpp'
--- src/LTL/LTL_algorithm/ProductSuccessorGenerator.cpp	2020-10-16 11:20:30 +0000
+++ src/LTL/LTL_algorithm/ProductSuccessorGenerator.cpp	2020-11-09 13:59:57 +0000
@@ -29,6 +29,27 @@
         fresh_marking = true;
     }
 
+    void ProductSuccessorGenerator::prepare(const LTL::Structures::ProductState *state, const successor_info &sucinfo) {
+        SuccessorGenerator::prepare(state);
+        buchi.prepare(state->getBuchiState());
+        buchi_parent = state->getBuchiState();
+        fresh_marking = sucinfo.pcounter == 0 && sucinfo.tcounter == std::numeric_limits<uint32_t>::max();
+        _suc_pcounter = sucinfo.pcounter;
+        _suc_tcounter = sucinfo.tcounter;
+        if (!fresh_marking) {
+            assert(sucinfo.buchi_state != std::numeric_limits<size_t>::max());
+            // spool Büchi successors until last state found.
+            // TODO is there perhaps a good way to avoid this, perhaps using raw edge vector?
+            // Caveat: it seems like there usually are not that many successors, so this is probably cheap regardless
+            size_t tmp;
+            while (buchi.next(tmp, cond)) {
+                if (tmp == sucinfo.buchi_state) {
+                    break;
+                }
+            }
+        }
+    }
+
     bool ProductSuccessorGenerator::next(LTL::Structures::ProductState &state) {
         if (fresh_marking) {
             fresh_marking = false;
@@ -75,14 +96,16 @@
 
     bool ProductSuccessorGenerator::guard_valid(const PetriEngine::Structures::State &state, bdd bdd) {
         EvaluationContext ctx{state.marking(), &_net};
-        while (!(bdd == bddtrue || bdd == bddfalse)) {
+        // IDs 0 and 1 are false and true atoms, respectively
+        while (bdd.id() > 1/*!(bdd == bddtrue || bdd == bddfalse)*/) {
+            // find variable to test, and test it
             size_t var = bdd_var(bdd);
             Condition::Result res = buchi.getExpression(var)->evaluate(ctx);
             switch (res) {
                 case Condition::RUNKNOWN:
                     std::cerr << "Unexpected unknown answer from evaluating query!\n";
                     assert(false);
-                    exit(0);
+                    exit(1);
                     break;
                 case Condition::RFALSE:
                     bdd = bdd_low(bdd);
@@ -95,23 +118,33 @@
         return bdd == bddtrue;
     }
 
-    bool ProductSuccessorGenerator::next(Structures::ProductState &state, uint32_t &tindex) {
+    bool ProductSuccessorGenerator::next(Structures::ProductState &state, successor_info &sucinfo) {
+        auto update_sucinfo = [&]() {
+            sucinfo.pcounter = _suc_pcounter;
+            sucinfo.tcounter = _suc_tcounter;
+            sucinfo.buchi_state = state.getBuchiState();
+        };
+
         if (fresh_marking) {
             fresh_marking = false;
-            if (!SuccessorGenerator::next(state, tindex)) {
-                // This is a fresh marking, so if there is no more successors for the state the state is deadlocked.
+            if (!SuccessorGenerator::next(state)) {
+                // This is a fresh marking, so if there are no more successors for the state the state is deadlocked.
                 // The semantics for deadlock is to just loop the marking so return true without changing the value of state.
-                // This assumes SuccessorGenerator::next only modifies &state if there is a successor.
+                std::copy(_parent->marking(), _parent->marking() + state.buchi_state_idx + 1, state.marking());
             }
         }
         if (next_buchi_succ(state)) {
+            update_sucinfo();
             return true;
         }
-            // No valid transition in Büchi automaton for current marking;
-            // Try next marking(s) and see if we find a successor.
+        // No valid transition in Büchi automaton for current marking;
+        // Try next marking(s) and see if we find a successor.
         else {
-            while (SuccessorGenerator::next(state, tindex)) {
+            while (SuccessorGenerator::next(state)) {
+                // reset buchi successors
+                buchi.prepare(buchi_parent);
                 if (next_buchi_succ(state)) {
+                    update_sucinfo();
                     return true;
                 }
             }
 
=== modified file 'src/LTL/LTL_algorithm/TarjanModelChecker.cpp'
--- src/LTL/LTL_algorithm/TarjanModelChecker.cpp	2020-10-19 12:35:11 +0000
+++ src/LTL/LTL_algorithm/TarjanModelChecker.cpp	2020-11-09 13:59:57 +0000
@@ -7,72 +7,123 @@
 
 #include "LTL/LTL_algorithm/TarjanModelChecker.h"
 
+#undef PRINTF_DEBUG
 namespace LTL {
 
-
-#ifdef PRINTF_DEBUG
-
-    inline void _dump_state(const LTL::Structures::ProductState &state, int nplaces = -1) {
-        if (nplaces == -1) nplaces = state.buchi_state_idx;
+    inline void _dump_state(const LTL::Structures::ProductState &state) {
         std::cerr << "marking: ";
         std::cerr << state.marking()[0];
-        for (int i = 1; i <= nplaces; ++i) {
+        for (int i = 1; i < state.size(); ++i) {
             std::cerr << ", " << state.marking()[i];
         }
         std::cerr << std::endl;
     }
 
-#endif
-
-    bool LTL::TarjanModelChecker::isSatisfied() {
-        {
-            std::vector<State> initial_states;
-            successorGenerator.makeInitialState(initial_states);
-            for (auto &state : initial_states) {
-                seen.add(state);
+    template<bool SaveTrace>
+    bool TarjanModelChecker<SaveTrace>::isSatisfied() {
+        std::vector<State> initial_states;
+        successorGenerator->makeInitialState(initial_states);
+        State working = factory.newState();
+        State parent = factory.newState();
+        for (auto &state : initial_states) {
+            auto res = seen.add(state);
+            if (res.first) {
                 push(state);
             }
-        }
-        State working = factory.newState();
-        while (!dstack.empty() && !violation) {
-            DStack &dtop = dstack.top();
-            if (!nexttrans(working, dtop)) {
-                pop();
-                continue;
-            }
-            // get ID of transition taken (nexttrans = lasttrans + 1)
-            idx_t stateid = (*dtop.neighbors)[dtop.nexttrans - 1];
-
-            // lookup successor in 'hash' table
-            auto p = chash[hash(stateid)];
-            while (p != std::numeric_limits<idx_t>::max() && cstack[p].stateid != stateid) {
-                p = cstack[p].next;
-            }
-            if (p != std::numeric_limits<idx_t>::max()) {
-                // we found the successor! update lowlinks etc
-                update(p);
-                continue;
-            }
-            if (store.find(stateid) == std::end(store)) {
-                push(working);
+            while (!dstack.empty() && !violation) {
+                DEntry &dtop = dstack.top();
+                if (!nexttrans(working, parent, dtop)) {
+                    pop();
+                    continue;
+                }
+                idx_t stateid = seen.add(working).second;
+                dtop.sucinfo.last_state = stateid;
+
+                // lookup successor in 'hash' table
+                auto p = chash[hash(stateid)];
+                while (p != std::numeric_limits<idx_t>::max() && cstack[p].stateid != stateid) {
+                    p = cstack[p].next;
+                }
+                if (p != std::numeric_limits<idx_t>::max()) {
+                    // we found the successor, i.e. there's a loop!
+                    // now update lowlinks and check whether the loop contains an accepting state
+                    update(p);
+                    continue;
+                }
+                if (store.find(stateid) == std::end(store)) {
+                    push(working);
+                }
+            }
+            if constexpr (SaveTrace) {
+                if (violation) {
+                    State next = factory.newState();
+                    std::cerr << "Printing trace: " << std::endl;
+                    std::vector<DEntry> rev;
+                    auto sz = dstack.size();
+                    // dump stack to vector to allow iteration
+                    for (int i = 0; i < sz; ++i) {
+                        rev.push_back(dstack.top());
+                        dstack.pop();
+                    }
+                    idx_t pos = 0;
+                    // print dstack in-order. rev[0] is dstack.top(), so loop vector in reverse
+                    for (int i = rev.size() - 1; i >= 0; --i) {
+                        pos = rev[i].pos;
+                        seen.decode(parent, cstack[pos].stateid);
+                        _dump_state(parent);
+                        cstack[pos].lowlink = std::numeric_limits<idx_t>::max();
+                        if (i > 0) {
+                            // print transition to next state
+                            seen.decode(next, cstack[rev[i - 1].pos].stateid);
+                            successorGenerator->prepare(&parent);
+                            while (successorGenerator->next(working)) {
+                                if (working == next) {
+                                    std::cerr << net.transitionNames()[successorGenerator->last_transition()]
+                                              << std::endl;
+                                    break;
+                                }
+                            }
+                        }
+                    }
+
+                    // follow lowsource until back in dstack
+                    pos = cstack[pos].lowsource;
+                    if (cstack[pos].lowlink != std::numeric_limits<idx_t>::max()) {
+                        std::cerr << "Printing looping part\n";
+                    }
+                    while (cstack[pos].lowlink != std::numeric_limits<idx_t>::max()) {
+                        seen.decode(parent, cstack[pos].stateid);
+                        _dump_state(parent);
+                        pos = cstack[pos].lowsource;
+                    }
+                }
             }
         }
         return !violation;
     }
 
-    void TarjanModelChecker::push(State &state) {
+    /**
+     * Push a state to the various stacks.
+     * @param state
+     */
+    template<bool SaveTrace>
+    void TarjanModelChecker<SaveTrace>::push(State &state) {
         const auto res = seen.add(state);
         const auto ctop = static_cast<idx_t>(cstack.size());
         const auto h = hash(res.second);
         cstack.emplace_back(ctop, res.second, chash[h]);
+        if constexpr (SaveTrace) {
+            cstack.back().lowsource = ctop;
+        }
         chash[h] = ctop;
-        dstack.push({ctop});
-        if (successorGenerator.isAccepting(state)) {
+        dstack.push(DEntry{ctop, initial_suc_info});
+        if (successorGenerator->isAccepting(state)) {
             astack.push(ctop);
         }
     }
 
-    void TarjanModelChecker::pop() {
+    template<bool SaveTrace>
+    void TarjanModelChecker<SaveTrace>::pop() {
         const size_t p = dstack.top().pos;
         dstack.pop();
         if (cstack[p].lowlink == p) {
@@ -91,42 +142,45 @@
         }
     }
 
-    void TarjanModelChecker::update(idx_t to) {
+    template<bool SaveTrace>
+    void TarjanModelChecker<SaveTrace>::update(idx_t to) {
         const auto from = dstack.top().pos;
         if (cstack[to].lowlink <= cstack[from].lowlink) {
+            // we have found a loop into earlier seen component cstack[to].lowlink.
+            // if this earlier component was found before an accepting state,
+            // we have found an accepting loop and thus a violation.
             violation = (!astack.empty() && to <= astack.top());
             cstack[from].lowlink = cstack[to].lowlink;
+            if constexpr (SaveTrace) {
+                cstack[from].lowsource = to;
+            }
         }
     }
 
-    bool TarjanModelChecker::nexttrans(State &state, TarjanModelChecker::DStack &delem) {
-        if (!delem.neighbors) {
-            delem.neighbors = std::vector<idx_t>();
-            delem.nexttrans = 0;
-            State src = factory.newState();
-            State dst = factory.newState();
-            seen.decode(src, cstack[delem.pos].stateid);
-            successorGenerator.prepare(&src);
-            while (successorGenerator.next(dst)) {
-                auto res = seen.add(dst);
+    template<bool SaveTrace>
+    bool TarjanModelChecker<SaveTrace>::nexttrans(State &state, State &parent, TarjanModelChecker::DEntry &delem) {
+        seen.decode(parent, cstack[delem.pos].stateid);
 #ifdef PRINTF_DEBUG
-                std::cerr << "adding state\n";
-                _dump_state(dst);
+        std::cerr << "loaded parent\n  ";
+        _dump_state(parent);
 #endif
-                delem.neighbors->push_back(res.second);
-            }
+        successorGenerator->prepare(&parent, delem.sucinfo);
+        if (delem.sucinfo.has_prev_state()) {
+            seen.decode(state, delem.sucinfo.last_state);
         }
-        if (delem.nexttrans == delem.neighbors->size()) {
-            return false;
-        } else {
-            seen.decode(state, (*delem.neighbors)[delem.nexttrans]);
+        auto res = successorGenerator->next(state, delem.sucinfo);
 #ifdef PRINTF_DEBUG
-            std::cerr << "loaded state\n";
+        if (res) {
+            std::cerr << "going to state\n";
             _dump_state(state);
+        }
 #endif
-            delem.nexttrans++;
-            return true;
-        }
+        return res;
     }
 
+    template
+    class TarjanModelChecker<true>;
+
+    template
+    class TarjanModelChecker<false>;
 }
 \ No newline at end of file
 
=== modified file 'src/LTLMain.cpp'
--- src/LTLMain.cpp	2020-10-16 11:40:41 +0000
+++ src/LTLMain.cpp	2020-11-09 13:59:57 +0000
@@ -32,10 +32,8 @@
 
 #include "CTL/CTLEngine.h"
 #include "PetriEngine/PQL/Expressions.h"
-#include "LTL/LTLToBuchi.h"
 #include "LTL/LTLValidator.h"
 #include "LTL/LTL_algorithm/NestedDepthFirstSearch.h"
-#include "LTL/LTL_algorithm/ProductPrinter.h"
 #include "LTL/LTL_algorithm/TarjanModelChecker.h"
 #include "LTL/LTL.h"
 
@@ -43,7 +41,6 @@
 using namespace PetriEngine::PQL;
 using namespace PetriEngine::Reachability;
 
-
 std::vector<std::string> explode(std::string const & s)
 {
     std::vector<std::string> result;
@@ -502,7 +499,10 @@
                     modelChecker = std::make_unique<LTL::NestedDepthFirstSearch>(*net, negated_formula);
                     break;
                 case LTL::Algorithm::Tarjan:
-                    modelChecker = std::make_unique<LTL::TarjanModelChecker>(*net, negated_formula);
+                    if (options.trace)
+                        modelChecker = std::make_unique<LTL::TarjanModelChecker<true>>(*net, negated_formula);
+                    else
+                        modelChecker = std::make_unique<LTL::TarjanModelChecker<false>>(*net, negated_formula);
                     break;
             }
 
 
=== modified file 'src/PetriEngine/SuccessorGenerator.cpp'
--- src/PetriEngine/SuccessorGenerator.cpp	2020-10-16 13:38:03 +0000
+++ src/PetriEngine/SuccessorGenerator.cpp	2020-11-09 13:59:57 +0000
@@ -97,7 +97,7 @@
                 for (; _suc_tcounter != last; ++_suc_tcounter) {
 
                     if (!checkPreset(_suc_tcounter)) continue;
-#ifdef PRINTF_DEBUG
+#ifdef _PRINTF_DEBUG
                     std::cerr << "trace: " << _net.transitionNames()[_suc_tcounter] << std::endl;
 #endif
                     memcpy(write.marking(), (*_parent).marking(), _net._nplaces * sizeof (MarkVal));