Merge lp:~tapaal-ltl/verifypn/ltl-spring-2021 into lp:verifypn

[Nikolaj Jensen Ulrik]

Full LTL engine with stubborn sets and all our fancy stuff.
New features:
- Stubborn sets, both classic Valmari method, new reachability method, and mix of the two
- Unified method for specifying heuristics on command-line
- Replay of traces (LTL only)

[lp:~tapaal-ltl/verifypn/ltl-spring-2021]

259. By Nikolaj Jensen Ulrik on 2021-07-07

Merge verifypn@243 into ltl-spring-2021@258

260. By Nikolaj Jensen Ulrik on 2021-07-22

Merge verifypn@245

261. By Nikolaj Jensen Ulrik on 2021-07-22

Fix stupid nullptr

262. By Nikolaj Jensen Ulrik on 2021-08-02

WIP fixing bad traces, still some bugs left

263. By Nikolaj Jensen Ulrik on 2021-08-03

More sane trace behaviour maybe

264. By Nikolaj Jensen Ulrik on 2021-08-03

Print GUI-friendly output string from LTL

265. By Nikolaj Jensen Ulrik on 2021-08-03

Fixing trace formats

266. By Nikolaj Jensen Ulrik on 2021-08-03

Fix traces also in NDFS

267. By Nikolaj Jensen Ulrik on 2021-08-03

Fix crash in Tarjan's algorithm when trying to generate a trace when the invariant self loop optimization triggers

268. By Nikolaj Jensen Ulrik on 2021-08-04

hov

269. By Nikolaj Jensen Ulrik on 2021-08-04

Fix heuristics not being used

270. By Nikolaj Jensen Ulrik on 2021-08-04

Refine MCC21 competition script with fresh heuristic and no stubborn sets in random phase

271. By Nikolaj Jensen Ulrik on 2021-08-04

fix warnings

272. By Nikolaj Jensen Ulrik on 2021-08-05

Move rev 270 change in tapaal.sh to new file and revert 270

273. By Nikolaj Jensen Ulrik on 2021-08-05

fully revert tapaal.sh back to trunk version (aka MCC submission), newer LTL script can be found in tapaal-tweaked-rev270.sh

[Jiri Srba (srba)]

review: Approve

=== modified file '.bzrignore'
--- .bzrignore	2020-03-04 14:25:25 +0000
+++ .bzrignore	2021-08-05 10:56:53 +0000
@@ -9,5 +9,8 @@
 src/PetriEngine/PQL/PQLQueryParser.parser.cpp
 src/PetriEngine/PQL/PQLQueryParser.parser.hpp
 src/PetriEngine/PQL/PQLQueryTokens.lexer.cpp
+src/LTL/SuccessorGeneration/HeuristicLexer.lexer.cpp
+src/LTL/SuccessorGeneration/HeuristicParser.parser.cpp
+src/LTL/SuccessorGeneration/HeuristicParser.parser.hpp
 build/
 

=== modified file 'CMakeLists.txt'
--- CMakeLists.txt	2021-04-16 19:23:03 +0000
+++ CMakeLists.txt	2021-08-05 10:56:53 +0000
@@ -51,7 +51,7 @@
 endif ()
 
 set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -s -Wall -pedantic-errors -O3 -DNDEBUG")
-set(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS_DEBUG} -O0 -fno-omit-frame-pointer")
+set(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS_DEBUG} -O0 -fno-omit-frame-pointer ")
 set(CMAKE_EXE_LINKER_FLAGS_RELEASE "${CMAKE_EXE_LINKER_FLAGS_RELEASE} -O3 -DNDEBUG")
 if (VERIFYPN_Static AND NOT APPLE)
     set(CMAKE_EXE_LINKER_FLAGS_RELEASE "${CMAKE_EXE_LINKER_FLAGS_RELEASE} -static")

=== added file 'Scripts/MCC21/competition-scripts/tapaal-tweaked-rev270.sh'
--- Scripts/MCC21/competition-scripts/tapaal-tweaked-rev270.sh	1970-01-01 00:00:00 +0000
+++ Scripts/MCC21/competition-scripts/tapaal-tweaked-rev270.sh	2021-08-05 10:56:53 +0000
@@ -0,0 +1,540 @@
+#!/bin/bash
+
+# This is the initialization script for the participation of TAPAAL
+# untimed engine verifypn in the Petri net competition 2021.
+
+DIR=$(dirname "${BASH_SOURCE[0]}")
+
+if [ -z "$MODEL_PATH" ] ; then
+	MODEL_PATH=.
+	echo "Setting MODEL_PATH=$MODEL_PATH"
+else
+	echo "Got MODEL_PATH=$MODEL_PATH"
+fi
+
+if [ -z "$VERIFYPN" ] ; then
+	VERIFYPN="$DIR"/verifypn
+	echo "Setting VERIFYPN=$VERIFYPN"
+else
+	echo "Got VERIFYPN=$VERIFYPN"
+fi
+
+if [ -z "$BK_TIME_CONFINEMENT" ] ; then
+	BK_TIME_CONFINEMENT=3600
+	echo "Setting BK_TIME_CONFINEMENT=$BK_TIME_CONFINEMENT"
+else
+	echo "Got BK_TIME_CONFINEMENT=$BK_TIME_CONFINEMENT"
+fi
+TIMEOUT_TOTAL=$(echo "$BK_TIME_CONFINEMENT-10" | bc) 
+
+if [ -z "$TEMPDIR" ]; then
+	TEMPDIR="$DIR/tmp"
+	echo "Setting TEMPDIR=$TEMPDIR"
+else
+	echo "Got TEMPDIR=$TEMPDIR"
+fi
+
+TIMEOUT_CMD=timeout
+TIME_CMD="/usr/bin/time -f \"@@@%e,%M@@@\" "
+
+START_TIME=$(date +"%s")
+SECONDS=0
+
+#Allowed memory in kB
+if [ -z "$BK_MEMORY_CONFINEMENT" ] ; then
+	BK_MEMORY_CONFINEMENT="16000"
+	echo "Setting BK_MEMORY_CONFINEMENT=$BK_MEMORY_CONFINEMENT"
+else
+	echo "Got BK_MEMORY_CONFINEMENT=$BK_MEMORY_CONFINEMENT"
+fi
+MEM=$(echo "$BK_MEMORY_CONFINEMENT-500" | bc)
+MEM=$(echo "$MEM*1024" | bc)
+echo "Limiting to $MEM kB"
+ulimit -v $MEM
+
+
+PAR_CMD=parallel
+
+# Verification options
+OPTIONS=""
+PARALLEL_SIMPLIFICATION_OPTIONS=""
+echo "Total timeout: " "$TIMEOUT_TOTAL"
+
+# Timeouts (in seconds)
+TIMEOUT_SIMP=$(echo "$TIMEOUT_TOTAL/5" | bc)
+TIMEOUT_LP=$(echo "$TIMEOUT_TOTAL/120" | bc)
+TIMEOUT_RED=$(echo "$TIMEOUT_TOTAL/12" | bc)
+TIMEOUT_PAR=$(echo "$TIMEOUT_TOTAL/14" | bc) # competition 4.29 min
+TIMEOUT_SEQ_MIN=$(echo "$TIMEOUT_TOTAL/7" | bc) # competition 8.6 min
+SIPHONTRAP=$(echo "$TIMEOUT_TOTAL/12" | bc)
+SHORTRED=$(echo "$TIMEOUT_TOTAL/30" | bc)
+EXTENDED=$(echo "$TIMEOUT_TOTAL/25" | bc)
+
+STRATEGIES_SEQ[0]="-s RDFS -q 40 -l 5 -d $SHORTRED"
+STRATEGIES_SEQ[1]="-tar -q 0 -d $SHORTRED"
+
+
+STRATEGY_MULTI="-s BFS -q 15 -l 3 -d $SHORTRED"
+
+STRATEGIES_PAR[0]="-tar -s RDFS -q 0 -l 0 -d $SHORTRED"
+STRATEGIES_PAR[1]="-s BestFS -q 0 -l 0 -d $SHORTRED"
+STRATEGIES_PAR[2]="-s BFS -q 0 -l 0 -d $SHORTRED"
+STRATEGIES_PAR[3]="-s DFS -q 0 -l 0 -d $SHORTRED"
+
+STRATEGIES_RAND[0]="-s RDFS --seed-offset 0 -q $TIMEOUT_TOTAL -l 0 -d $SHORTRED"
+STRATEGIES_RAND[1]="-s RDFS --seed-offset 1337 -q 0 -l 0 -d 0"
+STRATEGIES_RAND[2]="-s RDFS --seed-offset 2018 -q 0 -l 0 -d $SHORTRED"
+STRATEGIES_RAND[3]="-tar -s RDFS --seed-offset 9220 -q 0 -l 0 -d $SHORTRED"
+
+run_multi=false;
+
+function time_left {
+    T=$(date +"%s")
+    SECONDS=$(echo "$T-$START_TIME" | bc)
+    SECONDS=$(echo "$TIMEOUT_TOTAL-$SECONDS" | bc)
+    echo "Time left:  " $SECONDS
+    if [[ "$SECONDS" -le 0 ]] ; then
+        echo "Out of time, terminating!"
+        rm $QF
+        rm $MF
+        exit
+    fi
+}
+
+time_left
+
+function verifyparallel {
+    # Keep track of time passed (in seconds)
+    mkdir -p $TEMPDIR
+    QF=$(mktemp --tmpdir=$TEMPDIR )
+    MF=$(mktemp --tmpdir=$TEMPDIR )
+    echo $TEMPDIR
+    echo $QF
+    echo $MF
+    local NUMBER=`cat $CATEGORY | grep "<property>" | wc -l`
+    QUERIES=( $(seq 1 $NUMBER) )
+    #MULTIQUERY_INPUT=$(sed -e "s/ /,/g" <<< ${QUERIES[@]})
+    MULTIQUERY_INPUT=$(echo ${QUERIES[@]} | sed -e "s/ /,/g")
+    time_left
+
+    # Step -1: Colored Overapproximation
+    echo "---------------------------------------------------"
+    echo "            Step -1: Stripping Colors              "
+    echo "---------------------------------------------------"
+    echo "Verifying stripped models ($NUMBER in total)        "
+    TMP=$($TIMEOUT_CMD $TIMEOUT_SIMP $VERIFYPN -n -c -q $TIMEOUT_SIMP -l $TIMEOUT_LP -d $TIMEOUT_RED -z 4 -x $MULTIQUERY_INPUT $MODEL_PATH/model.pnml $CATEGORY )
+    CNT=0
+    SOLVED=$(echo "$TMP" | grep "FORMULA" | grep -oP "(?<=-)[0-9]+(?=( TRUE)|( FALSE)|( [0-9]))")
+
+    for i in $SOLVED ; do 
+        i=$(echo $i | sed -e "s/0*//")
+        if [ -z "$i" ] ; then i="0"; fi
+        echo "Solution found by stripping colors (step -1) for query index " $i
+        unset QUERIES[$i]
+        CNT=$(echo "$CNT+1" | bc)
+    done
+    NUMBER=$(echo "$NUMBER-$CNT" | bc)
+
+    echo "$TMP"
+    
+    #MULTIQUERY_INPUT=$(sed -e "s/ /,/g" <<< ${QUERIES[@]})
+    MULTIQUERY_INPUT=$(echo ${QUERIES[@]} | sed -e "s/ /,/g")
+    time_left
+
+    if [ -z "$MULTIQUERY_INPUT" ]; then echo "All queries are solved" ; time_left; rm $QF; rm $MF; exit; fi
+
+    # Step 0: Simplification 
+    echo "---------------------------------------------------"
+    echo "            Step 0: Parallel Simplification        "
+    echo "---------------------------------------------------"
+    echo "Doing parallel simplification ($NUMBER in total)"
+    echo "Total simplification timout is $TIMEOUT_SIMP -- reduction timeout is $TIMEOUT_RED"
+
+
+    if [[ $BK_EXAMINATION == "LTL"* ]]; then
+        PAR_SIMP_TIMEOUT=$(echo "$TIMEOUT_SIMP + $TIMEOUT_RED" | bc)
+    else
+        PAR_SIMP_TIMEOUT=$SECONDS
+    fi
+
+    echo "$TIMEOUT_CMD $PAR_SIMP_TIMEOUT $VERIFYPN -n $PARALLEL_SIMPLIFICATION_OPTIONS -q $TIMEOUT_SIMP -l $TIMEOUT_LP -d $TIMEOUT_RED -z 4 -s OverApprox --binary-query-io 2 --write-simplified $QF --write-reduced $MF -x $MULTIQUERY_INPUT $MODEL_PATH/model.pnml $CATEGORY"
+
+    TMP=$($TIMEOUT_CMD $PAR_SIMP_TIMEOUT $VERIFYPN -n $PARALLEL_SIMPLIFICATION_OPTIONS -q $TIMEOUT_SIMP -l $TIMEOUT_LP -d $TIMEOUT_RED -z 4 -s OverApprox --binary-query-io 2 --write-simplified $QF --write-reduced $MF -x $MULTIQUERY_INPUT $MODEL_PATH/model.pnml $CATEGORY)
+
+    echo "$TMP"
+    TMP=$(echo "$TMP" | grep "FORMULA" | wc -l)
+    for i in $(seq 1 $TMP); do
+      echo "Solution found by parallel simplification (step 0)"
+    done
+
+    local NUMBER=`echo "$NUMBER-$TMP" | bc`
+    QUERIES=( $(seq 1 $NUMBER) )
+
+    if [[ $BK_EXAMINATION == "LTL"* && ! -s $QF ]]; then
+        echo "No simplified files created. Constructing non simplified files."
+        time_left
+        echo "$VERIFYPN -n -ltl none -q 0 -d 0 -z 4 --binary-query-io 2 --write-simplified $QF --write-reduced $MF -x $MULTIQUERY_INPUT $MODEL_PATH/model.pnml $CATEGORY"
+        $TIMEOUT_CMD $SECONDS $VERIFYPN -n -ltl none -q 0 -d 0 -z 4 --binary-query-io 2 --write-simplified $QF --write-reduced $MF -x $MULTIQUERY_INPUT $MODEL_PATH/model.pnml $CATEGORY
+    fi
+
+    time_left
+    echo
+    if [ ! -s $MF ]; then
+      echo "Model file after phase 0 is empty (CPN unfolding failed), exiting ..."
+      rm $QF
+      rm $MF
+      exit
+    fi
+ 
+    # Step 1: Parallel
+    echo "---------------------------------------------------"
+    echo "            Step 1: Parallel processing            "
+    echo "---------------------------------------------------"
+    echo "Doing parallel verification of individual queries ($NUMBER in total)"
+    echo "Each query is verified by ${#STRATEGIES_PAR[@]} parallel strategies for $TIMEOUT_PAR seconds"
+    
+    i=0
+    for Q in ${QUERIES[@]}; do
+    
+        TIMEOUT_PAR=$(( $TIMEOUT_PAR < $SECONDS ? $TIMEOUT_PAR : $SECONDS))
+        if [[ "$TIMEOUT_PAR" -le 0 ]] ; then echo "Out of time, terminating!"; time_left; rm $QF; rm $MF; exit; fi
+        echo "------------------- QUERY ${Q} ----------------------"
+        # Execute verifypn on all parallel strategies
+        # All processes are killed if one process provides an answer 
+        step1="$($PAR_CMD --line-buffer --halt now,success=1 --timeout $TIMEOUT_PAR --xapply\
+            eval $TIME_CMD $VERIFYPN -n $OPTIONS {} $MF $QF --binary-query-io 1 -x $Q -n \
+            ::: "${STRATEGIES_PAR[@]}" 2>&1)"
+
+        if [[ $? == 0 ]]; then
+            #unset QUERIES[$Q-1]
+            QUERIES=(${QUERIES[@]:0:$i} ${QUERIES[@]:$(($i + 1))})
+            i=$(echo "$i - 1" | bc)
+            echo "Solution found by parallel processing (step 1)"
+        else
+            echo "No solution found"
+        fi
+        FORMULA_RESULT="$(echo "$step1"|grep -m 1 FORMULA)"
+        
+        if [[ -n "$FORMULA_RESULT" ]]; then 
+            echo "$step1" | sed "/$FORMULA_RESULT/d"
+        else 
+            echo "$step1"
+        fi
+        echo 
+        echo "$FORMULA_RESULT"
+        time_left
+        i=$(echo "$i + 1" | bc)
+    done
+
+    # Exit if all queries are answered
+    if [[ ${#QUERIES[@]} == 0 ]]; then echo "All queries are solved" ; time_left; rm $QF; rm $MF; exit; fi
+    
+
+    # Step 2: Sequential
+    echo "---------------------------------------------------"
+    echo "           Step 2: Sequential processing           "
+    echo "---------------------------------------------------"
+    echo "Remaining ${#QUERIES[@]} queries are verified sequentially."
+    echo "Each query is verified for a dynamic timeout (at least $TIMEOUT_SEQ_MIN seconds)"
+    
+    time_left
+    # Count the number of remaining queries to try solving sequentially
+    REMAINING_SEQ=${#QUERIES[@]}
+    if [[ "$TIMEOUT_SEQ_MIN" -ne "0" ]] ; then
+    i=0
+    for Q in ${QUERIES[@]}; do
+        echo "------------------- QUERY ${Q} ----------------------"
+        # Calculate remaining time
+        TIMEOUT_SEQ=$(echo "$SECONDS / $REMAINING_SEQ" | bc)
+        if [[ "$TIMEOUT_SEQ_MIN" -gt "$TIMEOUT_SEQ" ]]; then TIMEOUT_SEQ=$TIMEOUT_SEQ_MIN; fi
+        if [[ "$TIMEOUT_SEQ" -gt "$SECONDS" ]]; then TIMEOUT_SEQ=$SECONDS; break; fi
+        if [[ "$TIMEOUT_SEQ" -le 0 ]] ; then echo "Out of time, terminating!"; time_left; rm $QF; rm $MF; exit; fi 
+
+        # Execute verifypn on sequential strategy
+        echo "Running query $Q for $TIMEOUT_SEQ seconds. Remaining: $REMAINING_SEQ queries and $SECONDS seconds"
+	step1="$($PAR_CMD --line-buffer --halt now,success=1 --timeout $TIMEOUT_SEQ --xapply\
+            eval $TIME_CMD $VERIFYPN -n $OPTIONS {} $MF $QF --binary-query-io 1 -x $Q -n \
+            ::: "${STRATEGIES_SEQ[@]}" 2>&1)"
+        RETVAL=$?
+
+        if [[ $RETVAL == 0 ]]; then
+            #unset QUERIES[$Q-1]
+            QUERIES=(${QUERIES[@]:0:$i} ${QUERIES[@]:$(($i + 1))})
+            i=$(echo "$i - 1" | bc)
+            echo "Solution found by sequential processing (step 2)"
+	    echo "$step1"
+        else
+            echo "No solution found"
+        fi
+        FORMULA_RESULT="$(echo "$step1"|grep -m 1 FORMULA)"
+
+        if [[ -n "$FORMULA_RESULT" ]]; then
+            echo "$step1" | sed "/$FORMULA_RESULT/d"
+        else
+            echo "$step1"
+        fi
+        echo 
+        echo "$FORMULA_RESULT"
+
+        time_left
+        REMAINING_SEQ=$((REMAINING_SEQ - 1))
+        i=$(echo "$i + 1" | bc)
+    done
+    fi
+
+    # Exit if all queries are answered
+    if [[ ${#QUERIES[@]} == 0 ]]; then echo "All queries are solved" ; time_left; rm $QF; rm $MF; exit; fi
+
+  if $run_multi; then 
+    # Step 3: Multiquery
+    time_left 
+    echo "---------------------------------------------------"
+    echo "           Step 3: Multiquery processing           "
+    echo "---------------------------------------------------"
+    echo "Remaining ${#QUERIES[@]} queries are solved using multiquery"
+    echo "Time remaining: $SECONDS seconds of the initial $TIMEOUT_TOTAL seconds" 
+    
+    # Join remaining query indexes in comma separated string
+    #MULTIQUERY_INPUT=$(sed -e "s/ /,/g" <<< ${QUERIES[@]})
+    MULTIQUERY_INPUT=$(echo ${QUERIES[@]} | sed -e "s/ /,/g")
+    
+    RED=$(echo "$SECONDS/8" | bc)
+    RUN_TIME=$(echo "$SECONDS*6/8" | bc)
+    if [[ "$RUN_TIME" -le 0 ]] ; then echo "Out of time, terminating!"; time_left; rm $QF; rm $MF; exit; fi
+    echo "Running multiquery on -x $MULTIQUERY_INPUT for $RUN_TIME seconds" 
+    TMP=$($TIME_CMD $TIMEOUT_CMD $RUN_TIME $VERIFYPN -n $STRATEGY_MULTI $OPTIONS -d $RED -q $RED -p $MF $QF --binary-query-io 1 -n -x $MULTIQUERY_INPUT )
+
+    echo "$TMP"
+
+    SOLVED=$(echo "$TMP" | grep -oP "(?<=Query index )[0-9]+(?= was solved)")
+    SOLVED=$(echo $SOLVED | tr " " "\n" | sort -g -r)
+
+    for rem in $SOLVED ; do 
+            QUERIES=(${QUERIES[@]:0:$rem} ${QUERIES[@]:$(($rem + 1))})
+            echo "Solution found by multiquery processing (step 3) for query index" $rem 
+    done
+  fi
+
+
+    for trial in $(seq 0 20); do
+        time_left
+        if [[ ${#QUERIES[@]} == 0 ]]; then echo "All queries are solved" ; time_left; rm $QF; rm $MF; exit; fi
+        # Step 4: Parallel random search
+        echo "---------------------------------------------------"
+        echo "            Step 4: Random Parallel processing     "
+        echo "---------------------------------------------------"
+        echo "Doing random parallel verification of individual queries (${#QUERIES[@]}  in total)"
+        RUN_TIME=$(echo "$SECONDS/${#QUERIES[@]}" | bc)
+        echo "Each query is verified by ${#STRATEGIES_RAND[@]} parallel strategies for $RUN_TIME seconds"
+        
+        i=0 
+        for Q in ${QUERIES[@]}; do
+            echo "------------------- QUERY ${Q} ----------------------"
+            # Execute verifypn on all parallel strategies
+            # All processes are killed if one process provides an answer 
+            RUN_TIME=$(( $RUN_TIME < $SECONDS ? $RUN_TIME : $SECONDS))
+            if [[ "$RUN_TIME" -le 0 ]] ; then echo "Out of time, terminating!"; time_left; rm $QF; rm $MF; exit; fi
+            step1="$($PAR_CMD --line-buffer --halt now,success=1 --timeout $RUN_TIME --xapply\
+                eval $TIME_CMD $VERIFYPN -n $OPTIONS {} $MF $QF --binary-query-io 1 -x $Q -n \
+                ::: "${STRATEGIES_RAND[@]}" 2>&1)"
+
+            if [[ $? == 0 ]]; then
+                #unset QUERIES[$Q-1]
+                QUERIES=(${QUERIES[@]:0:$i} ${QUERIES[@]:$(($i + 1))})
+                i=$(echo "$i - 1" | bc)
+                echo "Solution found in random processing (step 4)"
+            else
+                echo "No solution found"
+            fi
+            FORMULA_RESULT="$(echo "$step1"|grep -m 1 FORMULA)"
+        
+            if [[ -n "$FORMULA_RESULT" ]]; then 
+                echo "$step1" | sed "/$FORMULA_RESULT/d"
+            else 
+                echo "$step1"
+            fi
+            echo 
+            echo "$FORMULA_RESULT"
+            time_left
+            i=$(echo "$i + 1" | bc)
+        done
+    # Exit if all queries are answered
+    done
+ 
+    time_left
+    echo "End of script."
+    rm $QF
+    rm $MF
+}
+
+function LTL {
+    unset STRATEGIES_PAR
+    STRATEGIES_PAR[0]="-ltl tarjan --ltl-heur dist -q 0 -l 0 -d $SHORTRED"
+    STRATEGIES_PAR[1]="-ltl tarjan --ltl-heur 'sum aut firecount(5000)' -q 0 -l 0 -d $SHORTRED"
+    STRATEGIES_PAR[2]="-ltl tarjan -s DFS -p -q 0 -l 0 -d $SHORTRED"
+    STRATEGIES_PAR[3]="-ltl ndfs -q 0 -l 0 -d $SHORTRED"
+    unset STRATEGIES_SEQ
+    STRATEGIES_SEQ[0]="-ltl tarjan -q 40 -l 5 -d $SHORTRED -s BestFS --ltl-por mix --ltl-heur weight-aut"
+    unset STRATEGIES_RAND
+    STRATEGIES_RAND[0]="-ltl tarjan -s RDFS --seed-offset 0 -p -q 0 -l 0 -d $SHORTRED"
+    STRATEGIES_RAND[1]="-ltl tarjan -s RDFS --seed-offset 1337 -p -q 0 -l 0 -d $SHORTRED"
+    STRATEGIES_RAND[2]="-ltl tarjan -s RDFS --seed-offset 2018 -p -q 0 -l 0 -d $SHORTRED"
+    STRATEGIES_RAND[3]="-ltl tarjan -s RDFS --seed-offset 9220 -p -q 0 -l 0 -d $SHORTRED"
+    PARALLEL_SIMPLIFICATION_OPTIONS="-ltl"
+    verifyparallel
+}
+
+case "$BK_EXAMINATION" in
+
+    StateSpace)
+        echo        
+        echo "*****************************************"
+        echo "*  TAPAAL performing StateSpace search  *"
+        echo "*****************************************"
+        $TIME_CMD $TIMEOUT_CMD $TIMEOUT_TOTAL $VERIFYPN -n -p -q 0 -e --disable-partitioning -s BFS $MODEL_PATH/model.pnml 
+        time_left
+        ;;
+
+    UpperBounds)    
+        echo        
+        echo "*****************************************"
+        echo "*  TAPAAL CLASSIC verifying UpperBounds *"
+        echo "*****************************************" 
+        #STRATEGIES_PAR[0]="-s BestFS -q 0 -l 0 -d $SHORTRED"
+        #STRATEGIES_PAR[1]="-s BestFS -q 0 -l 0 -d 0"
+        #STRATEGIES_PAR[0]="-s BFS -q 0 -l 0 -d $SHORTRED"
+        STRATEGIES_PAR[0]="-n -s BFS -q 0 -l 0 -d $SHORTRED"
+        STRATEGIES_PAR[1]="-n -p -q 0 -l 0 -d $SHORTRED"
+        STRATEGIES_PAR[2]="-n -p -s DFS -q 0 -l 0 -d $SHORTRED"
+        STRATEGIES_PAR[3]="-n -tar -q 0 -l 0 -d 0"
+        CATEGORY="${MODEL_PATH}/${BK_EXAMINATION}.xml"
+        TIMEOUT_SEQ_MIN=0 
+        TIMEOUT_PAR=$(echo "$TIMEOUT_TOTAL/26" | bc) # competition 2.3 min
+        run_multi=true
+        verifyparallel 
+        ;;
+
+    ReachabilityDeadlock)
+        echo        
+        echo "**********************************************"
+        echo "*  TAPAAL checking for ReachabilityDeadlock  *"
+        echo "**********************************************"
+        STRATEGIES_PAR[0]="-s RDFS --siphon-trap $SIPHONTRAP"
+        STRATEGIES_PAR[1]="-s BFS -q 0 -l 0 -d $EXTENDED"
+        STRATEGIES_PAR[2]="-s DFS -q 0 -l 0 -d $EXTENDED"
+        STRATEGIES_PAR[3]="-tar -q 0 -l 0 -d $EXTENDED"
+        TIMEOUT_SEQ_MIN=0 
+        CATEGORY="${DIR}/${BK_EXAMINATION}.xml"
+        TIMEOUT_PAR=$(echo "$TIMEOUT_TOTAL/6" | bc) # competition 10 min
+        verifyparallel 
+        ;;
+
+    QuasiLiveness)
+        echo        
+        echo "**********************************************"
+        echo "*  TAPAAL checking for QuasiLiveness         *"
+        echo "**********************************************"
+	TIMEOUT_SEQ_MIN=0 
+        CATEGORY="${DIR}/${BK_EXAMINATION}.xml"
+        TIMEOUT_PAR=$(echo "$TIMEOUT_TOTAL/6" | bc) # competition 10 min
+        verifyparallel 
+        ;;
+
+   Liveness)
+        echo        
+        echo "**********************************************"
+        echo "*  TAPAAL checking for Liveness              *"
+        echo "**********************************************"
+	TIMEOUT_SEQ_MIN=0 
+	CATEGORY="${DIR}/${BK_EXAMINATION}.xml"
+        TIMEOUT_PAR=$(echo "$TIMEOUT_TOTAL/6" | bc) # competition 10 min
+        verifyparallel 
+        ;;
+
+   StableMarking)
+        echo        
+        echo "**********************************************"
+        echo "*  TAPAAL checking for StableMarking         *"
+        echo "**********************************************"
+	TIMEOUT_SEQ_MIN=0 
+        CATEGORY="${DIR}/${BK_EXAMINATION}.xml"
+        TIMEOUT_PAR=$(echo "$TIMEOUT_TOTAL/6" | bc) # competition 10 min
+        verifyparallel 
+        ;;
+
+    OneSafe)
+        echo        
+        echo "**********************************************"
+        echo "*  TAPAAL checking for One-Safe              *"
+        echo "**********************************************"
+	TIMEOUT_SEQ_MIN=0 
+        CATEGORY="${DIR}/${BK_EXAMINATION}.xml"
+	TIMEOUT_PAR=$(echo "$TIMEOUT_TOTAL/6" | bc) # competition 10 min
+        verifyparallel 
+        ;;
+
+   ReachabilityCardinality)
+        echo        
+        echo "**********************************************"
+        echo "*  TAPAAL verifying ReachabilityCardinality  *"
+        echo "**********************************************"
+        CATEGORY="${MODEL_PATH}/${BK_EXAMINATION}.xml"
+        verifyparallel 
+        ;;
+
+    ReachabilityFireability)
+        echo        
+        echo "**********************************************"
+        echo "*  TAPAAL verifying ReachabilityFireability  *"
+        echo "**********************************************"
+        CATEGORY="${MODEL_PATH}/${BK_EXAMINATION}.xml"
+	TIMEOUT_SEQ_MIN=$(echo "$TIMEOUT_TOTAL/6" | bc) # competition 10 min
+        verifyparallel 
+        ;;
+
+    CTLCardinality)
+        echo        
+        echo "*************************************"
+        echo "*  TAPAAL verifying CTLCardinality  *"
+        echo "*************************************"
+	CATEGORY="${MODEL_PATH}/${BK_EXAMINATION}.xml"
+        TIMEOUT_PAR=$(echo "$TIMEOUT_TOTAL/12" | bc) # competition 5 min
+        verifyparallel
+        ;;
+
+    CTLFireability)
+        echo        
+        echo "*************************************"
+        echo "*  TAPAAL verifying CTLFireability  *"
+        echo "*************************************"
+ 	CATEGORY="${MODEL_PATH}/${BK_EXAMINATION}.xml"
+        TIMEOUT_PAR=$(echo "$TIMEOUT_TOTAL/12" | bc) # competition 5 min
+        TIMEOUT_SEQ_MIN=$(echo "$TIMEOUT_TOTAL/6" | bc) # competition 10 min
+        verifyparallel
+        ;;
+
+    LTLCardinality)
+        echo        
+        echo "*************************************"
+        echo "*  TAPAAL verifying LTLCardinality  *"
+        echo "*************************************"
+	      CATEGORY="${MODEL_PATH}/${BK_EXAMINATION}.xml"
+        TIMEOUT_PAR=$(echo "$TIMEOUT_TOTAL/12" | bc) # competition 5 min
+        LTL
+       ;;
+
+    LTLFireability)
+        echo        
+        echo "*************************************"
+        echo "*  TAPAAL verifying LTLFireability  *"
+        echo "*************************************"
+ 	      CATEGORY="${MODEL_PATH}/${BK_EXAMINATION}.xml"
+        TIMEOUT_PAR=$(echo "$TIMEOUT_TOTAL/12" | bc) # competition 5 min
+        TIMEOUT_SEQ_MIN=$(echo "$TIMEOUT_TOTAL/6" | bc) # competition 10 min
+        LTL
+        ;;
+    *)
+        echo "DO_NOT_COMPETE"  
+        exit 0
+        ;;
+esac

=== modified file 'Scripts/MCC21/competition-scripts/tapaal.sh'
--- Scripts/MCC21/competition-scripts/tapaal.sh	2021-04-28 11:15:57 +0000
+++ Scripts/MCC21/competition-scripts/tapaal.sh	2021-08-05 10:56:53 +0000
@@ -367,6 +367,23 @@
     rm $MF
 }
 
+function LTL {
+    unset STRATEGIES_PAR
+    STRATEGIES_PAR[0]="-ltl tarjan --ltl-heur dist -q 0 -l 0 -d $SHORTRED"
+    STRATEGIES_PAR[1]="-ltl tarjan --ltl-heur sum-composed-weight --log-fire-count-threshold 5000  -q 0 -l 0 -d $SHORTRED"
+    STRATEGIES_PAR[2]="-ltl tarjan -s DFS -p -q 0 -l 0 -d $SHORTRED"
+    STRATEGIES_PAR[3]="-ltl ndfs -q 0 -l 0 -d $SHORTRED"
+    unset STRATEGIES_SEQ
+    STRATEGIES_SEQ[0]="-ltl tarjan -q 40 -l 5 -d $SHORTRED -s BestFS --ltl-por mix --ltl-heur weight-aut"
+    unset STRATEGIES_RAND
+    STRATEGIES_RAND[0]="-ltl tarjan -s RDFS --seed-offset 0 -q 0 -l 0 -d $SHORTRED"
+    STRATEGIES_RAND[1]="-ltl tarjan -s RDFS --seed-offset 1337 -q 0 -l 0 -d $SHORTRED"
+    STRATEGIES_RAND[2]="-ltl tarjan -s RDFS --seed-offset 2018 -q 0 -l 0 -d $SHORTRED"
+    STRATEGIES_RAND[3]="-ltl tarjan -s RDFS --seed-offset 9220 -q 0 -l 0 -d $SHORTRED"
+    PARALLEL_SIMPLIFICATION_OPTIONS="-ltl"
+    verifyparallel
+}
+
 case "$BK_EXAMINATION" in
 
     StateSpace)
@@ -503,21 +520,8 @@
         echo "*************************************"
 	      CATEGORY="${MODEL_PATH}/${BK_EXAMINATION}.xml"
         TIMEOUT_PAR=$(echo "$TIMEOUT_TOTAL/12" | bc) # competition 5 min
-        unset STRATEGIES_PAR
-        STRATEGIES_PAR[0]="-ltl tarjan -s DFS -q 0 -l 0 -d $SHORTRED"
-        STRATEGIES_PAR[1]="-ltl tarjan -q 0 -l 0 -d $SHORTRED"
-        STRATEGIES_PAR[2]="-ltl tarjan -s RDFS -q 0 -l 0 -d $SHORTRED"
-        STRATEGIES_PAR[3]="-ltl ndfs -q 0 -l 0 -d $SHORTRED"
-        unset STRATEGIES_SEQ
-        STRATEGIES_SEQ[0]="-ltl tarjan -q 40 -l 5 -d $SHORTRED"
-        unset STRATEGIES_RAND
-        STRATEGIES_RAND[0]="-ltl tarjan -s RDFS --seed-offset 0 -q 0 -l 0 -d $SHORTRED"
-        STRATEGIES_RAND[1]="-ltl tarjan -s RDFS --seed-offset 1337 -q 0 -l 0 -d $SHORTRED"
-        STRATEGIES_RAND[2]="-ltl tarjan -s RDFS --seed-offset 2018 -q 0 -l 0 -d $SHORTRED"
-        STRATEGIES_RAND[3]="-ltl tarjan -s RDFS --seed-offset 9220 -q 0 -l 0 -d $SHORTRED"
-        PARALLEL_SIMPLIFICATION_OPTIONS="-ltl"
-        verifyparallel
-        ;;
+        LTL
+       ;;
 
     LTLFireability)
         echo        
@@ -527,20 +531,7 @@
  	      CATEGORY="${MODEL_PATH}/${BK_EXAMINATION}.xml"
         TIMEOUT_PAR=$(echo "$TIMEOUT_TOTAL/12" | bc) # competition 5 min
         TIMEOUT_SEQ_MIN=$(echo "$TIMEOUT_TOTAL/6" | bc) # competition 10 min
-        unset STRATEGIES_PAR
-        STRATEGIES_PAR[0]="-ltl tarjan -s DFS -q 0 -l 0 -d $SHORTRED"
-        STRATEGIES_PAR[1]="-ltl tarjan -q 0 -l 0 -d $SHORTRED"
-        STRATEGIES_PAR[2]="-ltl tarjan -s RDFS -q 0 -l 0 -d $SHORTRED"
-        STRATEGIES_PAR[3]="-ltl ndfs -q 0 -l 0 -d $SHORTRED"
-        unset STRATEGIES_SEQ
-        STRATEGIES_SEQ[0]="-ltl tarjan -q 40 -l 5 -d $SHORTRED"
-        unset STRATEGIES_RAND
-        STRATEGIES_RAND[0]="-ltl tarjan -s RDFS --seed-offset 0 -q 0 -l 0 -d $SHORTRED"
-        STRATEGIES_RAND[1]="-ltl tarjan -s RDFS --seed-offset 1337 -q 0 -l 0 -d $SHORTRED"
-        STRATEGIES_RAND[2]="-ltl tarjan -s RDFS --seed-offset 2018 -q 0 -l 0 -d $SHORTRED"
-        STRATEGIES_RAND[3]="-ltl tarjan -s RDFS --seed-offset 9220 -q 0 -l 0 -d $SHORTRED"
-        PARALLEL_SIMPLIFICATION_OPTIONS="-ltl"
-        verifyparallel
+        LTL
         ;;
     *)
         echo "DO_NOT_COMPETE"  

=== modified file 'include/LTL/Algorithm/ModelChecker.h'
--- include/LTL/Algorithm/ModelChecker.h	2021-04-02 09:54:38 +0000
+++ include/LTL/Algorithm/ModelChecker.h	2021-08-05 10:56:53 +0000
@@ -20,28 +20,34 @@
 
 #include "PetriEngine/PQL/PQL.h"
 #include "LTL/SuccessorGeneration/ProductSuccessorGenerator.h"
+#include "LTL/SuccessorGeneration/ReachStubProductSuccessorGenerator.h"
 #include "LTL/SuccessorGeneration/ResumingSuccessorGenerator.h"
 #include "LTL/SuccessorGeneration/SpoolingSuccessorGenerator.h"
 #include "LTL/Structures/BitProductStateSet.h"
+#include "LTL/SuccessorGeneration/ReachStubProductSuccessorGenerator.h"
 #include "PetriEngine/options.h"
+
 #include <iomanip>
 #include <algorithm>
 
 namespace LTL {
-    template<typename SuccessorGen>
+    template<template <typename, typename...> typename ProductSucGen, typename SuccessorGen, typename... Spooler>
     class ModelChecker {
     public:
         ModelChecker(const PetriEngine::PetriNet *net,
                      const PetriEngine::PQL::Condition_ptr &condition,
                      const Structures::BuchiAutomaton &buchi,
-                     SuccessorGen &&successorGen,
-                     const TraceLevel level = TraceLevel::Transitions,
-                     bool shortcircuitweak = true)
-                : net(net), formula(condition), traceLevel(level), shortcircuitweak(shortcircuitweak)
+                     SuccessorGen *successorGen,
+                     std::unique_ptr<Spooler> &&...spooler)
+                : net(net), formula(condition)
         {
-            successorGenerator = std::make_unique<ProductSuccessorGenerator<SuccessorGen>>(net, buchi,
-                                                                                           std::move(successorGen));
-            if (level != TraceLevel::None) {
+            successorGenerator = std::make_unique<ProductSucGen<SuccessorGen, Spooler...>>(net, buchi, successorGen, std::move(spooler)...);
+        }
+
+        void setOptions(const options_t &options) {
+            traceLevel = options.trace;
+            shortcircuitweak = options.ltluseweak;
+            if (traceLevel != TraceLevel::None) {
                 maxTransName = 0;
                 for (const auto &transname : net->transitionNames()) {
                     maxTransName = std::max(transname.size(), maxTransName);
@@ -75,14 +81,14 @@
                       << "\tmax tokens:        " << stateSet.max_tokens() << std::endl;
         }
 
-        std::unique_ptr<ProductSuccessorGenerator<SuccessorGen>> successorGenerator;
+        std::unique_ptr<ProductSucGen<SuccessorGen, Spooler...>> successorGenerator;
 
         const PetriEngine::PetriNet *net;
         PetriEngine::PQL::Condition_ptr formula;
         TraceLevel traceLevel;
 
         size_t _discovered = 0;
-        const bool shortcircuitweak;
+        bool shortcircuitweak;
         bool weakskip = false;
         bool is_weak = false;
         size_t maxTransName;
@@ -99,37 +105,29 @@
         printTransition(size_t transition, LTL::Structures::ProductState &state, std::ostream &os)
         {
             if (transition >= std::numeric_limits<ptrie::uint>::max() - 1) {
-                os << indent << "<deadlock buchi=\"" << state.getBuchiState() << "\"/>";
+                os << indent << "<deadlock/>";
                 return os;
             }
-            std::string tname = net->transitionNames()[transition];
+                os << indent << "<transition id="
+                   // field width stuff obsolete without büchi state printing.
+                   //<< std::setw(maxTransName + 2) << std::left
+                   << std::quoted(net->transitionNames()[transition]);
             if (traceLevel == TraceLevel::Full) {
-                os << indent << "<transition id=\"" << tname << "\">\n";
+                os << ">";
+                os << std::endl;
                 for (size_t i = 0; i < net->numberOfPlaces(); ++i) {
                     for (size_t j = 0; j < state.marking()[i]; ++j) {
                         os << tokenIndent << R"(<token age="0" place=")" << net->placeNames()[i] << "\"/>\n";
                     }
                 }
-#ifndef NDEBUG
-                os << '\n' << tokenIndent << "<buchi state=\"" << state.getBuchiState() << "\"/>\n";
-#endif
                 os << indent << "</transition>";
-            } else {
-                os << indent << "<transition id="
-                   << std::setw(maxTransName + 1 + 2) << std::left
-                   << std::quoted(tname) << " " << "buchisucc=\""
-                   << state.getBuchiState() << "\"/>";
+            }
+            else {
+                os << "/>";
             }
             return os;
         }
-
     };
-
-    extern template
-    class ModelChecker<LTL::ResumingSuccessorGenerator>;
-
-    extern template
-    class ModelChecker<LTL::SpoolingSuccessorGenerator>;
 }
 
 #endif //VERIFYPN_MODELCHECKER_H

=== modified file 'include/LTL/Algorithm/NestedDepthFirstSearch.h'
--- include/LTL/Algorithm/NestedDepthFirstSearch.h	2021-04-02 09:54:38 +0000
+++ include/LTL/Algorithm/NestedDepthFirstSearch.h	2021-08-05 10:56:53 +0000
@@ -45,14 +45,13 @@
      * @tparam W type used for state storage. Use <code>PetriEngine::Structures::TracableStateSet</code> if you want traces,
      *         <code>PetriEngine::Structures::StateSet</code> if you don't care (as it is faster).
      */
-    template<typename W>
-class NestedDepthFirstSearch : public ModelChecker<LTL::ResumingSuccessorGenerator> {
+    template<typename SucGen, typename W>
+class NestedDepthFirstSearch : public ModelChecker<ProductSuccessorGenerator, SucGen> {
     public:
         NestedDepthFirstSearch(const PetriEngine::PetriNet *net, const PetriEngine::PQL::Condition_ptr &query,
-                               const Structures::BuchiAutomaton &buchi,
-                               TraceLevel level = TraceLevel::Full, const bool shortcircuitweak = true)
-                : ModelChecker(net, query, buchi, LTL::ResumingSuccessorGenerator{*net, query}, level, shortcircuitweak),
-                  factory{net, successorGenerator->initial_buchi_state()},
+                               const Structures::BuchiAutomaton &buchi, SucGen *gen)
+                : ModelChecker<ProductSuccessorGenerator, SucGen>(net, query, buchi, gen),
+                  factory{net, this->successorGenerator->initial_buchi_state()},
                   states(*net, 0, (int) net->numberOfPlaces() + 1) {}
 
         bool isSatisfied() override;
@@ -69,7 +68,7 @@
 
         struct StackEntry {
             size_t id;
-            successor_info sucinfo;
+            typename SucGen::sucinfo sucinfo;
         };
 
         State *seed;
@@ -88,10 +87,16 @@
     };
 
     extern template
-    class NestedDepthFirstSearch<PetriEngine::Structures::StateSet>;
-
-    extern template
-    class NestedDepthFirstSearch<PetriEngine::Structures::TracableStateSet>;
+    class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, PetriEngine::Structures::StateSet>;
+
+    extern template
+    class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, PetriEngine::Structures::TracableStateSet>;
+
+    extern template
+    class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, PetriEngine::Structures::StateSet>;
+
+    extern template
+    class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, PetriEngine::Structures::TracableStateSet>;
 }
 
 #endif //VERIFYPN_NESTEDDEPTHFIRSTSEARCH_H

=== removed file 'include/LTL/Algorithm/RandomNDFS.h'
=== modified file 'include/LTL/Algorithm/TarjanModelChecker.h'
--- include/LTL/Algorithm/TarjanModelChecker.h	2021-04-06 13:25:35 +0000
+++ include/LTL/Algorithm/TarjanModelChecker.h	2021-08-05 10:56:53 +0000
@@ -25,6 +25,7 @@
 #include "LTL/SuccessorGeneration/ResumingSuccessorGenerator.h"
 #include "LTL/SuccessorGeneration/SpoolingSuccessorGenerator.h"
 
+#include <limits>
 #include <stack>
 #include <unordered_set>
 
@@ -36,21 +37,20 @@
      * which constitutes a counter-example.
      * For more details see
      * <p>
-     *   Jaco Geldenhuys & Antti Valmari,
-     *   More efficient on-the-fly LTL verification with Tarjan's algorithm,
+     *   Jaco Geldenhuys & Antti Valmari
+     *   More efficient on-the-fly LTL verification with Tarjan's algorithm
      *   https://doi.org/10.1016/j.tcs.2005.07.004
      * </p>
      * @tparam SaveTrace whether to save and print counter-examples when possible.
      */
-    template<typename SuccessorGen, bool SaveTrace = false>
-    class TarjanModelChecker : public ModelChecker<SuccessorGen> {
+    template<template <typename, typename...> typename ProductSucGen, typename SuccessorGen, bool SaveTrace = false, typename... Spooler>
+    class TarjanModelChecker : public ModelChecker<ProductSucGen, SuccessorGen, Spooler...> {
     public:
         TarjanModelChecker(const PetriEngine::PetriNet *net, const PetriEngine::PQL::Condition_ptr &cond,
                            const Structures::BuchiAutomaton &buchi,
-                           SuccessorGen &&successorGen,
-                           const TraceLevel level = TraceLevel::Full,
-                           const bool shortcircuitweak = true)
-                : ModelChecker<SuccessorGen>(net, cond, buchi, std::move(successorGen), level, shortcircuitweak),
+                           SuccessorGen *successorGen,
+                           std::unique_ptr<Spooler> &&...spooler)
+                : ModelChecker<ProductSucGen, SuccessorGen, Spooler...>(net, cond, buchi, successorGen, std::move(spooler)...),
                   factory(net, this->successorGenerator->initial_buchi_state()),
                   seen(net, 0)
         {
@@ -96,6 +96,7 @@
             idx_t lowlink;
             idx_t stateid;
             idx_t next = std::numeric_limits<idx_t>::max();
+            bool dstack = true;
 
             PlainCEntry(idx_t lowlink, idx_t stateid, idx_t next) : lowlink(lowlink), stateid(stateid), next(next) {}
         };
@@ -113,6 +114,7 @@
 
         struct DEntry {
             idx_t pos; // position in cstack.
+
             typename SuccessorGen::sucinfo sucinfo;
 
             explicit DEntry(idx_t pos) : pos(pos), sucinfo(SuccessorGen::initial_suc_info()) {}
@@ -143,18 +145,29 @@
         void printTrace(std::stack<DEntry> &&dstack, std::ostream &os = std::cout);
 
     };
-
-    extern template
-    class TarjanModelChecker<LTL::ResumingSuccessorGenerator, true>;
-
-    extern template
-    class TarjanModelChecker<LTL::ResumingSuccessorGenerator, false>;
-
-    extern template
-    class TarjanModelChecker<LTL::SpoolingSuccessorGenerator, true>;
-
-    extern template
-    class TarjanModelChecker<LTL::SpoolingSuccessorGenerator, false>;
+    extern template
+    class TarjanModelChecker<ProductSuccessorGenerator, LTL::ResumingSuccessorGenerator, true>;
+
+    extern template
+    class TarjanModelChecker<ProductSuccessorGenerator, LTL::ResumingSuccessorGenerator, false>;
+
+    extern template
+    class TarjanModelChecker<ProductSuccessorGenerator, LTL::SpoolingSuccessorGenerator, true>;
+
+    extern template
+    class TarjanModelChecker<ProductSuccessorGenerator, LTL::SpoolingSuccessorGenerator, false>;
+
+    extern template
+    class TarjanModelChecker<ReachStubProductSuccessorGenerator, LTL::SpoolingSuccessorGenerator, true, VisibleLTLStubbornSet>;
+
+    extern template
+    class TarjanModelChecker<ReachStubProductSuccessorGenerator, LTL::SpoolingSuccessorGenerator, false, VisibleLTLStubbornSet>;
+
+    extern template
+    class TarjanModelChecker<ReachStubProductSuccessorGenerator, LTL::SpoolingSuccessorGenerator, true, EnabledSpooler>;
+
+    extern template
+    class TarjanModelChecker<ReachStubProductSuccessorGenerator, LTL::SpoolingSuccessorGenerator, false, EnabledSpooler>;
 }
 
 #endif //VERIFYPN_TARJANMODELCHECKER_H

=== modified file 'include/LTL/LTL.h'
--- include/LTL/LTL.h	2021-03-23 14:10:04 +0000
+++ include/LTL/LTL.h	2021-08-05 10:56:53 +0000
@@ -21,7 +21,6 @@
 #include "LTL/LTLValidator.h"
 #include "LTL/Algorithm/TarjanModelChecker.h"
 #include "LTL/Algorithm/NestedDepthFirstSearch.h"
-#include "LTL/Algorithm/RandomNDFS.h"
 #include "LTL/Simplification/SpotToPQL.h"
 #include "LTL/LTLToBuchi.h"
 

=== modified file 'include/LTL/LTLMain.h'
--- include/LTL/LTLMain.h	2021-04-07 08:50:10 +0000
+++ include/LTL/LTLMain.h	2021-08-05 10:56:53 +0000
@@ -23,7 +23,7 @@
 #include "PetriEngine/options.h"
 
 namespace LTL {
-    ReturnValue LTLMain(const PetriEngine::PetriNet *net,
+    bool LTLMain(const PetriEngine::PetriNet *net,
                         const PetriEngine::PQL::Condition_ptr &query,
                         const std::string &queryName,
                         options_t &options);

=== modified file 'include/LTL/LTLToBuchi.h'
--- include/LTL/LTLToBuchi.h	2021-04-06 13:10:00 +0000
+++ include/LTL/LTLToBuchi.h	2021-08-05 10:56:53 +0000
@@ -26,7 +26,6 @@
 #include <string>
 
 #include <spot/tl/formula.hh>
-
 namespace LTL {
     struct AtomicProposition {
         PetriEngine::PQL::Condition_ptr expression;
@@ -40,7 +39,7 @@
     void toSpotFormat(const QueryItem &query, std::ostream &os);
 
     std::pair<spot::formula, APInfo>
-    to_spot_formula(const PetriEngine::PQL::Condition_ptr &query, APCompression compress_aps);
+    to_spot_formula(const PetriEngine::PQL::Condition_ptr &query, const options_t &options);
 
     class BuchiSuccessorGenerator;
     namespace Structures {
@@ -49,10 +48,10 @@
 
     Structures::BuchiAutomaton makeBuchiAutomaton(
             const PetriEngine::PQL::Condition_ptr &query,
-            APCompression compress_aps = APCompression::Choose);
+            const options_t &options);
 
     BuchiSuccessorGenerator
-    makeBuchiSuccessorGenerator(const PetriEngine::PQL::Condition_ptr &query, APCompression compress_aps = APCompression::Choose);
+    makeBuchiSuccessorGenerator(const PetriEngine::PQL::Condition_ptr &query, const options_t &options);
 
     class FormulaToSpotSyntax : public PetriEngine::PQL::QueryPrinter {
     protected:

=== added file 'include/LTL/Replay.h'
--- include/LTL/Replay.h	1970-01-01 00:00:00 +0000
+++ include/LTL/Replay.h	2021-08-05 10:56:53 +0000
@@ -0,0 +1,66 @@
+/* Copyright (C) 2021  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ * 
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ * 
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ * 
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_REPLAY_H
+#define VERIFYPN_REPLAY_H
+
+#include "LTL/SuccessorGeneration/BuchiSuccessorGenerator.h"
+
+#include <iostream>
+#include <utility>
+#include <rapidxml.hpp>
+
+namespace LTL {
+    class Replay {
+    public:
+        Replay(std::istream &is, const PetriEngine::PetriNet *net);
+
+        struct Token {
+            std::string place;
+        };
+
+        struct Transition {
+            explicit Transition(std::string id, int buchi) : id(std::move(id)), buchi_state(buchi) {}
+
+            std::string id;
+            int buchi_state;
+            std::unordered_map<uint32_t, uint32_t> tokens;
+        };
+
+        void parse(std::istream &xml, const PetriEngine::PetriNet *net);
+
+        bool replay(const PetriEngine::PetriNet *net, const PetriEngine::PQL::Condition_ptr &cond, const options_t &options);
+
+        std::vector<Transition> trace;
+    private:
+
+        static constexpr auto DEADLOCK_TRANS = "##deadlock";
+        void parseRoot(const rapidxml::xml_node<> *pNode);
+
+        Transition parseTransition(const rapidxml::xml_node<char> *pNode);
+
+        void parseToken(const rapidxml::xml_node<char> *pNode, std::unordered_map<uint32_t, uint32_t> &current_marking);
+
+        size_t loop_idx = std::numeric_limits<size_t>::max();
+        std::unordered_map<std::string, int> transitions;
+        std::unordered_map<std::string, int> places;
+        bool _play_trace(const PetriEngine::PetriNet *net, PetriEngine::SuccessorGenerator &successorGenerator,
+                         BuchiSuccessorGenerator &buchiGenerator, size_t init_buchi);
+    };
+}
+
+#endif //VERIFYPN_REPLAY_H

=== added file 'include/LTL/Simplification/SpotToPQL.h'
--- include/LTL/Simplification/SpotToPQL.h	1970-01-01 00:00:00 +0000
+++ include/LTL/Simplification/SpotToPQL.h	2021-08-05 10:56:53 +0000
@@ -36,7 +36,7 @@
      * @param formula The formula to simplify.
      * @return the simplified formula.
      */
-    PetriEngine::PQL::Condition_ptr simplify(const PetriEngine::PQL::Condition_ptr &formula, APCompression compress = APCompression::Choose);
+    PetriEngine::PQL::Condition_ptr simplify(const PetriEngine::PQL::Condition_ptr &formula, const options_t &options);
 }
 
 #endif // VERIFYPN_SPOTTOPQL_H

=== removed file 'include/LTL/Simplification/SpotToPQL.h'
--- include/LTL/Simplification/SpotToPQL.h	2021-04-06 13:10:00 +0000
+++ include/LTL/Simplification/SpotToPQL.h	1970-01-01 00:00:00 +0000
@@ -36,7 +36,7 @@
      * @param formula The formula to simplify.
      * @return the simplified formula.
      */
-    PetriEngine::PQL::Condition_ptr simplify(const PetriEngine::PQL::Condition_ptr &formula, APCompression compress = APCompression::Choose);
+    PetriEngine::PQL::Condition_ptr simplify(const PetriEngine::PQL::Condition_ptr &formula, const options_t &options);
 }
 
 #endif // VERIFYPN_SPOTTOPQL_H

=== modified file 'include/LTL/Structures/BitProductStateSet.h'
--- include/LTL/Structures/BitProductStateSet.h	2021-04-16 20:55:16 +0000
+++ include/LTL/Structures/BitProductStateSet.h	2021-08-05 10:56:53 +0000
@@ -22,6 +22,7 @@
 #include "LTL/Structures/ProductState.h"
 #include <cstdint>
 #include <unordered_set>
+#include <unordered_map>
 
 namespace LTL::Structures {
 
@@ -63,7 +64,7 @@
     template<uint8_t nbits = 16>
     class BitProductStateSet : public ProductStateSetInterface {
     public:
-        explicit BitProductStateSet(const PetriEngine::PetriNet *net, int kbound = 0)
+        explicit BitProductStateSet(const PetriEngine::PetriNet *net, int kbound = 0, size_t nplaces = -1)
                 : markings(*net, kbound, net->numberOfPlaces())
         {
         }

=== modified file 'include/LTL/Structures/BuchiAutomaton.h'
--- include/LTL/Structures/BuchiAutomaton.h	2021-03-25 10:36:36 +0000
+++ include/LTL/Structures/BuchiAutomaton.h	2021-08-05 10:56:53 +0000
@@ -54,6 +54,35 @@
                     break;
             }
         }
+
+        /**
+         * Evaluate binary decision diagram (BDD) representation of transition guard in given state.
+         */
+        bool guard_valid(PetriEngine::PQL::EvaluationContext &ctx, bdd bdd) const
+        {
+            // IDs 0 and 1 are false and true atoms, respectively
+            // More details in buddy manual ( http://buddy.sourceforge.net/manual/main.html )
+            while (bdd.id() > 1) {
+                // find variable to test, and test it
+                size_t var = bdd_var(bdd);
+                using PetriEngine::PQL::Condition;
+                Condition::Result res = ap_info.at(var).expression->evaluate(ctx);
+                switch (res) {
+                    case Condition::RUNKNOWN:
+                        std::cerr << "Unexpected unknown answer from evaluating query!\n";
+                        assert(false);
+                        exit(1);
+                        break;
+                    case Condition::RFALSE:
+                        bdd = bdd_low(bdd);
+                        break;
+                    case Condition::RTRUE:
+                        bdd = bdd_high(bdd);
+                        break;
+                }
+            }
+            return bdd == bddtrue;
+        }
     };
 }
 

=== modified file 'include/LTL/Structures/GuardInfo.h'
--- include/LTL/Structures/GuardInfo.h	2021-02-24 10:25:55 +0000
+++ include/LTL/Structures/GuardInfo.h	2021-08-05 10:56:53 +0000
@@ -19,16 +19,57 @@
 #define VERIFYPN_GUARDINFO_H
 
 #include "PetriEngine/PQL/PQL.h"
+#include "LTL/Structures/BuchiAutomaton.h"
+#include "LTL/Simplification/SpotToPQL.h"
+
 #include <vector>
+#include <spot/twa/twagraph.hh>
+#include <spot/twa/formula2bdd.hh>
+
+
 
 namespace LTL {
     struct GuardInfo {
+
+        struct Guard {
+            PetriEngine::PQL::Condition_ptr condition;
+            bdd decision_diagram;
+            uint32_t dest;
+
+            explicit operator bool () {
+                return bool(condition);
+            }
+        };
+
         GuardInfo(size_t buchiState, bool isAccepting) : buchi_state(buchiState), is_accepting(isAccepting) {}
 
         int buchi_state;
-        PetriEngine::PQL::Condition_ptr retarding;
-        std::vector<PetriEngine::PQL::Condition_ptr> progressing;
+        Guard retarding;
+        std::vector<Guard> progressing;
         bool is_accepting;
+
+
+        static std::vector<GuardInfo> from_automaton(const Structures::BuchiAutomaton &aut) {
+            std::vector<GuardInfo> state_guards;
+            std::vector<AtomicProposition> aps(aut.ap_info.size());
+            std::transform(std::begin(aut.ap_info), std::end(aut.ap_info), std::begin(aps),
+                           [](const std::pair<int, AtomicProposition> &pair) { return pair.second; });
+            for (unsigned state = 0; state < aut._buchi->num_states(); ++state) {
+                state_guards.emplace_back(state, aut._buchi->state_is_accepting(state));
+                for (auto &e : aut._buchi->out(state)) {
+                    auto formula = spot::bdd_to_formula(e.cond, aut.dict);
+                    if (e.dst == state) {
+                        state_guards.back().retarding = Guard{toPQL(formula, aps), e.cond, state};
+                    } else {
+                        state_guards.back().progressing.push_back(Guard{toPQL(formula, aps), e.cond, e.dst});
+                    }
+                }
+                if (!state_guards.back().retarding) {
+                    state_guards.back().retarding = Guard{std::make_shared<PetriEngine::PQL::BooleanCondition>(false), bddfalse, state};
+                }
+            }
+            return state_guards;
+        }
     };
 }
 

=== modified file 'include/LTL/Structures/ProductState.h'
--- include/LTL/Structures/ProductState.h	2021-03-23 14:10:04 +0000
+++ include/LTL/Structures/ProductState.h	2021-08-05 10:56:53 +0000
@@ -41,7 +41,6 @@
             buchi_state_idx = nplaces;
         }
 
-        //TODO override equality operators to handle both marking and NBA state
         uint32_t getBuchiState() const {
             return marking()[buchi_state_idx];
         }

=== added directory 'include/LTL/Stubborn'
=== added file 'include/LTL/Stubborn/AutomatonStubbornSet.h'
--- include/LTL/Stubborn/AutomatonStubbornSet.h	1970-01-01 00:00:00 +0000
+++ include/LTL/Stubborn/AutomatonStubbornSet.h	2021-08-05 10:56:53 +0000
@@ -0,0 +1,99 @@
+/* Copyright (C) 2021  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ * 
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ * 
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ * 
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_AUTOMATONSTUBBORNSET_H
+#define VERIFYPN_AUTOMATONSTUBBORNSET_H
+
+#include "LTL/Structures/BuchiAutomaton.h"
+#include "PetriEngine/Stubborn/ReachabilityStubbornSet.h"
+#include "PetriEngine/PQL/PQL.h"
+#include "LTL/Structures/GuardInfo.h"
+#include "LTL/SuccessorGeneration/SuccessorSpooler.h"
+#include "PetriEngine/SuccessorGenerator.h"
+
+namespace LTL {
+    class NondeterministicConjunctionVisitor;
+    class AutomatonStubbornSet : public PetriEngine::StubbornSet, public SuccessorSpooler {
+    public:
+        explicit AutomatonStubbornSet(const PetriEngine::PetriNet &net, const Structures::BuchiAutomaton &aut)
+        : PetriEngine::StubbornSet(net), _retarding_stubborn_set(net,false),
+            _state_guards(std::move(GuardInfo::from_automaton(aut))),
+            _aut(aut),
+            _place_checkpoint(new bool[net.numberOfPlaces()]),
+            _gen(_net)
+        {
+            _markbuf.setMarking(net.makeInitialMarking());
+            _retarding_stubborn_set.setInterestingVisitor<PetriEngine::AutomatonInterestingTransitionVisitor>();
+        }
+
+        bool prepare(const PetriEngine::Structures::State *marking) override {
+            return prepare(dynamic_cast<const LTL::Structures::ProductState*>(marking));
+        }
+
+        bool prepare(const LTL::Structures::ProductState *state) override;
+
+        uint32_t next() override;
+
+        void reset() override;
+
+
+    private:
+        static bool has_shared_mark(const bool* a, const bool* b, size_t size) {
+            for (size_t i = 0; i < size; ++i) {
+                if (a[i] && b[i]) return true;
+            }
+            return false;
+        }
+
+    protected:
+        void addToStub(uint32_t t) override;
+
+    private:
+
+        PetriEngine::ReachabilityStubbornSet _retarding_stubborn_set;
+        const std::vector<GuardInfo> _state_guards;
+        const Structures::BuchiAutomaton &_aut;
+        std::unique_ptr<bool[]> _place_checkpoint;
+        PetriEngine::SuccessorGenerator _gen;
+        PetriEngine::Structures::State _markbuf;
+        bool _has_enabled_stubborn = false;
+        bool _bad = false;
+        bool _done = false;
+        bool _track_changes = false;
+        bool _retarding_satisfied;
+
+        std::unordered_set<uint32_t> _pending_stubborn;
+
+
+        void _reset_pending();
+
+        void _apply_pending();
+
+        void __print_debug();
+
+        void set_all_stubborn();
+
+        bool _closure();
+
+        bool _cond3_valid(uint32_t t);
+
+        friend class NondeterministicConjunctionVisitor;
+    };
+
+}
+
+#endif //VERIFYPN_AUTOMATONSTUBBORNSET_H

=== added file 'include/LTL/Stubborn/EvalAndSetVisitor.h'
--- include/LTL/Stubborn/EvalAndSetVisitor.h	1970-01-01 00:00:00 +0000
+++ include/LTL/Stubborn/EvalAndSetVisitor.h	2021-08-05 10:56:53 +0000
@@ -0,0 +1,74 @@
+/* Copyright (C) 2021  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ * 
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ * 
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ * 
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_EVALANDSETVISITOR_H
+#define VERIFYPN_EVALANDSETVISITOR_H
+
+#include "PetriEngine/PQL/MutatingVisitor.h"
+#include "PetriEngine/PQL/Contexts.h"
+
+namespace LTL {
+
+    class EvalAndSetVisitor : public PetriEngine::PQL::MutatingVisitor {
+
+    public:
+        EvalAndSetVisitor(const PetriEngine::PQL::EvaluationContext &context) : _context(context) {}
+
+    private:
+        const PetriEngine::PQL::EvaluationContext &_context;
+    protected:
+
+    protected:
+        void _accept(PetriEngine::PQL::ACondition *condition) override;
+
+        void _accept(PetriEngine::PQL::ECondition *condition) override;
+
+        void _accept(PetriEngine::PQL::GCondition *condition) override;
+
+        void _accept(PetriEngine::PQL::FCondition *condition) override;
+
+        void _accept(PetriEngine::PQL::XCondition *condition) override;
+
+        void _accept(PetriEngine::PQL::UntilCondition *condition) override;
+
+        void _accept(PetriEngine::PQL::NotCondition *element) override;
+
+        void _accept(PetriEngine::PQL::AndCondition *element) override;
+
+        void _accept(PetriEngine::PQL::OrCondition *element) override;
+
+        void _accept(PetriEngine::PQL::LessThanCondition *element) override;
+
+        void _accept(PetriEngine::PQL::LessThanOrEqualCondition *element) override;
+
+        void _accept(PetriEngine::PQL::EqualCondition *element) override;
+
+        void _accept(PetriEngine::PQL::NotEqualCondition *element) override;
+
+        void _accept(PetriEngine::PQL::DeadlockCondition *element) override;
+
+        void _accept(PetriEngine::PQL::CompareConjunction *element) override;
+
+        void _accept(PetriEngine::PQL::UnfoldedUpperBoundsCondition *element) override;
+
+        void _accept(PetriEngine::PQL::BooleanCondition *element) override;
+    };
+
+}
+
+
+#endif //VERIFYPN_EVALANDSETVISITOR_H

=== added file 'include/LTL/Stubborn/ReachabilityStubbornSpooler.h'
--- include/LTL/Stubborn/ReachabilityStubbornSpooler.h	1970-01-01 00:00:00 +0000
+++ include/LTL/Stubborn/ReachabilityStubbornSpooler.h	2021-08-05 10:56:53 +0000
@@ -0,0 +1,52 @@
+/* Copyright (C) 2021  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ * 
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ * 
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ * 
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_REACHABILITYSTUBBORNSPOOLER_H
+#define VERIFYPN_REACHABILITYSTUBBORNSPOOLER_H
+
+#include "LTL/SuccessorGeneration/SuccessorSpooler.h"
+#include "PetriEngine/Stubborn/ReachabilityStubbornSet.h"
+#include "PetriEngine/Stubborn/InterestingTransitionVisitor.h"
+
+namespace LTL {
+    class ReachabilityStubbornSpooler : public SuccessorSpooler {
+    public:
+        ReachabilityStubbornSpooler(const PetriEngine::PetriNet &net, const std::vector<PetriEngine::PQL::Condition_ptr> &conds)
+                : _stubborn(net, conds) {
+            _stubborn.setInterestingVisitor<PetriEngine::InterestingLTLTransitionVisitor>();
+        }
+
+        bool prepare(const LTL::Structures::ProductState *state) override
+        {
+            return _stubborn.prepare(state);
+        }
+
+        uint32_t next() override
+        {
+            return _stubborn.next();
+        }
+
+        void reset() override
+        {
+            _stubborn.reset();
+        }
+
+    private:
+        PetriEngine::ReachabilityStubbornSet _stubborn;
+    };
+}
+#endif //VERIFYPN_REACHABILITYSTUBBORNSPOOLER_H

=== added file 'include/LTL/Stubborn/ReducingSuccessorGenerator.h'
--- include/LTL/Stubborn/ReducingSuccessorGenerator.h	1970-01-01 00:00:00 +0000
+++ include/LTL/Stubborn/ReducingSuccessorGenerator.h	2021-08-05 10:56:53 +0000
@@ -0,0 +1,46 @@
+/* Copyright (C) 2021  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ * 
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ * 
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ * 
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_REDUCINGSUCCESSORGENERATOR_H
+#define VERIFYPN_REDUCINGSUCCESSORGENERATOR_H
+
+#include "PetriEngine/ReducingSuccessorGenerator.h"
+#include "LTL/SuccessorGeneration/AutomatonStubbornSet.h"
+
+#include <utility>
+
+namespace LTL {
+    class ReducingSuccessorGenerator : public PetriEngine::ReducingSuccessorGenerator {
+    public:
+        ReducingSuccessorGenerator(const PetriEngine::PetriNet &net, const PetriEngine::PQL::Condition_ptr &query)
+                : PetriEngine::ReducingSuccessorGenerator(net, std::make_shared<AutomatonStubbornSet>(net, query)) {}
+
+        ReducingSuccessorGenerator(const PetriEngine::PetriNet &net, const std::shared_ptr<AutomatonStubbornSet> &stubSet)
+                : PetriEngine::ReducingSuccessorGenerator(net, stubSet) {}
+
+
+        bool prepare(const PetriEngine::Structures::State *state, const LTL::GuardInfo &info)
+        {
+            _current = 0;
+            _parent = state;
+            return (dynamic_pointer_cast<LTL::AutomatonStubbornSet>(_stubSet))->prepare(state, info);
+        }
+
+    };
+}
+
+#endif //VERIFYPN_REDUCINGSUCCESSORGENERATOR_H

=== added file 'include/LTL/Stubborn/SafeAutStubbornSet.h'
--- include/LTL/Stubborn/SafeAutStubbornSet.h	1970-01-01 00:00:00 +0000
+++ include/LTL/Stubborn/SafeAutStubbornSet.h	2021-08-05 10:56:53 +0000
@@ -0,0 +1,71 @@
+/* Copyright (C) 2021  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ * 
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ * 
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ * 
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_SAFEAUTSTUBBORNSET_H
+#define VERIFYPN_SAFEAUTSTUBBORNSET_H
+
+#include "PetriEngine/Stubborn/InterestingTransitionVisitor.h"
+#include "LTL/SuccessorGeneration/SuccessorSpooler.h"
+#include "PetriEngine/Stubborn/StubbornSet.h"
+#include "PetriEngine/PQL/PQL.h"
+
+namespace LTL {
+    class SafeAutStubbornSet : public PetriEngine::StubbornSet, public SuccessorSpooler {
+    public:
+        SafeAutStubbornSet(const PetriEngine::PetriNet &net,
+                           const std::vector<PetriEngine::PQL::Condition_ptr> &queries)
+                : StubbornSet(net, queries), _unsafe(std::make_unique<bool[]>(net.numberOfTransitions())) {}
+
+        bool prepare(const PetriEngine::Structures::State *marking) override
+        {
+            assert(false);
+            std::cerr << "Error: SafeAutStubbornSet is implemented only for product states\n";
+            exit(1);
+            return false;
+        }
+
+        bool prepare(const LTL::Structures::ProductState *state) override;
+
+        uint32_t next() override {
+            return StubbornSet::next();
+        }
+
+        void reset() override {
+            StubbornSet::reset();
+            memset(_unsafe.get(), false, sizeof(bool) * _net.numberOfTransitions());
+            _bad = false;
+        }
+
+    protected:
+        void addToStub(uint32_t t) override
+        {
+            //refinement of bad: can manually check whether firing t would violate some progressing formula.
+            if (_unsafe[t] && _enabled[t]) {
+                _bad = true;
+                return;
+            }
+            //TODO check safe-ness
+            StubbornSet::addToStub(t);
+        }
+
+    private:
+        std::unique_ptr<bool[]> _unsafe;
+        bool _bad = false;
+    };
+}
+
+#endif //VERIFYPN_SAFEAUTSTUBBORNSET_H

=== added file 'include/LTL/Stubborn/VisibleLTLStubbornSet.h'
--- include/LTL/Stubborn/VisibleLTLStubbornSet.h	1970-01-01 00:00:00 +0000
+++ include/LTL/Stubborn/VisibleLTLStubbornSet.h	2021-08-05 10:56:53 +0000
@@ -0,0 +1,111 @@
+/* Copyright (C) 2021  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_VISIBLELTLSTUBBORNSET_H
+#define VERIFYPN_VISIBLELTLSTUBBORNSET_H
+
+
+//#include "PetriEngine/ReducingSuccessorGenerator.h"
+#include "PetriEngine/Stubborn/StubbornSet.h"
+#include "PetriEngine/PQL/PQL.h"
+#include "LTL/Stubborn/VisibleTransitionVisitor.h"
+#include "LTL/SuccessorGeneration/SuccessorSpooler.h"
+
+// TODO LTL Stubborn sets should be subclassing just PetriEngine::StubbornSet, then a class
+// LTL::StubbornSuccessorSpooler : LTL::SuccessorSpooler has a stubborn set via simple wrapping.
+// This way we can avoid the super ugly multiple inheritance caused by both base classes
+// each having prepare, next, reset methods.q
+namespace LTL {
+    class VisibleLTLStubbornSet : public PetriEngine::StubbornSet, public SuccessorSpooler {
+    public:
+        VisibleLTLStubbornSet(const PetriEngine::PetriNet &net,
+                              const std::vector<PetriEngine::PQL::Condition_ptr> &queries)
+                : StubbornSet(net, queries), _visible(new bool[net.numberOfTransitions()])
+        {
+            assert(!_netContainsInhibitorArcs);
+            memset(_visible.get(), 0, sizeof(bool) * net.numberOfPlaces());
+            VisibleTransitionVisitor visible{_visible};
+            for (auto &q : queries) {
+                q->visit(visible);
+            }
+        }
+
+        VisibleLTLStubbornSet(const PetriEngine::PetriNet &net, const PetriEngine::PQL::Condition_ptr &query)
+                : StubbornSet(net, query), _visible(new bool[net.numberOfTransitions()])
+        {
+            assert(!_netContainsInhibitorArcs);
+            auto places = std::make_unique<bool[]>(net.numberOfPlaces());
+            memset(places.get(), 0, sizeof(bool) * net.numberOfPlaces());
+            memset(_visible.get(), 0, sizeof(bool) * net.numberOfTransitions());
+            VisibleTransitionVisitor visible{places};
+            query->visit(visible);
+
+            memset(_places_seen.get(), 0, _net.numberOfPlaces());
+            for (uint32_t p = 0; p < net.numberOfPlaces(); ++p) {
+                if (places[p]) {
+                    visTrans(p);
+                }
+            }
+        }
+
+        void visTrans(uint32_t place)
+        {
+            if (_places_seen[place] > 0) return;
+            _places_seen[place] = 1;
+            for (uint32_t t = _places[place].pre; t < _places[place].post; ++t) {
+                auto tr = _transitions[t];
+                _visible[tr.index] = true;
+            }
+            for (uint32_t t = _places.get()[place].post; t < _places.get()[place + 1].pre; t++) {
+                auto tr = _transitions[t];
+                if (tr.direction < 0)
+                    _visible[tr.index] = true;
+            }
+        }
+
+        bool prepare(const PetriEngine::Structures::State *marking) override;
+
+        bool prepare(const LTL::Structures::ProductState *marking) override
+        {
+            return prepare((const PetriEngine::Structures::State *) marking);
+        }
+
+        uint32_t next() override;
+
+        void reset();
+
+        bool generateAll(const LTL::Structures::ProductState *parent);
+
+    protected:
+        void addToStub(uint32_t t) override;
+
+    private:
+        std::unique_ptr<bool[]> _visible;
+        light_deque<uint32_t> _skipped;
+        uint32_t _key;
+        bool _has_enabled_stubborn;
+
+        void findKeyTransition();
+
+        void ensureRuleV();
+
+        void ensureRulesL();
+
+    };
+}
+
+#endif //VERIFYPN_VISIBLELTLSTUBBORNSET_H

=== added file 'include/LTL/Stubborn/VisibleTransitionVisitor.h'
--- include/LTL/Stubborn/VisibleTransitionVisitor.h	1970-01-01 00:00:00 +0000
+++ include/LTL/Stubborn/VisibleTransitionVisitor.h	2021-08-05 10:56:53 +0000
@@ -0,0 +1,82 @@
+/* Copyright (C) 2021  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ * 
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ * 
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ * 
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_VISIBLETRANSITIONVISITOR_H
+#define VERIFYPN_VISIBLETRANSITIONVISITOR_H
+
+#include "PetriEngine/PQL/Visitor.h"
+#include "PetriEngine/PQL/PQL.h"
+#include "PetriEngine/PetriNet.h"
+#include "PetriEngine/Structures/light_deque.h"
+
+namespace LTL {
+    class VisibleTransitionVisitor : public PetriEngine::PQL::Visitor {
+    public:
+        explicit VisibleTransitionVisitor(std::unique_ptr<bool[]> &visible)
+                : _places(visible) {}
+
+    protected:
+        void _accept(const PetriEngine::PQL::NotCondition *element) override;
+
+        void _accept(const PetriEngine::PQL::AndCondition *element) override;
+
+        void _accept(const PetriEngine::PQL::OrCondition *element) override;
+
+        void _accept(const PetriEngine::PQL::LessThanCondition *element) override;
+
+        void _accept(const PetriEngine::PQL::LessThanOrEqualCondition *element) override;
+
+        void _accept(const PetriEngine::PQL::EqualCondition *element) override;
+
+        void _accept(const PetriEngine::PQL::NotEqualCondition *element) override;
+
+        void _accept(const PetriEngine::PQL::DeadlockCondition *element) override;
+
+        void _accept(const PetriEngine::PQL::CompareConjunction *element) override;
+
+        void _accept(const PetriEngine::PQL::UnfoldedUpperBoundsCondition *element) override;
+
+        void _accept(const PetriEngine::PQL::UnfoldedIdentifierExpr *element) override;
+
+        void _accept(const PetriEngine::PQL::LiteralExpr *element) override;
+
+        void _accept(const PetriEngine::PQL::PlusExpr *element) override;
+
+        void _accept(const PetriEngine::PQL::MultiplyExpr *element) override;
+
+        void _accept(const PetriEngine::PQL::MinusExpr *element) override;
+
+        void _accept(const PetriEngine::PQL::SubtractExpr *element) override;
+
+        void _accept(const PetriEngine::PQL::ACondition *condition) override;
+
+        void _accept(const PetriEngine::PQL::ECondition *condition) override;
+
+        void _accept(const PetriEngine::PQL::GCondition *condition) override;
+
+        void _accept(const PetriEngine::PQL::FCondition *condition) override;
+
+        void _accept(const PetriEngine::PQL::XCondition *condition) override;
+
+        void _accept(const PetriEngine::PQL::UntilCondition *condition) override;
+
+    private:
+        std::unique_ptr<bool[]> &_places;
+    };
+}
+
+#endif //VERIFYPN_VISIBLETRANSITIONVISITOR_H

=== modified file 'include/LTL/SuccessorGeneration/AutomatonHeuristic.h'
--- include/LTL/SuccessorGeneration/AutomatonHeuristic.h	2021-03-24 07:31:53 +0000
+++ include/LTL/SuccessorGeneration/AutomatonHeuristic.h	2021-08-05 10:56:53 +0000
@@ -31,10 +31,16 @@
 
         bool has_heuristic(const Structures::ProductState &state) override;
 
-    private:
+        std::ostream &output(std::ostream &os) {
+            return os << "AUTOMATON_HEUR";
+        }
+
+    protected:
         const PetriEngine::PetriNet *_net;
         const LTL::Structures::BuchiAutomaton &_aut;
         std::vector<GuardInfo> _state_guards;
+
+        std::vector<uint32_t> _bfs_dists;
     };
 }
 

=== modified file 'include/LTL/SuccessorGeneration/BuchiSuccessorGenerator.h'
--- include/LTL/SuccessorGeneration/BuchiSuccessorGenerator.h	2021-03-31 11:41:47 +0000
+++ include/LTL/SuccessorGeneration/BuchiSuccessorGenerator.h	2021-08-05 10:56:53 +0000
@@ -114,7 +114,7 @@
 
         using _succ_iter = std::unique_ptr<spot::twa_succ_iterator, SuccIterDeleter>;
         _succ_iter succ = nullptr;
-            private:
+    private:
 
         enum class InvariantSelfLoop {
             TRUE, FALSE, UNKNOWN

=== added file 'include/LTL/SuccessorGeneration/ComposedHeuristic.h'
--- include/LTL/SuccessorGeneration/ComposedHeuristic.h	1970-01-01 00:00:00 +0000
+++ include/LTL/SuccessorGeneration/ComposedHeuristic.h	2021-08-05 10:56:53 +0000
@@ -0,0 +1,53 @@
+/* Copyright (C) 2021  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ * 
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ * 
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ * 
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_COMPOSEDHEURISTIC_H
+#define VERIFYPN_COMPOSEDHEURISTIC_H
+
+#include "Heuristic.h"
+
+#include <utility>
+
+namespace LTL {
+
+    class ComposedHeuristic : public Heuristic {
+    public:
+
+        ComposedHeuristic(std::unique_ptr<Heuristic> primary, std::unique_ptr<Heuristic> secondary)
+                : _primary(std::move(primary)), _secondary(std::move(secondary)) {}
+
+        void prepare(const Structures::ProductState &state) override {
+            _primary->prepare(state);
+            _secondary->prepare(state);
+        }
+
+        uint32_t eval(const Structures::ProductState &state, uint32_t tid) override = 0;
+
+        bool has_heuristic(const Structures::ProductState &state) override {
+            _primary_has_heuristic = _primary->has_heuristic(state);
+            _secondary_has_heuristic = _secondary->has_heuristic(state);
+            return _primary_has_heuristic || _secondary_has_heuristic;
+        }
+
+    protected:
+        std::unique_ptr<Heuristic> _primary, _secondary;
+        bool _primary_has_heuristic = false, _secondary_has_heuristic = false;
+    };
+
+}
+
+#endif //VERIFYPN_COMPOSEDHEURISTIC_H

=== modified file 'include/LTL/SuccessorGeneration/DistanceHeuristic.h'
--- include/LTL/SuccessorGeneration/DistanceHeuristic.h	2021-03-19 11:48:52 +0000
+++ include/LTL/SuccessorGeneration/DistanceHeuristic.h	2021-08-05 10:56:53 +0000
@@ -34,6 +34,9 @@
             return _cond->distance(context);
         }
 
+        std::ostream &output(std::ostream &os) {
+            return os << "DIST_HEUR";
+        }
     private:
         const PetriEngine::PetriNet *_net;
         const PetriEngine::PQL::Condition_ptr _cond;

=== added file 'include/LTL/SuccessorGeneration/FireCountHeuristic.h'
--- include/LTL/SuccessorGeneration/FireCountHeuristic.h	1970-01-01 00:00:00 +0000
+++ include/LTL/SuccessorGeneration/FireCountHeuristic.h	2021-08-05 10:56:53 +0000
@@ -0,0 +1,57 @@
+/* Copyright (C) 2021  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ * 
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ * 
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ * 
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_FIRECOUNTHEURISTIC_H
+#define VERIFYPN_FIRECOUNTHEURISTIC_H
+
+#include "LTL/SuccessorGeneration/Heuristic.h"
+
+namespace LTL {
+    class FireCountHeuristic : public Heuristic {
+    public:
+        explicit FireCountHeuristic(const PetriEngine::PetriNet *net) : _fireCount(net->numberOfTransitions()) {}
+
+        uint32_t eval(const Structures::ProductState &state, uint32_t tid) override {
+            assert(tid <= _fireCount.size());
+            return _fireCount[tid];
+        }
+
+        bool has_heuristic(const Structures::ProductState &state) override {
+            return true;
+        }
+
+        void push(uint32_t tid) override {
+            assert(tid <= _fireCount.size());
+            ++_fireCount[tid];
+        }
+
+        void pop(uint32_t tid) override {
+            assert(tid <= _fireCount.size());
+            --_fireCount[tid];
+        }
+
+        std::ostream &output(std::ostream &os) {
+            return os << "FIRECOUNT_HEUR";
+        }
+
+
+    protected:
+        std::vector<uint32_t> _fireCount;
+    };
+}
+
+#endif //VERIFYPN_FIRECOUNTHEURISTIC_H

=== modified file 'include/LTL/SuccessorGeneration/Heuristic.h'
--- include/LTL/SuccessorGeneration/Heuristic.h	2021-03-24 07:31:53 +0000
+++ include/LTL/SuccessorGeneration/Heuristic.h	2021-08-05 10:56:53 +0000
@@ -20,10 +20,13 @@
 
 #include "PetriEngine/PetriNet.h"
 #include "LTL/Structures/ProductState.h"
+#include <iostream>
 
 namespace LTL {
     class Heuristic {
     public:
+        virtual void prepare(const LTL::Structures::ProductState &state) {}
+
         virtual uint32_t eval(const LTL::Structures::ProductState &state, uint32_t tid) = 0;
 
         /**
@@ -35,7 +38,13 @@
             return true;
         }
 
+        virtual void push(uint32_t tid) {};
+
+        virtual void pop(uint32_t tid) {};
+
         virtual ~Heuristic() = default;
+
+        virtual std::ostream &output(std::ostream &os) = 0;
     };
 }
 

=== added file 'include/LTL/SuccessorGeneration/HeuristicParser.h'
--- include/LTL/SuccessorGeneration/HeuristicParser.h	1970-01-01 00:00:00 +0000
+++ include/LTL/SuccessorGeneration/HeuristicParser.h	2021-08-05 10:56:53 +0000
@@ -0,0 +1,28 @@
+/* Copyright (C) 2021  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ * 
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ * 
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ * 
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_HEURISTICPARSER_H
+#define VERIFYPN_HEURISTICPARSER_H
+
+namespace LTL {
+    std::unique_ptr<LTL::Heuristic> ParseHeuristic(const PetriEngine::PetriNet *net,
+                                                   const Structures::BuchiAutomaton &aut,
+                                                   const PetriEngine::PQL::Condition_ptr &cond,
+                                                   const char* heurString);
+}
+
+#endif //VERIFYPN_HEURISTICPARSER_H

=== modified file 'include/LTL/SuccessorGeneration/Heuristics.h'
--- include/LTL/SuccessorGeneration/Heuristics.h	2021-03-24 07:31:53 +0000
+++ include/LTL/SuccessorGeneration/Heuristics.h	2021-08-05 10:56:53 +0000
@@ -21,5 +21,9 @@
 #include "DistanceHeuristic.h"
 #include "RandomHeuristic.h"
 #include "AutomatonHeuristic.h"
+#include "ComposedHeuristic.h"
+#include "WeightedComposedHeuristic.h"
+#include "FireCountHeuristic.h"
+#include "LogFireCountHeuristic.h"
 
 #endif //VERIFYPN_HEURISTICS_H

=== added file 'include/LTL/SuccessorGeneration/LogFireCountHeuristic.h'
--- include/LTL/SuccessorGeneration/LogFireCountHeuristic.h	1970-01-01 00:00:00 +0000
+++ include/LTL/SuccessorGeneration/LogFireCountHeuristic.h	2021-08-05 10:56:53 +0000
@@ -0,0 +1,69 @@
+/* Copyright (C) 2021  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ * 
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ * 
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ * 
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_LOGFIRECOUNTHEURISTIC_H
+#define VERIFYPN_LOGFIRECOUNTHEURISTIC_H
+
+#include "Heuristic.h"
+#include "FireCountHeuristic.h"
+
+namespace LTL {
+    constexpr int _approx_log(uint32_t i)
+    {
+        // log2 of an integer is the highest set bit
+        // loop is not optimal but portable and likely reasonably performant for small-ish ints
+        // (which most of the time is the expected input)
+        int r = 0;
+        while (i >>= 1) {
+            ++r;
+        }
+        return r;
+    }
+
+    /**
+     * Piece-wise zero/logarithmic fire count heuristic, switching to log at threshold defined by parameter
+     * (default 200). Intent is to avoid firing the same transition excessively in models with massive token counts.
+     */
+    class LogFireCountHeuristic : public FireCountHeuristic {
+    public:
+        explicit LogFireCountHeuristic(const PetriEngine::PetriNet *net, uint32_t threshold = 200)
+                : FireCountHeuristic(net), _threshold(threshold) {}
+
+        uint32_t eval(const Structures::ProductState &state, uint32_t tid) override
+        {
+            if (_fireCount[tid] < _threshold) return 0;
+            return _approx_log(_fireCount[tid] - _threshold);
+        }
+
+        std::ostream &output(std::ostream &os) {
+            return os << "LOGFIRECOUNT_HEUR(" << _threshold << ")";
+        }
+
+    private:
+        uint32_t _threshold;
+
+        // compile-time sanity checks, feel free to remove if problematic
+        static_assert(_approx_log(1) == 0);
+        static_assert(_approx_log(2) == 1);
+        static_assert(_approx_log(3) == 1);
+        static_assert(_approx_log(9) == 3);
+        static_assert(_approx_log(15) == 3);
+        static_assert(_approx_log(16) == 4);
+    };
+}
+
+#endif //VERIFYPN_LOGFIRECOUNTHEURISTIC_H

=== modified file 'include/LTL/SuccessorGeneration/ProductSuccessorGenerator.h'
--- include/LTL/SuccessorGeneration/ProductSuccessorGenerator.h	2021-04-02 09:54:38 +0000
+++ include/LTL/SuccessorGeneration/ProductSuccessorGenerator.h	2021-08-05 10:56:53 +0000
@@ -24,9 +24,11 @@
 #include "LTL/Structures/ProductState.h"
 #include "BuchiSuccessorGenerator.h"
 #include "LTL/LTLToBuchi.h"
+#include "LTL/Stubborn/VisibleLTLStubbornSet.h"
 #include "LTL/Simplification/SpotToPQL.h"
 #include "LTL/Structures/GuardInfo.h"
 #include "LTL/SuccessorGeneration/SpoolingSuccessorGenerator.h"
+#include "LTL/SuccessorGeneration/ResumingSuccessorGenerator.h"
 
 #include <spot/twa/formula2bdd.hh>
 #include <spot/tl/formula.hh>
@@ -39,8 +41,8 @@
 
         ProductSuccessorGenerator(const PetriEngine::PetriNet *net,
                                   const Structures::BuchiAutomaton &buchi,
-                                  SuccessorGen &&successorGen)
-                : _successor_generator(std::move(successorGen)), _net(net),
+                                  SuccessorGen *successorGen)
+                : _successor_generator(successorGen), _net(net),
                   buchi(buchi), aut(buchi)
         {
 
@@ -48,22 +50,14 @@
 
         [[nodiscard]] size_t initial_buchi_state() const { return buchi.initial_state_number(); };
 
-        auto prepare(const LTL::Structures::ProductState *state)
-        {
-            buchi.prepare(state->getBuchiState());
-            buchi_parent = state->getBuchiState();
-            fresh_marking = true;
-            return _successor_generator.prepare(state);
-        }
-
         bool next(LTL::Structures::ProductState &state)
         {
             if (fresh_marking) {
                 fresh_marking = false;
-                if (!_successor_generator.next(state)) {
+                if (!_successor_generator->next(state)) {
                     // This is a fresh marking, so if there is no more successors for the state the state is deadlocked.
                     // The semantics for deadlock is to just loop the marking so return true without changing the value of state.
-                    std::copy(_successor_generator.getParent(), _successor_generator.getParent() + state.buchi_state_idx + 1,
+                    std::copy(_successor_generator->getParent(), _successor_generator->getParent() + state.buchi_state_idx + 1,
                               state.marking());
                 }
             }
@@ -73,7 +67,7 @@
                 // No valid transition in Büchi automaton for current marking;
                 // Try next marking(s) and see if we find a successor.
             else {
-                while (_successor_generator.next(state)) {
+                while (_successor_generator->next(state)) {
                     // reset buchi successors
                     buchi.prepare(buchi_parent);
                     if (next_buchi_succ(state)) {
@@ -118,9 +112,9 @@
          * @param state the source state to generate successors from
          * @param sucinfo the point in the iteration to start from, as returned by `next`.
          */
-        void prepare(const LTL::Structures::ProductState *state, typename SuccessorGen::sucinfo &sucinfo)
+        virtual void prepare(const LTL::Structures::ProductState *state, typename SuccessorGen::sucinfo &sucinfo)
         {
-            _successor_generator.prepare(state, sucinfo);
+            _successor_generator->prepare(state, sucinfo);
             fresh_marking = sucinfo.fresh();
             buchi.prepare(state->getBuchiState());
             buchi_parent = state->getBuchiState();
@@ -149,26 +143,26 @@
         {
             if (fresh_marking) {
                 fresh_marking = false;
-                if (!_successor_generator.next(state, sucinfo)) {
+                if (!_successor_generator->next(state, sucinfo)) {
                     // This is a fresh marking, so if there are no more successors for the state the state is deadlocked.
                     // The semantics for deadlock is to just loop the marking so return true without changing the value of state.
-                    std::copy(_successor_generator.getParent(), _successor_generator.getParent() + state.buchi_state_idx + 1,
+                    std::copy(_successor_generator->getParent(), _successor_generator->getParent() + state.buchi_state_idx + 1,
                               state.marking());
                 }
             }
             if (next_buchi_succ(state)) {
-                //_successor_generator.getSuccInfo(sucinfo);
+                //_successor_generator->getSuccInfo(sucinfo);
                 sucinfo.buchi_state = state.getBuchiState();
                 return true;
             }
                 // No valid transition in Büchi automaton for current marking;
                 // Try next marking(s) and see if we find a successor.
             else {
-                while (_successor_generator.next(state, sucinfo)) {
+                while (_successor_generator->next(state, sucinfo)) {
                     // reset buchi successors
                     buchi.prepare(buchi_parent);
                     if (next_buchi_succ(state)) {
-                        //_successor_generator.getSuccInfo(sucinfo);
+                        //_successor_generator->getSuccInfo(sucinfo);
                         sucinfo.buchi_state = state.getBuchiState();
                         return true;
                     }
@@ -183,91 +177,84 @@
             return buchi.is_weak();
         }
 
-        size_t last_transition() const { return _successor_generator.last_transition(); }
+        size_t last_transition() const { return _successor_generator->last_transition(); }
 
-        size_t fired() const { return _successor_generator.fired(); }
+        size_t fired() const { return _successor_generator->fired(); }
 
         //template<typename T = std::enable_if_t<std::is_same_v<SuccessorGen, PetriEngine::ReducingSuccessorGenerator>, void>>
-        void generateAll(typename SuccessorGen::sucinfo &sucinfo)
+        void generateAll(LTL::Structures::ProductState *parent, typename SuccessorGen::sucinfo &sucinfo)
         {
             if constexpr (std::is_same_v<SuccessorGen, LTL::SpoolingSuccessorGenerator>) {
-                _successor_generator.generate_all(sucinfo);
+                _successor_generator->generate_all(parent, sucinfo);
             }
         }
 
         size_t numEnabled()
         {
             if constexpr (std::is_same_v<SuccessorGen, LTL::SpoolingSuccessorGenerator>) {
-                return _successor_generator.nenabled();
+                return _successor_generator->nenabled();
             }
             return -1;
         }
 
-        // FIXME const if possible?
-        bool *enabled() const
+        const bool *enabled() const
         {
             if constexpr (std::is_same_v<SuccessorGen, LTL::SpoolingSuccessorGenerator>) {
-                return _successor_generator.enabled();
+                return _successor_generator->enabled();
             }
             return nullptr;
         };
 
-        // FIXME const if possible?
-        bool *stubborn() const
+        const bool *stubborn() const
         {
             if constexpr (std::is_same_v<SuccessorGen, LTL::SpoolingSuccessorGenerator>) {
-                return _successor_generator.stubborn();
+                return _successor_generator->stubborn();
             }
             return nullptr;
         };
 
         size_t buchiStates() { return buchi.buchiStates(); }
 
+        void push() {
+            if constexpr (std::is_same_v<SuccessorGen, LTL::SpoolingSuccessorGenerator>) {
+                _successor_generator->push();
+            }
+        }
+
+        void pop(const typename SuccessorGen::sucinfo &sucinfo) {
+            if constexpr (std::is_same_v<SuccessorGen, LTL::SpoolingSuccessorGenerator>) {
+                _successor_generator->pop(sucinfo);
+            }
+        }
+
         bool has_invariant_self_loop(const LTL::Structures::ProductState &state) {
             return buchi.has_invariant_self_loop(state.getBuchiState());
         }
-    private:
-        SuccessorGen _successor_generator;
+
+        virtual ~ProductSuccessorGenerator() = default;
+
+    protected:
+        SuccessorGen *_successor_generator;
         const PetriEngine::PetriNet *_net;
-
         BuchiSuccessorGenerator buchi;
+
         const LTL::Structures::BuchiAutomaton &aut;
         bdd cond;
         size_t buchi_parent;
         bool fresh_marking = true;
-
         std::vector<GuardInfo> stateToGuards;
-
         /**
          * Evaluate binary decision diagram (BDD) representation of transition guard in given state.
          */
         bool guard_valid(const PetriEngine::Structures::State &state, bdd bdd)
         {
             PetriEngine::PQL::EvaluationContext ctx{state.marking(), _net};
-            // IDs 0 and 1 are false and true atoms, respectively
-            // More details in buddy manual ( http://buddy.sourceforge.net/manual/main.html )
-            while (bdd.id() > 1) {
-                // find variable to test, and test it
-                size_t var = bdd_var(bdd);
-                using PetriEngine::PQL::Condition;
-                Condition::Result res = buchi.getExpression(var)->evaluate(ctx);
-                switch (res) {
-                    case Condition::RUNKNOWN:
-                        std::cerr << "Unexpected unknown answer from evaluating query!\n";
-                        assert(false);
-                        exit(1);
-                        break;
-                    case Condition::RFALSE:
-                        bdd = bdd_low(bdd);
-                        break;
-                    case Condition::RTRUE:
-                        bdd = bdd_high(bdd);
-                        break;
-                }
-            }
-            return bdd == bddtrue;
+            return buchi.aut.guard_valid(ctx, bdd);
         }
 
+
+    private:
+
         bool next_buchi_succ(LTL::Structures::ProductState &state)
         {
             size_t tmp;

=== modified file 'include/LTL/SuccessorGeneration/RandomHeuristic.h'
--- include/LTL/SuccessorGeneration/RandomHeuristic.h	2021-04-02 09:54:38 +0000
+++ include/LTL/SuccessorGeneration/RandomHeuristic.h	2021-08-05 10:56:53 +0000
@@ -31,7 +31,9 @@
             return g();
         }
 
-
+        std::ostream &output(std::ostream &os) {
+            return os << "RANDOM_HEUR";
+        }
     private:
         std::random_device rd;
         std::mt19937 g;

=== added file 'include/LTL/SuccessorGeneration/ReachStubProductSuccessorGenerator.h'
--- include/LTL/SuccessorGeneration/ReachStubProductSuccessorGenerator.h	1970-01-01 00:00:00 +0000
+++ include/LTL/SuccessorGeneration/ReachStubProductSuccessorGenerator.h	2021-08-05 10:56:53 +0000
@@ -0,0 +1,106 @@
+/* Copyright (C) 2021  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ * 
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ * 
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ * 
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_REACHSTUBPRODUCTSUCCESSORGENERATOR_H
+#define VERIFYPN_REACHSTUBPRODUCTSUCCESSORGENERATOR_H
+
+#include "LTL/SuccessorGeneration/ProductSuccessorGenerator.h"
+#include "LTL/SuccessorGeneration/Spoolers.h"
+
+
+namespace LTL {
+    template<typename S, typename Spooler>
+    class ReachStubProductSuccessorGenerator : public ProductSuccessorGenerator<S> {
+    public:
+        ReachStubProductSuccessorGenerator(const PetriEngine::PetriNet *net, const Structures::BuchiAutomaton &buchi,
+                                           S *successorGen, std::unique_ptr<Spooler> &&fallbackSpooler)
+                : ProductSuccessorGenerator<S>(net, buchi, successorGen), _fallback_spooler(std::move(fallbackSpooler))
+        {
+            //_fallback_spooler = std::make_unique<Spooler>(fallbackSpooler);
+/*            if constexpr (std::is_same_v<Spooler, EnabledSpooler>) {
+                _fallback_spooler = std::make_unique<Spooler>(net, static_cast<PetriEngine::SuccessorGenerator&>(this->_successor_generator));
+            }
+            else {
+                _fallback_spooler = std::make_unique<Spooler>(net);
+            }*/
+            // Create the set of büchi states from which we can use reachability stubborn sets.
+            calc_safe_reach_states(buchi);
+            _reach = std::make_unique<SafeAutStubbornSet>(*net, _progressing_formulae);
+
+        }
+
+        void calc_safe_reach_states(const Structures::BuchiAutomaton &buchi) {
+            assert(_reach_states.empty());
+            std::vector<AtomicProposition> aps(buchi.ap_info.size());
+            std::transform(std::begin(buchi.ap_info), std::end(buchi.ap_info), std::begin(aps),
+                           [](const std::pair<int, AtomicProposition> &pair) { return pair.second; });
+            for (unsigned state = 0; state < buchi._buchi->num_states(); ++state) {
+                if (buchi._buchi->state_is_accepting(state)) continue;
+
+                bdd retarding = bddfalse;
+                bdd progressing = bddfalse;
+                for (auto &e : buchi._buchi->out(state)) {
+                    if (e.dst == state) {
+                        retarding = e.cond;
+                    }
+                    else {
+                        progressing |= e.cond;
+                    }
+                }
+                if ((retarding | progressing) == bddtrue) {
+                    _reach_states.insert(std::make_pair(state, BuchiEdge{progressing, toPQL(spot::bdd_to_formula(progressing, buchi.dict), aps)}));
+                }
+            }
+        }
+
+        void prepare(const LTL::Structures::ProductState *state, typename S::sucinfo &sucinfo) override
+        {
+            if (auto suc = _reach_states.find(state->getBuchiState()); suc != std::end(_reach_states) && !this->guard_valid(*state, suc->second.bddCond)) {
+                (dynamic_cast<PetriEngine::StubbornSet*>(_reach.get()))->setQuery(suc->second.cond.get());
+                set_spooler(_reach.get());
+            }
+            else {
+                set_spooler(_fallback_spooler.get());
+            }
+            ProductSuccessorGenerator<S>::prepare(state, sucinfo);
+        }
+
+    private:
+        void set_spooler(SuccessorSpooler *spooler)
+        {
+            if constexpr (std::is_same_v<S, LTL::SpoolingSuccessorGenerator>)
+                this->_successor_generator->setSpooler(spooler);
+            else {
+                assert(false);
+                std::cerr << "Fatal error\n"; exit(1);
+            }
+        }
+
+        struct BuchiEdge{
+            bdd bddCond;
+            PetriEngine::PQL::Condition_ptr cond;
+        };
+
+        std::unique_ptr<Spooler> _fallback_spooler;
+        std::unique_ptr<LTL::SuccessorSpooler> _reach;
+        std::unordered_map<size_t, BuchiEdge> _reach_states;
+        std::vector<PetriEngine::PQL::Condition_ptr> _progressing_formulae;
+
+    };
+}
+
+#endif //VERIFYPN_REACHSTUBPRODUCTSUCCESSORGENERATOR_H

=== modified file 'include/LTL/SuccessorGeneration/ResumingSuccessorGenerator.h'
--- include/LTL/SuccessorGeneration/ResumingSuccessorGenerator.h	2021-03-19 11:48:52 +0000
+++ include/LTL/SuccessorGeneration/ResumingSuccessorGenerator.h	2021-08-05 10:56:53 +0000
@@ -81,14 +81,14 @@
     class ResumingSuccessorGenerator : public PetriEngine::SuccessorGenerator {
     public:
 
-        ResumingSuccessorGenerator(const PetriEngine::PetriNet &net);
-
-        ResumingSuccessorGenerator(const PetriEngine::PetriNet &net, const std::shared_ptr<PetriEngine::StubbornSet> &);
-
-        ResumingSuccessorGenerator(const PetriEngine::PetriNet &net,
+        ResumingSuccessorGenerator(const PetriEngine::PetriNet *net);
+
+        ResumingSuccessorGenerator(const PetriEngine::PetriNet *net, const std::shared_ptr<PetriEngine::StubbornSet> &);
+
+        ResumingSuccessorGenerator(const PetriEngine::PetriNet *net,
                                    std::vector<std::shared_ptr<PetriEngine::PQL::Condition> > &queries);
 
-        ResumingSuccessorGenerator(const PetriEngine::PetriNet &net,
+        ResumingSuccessorGenerator(const PetriEngine::PetriNet *net,
                                    const std::shared_ptr<PetriEngine::PQL::Condition> &query);
 
         ~ResumingSuccessorGenerator() override = default;

=== modified file 'include/LTL/SuccessorGeneration/Spoolers.h'
--- include/LTL/SuccessorGeneration/Spoolers.h	2021-03-31 11:31:54 +0000
+++ include/LTL/SuccessorGeneration/Spoolers.h	2021-08-05 10:56:53 +0000
@@ -19,5 +19,8 @@
 #define VERIFYPN_SPOOLERS_H
 
 #include "EnabledSpooler.h"
+#include "LTL/Stubborn/VisibleLTLStubbornSet.h"
+#include "LTL/Stubborn/AutomatonStubbornSet.h"
+#include "LTL/Stubborn/SafeAutStubbornSet.h"
 
 #endif //VERIFYPN_SPOOLERS_H

=== modified file 'include/LTL/SuccessorGeneration/SpoolingSuccessorGenerator.h'
--- include/LTL/SuccessorGeneration/SpoolingSuccessorGenerator.h	2021-04-02 09:54:38 +0000
+++ include/LTL/SuccessorGeneration/SpoolingSuccessorGenerator.h	2021-08-05 10:56:53 +0000
@@ -18,8 +18,10 @@
 #ifndef VERIFYPN_SPOOLINGSUCCESSORGENERATOR_H
 #define VERIFYPN_SPOOLINGSUCCESSORGENERATOR_H
 
+#include "LTL/Stubborn/AutomatonStubbornSet.h"
 #include "LTL/Structures/ProductState.h"
 #include "PetriEngine/Structures/SuccessorQueue.h"
+#include "LTL/SuccessorGeneration/DistanceHeuristic.h"
 #include "LTL/SuccessorGeneration/SuccessorSpooler.h"
 #include "LTL/SuccessorGeneration/Heuristics.h"
 
@@ -50,14 +52,14 @@
             static constexpr auto NoLastState = std::numeric_limits<size_t>::max();
         };
 
-        void setSpooler(std::unique_ptr<SuccessorSpooler> &&spooler)
+        void setSpooler(SuccessorSpooler *const spooler)
         {
-            _spooler.swap(spooler);
+            _spooler = spooler;
         }
 
-        void setHeuristic(std::unique_ptr<Heuristic> &&heuristic)
+        void setHeuristic(Heuristic *const heuristic)
         {
-            _heuristic.swap(heuristic);
+            _heuristic = heuristic;
         }
 
         [[nodiscard]] static sucinfo initial_suc_info()
@@ -96,6 +98,7 @@
 
                 } else {
                     // list of (transition, weight)
+                    _heuristic->prepare(*state);
                     std::vector<std::pair<uint32_t, uint32_t>> weighted_tids;
                     while ((tid = _spooler->next()) != SuccessorSpooler::NoTransition) {
                         assert(tid <= _net.numberOfTransitions());
@@ -106,20 +109,24 @@
                     // sort by least distance first.
                     std::sort(std::begin(weighted_tids), std::end(weighted_tids),
                               [](auto &l, auto &r) { return l.second < r.second; });
-                    sucinfo.successors = SuccessorQueue(weighted_tids.data(), weighted_tids.size(),
-                                                        [](auto &p) { return p.first; });
+                    sucinfo.successors = SuccessorQueue(weighted_tids, [](auto &p) { return p.first; });
                 }
             }
         }
-
         bool next(Structures::ProductState &state, sucinfo &sucinfo)
         {
             assert(sucinfo.successors != nullptr);
             if (sucinfo.successors.empty()) {
+#ifndef NDEBUG
+                //std::cerr << "Not Firing: " << (sucinfo.successors.has_consumed() ? "deadlock" : "done") << std::endl;
+#endif
                 _last = std::numeric_limits<uint32_t>::max();
                 return false;
             }
             _last = sucinfo.successors.front();
+#ifndef NDEBUG
+            //std::cerr << "Firing " << _net.transitionNames()[_last] << std::endl;
+#endif
             sucinfo.successors.pop();
             SuccessorGenerator::_fire(state, _last);
             return true;
@@ -127,18 +134,82 @@
 
         [[nodiscard]] uint32_t fired() const { return _last; }
 
-        void _fire(Structures::ProductState &parent, Structures::ProductState &write, uint32_t tid)
+        void generate_all(LTL::Structures::ProductState *parent, sucinfo &sucinfo)
         {
-            PetriEngine::SuccessorGenerator::_fire(write, tid);
-            write.setBuchiState(parent.getBuchiState());
-        }
-
+            assert(_spooler != nullptr);
+            assert(sucinfo.successors != nullptr);
+            if (!_spooler->generateAll(parent)) return;
+            assert(dynamic_cast<VisibleLTLStubbornSet*>(_spooler) != nullptr);
+
+            uint32_t tid;
+            if (!_heuristic) {
+                uint32_t nsuc = 0;
+                // generate list of transitions that generate a successor.
+                auto [first, last] = sucinfo.successors.all_successors();
+                for (; first < last; ++first) {
+                    tid = *first;
+                    // avoiding duplicates
+                    if (!static_cast<VisibleLTLStubbornSet*>(_spooler)->stubborn()[tid]) {
+                        _transbuf[nsuc++] = tid;
+                    }
+                }
+                while ((tid = _spooler->next()) != SuccessorSpooler::NoTransition) {
+                    assert(tid <= _net.numberOfTransitions());
+                    _transbuf[nsuc++] = tid;
+                    assert(nsuc <= _net.numberOfTransitions());
+                }
+                sucinfo.successors.extend_to(_transbuf.get(), nsuc);
+
+            } else {
+                auto evaluate_heuristic = [&] (uint32_t tid) {
+                    SuccessorGenerator::_fire(_statebuf, tid);
+                    _statebuf.setBuchiState(sucinfo.buchi_state);
+                    return _heuristic->eval(_statebuf, tid);
+                };
+
+                // list of (transition, weight)
+                std::vector<std::pair<uint32_t, uint32_t>> weighted_tids;
+                // grab previous stubborn transitions
+                auto [first, last] = sucinfo.successors.all_successors();
+                for (; first < last; ++first) {
+                    tid = *first;
+                    if (!static_cast<VisibleLTLStubbornSet*>(_spooler)->stubborn()[tid]) {
+                        weighted_tids.emplace_back(tid, evaluate_heuristic(tid));
+                    }
+                }
+
+                // add new stubborn transitions
+                while ((tid = _spooler->next()) != SuccessorSpooler::NoTransition) {
+                    assert(tid <= _net.numberOfTransitions());
+                    weighted_tids.emplace_back(tid, evaluate_heuristic(tid));
+                }
+                // sort by least distance first.
+                std::sort(std::begin(weighted_tids), std::end(weighted_tids),
+                          [](auto &l, auto &r) { return l.second < r.second; });
+                assert(weighted_tids.size() <= _net.numberOfTransitions());
+                std::transform(std::begin(weighted_tids), std::end(weighted_tids),
+                               _transbuf.get(),
+                               [](auto &p) { return p.first; });
+                sucinfo.successors.extend_to(_transbuf.get(), weighted_tids.size());
+            }
+        }
+
+        void push() {
+            // No transitions have been fired yet. We must be in the initial marking.
+            if (!_heuristic || fired() == std::numeric_limits<uint32_t>::max()) return;
+            _heuristic->push(fired());
+        }
+
+        void pop(const sucinfo &sc) {
+            if (_heuristic && sc.successors.has_consumed())
+                _heuristic->pop(sc.successors.last_pop());
+        }
 
     private:
-        std::unique_ptr<SuccessorSpooler> _spooler = nullptr;
-        std::unique_ptr<Heuristic> _heuristic = nullptr;
+        SuccessorSpooler *_spooler = nullptr;
+        Heuristic *_heuristic = nullptr;
 
-        uint32_t _last;
+        uint32_t _last = std::numeric_limits<uint32_t>::max();
         std::unique_ptr<uint32_t[]> _transbuf;   /* buffer for enabled transitions, size is ntransitions. */
         LTL::Structures::ProductState _statebuf;
     };

=== modified file 'include/LTL/SuccessorGeneration/SuccessorSpooler.h'
--- include/LTL/SuccessorGeneration/SuccessorSpooler.h	2021-03-19 11:48:52 +0000
+++ include/LTL/SuccessorGeneration/SuccessorSpooler.h	2021-08-05 10:56:53 +0000
@@ -34,9 +34,9 @@
 
         }
 
-        virtual void generateAll()
+        virtual bool generateAll(const LTL::Structures::ProductState *parent)
         {
-
+            return false;
         }
         static constexpr uint32_t NoTransition = std::numeric_limits<uint32_t>::max();
     };

=== added file 'include/LTL/SuccessorGeneration/WeightedComposedHeuristic.h'
--- include/LTL/SuccessorGeneration/WeightedComposedHeuristic.h	1970-01-01 00:00:00 +0000
+++ include/LTL/SuccessorGeneration/WeightedComposedHeuristic.h	2021-08-05 10:56:53 +0000
@@ -0,0 +1,55 @@
+/* Copyright (C) 2021  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ * 
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ * 
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ * 
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef VERIFYPN_WEIGHTEDCOMPOSEDHEURISTIC_H
+#define VERIFYPN_WEIGHTEDCOMPOSEDHEURISTIC_H
+
+namespace LTL {
+
+    class WeightedComposedHeuristic: public ComposedHeuristic {
+    public:
+
+        WeightedComposedHeuristic(std::unique_ptr<Heuristic> primary, std::unique_ptr<Heuristic> secondary, uint32_t primary_weight, uint32_t secondary_weight)
+                : ComposedHeuristic(std::move(primary), std::move(secondary)), _primary_weight(primary_weight), _secondary_weight(secondary_weight) {}
+
+        uint32_t eval(const Structures::ProductState &state, uint32_t tid) override {
+            if (_primary_has_heuristic && !_secondary_has_heuristic) {
+                return _primary->eval(state, tid);
+            } else if (!_primary_has_heuristic && _secondary_has_heuristic) {
+                return _secondary->eval(state, tid);
+            } else if (_primary_has_heuristic && _secondary_has_heuristic) {
+                return _primary->eval(state, tid) * _primary_weight + _secondary->eval(state, tid) * _secondary_weight;
+            } else {
+                return 0;
+            }
+        }
+
+
+        std::ostream &output(std::ostream &os) {
+            os << "WEIGHTED(" << _primary_weight << "*";
+            _primary->output(os) << ",";
+            os << _secondary_weight << "*";
+            _secondary->output(os) << ")";
+            return os;
+        }
+    private:
+        uint32_t _primary_weight, _secondary_weight;
+    };
+
+}
+
+#endif //VERIFYPN_WEIGHTEDCOMPOSEDHEURISTIC_H

=== modified file 'include/PetriEngine/PQL/Visitor.h'
--- include/PetriEngine/PQL/Visitor.h	2021-03-31 11:31:54 +0000
+++ include/PetriEngine/PQL/Visitor.h	2021-08-05 10:56:53 +0000
@@ -26,29 +26,20 @@
                 _accept(element);
             }
 
+            //virtual ~Visitor() = default;
+
         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 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;
+            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 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

=== modified file 'include/PetriEngine/Reachability/ReachabilitySearch.h'
--- include/PetriEngine/Reachability/ReachabilitySearch.h	2021-04-07 08:50:10 +0000
+++ include/PetriEngine/Reachability/ReachabilitySearch.h	2021-08-05 10:56:53 +0000
@@ -104,7 +104,9 @@
         }
         template <>
         inline ReducingSuccessorGenerator _makeSucGen(PetriNet &net, std::vector<PQL::Condition_ptr> &queries) {
-            return ReducingSuccessorGenerator{net, std::make_shared<ReachabilityStubbornSet>(net, queries)};
+            auto stubset = std::make_shared<ReachabilityStubbornSet>(net, queries);
+            stubset->setInterestingVisitor<InterestingTransitionVisitor>();
+            return ReducingSuccessorGenerator{net, stubset};
         }
 
         template<typename Q, typename W, typename G>

=== modified file 'include/PetriEngine/Reducer.h'
--- include/PetriEngine/Reducer.h	2021-07-05 19:55:24 +0000
+++ include/PetriEngine/Reducer.h	2021-08-05 10:56:53 +0000
@@ -14,6 +14,7 @@
 #include "NetStructures.h"
 
 #include <vector>
+#include <optional>
 
 namespace PetriEngine {
 

=== modified file 'include/PetriEngine/Structures/SuccessorQueue.h'
--- include/PetriEngine/Structures/SuccessorQueue.h	2021-03-19 13:48:21 +0000
+++ include/PetriEngine/Structures/SuccessorQueue.h	2021-08-05 10:56:53 +0000
@@ -39,11 +39,11 @@
 
     // construct from array of different type, using fn as transformation function.
     template <typename U, typename Fn>
-    SuccessorQueue(U *src, uint32_t nelem, Fn&& fn)
-            : _front(0), _size(nelem)
+    SuccessorQueue(std::vector<U> &src, Fn&& fn)
+            : _front(0), _size(src.size())
     {
-        _data = std::make_unique<T[]>(nelem);
-        std::transform(src, src + nelem, _data.get(), fn);
+        _data = std::make_unique<T[]>(src.size());
+        std::transform(std::begin(src), std::end(src), _data.get(), fn);
     }
 
     SuccessorQueue() noexcept :_front(0), _size(0), _data(nullptr) {}
@@ -60,7 +60,7 @@
         ++_front;
     }
 
-    [[nodiscard]] T size() const
+    [[nodiscard]] size_t size() const
     {
         return _size - _front;
     }
@@ -74,6 +74,11 @@
 
     [[nodiscard]] bool has_consumed() const { return _front > 0; }
 
+    T last_pop() const {
+        assert(has_consumed());
+        return _data[_front - 1];
+    }
+
     bool operator==(std::nullptr_t) { return _data == nullptr; }
     bool operator!=(std::nullptr_t) { return _data != nullptr; }
 
@@ -84,6 +89,7 @@
      */
     void extend_to(T *src, uint32_t nelem)
     {
+        assert(nelem >= _size); // Cannot extend to fewer elements.
         auto newdata = std::make_unique<T[]>(nelem);
         if (_front != 0) {
             //Add previously fired transitions to start of array.
@@ -92,7 +98,6 @@
         uint32_t sz = _front;
         // copy over extended successor list, excluding previously popped elements.
         for (uint32_t i = 0; i < nelem; ++i) {
-            // FIXME potential optimization target if poor performance is found.
             auto begin = _data.get(), end = _data.get() + _front;
             auto it = std::find(begin, end, src[i]);
 
@@ -107,6 +112,18 @@
         _data.swap(newdata);
     }
 
+    void append(T *src, uint32_t nelem) {
+        auto newdata = std::make_unique<T[]>(nelem + _size);
+        memcpy(newdata.get(), _data.get(), sizeof(T) * _size);
+        memcpy(newdata.get() + _size, src, sizeof(T) * nelem);
+        _size = nelem + _size;
+        _data.swap(newdata);
+    }
+
+    std::pair<T*, T*> all_successors() {
+        return std::make_pair(_data.get(), &_data[_size]);
+    }
+
 private:
     uint32_t _front; /* index of first element */
     uint32_t _size;  /* size of data array */

=== modified file 'include/PetriEngine/Stubborn/InterestingTransitionVisitor.h'
--- include/PetriEngine/Stubborn/InterestingTransitionVisitor.h	2021-04-06 08:36:53 +0000
+++ include/PetriEngine/Stubborn/InterestingTransitionVisitor.h	2021-08-05 10:56:53 +0000
@@ -33,12 +33,13 @@
 
         void negate() { negated = !negated; }
 
-    private:
+        bool get_negated() const { return negated; }
+
+    protected:
         PetriEngine::StubbornSet &_stubborn;
 
         bool closure;
 
-    protected:
         void _accept(const PQL::NotCondition *element) override;
 
         void _accept(const PQL::AndCondition *element) override;
@@ -222,6 +223,13 @@
         void negate_if_satisfied(const Condition *element);
     };
 
+    class AutomatonInterestingTransitionVisitor : public InterestingTransitionVisitor {
+    public:
+        explicit AutomatonInterestingTransitionVisitor(StubbornSet &stubbornSet, bool closure) : InterestingTransitionVisitor(stubbornSet, closure) {}
+
+    protected:
+        void _accept(const PQL::CompareConjunction *element) override;
+    };
 }
 
 

=== modified file 'include/PetriEngine/Stubborn/ReachabilityStubbornSet.h'
--- include/PetriEngine/Stubborn/ReachabilityStubbornSet.h	2021-03-23 14:10:04 +0000
+++ include/PetriEngine/Stubborn/ReachabilityStubbornSet.h	2021-08-05 10:56:53 +0000
@@ -20,17 +20,33 @@
 
 
 #include "PetriEngine/Stubborn/StubbornSet.h"
+#include "InterestingTransitionVisitor.h"
 
 namespace PetriEngine {
     class ReachabilityStubbornSet : public StubbornSet {
     public:
-        ReachabilityStubbornSet(const PetriNet &net, const std::vector<PQL::Condition_ptr> &queries)
-                : StubbornSet(net, queries) {}
+        ReachabilityStubbornSet(const PetriNet &net, const std::vector<PQL::Condition_ptr> &queries, bool closure = true)
+                : StubbornSet(net, queries), _closure(closure) {
+            setInterestingVisitor<InterestingTransitionVisitor>();
+        }
 
-        ReachabilityStubbornSet(const PetriNet &net)
-                : StubbornSet(net) {}
+        ReachabilityStubbornSet(const PetriNet &net, bool closure = true)
+                : StubbornSet(net) , _closure(closure) {
+            setInterestingVisitor<InterestingTransitionVisitor>();
+        }
 
         bool prepare(const Structures::State *state) override;
+
+        template <typename TVisitor>
+        void setInterestingVisitor()
+        {
+            _interesting = std::make_unique<TVisitor>(*this, _closure);
+        }
+
+    private:
+        std::unique_ptr<InterestingTransitionVisitor> _interesting;
+
+        bool _closure;
     };
 }
 

=== modified file 'include/PetriEngine/Stubborn/StubbornSet.h'
--- include/PetriEngine/Stubborn/StubbornSet.h	2021-03-23 14:10:04 +0000
+++ include/PetriEngine/Stubborn/StubbornSet.h	2021-08-05 10:56:53 +0000
@@ -92,13 +92,24 @@
             _queries = {ptr};
         }
 
+        void setQueries(std::vector<PQL::Condition*> conds) {
+            _queries = conds;
+        }
+
         [[nodiscard]] size_t nenabled() const { return _nenabled; }
 
         [[nodiscard]] bool *enabled() const { return _enabled.get(); };
         [[nodiscard]] bool *stubborn() const { return _stubborn.get(); };
 
-    protected:
         const PetriEngine::PetriNet &_net;
+
+        // Bit flags for _places_seen array.
+        static constexpr auto PresetSeen = 1;
+        static constexpr auto PostsetSeen = 2;
+        static constexpr auto InhibPostsetSeen = 4;
+        static constexpr auto PresetBad = 8;
+        static constexpr auto PostsetBad = 16;
+    protected:
         const Structures::State *_parent;
 
         struct place_t {
@@ -128,18 +139,73 @@
 
         virtual void addToStub(uint32_t t);
 
-        void closure();
+        template <typename T = std::nullptr_t>
+        void closure(T callback = nullptr) {
+            while (!_unprocessed.empty()) {
+                if constexpr (!std::is_null_pointer_v<T>) {
+                    if (!callback()) return;
+                }
+                uint32_t tr = _unprocessed.front();
+                _unprocessed.pop_front();
+                const TransPtr &ptr = transitions()[tr];
+                uint32_t finv = ptr.inputs;
+                uint32_t linv = ptr.outputs;
+                if (_enabled[tr]) {
+                    for (; finv < linv; finv++) {
+                        if (invariants()[finv].direction < 0) {
+                            auto place = invariants()[finv].place;
+                            for (uint32_t t = _places.get()[place].post; t < _places.get()[place + 1].pre; t++)
+                                addToStub(_transitions.get()[t].index);
+                        }
+                    }
+                    if (_netContainsInhibitorArcs) {
+                        uint32_t next_finv = transitions()[tr + 1].inputs;
+                        for (; linv < next_finv; linv++) {
+                            if (invariants()[linv].direction > 0)
+                                inhibitorPostsetOf(invariants()[linv].place);
+                        }
+                    }
+                } else {
+                    bool ok = false;
+                    bool inhib = false;
+                    uint32_t cand = std::numeric_limits<uint32_t>::max();
+
+                    // Lets try to see if we havent already added sufficient pre/post
+                    // for this transition.
+                    for (; finv < linv; ++finv) {
+                        const Invariant &inv = invariants()[finv];
+                        if ((*_parent).marking()[inv.place] < inv.tokens && !inv.inhibitor) {
+                            inhib = false;
+                            ok = (_places_seen.get()[inv.place] & 1) != 0;
+                            cand = inv.place;
+                        } else if ((*_parent).marking()[inv.place] >= inv.tokens && inv.inhibitor) {
+                            inhib = true;
+                            ok = (_places_seen.get()[inv.place] & 2) != 0;
+                            cand = inv.place;
+                        }
+                        if (ok) break;
+
+                    }
+
+                    // OK, we didnt have sufficient, we just pick whatever is left
+                    // in cand.
+                    assert(cand != std::numeric_limits<uint32_t>::max());
+                    if (!ok && cand != std::numeric_limits<uint32_t>::max()) {
+                        if (!inhib) presetOf(cand);
+                        else postsetOf(cand);
+                    }
+                }
+            }
+        }
 
         std::unique_ptr<bool[]> _enabled, _stubborn;
         size_t _nenabled;
-
-    protected:
         std::unique_ptr<uint8_t[]> _places_seen;
         std::unique_ptr<place_t[]> _places;
         std::unique_ptr<trans_t[]> _transitions;
         light_deque<uint32_t> _unprocessed, _ordering;
         std::unique_ptr<uint32_t[]> _dependency;
-        bool _netContainsInhibitorArcs;
+        bool _netContainsInhibitorArcs, _done;
         std::vector<std::vector<uint32_t>> _inhibpost;
 
         std::vector<PQL::Condition *> _queries;
@@ -151,6 +217,11 @@
         void constructDependency();
 
         void checkForInhibitor();
+
+        void set_all_stubborn() {
+            memset(_stubborn.get(), true, _net.numberOfTransitions());
+            _done = true;
+        }
     };
 }
 

=== modified file 'include/PetriEngine/options.h'
--- include/PetriEngine/options.h	2021-05-24 13:20:23 +0000
+++ include/PetriEngine/options.h	2021-08-05 10:56:53 +0000
@@ -16,6 +16,7 @@
     CTL, LTL
 };
 
+//TODO can be moved to LTL/AlgorithmTypes.h?
 enum class TraceLevel {
     None,
     Transitions,
@@ -28,6 +29,20 @@
     Full
 };
 
+enum class LTLPartialOrder {
+    None,
+    Visible,
+    AutomatonReach,
+    VisibleReach,
+    FullAutomaton
+};
+
+enum class BuchiOptimization {
+    Low = 1,
+    Medium = 2,
+    High = 3
+};
+
 struct options_t {
 //    bool outputtrace = false;
     int kbound = 0;
@@ -66,6 +81,13 @@
     std::string buchi_out_file;
     LTL::BuchiOutType buchi_out_type = LTL::BuchiOutType::Dot;
     APCompression ltl_compress_aps = APCompression::None;
+    LTLPartialOrder ltl_por = LTLPartialOrder::VisibleReach;
+    BuchiOptimization buchiOptimization = BuchiOptimization::Low;
+    const char* ltlHeuristic = "aut";
+
+    bool replay = false;
+    std::string replay_file;
+
 
     std::string query_out_file;
     std::string model_out_file;
@@ -82,7 +104,6 @@
     uint32_t seed_offset = 0;
     int max_intervals = 250; //0 disabled
     int max_intervals_reduced = 5;
-    
     size_t seed() { return ++seed_offset; }
 
     void print() {

=== modified file 'src/LTL/Algorithm/CMakeLists.txt'
--- src/LTL/Algorithm/CMakeLists.txt	2021-04-06 13:25:35 +0000
+++ src/LTL/Algorithm/CMakeLists.txt	2021-08-05 10:56:53 +0000
@@ -1,7 +1,7 @@
 set(CMAKE_INCLUDE_CURRENT_DIR ON)
 
 add_library(LTL_algorithm ${HEADER_FILES}
-        NestedDepthFirstSearch.cpp LTLToBuchi.cpp TarjanModelChecker.cpp RandomNDFS.cpp ModelChecker.cpp)
+        NestedDepthFirstSearch.cpp LTLToBuchi.cpp TarjanModelChecker.cpp)
 
 target_link_libraries(LTL_algorithm PetriEngine)
 add_dependencies(LTL_algorithm ptrie-ext spot-ext)

=== modified file 'src/LTL/Algorithm/LTLToBuchi.cpp'
--- src/LTL/Algorithm/LTLToBuchi.cpp	2021-04-07 07:18:00 +0000
+++ src/LTL/Algorithm/LTLToBuchi.cpp	2021-08-05 10:56:53 +0000
@@ -17,14 +17,13 @@
 
 #include "LTL/LTLToBuchi.h"
 #include "LTL/SuccessorGeneration/BuchiSuccessorGenerator.h"
+#include "PetriEngine/options.h"
 
 #include <spot/twaalgos/translate.hh>
 #include <spot/tl/parse.hh>
 #include <spot/twa/bddprint.hh>
 #include <sstream>
 #include <spot/twaalgos/dot.hh>
-#include <PetriEngine/options.h>
-
 
 using namespace PetriEngine::PQL;
 
@@ -130,9 +129,10 @@
         (*condition)[0]->visit(*this);
     }
 
-    std::pair<spot::formula, APInfo> to_spot_formula(const PetriEngine::PQL::Condition_ptr& query, APCompression compress) {
+    std::pair<spot::formula, APInfo>
+    to_spot_formula (const PetriEngine::PQL::Condition_ptr &query, const options_t &options) {
         std::stringstream ss;
-        FormulaToSpotSyntax spotConverter{ss, compress};
+        FormulaToSpotSyntax spotConverter{ss, options.ltl_compress_aps};
         query->visit(spotConverter);
         std::string spotFormula = ss.str();
         if (spotFormula.at(0) == 'E' || spotFormula.at(0) == 'A') {
@@ -142,14 +142,26 @@
         return std::make_pair(spot_formula, spotConverter.apInfo());
     }
 
-    Structures::BuchiAutomaton makeBuchiAutomaton(const PetriEngine::PQL::Condition_ptr &query, APCompression compress) {
-        auto [formula, apinfo] = to_spot_formula(query, compress);
+    Structures::BuchiAutomaton makeBuchiAutomaton(const PetriEngine::PQL::Condition_ptr &query, const options_t &options) {
+        auto [formula, apinfo] = to_spot_formula(query, options);
         formula = spot::formula::Not(formula);
         spot::translator translator;
         // Ask for Büchi acceptance (rather than generalized Büchi) and medium optimizations
         // (default is high which causes many worst case BDD constructions i.e. exponential blow-up)
         translator.set_type(spot::postprocessor::BA);
-        translator.set_level(spot::postprocessor::Low);
+        spot::postprocessor::optimization_level level;
+        switch(options.buchiOptimization) {
+            case BuchiOptimization::Low:
+                level = spot::postprocessor::Low;
+                break;
+            case BuchiOptimization::Medium:
+                level = spot::postprocessor::Medium;
+                break;
+            case BuchiOptimization::High:
+                level = spot::postprocessor::High;
+                break;
+        }
+        translator.set_level(level);
         spot::twa_graph_ptr automaton = translator.run(formula);
         std::unordered_map<int, AtomicProposition> ap_map;
         // bind PQL expressions to the atomic proposition IDs used by spot.
@@ -162,8 +174,8 @@
         return Structures::BuchiAutomaton{automaton, ap_map};
     }
 
-    BuchiSuccessorGenerator makeBuchiSuccessorGenerator(const Condition_ptr &query, APCompression compress) {
-        return BuchiSuccessorGenerator{makeBuchiAutomaton(query, compress)};
+    BuchiSuccessorGenerator makeBuchiSuccessorGenerator(const Condition_ptr &query, const options_t &options) {
+        return BuchiSuccessorGenerator{makeBuchiAutomaton(query, options)};
     }
 
 }

=== removed file 'src/LTL/Algorithm/ModelChecker.cpp'
=== modified file 'src/LTL/Algorithm/NestedDepthFirstSearch.cpp'
--- src/LTL/Algorithm/NestedDepthFirstSearch.cpp	2021-04-02 09:54:38 +0000
+++ src/LTL/Algorithm/NestedDepthFirstSearch.cpp	2021-08-05 10:56:53 +0000
@@ -18,16 +18,16 @@
 #include "LTL/Algorithm/NestedDepthFirstSearch.h"
 
 namespace LTL {
-    template<typename W>
-    bool NestedDepthFirstSearch<W>::isSatisfied()
+    template<typename S, typename W>
+    bool NestedDepthFirstSearch<S, W>::isSatisfied()
     {
-        is_weak = successorGenerator->is_weak() && shortcircuitweak;
+        this->is_weak = this->successorGenerator->is_weak() && this->shortcircuitweak;
         dfs();
         return !violation;
     }
 
-    template<typename W>
-    void NestedDepthFirstSearch<W>::dfs()
+    template<typename S, typename W>
+    void NestedDepthFirstSearch<S, W>::dfs()
     {
         std::stack<size_t> call_stack;
         std::stack<StackEntry> todo;
@@ -36,26 +36,27 @@
         State curState = factory.newState();
 
         {
-            std::vector<State> initial_states = successorGenerator->makeInitialState();
+
+            std::vector<State> initial_states = this->successorGenerator->makeInitialState();
             for (auto &state : initial_states) {
                 auto res = states.add(state);
                 assert(res.first);
-                todo.push(StackEntry{res.second, LTL::ResumingSuccessorGenerator::initial_suc_info()});
-                _discovered++;
+                todo.push(StackEntry{res.second, S::initial_suc_info()});
+                this->_discovered++;
             }
         }
 
         while (!todo.empty()) {
             auto &top = todo.top();
             states.decode(curState, top.id);
-            successorGenerator->prepare(&curState, top.sucinfo);
+            this->successorGenerator->prepare(&curState, top.sucinfo);
             if (top.sucinfo.has_prev_state()) {
                 states.decode(working, top.sucinfo.last_state);
             }
-            if (!successorGenerator->next(working, top.sucinfo)) {
+            if (!this->successorGenerator->next(working, top.sucinfo)) {
                 // no successor
                 todo.pop();
-                if (successorGenerator->isAccepting(curState)) {
+                if (this->successorGenerator->isAccepting(curState)) {
                     seed = &curState;
                     ndfs(curState);
                     if (violation) {
@@ -63,9 +64,9 @@
                             std::stack<std::pair<size_t, size_t>> transitions;
                             size_t next = top.id;
                             states.decode(working, next);
-                            while (!successorGenerator->isInitialState(working)) {
+                            while (!this->successorGenerator->isInitialState(working)) {
                                 auto[parent, transition] = states.getHistory(next);
-                                transitions.push(std::make_pair(next, transition));
+                                transitions.push(std::make_pair(parent, transition));
                                 next = parent;
                                 states.decode(working, next);
                             }
@@ -81,36 +82,36 @@
                 if (is_new) {
                     if constexpr (SaveTrace) {
                         states.setParent(top.id);
-                        states.setHistory(stateid, successorGenerator->fired());
+                        states.setHistory(stateid, this->successorGenerator->fired());
                     }
-                    _discovered++;
-                    todo.push(StackEntry{stateid, LTL::ResumingSuccessorGenerator::initial_suc_info()});
+                    this->_discovered++;
+                    todo.push(StackEntry{stateid, S::initial_suc_info()});
                 }
             }
         }
     }
 
-    template<typename W>
-    void NestedDepthFirstSearch<W>::ndfs(State &state)
+    template<typename S, typename W>
+    void NestedDepthFirstSearch<S, W>::ndfs(State &state)
     {
         std::stack<StackEntry> todo;
 
         State working = factory.newState();
         State curState = factory.newState();
 
-        todo.push(StackEntry{states.add(state).second, LTL::ResumingSuccessorGenerator::initial_suc_info()});
+        todo.push(StackEntry{states.add(state).second, S::initial_suc_info()});
 
         while (!todo.empty()) {
             auto &top = todo.top();
             states.decode(curState, top.id);
-            successorGenerator->prepare(&curState, top.sucinfo);
+            this->successorGenerator->prepare(&curState, top.sucinfo);
             if (top.sucinfo.has_prev_state()) {
                 states.decode(working, top.sucinfo.last_state);
             }
-            if (!successorGenerator->next(working, top.sucinfo)) {
+            if (!this->successorGenerator->next(working, top.sucinfo)) {
                 todo.pop();
             } else {
-                if (is_weak && !successorGenerator->isAccepting(working)) {
+                if (this->is_weak && !this->successorGenerator->isAccepting(working)) {
                     continue;
                 }
                 if (working == *seed) {
@@ -118,12 +119,12 @@
                     if constexpr (SaveTrace) {
                         auto[_, stateid] = states.add(working);
                         auto seedId = stateid;
-                        states.setHistory2(stateid, successorGenerator->fired());
+                        states.setHistory2(stateid, this->successorGenerator->fired());
                         size_t next = stateid;
                         // follow trace until back at seed state.
                         do {
                             auto[state, transition] = states.getHistory2(next);
-                            nested_transitions.push(std::make_pair(next, transition));
+                            nested_transitions.push(std::make_pair(state, transition));
                             next = state;
                         } while (next != seedId);
                     }
@@ -135,18 +136,18 @@
                 if (is_new) {
                     if constexpr (SaveTrace) {
                         states.setParent(top.id);
-                        states.setHistory2(stateid, successorGenerator->fired());
+                        states.setHistory2(stateid, this->successorGenerator->fired());
                     }
-                    _discovered++;
-                    todo.push(StackEntry{stateid, LTL::ResumingSuccessorGenerator::initial_suc_info()});
+                    this->_discovered++;
+                    todo.push(StackEntry{stateid, S::initial_suc_info()});
                 }
 
             }
         }
     }
 
-    template<typename W>
-    void NestedDepthFirstSearch<W>::printStats(std::ostream &os)
+    template<typename S, typename W>
+    void NestedDepthFirstSearch<S, W>::printStats(std::ostream &os)
     {
         std::cout << "STATS:\n"
                   << "\tdiscovered states:          " << states.discovered() << std::endl
@@ -156,8 +157,8 @@
     }
 
 
-    template<typename W>
-    void NestedDepthFirstSearch<W>::printTrace(std::stack<std::pair<size_t, size_t>> &transitions, std::ostream &os)
+    template<typename S, typename W>
+    void NestedDepthFirstSearch<S, W>::printTrace(std::stack<std::pair<size_t, size_t>> &transitions, std::ostream &os)
     {
         State state = factory.newState();
         os << "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n"
@@ -165,23 +166,29 @@
         while (!transitions.empty()) {
             auto[stateid, transition] = transitions.top();
             states.decode(state, stateid);
-            printTransition(transition, state, os) << std::endl;
+            this->printTransition(transition, state, os) << std::endl;
             transitions.pop();
         }
-        printLoop(os);
+        this->printLoop(os);
         while (!nested_transitions.empty()) {
             auto[stateid, transition] = nested_transitions.top();
             states.decode(state, stateid);
 
-            printTransition(transition, state, os) << std::endl;
+            this->printTransition(transition, state, os) << std::endl;
             nested_transitions.pop();
         }
         os << std::endl << "</trace>" << std::endl;
     }
 
     template
-    class NestedDepthFirstSearch<PetriEngine::Structures::StateSet>;
-
-    template
-    class NestedDepthFirstSearch<PetriEngine::Structures::TracableStateSet>;
-}
\ No newline at end of file
+    class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, PetriEngine::Structures::StateSet>;
+
+    template
+    class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, PetriEngine::Structures::TracableStateSet>;
+
+    template
+    class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, PetriEngine::Structures::StateSet>;
+
+    template
+    class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, PetriEngine::Structures::TracableStateSet>;
+}

=== removed file 'src/LTL/Algorithm/RandomNDFS.cpp'
=== modified file 'src/LTL/Algorithm/TarjanModelChecker.cpp'
--- src/LTL/Algorithm/TarjanModelChecker.cpp	2021-04-02 09:54:38 +0000
+++ src/LTL/Algorithm/TarjanModelChecker.cpp	2021-08-05 10:56:53 +0000
@@ -19,8 +19,8 @@
 
 namespace LTL {
 
-    template<typename S, bool SaveTrace>
-    bool TarjanModelChecker<S, SaveTrace>::isSatisfied()
+    template<template<typename, typename...> typename S, typename G, bool SaveTrace, typename... Spooler>
+    bool TarjanModelChecker<S, G, SaveTrace, Spooler...>::isSatisfied()
     {
         this->is_weak = this->successorGenerator->is_weak() && this->shortcircuitweak;
         std::vector<State> initial_states = this->successorGenerator->makeInitialState();
@@ -47,14 +47,26 @@
                         seen.setHistory(stateid, this->successorGenerator->fired());
                     }
                 }
+
                 dtop.sucinfo.last_state = stateid;
 
                 // lookup successor in 'hash' table
                 auto suc_pos = chash[hash(stateid)];
+                auto marking = seen.getMarkingId(stateid);
                 while (suc_pos != std::numeric_limits<idx_t>::max() && cstack[suc_pos].stateid != stateid) {
+                    if constexpr (IsSpooling) {
+                        if (cstack[suc_pos].dstack && seen.getMarkingId(cstack[suc_pos].stateid) == marking) {
+                            this->successorGenerator->generateAll(&parent, dtop.sucinfo);
+                        }
+                    }
                     suc_pos = cstack[suc_pos].next;
                 }
                 if (suc_pos != std::numeric_limits<idx_t>::max()) {
+                    if constexpr (IsSpooling) {
+                        if (cstack[suc_pos].dstack) {
+                            this->successorGenerator->generateAll(&parent, dtop.sucinfo);
+                        }
+                    }
                     // we found the successor, i.e. there's a loop!
                     // now update lowlinks and check whether the loop contains an accepting state
                     update(suc_pos);
@@ -84,8 +96,8 @@
      * Push a state to the various stacks.
      * @param state
      */
-    template<typename S, bool SaveTrace>
-    void TarjanModelChecker<S, SaveTrace>::push(State &state, size_t stateid) {
+    template<template<typename, typename...> typename S, typename G, bool SaveTrace, typename... Spooler>
+    void TarjanModelChecker<S, G, SaveTrace, Spooler...>::push(State &state, size_t stateid) {
         const auto ctop = static_cast<idx_t>(cstack.size());
         const auto h = hash(stateid);
         cstack.emplace_back(ctop, stateid, chash[h]);
@@ -93,19 +105,23 @@
         dstack.push(DEntry{ctop});
         if (this->successorGenerator->isAccepting(state)) {
             astack.push(ctop);
-            if (this->successorGenerator->has_invariant_self_loop(state)){
+            if (this->successorGenerator->has_invariant_self_loop(state) && !SaveTrace){
                 //std::cerr << "Invariant self loop found. Violation is true" << std::endl;
                 violation = true;
                 invariant_loop = true;
             }
         }
+        if constexpr (IsSpooling) {
+            this->successorGenerator->push();
+        }
     }
 
-    template<typename S, bool SaveTrace>
-    void TarjanModelChecker<S, SaveTrace>::pop()
+    template<template<typename, typename...> typename S, typename G, bool SaveTrace, typename... Spooler>
+    void TarjanModelChecker<S, G, SaveTrace, Spooler...>::pop()
     {
         const auto p = dstack.top().pos;
         dstack.pop();
+        cstack[p].dstack = false;
         if (cstack[p].lowlink == p) {
             while (cstack.size() > p) {
                 popCStack();
@@ -122,11 +138,14 @@
         }
         if (!dstack.empty()) {
             update(p);
+            if constexpr (IsSpooling) {
+                this->successorGenerator->pop(dstack.top().sucinfo);
+            }
         }
     }
 
-    template<typename S, bool SaveTrace>
-    void TarjanModelChecker<S, SaveTrace>::popCStack()
+    template<template<typename, typename...> typename S, typename G, bool SaveTrace, typename... Spooler>
+    void TarjanModelChecker<S, G, SaveTrace, Spooler...>::popCStack()
     {
         auto h = hash(cstack.back().stateid);
         store.insert(cstack.back().stateid);
@@ -134,10 +153,11 @@
         cstack.pop_back();
     }
 
-    template<typename S, bool SaveTrace>
-    void TarjanModelChecker<S, SaveTrace>::update(idx_t to)
+    template<template<typename, typename...> typename S, typename G, bool SaveTrace, typename... Spooler>
+    void TarjanModelChecker<S, G, SaveTrace, Spooler...>::update(idx_t to)
     {
         const auto from = dstack.top().pos;
+        assert(cstack[to].lowlink != std::numeric_limits<idx_t>::max() && cstack[from].lowlink != std::numeric_limits<idx_t>::max());
         if (cstack[to].lowlink <= cstack[from].lowlink) {
             // we have now found a loop into earlier seen component cstack[to].lowlink.
             // if this earlier component precedes an accepting state,
@@ -146,7 +166,7 @@
             // either way update the component ID of the state we came from.
             cstack[from].lowlink = cstack[to].lowlink;
             if constexpr (SaveTrace) {
-                loopstate = cstack[to].stateid;
+                loopstate = cstack[from].stateid;
                 looptrans = this->successorGenerator->fired();
                 cstack[from].lowsource = to;
 
@@ -154,8 +174,8 @@
         }
     }
 
-    template<typename S, bool SaveTrace>
-    bool TarjanModelChecker<S, SaveTrace>::nexttrans(State &state, State &parent, TarjanModelChecker::DEntry &delem)
+    template<template<typename, typename...> typename S, typename G, bool SaveTrace, typename... Spooler>
+    bool TarjanModelChecker<S, G, SaveTrace, Spooler...>::nexttrans(State &state, State &parent, TarjanModelChecker::DEntry &delem)
     {
         seen.decode(parent, cstack[delem.pos].stateid);
         this->successorGenerator->prepare(&parent, delem.sucinfo);
@@ -167,12 +187,13 @@
         return res;
     }
 
-    template<typename S, bool SaveTrace>
-    void TarjanModelChecker<S, SaveTrace>::printTrace(std::stack<DEntry> &&dstack, std::ostream &os)
+    template<template<typename, typename...> typename S, typename G, bool SaveTrace, typename... Spooler>
+    void TarjanModelChecker<S, G, SaveTrace, Spooler...>::printTrace(std::stack<DEntry> &&dstack, std::ostream &os)
     {
         if constexpr (!SaveTrace) {
             return;
         } else {
+            assert(violation);
             State state = factory.newState();
             os << "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n"
                   "<trace>\n";
@@ -185,10 +206,10 @@
                 p = dstack.top().pos;
                 auto stateid = cstack[p].stateid;
                 auto[parent, tid] = seen.getHistory(stateid);
-                seen.decode(state, stateid);
+                seen.decode(state, parent);
 
-                this->printTransition(tid, state, os) << '\n';
                 if (stateid == loopstate) this->printLoop(os);
+                this->printTransition(tid, state, os) << '\n';
 
                 cstack[p].lowlink = std::numeric_limits<idx_t>::max();
                 dstack.pop();
@@ -198,7 +219,7 @@
             p = cstack[p].lowsource;
             while (cstack[p].lowlink != std::numeric_limits<idx_t>::max()) {
                 auto[parent, tid] = seen.getHistory(cstack[p].stateid);
-                seen.decode(state, cstack[p].stateid);
+                seen.decode(state, parent);
                 this->printTransition(tid, state, os) << '\n';
                 assert(cstack[p].lowsource != std::numeric_limits<idx_t>::max());
                 p = cstack[p].lowsource;
@@ -211,14 +232,26 @@
     }
 
     template
-    class TarjanModelChecker<LTL::ResumingSuccessorGenerator, true>;
-
-    template
-    class TarjanModelChecker<LTL::ResumingSuccessorGenerator, false>;
-
-    template
-    class TarjanModelChecker<LTL::SpoolingSuccessorGenerator, true>;
-
-    template
-    class TarjanModelChecker<LTL::SpoolingSuccessorGenerator, false>;
+    class TarjanModelChecker<ProductSuccessorGenerator, LTL::ResumingSuccessorGenerator, true>;
+
+    template
+    class TarjanModelChecker<ProductSuccessorGenerator, LTL::ResumingSuccessorGenerator, false>;
+
+    template
+    class TarjanModelChecker<ProductSuccessorGenerator, LTL::SpoolingSuccessorGenerator, true>;
+
+    template
+    class TarjanModelChecker<ProductSuccessorGenerator, LTL::SpoolingSuccessorGenerator, false>;
+
+    template
+    class TarjanModelChecker<ReachStubProductSuccessorGenerator, LTL::SpoolingSuccessorGenerator, true, VisibleLTLStubbornSet>;
+
+    template
+    class TarjanModelChecker<ReachStubProductSuccessorGenerator, LTL::SpoolingSuccessorGenerator, false, VisibleLTLStubbornSet>;
+
+    template
+    class TarjanModelChecker<ReachStubProductSuccessorGenerator, LTL::SpoolingSuccessorGenerator, true, EnabledSpooler>;
+
+    template
+    class TarjanModelChecker<ReachStubProductSuccessorGenerator, LTL::SpoolingSuccessorGenerator, false, EnabledSpooler>;
 }

=== modified file 'src/LTL/CMakeLists.txt'
--- src/LTL/CMakeLists.txt	2021-04-06 07:37:30 +0000
+++ src/LTL/CMakeLists.txt	2021-08-05 10:56:53 +0000
@@ -3,13 +3,15 @@
 
 add_subdirectory(Algorithm)
 add_subdirectory(Simplification)
+
+add_subdirectory(Stubborn)
 add_subdirectory(SuccessorGeneration)
 
-add_library(LTL ${HEADER_FILES} LTLMain.cpp)
+add_library(LTL ${HEADER_FILES} LTLMain.cpp Replay.cpp)
 
 if (VERIFYPN_Static OR APPLE)
-    target_link_libraries(LTL PRIVATE LTL_algorithm LTL_simplification LTLSuccessorGeneration spot bddx)
+    target_link_libraries(LTL PRIVATE LTL_algorithm LTLStubborn LTL_simplification LTLSuccessorGeneration spot bddx)
 else()
-    target_link_libraries(LTL PRIVATE LTL_algorithm LTL_simplification LTLSuccessorGeneration
-                              -Wl,-Bstatic spot bddx -Wl,-Bdynamic)
+    target_link_libraries(LTL PRIVATE LTL_algorithm LTLStubborn LTL_simplification LTLSuccessorGeneration
+                          -Wl,-Bstatic spot bddx -Wl,-Bdynamic)
 endif()

=== modified file 'src/LTL/LTLMain.cpp'
--- src/LTL/LTLMain.cpp	2021-07-05 19:55:24 +0000
+++ src/LTL/LTLMain.cpp	2021-08-05 10:56:53 +0000
@@ -22,13 +22,15 @@
 
 #include "LTL/SuccessorGeneration/Spoolers.h"
 #include "LTL/SuccessorGeneration/Heuristics.h"
+#include "LTL/SuccessorGeneration/HeuristicParser.h"
 
 #include <utility>
 
 using namespace PetriEngine::PQL;
 using namespace PetriEngine;
 
-//#define DEBUG_EXPLORED_STATES
+// Causes FORMULA <qname> STATS EXPLORED <nexplored> to be printed after verification. Remove if this causes a nuisance.
+// #define DEBUG_EXPLORED_STATES
 
 namespace LTL {
     struct Result {
@@ -75,6 +77,7 @@
                    const options_t &options)
     {
         Result result;
+        checker->setOptions(options);
         result.satisfied = checker->isSatisfied();
         result.is_weak = checker->isweak();
 #ifdef DEBUG_EXPLORED_STATES
@@ -86,7 +89,25 @@
         return result;
     }
 
-    ReturnValue LTLMain(const PetriNet *net,
+    std::unique_ptr<Heuristic> make_heuristic(const PetriNet *net,
+                                              const Condition_ptr &negated_formula,
+                                              const Structures::BuchiAutomaton& automaton,
+                                              options_t &options) {
+        if (options.strategy == Reachability::Strategy::RDFS) {
+            return std::make_unique<RandomHeuristic>(options.seed());
+        }
+        if (options.strategy != Reachability::Strategy::HEUR && options.strategy != Reachability::Strategy::DEFAULT) {
+            return nullptr;
+        }
+        auto heur = ParseHeuristic(net, automaton, negated_formula, options.ltlHeuristic);
+        if (heur == nullptr) {
+            std::cerr << "Invalid heuristic specification, terminating.\n";
+            exit(1);
+        }
+        else return heur;
+    }
+
+    bool LTLMain(const PetriNet *net,
                         const Condition_ptr &query,
                         const std::string &queryName,
                         options_t &options)
@@ -96,92 +117,174 @@
         bool negate_answer = res.second;
 
         // force AP compress off for Büchi prints
-        auto compress = options.buchi_out_file.empty() ? options.ltl_compress_aps : APCompression::None;
+        options.ltl_compress_aps = options.buchi_out_file.empty() ? options.ltl_compress_aps : APCompression::None;
 
-        Structures::BuchiAutomaton automaton = makeBuchiAutomaton(negated_formula, compress);
+        Structures::BuchiAutomaton automaton = makeBuchiAutomaton(negated_formula, options);
         if (!options.buchi_out_file.empty()) {
             automaton.output_buchi(options.buchi_out_file, options.buchi_out_type);
         }
 
+        bool is_visible_stub = options.stubbornreduction
+                               && (options.ltl_por == LTLPartialOrder::Visible || options.ltl_por == LTLPartialOrder::VisibleReach)
+                               && !net->has_inhibitor()
+                                 && !negated_formula->containsNext();
+        bool is_autreach_stub = options.stubbornreduction
+                && (options.ltl_por == LTLPartialOrder::AutomatonReach ||
+                    options.ltl_por == LTLPartialOrder::VisibleReach)
+                && !net->has_inhibitor();
+        bool is_buchi_stub = options.stubbornreduction
+                && options.ltl_por == LTLPartialOrder::FullAutomaton
+                && !net->has_inhibitor();
+
+        bool is_stubborn = options.ltl_por != LTLPartialOrder::None && (is_visible_stub || is_autreach_stub || is_buchi_stub);
+
+        std::unique_ptr<SuccessorSpooler> spooler;
+        std::unique_ptr<Heuristic> heuristic = make_heuristic(net, negated_formula, automaton, options);
+
         Result result;
         switch (options.ltlalgorithm) {
             case Algorithm::NDFS:
-                if (options.strategy == PetriEngine::Reachability::RDFS) {
+                if (options.strategy != PetriEngine::Reachability::DFS) {
                     SpoolingSuccessorGenerator gen{net, negated_formula};
-                    gen.setSpooler(std::make_unique<EnabledSpooler>(net, gen));
-                    gen.setHeuristic(std::make_unique<RandomHeuristic>());
+                    spooler = std::make_unique<EnabledSpooler>(net, gen);
+                    gen.setSpooler(spooler.get());
+                    gen.setHeuristic(heuristic.get());
 
-                    result = _verify(net, negated_formula,
-                                     std::make_unique<RandomNDFS>(net, negated_formula, automaton, std::move(gen),
-                                                                  options.trace,
-                                                                  options.ltluseweak, options.seed()),
-                                     options);
-                } else if (options.trace != TraceLevel::None) {
-                    result = _verify(net, negated_formula,
-                                     std::make_unique<NestedDepthFirstSearch<PetriEngine::Structures::TracableStateSet>>(
-                                             net, negated_formula, automaton, options.trace, options.ltluseweak),
-                                     options);
+                    if (options.trace != TraceLevel::None) {
+                        result = _verify(
+                                net, negated_formula,
+                                std::make_unique<NestedDepthFirstSearch<SpoolingSuccessorGenerator, PetriEngine::Structures::TracableStateSet>>(
+                                        net, negated_formula, automaton, &gen),
+                                options);
+                    } else {
+                        result = _verify(
+                                net, negated_formula,
+                                std::make_unique<NestedDepthFirstSearch<SpoolingSuccessorGenerator, PetriEngine::Structures::StateSet>>(
+                                        net, negated_formula, automaton, &gen),
+                                options);
+                    }
                 } else {
-                    result = _verify(net, negated_formula,
-                                     std::make_unique<NestedDepthFirstSearch<PetriEngine::Structures::StateSet>>(
-                                             net, negated_formula, automaton, options.trace, options.ltluseweak),
-                                     options);
+                    ResumingSuccessorGenerator gen{net};
+                    if (options.trace != TraceLevel::None) {
+                        result = _verify(
+                                net, negated_formula,
+                                std::make_unique<NestedDepthFirstSearch<ResumingSuccessorGenerator, PetriEngine::Structures::TracableStateSet>>(
+                                        net, negated_formula, automaton, &gen),
+                                options);
+                    } else {
+                        result = _verify(
+                                net, negated_formula,
+                                std::make_unique<NestedDepthFirstSearch<ResumingSuccessorGenerator, PetriEngine::Structures::StateSet>>(
+                                        net, negated_formula, automaton, &gen),
+                                options);
+                    }
                 }
                 break;
+
             case Algorithm::Tarjan:
-                if (options.strategy != PetriEngine::Reachability::DFS) {
+                if (options.strategy != PetriEngine::Reachability::DFS || is_stubborn) {
+                    // Use spooling successor generator in case of different search strategy or stubborn set method.
                     // Running default, BestFS, or RDFS search strategy so use spooling successor generator to enable heuristics.
                     SpoolingSuccessorGenerator gen{net, negated_formula};
-                    gen.setSpooler(std::make_unique<EnabledSpooler>(net, gen));
-                    if (options.strategy == PetriEngine::Reachability::RDFS) {
-                        gen.setHeuristic(std::make_unique<RandomHeuristic>(options.seed()));
-                    } else if (options.strategy == PetriEngine::Reachability::HEUR
-                               || options.strategy == PetriEngine::Reachability::DEFAULT) {
-                        gen.setHeuristic(std::make_unique<AutomatonHeuristic>(net, automaton));
+                    if (is_visible_stub) {
+                        std::cout << "Running stubborn version!" << std::endl;
+                        spooler = std::make_unique<VisibleLTLStubbornSet>(*net, negated_formula);
+                    } else if (is_buchi_stub) {
+                        spooler = std::make_unique<AutomatonStubbornSet>(*net, automaton);
+                    }
+                    else {
+                        spooler = std::make_unique<EnabledSpooler>(net, gen);
+                    }
+
+                    assert(spooler);
+                    gen.setSpooler(spooler.get());
+                    // if search strategy used, set heuristic, otherwise ignore it
+                    // (default is null which is checked elsewhere)
+                    if (options.strategy != PetriEngine::Reachability::DFS) {
+                        assert(heuristic != nullptr);
+                        gen.setHeuristic(heuristic.get());
                     }
 
                     if (options.trace != TraceLevel::None) {
-                        result = _verify(net, negated_formula,
-                                         std::make_unique<TarjanModelChecker<SpoolingSuccessorGenerator, true>>(
-                                                 net,
-                                                 negated_formula,
-                                                 automaton,
-                                                 std::move(gen),
-                                                 options.trace,
-                                                 options.ltluseweak),
-                                         options);
+                        if (is_autreach_stub && is_visible_stub) {
+                            result = _verify(net, negated_formula,
+                                             std::make_unique<TarjanModelChecker<ReachStubProductSuccessorGenerator, SpoolingSuccessorGenerator, true, VisibleLTLStubbornSet>>(
+                                                     net,
+                                                     negated_formula,
+                                                     automaton,
+                                                     &gen,
+                                                     std::make_unique<VisibleLTLStubbornSet>(*net, negated_formula)),
+                                             options);
+                        }
+                        else if (is_autreach_stub && !is_visible_stub) {
+                            result = _verify(net, negated_formula,
+                                             std::make_unique<TarjanModelChecker<ReachStubProductSuccessorGenerator, SpoolingSuccessorGenerator, true, EnabledSpooler>>(
+                                                     net,
+                                                     negated_formula,
+                                                     automaton,
+                                                     &gen,
+                                                     std::make_unique<EnabledSpooler>(net, gen)),
+                                             options);
+                        }
+                        else {
+                            result = _verify(net, negated_formula,
+                                             std::make_unique<TarjanModelChecker<ProductSuccessorGenerator, SpoolingSuccessorGenerator, true>>(
+                                                     net,
+                                                     negated_formula,
+                                                     automaton,
+                                                     &gen),
+                                             options);
+                        }
                     } else {
-                        result = _verify(net, negated_formula,
-                                         std::make_unique<TarjanModelChecker<SpoolingSuccessorGenerator, false>>(
-                                                 net,
-                                                 negated_formula,
-                                                 automaton,
-                                                 std::move(gen),
-                                                 options.trace,
-                                                 options.ltluseweak),
-                                         options);
+
+                        if (is_autreach_stub && is_visible_stub) {
+                            result = _verify(net, negated_formula,
+                                             std::make_unique<TarjanModelChecker<ReachStubProductSuccessorGenerator, SpoolingSuccessorGenerator, false, VisibleLTLStubbornSet>>(
+                                                     net,
+                                                     negated_formula,
+                                                     automaton,
+                                                     &gen,
+                                                     std::make_unique<VisibleLTLStubbornSet>(*net, negated_formula)),
+                                             options);
+                        } else if (is_autreach_stub && !is_visible_stub) {
+                            result = _verify(net, negated_formula,
+                                             std::make_unique<TarjanModelChecker<ReachStubProductSuccessorGenerator, SpoolingSuccessorGenerator, false, EnabledSpooler>>(
+                                                     net,
+                                                     negated_formula,
+                                                     automaton,
+                                                     &gen,
+                                                     std::make_unique<EnabledSpooler>(net, gen)),
+                                             options);
+                        }
+                        else {
+                            result = _verify(net, negated_formula,
+                                             std::make_unique<TarjanModelChecker<ProductSuccessorGenerator, SpoolingSuccessorGenerator, false>>(
+                                                     net,
+                                                     negated_formula,
+                                                     automaton,
+                                                     &gen),
+                                             options);
+                        }
                     }
                 } else {
+                    ResumingSuccessorGenerator gen{net};
+
                     // no spooling needed, thus use resuming successor generation
                     if (options.trace != TraceLevel::None) {
                         result = _verify(net, negated_formula,
-                                         std::make_unique<TarjanModelChecker<ResumingSuccessorGenerator, true>>(
+                                         std::make_unique<TarjanModelChecker<ProductSuccessorGenerator, ResumingSuccessorGenerator, true>>(
                                                  net,
                                                  negated_formula,
                                                  automaton,
-                                                 ResumingSuccessorGenerator{*net},
-                                                 options.trace,
-                                                 options.ltluseweak),
+                                                 &gen),
                                          options);
                     } else {
                         result = _verify(net, negated_formula,
-                                         std::make_unique<TarjanModelChecker<ResumingSuccessorGenerator, false>>(
+                                         std::make_unique<TarjanModelChecker<ProductSuccessorGenerator, ResumingSuccessorGenerator, false>>(
                                                  net,
                                                  negated_formula,
                                                  automaton,
-                                                 ResumingSuccessorGenerator{*net},
-                                                 options.trace,
-                                                 options.ltluseweak),
+                                                 &gen),
                                          options);
                     }
                 }
@@ -194,11 +297,18 @@
                   << (result.satisfied ^ negate_answer ? " TRUE" : " FALSE") << " TECHNIQUES EXPLICIT "
                   << LTL::to_string(options.ltlalgorithm)
                   << (result.is_weak ? " WEAK_SKIP" : "")
-                  << std::endl;
+                  << (is_stubborn ? " STUBBORN" : "")
+                  << (is_visible_stub ? " CLASSIC_STUB" : "")
+                  << (is_autreach_stub ? " REACH_STUB" : "")
+                  << (is_buchi_stub ? " BUCHI_STUB" : "");
+        if (heuristic != nullptr) {
+            std::cout << " HEURISTIC ";
+            heuristic->output(std::cout);
+        }
+        std::cout << " OPTIM-" << static_cast<int>(options.buchiOptimization) << std::endl;
 #ifdef DEBUG_EXPLORED_STATES
         std::cout << "FORMULA " << queryName << " STATS EXPLORED " << result.explored_states << std::endl;
 #endif
-
-        return SuccessCode;
+        return result.satisfied ^ negate_answer;
     }
 }

=== added file 'src/LTL/Replay.cpp'
--- src/LTL/Replay.cpp	1970-01-01 00:00:00 +0000
+++ src/LTL/Replay.cpp	2021-08-05 10:56:53 +0000
@@ -0,0 +1,326 @@
+/* Copyright (C) 2021  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ * 
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ * 
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ * 
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#include "PetriEngine/PQL/PQL.h"
+#include "PetriEngine/PetriNet.h"
+#include "LTL/Replay.h"
+#include "PetriEngine/Structures/State.h"
+#include "PetriEngine/SuccessorGenerator.h"
+#include "LTL/LTLToBuchi.h"
+
+#include <rapidxml.hpp>
+#include <vector>
+#include <iostream>
+#include <cstring>
+
+using namespace PetriEngine;
+using namespace PetriEngine::PQL;
+
+namespace LTL {
+    bool guard_valid(const PQL::EvaluationContext &ctx, const BuchiSuccessorGenerator &buchi, bdd bdd);
+
+    Replay::Replay(std::istream &is, const PetriEngine::PetriNet *net)
+    {
+        parse(is, net);
+    }
+
+    void Replay::parse(std::istream &xml, const PetriNet *net)
+    {
+        places.clear();
+        transitions.clear();
+        // preallocate reverse lookup for transition and place names. Assume this is always called with the same Petri net.
+        for (int i = 0; i < net->placeNames().size(); ++i) {
+            places[net->placeNames()[i]] = i;
+        }
+        for (int i = 0; i < net->transitionNames().size(); ++i) {
+            transitions[net->transitionNames()[i]] = i;
+        }
+        transitions[DEADLOCK_TRANS] = -1;
+
+        // TODO can also validate transition names up front.
+        rapidxml::xml_document<> doc;
+        std::vector<char> buffer((std::istreambuf_iterator<char>(xml)), std::istreambuf_iterator<char>());
+        buffer.push_back('\0');
+        doc.parse<0>(buffer.data());
+        rapidxml::xml_node<> *root = doc.first_node();
+
+        if (root) {
+            parseRoot(root);
+        } else {
+            std::cerr << "Error getting root node." << std::endl;
+            assert(false);
+            exit(1);
+        }
+
+    }
+
+    void Replay::parseRoot(const rapidxml::xml_node<> *pNode)
+    {
+        if (std::strcmp(pNode->name(), "trace") != 0) {
+            std::cerr << "Error: Expected trace node. Got: " << pNode->name() << std::endl;
+            assert(false);
+            exit(1);
+        }
+        for (auto it = pNode->first_node(); it; it = it->next_sibling()) {
+            if (std::strcmp(it->name(), "loop") == 0) loop_idx = trace.size();
+            else if (std::strcmp(it->name(), "transition") == 0 || std::strcmp(it->name(), "deadlock") == 0) {
+                trace.push_back(parseTransition(it));
+            } else {
+                std::cerr << "Error: Expected transition or loop node. Got: " << it->name() << std::endl;
+                assert(false);
+                exit(1);
+            }
+        }
+        if (loop_idx == std::numeric_limits<size_t>::max()) {
+            std::cerr << "Error: Missing <loop/> statement in trace\n";
+            exit(1);
+        }
+    }
+
+    Replay::Transition Replay::parseTransition(const rapidxml::xml_node<char> *pNode)
+    {
+        std::string id;
+        int buchi = -1;
+        for (auto it = pNode->first_attribute(); it; it = it->next_attribute()) {
+            if (std::strcmp(it->name(), "id") == 0) {
+                id = std::string(it->value());
+            }
+            if (std::strstr(it->name(), "buchi") != nullptr) {
+                // buchi field is sometimes spelled slightly differently, but will always contain 'buchi'
+                buchi = std::stoi(it->value());
+            }
+        }
+        if (strcmp(pNode->name(), "deadlock") == 0) {
+            id = DEADLOCK_TRANS;
+        }
+        if (id.empty()) {
+            std::cerr << "Error: Transition has no id attribute" << std::endl;
+            assert(false);
+            exit(1);
+        }
+        if (buchi == -1) {
+            std::cerr << "Error: Missing Büchi state" << std::endl;
+            assert(false);
+            exit(1);
+        }
+
+        Transition transition(id, buchi);
+
+        for (auto it = pNode->first_node(); it; it = it->next_sibling()) {
+            if (std::strcmp(it->name(), "token") != 0) {
+                std::cerr << "Warning: Unexpected transition child. Expected: token, but got: " << it->name()
+                          << std::endl;
+            }
+            parseToken(it, transition.tokens);
+        }
+
+        return transition;
+    }
+
+    void
+    Replay::parseToken(const rapidxml::xml_node<char> *pNode, std::unordered_map<uint32_t, uint32_t> &current_marking)
+    {
+        for (auto it = pNode->first_attribute(); it; it = it->next_attribute()) {
+            if (std::strcmp(it->name(), "place") == 0) {
+                std::string val{it->value()};
+                if (current_marking.find(places.at(val)) == current_marking.end()) {
+                    current_marking[places.at(val)] = 1;
+                } else {
+                    ++current_marking[places.at(val)];
+                }
+            }
+        }
+    }
+
+    bool Replay::replay(const PetriEngine::PetriNet *net, const PetriEngine::PQL::Condition_ptr &cond, const options_t &options)
+    {
+        BuchiSuccessorGenerator buchiGenerator = makeBuchiSuccessorGenerator(cond, options);
+        //spot::print_dot(std::cerr, buchiGenerator.aut._buchi);
+        PetriEngine::Structures::State state;
+        state.setMarking(net->makeInitialMarking());
+        PetriEngine::SuccessorGenerator successorGenerator(*net);
+
+        // generate all initial Buchi states since trace may be dependent on only some initial state.
+        size_t prev_buchi = buchiGenerator.initial_state_number();
+        buchiGenerator.prepare(prev_buchi);
+        bdd bdd;
+        std::vector<size_t> init_buchi_states;
+        while (buchiGenerator.next(prev_buchi, bdd)) {
+            if (guard_valid(EvaluationContext{state.marking(), net}, buchiGenerator, bdd)) {
+                init_buchi_states.push_back(prev_buchi);
+            }
+        }
+        std::cout << "Playing back trace. Length: " << trace.size() << std::endl;
+        for (int i = 0; i < init_buchi_states.size(); ++i) {
+            std::cerr << "Replaying initial state " << i << "/" << init_buchi_states.size() << std::endl;
+            if (_play_trace(net, successorGenerator, buchiGenerator, init_buchi_states[i])) {
+                std::cerr << "Replay complete. No errors" << std::endl;
+                return true;
+            }
+        }
+        std::cerr << "ERROR The trace could not be played back using any valid initial Büchi state. "
+                  << "See previous output for details."
+                  << std::endl;
+        return false;
+    }
+
+    bool Replay::_play_trace(const PetriEngine::PetriNet *net, PetriEngine::SuccessorGenerator &successorGenerator,
+                             BuchiSuccessorGenerator &buchiGenerator, size_t init_buchi)
+    {
+        PetriEngine::Structures::State state;
+        PetriEngine::Structures::State loopstate;
+        size_t loop_buchi;
+        bool loop_accepting = false;
+        bool looping = false;
+        state.setMarking(net->makeInitialMarking());
+        loopstate.setMarking(net->makeInitialMarking());
+        size_t prev_buchi = init_buchi;
+        bdd bdd;
+        bool buchi_failed = false;
+        for (int i = 0; i < trace.size(); ++i) {
+            const Transition &transition = trace[i];
+            // looping part should end up at the state _before_ the <loop/> tag,
+            // hence copy state from previous iteration.
+            if (i == loop_idx) {
+                memcpy(loopstate.marking(), state.marking(), sizeof(uint32_t) * net->numberOfPlaces());
+                loop_buchi = prev_buchi;
+                looping = true;
+            }
+            successorGenerator.prepare(&state);
+            buchiGenerator.prepare(prev_buchi);
+            auto it = transitions.find(transition.id);
+            if (it == std::end(transitions)) {
+                std::cerr << "Unrecognized transition name " << transition.id << std::endl;
+                assert(false);
+                exit(1);
+            }
+            int tid = it->second;
+
+            if (tid != -1) {
+                // fire transition
+                if (!successorGenerator.checkPreset(tid)) {
+                    std::cerr
+                            << "ERROR the provided trace cannot be replayed on the provided model. Offending transition: "
+                            << transition.id << " at index: " << i << "\n";
+                    exit(1);
+                }
+                successorGenerator.consumePreset(state, tid);
+                successorGenerator.producePostset(state, tid);
+            }
+            else {
+                // NOTE Deadlock check, not yet implemented. This assumes no transition in the net is named ##deadlock.
+            }
+
+            if (!transition.tokens.empty()) {
+                for (int pid = 0; pid < net->numberOfPlaces(); ++pid) {
+                    if (transition.tokens.find(pid) == std::end(transition.tokens)) {
+                        // If trace didn't mention the place, then it must have 0 tokens.
+                        if (state.marking()[pid] > 0) {
+                            std::cerr << "ERROR the playback of the trace resulted in mismatch of token counts. \n"
+                                         "  Offending place " << net->placeNames()[pid] << ", expected " << 0
+                                      << " tokens but got " << state.marking()[pid] << std::endl;
+                            std::cerr << "  Offending transition: " << transition.id << " at index: " << i << "\n";
+                            exit(1);
+                        }
+                    } else if (transition.tokens.at(pid) != state.marking()[pid]) {
+                        // If trace did mention the place, then validate token count.
+                        std::cerr << "ERROR the playback of the trace resulted in mismatch of token counts. \n"
+                                     "  Offending place " << net->placeNames()[pid] << ", expected "
+                                  << transition.tokens.at(pid)
+                                  << " tokens but got " << state.marking()[pid] << std::endl;
+                        std::cerr << "Offending transition: " << transition.id << " at index: " << i << "\n";
+                        exit(1);
+                    }
+                }
+            }
+            size_t next_buchi = -1;
+            const EvaluationContext &ctx = EvaluationContext{state.marking(), net};
+            while (buchiGenerator.next(next_buchi, bdd)) {
+                if (next_buchi == transition.buchi_state) break;
+            }
+            if (!guard_valid(ctx, buchiGenerator, bdd)) {
+                // warning since technically we may have multiple initial buchi states,
+                // and maybe only some will allow replaying the trace.
+                std::cerr << "WARNING guard invalid for noted buchi state " << transition.buchi_state
+                          << " at index " << i << ". Attempting to proceed anyway.\n";
+                buchi_failed = true;
+            }
+            prev_buchi = next_buchi;
+            if (looping && buchiGenerator.is_accepting(prev_buchi)) {
+                loop_accepting = true;
+            }
+
+            if (i % 100000 == 0)
+                std::cerr << i << "/" << trace.size() << std::endl;
+        }
+
+        bool err = false;
+        for (int i = 0; i < net->numberOfPlaces(); ++i) {
+            if (state.marking()[i] != loopstate.marking()[i]) {
+                if (!err) {
+                    std::cerr << "ERROR end state not equal to expected loop state.\n";
+                    err = true;
+                }
+                std::cerr << "  " << net->placeNames()[i] << ": expected" << loopstate.marking()[i] << ", actual "
+                          << state.marking()[i] << '\n';
+            }
+        }
+        if (prev_buchi != loop_buchi) {
+            if (!err) {
+                std::cerr << "ERROR end state not equal to expected loop state.\n";
+                err = true;
+            }
+            std::cerr << "Buchi state: expected " << loop_buchi << ", actual " << prev_buchi << std::endl;
+        }
+        if (err) exit(1);
+
+        if (!loop_accepting) {
+            std::cerr << "WARNING trace did not demonstrate accepting loop using initial Buchi state " << init_buchi
+                      << ".\n";
+            return false;
+        }
+
+        return !buchi_failed;
+    }
+
+    bool guard_valid(const PQL::EvaluationContext &ctx, const BuchiSuccessorGenerator &buchi, bdd bdd)
+    {
+        using namespace PetriEngine::PQL;
+        // IDs 0 and 1 are false and true atoms, respectively
+        // More details in buddy manual for details ( http://buddy.sourceforge.net/manual/main.html )
+        while (bdd.id() > 1) {
+            // find variable to test, and test it
+            size_t var = bdd_var(bdd);
+            Condition::Result res = buchi.getExpression(var)->evaluate(ctx);
+            switch (res) {
+                case Condition::RUNKNOWN:
+                    std::cerr << "Unexpected unknown answer from evaluating query!\n";
+                    assert(false);
+                    exit(1);
+                    break;
+                case Condition::RFALSE:
+                    bdd = bdd_low(bdd);
+                    break;
+                case Condition::RTRUE:
+                    bdd = bdd_high(bdd);
+                    break;
+            }
+        }
+        return bdd == bddtrue;
+    }
+
+}

=== added file 'src/LTL/Simplification/CMakeLists.txt'
=== removed file 'src/LTL/Simplification/CMakeLists.txt'
=== modified file 'src/LTL/Simplification/SpotToPQL.cpp'
--- src/LTL/Simplification/SpotToPQL.cpp	2021-04-06 13:10:00 +0000
+++ src/LTL/Simplification/SpotToPQL.cpp	2021-08-05 10:56:53 +0000
@@ -143,15 +143,15 @@
         }
     }
 
-    PetriEngine::PQL::Condition_ptr simplify(const PetriEngine::PQL::Condition_ptr &formula, APCompression compress) {
+    PetriEngine::PQL::Condition_ptr simplify(const PetriEngine::PQL::Condition_ptr &formula, const options_t &options) {
         using namespace PetriEngine::PQL;
         if (auto e = std::dynamic_pointer_cast<ECondition>(formula); e != nullptr) {
-            return std::make_shared<ECondition>(simplify((*e)[0]));
+            return std::make_shared<ECondition>(simplify((*e)[0], options));
         } else if (auto a = std::dynamic_pointer_cast<ACondition>(formula); a != nullptr) {
-            return std::make_shared<ACondition>(simplify((*a)[0]));
+            return std::make_shared<ACondition>(simplify((*a)[0], options));
         }
-        auto[f, apinfo] = LTL::to_spot_formula(formula, compress);
-        spot::tl_simplifier simplifier{1};
+        auto[f, apinfo] = LTL::to_spot_formula(formula, options);
+        spot::tl_simplifier simplifier{static_cast<int>(options.buchiOptimization)};
         f = simplifier.simplify(f);
         // spot simplifies using unsupported operators R, W, and M, which we now remove.
         f = spot::unabbreviate(f, "RWM");

=== added directory 'src/LTL/Stubborn'
=== added file 'src/LTL/Stubborn/AutomatonStubbornSet.cpp'
--- src/LTL/Stubborn/AutomatonStubbornSet.cpp	1970-01-01 00:00:00 +0000
+++ src/LTL/Stubborn/AutomatonStubbornSet.cpp	2021-08-05 10:56:53 +0000
@@ -0,0 +1,355 @@
+/* Copyright (C) 2021  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#include "LTL/Structures/GuardInfo.h"
+#include "LTL/Stubborn/AutomatonStubbornSet.h"
+#include "LTL/Stubborn/EvalAndSetVisitor.h"
+#include "PetriEngine/Stubborn/InterestingTransitionVisitor.h"
+
+using namespace PetriEngine;
+using namespace PetriEngine::PQL;
+
+namespace LTL {
+    class NondeterministicConjunctionVisitor : public InterestingLTLTransitionVisitor {
+    public:
+        NondeterministicConjunctionVisitor(AutomatonStubbornSet &stubbornSet) :
+                InterestingLTLTransitionVisitor(stubbornSet, false),
+                _stubborn(stubbornSet), _net(stubbornSet._net) {}
+
+    protected:
+        static constexpr auto PresetBad = StubbornSet::PresetBad;
+        static constexpr auto PostsetBad = StubbornSet::PostsetBad;
+
+        void _accept(const PQL::CompareConjunction *element) override
+        {
+            if (_stubborn._track_changes || element->isNegated() != negated) {
+                InterestingLTLTransitionVisitor::_accept(element);
+                return;
+            }
+            _stubborn._track_changes = true;
+            memcpy(_stubborn._place_checkpoint.get(), _stubborn._places_seen.get(), _net.numberOfPlaces());
+            _accept_conjunction(element);
+            _stubborn._track_changes = false;
+            assert(_stubborn._pending_stubborn.empty());
+
+        }
+
+        void _accept_conjunction(const PQL::CompareConjunction *element)
+        {
+            assert(_stubborn._track_changes);
+            assert(_stubborn._pending_stubborn.empty());
+            assert(element->isNegated() == negated);
+            std::vector<std::pair<uint32_t, bool>> cands; // Transition id, Preset
+            for (auto &cons : *element) {
+                uint32_t tokens = _stubborn.getParent()[cons._place];
+
+                if (cons._lower == cons._upper) {
+                    //Compare is equality
+                    if (cons._lower == tokens) {
+                        continue;
+                    } else if (tokens < cons._lower) {
+                        // Valid candidate, explore preset
+                        cands.emplace_back(cons._place, true);
+                    } else {
+                        // Valid candidate, explore postset
+                        cands.emplace_back(cons._place, false);
+                    }
+                } else {
+                    if (tokens < cons._lower && cons._lower != 0) {
+                        // explore preset
+                        cands.emplace_back(cons._place, true);
+                    }
+
+                    if (tokens > cons._upper && cons._upper != std::numeric_limits<uint32_t>::max()) {
+                        // explore postset
+                        cands.emplace_back(cons._place, false);
+                    }
+                }
+
+                // explore cand if available
+                // if cand seen previously, return do not add additional (good case)
+                // else add cand to candidate list
+                auto &[cand, pre] = cands.back();
+                if (!cands.empty() && cand == cons._place) {
+                    assert(_stubborn._pending_stubborn.empty());
+                    if ((pre && _stubborn._places_seen[cand] & PresetBad) ||
+                        (!pre && _stubborn._places_seen[cand] & PostsetBad)) {
+                        cands.pop_back();
+                        continue;
+                    }
+                    // this constraint was a candidate previously, thus we are happy
+                    if ((pre && _stubborn.seenPre(cand)) || (!pre && _stubborn.seenPost(cand)))
+                        return;
+                }
+            }
+
+            // Run through candidate list and find first candidate not violating s-inv and add it to stub, then return.
+            for (size_t i = cands.size(); i > 0; --i) {
+                auto &[cand, pre] = cands[i - 1];
+                if (pre) {
+                    //explore pre
+                    assert(!(_stubborn._places_seen[cand] & PresetBad));
+                    _stubborn.presetOf(cand, false);
+                } else {
+                    //explore post
+                    assert(!(_stubborn._places_seen[cand] & PostsetBad));
+                    _stubborn.postsetOf(cand, false);
+                }
+
+                if (_stubborn._bad) {
+                    _stubborn._places_seen[cand] |= pre ? PresetBad : PostsetBad;
+#ifndef NDEBUG
+                    //std::cerr << "Bad pre/post and reset" << std::endl;
+#endif
+                    _stubborn._reset_pending();
+                    continue;
+                }
+
+                if (_stubborn._closure()) {
+                    // success, return this stubborn set
+                    _stubborn._apply_pending();
+                    return;
+                } else {
+#ifndef NDEBUG
+                    //std::cerr << "Bad closure and reset" << std::endl;
+#endif
+                    _stubborn._places_seen[cand] |= pre ? PresetBad : PostsetBad;
+                    _stubborn._reset_pending();
+                }
+            }
+
+            // If no candidate not violating s-inv set St=T.
+            _stubborn.set_all_stubborn();
+        }
+
+        const PetriEngine::PetriNet &_net;
+        AutomatonStubbornSet &_stubborn;
+
+    };
+
+    bool AutomatonStubbornSet::prepare(const LTL::Structures::ProductState *state)
+    {
+        reset();
+        _parent = state;
+        _gen.prepare(state);
+        memset(_places_seen.get(), 0, sizeof(uint8_t) * _net.numberOfPlaces());
+        constructEnabled();
+        if (_ordering.empty())
+            return false;
+        if (_ordering.size() == 1) {
+            _stubborn[_ordering.front()] = true;
+#ifndef NDEBUG
+            std::cerr << "Lone successor " << _net.transitionNames()[_ordering.front()] << std::endl;
+#endif
+            return true;
+        }
+
+
+        GuardInfo buchi_state = _state_guards[state->getBuchiState()];
+
+        PQL::EvaluationContext evaluationContext{_parent->marking(), &_net};
+
+        // Check if retarding is satisfied for condition 3.
+        _retarding_satisfied = _aut.guard_valid(evaluationContext, buchi_state.retarding.decision_diagram);
+        /*
+        if (!_aut.guard_valid(evaluationContext, buchi_state.retarding.decision_diagram)) {
+            set_all_stubborn();
+            __print_debug();
+            return true;
+        }*/
+
+        // Calculate retarding subborn set to ensure S-INV.
+        auto negated_retarding = std::make_unique<NotCondition>(buchi_state.retarding.condition);
+        _retarding_stubborn_set.setQuery(negated_retarding.get());
+        _retarding_stubborn_set.prepare(state);
+
+
+        _nenabled = _ordering.size();
+
+        // If a progressing formula satisfies the guard St=T is the only way to ensure NLG.
+        for (auto &q : buchi_state.progressing) {
+            if (_aut.guard_valid(evaluationContext, q.decision_diagram)) {
+                set_all_stubborn();
+                __print_debug();
+                return true;
+            }
+        }
+
+        //Interesting on each progressing formula gives NLG.
+        for (auto &q : buchi_state.progressing) {
+            EvalAndSetVisitor evalAndSetVisitor{evaluationContext};
+            q.condition->visit(evalAndSetVisitor);
+
+            NondeterministicConjunctionVisitor interesting{*this};
+            q.condition->visit(interesting);
+            if (_done) return true;
+            else {
+                assert(!_track_changes);
+                assert(_pending_stubborn.empty());
+                // Closure to ensure COM.
+                _closure();
+                if (_bad) {
+                    set_all_stubborn();
+                    return true;
+                }
+            }
+        }
+
+        assert(_unprocessed.empty());
+        assert(_pending_stubborn.empty());
+        assert(!_bad);
+        assert(!_done);
+
+
+
+        /*//Check that S-INV is satisfied
+        if (has_shared_mark(_stubborn.get(), _retarding_stubborn_set.stubborn(), _net.numberOfTransitions())) {
+            memset(_stubborn.get(), true, sizeof(bool) * _net.numberOfTransitions());
+            //return true;
+        }*/
+
+        // Ensure we have a key transition in accepting buchi states.
+        if (!_has_enabled_stubborn && buchi_state.is_accepting) {
+            for (uint32_t i = 0; i < _net.numberOfTransitions(); ++i) {
+                if (!_stubborn[i] && _enabled[i]) {
+                    addToStub(i);
+                    _closure();
+                    if (_bad) {
+                        set_all_stubborn();
+                        return true;
+                    }
+                    break;
+                }
+            }
+        }
+
+        assert(!has_shared_mark(_stubborn.get(), _retarding_stubborn_set.stubborn(), _net.numberOfTransitions()));
+
+        __print_debug();
+
+        return true;
+    }
+
+
+    uint32_t AutomatonStubbornSet::next()
+    {
+        while (!_ordering.empty()) {
+            _current = _ordering.front();
+            _ordering.pop_front();
+            if (_stubborn[_current] && _enabled[_current]) {
+                return _current;
+            }
+        }
+        reset();
+        return std::numeric_limits<uint32_t>::max();
+    }
+
+    void AutomatonStubbornSet::__print_debug()
+    {
+#ifndef NDEBUG
+        return;
+        std::cout << "Enabled: ";
+        for (int i = 0; i < _net.numberOfTransitions(); ++i) {
+            if (_enabled[i]) {
+                std::cout << _net.transitionNames()[i] << ' ';
+            }
+        }
+        std::cout << "\nStubborn: ";
+        for (int i = 0; i < _net.numberOfTransitions(); ++i) {
+            if (_stubborn[i]) {
+                std::cout << _net.transitionNames()[i] << ' ';
+            }
+        }
+        std::cout << std::endl;
+#endif
+    }
+
+    void AutomatonStubbornSet::reset()
+    {
+        StubbornSet::reset();
+        memset(_place_checkpoint.get(), 0, _net.numberOfPlaces());
+        _retarding_stubborn_set.reset();
+        _has_enabled_stubborn = false;
+        _bad = false;
+        _done = false;
+        _track_changes = false;
+        _pending_stubborn.clear();
+        _unprocessed.clear();
+    }
+
+    void AutomatonStubbornSet::addToStub(uint32_t t)
+    {
+        if (_retarding_stubborn_set.stubborn()[t] || !_cond3_valid(t)) {
+            _bad = true;
+            return;
+        }
+        if (_track_changes) {
+            if (_enabled[t])
+                _has_enabled_stubborn = true;
+            if (_pending_stubborn.insert(t).second) {
+                _unprocessed.push_back(t);
+            }
+        } else {
+            StubbornSet::addToStub(t);
+        }
+    }
+
+    bool AutomatonStubbornSet::_cond3_valid(uint32_t t)
+    {
+        EvaluationContext ctx{_markbuf.marking(), &_net};
+        if (_retarding_satisfied || !_enabled[t]) return true;
+        else {
+            assert(_gen.checkPreset(t));
+            assert(dynamic_cast<const LTL::Structures::ProductState *>(_parent) != nullptr);
+            memcpy(_markbuf.marking(), (*_parent).marking(), _net.numberOfPlaces() * sizeof(MarkVal));
+            _gen.consumePreset(_markbuf, t);
+            _gen.producePostset(_markbuf, t);
+            return _aut.guard_valid(ctx,
+                                    _state_guards[static_cast<const LTL::Structures::ProductState *>(_parent)->getBuchiState()].retarding.decision_diagram);
+        }
+    }
+
+    void AutomatonStubbornSet::_reset_pending()
+    {
+        _bad = false;
+        _pending_stubborn.clear();
+        _unprocessed.clear();
+        memcpy(_places_seen.get(), _place_checkpoint.get(), _net.numberOfPlaces());
+    }
+
+    void AutomatonStubbornSet::_apply_pending()
+    {
+        assert(!_bad);
+        for (auto t : _pending_stubborn) {
+            _stubborn[t] = true;
+        }
+        _pending_stubborn.clear();
+        assert(_unprocessed.empty());
+    }
+
+    void AutomatonStubbornSet::set_all_stubborn()
+    {
+        memset(_stubborn.get(), true, sizeof(bool) * _net.numberOfTransitions());
+        _done = true;
+    }
+
+    bool AutomatonStubbornSet::_closure()
+    {
+        StubbornSet::closure([&]() { return !_bad; });
+        return !_bad;
+    }
+}

=== added file 'src/LTL/Stubborn/CMakeLists.txt'
--- src/LTL/Stubborn/CMakeLists.txt	1970-01-01 00:00:00 +0000
+++ src/LTL/Stubborn/CMakeLists.txt	2021-08-05 10:56:53 +0000
@@ -0,0 +1,4 @@
+set(CMAKE_INCLUDE_CURRENT_DIR ON)
+
+add_library(LTLStubborn EvalAndSetVisitor.cpp VisibleTransitionVisitor.cpp VisibleLTLStubbornSet.cpp AutomatonStubbornSet.cpp SafeAutStubbornSet.cpp)
+add_dependencies(LTLStubborn PetriEngine)

=== added file 'src/LTL/Stubborn/EvalAndSetVisitor.cpp'
--- src/LTL/Stubborn/EvalAndSetVisitor.cpp	1970-01-01 00:00:00 +0000
+++ src/LTL/Stubborn/EvalAndSetVisitor.cpp	2021-08-05 10:56:53 +0000
@@ -0,0 +1,126 @@
+/* Copyright (C) 2021  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ * 
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ * 
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ * 
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#include "LTL/Stubborn/EvalAndSetVisitor.h"
+
+namespace LTL {
+
+    using namespace PetriEngine::PQL;
+
+    void EvalAndSetVisitor::_accept(PetriEngine::PQL::ACondition *condition) {
+        condition->getCond()->visit(*this);
+    }
+
+    void EvalAndSetVisitor::_accept(PetriEngine::PQL::ECondition *condition) {
+        condition->getCond()->visit(*this);
+    }
+
+    void EvalAndSetVisitor::_accept(PetriEngine::PQL::XCondition *condition) {
+        condition->getCond()->visit(*this);
+    }
+
+    void EvalAndSetVisitor::_accept(PetriEngine::PQL::GCondition *condition) {
+        condition->getCond()->visit(*this);
+        auto res = condition->getCond()->getSatisfied();
+        if (res != Condition::RFALSE) res = Condition::RUNKNOWN;
+        condition->setSatisfied(res);
+    }
+
+    void EvalAndSetVisitor::_accept(PetriEngine::PQL::FCondition *condition) {
+        condition->getCond()->visit(*this);
+        auto res = condition->getCond()->getSatisfied();
+        if (res != Condition::RTRUE) res = Condition::RUNKNOWN;
+        condition->setSatisfied(res);
+    }
+
+    void EvalAndSetVisitor::_accept(PetriEngine::PQL::UntilCondition *condition) {
+        condition->getCond1()->visit(*this);
+        condition->getCond2()->visit(*this);
+        auto r2 = condition->getCond2()->getSatisfied();
+        if (r2 != Condition::RFALSE) {
+            condition->setSatisfied(r2);
+            return;
+        }
+        auto r1 = condition->getCond1()->getSatisfied();
+        if (r1 == Condition::RFALSE) {
+            condition->setSatisfied(Condition::RFALSE);
+            return;
+        }
+        condition->setSatisfied(Condition::RUNKNOWN);
+    }
+
+    void EvalAndSetVisitor::_accept(NotCondition *element) {
+        element->getCond()->visit(*this);
+        auto res = element->getCond()->getSatisfied();
+        if (res != Condition::RUNKNOWN) res = res == Condition::RFALSE ? Condition::RTRUE : Condition::RFALSE;
+        element->setSatisfied(res);
+    }
+
+    void EvalAndSetVisitor::_accept(AndCondition *element) {
+        auto res = Condition::RTRUE;
+        for (auto &c : *element) {
+            c->visit(*this);
+            auto r = c->getSatisfied();
+            if (r == Condition::RFALSE) res = Condition::RFALSE;
+            else if (r == Condition::RUNKNOWN && res != Condition::RFALSE) res = Condition::RUNKNOWN;
+        }
+        element->setSatisfied(res);
+    }
+
+    void EvalAndSetVisitor::_accept(OrCondition *element) {
+        auto res = Condition::RFALSE;
+        for (auto &c : *element) {
+            c->visit(*this);
+            auto r = c->getSatisfied();
+            if (r == Condition::RTRUE) res = Condition::RTRUE;
+            else if (r == Condition::RUNKNOWN && res != Condition::RTRUE) res = Condition::RUNKNOWN;
+        }
+        element->setSatisfied(res);
+    }
+
+    void EvalAndSetVisitor::_accept(LessThanCondition *element) {
+        element->evalAndSet(_context);
+    }
+
+    void EvalAndSetVisitor::_accept(LessThanOrEqualCondition *element) {
+        element->evalAndSet(_context);
+    }
+
+    void EvalAndSetVisitor::_accept(EqualCondition *element) {
+        element->evalAndSet(_context);
+    }
+
+    void EvalAndSetVisitor::_accept(NotEqualCondition *element) {
+        element->evalAndSet(_context);
+    }
+
+    void EvalAndSetVisitor::_accept(DeadlockCondition *element) {
+        element->evalAndSet(_context);
+    }
+
+    void EvalAndSetVisitor::_accept(CompareConjunction *element) {
+        element->evalAndSet(_context);
+    }
+
+    void EvalAndSetVisitor::_accept(UnfoldedUpperBoundsCondition *element) {
+        element->evalAndSet(_context);
+    }
+
+    void EvalAndSetVisitor::_accept(BooleanCondition *element) {
+        element->evalAndSet(_context);
+    }
+}

=== added file 'src/LTL/Stubborn/SafeAutStubbornSet.cpp'
--- src/LTL/Stubborn/SafeAutStubbornSet.cpp	1970-01-01 00:00:00 +0000
+++ src/LTL/Stubborn/SafeAutStubbornSet.cpp	2021-08-05 10:56:53 +0000
@@ -0,0 +1,64 @@
+/* Copyright (C) 2021  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ * 
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ * 
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ * 
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#include "LTL/Stubborn/SafeAutStubbornSet.h"
+
+namespace LTL {
+    using namespace PetriEngine;
+
+    bool SafeAutStubbornSet::prepare(const LTL::Structures::ProductState *state)
+    {
+        reset();
+        _parent = state;
+        memset(_places_seen.get(), 0, _net.numberOfPlaces());
+
+        constructEnabled();
+        if (_ordering.empty()) {
+            return false;
+        }
+        if (_ordering.size() == 1) {
+            _stubborn[_ordering.front()] = true;
+            return true;
+        }
+
+        InterestingTransitionVisitor interesting{*this, false};
+
+        for (auto &q : _queries) {
+            q->evalAndSet(PQL::EvaluationContext((*_parent).marking(), &_net));
+            q->visit(interesting);
+        }
+        assert(!_bad);
+
+        _unsafe.swap(_stubborn);
+        //memset(_stubborn.get(), false, sizeof(bool) * _net.numberOfTransitions());
+        _unprocessed.clear();
+        memset(_places_seen.get(), 0, _net.numberOfPlaces());
+
+        assert(_unprocessed.empty());
+
+        for (auto &q : _queries) {
+            q->visit(interesting);
+            closure();
+            if (_bad) {
+                // abort
+                set_all_stubborn();
+                return true;
+            }
+        }
+        return true;
+    }
+}
\ No newline at end of file

=== added file 'src/LTL/Stubborn/VisibleLTLStubbornSet.cpp'
--- src/LTL/Stubborn/VisibleLTLStubbornSet.cpp	1970-01-01 00:00:00 +0000
+++ src/LTL/Stubborn/VisibleLTLStubbornSet.cpp	2021-08-05 10:56:53 +0000
@@ -0,0 +1,176 @@
+/* Copyright (C) 2021  Nikolaj J. Ulrik <[e-mail]>,
+ *                     Simon M. Virenfeldt <[e-mail]>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#include "PetriEngine/Stubborn/InterestingTransitionVisitor.h"
+#include "LTL/Stubborn/VisibleLTLStubbornSet.h"
+#include "LTL/Stubborn/EvalAndSetVisitor.h"
+
+using namespace PetriEngine;
+using namespace PetriEngine::PQL;
+
+namespace LTL {
+    bool VisibleLTLStubbornSet::prepare(const PetriEngine::Structures::State *marking) {
+        reset();
+        _parent = marking;
+        PQL::EvaluationContext evaluationContext{_parent->marking(), &_net};
+        memset(_places_seen.get(), 0, _net.numberOfPlaces());
+        constructEnabled();
+        if (_ordering.empty()) return false;
+        if (_ordering.size() == 1) {
+            _stubborn[_ordering.front()] = true;
+            return true;
+        }
+        //TODO needed? We do not run Interesting visitor so we do not immediately need it, but is is needed by closure?
+        for (auto &q : _queries) {
+            EvalAndSetVisitor evalAndSetVisitor{evaluationContext};
+            q->visit(evalAndSetVisitor);
+        }
+        findKeyTransition();
+
+        ensureRuleV();
+
+        ensureRulesL();
+
+        _nenabled = _ordering.size();
+
+
+        if (!_has_enabled_stubborn) {
+            memset(_stubborn.get(), 1, _net.numberOfTransitions());
+        }
+#ifdef STUBBORN_STATISTICS
+        float num_stubborn = 0;
+        float num_enabled = 0;
+        float num_enabled_stubborn = 0;
+        for (int i = 0; i < _net.numberOfTransitions(); ++i) {
+            if (_stubborn[i]) ++num_stubborn;
+            if (_fallback_spooler[i]) ++num_enabled;
+            if (_stubborn[i] && _fallback_spooler[i]) ++num_enabled_stubborn;
+        }
+        std::cerr << "Enabled: " << num_enabled << "/" << _net.numberOfTransitions() << " (" << num_enabled/_net.numberOfTransitions()*100.0 << "%),\t\t "
+                  << "Stubborn: " << num_stubborn << "/" << _net.numberOfTransitions() << " (" << num_stubborn/_net.numberOfTransitions()*100.0 << "%),\t\t "
+                  << "Enabled stubborn: " << num_enabled_stubborn << "/" << num_enabled << " (" << num_enabled_stubborn/num_enabled*100.0 << "%)" << std::endl;
+#endif
+        return true;
+    }
+
+    uint32_t VisibleLTLStubbornSet::next() {
+        while (!_ordering.empty()) {
+            _current = _ordering.front();
+            _ordering.pop_front();
+            if (_stubborn[_current] && _enabled[_current]) {
+                return _current;
+            }
+            else {
+                _skipped.push_back(_current);
+            }
+        }
+        reset();
+        return std::numeric_limits<uint32_t>::max();
+    }
+
+    void VisibleLTLStubbornSet::findKeyTransition() {
+        // try to find invisible key transition first
+        assert(!_ordering.empty());
+        auto tkey = _ordering.front();
+        if (_visible[tkey]) {
+            for (uint32_t tid = 0; tid < _net.numberOfTransitions(); ++tid) {
+                if (_enabled[tid] && !_visible[tid]) {
+                    tkey = tid;
+                    break;
+                }
+            }
+        }
+        addToStub(tkey);
+
+        // include relevant transitions
+        auto ptr = transitions()[tkey];
+        uint32_t finv = ptr.inputs;
+        uint32_t linv = ptr.outputs;
+
+        for (; finv < linv; ++finv) {
+            auto inv = invariants()[finv];
+            postsetOf(inv.place, true);
+        }
+    }
+