Merge lp:~tapaal-ltl/verifypn/reach-stub-new into lp:verifypn

[Peter Gjøl Jensen]

Adds POR for LTL, improves performance of NDFS.

Passes regression on MCC21 models using competition script.

[lp:~tapaal-ltl/verifypn/reach-stub-new]

279. By Nikolaj Jensen Ulrik on 2021-10-14

Probably properly fixed k-bounds in NDFS. Fixes https://bugs.launchpad.net/tapaal/+bug/1947036

280. By Nikolaj Jensen Ulrik on 2021-10-14

LTL Query simplification more robust against queries without leading A/E quantifier.

281. By Nikolaj Jensen Ulrik on 2021-10-15

Fixing infinite loop in Tarjan trace generation

282. By Peter G. Jensen <email address hidden> on 2021-10-15

avoiding double-addition of extra-consume during ruleB trace reconstruction

283. By Nikolaj Jensen Ulrik on 2021-10-16

extraConsume in the right place

284. By <email address hidden> on 2021-10-17

increased version number to 4.2.0

[Jiri Srba (srba)]

Merging to trunk now - small issue with loop at the end in once case but let's address this in 3.9.1 release.

review: Approve

=== modified file 'CMakeLists.txt'
--- CMakeLists.txt	2021-08-11 09:06:51 +0000
+++ CMakeLists.txt	2021-10-17 18:21:15 +0000
@@ -15,7 +15,7 @@
 set(CMAKE_POSITION_INDEPENDENT_CODE ON)
 
 
-set(VERIFYPN_VERSION 4.1.0)
+set(VERIFYPN_VERSION 4.2.0)
 add_compile_definitions(VERIFYPN_VERSION=\"${VERIFYPN_VERSION}\")
 
 project(verifypn VERSION ${VERIFYPN_VERSION} LANGUAGES CXX C)

=== modified file 'include/LTL/Algorithm/ModelChecker.h'
--- include/LTL/Algorithm/ModelChecker.h	2021-08-06 09:34:01 +0000
+++ include/LTL/Algorithm/ModelChecker.h	2021-10-17 18:21:15 +0000
@@ -25,7 +25,9 @@
 #include "LTL/SuccessorGeneration/SpoolingSuccessorGenerator.h"
 #include "LTL/Structures/BitProductStateSet.h"
 #include "LTL/SuccessorGeneration/ReachStubProductSuccessorGenerator.h"
+#include "LTL/Structures/ProductStateFactory.h"
 #include "PetriEngine/options.h"
+#include "PetriEngine/Reducer.h"
 
 #include <iomanip>
 #include <algorithm>
@@ -37,11 +39,14 @@
         ModelChecker(const PetriEngine::PetriNet *net,
                      const PetriEngine::PQL::Condition_ptr &condition,
                      const Structures::BuchiAutomaton &buchi,
-                     SuccessorGen *successorGen,
+                     SuccessorGen *successorGen, const PetriEngine::Reducer* reducer,
                      std::unique_ptr<Spooler> &&...spooler)
-                : net(net), formula(condition)
+                : net(net), formula(condition), _reducer(reducer), successorGenerator(
+                std::make_unique<ProductSucGen<SuccessorGen, Spooler...>>(net, buchi, successorGen,
+                                                                          std::move(spooler)...)),
+                  _factory(net, buchi, this->successorGenerator->initial_buchi_state())
         {
-            successorGenerator = std::make_unique<ProductSucGen<SuccessorGen, Spooler...>>(net, buchi, successorGen, std::move(spooler)...);
+//            successorGenerator = std::make_unique<ProductSucGen<SuccessorGen, Spooler...>>(net, buchi, successorGen, std::move(spooler)...);
         }
 
         void setOptions(const options_t &options) {
@@ -81,11 +86,14 @@
                       << "\tmax tokens:        " << stateSet.max_tokens() << std::endl;
         }
 
+        const PetriEngine::Reducer* _reducer;
         std::unique_ptr<ProductSucGen<SuccessorGen, Spooler...>> successorGenerator;
 
         const PetriEngine::PetriNet *net;
         PetriEngine::PQL::Condition_ptr formula;
+        //const Structures::BuchiAutomaton *_aut;
         TraceLevel traceLevel;
+        LTL::Structures::ProductStateFactory _factory;
 
         size_t _discovered = 0;
         bool shortcircuitweak;
@@ -102,41 +110,37 @@
         }
 
         std::ostream &
-        printTransition(size_t transition, LTL::Structures::ProductState &state, std::ostream &os)
+        printTransition(size_t transition, std::ostream &os, const LTL::Structures::ProductState* state = nullptr)
         {
             if (transition >= std::numeric_limits<ptrie::uint>::max() - 1) {
                 os << indent << "<deadlock/>";
                 return os;
             }
-                os << indent << "<transition id="
-                   // field width stuff obsolete without büchi state printing.
-                   //<< std::setw(maxTransName + 2) << std::left
-                   << std::quoted(net->transitionNames()[transition]);
-            if (traceLevel == TraceLevel::Full) {
-                os << ">";
-                os << std::endl;
-                auto [fpre, lpre] = net->preset(transition);
-                for(; fpre < lpre; ++fpre) {
-                    if (fpre->inhibitor) {
-                        assert(state.marking()[fpre->place] < fpre->tokens);
-                        continue;
-                    }
-                    for (size_t i = 0; i < fpre->tokens; ++i) {
-                        assert(state.marking()[fpre->place] >= fpre->tokens);
-                        os << tokenIndent << R"(<token age="0" place=")" << net->placeNames()[fpre->place] << "\"/>\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";
-                    }
-                }*/
-                os << indent << "</transition>";
-            }
-            else {
-                os << "/>";
-            }
-            return os;
+            os << indent << "<transition id="
+                // field width stuff obsolete without büchi state printing.
+                << std::quoted(net->transitionNames()[transition]);
+            os << ">";
+            if(_reducer) {
+                _reducer->extraConsume(os, net->transitionNames()[transition]);
+            }
+            os << std::endl;
+            auto [fpre, lpre] = net->preset(transition);
+            for(; fpre < lpre; ++fpre) {
+                if (fpre->inhibitor) {
+                    assert(state == nullptr || state->marking()[fpre->place] < fpre->tokens);
+                    continue;
+                }
+                for (size_t i = 0; i < fpre->tokens; ++i) {
+                    assert(state == nullptr || state->marking()[fpre->place] >= fpre->tokens);
+                    os << tokenIndent << R"(<token age="0" place=")" << net->placeNames()[fpre->place] << "\"/>\n";
+                }
+            }
+            os << indent << "</transition>\n";
+            if(_reducer)
+            {
+                _reducer->postFire(os, net->transitionNames()[transition]);
+            }
+           return os;
         }
     };
 }

=== modified file 'include/LTL/Algorithm/NestedDepthFirstSearch.h'
--- include/LTL/Algorithm/NestedDepthFirstSearch.h	2021-08-10 13:44:22 +0000
+++ include/LTL/Algorithm/NestedDepthFirstSearch.h	2021-10-17 18:21:15 +0000
@@ -22,12 +22,11 @@
 #include "PetriEngine/Structures/StateSet.h"
 #include "PetriEngine/Structures/State.h"
 #include "PetriEngine/Structures/Queue.h"
+#include "PetriEngine/Structures/light_deque.h"
 #include "LTL/Structures/ProductStateFactory.h"
 
-#include <ptrie/ptrie_stable.h>
-#include <unordered_set>
-
 namespace LTL {
+
     /**
      * Implement the nested DFS algorithm for LTL model checking. Roughly based on versions given in
      * <p>
@@ -45,14 +44,13 @@
      * @tparam W type used for state storage. Use <code>PetriEngine::Structures::TracableStateSet</code> if you want traces,
      *         <code>PetriEngine::Structures::StateSet</code> if you don't care (as it is faster).
      */
-    template<typename SucGen, typename W>
-class NestedDepthFirstSearch : public ModelChecker<ProductSuccessorGenerator, SucGen> {
+    template<typename SucGen>
+    class NestedDepthFirstSearch : public ModelChecker<ProductSuccessorGenerator, SucGen> {
     public:
         NestedDepthFirstSearch(const PetriEngine::PetriNet *net, const PetriEngine::PQL::Condition_ptr &query,
-                               const Structures::BuchiAutomaton &buchi, SucGen *gen, int kbound)
-                : ModelChecker<ProductSuccessorGenerator, SucGen>(net, query, buchi, gen),
-                  factory{net, this->successorGenerator->initial_buchi_state()},
-                  states(net, kbound) {}
+                               const Structures::BuchiAutomaton &buchi, SucGen *gen, const bool print_trace, int kbound, const PetriEngine::Reducer* reducer)
+                : ModelChecker<ProductSuccessorGenerator, SucGen>(net, query, buchi, gen, reducer),
+                  _states(net, kbound), _print_trace(print_trace) {}
 
         bool isSatisfied() override;
 
@@ -60,43 +58,40 @@
 
     private:
         using State = LTL::Structures::ProductState;
-
-        Structures::ProductStateFactory factory;
-        W states; //StateSet
-        std::set<size_t> mark1;
-        std::set<size_t> mark2;
+        std::pair<bool,size_t> mark(State& state, uint8_t);
+
+
+        LTL::Structures::BitProductStateSet<> _states;
+
+        std::unordered_map<size_t, uint8_t> _markers;
+        //std::vector<uint8_t> _markers;
+        static constexpr uint8_t MARKER1 = 1;
+        static constexpr uint8_t MARKER2 = 2;
+        size_t _mark_count[3] = {0,0,0};
 
         struct StackEntry {
-            size_t id;
-            typename SucGen::sucinfo sucinfo;
+            size_t _id;
+            typename SucGen::successor_info_t _sucinfo;
         };
 
-        State *seed;
-        bool violation = false;
+        bool _violation = false;
+        const bool _print_trace = false;
 
         //Used for printing the trace
-        std::stack<std::pair<size_t, size_t>> nested_transitions;
+        std::stack<std::pair<size_t, size_t>> _nested_transitions;
 
         void dfs();
 
-        void ndfs(State &state);
-
-        void printTrace(std::stack<std::pair<size_t, size_t>> &transitions, std::ostream &os = std::cout);
-
-        static constexpr bool SaveTrace = std::is_same_v<W, PetriEngine::Structures::TracableStateSet>;
+        void ndfs(const State &state, light_deque<StackEntry>& nested_todo);
+
+        void print_trace(light_deque<StackEntry>& todo, light_deque<StackEntry>& nested_todo, std::ostream &os = std::cout);
     };
 
     extern template
-    class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, LTL::Structures::BitProductStateSet<>>;
-
-    extern template
-    class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, LTL::Structures::TraceableBitProductStateSet<>>;
-
-    extern template
-    class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, LTL::Structures::BitProductStateSet<>>;
-
-    extern template
-    class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, LTL::Structures::TraceableBitProductStateSet<>>;
+    class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator>;
+
+    extern template
+    class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator>;
 }
 
 #endif //VERIFYPN_NESTEDDEPTHFIRSTSEARCH_H

=== modified file 'include/LTL/Algorithm/TarjanModelChecker.h'
--- include/LTL/Algorithm/TarjanModelChecker.h	2021-08-10 13:44:22 +0000
+++ include/LTL/Algorithm/TarjanModelChecker.h	2021-10-17 18:21:15 +0000
@@ -49,62 +49,60 @@
         TarjanModelChecker(const PetriEngine::PetriNet *net, const PetriEngine::PQL::Condition_ptr &cond,
                            const Structures::BuchiAutomaton &buchi,
                            SuccessorGen *successorGen,
-                           int kbound,
+                           int kbound, const PetriEngine::Reducer* reducer,
                            std::unique_ptr<Spooler> &&...spooler)
-                : ModelChecker<ProductSucGen, SuccessorGen, Spooler...>(net, cond, buchi, successorGen, std::move(spooler)...),
-                  factory(net, this->successorGenerator->initial_buchi_state()),
-                  seen(net, kbound)
+                : ModelChecker<ProductSucGen, SuccessorGen, Spooler...>(net, cond, buchi, successorGen, reducer, std::move(spooler)...),
+                  _seen(net, kbound)
         {
             if (buchi._buchi->num_states() > 65535) {
                 std::cerr << "Fatal error: cannot handle Büchi automata larger than 2^16 states\n";
                 exit(1);
             }
-            chash.fill(std::numeric_limits<idx_t>::max());
+            _chash.fill(std::numeric_limits<idx_t>::max());
         }
 
         bool isSatisfied() override;
 
         void printStats(std::ostream &os) override
         {
-            this->_printStats(os, seen);
+            this->_printStats(os, _seen);
         }
 
     private:
         using State = LTL::Structures::ProductState;
         using idx_t = size_t;
         // 64 MB hash table
-        static constexpr idx_t HashSz = 16777216;
+        static constexpr idx_t _hash_sz = 16777216;
 
-        LTL::Structures::ProductStateFactory factory;
 
         using StateSet = std::conditional_t<SaveTrace, LTL::Structures::TraceableBitProductStateSet<>, LTL::Structures::BitProductStateSet<>>;
-        static constexpr bool IsSpooling = std::is_same_v<SuccessorGen, SpoolingSuccessorGenerator>;
+        static constexpr bool _is_spooling = std::is_same_v<SuccessorGen, SpoolingSuccessorGenerator>;
 
-        StateSet seen;
-        std::unordered_set<idx_t> store;
+        StateSet _seen;
+        std::unordered_set<idx_t> _store;
 
         // rudimentary hash table of state IDs. chash[hash(state)] is the top index in cstack
         // corresponding to state. Collisions are resolved using linked list via CEntry::next.
-        std::array<idx_t, HashSz> chash;
-        static_assert(sizeof(chash) == (1U << 27U));
+        std::array<idx_t, _hash_sz> _chash;
+        static_assert(sizeof(_chash) == (1U << 27U));
 
         static inline idx_t hash(idx_t id)
         {
-            return id % HashSz;
+            return id % _hash_sz;
         }
 
         struct PlainCEntry {
-            idx_t lowlink;
-            idx_t stateid;
-            idx_t next = std::numeric_limits<idx_t>::max();
-            bool dstack = true;
+            idx_t _lowlink;
+            idx_t _stateid;
+            idx_t _next = std::numeric_limits<idx_t>::max();
+            bool _dstack = true;
 
-            PlainCEntry(idx_t lowlink, idx_t stateid, idx_t next) : lowlink(lowlink), stateid(stateid), next(next) {}
+            PlainCEntry(idx_t lowlink, idx_t stateid, idx_t next) : _lowlink(lowlink), _stateid(stateid), _next(next) {}
         };
 
         struct TracableCEntry : PlainCEntry {
-            idx_t lowsource = std::numeric_limits<idx_t>::max();
-            idx_t sourcetrans;
+            idx_t _lowsource = std::numeric_limits<idx_t>::max();
+            idx_t _sourcetrans;
 
             TracableCEntry(idx_t lowlink, idx_t stateid, idx_t next) : PlainCEntry(lowlink, stateid, next) {}
         };
@@ -114,24 +112,24 @@
                 PlainCEntry>;
 
         struct DEntry {
-            idx_t pos; // position in cstack.
-
-            typename SuccessorGen::sucinfo sucinfo;
-
-            explicit DEntry(idx_t pos) : pos(pos), sucinfo(SuccessorGen::initial_suc_info()) {}
+            idx_t _pos; // position in cstack.
+
+            typename SuccessorGen::successor_info_t _sucinfo;
+
+            explicit DEntry(idx_t pos) : _pos(pos), _sucinfo(SuccessorGen::initial_suc_info()) {}
         };
 
         // master list of state information.
-        std::vector<CEntry> cstack;
+        std::vector<CEntry> _cstack;
         // depth-first search stack, contains current search path.
-        std::stack<DEntry> dstack;
+        std::stack<DEntry> _dstack;
         // cstack positions of accepting states in current search path, for quick access.
-        std::stack<idx_t> astack;
+        std::stack<idx_t> _astack;
 
-        bool violation = false;
-        bool invariant_loop = true;
-        size_t loopstate = std::numeric_limits<size_t>::max();
-        size_t looptrans = std::numeric_limits<size_t>::max();
+        bool _violation = false;
+        bool _invariant_loop = true;
+        size_t _loop_state = std::numeric_limits<size_t>::max();
+        size_t _loop_trans = std::numeric_limits<size_t>::max();
 
         void push(State &state, size_t stateid);
 
@@ -144,8 +142,8 @@
         void popCStack();
 
         void printTrace(std::stack<DEntry> &&dstack, std::ostream &os = std::cout);
-
     };
+
     extern template
     class TarjanModelChecker<ProductSuccessorGenerator, LTL::ResumingSuccessorGenerator, true>;
 

=== modified file 'include/LTL/LTLMain.h'
--- include/LTL/LTLMain.h	2021-08-03 12:00:44 +0000
+++ include/LTL/LTLMain.h	2021-10-17 18:21:15 +0000
@@ -1,16 +1,16 @@
 /* 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/>.
  */
@@ -26,7 +26,8 @@
     bool LTLMain(const PetriEngine::PetriNet *net,
                         const PetriEngine::PQL::Condition_ptr &query,
                         const std::string &queryName,
-                        options_t &options);
+                        options_t &options,
+                        const PetriEngine::Reducer* reducer);
 }
 
 #endif //VERIFYPN_LTLMAIN_H

=== modified file 'include/LTL/Structures/BitProductStateSet.h'
--- include/LTL/Structures/BitProductStateSet.h	2021-08-10 13:44:22 +0000
+++ include/LTL/Structures/BitProductStateSet.h	2021-10-17 18:21:15 +0000
@@ -1,16 +1,16 @@
 /* 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/>.
  */
@@ -64,7 +64,7 @@
     template<uint8_t nbits = 16>
     class BitProductStateSet : public ProductStateSetInterface {
     public:
-        explicit BitProductStateSet(const PetriEngine::PetriNet *net, int kbound = 0, size_t nplaces = -1)
+        explicit BitProductStateSet(const PetriEngine::PetriNet *net, int kbound = 0)
                 : markings(*net, kbound, net->numberOfPlaces())
         {
         }

=== modified file 'include/LTL/Structures/ProductState.h'
--- include/LTL/Structures/ProductState.h	2021-04-29 13:19:53 +0000
+++ include/LTL/Structures/ProductState.h	2021-10-17 18:21:15 +0000
@@ -19,6 +19,7 @@
 #define VERIFYPN_PRODUCTSTATE_H
 
 #include "PetriEngine/Structures/State.h"
+#include "LTL/Structures/BuchiAutomaton.h"
 
 namespace LTL {
     template <class SuccessorGen>
@@ -32,7 +33,7 @@
      */
     class ProductState : public PetriEngine::Structures::State {
     public:
-        ProductState() : PetriEngine::Structures::State() {}
+        explicit ProductState(const BuchiAutomaton* aut = nullptr) : PetriEngine::Structures::State(), _aut(aut) {}
 
         void setMarking(PetriEngine::MarkVal* marking, size_t nplaces)
         {
@@ -74,10 +75,17 @@
         bool operator!=(const ProductState &rhs) const {
             return !(rhs == *this);
         }
+
+        [[nodiscard]] bool is_accepting() const {
+            assert(_aut);
+            return _aut->_buchi->state_is_accepting(getBuchiState());
+        }
+
     private:
         template <typename T>
         friend class LTL::ProductSuccessorGenerator;
         size_t buchi_state_idx;
+        const LTL::Structures::BuchiAutomaton *_aut = nullptr;
     };
 }
 

=== modified file 'include/LTL/Structures/ProductStateFactory.h'
--- include/LTL/Structures/ProductStateFactory.h	2021-04-29 07:47:52 +0000
+++ include/LTL/Structures/ProductStateFactory.h	2021-10-17 18:21:15 +0000
@@ -25,14 +25,14 @@
 namespace LTL::Structures{
     class ProductStateFactory {
     public:
-        ProductStateFactory(const PetriEngine::PetriNet *net, size_t initial_buchi_state)
-            : net(net), buchi_init(initial_buchi_state) {}
+        ProductStateFactory(const PetriEngine::PetriNet *net, const BuchiAutomaton& aut, size_t initial_buchi_state)
+            : net(net), _aut(aut), buchi_init(initial_buchi_state) {}
 
         ProductState newState() {
             auto buf = new PetriEngine::MarkVal[net->numberOfPlaces()+1];
             std::copy(net->initial(), net->initial() + net->numberOfPlaces(), buf);
             buf[net->numberOfPlaces()] = 0;
-            ProductState state;
+            ProductState state{&_aut};
             state.setMarking(buf, net->numberOfPlaces());
             state.setBuchiState(buchi_init);
             return state;
@@ -40,6 +40,7 @@
 
     private:
         const PetriEngine::PetriNet *net;
+        const LTL::Structures::BuchiAutomaton _aut;
         const size_t buchi_init;
     };
 }

=== modified file 'include/LTL/Stubborn/SafeAutStubbornSet.h'
--- include/LTL/Stubborn/SafeAutStubbornSet.h	2021-05-13 09:19:31 +0000
+++ include/LTL/Stubborn/SafeAutStubbornSet.h	2021-10-17 18:21:15 +0000
@@ -48,23 +48,40 @@
             StubbornSet::reset();
             memset(_unsafe.get(), false, sizeof(bool) * _net.numberOfTransitions());
             _bad = false;
+            _has_enabled_stubborn = false;
+        }
+
+        void set_buchi_conds(PetriEngine::PQL::Condition_ptr ret_cond,
+                             PetriEngine::PQL::Condition_ptr prog_cond,
+                             PetriEngine::PQL::Condition_ptr sink_cond) {
+            _ret_cond = ret_cond;
+            _prog_cond = prog_cond;
+            _sink_cond = sink_cond;
         }
 
     protected:
         void addToStub(uint32_t t) override
         {
-            //refinement of bad: can manually check whether firing t would violate some progressing formula.
-            if (_unsafe[t] && _enabled[t]) {
-                _bad = true;
-                return;
+            // potential refinement of bad: can manually check whether firing t would violate some progressing formula.
+            if (_enabled[t]) {
+                _has_enabled_stubborn = true;
+                if (_unsafe[t]) {
+                    _bad = true;
+                    return;
+                }
             }
-            //TODO check safe-ness
             StubbornSet::addToStub(t);
         }
 
     private:
         std::unique_ptr<bool[]> _unsafe;
         bool _bad = false;
+        bool _has_enabled_stubborn = false;
+        PetriEngine::PQL::Condition_ptr _ret_cond;
+        PetriEngine::PQL::Condition_ptr _prog_cond;
+        PetriEngine::PQL::Condition_ptr _sink_cond;
+
+        void _print_debug();
     };
 }
 

=== modified file 'include/LTL/SuccessorGeneration/BuchiSuccessorGenerator.h'
--- include/LTL/SuccessorGeneration/BuchiSuccessorGenerator.h	2021-04-14 09:38:34 +0000
+++ include/LTL/SuccessorGeneration/BuchiSuccessorGenerator.h	2021-10-17 18:21:15 +0000
@@ -78,6 +78,7 @@
         {
             return (bool) aut._buchi->prop_weak();
         }
+
         size_t buchiStates() { return aut._buchi->num_states(); }
 
         Structures::BuchiAutomaton aut;
@@ -91,7 +92,6 @@
             }
         };
 
-
         bool has_invariant_self_loop(size_t state) {
             if (self_loops[state] != InvariantSelfLoop::UNKNOWN)
                 return self_loops[state] == InvariantSelfLoop::TRUE;

=== modified file 'include/LTL/SuccessorGeneration/ProductSuccessorGenerator.h'
--- include/LTL/SuccessorGeneration/ProductSuccessorGenerator.h	2021-04-29 13:19:53 +0000
+++ include/LTL/SuccessorGeneration/ProductSuccessorGenerator.h	2021-10-17 18:21:15 +0000
@@ -48,6 +48,8 @@
 
         }
 
+        const PetriEngine::PetriNet& net() const { return *_net; }
+
         [[nodiscard]] size_t initial_buchi_state() const { return buchi.initial_state_number(); };
 
         bool next(LTL::Structures::ProductState &state)
@@ -89,12 +91,12 @@
             auto buf = new PetriEngine::MarkVal[_net->numberOfPlaces() + 1];
             std::copy(_net->initial(), _net->initial() + _net->numberOfPlaces(), buf);
             buf[_net->numberOfPlaces()] = initial_buchi_state();
-            LTL::Structures::ProductState state;
+            LTL::Structures::ProductState state{&buchi.aut};
             state.setMarking(buf, _net->numberOfPlaces());
             //state.setBuchiState(initial_buchi_state());
             buchi.prepare(state.getBuchiState());
             while (next_buchi_succ(state)) {
-                states.emplace_back();
+                states.emplace_back(&buchi.aut);
                 states.back().setMarking(new PetriEngine::MarkVal[_net->numberOfPlaces() + 1], _net->numberOfPlaces());
                 std::copy(state.marking(), state.marking() + _net->numberOfPlaces(), states.back().marking());
                 states.back().setBuchiState(state.getBuchiState());
@@ -112,7 +114,7 @@
          * @param state the source state to generate successors from
          * @param sucinfo the point in the iteration to start from, as returned by `next`.
          */
-        virtual void prepare(const LTL::Structures::ProductState *state, typename SuccessorGen::sucinfo &sucinfo)
+        virtual void prepare(const LTL::Structures::ProductState *state, typename SuccessorGen::successor_info_t &sucinfo)
         {
             _successor_generator->prepare(state, sucinfo);
             fresh_marking = sucinfo.fresh();
@@ -139,7 +141,7 @@
          * @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, typename SuccessorGen::sucinfo &sucinfo)
+        bool next(Structures::ProductState &state, typename SuccessorGen::successor_info_t &sucinfo)
         {
             if (fresh_marking) {
                 fresh_marking = false;
@@ -182,7 +184,7 @@
         size_t fired() const { return _successor_generator->fired(); }
 
         //template<typename T = std::enable_if_t<std::is_same_v<SuccessorGen, PetriEngine::ReducingSuccessorGenerator>, void>>
-        void generateAll(LTL::Structures::ProductState *parent, typename SuccessorGen::sucinfo &sucinfo)
+        void generateAll(LTL::Structures::ProductState *parent, typename SuccessorGen::successor_info_t &sucinfo)
         {
             if constexpr (std::is_same_v<SuccessorGen, LTL::SpoolingSuccessorGenerator>) {
                 _successor_generator->generate_all(parent, sucinfo);
@@ -221,7 +223,7 @@
             }
         }
 
-        void pop(const typename SuccessorGen::sucinfo &sucinfo) {
+        void pop(const typename SuccessorGen::successor_info_t &sucinfo) {
             if constexpr (std::is_same_v<SuccessorGen, LTL::SpoolingSuccessorGenerator>) {
                 _successor_generator->pop(sucinfo);
             }

=== modified file 'include/LTL/SuccessorGeneration/ReachStubProductSuccessorGenerator.h'
--- include/LTL/SuccessorGeneration/ReachStubProductSuccessorGenerator.h	2021-08-04 08:13:25 +0000
+++ include/LTL/SuccessorGeneration/ReachStubProductSuccessorGenerator.h	2021-10-17 18:21:15 +0000
@@ -49,7 +49,7 @@
             std::transform(std::begin(buchi.ap_info), std::end(buchi.ap_info), std::begin(aps),
                            [](const std::pair<int, AtomicProposition> &pair) { return pair.second; });
             for (unsigned state = 0; state < buchi._buchi->num_states(); ++state) {
-                if (buchi._buchi->state_is_accepting(state)) continue;
+                //if (buchi._buchi->state_is_accepting(state)) continue;
 
                 bdd retarding = bddfalse;
                 bdd progressing = bddfalse;
@@ -61,16 +61,32 @@
                         progressing |= e.cond;
                     }
                 }
-                if ((retarding | progressing) == bddtrue) {
-                    _reach_states.insert(std::make_pair(state, BuchiEdge{progressing, toPQL(spot::bdd_to_formula(progressing, buchi.dict), aps)}));
-                }
+                bdd sink_prop = bdd_not(retarding | progressing);
+                auto prog_cond = toPQL(spot::bdd_to_formula(progressing, buchi.dict), aps);
+                auto ret_cond = toPQL(spot::bdd_to_formula(retarding, buchi.dict), aps);
+                auto sink_cond = sink_prop == bdd_false()
+                                 ? PetriEngine::PQL::BooleanCondition::FALSE_CONSTANT
+                                 : std::make_shared<PetriEngine::PQL::NotCondition>(
+                                std::make_shared<PetriEngine::PQL::OrCondition>(prog_cond, ret_cond)
+                        );
+                _reach_states.insert(std::make_pair(
+                        state,
+                        BuchiEdge{progressing | sink_prop,
+                                  ret_cond,
+                                  prog_cond,
+                                  sink_cond}));
             }
         }
 
-        void prepare(const LTL::Structures::ProductState *state, typename S::sucinfo &sucinfo) override
+        void prepare(const LTL::Structures::ProductState *state, typename S::successor_info_t &sucinfo) override
         {
-            if (auto suc = _reach_states.find(state->getBuchiState()); suc != std::end(_reach_states) && !this->guard_valid(*state, suc->second.bddCond)) {
-                (dynamic_cast<PetriEngine::StubbornSet*>(_reach.get()))->setQuery(suc->second.cond.get());
+            auto suc = _reach_states.find(state->getBuchiState());
+            // assert valid since all states are reducible when considering
+            // the sink progressing formula and key transitions in accepting states.
+            assert(suc != std::end(_reach_states));
+            if (suc != std::end(_reach_states) && !this->guard_valid(*state, suc->second.bddCond)) {
+                //_reach->setQuery(suc->second.prog_cond.get());
+                _reach->set_buchi_conds(suc->second.ret_cond, suc->second.prog_cond, suc->second.pseudo_sink_cond);
                 set_spooler(_reach.get());
             }
             else {
@@ -92,11 +108,13 @@
 
         struct BuchiEdge{
             bdd bddCond;
-            PetriEngine::PQL::Condition_ptr cond;
+            PetriEngine::PQL::Condition_ptr ret_cond;
+            PetriEngine::PQL::Condition_ptr prog_cond;
+            PetriEngine::PQL::Condition_ptr pseudo_sink_cond;
         };
 
         std::unique_ptr<Spooler> _fallback_spooler;
-        std::unique_ptr<LTL::SuccessorSpooler> _reach;
+        std::unique_ptr<LTL::SafeAutStubbornSet> _reach;
         std::unordered_map<size_t, BuchiEdge> _reach_states;
         std::vector<PetriEngine::PQL::Condition_ptr> _progressing_formulae;
 

=== modified file 'include/LTL/SuccessorGeneration/ResumingSuccessorGenerator.h'
--- include/LTL/SuccessorGeneration/ResumingSuccessorGenerator.h	2021-04-29 07:47:52 +0000
+++ include/LTL/SuccessorGeneration/ResumingSuccessorGenerator.h	2021-10-17 18:21:15 +0000
@@ -25,114 +25,107 @@
 #include "PetriEngine/Stubborn/StubbornSet.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;
-        }
-
-        [[nodiscard]] inline bool fresh() const
-        {
-            return pcounter == NoPCounter && tcounter == NoTCounter;
-        }
-
-        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();
-    };
 
     class ResumingSuccessorGenerator : public PetriEngine::SuccessorGenerator {
     public:
 
+        struct successor_info_t {
+            uint32_t pcounter;
+            uint32_t tcounter;
+            size_t buchi_state;
+            size_t last_state;
+
+            friend bool operator==(const successor_info_t &lhs, const successor_info_t &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_t &lhs, const successor_info_t &rhs) {
+                return !(rhs == lhs);
+            }
+
+            bool has_pcounter() const {
+                return pcounter != NoPCounter;
+            }
+
+            bool has_tcounter() const {
+                return tcounter != NoTCounter;
+            }
+
+            bool has_buchistate() const {
+                return buchi_state != NoBuchiState;
+            }
+
+            bool has_prev_state() const {
+                return last_state != NoLastState;
+            }
+
+            size_t state() const {
+                return last_state;
+            }
+            
+            size_t transition() const {
+                return tcounter - 1;
+            }
+            
+            [[nodiscard]] bool fresh() const {
+                return pcounter == NoPCounter && tcounter == NoTCounter;
+            }
+
+            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();
+        };
+    public:
+
         ResumingSuccessorGenerator(const PetriEngine::PetriNet *net);
 
         ResumingSuccessorGenerator(const PetriEngine::PetriNet *net, const std::shared_ptr<PetriEngine::StubbornSet> &);
 
         ResumingSuccessorGenerator(const PetriEngine::PetriNet *net,
-                                   std::vector<std::shared_ptr<PetriEngine::PQL::Condition> > &queries);
+                std::vector<std::shared_ptr<PetriEngine::PQL::Condition> > &queries);
 
         ResumingSuccessorGenerator(const PetriEngine::PetriNet *net,
-                                   const std::shared_ptr<PetriEngine::PQL::Condition> &query);
+                const std::shared_ptr<PetriEngine::PQL::Condition> &query);
 
         ~ResumingSuccessorGenerator() override = default;
 
-        void prepare(const PetriEngine::Structures::State *state, const successor_info &sucinfo);
-
-
-        bool next(PetriEngine::Structures::State &write, successor_info &sucinfo)
-        {
+        void prepare(const PetriEngine::Structures::State *state, const successor_info_t &sucinfo);
+
+        bool next(PetriEngine::Structures::State &write, successor_info_t &sucinfo) {
             bool has_suc = PetriEngine::SuccessorGenerator::next(write);
-            getSuccInfo(sucinfo);
+            get_succ_info(sucinfo);
             return has_suc;
         }
 
-        uint32_t fired() const
-        {
+        uint32_t fired() const {
             return _suc_tcounter - 1;
         }
 
-        const PetriEngine::MarkVal *getParent() const
-        {
+        const PetriEngine::MarkVal *get_parent() const {
             return _parent->marking();
         }
 
-
-        size_t last_transition() const
-        {
+        size_t last_transition() const {
             return _suc_tcounter == std::numeric_limits<uint32_t>::max() ? std::numeric_limits<uint32_t>::max() :
-                   _suc_tcounter - 1;
-        }
-
-        using sucinfo = successor_info;
-
-        static constexpr sucinfo _initial_suc_info{
-                successor_info::NoPCounter,
-                successor_info::NoTCounter,
-                successor_info::NoBuchiState,
-                successor_info::NoLastState
-        };
-
-        static constexpr auto initial_suc_info() { return _initial_suc_info; }
+                    _suc_tcounter - 1;
+        }
+
+        static constexpr successor_info_t _initial_suc_info{
+            successor_info_t::NoPCounter,
+            successor_info_t::NoTCounter,
+            successor_info_t::NoBuchiState,
+            successor_info_t::NoLastState};
+
+        static constexpr auto initial_suc_info() {
+            return _initial_suc_info;
+        }
 
     private:
-        void getSuccInfo(successor_info &sucinfo) const;
+        void get_succ_info(successor_info_t &sucinfo) const;
 
         //friend class ReducingSuccessorGenerator;
     };

=== modified file 'include/LTL/SuccessorGeneration/SpoolingSuccessorGenerator.h'
--- include/LTL/SuccessorGeneration/SpoolingSuccessorGenerator.h	2021-04-30 07:02:31 +0000
+++ include/LTL/SuccessorGeneration/SpoolingSuccessorGenerator.h	2021-10-17 18:21:15 +0000
@@ -1,16 +1,16 @@
 /* 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/>.
  */
@@ -34,18 +34,27 @@
             _statebuf.setMarking(new PetriEngine::MarkVal[net->numberOfPlaces() + 1], net->numberOfPlaces());
         }
 
-        struct sucinfo {
+        struct successor_info_t {
             SuccessorQueue<> successors;
             size_t buchi_state;
             size_t last_state;
-
-            sucinfo(size_t buchiState, size_t lastState) : buchi_state(buchiState), last_state(lastState) {}
-
-            [[nodiscard]] inline bool has_prev_state() const
+            size_t _transition;
+
+            successor_info_t(size_t buchiState, size_t lastState) : buchi_state(buchiState), last_state(lastState) {}
+
+            [[nodiscard]] bool has_prev_state() const
             {
                 return last_state != NoLastState;
             }
 
+            size_t state() const {
+                return last_state;
+            }
+
+            size_t transition() const {
+                return _transition;
+            }
+
             [[nodiscard]] bool fresh() const { return buchi_state == NoBuchiState && last_state == NoLastState; }
 
             static constexpr auto NoBuchiState = std::numeric_limits<size_t>::max();
@@ -62,9 +71,9 @@
             _heuristic = heuristic;
         }
 
-        [[nodiscard]] static sucinfo initial_suc_info()
+        [[nodiscard]] static successor_info_t initial_suc_info()
         {
-            return sucinfo{sucinfo::NoBuchiState, sucinfo::NoLastState};
+            return successor_info_t{successor_info_t::NoBuchiState, successor_info_t::NoLastState};
         }
 
         bool prepare(const PetriEngine::Structures::State *state)
@@ -78,14 +87,15 @@
         }
 
 
-        void prepare(const Structures::ProductState *state, sucinfo &sucinfo)
+        void prepare(const Structures::ProductState *state, successor_info_t &sucinfo)
         {
             assert(_spooler != nullptr);
 
             PetriEngine::SuccessorGenerator::prepare(state);
             if (sucinfo.successors == nullptr) {
                 uint32_t tid;
-                _spooler->prepare(state);
+                bool res = _spooler->prepare(state);
+                //assert(!res/* || !_net.deadlocked(state->marking())*/);
                 if (!_heuristic || !_heuristic->has_heuristic(*state)) {
                     uint32_t nsuc = 0;
                     // generate list of transitions that generate a successor.
@@ -95,7 +105,7 @@
                         assert(nsuc <= _net.numberOfTransitions());
                     }
                     sucinfo.successors = SuccessorQueue(_transbuf.get(), nsuc);
-
+                    assert((res && !sucinfo.successors.empty()) || !res);
                 } else {
                     // list of (transition, weight)
                     _heuristic->prepare(*state);
@@ -113,7 +123,7 @@
                 }
             }
         }
-        bool next(Structures::ProductState &state, sucinfo &sucinfo)
+        bool next(Structures::ProductState &state, successor_info_t &sucinfo)
         {
             assert(sucinfo.successors != nullptr);
             if (sucinfo.successors.empty()) {
@@ -124,6 +134,7 @@
                 return false;
             }
             _last = sucinfo.successors.front();
+            sucinfo._transition = _last;
 #ifndef NDEBUG
             //std::cerr << "Firing " << _net.transitionNames()[_last] << std::endl;
 #endif
@@ -134,7 +145,7 @@
 
         [[nodiscard]] uint32_t fired() const { return _last; }
 
-        void generate_all(LTL::Structures::ProductState *parent, sucinfo &sucinfo)
+        void generate_all(LTL::Structures::ProductState *parent, successor_info_t &sucinfo)
         {
             assert(_spooler != nullptr);
             assert(sucinfo.successors != nullptr);
@@ -200,7 +211,7 @@
             _heuristic->push(fired());
         }
 
-        void pop(const sucinfo &sc) {
+        void pop(const successor_info_t &sc) {
             if (_heuristic && sc.successors.has_consumed())
                 _heuristic->pop(sc.successors.last_pop());
         }

=== modified file 'include/PetriEngine/Reducer.h'
--- include/PetriEngine/Reducer.h	2021-07-07 13:19:23 +0000
+++ include/PetriEngine/Reducer.h	2021-10-17 18:21:15 +0000
@@ -1,4 +1,4 @@
-/* 
+/*
  * File:   Reducer.h
  * Author: srba
  *
@@ -19,34 +19,34 @@
 namespace PetriEngine {
 
     using ArcIter = std::vector<Arc>::iterator;
-    
+
     class PetriNetBuilder;
-        
+
     class QueryPlaceAnalysisContext : public PQL::AnalysisContext {
         std::vector<uint32_t> _placeInQuery;
         bool _deadlock;
     public:
 
-        QueryPlaceAnalysisContext(const std::unordered_map<std::string, uint32_t>& pnames, const std::unordered_map<std::string, uint32_t>& tnames, const PetriNet* net) 
+        QueryPlaceAnalysisContext(const std::unordered_map<std::string, uint32_t>& pnames, const std::unordered_map<std::string, uint32_t>& tnames, const PetriNet* net)
         : PQL::AnalysisContext(pnames, tnames, net) {
             _placeInQuery.resize(_placeNames.size(), 0);
             _deadlock = false;
         };
-        
+
         virtual ~QueryPlaceAnalysisContext()
         {
         }
-        
+
         uint32_t*  getQueryPlaceCount(){
             return _placeInQuery.data();
         }
 
         bool hasDeadlock() { return _deadlock; }
-        
+
         virtual void setHasDeadlock() override {
             _deadlock = true;
         };
-        
+
         ResolutionResult resolve(const std::string& identifier, bool place) override {
             if(!place) return PQL::AnalysisContext::resolve(identifier, false);
             ResolutionResult result;
@@ -61,7 +61,7 @@
                 _placeInQuery[i]++;
                 return result;
             }
-            
+
             return result;
         }
 
@@ -70,7 +70,7 @@
    struct ExpandedArc
    {
        ExpandedArc(std::string place, size_t weight) : place(place), weight(weight) {}
-       
+
         friend std::ostream& operator<<(std::ostream& os, ExpandedArc const & ea) {
             for(size_t i = 0; i < ea.weight; ++i)
             {
@@ -78,18 +78,18 @@
             }
             return os;
         }
-       
-        std::string place;        
+
+        std::string place;
         size_t weight;
    };
-    
+
     class Reducer {
     public:
         Reducer(PetriNetBuilder*);
         ~Reducer();
         void Print(QueryPlaceAnalysisContext& context); // prints the net, just for debugging
         void Reduce(QueryPlaceAnalysisContext& context, int enablereduction, bool reconstructTrace, int timeout, bool remove_loops, bool remove_consumers, bool next_safe, std::vector<uint32_t>& reductions);
-        
+
         size_t RemovedTransitions() const {
             return _removedTransitions;
         }
@@ -115,9 +115,9 @@
                 << "Applications of rule K: " << _ruleK << std::endl;
         }
 
-        void postFire(std::ostream&, const std::string& transition);
-        void extraConsume(std::ostream&, const std::string& transition);
-        void initFire(std::ostream&);
+        void postFire(std::ostream&, const std::string& transition) const;
+        void extraConsume(std::ostream&, const std::string& transition) const;
+        void initFire(std::ostream&) const;
 
     private:
         size_t _removedTransitions = 0;
@@ -146,7 +146,7 @@
 
         std::string getTransitionName(uint32_t transition);
         std::string getPlaceName(uint32_t place);
-        
+
         PetriEngine::Transition& getTransition(uint32_t transition);
         ArcIter getOutArc(PetriEngine::Transition&, uint32_t place);
         ArcIter getInArc(uint32_t place, PetriEngine::Transition&);
@@ -154,14 +154,14 @@
         void skipTransition(uint32_t);
         void skipPlace(uint32_t);
         std::string newTransName();
-        
+
         bool consistent();
         bool hasTimedout() const {
             auto end = std::chrono::high_resolution_clock::now();
             auto diff = std::chrono::duration_cast<std::chrono::seconds>(end - _timer);
             return (diff.count() >= _timeout);
         }
-        
+
         std::vector<std::string> _initfire;
         std::unordered_map<std::string, std::vector<std::string>> _postfire;
         std::unordered_map<std::string, std::vector<ExpandedArc>> _extraconsume;
@@ -171,7 +171,7 @@
         std::vector<uint32_t> _skipped_trans;
     };
 
-    
+
 
 
 }

=== modified file 'include/PetriEngine/Structures/StateSet.h'
--- include/PetriEngine/Structures/StateSet.h	2021-04-29 07:47:52 +0000
+++ include/PetriEngine/Structures/StateSet.h	2021-10-17 18:21:15 +0000
@@ -42,10 +42,11 @@
                 _maxPlaceBound = std::vector<uint32_t>(net.numberOfPlaces(), 0);
                 _sp = binarywrapper_t(sizeof(uint32_t) * _nplaces * 8);
             }
-	    virtual ~StateSetInterface()
-	    {
-		_sp.release();
-	    }
+            
+            virtual ~StateSetInterface()
+            {
+                _sp.release();
+            }
             
             virtual std::pair<bool, size_t> add(const State& state) = 0;
             
@@ -59,10 +60,6 @@
             
             virtual std::pair<size_t, size_t> getHistory(size_t markingid) = 0;
 
-            virtual void setHistory2(size_t id, size_t transition) = 0;
-
-            virtual std::pair<size_t, size_t> getHistory2(size_t markingid) = 0;
-            
         protected:
             size_t _discovered;
             uint32_t _kbound;
@@ -235,14 +232,6 @@
                 return std::make_pair(0,0); 
             }
 
-            virtual void setHistory2(size_t id, size_t transition) override {}
-
-            virtual std::pair<size_t, size_t> getHistory2(size_t markingid) override
-            {
-                assert(false);
-                return std::make_pair(std::numeric_limits<std::size_t>::max(), std::numeric_limits<std::size_t>::max());
-            }
-            
         private:
             ptrie_t _trie;
         };
@@ -254,8 +243,6 @@
             {
                 ptrie::uint parent;
                 ptrie::uint transition = std::numeric_limits<ptrie::uint>::max();
-                ptrie::uint parent2;
-                ptrie::uint transition2 = std::numeric_limits<ptrie::uint>::max();
             };
             
         private:
@@ -301,21 +288,6 @@
                 return std::pair<size_t, size_t>(t.parent, t.transition);
             }
 
-            virtual void setHistory2(size_t id, size_t transition) override {
-                traceable_t &t = _trie.get_data(id);
-                t.parent2 = _parent;
-                t.transition2 = transition;
-            }
-
-            virtual std::pair<size_t, size_t> getHistory2(size_t markingid) override {
-                traceable_t &t = _trie.get_data(markingid);
-                return std::pair<size_t, size_t>(t.parent2, t.transition2);
-            }
-
-            void setParent(size_t id) {
-                _parent = id;
-            }
-            
         private:
             ptrie_t _trie;
             size_t _parent = 0;

=== modified file 'include/PetriEngine/Structures/light_deque.h'
--- include/PetriEngine/Structures/light_deque.h	2021-03-23 14:10:04 +0000
+++ include/PetriEngine/Structures/light_deque.h	2021-10-17 18:21:15 +0000
@@ -1,4 +1,4 @@
-/* 
+/*
  * File:   light_deque.h
  * Author: Peter G. Jensen <[e-mail]>
  *
@@ -18,30 +18,40 @@
         size_t _front = 0;
         size_t _back = 0;
         size_t _size = 0;
-        std::unique_ptr<T[]> _data;
+        T* _data = nullptr;
     public:
         light_deque(size_t initial_size = 64)
         {
             if(initial_size == 0) initial_size = 1;
-            _data.reset(new T[initial_size]);
+            _data = (T*)new uint8_t[initial_size*sizeof(T)]; // TODO, revisit with cast and initialization
             _size = initial_size;
         }
 
         light_deque<T> &operator=(const light_deque<T> &other) {
-            _front = other._front;
-            _back = other._back;
+            for(auto& e : *this)
+                e.~T();
+            delete[] (uint8_t*)_data;
+            _front = 0;
+            _back = 0;
             _size = other.size();
-            _data.reset(new T[_size]);
-            memcpy(_data.get(), other._data.get(), _size * sizeof(T));
+            _data = (T*)new uint8_t[_size*sizeof(T)];
+            for(auto& e : other)
+                push_back(e);
             return *this;
         }
 
-        light_deque(light_deque &&) noexcept = default;
-        light_deque &operator=(light_deque &&) noexcept = default;
+        ~light_deque() {
+            for(auto& e : *this)
+            {
+                e.~T();
+            }
+            delete[] (uint8_t*)_data;
+            _data = nullptr;
+        }
 
         void push_back(const T& element)
         {
-            _data.get()[_back] = element;
+            new (&_data[_back]) T(element);
             ++_back;
             if(_back == _size)
             {
@@ -51,7 +61,7 @@
 
         void push_back(T&& element)
         {
-            _data.get()[_back] = element;
+            new (&_data[_back]) T(std::move(element));
             ++_back;
             if(_back == _size) {
                 expand();
@@ -62,39 +72,88 @@
         {
             return _front == _back;
         }
-        
+
         size_t size() const
         {
             return _back - _front;
         }
-        
-        T front() const
-        {
-            return _data.get()[_front];
-        }
-        const T& front() {
-            return _data.get()[_front];
+
+        const T& front() const
+        {
+            return _data[_front];
+        }
+
+        T& front() {
+            return _data[_front];
+        }
+
+        const T& back() const
+        {
+            return _data[_back - 1];
+        }
+
+        T& back() {
+            return _data[_back - 1];
         }
 
         void pop_front()
         {
+            _data[_front].~T();
             ++_front;
             if(_front >= _back)
             {
                 _front = _back = 0;
             }
         }
-        
+
+        void pop_back()
+        {
+            if(_back > _front)
+            {
+                --_back;
+                _data[_back].~T();
+            }
+            if(_back == _front)
+                clear();
+        }
+
         void clear()
         {
+            for(auto& e : *this)
+                e.~T();
             _front = _back = 0;
         }
-    private:
+
+        T* begin() {
+            return &front();
+        }
+
+        T* end() {
+            return &_data[_back];
+        }
+
+        const T* begin() const {
+            return &front();
+        }
+
+        const T* end() const {
+            return &_data[_back];
+        }
+
+        private:
         void expand() {
-            std::unique_ptr<T[]> ndata(new T[_size*2]);
-            memcpy(ndata.get(), _data.get(), _size*sizeof(T));
+            T* ndata = (T*)new uint8_t[_size*2*sizeof(T)];
+            size_t n = 0;
+            for(auto& e : *this)
+            {
+                new (ndata + n) T(std::move(e));
+                ++n;
+            }
             _size *= 2;
-            _data.swap(ndata);
+            _back = (_back - _front);
+            _front = 0;
+            std::swap(_data, ndata);
+            delete[] (uint8_t*)ndata;
         }
 };
 

=== modified file 'include/PetriEngine/SuccessorGenerator.h'
--- include/PetriEngine/SuccessorGenerator.h	2021-03-19 11:48:52 +0000
+++ include/PetriEngine/SuccessorGenerator.h	2021-10-17 18:21:15 +0000
@@ -4,7 +4,7 @@
  * and open the template in the editor.
  */
 
-/* 
+/*
  * File:   SuccessorGenerator.h
  * Author: Peter G. Jensen
  *
@@ -32,13 +32,15 @@
     virtual bool next(Structures::State& write);
     uint32_t fired() const
     {
-        return _suc_tcounter -1;
+        return _suc_tcounter == std::numeric_limits<uint32_t>::max() ? std::numeric_limits<uint32_t>::max() : _suc_tcounter - 1;
     }
 
     const MarkVal* getParent() const {
         return _parent->marking();
     }
 
+    const PetriNet& net() const { return _net; }
+
     void reset();
 
     /**
@@ -64,8 +66,6 @@
      */
     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;
 

=== modified file 'src/LTL/Algorithm/NestedDepthFirstSearch.cpp'
--- src/LTL/Algorithm/NestedDepthFirstSearch.cpp	2021-08-10 13:44:22 +0000
+++ src/LTL/Algorithm/NestedDepthFirstSearch.cpp	2021-10-17 18:21:15 +0000
@@ -18,186 +18,186 @@
 #include "LTL/Algorithm/NestedDepthFirstSearch.h"
 
 namespace LTL {
-    template<typename S, typename W>
-    bool NestedDepthFirstSearch<S, W>::isSatisfied()
+    template<typename S>
+    bool NestedDepthFirstSearch<S>::isSatisfied()
     {
         this->is_weak = this->successorGenerator->is_weak() && this->shortcircuitweak;
         dfs();
-        return !violation;
-    }
-
-    template<typename S, typename W>
-    void NestedDepthFirstSearch<S, W>::dfs()
-    {
-        std::stack<size_t> call_stack;
-        std::stack<StackEntry> todo;
-
-        State working = factory.newState();
-        State curState = factory.newState();
-
-        {
-
+        return !_violation;
+    }
+
+    template<typename S>
+    std::pair<bool,size_t> NestedDepthFirstSearch<S>::mark(State& state, const uint8_t MARKER)
+    {
+        auto[_, stateid] = _states.add(state);
+        if (stateid == std::numeric_limits<size_t>::max()) {
+            return std::make_pair(false, stateid);
+        }
+
+        auto r = _markers[stateid];
+        _markers[stateid] = (MARKER | r);
+        const bool is_new = (r & MARKER) == 0;
+        if(is_new)
+        {
+            ++_mark_count[MARKER];
+            ++this->_discovered;
+        }
+        return std::make_pair(is_new, stateid);
+    }
+
+    template<typename S>
+    void NestedDepthFirstSearch<S>::dfs()
+    {
+
+        light_deque<StackEntry> todo;
+        light_deque<StackEntry> nested_todo;
+
+        State working = this->_factory.newState();
+        State curState = this->_factory.newState();
+
+        {
             std::vector<State> initial_states = this->successorGenerator->makeInitialState();
             for (auto &state : initial_states) {
-                auto res = states.add(state);
+                auto res = _states.add(state);
                 if (res.first) {
-                    assert(res.first);
-                    todo.push(StackEntry{res.second, S::initial_suc_info()});
-                    this->_discovered++;
+                    todo.push_back(StackEntry{res.second, S::initial_suc_info()});
+                    ++this->_discovered;
                 }
             }
         }
 
         while (!todo.empty()) {
-            auto &top = todo.top();
-            states.decode(curState, top.id);
-            this->successorGenerator->prepare(&curState, top.sucinfo);
-            if (top.sucinfo.has_prev_state()) {
-                states.decode(working, top.sucinfo.last_state);
+            auto &top = todo.back();
+            _states.decode(curState, top._id);
+            this->successorGenerator->prepare(&curState, top._sucinfo);
+            if (top._sucinfo.has_prev_state()) {
+                _states.decode(working, top._sucinfo.last_state);
             }
-            if (!this->successorGenerator->next(working, top.sucinfo)) {
+            if (!this->successorGenerator->next(working, top._sucinfo)) {
                 // no successor
-                todo.pop();
-                if (this->successorGenerator->isAccepting(curState)) {
-                    seed = &curState;
-                    ndfs(curState);
-                    if (violation) {
-                        if constexpr (SaveTrace) {
-                            std::stack<std::pair<size_t, size_t>> transitions;
-                            size_t next = top.id;
-                            states.decode(working, next);
-                            while (!this->successorGenerator->isInitialState(working)) {
-                                auto[parent, transition] = states.getHistory(next);
-                                transitions.push(std::make_pair(parent, transition));
-                                next = parent;
-                                states.decode(working, next);
-                            }
-                            printTrace(transitions);
+                if (curState.is_accepting()) {
+                    if(this->successorGenerator->has_invariant_self_loop(curState))
+                        _violation = true;
+                    else
+                        ndfs(curState, nested_todo);
+                    if (_violation) {
+                        if (_print_trace) {
+                            print_trace(todo, nested_todo);
                         }
                         return;
                     }
                 }
+                todo.pop_back();
             } else {
-                auto[_, stateid] = states.add(working);
+                auto [is_new, stateid] = mark(working, MARKER1);
                 if (stateid == std::numeric_limits<size_t>::max()) {
                     continue;
                 }
-                auto[it, is_new] = mark1.insert(stateid);
-                top.sucinfo.last_state = stateid;
+                top._sucinfo.last_state = stateid;
                 if (is_new) {
-                    if constexpr (SaveTrace) {
-                        states.setParent(top.id);
-                        states.setHistory(stateid, this->successorGenerator->fired());
+                    ++this->_discovered;
+                    if(this->successorGenerator->isAccepting(curState) &&
+                       this->successorGenerator->has_invariant_self_loop(curState))
+                    {
+                        _violation = true;
+                        if(_print_trace)
+                            print_trace(todo, nested_todo);
+                        return;
                     }
-                    this->_discovered++;
-                    todo.push(StackEntry{stateid, S::initial_suc_info()});
+                    todo.push_back(StackEntry{stateid, S::initial_suc_info()});
                 }
             }
         }
     }
 
-    template<typename S, typename W>
-    void NestedDepthFirstSearch<S, W>::ndfs(State &state)
+    template<typename S>
+    void NestedDepthFirstSearch<S>::ndfs(const State &state, light_deque<StackEntry>& nested_todo)
     {
-        std::stack<StackEntry> todo;
-
-        State working = factory.newState();
-        State curState = factory.newState();
-
-        todo.push(StackEntry{states.add(state).second, S::initial_suc_info()});
-
-        while (!todo.empty()) {
-            auto &top = todo.top();
-            states.decode(curState, top.id);
-            this->successorGenerator->prepare(&curState, top.sucinfo);
-            if (top.sucinfo.has_prev_state()) {
-                states.decode(working, top.sucinfo.last_state);
+
+        State working = this->_factory.newState();
+        State curState = this->_factory.newState();
+
+        nested_todo.push_back(StackEntry{_states.add(state).second, S::initial_suc_info()});
+
+        while (!nested_todo.empty()) {
+            auto &top = nested_todo.back();
+            _states.decode(curState, top._id);
+            this->successorGenerator->prepare(&curState, top._sucinfo);
+            if (top._sucinfo.has_prev_state()) {
+                _states.decode(working, top._sucinfo.last_state);
             }
-            if (!this->successorGenerator->next(working, top.sucinfo)) {
-                todo.pop();
+            if (!this->successorGenerator->next(working, top._sucinfo)) {
+                nested_todo.pop_back();
             } else {
                 if (this->is_weak && !this->successorGenerator->isAccepting(working)) {
                     continue;
                 }
-                if (working == *seed) {
-                    violation = true;
-                    if constexpr (SaveTrace) {
-                        auto[_, stateid] = states.add(working);
-                        auto seedId = stateid;
-                        states.setHistory2(stateid, this->successorGenerator->fired());
-                        size_t next = stateid;
-                        // follow trace until back at seed state.
-                        do {
-                            auto[state, transition] = states.getHistory2(next);
-                            nested_transitions.push(std::make_pair(state, transition));
-                            next = state;
-                        } while (next != seedId);
-                    }
+                if (working == state) {
+                    _violation = true;
                     return;
                 }
-                auto[_, stateid] = states.add(working);
-                if (stateid == std::numeric_limits<size_t>::max()) {
+                auto [is_new, stateid] = mark(working, MARKER2);
+                if (stateid == std::numeric_limits<size_t>::max())
                     continue;
-                }
-                auto[it, is_new] = mark2.insert(stateid);
-                top.sucinfo.last_state = stateid;
+                top._sucinfo.last_state = stateid;
                 if (is_new) {
-                    if constexpr (SaveTrace) {
-                        states.setParent(top.id);
-                        states.setHistory2(stateid, this->successorGenerator->fired());
-                    }
-                    this->_discovered++;
-                    todo.push(StackEntry{stateid, S::initial_suc_info()});
+                    nested_todo.push_back(StackEntry{stateid, S::initial_suc_info()});
                 }
-
             }
         }
     }
 
-    template<typename S, typename W>
-    void NestedDepthFirstSearch<S, W>::printStats(std::ostream &os)
+    template<typename S>
+    void NestedDepthFirstSearch<S>::printStats(std::ostream &os)
     {
         std::cout << "STATS:\n"
-                  << "\tdiscovered states:          " << states.discovered() << std::endl
-                  << "\tmax tokens:                 " << states.max_tokens() << std::endl
-                  << "\texplored states:            " << mark1.size() << std::endl
-                  << "\texplored states (nested):   " << mark2.size() << std::endl;
+                  << "\tdiscovered states:          " << _states.discovered() << std::endl
+                  << "\tmax tokens:                 " << _states.max_tokens() << std::endl
+                  << "\texplored states:            " << _mark_count[MARKER1] << std::endl
+                  << "\texplored states (nested):   " << _mark_count[MARKER2] << std::endl;
     }
 
 
-    template<typename S, typename W>
-    void NestedDepthFirstSearch<S, W>::printTrace(std::stack<std::pair<size_t, size_t>> &transitions, std::ostream &os)
+    template<typename S>
+    void NestedDepthFirstSearch<S>::print_trace(light_deque<StackEntry>& _todo, light_deque<StackEntry>& _nested_todo, std::ostream &os)
     {
-        State state = factory.newState();
         os << "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n"
               "<trace>\n";
-        while (!transitions.empty()) {
-            auto[stateid, transition] = transitions.top();
-            states.decode(state, stateid);
-            this->printTransition(transition, state, os) << std::endl;
-            transitions.pop();
+        if(this->_reducer)
+            this->_reducer->initFire(os);
+        size_t loop_id = std::numeric_limits<size_t>::max();
+        // last element of todo-stack always has a "garbage" transition, it is the
+        // current working element OR first element of nested.
+
+        if(!_todo.empty())
+            _todo.pop_back();
+        if(!_nested_todo.empty()) {
+            // here the last state is significant
+            // of the successor is the check that demonstrates the violation.
+            loop_id = _nested_todo.back()._id;
+            _nested_todo.pop_back();
         }
-        this->printLoop(os);
-        while (!nested_transitions.empty()) {
-            auto[stateid, transition] = nested_transitions.top();
-            states.decode(state, stateid);
 
-            this->printTransition(transition, state, os) << std::endl;
-            nested_transitions.pop();
+        for(auto* stck : {&_todo, &_nested_todo})
+        {
+            while(!(*stck).empty())
+            {
+                auto& top = (*stck).front();
+                if(top._id == loop_id)
+                {
+                    this->printLoop(os);
+                    loop_id = std::numeric_limits<size_t>::max();
+                }
+                this->printTransition(top._sucinfo.transition(), os) << std::endl;
+                (*stck).pop_front();
+            }
         }
         os << std::endl << "</trace>" << std::endl;
     }
 
     template
-    class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, LTL::Structures::BitProductStateSet<>>;
-
-    template
-    class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, LTL::Structures::TraceableBitProductStateSet<>>;
-
-    template
-    class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, LTL::Structures::BitProductStateSet<>>;
-
-    template
-    class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, LTL::Structures::TraceableBitProductStateSet<>>;
-
+    class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator>;
+
+    template
+    class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator>;
 }

=== modified file 'src/LTL/Algorithm/TarjanModelChecker.cpp'
--- src/LTL/Algorithm/TarjanModelChecker.cpp	2021-08-10 13:44:22 +0000
+++ src/LTL/Algorithm/TarjanModelChecker.cpp	2021-10-17 18:21:15 +0000
@@ -24,50 +24,62 @@
     {
         this->is_weak = this->successorGenerator->is_weak() && this->shortcircuitweak;
         std::vector<State> initial_states = this->successorGenerator->makeInitialState();
-        State working = factory.newState();
-        State parent = factory.newState();
+        State working = this->_factory.newState();
+        State parent = this->_factory.newState();
         for (auto &state : initial_states) {
-            const auto res = seen.add(state);
+            const auto res = _seen.add(state);
             if (res.first) {
                 push(state, res.second);
             }
-            while (!dstack.empty() && !violation) {
-                DEntry &dtop = dstack.top();
+            while (!_dstack.empty() && !_violation) {
+                DEntry &dtop = _dstack.top();
                 // write next successor state to working.
                 if (!nexttrans(working, parent, dtop)) {
                     ++this->stats.expanded;
+#ifndef NDEBUG
+                    std::cerr << "backtrack\n";
+#endif
                     pop();
                     continue;
                 }
+                auto fired = this->successorGenerator->fired();
+#ifndef NDEBUG
+                if (fired >= std::numeric_limits<uint32_t>::max() - 3) {
+                    std::cerr << "looping\n";
+                }
+                else {
+                    //state.print(*this->net, std::cerr); std::cerr << ": <transition id='" << this->net->transitionNames()[fired] << "'>" << std::endl ;
+                }
+#endif
                 ++this->stats.explored;
-                const auto[isnew, stateid] = seen.add(working);
+                const auto[isnew, stateid] = _seen.add(working);
                 if (stateid == std::numeric_limits<idx_t>::max()) {
                     continue;
                 }
 
                 if constexpr (SaveTrace) {
                     if (isnew) {
-                        seen.setHistory(stateid, this->successorGenerator->fired());
+                        _seen.setHistory(stateid, this->successorGenerator->fired());
                     }
                 }
 
-                dtop.sucinfo.last_state = stateid;
+                dtop._sucinfo.last_state = stateid;
 
                 // lookup successor in 'hash' table
-                auto suc_pos = chash[hash(stateid)];
-                auto marking = seen.getMarkingId(stateid);
-                while (suc_pos != std::numeric_limits<idx_t>::max() && cstack[suc_pos].stateid != stateid) {
-                    if constexpr (IsSpooling) {
-                        if (cstack[suc_pos].dstack && seen.getMarkingId(cstack[suc_pos].stateid) == marking) {
-                            this->successorGenerator->generateAll(&parent, dtop.sucinfo);
+                auto suc_pos = _chash[hash(stateid)];
+                auto marking = _seen.getMarkingId(stateid);
+                while (suc_pos != std::numeric_limits<idx_t>::max() && _cstack[suc_pos]._stateid != stateid) {
+                    if constexpr (_is_spooling) {
+                        if (_cstack[suc_pos]._dstack && _seen.getMarkingId(_cstack[suc_pos]._stateid) == marking) {
+                            this->successorGenerator->generateAll(&parent, dtop._sucinfo);
                         }
                     }
-                    suc_pos = cstack[suc_pos].next;
+                    suc_pos = _cstack[suc_pos]._next;
                 }
                 if (suc_pos != std::numeric_limits<idx_t>::max()) {
-                    if constexpr (IsSpooling) {
-                        if (cstack[suc_pos].dstack) {
-                            this->successorGenerator->generateAll(&parent, dtop.sucinfo);
+                    if constexpr (_is_spooling) {
+                        if (_cstack[suc_pos]._dstack) {
+                            this->successorGenerator->generateAll(&parent, dtop._sucinfo);
                         }
                     }
                     // we found the successor, i.e. there's a loop!
@@ -75,24 +87,24 @@
                     update(suc_pos);
                     continue;
                 }
-                if (store.find(stateid) == std::end(store)) {
+                if (_store.find(stateid) == std::end(_store)) {
                     push(working, stateid);
                 }
             }
             if constexpr (SaveTrace) {
                 // print counter-example if it exists.
-                if (violation) {
+                if (_violation) {
                     std::stack<DEntry> revstack;
-                    while (!dstack.empty()) {
-                        revstack.push(std::move(dstack.top()));
-                        dstack.pop();
+                    while (!_dstack.empty()) {
+                        revstack.push(std::move(_dstack.top()));
+                        _dstack.pop();
                     }
                     printTrace(std::move(revstack));
                     return false;
                 }
             }
         }
-        return !violation;
+        return !_violation;
     }
 
     /**
@@ -101,20 +113,19 @@
      */
     template<template<typename, typename...> typename S, typename G, bool SaveTrace, typename... Spooler>
     void TarjanModelChecker<S, G, SaveTrace, Spooler...>::push(State &state, size_t stateid) {
-        const auto ctop = static_cast<idx_t>(cstack.size());
+        const auto ctop = static_cast<idx_t>(_cstack.size());
         const auto h = hash(stateid);
-        cstack.emplace_back(ctop, stateid, chash[h]);
-        chash[h] = ctop;
-        dstack.push(DEntry{ctop});
+        _cstack.emplace_back(ctop, stateid, _chash[h]);
+        _chash[h] = ctop;
+        _dstack.push(DEntry{ctop});
         if (this->successorGenerator->isAccepting(state)) {
-            astack.push(ctop);
-            if (this->successorGenerator->has_invariant_self_loop(state) && !SaveTrace){
-                //std::cerr << "Invariant self loop found. Violation is true" << std::endl;
-                violation = true;
-                invariant_loop = true;
+            _astack.push(ctop);
+            if (this->successorGenerator->has_invariant_self_loop(state)){
+                _violation = true;
+                _invariant_loop = true;
             }
         }
-        if constexpr (IsSpooling) {
+        if constexpr (_is_spooling) {
             this->successorGenerator->push();
         }
     }
@@ -122,27 +133,27 @@
     template<template<typename, typename...> typename S, typename G, bool SaveTrace, typename... Spooler>
     void TarjanModelChecker<S, G, SaveTrace, Spooler...>::pop()
     {
-        const auto p = dstack.top().pos;
-        dstack.pop();
-        cstack[p].dstack = false;
-        if (cstack[p].lowlink == p) {
-            while (cstack.size() > p) {
+        const auto p = _dstack.top()._pos;
+        _dstack.pop();
+        _cstack[p]._dstack = false;
+        if (_cstack[p]._lowlink == p) {
+            while (_cstack.size() > p) {
                 popCStack();
             }
         } else if (this->is_weak) {
-            State state = factory.newState();
-            seen.decode(state, cstack[p].stateid);
+            State state = this->_factory.newState();
+            _seen.decode(state, _cstack[p]._stateid);
             if (!this->successorGenerator->isAccepting(state)) {
                 popCStack();
             }
         }
-        if (!astack.empty() && p == astack.top()) {
-            astack.pop();
+        if (!_astack.empty() && p == _astack.top()) {
+            _astack.pop();
         }
-        if (!dstack.empty()) {
+        if (!_dstack.empty()) {
             update(p);
-            if constexpr (IsSpooling) {
-                this->successorGenerator->pop(dstack.top().sucinfo);
+            if constexpr (_is_spooling) {
+                this->successorGenerator->pop(_dstack.top()._sucinfo);
             }
         }
     }
@@ -150,28 +161,28 @@
     template<template<typename, typename...> typename S, typename G, bool SaveTrace, typename... Spooler>
     void TarjanModelChecker<S, G, SaveTrace, Spooler...>::popCStack()
     {
-        auto h = hash(cstack.back().stateid);
-        store.insert(cstack.back().stateid);
-        chash[h] = cstack.back().next;
-        cstack.pop_back();
+        auto h = hash(_cstack.back()._stateid);
+        _store.insert(_cstack.back()._stateid);
+        _chash[h] = _cstack.back()._next;
+        _cstack.pop_back();
     }
 
     template<template<typename, typename...> typename S, typename G, bool SaveTrace, typename... Spooler>
     void TarjanModelChecker<S, G, SaveTrace, Spooler...>::update(idx_t to)
     {
-        const auto from = dstack.top().pos;
-        assert(cstack[to].lowlink != std::numeric_limits<idx_t>::max() && cstack[from].lowlink != std::numeric_limits<idx_t>::max());
-        if (cstack[to].lowlink <= cstack[from].lowlink) {
+        const auto from = _dstack.top()._pos;
+        assert(_cstack[to]._lowlink != std::numeric_limits<idx_t>::max() && _cstack[from]._lowlink != std::numeric_limits<idx_t>::max());
+        if (_cstack[to]._lowlink <= _cstack[from]._lowlink) {
             // we have now found a loop into earlier seen component cstack[to].lowlink.
             // if this earlier component precedes an accepting state,
             // the found loop is accepting and thus a violation.
-            violation = (!astack.empty() && to <= astack.top());
+            _violation = (!_astack.empty() && to <= _astack.top());
             // either way update the component ID of the state we came from.
-            cstack[from].lowlink = cstack[to].lowlink;
+            _cstack[from]._lowlink = _cstack[to]._lowlink;
             if constexpr (SaveTrace) {
-                loopstate = cstack[from].stateid;
-                looptrans = this->successorGenerator->fired();
-                cstack[from].lowsource = to;
+                _loop_state = _cstack[to]._stateid;
+                _loop_trans = this->successorGenerator->fired();
+                _cstack[from]._lowsource = to;
 
             }
         }
@@ -180,13 +191,13 @@
     template<template<typename, typename...> typename S, typename G, bool SaveTrace, typename... Spooler>
     bool TarjanModelChecker<S, G, SaveTrace, Spooler...>::nexttrans(State &state, State &parent, TarjanModelChecker::DEntry &delem)
     {
-        seen.decode(parent, cstack[delem.pos].stateid);
-        this->successorGenerator->prepare(&parent, delem.sucinfo);
+        _seen.decode(parent, _cstack[delem._pos]._stateid);
+        this->successorGenerator->prepare(&parent, delem._sucinfo);
         // ensure that `state` buffer contains the correct state for Büchi successor generation.
-        if (delem.sucinfo.has_prev_state()) {
-            seen.decode(state, delem.sucinfo.last_state);
+        if (delem._sucinfo.has_prev_state()) {
+            _seen.decode(state, delem._sucinfo.last_state);
         }
-        auto res = this->successorGenerator->next(state, delem.sucinfo);
+        auto res = this->successorGenerator->next(state, delem._sucinfo);
         return res;
     }
 
@@ -196,39 +207,49 @@
         if constexpr (!SaveTrace) {
             return;
         } else {
-            assert(violation);
-            State state = factory.newState();
+            assert(_violation);
             os << "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n"
                   "<trace>\n";
-            if (cstack[dstack.top().pos].stateid == loopstate) this->printLoop(os);
-            cstack[dstack.top().pos].lowlink = std::numeric_limits<idx_t>::max();
+            this->_reducer->initFire(os);
+            if (_cstack[dstack.top()._pos]._stateid == _loop_state)
+                this->printLoop(os);
             dstack.pop();
             unsigned long p;
+            bool had_deadlock = false;
             // print (reverted) dstack
             while (!dstack.empty()) {
-                p = dstack.top().pos;
-                auto stateid = cstack[p].stateid;
-                auto[parent, tid] = seen.getHistory(stateid);
-                seen.decode(state, parent);
-
-                if (stateid == loopstate) this->printLoop(os);
-                this->printTransition(tid, state, os) << '\n';
-
-                cstack[p].lowlink = std::numeric_limits<idx_t>::max();
+                p = dstack.top()._pos;
                 dstack.pop();
+                auto stateid = _cstack[p]._stateid;
+                auto[parent, tid] = _seen.getHistory(stateid);
+                this->printTransition(tid, os) << '\n';
+                if(tid >= std::numeric_limits<ptrie::uint>::max() - 1)
+                {
+                    had_deadlock = true;
+                    break;
+                }
+                if(_cstack[p]._stateid == _loop_state)
+                    this->printLoop(os);
+                _cstack[p]._lowlink = std::numeric_limits<idx_t>::max();
             }
             // follow previously found back edges via lowsource until back in dstack.
-            assert(cstack[p].lowsource != std::numeric_limits<idx_t>::max());
-            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, parent);
-                this->printTransition(tid, state, os) << '\n';
-                assert(cstack[p].lowsource != std::numeric_limits<idx_t>::max());
-                p = cstack[p].lowsource;
+            if(_cstack[p]._lowsource != std::numeric_limits<idx_t>::max() && !had_deadlock)
+            {
+                p = _cstack[p]._lowsource;
+                while (_cstack[p]._lowlink != std::numeric_limits<idx_t>::max()) {
+                    auto[parent, tid] = _seen.getHistory(_cstack[p]._stateid);
+                    this->printTransition(tid, os) << '\n';
+                    if(tid >= std::numeric_limits<ptrie::uint>::max() - 1)
+                    {
+                        had_deadlock = true;
+                        break;
+                    }
+                    assert(_cstack[p]._lowsource != std::numeric_limits<idx_t>::max());
+                    p = _cstack[p]._lowsource;
+                }
+                if(!had_deadlock)
+                    this->printTransition(_loop_trans, os) << '\n';
             }
-            seen.decode(state, loopstate);
-            this->printTransition(looptrans, state, os) << '\n';
 
             os << "</trace>" << std::endl;
         }

=== modified file 'src/LTL/LTLMain.cpp'
--- src/LTL/LTLMain.cpp	2021-08-10 13:44:22 +0000
+++ src/LTL/LTLMain.cpp	2021-10-17 18:21:15 +0000
@@ -71,9 +71,7 @@
     }
 
     template<typename Checker>
-    Result _verify(const PetriNet *net,
-                   Condition_ptr &negatedQuery,
-                   std::unique_ptr<Checker> checker,
+    Result _verify(std::unique_ptr<Checker> checker,
                    const options_t &options)
     {
         Result result;
@@ -110,15 +108,14 @@
     bool LTLMain(const PetriNet *net,
                         const Condition_ptr &query,
                         const std::string &queryName,
-                        options_t &options)
+                        options_t &options, const Reducer* reducer)
     {
-        auto res = to_ltl(query);
-        Condition_ptr negated_formula = res.first;
-        bool negate_answer = res.second;
 
         // force AP compress off for Büchi prints
         options.ltl_compress_aps = options.buchi_out_file.empty() ? options.ltl_compress_aps : APCompression::None;
 
+        auto [negated_formula, negate_answer] = to_ltl(query);
+
         Structures::BuchiAutomaton automaton = makeBuchiAutomaton(negated_formula, options);
         if (!options.buchi_out_file.empty()) {
             automaton.output_buchi(options.buchi_out_file, options.buchi_out_type);
@@ -127,7 +124,7 @@
         bool is_visible_stub = options.stubbornreduction
                                && (options.ltl_por == LTLPartialOrder::Visible || options.ltl_por == LTLPartialOrder::VisibleReach)
                                && !net->has_inhibitor()
-                                 && !negated_formula->containsNext();
+                               && !negated_formula->containsNext();
         bool is_autreach_stub = options.stubbornreduction
                 && (options.ltl_por == LTLPartialOrder::AutomatonReach ||
                     options.ltl_por == LTLPartialOrder::VisibleReach)
@@ -149,39 +146,17 @@
                     spooler = std::make_unique<EnabledSpooler>(net, gen);
                     gen.setSpooler(spooler.get());
                     gen.setHeuristic(heuristic.get());
+                    result = _verify(
+                            std::make_unique<NestedDepthFirstSearch<SpoolingSuccessorGenerator>>(
+                                    net, negated_formula, automaton, &gen, options.trace != TraceLevel::None, options.kbound, reducer),
+                            options);
 
-                    if (options.trace != TraceLevel::None) {
-                        result = _verify(
-                                net, negated_formula,
-                                std::make_unique<NestedDepthFirstSearch<SpoolingSuccessorGenerator, LTL::Structures::TraceableBitProductStateSet<> >>(
-                                        net, negated_formula, automaton, &gen,
-                                        options.kbound),
-                                options);
-                    } else {
-                        result = _verify(
-                                net, negated_formula,
-                                std::make_unique<NestedDepthFirstSearch<SpoolingSuccessorGenerator, LTL::Structures::BitProductStateSet<> >>(
-                                        net, negated_formula, automaton, &gen,
-                                        options.kbound),
-                                options);
-                    }
                 } else {
                     ResumingSuccessorGenerator gen{net};
-                    if (options.trace != TraceLevel::None) {
-                        result = _verify(
-                                net, negated_formula,
-                                std::make_unique<NestedDepthFirstSearch<ResumingSuccessorGenerator, LTL::Structures::TraceableBitProductStateSet<> >>(
-                                        net, negated_formula, automaton, &gen,
-                                        options.kbound),
-                                options);
-                    } else {
-                        result = _verify(
-                                net, negated_formula,
-                                std::make_unique<NestedDepthFirstSearch<ResumingSuccessorGenerator, LTL::Structures::BitProductStateSet<> >>(
-                                        net, negated_formula, automaton, &gen,
-                                        options.kbound),
-                                options);
-                    }
+                    result = _verify(
+                            std::make_unique<NestedDepthFirstSearch<ResumingSuccessorGenerator>>(
+                                    net, negated_formula, automaton, &gen, options.trace != TraceLevel::None, options.kbound, reducer),
+                            options);
                 }
                 break;
 
@@ -191,7 +166,6 @@
                     // Running default, BestFS, or RDFS search strategy so use spooling successor generator to enable heuristics.
                     SpoolingSuccessorGenerator gen{net, negated_formula};
                     if (is_visible_stub) {
-                        std::cout << "Running stubborn version!" << std::endl;
                         spooler = std::make_unique<VisibleLTLStubbornSet>(*net, negated_formula);
                     } else if (is_buchi_stub) {
                         spooler = std::make_unique<AutomatonStubbornSet>(*net, automaton);
@@ -211,68 +185,62 @@
 
                     if (options.trace != TraceLevel::None) {
                         if (is_autreach_stub && is_visible_stub) {
-                            result = _verify(net, negated_formula,
-                                             std::make_unique<TarjanModelChecker<ReachStubProductSuccessorGenerator, SpoolingSuccessorGenerator, true, VisibleLTLStubbornSet>>(
+                            result = _verify(std::make_unique<TarjanModelChecker<ReachStubProductSuccessorGenerator, SpoolingSuccessorGenerator, true, VisibleLTLStubbornSet>>(
                                                      net,
                                                      negated_formula,
                                                      automaton,
                                                      &gen,
-                                                     options.kbound,
+                                                     options.kbound, reducer,
                                                      std::make_unique<VisibleLTLStubbornSet>(*net, negated_formula)),
                                              options);
                         }
                         else if (is_autreach_stub && !is_visible_stub) {
-                            result = _verify(net, negated_formula,
-                                             std::make_unique<TarjanModelChecker<ReachStubProductSuccessorGenerator, SpoolingSuccessorGenerator, true, EnabledSpooler>>(
+                            result = _verify(std::make_unique<TarjanModelChecker<ReachStubProductSuccessorGenerator, SpoolingSuccessorGenerator, true, EnabledSpooler>>(
                                                      net,
                                                      negated_formula,
                                                      automaton,
                                                      &gen,
-                                                     options.kbound,
+                                                     options.kbound, reducer,
                                                      std::make_unique<EnabledSpooler>(net, gen)),
                                              options);
                         }
                         else {
-                            result = _verify(net, negated_formula,
-                                             std::make_unique<TarjanModelChecker<ProductSuccessorGenerator, SpoolingSuccessorGenerator, true>>(
+                            result = _verify(std::make_unique<TarjanModelChecker<ProductSuccessorGenerator, SpoolingSuccessorGenerator, true>>(
                                                      net,
                                                      negated_formula,
                                                      automaton,
                                                      &gen,
-                                                     options.kbound),
+                                                     options.kbound, reducer),
                                              options);
                         }
                     } else {
 
                         if (is_autreach_stub && is_visible_stub) {
-                            result = _verify(net, negated_formula,
-                                             std::make_unique<TarjanModelChecker<ReachStubProductSuccessorGenerator, SpoolingSuccessorGenerator, false, VisibleLTLStubbornSet>>(
+                            result = _verify(std::make_unique<TarjanModelChecker<ReachStubProductSuccessorGenerator, SpoolingSuccessorGenerator, false, VisibleLTLStubbornSet>>(
                                                      net,
                                                      negated_formula,
                                                      automaton,
                                                      &gen,
-                                                     options.kbound,
+                                                     options.kbound, reducer,
                                                      std::make_unique<VisibleLTLStubbornSet>(*net, negated_formula)),
                                              options);
                         } else if (is_autreach_stub && !is_visible_stub) {
-                            result = _verify(net, negated_formula,
-                                             std::make_unique<TarjanModelChecker<ReachStubProductSuccessorGenerator, SpoolingSuccessorGenerator, false, EnabledSpooler>>(
+                            result = _verify(std::make_unique<TarjanModelChecker<ReachStubProductSuccessorGenerator, SpoolingSuccessorGenerator, false, EnabledSpooler>>(
                                                      net,
                                                      negated_formula,
                                                      automaton,
                                                      &gen,
-                                                     options.kbound,
+                                                     options.kbound, reducer,
                                                      std::make_unique<EnabledSpooler>(net, gen)),
                                              options);
                         }
                         else {
-                            result = _verify(net, negated_formula,
-                                             std::make_unique<TarjanModelChecker<ProductSuccessorGenerator, SpoolingSuccessorGenerator, false>>(
+                            result = _verify(std::make_unique<TarjanModelChecker<ProductSuccessorGenerator, SpoolingSuccessorGenerator, false>>(
                                                      net,
                                                      negated_formula,
                                                      automaton,
                                                      &gen,
-                                                     options.kbound),
+                                                     options.kbound, reducer),
                                              options);
                         }
                     }
@@ -281,22 +249,20 @@
 
                     // no spooling needed, thus use resuming successor generation
                     if (options.trace != TraceLevel::None) {
-                        result = _verify(net, negated_formula,
-                                         std::make_unique<TarjanModelChecker<ProductSuccessorGenerator, ResumingSuccessorGenerator, true>>(
+                        result = _verify(std::make_unique<TarjanModelChecker<ProductSuccessorGenerator, ResumingSuccessorGenerator, true>>(
                                                  net,
                                                  negated_formula,
                                                  automaton,
                                                  &gen,
-                                                 options.kbound),
+                                                 options.kbound, reducer),
                                          options);
                     } else {
-                        result = _verify(net, negated_formula,
-                                         std::make_unique<TarjanModelChecker<ProductSuccessorGenerator, ResumingSuccessorGenerator, false>>(
+                        result = _verify(std::make_unique<TarjanModelChecker<ProductSuccessorGenerator, ResumingSuccessorGenerator, false>>(
                                                  net,
                                                  negated_formula,
                                                  automaton,
                                                  &gen,
-                                                 options.kbound),
+                                                 options.kbound, reducer),
                                          options);
                     }
                 }

=== modified file 'src/LTL/Stubborn/AutomatonStubbornSet.cpp'
--- src/LTL/Stubborn/AutomatonStubbornSet.cpp	2021-04-29 13:19:53 +0000
+++ src/LTL/Stubborn/AutomatonStubbornSet.cpp	2021-10-17 18:21:15 +0000
@@ -28,7 +28,7 @@
     public:
         NondeterministicConjunctionVisitor(AutomatonStubbornSet &stubbornSet) :
                 InterestingLTLTransitionVisitor(stubbornSet, false),
-                _stubborn(stubbornSet), _net(stubbornSet._net) {}
+                _net(stubbornSet._net), _stubborn(stubbornSet){}
 
     protected:
         static constexpr auto PresetBad = StubbornSet::PresetBad;

=== modified file 'src/LTL/Stubborn/SafeAutStubbornSet.cpp'
--- src/LTL/Stubborn/SafeAutStubbornSet.cpp	2021-05-13 09:19:31 +0000
+++ src/LTL/Stubborn/SafeAutStubbornSet.cpp	2021-10-17 18:21:15 +0000
@@ -16,6 +16,7 @@
  */
 
 #include "LTL/Stubborn/SafeAutStubbornSet.h"
+#include "LTL/Stubborn/VisibleTransitionVisitor.h"
 
 namespace LTL {
     using namespace PetriEngine;
@@ -28,37 +29,84 @@
 
         constructEnabled();
         if (_ordering.empty()) {
+            _print_debug();
             return false;
         }
         if (_ordering.size() == 1) {
             _stubborn[_ordering.front()] = true;
+            _print_debug();
             return true;
         }
 
+        InterestingLTLTransitionVisitor unsafe{*this, false};
         InterestingTransitionVisitor interesting{*this, false};
 
-        for (auto &q : _queries) {
-            q->evalAndSet(PQL::EvaluationContext((*_parent).marking(), &_net));
-            q->visit(interesting);
-        }
+        PQL::EvaluationContext ctx((*_parent).marking(), &_net);
+        _prog_cond->evalAndSet(ctx);
+        _sink_cond->evalAndSet(ctx);
+        _prog_cond->visit(unsafe);
+        _sink_cond->visit(unsafe);
+
+        //_ret_cond->evalAndSet(ctx);
+        //(std::make_shared<PetriEngine::PQL::NotCondition>(_ret_cond))->visit(interesting);
+
         assert(!_bad);
 
         _unsafe.swap(_stubborn);
+        _has_enabled_stubborn = false;
         //memset(_stubborn.get(), false, sizeof(bool) * _net.numberOfTransitions());
         _unprocessed.clear();
         memset(_places_seen.get(), 0, _net.numberOfPlaces());
 
         assert(_unprocessed.empty());
 
-        for (auto &q : _queries) {
-            q->visit(interesting);
+
+
+        // sink condition is not interesting, just unsafe.
+        _prog_cond->visit(interesting);
+        //_sink_cond->visit(interesting);
+        closure();
+        if (_bad) {
+            // abort
+            set_all_stubborn();
+            _print_debug();
+            return true;
+        }
+        // accepting states need key transition. add firs   t enabled by index.
+        if (state->is_accepting() && !_has_enabled_stubborn) {
+            //set_all_stubborn();
+            //_print_debug();
+            //return true;
+            addToStub(_ordering.front());
             closure();
+/*            for (int i = 0; i < _net.numberOfPlaces(); ++i) {
+                if (_enabled[i]) {
+                    addToStub(i);
+                    closure();
+                    break;
+                }
+            }*/
             if (_bad) {
-                // abort
                 set_all_stubborn();
-                return true;
             }
         }
+        _print_debug();
         return true;
     }
-}
\ No newline at end of file
+
+    void SafeAutStubbornSet::_print_debug() {
+#ifndef NDEBUG
+        float num_stubborn = 0;
+        float num_enabled = 0;
+        float num_enabled_stubborn = 0;
+        for (int i = 0; i < _net.numberOfTransitions(); ++i) {
+            if (_stubborn[i]) ++num_stubborn;
+            if (_enabled[i]) ++num_enabled;
+            if (_stubborn[i] && _enabled[i]) ++num_enabled_stubborn;
+        }
+        std::cerr << "Enabled: " << num_enabled << "/" << _net.numberOfTransitions() << " (" << num_enabled/_net.numberOfTransitions()*100.0 << "%),\t\t "
+        << "Stubborn: " << num_stubborn << "/" << _net.numberOfTransitions() << " (" << num_stubborn/_net.numberOfTransitions()*100.0 << "%),\t\t "
+        << "Enabled stubborn: " << num_enabled_stubborn << "/" << num_enabled << " (" << num_enabled_stubborn/num_enabled*100.0 << "%)" << std::endl;
+#endif
+    }
+}

=== modified file 'src/LTL/SuccessorGeneration/ResumingSuccessorGenerator.cpp'
--- src/LTL/SuccessorGeneration/ResumingSuccessorGenerator.cpp	2021-04-29 07:47:52 +0000
+++ src/LTL/SuccessorGeneration/ResumingSuccessorGenerator.cpp	2021-10-17 18:21:15 +0000
@@ -34,13 +34,13 @@
     }
 
 
-    void ResumingSuccessorGenerator::prepare(const Structures::State* state, const successor_info &sucinfo) {
+    void ResumingSuccessorGenerator::prepare(const Structures::State* state, const successor_info_t &sucinfo) {
         SuccessorGenerator::prepare(state);
         _suc_pcounter = sucinfo.pcounter;
         _suc_tcounter = sucinfo.tcounter;
     }
 
-    void ResumingSuccessorGenerator::getSuccInfo(successor_info &sucinfo) const {
+    void ResumingSuccessorGenerator::get_succ_info(successor_info_t &sucinfo) const {
         sucinfo.pcounter = _suc_pcounter;
         sucinfo.tcounter = _suc_tcounter;
     }

=== modified file 'src/PetriEngine/PQL/Expressions.cpp'
--- src/PetriEngine/PQL/Expressions.cpp	2021-08-21 10:20:38 +0000
+++ src/PetriEngine/PQL/Expressions.cpp	2021-10-17 18:21:15 +0000
@@ -3,17 +3,17 @@
  *                     Thomas Søndersø Nielsen <[e-mail]>,
  *                     Lars Kærlund Østergaard <[e-mail]>,
  *                     Peter Gjøl Jensen <[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/>.
  */
@@ -38,7 +38,7 @@
 
 namespace PetriEngine {
     namespace PQL {
-        
+
         std::ostream& generateTabs(std::ostream& out, uint32_t tabs) {
 
             for(uint32_t i = 0; i < tabs; i++) {
@@ -46,7 +46,7 @@
             }
             return out;
         }
-        
+
         /** FOR COMPILING AND CONSTRUCTING LOGICAL OPERATORS **/
 
         template<typename T>
@@ -61,7 +61,7 @@
                 _conds.emplace_back(ptr);
             }
             else if (auto comp = std::dynamic_pointer_cast<CompareCondition>(ptr))
-            {                
+            {
                 if((std::is_same<T, AndCondition>::value && std::dynamic_pointer_cast<NotEqualCondition>(ptr)) ||
                    (std::is_same<T, OrCondition>::value && std::dynamic_pointer_cast<EqualCondition>(ptr)))
                 {
@@ -113,7 +113,7 @@
                 }
                 else
                 {
-                    _conds.emplace_back(ptr);                    
+                    _conds.emplace_back(ptr);
                 }
             }
             else
@@ -122,7 +122,7 @@
             }
 
         }
-        
+
         template<typename T, bool K>
         Condition_ptr makeLog(const std::vector<Condition_ptr>& conds, bool aggressive)
         {
@@ -138,28 +138,28 @@
                 return BooleanCondition::getShared(K);
             return res;
         }
-        
-        Condition_ptr makeOr(const std::vector<Condition_ptr>& cptr) 
+
+        Condition_ptr makeOr(const std::vector<Condition_ptr>& cptr)
         { return makeLog<OrCondition,false>(cptr, true); }
-        Condition_ptr makeAnd(const std::vector<Condition_ptr>& cptr) 
+        Condition_ptr makeAnd(const std::vector<Condition_ptr>& cptr)
         { return makeLog<AndCondition,true>(cptr, true); }
-        Condition_ptr makeOr(const Condition_ptr& a, const Condition_ptr& b) {  
-            std::vector<Condition_ptr> cnds{a,b};
-            return makeLog<OrCondition,false>(cnds, true); 
-        }
-        Condition_ptr makeAnd(const Condition_ptr& a, const Condition_ptr& b) 
-        {             
-            std::vector<Condition_ptr> cnds{a,b};
-            return makeLog<AndCondition,true>(cnds, true); 
-        }
-        
-        
+        Condition_ptr makeOr(const Condition_ptr& a, const Condition_ptr& b) {
+            std::vector<Condition_ptr> cnds{a,b};
+            return makeLog<OrCondition,false>(cnds, true);
+        }
+        Condition_ptr makeAnd(const Condition_ptr& a, const Condition_ptr& b)
+        {
+            std::vector<Condition_ptr> cnds{a,b};
+            return makeLog<AndCondition,true>(cnds, true);
+        }
+
+
         // CONSTANTS
         Condition_ptr BooleanCondition::FALSE_CONSTANT = std::make_shared<BooleanCondition>(false);
         Condition_ptr BooleanCondition::TRUE_CONSTANT = std::make_shared<BooleanCondition>(true);
         Condition_ptr DeadlockCondition::DEADLOCK = std::make_shared<DeadlockCondition>();
-        
-        
+
+
         Condition_ptr BooleanCondition::getShared(bool val)
         {
             if(val)
@@ -178,7 +178,7 @@
             out << op() << " ";
             _cond->toTAPAALQuery(out,context);
         }
-        
+
         void UntilCondition::toTAPAALQuery(std::ostream& out,TAPAALConditionExportContext& context) const {
             out << op() << " (";
             _cond1->toTAPAALQuery(out, context);
@@ -186,7 +186,7 @@
             _cond2->toTAPAALQuery(out,context);
             out << ")";
         }
-        
+
         void LogicalCondition::toTAPAALQuery(std::ostream& out,TAPAALConditionExportContext& context) const {
             out << "(";
             _conds[0]->toTAPAALQuery(out, context);
@@ -197,7 +197,7 @@
             }
             out << ")";
         }
-        
+
         void CompareConjunction::toTAPAALQuery(std::ostream& out,TAPAALConditionExportContext& context) const {
             out << "(";
             if(_negated) out << "!";
@@ -205,11 +205,11 @@
             for(auto& c : _constraints)
             {
                 if(!first) out << " and ";
-                if(c._lower != 0) 
+                if(c._lower != 0)
                     out << "(" << c._lower << " <= " << context.netName << "." << c._name << ")";
-                if(c._lower != 0 && c._upper != std::numeric_limits<uint32_t>::max()) 
+                if(c._lower != 0 && c._upper != std::numeric_limits<uint32_t>::max())
                     out << " and ";
-                if(c._lower != 0) 
+                if(c._lower != 0)
                     out << "(" << c._upper << " >= " << context.netName << "." << c._name << ")";
                 first = false;
             }
@@ -270,7 +270,7 @@
             }
             out << ")";
         }
-        
+
         /******************** opTAPAAL ********************/
 
         std::string EqualCondition::opTAPAAL() const {
@@ -405,16 +405,16 @@
         void SimpleQuantifierCondition::analyze(AnalysisContext& context) {
             _cond->analyze(context);
         }
-        
+
         void UntilCondition::analyze(AnalysisContext& context) {
             _cond1->analyze(context);
             _cond2->analyze(context);
         }
-        
+
         void LogicalCondition::analyze(AnalysisContext& context) {
             for(auto& c : _conds) c->analyze(context);
         }
-        
+
         void UnfoldedFireableCondition::_analyze(AnalysisContext& context)
         {
             std::vector<Condition_ptr> conds;
@@ -425,7 +425,7 @@
                         _name.length());
                 context.reportError(error);
                 return;
-            }            
+            }
 
             assert(_name.compare(context.net()->transitionNames()[result.offset]) == 0);
             auto preset = context.net()->preset(result.offset);
@@ -462,9 +462,9 @@
                     ExprError error("Unable to resolve colored identifier \"" + _name + "\"", _name.length());
                     coloredContext->reportError(error);
                     return;
-                } 
+                }
                 if(names.size() < 1){
-                    //If the transition points to empty vector we know that it has 
+                    //If the transition points to empty vector we know that it has
                     //no legal bindings and can never fire
                     _compiled = std::make_shared<BooleanCondition>(false);
                     _compiled->analyze(context);
@@ -497,7 +497,7 @@
             _expr1->analyze(context);
             _expr2->analyze(context);
         }
-        
+
         void NotCondition::analyze(AnalysisContext& context) {
             _cond->analyze(context);
         }
@@ -639,7 +639,7 @@
             }
             _compiled->analyze(context);
         }
-        
+
         void UnfoldedUpperBoundsCondition::analyze(AnalysisContext& c)
         {
             for(auto& p : _places)
@@ -833,7 +833,7 @@
             setUpperBound(value(context.marking()));
             return _max <= _bound ? RTRUE : RUNKNOWN;
         }
-        
+
         /******************** Evaluation - save result ********************/
         Condition::Result SimpleQuantifierCondition::evalAndSet(const EvaluationContext& context) {
 	    return RUNKNOWN;
@@ -880,14 +880,14 @@
             setSatisfied(res);
             return res;
         }
-        
+
         Condition::Result UntilCondition::evalAndSet(const EvaluationContext& context) {
             auto r2 = _cond2->evalAndSet(context);
             if(r2 != RFALSE) return r2;
             auto r1 = _cond1->evalAndSet(context);
             if(r1 == RFALSE) return RFALSE;
             return RUNKNOWN;
-        }        
+        }
 
         int Expr::evalAndSet(const EvaluationContext& context) {
             int r = evaluate(context);
@@ -939,7 +939,7 @@
             setSatisfied(res);
             return res;
         }
-        
+
         Condition::Result CompareCondition::evalAndSet(const EvaluationContext& context) {
             int v1 = _expr1->evalAndSet(context);
             int v2 = _expr2->evalAndSet(context);
@@ -966,7 +966,7 @@
             setSatisfied(context.net()->deadlocked(context.marking()));
             return isSatisfied() ? RTRUE : RFALSE;
         }
-        
+
         Condition::Result UnfoldedUpperBoundsCondition::evalAndSet(const EvaluationContext& context)
         {
             auto res = evaluate(context);
@@ -990,12 +990,12 @@
         {
             ctx.accept<decltype(this)>(this);
         }
-        
+
         void EXCondition::visit(Visitor& ctx) const
         {
             ctx.accept<decltype(this)>(this);
         }
-        
+
         void EFCondition::visit(Visitor& ctx) const
         {
             ctx.accept<decltype(this)>(this);
@@ -1004,7 +1004,7 @@
         void AUCondition::visit(Visitor& ctx) const
         {
             ctx.accept<decltype(this)>(this);
-        }        
+        }
 
         void AXCondition::visit(Visitor& ctx) const
         {
@@ -1014,7 +1014,7 @@
         void AFCondition::visit(Visitor& ctx) const
         {
             ctx.accept<decltype(this)>(this);
-        } 
+        }
 
         void AGCondition::visit(Visitor& ctx) const
         {
@@ -1060,7 +1060,7 @@
         {
             ctx.accept<decltype(this)>(this);
         }
-        
+
         void EqualCondition::visit(Visitor& ctx) const
         {
             ctx.accept<decltype(this)>(this);
@@ -1075,22 +1075,22 @@
         {
             ctx.accept<decltype(this)>(this);
         }
-        
+
         void LessThanOrEqualCondition::visit(Visitor& ctx) const
         {
             ctx.accept<decltype(this)>(this);
         }
-        
+
         void LessThanCondition::visit(Visitor& ctx) const
         {
             ctx.accept<decltype(this)>(this);
         }
-        
+
         void BooleanCondition::visit(Visitor& ctx) const
         {
             ctx.accept<decltype(this)>(this);
         }
-        
+
         void DeadlockCondition::visit(Visitor& ctx) const
         {
             ctx.accept<decltype(this)>(this);
@@ -1143,7 +1143,7 @@
             else
                 ctx.accept<decltype(this)>(this);
         }
-        
+
         void UnfoldedFireableCondition::visit(Visitor& ctx) const
         {
             if(_compiled)
@@ -1152,12 +1152,12 @@
                 ctx.accept<decltype(this)>(this);
         }
 
-               
+
         void UnfoldedUpperBoundsCondition::visit(Visitor& ctx) const
         {
             ctx.accept<decltype(this)>(this);
         }
-        
+
         void LiteralExpr::visit(Visitor& ctx) const
         {
             ctx.accept<decltype(this)>(this);
@@ -1393,7 +1393,7 @@
         int MultiplyExpr::apply(int v1, int v2) const {
             return v1 * v2;
         }
-        
+
         /******************** Apply (CompareCondition subclasses) ********************/
 
         bool EqualCondition::apply(int v1, int v2) const {
@@ -1425,7 +1425,7 @@
         std::string MultiplyExpr::op() const {
             return "*";
         }
-        
+
         /******************** Op (QuantifierCondition subclasses) ********************/
 
         std::string ACondition::op() const {
@@ -1447,27 +1447,27 @@
         std::string XCondition::op() const {
             return "X";
         }
-        
+
         std::string EXCondition::op() const {
             return "EX";
         }
-        
+
         std::string EGCondition::op() const {
             return "EG";
         }
-        
+
         std::string EFCondition::op() const {
             return "EF";
         }
-        
+
         std::string AXCondition::op() const {
             return "AX";
         }
-        
+
         std::string AGCondition::op() const {
             return "AG";
         }
-        
+
         std::string AFCondition::op() const {
             return "AF";
         }
@@ -1481,11 +1481,11 @@
         std::string EUCondition::op() const {
             return "E";
         }
-        
+
         std::string AUCondition::op() const {
             return "A";
         }
-        
+
         /******************** Op (LogicalCondition subclasses) ********************/
 
         std::string AndCondition::op() const {
@@ -1514,7 +1514,7 @@
             return "<=";
         }
 
-        /******************** free of places ********************/        
+        /******************** free of places ********************/
 
         bool NaryExpr::placeFree() const
         {
@@ -1523,18 +1523,18 @@
                     return false;
             return true;
         }
-        
+
         bool CommutativeExpr::placeFree() const
         {
             if(_ids.size() > 0) return false;
             return NaryExpr::placeFree();
         }
-        
+
         bool MinusExpr::placeFree() const
         {
             return _expr->placeFree();
         }
-        
+
         /******************** Expr::type() implementation ********************/
 
         Expr::Types PlusExpr::type() const {
@@ -1610,17 +1610,17 @@
             return 0;
         }
 
-        uint32_t UnfoldedUpperBoundsCondition::distance(DistanceContext& context) const 
+        uint32_t UnfoldedUpperBoundsCondition::distance(DistanceContext& context) const
         {
             size_t tmp = 0;
             for(auto& p : _places)
             {
                 tmp += context.marking()[p._place];
             }
-            
+
             return _max - tmp;
         }
-        
+
         uint32_t EFCondition::distance(DistanceContext& context) const {
             return _cond->distance(context);
         }
@@ -1636,14 +1636,14 @@
         uint32_t EUCondition::distance(DistanceContext& context) const {
             return _cond2->distance(context);
         }
-        
+
         uint32_t AFCondition::distance(DistanceContext& context) const {
             context.negate();
             uint32_t retval = _cond->distance(context);
             context.negate();
             return retval;
         }
-        
+
         uint32_t AXCondition::distance(DistanceContext& context) const {
             context.negate();
             uint32_t retval = _cond->distance(context);
@@ -1665,7 +1665,7 @@
             context.negate();
             return r1 + r2;
         }
-        
+
         uint32_t CompareConjunction::distance(DistanceContext& context) const {
             uint32_t d = 0;
             auto neg = context.negated() != _negated;
@@ -1691,7 +1691,7 @@
                         else      d = std::min(d, d2);
                         first = false;
                     }
-                    
+
                     if(c._lower != 0)
                     {
                         auto d2 = delta<LessThanOrEqualCondition>(c._upper, pv, neg);
@@ -1739,35 +1739,35 @@
             int d;
             unsigned int p;
         };
-       
+
         uint32_t LessThanOrEqualCondition::distance(DistanceContext& context) const {
             return _distance(context, delta<LessThanOrEqualCondition>);
         }
-        
+
         uint32_t LessThanCondition::distance(DistanceContext& context) const {
             return _distance(context, delta<LessThanCondition>);
         }
-       
+
         uint32_t NotEqualCondition::distance(DistanceContext& context) const {
             return _distance(context, delta<NotEqualCondition>);
         }
-       
+
         uint32_t EqualCondition::distance(DistanceContext& context) const {
             return _distance(context, delta<EqualCondition>);
         }
 
         /******************** BIN output ********************/
-        
+
         void LiteralExpr::toBinary(std::ostream& out) const {
             out.write("l", sizeof(char));
             out.write(reinterpret_cast<const char*>(&_value), sizeof(int));
         }
-        
+
         void UnfoldedIdentifierExpr::toBinary(std::ostream& out) const {
             out.write("i", sizeof(char));
-            out.write(reinterpret_cast<const char*>(&_offsetInMarking), sizeof(int));            
+            out.write(reinterpret_cast<const char*>(&_offsetInMarking), sizeof(int));
         }
-        
+
         void MinusExpr::toBinary(std::ostream& out) const
         {
             auto e1 = std::make_shared<PQL::LiteralExpr>(0);
@@ -1776,7 +1776,7 @@
             exprs.push_back(_expr);
             PQL::SubtractExpr(std::move(exprs)).toBinary(out);
         }
-        
+
         void SubtractExpr::toBinary(std::ostream& out) const {
             out.write("-", sizeof(char));
             uint32_t size = _exprs.size();
@@ -1799,7 +1799,7 @@
             for(auto& e : _exprs)
                 e->toBinary(out);
         }
-        
+
         void SimpleQuantifierCondition::toBinary(std::ostream& out) const
         {
             auto path = getPath();
@@ -1818,7 +1818,7 @@
             _cond1->toBinary(out);
             _cond2->toBinary(out);
         }
-        
+
         void LogicalCondition::toBinary(std::ostream& out) const
         {
             auto path = getPath();
@@ -1829,7 +1829,7 @@
             out.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));
             for(auto& c : _conds) c->toBinary(out);
         }
-        
+
         void CompareConjunction::toBinary(std::ostream& out) const
         {
             auto path = getPath();
@@ -1841,12 +1841,12 @@
             out.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));
             for(auto& c : _constraints)
             {
-                out.write(reinterpret_cast<const char*>(&c._place), sizeof(int32_t));                
+                out.write(reinterpret_cast<const char*>(&c._place), sizeof(int32_t));
                 out.write(reinterpret_cast<const char*>(&c._lower), sizeof(uint32_t));
                 out.write(reinterpret_cast<const char*>(&c._upper), sizeof(uint32_t));
             }
         }
-        
+
         void CompareCondition::toBinary(std::ostream& out) const
         {
             auto path = getPath();
@@ -1859,7 +1859,7 @@
             _expr1->toBinary(out);
             _expr2->toBinary(out);
         }
-        
+
         void DeadlockCondition::toBinary(std::ostream& out) const
         {
             auto path = getPath();
@@ -1867,7 +1867,7 @@
             out.write(reinterpret_cast<const char*>(&path), sizeof(Path));
             out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
         }
-        
+
         void BooleanCondition::toBinary(std::ostream& out) const
         {
             auto path = getPath();
@@ -1876,24 +1876,24 @@
             out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
             out.write(reinterpret_cast<const char*>(&value), sizeof(bool));
         }
-        
+
         void UnfoldedUpperBoundsCondition::toBinary(std::ostream& out) const
         {
             auto path = getPath();
             auto quant = Quantifier::UPPERBOUNDS;
             out.write(reinterpret_cast<const char*>(&path), sizeof(Path));
-            out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));            
+            out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
             uint32_t size = _places.size();
-            out.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));                        
-            out.write(reinterpret_cast<const char*>(&_max), sizeof(double));     
-            out.write(reinterpret_cast<const char*>(&_offset), sizeof(double));     
+            out.write(reinterpret_cast<const char*>(&size), sizeof(uint32_t));
+            out.write(reinterpret_cast<const char*>(&_max), sizeof(double));
+            out.write(reinterpret_cast<const char*>(&_offset), sizeof(double));
             for(auto& b : _places)
             {
-                out.write(reinterpret_cast<const char*>(&b._place), sizeof(uint32_t));                        
+                out.write(reinterpret_cast<const char*>(&b._place), sizeof(uint32_t));
                 out.write(reinterpret_cast<const char*>(&b._max), sizeof(double));
             }
         }
-        
+
         void NotCondition::toBinary(std::ostream& out) const
         {
             auto path = getPath();
@@ -1902,9 +1902,9 @@
             out.write(reinterpret_cast<const char*>(&quant), sizeof(Quantifier));
             _cond->toBinary(out);
         }
-        
-        /******************** CTL Output ********************/ 
-        
+
+        /******************** CTL Output ********************/
+
         void LiteralExpr::toXML(std::ostream& out,uint32_t tabs, bool tokencount) const {
             generateTabs(out,tabs) << "<integer-constant>" + std::to_string(_value) + "</integer-constant>\n";
         }
@@ -1929,14 +1929,14 @@
                     ExprError error("Unable to resolve colored identifier \"" + _name + "\"", _name.length());
                     coloredContext->reportError(error);
                     return;
-                } 
+                }
                 if(names.size() < 1){
-                    //If the transition points to empty vector we know that it has 
+                    //If the transition points to empty vector we know that it has
                     //no legal bindings and can never fire
                     out << "<false/>";
                     return;
                 }
-                
+
                 out << "<is-fireable>";
                 for (auto& unfoldedName : names) {
                     out << "<transition>" + unfoldedName << "</transition>";
@@ -1944,14 +1944,14 @@
                 out << "</is-fireable>";
             }
         }
-        
+
         void UnfoldedIdentifierExpr::toXML(std::ostream& out,uint32_t tabs, bool tokencount) const {
             if (tokencount) {
                 generateTabs(out,tabs) << "<place>" << _name << "</place>\n";
             }
             else
             {
-                generateTabs(out,tabs) << "<tokens-count>\n"; 
+                generateTabs(out,tabs) << "<tokens-count>\n";
                 generateTabs(out,tabs+1) << "<place>" << _name << "</place>\n";
                 generateTabs(out,tabs) << "</tokens-count>\n";
             }
@@ -1963,7 +1963,7 @@
             }
             else
             {
-                out << "<tokens-count>\n"; 
+                out << "<tokens-count>\n";
                 out << "<place>" << _name << "</place>\n";
                 out << "</tokens-count>\n";
             }
@@ -1977,9 +1977,9 @@
                     ExprError error("Unable to resolve colored identifier \"" + _name + "\"", _name.length());
                     coloredContext->reportError(error);
                     return;
-                } 
-                
-                
+                }
+
+
                 out << "<tokens-count>\n";
                 for (auto& unfoldedName : names) {
                     out << "<place>" << unfoldedName.second << "</place>\n";
@@ -1991,19 +1991,19 @@
                 }
                 else
                 {
-                    out << "<tokens-count>\n"; 
+                    out << "<tokens-count>\n";
                     out << "<place>" << _name << "</place>\n";
                     out << "</tokens-count>\n";
                 }
             }
         }
-        
+
         void PlusExpr::toXML(std::ostream& ss,uint32_t tabs, bool tokencount) const {
             if (tokencount) {
                 for(auto& e : _exprs) e->toXML(ss,tabs, tokencount);
                 return;
             }
-            
+
             if(tk) {
                 generateTabs(ss,tabs) << "<tokens-count>\n";
                 for(auto& e : _ids) generateTabs(ss,tabs+1) << "<place>" << e.second << "</place>\n";
@@ -2015,9 +2015,9 @@
             generateTabs(ss,tabs+1) << "<integer-constant>" + std::to_string(_constant) + "</integer-constant>\n";
             for(auto& i : _ids)
             {
-                generateTabs(ss,tabs+1) << "<tokens-count>\n"; 
+                generateTabs(ss,tabs+1) << "<tokens-count>\n";
                 generateTabs(ss,tabs+2) << "<place>" << i.second << "</place>\n";
-                generateTabs(ss,tabs+1) << "</tokens-count>\n";                
+                generateTabs(ss,tabs+1) << "</tokens-count>\n";
             }
             for(auto& e : _exprs) e->toXML(ss,tabs+1, tokencount);
             generateTabs(ss,tabs) << "</integer-sum>\n";
@@ -2028,7 +2028,7 @@
                 for(auto& e : _exprs) e->toCompactXML(out,tabs, context, tokencount);
                 return;
             }
-            
+
             if(tk) {
                 out << "<tokens-count>\n";
                 for(auto& e : _ids) out << "<place>" << e.second << "</place>\n";
@@ -2040,14 +2040,14 @@
             out << "<integer-constant>" + std::to_string(_constant) + "</integer-constant>\n";
             for(auto& i : _ids)
             {
-                out << "<tokens-count>\n"; 
+                out << "<tokens-count>\n";
                 out << "<place>" << i.second << "</place>\n";
-                out << "</tokens-count>\n";                
+                out << "</tokens-count>\n";
             }
             for(auto& e : _exprs) e->toCompactXML(out,tabs, context, tokencount);
             out << "</integer-sum>\n";
         }
-        
+
         void SubtractExpr::toXML(std::ostream& ss,uint32_t tabs, bool tokencount) const {
             generateTabs(ss,tabs) << "<integer-difference>\n";
             for(auto& e : _exprs) e->toXML(ss,tabs+1);
@@ -2059,7 +2059,7 @@
             for(auto& e : _exprs) e->toCompactXML(out,tabs, context);
             out << "</integer-difference>\n";
         }
-        
+
         void MultiplyExpr::toXML(std::ostream& ss,uint32_t tabs, bool tokencount) const {
             generateTabs(ss,tabs) << "<integer-product>\n";
             for(auto& e : _exprs) e->toXML(ss,tabs+1);
@@ -2071,13 +2071,13 @@
             for(auto& e : _exprs) e->toCompactXML(out,tabs, context);
             out << "</integer-product>\n";
         }
-        
+
         void MinusExpr::toXML(std::ostream& out,uint32_t tabs, bool tokencount) const {
-            
+
             generateTabs(out,tabs) << "<integer-product>\n";
             _expr->toXML(out,tabs+1);
             generateTabs(out,tabs+1) << "<integer-difference>\n" ; generateTabs(out,tabs+2) <<
-                    "<integer-constant>0</integer-constant>\n" ; generateTabs(out,tabs+2) << 
+                    "<integer-constant>0</integer-constant>\n" ; generateTabs(out,tabs+2) <<
                     "<integer-constant>1</integer-constant>\n" ; generateTabs(out,tabs+1) <<
                     "</integer-difference>\n" ; generateTabs(out,tabs) << "</integer-product>\n";
         }
@@ -2086,11 +2086,11 @@
             out << "<integer-product>\n";
             _expr->toCompactXML(out,tabs, context);
             out << "<integer-difference>\n" ; out <<
-                    "<integer-constant>0</integer-constant>\n" ; out << 
+                    "<integer-constant>0</integer-constant>\n" ; out <<
                     "<integer-constant>1</integer-constant>\n" ; out <<
                     "</integer-difference>\n" ; out << "</integer-product>\n";
         }
-        
+
         void EXCondition::toXML(std::ostream& out,uint32_t tabs) const {
             generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<next>\n";
             _cond->toXML(out,tabs+2);
@@ -2103,66 +2103,66 @@
             out << "</next>\n" ; out << "</exists-path>\n";
         }
 
-        void AXCondition::toXML(std::ostream& out,uint32_t tabs) const {           
+        void AXCondition::toXML(std::ostream& out,uint32_t tabs) const {
             generateTabs(out,tabs) << "<all-paths>\n"; generateTabs(out,tabs+1) << "<next>\n";
-            _cond->toXML(out,tabs+2);            
+            _cond->toXML(out,tabs+2);
             generateTabs(out,tabs+1) << "</next>\n"; generateTabs(out,tabs) << "</all-paths>\n";
         }
 
-        void AXCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+        void AXCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<all-paths>\n" ;out << "<next>\n";
             _cond->toCompactXML(out,tabs+2, context);
             out << "</next>\n" ; out << "</all-paths>\n";
         }
-        
+
         void EFCondition::toXML(std::ostream& out,uint32_t tabs) const {
             generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<finally>\n";
             _cond->toXML(out,tabs+2);
             generateTabs(out,tabs+1) << "</finally>\n" ; generateTabs(out,tabs) << "</exists-path>\n";
         }
 
-        void EFCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+        void EFCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<exists-path>\n" ;out << "<finally>\n";
             _cond->toCompactXML(out,tabs+2, context);
             out << "</finally>\n" ; out << "</exists-path>\n";
         }
-        
+
         void AFCondition::toXML(std::ostream& out,uint32_t tabs) const {
             generateTabs(out,tabs) << "<all-paths>\n" ; generateTabs(out,tabs+1) << "<finally>\n";
             _cond->toXML(out,tabs+2);
             generateTabs(out,tabs+1) << "</finally>\n" ; generateTabs(out,tabs) << "</all-paths>\n";
         }
 
-        void AFCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+        void AFCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<all-paths>\n" ;out << "<finally>\n";
             _cond->toCompactXML(out,tabs+2, context);
             out << "</finally>\n" ; out << "</all-paths>\n";
         }
-        
-        void EGCondition::toXML(std::ostream& out,uint32_t tabs) const {            
+
+        void EGCondition::toXML(std::ostream& out,uint32_t tabs) const {
             generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<globally>\n";
-            _cond->toXML(out,tabs+2);            
+            _cond->toXML(out,tabs+2);
             generateTabs(out,tabs+1) <<  "</globally>\n" ; generateTabs(out,tabs) << "</exists-path>\n";
         }
 
-        void EGCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+        void EGCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<exists-path>\n" ;out << "<globally>\n";
             _cond->toCompactXML(out,tabs+2, context);
             out << "</globally>\n" ; out << "</exists-path>\n";
         }
-        
-        void AGCondition::toXML(std::ostream& out,uint32_t tabs) const {            
+
+        void AGCondition::toXML(std::ostream& out,uint32_t tabs) const {
             generateTabs(out,tabs) << "<all-paths>\n" ; generateTabs(out,tabs+1) << "<globally>\n";
             _cond->toXML(out,tabs+2);
             generateTabs(out,tabs+1) << "</globally>\n" ; generateTabs(out,tabs) << "</all-paths>\n";
         }
 
-        void AGCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+        void AGCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<all-paths>\n" ;out << "<globally>\n";
             _cond->toCompactXML(out,tabs+2, context);
             out << "</globally>\n" ; out << "</all-paths>\n";
         }
-        
+
         void EUCondition::toXML(std::ostream& out,uint32_t tabs) const {
             generateTabs(out,tabs) << "<exists-path>\n" ; generateTabs(out,tabs+1) << "<until>\n" ; generateTabs(out,tabs+2) << "<before>\n";
             _cond1->toXML(out,tabs+3);
@@ -2171,14 +2171,14 @@
             generateTabs(out,tabs+2) << "</reach>\n" ; generateTabs(out,tabs+1) << "</until>\n" ; generateTabs(out,tabs) << "</exists-path>\n";
         }
 
-        void EUCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+        void EUCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<exists-path>\n" ; out << "<until>\n" ; out << "<before>\n";
             _cond1->toCompactXML(out,tabs+2, context);
             out << "</before>\n" ; out << "<reach>\n";
             _cond2->toCompactXML(out,tabs+2, context);
             out << "</reach>\n" ; out << "</until>\n" ; out << "</exists-path>\n";
         }
-        
+
         void AUCondition::toXML(std::ostream& out,uint32_t tabs) const {
             generateTabs(out,tabs) << "<all-paths>\n" ; generateTabs(out,tabs+1) << "<until>\n" ; generateTabs(out,tabs+2) << "<before>\n";
             _cond1->toXML(out,tabs+3);
@@ -2187,7 +2187,7 @@
             generateTabs(out,tabs+2) << "</reach>\n" ; generateTabs(out,tabs+1) << "</until>\n" ; generateTabs(out,tabs) << "</all-paths>\n";
         }
 
-        void AUCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+        void AUCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<all-paths>\n" ; out << "<until>\n" ; out << "<before>\n";
             _cond1->toCompactXML(out,tabs+2, context);
             out << "</before>\n" ; out << "<reach>\n";
@@ -2201,7 +2201,7 @@
             generateTabs(out, tabs) << "</all-paths>\n";
         }
 
-        void ACondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+        void ACondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<all-paths>\n" ;
             _cond->toCompactXML(out,tabs+2, context);
             out << "</all-paths>\n";
@@ -2213,7 +2213,7 @@
             generateTabs(out, tabs) << "</exists-path>\n";
         }
 
-        void ECondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+        void ECondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<exists-path>\n" ;
             _cond->toCompactXML(out,tabs+2, context);
             out << "</exists-path>\n";
@@ -2225,7 +2225,7 @@
             generateTabs(out, tabs) << "</finally>\n";
         }
 
-        void FCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+        void FCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<finally>\n" ;
             _cond->toCompactXML(out,tabs+2, context);
             out << "</finally>\n";
@@ -2237,7 +2237,7 @@
             generateTabs(out, tabs) << "</globally>\n";
         }
 
-        void GCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+        void GCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<globally>\n" ;
             _cond->toCompactXML(out,tabs+2, context);
             out << "</globally>\n";
@@ -2249,7 +2249,7 @@
             generateTabs(out, tabs) << "</next>\n";
         }
 
-        void XCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+        void XCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<next>\n" ;
             _cond->toCompactXML(out,tabs+2, context);
             out << "</next>\n";
@@ -2263,7 +2263,7 @@
             generateTabs(out,tabs+1) << "</reach>\n" ; generateTabs(out,tabs) << "</until>\n" ;
         }
 
-        void UntilCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+        void UntilCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<until>\n" ; out << "<before>\n";
             _cond1->toCompactXML(out,tabs+2, context);
             out << "</before>\n" ; out << "<reach>\n";
@@ -2298,12 +2298,12 @@
             }
             for(size_t i = _conds.size() - 1; i > 1; --i)
             {
-                generateTabs(out,tabs + i) << "</conjunction>\n";                
+                generateTabs(out,tabs + i) << "</conjunction>\n";
             }
-            generateTabs(out,tabs) << "</conjunction>\n";              
+            generateTabs(out,tabs) << "</conjunction>\n";
         }
 
-        void AndCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+        void AndCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             if(_conds.size() == 0)
             {
                 BooleanCondition::TRUE_CONSTANT->toCompactXML(out,tabs, context);
@@ -2330,11 +2330,11 @@
             }
             for(size_t i = _conds.size() - 1; i > 1; --i)
             {
-                out << "</conjunction>\n";                
+                out << "</conjunction>\n";
             }
-            out << "</conjunction>\n";      
+            out << "</conjunction>\n";
         }
-        
+
         void OrCondition::toXML(std::ostream& out,uint32_t tabs) const {
             if(_conds.size() == 0)
             {
@@ -2362,12 +2362,12 @@
             }
             for(size_t i = _conds.size() - 1; i > 1; --i)
             {
-                generateTabs(out,tabs + i) << "</disjunction>\n";                
+                generateTabs(out,tabs + i) << "</disjunction>\n";
             }
-            generateTabs(out,tabs) << "</disjunction>\n";               
+            generateTabs(out,tabs) << "</disjunction>\n";
         }
 
-        void OrCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+        void OrCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             if(_conds.size() == 0)
             {
                 BooleanCondition::FALSE_CONSTANT->toCompactXML(out,tabs, context);
@@ -2394,9 +2394,9 @@
             }
             for(size_t i = _conds.size() - 1; i > 1; --i)
             {
-                out << "</disjunction>\n";                
+                out << "</disjunction>\n";
             }
-            out << "</disjunction>\n";      
+            out << "</disjunction>\n";
         }
 
         void CompareConjunction::toXML(std::ostream& out, uint32_t tabs) const
@@ -2405,10 +2405,10 @@
             if(_constraints.size() == 0) BooleanCondition::TRUE_CONSTANT->toXML(out, tabs);
             else
             {
-                bool single = _constraints.size() == 1 && 
+                bool single = _constraints.size() == 1 &&
                                 (_constraints[0]._lower == 0 ||
                                  _constraints[0]._upper == std::numeric_limits<uint32_t>::max());
-                if(!single) 
+                if(!single)
                     generateTabs(out,tabs) << "<conjunction>\n";
                 for(auto& c : _constraints)
                 {
@@ -2419,7 +2419,7 @@
                         generateTabs(out,tabs+3) << "<place>" << c._name << "</place>\n";
                         generateTabs(out,tabs+2) << "</tokens-count>\n";
                         generateTabs(out,tabs+2) << "<integer-constant>" << c._lower << "</integer-constant>\n";
-                        generateTabs(out,tabs+1) << "</integer-ge>\n";  
+                        generateTabs(out,tabs+1) << "</integer-ge>\n";
                     }
                     if(c._upper != std::numeric_limits<uint32_t>::max())
                     {
@@ -2428,7 +2428,7 @@
                         generateTabs(out,tabs+3) << "<place>" << c._name << "</place>\n";
                         generateTabs(out,tabs+2) << "</tokens-count>\n";
                         generateTabs(out,tabs+2) << "<integer-constant>" << c._upper << "</integer-constant>\n";
-                        generateTabs(out,tabs+1) << "</integer-le>\n";                      
+                        generateTabs(out,tabs+1) << "</integer-le>\n";
                     }
                 }
                 if(!single)
@@ -2437,15 +2437,15 @@
             if(_negated) generateTabs(out,--tabs) << "</negation>";
         }
 
-        void CompareConjunction::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+        void CompareConjunction::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             if(_negated) out << "<negation>";
             if(_constraints.size() == 0) BooleanCondition::TRUE_CONSTANT->toCompactXML(out,tabs, context);
             else
             {
-                bool single = _constraints.size() == 1 && 
+                bool single = _constraints.size() == 1 &&
                                 (_constraints[0]._lower == 0 ||
                                  _constraints[0]._upper == std::numeric_limits<uint32_t>::max());
-                if(!single) 
+                if(!single)
                     out << "<conjunction>\n";
                 for(auto& c : _constraints)
                 {
@@ -2456,7 +2456,7 @@
                         out << "<place>" << c._name << "</place>\n";
                         out << "</tokens-count>\n";
                         out << "<integer-constant>" << c._lower << "</integer-constant>\n";
-                        out << "</integer-ge>\n";  
+                        out << "</integer-ge>\n";
                     }
                     if(c._upper != std::numeric_limits<uint32_t>::max())
                     {
@@ -2465,104 +2465,104 @@
                         out << "<place>" << c._name << "</place>\n";
                         out << "</tokens-count>\n";
                         out << "<integer-constant>" << c._upper << "</integer-constant>\n";
-                        out << "</integer-le>\n";                      
+                        out << "</integer-le>\n";
                     }
                 }
                 if(!single)
                     out << "</conjunction>\n";
             }
-            if(_negated) out << "</negation>";      
+            if(_negated) out << "</negation>";
         }
 
         void EqualCondition::toXML(std::ostream& out,uint32_t tabs) const {
             generateTabs(out,tabs) << "<integer-eq>\n";
             _expr1->toXML(out,tabs+1);
             _expr2->toXML(out,tabs+1);
-            generateTabs(out,tabs) << "</integer-eq>\n";  
+            generateTabs(out,tabs) << "</integer-eq>\n";
         }
 
-        void EqualCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+        void EqualCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<integer-eq>\n";
             _expr1->toCompactXML(out,tabs, context);
             _expr2->toCompactXML(out,tabs, context);
             out << "</integer-eq>\n";
         }
-        
+
         void NotEqualCondition::toXML(std::ostream& out,uint32_t tabs) const {
             generateTabs(out,tabs) << "<integer-ne>\n";
             _expr1->toXML(out,tabs+1);
             _expr2->toXML(out,tabs+1);
-            generateTabs(out,tabs) << "</integer-ne>\n";  
+            generateTabs(out,tabs) << "</integer-ne>\n";
         }
 
-        void NotEqualCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+        void NotEqualCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<integer-ne>\n";
             _expr1->toCompactXML(out,tabs, context);
             _expr2->toCompactXML(out,tabs, context);
             out << "</integer-ne>\n";
         }
-        
+
         void LessThanCondition::toXML(std::ostream& out,uint32_t tabs) const {
             generateTabs(out,tabs) << "<integer-lt>\n";
             _expr1->toXML(out,tabs+1);
             _expr2->toXML(out,tabs+1);
-            generateTabs(out,tabs) << "</integer-lt>\n";  
+            generateTabs(out,tabs) << "</integer-lt>\n";
         }
 
-        void LessThanCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+        void LessThanCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<integer-lt>\n";
             _expr1->toCompactXML(out,tabs, context);
             _expr2->toCompactXML(out,tabs, context);
             out << "</integer-lt>\n";
         }
-        
+
         void LessThanOrEqualCondition::toXML(std::ostream& out,uint32_t tabs) const {
             generateTabs(out,tabs) << "<integer-le>\n";
             _expr1->toXML(out,tabs+1);
             _expr2->toXML(out,tabs+1);
-            generateTabs(out,tabs) << "</integer-le>\n";  
+            generateTabs(out,tabs) << "</integer-le>\n";
         }
 
-        void LessThanOrEqualCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+        void LessThanOrEqualCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<integer-le>\n";
             _expr1->toCompactXML(out,tabs, context);
             _expr2->toCompactXML(out,tabs, context);
             out << "</integer-le>\n";
         }
-        
+
         void NotCondition::toXML(std::ostream& out,uint32_t tabs) const {
-            
+
             generateTabs(out,tabs) << "<negation>\n";
             _cond->toXML(out,tabs+1);
-            generateTabs(out,tabs) << "</negation>\n";  
+            generateTabs(out,tabs) << "</negation>\n";
         }
 
-        void NotCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+        void NotCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<negation>\n";
             _cond->toCompactXML(out,tabs, context);
             out << "</negation>\n";
         }
-        
-        void BooleanCondition::toXML(std::ostream& out,uint32_t tabs) const {            
-            generateTabs(out,tabs) << "<" << 
-                    (value ? "true" : "false")
-                    << "/>\n"; 
-        }
-
-        void BooleanCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
-            out << "<" << 
-                    (value ? "true" : "false")
-                    << "/>\n"; 
-        }
-        
+
+        void BooleanCondition::toXML(std::ostream& out,uint32_t tabs) const {
+            generateTabs(out,tabs) << "<" <<
+                    (value ? "true" : "false")
+                    << "/>\n";
+        }
+
+        void BooleanCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
+            out << "<" <<
+                    (value ? "true" : "false")
+                    << "/>\n";
+        }
+
         void DeadlockCondition::toXML(std::ostream& out,uint32_t tabs) const {
-            generateTabs(out,tabs) << "<deadlock/>\n"; 
+            generateTabs(out,tabs) << "<deadlock/>\n";
         }
 
-        void DeadlockCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+        void DeadlockCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<deadlock/>\n";
         }
-        
+
         void UnfoldedUpperBoundsCondition::toXML(std::ostream& out, uint32_t tabs) const {
             generateTabs(out, tabs) << "<place-bound>\n";
             for(auto& p : _places)
@@ -2570,33 +2570,33 @@
             generateTabs(out, tabs) << "</place-bound>\n";
         }
 
-        void UnfoldedUpperBoundsCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{ 
+        void UnfoldedUpperBoundsCondition::toCompactXML(std::ostream& out, uint32_t tabs, AnalysisContext& context) const{
             out << "<place-bound>\n";
             for(auto& p : _places)
                 out << "<place>" << p._name << "</place>\n";
-            out << "</place-bound>\n"; 
+            out << "</place-bound>\n";
         }
-        
-        /******************** Query Simplification ********************/       
-        
+
+        /******************** Query Simplification ********************/
+
         Member LiteralExpr::constraint(SimplificationContext& context) const {
             return Member(_value);
         }
-        
-        Member memberForPlace(size_t p, SimplificationContext& context) 
+
+        Member memberForPlace(size_t p, SimplificationContext& context)
         {
             std::vector<int> row(context.net()->numberOfTransitions(), 0);
             row.shrink_to_fit();
             for (size_t t = 0; t < context.net()->numberOfTransitions(); t++) {
                 row[t] = context.net()->outArc(t, p) - context.net()->inArc(p, t);
             }
-            return Member(std::move(row), context.marking()[p]);            
+            return Member(std::move(row), context.marking()[p]);
         }
-        
+
         Member UnfoldedIdentifierExpr::constraint(SimplificationContext& context) const {
             return memberForPlace(_offsetInMarking, context);
         }
-        
+
         Member CommutativeExpr::commutativeCons(int constant, SimplificationContext& context, std::function<void(Member& a, Member b)> op) const
         {
             Member res;
@@ -2606,7 +2606,7 @@
                 first = false;
                 res = Member(_constant);
             }
-            
+
             for(auto& i : _ids)
             {
                 if(first) res = memberForPlace(i.first, context);
@@ -2620,28 +2620,28 @@
                 else op(res, e->constraint(context));
                 first = false;
             }
-            return res;            
+            return res;
         }
-        
+
         Member PlusExpr::constraint(SimplificationContext& context) const {
             return commutativeCons(0, context, [](auto& a , auto b){ a += b;});
         }
-        
+
         Member SubtractExpr::constraint(SimplificationContext& context) const {
             Member res = _exprs[0]->constraint(context);
             for(size_t i = 1; i < _exprs.size(); ++i) res -= _exprs[i]->constraint(context);
             return res;
         }
-        
+
         Member MultiplyExpr::constraint(SimplificationContext& context) const {
             return commutativeCons(1, context, [](auto& a , auto b){ a *= b;});
         }
-        
+
         Member MinusExpr::constraint(SimplificationContext& context) const {
             Member neg(-1);
             return _expr->constraint(context) *= neg;
         }
-        
+
         Retval simplifyEX(Retval& r, SimplificationContext& context) {
             if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)) {
                 return Retval(std::make_shared<NotCondition>(
@@ -2652,7 +2652,7 @@
                 return Retval(std::make_shared<EXCondition>(r.formula));
             }
         }
-        
+
         Retval simplifyAX(Retval& r, SimplificationContext& context) {
             if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)){
                 return Retval(BooleanCondition::TRUE_CONSTANT);
@@ -2672,7 +2672,7 @@
                 return Retval(std::make_shared<EFCondition>(r.formula));
             }
         }
-        
+
         Retval simplifyAF(Retval& r, SimplificationContext& context){
             if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)){
                 return Retval(BooleanCondition::TRUE_CONSTANT);
@@ -2682,7 +2682,7 @@
                 return Retval(std::make_shared<AFCondition>(r.formula));
             }
         }
-        
+
         Retval simplifyEG(Retval& r, SimplificationContext& context){
             if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)){
                 return Retval(BooleanCondition::TRUE_CONSTANT);
@@ -2692,7 +2692,7 @@
                 return Retval(std::make_shared<EGCondition>(r.formula));
             }
         }
-        
+
         Retval simplifyAG(Retval& r, SimplificationContext& context){
             if(r.formula->isTriviallyTrue() || !r.neglps->satisfiable(context)){
                 return Retval(BooleanCondition::TRUE_CONSTANT);
@@ -2720,32 +2720,32 @@
             Retval r = _cond->simplify(context);
             return context.negated() ? simplifyAX(r, context) : simplifyEX(r, context);
         }
-        
+
         Retval AXCondition::simplify(SimplificationContext& context) const {
             Retval r = _cond->simplify(context);
             return context.negated() ? simplifyEX(r, context) : simplifyAX(r, context);
-        }  
-        
+        }
+
         Retval EFCondition::simplify(SimplificationContext& context) const {
             Retval r = _cond->simplify(context);
-            return context.negated() ? simplifyAG(r, context) : simplifyEF(r, context);  
+            return context.negated() ? simplifyAG(r, context) : simplifyEF(r, context);
         }
-        
+
         Retval AFCondition::simplify(SimplificationContext& context) const {
             Retval r = _cond->simplify(context);
-            return context.negated() ? simplifyEG(r, context) : simplifyAF(r, context);  
+            return context.negated() ? simplifyEG(r, context) : simplifyAF(r, context);
         }
-        
+
         Retval EGCondition::simplify(SimplificationContext& context) const {
             Retval r = _cond->simplify(context);
-            return context.negated() ? simplifyAF(r, context) : simplifyEG(r, context);  
+            return context.negated() ? simplifyAF(r, context) : simplifyEG(r, context);
         }
-        
+
         Retval AGCondition::simplify(SimplificationContext& context) const {
             Retval r = _cond->simplify(context);
-            return context.negated() ? simplifyEF(r, context) : simplifyAG(r, context);  
+            return context.negated() ? simplifyEF(r, context) : simplifyAG(r, context);
         }
-        
+
         Retval EUCondition::simplify(SimplificationContext& context) const {
             // cannot push negation any further
             bool neg = context.negated();
@@ -2754,20 +2754,20 @@
             if(r2.formula->isTriviallyTrue() || !r2.neglps->satisfiable(context))
             {
                 context.setNegate(neg);
-                return neg ? 
+                return neg ?
                             Retval(BooleanCondition::FALSE_CONSTANT) :
                             Retval(BooleanCondition::TRUE_CONSTANT);
             }
             else if(r2.formula->isTriviallyFalse() || !r2.lps->satisfiable(context))
             {
                 context.setNegate(neg);
-                return neg ? 
+                return neg ?
                             Retval(BooleanCondition::TRUE_CONSTANT) :
-                            Retval(BooleanCondition::FALSE_CONSTANT);                
+                            Retval(BooleanCondition::FALSE_CONSTANT);
             }
             Retval r1 = _cond1->simplify(context);
             context.setNegate(neg);
-            
+
             if(context.negated()){
                 if(r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(context)){
                     return Retval(std::make_shared<NotCondition>(
@@ -2788,7 +2788,7 @@
                 }
             }
         }
-        
+
         Retval AUCondition::simplify(SimplificationContext& context) const {
             // cannot push negation any further
             bool neg = context.negated();
@@ -2797,20 +2797,20 @@
             if(r2.formula->isTriviallyTrue() || !r2.neglps->satisfiable(context))
             {
                 context.setNegate(neg);
-                return neg ? 
+                return neg ?
                             Retval(BooleanCondition::FALSE_CONSTANT) :
                             Retval(BooleanCondition::TRUE_CONSTANT);
             }
             else if(r2.formula->isTriviallyFalse() || !r2.lps->satisfiable(context))
             {
                 context.setNegate(neg);
-                return neg ? 
+                return neg ?
                             Retval(BooleanCondition::TRUE_CONSTANT) :
                             Retval(BooleanCondition::FALSE_CONSTANT);
             }
             Retval r1 = _cond1->simplify(context);
             context.setNegate(neg);
-            
+
             if(context.negated()){
                 if(r1.formula->isTriviallyTrue() || !r1.neglps->satisfiable(context)){
                     return Retval(std::make_shared<NotCondition>(
@@ -2919,7 +2919,7 @@
             }
             return lps[0];
         }
-        
+
         Retval LogicalCondition::simplifyAnd(SimplificationContext& context) const {
 
             std::vector<Condition_ptr> conditions;
@@ -2936,12 +2936,12 @@
                 {
                     continue;
                 }
-                
+
                 conditions.push_back(r.formula);
                 lpsv.emplace_back(r.lps);
                 neglps.emplace_back(r.neglps);
             }
-            
+
             if(conditions.size() == 0)
             {
                 return Retval(BooleanCondition::TRUE_CONSTANT);
@@ -2953,24 +2953,24 @@
                 if(!context.timeout() && !lps->satisfiable(context))
                 {
                     return Retval(BooleanCondition::FALSE_CONSTANT);
-                }           
+                }
              }
              catch(std::bad_alloc& e)
              {
                 // we are out of memory, deal with it.
                 std::cout<<"Query reduction: memory exceeded during LPS merge."<<std::endl;
              }
-            
+
             // Lets try to see if the r1 AND r2 can ever be false at the same time
             // If not, then we know that r1 || r2 must be true.
             // we check this by checking if !r1 && !r2 is unsat
-            
+
             return Retval(
-                    makeAnd(conditions), 
+                    makeAnd(conditions),
                     std::move(lps),
                     std::make_shared<UnionCollection>(std::move(neglps)));
         }
-        
+
         Retval LogicalCondition::simplifyOr(SimplificationContext& context) const {
 
             std::vector<Condition_ptr> conditions;
@@ -2993,7 +2993,7 @@
                 lps.push_back(r.lps);
                 neglpsv.emplace_back(r.neglps);
             }
-            
+
             AbstractProgramCollection_ptr  neglps = mergeLps(std::move(neglpsv));
 
             if(conditions.size() == 0)
@@ -3005,7 +3005,7 @@
                if(!context.timeout() && !neglps->satisfiable(context))
                {
                    return Retval(BooleanCondition::TRUE_CONSTANT);
-               }           
+               }
             }
             catch(std::bad_alloc& e)
             {
@@ -3016,20 +3016,20 @@
             // Lets try to see if the r1 AND r2 can ever be false at the same time
             // If not, then we know that r1 || r2 must be true.
             // we check this by checking if !r1 && !r2 is unsat
-          
+
             return Retval(
-                    makeOr(conditions), 
-                    std::make_shared<UnionCollection>(std::move(lps)), 
-                    std::move(neglps));            
+                    makeOr(conditions),
+                    std::make_shared<UnionCollection>(std::move(lps)),
+                    std::move(neglps));
         }
-        
+
         Retval AndCondition::simplify(SimplificationContext& context) const {
             if(context.timeout())
             {
-                if(context.negated()) 
+                if(context.negated())
                     return Retval(std::make_shared<NotCondition>(
                             makeAnd(_conds)));
-                else                  
+                else
                     return Retval(
                             makeAnd(_conds));
             }
@@ -3038,16 +3038,16 @@
                 return simplifyOr(context);
             else
                 return simplifyAnd(context);
-            
+
         }
-        
-        Retval OrCondition::simplify(SimplificationContext& context) const {            
+
+        Retval OrCondition::simplify(SimplificationContext& context) const {
             if(context.timeout())
             {
-                if(context.negated()) 
+                if(context.negated())
                     return Retval(std::make_shared<NotCondition>(
                             makeOr(_conds)));
-                else                 
+                else
                     return Retval(makeOr(_conds));
             }
             if(context.negated())
@@ -3055,7 +3055,7 @@
             else
                 return simplifyOr(context);
         }
-        
+
         Retval CompareConjunction::simplify(SimplificationContext& context) const {
             if(context.timeout())
             {
@@ -3064,7 +3064,7 @@
             std::vector<AbstractProgramCollection_ptr>  neglps, lpsv;
             auto neg = context.negated() != _negated;
             std::vector<cons_t> nconstraints;
-            for(auto& c : _constraints) 
+            for(auto& c : _constraints)
             {
                 nconstraints.push_back(c);
                 if(c._lower != 0 /*&& !context.timeout()*/ )
@@ -3088,7 +3088,7 @@
                         neglps.push_back(nlp);
                    }
                 }
-         
+
                 if(c._upper != std::numeric_limits<uint32_t>::max() /*&& !context.timeout()*/)
                 {
                     auto m1 = memberForPlace(c._place, context);
@@ -3110,26 +3110,26 @@
                         neglps.push_back(nlp);
                    }
                 }
-                
+
                 assert(nconstraints.size() > 0);
                 if(nconstraints.back()._lower == 0 && nconstraints.back()._upper == std::numeric_limits<uint32_t>::max())
                     nconstraints.pop_back();
 
                 assert(nconstraints.size() <= neglps.size()*2);
             }
-            
+
             auto lps = mergeLps(std::move(lpsv));
-            
-            if(lps == nullptr && !context.timeout()) 
+
+            if(lps == nullptr && !context.timeout())
             {
                 return Retval(BooleanCondition::getShared(!neg));
             }
-            
+
             try {
                 if(!context.timeout() && lps &&  !lps->satisfiable(context))
                 {
                     return Retval(BooleanCondition::getShared(neg));
-                }           
+                }
              }
              catch(std::bad_alloc& e)
              {
@@ -3142,7 +3142,7 @@
             try {
                 // remove trivial rules from neglp
                 int ncnt = neglps.size() - 1;
-                for(int i = nconstraints.size() - 1; i >= 0; --i) 
+                for(int i = nconstraints.size() - 1; i >= 0; --i)
                 {
                     if(context.timeout()) break;
                     assert(ncnt >= 0);
@@ -3161,7 +3161,7 @@
                                 c._upper = std::numeric_limits<uint32_t>::max();
                             neglps.erase(neglps.begin() + ncnt);
                         }
-                        if(c._upper == std::numeric_limits<uint32_t>::max() && c._lower == 0) 
+                        if(c._upper == std::numeric_limits<uint32_t>::max() && c._lower == 0)
                             nconstraints.erase(nconstraints.begin() + i);
                         --ncnt;
                     }
@@ -3171,13 +3171,13 @@
             {
                // we are out of memory, deal with it.
                std::cout<<"Query reduction: memory exceeded during LPS merge."<<std::endl;
-            }            
+            }
             if(nconstraints.size() == 0)
             {
-                return Retval(BooleanCondition::getShared(!neg));                
+                return Retval(BooleanCondition::getShared(!neg));
             }
 
-            
+
             Condition_ptr rc = [&]() -> Condition_ptr {
                 if(nconstraints.size() == 1)
                 {
@@ -3209,7 +3209,7 @@
                         else
                         {
                             if(neg) return std::make_shared<LessThanCondition>(lu, id);
-                            else    return std::make_shared<LessThanOrEqualCondition>(id, lu);                        
+                            else    return std::make_shared<LessThanOrEqualCondition>(id, lu);
                         }
                     }
                 }
@@ -3218,26 +3218,26 @@
                     return std::make_shared<CompareConjunction>(std::move(nconstraints), context.negated() != _negated);
                 }
             }();
-            
+
 
             if(!neg)
             {
                 return Retval(
-                    rc, 
+                    rc,
                     std::move(lps),
                     std::make_shared<UnionCollection>(std::move(neglps)));
             }
             else
             {
                 return Retval(
-                    rc, 
+                    rc,
                     std::make_shared<UnionCollection>(std::move(neglps)),
-                    std::move(lps));                
+                    std::move(lps));
             }
         }
 
         Retval EqualCondition::simplify(SimplificationContext& context) const {
-            
+
             Member m1 = _expr1->constraint(context);
             Member m2 = _expr2->constraint(context);
             std::shared_ptr<AbstractProgramCollection> lps, neglps;
@@ -3249,27 +3249,27 @@
                     int constant = m2.constant() - m1.constant();
                     m1 -= m2;
                     m2 = m1;
-                    neglps = 
+                    neglps =
                             std::make_shared<UnionCollection>(
                             std::make_shared<SingleProgram>(context.cache(), std::move(m1), constant, Simplification::OP_GT),
                             std::make_shared<SingleProgram>(context.cache(), std::move(m2), constant, Simplification::OP_LT));
                     Member m3 = m2;
                     lps = std::make_shared<SingleProgram>(context.cache(), std::move(m3), constant, Simplification::OP_EQ);
-                    
+
                     if(context.negated()) lps.swap(neglps);
                 }
             } else {
                 lps = std::make_shared<SingleProgram>();
                 neglps = std::make_shared<SingleProgram>();
             }
-            
+
             if (!context.timeout() && !lps->satisfiable(context)) {
                 return Retval(BooleanCondition::FALSE_CONSTANT);
-            } 
+            }
             else if(!context.timeout() && !neglps->satisfiable(context))
             {
-                return Retval(BooleanCondition::TRUE_CONSTANT);            
-            } 
+                return Retval(BooleanCondition::TRUE_CONSTANT);
+            }
             else {
                 if (context.negated()) {
                     return Retval(std::make_shared<NotEqualCondition>(_expr1, _expr2), std::move(lps), std::move(neglps));
@@ -3278,7 +3278,7 @@
                 }
             }
         }
-        
+
         Retval NotEqualCondition::simplify(SimplificationContext& context) const {
             Member m1 = _expr1->constraint(context);
             Member m2 = _expr2->constraint(context);
@@ -3287,17 +3287,17 @@
                 if ((m1.isZero() && m2.isZero()) || m1.substrationIsZero(m2)) {
                     return Retval(std::make_shared<BooleanCondition>(
                         context.negated() ? (m1.constant() == m2.constant()) : (m1.constant() != m2.constant())));
-                } else{ 
+                } else{
                     int constant = m2.constant() - m1.constant();
                     m1 -= m2;
                     m2 = m1;
-                    lps = 
+                    lps =
                             std::make_shared<UnionCollection>(
                             std::make_shared<SingleProgram>(context.cache(), std::move(m1), constant, Simplification::OP_GT),
                             std::make_shared<SingleProgram>(context.cache(), std::move(m2), constant, Simplification::OP_LT));
                     Member m3 = m2;
-                    neglps = std::make_shared<SingleProgram>(context.cache(), std::move(m3), constant, Simplification::OP_EQ); 
-                    
+                    neglps = std::make_shared<SingleProgram>(context.cache(), std::move(m3), constant, Simplification::OP_EQ);
+
                     if(context.negated()) lps.swap(neglps);
                 }
             } else {
@@ -3306,20 +3306,20 @@
             }
             if (!context.timeout() && !lps->satisfiable(context)) {
                 return Retval(BooleanCondition::FALSE_CONSTANT);
-            } 
+            }
             else if(!context.timeout() && !neglps->satisfiable(context))
             {
-                return Retval(BooleanCondition::TRUE_CONSTANT);            
+                return Retval(BooleanCondition::TRUE_CONSTANT);
             }
             else {
                 if (context.negated()) {
                     return Retval(std::make_shared<EqualCondition>(_expr1, _expr2), std::move(lps), std::move(neglps));
                 } else {
                     return Retval(std::make_shared<NotEqualCondition>(_expr1, _expr2), std::move(lps), std::move(neglps));
-                }                         
+                }
             }
         }
-            
+
         Retval LessThanCondition::simplify(SimplificationContext& context) const {
             Member m1 = _expr1->constraint(context);
             Member m2 = _expr2->constraint(context);
@@ -3340,27 +3340,27 @@
                 lps = std::make_shared<SingleProgram>();
                 neglps = std::make_shared<SingleProgram>();
             }
-            
+
             if (!context.timeout() && !lps->satisfiable(context)) {
                 return Retval(BooleanCondition::FALSE_CONSTANT);
             }
             else if(!context.timeout() && !neglps->satisfiable(context))
             {
-                return Retval(BooleanCondition::TRUE_CONSTANT);                
+                return Retval(BooleanCondition::TRUE_CONSTANT);
             }
             else {
                 if (context.negated()) {
                     return Retval(std::make_shared<LessThanOrEqualCondition>(_expr2, _expr1), std::move(lps), std::move(neglps));
                 } else {
                     return Retval(std::make_shared<LessThanCondition>(_expr1, _expr2), std::move(lps), std::move(neglps));
-                }                         
+                }
             }
-        }        
-        
+        }
+
         Retval LessThanOrEqualCondition::simplify(SimplificationContext& context) const {
             Member m1 = _expr1->constraint(context);
             Member m2 = _expr2->constraint(context);
-            
+
             AbstractProgramCollection_ptr lps, neglps;
             if (!context.timeout() && m1.canAnalyze() && m2.canAnalyze()) {
                 // test for trivial comparison
@@ -3378,7 +3378,7 @@
                 lps = std::make_shared<SingleProgram>();
                 neglps = std::make_shared<SingleProgram>();
             }
-            
+
             assert(lps);
             assert(neglps);
 
@@ -3390,19 +3390,19 @@
                 if (context.negated()) {
                     return Retval(std::make_shared<LessThanCondition>(_expr2, _expr1), std::move(lps), std::move(neglps));
                 } else {
-                    return Retval(std::make_shared<LessThanOrEqualCondition>(_expr1, _expr2), 
+                    return Retval(std::make_shared<LessThanOrEqualCondition>(_expr1, _expr2),
                             std::move(lps), std::move(neglps));
-                }                         
+                }
             }
         }
-        
+
         Retval NotCondition::simplify(SimplificationContext& context) const {
             context.negate();
             Retval r = _cond->simplify(context);
             context.negate();
             return r;
         }
-        
+
         Retval BooleanCondition::simplify(SimplificationContext& context) const {
             if (context.negated()) {
                 return Retval(getShared(!value));
@@ -3410,7 +3410,7 @@
                 return Retval(getShared(value));
             }
         }
-        
+
         Retval DeadlockCondition::simplify(SimplificationContext& context) const {
             if (context.negated()) {
                 return Retval(std::make_shared<NotCondition>(DeadlockCondition::DEADLOCK));
@@ -3418,8 +3418,8 @@
                 return Retval(DeadlockCondition::DEADLOCK);
             }
         }
-        
-        Retval UnfoldedUpperBoundsCondition::simplify(SimplificationContext& context) const 
+
+        Retval UnfoldedUpperBoundsCondition::simplify(SimplificationContext& context) const
         {
             std::vector<place_t> next;
             std::vector<uint32_t> places;
@@ -3442,29 +3442,29 @@
             }
             return Retval(std::make_shared<UnfoldedUpperBoundsCondition>(next, bounds[nplaces].first-offset, offset));
         }
-        
+
         /******************** Check if query is a reachability query ********************/
-        
+
         bool EXCondition::isReachability(uint32_t depth) const {
             return false;
         }
-        
+
         bool EGCondition::isReachability(uint32_t depth) const {
             return false;
         }
-        
+
         bool EFCondition::isReachability(uint32_t depth) const {
             return depth > 0 ? false : _cond->isReachability(depth + 1);
         }
-        
+
         bool AXCondition::isReachability(uint32_t depth) const {
             return false;
         }
-        
+
         bool AGCondition::isReachability(uint32_t depth) const {
             return depth > 0 ? false : _cond->isReachability(depth + 1);
         }
-        
+
         bool AFCondition::isReachability(uint32_t depth) const {
             return false;
         }
@@ -3473,28 +3473,27 @@
             if (depth != 0) {
                 return false;
             }
-
-            if (auto cond = dynamic_cast<FCondition*>(_cond.get())) {
+            else if (auto cond = dynamic_cast<FCondition*>(_cond.get())) {
                 // EF is a reachability formula so skip checking the F.
                 return (*cond)[0]->isReachability(depth + 1);
             }
-            return _cond->isReachability(depth + 1);
+            else return false;
         }
 
         bool ACondition::isReachability(uint32_t depth) const {
             if (depth != 0) {
                 return false;
             }
-            if (auto cond = dynamic_cast<GCondition*>(_cond.get())) {
+            else if (auto cond = dynamic_cast<GCondition*>(_cond.get())) {
                 return (*cond)[0]->isReachability(depth + 1);
             }
-            return _cond->isReachability(depth + 1);
+            else return false;
         }
-        
+
         bool UntilCondition::isReachability(uint32_t depth) const {
             return false;
         }
-        
+
         bool LogicalCondition::isReachability(uint32_t depth) const {
             if(depth == 0) return false;
             bool reachability = true;
@@ -3505,69 +3504,59 @@
             }
             return reachability;
         }
-        
+
         bool CompareCondition::isReachability(uint32_t depth) const {
             return depth > 0;
         }
-        
+
         bool NotCondition::isReachability(uint32_t depth) const {
             return _cond->isReachability(depth);
         }
-        
+
         bool BooleanCondition::isReachability(uint32_t depth) const {
             return depth > 0;
         }
-        
+
         bool DeadlockCondition::isReachability(uint32_t depth) const {
             return depth > 0;
         }
-        
+
         bool UnfoldedUpperBoundsCondition::isReachability(uint32_t depth) const {
             return depth > 0;
         }
-                
+
         /******************** Prepare Reachability Queries ********************/
-        
+
         Condition_ptr EXCondition::prepareForReachability(bool negated) const {
             return nullptr;
         }
-        
+
         Condition_ptr EGCondition::prepareForReachability(bool negated) const {
             return nullptr;
         }
-        
+
         Condition_ptr EFCondition::prepareForReachability(bool negated) const {
             _cond->setInvariant(negated);
             return _cond;
         }
-        
+
         Condition_ptr AXCondition::prepareForReachability(bool negated) const {
             return nullptr;
         }
-        
+
         Condition_ptr AGCondition::prepareForReachability(bool negated) const {
             Condition_ptr cond = std::make_shared<NotCondition>(_cond);
             cond->setInvariant(!negated);
             return cond;
         }
-        
+
         Condition_ptr AFCondition::prepareForReachability(bool negated) const {
             return nullptr;
         }
 
         Condition_ptr ACondition::prepareForReachability(bool negated) const {
             auto g = std::dynamic_pointer_cast<GCondition>(_cond);
-            if (g) {
-                return AGCondition((*g)[0]).prepareForReachability(negated);
-            }
-            else {
-                // ugly hacking for `A true`.
-                auto bcond = std::dynamic_pointer_cast<BooleanCondition>(_cond);
-                if (bcond) {
-                    return bcond;
-                }
-                else return nullptr;
-            }
+            return g ? AGCondition((*g)[0]).prepareForReachability(negated) : nullptr;
         }
 
         Condition_ptr ECondition::prepareForReachability(bool negated) const {
@@ -3578,7 +3567,7 @@
         Condition_ptr UntilCondition::prepareForReachability(bool negated) const {
             return nullptr;
         }
-        
+
         Condition_ptr LogicalCondition::prepareForReachability(bool negated) const {
             return nullptr;
         }
@@ -3586,19 +3575,19 @@
         Condition_ptr CompareConjunction::prepareForReachability(bool negated) const {
             return nullptr;
         }
-        
+
         Condition_ptr CompareCondition::prepareForReachability(bool negated) const {
             return nullptr;
         }
-        
+
         Condition_ptr NotCondition::prepareForReachability(bool negated) const {
             return _cond->prepareForReachability(!negated);
         }
-        
+
         Condition_ptr BooleanCondition::prepareForReachability(bool negated) const {
             return nullptr;
         }
-        
+
         Condition_ptr DeadlockCondition::prepareForReachability(bool negated) const {
             return nullptr;
         }
@@ -3606,9 +3595,9 @@
         Condition_ptr UnfoldedUpperBoundsCondition::prepareForReachability(bool negated) const {
             return nullptr;
         }
-        
+
 /******************** Prepare CTL Queries ********************/
-        
+
         Condition_ptr EGCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
             ++stats[0];
             return AFCondition(std::make_shared<NotCondition>(_cond)).pushNegation(stats, context, nested, !negated, initrw);
@@ -3618,7 +3607,7 @@
             ++stats[1];
             return EFCondition(std::make_shared<NotCondition>(_cond)).pushNegation(stats, context, nested, !negated, initrw);
         }
-        
+
         Condition_ptr EXCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
             return initialMarkingRW([&]() -> Condition_ptr {
             auto a = _cond->pushNegation(stats, context, true, negated, initrw);
@@ -3629,9 +3618,9 @@
             }
             else
             {
-                if(a == BooleanCondition::FALSE_CONSTANT) 
+                if(a == BooleanCondition::FALSE_CONSTANT)
                 { ++stats[3]; return a;}
-                if(a == BooleanCondition::TRUE_CONSTANT)  
+                if(a == BooleanCondition::TRUE_CONSTANT)
                 { ++stats[4]; return std::make_shared<NotCondition>(DeadlockCondition::DEADLOCK); }
                 a = std::make_shared<EXCondition>(a);
             }
@@ -3649,7 +3638,7 @@
             }
             else
             {
-                if(a == BooleanCondition::TRUE_CONSTANT) 
+                if(a == BooleanCondition::TRUE_CONSTANT)
                 { ++stats[6]; return a;}
                 if(a == BooleanCondition::FALSE_CONSTANT)
                 { ++stats[7]; return DeadlockCondition::DEADLOCK; }
@@ -3659,7 +3648,7 @@
             }, stats, context, nested, negated, initrw);
         }
 
-        
+
         Condition_ptr EFCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
             return initialMarkingRW([&]() -> Condition_ptr {
             auto a = _cond->pushNegation(stats, context, true, false, initrw);
@@ -3670,7 +3659,7 @@
                 {
                     ++stats[8];
                     return a->pushNegation(stats, context, nested, negated, initrw);
-                }                
+                }
             }
 
             if(!a->isTemporal())
@@ -3679,7 +3668,7 @@
                 if(negated) return std::make_shared<NotCondition>(res);
                 return res;
             }
-            
+
             if( dynamic_cast<EFCondition*>(a.get()))
             {
                 ++stats[9];
@@ -3714,7 +3703,7 @@
                 }
                 ++stats[13];
                 std::vector<Condition_ptr> pef, atomic;
-                for(auto& i : *cond) 
+                for(auto& i : *cond)
                 {
                     pef.push_back(std::make_shared<EFCondition>(i));
                 }
@@ -3722,7 +3711,7 @@
                 return a;
             }
             else
-            {        
+            {
                 Condition_ptr b = std::make_shared<EFCondition>(a);
                 if(negated) b = std::make_shared<NotCondition>(b);
                 return b;
@@ -3740,9 +3729,9 @@
                 {
                     ++stats[14];
                     return a->pushNegation(stats, context, nested, negated, initrw);
-                }                
+                }
             }
-            
+
             if(dynamic_cast<AFCondition*>(a.get()))
             {
                 ++stats[15];
@@ -3814,7 +3803,7 @@
                     return AFCondition(b).pushNegation(stats, context, nested, negated, initrw);
                 }
             }
-            
+
             if(auto cond = dynamic_cast<AFCondition*>(b.get()))
             {
                 ++stats[22];
@@ -3855,7 +3844,7 @@
                     return makeOr(pef)->pushNegation(stats, context, nested, negated, initrw);
                 }
             }
-            
+
             auto c = std::make_shared<AUCondition>(a, b);
             if(negated) return std::make_shared<NotCondition>(c);
             return c;
@@ -3889,7 +3878,7 @@
                     return EFCondition(b).pushNegation(stats, context, nested, negated, initrw);
                 }
             }
-            
+
             if(dynamic_cast<EFCondition*>(b.get()))
             {
                 ++stats[28];
@@ -4026,7 +4015,7 @@
         /*Boolean connectives */
         Condition_ptr pushAnd(const std::vector<Condition_ptr>& _conds, negstat_t& stats, const EvaluationContext& context, bool nested, bool negate_children, bool initrw)
         {
-            std::vector<Condition_ptr> nef, other;            
+            std::vector<Condition_ptr> nef, other;
             for(auto& c : _conds)
             {
                 auto n = c->pushNegation(stats, context, nested, negate_children, initrw);
@@ -4047,27 +4036,27 @@
                 {
                     other.emplace_back(n);
                 }
-            }         
+            }
             if(nef.size() + other.size() == 0)
                 return BooleanCondition::TRUE_CONSTANT;
-            if(nef.size() + other.size() == 1) 
-            { 
-                return nef.size() == 0 ? 
-                    other[0] : 
+            if(nef.size() + other.size() == 1)
+            {
+                return nef.size() == 0 ?
+                    other[0] :
                     std::make_shared<NotCondition>(std::make_shared<EFCondition>(nef[0]));
             }
             if(nef.size() != 0) other.push_back(
                     std::make_shared<NotCondition>(
                     std::make_shared<EFCondition>(
-                    makeOr(nef)))); 
+                    makeOr(nef))));
             if(other.size() == 1) return other[0];
             auto res = makeAnd(other);
             return res;
         }
-        
+
         Condition_ptr pushOr(const std::vector<Condition_ptr>& _conds, negstat_t& stats, const EvaluationContext& context, bool nested, bool negate_children, bool initrw)
         {
-            std::vector<Condition_ptr> nef, other;       
+            std::vector<Condition_ptr> nef, other;
             for(auto& c : _conds)
             {
                 auto n = c->pushNegation(stats, context, nested, negate_children, initrw);
@@ -4090,7 +4079,7 @@
             if(nef.size() + other.size() == 1) { return nef.size() == 0 ? other[0] : std::make_shared<EFCondition>(nef[0]);}
             if(nef.size() != 0) other.push_back(
                     std::make_shared<EFCondition>(
-                    makeOr(nef))); 
+                    makeOr(nef)));
             if(other.size() == 1) return other[0];
             return makeOr(other);
         }
@@ -4102,7 +4091,7 @@
             }, stats, context, nested, negated, initrw);
         }
 
-        
+
         Condition_ptr AndCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
             return initialMarkingRW([&]() -> Condition_ptr {
             return negated ? pushOr (_conds, stats, context, nested, true, initrw) :
@@ -4110,14 +4099,14 @@
 
             }, stats, context, nested, negated, initrw);
         }
-        
+
         Condition_ptr CompareConjunction::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
             return initialMarkingRW([&]() -> Condition_ptr {
             return std::make_shared<CompareConjunction>(*this, negated);
             }, stats, context, nested, negated, initrw);
         }
 
-        
+
         Condition_ptr NotCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
             return initialMarkingRW([&]() -> Condition_ptr {
             if(negated) ++stats[30];
@@ -4173,11 +4162,11 @@
             if(auto p1 = std::dynamic_pointer_cast<PlusExpr>(_expr1))
                 if(auto p2 = std::dynamic_pointer_cast<PlusExpr>(_expr2))
                     remdup(p1, p2);
-            
+
             if(auto m1 = std::dynamic_pointer_cast<MultiplyExpr>(_expr1))
                 if(auto m2 = std::dynamic_pointer_cast<MultiplyExpr>(_expr2))
-                    remdup(m1, m2);                    
-            
+                    remdup(m1, m2);
+
             if(auto p1 = std::dynamic_pointer_cast<CommutativeExpr>(_expr1))
                 if(auto p2 = std::dynamic_pointer_cast<CommutativeExpr>(_expr2))
                     return p1->_exprs.size() + p1->_ids.size() + p2->_exprs.size() + p2->_ids.size() == 0;
@@ -4217,34 +4206,34 @@
             if(negated == noteq) return std::make_shared<EqualCondition>((*org)[0], (*org)[1]);
             else                 return std::make_shared<NotEqualCondition>((*org)[0], (*org)[1]);
         }
-        
+
         Condition_ptr NotEqualCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
             return initialMarkingRW([&]() -> Condition_ptr {
                 return pushEqual(this, negated, true, context);
             }, stats, context, nested, negated, initrw);
         }
 
-        
+
         Condition_ptr EqualCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
             return initialMarkingRW([&]() -> Condition_ptr {
                 return pushEqual(this, negated, false, context);
             }, stats, context, nested, negated, initrw);
         }
-                
+
         Condition_ptr BooleanCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
             return initialMarkingRW([&]() -> Condition_ptr {
             if(negated) return getShared(!value);
             else        return getShared(value);
             }, stats, context, nested, negated, initrw);
         }
-        
+
         Condition_ptr DeadlockCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
             return initialMarkingRW([&]() -> Condition_ptr {
             if(negated) return std::make_shared<NotCondition>(DEADLOCK);
             else        return DEADLOCK;
             }, stats, context, nested, negated, initrw);
         }
-        
+
         Condition_ptr UnfoldedUpperBoundsCondition::pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
             if(negated)
             {
@@ -4260,24 +4249,24 @@
         void postMerge(std::vector<Condition_ptr>& conds) {
             std::sort(std::begin(conds), std::end(conds),
                     [](auto& a, auto& b) {
-                        return a->isTemporal() < b->isTemporal(); 
+                        return a->isTemporal() < b->isTemporal();
                     });
-        } 
-        
+        }
+
         AndCondition::AndCondition(std::vector<Condition_ptr>&& conds) {
             for (auto& c : conds) tryMerge<AndCondition>(_conds, c);
             for (auto& c : _conds) _temporal = _temporal || c->isTemporal();
             for (auto& c : _conds) _loop_sensitive = _loop_sensitive || c->isLoopSensitive();
             postMerge(_conds);
         }
-        
+
         AndCondition::AndCondition(const std::vector<Condition_ptr>& conds) {
             for (auto& c : conds) tryMerge<AndCondition>(_conds, c);
             for (auto& c : _conds) _temporal = _temporal || c->isTemporal();
             for (auto& c : _conds) _loop_sensitive = _loop_sensitive || c->isLoopSensitive();
             postMerge(_conds);
         }
-       
+
         AndCondition::AndCondition(Condition_ptr left, Condition_ptr right) {
             tryMerge<AndCondition>(_conds, left);
             tryMerge<AndCondition>(_conds, right);
@@ -4285,21 +4274,21 @@
             for (auto& c : _conds) _loop_sensitive = _loop_sensitive || c->isLoopSensitive();
             postMerge(_conds);
         }
-       
+
         OrCondition::OrCondition(std::vector<Condition_ptr>&& conds) {
             for (auto& c : conds) tryMerge<OrCondition>(_conds, c);
             for (auto& c : _conds) _temporal = _temporal || c->isTemporal();
             for (auto& c : _conds) _loop_sensitive = _loop_sensitive || c->isLoopSensitive();
             postMerge(_conds);
         }
-       
+
         OrCondition::OrCondition(const std::vector<Condition_ptr>& conds) {
             for (auto& c : conds) tryMerge<OrCondition>(_conds, c);
             for (auto& c : _conds) _temporal = _temporal || c->isTemporal();
             for (auto& c : _conds) _loop_sensitive = _loop_sensitive || c->isLoopSensitive();
             postMerge(_conds);
         }
-       
+
         OrCondition::OrCondition(Condition_ptr left, Condition_ptr right) {
             tryMerge<OrCondition>(_conds, left);
             tryMerge<OrCondition>(_conds, right);
@@ -4307,14 +4296,14 @@
             for (auto& c : _conds) _loop_sensitive = _loop_sensitive || c->isLoopSensitive();
             postMerge(_conds);
         }
-        
+
 
         CompareConjunction::CompareConjunction(const std::vector<Condition_ptr>& conditions, bool negated)
         {
             _negated = negated;
             merge(conditions, negated);
         }
-        
+
         void CompareConjunction::merge(const CompareConjunction& other)
         {
             auto neg = _negated != other._negated;
@@ -4329,7 +4318,7 @@
             {
                 if(neg)
                     c.invert();
-                                
+
                 if(c._upper == std::numeric_limits<uint32_t>::max() && c._lower == 0)
                 {
                     continue;
@@ -4340,7 +4329,7 @@
                     assert(false);
                     exit(ErrorCode);
                 }
-                
+
                 il = std::lower_bound(_constraints.begin(), _constraints.end(), c);
                 if(il == _constraints.end() || il->_place != c._place)
                 {
@@ -4353,7 +4342,7 @@
                 }
             }
         }
-        
+
         void CompareConjunction::merge(const std::vector<Condition_ptr>& conditions, bool negated)
         {
             for(auto& c : conditions)
@@ -4405,21 +4394,21 @@
                 }
                 if(negated)
                     next.invert();
-                
+
                 auto lb = std::lower_bound(std::begin(_constraints), std::end(_constraints), next);
                 if(lb == std::end(_constraints) || lb->_place != next._place)
                 {
                     next._name = id->name();
                     _constraints.insert(lb, next);
-                }  
+                }
                 else
                 {
                     assert(id->name().compare(lb->_name) == 0);
                     lb->intersect(next);
                 }
-            }            
+            }
         }
-       
+
         void CommutativeExpr::init(std::vector<Expr_ptr>&& exprs)
         {
             for (auto& e : exprs) {
@@ -4430,7 +4419,7 @@
                 }
                 else if (auto id = std::dynamic_pointer_cast<PQL::UnfoldedIdentifierExpr>(e)) {
                     _ids.emplace_back(id->offset(), id->name());
-                } 
+                }
                 else if(auto c = std::dynamic_pointer_cast<CommutativeExpr>(e))
                 {
                     // we should move up plus/multiply here when possible;
@@ -4440,19 +4429,19 @@
                     }
                     else
                     {
-                        _exprs.emplace_back(std::move(e));                        
+                        _exprs.emplace_back(std::move(e));
                     }
                 } else {
                     _exprs.emplace_back(std::move(e));
                 }
             }
         }
-        
+
         PlusExpr::PlusExpr(std::vector<Expr_ptr>&& exprs, bool tk) : CommutativeExpr(0), tk(tk)
         {
             init(std::move(exprs));
         }
-        
+
         MultiplyExpr::MultiplyExpr(std::vector<Expr_ptr>&& exprs) : CommutativeExpr(1)
         {
             init(std::move(exprs));

=== modified file 'src/PetriEngine/Reducer.cpp'
--- src/PetriEngine/Reducer.cpp	2021-07-07 13:19:23 +0000
+++ src/PetriEngine/Reducer.cpp	2021-10-17 18:21:15 +0000
@@ -1,4 +1,4 @@
-/* 
+/*
  * File:   Reducer.cpp
  * Author: srba
  *
@@ -15,7 +15,7 @@
 
 namespace PetriEngine {
 
-    Reducer::Reducer(PetriNetBuilder* p) 
+    Reducer::Reducer(PetriNetBuilder* p)
     : parent(p) {
     }
 
@@ -24,9 +24,9 @@
     }
 
     void Reducer::Print(QueryPlaceAnalysisContext& context) {
-        std::cout   << "\nNET INFO:\n" 
+        std::cout   << "\nNET INFO:\n"
                     << "Number of places: " << parent->numberOfPlaces() << std::endl
-                    << "Number of transitions: " << parent->numberOfTransitions() 
+                    << "Number of transitions: " << parent->numberOfTransitions()
                     << std::endl << std::endl;
         for (uint32_t t = 0; t < parent->numberOfTransitions(); t++) {
             std::cout << "Transition " << t << " :\n";
@@ -36,30 +36,30 @@
             }
             for(auto& arc : parent->_transitions[t].pre)
             {
-                if (arc.weight > 0) 
-                    std::cout   << "\tInput place " << arc.place  
+                if (arc.weight > 0)
+                    std::cout   << "\tInput place " << arc.place
                                 << " (" << getPlaceName(arc.place) << ")"
                                 << " with arc-weight " << arc.weight << std::endl;
             }
             for(auto& arc : parent->_transitions[t].post)
             {
-                if (arc.weight > 0) 
-                    std::cout   << "\tOutput place " << arc.place 
-                                << " (" << getPlaceName(arc.place) << ")"