Merge lp:~tapaal-ltl/verifypn/mcc2021 into lp:verifypn

[Jiri Srba]

Numerous efficiency improvements, new LTL engine and improved CPN unfolding via color fixed-point computation.

Consistency verified against the current trunk version on MCC 2020 models and queries.

=== modified file 'CMakeLists.txt'
--- CMakeLists.txt	2020-10-31 18:57:21 +0000
+++ CMakeLists.txt	2021-04-02 18:07:40 +0000
@@ -15,7 +15,7 @@
 set(CMAKE_POSITION_INDEPENDENT_CODE ON)
 
 
-set(VERIFYPN_VERSION 3.1.1)
+set(VERIFYPN_VERSION 4.0.0)
 add_compile_definitions(VERIFYPN_VERSION=\"${VERIFYPN_VERSION}\")
 
 project(verifypn VERSION ${VERIFYPN_VERSION} LANGUAGES CXX C)
@@ -32,11 +32,7 @@
     endif(VERIFYPN_MC_Simplification)
     if (NOT APPLE)
         set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -static")
-    else(NOT APPLE)
-    	set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -static-libgcc -static-libstdc++")
     endif(NOT APPLE)
-else(VERIFYPN_Static)
-    set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -static-libgcc -static-libstdc++")
 endif (VERIFYPN_Static)
 
 if (VERIFYPN_MC_Simplification)
@@ -47,14 +43,15 @@
     set(ARCH_TYPE "linux64")
 elseif(APPLE)
     set(ARCH_TYPE "osx64")
-    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mmacosx-version-min=10.8 -m64 ")
-    set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -mmacosx-version-min=10.8 -m64 ")
+    set(CMAKE_OSX_DEPLOYMENT_TARGET 10.8)
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -m64 ")
+    set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -m64 ")
 else()
     set(ARCH_TYPE "win64")
 endif ()
 
-set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -Wall -pedantic-errors -O3 -DNDEBUG")
-
+set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -s -Wall -pedantic-errors -O3 -DNDEBUG")
+set(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS_DEBUG} -O0 -fno-omit-frame-pointer")
 set(CMAKE_EXE_LINKER_FLAGS_RELEASE "${CMAKE_EXE_LINKER_FLAGS_RELEASE} -O3 -DNDEBUG")
 if (VERIFYPN_Static AND NOT APPLE)
     set(CMAKE_EXE_LINKER_FLAGS_RELEASE "${CMAKE_EXE_LINKER_FLAGS_RELEASE} -static")
@@ -81,6 +78,23 @@
         CONFIGURE_COMMAND mkdir -p ${CMAKE_BINARY_DIR}/external/include
         INSTALL_COMMAND cd ../rapidxml-ext && ${CMAKE_COMMAND} -E copy rapidxml.hpp rapidxml_iterators.hpp rapidxml_print.hpp rapidxml_utils.hpp ${EXTERNAL_INSTALL_LOCATION}/include    
     )
+    if (UNIX AND NOT APPLE)
+        ExternalProject_add(spot-ext
+            URL http://www.lrde.epita.fr/dload/spot/spot-2.9.6.tar.gz
+            URL_HASH SHA512=69ec8a3ce84b2c069bf40b8d2127e5085724c8e4ba88ffdefc3e2225f6334955959afd17bcfcde29fd6826d78d49a7f1303bd07ba756a8695473ff6cc5ade3a2
+            BUILD_COMMAND make
+            CONFIGURE_COMMAND CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} <SOURCE_DIR>/configure --prefix ${EXTERNAL_INSTALL_LOCATION} --disable-python --disable-devel --disable-debug --disable-shared --enable-static CFLAGS=-flto CXXFLAGS=-flto LDFLAGS=-fuse-linker-plugin
+            INSTALL_COMMAND make install
+        )
+    else ()
+        ExternalProject_add(spot-ext
+            URL http://www.lrde.epita.fr/dload/spot/spot-2.9.6.tar.gz
+            URL_HASH SHA512=69ec8a3ce84b2c069bf40b8d2127e5085724c8e4ba88ffdefc3e2225f6334955959afd17bcfcde29fd6826d78d49a7f1303bd07ba756a8695473ff6cc5ade3a2
+            BUILD_COMMAND make 
+            CONFIGURE_COMMAND CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} <SOURCE_DIR>/configure --prefix ${EXTERNAL_INSTALL_LOCATION} --disable-python --disable-devel --disable-debug --disable-shared --enable-static CFLAGS=${CMAKE_CXX_FLAGS} LDFLAGS=${CMAKE_LINKER_FLAGS}
+            INSTALL_COMMAND make install
+        )
+    endif ()
 
     if (WIN32) #If windows 32 or 64 
       set(GLPK_CFLAGS "-D __WOE__ -O3" )
 
=== modified file 'Scripts/MCC20/competition-scripts/tapaal.sh' (properties changed: -x to +x)
=== modified file 'include/CTL/Algorithm/CertainZeroFPA.h'
--- include/CTL/Algorithm/CertainZeroFPA.h	2020-03-02 21:03:24 +0000
+++ include/CTL/Algorithm/CertainZeroFPA.h	2021-04-02 18:07:40 +0000
@@ -27,9 +27,8 @@
     
     void checkEdge(DependencyGraph::Edge* e, bool only_assign = false);
     void finalAssign(DependencyGraph::Configuration *c, DependencyGraph::Assignment a);
+    void finalAssign(DependencyGraph::Edge *e, DependencyGraph::Assignment a);
     void explore(DependencyGraph::Configuration *c);
-    void addDependency(DependencyGraph::Edge *e,
-                          DependencyGraph::Configuration *target);
 
 };
 }
 
=== modified file 'include/CTL/DependencyGraph/Configuration.h'
--- include/CTL/DependencyGraph/Configuration.h	2020-03-10 13:29:26 +0000
+++ include/CTL/DependencyGraph/Configuration.h	2021-04-02 18:07:40 +0000
@@ -7,32 +7,29 @@
 #include <cstdio>
 #include <iostream>
 #include <vector>
+#include <forward_list>
 
 namespace DependencyGraph {
 
 class Edge;
 
-enum Assignment {
-    ONE = 1, UNKNOWN = 0, ZERO = -1, CZERO = -2
-};
-
 class Configuration
 {
+public:
+    std::forward_list<Edge*> dependency_set;   
+    uint32_t nsuccs = 0;
+private:
     uint32_t distance = 0;
-public:
-
-    uint32_t getDistance() const { return distance; }
     void setDistance(uint32_t value) { distance = value; }
-
+public:
+    int8_t assignment = UNKNOWN;
     Configuration() {}
-    virtual ~Configuration();
-
+    uint32_t getDistance() const { return distance; }
     bool isDone() const { return assignment == ONE || assignment == CZERO; }
-
-    uint32_t owner = 0;
-    uint32_t nsuccs = 0;
-    std::vector<Edge*> dependency_set;
-    Assignment assignment = UNKNOWN;
+    void addDependency(Edge* e);
+    void setOwner(uint32_t) { }
+    uint32_t getOwner() { return 0; }
+    
 };
 
 
 
=== modified file 'include/CTL/DependencyGraph/Edge.h'
--- include/CTL/DependencyGraph/Edge.h	2020-03-02 21:03:24 +0000
+++ include/CTL/DependencyGraph/Edge.h	2021-04-02 18:07:40 +0000
@@ -6,13 +6,17 @@
 #include <string>
 #include <algorithm>
 #include <cassert>
+#include <forward_list>
 
 namespace DependencyGraph {
 
 class Configuration;
+enum Assignment {
+    ONE = 1, UNKNOWN = 0, ZERO = -1, CZERO = -2
+};
 
 class Edge {
-    typedef std::vector<Configuration*> container;
+    typedef std::forward_list<Configuration*> container;
 public:
     Edge(){}
     Edge(Configuration &t_source) : source(&t_source) {}
@@ -20,17 +24,19 @@
     void addTarget(Configuration* conf)
     {
         assert(conf);
-        targets.push_back(conf);
+        targets.push_front(conf);
+        //++children;
     }
     
+    container targets;    
     Configuration* source;
-    container targets;
     uint8_t status = 0;
     bool processed = false;
     bool is_negated = false;
+    bool handled = false;
     int32_t refcnt = 0;
-    bool handled = false;
-    uint32_t weight = 0;
+    /*size_t children;
+    Assignment assignment;*/
 };
 }
 #endif // EDGE_H
 
=== modified file 'include/CTL/PetriNets/PetriConfig.h'
--- include/CTL/PetriNets/PetriConfig.h	2020-03-02 21:03:24 +0000
+++ include/CTL/PetriNets/PetriConfig.h	2021-04-02 18:07:40 +0000
@@ -20,8 +20,6 @@
         DependencyGraph::Configuration(), marking(t_marking), query(t_query) {
     }
 
-    virtual ~PetriConfig(){};
-
     size_t marking;
     Condition *query;
 
 
=== added directory 'include/LTL'
=== added directory 'include/LTL/Algorithm'
=== added file 'include/LTL/Algorithm/ModelChecker.h'
--- include/LTL/Algorithm/ModelChecker.h	1970-01-01 00:00:00 +0000
+++ include/LTL/Algorithm/ModelChecker.h	2021-04-02 18:07:40 +0000
@@ -0,0 +1,72 @@
+/* Copyright (C) 2020  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_MODELCHECKER_H
+#define VERIFYPN_MODELCHECKER_H
+
+#include "PetriEngine/PQL/PQL.h"
+#include "LTL/ProductSuccessorGenerator.h"
+#include "LTL/Algorithm/ProductPrinter.h"
+#include "PetriEngine/options.h"
+
+namespace LTL {
+
+    class ModelChecker {
+    public:
+        ModelChecker(const PetriEngine::PetriNet &net, PetriEngine::PQL::Condition_ptr, const bool shortcircuitweak,
+                     TraceLevel level = TraceLevel::Transitions);
+
+        virtual bool isSatisfied() = 0;
+
+        virtual ~ModelChecker() = default;
+
+        virtual void printStats(std::ostream &os) = 0;
+
+        [[nodiscard]] bool isweak() const { return is_weak; }
+
+    protected:
+        struct stats_t {
+            size_t explored = 0, expanded = 0;
+        };
+
+        stats_t stats;
+        virtual void _printStats(std::ostream &os, const PetriEngine::Structures::StateSetInterface &stateSet) {
+            std::cout   << "STATS:\n"
+                        << "\tdiscovered states: " << stateSet.discovered() << std::endl
+                        << "\texplored states:   " << stats.explored << std::endl
+                        << "\texpanded states:   " << stats.expanded << std::endl
+                        << "\tmax tokens:        " << stateSet.maxTokens() << std::endl;
+        }
+
+        std::unique_ptr<ProductSuccessorGenerator> successorGenerator;
+        const PetriEngine::PetriNet &net;
+        PetriEngine::PQL::Condition_ptr formula;
+        TraceLevel traceLevel;
+
+        size_t _discovered = 0;
+        const bool shortcircuitweak;
+        bool weakskip = false;
+        bool is_weak = false;
+        int maxTransName;
+
+        std::ostream &printTransition(size_t transition, LTL::Structures::ProductState &state, std::ostream &os);
+
+        void printLoop(std::ostream &os);
+    };
+}
+
+#endif //VERIFYPN_MODELCHECKER_H
 
=== added file 'include/LTL/Algorithm/NestedDepthFirstSearch.h'
--- include/LTL/Algorithm/NestedDepthFirstSearch.h	1970-01-01 00:00:00 +0000
+++ include/LTL/Algorithm/NestedDepthFirstSearch.h	2021-04-02 18:07:40 +0000
@@ -0,0 +1,91 @@
+/* Copyright (C) 2020  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_NESTEDDEPTHFIRSTSEARCH_H
+#define VERIFYPN_NESTEDDEPTHFIRSTSEARCH_H
+
+#include "ModelChecker.h"
+#include "PetriEngine/Structures/StateSet.h"
+#include "PetriEngine/Structures/State.h"
+#include "PetriEngine/Structures/Queue.h"
+#include "LTL/Structures/ProductStateFactory.h"
+
+#include <ptrie/ptrie_stable.h>
+#include <unordered_set>
+
+using namespace PetriEngine;
+
+namespace LTL {
+    /**
+     * Implement the nested DFS algorithm for LTL model checking. Roughly based on versions given in
+     * <p>
+     *   Jaco Geldenhuys & Antti Valmari,<br>
+     *   More efficient on-the-fly LTL verification with Tarjan's algorithm,<br>
+     *   https://doi.org/10.1016/j.tcs.2005.07.004
+     * </p>
+     * and
+     * <p>
+     *   Gerard J. Holzmann, Doron Peled, and Mihalis Yannakakis<br>
+     *   On Nested Depth First Search<br>
+     *   https://spinroot.com/gerard/pdf/inprint/spin96.pdf
+     * </p>
+     * For most use cases, Tarjan's algorithm (see LTL::TarjanModelChecker) is faster.
+     * @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 W>
+    class NestedDepthFirstSearch : public ModelChecker {
+    public:
+        NestedDepthFirstSearch(const PetriNet &net, PetriEngine::PQL::Condition_ptr ptr, const bool shortcircuitweak, TraceLevel level = TraceLevel::Full)
+                : ModelChecker(net, ptr, shortcircuitweak, level), factory{net, successorGenerator->initial_buchi_state()},
+                states(net, 0, (int)net.numberOfPlaces() + 1) {}
+
+        bool isSatisfied() override;
+
+        void printStats(std::ostream &os) override;
+
+    private:
+        using State = LTL::Structures::ProductState;
+
+        Structures::ProductStateFactory factory;
+        W states; //StateSet
+        std::set<size_t> mark1;
+        std::set<size_t> mark2;
+
+        struct StackEntry {
+            size_t id;
+            successor_info sucinfo;
+        };
+
+        State *seed;
+        bool violation = false;
+
+        //Used for printing the trace
+        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>;
+    };
+    extern template class NestedDepthFirstSearch<PetriEngine::Structures::StateSet>;
+    extern template class NestedDepthFirstSearch<PetriEngine::Structures::TracableStateSet>;
+}
+
+#endif //VERIFYPN_NESTEDDEPTHFIRSTSEARCH_H
 
=== added file 'include/LTL/Algorithm/ProductPrinter.h'
--- include/LTL/Algorithm/ProductPrinter.h	1970-01-01 00:00:00 +0000
+++ include/LTL/Algorithm/ProductPrinter.h	2021-04-02 18:07:40 +0000
@@ -0,0 +1,31 @@
+/* Copyright (C) 2020  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_PRODUCTPRINTER_H
+#define VERIFYPN_PRODUCTPRINTER_H
+
+#include "LTL/Structures/ProductStateFactory.h"
+#include "LTL/ProductSuccessorGenerator.h"
+#include "PetriEngine/Structures/StateSet.h"
+#include "PetriEngine/Structures/Queue.h"
+#include "PetriEngine/PQL/Contexts.h"
+
+namespace LTL::ProductPrinter {
+    void printProduct(ProductSuccessorGenerator &successorGenerator, std::ostream &os, const PetriEngine::PetriNet &net,
+                      PetriEngine::PQL::Condition_ptr formula);
+}
+#endif //VERIFYPN_PRODUCTPRINTER_H
 
=== added file 'include/LTL/Algorithm/RandomNDFS.h'
--- include/LTL/Algorithm/RandomNDFS.h	1970-01-01 00:00:00 +0000
+++ include/LTL/Algorithm/RandomNDFS.h	2021-04-02 18:07:40 +0000
@@ -0,0 +1,59 @@
+/* Copyright (C) 2020  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_RANDOMNDFS_H
+#define VERIFYPN_RANDOMNDFS_H
+
+#include "ModelChecker.h"
+#include "PetriEngine/Structures/StateSet.h"
+#include "PetriEngine/Structures/State.h"
+#include "PetriEngine/Structures/Queue.h"
+#include "LTL/Structures/ProductStateFactory.h"
+
+#include <ptrie/ptrie_stable.h>
+
+using namespace PetriEngine;
+
+namespace LTL {
+    class RandomNDFS : public ModelChecker {
+    public:
+        RandomNDFS(const PetriNet &net, PetriEngine::PQL::Condition_ptr ptr)
+                : ModelChecker(net, ptr, false), factory{net, successorGenerator->initial_buchi_state()},
+                  mark1(net, 0, (int) net.numberOfPlaces() + 1), mark2(net, 0, (int) net.numberOfPlaces() + 1) {}
+
+        bool isSatisfied() override;
+
+        void printStats(std::ostream &os) override;
+
+    private:
+        using State = LTL::Structures::ProductState;
+
+        Structures::ProductStateFactory factory;
+        PetriEngine::Structures::StateSet mark1;
+        PetriEngine::Structures::StateSet mark2;
+
+
+        State *seed;
+        bool violation = false;
+
+        void dfs();
+
+        void ndfs(State &state);
+    };
+}
+
+#endif //VERIFYPN_RANDOMNDFS_H
 
=== added file 'include/LTL/Algorithm/TarjanModelChecker.h'
--- include/LTL/Algorithm/TarjanModelChecker.h	1970-01-01 00:00:00 +0000
+++ include/LTL/Algorithm/TarjanModelChecker.h	2021-04-02 18:07:40 +0000
@@ -0,0 +1,140 @@
+/* Copyright (C) 2020  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_TARJANMODELCHECKER_H
+#define VERIFYPN_TARJANMODELCHECKER_H
+
+
+#include "LTL/Algorithm/ModelChecker.h"
+#include "LTL/Structures/ProductStateFactory.h"
+#include "PetriEngine/Structures/StateSet.h"
+
+#include <stack>
+#include <unordered_set>
+
+namespace LTL {
+
+    /**
+     * Implements on-the-fly version of Tarjan's algorithm suitable for LTL model checking.
+     * The idea is to detect some reachable strongly connected component containing an accepting state,
+     * which constitutes a counter-example.
+     * For more details see
+     * <p>
+     *   Jaco Geldenhuys & Antti Valmari,
+     *   More efficient on-the-fly LTL verification with Tarjan's algorithm,
+     *   https://doi.org/10.1016/j.tcs.2005.07.004
+     * </p>
+     * @tparam SaveTrace whether to save and print counter-examples when possible.
+     */
+    template<bool SaveTrace>
+    class TarjanModelChecker : public ModelChecker {
+    public:
+        TarjanModelChecker(const PetriEngine::PetriNet &net, const PetriEngine::PQL::Condition_ptr &cond, const bool shortcircuitweak,
+                           TraceLevel level = TraceLevel::Full)
+                : ModelChecker(net, cond, shortcircuitweak, level), factory(net, successorGenerator->initial_buchi_state()),
+                  seen(net, 0, (int) net.numberOfPlaces() + 1)
+        {
+            chash.fill(std::numeric_limits<idx_t>::max());
+        }
+
+        bool isSatisfied() override;
+
+        void printStats(std::ostream &os) override
+        {
+            _printStats(os, seen);
+        }
+
+    private:
+        using State = LTL::Structures::ProductState;
+        using idx_t = size_t;
+        // 64 MB hash table
+        static constexpr idx_t HashSz = 16777216;
+
+        LTL::Structures::ProductStateFactory factory;
+
+        using StateSet = std::conditional_t<SaveTrace, PetriEngine::Structures::TracableStateSet, PetriEngine::Structures::StateSet>;
+
+        StateSet seen;
+        std::unordered_set<idx_t> store;
+
+        // rudimentary hash table of state IDs. chash[hash(state)] is the top index in cstack
+        // corresponding to state. Collisions are resolved using linked list via CEntry::next.
+        std::array<idx_t, HashSz> chash;
+        static_assert(sizeof(chash) == (1U << 27U));
+
+        static inline idx_t hash(idx_t id)
+        {
+            return id % HashSz;
+        }
+
+        struct PlainCEntry {
+            idx_t lowlink;
+            idx_t stateid;
+            idx_t next = std::numeric_limits<idx_t>::max();
+
+            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;
+
+            TracableCEntry(idx_t lowlink, idx_t stateid, idx_t next) : PlainCEntry(lowlink, stateid, next) {}
+        };
+
+        using CEntry = std::conditional_t<SaveTrace,
+                TracableCEntry,
+                PlainCEntry>;
+
+
+        struct DEntry {
+            idx_t pos; // position in cstack.
+            successor_info sucinfo;
+        };
+
+        // master list of state information.
+        std::vector<CEntry> cstack;
+        // depth-first search stack, contains current search path.
+        std::stack<DEntry> dstack;
+        // cstack positions of accepting states in current search path, for quick access.
+        std::stack<idx_t> astack;
+        bool violation = false;
+        size_t loopstate = std::numeric_limits<size_t>::max();
+        size_t looptrans = std::numeric_limits<size_t>::max();
+
+        void push(State &state, size_t stateid);
+
+        void pop();
+
+        void update(idx_t to);
+
+        bool nexttrans(State &state, State &parent, DEntry &delem);
+
+        void popCStack();
+
+        void printTrace(std::stack<DEntry> &&dstack, std::ostream &os = std::cout);
+
+    };
+
+    extern template
+    class TarjanModelChecker<true>;
+
+    extern template
+    class TarjanModelChecker<false>;
+}
+
+#endif //VERIFYPN_TARJANMODELCHECKER_H
 
=== added file 'include/LTL/AlgorithmTypes.h'
--- include/LTL/AlgorithmTypes.h	1970-01-01 00:00:00 +0000
+++ include/LTL/AlgorithmTypes.h	2021-04-02 18:07:40 +0000
@@ -0,0 +1,40 @@
+/* Copyright (C) 2021  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ * 
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ * 
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ * 
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_ALGORITHMTYPES_H
+#define VERIFYPN_ALGORITHMTYPES_H
+
+namespace LTL {
+    enum class Algorithm {
+        NDFS, Tarjan, None=-1
+    };
+    inline auto to_string(Algorithm alg) {
+        switch (alg) {
+            case Algorithm::NDFS:
+                return "NDFS";
+            case Algorithm::Tarjan:
+                return "TARJAN";
+            case Algorithm::None:
+            default:
+                std::cerr << "to_string: Invalid LTL Algorithm " << static_cast<int>(alg) << '\n';
+                assert(false);
+                return "None";
+        }
+    }
+}
+
+#endif //VERIFYPN_ALGORITHMTYPES_H
 
=== added file 'include/LTL/BuchiSuccessorGenerator.h'
--- include/LTL/BuchiSuccessorGenerator.h	1970-01-01 00:00:00 +0000
+++ include/LTL/BuchiSuccessorGenerator.h	2021-04-02 18:07:40 +0000
@@ -0,0 +1,95 @@
+/* Copyright (C) 2020  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_BUCHISUCCESSORGENERATOR_H
+#define VERIFYPN_BUCHISUCCESSORGENERATOR_H
+
+#include "PetriEngine/SuccessorGenerator.h"
+#include "LTL/Structures/BuchiAutomaton.h"
+
+#include <spot/twa/twagraph.hh>
+#include <utility>
+#include <memory>
+
+namespace LTL {
+    class BuchiSuccessorGenerator {
+    public:
+        explicit BuchiSuccessorGenerator(Structures::BuchiAutomaton automaton)
+                : aut(std::move(automaton))
+        {
+            deleter = SuccIterDeleter{&aut};
+        }
+
+        void prepare(size_t state)
+        {
+            auto curstate = aut.buchi->state_from_number(state);
+            succ = _succ_iter{aut.buchi->succ_iter(curstate), SuccIterDeleter{&aut}};
+            succ->first();
+        }
+
+        bool next(size_t &state, bdd &cond)
+        {
+            if (!succ->done()) {
+                auto dst = succ->dst();
+                state = aut.buchi->state_number(dst);
+                cond = succ->cond();
+                succ->next();
+                dst->destroy();
+                return true;
+            }
+            return false;
+        }
+
+        [[nodiscard]] bool is_accepting(size_t state) const
+        {
+            return aut.buchi->state_is_accepting(state);
+        }
+
+        [[nodiscard]] size_t initial_state_number() const
+        {
+            return aut.buchi->get_init_state_number();
+        }
+
+        [[nodiscard]] PetriEngine::PQL::Condition_ptr getExpression(size_t i) const
+        {
+            return aut.ap_info.at(i).expression;
+        }
+
+        [[nodiscard]] bool is_weak() const
+        {
+            return (bool) aut.buchi->prop_weak();
+        }
+
+    private:
+        Structures::BuchiAutomaton aut;
+
+        struct SuccIterDeleter {
+            Structures::BuchiAutomaton *aut;
+
+            void operator()(spot::twa_succ_iterator *iter) const
+            {
+                aut->buchi->release_iter(iter);
+            }
+        };
+
+        SuccIterDeleter deleter{};
+
+        using _succ_iter = std::unique_ptr<spot::twa_succ_iterator, SuccIterDeleter>;
+        _succ_iter succ = nullptr;
+    };
+}
+#endif //VERIFYPN_BUCHISUCCESSORGENERATOR_H
 
=== added file 'include/LTL/LTL.h'
--- include/LTL/LTL.h	1970-01-01 00:00:00 +0000
+++ include/LTL/LTL.h	2021-04-02 18:07:40 +0000
@@ -0,0 +1,34 @@
+/* Copyright (C) 2020  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_LTLALGORITHM_H
+#define VERIFYPN_LTLALGORITHM_H
+
+#include "LTL/LTLValidator.h"
+#include "LTL/Algorithm/TarjanModelChecker.h"
+#include "LTL/Algorithm/NestedDepthFirstSearch.h"
+#include "LTL/Algorithm/RandomNDFS.h"
+#include "LTL/Simplification/SpotToPQL.h"
+#include "LTL/LTLToBuchi.h"
+
+namespace LTL {
+
+
+    std::pair<Condition_ptr, bool> to_ltl(const Condition_ptr &formula);
+}
+
+#endif
 \ No newline at end of file
 
=== added file 'include/LTL/LTLToBuchi.h'
--- include/LTL/LTLToBuchi.h	1970-01-01 00:00:00 +0000
+++ include/LTL/LTLToBuchi.h	2021-04-02 18:07:40 +0000
@@ -0,0 +1,131 @@
+/* Copyright (C) 2020  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_LTLTOBUCHI_H
+#define VERIFYPN_LTLTOBUCHI_H
+
+#include "PetriParse/QueryParser.h"
+#include "PetriEngine/PQL/QueryPrinter.h"
+
+#include <iostream>
+#include <string>
+
+#include <spot/tl/formula.hh>
+
+namespace LTL {
+    struct AtomicProposition {
+        PetriEngine::PQL::Condition_ptr expression;
+        std::string text;
+    };
+
+    using APInfo = std::vector<AtomicProposition>;
+    std::string toSpotFormat(const QueryItem &query);
+    void toSpotFormat(const QueryItem &query, std::ostream &os);
+    std::pair<spot::formula, APInfo> to_spot_formula(const PetriEngine::PQL::Condition_ptr& query);
+
+    class BuchiSuccessorGenerator;
+    BuchiSuccessorGenerator makeBuchiAutomaton(const PetriEngine::PQL::Condition_ptr &query);
+
+
+    class FormulaToSpotSyntax : public PetriEngine::PQL::QueryPrinter {
+    protected:
+        void _accept(const PetriEngine::PQL::ACondition *condition) override;
+
+        void _accept(const PetriEngine::PQL::ECondition *condition) override;
+
+        void _accept(const PetriEngine::PQL::NotCondition *element) override;
+
+        void _accept(const PetriEngine::PQL::AndCondition *element) override;
+
+        void _accept(const PetriEngine::PQL::OrCondition *element) override;
+
+        void _accept(const PetriEngine::PQL::LessThanCondition *element) override;
+
+        void _accept(const PetriEngine::PQL::LessThanOrEqualCondition *element) override;
+
+        void _accept(const PetriEngine::PQL::EqualCondition *element) override;
+
+        void _accept(const PetriEngine::PQL::NotEqualCondition *element) override;
+
+        void _accept(const PetriEngine::PQL::UnfoldedFireableCondition *element) override;
+
+        void _accept(const PetriEngine::PQL::FireableCondition *element) override;
+
+        void _accept(const PetriEngine::PQL::BooleanCondition *element) override;
+
+        void _accept(const PetriEngine::PQL::LiteralExpr *element) override;
+
+        void _accept(const PetriEngine::PQL::PlusExpr *element) override;
+
+        void _accept(const PetriEngine::PQL::MultiplyExpr *element) override;
+
+        void _accept(const PetriEngine::PQL::MinusExpr *element) override;
+
+        void _accept(const PetriEngine::PQL::SubtractExpr *element) override;
+
+        void _accept(const PetriEngine::PQL::IdentifierExpr *element) override;
+
+        void _accept(const PetriEngine::PQL::CompareConjunction *element) override;
+
+    public:
+
+        explicit FormulaToSpotSyntax(std::ostream &os = std::cout)
+                : PetriEngine::PQL::QueryPrinter(os), compress(true) {}
+
+        auto begin() const {
+            return std::begin(ap_info);
+        }
+
+        auto end() const {
+            return std::end(ap_info);
+        }
+
+        const APInfo &apInfo() const {
+            return ap_info;
+        }
+
+    private:
+        APInfo ap_info;
+        bool is_quoted = false;
+        bool compress;
+
+        void make_atomic_prop(const PetriEngine::PQL::Condition_constptr &element)
+        {
+            auto cond =
+                const_cast<PetriEngine::PQL::Condition *>(element.get())->shared_from_this();
+            std::stringstream ss;
+            ss << "\"";
+            if (compress) {
+                // FIXME Very naive; this completely removes APs being in multiple places in the query,
+                // leading to some query not being answered as is. The net gain is large in the firebaility category,
+                // but ideally it would be possible to make a smarter approach that looks at previously stored APs
+                // and efficiently checks for repeat APs such that we can reuse APs.
+                ss << ap_info.size();
+            }
+            else {
+                PetriEngine::PQL::QueryPrinter _printer{ss};
+                cond->visit(_printer);
+            }
+            ss << "\"";
+            os << ss.str();
+            ap_info.push_back(AtomicProposition{cond, ss.str().substr(1, ss.str().size() - 2)});
+        }
+    };
+
+}
+
+#endif //VERIFYPN_LTLTOBUCHI_H
 
=== added file 'include/LTL/LTLValidator.h'
--- include/LTL/LTLValidator.h	1970-01-01 00:00:00 +0000
+++ include/LTL/LTLValidator.h	2021-04-02 18:07:40 +0000
@@ -0,0 +1,201 @@
+/* Copyright (C) 2020  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_LTLVALIDATOR_H
+#define VERIFYPN_LTLVALIDATOR_H
+
+#include "PetriEngine/PQL/Visitor.h"
+
+namespace LTL {
+    using namespace PetriEngine::PQL;
+    class LTLValidator : public PetriEngine::PQL::Visitor {
+    public:
+        bool bad() const { return _bad; }
+
+        operator bool() const { return !bad(); }
+
+        bool isLTL(const Condition_ptr& condition) {
+            std::shared_ptr<SimpleQuantifierCondition> quantifierCondition;
+            if ((quantifierCondition = std::dynamic_pointer_cast<ACondition>(condition)) != nullptr ||
+                (quantifierCondition = std::dynamic_pointer_cast<ECondition>(condition)) != nullptr ){
+                (*quantifierCondition)[0]->visit(*this);
+            } else {
+                condition->visit(*this);
+            }
+            return !bad();
+        }
+
+    protected:
+
+        void _visitNary(const LogicalCondition *condition) {
+            for (const auto &cond : *condition) {
+                cond->visit(*this);
+            }
+        };
+
+        void _accept(const PetriEngine::PQL::EFCondition *condition) override {
+            setBad();
+            std::cerr << "found EFCondition" << std::endl;
+        }
+
+        void _accept(const PetriEngine::PQL::EGCondition *condition) override {
+            setBad();
+            std::cerr << "found EGCondition" << std::endl;
+        }
+
+        void _accept(const PetriEngine::PQL::AGCondition *condition) override {
+            setBad();
+            std::cerr << "found AGCondition" << std::endl;
+        }
+
+        void _accept(const PetriEngine::PQL::AFCondition *condition) override {
+            setBad();
+            std::cerr << "found AFCondition" << std::endl;
+        }
+
+        void _accept(const PetriEngine::PQL::EXCondition *condition) override {
+            setBad();
+            std::cerr << "found EXCondition" << std::endl;
+        }
+
+        void _accept(const PetriEngine::PQL::AXCondition *condition) override {
+            setBad();
+            std::cerr << "found AXCondition" << std::endl;
+        }
+
+        void _accept(const PetriEngine::PQL::EUCondition *condition) override {
+            setBad();
+            std::cerr << "found EUCondition" << std::endl;
+        }
+
+        void _accept(const PetriEngine::PQL::AUCondition *condition) override {
+            setBad();
+            std::cerr << "found AUCondition" << std::endl;
+        }
+
+        void _accept(const PetriEngine::PQL::ACondition *condition) override {
+            setBad();
+        }
+
+        void _accept(const PetriEngine::PQL::ECondition *condition) override {
+            setBad();
+        }
+
+        void _accept(const PetriEngine::PQL::NotCondition *element) override {
+            (*element)[0]->visit(*this);
+        }
+
+        void _accept(const PetriEngine::PQL::AndCondition *element) override {
+            _visitNary(element);
+        }
+
+        void _accept(const PetriEngine::PQL::OrCondition *element) override {
+            _visitNary(element);
+        }
+
+        void _accept(const PetriEngine::PQL::LessThanCondition *element) override {
+            (*element)[0]->visit(*this);
+            (*element)[1]->visit(*this);
+        }
+
+        void _accept(const PetriEngine::PQL::LessThanOrEqualCondition *element) override {
+            (*element)[0]->visit(*this);
+            (*element)[1]->visit(*this);
+        }
+
+        void _accept(const PetriEngine::PQL::EqualCondition *element) override {
+            (*element)[0]->visit(*this);
+            (*element)[1]->visit(*this);
+        }
+
+        void _accept(const PetriEngine::PQL::NotEqualCondition *element) override {
+            (*element)[0]->visit(*this);
+            (*element)[1]->visit(*this);
+        }
+
+        void _accept(const PetriEngine::PQL::DeadlockCondition *element) override {
+
+        }
+
+        void _accept(const PetriEngine::PQL::CompareConjunction *element) override {
+
+        }
+
+        void _accept(const PetriEngine::PQL::UnfoldedUpperBoundsCondition *element) override {
+
+        }
+
+        void _accept(const PetriEngine::PQL::GCondition *condition) override {
+            (*condition)[0]->visit(*this);
+        }
+
+        void _accept(const PetriEngine::PQL::FCondition *condition) override {
+            (*condition)[0]->visit(*this);
+        }
+
+        void _accept(const PetriEngine::PQL::XCondition *condition) override {
+            (*condition)[0]->visit(*this);
+        }
+
+        void _accept(const PetriEngine::PQL::UntilCondition *condition) override {
+            (*condition)[0]->visit(*this);
+        }
+
+        void _accept(const PetriEngine::PQL::UnfoldedFireableCondition *element) override {
+        }
+
+        void _accept(const PetriEngine::PQL::FireableCondition *element) override {
+        }
+
+        void _accept(const PetriEngine::PQL::UpperBoundsCondition *element) override {
+        }
+
+        void _accept(const PetriEngine::PQL::LivenessCondition *element) override {
+        }
+
+        void _accept(const PetriEngine::PQL::KSafeCondition *element) override {
+        }
+
+        void _accept(const PetriEngine::PQL::QuasiLivenessCondition *element) override {
+        }
+
+        void _accept(const PetriEngine::PQL::StableMarkingCondition *element) override {
+        }
+
+        void _accept(const PetriEngine::PQL::BooleanCondition *element) override {}
+
+        void _accept(const PetriEngine::PQL::UnfoldedIdentifierExpr *element) override {}
+
+        void _accept(const PetriEngine::PQL::LiteralExpr *element) override {}
+
+        void _accept(const PetriEngine::PQL::PlusExpr *element) override {}
+
+        void _accept(const PetriEngine::PQL::MultiplyExpr *element) override {}
+
+        void _accept(const PetriEngine::PQL::MinusExpr *element) override {}
+
+        void _accept(const PetriEngine::PQL::SubtractExpr *element) override {}
+
+        void _accept(const PetriEngine::PQL::IdentifierExpr *element) override {}
+
+    private:
+        bool _bad = false;
+
+        void setBad() { _bad = true; }
+    };
+}
+#endif //VERIFYPN_LTLVALIDATOR_H
 
=== added file 'include/LTL/ProductSuccessorGenerator.h'
--- include/LTL/ProductSuccessorGenerator.h	1970-01-01 00:00:00 +0000
+++ include/LTL/ProductSuccessorGenerator.h	2021-04-02 18:07:40 +0000
@@ -0,0 +1,146 @@
+/* Copyright (C) 2020  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_PRODUCTSUCCESSORGENERATOR_H
+#define VERIFYPN_PRODUCTSUCCESSORGENERATOR_H
+
+#include "PetriEngine/SuccessorGenerator.h"
+#include "PetriEngine/PQL/PQL.h"
+#include "LTL/Structures/ProductState.h"
+#include "LTL/BuchiSuccessorGenerator.h"
+#include "LTL/LTLToBuchi.h"
+
+
+namespace LTL {
+    /**
+     * type holding sufficient information to resume successor generation for a state from a given point.
+     */
+    struct successor_info {
+        uint32_t pcounter;
+        uint32_t tcounter;
+        size_t buchi_state;
+        size_t last_state;
+
+        friend bool operator==(const successor_info &lhs, const successor_info &rhs) {
+            return lhs.pcounter == rhs.pcounter &&
+                   lhs.tcounter == rhs.tcounter &&
+                   lhs.buchi_state == rhs.buchi_state &&
+                   lhs.last_state == rhs.last_state;
+        }
+
+        friend bool operator!=(const successor_info &lhs, const successor_info &rhs) {
+            return !(rhs == lhs);
+        }
+
+        inline bool has_pcounter() const {
+            return pcounter != NoPCounter;
+        }
+
+        inline bool has_tcounter() const {
+            return tcounter != NoTCounter;
+        }
+
+        inline bool has_buchistate() const {
+            return buchi_state != NoBuchiState;
+        }
+
+        inline bool has_prev_state() const {
+            return last_state != NoLastState;
+        }
+
+        static constexpr auto NoPCounter = 0;
+        static constexpr auto NoTCounter = std::numeric_limits<uint32_t>::max();
+        static constexpr auto NoBuchiState = std::numeric_limits<size_t>::max();
+        static constexpr auto NoLastState = std::numeric_limits<size_t>::max();
+    };
+
+    constexpr successor_info initial_suc_info{
+            successor_info::NoPCounter,
+            successor_info::NoTCounter,
+            successor_info::NoBuchiState,
+            successor_info::NoLastState
+    };
+
+    class ProductSuccessorGenerator : public PetriEngine::SuccessorGenerator {
+    public:
+
+        ProductSuccessorGenerator(const PetriEngine::PetriNet &net,
+                                  const PetriEngine::PQL::Condition_ptr &cond)
+                : PetriEngine::SuccessorGenerator(net), buchi(makeBuchiAutomaton(cond)) {}
+
+        [[nodiscard]] size_t initial_buchi_state() const { return buchi.initial_state_number(); };
+
+        void prepare(const LTL::Structures::ProductState *state);
+
+        bool next(LTL::Structures::ProductState &state);
+
+        bool isAccepting(const LTL::Structures::ProductState &state);
+
+        void makeInitialState(std::vector<LTL::Structures::ProductState> &states) {
+            auto buf = new PetriEngine::MarkVal[_net.numberOfPlaces() + 1];
+            std::copy(_net.initial(), _net.initial() + _net.numberOfPlaces(), buf);
+            buf[_net.numberOfPlaces()] = 0;
+            LTL::Structures::ProductState state;
+            state.setMarking(buf, _net.numberOfPlaces());
+            state.setBuchiState(initial_buchi_state());
+            buchi.prepare(state.getBuchiState());
+            while (next_buchi_succ(state)) {
+                states.emplace_back();
+                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());
+            }
+        }
+
+        [[nodiscard]] bool isInitialState(const LTL::Structures::ProductState &state) const {
+            return state.markingEqual(_net.initial());
+        }
+
+        /**
+         * prepare a state for successor generation, starting from specific point in iteration
+         * @param state the source state to generate successors from
+         * @param sucinfo the point in the iteration to start from, as returned by `next`.
+         */
+        void prepare(const LTL::Structures::ProductState *state, const successor_info &sucinfo);
+
+        /**
+         * compute the next successor from the last state that was sent to `prepare`.
+         * @param[out] state the state to write
+         * @param[out] sucinfo checkpoint information from which iteration can later be resumed.
+         * @return `true` if a successor was successfully generated, `false` otherwise.
+         * @warning do not use the same State for both prepare and next, this will cause wildly incorrect behaviour!
+         */
+        bool next(Structures::ProductState &state, successor_info &sucinfo);
+
+        [[nodiscard]] bool is_weak() const {
+            return buchi.is_weak();
+        }
+
+    private:
+        BuchiSuccessorGenerator buchi;
+        bdd cond;
+        size_t buchi_parent;
+        bool fresh_marking = true;
+
+        bool guard_valid(const PetriEngine::Structures::State &state, bdd bdd);
+
+        bool next_buchi_succ(LTL::Structures::ProductState &state);
+    };
+
+}
+
+#endif //VERIFYPN_PRODUCTSUCCESSORGENERATOR_H
 
=== added directory 'include/LTL/Simplification'
=== added file 'include/LTL/Simplification/SpotToPQL.h'
--- include/LTL/Simplification/SpotToPQL.h	1970-01-01 00:00:00 +0000
+++ include/LTL/Simplification/SpotToPQL.h	2021-04-02 18:07:40 +0000
@@ -0,0 +1,42 @@
+/* Copyright (C) 2020  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_SPOTTOPQL_H
+#define VERIFYPN_SPOTTOPQL_H
+
+#include "PetriEngine/PQL/Expressions.h"
+#include "LTL/LTLToBuchi.h"
+#include <spot/tl/formula.hh>
+
+namespace LTL {
+    /**
+     * Transform a Spot formula back into the PQL expression tree form.
+     * @param formula The formula to translate to PQL
+     * @param apinfo List of atomic propositions in the formula. This should have been created by {@link LTL::to_spot_formula}.
+     * @return A PQL formula equivalent to the passed spot formula.
+     */
+    PetriEngine::PQL::Condition_ptr toPQL(const spot::formula &formula, const APInfo &apinfo);
+
+    /**
+     * Simplify an LTL formula using Spot's formula simplifier. Throws if formula is not valid LTL.
+     * @param formula The formula to simplify.
+     * @return the simplified formula.
+     */
+    PetriEngine::PQL::Condition_ptr simplify(const PetriEngine::PQL::Condition_ptr &formula);
+}
+
+#endif // VERIFYPN_SPOTTOPQL_H
 
=== added directory 'include/LTL/Structures'
=== added file 'include/LTL/Structures/BuchiAutomaton.h'
--- include/LTL/Structures/BuchiAutomaton.h	1970-01-01 00:00:00 +0000
+++ include/LTL/Structures/BuchiAutomaton.h	2021-04-02 18:07:40 +0000
@@ -0,0 +1,31 @@
+/* Copyright (C) 2020  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_BUCHIAUTOMATON_H
+#define VERIFYPN_BUCHIAUTOMATON_H
+
+#include "LTL/LTLToBuchi.h"
+#include <spot/twa/twagraph.hh>
+
+namespace LTL::Structures {
+    struct BuchiAutomaton {
+        spot::twa_graph_ptr buchi;
+        const std::unordered_map<int, AtomicProposition> ap_info;
+    };
+}
+
+#endif //VERIFYPN_BUCHIAUTOMATON_H
 
=== added file 'include/LTL/Structures/ProductState.h'
--- include/LTL/Structures/ProductState.h	1970-01-01 00:00:00 +0000
+++ include/LTL/Structures/ProductState.h	2021-04-02 18:07:40 +0000
@@ -0,0 +1,81 @@
+/* Copyright (C) 2020  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_PRODUCTSTATE_H
+#define VERIFYPN_PRODUCTSTATE_H
+
+#include "PetriEngine/Structures/State.h"
+
+namespace LTL {
+    class ProductSuccessorGenerator;
+}
+namespace LTL::Structures {
+    /**
+     * State on the form (M, q) for marking M and NBA state q.
+     * Represented as array of size nplaces + 1, where the last element is the number
+     * of NBA state q, and the first nplaces elements are the actual marking.
+     */
+    class ProductState : public PetriEngine::Structures::State {
+    public:
+        ProductState() : PetriEngine::Structures::State() {}
+
+        void setMarking(PetriEngine::MarkVal* marking, size_t nplaces)
+        {
+            State::setMarking(marking);
+            // because zero-indexing
+            buchi_state_idx = nplaces;
+        }
+
+        //TODO override equality operators to handle both marking and NBA state
+        size_t getBuchiState() const {
+            return marking()[buchi_state_idx];
+        }
+
+        void setBuchiState(size_t state) {
+            marking()[buchi_state_idx] = state;
+        }
+
+        [[nodiscard]] bool markingEqual(const PetriEngine::MarkVal *rhs) const {
+            for (size_t i = 0; i < buchi_state_idx; ++i) {
+                if (marking()[i] != rhs[i]) {
+                    return false;
+                }
+            }
+            return true;
+        }
+
+        bool operator==(const ProductState &rhs) const {
+            for (size_t i = 0; i <= buchi_state_idx; ++i) {
+                if (marking()[i] != rhs.marking()[i]) {
+                    return false;
+                }
+            }
+            return true;
+        }
+
+        size_t size() const { return buchi_state_idx + 1; }
+
+        bool operator!=(const ProductState &rhs) const {
+            return !(rhs == *this);
+        }
+    private:
+        friend class LTL::ProductSuccessorGenerator;
+        size_t buchi_state_idx;
+    };
+}
+
+#endif //VERIFYPN_PRODUCTSTATE_H
 
=== added file 'include/LTL/Structures/ProductStateFactory.h'
--- include/LTL/Structures/ProductStateFactory.h	1970-01-01 00:00:00 +0000
+++ include/LTL/Structures/ProductStateFactory.h	2021-04-02 18:07:40 +0000
@@ -0,0 +1,46 @@
+/* Copyright (C) 2020  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_PRODUCTSTATEFACTORY_H
+#define VERIFYPN_PRODUCTSTATEFACTORY_H
+
+#include "LTL/Structures/ProductState.h"
+
+#include <memory>
+
+namespace LTL::Structures{
+    class ProductStateFactory {
+    public:
+        ProductStateFactory(const PetriEngine::PetriNet &net, size_t initial_buchi_state)
+            : net(net), 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;
+            state.setMarking(buf, net.numberOfPlaces());
+            state.setBuchiState(buchi_init);
+            return state;
+        }
+
+    private:
+        const PetriEngine::PetriNet &net;
+        const size_t buchi_init;
+    };
+}
+#endif //VERIFYPN_PRODUCTSTATEFACTORY_H
 
=== added file 'include/PetriEngine/Colored/ArcIntervals.h'
--- include/PetriEngine/Colored/ArcIntervals.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/Colored/ArcIntervals.h	2021-04-02 18:07:40 +0000
@@ -0,0 +1,108 @@
+/* Copyright (C) 2020  Alexander Bilgram <[e-mail]>,
+ *                     Peter Haar Taankvist <[e-mail]>,
+ *                     Thomas Pedersen <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef ARCINTERVALS_H
+#define ARCINTERVALS_H
+
+#include "Colors.h"
+
+namespace PetriEngine {
+    namespace Colored {
+
+        struct ArcIntervals {
+            std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>> _varIndexModMap;
+            std::vector<Colored::intervalTuple_t> _intervalTupleVec;
+            Colored::ColorFixpoint * _source;
+            
+            ~ArcIntervals() {_varIndexModMap.clear();}
+            ArcIntervals() {
+            }
+
+            ArcIntervals(Colored::ColorFixpoint * source) : _source(source){
+            }
+
+            ArcIntervals(Colored::ColorFixpoint * source, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>> varIndexModMap) : _varIndexModMap(varIndexModMap), _source(source) {
+            };
+
+            ArcIntervals(Colored::ColorFixpoint * source, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>> varIndexModMap,  std::vector<Colored::intervalTuple_t> ranges) : _varIndexModMap(varIndexModMap), _intervalTupleVec(ranges), _source(source) {
+            };
+
+            size_t size() {
+                return _intervalTupleVec.size();
+            }
+
+            Colored::intervalTuple_t& operator[] (size_t index) {
+                return _intervalTupleVec[index];
+            }
+            
+            Colored::intervalTuple_t& operator[] (int index) {
+                return _intervalTupleVec[index];
+            }
+            
+            Colored::intervalTuple_t& operator[] (uint32_t index) {
+                assert(index < _intervalTupleVec.size());
+                return _intervalTupleVec[index];
+            }
+
+            Colored::intervalTuple_t& back(){
+                return _intervalTupleVec.back();
+            }
+
+            bool hasValidIntervals(){
+                for(auto intervalTuple : _intervalTupleVec){
+                    if (intervalTuple.hasValidIntervals()){
+                        return true;
+                    }
+                }
+                return false;
+            }
+
+            bool containsVariable(Colored::Variable * var){
+                for (auto varModPair : _varIndexModMap){
+                    if(varModPair.first == var){
+                        return true;
+                    }
+                }
+                return false;
+            }
+
+            std::set<const Colored::Variable *> getVariables(){
+                std::set<const Colored::Variable *> res;
+                for (auto varModPair : _varIndexModMap){
+                    res.insert(varModPair.first);
+                }
+                return res;
+            }
+
+            void print() {
+                std::cout << "[ ";
+                for(auto varModifierPair : _varIndexModMap){
+                    std::cout << "(" << varModifierPair.first->name << ", " << varModifierPair.first->colorType->productSize() <<  ") ";
+                }
+                std::cout << "]" << std::endl;
+                for(auto intervalTuple: _intervalTupleVec){
+                    std::cout << "--------------------------------------------------------------------" << std::endl;
+                    intervalTuple.print();
+                    std::cout << "--------------------------------------------------------------------" << std::endl;
+                }
+            }
+        };
+    }
+}
+
+#endif /* INTERVALGENERATOR_H */
 \ No newline at end of file
 
=== added file 'include/PetriEngine/Colored/BindingGenerator.h'
--- include/PetriEngine/Colored/BindingGenerator.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/Colored/BindingGenerator.h	2021-04-02 18:07:40 +0000
@@ -0,0 +1,71 @@
+/* Copyright (C) 2020  Alexander Bilgram <[e-mail]>,
+ *                     Peter Haar Taankvist <[e-mail]>,
+ *                     Thomas Pedersen <[e-mail]>
+ *                     Andreas H. Klostergaard
+ *
+ * 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/>.
+ */
+
+#include <vector>
+#include <unordered_map>
+
+#include "ColoredNetStructures.h"
+
+namespace PetriEngine {
+
+    typedef std::unordered_map<std::string, Colored::ColorType*> ColorTypeMap;
+
+    class FixpointBindingGenerator {
+    public:
+        class Iterator {
+        private:
+            FixpointBindingGenerator* _generator;
+                        
+        public:
+            Iterator(FixpointBindingGenerator* generator);
+            
+            bool operator==(Iterator& other);
+            bool operator!=(Iterator& other);
+            Iterator& operator++();
+            const Colored::ExpressionContext::BindingMap operator++(int);
+            Colored::ExpressionContext::BindingMap& operator*();
+        };
+    private:
+        Colored::GuardExpression_ptr _expr;
+        Colored::ExpressionContext::BindingMap _bindings;
+        ColorTypeMap& _colorTypes;
+        Colored::Transition &_transition;
+        bool _isDone;
+        bool _noValidBindings;
+        uint32_t _nextIndex = 0;
+        
+        bool eval();
+        
+    public:
+        FixpointBindingGenerator(Colored::Transition& transition,
+                ColorTypeMap& colorTypes);
+
+        FixpointBindingGenerator(const FixpointBindingGenerator& ) = default;
+        
+        FixpointBindingGenerator operator= (const FixpointBindingGenerator& b) {
+            return FixpointBindingGenerator(b);
+        }
+
+        Colored::ExpressionContext::BindingMap& nextBinding();
+        Colored::ExpressionContext::BindingMap& currentBinding();
+        bool isInitial() const;
+        Iterator begin();
+        Iterator end();
+    };    
+}
 \ No newline at end of file
 
=== modified file 'include/PetriEngine/Colored/ColoredNetStructures.h'
--- include/PetriEngine/Colored/ColoredNetStructures.h	2020-03-02 21:03:24 +0000
+++ include/PetriEngine/Colored/ColoredNetStructures.h	2021-04-02 18:07:40 +0000
@@ -1,14 +1,20 @@
-/*
- * To change this license header, choose License Headers in Project Properties.
- * To change this template file, choose Tools | Templates
- * and open the template in the editor.
- */
-
-/* 
- * File:   ColoredNetStructures.h
- * Author: Klostergaard
- *
- * Created on 17. februar 2018, 17:07
+/* Copyright (C) 2020  Alexander Bilgram <[e-mail]>,
+ *                     Peter Haar Taankvist <[e-mail]>,
+ *                     Thomas Pedersen <[e-mail]>
+ *                     Andreas H. Klostergaard
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
  */
 
 #ifndef COLOREDNETSTRUCTURES_H
@@ -16,6 +22,7 @@
 
 #include <vector>
 #include <set>
+#include <assert.h>
 #include "Colors.h"
 #include "Expressions.h"
 #include "Multiset.h"
@@ -33,7 +40,10 @@
         struct Transition {
             std::string name;
             GuardExpression_ptr guard;
-            std::vector<Arc> arcs;
+            std::vector<Arc> input_arcs;
+            std::vector<Arc> output_arcs;
+            std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>> variableMaps;
+            bool considered;
         };
         
         struct Place {
 
=== modified file 'include/PetriEngine/Colored/ColoredPetriNetBuilder.h'
--- include/PetriEngine/Colored/ColoredPetriNetBuilder.h	2020-03-02 21:03:24 +0000
+++ include/PetriEngine/Colored/ColoredPetriNetBuilder.h	2021-04-02 18:07:40 +0000
@@ -1,8 +1,20 @@
-/*
- * File:   ColoredPetriNetBuilder.h
- * Author: Klostergaard
- *
- * Created on 17. februar 2018, 16:25
+/* Copyright (C) 2020  Alexander Bilgram <[e-mail]>,
+ *                     Peter Haar Taankvist <[e-mail]>,
+ *                     Thomas Pedersen <[e-mail]>
+ *                     Andreas H. Klostergaard
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
  */
 
 #ifndef COLOREDPETRINETBUILDER_H
@@ -11,14 +23,16 @@
 #include <vector>
 #include <unordered_map>
 
-#include "ColoredNetStructures.h"
 #include "../AbstractPetriNetBuilder.h"
 #include "../PetriNetBuilder.h"
+#include "BindingGenerator.h"
+#include "IntervalGenerator.h"
+#include "ArcIntervals.h"
 
 namespace PetriEngine {
+
     class ColoredPetriNetBuilder : public AbstractPetriNetBuilder {
     public:
-        typedef std::unordered_map<std::string, Colored::ColorType*> ColorTypeMap;
         typedef std::unordered_map<std::string, std::unordered_map<uint32_t , std::string>> PTPlaceMap;
         typedef std::unordered_map<std::string, std::vector<std::string>> PTTransitionMap;
         
@@ -66,10 +80,18 @@
             return _time;
         }
 
+        double getFixpointTime() const {
+            return _fixPointCreationTime;
+        }
+
         uint32_t getPlaceCount() const {
             return _places.size();
         }
 
+        uint32_t getMaxIntervals() const {
+            return _maxIntervals;
+        }
+
         uint32_t getTransitionCount() const {
             return _transitions.size();
         }
@@ -77,7 +99,8 @@
         uint32_t getArcCount() const {
             uint32_t sum = 0;
             for (auto& t : _transitions) {
-                sum += t.arcs.size();
+                sum += t.input_arcs.size();
+                sum += t.output_arcs.size();
             }
             return sum;
         }
@@ -109,71 +132,69 @@
         
         PetriNetBuilder& unfold();
         PetriNetBuilder& stripColors();
+        void computePlaceColorFixpoint(uint32_t maxIntervals, uint32_t maxIntervalsReduced, int32_t timeout);
+        
     private:
         std::unordered_map<std::string,uint32_t> _placenames;
         std::unordered_map<std::string,uint32_t> _transitionnames;
+        std::unordered_map<uint32_t, std::unordered_map<uint32_t, Colored::ArcIntervals>> _arcIntervals;
+        std::unordered_map<uint32_t,std::vector<uint32_t>> _placePostTransitionMap;
+        std::unordered_map<uint32_t,FixpointBindingGenerator> _bindings;
         PTPlaceMap _ptplacenames;
         PTTransitionMap _pttransitionnames;
         uint32_t _nptplaces = 0;
         uint32_t _npttransitions = 0;
         uint32_t _nptarcs = 0;
+        uint32_t _maxIntervals = 0;
+        PetriEngine::IntervalGenerator intervalGenerator;
         
         std::vector<Colored::Place> _places;
         std::vector<Colored::Transition> _transitions;
         std::vector<Colored::Arc> _arcs;
+        std::vector<Colored::ColorFixpoint> _placeColorFixpoints;
         ColorTypeMap _colors;
         PetriNetBuilder _ptBuilder;
         bool _unfolded = false;
         bool _stripped = false;
 
+        std::vector<uint32_t> _placeFixpointQueue;
+
         double _time;
+        double _fixPointCreationTime;
+
+        double _timer;
 
         std::string arcToString(Colored::Arc& arc) const ;
+
+        void printPlaceTable();
+
+        std::unordered_map<uint32_t, Colored::ArcIntervals> setupTransitionVars(Colored::Transition transition);
         
         void addArc(const std::string& place,
                 const std::string& transition,
                 const Colored::ArcExpression_ptr& expr,
                 bool input);
+
+
+        void getArcIntervals(Colored::Transition& transition, bool &transitionActivated, uint32_t max_intervals, uint32_t transitionId);      
+        void processInputArcs(Colored::Transition& transition, uint32_t currentPlaceId, uint32_t transitionId, bool &transitionActivated, uint32_t max_intervals);
+        void processOutputArcs(Colored::Transition& transition);
         
-        void unfoldPlace(Colored::Place& place);
+        void unfoldPlace(const Colored::Place* place, const PetriEngine::Colored::Color *color);
         void unfoldTransition(Colored::Transition& transition);
-        void unfoldArc(Colored::Arc& arc, Colored::ExpressionContext::BindingMap& binding, std::string& name);
+        void handleOrphanPlace(Colored::Place& place, std::unordered_map<std::string, uint32_t> unfoldedPlaceMap);
+
+        void unfoldArc(Colored::Arc& arc, Colored::ExpressionContext::BindingMap& binding, std::string& name, bool input);
     };
     
-    class BindingGenerator {
-    public:
-        class Iterator {
-        private:
-            BindingGenerator* _generator;
-            
-        public:
-            Iterator(BindingGenerator* generator);
-            
-            bool operator==(Iterator& other);
-            bool operator!=(Iterator& other);
-            Iterator& operator++();
-            const Colored::ExpressionContext::BindingMap operator++(int);
-            Colored::ExpressionContext::BindingMap& operator*();
-        };
-    private:
-        Colored::GuardExpression_ptr _expr;
-        Colored::ExpressionContext::BindingMap _bindings;
-        ColoredPetriNetBuilder::ColorTypeMap& _colorTypes;
-        
-        bool eval();
-        
-    public:
-        BindingGenerator(Colored::Transition& transition,
-                const std::vector<Colored::Arc>& arcs,
-                ColoredPetriNetBuilder::ColorTypeMap& colorTypes);
+    //Used for checking if a variable is inside either a succ or pred expression
+    enum ExpressionType {
+        None,
+        Pred,
+        Succ
+    };
+ 
 
-        Colored::ExpressionContext::BindingMap& nextBinding();
-        Colored::ExpressionContext::BindingMap& currentBinding();
-        bool isInitial() const;
-        Iterator begin();
-        Iterator end();
-    };
 }
 
 #endif /* COLOREDPETRINETBUILDER_H */
-
 
=== modified file 'include/PetriEngine/Colored/Colors.h'
--- include/PetriEngine/Colored/Colors.h	2020-03-02 22:05:53 +0000
+++ include/PetriEngine/Colored/Colors.h	2021-04-02 18:07:40 +0000
@@ -1,14 +1,20 @@
-/*
- * To change this license header, choose License Headers in Project Properties.
- * To change this template file, choose Tools | Templates
- * and open the template in the editor.
- */
-
-/* 
- * File:   Colors.h
- * Author: andreas
- *
- * Created on February 19, 2018, 8:22 PM
+/* Copyright (C) 2020  Alexander Bilgram <[e-mail]>,
+ *                     Peter Haar Taankvist <[e-mail]>,
+ *                     Thomas Pedersen <[e-mail]>
+ *                     Andreas H. Klostergaard
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
  */
 
 #ifndef COLORS_H
@@ -21,6 +27,10 @@
 #include <utility>
 #include <vector>
 #include <unordered_map>
+#include <iostream>
+#include <cassert>
+
+#include "Intervals.h"
 
 namespace PetriEngine {
     namespace Colored {
@@ -44,7 +54,15 @@
             bool isTuple() const {
                 return _tuple.size() > 1;
             }
+
+            void getColorConstraints(Colored::interval_t *constraintsVector, uint32_t *index) const;
             
+            std::vector<const Color*> getTupleColors() const {
+                return _tuple;
+            }
+
+            void getTupleId(std::vector<uint32_t> *idVector) const;
+
             const std::string& getColorName() const {
                 if (this->isTuple()) {
                     throw "Cannot get color from a tuple color.";
@@ -90,9 +108,11 @@
             DotConstant();
             
         public:
-            static const Color* dotConstant() {
+            static const Color* dotConstant(ColorType *ct) {
                 static DotConstant _instance;
-                
+                if(ct != nullptr){
+                    _instance._colorType = ct;
+                }
                 return &_instance;
             }
             
@@ -160,12 +180,33 @@
             virtual void addColor(const char* colorName);
             virtual void addColor(std::vector<const Color*>& colors);
             virtual void addDot() {
-                _colors.push_back(*DotConstant::dotConstant());
+                _colors.push_back(*DotConstant::dotConstant(this));
             }
             
             virtual size_t size() const {
                 return _colors.size();
             }
+
+            virtual size_t productSize() {
+                return 1;
+            }
+
+            virtual std::vector<size_t> getConstituentsSizes(){
+                std::vector<size_t> result;                
+                result.push_back(_colors.size());
+                
+                return result;
+            }
+
+            virtual Colored::interval_t getFullInterval(){
+                Colored::interval_t interval;
+                interval.addRange(Reachability::range_t(0, size()-1));
+                return interval;
+            }
+
+            virtual void getColortypes(std::vector<ColorType *> &colorTypes){
+                colorTypes.push_back(this);
+            }
             
             virtual const Color& operator[] (size_t index) {
                 return _colors[index];
@@ -176,6 +217,7 @@
             }
             
             virtual const Color& operator[] (uint32_t index) {
+                assert(index < _colors.size());
                 return _colors[index];
             }
             
@@ -184,6 +226,11 @@
             virtual const Color* operator[] (const std::string& index) {
                 return (*this)[index.c_str()];
             }
+
+            virtual const Color* getColor(std::vector<uint32_t> ids){
+                assert(ids.size() == 1);
+                return &_colors[ids[0]];
+            }
             
             bool operator== (const ColorType& other) const {
                 return _id == other._id;
@@ -233,6 +280,36 @@
                 return product;
             }
 
+            virtual size_t productSize() {
+                size_t size = 0;
+                for (auto ct : constituents){
+                    size += ct->productSize();
+                }
+                return size;
+            }
+
+            std::vector<size_t> getConstituentsSizes() override{
+                std::vector<size_t> result;
+                for (auto ct : constituents) {
+                    result.push_back(ct->size());
+                }
+                return result;
+            }
+
+            Colored::interval_t getFullInterval() override{
+                Colored::interval_t interval;
+                for(auto ct : constituents) {
+                    interval.addRange(Reachability::range_t(0, ct->size()-1));
+                }                
+                return interval;
+            }
+
+            void getColortypes(std::vector<ColorType *> &colorTypes) override{
+                for(auto ct : constituents){
+                    ct->getColortypes(colorTypes);
+                }
+            }
+
             bool containsTypes(const std::vector<const ColorType*>& types) const {
                 if (constituents.size() != types.size()) return false;
 
@@ -245,6 +322,19 @@
                 return true;
             }
 
+            const ColorType* getNestedColorType(size_t index) {
+                return constituents[index];
+            }
+
+            const Color* getColor(std::vector<uint32_t> ids){
+                assert(ids.size() == constituents.size());
+                std::vector<const Color *> colors;
+                for(uint32_t i = 0; i < ids.size(); i++){
+                    colors.push_back(&constituents[i]->operator[](i));
+                }
+                return getColor(colors);
+            }
+
             const Color* getColor(const std::vector<const Color*>& colors);
 
             const Color& operator[](size_t index) override;
@@ -263,13 +353,29 @@
             std::string name;
             ColorType* colorType;
         };
-        
-        struct Binding {
-            Variable* var;
-            const Color* color;
-            
-            bool operator==(Binding& other) {
-                return var->name.compare(other.var->name);
+
+        struct ColorFixpoint {
+            Colored::intervalTuple_t constraints;
+            bool inQueue;
+            uint32_t productSize;
+
+            bool constainsColor(std::pair<const PetriEngine::Colored::Color *const, std::vector<uint32_t>> constPair) {
+                std::unordered_map<uint32_t, bool> contained;
+                for(auto interval : constraints._intervals) {
+                    for(uint32_t id : constPair.second){
+                        
+                        if(contained[id] != true){
+                            contained[id] = interval[id].contains(constPair.first->getId());
+                        }                        
+                    }
+                }
+
+                for(auto pair : contained){
+                    if (!pair.second){
+                        return false;
+                    }
+                }
+                return true;
             }
         };
     }
 
=== modified file 'include/PetriEngine/Colored/Expressions.h'
--- include/PetriEngine/Colored/Expressions.h	2020-03-02 21:03:24 +0000
+++ include/PetriEngine/Colored/Expressions.h	2021-04-02 18:07:40 +0000
@@ -1,14 +1,20 @@
-/*
- * To change this license header, choose License Headers in Project Properties.
- * To change this template file, choose Tools | Templates
- * and open the template in the editor.
- */
-
-/* 
- * File:   Expressions.h
- * Author: andreas
- *
- * Created on February 19, 2018, 7:00 PM
+/* Copyright (C) 2020  Alexander Bilgram <[e-mail]>,
+ *                     Peter Haar Taankvist <[e-mail]>,
+ *                     Thomas Pedersen <[e-mail]>
+ *                     Andreas H. Klostergaard
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
  */
 
 #ifndef COLORED_EXPRESSIONS_H
@@ -25,6 +31,8 @@
 
 #include "Colors.h"
 #include "Multiset.h"
+#include "ArcIntervals.h"
+#include "GuardRestrictor.h"
 #include "../errorcodes.h"
 
 namespace PetriEngine {
@@ -32,14 +40,14 @@
     
     namespace Colored {
         struct ExpressionContext {
-            typedef std::unordered_map<std::string, const Color*> BindingMap;
+            typedef std::unordered_map<const Colored::Variable *, const PetriEngine::Colored::Color *> BindingMap;
 
             BindingMap& binding;
             std::unordered_map<std::string, ColorType*>& colorTypes;
             
             const Color* findColor(const std::string& color) const {
                 if (color.compare("dot") == 0)
-                    return DotConstant::dotConstant();
+                    return DotConstant::dotConstant(nullptr);
                 for (auto& elem : colorTypes) {
                     auto col = (*elem.second)[color];
                     if (col)
@@ -74,8 +82,29 @@
         class Expression {
         public:
             Expression() {}
-            
-            virtual void getVariables(std::set<Variable*>& variables) const {
+        
+            virtual void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const {}
+
+            virtual void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap) const {
+                uint32_t index = 0;
+                getVariables(variables, varPositions, varModifierMap, &index);
+            }
+
+            virtual void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions) const {
+                std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMap;
+                uint32_t index = 0;
+                getVariables(variables, varPositions, varModifierMap, &index);
+            }
+
+            virtual bool isTuple() const {
+                return false;
+            }
+
+            virtual void getVariables(std::set<const Colored::Variable*>& variables) const {
+                std::unordered_map<uint32_t, const Colored::Variable *> varPositions;
+                std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMap;
+
+                getVariables(variables, varPositions, varModifierMap);
             }
             
             virtual void expressionType() {
@@ -93,12 +122,55 @@
             virtual ~ColorExpression() {}
             
             virtual const Color* eval(ExpressionContext& context) const = 0;
+
+            virtual void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const = 0;
+
+            virtual bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const = 0;
+
+            virtual ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const = 0;
+
+            virtual Colored::intervalTuple_t getOutputIntervals(std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>& varMap, std::vector<const Colored::ColorType *> *colortypes) const {
+                return Colored::intervalTuple_t();
+            }
+
         };
         
         class DotConstantExpression : public ColorExpression {
         public:
             const Color* eval(ExpressionContext& context) const override {
-                return DotConstant::dotConstant();
+                return DotConstant::dotConstant(nullptr);
+            }
+
+            bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override {
+                if (arcIntervals._intervalTupleVec.empty()) {
+                    //We can add all place tokens when considering the dot constant as, that must be present
+                    arcIntervals._intervalTupleVec.push_back(cfp.constraints);
+                }
+                return !cfp.constraints._intervals.empty();
+            }
+
+            Colored::intervalTuple_t getOutputIntervals(std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>& varMap, std::vector<const Colored::ColorType *> *colortypes) const override {
+                Colored::interval_t interval;
+                Colored::intervalTuple_t tupleInterval;
+                const Color *dotColor = DotConstant::dotConstant(nullptr);
+                 
+                colortypes->push_back(dotColor->getColorType());
+                
+                interval.addRange(dotColor->getId(), dotColor->getId());
+                tupleInterval.addInterval(interval);
+                return tupleInterval;
+            }
+
+            void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const override {
+                const Color *dotColor = DotConstant::dotConstant(nullptr);
+                constantMap[index] = dotColor;
+            }
+            ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{
+                return DotConstant::dotConstant(nullptr)->getColorType();
+            }
+
+            std::string toString() const override {
+                return "dot";
             }
         };
 
@@ -110,17 +182,74 @@
             
         public:
             const Color* eval(ExpressionContext& context) const override {
-                return context.binding[_variable->name];
+                return context.binding[_variable];
             }
             
-            void getVariables(std::set<Variable*>& variables) const override {
+            void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
                 variables.insert(_variable);
+                varPositions[*index] = _variable;
+                if(varModifierMap.count(_variable) == 0){
+                    std::vector<std::unordered_map<uint32_t, int32_t>> newVec;
+                    
+                    for(auto pair : varModifierMap){
+                        for(uint32_t i = 0; i < pair.second.size()-1; i++){
+                            std::unordered_map<uint32_t, int32_t> emptyMap;
+                            newVec.push_back(emptyMap);
+                        }
+                        break;
+                    }
+                    std::unordered_map<uint32_t, int32_t> newMap;
+                    newMap[*index] = 0;
+                    newVec.push_back(newMap);
+                    varModifierMap[_variable] = newVec;
+                } else {
+                    varModifierMap[_variable].back()[*index] = 0;
+                }                
+            }
+
+            Colored::intervalTuple_t getOutputIntervals(std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>& varMap, std::vector<const Colored::ColorType *> *colortypes) const override {
+                Colored::intervalTuple_t varInterval;
+                
+                // If we see a new variable on an out arc, it gets its full interval
+                if (varMap.count(_variable) == 0){
+                    Colored::intervalTuple_t intervalTuple;
+                    intervalTuple.addInterval(_variable->colorType->getFullInterval());
+                    varMap[_variable] = intervalTuple;
+                }
+
+                for(auto interval : varMap[_variable]._intervals){
+                    varInterval.addInterval(interval);
+                }
+                                           
+                std::vector<ColorType*> varColorTypes;
+                _variable->colorType->getColortypes(varColorTypes);
+
+                for(auto ct : varColorTypes){
+                    colortypes->push_back(ct);
+                }
+
+                return varInterval;
+            }
+
+            bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override {
+                if (arcIntervals._intervalTupleVec.empty()){
+                    //As variables does not restrict the values before the guard we include all tokens
+                    arcIntervals._intervalTupleVec.push_back(cfp.constraints);
+                }
+                return !cfp.constraints._intervals.empty();
+            }
+
+            void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const override {
             }
 
             std::string toString() const override {
                 return _variable->name;
             }
 
+            ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{
+                return _variable->colorType;
+            }
+
             VariableExpression(Variable* variable)
                     : _variable(variable) {}
         };
@@ -134,10 +263,63 @@
                 return _userOperator;
             }
 
+            bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override {
+                uint32_t colorId = _userOperator->getId() + modifier;
+                while(colorId < 0){
+                    colorId += _userOperator->getColorType()->size();
+                }
+                colorId = colorId % _userOperator->getColorType()->size();
+                
+                if(arcIntervals._intervalTupleVec.empty()){
+                    Colored::intervalTuple_t newIntervalTuple;
+                    bool colorInFixpoint = false;
+                    for (auto interval : cfp.constraints._intervals){
+                        if(interval[*index].contains(colorId)){
+                            newIntervalTuple.addInterval(interval);
+                            colorInFixpoint = true;
+                        }
+                    }
+                    arcIntervals._intervalTupleVec.push_back(newIntervalTuple);
+                    return colorInFixpoint;
+                } else {
+                    std::vector<uint32_t> intervalsToRemove;
+                    for(auto& intervalTuple : arcIntervals._intervalTupleVec){
+                        for (uint32_t i = 0; i < intervalTuple._intervals.size(); i++){
+                            if(!intervalTuple[i][*index].contains(colorId)){
+                                intervalsToRemove.push_back(i);
+                            }
+                        }
+
+                        for (auto i = intervalsToRemove.rbegin(); i != intervalsToRemove.rend(); ++i) {
+                            intervalTuple.removeInterval(*i);
+                        }
+                    }              
+                    return !arcIntervals._intervalTupleVec[0]._intervals.empty();
+                }
+            }
+
             std::string toString() const override {
                 return _userOperator->toString();
             }
 
+            void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const override {
+                constantMap[index] = _userOperator;
+            }
+            ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{
+                return _userOperator->getColorType();
+            }
+
+            Colored::intervalTuple_t getOutputIntervals(std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>& varMap, std::vector<const Colored::ColorType *> *colortypes) const override {
+                Colored::interval_t interval;
+                Colored::intervalTuple_t tupleInterval;
+                 
+                colortypes->push_back(_userOperator->getColorType());
+                
+                interval.addRange(_userOperator->getId(), _userOperator->getId());
+                tupleInterval.addInterval(interval);
+                return tupleInterval;
+            }
+
             UserOperatorExpression(const Color* userOperator)
                     : _userOperator(userOperator) {}
         };
@@ -185,14 +367,47 @@
                 return &++(*_color->eval(context));
             }
             
-            void getVariables(std::set<Variable*>& variables) const override {
-                _color->getVariables(variables);
+            void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
+                //save index before evaluating nested expression to decrease all the correct modifiers
+                uint32_t indexBefore = *index;
+                _color->getVariables(variables, varPositions, varModifierMap, index);
+                for(auto& varModifierPair : varModifierMap){
+                    for(auto& idModPair : varModifierPair.second.back()){
+                        if(idModPair.first <= *index && idModPair.first >= indexBefore){
+                            idModPair.second--;
+                        } 
+                    }                   
+                }                
+            }
+
+            bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override {
+               return _color->getArcIntervals(arcIntervals, cfp, index, modifier+1);
+            }
+
+            Colored::intervalTuple_t getOutputIntervals(std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>& varMap, std::vector<const Colored::ColorType *> *colortypes) const override {
+                //store the number of colortyps already in colortypes vector and use that as offset when indexing it
+                auto colortypesBefore = colortypes->size();
+
+                auto nestedInterval = _color->getOutputIntervals(varMap, colortypes);
+                Colored::GuardRestrictor guardRestrictor = Colored::GuardRestrictor();
+                return guardRestrictor.shiftIntervals(colortypes, &nestedInterval, 1, colortypesBefore);
+            }
+
+            void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const override {
+                _color->getConstants(constantMap, index);
+                for(auto& constIndexPair : constantMap){
+                    constIndexPair.second = &constIndexPair.second->operator++();
+                }
             }
 
             std::string toString() const override {
                 return _color->toString() + "++";
             }
 
+            ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{
+                return _color->getColorType(colorTypes);
+            }
+
             SuccessorExpression(ColorExpression_ptr&& color)
                     : _color(std::move(color)) {}
         };
@@ -206,14 +421,47 @@
                 return &--(*_color->eval(context));
             }
             
-            void getVariables(std::set<Variable*>& variables) const override {
-                _color->getVariables(variables);
+            void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
+                //save index before evaluating nested expression to decrease all the correct modifiers
+                uint32_t indexBefore = *index;
+                _color->getVariables(variables, varPositions, varModifierMap, index);
+                for(auto& varModifierPair : varModifierMap){
+                    for(auto& idModPair : varModifierPair.second.back()){
+                        if(idModPair.first <= *index && idModPair.first >= indexBefore){
+                            idModPair.second++;
+                        } 
+                    }                   
+                } 
+            }
+
+            bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override {
+                return _color->getArcIntervals(arcIntervals, cfp, index, modifier-1);
+            }
+            
+            Colored::intervalTuple_t getOutputIntervals(std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>& varMap, std::vector<const Colored::ColorType *> *colortypes) const override {
+                //store the number of colortyps already in colortypes vector and use that as offset when indexing it
+                auto colortypesBefore = colortypes->size();
+
+                auto nestedInterval = _color->getOutputIntervals(varMap, colortypes);
+                Colored::GuardRestrictor guardRestrictor;
+                return guardRestrictor.shiftIntervals(colortypes, &nestedInterval, -1, colortypesBefore);
+            }
+
+            void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const override {
+                _color->getConstants(constantMap, index);
+                for(auto& constIndexPair : constantMap){
+                    constIndexPair.second = &constIndexPair.second->operator--();
+                }
             }
 
             std::string toString() const override {
                 return _color->toString() + "--";
             }
 
+            ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{
+                return _color->getColorType(colorTypes);
+            }
+
             PredecessorExpression(ColorExpression_ptr&& color)
                     : _color(std::move(color)) {}
         };
@@ -221,6 +469,7 @@
         class TupleExpression : public ColorExpression {
         private:
             std::vector<ColorExpression_ptr> _colors;
+            ColorType* _colorType;
             
         public:
             const Color* eval(ExpressionContext& context) const override {
@@ -236,10 +485,77 @@
                 assert(col != nullptr);
                 return col;
             }
+
+            bool isTuple() const override {
+                return true;
+            }
+
+            Colored::intervalTuple_t getOutputIntervals(std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>& varMap, std::vector<const Colored::ColorType *> *colortypes) const override {
+                Colored::intervalTuple_t intervals;
+                Colored::intervalTuple_t intervalHolder;                
+
+                for(auto colorExp : _colors) {
+                    Colored::intervalTuple_t intervalHolder;
+                    auto nested_intervals = colorExp->getOutputIntervals(varMap, colortypes);
+
+                    if(intervals._intervals.empty()){
+                        intervals = nested_intervals;
+                    } else {                        
+                        for(auto nested_interval : nested_intervals._intervals){
+                            Colored::intervalTuple_t newIntervals;
+                            for(auto interval : intervals._intervals){
+                                for(auto nestedRange : nested_interval._ranges) {
+                                    interval.addRange(nestedRange);    
+                                }
+                                newIntervals.addInterval(interval);
+                            }
+                            for(auto newInterval : newIntervals._intervals){
+                                intervalHolder.addInterval(newInterval);
+                            }
+                        }
+                        intervals = intervalHolder;
+                    }                  
+                }
+                return intervals;
+            }
+
+            bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override {
+                for (auto expr : _colors) {
+                    bool res = expr->getArcIntervals(arcIntervals, cfp, index, modifier);
+                    if(!res){
+                        return false;
+                    }
+                    (*index)++;
+                }
+                return true;
+            }
             
-            void getVariables(std::set<Variable*>& variables) const override {
-                for (auto elem : _colors) {
-                    elem->getVariables(variables);
+            void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
+                for (auto elem : _colors) {
+                    elem->getVariables(variables, varPositions, varModifierMap, index);
+                    (*index)++;
+                }
+            }
+
+            ColorType* getColorType(std::unordered_map<std::string, Colored::ColorType*>& colorTypes) const override{
+                std::vector<const ColorType*> types;
+                for (auto color : _colors) {
+                    types.push_back(color->getColorType(colorTypes));
+                }
+                for (auto& elem : colorTypes) {
+                    auto* pt = dynamic_cast<ProductType*>(elem.second);
+                    if (pt && pt->containsTypes(types)) {
+                        return pt;
+                    }
+                }
+                std::cout << "COULD NOT FIND PRODUCT TYPE" << std::endl;
+                return nullptr;
+            }
+
+            void getConstants(std::unordered_map<uint32_t, const Color*> &constantMap, uint32_t &index) const override {
+                for (auto elem : _colors) {
+                    elem->getConstants(constantMap, index);
+                    index++;
                 }
             }
 
@@ -252,6 +568,10 @@
                 return res;
             }
 
+            void setColorType(ColorType* ct){
+                _colorType = ct;
+            }
+
             TupleExpression(std::vector<ColorExpression_ptr>&& colors)
                     : _colors(std::move(colors)) {}
         };
@@ -262,6 +582,8 @@
             virtual ~GuardExpression() {}
             
             virtual bool eval(ExpressionContext& context) const = 0;
+
+            virtual void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const = 0;
         };
 
         typedef std::shared_ptr<GuardExpression> GuardExpression_ptr;
@@ -275,11 +597,40 @@
             bool eval(ExpressionContext& context) const override {
                 return _left->eval(context) < _right->eval(context);
             }
+
+            void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
+                _left->getVariables(variables, varPositions, varModifierMap);
+                _right->getVariables(variables, varPositions, varModifierMap);
+            }
+
+            void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const override {
+                std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapL;
+                std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapR;
+                std::unordered_map<uint32_t, const Colored::Variable *> varPositionsL;
+                std::unordered_map<uint32_t, const Colored::Variable *> varPositionsR;
+                std::unordered_map<uint32_t, const Color*> constantMapL;
+                std::unordered_map<uint32_t, const Color*> constantMapR;
+                std::set<const Variable *> leftVars;
+                std::set<const Variable *> rightVars;
+                uint32_t index = 0;
+                _left->getVariables(leftVars, varPositionsL, varModifierMapL);
+                _right->getVariables(rightVars, varPositionsR, varModifierMapR);
+                _left->getConstants(constantMapL, index);
+                index = 0;
+                _right->getConstants(constantMapR, index);
+
+                if(leftVars.empty() && rightVars.empty()){
+                    return;
+                }
+                Colored::GuardRestrictor guardRestrictor;
+                guardRestrictor.restrictDiagonal(&variableMap, &varModifierMapL, &varModifierMapR, &varPositionsL, &varPositionsR, &constantMapL, &constantMapR, true, true);
+            }
             
-            void getVariables(std::set<Variable*>& variables) const override {
-                _left->getVariables(variables);
-                _right->getVariables(variables);
+            std::string toString() const override {
+                std::string res = _left->toString() + " < " + _right->toString();
+                return res;
             }
+
             
             LessThanExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right)
                     : _left(std::move(left)), _right(std::move(right)) {}
@@ -295,9 +646,38 @@
                 return _left->eval(context) > _right->eval(context);
             }
             
-            void getVariables(std::set<Variable*>& variables) const override {
-                _left->getVariables(variables);
-                _right->getVariables(variables);
+            void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
+                _left->getVariables(variables, varPositions, varModifierMap);
+                _right->getVariables(variables, varPositions, varModifierMap);
+            }
+
+            void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const override {
+                std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapL;
+                std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapR;
+                std::unordered_map<uint32_t, const Colored::Variable *> varPositionsL;
+                std::unordered_map<uint32_t, const Colored::Variable *> varPositionsR;
+                std::unordered_map<uint32_t, const Color*> constantMapL;
+                std::unordered_map<uint32_t, const Color*> constantMapR;
+                std::set<const Colored::Variable *> leftVars;
+                std::set<const Colored::Variable *> rightVars;
+                uint32_t index = 0;
+                _left->getVariables(leftVars, varPositionsL, varModifierMapL);
+                _right->getVariables(rightVars, varPositionsR, varModifierMapR);
+                _left->getConstants(constantMapL, index);
+                index = 0;
+                _right->getConstants(constantMapR, index);
+
+                if(leftVars.empty() && rightVars.empty()){
+                    return;
+                }
+
+                Colored::GuardRestrictor guardRestrictor;
+                guardRestrictor.restrictDiagonal(&variableMap, &varModifierMapL, &varModifierMapR, &varPositionsL, &varPositionsR, &constantMapL, &constantMapR, false, true);
+            }
+
+            std::string toString() const override {
+                std::string res = _left->toString() + " > " + _right->toString();
+                return res;
             }
             
             GreaterThanExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right)
@@ -314,10 +694,40 @@
                 return _left->eval(context) <= _right->eval(context);
             }
             
-            void getVariables(std::set<Variable*>& variables) const override {
-                _left->getVariables(variables);
-                _right->getVariables(variables);
-            }
+            void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
+                _left->getVariables(variables, varPositions, varModifierMap);
+                _right->getVariables(variables, varPositions, varModifierMap);
+            }
+
+            void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const override {
+                std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapL;
+                std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapR;
+                std::unordered_map<uint32_t, const Colored::Variable *> varPositionsL;
+                std::unordered_map<uint32_t, const Colored::Variable *> varPositionsR;
+                std::unordered_map<uint32_t, const Color*> constantMapL;
+                std::unordered_map<uint32_t, const Color*> constantMapR;
+                std::set<const Colored::Variable *> leftVars;
+                std::set<const Colored::Variable *> rightVars;
+                uint32_t index = 0;
+                _left->getVariables(leftVars, varPositionsL, varModifierMapL);
+                _right->getVariables(rightVars, varPositionsR, varModifierMapR);
+                _left->getConstants(constantMapL, index);
+                index = 0;
+                _right->getConstants(constantMapR, index);
+
+                if(leftVars.empty() && rightVars.empty()){
+                    return;
+                }
+
+                Colored::GuardRestrictor guardRestrictor;
+                guardRestrictor.restrictDiagonal(&variableMap, &varModifierMapL, &varModifierMapR, &varPositionsL, &varPositionsR, &constantMapL, &constantMapR, true, false); 
+            }
+
+            std::string toString() const override {
+                std::string res = _left->toString() + " <= " + _right->toString();
+                return res;
+            }
+
             
             LessThanEqExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right)
                     : _left(std::move(left)), _right(std::move(right)) {}
@@ -333,11 +743,40 @@
                 return _left->eval(context) >= _right->eval(context);
             }
             
-            void getVariables(std::set<Variable*>& variables) const override {
-                _left->getVariables(variables);
-                _right->getVariables(variables);
+            void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
+                _left->getVariables(variables, varPositions, varModifierMap);
+                _right->getVariables(variables, varPositions, varModifierMap);
+            }
+
+            void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const override {
+                std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapL;
+                std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapR;
+                std::unordered_map<uint32_t, const Colored::Variable *> varPositionsL;
+                std::unordered_map<uint32_t, const Colored::Variable *> varPositionsR;
+                std::unordered_map<uint32_t, const Color*> constantMapL;
+                std::unordered_map<uint32_t, const Color*> constantMapR;
+                std::set<const Colored::Variable *> leftVars;
+                std::set<const Colored::Variable *> rightVars;
+                uint32_t index = 0;
+                _left->getVariables(leftVars, varPositionsL, varModifierMapL);
+                _right->getVariables(rightVars, varPositionsR, varModifierMapR);
+                _left->getConstants(constantMapL, index);
+                index = 0;
+                _right->getConstants(constantMapR, index);
+
+                if(leftVars.empty() && rightVars.empty()){
+                    return;
+                }
+
+                Colored::GuardRestrictor guardRestrictor;
+                guardRestrictor.restrictDiagonal(&variableMap, &varModifierMapL, &varModifierMapR, &varPositionsL, &varPositionsR, &constantMapL, &constantMapR, false, false);                
             }
             
+            std::string toString() const override {
+                std::string res = _left->toString() + " >= " + _right->toString();
+                return res;
+            }
+
             GreaterThanEqExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right)
                     : _left(std::move(left)), _right(std::move(right)) {}
         };
@@ -352,11 +791,41 @@
                 return _left->eval(context) == _right->eval(context);
             }
             
-            void getVariables(std::set<Variable*>& variables) const override {
-                _left->getVariables(variables);
-                _right->getVariables(variables);
+            void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
+                _left->getVariables(variables, varPositions, varModifierMap);
+                _right->getVariables(variables, varPositions, varModifierMap);
             }
             
+
+            void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const override {
+                std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapL;
+                std::unordered_map<const Colored::Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> varModifierMapR;
+                std::unordered_map<uint32_t, const Colored::Variable *> varPositionsL;
+                std::unordered_map<uint32_t, const Colored::Variable *> varPositionsR;
+                std::unordered_map<uint32_t, const Color*> constantMapL;
+                std::unordered_map<uint32_t, const Color*> constantMapR;
+                std::set<const Colored::Variable *> leftVars;
+                std::set<const Colored::Variable *> rightVars;
+                uint32_t index = 0;
+                _left->getVariables(leftVars, varPositionsL, varModifierMapL);
+                _right->getVariables(rightVars, varPositionsR, varModifierMapR);
+                _left->getConstants(constantMapL, index);
+                index = 0;
+                _right->getConstants(constantMapR, index);
+
+                if(leftVars.empty() && rightVars.empty()){
+                    return;
+                }
+                
+                Colored::GuardRestrictor guardRestrictor;
+                guardRestrictor.restrictEquality(&variableMap, &varModifierMapL, &varModifierMapR, &varPositionsL, &varPositionsR, &constantMapL, &constantMapR);
+            }
+
+            std::string toString() const override {
+                std::string res = _left->toString() + " == " + _right->toString();
+                return res;
+            }
+
             EqualityExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right)
                     : _left(std::move(left)), _right(std::move(right)) {}
         };
@@ -371,9 +840,18 @@
                 return _left->eval(context) != _right->eval(context);
             }
             
-            void getVariables(std::set<Variable*>& variables) const override {
-                _left->getVariables(variables);
-                _right->getVariables(variables);
+            void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
+                _left->getVariables(variables, varPositions, varModifierMap);
+                _right->getVariables(variables, varPositions, varModifierMap);
+            }
+
+            void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const override {
+                
+            }
+
+            std::string toString() const override {
+                std::string res = _left->toString() + " != " + _right->toString();
+                return res;
             }
             
             InequalityExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right)
@@ -389,8 +867,28 @@
                 return !_expr->eval(context);
             }
             
-            void getVariables(std::set<Variable*>& variables) const override {
+            void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
+                _expr->getVariables(variables, varPositions, varModifierMap, index);
+            }
+
+            std::string toString() const override {
+                std::string res = "!" + _expr->toString();
+                return res;
+            }
+
+            void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const override {
+                std::set<const Colored::Variable *> variables;
                 _expr->getVariables(variables);
+                //TODO: invert the var intervals here instead of using the full intervals
+
+                for(auto var : variables){
+                    auto fullInterval = var->colorType->getFullInterval();
+                    Colored::intervalTuple_t fullTuple;
+                    fullTuple.addInterval(fullInterval);
+                    for(auto& varMap : variableMap){
+                        varMap[var] = fullTuple;
+                    }                    
+                }
             }
             
             NotExpression(GuardExpression_ptr&& expr) : _expr(std::move(expr)) {}
@@ -406,11 +904,21 @@
                 return _left->eval(context) && _right->eval(context);
             }
             
-            void getVariables(std::set<Variable*>& variables) const override {
-                _left->getVariables(variables);
-                _right->getVariables(variables);
-            }
-            
+            void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
+                _left->getVariables(variables, varPositions, varModifierMap);
+                _right->getVariables(variables, varPositions, varModifierMap);
+            }
+
+            void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const override {
+                _left->restrictVars(variableMap);
+                _right->restrictVars(variableMap);
+            }
+
+            std::string toString() const override {
+                std::string res = _left->toString() + " && " + _right->toString();
+                return res;
+            }
+
             AndExpression(GuardExpression_ptr&& left, GuardExpression_ptr&& right)
                     : _left(left), _right(right) {}
         };
@@ -425,11 +933,30 @@
                 return _left->eval(context) || _right->eval(context);
             }
             
-            void getVariables(std::set<Variable*>& variables) const override {
-                _left->getVariables(variables);
-                _right->getVariables(variables);
-            }
-            
+            void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
+                _left->getVariables(variables, varPositions, varModifierMap);
+                _right->getVariables(variables, varPositions, varModifierMap);
+            }
+
+            void restrictVars(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMap) const override{
+                auto varMapCopy = variableMap;
+                _left->restrictVars(variableMap);
+                _right->restrictVars(varMapCopy);
+
+                for(size_t i = 0; i < variableMap.size(); i++){
+                    for(auto& varPair : varMapCopy[i]){
+                        for(auto& interval : varPair.second._intervals){
+                            variableMap[i][varPair.first].addInterval(std::move(interval));
+                        }
+                    }
+                }
+            }
+
+            std::string toString() const override {
+                std::string res = _left->toString() + " || " + _right->toString();
+                return res;
+            }
+
             OrExpression(GuardExpression_ptr&& left, GuardExpression_ptr&& right)
                     : _left(std::move(left)), _right(std::move(right)) {}
         };
@@ -444,8 +971,21 @@
             virtual void expressionType() override {
                 std::cout << "ArcExpression" << std::endl;
             }
+            virtual void getConstants(std::unordered_map<uint32_t, std::vector<const Color*>> &constantMap, uint32_t &index) const = 0;
+
+            virtual bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const = 0;
 
             virtual uint32_t weight() const = 0;
+
+            virtual Colored::intervalTuple_t getOutputIntervals(std::vector<std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>>& varMapVec) const {
+                std::vector<const Colored::ColorType *> colortypes;
+                
+                return getOutputIntervals(varMapVec, &colortypes);
+            }
+
+            virtual Colored::intervalTuple_t getOutputIntervals(std::vector<std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>>& varMapVec, std::vector<const Colored::ColorType *> *colortypes) const {
+                return Colored::intervalTuple_t();
+            }
         };
 
         typedef std::shared_ptr<ArcExpression> ArcExpression_ptr;
@@ -465,6 +1005,45 @@
                 return colors;
             }
 
+            void getConstants(std::unordered_map<uint32_t, std::vector<const Color*>> &constantMap, uint32_t &index) const {
+                for (size_t i = 0; i < _sort->size(); i++) {
+                    constantMap[index].push_back(&(*_sort)[i]);
+                }
+            }
+
+            Colored::intervalTuple_t getOutputIntervals(std::vector<std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>>& varMapVec, std::vector<const Colored::ColorType *> *colortypes) const {
+                Colored::intervalTuple_t newIntervalTuple;
+                newIntervalTuple.addInterval(_sort->getFullInterval());
+                return newIntervalTuple;
+            }
+
+            bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const {
+                
+                if(arcIntervals._intervalTupleVec.empty()){
+                    bool colorsInFixpoint = false;
+                    Colored::intervalTuple_t newIntervalTuple;
+                    cfp.constraints.simplify();
+                    if(cfp.constraints.getContainedColors() == _sort->size()){
+                        colorsInFixpoint = true;
+                        for(auto interval : cfp.constraints._intervals){                            
+                            newIntervalTuple.addInterval(interval);
+                        }
+                    }                    
+                    arcIntervals._intervalTupleVec.push_back(newIntervalTuple);
+                    return colorsInFixpoint;
+                } else {
+                    std::vector<Colored::intervalTuple_t> newIntervalTupleVec;
+                    for(uint32_t i = 0; i < arcIntervals._intervalTupleVec.size(); i++){
+                        auto& intervalTuple = arcIntervals._intervalTupleVec[i];
+                        if(intervalTuple.getContainedColors() == _sort->size()){
+                            newIntervalTupleVec.push_back(intervalTuple);
+                        }
+                    }
+                    arcIntervals._intervalTupleVec = std::move(newIntervalTupleVec);
+                    return !arcIntervals._intervalTupleVec.empty();
+                }
+            }
+
             size_t size() const {
                 return  _sort->size();
             }
@@ -503,12 +1082,64 @@
                 }
                 return Multiset(col);
             }
-            
-            void getVariables(std::set<Variable*>& variables) const override {
+
+            void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
                 if (_all != nullptr)
                     return;
                 for (auto elem : _color) {
-                    elem->getVariables(variables);
+                    //TODO: can there be more than one element in a number of expression?
+                    elem->getVariables(variables, varPositions, varModifierMap, index);
+                    //(*index)++;
+                }
+            }
+
+            bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override {
+                if (_all != nullptr) {
+                    return _all->getArcIntervals(arcIntervals, cfp, index, modifier);
+                }
+                uint32_t i = 0;
+                for (auto elem : _color) {
+                    (*index) += i;
+                    if(!elem->getArcIntervals(arcIntervals, cfp, index, modifier)){
+                        return false;
+                    }
+                    i++;
+                }
+                return true;
+            }
+
+            Colored::intervalTuple_t getOutputIntervals(std::vector<std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>>& varMapVec, std::vector<const Colored::ColorType *> *colortypes) const override {
+                Colored::intervalTuple_t intervals;
+                if (_all == nullptr) {
+                    for (auto elem : _color) {
+                        for(auto& varMap : varMapVec){
+                            auto nestedIntervals = elem->getOutputIntervals(varMap, colortypes);
+
+                            if (intervals._intervals.empty()) {
+                                intervals = nestedIntervals;
+                            } else {
+                                for(auto interval : nestedIntervals._intervals) {
+                                    intervals.addInterval(interval);
+                                }
+                            }
+                        }                        
+                    }
+                } else {
+                    return _all->getOutputIntervals(varMapVec, colortypes);
+                }
+                return intervals;
+            }
+
+            void getConstants(std::unordered_map<uint32_t, std::vector<const Color*>> &constantMap, uint32_t &index) const override {
+                if (_all != nullptr)
+                    _all->getConstants(constantMap, index);
+                else for (auto elem : _color) {
+                    std::unordered_map<uint32_t, const Color*> elemMap;
+                    elem->getConstants(elemMap, index);
+                    for(auto pair : elemMap){
+                        constantMap[pair.first].push_back(pair.second);
+                    }
+                    index++;//not sure if index should be increased here, but no number expression have multiple elements
                 }
             }
 
@@ -563,9 +1194,57 @@
                 return ms;
             }
             
-            void getVariables(std::set<Variable*>& variables) const override {
-                for (auto elem : _constituents) {
-                    elem->getVariables(variables);
+            void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
+                for (auto elem : _constituents) {
+                    for(auto& pair : varModifierMap){
+                        std::unordered_map<uint32_t, int32_t> newMap;
+                        pair.second.push_back(newMap);
+                    }
+                    elem->getVariables(variables, varPositions, varModifierMap);
+                }
+            }
+
+            bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override {
+                for (auto elem : _constituents) {
+                    uint32_t newIndex = 0;
+                    Colored::ArcIntervals newArcIntervals;
+                    std::vector<uint32_t> intervalsForRemoval;
+                    std::vector<Colored::interval_t> newIntervals;
+                    if(!elem->getArcIntervals(newArcIntervals, cfp, &newIndex, modifier)){
+                        return false;
+                    }
+
+                    if(newArcIntervals._intervalTupleVec.empty()){
+                        return false;
+                    }
+
+                    arcIntervals._intervalTupleVec.insert(arcIntervals._intervalTupleVec.end(), newArcIntervals._intervalTupleVec.begin(), newArcIntervals._intervalTupleVec.end());
+                }
+                return true;
+            }            
+
+            Colored::intervalTuple_t getOutputIntervals(std::vector<std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>>& varMapVec, std::vector<const Colored::ColorType *> *colortypes) const override {
+                Colored::intervalTuple_t intervals;
+                
+                for (auto elem : _constituents) {
+                    auto nestedIntervals = elem->getOutputIntervals(varMapVec, colortypes);
+
+                    if (intervals._intervals.empty()) {
+                        intervals = nestedIntervals;
+                    } else {
+                        for(auto interval : nestedIntervals._intervals) {
+                            intervals.addInterval(interval);
+                        }
+                    }
+                }
+                return intervals;
+            }
+
+            void getConstants(std::unordered_map<uint32_t, std::vector<const Color*>> &constantMap, uint32_t &index) const override {
+                uint32_t indexCopy = index;
+                for (auto elem : _constituents) {
+                    uint32_t localIndex = indexCopy;
+                    elem->getConstants(constantMap, localIndex);
                 }
             }
 
@@ -599,9 +1278,29 @@
                 return _left->eval(context) - _right->eval(context);
             }
             
-            void getVariables(std::set<Variable*>& variables) const override {
-                _left->getVariables(variables);
-                _right->getVariables(variables);
+            void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
+                _left->getVariables(variables, varPositions, varModifierMap);
+                //We ignore the restrictions imposed by the subtraction for now
+                //_right->getVariables(variables, varPositions, varModifierMap);
+            }
+
+            bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override {
+                return _left->getArcIntervals(arcIntervals, cfp, index, modifier);
+                //We ignore the restrictions imposed by the subtraction for now
+                //_right->getArcIntervals(arcIntervals, cfp, &rightIndex);
+            }
+
+            Colored::intervalTuple_t getOutputIntervals(std::vector<std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>>& varMapVec, std::vector<const Colored::ColorType *> *colortypes) const override {
+                //We could maybe reduce the intervals slightly by checking if the upper or lower bound is being subtracted
+                auto leftIntervals = _left->getOutputIntervals(varMapVec, colortypes);
+
+                return leftIntervals;
+            }   
+
+            void getConstants(std::unordered_map<uint32_t, std::vector<const Color*>> &constantMap, uint32_t &index) const override {
+                uint32_t rIndex = index;
+                _left->getConstants(constantMap, index);
+                _right->getConstants(constantMap, rIndex);
             }
 
             uint32_t weight() const override {
@@ -636,8 +1335,20 @@
                 return _expr->eval(context) * _scalar;
             }
             
-            void getVariables(std::set<Variable*>& variables) const override {
-                _expr->getVariables(variables);
+            void getVariables(std::set<const Colored::Variable*>& variables, std::unordered_map<uint32_t, const Colored::Variable *>& varPositions, std::unordered_map<const Colored::Variable *, std::vector<std::unordered_map<uint32_t, int32_t>>>& varModifierMap, uint32_t *index) const override {
+                _expr->getVariables(variables, varPositions,varModifierMap);
+            }
+
+            bool getArcIntervals(Colored::ArcIntervals& arcIntervals, PetriEngine::Colored::ColorFixpoint& cfp, uint32_t *index, int32_t modifier) const override {
+               return _expr ->getArcIntervals(arcIntervals, cfp, index, modifier);
+            }
+
+            Colored::intervalTuple_t getOutputIntervals(std::vector<std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>>& varMapVec, std::vector<const Colored::ColorType *> *colortypes) const override {
+                return _expr->getOutputIntervals(varMapVec, colortypes);
+            }
+
+            void getConstants(std::unordered_map<uint32_t, std::vector<const Color*>> &constantMap, uint32_t &index) const override {
+                _expr->getConstants(constantMap, index);
             }
 
             uint32_t weight() const override {
 
=== added file 'include/PetriEngine/Colored/GuardRestrictor.h'
--- include/PetriEngine/Colored/GuardRestrictor.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/Colored/GuardRestrictor.h	2021-04-02 18:07:40 +0000
@@ -0,0 +1,83 @@
+/* Copyright (C) 2020  Alexander Bilgram <[e-mail]>,
+ *                     Peter Haar Taankvist <[e-mail]>,
+ *                     Thomas Pedersen <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef GuardRestrictions_H
+#define GuardRestrictions_H
+
+#include "Colors.h"
+#include "Multiset.h"
+#include <unordered_map>
+#include <set>
+#include <stdlib.h>
+
+namespace PetriEngine {
+    namespace Colored {
+
+        class GuardRestrictor {
+            public:
+
+                GuardRestrictor();
+
+                void restrictDiagonal(std::vector<std::unordered_map<const Variable *, intervalTuple_t>> *variableMap,
+                            std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapL,
+                            std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapR,
+                            std::unordered_map<uint32_t, const Variable *> *varPositionsL,
+                            std::unordered_map<uint32_t, const Variable *> *varPositionsR,
+                            std::unordered_map<uint32_t, const Color*> *constantMapL,
+                            std::unordered_map<uint32_t, const Color*> *constantMapR, 
+                            bool lessthan, bool strict);
+
+                void restrictEquality(std::vector<std::unordered_map<const Variable *, intervalTuple_t>> *variableMap,
+                            std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapL,
+                            std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *varModifierMapR,
+                            std::unordered_map<uint32_t, const Variable *> *varPositionsL,
+                            std::unordered_map<uint32_t, const Variable *> *varPositionsR,
+                            std::unordered_map<uint32_t, const Color*> *constantMapL,
+                            std::unordered_map<uint32_t, const Color*> *constantMapR);
+
+                intervalTuple_t shiftIntervals(std::vector<const ColorType *> *colortypes,
+                            intervalTuple_t *intervals, 
+                            int32_t modifier, 
+                            uint32_t ctSizeBefore) const; 
+
+            private:
+                int32_t getVarModifier(std::unordered_map<uint32_t, int32_t> *modPairMap, uint32_t index);
+                interval_t getIntervalFromIds(std::vector<uint32_t> *idVec, uint32_t ctSize, int32_t modifier);
+                intervalTuple_t getIntervalOverlap(std::vector<interval_t> *intervals1, std::vector<interval_t> *intervals2);
+
+                void expandIdVec(std::unordered_map<const Variable *, intervalTuple_t> *varMap,
+                            std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *mainVarModifierMap,
+                            std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *otherVarModifierMap,
+                            std::unordered_map<uint32_t, const Variable *> *varPositions,
+                            std::unordered_map<uint32_t, const Color*> *constantMap,
+                            const Variable *otherVar, 
+                            std::vector<uint32_t> &idVec, size_t targetSize, uint32_t index);
+
+                void expandIntervalVec(std::unordered_map<const Variable *, intervalTuple_t> *varMap,
+                            std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *mainVarModifierMap,
+                            std::unordered_map<const Variable *,std::vector<std::unordered_map<uint32_t, int32_t>>> *otherVarModifierMap,
+                            std::unordered_map<uint32_t, const Variable *> *varPositions,
+                            std::unordered_map<uint32_t, const Color*> *constantMap,
+                            const Variable *otherVar, 
+                            std::vector<interval_t> &intervalVec, size_t targetSize, uint32_t index);                               
+        };
+    }
+}
+
+
+#endif /* GuardRestrictions_H */
 \ No newline at end of file
 
=== added file 'include/PetriEngine/Colored/IntervalGenerator.h'
--- include/PetriEngine/Colored/IntervalGenerator.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/Colored/IntervalGenerator.h	2021-04-02 18:07:40 +0000
@@ -0,0 +1,197 @@
+/* Copyright (C) 2020  Alexander Bilgram <[e-mail]>,
+ *                     Peter Haar Taankvist <[e-mail]>,
+ *                     Thomas Pedersen <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+#ifndef INTERVALGENERATOR_H
+#define INTERVALGENERATOR_H
+
+#include "ColoredNetStructures.h"
+
+namespace PetriEngine {
+    struct IntervalGenerator {
+        std::vector<Colored::interval_t> getIntervalsFromInterval(Colored::interval_t *interval, uint32_t varPosition, int32_t varModifier, std::vector<Colored::ColorType*> *varColorTypes){
+            std::vector<Colored::interval_t> varIntervals;
+            Colored::interval_t firstVarInterval;
+            varIntervals.push_back(firstVarInterval);
+            for(uint32_t i = varPosition; i < varPosition + varColorTypes->size(); i++){
+                auto ctSize = varColorTypes->operator[](i - varPosition)->size();
+                int32_t lower_val = ctSize + (interval->operator[](i)._lower + varModifier);
+                int32_t upper_val = ctSize + (interval->operator[](i)._upper + varModifier);
+                uint32_t lower = lower_val % ctSize;
+                uint32_t upper = upper_val % ctSize;
+
+                if(lower > upper ){
+                    if(lower == upper+1){
+                        for (auto& varInterval : varIntervals){
+                            varInterval.addRange(0, ctSize -1);
+                        }
+                    } else {
+                        std::vector<Colored::interval_t> newIntervals;
+                        for (auto& varInterval : varIntervals){
+                            Colored::interval_t newVarInterval = varInterval;                                  
+                            varInterval.addRange(0, upper);
+                            newVarInterval.addRange(lower, ctSize -1);
+                            newIntervals.push_back(newVarInterval);
+                        }
+                        varIntervals.insert(varIntervals.end(), newIntervals.begin(), newIntervals.end());
+                    }                
+                } else {
+                    for (auto& varInterval : varIntervals){
+                        varInterval.addRange(lower, upper);
+                    }
+                }            
+            }
+            return varIntervals;
+        }
+
+        void getArcVarIntervals(Colored::intervalTuple_t& varIntervals, std::unordered_map<uint32_t, int32_t> *modIndexMap, Colored::interval_t *interval, std::vector<Colored::ColorType*> *varColorTypes){
+            for(auto& posModPair : *modIndexMap){
+                auto intervals = getIntervalsFromInterval(interval, posModPair.first, posModPair.second, varColorTypes);
+
+                if(varIntervals._intervals.empty()){
+                    for(auto& interval : intervals){
+                        varIntervals.addInterval(std::move(interval));
+                    }
+                } else {
+                    Colored::intervalTuple_t newVarIntervals; 
+                    for(uint32_t i = 0; i < varIntervals.size(); i++){
+                        auto varInterval = &varIntervals[i];
+                        for(auto& interval : intervals){
+                            auto overlap = varInterval->getOverlap(std::move(interval));
+                            if(overlap.isSound()){ 
+                                newVarIntervals.addInterval(std::move(overlap));
+                                //break;
+                            }                                                
+                        }                                   
+                    }                                                                                       
+                    varIntervals = std::move(newVarIntervals);                                          
+                }     
+            } 
+        }
+
+        void populateLocalMap(Colored::ArcIntervals *arcIntervals, 
+                                                std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t> &varMap,
+                                                std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t> &localVarMap,
+                                                Colored::interval_t* interval, bool& allVarsAssigned,  uint32_t tuplePos){
+            for(auto& pair : arcIntervals->_varIndexModMap){                     
+                Colored::intervalTuple_t varIntervals; 
+                std::vector<Colored::ColorType*> varColorTypes;
+                pair.first->colorType->getColortypes(varColorTypes);
+                
+                getArcVarIntervals(varIntervals, &pair.second[tuplePos], interval, &varColorTypes);                          
+                
+                if (arcIntervals->_intervalTupleVec.size() > 1 && pair.second[tuplePos].empty()) {
+                    //The variable is not on this side of the add expression, so we add a full interval to compare against for the other side
+                    varIntervals.addInterval(pair.first->colorType->getFullInterval());
+                }
+
+                if(varMap.count(pair.first) == 0){
+                    localVarMap[pair.first] = std::move(varIntervals);                                  
+                } else {                                    
+                    for(auto& varInterval : varIntervals._intervals){
+                        for(auto& interval : varMap[pair.first]._intervals){
+                            auto overlapInterval = varInterval.getOverlap(interval);
+
+                            if(overlapInterval.isSound()){
+                                localVarMap[pair.first].addInterval(overlapInterval);
+                            }
+                        }
+                    }                                    
+                }
+
+                if(localVarMap[pair.first]._intervals.empty()){
+                    allVarsAssigned = false;
+                }                                
+            }         
+        }
+
+        void fillVarMaps(std::vector<std::unordered_map<const PetriEngine::Colored::Variable *, PetriEngine::Colored::intervalTuple_t>> &variableMaps,
+                                            Colored::ArcIntervals *arcIntervals,
+                                            uint32_t *intervalTupleSize,
+                                            uint32_t *tuplePos)
+        {
+            for(uint32_t i = 0; i < *intervalTupleSize; i++){
+                std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t> localVarMap;
+                bool validInterval = true;
+                auto interval = &arcIntervals->_intervalTupleVec[*tuplePos]._intervals[i];
+            
+                for(auto pair : arcIntervals->_varIndexModMap){
+                    Colored::intervalTuple_t varIntervals;
+                    std::vector<Colored::ColorType*> varColorTypes;
+                    pair.first->colorType->getColortypes(varColorTypes);
+                    getArcVarIntervals(varIntervals, &pair.second[*tuplePos], interval, &varColorTypes); 
+
+                    if(arcIntervals->_intervalTupleVec.size() > 1 && pair.second[*tuplePos].empty()){
+                        //The variable is not on this side of the add expression, so we add a full interval to compare against for the other side
+                        varIntervals.addInterval(pair.first->colorType->getFullInterval());
+                    } else if(varIntervals.size() < 1){
+                        //If any varinterval ends up empty then we were unable to use this arc interval
+                        validInterval = false;
+                        break;
+                    }
+                    localVarMap[pair.first] = varIntervals;
+                }
+
+                if(validInterval){
+                    variableMaps.push_back(localVarMap);
+                }                          
+            }  
+        }
+
+        bool getVarIntervals(std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>>& variableMaps, std::unordered_map<uint32_t, Colored::ArcIntervals> placeArcIntervals){
+            for(auto& placeArcInterval : placeArcIntervals){            
+                for(uint32_t j = 0; j < placeArcInterval.second._intervalTupleVec.size(); j++){
+                    uint32_t intervalTupleSize = placeArcInterval.second._intervalTupleVec[j].size();
+                    //If we have not found intervals for any place yet, we fill the intervals from this place
+                    //Else we restrict the intervals we already found to only keep those that can also be matched in this place
+                    if(variableMaps.empty()){                    
+                        fillVarMaps(variableMaps, &placeArcInterval.second, &intervalTupleSize, &j);                                            
+                    } else {
+                        std::vector<std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t>> newVarMapVec;
+                        
+                        for(auto& varMap : variableMaps){          
+                            for(uint32_t i = 0; i < intervalTupleSize; i++){
+                                std::unordered_map<const Colored::Variable *, Colored::intervalTuple_t> localVarMap;
+                                bool allVarsAssigned = true;
+                                auto interval = &placeArcInterval.second._intervalTupleVec[j]._intervals[i];
+                                
+                                populateLocalMap(&placeArcInterval.second, varMap, localVarMap, interval, allVarsAssigned, j);                       
+                                
+                                for(auto& varTuplePair : varMap){
+                                    if(localVarMap.count(varTuplePair.first) == 0){
+                                        localVarMap[varTuplePair.first] = std::move(varTuplePair.second);
+                                    }
+                                }
+
+                                if(allVarsAssigned){
+                                    newVarMapVec.push_back(std::move(localVarMap));
+                                }                               
+                            }                                                                                    
+                        }               
+                        variableMaps = std::move(newVarMapVec);                    
+                    }
+                    //If we did not find any intervals for an arc, then the transition cannot be activated
+                    if(variableMaps.empty()){
+                        return false;
+                    }                          
+                }
+            }
+            return true;
+        }
+    };    
+}
+
+#endif /* INTERVALGENERATOR_H */
 \ No newline at end of file
 
=== added file 'include/PetriEngine/Colored/Intervals.h'
--- include/PetriEngine/Colored/Intervals.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/Colored/Intervals.h	2021-04-02 18:07:40 +0000
@@ -0,0 +1,630 @@
+/* Copyright (C) 2020  Alexander Bilgram <[e-mail]>,
+ *                     Peter Haar Taankvist <[e-mail]>,
+ *                     Thomas Pedersen <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef INTERVALS_H
+#define INTERVALS_H
+
+#include "../TAR/range.h"
+#include <set>
+#include <unordered_map>
+#include <chrono>
+
+
+namespace PetriEngine {
+    namespace Colored {
+
+        struct interval_t {
+            std::vector<Reachability::range_t> _ranges;
+
+            interval_t() {
+            }
+
+            ~interval_t(){}
+
+            interval_t(std::vector<Reachability::range_t> ranges) : _ranges(ranges) {
+            }
+
+            size_t size(){
+                return _ranges.size();
+            }
+
+            uint32_t intervalCombinations(){
+                uint32_t product = 1;
+                for(auto range : _ranges){
+                    product *= range.size();
+                }
+                if(_ranges.empty()){
+                    return 0;
+                }
+                return product;
+            }
+
+            bool isSound(){
+                for(auto range: _ranges) {
+                    if(!range.isSound()){
+                        return false;
+                    }
+                }
+                return true;
+            }
+
+            void addRange(Reachability::range_t newRange) {
+                _ranges.push_back(newRange);
+            }
+
+            void addRange(Reachability::range_t newRange, uint32_t index){
+                _ranges.insert(_ranges.begin() + index, newRange);
+            }
+
+            void addRange(uint32_t l, uint32_t u) {
+                _ranges.push_back(Reachability::range_t(l, u));
+            }
+
+            void addRange(uint32_t lower, uint32_t upper, uint32_t index){
+                _ranges.insert(_ranges.begin() + index, Reachability::range_t(lower, upper));
+            }
+
+            Reachability::range_t& operator[] (size_t index) {
+                return _ranges[index];
+            }
+            
+            Reachability::range_t& operator[] (int index) {
+                return _ranges[index];
+            }
+            
+            Reachability::range_t& operator[] (uint32_t index) {
+                assert(index < _ranges.size());
+                return _ranges[index];
+            }
+
+            Reachability::range_t& getFirst() {
+                return _ranges[0];
+            }
+
+            Reachability::range_t& getLast() {
+                return _ranges.back();
+            }
+
+            std::vector<uint32_t> getLowerIds(){
+                std::vector<uint32_t> ids;
+                for(auto range : _ranges){
+                    ids.push_back(range._lower);
+                }
+                return ids;
+            }
+
+            std::vector<uint32_t> getUpperIds(){
+                std::vector<uint32_t> ids;
+                for(auto range : _ranges){
+                    ids.push_back(range._upper);
+                }
+                return ids;
+            }
+
+            bool equals(interval_t other){
+                if(other.size() != size()){
+                    return false;
+                }
+                for(uint32_t i = 0; i < size(); i++){
+                    auto comparisonRes = _ranges[i].compare(other[i]);
+                    if(!comparisonRes.first || !comparisonRes.second){
+                        return false;
+                    }
+                }
+                return true;
+            }
+
+            uint32_t getContainedColors(){
+                uint32_t colors = 1;
+                for(auto range: _ranges) {
+                    colors *= 1+  range._upper - range._lower;
+                }          
+                return colors;
+            }
+
+            bool contains(interval_t other){
+                if(other.size() != size()){
+                    return false;
+                }
+                for(uint32_t i = 0; i < size(); i++){
+                    if(!_ranges[i].compare(other[i]).first){
+                        return false;
+                    }
+                }
+                return true;
+            }
+
+            void constrain(interval_t other){
+                for(uint32_t i = 0; i < _ranges.size(); i++){
+                    _ranges[i] &= other._ranges[i];
+                }
+            }
+
+            interval_t getOverlap(interval_t other){
+                interval_t overlapInterval;
+                if(size() != other.size()){
+                    return overlapInterval;
+                }
+
+                for(uint32_t i = 0; i < size(); i++){
+                    auto rangeCopy = _ranges[i];
+                    overlapInterval.addRange(rangeCopy &= other[i]);
+                }
+
+                return overlapInterval;
+            }
+
+            void print() {
+                for(auto range : _ranges){
+                    std::cout << " " << range._lower << "-" << range._upper << " ";
+                }
+            }
+        };
+
+        struct closestIntervals {
+            uint32_t intervalId1;
+            uint32_t intervalId2;
+            uint32_t distance;
+        };
+
+        struct intervalTuple_t {
+            std::vector<interval_t> _intervals;
+            double totalinputtime = 0;
+
+            ~intervalTuple_t() {
+            }
+
+            intervalTuple_t() {
+            }
+
+            intervalTuple_t(std::vector<interval_t> ranges) :  _intervals(ranges) {
+            };
+
+            interval_t& getFirst(){
+                return _intervals[0];
+            }
+
+            interval_t& back() {
+                return _intervals.back();
+            }
+
+            size_t size() {
+                return _intervals.size();
+            }
+
+            size_t tupleSize() {
+                return _intervals[0].size();
+            }
+
+            uint32_t getContainedColors(){
+                uint32_t colors = 0;
+                for (auto interval : _intervals) {
+                    colors += interval.getContainedColors();              
+                }
+                return colors;
+            }
+
+            std::pair<uint32_t,uint32_t> shiftInterval(uint32_t lower, uint32_t upper, uint32_t ctSize, int32_t modifier){
+                int32_t lower_val = ctSize + (lower + modifier);
+                int32_t upper_val = ctSize + (upper + modifier);
+                return std::make_pair(lower_val % ctSize, upper_val % ctSize);
+            }
+
+            uint32_t intervalCombinations(){
+                uint32_t res = 0;
+                for(auto interval : _intervals){
+                    res += interval.intervalCombinations();
+                }
+                return res;
+            }
+
+            bool hasValidIntervals(){
+                for(auto interval : _intervals) {
+                    if(interval.isSound()){
+                        return true;
+                    }
+                }
+                return false;
+            }
+
+            interval_t& operator[] (size_t index) {
+                return _intervals[index];
+            }
+            
+            interval_t& operator[] (int index) {
+                return _intervals[index];
+            }
+            
+            interval_t& operator[] (uint32_t index) {
+                assert(index < _intervals.size());
+                return _intervals[index];
+            }
+
+            interval_t isRangeEnd(std::vector<uint32_t> ids) {
+                for (uint32_t j = 0; j < _intervals.size(); j++) {
+                    bool rangeEnd = true;
+                    for (uint32_t i = 0; i < _intervals[j].size(); i++) {
+                        auto range =  _intervals[j][i];
+                        if (range._upper != ids[i]) {
+                            rangeEnd = false;
+                            break;
+                        }
+                    }
+                    if(rangeEnd) {
+                        if(j+1 != _intervals.size()) {
+                            return _intervals[j+1];
+                        } else {
+                            return getFirst();
+                        }
+                    }
+                }
+                return interval_t();
+            }
+
+            std::vector<Colored::interval_t> shrinkIntervals(uint32_t newSize){
+                std::vector<Colored::interval_t> resizedIntervals;
+                for(auto interval : _intervals){
+                    Colored::interval_t resizedInterval;
+                    for(uint32_t i = 0; i < newSize; i++){
+                        resizedInterval.addRange(interval[i]);
+                    }
+                    resizedIntervals.push_back(resizedInterval);
+                }
+                return resizedIntervals;
+            }
+
+            void addInterval(interval_t interval) {
+                uint32_t vecIndex = 0;
+
+                if(!_intervals.empty()) {
+                    assert(_intervals[0].size() == interval.size());
+                } else {
+                    _intervals.push_back(interval);
+                    return;
+                }
+
+                for (auto& localInterval : _intervals) {
+                    bool overlap = true;
+                    enum FoundPlace {undecided, greater, lower};
+                    FoundPlace foundPlace = undecided;
+
+                    for(uint32_t k = 0; k < interval.size(); k++){
+                        if(interval[k]._lower > localInterval[k]._upper  || localInterval[k]._lower > interval[k]._upper){
+                            overlap = false;
+                        }
+                        if(interval[k]._lower < localInterval[k]._lower){
+                            if(foundPlace == undecided){
+                                foundPlace = lower;
+                            }                            
+                        } else if (interval[k]._lower > localInterval[k]._lower){
+                            if(foundPlace == undecided){
+                                foundPlace = greater;
+                            }                            
+                        }
+                        if(!overlap && foundPlace != undecided){
+                            break;
+                        }
+                    }
+
+                    if(overlap) {
+                        for(uint32_t k = 0; k < interval.size(); k++){
+                            localInterval[k] |= interval[k];
+                        }
+                        return;
+                    } else if(foundPlace == lower){
+                        break;
+                    }                    
+                    vecIndex++;
+                }
+
+                _intervals.insert(_intervals.begin() + vecIndex, interval);
+            }
+
+            void constrainLower(std::vector<uint32_t> values, bool strict) {
+                for(uint32_t i = 0; i < _intervals.size(); i++) {
+                    for(uint32_t j = 0; j < values.size(); j++){
+                        if(strict && _intervals[i][j]._lower <= values[j]){
+                            _intervals[i][j]._lower = values[j]+1;
+                        } 
+                        else if(!strict && _intervals[i][j]._lower < values[j]){
+                            _intervals[i][j]._lower = values[j];
+                        }                          
+                    }
+                }
+                simplify();
+            }
+
+            void constrainUpper(std::vector<uint32_t> values, bool strict) {
+                for(uint32_t i = 0; i < _intervals.size(); i++) {
+                    for(uint32_t j = 0; j < values.size(); j++){
+                        if(strict && _intervals[i][j]._upper >= values[j]){
+                            _intervals[i][j]._upper = values[j]-1;
+                        } 
+                        else if(!strict && _intervals[i][j]._upper > values[j]){
+                            _intervals[i][j]._upper = values[j];
+                        }                        
+                    }
+                }
+                simplify();
+            }
+
+            void expandLower(std::vector<uint32_t> values) {
+                for(uint32_t i = 0; i < values.size(); i++) {
+                    _intervals[0][i]._lower = std::min(values[i],_intervals[0][i]._lower);
+                }
+            }
+
+            void expandUpper(std::vector<uint32_t> values) {
+                for(uint32_t i = 0; i < values.size(); i++) {
+                    _intervals[0][i]._upper = std::max(values[i],_intervals[0][i]._upper);
+                }
+            }
+
+            void print() {
+                for (auto interval : _intervals){
+                    std::cout << "[";
+                    interval.print();
+                    std::cout << "]" << std::endl;
+                }
+            }
+
+            std::vector<uint32_t> getLowerIds(){
+                std::vector<uint32_t> ids;
+                for(auto interval : _intervals){
+                    if(ids.empty()){
+                        ids = interval.getLowerIds();
+                    } else {
+                        for(uint32_t i = 0; i < ids.size(); i++){
+                            ids[i] = std::min(ids[i], interval[i]._lower);
+                        }
+                    }
+                }
+                return ids;
+            }
+
+            std::vector<uint32_t> getLowerIds(int32_t modifier, std::vector<size_t> sizes){
+                std::vector<uint32_t> ids;
+                for(uint32_t j = 0; j < size(); j++){
+                    auto interval = &_intervals[j];
+                    if(ids.empty()){
+                        for(uint32_t i = 0; i < ids.size(); i++){
+                            auto shiftedInterval = shiftInterval(interval->operator[](i)._lower, interval->operator[](i)._upper, sizes[i], modifier);
+                            if(shiftedInterval.first > shiftedInterval.second){
+                                ids.push_back(0);
+                            } else {
+                                ids.push_back(shiftedInterval.first);
+                            }                            
+                        }
+                    } else {
+                        for(uint32_t i = 0; i < ids.size(); i++){
+                            if(ids[i] == 0){
+                                continue;
+                            }
+                            auto shiftedInterval = shiftInterval(interval->operator[](i)._lower, interval->operator[](i)._upper, sizes[i], modifier);
+                            if(shiftedInterval.first > shiftedInterval.second){
+                                ids[i] = 0;
+                            } else {
+                                ids[i] = std::max(ids[i], shiftedInterval.first);
+                            }                            
+                        }
+                    }
+                }
+                return ids;
+            }
+
+            std::vector<uint32_t> getUpperIds(){
+                std::vector<uint32_t> ids;
+                for(auto interval : _intervals){
+                    if(ids.empty()){
+                        ids = interval.getUpperIds();
+                    } else {
+                        for(uint32_t i = 0; i < ids.size(); i++){
+                            ids[i] = std::max(ids[i], interval[i]._upper);
+                        }
+                    }
+                }
+                return ids;
+            }
+
+            std::vector<uint32_t> getUpperIds(int32_t modifier, std::vector<size_t> sizes){
+                std::vector<uint32_t> ids;
+                for(uint32_t j = 0; j < size(); j++){
+                    auto interval = &_intervals[j];
+                    if(ids.empty()){
+                        for(uint32_t i = 0; i < ids.size(); i++){
+                            auto shiftedInterval = shiftInterval(interval->operator[](i)._lower, interval->operator[](i)._upper, sizes[i], modifier);
+
+                            if(shiftedInterval.first > shiftedInterval.second){
+                                ids.push_back(sizes[i]-1);
+                            } else {
+                                ids.push_back(shiftedInterval.second);
+                            }                            
+                        }
+                    } else {
+                        for(uint32_t i = 0; i < ids.size(); i++){
+                            if(ids[i] == sizes[i]-1){
+                                continue;
+                            }
+                            auto shiftedInterval = shiftInterval(interval->operator[](i)._lower, interval->operator[](i)._upper, sizes[i], modifier);
+
+                            if(shiftedInterval.first > shiftedInterval.second){
+                                ids[i] = sizes[i]-1;
+                            } else {
+                                ids[i] = std::max(ids[i], shiftedInterval.second);
+                            }                            
+                        }
+                    }
+                }
+                return ids;
+            }
+
+            void applyModifier(int32_t modifier, std::vector<size_t> sizes){
+                std::vector<interval_t> collectedIntervals;
+                for(auto& interval : _intervals){
+                    std::vector<interval_t> newIntervals;
+                    newIntervals.push_back(std::move(interval));
+                    for(uint32_t i = 0; i < interval.size(); i++){
+                        std::vector<interval_t> tempIntervals;
+                        for(auto& interval1 : newIntervals){
+                            auto shiftedInterval = shiftInterval(interval1[i]._lower, interval1[i]._upper, sizes[i], modifier);
+
+                            if(shiftedInterval.first > shiftedInterval.second){
+                                auto newInterval = interval1;
+
+                                interval1[i]._lower = 0;
+                                interval1[i]._upper = shiftedInterval.second;
+
+                                newInterval[i]._lower = shiftedInterval.first;
+                                newInterval[i]._upper = sizes[i]-1;
+                                tempIntervals.push_back(std::move(newInterval));
+                            }else {
+                                interval1[i]._lower = shiftedInterval.first;
+                                interval1[i]._upper = shiftedInterval.second;
+                            }
+                        }
+                        newIntervals.insert(newIntervals.end(), tempIntervals.begin(), tempIntervals.end());                                                
+                    }
+                    collectedIntervals.insert(collectedIntervals.end(), newIntervals.begin(), newIntervals.end());
+                }
+                
+                _intervals = std::move(collectedIntervals);
+            }
+
+            bool contains(interval_t interval){
+                for(auto localInterval : _intervals){
+                    if(localInterval.contains(interval)){
+                        return true;
+                    }
+                }
+                return false;
+            }
+
+            void removeInterval(interval_t interval) {
+                for (uint32_t i = 0; i < _intervals.size(); i++) {
+                    if(interval.equals(_intervals[i])){
+                        removeInterval(i);
+                        return;
+                    }
+                }
+            }
+
+            void removeInterval(uint32_t index) {               
+                _intervals.erase(_intervals.begin() + index); 
+            }
+
+            
+
+            void restrict(uint32_t k){              
+                simplify();
+                if(k == 0){
+                    return;
+                }
+                
+                while (size() > k){ 
+                    closestIntervals closestInterval = getClosestIntervals();
+                    auto interval = &_intervals[closestInterval.intervalId1]; 
+                    auto otherInterval = &_intervals[closestInterval.intervalId2]; 
+
+                    for(uint32_t l = 0; l < interval->size(); l++) {
+                        interval->operator[](l) |= otherInterval->operator[](l);
+                    }
+                    
+                    _intervals.erase(_intervals.begin() + closestInterval.intervalId2);
+                    
+                }
+            }
+
+            closestIntervals getClosestIntervals(){
+                closestIntervals currentBest = {0,0, UINT32_MAX};
+                    for (uint32_t i = 0; i < size()-1; i++) {
+                        auto interval = &_intervals[i];
+                        for(uint32_t j = i+1; j < size(); j++){
+                            auto otherInterval = &_intervals[j];
+                            uint32_t dist = 0;
+                            
+                            for(uint32_t k = 0; k < interval->size(); k++) {
+                                int32_t val1 = otherInterval->operator[](k)._lower - interval->operator[](k)._upper;
+                                int32_t val2 = interval->operator[](k)._lower - otherInterval->operator[](k)._upper;
+                                dist += std::max(0, std::max(val1, val2));
+                                if(dist >= currentBest.distance){
+                                    break;
+                                }
+                            }
+                            
+                            if(dist < currentBest.distance){
+                                currentBest.distance = dist;
+                                currentBest.intervalId1 = i;
+                                currentBest.intervalId2 = j;
+
+                                //if the distance is 1 we cannot find any intervals that are closer so we stop searching
+                                if(currentBest.distance == 1){
+                                    return currentBest;
+                                }
+                            }                           
+                        }
+                    }
+                return currentBest;
+            }
+
+            void simplify() {
+                std::set<uint32_t> rangesToRemove;
+                if(_intervals.empty()){
+                    return;
+                }
+
+                for (uint32_t i = 0; i < _intervals.size(); i++) {
+                    auto interval = &_intervals[i];
+                    if(!interval->isSound()){
+                        rangesToRemove.insert(i);
+                        continue;
+                    }   
+                    for(uint32_t j = i+1; j < _intervals.size(); j++){
+                        auto otherInterval = &_intervals[j];
+
+                        if(!otherInterval->isSound()){
+                            continue;
+                        }   
+                        bool overlap = true;
+
+                        if(overlap){
+                            for(uint32_t k = 0; k < interval->size(); k++) {                            
+                                if(interval->operator[](k)._lower > otherInterval->operator[](k)._upper  || otherInterval->operator[](k)._lower > interval->operator[](k)._upper) {
+                                    overlap = false;
+                                    break;
+                                }
+                            }
+                        }
+                        
+                        if(overlap) {
+                            for(uint32_t l = 0; l < interval->size(); l++) {
+                                interval->operator[](l) |= otherInterval->operator[](l);
+                            }
+                            rangesToRemove.insert(j);
+                        }  
+                    }
+                }
+                for (auto i = rangesToRemove.rbegin(); i != rangesToRemove.rend(); ++i) {
+                    _intervals.erase(_intervals.begin() + *i);
+                }
+            } 
+        };
+    }
+}
+
+
+#endif /* INTERVALS_H */
 \ No newline at end of file
 
=== added file 'include/PetriEngine/PQL/CTLVisitor.h'
--- include/PetriEngine/PQL/CTLVisitor.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/PQL/CTLVisitor.h	2021-04-02 18:07:40 +0000
@@ -0,0 +1,197 @@
+#ifndef VERIFYPN_CTLVISITOR_H
+#define VERIFYPN_CTLVISITOR_H
+
+#include "Visitor.h"
+
+namespace PetriEngine::PQL {
+
+    enum CTLSyntaxType {BOOLEAN, PATH, ERROR = -1};
+
+    class IsCTLVisitor : public Visitor {
+    public:
+        bool isCTL = true;
+
+    protected:
+        void _accept(const NotCondition *element) override;
+
+        void _accept(const AndCondition *element) override;
+
+        void _accept(const OrCondition *element) override;
+
+        void _accept(const LessThanCondition *element) override;
+
+        void _accept(const LessThanOrEqualCondition *element) override;
+
+        void _accept(const EqualCondition *element) override;
+
+        void _accept(const NotEqualCondition *element) override;
+
+        void _accept(const DeadlockCondition *element) override;
+
+        void _accept(const CompareConjunction *element) override;
+
+        void _accept(const UnfoldedUpperBoundsCondition *element) override;
+
+        void _accept(const EFCondition *condition) override;
+
+        void _accept(const EGCondition *condition) override;
+
+        void _accept(const AGCondition *condition) override;
+
+        void _accept(const AFCondition *condition) override;
+
+        void _accept(const EXCondition *condition) override;
+
+        void _accept(const AXCondition *condition) override;
+
+        void _accept(const EUCondition *condition) override;
+
+        void _accept(const AUCondition *condition) override;
+
+        void _accept(const ACondition *condition) override;
+
+        void _accept(const ECondition *condition) override;
+
+        void _accept(const GCondition *condition) override;
+
+        void _accept(const FCondition *condition) override;
+
+        void _accept(const XCondition *condition) override;
+
+        void _accept(const UntilCondition *condition) override;
+
+        void _accept(const UnfoldedFireableCondition *element) override;
+
+        void _accept(const FireableCondition *element) override;
+
+        void _accept(const UpperBoundsCondition *element) override;
+
+        void _accept(const LivenessCondition *element) override;
+
+        void _accept(const KSafeCondition *element) override;
+
+        void _accept(const QuasiLivenessCondition *element) override;
+
+        void _accept(const StableMarkingCondition *element) override;
+
+        void _accept(const BooleanCondition *element) override;
+
+        void _accept(const UnfoldedIdentifierExpr *element) override;
+
+        void _accept(const LiteralExpr *element) override;
+
+        void _accept(const PlusExpr *element) override;
+
+        void _accept(const MultiplyExpr *element) override;
+
+        void _accept(const MinusExpr *element) override;
+
+        void _accept(const SubtractExpr *element) override;
+
+        void _accept(const IdentifierExpr *element) override;
+
+    private:
+        CTLSyntaxType _cur_type;
+
+        void _accept(const LogicalCondition *element);
+
+        void _accept(const CompareCondition *element);
+    };
+
+    class AsCTL : public Visitor {
+    public:
+        Condition_ptr _ctl_query = nullptr;
+        Expr_ptr _expression = nullptr;
+
+    protected:
+        void _accept(const NotCondition *element) override;
+
+        void _accept(const AndCondition *element) override;
+
+        void _accept(const OrCondition *element) override;
+
+        void _accept(const LessThanCondition *element) override;
+
+        void _accept(const LessThanOrEqualCondition *element) override;
+
+        void _accept(const EqualCondition *element) override;
+
+        void _accept(const NotEqualCondition *element) override;
+
+        void _accept(const DeadlockCondition *element) override;
+
+        void _accept(const CompareConjunction *element) override;
+
+        void _accept(const UnfoldedUpperBoundsCondition *element) override;
+
+        void _accept(const EFCondition *condition) override;
+
+        void _accept(const EGCondition *condition) override;
+
+        void _accept(const AGCondition *condition) override;
+
+        void _accept(const AFCondition *condition) override;
+
+        void _accept(const EXCondition *condition) override;
+
+        void _accept(const AXCondition *condition) override;
+
+        void _accept(const EUCondition *condition) override;
+
+        void _accept(const AUCondition *condition) override;
+
+        void _accept(const ACondition *condition) override;
+
+        void _accept(const ECondition *condition) override;
+
+        void _accept(const GCondition *condition) override;
+
+        void _accept(const FCondition *condition) override;
+
+        void _accept(const XCondition *condition) override;
+
+        void _accept(const UntilCondition *condition) override;
+
+        void _accept(const UnfoldedFireableCondition *element) override;
+
+        void _accept(const FireableCondition *element) override;
+
+        void _accept(const UpperBoundsCondition *element) override;
+
+        void _accept(const LivenessCondition *element) override;
+
+        void _accept(const KSafeCondition *element) override;
+
+        void _accept(const QuasiLivenessCondition *element) override;
+
+        void _accept(const StableMarkingCondition *element) override;
+
+        void _accept(const BooleanCondition *element) override;
+
+        void _accept(const UnfoldedIdentifierExpr *element) override;
+
+        void _accept(const LiteralExpr *element) override;
+
+        void _accept(const PlusExpr *element) override;
+
+        void _accept(const MultiplyExpr *element) override;
+
+        void _accept(const MinusExpr *element) override;
+
+        void _accept(const SubtractExpr *element) override;
+
+        void _accept(const IdentifierExpr *element) override;
+
+    private:
+        template<typename T>
+        void _acceptNary(const T *element);
+    
+        template<typename T>
+        Expr_ptr copy_narry_expr(const T* el);
+        
+        template<typename T>
+        std::shared_ptr<T> copy_compare_condition(const T *element);
+    };
+}
+
+#endif //VERIFYPN_CTLVISITOR_H
 
=== modified file 'include/PetriEngine/PQL/Contexts.h'
--- include/PetriEngine/PQL/Contexts.h	2020-04-27 14:47:10 +0000
+++ include/PetriEngine/PQL/Contexts.h	2021-04-02 18:07:40 +0000
@@ -38,8 +38,8 @@
         /** Context provided for context analysis */
         class AnalysisContext {
         protected:
-            const unordered_map<std::string, uint32_t>& _placeNames;
-            const unordered_map<std::string, uint32_t>& _transitionNames;
+            const std::unordered_map<std::string, uint32_t>& _placeNames;
+            const std::unordered_map<std::string, uint32_t>& _transitionNames;
             const PetriNet* _net;
             std::vector<ExprError> _errors;
         public:
@@ -176,7 +176,7 @@
 
             SimplificationContext(const MarkVal* marking,
                     const PetriNet* net, uint32_t queryTimeout, uint32_t lpTimeout,
-                    LPCache* cache)
+                    Simplification::LPCache* cache)
                     : _queryTimeout(queryTimeout), _lpTimeout(lpTimeout) {
                 _negated = false;
                 _marking = marking;
@@ -222,8 +222,8 @@
             }
             
             uint32_t getLpTimeout() const;
-            
-            LPCache* cache() const
+
+            Simplification::LPCache* cache() const
             {
                 return _cache;
             }
@@ -237,7 +237,7 @@
             const PetriNet* _net;
             uint32_t _queryTimeout, _lpTimeout;
             std::chrono::high_resolution_clock::time_point _start;
-            LPCache* _cache;
+            Simplification::LPCache* _cache;
             mutable glp_prob* _base_lp = nullptr;
 
             glp_prob* buildBase() const;
 
=== modified file 'include/PetriEngine/PQL/Expressions.h'
--- include/PetriEngine/PQL/Expressions.h	2020-06-02 16:20:24 +0000
+++ include/PetriEngine/PQL/Expressions.h	2021-04-02 18:07:40 +0000
@@ -34,7 +34,7 @@
 
 namespace PetriEngine {
     namespace PQL {
-        
+
         std::string generateTabs(uint32_t tabs);
         class CompareCondition;
         class NotCondition;
@@ -55,19 +55,22 @@
                 for(auto& e : _exprs) sum += e->formulaSize();
                 return sum + 1;
             }
-            void toString(std::ostream&) const override;
             bool placeFree() const override;
             auto& expressions() const { return _exprs; }
+            size_t operands() const { return _exprs.size(); }
+            const Expr_ptr &operator[](size_t i) const {
+                return _exprs[i];
+            }
         protected:
             virtual int apply(int v1, int v2) const = 0;
             virtual std::string op() const = 0;
             std::vector<Expr_ptr> _exprs;
             virtual int32_t preOp(const EvaluationContext& context) const;
         };
-        
+
         class PlusExpr;
         class MultiplyExpr;
-        
+
         class CommutativeExpr : public NaryExpr
         {
         public:
@@ -80,7 +83,6 @@
                 for(auto& e : _exprs) sum += e->formulaSize();
                 return sum + 1;
             }
-            void toString(std::ostream&) const override;            
             bool placeFree() const override;
             auto constant() const { return _constant; }
             auto& places() const { return _ids; }
@@ -98,13 +100,12 @@
         public:
 
             PlusExpr(std::vector<Expr_ptr>&& exprs, bool tk = false);
-            
+
             Expr::Types type() const override;
             Member constraint(SimplificationContext& context) const override;
             void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
             bool tk = false;
-            void incr(ReducingSuccessorGenerator& generator) const override;
-            void decr(ReducingSuccessorGenerator& generator) const override;
+
             void visit(Visitor& visitor) const override;
         protected:
             int apply(int v1, int v2) const override;
@@ -122,8 +123,7 @@
             Expr::Types type() const override;
             Member constraint(SimplificationContext& context) const override;
             void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
-            void incr(ReducingSuccessorGenerator& generator) const override;
-            void decr(ReducingSuccessorGenerator& generator) const override;
+
             void toBinary(std::ostream&) const override;
             void visit(Visitor& visitor) const override;
         protected:
@@ -140,8 +140,7 @@
             Expr::Types type() const override;
             Member constraint(SimplificationContext& context) const override;
             void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
-            void incr(ReducingSuccessorGenerator& generator) const override;
-            void decr(ReducingSuccessorGenerator& generator) const override;
+
             void visit(Visitor& visitor) const override;
         protected:
             int apply(int v1, int v2) const override;
@@ -158,13 +157,11 @@
             }
             void analyze(AnalysisContext& context) override;
             int evaluate(const EvaluationContext& context) override;
-            void toString(std::ostream&) const override;
             Expr::Types type() const override;
             Member constraint(SimplificationContext& context) const override;
             void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
             void toBinary(std::ostream&) const override;
-            void incr(ReducingSuccessorGenerator& generator) const override;
-            void decr(ReducingSuccessorGenerator& generator) const override;
+
             void visit(Visitor& visitor) const override;
             int formulaSize() const override{
                 return _expr->formulaSize() + 1;
@@ -181,14 +178,13 @@
 
             LiteralExpr(int value) : _value(value) {
             }
+            LiteralExpr(const LiteralExpr&) = default;
             void analyze(AnalysisContext& context) override;
             int evaluate(const EvaluationContext& context) override;
-            void toString(std::ostream&) const override;
             Expr::Types type() const override;
             void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
             void toBinary(std::ostream&) const override;
-            void incr(ReducingSuccessorGenerator& generator) const override;
-            void decr(ReducingSuccessorGenerator& generator) const override;
+
             void visit(Visitor& visitor) const override;
             int formulaSize() const override{
                 return 1;
@@ -206,29 +202,18 @@
         class IdentifierExpr : public Expr {
         public:
             IdentifierExpr(const std::string& name) : _name(name) {}
+            IdentifierExpr(const IdentifierExpr&) = default;
             void analyze(AnalysisContext& context) override;
             int evaluate(const EvaluationContext& context) override {
                 return _compiled->evaluate(context);
             }
-            void toString(std::ostream& os) const override {
-                if(_compiled)
-                    _compiled->toString(os);
-                else
-                    os << _name;
-            }
-            Expr::Types type() const override {
+            [[nodiscard]] Expr::Types type() const override {
                 if(_compiled) return _compiled->type();
                 return Expr::IdentifierExpr;
             }
             void toXML(std::ostream& os, uint32_t tabs, bool tokencount = false) const override {
                 _compiled->toXML(os, tabs, tokencount);
             }
-            void incr(ReducingSuccessorGenerator& generator) const override {
-                _compiled->incr(generator);
-            }
-            void decr(ReducingSuccessorGenerator& generator) const override {
-                _compiled->decr(generator);
-            }
             int formulaSize() const override {
                 if(_compiled) return _compiled->formulaSize();
                 return 1;
@@ -241,11 +226,20 @@
             Member constraint(SimplificationContext& context) const override {
                 return _compiled->constraint(context);
             }
-            
+
             void toBinary(std::ostream& s) const override {
                 _compiled->toBinary(s);
             }
-            void visit(Visitor& visitor) const override;            
+            void visit(Visitor& visitor) const override;
+
+            [[nodiscard]] const std::string &name() const {
+                return _name;
+            }
+            
+            [[nodiscard]] const Expr_ptr &compiled() const {
+                return _compiled;
+            }
+
         private:
             std::string _name;
             Expr_ptr _compiled;
@@ -257,18 +251,17 @@
             UnfoldedIdentifierExpr(const std::string& name, int offest)
             : _offsetInMarking(offest), _name(name) {
             }
-            
+
             UnfoldedIdentifierExpr(const std::string& name) : UnfoldedIdentifierExpr(name, -1) {
             }
             
+            UnfoldedIdentifierExpr(const UnfoldedIdentifierExpr&) = default;
+
             void analyze(AnalysisContext& context) override;
             int evaluate(const EvaluationContext& context) override;
-            void toString(std::ostream&) const override;
             Expr::Types type() const override;
             void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
             void toBinary(std::ostream&) const override;
-            void incr(ReducingSuccessorGenerator& generator) const override;
-            void decr(ReducingSuccessorGenerator& generator) const override;
             int formulaSize() const override{
                 return 1;
             }
@@ -276,7 +269,7 @@
             int offset() const {
                 return _offsetInMarking;
             }
-            const std::string& name()
+            const std::string& name() const
             {
                 return _name;
             }
@@ -311,18 +304,14 @@
 
             void toXML(std::ostream& out, uint32_t tabs) const override
             { _compiled->toXML(out, tabs); }
-            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override
-            { _compiled->findInteresting(generator, negated);}
+
+
             Quantifier getQuantifier() const override
             { return _compiled->getQuantifier(); }
             Path getPath() const override { return _compiled->getPath(); }
             CTLType getQueryType() const override { return _compiled->getQueryType(); }
             bool containsNext() const override { return _compiled->containsNext(); }
             bool nestedDeadlock() const override { return _compiled->nestedDeadlock(); }
-#ifdef VERIFYPN_TAR
-            virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const
-            { return _compiled->encodeSat(net, context, uses, incremented); }
-#endif
             int formulaSize() const override{
                 return _compiled->formulaSize();
             }
@@ -344,14 +333,13 @@
                 if (_compiled) _compiled->analyze(context);
                 else _analyze(context);
             }
-            void toString(std::ostream &out) const {
-                if (_compiled) _compiled->toString(out);
-                else _toString(out);
+        public:
+            const Condition_ptr &getCompiled() const {
+                return _compiled;
             }
 
         protected:
             virtual void _analyze(AnalysisContext& context) = 0;
-            virtual void _toString(std::ostream& out) const = 0;
             virtual Condition_ptr clone() = 0;
             Condition_ptr _compiled = nullptr;
         };
@@ -373,7 +361,6 @@
             Result evalAndSet(const EvaluationContext& context) override;
             void visit(Visitor&) const override;
             uint32_t distance(DistanceContext& context) const override;
-            void toString(std::ostream&) const override;
             void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
             Retval simplify(SimplificationContext& context) const override;
             bool isReachability(uint32_t depth) const override;
@@ -381,7 +368,7 @@
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
             void toXML(std::ostream&, uint32_t tabs) const override;
             void toBinary(std::ostream&) const override;
-            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
+
             Quantifier getQuantifier() const override { return Quantifier::NEG; }
             Path getPath() const override { return Path::pError; }
             CTLType getQueryType() const override { return CTLType::LOPERATOR; }
@@ -393,18 +380,18 @@
             Condition_ptr _cond;
             bool _temporal = false;
         };
-        
-        
-        /******************** TEMPORAL OPERATORS ********************/        
-        
+
+
+        /******************** TEMPORAL OPERATORS ********************/
+
         class QuantifierCondition : public Condition
         {
         public:
-            virtual bool isTemporal() const override { return true;}
+            bool isTemporal() const override { return true;}
             CTLType getQueryType() const override { return CTLType::PATHQEURY; }
             virtual const Condition_ptr& operator[] (size_t i) const = 0;
         };
-        
+
         class SimpleQuantifierCondition : public QuantifierCondition {
         public:
             SimpleQuantifierCondition(const Condition_ptr cond) {
@@ -414,24 +401,174 @@
             int formulaSize() const override{
                 return _cond->formulaSize() + 1;
             }
-            
+
             void analyze(AnalysisContext& context) override;
             Result evaluate(const EvaluationContext& context) override;
             Result evalAndSet(const EvaluationContext& context) override;
-            void toString(std::ostream&) const override;
             void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
             void toBinary(std::ostream& out) const override;
-            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
+
             virtual const Condition_ptr& operator[] (size_t i) const override { return _cond;}
-            virtual bool containsNext() const override { return _cond->containsNext(); }
+            bool containsNext() const override { return _cond->containsNext(); }
             bool nestedDeadlock() const override { return _cond->nestedDeadlock(); }
         private:
             virtual std::string op() const = 0;
-            
+
         protected:
             Condition_ptr _cond;
         };
-        
+
+        class ECondition : public SimpleQuantifierCondition {
+        public:
+            using SimpleQuantifierCondition::SimpleQuantifierCondition;
+
+            Result evaluate(const EvaluationContext& context) override;
+
+            Retval simplify(SimplificationContext& context) const override;
+
+            bool isReachability(uint32_t depth) const override;
+            Condition_ptr prepareForReachability(bool negated) const override;
+            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
+            void toXML(std::ostream&, uint32_t tabs) const override;
+            Quantifier getQuantifier() const override { return Quantifier::E; }
+            Path getPath() const override             { return Path::pError; }
+            uint32_t distance(DistanceContext& context) const override {
+                // TODO implement
+                assert(false); std::cerr << "TODO implement" << std::endl; exit(0);
+            }
+            bool isLoopSensitive() const override {
+                // Other LTL Loop sensitivity depend on the outermost quantifier being an A,
+                // so if it is an E we disable loop sensitive reductions.
+                return true;
+            }
+            void visit(Visitor&) const override;
+        private:
+            std::string op() const override;
+        };
+
+      class ACondition : public SimpleQuantifierCondition {
+        public:
+            using SimpleQuantifierCondition::SimpleQuantifierCondition;
+
+            Result evaluate(const EvaluationContext& context) override;
+
+            Retval simplify(SimplificationContext& context) const override;
+            bool isReachability(uint32_t depth) const override;
+            Condition_ptr prepareForReachability(bool negated) const override;
+            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
+            void toXML(std::ostream&, uint32_t tabs) const override;
+            Quantifier getQuantifier() const override { return Quantifier::A; }
+            Path getPath() const override             { return Path::pError; }
+            uint32_t distance(DistanceContext& context) const override {
+                uint32_t retval = _cond->distance(context);
+                return retval;
+            }
+            void visit(Visitor&) const override;
+
+      private:
+            std::string op() const override;
+        };
+
+      class GCondition : public SimpleQuantifierCondition {
+      public:
+          using SimpleQuantifierCondition::SimpleQuantifierCondition;
+
+          Result evaluate(const EvaluationContext &context) override;
+
+          bool isReachability(uint32_t depth) const override {
+              // This could potentially be a reachability formula if the parent is an A.
+              // This case is however already handled by ACondition.
+              return false;
+          }
+
+          Condition_ptr prepareForReachability(bool negated) const override {
+              // TODO implement
+              assert(false);
+              std::cerr << "TODO implement" << std::endl;
+              exit(0);
+          }
+
+          Condition_ptr
+          pushNegation(negstat_t &, const EvaluationContext &context, bool nested, bool negated, bool initrw) override;
+
+          Retval simplify(SimplificationContext &context) const override;
+
+          void toXML(std::ostream &, uint32_t tabs) const override;
+
+          Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
+
+          Path getPath() const override { return Path::G; }
+
+          uint32_t distance(DistanceContext &context) const override {
+              context.negate();
+              uint32_t retval = _cond->distance(context);
+              context.negate();
+              return retval;
+          }
+
+          bool isLoopSensitive() const override { return true; }
+
+          void visit(Visitor &) const override;
+
+      private:
+          std::string op() const override;
+      };
+
+      class FCondition : public SimpleQuantifierCondition {
+        public:
+            using SimpleQuantifierCondition::SimpleQuantifierCondition;
+
+            Result evaluate(const EvaluationContext& context) override;
+
+            Retval simplify(SimplificationContext& context) const override;
+          bool isReachability(uint32_t depth) const override {
+              // This could potentially be a reachability formula if the parent is an E.
+              // This case is however already handled by ECondition.
+              return false;
+          }
+            Condition_ptr prepareForReachability(bool negated) const override {
+                // TODO implement
+                assert(false); std::cerr << "TODO implement" << std::endl; exit(0);
+            }
+            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
+            void toXML(std::ostream&, uint32_t tabs) const override;
+            Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
+            Path getPath() const override             { return Path::F; }
+            uint32_t distance(DistanceContext& context) const override {
+                return _cond->distance(context);
+            }
+            bool isLoopSensitive() const override { return true; }
+            void visit(Visitor&) const override;
+        private:
+            std::string op() const override;
+        };
+
+        class XCondition : public SimpleQuantifierCondition {
+        public:
+            using SimpleQuantifierCondition::SimpleQuantifierCondition;
+
+            bool isReachability(uint32_t depth) const override {
+                return false;
+            }
+            Condition_ptr prepareForReachability(bool negated) const override {
+                // TODO implement
+                assert(false); std::cerr << "TODO implement" << std::endl; exit(0);
+            }
+            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
+            Retval simplify(SimplificationContext& context) const override;
+            void toXML(std::ostream&, uint32_t tabs) const override;
+            Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
+            Path getPath() const override             { return Path::X; }
+            uint32_t distance(DistanceContext& context) const override {
+                return _cond->distance(context);
+            }
+            bool containsNext() const override { return true; }
+            bool isLoopSensitive() const override { return true; }
+            void visit(Visitor&) const override;
+        private:
+            std::string op() const override;
+        };
+
         class EXCondition : public SimpleQuantifierCondition {
         public:
             using SimpleQuantifierCondition::SimpleQuantifierCondition;
@@ -443,24 +580,24 @@
             Quantifier getQuantifier() const override { return Quantifier::E; }
             Path getPath() const override             { return Path::X; }
             uint32_t distance(DistanceContext& context) const override;
-            bool containsNext() const override { return true; }            
+            bool containsNext() const override { return true; }
             virtual bool isLoopSensitive() const override { return true; }
             void visit(Visitor&) const override;
         private:
             std::string op() const override;
         };
-        
+
         class EGCondition : public SimpleQuantifierCondition {
         public:
             using SimpleQuantifierCondition::SimpleQuantifierCondition;
- 
+
  	    Retval simplify(SimplificationContext& context) const override;
             bool isReachability(uint32_t depth) const override;
             Condition_ptr prepareForReachability(bool negated) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
             void toXML(std::ostream&, uint32_t tabs) const override;
             Quantifier getQuantifier() const override { return Quantifier::E; }
-            Path getPath() const override             { return Path::G; }            
+            Path getPath() const override             { return Path::G; }
             uint32_t distance(DistanceContext& context) const override;
             Result evaluate(const EvaluationContext& context) override;
             Result evalAndSet(const EvaluationContext& context) override;
@@ -469,18 +606,18 @@
         private:
             std::string op() const override;
         };
-        
+
         class EFCondition : public SimpleQuantifierCondition {
         public:
             using SimpleQuantifierCondition::SimpleQuantifierCondition;
- 
+
  	    Retval simplify(SimplificationContext& context) const override;
             bool isReachability(uint32_t depth) const override;
             Condition_ptr prepareForReachability(bool negated) const override;
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
             void toXML(std::ostream&, uint32_t tabs) const override;
             Quantifier getQuantifier() const override { return Quantifier::E; }
-            Path getPath() const override             { return Path::F; }            
+            Path getPath() const override             { return Path::F; }
             uint32_t distance(DistanceContext& context) const override;
             Result evaluate(const EvaluationContext& context) override;
             Result evalAndSet(const EvaluationContext& context) override;
@@ -506,7 +643,7 @@
         private:
             std::string op() const override;
         };
-        
+
         class AGCondition : public SimpleQuantifierCondition {
         public:
             using SimpleQuantifierCondition::SimpleQuantifierCondition;
@@ -516,7 +653,7 @@
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
             void toXML(std::ostream&, uint32_t tabs) const override;
             Quantifier getQuantifier() const override { return Quantifier::A; }
-            Path getPath() const override             { return Path::G; } 
+            Path getPath() const override             { return Path::G; }
             uint32_t distance(DistanceContext& context) const override;
             Result evaluate(const EvaluationContext& context) override;
             Result evalAndSet(const EvaluationContext& context) override;
@@ -524,7 +661,7 @@
         private:
             std::string op() const override;
         };
-        
+
         class AFCondition : public SimpleQuantifierCondition {
         public:
             using SimpleQuantifierCondition::SimpleQuantifierCondition;
@@ -534,7 +671,7 @@
             Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
             void toXML(std::ostream&, uint32_t tabs) const override;
             Quantifier getQuantifier() const override { return Quantifier::A; }
-            Path getPath() const override             { return Path::F; }            
+            Path getPath() const override             { return Path::F; }
             uint32_t distance(DistanceContext& context) const override;
             Result evaluate(const EvaluationContext& context) override;
             Result evalAndSet(const EvaluationContext& context) override;
@@ -542,8 +679,8 @@
             virtual bool isLoopSensitive() const override { return true; }
         private:
             std::string op() const override;
-        };     
-        
+        };
+
         class UntilCondition : public QuantifierCondition {
         public:
             UntilCondition(const Condition_ptr cond1, const Condition_ptr cond2) {
@@ -554,50 +691,59 @@
             int formulaSize() const override{
                 return _cond1->formulaSize() + _cond2->formulaSize() + 1;
             }
-            
+
             void analyze(AnalysisContext& context) override;