Merge lp:~tapaal-ltl/verifypn/traceable-tarjan into lp:~tapaal-ltl/verifypn/ltl-model-checker

[Nikolaj Jensen Ulrik]

Trace printing in Tarjan's algorithm

[Simon Virenfeldt (simwir)]

Kun en lille addition til docstring.

review: Approve

[lp:~tapaal-ltl/verifypn/traceable-tarjan]

256. By Nikolaj Jensen Ulrik on 2021-02-24

Hotfix and docstring

257. By Nikolaj Jensen Ulrik on 2021-03-03

TAPAAL compatible trace format, correct NDFS traces

258. By Nikolaj Jensen Ulrik on 2021-03-03

Add trace levels for internal usage

259. By Simon Virenfeldt on 2021-03-04

Added some additional newlines

=== modified file 'include/LTL/Algorithm/ModelChecker.h'
--- include/LTL/Algorithm/ModelChecker.h	2021-02-01 11:17:38 +0000
+++ include/LTL/Algorithm/ModelChecker.h	2021-03-04 10:04:52 +0000
@@ -21,24 +21,37 @@
 #include "PetriEngine/PQL/PQL.h"
 #include "LTL/ProductSuccessorGenerator.h"
 #include "LTL/Algorithm/ProductPrinter.h"
+#include "PetriEngine/options.h"
 
 namespace LTL {
+
     class ModelChecker {
     public:
-        ModelChecker(const PetriEngine::PetriNet& net, PetriEngine::PQL::Condition_ptr, const bool shortcircuitweak);
+        ModelChecker(const PetriEngine::PetriNet &net, PetriEngine::PQL::Condition_ptr, const bool shortcircuitweak,
+                     TraceLevel level = TraceLevel::Transitions);
+
         virtual bool isSatisfied() = 0;
-        
+
         virtual ~ModelChecker() = default;
+
         [[nodiscard]] bool isweak() const { return is_weak; }
+
+
     protected:
         std::unique_ptr<ProductSuccessorGenerator> successorGenerator;
         const PetriEngine::PetriNet &net;
         PetriEngine::PQL::Condition_ptr formula;
+        TraceLevel traceLevel;
 
         size_t _discovered = 0;
         const bool shortcircuitweak;
         bool weakskip = false;
         bool is_weak = false;
+        int maxTransName;
+
+        std::ostream &printTransition(size_t transition, LTL::Structures::ProductState &state, std::ostream &os);
+
+        void printLoop(std::ostream &os);
     };
 }
 

=== modified file 'include/LTL/Algorithm/NestedDepthFirstSearch.h'
--- include/LTL/Algorithm/NestedDepthFirstSearch.h	2021-03-02 12:06:17 +0000
+++ include/LTL/Algorithm/NestedDepthFirstSearch.h	2021-03-04 10:04:52 +0000
@@ -50,8 +50,8 @@
     template <typename W>
     class NestedDepthFirstSearch : public ModelChecker {
     public:
-        NestedDepthFirstSearch(const PetriNet &net, PetriEngine::PQL::Condition_ptr ptr, const bool shortcircuitweak)
-                : ModelChecker(net, ptr, shortcircuitweak), factory{net, successorGenerator->initial_buchi_state()},
+        NestedDepthFirstSearch(const PetriNet &net, PetriEngine::PQL::Condition_ptr ptr, const bool shortcircuitweak, TraceLevel level = TraceLevel::Full)
+                : ModelChecker(net, ptr, shortcircuitweak, level), factory{net, successorGenerator->initial_buchi_state()},
                 states(net, 0, (int)net.numberOfPlaces() + 1) {}
 
         bool isSatisfied() override;
@@ -73,14 +73,13 @@
         bool violation = false;
 
         //Used for printing the trace
-        std::stack<size_t> nested_transitions;
+        std::stack<std::pair<size_t, size_t>> nested_transitions;
 
         void dfs();
 
         void ndfs(State &state);
-        void printTrace(stack<size_t> &transitions);
+        void printTrace(std::stack<std::pair<size_t, size_t>> &transitions, std::ostream &os = std::cout);
 
-        ostream & printTransition(size_t transition, uint indent, ostream &os = std::cerr);
         static constexpr bool SaveTrace = std::is_same_v<W, PetriEngine::Structures::TracableStateSet>;
     };
     extern template class NestedDepthFirstSearch<PetriEngine::Structures::StateSet>;

=== modified file 'include/LTL/Algorithm/TarjanModelChecker.h'
--- include/LTL/Algorithm/TarjanModelChecker.h	2021-03-02 12:06:17 +0000
+++ include/LTL/Algorithm/TarjanModelChecker.h	2021-03-04 10:04:52 +0000
@@ -28,6 +28,7 @@
 
 namespace LTL {
 
+<<<<<<< TREE
     /**
      * Implements on-the-fly version of Tarjan's algorithm suitable for LTL model checking.
      * The idea is to detect some reachable strongly connected component containing an accepting state,
@@ -40,11 +41,27 @@
      * </p>
      */
     template <bool SaveTrace>
+=======
+    /**
+     * Implements on-the-fly version of Tarjan's algorithm suitable for LTL model checking.
+     * The idea is to detect some reachable strongly connected component containing an accepting state,
+     * which constitutes a counter-example.
+     * For more details see
+     *   Jaco Geldenhuys & Antti Valmari,
+     *   More efficient on-the-fly LTL verification with Tarjan's algorithm,
+     *   https://doi.org/10.1016/j.tcs.2005.07.004
+     *
+     * @tparam SaveTrace whether to save and print counter-examples when possible.
+     */
+    template<bool SaveTrace>
+>>>>>>> MERGE-SOURCE
     class TarjanModelChecker : public ModelChecker {
     public:
-        TarjanModelChecker(const PetriEngine::PetriNet &net, const Condition_ptr &cond, const bool shortcircuitweak)
-                : ModelChecker(net, cond, shortcircuitweak), factory(net, successorGenerator->initial_buchi_state()),
-                  seen(net, 0, (int) net.numberOfPlaces() + 1) {
+        TarjanModelChecker(const PetriEngine::PetriNet &net, const Condition_ptr &cond, const bool shortcircuitweak,
+                           TraceLevel level = TraceLevel::Full)
+                : ModelChecker(net, cond, shortcircuitweak, level), factory(net, successorGenerator->initial_buchi_state()),
+                  seen(net, 0, (int) net.numberOfPlaces() + 1)
+        {
             chash.fill(std::numeric_limits<idx_t>::max());
         }
 
@@ -58,7 +75,9 @@
 
         LTL::Structures::ProductStateFactory factory;
 
-        PetriEngine::Structures::StateSet seen;
+        using StateSet = std::conditional_t<SaveTrace, PetriEngine::Structures::TracableStateSet, PetriEngine::Structures::StateSet>;
+
+        StateSet seen;
         std::unordered_set<idx_t> store;
 
         // rudimentary hash table of state IDs. chash[hash(state)] is the top index in cstack
@@ -66,7 +85,8 @@
         std::array<idx_t, HashSz> chash;
         static_assert(sizeof(chash) == (1U << 27U));
 
-        static inline idx_t hash(idx_t id) {
+        static inline idx_t hash(idx_t id)
+        {
             return id % HashSz;
         }
 
@@ -86,21 +106,27 @@
         };
 
         using CEntry = std::conditional_t<SaveTrace,
-            TracableCEntry,
-            PlainCEntry>;
+                TracableCEntry,
+                PlainCEntry>;
+
 
         struct DEntry {
             idx_t pos; // position in cstack.
             successor_info sucinfo;
         };
 
+<<<<<<< TREE
         // master list of state information.
+=======
+>>>>>>> MERGE-SOURCE
         std::vector<CEntry> cstack;
         // depth-first search stack, contains current search path.
         std::stack<DEntry> dstack;
         // cstack positions of accepting states in current search path, for quick access.
         std::stack<idx_t> astack;
         bool violation = false;
+        size_t loopstate = std::numeric_limits<size_t>::max();
+        size_t looptrans = std::numeric_limits<size_t>::max();
 
         void push(State &state);
 
@@ -108,12 +134,19 @@
 
         void update(idx_t to);
 
-        bool nexttrans(State &state, State& parent, DEntry &delem);
+        bool nexttrans(State &state, State &parent, DEntry &delem);
 
         void popCStack();
+
+        void printTrace(std::stack<DEntry> &&dstack, std::ostream &os = std::cout);
+
     };
-extern template class TarjanModelChecker<true>;
-extern template class TarjanModelChecker<false>;
+
+    extern template
+    class TarjanModelChecker<true>;
+
+    extern template
+    class TarjanModelChecker<false>;
 }
 
 #endif //VERIFYPN_TARJANMODELCHECKER_H

=== added file 'include/LTL/AlgorithmTypes.h'
--- include/LTL/AlgorithmTypes.h	1970-01-01 00:00:00 +0000
+++ include/LTL/AlgorithmTypes.h	2021-03-04 10:04:52 +0000
@@ -0,0 +1,41 @@
+/* Copyright (C) 2021  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ * 
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ * 
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ * 
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_ALGORITHMTYPES_H
+#define VERIFYPN_ALGORITHMTYPES_H
+
+namespace LTL {
+    enum class Algorithm {
+        NDFS, RandomNDFS, Tarjan, None=-1
+    };
+    inline auto to_string(Algorithm alg) {
+        switch (alg) {
+            case Algorithm::NDFS:
+                return "NDFS";
+            case Algorithm::RandomNDFS:
+                return "RNDFS";
+            case Algorithm::Tarjan:
+                return "TARJAN";
+            case Algorithm::None:
+            default:
+                std::cerr << "to_string: Invalid LTL Algorithm " << static_cast<int>(alg) << '\n';
+                assert(false);
+        }
+    }
+}
+
+#endif //VERIFYPN_ALGORITHMTYPES_H

=== modified file 'include/LTL/LTL.h'
--- include/LTL/LTL.h	2021-02-01 11:17:38 +0000
+++ include/LTL/LTL.h	2021-03-04 10:04:52 +0000
@@ -26,23 +26,7 @@
 #include "LTL/LTLToBuchi.h"
 
 namespace LTL {
-    enum class Algorithm {
-        NDFS, RandomNDFS, Tarjan, None=-1
-    };
-    inline auto to_string(Algorithm alg) {
-        switch (alg) {
-            case Algorithm::NDFS:
-                return "NDFS";
-            case Algorithm::RandomNDFS:
-                return "RNDFS";
-            case Algorithm::Tarjan:
-                return "TARJAN";
-            case Algorithm::None:
-            default:
-                std::cerr << "to_string: Invalid LTL Algorithm " << static_cast<int>(alg) << '\n';
-                assert(false);
-        }
-    }
+
 
     std::pair<Condition_ptr, bool> to_ltl(const Condition_ptr &formula);
 }

=== modified file 'include/PetriEngine/options.h'
--- include/PetriEngine/options.h	2021-01-08 09:12:40 +0000
+++ include/PetriEngine/options.h	2021-03-04 10:04:52 +0000
@@ -9,13 +9,19 @@
 
 #include "Reachability/ReachabilitySearch.h"
 #include "../CTL/Algorithm/AlgorithmTypes.h"
-#include "../LTL/LTL.h"
+#include "../LTL/AlgorithmTypes.h"
 
 
 enum class TemporalLogic {
     CTL, LTL
 };
 
+enum class TraceLevel {
+    None,
+    Transitions,
+    Full
+};
+
 struct options_t {
 //    bool outputtrace = false;
     int kbound = 0;
@@ -29,7 +35,7 @@
     bool printstatistics = true;
     std::set<size_t> querynumbers;
     PetriEngine::Reachability::Strategy strategy = PetriEngine::Reachability::DEFAULT;
-    bool trace = false;
+    TraceLevel trace = TraceLevel::None;
     bool use_query_reductions = true;
     int queryReductionTimeout = 30, lpsolveTimeout = 10;
     uint32_t siphontrapTimeout = 0;
@@ -78,7 +84,7 @@
             optionsOut = "\nSearch=OverApprox";
         }
         
-        if (trace) {
+        if (trace != TraceLevel::None) {
             optionsOut += ",Trace=ENABLED";
         } else {
             optionsOut += ",Trace=DISABLED";

=== modified file 'src/CMakeLists.txt'
--- src/CMakeLists.txt	2021-02-01 11:17:38 +0000
+++ src/CMakeLists.txt	2021-03-04 10:04:52 +0000
@@ -5,7 +5,7 @@
 add_subdirectory(PetriParse)
 add_subdirectory(PetriEngine)
 
-add_executable(verifypn-${ARCH_TYPE} VerifyPN.cpp)
+add_executable(verifypn-${ARCH_TYPE} VerifyPN.cpp ../include/LTL/AlgorithmTypes.h)
 add_dependencies(verifypn-${ARCH_TYPE} glpk-ext spot-ext)
 
 target_link_libraries(verifypn-${ARCH_TYPE} PRIVATE CTL LTL PetriEngine PetriParse glpk spot)

=== modified file 'src/LTL/Algorithm/LTLToBuchi.cpp'
=== modified file 'src/LTL/Algorithm/ModelChecker.cpp'
--- src/LTL/Algorithm/ModelChecker.cpp	2021-02-01 11:17:38 +0000
+++ src/LTL/Algorithm/ModelChecker.cpp	2021-03-04 10:04:52 +0000
@@ -18,16 +18,54 @@
 #include "LTL/Algorithm/ModelChecker.h"
 
 #include <utility>
+#include <iomanip>
 
 namespace LTL {
-    ModelChecker::ModelChecker(const PetriEngine::PetriNet& net, PetriEngine::PQL::Condition_ptr condition, const bool shortcircuitweak)
-        : net(net), formula(condition), shortcircuitweak(shortcircuitweak)
+    ModelChecker::ModelChecker(const PetriEngine::PetriNet &net, PetriEngine::PQL::Condition_ptr condition,
+                               const bool shortcircuitweak, TraceLevel level)
+            : net(net), formula(condition), traceLevel(level), shortcircuitweak(shortcircuitweak)
     {
 
         successorGenerator = std::make_unique<ProductSuccessorGenerator>(net, condition);
-        //TODO Create successor generator from net and condition
-
-        //LTL::ProductPrinter::printProduct(*successorGenerator, std::cout, net, condition);
-    }
+
+        maxTransName = std::max_element(std::begin(net.transitionNames()), std::end(net.transitionNames()),
+                                        [](auto &a, auto &b) { return a.size() < b.size(); })->size();
+
+    }
+
+    static constexpr auto indent = "  ";
+    static constexpr auto tokenIndent = "    ";
+
+    void ModelChecker::printLoop(std::ostream &os)
+    {
+        os << indent << "<loop/>\n";
+    }
+
+    std::ostream &
+    ModelChecker::printTransition(size_t transition, LTL::Structures::ProductState &state, std::ostream &os)
+    {
+        if (transition >= std::numeric_limits<ptrie::uint>::max() - 1) {
+            os << indent << "<deadlock/>";
+            return os;
+        }
+        std::string tname = net.transitionNames()[transition];
+        if (traceLevel == TraceLevel::Full) {
+            os << indent << "<transition id=\"" << tname << "\">\n";
+            for (size_t i = 0; i < net.numberOfPlaces(); ++i) {
+                for (size_t j = 0; j < state.marking()[i]; ++j) {
+                    os << tokenIndent << R"(<token age="0" place=")" << net.placeNames()[i] << "\"/>\n";
+                }
+            }
+#ifndef NDEBUG
+            os << '\n' << tokenIndent << "<buchi state=\"" << state.getBuchiState() << "\"/>\n";
+#endif
+            os << indent << "</transition>";
+        } else {
+            os << indent << "<transition id=" << std::setw(maxTransName + 1) << std::quoted(tname) << "\tbuchisucc=\""
+               << state.getBuchiState() << "\"/>";
+        }
+        return os;
+    }
+
 }
 

=== modified file 'src/LTL/Algorithm/NestedDepthFirstSearch.cpp'
--- src/LTL/Algorithm/NestedDepthFirstSearch.cpp	2021-03-02 12:06:17 +0000
+++ src/LTL/Algorithm/NestedDepthFirstSearch.cpp	2021-03-04 10:04:52 +0000
@@ -19,14 +19,16 @@
 
 namespace LTL {
     template<typename W>
-    bool NestedDepthFirstSearch<W>::isSatisfied() {
+    bool NestedDepthFirstSearch<W>::isSatisfied()
+    {
         is_weak = successorGenerator->is_weak() && shortcircuitweak;
         dfs();
         return !violation;
     }
 
     template<typename W>
-    void NestedDepthFirstSearch<W>::dfs() {
+    void NestedDepthFirstSearch<W>::dfs()
+    {
         std::stack<size_t> call_stack;
         std::stack<StackEntry> todo;
 
@@ -59,13 +61,13 @@
                     ndfs(curState);
                     if (violation) {
                         if constexpr (SaveTrace) {
-                            std::stack<size_t> transitions;
+                            std::stack<std::pair<size_t, size_t>> transitions;
                             size_t next = top.id;
                             states.decode(working, next);
                             while (!successorGenerator->isInitialState(working)) {
                                 auto[parent, transition] = states.getHistory(next);
+                                transitions.push(std::make_pair(next, transition));
                                 next = parent;
-                                transitions.push(transition);
                                 states.decode(working, next);
                             }
                             printTrace(transitions);
@@ -90,7 +92,8 @@
     }
 
     template<typename W>
-    void NestedDepthFirstSearch<W>::ndfs(State &state) {
+    void NestedDepthFirstSearch<W>::ndfs(State &state)
+    {
         std::stack<StackEntry> todo;
 
         State working = factory.newState();
@@ -115,22 +118,22 @@
                     violation = true;
                     if constexpr (SaveTrace) {
                         auto[_, stateid] = states.add(working);
+                        auto seedId = stateid;
                         states.setHistory2(stateid, successorGenerator->fired());
                         size_t next = stateid;
+<<<<<<< TREE
                         ptrie::uint trans = 0;
                         // SuccessorGenerator returns tcount - 1, but resets tcount to UINT_MAX when done,
                         // hence loop until transition >= UINT_MAX - 1.
                         while (trans < std::numeric_limits<ptrie::uint>::max() - 1) {
+=======
+                        // follow trace until back at seed state.
+                        do {
+>>>>>>> MERGE-SOURCE
                             auto[state, transition] = states.getHistory2(next);
-                            if (transition >= std::numeric_limits<ptrie::uint>::max() - 1) {
-                                auto[_, transition] = states.getHistory(next);
-                                nested_transitions.push(transition);
-                                break;
-                            }
+                            nested_transitions.push(std::make_pair(next, transition));
                             next = state;
-                            trans = transition;
-                            nested_transitions.push(transition);
-                        }
+                        } while (next != seedId);
                     }
                     return;
                 }
@@ -151,29 +154,26 @@
     }
 
     template<typename W>
-    ostream &NestedDepthFirstSearch<W>::printTransition(size_t transition, uint indent, ostream &os) {
-        if (transition == std::numeric_limits<ptrie::uint>::max() - 1) {
-            os << std::string(indent, '\t') << "<deadlock/>";
-            return os;
-        }
-        std::string tname = states.net().transitionNames()[transition];
-        os << std::string(indent, '\t') << "<transition id=\"" << tname << "\" index=\"" << transition << "\"/>";
-        return os;
-    }
-
-    template<typename W>
-    void NestedDepthFirstSearch<W>::printTrace(std::stack<size_t> &transitions) {
-        std::cerr << "Trace:\n<trace>\n";
+    void NestedDepthFirstSearch<W>::printTrace(std::stack<std::pair<size_t, size_t>> &transitions, std::ostream &os)
+    {
+        State state = factory.newState();
+        os << "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n"
+              "<trace>\n";
         while (!transitions.empty()) {
-            printTransition(transitions.top(), 1) << std::endl;
+            auto [stateid, transition] = transitions.top();
+            states.decode(state, stateid);
+            printTransition(transition, state, os) << std::endl;
             transitions.pop();
         }
-        std::cerr << "\t<loop>" << std::endl;
+        printLoop(os);
         while (!nested_transitions.empty()) {
-            printTransition(nested_transitions.top(), 2) << std::endl;
+            auto [stateid, transition] = nested_transitions.top();
+            states.decode(state, stateid);
+
+            printTransition(transition, state, os) << std::endl;
             nested_transitions.pop();
         }
-        std::cerr << "\t</loop>" << std::endl << "</trace>" << std::endl;
+        os << std::endl << "</trace>" << std::endl;
     }
 
 

=== modified file 'src/LTL/Algorithm/TarjanModelChecker.cpp'
--- src/LTL/Algorithm/TarjanModelChecker.cpp	2021-03-02 12:06:17 +0000
+++ src/LTL/Algorithm/TarjanModelChecker.cpp	2021-03-04 10:04:52 +0000
@@ -47,7 +47,12 @@
                     pop();
                     continue;
                 }
-                const idx_t stateid = seen.add(working).second;
+                auto[isnew, stateid] = seen.add(working);
+                if constexpr (SaveTrace) {
+                    if (isnew) {
+                        seen.setHistory(stateid, successorGenerator->fired());
+                    }
+                }
                 dtop.sucinfo.last_state = stateid;
 
                 // lookup successor in 'hash' table
@@ -68,46 +73,13 @@
             if constexpr (SaveTrace) {
                 // print counter-example if it exists.
                 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 (idx_t i = 0; i < sz; ++i) {
-                        rev.push_back(dstack.top());
+                    std::stack<DEntry> revstack;
+                    while (!dstack.empty()) {
+                        revstack.push(std::move(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;
-                    }
+                    printTrace(std::move(revstack));
+                    return false;
                 }
             }
         }
@@ -176,7 +148,10 @@
             // either way update the component ID of the state we came from.
             cstack[from].lowlink = cstack[to].lowlink;
             if constexpr (SaveTrace) {
-                cstack[from].lowsource = to;
+                loopstate = cstack[to].stateid;
+                looptrans = successorGenerator->fired();
+                cstack[from].lowsource = cstack[to].lowlink;
+
             }
         }
     }
@@ -192,9 +167,46 @@
         return res;
     }
 
+
+    template<bool SaveTrace>
+    void TarjanModelChecker<SaveTrace>::printTrace(std::stack<DEntry> &&dstack, std::ostream &os)
+    {
+        if constexpr (!SaveTrace) {
+            return;
+        } else {
+            State state = factory.newState();
+            dstack.pop();
+            os << "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n"
+                  "<trace>\n";
+            unsigned long p;
+            // print (reverted) dstack
+            while (!dstack.empty()) {
+                p = dstack.top().pos;
+                auto stateid = cstack[p].stateid;
+                auto[parent, tid] = seen.getHistory(stateid);
+                seen.decode(state, stateid);
+                printTransition(tid, state, os) << '\n';
+                cstack[p].lowlink = std::numeric_limits<idx_t>::max();
+                dstack.pop();
+            }
+            printLoop(os);
+            // follow previously found back edges via lowsource until back in dstack.
+            p = cstack[p].lowsource;
+            while (cstack[p].lowlink != std::numeric_limits<idx_t>::max()) {
+                auto[parent, tid] = seen.getHistory(cstack[p].stateid);
+                seen.decode(state, cstack[p].stateid);
+                printTransition(tid, state, os) << '\n';
+                p = cstack[p].lowsource;
+            }
+            printTransition(looptrans, state, os) << '\n';
+
+            os << "</trace>" << std::endl;
+        }
+    }
+
     template
     class TarjanModelChecker<true>;
 
     template
     class TarjanModelChecker<false>;
-}
\ No newline at end of file
+}

=== modified file 'src/PetriEngine/Reachability/ResultPrinter.cpp'
--- src/PetriEngine/Reachability/ResultPrinter.cpp	2020-04-23 15:26:52 +0000
+++ src/PetriEngine/Reachability/ResultPrinter.cpp	2021-03-04 10:04:52 +0000
@@ -132,7 +132,7 @@
             if(options->cpnOverApprox)
                 std::cout << "\nSolved using CPN Approximation\n" << std::endl;
             
-            if(showTrace && options->trace)
+            if(showTrace && options->trace != TraceLevel::None)
             {
                 if(stateset == nullptr)
                 {

=== modified file 'src/VerifyPN.cpp'
--- src/VerifyPN.cpp	2021-03-03 08:34:27 +0000
+++ src/VerifyPN.cpp	2021-03-04 10:04:52 +0000
@@ -169,7 +169,22 @@
         } else if (strcmp(argv[i], "-n") == 0 || strcmp(argv[i], "--no-statistics") == 0) {
             options.printstatistics = false;
         } else if (strcmp(argv[i], "-t") == 0 || strcmp(argv[i], "--trace") == 0) {
-            options.trace = true;
+            if (argc > i + 1) {
+                if (strcmp("1", argv[i+1]) == 0) {
+                    options.trace = TraceLevel::Transitions;
+                }
+                else if (strcmp("2", argv[i+1]) == 0) {
+                    options.trace = TraceLevel::Full;
+                }
+                else {
+                    options.trace = TraceLevel::Full;
+                    continue;
+                }
+                ++i;
+            }
+            else {
+                options.trace = TraceLevel::Full;
+            }
         } else if (strcmp(argv[i], "-x") == 0 || strcmp(argv[i], "--xml-queries") == 0) {
             if (i == argc - 1) {
                 fprintf(stderr, "Missing number after \"%s\"\n\n", argv[i]);
@@ -1122,7 +1137,7 @@
     if (options.enablereduction > 0) {
         // Compute how many times each place appears in the query
         builder.startTimer();
-        builder.reduce(queries, results, options.enablereduction, options.trace, nullptr, options.reductionTimeout, options.reductions);
+        builder.reduce(queries, results, options.enablereduction, options.trace != TraceLevel::None, nullptr, options.reductionTimeout, options.reductions);
         printer.setReducer(builder.getReducer());
     }
 
@@ -1199,9 +1214,9 @@
             std::unique_ptr<LTL::ModelChecker> modelChecker;
             switch (options.ltlalgorithm) {
                 case LTL::Algorithm::NDFS:
-                    if (options.trace)
+                    if (options.trace != TraceLevel::None)
                         modelChecker = std::make_unique<LTL::NestedDepthFirstSearch<PetriEngine::Structures::TracableStateSet>>
-                                (*net, negated_formula, options.ltluseweak);
+                                (*net, negated_formula, options.ltluseweak, options.trace);
                     else
                         modelChecker = std::make_unique<LTL::NestedDepthFirstSearch<PetriEngine::Structures::StateSet>>
                                 (*net, negated_formula, options.ltluseweak);
@@ -1209,8 +1224,8 @@
                 case LTL::Algorithm::RandomNDFS:
                     modelChecker = std::make_unique<LTL::RandomNDFS>(*net, negated_formula);
                 case LTL::Algorithm::Tarjan:
-                    if (options.trace)
-                        modelChecker = std::make_unique<LTL::TarjanModelChecker<true>>(*net, negated_formula, options.ltluseweak);
+                    if (options.trace != TraceLevel::None)
+                        modelChecker = std::make_unique<LTL::TarjanModelChecker<true>>(*net, negated_formula, options.ltluseweak, options.trace);
                     else
                         modelChecker = std::make_unique<LTL::TarjanModelChecker<false>>(*net, negated_formula, options.ltluseweak);
                     break;
@@ -1266,7 +1281,7 @@
         //Reachability search
         strategy.reachable(queries, results,
                 options.printstatistics,
-                options.trace);
+                options.trace != TraceLevel::None);
     }
     else
     {
@@ -1281,7 +1296,7 @@
                            options.stubbornreduction,
                            options.statespaceexploration,
                            options.printstatistics,
-                           options.trace);
+                           options.trace != TraceLevel::None);
     }
 
     return SuccessCode;