Merge lp:~verifypn-maintainers/verifypn/interval_tar into lp:verifypn

[Peter Gjøl Jensen]

 - Implements TAR w/o z3, but using a simple integer inference engine for Hoare logic.
 - Replaces LP-Solve with GLPK, reduces computation-time and memory overhead
 - Implements new global properties, translated into CTL formulae.

Passes MCC'19 models, needs manual validation.

[lp:~verifypn-maintainers/verifypn/interval_tar]

353. By Peter G. Jensen <email address hidden> on 2020-07-02

Merged in trunk

354. By Peter G. Jensen <email address hidden> on 2020-07-03

added simple test-script and test models

355. By Peter G. Jensen <email address hidden> on 2020-07-03

inhibitor arcs are not yet handled by TAR solver, so return error if used with TAR

356. By Peter G. Jensen <email address hidden> on 2020-07-06

fixed handling of inhibitor

357. By Peter G. Jensen <email address hidden> on 2020-07-06

removing unused glpk import from STSolver

358. By Peter G. Jensen <email address hidden> on 2020-07-06

another missing inhib check

359. By <email address hidden> on 2020-07-08

allowed compilation for Mac

360. By <email address hidden> on 2020-07-08

updated readme as TAR is now possible for all platforms

361. By Kenneth Yrke Jørgensen on 2020-07-09

Updated argeument for cross compile glpk for windows

362. By Kenneth Yrke Jørgensen on 2020-08-18

Updated readme with info for cross-compile

363. By Kenneth Yrke Jørgensen on 2020-09-11

Updated readme

364. By <email address hidden> on 2020-09-11

updated README with compilation instructions for mac

[Jiri Srba (srba)]

It now compiles for all three platforms!

review: Approve

=== modified file '.bzrignore'
--- .bzrignore	2018-03-06 02:18:12 +0000
+++ .bzrignore	2020-09-11 14:21:20 +0000
@@ -2,10 +2,12 @@
 *.creator
 *.files
 *.includes
-verifypn-experimental-linux64
 *.user
-verifypn-linux64
-verifypn-osx64
 nbproject/
 cmake-build-*
-.idea/
 \ No newline at end of file
+.idea/
+src/PetriEngine/PQL/PQLQueryParser.parser.cpp
+src/PetriEngine/PQL/PQLQueryParser.parser.hpp
+src/PetriEngine/PQL/PQLQueryTokens.lexer.cpp
+build/
+
 
=== modified file 'CMakeLists.txt'
--- CMakeLists.txt	2018-06-12 16:18:51 +0000
+++ CMakeLists.txt	2020-09-11 14:21:20 +0000
@@ -1,46 +1,105 @@
-cmake_minimum_required(VERSION 2.8.4)
-project(verifypn)
+cmake_minimum_required(VERSION 3.9)
+cmake_policy(SET CMP0048 NEW)
+cmake_policy(SET CMP0069 NEW)
+
+set(CMAKE_CXX_STANDARD 17)
+if (NOT CMAKE_BUILD_TYPE)
+        set(CMAKE_BUILD_TYPE Release)
+endif (NOT CMAKE_BUILD_TYPE)
+
+if (CMAKE_BUILD_TYPE MATCHES Release)
+    if (NOT APPLE)
+    	set(CMAKE_INTERPROCEDURAL_OPTIMIZATION TRUE)
+    endif ()
+endif ()
+set(CMAKE_POSITION_INDEPENDENT_CODE ON)
+
+
+set(VERIFYPN_VERSION 3.0.1)
+add_compile_definitions(VERIFYPN_VERSION=\"${VERIFYPN_VERSION}\")
+
+project(verifypn VERSION ${VERIFYPN_VERSION} LANGUAGES CXX C)
+
+option(VERIFYPN_Static "Link libraries statically" ON)
+option(VERIFYPN_MC_Simplification "Enables multicore simplification, incompatible with static linking" OFF)
+option(VERIFYPN_GetDependencies "Fetch external dependencies from web." ON)
+
+
+if (VERIFYPN_Static)
+    set(BUILD_SHARED_LIBS OFF)
+    if (VERIFYPN_MC_Simplification)
+        message( FATAL_ERROR "Multicore Simplification is not compatible with static linking" )
+    endif(VERIFYPN_MC_Simplification)
+    if (NOT APPLE)
+        set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -static")
+    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)
+    add_compile_definitions(VERIFYPN_MC_Simplification)
+endif(VERIFYPN_MC_Simplification)
 
 if (UNIX AND NOT APPLE)
-    if (CMAKE_SIZEOF_VOID_P EQUAL 8) # is system 64-bit?
-        set(ARCH_TYPE "linux64")
-        set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fPIC -flto -march=x86-64 -std=c++14  -m64 -I.")
-        set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -flto=4 -march=x86-64 -std=c++14 -m64 -static -static-libgcc -static-libstdc++")
-    else()
-        set(ARCH_TYPE "linux32")
-    endif ()
+    set(ARCH_TYPE "linux64")
 elseif(APPLE)
-    if (CMAKE_SIZEOF_VOID_P EQUAL 8) # is system 64-bit?
-        set(ARCH_TYPE "osx64")
-        set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mmacosx-version-min=10.7 -std=c++14  -m64 -I. -stdlib=libc++")
-        set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -dynamic -mmacosx-version-min=10.7 -std=c++14 -m64 -stdlib=libc++ -lc++")
-    else()
-        set(ARCH_TYPE "osx32")
-    endif ()
+    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 ")
 else()
-    if (CMAKE_CL_64)
-        set(ARCH_TYPE "win64")
-    else()
-        set(ARCH_TYPE "win32")
-    endif()
+    set(ARCH_TYPE "win64")
 endif ()
 
-set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -Wall -pedantic-errors -O2 -DNDEBUG")
-set(CMAKE_CXX_FLAGS_DEBUG  "${CMAKE_CXX_FLAGS_DEBUG} -g")
-
-set(CMAKE_EXE_LINKER_FLAGS_RELEASE "${CMAKE_EXE_LINKER_FLAGS_RELEASE} -O2 -DNDEBUG")
-set(CMAKE_EXE_LINKER_FLAGS_DEBUG "${CMAKE_EXE_LINKER_FLAGS_DEBUG} -g")
-
-include_directories(PUBLIC .)
-
-file(GLOB verifypn_SRC
-        "*.h"
-        "*.cpp"
-        "**/*.cpp"
-        "**/*.h"
-        "**/**/*.cpp"
-        "**/**/*.h"
-)
-
-add_executable(verifypn ${verifypn_SRC})
-target_link_libraries(verifypn ${CMAKE_SOURCE_DIR}/lpsolve/liblpsolve55-${ARCH_TYPE}.a)
+set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -Wall -pedantic-errors -O3 -DNDEBUG")
+
+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")
+endif()
+
+set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
+set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
+set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
+
+if (VERIFYPN_GetDependencies)
+    # setup for external imports
+    include(ExternalProject)
+    set(EXTERNAL_INSTALL_LOCATION ${CMAKE_BINARY_DIR}/external)
+
+    ExternalProject_add(ptrie-ext
+        GIT_REPOSITORY https://github.com/petergjoel/ptrie
+        GIT_TAG 230b3640bfbe2ed5befdafbaf17bd3804231b50f
+        CMAKE_ARGS -DCMAKE_INSTALL_PREFIX=${EXTERNAL_INSTALL_LOCATION} -DPTRIE_BuildTest=OFF -DCMAKE_BUILD_TYPE=Release
+    )
+    ExternalProject_add(rapidxml-ext
+        URL https://downloads.sourceforge.net/project/rapidxml/rapidxml/rapidxml%201.13/rapidxml-1.13.zip
+        URL_HASH SHA512=6c10583e6631ccdb0217d0a5381172cb4c1046226de6ef1acf398d85e81d145228e14c3016aefcd7b70a1db8631505b048d8b4f5d4b0dbf1811d2482eefdd265
+        BUILD_COMMAND ""
+        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 (WIN32) #If windows 32 or 64 
+      set(GLPK_CFLAGS "-D __WOE__ -O3" )
+    else(WIN32)
+      set(GLPK_CFLAGS "-O3" )
+    endif(WIN32)
+    ExternalProject_add(glpk-ext
+        URL https://ftp.gnu.org/gnu/glpk/glpk-4.65.tar.gz
+        URL_HASH SHA512=997e8e599ff1718a08c66b86eadd0e01f4644899f1e95920f8ae91d66b4d8361021766b346845f4dcbcfe667b41ab72ea3d377017a0ebf85d7ece091cfd81375
+	CONFIGURE_COMMAND CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} <SOURCE_DIR>/configure --enable-shared=no --prefix=${EXTERNAL_INSTALL_LOCATION} CFLAGS=${GLPK_CFLAGS}
+	BUILD_COMMAND make
+        INSTALL_COMMAND make install
+        PATCH_COMMAND patch -p1 < ${PROJECT_SOURCE_DIR}/glpk-warning.patch
+    )
+
+    link_directories(${EXTERNAL_INSTALL_LOCATION}/lib)
+    link_directories(${EXTERNAL_INSTALL_LOCATION}/lib64)
+
+    # we can now include external libraries
+    include_directories(${EXTERNAL_INSTALL_LOCATION}/include)
+endif (VERIFYPN_GetDependencies)
+include_directories(include)
+
+add_subdirectory(${CMAKE_SOURCE_DIR}/src/)
 
=== removed directory 'CTL'
=== removed directory 'CTL/Algorithm'
=== removed file 'CTL/Algorithm/AlgorithmTypes.h'
=== removed file 'CTL/Algorithm/CertainZeroFPA.cpp'
=== removed file 'CTL/Algorithm/CertainZeroFPA.h'
=== removed file 'CTL/Algorithm/FixedPointAlgorithm.cpp'
=== removed file 'CTL/Algorithm/FixedPointAlgorithm.h'
=== removed file 'CTL/Algorithm/LocalFPA.cpp'
=== removed file 'CTL/Algorithm/LocalFPA.h'
=== removed file 'CTL/CTLEngine.cpp'
=== removed file 'CTL/CTLEngine.h'
=== removed file 'CTL/CTLResult.h'
=== removed directory 'CTL/DependencyGraph'
=== removed file 'CTL/DependencyGraph/BasicDependencyGraph.h'
=== removed file 'CTL/DependencyGraph/Configuration.cpp'
=== removed file 'CTL/DependencyGraph/Configuration.h'
=== removed file 'CTL/DependencyGraph/Edge.h'
=== removed file 'CTL/DependencyGraph/assignment.h'
=== removed directory 'CTL/PetriNets'
=== removed file 'CTL/PetriNets/OnTheFlyDG.cpp'
=== removed file 'CTL/PetriNets/OnTheFlyDG.h'
=== removed file 'CTL/PetriNets/PetriConfig.h'
=== removed directory 'CTL/SearchStrategy'
=== removed file 'CTL/SearchStrategy/BFSSearch.h'
=== removed file 'CTL/SearchStrategy/DFSSearch.h'
=== removed file 'CTL/SearchStrategy/HeuristicSearch.cpp'
=== removed file 'CTL/SearchStrategy/HeuristicSearch.h'
=== removed file 'CTL/SearchStrategy/RDFSSearch.cpp'
=== removed file 'CTL/SearchStrategy/RDFSSearch.h'
=== removed file 'CTL/SearchStrategy/SearchStrategy.cpp'
=== removed file 'CTL/SearchStrategy/SearchStrategy.h'
=== removed file 'CTL/Stopwatch.h'
=== removed directory 'PetriEngine'
=== removed file 'PetriEngine/AbstractPetriNetBuilder.h'
=== removed directory 'PetriEngine/Colored'
=== removed file 'PetriEngine/Colored/ColoredNetStructures.h'
=== removed file 'PetriEngine/Colored/ColoredPetriNetBuilder.cpp'
=== removed file 'PetriEngine/Colored/ColoredPetriNetBuilder.h'
=== removed file 'PetriEngine/Colored/Colors.cpp'
=== removed file 'PetriEngine/Colored/Colors.h'
=== removed file 'PetriEngine/Colored/Expressions.h'
=== removed file 'PetriEngine/Colored/Multiset.cpp'
=== removed file 'PetriEngine/Colored/Multiset.h'
=== removed file 'PetriEngine/NetStructures.h'
=== removed directory 'PetriEngine/PQL'
=== removed file 'PetriEngine/PQL/Contexts.h'
=== removed file 'PetriEngine/PQL/Expressions.cpp'
=== removed file 'PetriEngine/PQL/Expressions.h'
=== removed file 'PetriEngine/PQL/PQL.cpp'
=== removed file 'PetriEngine/PQL/PQL.h'
=== removed file 'PetriEngine/PQL/PQLParser.h'
=== removed file 'PetriEngine/PQL/PQLQueryParser.parser.cpp'
=== removed file 'PetriEngine/PQL/PQLQueryParser.parser.hpp'
=== removed file 'PetriEngine/PQL/PQLQueryParser.y'
=== removed file 'PetriEngine/PQL/PQLQueryTokens.l'
=== removed file 'PetriEngine/PQL/PQLQueryTokens.lexer.cpp'
=== removed file 'PetriEngine/PetriNet.cpp'
=== removed file 'PetriEngine/PetriNet.h'
=== removed file 'PetriEngine/PetriNetBuilder.cpp'
=== removed file 'PetriEngine/PetriNetBuilder.h'
=== removed directory 'PetriEngine/Reachability'
=== removed file 'PetriEngine/Reachability/ReachabilityResult.h'
=== removed file 'PetriEngine/Reachability/ReachabilitySearch.cpp'
=== removed file 'PetriEngine/Reachability/ReachabilitySearch.h'
=== removed file 'PetriEngine/Reachability/ResultPrinter.cpp'
=== removed file 'PetriEngine/Reachability/TARReachability.cpp'
=== removed file 'PetriEngine/Reachability/TARReachability.h'
=== removed file 'PetriEngine/Reducer.cpp'
=== removed file 'PetriEngine/Reducer.h'
=== removed file 'PetriEngine/ReducingSuccessorGenerator.cpp'
=== removed file 'PetriEngine/ReducingSuccessorGenerator.h'
=== removed file 'PetriEngine/STSolver.cpp'
=== removed file 'PetriEngine/STSolver.h'
=== removed directory 'PetriEngine/Simplification'
=== removed file 'PetriEngine/Simplification/LPCache.cpp'
=== removed file 'PetriEngine/Simplification/LPCache.h'
=== removed file 'PetriEngine/Simplification/LinearProgram.cpp'
=== removed file 'PetriEngine/Simplification/LinearProgram.h'
=== removed file 'PetriEngine/Simplification/LinearPrograms.h'
=== removed file 'PetriEngine/Simplification/Member.h'
=== removed file 'PetriEngine/Simplification/MurmurHash2.cpp'
=== removed file 'PetriEngine/Simplification/MurmurHash2.h'
=== removed file 'PetriEngine/Simplification/Retval.h'
=== removed file 'PetriEngine/Simplification/Vector.cpp'
=== removed file 'PetriEngine/Simplification/Vector.h'
=== removed directory 'PetriEngine/Structures'
=== removed file 'PetriEngine/Structures/AlignedEncoder.cpp'
=== removed file 'PetriEngine/Structures/AlignedEncoder.h'
=== removed file 'PetriEngine/Structures/BitField.h'
=== removed file 'PetriEngine/Structures/Queue.cpp'
=== removed file 'PetriEngine/Structures/Queue.h'
=== removed file 'PetriEngine/Structures/State.h'
=== removed file 'PetriEngine/Structures/StateSet.h'
=== removed file 'PetriEngine/Structures/binarywrapper.cpp'
=== removed file 'PetriEngine/Structures/binarywrapper.h'
=== removed file 'PetriEngine/Structures/light_deque.h'
=== removed file 'PetriEngine/Structures/linked_bucket.h'
=== removed file 'PetriEngine/Structures/ptrie.h'
=== removed file 'PetriEngine/Structures/ptrie_map.h'
=== removed file 'PetriEngine/Structures/ptrie_stable.h'
=== removed file 'PetriEngine/SuccessorGenerator.cpp'
=== removed file 'PetriEngine/SuccessorGenerator.h'
=== removed directory 'PetriEngine/TAR'
=== removed file 'PetriEngine/TAR/AntiChain.h'
=== removed file 'PetriEngine/TAR/Renamer.h'
=== removed file 'PetriEngine/TAR/TARAutomata.h'
=== removed file 'PetriEngine/errorcodes.h'
=== removed file 'PetriEngine/options.h'
=== removed directory 'PetriParse'
=== removed file 'PetriParse/PNMLParser.cpp'
=== removed file 'PetriParse/PNMLParser.h'
=== removed file 'PetriParse/QueryBinaryParser.cpp'
=== removed file 'PetriParse/QueryBinaryParser.h'
=== removed file 'PetriParse/QueryParser.h'
=== removed file 'PetriParse/QueryXMLParser.cpp'
=== removed file 'PetriParse/QueryXMLParser.h'
=== removed directory 'PetriParse/rapidxml'
=== removed file 'PetriParse/rapidxml/license.txt'
=== removed file 'PetriParse/rapidxml/manual.html'
=== removed file 'PetriParse/rapidxml/rapidxml.hpp'
=== removed file 'PetriParse/rapidxml/rapidxml_iterators.hpp'
=== removed file 'PetriParse/rapidxml/rapidxml_print.hpp'
=== removed file 'PetriParse/rapidxml/rapidxml_utils.hpp'
=== renamed file 'README.mkd' => 'README.md'
--- README.mkd	2014-04-21 18:12:28 +0000
+++ README.md	2020-09-11 14:21:20 +0000
@@ -1,58 +1,71 @@
-VerifyPN
-========
+# VerifyPN
 VerifyPN is based on [PeTe](https://github.com/jopsen/PeTe) and aims to provide
 a fast untimed engine for TAPAAL.
 
-Building VerifyPN
------------------
-VerifyPN is build using a simple makefile, depending on you platform and
-configuration of it, you might need to modify the makefile in order link
-correctly against following dependencies: 
-
-  * GNU Bison (>= 2.4)
-  * flex (>= 2.5)
-  * lp_solve (>= 5.5)
-
-For simplicity, compiled output form GNU Bison, flex and binaries of lpsolve
-are included in the source tree.
-
-To cross compile for Windows on linux install `g++-mingw-w64` and run
-`make -f makefile.win32` for 32 bit version, and `make -f makefile.win64` for
-64 bit version.
-
-**Warning** both `verifypn-win32` and `verifypn-win64` are accompanied by a dll
-called `lpsolve55.dll`, however, this is **not** the same dll for both 32 and 64
-bit versions. Unfortunately, we cannot rename the dll either, so either we need
-to build with MSVC or accept this pain, and distribute Windows 32 and 64 bit
-versions in different folders, and watch out of this during deployment.
-
-To cross compile for 32 bit linux you need to run install `gcc-multilib`,
-`g++-multilib` and probably a few others.
-
-To build on OS X run `make -f makefile.osx32` or `make -f makefile.osx64`,
-as cross compilers for OS X are not readily available (e.g. in package manager)
-cross compilation for OS X is not supported.
-
-Testing
--------
-VerifyPN builds can be validated with `make check` (for the respective makefiles).
-This executes a simple script that iterates over the files in the Tests/ folder,
-the tested Petri net is <test-name>-<exit-code>-<strategy>.xml and queries for
-this network is in <test-name>-<exit-code>-<strategy>.xml.q, here <test-name> is
-an identifier for the test, <exit-code> is the exit code expected by VerifyPN when
-given the Petri net and query. <strategy> is the search strategy used for the
-verification, `All` if all strategies should be tested.
-
-License
--------
-VerifyPN is available under the terms of the GNU GPL versoin 3 or
+## License
+VerifyPN is available under the terms of the GNU GPL version 3 or
 (at your option) any later version.
 If this license doesn't suit you're welcome to contact us, and purpose an
 alternative license.
 
-Authors
--------
-  * Jonas Finnemann Jensen
-  * Thomas Søndersø Nielsen
-  * Lars Kærlund Østergaard
-  * Jiri Srba
+## Compilation
+Requirements for compilation
+```
+cmake >= 3.9
+flex >= 2.6.4
+bison >= 3.0.5
+gmp-static (required only for model checking competition)
+
+sudo apt update
+sudo apt install build-essential cmake flex bison brz
+
+```
+
+The four distributions of VerifyPN can be compiled as follows
+### Linux64 and OSX64
+```
+bzr branch lp:verifypn
+mkdir build && cd  build
+cmake .. -DVERIFYPN_Static=ON -DVERIFYPN_MC_Simplification=OFF 
+
+#For mac, one need to enforce that we use the GCC compiler using:
+export CC=gcc-9
+export CXX=g++-9
+#and point to the correct version of flex and bison by adding
+#-DBISON_EXECUTABLE=/usr/local/opt/bison/bin/bison -DFLEX_EXECUTABLE=/usr/local/opt/flex/bin/flex 
+#to cmake call
+
+```
+
+### Windows 64 cross-compilation with minGW
+Install cross-compiler and libs
+
+```
+sudo apt install mingw-w64-x86-64-dev mingw-w64-tools g++-mingw-w64-x86-64
+sudo apt install wine wine-binfmt #Needed to run tests compile
+```
+
+To build
+
+```
+mkdir build-win && cd  build-win
+cmake .. -DVERIFYPN_Static=ON -DVERIFYPN_MC_Simplification=OFF -DCMAKE_TOOLCHAIN_FILE=../toolchain-x86_64-w64-mingw32.cmake
+make
+```
+
+### Linux64 - Model Checking Competition
+```
+mkdir build
+cd  build
+cmake .. -DVERIFYPN_Static=OFF -DVERIFYPN_MC_Simplification=ON 
+make
+```
+
+### Mac 64 compilation
+```
+mkdir build
+cd build
+cmake -DVERIFYPN_MC_Simplification=OFF  -DBISON_EXECUTABLE=/usr/local/opt/bison/bin/bison -DFLEX_EXECUTABLE=/usr/local/opt/flex/bin/flex -DCMAKE_C_COMPILER=/usr/local/bin/gcc-9 -DCMAKE_CXX_COMPILER=/usr/local/bin/g++-9 ..
+make
+```
+
 
=== removed file 'VerifyPN.cpp'
=== added file 'glpk-warning.patch'
--- glpk-warning.patch	1970-01-01 00:00:00 +0000
+++ glpk-warning.patch	2020-09-11 14:21:20 +0000
@@ -0,0 +1,10 @@
+--- a/src/draft/glpios03.c
++++ b/src/draft/glpios03.c
+@@ -925,7 +925,6 @@
+ #if 0 /* 20/I-2018 */
+          xprintf("WARNING: LONG-STEP DUAL SIMPLEX WILL BE USED\n");
+ #else
+-         xprintf("Long-step dual simplex will be used\n");
+ #endif
+ #endif
+       /* on entry to the B&B driver it is assumed that the active list
 
=== added directory 'include'
=== added directory 'include/CTL'
=== added directory 'include/CTL/Algorithm'
=== added file 'include/CTL/Algorithm/AlgorithmTypes.h'
--- include/CTL/Algorithm/AlgorithmTypes.h	1970-01-01 00:00:00 +0000
+++ include/CTL/Algorithm/AlgorithmTypes.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,10 @@
+#ifndef ALGORITHMTYPES_H
+#define ALGORITHMTYPES_H
+
+namespace CTL {
+
+enum CTLAlgorithmType{
+    Local = 0, CZero = 1
+};
+}
+#endif // ALGORITHMTYPES_H
 
=== added file 'include/CTL/Algorithm/CertainZeroFPA.h'
--- include/CTL/Algorithm/CertainZeroFPA.h	1970-01-01 00:00:00 +0000
+++ include/CTL/Algorithm/CertainZeroFPA.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,36 @@
+#ifndef CERTAINZEROFPA_H
+#define CERTAINZEROFPA_H
+
+#include "FixedPointAlgorithm.h"
+#include "CTL/DependencyGraph/Edge.h"
+#include "CTL/DependencyGraph/Configuration.h"
+#include "PetriEngine/Reachability/ReachabilitySearch.h"
+#include "CTL/SearchStrategy/SearchStrategy.h"
+
+
+namespace Algorithm {
+
+class CertainZeroFPA : public FixedPointAlgorithm
+{
+public:
+    CertainZeroFPA(PetriEngine::Reachability::Strategy type) : FixedPointAlgorithm(type)
+    {
+    }
+    virtual ~CertainZeroFPA()
+    {
+    }
+    virtual bool search(DependencyGraph::BasicDependencyGraph &t_graph) override;
+protected:
+
+    DependencyGraph::BasicDependencyGraph *graph;
+    DependencyGraph::Configuration* vertex;
+    
+    void checkEdge(DependencyGraph::Edge* e, bool only_assign = false);
+    void finalAssign(DependencyGraph::Configuration *c, DependencyGraph::Assignment a);
+    void explore(DependencyGraph::Configuration *c);
+    void addDependency(DependencyGraph::Edge *e,
+                          DependencyGraph::Configuration *target);
+
+};
+}
+#endif // CERTAINZEROFPA_H
 
=== added file 'include/CTL/Algorithm/FixedPointAlgorithm.h'
--- include/CTL/Algorithm/FixedPointAlgorithm.h	1970-01-01 00:00:00 +0000
+++ include/CTL/Algorithm/FixedPointAlgorithm.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,32 @@
+#ifndef FIXEDPOINTALGORITHM_H
+#define FIXEDPOINTALGORITHM_H
+
+#include "CTL/DependencyGraph/BasicDependencyGraph.h"
+#include "CTL/SearchStrategy/SearchStrategy.h"
+#include "PetriEngine/Reachability/ReachabilitySearch.h"
+
+namespace Algorithm {
+
+class FixedPointAlgorithm {
+public:
+    virtual bool search(DependencyGraph::BasicDependencyGraph &graph) =0;
+    FixedPointAlgorithm(PetriEngine::Reachability::Strategy type);
+    virtual ~FixedPointAlgorithm(){}
+
+    size_t processedEdges() const { return _processedEdges; }
+    size_t processedNegationEdges() const { return _processedNegationEdges; }
+    size_t exploredConfigurations() const { return _exploredConfigurations; }
+    size_t numberOfEdges() const { return _numberOfEdges; }
+protected:
+    std::shared_ptr<SearchStrategy::SearchStrategy> strategy;
+    //total number of processed edges
+    size_t _processedEdges = 0;
+    //total number of processed negation edges
+    size_t _processedNegationEdges = 0;
+    //number of explored configurations
+    size_t _exploredConfigurations = 0;
+    //total number of edges found when computing successors
+    size_t _numberOfEdges = 0;
+};
+}
+#endif // FIXEDPOINTALGORITHM_H
 
=== added file 'include/CTL/Algorithm/LocalFPA.h'
--- include/CTL/Algorithm/LocalFPA.h	1970-01-01 00:00:00 +0000
+++ include/CTL/Algorithm/LocalFPA.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,29 @@
+#ifndef LOCALFPA_H
+#define LOCALFPA_H
+
+#include "FixedPointAlgorithm.h"
+#include "../DependencyGraph/Configuration.h"
+
+namespace Algorithm {
+
+class LocalFPA : public FixedPointAlgorithm
+{
+
+    // FixedPointAlgorithm interface
+public:
+    LocalFPA(PetriEngine::Reachability::Strategy type) : FixedPointAlgorithm(type)
+    {
+    }
+    virtual ~LocalFPA (){}
+    virtual bool search(DependencyGraph::BasicDependencyGraph &graph);
+
+protected:
+    DependencyGraph::BasicDependencyGraph *graph;
+
+    void finalAssign(DependencyGraph::Configuration *c, DependencyGraph::Assignment a);
+    void explore(DependencyGraph::Configuration *c);
+    void addDependency(DependencyGraph::Edge *e,
+                          DependencyGraph::Configuration *target);
+};
+}
+#endif // LOCALFPA_H
 
=== added file 'include/CTL/CTLEngine.h'
--- include/CTL/CTLEngine.h	1970-01-01 00:00:00 +0000
+++ include/CTL/CTLEngine.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,25 @@
+#ifndef CTLENGINE_H
+#define CTLENGINE_H
+
+#include "../PetriEngine/errorcodes.h"
+#include "../PetriEngine/PetriNet.h"
+#include "../PetriEngine/Reachability/ReachabilitySearch.h"
+
+#include "Algorithm/AlgorithmTypes.h"
+#include "../PetriEngine/PQL/PQL.h"
+
+#include <set>
+
+ReturnValue CTLMain(PetriEngine::PetriNet* net,
+                    CTL::CTLAlgorithmType algorithmtype,
+                    PetriEngine::Reachability::Strategy strategytype,
+                    bool gamemode,
+                    bool printstatistics,
+                    bool mccoutput,
+                    bool partial_order,
+                    const std::vector<std::string>& querynames,
+                    const std::vector<std::shared_ptr<PetriEngine::PQL::Condition>>& reducedQueries,
+                    const std::vector<size_t>& ids,
+                    options_t& options);
+
+#endif // CTLENGINE_H
 
=== added file 'include/CTL/CTLResult.h'
--- include/CTL/CTLResult.h	1970-01-01 00:00:00 +0000
+++ include/CTL/CTLResult.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,33 @@
+#ifndef CTLRESULT_H
+#define CTLRESULT_H
+
+#include "../PetriEngine/errorcodes.h"
+#include "../PetriEngine/PQL/PQL.h"
+
+#include <string>
+
+struct CTLResult {
+    CTLResult(const PetriEngine::PQL::Condition_ptr& qry){
+        query = qry;
+    }
+
+    PetriEngine::PQL::Condition_ptr query;
+    bool result;
+
+    double duration = 0;
+    size_t numberOfMarkings = 0;
+    size_t numberOfConfigurations = 0;
+    size_t processedEdges = 0;
+    size_t processedNegationEdges = 0;
+    size_t exploredConfigurations = 0;
+    size_t numberOfEdges = 0;
+#ifdef VERIFYPNDIST
+    size_t numberOfRoundsComputingDistance = 0;
+    size_t numberOfTokensReceived = 0;
+    size_t numberOfRequestsReceived = 0;
+    size_t numberOfAnswersReceived = 0;
+    size_t numberOfMessagesSend = 0;
+#endif
+};
+
+#endif // CTLRESULT_H
 
=== added directory 'include/CTL/DependencyGraph'
=== added file 'include/CTL/DependencyGraph/BasicDependencyGraph.h'
--- include/CTL/DependencyGraph/BasicDependencyGraph.h	1970-01-01 00:00:00 +0000
+++ include/CTL/DependencyGraph/BasicDependencyGraph.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,23 @@
+#ifndef ABSTRACTDEPENDENCYGRAPH_H
+#define ABSTRACTDEPENDENCYGRAPH_H
+
+#include <cstddef>
+#include <vector>
+#include <cstdint>
+
+namespace DependencyGraph {
+
+class Configuration;
+class Edge;
+
+class BasicDependencyGraph {
+
+public:
+    virtual std::vector<Edge*> successors(Configuration *c) =0;
+    virtual Configuration *initialConfiguration() =0;
+    virtual void release(Edge* e) = 0;
+    virtual void cleanUp() =0;
+};
+
+}
+#endif // ABSTRACTDEPENDENCYGRAPH_H
 
=== added file 'include/CTL/DependencyGraph/Configuration.h'
--- include/CTL/DependencyGraph/Configuration.h	1970-01-01 00:00:00 +0000
+++ include/CTL/DependencyGraph/Configuration.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,40 @@
+#ifndef CONFIGURATION_H
+#define CONFIGURATION_H
+
+#include "Edge.h"
+
+#include <string>
+#include <cstdio>
+#include <iostream>
+#include <vector>
+
+namespace DependencyGraph {
+
+class Edge;
+
+enum Assignment {
+    ONE = 1, UNKNOWN = 0, ZERO = -1, CZERO = -2
+};
+
+class Configuration
+{
+    uint32_t distance = 0;
+public:
+
+    uint32_t getDistance() const { return distance; }
+    void setDistance(uint32_t value) { distance = value; }
+
+    Configuration() {}
+    virtual ~Configuration();
+
+    bool isDone() const { return assignment == ONE || assignment == CZERO; }
+
+    uint32_t owner = 0;
+    uint32_t nsuccs = 0;
+    std::vector<Edge*> dependency_set;
+    Assignment assignment = UNKNOWN;
+};
+
+
+}
+#endif // CONFIGURATION_H
 
=== added file 'include/CTL/DependencyGraph/Edge.h'
--- include/CTL/DependencyGraph/Edge.h	1970-01-01 00:00:00 +0000
+++ include/CTL/DependencyGraph/Edge.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,36 @@
+#ifndef EDGE_H
+#define EDGE_H
+
+#include <cstdio>
+#include <vector>
+#include <string>
+#include <algorithm>
+#include <cassert>
+
+namespace DependencyGraph {
+
+class Configuration;
+
+class Edge {
+    typedef std::vector<Configuration*> container;
+public:
+    Edge(){}
+    Edge(Configuration &t_source) : source(&t_source) {}
+
+    void addTarget(Configuration* conf)
+    {
+        assert(conf);
+        targets.push_back(conf);
+    }
+    
+    Configuration* source;
+    container targets;
+    uint8_t status = 0;
+    bool processed = false;
+    bool is_negated = false;
+    int32_t refcnt = 0;
+    bool handled = false;
+    uint32_t weight = 0;
+};
+}
+#endif // EDGE_H
 
=== added file 'include/CTL/DependencyGraph/assignment.h'
--- include/CTL/DependencyGraph/assignment.h	1970-01-01 00:00:00 +0000
+++ include/CTL/DependencyGraph/assignment.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,11 @@
+#ifndef ASSIGNMENT_H
+#define ASSIGNMENT_H
+
+namespace DependencyGraph {
+
+enum Assignment {
+    ONE = 1, UNKNOWN = 0, ZERO = -1, CZERO = -2
+};
+}
+
+#endif // ASSIGNMENT_H
 
=== added directory 'include/CTL/PetriNets'
=== added file 'include/CTL/PetriNets/OnTheFlyDG.h'
--- include/CTL/PetriNets/OnTheFlyDG.h	1970-01-01 00:00:00 +0000
+++ include/CTL/PetriNets/OnTheFlyDG.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,115 @@
+#ifndef ONTHEFLYDG_H
+#define ONTHEFLYDG_H
+
+#include <functional>
+#include <stack>
+#include <ptrie/ptrie_map.h>
+
+#include "CTL/DependencyGraph/BasicDependencyGraph.h"
+#include "CTL/DependencyGraph/Configuration.h"
+#include "CTL/DependencyGraph/Edge.h"
+#include "PetriConfig.h"
+#include "PetriParse/PNMLParser.h"
+#include "PetriEngine/PQL/PQL.h"
+#include "PetriEngine/Structures/AlignedEncoder.h"
+#include "PetriEngine/Structures/linked_bucket.h"
+#include "PetriEngine/ReducingSuccessorGenerator.h"
+
+namespace PetriNets {
+class OnTheFlyDG : public DependencyGraph::BasicDependencyGraph
+{
+public:
+    using Condition = PetriEngine::PQL::Condition;
+    using Condition_ptr = PetriEngine::PQL::Condition_ptr;
+    using Marking = PetriEngine::Structures::State;
+    OnTheFlyDG(PetriEngine::PetriNet *t_net, bool partial_order);
+
+    virtual ~OnTheFlyDG();
+
+    //Dependency graph interface
+    virtual std::vector<DependencyGraph::Edge*> successors(DependencyGraph::Configuration *c) override;
+    virtual DependencyGraph::Configuration *initialConfiguration() override;
+    virtual void cleanUp() override;
+    void setQuery(const Condition_ptr& query);
+
+    virtual void release(DependencyGraph::Edge* e) override;
+
+    size_t owner(Marking& marking, Condition* cond);
+    size_t owner(Marking& marking, const Condition_ptr& cond)
+    {
+        return owner(marking, cond.get());
+    }
+
+
+    //stats
+    size_t configurationCount() const;
+    size_t markingCount() const;
+    
+    Condition::Result initialEval();
+
+protected:
+
+    //initialized from constructor
+    AlignedEncoder encoder;
+    PetriEngine::PetriNet *net = nullptr;
+    PetriConfig* initial_config;
+    Marking working_marking;
+    Marking query_marking;
+    uint32_t n_transitions = 0;
+    uint32_t n_places = 0;
+    size_t _markingCount = 0;
+    size_t _configurationCount = 0;
+    //used after query is set
+    Condition_ptr query = nullptr;
+
+    Condition::Result fastEval(Condition* query, Marking* unfolded);
+    Condition::Result fastEval(const Condition_ptr& query, Marking* unfolded)
+    {
+        return fastEval(query.get(), unfolded);
+    }
+    void nextStates(Marking& t_marking, Condition*,
+    std::function<void ()> pre, 
+    std::function<bool (Marking&)> foreach, 
+    std::function<void ()> post);
+    template<typename T>
+    void dowork(T& gen, bool& first, 
+    std::function<void ()>& pre, 
+    std::function<bool (Marking&)>& foreach)
+    {
+        gen.prepare(&query_marking);
+
+        while(gen.next(working_marking)){
+            if(first) pre();
+            first = false;
+            if(!foreach(working_marking))
+            {
+                gen.reset();
+                break;
+            }
+        }
+    }
+    PetriConfig *createConfiguration(size_t marking, size_t own, Condition* query);
+    PetriConfig *createConfiguration(size_t marking, size_t own, const Condition_ptr& query)
+    {
+        return createConfiguration(marking, own, query.get());
+    }
+    size_t createMarking(Marking &marking);
+    void markingStats(const uint32_t* marking, size_t& sum, bool& allsame, uint32_t& val, uint32_t& active, uint32_t& last);
+    
+    DependencyGraph::Edge* newEdge(DependencyGraph::Configuration &t_source, uint32_t weight);
+
+    std::stack<DependencyGraph::Edge*> recycle;
+    ptrie::map<ptrie::uchar, std::vector<PetriConfig*> > trie;
+    linked_bucket_t<DependencyGraph::Edge,1024*10>* edge_alloc = nullptr;
+
+    // Problem  with linked bucket and complex constructor
+    linked_bucket_t<char[sizeof(PetriConfig)], 1024*1024>* conf_alloc = nullptr;
+    
+    PetriEngine::ReducingSuccessorGenerator _redgen;
+    bool _partial_order = false;
+
+};
+
+
+}
+#endif // ONTHEFLYDG_H
 
=== added file 'include/CTL/PetriNets/PetriConfig.h'
--- include/CTL/PetriNets/PetriConfig.h	1970-01-01 00:00:00 +0000
+++ include/CTL/PetriNets/PetriConfig.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,31 @@
+#ifndef PETRICONFIG_H
+#define PETRICONFIG_H
+
+#include "CTL/DependencyGraph/Configuration.h"
+#include "PetriEngine/PQL/PQL.h"
+
+#include <sstream>
+
+namespace PetriNets {
+
+class PetriConfig : public DependencyGraph::Configuration {
+
+public:
+    using Condition = PetriEngine::PQL::Condition;
+    PetriConfig() : 
+        DependencyGraph::Configuration(), marking(0), query(NULL) 
+    {}
+    
+    PetriConfig(size_t t_marking, Condition *t_query) :
+        DependencyGraph::Configuration(), marking(t_marking), query(t_query) {
+    }
+
+    virtual ~PetriConfig(){};
+
+    size_t marking;
+    Condition *query;
+
+};
+
+}
+#endif // PETRICONFIG_H
 
=== added directory 'include/CTL/SearchStrategy'
=== added file 'include/CTL/SearchStrategy/BFSSearch.h'
--- include/CTL/SearchStrategy/BFSSearch.h	1970-01-01 00:00:00 +0000
+++ include/CTL/SearchStrategy/BFSSearch.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,36 @@
+/* 
+ * File:   Encoder.h
+ * Author: Peter G. Jensen
+ *
+ * Created on March 7, 2018, 1:50 PM
+ */
+
+#ifndef BFSSEARCH_H
+#define BFSSEARCH_H
+#include <queue>
+#include "CTL/DependencyGraph/Edge.h"
+#include "SearchStrategy.h"
+
+namespace SearchStrategy {
+
+// A custom search strategy that should ensure as little overhead as possible
+// while running sequential computation.
+
+class BFSSearch : public SearchStrategy {
+
+protected:
+    size_t Wsize() const { return W.size(); };
+    void pushToW(DependencyGraph::Edge* edge) { W.push(edge); };
+    DependencyGraph::Edge* popFromW() 
+    {
+        auto e = W.front();
+        W.pop();
+        return e;
+    };    
+    std::queue<DependencyGraph::Edge*> W;
+};
+
+}   // end SearchStrategy
+
+#endif /* BFSSEARCH_H */
+
 
=== added file 'include/CTL/SearchStrategy/DFSSearch.h'
--- include/CTL/SearchStrategy/DFSSearch.h	1970-01-01 00:00:00 +0000
+++ include/CTL/SearchStrategy/DFSSearch.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,29 @@
+#ifndef DFSSEARCH_H
+#define DFSSEARCH_H
+
+#include <stack>
+#include "CTL/DependencyGraph/Edge.h"
+#include "SearchStrategy.h"
+
+namespace SearchStrategy {
+
+// A custom search strategy that should ensure as little overhead as possible
+// while running sequential computation.
+
+class DFSSearch : public SearchStrategy {
+
+protected:
+    size_t Wsize() const { return W.size(); };
+    void pushToW(DependencyGraph::Edge* edge) { W.push(edge); };
+    DependencyGraph::Edge* popFromW() 
+    {
+        auto e = W.top();
+        W.pop();
+        return e;
+    };
+    std::stack<DependencyGraph::Edge*> W;
+};
+
+}   // end SearchStrategy
+
+#endif // DFSSEARCH_H
 
=== added file 'include/CTL/SearchStrategy/HeuristicSearch.h'
--- include/CTL/SearchStrategy/HeuristicSearch.h	1970-01-01 00:00:00 +0000
+++ include/CTL/SearchStrategy/HeuristicSearch.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,32 @@
+/* 
+ * File:   Encoder.h
+ * Author: Peter G. Jensen
+ *
+ * Created on March 7, 2018, 1:51 PM
+ */
+
+#ifndef HEURISTICSEARCH_H
+#define HEURISTICSEARCH_H
+
+#include <vector>
+#include "CTL/DependencyGraph/Edge.h"
+#include "SearchStrategy.h"
+
+namespace SearchStrategy {
+
+// A custom search strategy that should ensure as little overhead as possible
+// while running sequential computation.
+
+class HeuristicSearch : public SearchStrategy {
+
+protected:
+    size_t Wsize() const;
+    void pushToW(DependencyGraph::Edge* edge);
+    DependencyGraph::Edge* popFromW();
+    std::vector<DependencyGraph::Edge*> W;
+};
+
+}   // end SearchStrategy
+
+#endif /* HEURISTICSEARCH_H */
+
 
=== added file 'include/CTL/SearchStrategy/RDFSSearch.h'
--- include/CTL/SearchStrategy/RDFSSearch.h	1970-01-01 00:00:00 +0000
+++ include/CTL/SearchStrategy/RDFSSearch.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,34 @@
+/* 
+ * File:   Encoder.h
+ * Author: Peter G. Jensen
+ *
+ * Created on March 7, 2018, 1:52 PM
+ */
+
+#ifndef RDFSSEARCH_H
+#define RDFSSEARCH_H
+
+#include <deque>
+#include "CTL/DependencyGraph/Edge.h"
+#include "SearchStrategy.h"
+
+namespace SearchStrategy {
+
+// A custom search strategy that should ensure as little overhead as possible
+// while running sequential computation.
+
+class RDFSSearch : public SearchStrategy {
+public:
+    void flush();
+protected:
+    size_t Wsize() const;
+    void pushToW(DependencyGraph::Edge* edge);
+    DependencyGraph::Edge* popFromW();
+    std::vector<DependencyGraph::Edge*> W;
+    size_t last_parent = 0;
+};
+
+}   // end SearchStrategy
+
+#endif /* RDFSSEARCH_H */
+
 
=== added file 'include/CTL/SearchStrategy/SearchStrategy.h'
--- include/CTL/SearchStrategy/SearchStrategy.h	1970-01-01 00:00:00 +0000
+++ include/CTL/SearchStrategy/SearchStrategy.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,56 @@
+#ifndef ISEARCHSTRATEGY_H
+#define ISEARCHSTRATEGY_H
+
+#include "CTL/DependencyGraph/Edge.h"
+#include <sstream>
+
+namespace SearchStrategy {
+
+struct Message {    
+    uint32_t sender;
+    uint32_t distance;
+    enum Type {HALT = 0, REQUEST = 1, ANSWER_ONE = 2, ANSWER_ZERO = 3} type;
+    DependencyGraph::Configuration *configuration;
+
+    Message() {}
+    Message(size_t sender, uint32_t distance, Type type, DependencyGraph::Configuration *configuration) :
+           sender(sender), distance(distance), type(type), configuration(configuration) {}
+
+    std::string ToString() {
+        std::stringstream ss;
+        ss << "Message from " << sender << ": ";
+        ss << (type == HALT ? "Halt" : type == REQUEST ? "Request" : type == ANSWER_ONE ? "Answer 1" : "Answer 0");
+        ss << configuration << "\n";
+        return ss.str();
+    }
+};
+
+
+class SearchStrategy
+{
+public:
+    virtual ~SearchStrategy() {};
+    bool empty() const;
+    void pushEdge(DependencyGraph::Edge *edge);
+    void pushDependency(DependencyGraph::Edge* edge);
+    void pushNegation(DependencyGraph::Edge *edge);
+    DependencyGraph::Edge* popEdge(bool saturate = false);
+    size_t size() const;
+//#ifdef VERIFYPNDIST
+    uint32_t maxDistance() const;
+    bool available() const;
+    void releaseNegationEdges(uint32_t );
+    bool trivialNegation();
+    virtual void flush() {};
+//#endif
+protected:
+    virtual size_t Wsize() const = 0;
+    virtual void pushToW(DependencyGraph::Edge* edge) = 0;
+    virtual DependencyGraph::Edge* popFromW() = 0;
+    
+    std::vector<DependencyGraph::Edge*> N;
+    std::vector<DependencyGraph::Edge*> D;
+};
+
+}
+#endif // SEARCHSTRATEGY_H
 
=== added file 'include/CTL/Stopwatch.h'
--- include/CTL/Stopwatch.h	1970-01-01 00:00:00 +0000
+++ include/CTL/Stopwatch.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,40 @@
+#ifndef STOPWATCH_H
+#define STOPWATCH_H
+
+#include <ctime>
+#include <sstream>
+
+using namespace std;
+
+class stopwatch {
+    bool _running = false;
+    clock_t _start;
+    clock_t _stop;
+
+public:
+    double started() const { return _start; }
+    double stopped() const { return _stop; }
+    bool running() const { return _running; }
+    void start() {
+        _running = true;
+        _start = clock();
+    }
+    void stop() {
+        _stop = clock();
+        _running = false;
+    }
+    double duration() const { return ( (double(_stop - _start))*1000)/CLOCKS_PER_SEC; }
+
+    ostream &operator<<(ostream &os){
+        os << duration() << " ms";
+        return os;
+    }
+
+    std::string toString(){
+        stringstream ss;
+        ss << this;
+        return ss.str();
+    }
+};
+
+#endif // STOPWATCH_H
 
=== added directory 'include/PetriEngine'
=== added file 'include/PetriEngine/AbstractPetriNetBuilder.h'
--- include/PetriEngine/AbstractPetriNetBuilder.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/AbstractPetriNetBuilder.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,114 @@
+/* PeTe - Petri Engine exTremE
+ * Copyright (C) 2011  Jonas Finnemann Jensen <[e-mail]>,
+ *                     Thomas Søndersø Nielsen <[e-mail]>,
+ *                     Lars Kærlund Østergaard <[e-mail]>,
+ *                     Peter Gjøl Jensen <[e-mail]>
+ * 
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ * 
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ * 
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+#ifndef ABSTRACTPETRINETBUILDER_H
+#define ABSTRACTPETRINETBUILDER_H
+
+#include <string>
+
+#include "PQL/PQL.h"
+#include "Colored/Multiset.h"
+#include "Colored/Expressions.h"
+
+namespace PetriEngine {
+
+    /** Abstract builder for petri nets */
+    class AbstractPetriNetBuilder {
+    protected:
+        bool _isColored = false;
+        
+    public:
+        /** Add a new place with a unique name */
+        virtual void addPlace(const std::string& name,
+                int tokens,
+                double x = 0,
+                double y = 0) = 0;
+        /** Add a new colored place with a unique name */
+        virtual void addPlace(const std::string& name,
+                Colored::ColorType* type,
+                Colored::Multiset&& tokens,
+                double x = 0,
+                double y = 0)
+        {
+            std::cerr << "Colored places are not supported in standard P/T nets" << std::endl;
+            exit(ErrorCode);
+        }
+        /** Add a new transition with a unique name */
+        virtual void addTransition(const std::string& name,
+                double x = 0,
+                double y = 0) = 0;
+        /** Add a new colored transition with a unique name */
+        virtual void addTransition(const std::string& name,
+                const Colored::GuardExpression_ptr& guard,
+                double x = 0,
+                double y = 0)
+        {
+            std::cerr << "Colored transitions are not supported in standard P/T nets" << std::endl;
+            exit(ErrorCode);
+        }
+        /** Add input arc with given weight */
+        virtual void addInputArc(const std::string& place,
+                const std::string& transition,
+                bool inhibitor,
+                int) = 0;
+        /** Add colored input arc with given arc expression */
+        virtual void addInputArc(const std::string& place,
+                const std::string& transition,
+                const Colored::ArcExpression_ptr& expr)
+        {
+            std::cerr << "Colored input arcs are not supported in standard P/T nets" << std::endl;
+            exit(ErrorCode);
+        }
+        /** Add output arc with given weight */
+        virtual void addOutputArc(const std::string& transition,
+                const std::string& place,
+                int weight = 1) = 0;
+        /** Add output arc with given arc expression */
+        virtual void addOutputArc(const std::string& transition,
+                const std::string& place,
+                const Colored::ArcExpression_ptr& expr)
+        {
+            std::cerr << "Colored output arcs are not supported in standard P/T nets" << std::endl;
+            exit(ErrorCode);
+        }
+        /** Add color types with id */
+        virtual void addColorType(const std::string& id,
+                Colored::ColorType* type)
+        {
+            std::cerr << "Color types are not supported in standard P/T nets" << std::endl;
+            exit(ErrorCode);
+        }
+        
+        virtual void enableColors() {
+            _isColored = true;
+        }
+
+        virtual bool isColored() const {
+            return _isColored;
+        }
+
+        virtual void sort() = 0;
+        
+        virtual ~AbstractPetriNetBuilder() {
+        }
+    };
+
+}
+
+#endif // ABSTRACTPETRINETBUILDER_H
 
=== added directory 'include/PetriEngine/Colored'
=== added file 'include/PetriEngine/Colored/ColoredNetStructures.h'
--- include/PetriEngine/Colored/ColoredNetStructures.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/Colored/ColoredNetStructures.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,48 @@
+/*
+ * 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
+ */
+
+#ifndef COLOREDNETSTRUCTURES_H
+#define COLOREDNETSTRUCTURES_H
+
+#include <vector>
+#include <set>
+#include "Colors.h"
+#include "Expressions.h"
+#include "Multiset.h"
+
+namespace PetriEngine {
+    namespace Colored {
+        
+        struct Arc {
+            uint32_t place;
+            uint32_t transition;
+            ArcExpression_ptr expr;
+            bool input;
+        };
+        
+        struct Transition {
+            std::string name;
+            GuardExpression_ptr guard;
+            std::vector<Arc> arcs;
+        };
+        
+        struct Place {
+            std::string name;
+            ColorType* type;
+            Multiset marking;
+        };
+    }
+}
+
+#endif /* COLOREDNETSTRUCTURES_H */
+
 
=== added file 'include/PetriEngine/Colored/ColoredPetriNetBuilder.h'
--- include/PetriEngine/Colored/ColoredPetriNetBuilder.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/Colored/ColoredPetriNetBuilder.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,179 @@
+/*
+ * File:   ColoredPetriNetBuilder.h
+ * Author: Klostergaard
+ *
+ * Created on 17. februar 2018, 16:25
+ */
+
+#ifndef COLOREDPETRINETBUILDER_H
+#define COLOREDPETRINETBUILDER_H
+
+#include <vector>
+#include <unordered_map>
+
+#include "ColoredNetStructures.h"
+#include "../AbstractPetriNetBuilder.h"
+#include "../PetriNetBuilder.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;
+        
+    public:
+        ColoredPetriNetBuilder();
+        ColoredPetriNetBuilder(const ColoredPetriNetBuilder& orig);
+        virtual ~ColoredPetriNetBuilder();
+        
+        void addPlace(const std::string& name,
+                int tokens,
+                double x = 0,
+                double y = 0) override ;
+        void addPlace(const std::string& name,
+                Colored::ColorType* type,
+                Colored::Multiset&& tokens,
+                double x = 0,
+                double y = 0) override;
+        void addTransition(const std::string& name,
+                double x = 0,
+                double y = 0) override;
+        void addTransition(const std::string& name,
+                const Colored::GuardExpression_ptr& guard,
+                double x = 0,
+                double y = 0) override;
+        void addInputArc(const std::string& place,
+                const std::string& transition,
+                bool inhibitor,
+                int) override;
+        void addInputArc(const std::string& place,
+                const std::string& transition,
+                const Colored::ArcExpression_ptr& expr) override;
+        void addOutputArc(const std::string& transition,
+                const std::string& place,
+                int weight = 1) override;
+        void addOutputArc(const std::string& transition,
+                const std::string& place,
+                const Colored::ArcExpression_ptr& expr) override;
+        void addColorType(const std::string& id,
+                Colored::ColorType* type) override;
+
+
+        void sort() override;
+
+        double getUnfoldTime() const {
+            return _time;
+        }
+
+        uint32_t getPlaceCount() const {
+            return _places.size();
+        }
+
+        uint32_t getTransitionCount() const {
+            return _transitions.size();
+        }
+
+        uint32_t getArcCount() const {
+            uint32_t sum = 0;
+            for (auto& t : _transitions) {
+                sum += t.arcs.size();
+            }
+            return sum;
+        }
+
+        uint32_t getUnfoldedPlaceCount() const {
+            //return _nptplaces;
+            return _ptBuilder.numberOfPlaces();
+        }
+
+        uint32_t getUnfoldedTransitionCount() const {
+            return _ptBuilder.numberOfTransitions();
+        }
+
+        uint32_t getUnfoldedArcCount() const {
+            return _nptarcs;
+        }
+
+        bool isUnfolded() const {
+            return _unfolded;
+        }
+
+        const PTPlaceMap& getUnfoldedPlaceNames() const {
+            return _ptplacenames;
+        }
+
+        const PTTransitionMap& getUnfoldedTransitionNames() const {
+            return _pttransitionnames;
+        }
+        
+        PetriNetBuilder& unfold();
+        PetriNetBuilder& stripColors();
+    private:
+        std::unordered_map<std::string,uint32_t> _placenames;
+        std::unordered_map<std::string,uint32_t> _transitionnames;
+        PTPlaceMap _ptplacenames;
+        PTTransitionMap _pttransitionnames;
+        uint32_t _nptplaces = 0;
+        uint32_t _npttransitions = 0;
+        uint32_t _nptarcs = 0;
+        
+        std::vector<Colored::Place> _places;
+        std::vector<Colored::Transition> _transitions;
+        std::vector<Colored::Arc> _arcs;
+        ColorTypeMap _colors;
+        PetriNetBuilder _ptBuilder;
+        bool _unfolded = false;
+        bool _stripped = false;
+
+        double _time;
+
+        std::string arcToString(Colored::Arc& arc) const ;
+        
+        void addArc(const std::string& place,
+                const std::string& transition,
+                const Colored::ArcExpression_ptr& expr,
+                bool input);
+        
+        void unfoldPlace(Colored::Place& place);
+        void unfoldTransition(Colored::Transition& transition);
+        void unfoldArc(Colored::Arc& arc, Colored::ExpressionContext::BindingMap& binding, std::string& name);
+    };
+    
+    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);
+
+        Colored::ExpressionContext::BindingMap& nextBinding();
+        Colored::ExpressionContext::BindingMap& currentBinding();
+        bool isInitial() const;
+        Iterator begin();
+        Iterator end();
+    };
+}
+
+#endif /* COLOREDPETRINETBUILDER_H */
+
 
=== added file 'include/PetriEngine/Colored/Colors.h'
--- include/PetriEngine/Colored/Colors.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/Colored/Colors.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,279 @@
+/*
+ * 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
+ */
+
+#ifndef COLORS_H
+#define COLORS_H
+
+#include <stdint.h>
+#include <stddef.h>
+#include <string>
+#include <string.h>
+#include <utility>
+#include <vector>
+#include <unordered_map>
+
+namespace PetriEngine {
+    namespace Colored {
+        class ColorType;
+
+        class Color {
+        public:
+            friend std::ostream& operator<< (std::ostream& stream, const Color& color);
+            
+        protected:
+            const std::vector<const Color*> _tuple;
+            ColorType* _colorType;
+            std::string _colorName;
+            uint32_t _id;
+            
+        public:
+            Color(ColorType* colorType, uint32_t id, std::vector<const Color*>& colors);
+            Color(ColorType* colorType, uint32_t id, const char* color);
+            ~Color() {}
+            
+            bool isTuple() const {
+                return _tuple.size() > 1;
+            }
+            
+            const std::string& getColorName() const {
+                if (this->isTuple()) {
+                    throw "Cannot get color from a tuple color.";
+                }
+                return _colorName;
+            }
+            
+            ColorType* getColorType() const {
+                return _colorType;
+            }
+            
+            uint32_t getId() const {
+                return _id;
+            }
+            
+            const Color* operator[] (size_t index) const;
+            bool operator< (const Color& other) const;
+            bool operator> (const Color& other) const;
+            bool operator<= (const Color& other) const;
+            bool operator>= (const Color& other) const;
+            
+            bool operator== (const Color& other) const {
+                return _colorType == other._colorType && _id == other._id;
+            }
+            bool operator!= (const Color& other) const {
+                return !((*this) == other);
+            }
+            
+            const Color& operator++ () const;
+            const Color& operator-- () const;
+            
+            std::string toString() const;
+            static std::string toString(const Color* color);
+            static std::string toString(const std::vector<const Color*>& colors);
+        };
+        
+        /*
+         *  Singleton pattern from: 
+         * https://stackoverflow.com/questions/1008019/c-singleton-design-pattern
+         */
+        class DotConstant : public Color {
+        private:
+            DotConstant();
+            
+        public:
+            static const Color* dotConstant() {
+                static DotConstant _instance;
+                
+                return &_instance;
+            }
+            
+            DotConstant(DotConstant const&) = delete;
+            void operator=(DotConstant const&) = delete;
+
+            bool operator== (const DotConstant& other) {
+                return true;
+            }
+        };
+        
+        class ColorType {
+        public:
+            class iterator {
+            private:
+                ColorType& type;
+                size_t index;
+
+            public:
+                iterator(ColorType& type, size_t index) : type(type), index(index) {}
+
+                const Color& operator++() {
+                    return type[++index];
+                }
+
+                const Color& operator++(int) {
+                    return type[index++];
+                }
+
+                const Color& operator--() {
+                    return type[--index];
+                }
+                const Color& operator--(int) {
+                    return type[index--];
+                }
+
+                const Color& operator*() {
+                    return type[index];
+                }
+
+                const Color* operator->() {
+                    return &type[index];
+                }
+
+                bool operator==(iterator& other) {
+                    return type == other.type && index == other.index;
+                }
+
+                bool operator!=(iterator& other) {
+                    return !(type == other.type) || index != other.index;
+                }
+            };
+            
+        private:
+            std::vector<Color> _colors;
+            uintptr_t _id;
+            std::string _name;
+            
+        public:
+            ColorType(std::vector<ColorType*> elements);
+            ColorType(std::string name = "Undefined") : _colors(), _name(std::move(name)) {
+                _id = (uintptr_t)this;
+            }
+            
+            virtual void addColor(const char* colorName);
+            virtual void addColor(std::vector<const Color*>& colors);
+            virtual void addDot() {
+                _colors.push_back(*DotConstant::dotConstant());
+            }
+            
+            virtual size_t size() const {
+                return _colors.size();
+            }
+            
+            virtual const Color& operator[] (size_t index) {
+                return _colors[index];
+            }
+            
+            virtual const Color& operator[] (int index) {
+                return _colors[index];
+            }
+            
+            virtual const Color& operator[] (uint32_t index) {
+                return _colors[index];
+            }
+            
+            virtual const Color* operator[] (const char* index);
+            
+            virtual const Color* operator[] (const std::string& index) {
+                return (*this)[index.c_str()];
+            }
+            
+            bool operator== (const ColorType& other) const {
+                return _id == other._id;
+            }
+
+            uintptr_t getId() {
+                return _id;
+            }
+
+            const std::string& getName() const {
+                return _name;
+            }
+            
+            iterator begin() {
+                return {*this, 0};
+            }
+
+            iterator end() {
+                return {*this, size()};
+            }
+        };
+
+        class ProductType : public ColorType {
+        private:
+            std::vector<ColorType*> constituents;
+            std::unordered_map<size_t,Color> cache;
+
+        public:
+            ProductType(const std::string& name = "Undefined") : ColorType(name) {}
+            ~ProductType() {
+                cache.clear();
+            }
+
+            void addType(ColorType* type) {
+                constituents.push_back(type);
+            }
+
+            void addColor(const char* colorName) override {}
+            void addColor(std::vector<const Color*>& colors) override {}
+            void addDot() override {}
+
+            size_t size() const override {
+                size_t product = 1;
+                for (auto ct : constituents) {
+                    product *= ct->size();
+                }
+                return product;
+            }
+
+            bool containsTypes(const std::vector<const ColorType*>& types) const {
+                if (constituents.size() != types.size()) return false;
+
+                for (size_t i = 0; i < constituents.size(); ++i) {
+                    if (!(*constituents[i] == *types[i])) {
+                        return false;
+                    }
+                }
+
+                return true;
+            }
+
+            const Color* getColor(const std::vector<const Color*>& colors);
+
+            const Color& operator[](size_t index) override;
+            const Color& operator[](int index) override {
+                return operator[]((size_t)index);
+            }
+            const Color& operator[](uint32_t index) override {
+                return operator[]((size_t)index);
+            }
+
+            const Color* operator[](const char* index) override;
+            const Color* operator[](const std::string& index) override;
+        };
+        
+        struct Variable {
+            std::string name;
+            ColorType* colorType;
+        };
+        
+        struct Binding {
+            Variable* var;
+            const Color* color;
+            
+            bool operator==(Binding& other) {
+                return var->name.compare(other.var->name);
+            }
+        };
+    }
+}
+
+#endif /* COLORS_H */
+
 
=== added file 'include/PetriEngine/Colored/Expressions.h'
--- include/PetriEngine/Colored/Expressions.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/Colored/Expressions.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,658 @@
+/*
+ * 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
+ */
+
+#ifndef COLORED_EXPRESSIONS_H
+#define COLORED_EXPRESSIONS_H
+
+#include <string>
+#include <unordered_map>
+#include <set>
+#include <stdlib.h>
+#include <iostream>
+#include <cassert>
+#include <memory>
+
+
+#include "Colors.h"
+#include "Multiset.h"
+#include "../errorcodes.h"
+
+namespace PetriEngine {
+    class ColoredPetriNetBuilder;
+    
+    namespace Colored {
+        struct ExpressionContext {
+            typedef std::unordered_map<std::string, const 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();
+                for (auto& elem : colorTypes) {
+                    auto col = (*elem.second)[color];
+                    if (col)
+                        return col;
+                }
+                printf("Could not find color: %s\nCANNOT_COMPUTE\n", color.c_str());
+                exit(ErrorCode);
+            }
+
+            ProductType* findProductColorType(const std::vector<const ColorType*>& types) const {
+                for (auto& elem : colorTypes) {
+                    auto* pt = dynamic_cast<ProductType*>(elem.second);
+                    if (pt && pt->containsTypes(types)) {
+                        return pt;
+                    }
+                }
+                return nullptr;
+            }
+        };
+
+        class WeightException : public std::exception {
+        private:
+            std::string _message;
+        public:
+            explicit WeightException(std::string message) : _message(message) {}
+
+            const char* what() const noexcept override {
+                return ("Undefined weight: " + _message).c_str();
+            }
+        };
+        
+        class Expression {
+        public:
+            Expression() {}
+            
+            virtual void getVariables(std::set<Variable*>& variables) const {
+            }
+            
+            virtual void expressionType() {
+                std::cout << "Expression" << std::endl;
+            }
+
+            virtual std::string toString() const {
+                return "Unsupported";
+            }
+        };
+        
+        class ColorExpression : public Expression {
+        public:
+            ColorExpression() {}
+            virtual ~ColorExpression() {}
+            
+            virtual const Color* eval(ExpressionContext& context) const = 0;
+        };
+        
+        class DotConstantExpression : public ColorExpression {
+        public:
+            const Color* eval(ExpressionContext& context) const override {
+                return DotConstant::dotConstant();
+            }
+        };
+
+        typedef std::shared_ptr<ColorExpression> ColorExpression_ptr;
+        
+        class VariableExpression : public ColorExpression {
+        private:
+            Variable* _variable;
+            
+        public:
+            const Color* eval(ExpressionContext& context) const override {
+                return context.binding[_variable->name];
+            }
+            
+            void getVariables(std::set<Variable*>& variables) const override {
+                variables.insert(_variable);
+            }
+
+            std::string toString() const override {
+                return _variable->name;
+            }
+
+            VariableExpression(Variable* variable)
+                    : _variable(variable) {}
+        };
+        
+        class UserOperatorExpression : public ColorExpression {
+        private:
+            const Color* _userOperator;
+            
+        public:
+            const Color* eval(ExpressionContext& context) const override {
+                return _userOperator;
+            }
+
+            std::string toString() const override {
+                return _userOperator->toString();
+            }
+
+            UserOperatorExpression(const Color* userOperator)
+                    : _userOperator(userOperator) {}
+        };
+        
+        class UserSortExpression : public Expression {
+        private:
+            ColorType* _userSort;
+            
+        public:
+            ColorType* eval(ExpressionContext& context) const {
+                return _userSort;
+            }
+
+            std::string toString() const override {
+                return _userSort->getName();
+            }
+
+            UserSortExpression(ColorType* userSort)
+                    : _userSort(userSort) {}
+        };
+
+        typedef std::shared_ptr<UserSortExpression> UserSortExpression_ptr;
+        
+        class NumberConstantExpression : public Expression {
+        private:
+            uint32_t _number;
+            
+        public:
+            uint32_t eval(ExpressionContext& context) const {
+                return _number;
+            }
+            
+            NumberConstantExpression(uint32_t number)
+                    : _number(number) {}
+        };
+
+        typedef std::shared_ptr<NumberConstantExpression> NumberConstantExpression_ptr;
+        
+        class SuccessorExpression : public ColorExpression {
+        private:
+            ColorExpression_ptr _color;
+            
+        public:
+            const Color* eval(ExpressionContext& context) const override {
+                return &++(*_color->eval(context));
+            }
+            
+            void getVariables(std::set<Variable*>& variables) const override {
+                _color->getVariables(variables);
+            }
+
+            std::string toString() const override {
+                return _color->toString() + "++";
+            }
+
+            SuccessorExpression(ColorExpression_ptr&& color)
+                    : _color(std::move(color)) {}
+        };
+        
+        class PredecessorExpression : public ColorExpression {
+        private:
+            ColorExpression_ptr _color;
+            
+        public:
+            const Color* eval(ExpressionContext& context) const override {
+                return &--(*_color->eval(context));
+            }
+            
+            void getVariables(std::set<Variable*>& variables) const override {
+                _color->getVariables(variables);
+            }
+
+            std::string toString() const override {
+                return _color->toString() + "--";
+            }
+
+            PredecessorExpression(ColorExpression_ptr&& color)
+                    : _color(std::move(color)) {}
+        };
+        
+        class TupleExpression : public ColorExpression {
+        private:
+            std::vector<ColorExpression_ptr> _colors;
+            
+        public:
+            const Color* eval(ExpressionContext& context) const override {
+                std::vector<const Color*> colors;
+                std::vector<const ColorType*> types;
+                for (auto color : _colors) {
+                    colors.push_back(color->eval(context));
+                    types.push_back(colors.back()->getColorType());
+                }
+                ProductType* pt = context.findProductColorType(types);
+
+                const Color* col = pt->getColor(colors);
+                assert(col != nullptr);
+                return col;
+            }
+            
+            void getVariables(std::set<Variable*>& variables) const override {
+                for (auto elem : _colors) {
+                    elem->getVariables(variables);
+                }
+            }
+
+            std::string toString() const override {
+                std::string res = "(" + _colors[0]->toString();
+                for (uint32_t i = 1; i < _colors.size(); ++i) {
+                    res += "," + _colors[i]->toString();
+                }
+                res += ")";
+                return res;
+            }
+
+            TupleExpression(std::vector<ColorExpression_ptr>&& colors)
+                    : _colors(std::move(colors)) {}
+        };
+        
+        class GuardExpression : public Expression {
+        public:
+            GuardExpression() {}
+            virtual ~GuardExpression() {}
+            
+            virtual bool eval(ExpressionContext& context) const = 0;
+        };
+
+        typedef std::shared_ptr<GuardExpression> GuardExpression_ptr;
+        
+        class LessThanExpression : public GuardExpression {
+        private:
+            ColorExpression_ptr _left;
+            ColorExpression_ptr _right;
+            
+        public:
+            bool eval(ExpressionContext& context) const override {
+                return _left->eval(context) < _right->eval(context);
+            }
+            
+            void getVariables(std::set<Variable*>& variables) const override {
+                _left->getVariables(variables);
+                _right->getVariables(variables);
+            }
+            
+            LessThanExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right)
+                    : _left(std::move(left)), _right(std::move(right)) {}
+        };
+        
+        class GreaterThanExpression : public GuardExpression {
+        private:
+            ColorExpression_ptr _left;
+            ColorExpression_ptr _right;
+            
+        public:
+            bool eval(ExpressionContext& context) const override {
+                return _left->eval(context) > _right->eval(context);
+            }
+            
+            void getVariables(std::set<Variable*>& variables) const override {
+                _left->getVariables(variables);
+                _right->getVariables(variables);
+            }
+            
+            GreaterThanExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right)
+                    : _left(std::move(left)), _right(std::move(right)) {}
+        };
+        
+        class LessThanEqExpression : public GuardExpression {
+        private:
+            ColorExpression_ptr _left;
+            ColorExpression_ptr _right;
+            
+        public:
+            bool eval(ExpressionContext& context) const override {
+                return _left->eval(context) <= _right->eval(context);
+            }
+            
+            void getVariables(std::set<Variable*>& variables) const override {
+                _left->getVariables(variables);
+                _right->getVariables(variables);
+            }
+            
+            LessThanEqExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right)
+                    : _left(std::move(left)), _right(std::move(right)) {}
+        };
+        
+        class GreaterThanEqExpression : public GuardExpression {
+        private:
+            ColorExpression_ptr _left;
+            ColorExpression_ptr _right;
+            
+        public:
+            bool eval(ExpressionContext& context) const override {
+                return _left->eval(context) >= _right->eval(context);
+            }
+            
+            void getVariables(std::set<Variable*>& variables) const override {
+                _left->getVariables(variables);
+                _right->getVariables(variables);
+            }
+            
+            GreaterThanEqExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right)
+                    : _left(std::move(left)), _right(std::move(right)) {}
+        };
+        
+        class EqualityExpression : public GuardExpression {
+        private:
+            ColorExpression_ptr _left;
+            ColorExpression_ptr _right;
+            
+        public:
+            bool eval(ExpressionContext& context) const override {
+                return _left->eval(context) == _right->eval(context);
+            }
+            
+            void getVariables(std::set<Variable*>& variables) const override {
+                _left->getVariables(variables);
+                _right->getVariables(variables);
+            }
+            
+            EqualityExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right)
+                    : _left(std::move(left)), _right(std::move(right)) {}
+        };
+        
+        class InequalityExpression : public GuardExpression {
+        private:
+            ColorExpression_ptr _left;
+            ColorExpression_ptr _right;
+            
+        public:
+            bool eval(ExpressionContext& context) const override {
+                return _left->eval(context) != _right->eval(context);
+            }
+            
+            void getVariables(std::set<Variable*>& variables) const override {
+                _left->getVariables(variables);
+                _right->getVariables(variables);
+            }
+            
+            InequalityExpression(ColorExpression_ptr&& left, ColorExpression_ptr&& right)
+                    : _left(std::move(left)), _right(std::move(right)) {}
+        };
+        
+        class NotExpression : public GuardExpression {
+        private:
+            GuardExpression_ptr _expr;
+            
+        public:
+            bool eval(ExpressionContext& context) const override {
+                return !_expr->eval(context);
+            }
+            
+            void getVariables(std::set<Variable*>& variables) const override {
+                _expr->getVariables(variables);
+            }
+            
+            NotExpression(GuardExpression_ptr&& expr) : _expr(std::move(expr)) {}
+        };
+        
+        class AndExpression : public GuardExpression {
+        private:
+            GuardExpression_ptr _left;
+            GuardExpression_ptr _right;
+            
+        public:
+            bool eval(ExpressionContext& context) const override {
+                return _left->eval(context) && _right->eval(context);
+            }
+            
+            void getVariables(std::set<Variable*>& variables) const override {
+                _left->getVariables(variables);
+                _right->getVariables(variables);
+            }
+            
+            AndExpression(GuardExpression_ptr&& left, GuardExpression_ptr&& right)
+                    : _left(left), _right(right) {}
+        };
+        
+        class OrExpression : public GuardExpression {
+        private:
+            GuardExpression_ptr _left;
+            GuardExpression_ptr _right;
+            
+        public:
+            bool eval(ExpressionContext& context) const override {
+                return _left->eval(context) || _right->eval(context);
+            }
+            
+            void getVariables(std::set<Variable*>& variables) const override {
+                _left->getVariables(variables);
+                _right->getVariables(variables);
+            }
+            
+            OrExpression(GuardExpression_ptr&& left, GuardExpression_ptr&& right)
+                    : _left(std::move(left)), _right(std::move(right)) {}
+        };
+        
+        class ArcExpression : public Expression {
+        public:
+            ArcExpression() {}
+            virtual ~ArcExpression() {}
+            
+            virtual Multiset eval(ExpressionContext& context) const = 0;
+
+            virtual void expressionType() override {
+                std::cout << "ArcExpression" << std::endl;
+            }
+
+            virtual uint32_t weight() const = 0;
+        };
+
+        typedef std::shared_ptr<ArcExpression> ArcExpression_ptr;
+        
+        class AllExpression : public Expression {
+        private:
+            ColorType* _sort;
+            
+        public:
+            virtual ~AllExpression() {};
+            std::vector<const Color*> eval(ExpressionContext& context) const {
+                std::vector<const Color*> colors;
+                assert(_sort != nullptr);
+                for (size_t i = 0; i < _sort->size(); i++) {
+                    colors.push_back(&(*_sort)[i]);
+                }
+                return colors;
+            }
+
+            size_t size() const {
+                return  _sort->size();
+            }
+
+            std::string toString() const override {
+                return _sort->getName() + ".all";
+            }
+
+            AllExpression(ColorType* sort) : _sort(sort) 
+            {
+                assert(sort != nullptr);
+            }
+        };
+
+        typedef std::shared_ptr<AllExpression> AllExpression_ptr;
+        
+        class NumberOfExpression : public ArcExpression {
+        private:
+            uint32_t _number;
+            std::vector<ColorExpression_ptr> _color;
+            AllExpression_ptr _all;
+            
+        public:
+            Multiset eval(ExpressionContext& context) const override {
+                std::vector<const Color*> colors;
+                if (!_color.empty()) {
+                    for (auto elem : _color) {
+                        colors.push_back(elem->eval(context));
+                    }
+                } else if (_all != nullptr) {
+                    colors = _all->eval(context);
+                }
+                std::vector<std::pair<const Color*,uint32_t>> col;
+                for (auto elem : colors) {
+                    col.push_back(std::make_pair(elem, _number));
+                }
+                return Multiset(col);
+            }
+            
+            void getVariables(std::set<Variable*>& variables) const override {
+                if (_all != nullptr)
+                    return;
+                for (auto elem : _color) {
+                    elem->getVariables(variables);
+                }
+            }
+
+            uint32_t weight() const override {
+                if (_all == nullptr)
+                    return _number * _color.size();
+                else
+                    return _number * _all->size();
+            }
+
+            bool isAll() const {
+                return (bool)_all;
+            }
+
+            bool isSingleColor() const {
+                return !isAll() && _color.size() == 1;
+            }
+
+            uint32_t number() const {
+                return _number;
+            }
+
+            std::string toString() const override {
+                if (isAll())
+                    return std::to_string(_number) + "'(" + _all->toString() + ")";
+                std::string res = std::to_string(_number) + "'(" + _color[0]->toString() + ")";
+                for (uint32_t i = 1; i < _color.size(); ++i) {
+                    res += " + ";
+                    res += std::to_string(_number) + "'(" + _color[i]->toString() + ")";
+                }
+                return res;
+            }
+
+            NumberOfExpression(std::vector<ColorExpression_ptr>&& color, uint32_t number = 1)
+                    : _number(number), _color(std::move(color)), _all(nullptr) {}
+            NumberOfExpression(AllExpression_ptr&& all, uint32_t number = 1)
+                    : _number(number), _color(), _all(std::move(all)) {}
+        };
+
+        typedef std::shared_ptr<NumberOfExpression> NumberOfExpression_ptr;
+        
+        class AddExpression : public ArcExpression {
+        private:
+            std::vector<ArcExpression_ptr> _constituents;
+            
+        public:
+            Multiset eval(ExpressionContext& context) const override {
+                Multiset ms;
+                for (auto expr : _constituents) {
+                    ms += expr->eval(context);
+                }
+                return ms;
+            }
+            
+            void getVariables(std::set<Variable*>& variables) const override {
+                for (auto elem : _constituents) {
+                    elem->getVariables(variables);
+                }
+            }
+
+            uint32_t weight() const override {
+                uint32_t res = 0;
+                for (auto expr : _constituents) {
+                    res += expr->weight();
+                }
+                return res;
+            }
+
+            std::string toString() const override {
+                std::string res = _constituents[0]->toString();
+                for (uint32_t i = 1; i < _constituents.size(); ++i) {
+                    res += " + " + _constituents[i]->toString();
+                }
+                return res;
+            }
+
+            AddExpression(std::vector<ArcExpression_ptr>&& constituents)
+                    : _constituents(std::move(constituents)) {}
+        };
+        
+        class SubtractExpression : public ArcExpression {
+        private:
+            ArcExpression_ptr _left;
+            ArcExpression_ptr _right;
+            
+        public:
+            Multiset eval(ExpressionContext& context) const override {
+                return _left->eval(context) - _right->eval(context);
+            }
+            
+            void getVariables(std::set<Variable*>& variables) const override {
+                _left->getVariables(variables);
+                _right->getVariables(variables);
+            }
+
+            uint32_t weight() const override {
+                auto* left = dynamic_cast<NumberOfExpression*>(_left.get());
+                if (!left || !left->isAll()) {
+                    throw WeightException("Left constituent of subtract is not an all expression!");
+                }
+                auto* right = dynamic_cast<NumberOfExpression*>(_right.get());
+                if (!right || !right->isSingleColor()) {
+                    throw WeightException("Right constituent of subtract is not a single color number of expression!");
+                }
+
+                uint32_t val = std::min(left->number(), right->number());
+                return _left->weight() - val;
+            }
+
+            std::string toString() const override {
+                return _left->toString() + " - " + _right->toString();
+            }
+
+            SubtractExpression(ArcExpression_ptr&& left, ArcExpression_ptr&& right)
+                    : _left(std::move(left)), _right(std::move(right)) {}
+        };
+        
+        class ScalarProductExpression : public ArcExpression {
+        private:
+            uint32_t _scalar;
+            ArcExpression_ptr _expr;
+            
+        public:
+            Multiset eval(ExpressionContext& context) const override {
+                return _expr->eval(context) * _scalar;
+            }
+            
+            void getVariables(std::set<Variable*>& variables) const override {
+                _expr->getVariables(variables);
+            }
+
+            uint32_t weight() const override {
+                return _scalar * _expr->weight();
+            }
+
+            std::string toString() const override {
+                return std::to_string(_scalar) + " * " + _expr->toString();
+            }
+
+            ScalarProductExpression(ArcExpression_ptr&& expr, uint32_t scalar)
+                    : _scalar(std::move(scalar)), _expr(expr) {}
+        };
+    }
+}
+
+#endif /* COLORED_EXPRESSIONS_H */
+
 
=== added file 'include/PetriEngine/Colored/Multiset.h'
--- include/PetriEngine/Colored/Multiset.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/Colored/Multiset.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,83 @@
+/*
+ * 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:   Multiset.h
+ * Author: andreas
+ *
+ * Created on February 20, 2018, 10:37 AM
+ */
+
+#ifndef MULTISET_H
+#define MULTISET_H
+
+#include <vector>
+#include <utility>
+
+#include "Colors.h"
+
+
+namespace PetriEngine {
+    namespace Colored {
+        class Multiset {
+        private:
+            class Iterator {
+            private:
+                Multiset* ms;
+                size_t index;
+
+            public:
+                Iterator(Multiset* ms, size_t index)
+                        : ms(ms), index(index) {}
+
+                bool operator==(Iterator& other);
+                bool operator!=(Iterator& other);
+                Iterator& operator++();
+                std::pair<const Color*,uint32_t&> operator++(int);
+                std::pair<const Color*,uint32_t&> operator*();
+            };
+
+            typedef std::vector<std::pair<uint32_t,uint32_t>> Internal;
+            
+        public:
+            Multiset();
+            Multiset(const Multiset& orig);
+            Multiset(std::pair<const Color*,uint32_t> color);
+            Multiset(std::vector<std::pair<const Color*,uint32_t>>& colors);
+            virtual ~Multiset();
+            
+            Multiset operator+ (const Multiset& other) const;
+            Multiset operator- (const Multiset& other) const;
+            Multiset operator* (uint32_t scalar) const;
+            void operator+= (const Multiset& other);
+            void operator-= (const Multiset& other);
+            void operator*= (uint32_t scalar);
+            uint32_t operator[] (const Color* color) const;
+            uint32_t& operator[] (const Color* color);
+            
+            bool empty() const;
+            void clean();
+
+            size_t distinctSize() const {
+                return _set.size();
+            }
+
+            size_t size() const;
+            
+            Iterator begin();
+            Iterator end();
+
+            std::string toString() const;
+            
+        private:
+            Internal _set;
+            ColorType* type;
+        };
+    }
+}
+
+#endif /* MULTISET_H */
+
 
=== added file 'include/PetriEngine/NetStructures.h'
--- include/PetriEngine/NetStructures.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/NetStructures.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,91 @@
+/* 
+ * File:   NetStructures.h
+ * Author: Peter G. Jensen
+ *
+ * Created on 09 March 2016, 21:08
+ */
+
+#ifndef NETSTRUCTURES_H
+#define NETSTRUCTURES_H
+
+#include <limits>
+#include <vector>
+
+namespace PetriEngine {
+
+    struct Arc {
+        uint32_t place;
+        uint32_t weight;
+        bool skip = false;
+        bool inhib = false;
+
+        Arc() :
+        place(std::numeric_limits<uint32_t>::max()),
+        weight(std::numeric_limits<uint32_t>::max()),
+        skip(false),
+        inhib(false) {
+        };
+        
+        bool operator < (const Arc& other) const
+        {
+            return place < other.place;
+        }
+        
+        bool operator == (const Arc& other) const
+        {
+            return place == other.place && weight == other.weight && inhib == other.inhib;
+        }
+    };
+
+    struct Transition {
+        std::vector<Arc> pre;
+        std::vector<Arc> post;
+        bool skip = false;
+        bool inhib = false;
+        
+        void addPreArc(const Arc& arc)
+        {
+            auto lb = std::lower_bound(pre.begin(), pre.end(), arc);
+            if(lb != pre.end() && lb->place == arc.place)
+                lb->weight += arc.weight;
+            else
+                lb = pre.insert(lb, arc);
+            assert(lb->weight > 0);
+        }
+        
+        void addPostArc(const Arc& arc)
+        {
+            auto lb = std::lower_bound(post.begin(), post.end(), arc);
+            if(lb != post.end() && lb->place == arc.place)
+                lb->weight += arc.weight;
+            else
+                lb = post.insert(lb, arc);
+            assert(lb->weight > 0);
+            
+        }
+    };
+
+    struct Place {
+        std::vector<uint32_t> consumers; // things consuming
+        std::vector<uint32_t> producers; // things producing
+        bool skip = false;
+        bool inhib = false;
+        
+        // should be replaced using concepts in c++20
+        void addConsumer(uint32_t id)
+        {
+            auto lb = std::lower_bound(consumers.begin(), consumers.end(), id);
+            if(lb == consumers.end() || *lb != id)
+                consumers.insert(lb, id);
+        }
+        
+        void addProducer(uint32_t id)
+        {
+            auto lb = std::lower_bound(producers.begin(), producers.end(), id);
+            if(lb == producers.end() || *lb != id)
+                producers.insert(lb, id);
+        }
+    };
+}
+#endif /* NETSTRUCTURES_H */
+
 
=== added directory 'include/PetriEngine/PQL'
=== added file 'include/PetriEngine/PQL/Contexts.h'
--- include/PetriEngine/PQL/Contexts.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/PQL/Contexts.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,250 @@
+/* PeTe - Petri Engine exTremE
+ * Copyright (C) 2011  Jonas Finnemann Jensen <[e-mail]>,
+ *                     Thomas Søndersø Nielsen <[e-mail]>,
+ *                     Lars Kærlund Østergaard <[e-mail]>,
+ *                     Peter Gjøl Jensen <[e-mail]>
+ * 
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ * 
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ * 
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+#ifndef CONTEXTS_H
+#define CONTEXTS_H
+
+#include "../PetriNet.h"
+#include "../Simplification/LPCache.h"
+#include "PQL.h"
+#include "../NetStructures.h"
+
+#include <string>
+#include <vector>
+#include <list>
+#include <map>
+#include <chrono>
+#include <glpk.h>
+
+namespace PetriEngine {
+    namespace PQL {
+
+        /** 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 PetriNet* _net;
+            std::vector<ExprError> _errors;
+        public:
+
+            /** A resolution result */
+            struct ResolutionResult {
+                /** Offset in relevant vector */
+                int offset;
+                /** True, if the resolution was successful */
+                bool success;
+            };
+
+            AnalysisContext(const std::unordered_map<std::string, uint32_t>& places, const std::unordered_map<std::string, uint32_t>& tnames, const PetriNet* net)
+            : _placeNames(places), _transitionNames(tnames), _net(net) {
+
+            }
+            
+            virtual void setHasDeadlock(){};
+            
+            const PetriNet* net() const
+            {
+                return _net;
+            }
+            
+            /** Resolve an identifier */
+            virtual ResolutionResult resolve(const std::string& identifier, bool place = true);
+
+            /** Report error */
+            void reportError(const ExprError& error) {
+                _errors.push_back(error);
+            }
+
+            /** Get list of errors */
+            const std::vector<ExprError>& errors() const {
+                return _errors;
+            }
+            auto& allPlaceNames() const { return _placeNames; }
+            auto& allTransitionNames() const { return _transitionNames; }
+
+        };
+
+        class ColoredAnalysisContext : public AnalysisContext {
+        protected:
+            const std::unordered_map<std::string, std::unordered_map<uint32_t , std::string>>& _coloredPlaceNames;
+            const std::unordered_map<std::string, std::vector<std::string>>& _coloredTransitionNames;
+
+            bool _colored;
+
+        public:
+            ColoredAnalysisContext(const std::unordered_map<std::string, uint32_t>& places,
+                                   const std::unordered_map<std::string, uint32_t>& tnames,
+                                   const PetriNet* net,
+                                   const std::unordered_map<std::string, std::unordered_map<uint32_t , std::string>>& cplaces,
+                                   const std::unordered_map<std::string, std::vector<std::string>>& ctnames,
+                                   bool colored)
+                    : AnalysisContext(places, tnames, net),
+                      _coloredPlaceNames(cplaces),
+                      _coloredTransitionNames(ctnames),
+                      _colored(colored)
+            {}
+
+            bool resolvePlace(const std::string& place, std::unordered_map<uint32_t,std::string>& out);
+
+            bool resolveTransition(const std::string& transition, std::vector<std::string>& out);
+
+            bool isColored() const {
+                return _colored;
+            }
+            auto& allColoredPlaceNames() const { return _coloredPlaceNames; }
+            auto& allColoredTransitionNames() const { return _coloredTransitionNames; }
+        };
+
+        /** Context provided for evalation */
+        class EvaluationContext {
+        public:
+
+            /** Create evaluation context, this doesn't take ownership */
+            EvaluationContext(const MarkVal* marking,
+                    const PetriNet* net) {
+                _marking = marking;
+                _net = net;
+            }
+            
+            EvaluationContext() {};
+
+            const MarkVal* marking() const {
+                return _marking;
+            }
+            
+            void setMarking(MarkVal* marking) {
+                _marking = marking;
+            }
+
+            const PetriNet* net() const {
+                return _net;
+            }
+        private:
+            const MarkVal* _marking = nullptr;
+            const PetriNet* _net = nullptr;
+        };
+
+        /** Context for distance computation */
+        class DistanceContext : public EvaluationContext {
+        public:
+
+            DistanceContext(const PetriNet* net,
+                    const MarkVal* marking)
+            : EvaluationContext(marking, net) {
+                _negated = false;
+            }
+
+
+            void negate() {
+                _negated = !_negated;
+            }
+
+            bool negated() const {
+                return _negated;
+            }
+
+        private:
+            bool _negated;
+        };
+
+        /** Context for condition to TAPAAL export */
+        class TAPAALConditionExportContext {
+        public:
+            bool failed;
+            std::string netName;
+        };
+
+        class SimplificationContext {
+        public:
+
+            SimplificationContext(const MarkVal* marking,
+                    const PetriNet* net, uint32_t queryTimeout, uint32_t lpTimeout,
+                    LPCache* cache)
+                    : _queryTimeout(queryTimeout), _lpTimeout(lpTimeout) {
+                _negated = false;
+                _marking = marking;
+                _net = net;
+                _base_lp = buildBase();
+                _start = std::chrono::high_resolution_clock::now();
+                _cache = cache;
+            }
+                    
+            virtual ~SimplificationContext() {
+                if(_base_lp != nullptr)
+                    glp_delete_prob(_base_lp);
+                _base_lp = nullptr;
+            }
+
+
+            const MarkVal* marking() const {
+                return _marking;
+            }
+
+            const PetriNet* net() const {
+                return _net;
+            }
+
+            void negate() {
+                _negated = !_negated;
+            }
+
+            bool negated() const {
+                return _negated;
+            }
+            
+            void setNegate(bool b){
+                _negated = b;
+            }
+            
+            double getReductionTime();
+            
+            bool timeout() const {
+                auto end = std::chrono::high_resolution_clock::now();
+                auto diff = std::chrono::duration_cast<std::chrono::seconds>(end - _start);
+                return (diff.count() >= _queryTimeout);
+            }
+            
+            uint32_t getLpTimeout() const;
+            
+            LPCache* cache() const
+            {
+                return _cache;
+            }
+            
+            
+            glp_prob* makeBaseLP() const;
+
+        private:
+            bool _negated;
+            const MarkVal* _marking;
+            const PetriNet* _net;
+            uint32_t _queryTimeout, _lpTimeout;
+            std::chrono::high_resolution_clock::time_point _start;
+            LPCache* _cache;
+            mutable glp_prob* _base_lp = nullptr;
+
+            glp_prob* buildBase() const;
+
+        };
+
+    } // PQL
+} // PetriEngine
+
+#endif // CONTEXTS_H
 
=== added file 'include/PetriEngine/PQL/Expressions.h'
--- include/PetriEngine/PQL/Expressions.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/PQL/Expressions.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,1221 @@
+/* PeTe - Petri Engine exTremE
+ * Copyright (C) 2011  Jonas Finnemann Jensen <[e-mail]>,
+ *                     Thomas Søndersø Nielsen <[e-mail]>,
+ *                     Lars Kærlund Østergaard <[e-mail]>,
+ *                     Peter Gjøl Jensen <[e-mail]>
+ * 
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ * 
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ * 
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+#ifndef EXPRESSIONS_H
+#define EXPRESSIONS_H
+
+
+#include <iostream>
+#include <fstream>
+#include <algorithm>
+#include "PQL.h"
+#include "Contexts.h"
+#include "..//Simplification/Member.h"
+#include "../Simplification/LinearPrograms.h"
+#include "../Simplification/Retval.h"
+
+using namespace PetriEngine::Simplification;
+
+namespace PetriEngine {
+    namespace PQL {
+        
+        std::string generateTabs(uint32_t tabs);
+        class CompareCondition;
+        class NotCondition;
+        /******************** EXPRESSIONS ********************/
+
+        /** Base class for all binary expressions */
+        class NaryExpr : public Expr {
+        protected:
+            NaryExpr() {};
+        public:
+
+            NaryExpr(std::vector<Expr_ptr>&& exprs) : _exprs(std::move(exprs)) {
+            }
+            virtual void analyze(AnalysisContext& context) override;
+            int evaluate(const EvaluationContext& context) override;
+            int formulaSize() const override{
+                size_t sum = 0;
+                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; }
+        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:
+            friend CompareCondition;
+            virtual void analyze(AnalysisContext& context) override;
+            int evaluate(const EvaluationContext& context) override;
+            void toBinary(std::ostream&) const override;
+            int formulaSize() const override{
+                size_t sum = _ids.size();
+                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; }
+        protected:
+            CommutativeExpr(int constant): _constant(constant) {};
+            void init(std::vector<Expr_ptr>&& exprs);
+            virtual int32_t preOp(const EvaluationContext& context) const override;
+            int32_t _constant;
+            std::vector<std::pair<uint32_t,std::string>> _ids;
+            Member commutativeCons(int constant, SimplificationContext& context, std::function<void(Member& a, Member b)> op) const;
+        };
+
+        /** Binary plus expression */
+        class PlusExpr : public CommutativeExpr {
+        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;
+            //int binaryOp() const;
+            std::string op() const override;
+        };
+
+        /** Binary minus expression */
+        class SubtractExpr : public NaryExpr {
+        public:
+
+            SubtractExpr(std::vector<Expr_ptr>&& exprs) : NaryExpr(std::move(exprs))
+            {
+            }
+            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:
+            int apply(int v1, int v2) const override;
+            //int binaryOp() const;
+            std::string op() const override;
+        };
+
+        /** Binary multiplication expression **/
+        class MultiplyExpr : public CommutativeExpr {
+        public:
+
+            MultiplyExpr(std::vector<Expr_ptr>&& exprs);
+            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;
+            //int binaryOp() const;
+            std::string op() const override;
+        };
+
+        /** Unary minus expression*/
+        class MinusExpr : public Expr {
+        public:
+
+            MinusExpr(const Expr_ptr expr) {
+                _expr = expr;
+            }
+            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;
+            }
+            bool placeFree() const override;
+            const Expr_ptr& operator[](size_t i) const { return _expr; };
+        private:
+            Expr_ptr _expr;
+        };
+
+        /** Literal integer value expression */
+        class LiteralExpr : public Expr {
+        public:
+
+            LiteralExpr(int value) : _value(value) {
+            }
+            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;
+            }
+            int value() const {
+                return _value;
+            };
+            Member constraint(SimplificationContext& context) const override;
+            bool placeFree() const override { return true; }
+        private:
+            int _value;
+        };
+
+
+        class IdentifierExpr : public Expr {
+        public:
+            IdentifierExpr(const std::string& name) : _name(name) {}
+            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 {
+                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;
+            }
+            virtual bool placeFree() const override {
+                if(_compiled) return _compiled->placeFree();
+                return false;
+            }
+
+            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;            
+        private:
+            std::string _name;
+            Expr_ptr _compiled;
+        };
+
+        /** Identifier expression */
+        class UnfoldedIdentifierExpr : public Expr {
+        public:
+            UnfoldedIdentifierExpr(const std::string& name, int offest)
+            : _offsetInMarking(offest), _name(name) {
+            }
+            
+            UnfoldedIdentifierExpr(const std::string& name) : UnfoldedIdentifierExpr(name, -1) {
+            }
+            
+            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;
+            }
+            /** Offset in marking or valuation */
+            int offset() const {
+                return _offsetInMarking;
+            }
+            const std::string& name()
+            {
+                return _name;
+            }
+            Member constraint(SimplificationContext& context) const override;
+            bool placeFree() const override { return false; }
+            void visit(Visitor& visitor) const override;
+        private:
+            /** Offset in marking, -1 if undefined, should be resolved during analysis */
+            int _offsetInMarking;
+            /** Identifier text */
+            std::string _name;
+        };
+
+        class ShallowCondition : public Condition
+        {
+            Result evaluate(const EvaluationContext& context) override
+            { return _compiled->evaluate(context); }
+            Result evalAndSet(const EvaluationContext& context) override
+            { return _compiled->evalAndSet(context); }
+            uint32_t distance(DistanceContext& context) const override
+            { return _compiled->distance(context); }
+            void toTAPAALQuery(std::ostream& out,TAPAALConditionExportContext& context) const override
+            { _compiled->toTAPAALQuery(out, context); }
+            void toBinary(std::ostream& out) const override
+            { return _compiled->toBinary(out); }
+            Retval simplify(SimplificationContext& context) const override
+            { return _compiled->simplify(context); }
+            Condition_ptr prepareForReachability(bool negated) const override
+            { return _compiled->prepareForReachability(negated); }
+            bool isReachability(uint32_t depth) const override
+            { return _compiled->isReachability(depth); }
+
+            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();
+            }
+
+            virtual Condition_ptr pushNegation(negstat_t& neg, const EvaluationContext& context, bool nested, bool negated, bool initrw) override
+            {
+                if(_compiled)
+                    return _compiled->pushNegation(neg, context, nested, negated, initrw);
+                else {
+                    if(negated)
+                        return std::static_pointer_cast<Condition>(std::make_shared<NotCondition>(clone()));
+                    else
+                        return clone();
+                }
+            }
+
+            void analyze(AnalysisContext& context) override
+            {
+                if (_compiled) _compiled->analyze(context);
+                else _analyze(context);
+            }
+            void toString(std::ostream &out) const {
+                if (_compiled) _compiled->toString(out);
+                else _toString(out);
+            }
+
+        protected:
+            virtual void _analyze(AnalysisContext& context) = 0;
+            virtual void _toString(std::ostream& out) const = 0;
+            virtual Condition_ptr clone() = 0;
+            Condition_ptr _compiled = nullptr;
+        };
+
+        /* Not condition */
+        class NotCondition : public Condition {
+        public:
+
+            NotCondition(const Condition_ptr cond) {
+                _cond = cond;
+                _temporal = _cond->isTemporal();
+                _loop_sensitive = _cond->isLoopSensitive();
+            }
+            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 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;
+            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;
+            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; }
+            const Condition_ptr& operator[](size_t i) const { return _cond; };
+            virtual bool isTemporal() const override { return _temporal;}
+            bool containsNext() const override { return _cond->containsNext(); }
+            bool nestedDeadlock() const override { return _cond->nestedDeadlock(); }
+        private:
+            Condition_ptr _cond;
+            bool _temporal = false;
+        };
+        
+        
+        /******************** TEMPORAL OPERATORS ********************/        
+        
+        class QuantifierCondition : public Condition
+        {
+        public:
+            virtual 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) {
+                _cond = cond;
+                _loop_sensitive = cond->isLoopSensitive();
+            }
+            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 nestedDeadlock() const override { return _cond->nestedDeadlock(); }
+        private:
+            virtual std::string op() const = 0;
+            
+        protected:
+            Condition_ptr _cond;
+        };
+        
+        class EXCondition : 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::X; }
+            uint32_t distance(DistanceContext& context) const override;
+            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; }            
+            uint32_t distance(DistanceContext& context) const override;
+            Result evaluate(const EvaluationContext& context) override;
+            Result evalAndSet(const EvaluationContext& context) override;
+            virtual bool isLoopSensitive() const override { return true; }
+            void visit(Visitor&) const override;
+        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; }            
+            uint32_t distance(DistanceContext& context) const override;
+            Result evaluate(const EvaluationContext& context) override;
+            Result evalAndSet(const EvaluationContext& context) override;
+            void visit(Visitor&) const override;
+        private:
+            std::string op() const override;
+        };
+
+        class AXCondition : 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::A; }
+            Path getPath() const override             { return Path::X; }
+            uint32_t distance(DistanceContext& context) const override;
+            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 AGCondition : 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::A; }
+            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;
+            void visit(Visitor&) const override;
+        private:
+            std::string op() const override;
+        };
+        
+        class AFCondition : 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::A; }
+            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;
+            void visit(Visitor&) const override;
+            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) {
+                _cond1 = cond1;
+                _cond2 = cond2;
+                _loop_sensitive = _cond1->isLoopSensitive() || _cond2->isLoopSensitive();
+            }
+            int formulaSize() const override{
+                return _cond1->formulaSize() + _cond2->formulaSize() + 1;
+            }
+            
+            void analyze(AnalysisContext& context) override;
+            Result evaluate(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;            
+            bool isReachability(uint32_t depth) const override;
+            Condition_ptr prepareForReachability(bool negated) const override;
+            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
+            Result evalAndSet(const EvaluationContext& context) override;
+
+            virtual const Condition_ptr& operator[] (size_t i) const override
+            { if(i == 0) return _cond1; return _cond2;}
+            Path getPath() const override             
+            { return Path::U; }
+            bool containsNext() const override { return _cond1->containsNext() || _cond2->containsNext(); }
+            bool nestedDeadlock() const override { return _cond1->nestedDeadlock() || _cond2->nestedDeadlock(); }
+        private:
+            virtual std::string op() const = 0; 
+            
+        protected:
+            Condition_ptr _cond1;
+            Condition_ptr _cond2;
+        };
+        
+        class EUCondition : public UntilCondition {
+        public:
+            using UntilCondition::UntilCondition;  
+            Retval simplify(SimplificationContext& context) const override;
+            Quantifier getQuantifier() const override { return Quantifier::E; }
+            void visit(Visitor&) const override;
+            uint32_t distance(DistanceContext& context) 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;
+            
+        private:
+            std::string op() const override;
+        };
+        
+        class AUCondition : public UntilCondition {
+        public:
+            using UntilCondition::UntilCondition;
+            Retval simplify(SimplificationContext& context) const override;
+            Quantifier getQuantifier() const override { return Quantifier::A; }            
+            void visit(Visitor&) const override;
+            uint32_t distance(DistanceContext& context) const override;
+            void toXML(std::ostream&, uint32_t tabs) const override;
+            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
+            virtual bool isLoopSensitive() const override { return true; }
+        private:
+            std::string op() const override;
+        };
+        
+        /******************** CONDITIONS ********************/
+
+        class UnfoldedFireableCondition : public ShallowCondition {
+        public:
+            UnfoldedFireableCondition(const std::string& tname) : ShallowCondition(), _name(tname) {};
+            Condition_ptr pushNegation(negstat_t& stat, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
+            void visit(Visitor&) const override;
+        protected:
+            void _analyze(AnalysisContext& context) override;
+            virtual void _toString(std::ostream& out) const;
+            Condition_ptr clone() { return std::make_shared<UnfoldedFireableCondition>(_name); }
+        private:
+            const std::string _name;
+        };
+
+        class FireableCondition : public ShallowCondition {
+        public:
+            FireableCondition(const std::string& tname) : _name(tname) {};
+            Condition_ptr pushNegation(negstat_t& stat, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
+            void visit(Visitor&) const override;
+        protected:
+            void _analyze(AnalysisContext& context) override;
+            virtual void _toString(std::ostream& out) const;
+            Condition_ptr clone() { return std::make_shared<FireableCondition>(_name); }
+        private:
+            const std::string _name;
+        };
+
+        /* Logical conditon */
+        class LogicalCondition : public Condition {
+        public:
+            int formulaSize() const override {
+                size_t i = 1;
+                for(auto& c : _conds) i += c->formulaSize();
+                return i;
+            }
+            void analyze(AnalysisContext& context) override;
+            
+            uint32_t distance(DistanceContext& context) const override;
+            void toString(std::ostream&) const override;
+            void toBinary(std::ostream& out) const override;
+            void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
+            bool isReachability(uint32_t depth) const override;
+            Condition_ptr prepareForReachability(bool negated) const override;
+            const Condition_ptr& operator[](size_t i) const
+            { 
+                return _conds[i];
+            };            
+            CTLType getQueryType() const override { return CTLType::LOPERATOR; }
+            Path getPath() const override         { return Path::pError; }
+            
+            bool isTemporal() const override
+            {
+                return _temporal;
+            }
+            auto begin() { return _conds.begin(); }
+            auto end() { return _conds.end(); }
+            auto begin() const { return _conds.begin(); }
+            auto end() const { return _conds.end(); }
+            bool empty() const { return _conds.size() == 0; }
+            bool singular() const { return _conds.size() == 1; }
+            size_t size() const { return _conds.size(); }
+            bool containsNext() const override 
+            { return std::any_of(begin(), end(), [](auto& a){return a->containsNext();}); }
+            bool nestedDeadlock() const override;
+
+        protected:
+            LogicalCondition() {};
+            Retval simplifyOr(SimplificationContext& context) const;
+            Retval simplifyAnd(SimplificationContext& context) const;                  
+
+        private:
+            virtual uint32_t delta(uint32_t d1, uint32_t d2, const DistanceContext& context) const = 0;
+            virtual std::string op() const = 0;
+            
+        protected:
+            bool _temporal = false;
+            std::vector<Condition_ptr> _conds;
+        };
+
+        /* Conjunctive and condition */
+        class AndCondition : public LogicalCondition {
+        public:
+
+            AndCondition(std::vector<Condition_ptr>&& conds);
+
+            AndCondition(const std::vector<Condition_ptr>& conds);
+            
+            AndCondition(Condition_ptr left, Condition_ptr right);
+            
+            Retval simplify(SimplificationContext& context) const override;
+            Result evaluate(const EvaluationContext& context) override;
+            Result evalAndSet(const EvaluationContext& context) override;
+            void visit(Visitor&) const override;
+            void toXML(std::ostream&, uint32_t tabs) const override;
+            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
+            Quantifier getQuantifier() const override { return Quantifier::AND; }
+            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
+        private:
+            //int logicalOp() const;
+            uint32_t delta(uint32_t d1, uint32_t d2, const DistanceContext& context) const override;
+            std::string op() const override;
+        };
+
+        /* Disjunctive or conditon */
+        class OrCondition : public LogicalCondition {
+        public:
+
+            OrCondition(std::vector<Condition_ptr>&& conds);
+
+            OrCondition(const std::vector<Condition_ptr>& conds);
+
+            OrCondition(Condition_ptr left, Condition_ptr right);
+            
+            Retval simplify(SimplificationContext& context) const override;
+            Result evaluate(const EvaluationContext& context) override;
+            Result evalAndSet(const EvaluationContext& context) override;
+            void visit(Visitor&) const override;
+            void toXML(std::ostream&, uint32_t tabs) const override;
+            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;   
+            Quantifier getQuantifier() const override { return Quantifier::OR; }
+            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
+        private:
+            //int logicalOp() const;
+            uint32_t delta(uint32_t d1, uint32_t d2, const DistanceContext& context) const override;
+            std::string op() const override;
+        };
+
+        class CompareConjunction : public Condition
+        {
+        public:
+            struct cons_t {
+                int32_t _place  = -1;
+                uint32_t _upper = std::numeric_limits<uint32_t>::max();
+                uint32_t _lower = 0;
+                std::string _name;
+                bool operator<(const cons_t& other) const
+                {
+                    return _place < other._place;
+                }
+                
+                void invert()
+                {
+                    if(_lower == 0 && _upper == std::numeric_limits<uint32_t>::max())
+                        return;
+                    assert(_lower == 0 || _upper == std::numeric_limits<uint32_t>::max());
+                    if(_lower == 0)
+                    {
+                        _lower = _upper + 1;
+                        _upper = std::numeric_limits<uint32_t>::max();
+                    }
+                    else if(_upper == std::numeric_limits<uint32_t>::max())
+                    {
+                        _upper = _lower - 1;
+                        _lower = 0;
+                    }
+                    else
+                    {
+                        assert(false);
+                    }
+                }
+                
+                void intersect(const cons_t& other)
+                {
+                    _lower = std::max(_lower, other._lower);
+                    _upper = std::min(_upper, other._upper);
+                }
+            };
+
+            CompareConjunction(bool negated = false) 
+                    : _negated(false) {};
+            friend FireableCondition;
+            CompareConjunction(const std::vector<cons_t>&& cons, bool negated) 
+                    : _constraints(cons), _negated(negated) {};
+            CompareConjunction(const std::vector<Condition_ptr>&, bool negated);
+            CompareConjunction(const CompareConjunction& other, bool negated = false)
+            : _constraints(other._constraints), _negated(other._negated != negated)
+            {
+            };
+
+            void merge(const CompareConjunction& other);
+            void merge(const std::vector<Condition_ptr>&, bool negated);
+            
+            int formulaSize() const override{
+                int sum = 0;
+                for(auto& c : _constraints)
+                {
+                    assert(c._place >= 0);
+                    if(c._lower == c._upper) ++sum;
+                    else {
+                        if(c._lower != 0) ++sum;
+                        if(c._upper != std::numeric_limits<uint32_t>::max()) ++sum;
+                    }
+                }
+                if(sum == 1) return 2;
+                else return (sum*2) + 1;
+            }
+            void analyze(AnalysisContext& context) override;
+            uint32_t distance(DistanceContext& context) const override;
+            void toString(std::ostream& stream) const override;
+            void toTAPAALQuery(std::ostream& stream,TAPAALConditionExportContext& context) const override;
+            void toBinary(std::ostream& out) const override;
+            bool isReachability(uint32_t depth) const override { return depth > 0; };
+            Condition_ptr prepareForReachability(bool negated) const override;
+            CTLType getQueryType() const override { return CTLType::LOPERATOR; }
+            Path getPath() const override         { return Path::pError; }            
+            virtual void toXML(std::ostream& stream, uint32_t tabs) const override;
+            Retval simplify(SimplificationContext& context) const override;
+            Result evaluate(const EvaluationContext& context) override;
+            Result evalAndSet(const EvaluationContext& context) override;
+            void visit(Visitor&) const override;
+            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;   
+            Quantifier getQuantifier() const override { return _negated ? Quantifier::OR : Quantifier::AND; }
+            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
+            bool isNegated() const { return _negated; }
+            bool singular() const 
+            { 
+                return _constraints.size() == 1 && 
+                                    (_constraints[0]._lower == 0 || 
+                                     _constraints[0]._upper == std::numeric_limits<uint32_t>::max());
+            };
+            bool containsNext() const override { return false;}
+            bool nestedDeadlock() const override { return false; }
+            const std::vector<cons_t>& constraints() const { return _constraints; }
+            std::vector<cons_t>::const_iterator begin() const { return _constraints.begin(); }
+            std::vector<cons_t>::const_iterator end() const { return _constraints.end(); }
+        private:
+            std::vector<cons_t> _constraints;
+            bool _negated = false;
+        };
+
+
+        /* Comparison conditon */
+        class CompareCondition : public Condition {
+        public:
+
+            CompareCondition(const Expr_ptr expr1, const Expr_ptr expr2)
+            : _expr1(expr1), _expr2(expr2) {}
+
+            int formulaSize() const override{
+                return _expr1->formulaSize() + _expr2->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;
+            bool isReachability(uint32_t depth) const override;
+            Condition_ptr prepareForReachability(bool negated) const override;
+            Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
+            Path getPath() const override { return Path::pError; }
+            CTLType getQueryType() const override { return CTLType::EVAL; }
+            const Expr_ptr& operator[](uint32_t id) const
+            {
+                if(id == 0) return _expr1;
+                else return _expr2;
+            }
+            bool containsNext() const override { return false; }
+            bool nestedDeadlock() const override { return false; }
+            bool isTrivial() const;
+        protected:
+            uint32_t _distance(DistanceContext& c, 
+                    std::function<uint32_t(uint32_t, uint32_t, bool)> d) const
+            {
+                return d(_expr1->evaluate(c), _expr2->evaluate(c), c.negated());
+            }
+        private:
+            virtual bool apply(int v1, int v2) const = 0;
+            virtual std::string op() const = 0;
+            /** Operator when exported to TAPAAL */
+            virtual std::string opTAPAAL() const = 0;
+            /** Swapped operator when exported to TAPAAL, e.g. operator when operands are swapped */
+            virtual std::string sopTAPAAL() const = 0;
+
+        protected:
+            Expr_ptr _expr1;
+            Expr_ptr _expr2;
+        };
+
+        /* delta */
+        template<typename T>
+        uint32_t delta(int v1, int v2, bool negated)
+        { return 0; }
+        
+        class EqualCondition : public CompareCondition {
+        public:
+
+            using CompareCondition::CompareCondition;
+            Retval simplify(SimplificationContext& context) const override;
+            void toXML(std::ostream&, uint32_t tabs) const override;
+            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
+            uint32_t distance(DistanceContext& context) const override;
+            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
+            void visit(Visitor&) const override;
+        private:
+            bool apply(int v1, int v2) const override;
+            std::string op() const override;
+            std::string opTAPAAL() const override;
+            std::string sopTAPAAL() const override;
+        };
+
+        /* None equality conditon */
+        class NotEqualCondition : public CompareCondition {
+        public:
+
+            using CompareCondition::CompareCondition;
+            void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
+            Retval simplify(SimplificationContext& context) const override;
+            void toXML(std::ostream&, uint32_t tabs) const override;
+            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
+            uint32_t distance(DistanceContext& context) const override;
+            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
+            void visit(Visitor&) const override;
+        private:
+            bool apply(int v1, int v2) const override;
+            std::string op() const override;
+            std::string opTAPAAL() const override;
+            std::string sopTAPAAL() const override;
+        };
+
+        /* Less-than conditon */
+        class LessThanCondition : public CompareCondition {
+        public:
+
+            using CompareCondition::CompareCondition;
+            Retval simplify(SimplificationContext& context) const override;
+            void toXML(std::ostream&, uint32_t tabs) const override;
+            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
+            uint32_t distance(DistanceContext& context) const override;
+            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
+            void visit(Visitor&) const override;
+        private:
+            bool apply(int v1, int v2) const override;
+            std::string op() const override;
+            std::string opTAPAAL() const override;
+            std::string sopTAPAAL() const override;
+        };
+
+        /* Less-than-or-equal conditon */
+        class LessThanOrEqualCondition : public CompareCondition {
+        public:
+
+            using CompareCondition::CompareCondition;
+            Retval simplify(SimplificationContext& context) const override;
+            void toXML(std::ostream&, uint32_t tabs) const override;
+            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
+            uint32_t distance(DistanceContext& context) const override;
+            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
+            void visit(Visitor&) const override;
+        private:
+            bool apply(int v1, int v2) const override;
+            std::string op() const override;
+            std::string opTAPAAL() const override;
+            std::string sopTAPAAL() const override;
+        };
+
+        /* Greater-than conditon */
+        class GreaterThanCondition : public CompareCondition {
+        public:
+
+            using CompareCondition::CompareCondition;
+            Retval simplify(SimplificationContext& context) const override;
+            void toXML(std::ostream&, uint32_t tabs) const override;
+            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
+            uint32_t distance(DistanceContext& context) const override;
+            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
+            void visit(Visitor&) const override;
+        private:
+            bool apply(int v1, int v2) const override;
+            std::string op() const override;
+            std::string opTAPAAL() const override;
+            std::string sopTAPAAL() const override;
+        };
+
+        /* Greater-than-or-equal conditon */
+        class GreaterThanOrEqualCondition : public CompareCondition {
+        public:
+            using CompareCondition::CompareCondition;
+            Retval simplify(SimplificationContext& context) const override;
+            void toXML(std::ostream&, uint32_t tabs) const override;
+            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
+            uint32_t distance(DistanceContext& context) const override;
+            Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
+            void visit(Visitor&) const override;
+        private:
+            bool apply(int v1, int v2) const override;
+            std::string op() const override;
+            std::string opTAPAAL() const override;
+            std::string sopTAPAAL() const override;
+        };
+
+        /* Bool condition */
+        class BooleanCondition : public Condition {
+        public:
+
+            BooleanCondition(bool value) : _value(value) {
+                if (value) {
+                    trivial = 1;
+                } else {
+                    trivial = 2;
+                }
+            }
+            int formulaSize() const override{
+                return 0;
+            }
+            void analyze(AnalysisContext& context) override;
+            Result evaluate(const EvaluationContext& context) override;
+            Result evalAndSet(const EvaluationContext& context) override;
+            void visit(Visitor&) const override;           
+            uint32_t distance(DistanceContext& context) const override;
+            static Condition_ptr TRUE_CONSTANT;
+            static Condition_ptr FALSE_CONSTANT;
+            void toString(std::ostream&) const override;
+            void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
+            static Condition_ptr getShared(bool val);
+            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;
+            void toBinary(std::ostream&) const override;
+            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
+            Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
+            Path getPath() const override { return Path::pError; }
+            CTLType getQueryType() const override { return CTLType::EVAL; }
+            bool containsNext() const override { return false; }
+            bool nestedDeadlock() const override { return false; }
+        private:
+            const bool _value;
+        };
+
+        /* Deadlock condition */
+        class DeadlockCondition : public Condition {
+        public:
+
+            DeadlockCondition() {
+                _loop_sensitive = true;
+            }
+            int formulaSize() const override{
+                return 1;
+            }
+            void analyze(AnalysisContext& context) override;
+            Result evaluate(const EvaluationContext& context) override;
+            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;
+            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;
+            void toBinary(std::ostream&) const override;
+            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
+            static Condition_ptr DEADLOCK;
+            Quantifier getQuantifier() const override { return Quantifier::DEADLOCK; }
+            Path getPath() const override { return Path::pError; }
+            CTLType getQueryType() const override { return CTLType::EVAL; }
+            bool containsNext() const override { return false; }
+            bool nestedDeadlock() const override { return false; }
+        };
+
+        class KSafeCondition : public ShallowCondition
+        {
+        public:
+            KSafeCondition(const Expr_ptr& expr1) : _bound(expr1)
+            {}
+
+        protected:
+            void _analyze(AnalysisContext& context) override;
+            void _toString(std::ostream& out) const override;
+            void visit(Visitor&) const override;
+            Condition_ptr clone() override
+            {
+                return std::make_shared<KSafeCondition>(_bound);
+            }
+        private:
+            Expr_ptr _bound = nullptr;
+        };
+
+        class LivenessCondition : public ShallowCondition
+        {
+        public:
+            LivenessCondition() {}
+        protected:
+            void _analyze(AnalysisContext& context) override;
+            void _toString(std::ostream& out) const override;
+            void visit(Visitor&) const override;
+            Condition_ptr clone() override { return std::make_shared<LivenessCondition>(); }
+        };
+
+        class QuasiLivenessCondition : public ShallowCondition
+        {
+        public:
+            QuasiLivenessCondition() {}
+        protected:
+            void _analyze(AnalysisContext& context) override;
+            void _toString(std::ostream& out) const override;
+            void visit(Visitor&) const override;
+            Condition_ptr clone() override { return std::make_shared<QuasiLivenessCondition>(); }
+        };
+
+        class StableMarkingCondition : public ShallowCondition
+        {
+        public:
+            StableMarkingCondition() {}
+        protected:
+            void _analyze(AnalysisContext& context) override;
+            void _toString(std::ostream& out) const override;
+            void visit(Visitor&) const override;
+            Condition_ptr clone() override { return std::make_shared<StableMarkingCondition>(); }
+        };
+
+        class UpperBoundsCondition : public ShallowCondition
+        {
+        public:
+            
+            UpperBoundsCondition(const std::vector<std::string>& places) : _places(places)
+            {}
+        protected:
+            void _toString(std::ostream& out) const override;
+            void _analyze(AnalysisContext& context) override;
+            void visit(Visitor&) const override;
+            Condition_ptr clone() override
+            {
+                return std::make_shared<UpperBoundsCondition>(_places);
+            }
+
+        private:
+            std::vector<std::string> _places;
+        };
+
+        class UnfoldedUpperBoundsCondition : public Condition
+        {
+        public:
+            struct place_t {
+                std::string _name;
+                uint32_t _place = 0;
+                double _max = std::numeric_limits<double>::infinity();
+                bool _maxed_out = false;
+                place_t(const std::string& name)
+                {
+                    _name = name;
+                }
+                place_t(const place_t& other, double max)
+                {
+                    _name = other._name;
+                    _place = other._place;
+                    _max = max;
+                }
+                bool operator<(const place_t& other) const{
+                    return _place < other._place;
+                }
+            };
+            
+            UnfoldedUpperBoundsCondition(const std::vector<std::string>& places)
+            {
+                for(auto& s : places) _places.push_back(s);
+            }
+            UnfoldedUpperBoundsCondition(const std::vector<place_t>& places, double max, double offset)
+                    : _places(places), _max(max), _offset(offset) {
+            };
+            int formulaSize() const override{
+                return _places.size();
+            }
+            void analyze(AnalysisContext& context) override;
+            size_t value(const MarkVal*);
+            Result evaluate(const EvaluationContext& context) override;
+            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;
+            void toBinary(std::ostream&) const 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;
+            void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
+            Quantifier getQuantifier() const override { return Quantifier::UPPERBOUNDS; }
+            Path getPath() const override { return Path::pError; }
+            CTLType getQueryType() const override { return CTLType::EVAL; }
+            bool containsNext() const override { return false; }
+            bool nestedDeadlock() const override { return false; }
+            
+            double bounds(bool add_offset = true) const { 
+                return (add_offset ? _offset : 0 ) + _bound; 
+            }
+            
+            virtual void setUpperBound(size_t bound)
+            {
+                _bound = std::max(_bound, bound);
+            }
+            
+            const std::vector<place_t>& places() const { return _places; }
+            
+        private:
+            std::vector<place_t> _places;
+            size_t _bound = 0;
+            double _max = std::numeric_limits<double>::infinity();
+            double _offset = 0;
+        };
+
+    }
+}
+
+
+
+#endif // EXPRESSIONS_H
 
=== added file 'include/PetriEngine/PQL/PQL.h'
--- include/PetriEngine/PQL/PQL.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/PQL/PQL.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,285 @@
+/* PeTe - Petri Engine exTremE
+ * Copyright (C) 2011  Jonas Finnemann Jensen <[e-mail]>,
+ *                     Thomas Søndersø Nielsen <[e-mail]>,
+ *                     Lars Kærlund Østergaard <[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 PQL_H
+#define PQL_H
+#include <string>
+#include <list>
+#include <vector>
+#include <algorithm>
+#include <unordered_map>
+#include <memory>
+
+#include "../PetriNet.h"
+#include "../Structures/State.h"
+#include "../ReducingSuccessorGenerator.h"
+#include "../Simplification/LPCache.h"
+
+namespace PetriEngine {
+    class ReducingSuccessorGenerator;
+    namespace Simplification
+    {
+        class Member;
+        struct Retval;
+    }
+    namespace PQL {
+        class Visitor;
+        
+        enum CTLType {PATHQEURY = 1, LOPERATOR = 2, EVAL = 3, TYPE_ERROR = -1};
+        enum Quantifier { AND = 1, OR = 2, A = 3, E = 4, NEG = 5, COMPCONJ = 6, DEADLOCK = 7, UPPERBOUNDS = 8, PN_BOOLEAN = 9, EMPTY = -1 };
+        enum Path { G = 1, X = 2, F = 3, U = 4, pError = -1 };
+        
+        
+        class AnalysisContext;
+        class EvaluationContext;
+        class DistanceContext;
+        class TAPAALConditionExportContext;
+        class SimplificationContext;
+
+        /** Representation of a PQL error */
+        class ExprError {
+            std::string _text;
+            int _length;
+        public:
+
+            ExprError(std::string text = "", int length = 0) {
+                _text = text;
+                _length = length;
+            }
+
+            /** Human readable explaination of the error */
+            const std::string& text() const {
+                return _text;
+            }
+
+            /** length in the source, 0 if not applicable */
+            int length() const {
+                return _length;
+            }
+
+            /** Convert error to string */
+            std::string toString() const {
+                return "Parsing error \"" + text() + "\"";
+            }
+
+            /** True, if this is a default created ExprError without any information */
+            bool isEmpty() const {
+                return _text.empty() && _length == 0;
+            }
+        };
+
+        /** Representation of an expression */
+        class Expr {
+            int _eval = 0;
+        public:
+            /** Types of expressions */
+            enum Types {
+                /** Binary addition expression */
+                PlusExpr,
+                /** Binary subtraction expression */
+                SubtractExpr,
+                /** Binary multiplication expression */
+                MultiplyExpr,
+                /** Unary minus expression */
+                MinusExpr,
+                /** Literal integer expression */
+                LiteralExpr,
+                /** Identifier expression */
+                IdentifierExpr
+            };
+        public:
+            /** Virtual destructor, an expression should know it subexpressions */
+            virtual ~Expr();
+            /** Perform context analysis */
+            virtual void analyze(AnalysisContext& context) = 0;
+            /** Evaluate the expression given marking and assignment */
+            virtual int evaluate(const EvaluationContext& context) = 0;
+            int evalAndSet(const EvaluationContext& context);
+            virtual void visit(Visitor& visitor) const = 0;
+            /** Convert expression to string */
+            virtual void toString(std::ostream&) const = 0;
+            /** Expression type */
+            virtual Types type() const = 0;
+            /** Construct left/right side of equations used in query simplification */
+            virtual Simplification::Member constraint(SimplificationContext& context) const = 0;
+            /** Output the expression as it currently is to a file in XML */
+            virtual void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const = 0;
+            virtual void toBinary(std::ostream&) const = 0;
+            /** Stubborn reduction: increasing and decreasing sets */
+            virtual void incr(ReducingSuccessorGenerator& generator) const = 0;
+            virtual void decr(ReducingSuccessorGenerator& generator) const = 0;
+            /** Count size of the entire formula in number of nodes */
+            virtual int formulaSize() const = 0;
+            
+            virtual bool placeFree() const = 0;
+            
+            void setEval(int eval) {
+                _eval = eval;
+            }
+            
+            int getEval() const {
+                return _eval;
+            }
+        };
+/******************* NEGATION PUSH STATS  *******************/
+        
+        struct negstat_t
+        {
+            negstat_t()
+            {
+                for(size_t i = 0; i < 31; ++i) _used[i] = 0;
+            }
+            void print(std::ostream& stream)
+            {
+                for(size_t i = 0; i < 31; ++i) stream << _used[i] << ",";                
+            }
+            void printRules(std::ostream& stream)
+            {
+                for(size_t i = 0; i < 31; ++i) stream << _rulename[i] << ",";                
+            }
+            int _used[31];
+            const std::vector<const char*> _rulename = {
+                "EG p-> !EF !p",
+                "AG p-> !AF !p",
+                "!EX p -> AX p",
+                "EX false -> false",
+                "EX true -> !deadlock",
+                "!AX p -> EX p",
+                "AX false -> deadlock",
+                "AX true -> true",             
+                "EF !deadlock -> !deadlock",
+                "EF EF p -> EF p",
+                "EF AF p -> AF p",
+                "EF E p U q -> EF q",
+                "EF A p U q -> EF q",
+                "EF .. or .. -> EF .. or EF ..",
+                "AF !deadlock -> !deadlock",
+                "AF AF p -> AF p",
+                "AF EF p -> EF p",
+                "AF .. or EF p -> EF p or AF ..",
+                "AF A p U q -> AF q",
+                "A p U !deadlock -> !deadlock",
+                "A deadlock U q -> q",
+                "A !deadlock U q -> AF q",
+                "A p U AF q -> AF q",
+                "A p U EF q -> EF q",
+                "A p U .. or EF q -> EF q or A p U ..",
+                "E p U !deadlock -> !deadlock",
+                "E deadlock U q -> q",
+                "E !deadlock U q -> EF q",
+                "E p U EF q -> EF q",
+                "E p U .. or EF q -> EF q or E p U ..",
+                "!! p -> p"
+                
+            };
+            int& operator[](size_t i) { return _used[i]; }
+            bool negated_fireability = false;
+        };
+        
+        /** Base condition */
+        class Condition {
+        public:
+            enum Result {RUNKNOWN=-1,RFALSE=0,RTRUE=1};
+        private:
+            bool _inv = false;
+            Result _eval = RUNKNOWN;
+        protected:
+            bool _loop_sensitive = false;            
+        public:
+            /** Virtual destructor */
+            virtual ~Condition();
+            /** Perform context analysis  */
+            virtual void analyze(AnalysisContext& context) = 0;
+            /** Evaluate condition */
+            virtual Result evaluate(const EvaluationContext& context) = 0;
+            virtual Result evalAndSet(const EvaluationContext& context) = 0;
+            virtual void visit(Visitor& visitor) const = 0;
+            
+            /** Convert condition to string */
+            virtual void toString(std::ostream&) const = 0;
+            /** Export condition to TAPAAL query (add EF manually!) */
+            virtual void toTAPAALQuery(std::ostream&, TAPAALConditionExportContext& context) const = 0;
+            /** Get distance to query */
+            virtual uint32_t distance(DistanceContext& context) const = 0;
+            /** Query Simplification */
+            virtual Simplification::Retval simplify(SimplificationContext& context) const = 0;
+            /** Check if query is a reachability query */
+            virtual bool isReachability(uint32_t depth = 0) const = 0;
+
+            virtual bool isLoopSensitive() const { return _loop_sensitive; };
+            /** Prepare reachability queries */
+            virtual std::shared_ptr<Condition> prepareForReachability(bool negated = false) const = 0;
+            virtual std::shared_ptr<Condition> pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated = false, bool initrw = true) = 0;
+            
+            /** Output the condition as it currently is to a file in XML */
+            virtual void toXML(std::ostream&, uint32_t tabs) const = 0;
+            virtual void toBinary(std::ostream& out) const = 0;
+
+            /** Find interesting transitions in stubborn reduction*/
+            virtual void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const = 0;
+            /** Checks if the condition is trivially true */
+            bool isTriviallyTrue();
+            /*** Checks if the condition is trivially false */
+            bool isTriviallyFalse();
+            /** Count size of the entire formula in number of nodes */
+            virtual int formulaSize() const = 0;
+
+            bool isSatisfied() const
+            {
+                return _eval == RTRUE;
+            }
+            
+            void setSatisfied(bool isSatisfied)
+            {
+                _eval = isSatisfied ? RTRUE : RFALSE;
+            }
+            
+            void setSatisfied(Result isSatisfied)
+            {
+                _eval = isSatisfied;
+            }
+            
+            void setInvariant(bool isInvariant)
+            {
+                _inv = isInvariant;
+            }
+           
+            bool isInvariant()
+            {
+                return _inv;
+            }
+            
+            virtual bool isTemporal() const { return false;}
+            virtual CTLType getQueryType() const = 0;
+            virtual Quantifier getQuantifier() const = 0;
+            virtual Path getPath() const = 0;
+            static std::shared_ptr<Condition> 
+            initialMarkingRW(const std::function<std::shared_ptr<Condition> ()>& func, negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw);
+            virtual bool containsNext() const = 0;   
+            virtual bool nestedDeadlock() const = 0;
+        protected:
+            //Value for checking if condition is trivially true or false.
+            //0 is undecided (default), 1 is true, 2 is false.
+            uint32_t trivial = 0;
+        };
+        typedef std::shared_ptr<Condition> Condition_ptr;
+        typedef std::shared_ptr<Expr> Expr_ptr;
+    } // PQL
+} // PetriEngine
+
+#endif // PQL_H
 
=== added file 'include/PetriEngine/PQL/PQLParser.h'
--- include/PetriEngine/PQL/PQLParser.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/PQL/PQLParser.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,34 @@
+/* PeTe - Petri Engine exTremE
+ * Copyright (C) 2011  Jonas Finnemann Jensen <[e-mail]>,
+ *                     Thomas Søndersø Nielsen <[e-mail]>,
+ *                     Lars Kærlund Østergaard <[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 PQLPARSER_H
+#define PQLPARSER_H
+
+#include <string>
+#include <memory>
+#include <vector>
+
+namespace PetriEngine {
+    namespace PQL {
+
+        class Condition;
+
+        std::shared_ptr<Condition> ParseQuery(const std::string& queryString, std::vector<std::string>& placenameforbound);
+    }
+}
+#endif // PQLPARSER_H
 
=== added file 'include/PetriEngine/PQL/Visitor.h'
--- include/PetriEngine/PQL/Visitor.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/PQL/Visitor.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,101 @@
+/*
+ *  Copyright Peter G. Jensen, all rights reserved.
+ */
+
+/* 
+ * File:   Visitor.h
+ * Author: Peter G. Jensen <[e-mail]>
+ *
+ * Created on April 11, 2020, 1:07 PM
+ */
+
+#ifndef VISITOR_H
+#define VISITOR_H
+
+#include "PetriEngine/PQL/Expressions.h"
+#include <type_traits>
+
+namespace PetriEngine
+{
+    namespace PQL
+    {
+        class Visitor {
+        public:
+            Visitor() {}
+
+            template<typename T>
+            void accept(T element)
+            {
+                _accept(element);
+            }
+
+        protected:
+
+            virtual void _accept(const NotCondition* element) = 0;
+            virtual void _accept(const AndCondition* element) = 0;
+            virtual void _accept(const OrCondition* element) = 0;
+            virtual void _accept(const LessThanCondition* element) = 0;
+            virtual void _accept(const LessThanOrEqualCondition* element) = 0;
+            virtual void _accept(const GreaterThanCondition* element) = 0;
+            virtual void _accept(const GreaterThanOrEqualCondition* element) = 0;
+            virtual void _accept(const EqualCondition* element) = 0;
+            virtual void _accept(const NotEqualCondition* element) = 0;
+
+            virtual void _accept(const DeadlockCondition* element) = 0;
+            virtual void _accept(const CompareConjunction* element) = 0;
+            virtual void _accept(const UnfoldedUpperBoundsCondition* element) = 0;
+            
+            // Quantifiers, most uses of the visitor will not use the quantifiers - so we give a default implementation.
+            // default behaviour is error
+            virtual void _accept(const EFCondition*)
+            {   assert(false); std::cerr << "No accept for EFCondition" << std::endl; exit(0);};
+            virtual void _accept(const EGCondition*)
+            {   assert(false); std::cerr << "No accept for EGCondition" << std::endl; exit(0);};
+            virtual void _accept(const AGCondition*)
+            {   assert(false); std::cerr << "No accept for AGCondition" << std::endl; exit(0);};
+            virtual void _accept(const AFCondition*)
+            {   assert(false); std::cerr << "No accept for AFCondition" << std::endl; exit(0);};
+            virtual void _accept(const EXCondition*)
+            {   assert(false); std::cerr << "No accept for EXCondition" << std::endl; exit(0);};            
+            virtual void _accept(const AXCondition*)
+            {   assert(false); std::cerr << "No accept for AXCondition" << std::endl; exit(0);};            
+            virtual void _accept(const EUCondition*)
+            {   assert(false); std::cerr << "No accept for EUCondition" << std::endl; exit(0);};
+            virtual void _accept(const AUCondition*)
+            {   assert(false); std::cerr << "No accept for AUCondition" << std::endl; exit(0);};            
+            
+            // shallow elements, neither of these should exist in a compiled expression
+            virtual void _accept(const UnfoldedFireableCondition* element) 
+            {   assert(false); std::cerr << "No accept for UnfoldedFireableCondition" << std::endl; exit(0);};
+            virtual void _accept(const FireableCondition* element)
+            {   assert(false); std::cerr << "No accept for FireableCondition" << std::endl; exit(0);};            
+            virtual void _accept(const UpperBoundsCondition* element)
+            {   assert(false); std::cerr << "No accept for UpperBoundsCondition" << std::endl; exit(0);};
+            virtual void _accept(const LivenessCondition* element)
+            {   assert(false); std::cerr << "No accept for LivenessCondition" << std::endl; exit(0);};
+            virtual void _accept(const KSafeCondition* element)
+            {   assert(false); std::cerr << "No accept for KSafeCondition" << std::endl; exit(0);};
+            virtual void _accept(const QuasiLivenessCondition* element)
+            {   assert(false); std::cerr << "No accept for QuasiLivenessCondition" << std::endl; exit(0);};
+            virtual void _accept(const StableMarkingCondition* element)
+            {   assert(false); std::cerr << "No accept for StableMarkingCondition" << std::endl; exit(0);};
+            virtual void _accept(const BooleanCondition* element)
+            {   assert(false); std::cerr << "No accept for BooleanCondition" << std::endl; exit(0);};
+            
+            // Expression
+            virtual void _accept(const UnfoldedIdentifierExpr* element) = 0;
+            virtual void _accept(const LiteralExpr* element) = 0;
+            virtual void _accept(const PlusExpr* element) = 0;
+            virtual void _accept(const MultiplyExpr* element) = 0;
+            virtual void _accept(const MinusExpr* element) = 0;
+            virtual void _accept(const SubtractExpr* element) = 0;
+            
+            // shallow expression, default to error
+            virtual void _accept(const IdentifierExpr* element)
+            {   assert(false); std::cerr << "No accept for IdentifierExpr" << std::endl; exit(0);};
+        }; 
+    }
+}
+
+#endif /* VISITOR_H */
+
 
=== added file 'include/PetriEngine/PetriNet.h'
--- include/PetriEngine/PetriNet.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/PetriNet.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,136 @@
+/* PeTe - Petri Engine exTremE
+ * Copyright (C) 2011  Jonas Finnemann Jensen <[e-mail]>,
+ *                     Thomas Søndersø Nielsen <[e-mail]>,
+ *                     Lars Kærlund Østergaard <[e-mail]>,
+ *                     Peter Gjøl Jensen <[e-mail]>
+ * 
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ * 
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ * 
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+#ifndef PETRINET_H
+#define PETRINET_H
+
+#include <string>
+#include <vector>
+#include <climits>
+#include <limits>
+#include <iostream>
+
+namespace PetriEngine {
+
+    namespace PQL {
+        class Condition;
+    }
+
+    namespace Structures {
+        class State;
+    }
+
+    class PetriNetBuilder;
+    class SuccessorGenerator;
+    
+    struct TransPtr {
+        uint32_t inputs;
+        uint32_t outputs;
+    };
+    
+    struct Invariant {
+        uint32_t place;
+        uint32_t tokens;
+        bool inhibitor;
+        int8_t direction;
+        // we can pack things here, but might give slowdown
+    } /*__attribute__((packed))*/; 
+    
+    /** Type used for holding markings values */
+    typedef uint32_t MarkVal;
+
+    /** Efficient representation of PetriNet */
+    class PetriNet {
+        PetriNet(uint32_t transitions, uint32_t invariants, uint32_t places);
+    public:
+        ~PetriNet();
+
+        uint32_t initial(size_t id) const;
+        MarkVal* makeInitialMarking() const;
+        /** Fire transition if possible and store result in result */
+        bool deadlocked(const MarkVal* marking) const;
+        bool fireable(const MarkVal* marking, int transitionIndex);
+        std::pair<const Invariant*, const Invariant*> preset(uint32_t id) const;
+        std::pair<const Invariant*, const Invariant*> postset(uint32_t id) const;
+        uint32_t numberOfTransitions() const {
+            return _ntransitions;
+        }
+
+        uint32_t numberOfPlaces() const {
+            return _nplaces;
+        }
+        int inArc(uint32_t place, uint32_t transition) const;
+        int outArc(uint32_t transition, uint32_t place) const;
+        
+
+        const std::vector<std::string>& transitionNames() const
+        {
+            return _transitionnames;
+        }
+        
+        const std::vector<std::string>& placeNames() const
+        {
+            return _placenames;
+        }
+               
+        void print(MarkVal const * const val) const
+        {
+            for(size_t i = 0; i < _nplaces; ++i)
+            {
+                if(val[i] != 0)
+                {
+                    std::cout << _placenames[i] << "(" << i << ")" << " -> " << val[i] << std::endl;
+                }
+            }
+        }
+        
+        void sort();
+        
+        void toXML(std::ostream& out);
+        
+        const MarkVal* initial() const {
+            return _initialMarking;
+        }
+
+    private:        
+
+        /** Number of x variables
+         * @remarks We could also get this from the _places vector, but I don't see any
+         * any complexity garentees for this type.
+         */
+        uint32_t _ninvariants, _ntransitions, _nplaces;
+
+        std::vector<TransPtr> _transitions;
+        std::vector<Invariant> _invariants;
+        std::vector<uint32_t> _placeToPtrs;
+        MarkVal* _initialMarking;
+
+        std::vector<std::string> _transitionnames;
+        std::vector<std::string> _placenames;
+
+        friend class PetriNetBuilder;
+        friend class Reducer;
+        friend class SuccessorGenerator;
+        friend class ReducingSuccessorGenerator;
+        friend class STSolver;
+    };
+
+} // PetriEngine
+
+#endif // PETRINET_H
 
=== added file 'include/PetriEngine/PetriNetBuilder.h'
--- include/PetriEngine/PetriNetBuilder.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/PetriNetBuilder.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,145 @@
+/* PeTe - Petri Engine exTremE
+ * Copyright (C) 2011  Jonas Finnemann Jensen <[e-mail]>,
+ *                     Thomas Søndersø Nielsen <[e-mail]>,
+ *                     Lars Kærlund Østergaard <[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 PETRINETBUILDER_H
+#define PETRINETBUILDER_H
+
+#include <vector>
+#include <string>
+#include <memory>
+#include <chrono>
+#include "AbstractPetriNetBuilder.h"
+#include "PQL/PQL.h"
+#include "PetriNet.h"
+#include "Reducer.h"
+#include "NetStructures.h"
+#include "Reachability/ReachabilityResult.h"
+namespace PetriEngine {
+    /** Builder for building engine representations of PetriNets */
+    class PetriNetBuilder : public AbstractPetriNetBuilder {
+    public:
+        friend class Reducer;
+        
+    public:
+        PetriNetBuilder();
+        PetriNetBuilder(const PetriNetBuilder& other);
+        void addPlace(const std::string& name, int tokens, double x, double y) override;
+        void addTransition(const std::string& name,
+                double x,
+                double y) override;
+        void addInputArc(const std::string& place,
+                const std::string& transition,
+                bool inhibitor,
+                int weight) override;
+        void addOutputArc(const std::string& transition, const std::string& place, int weight) override;
+
+        virtual void sort() override;
+        /** Make the resulting petri net, you take ownership */
+        PetriNet* makePetriNet(bool reorder = true);
+        /** Make the resulting initial marking, you take ownership */
+
+        MarkVal const * initMarking()
+        {
+            return initialMarking.data();
+        }
+        
+        uint32_t numberOfPlaces() const
+        {
+            return _placenames.size();
+        }
+        
+        uint32_t numberOfTransitions() const
+        {
+            return _transitionnames.size();
+        }
+        
+        const std::unordered_map<std::string, uint32_t>& getPlaceNames() const
+        {
+            return _placenames;
+        }
+        
+        const std::unordered_map<std::string, uint32_t>& getTransitionNames() const
+        {
+            return _transitionnames;
+        }
+
+        void reduce(std::vector<std::shared_ptr<PQL::Condition> >& query, 
+                    std::vector<Reachability::ResultPrinter::Result>& results, 
+                    int reductiontype, bool reconstructTrace, const PetriNet* net, int timeout, std::vector<uint32_t>& reductions);
+        
+        size_t RemovedTransitions() const
+        {
+            return reducer.RemovedTransitions();
+        }
+        
+        size_t RemovedPlaces() const
+        {
+            return reducer.RemovedPlaces();
+        }
+
+        void printStats(std::ostream& out)
+        {
+            reducer.printStats(out);
+        }
+        
+        Reducer* getReducer() { return &reducer; }
+        
+        std::vector<std::pair<std::string, uint32_t>> orphanPlaces() const {
+            std::vector<std::pair<std::string, uint32_t>> res;
+            for(uint32_t p = 0; p < _places.size(); p++) {
+                if(_places[p].consumers.size() == 0 && _places[p].producers.size() == 0) {
+                    for(auto &n : _placenames) {
+                        if(n.second == p) {
+                            res.push_back(std::make_pair(n.first, initialMarking[p]));
+                            break;
+                        }
+                    }
+                }
+            }
+            return res;
+        }
+
+        double getReductionTime() const {
+            // duration in seconds
+            auto end = std::chrono::high_resolution_clock::now();
+            return (std::chrono::duration_cast<std::chrono::microseconds>(end - _start).count())*0.000001;
+        }
+
+        void startTimer() {
+            _start = std::chrono::high_resolution_clock::now();
+        }
+        
+    private:
+        uint32_t nextPlaceId(std::vector<uint32_t>& counts,  std::vector<uint32_t>& pcounts, std::vector<uint32_t>& ids, bool reorder);
+        std::chrono::high_resolution_clock::time_point _start;
+
+    protected:
+        std::unordered_map<std::string, uint32_t> _placenames;
+        std::unordered_map<std::string, uint32_t> _transitionnames;
+        
+        std::vector<Transition> _transitions;
+        std::vector<Place> _places;
+        
+        std::vector<MarkVal> initialMarking;
+        Reducer reducer;
+    };
+
+}
+
+#endif // PETRINETBUILDER_H
+
 
=== added directory 'include/PetriEngine/Reachability'
=== added file 'include/PetriEngine/Reachability/ReachabilityResult.h'
--- include/PetriEngine/Reachability/ReachabilityResult.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/Reachability/ReachabilityResult.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,97 @@
+/* PeTe - Petri Engine exTremE
+ * Copyright (C) 2011  Jonas Finnemann Jensen <[e-mail]>,
+ *                     Thomas Søndersø Nielsen <[e-mail]>,
+ *                     Lars Kærlund Østergaard <[e-mail]>,
+ *                     Peter Gjøl Jensen <[e-mail]>
+ * 
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ * 
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ * 
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+#ifndef REACHABILITYRESULT_H
+#define REACHABILITYRESULT_H
+
+#include <vector>
+#include "../PQL/PQL.h"
+#include "../Structures/StateSet.h"
+#include "../Reducer.h"
+
+struct options_t;
+
+namespace PetriEngine {
+    class PetriNetBuilder;
+    namespace Reachability {
+
+        /** Result of a reachability search */
+
+        class AbstractHandler {
+        public:
+            enum Result {
+                /** The query was satisfied */
+                Satisfied,
+                /** The query cannot be satisfied */
+                NotSatisfied,
+                /** We're unable to say if the query can be satisfied */
+                Unknown,
+                /** The query should be verified using the CTL engine */
+                CTL,
+                /** Just ignore */
+                Ignore
+            };
+            virtual std::pair<Result, bool> handle(
+                size_t index,
+                PQL::Condition* query, 
+                Result result,
+                const std::vector<uint32_t>* maxPlaceBound = nullptr,
+                size_t expandedStates = 0,
+                size_t exploredStates = 0,
+                size_t discoveredStates = 0,
+                int maxTokens = 0,                
+                Structures::StateSetInterface* stateset = nullptr, size_t lastmarking = 0, const MarkVal* initialMarking = nullptr) = 0;
+        };
+        
+        class ResultPrinter : public AbstractHandler {
+        protected:
+            PetriNetBuilder* builder;
+            options_t* options;
+            std::vector<std::string>& querynames;
+            Reducer* reducer;
+        public:
+            const string techniques = "TECHNIQUES COLLATERAL_PROCESSING STRUCTURAL_REDUCTION QUERY_REDUCTION SAT_SMT ";
+            const string techniquesStateSpace = "TECHNIQUES EXPLICIT STATE_COMPRESSION";
+            
+            ResultPrinter(PetriNetBuilder* b, options_t* o, std::vector<std::string>& querynames) 
+            : builder(b), options(o), querynames(querynames), reducer(NULL)
+            {};
+            
+            void setReducer(Reducer* r) { this->reducer = r; }
+            
+            std::pair<Result, bool> handle(
+                size_t index,
+                PQL::Condition* query, 
+                Result result,
+                const std::vector<uint32_t>* maxPlaceBound = nullptr,
+                size_t expandedStates = 0,
+                size_t exploredStates = 0,
+                size_t discoveredStates = 0,
+                int maxTokens = 0,                
+                Structures::StateSetInterface* stateset = nullptr, size_t lastmarking = 0, const MarkVal* initialMarking = nullptr) override;
+            
+            std::string printTechniques();
+            
+            void printTrace(Structures::StateSetInterface*, size_t lastmarking);
+            
+        };
+    } // Reachability
+} // PetriEngine
+
+#endif // REACHABILITYRESULT_H
 
=== added file 'include/PetriEngine/Reachability/ReachabilitySearch.h'
--- include/PetriEngine/Reachability/ReachabilitySearch.h	1970-01-01 00:00:00 +0000
+++ include/PetriEngine/Reachability/ReachabilitySearch.h	2020-09-11 14:21:20 +0000
@@ -0,0 +1,182 @@
+/* PeTe - Petri Engine exTremE
+ * Copyright (C) 2011  Jonas Finnemann Jensen <[e-mail]>,
+ *                     Thomas Søndersø Nielsen <[e-mail]>,
+ *                     Lars Kærlund Østergaard <[e-mail]>,
+ *                     Peter Gjøl Jensen <[e-mail]>
+ * 
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ * 
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the