Merge lp:~tapaal-contributor/tapaal/cpn-tapn into lp:~tapaal-contributor/tapaal/cpn-gui-dev

[Kenneth Yrke Jørgensen]

Needs new version of verifytapn from https://github.com/TAPAAL/verifytapn/pull/14

[Jiri Srba (srba)]

Tested and works. Engine is also merged to trunk now.

review: Approve

=== modified file 'src/dk/aau/cs/verification/QueryResult.java'
--- src/dk/aau/cs/verification/QueryResult.java	2022-01-09 16:46:17 +0000
+++ src/dk/aau/cs/verification/QueryResult.java	2022-02-07 08:12:13 +0000
@@ -10,6 +10,43 @@
 	private final TAPNQuery query;
 	private final BoundednessAnalysisResult boundednessAnalysis;
 
+    public boolean isSolvedUsingQuerySimplification() {
+        return solvedUsingQuerySimplification;
+    }
+
+    public void setSolvedUsingQuerySimplification(boolean solvedUsingQuerySimplification) {
+        this.solvedUsingQuerySimplification = solvedUsingQuerySimplification;
+    }
+
+    public boolean isSolvedUsingTraceAbstractRefinement() {
+        return solvedUsingTraceAbstractRefinement;
+    }
+
+    public void setSolvedUsingTraceAbstractRefinement(boolean solvedUsingTraceAbstractRefinement) {
+        this.solvedUsingTraceAbstractRefinement = solvedUsingTraceAbstractRefinement;
+    }
+
+    public boolean isSolvedUsingStateEquation() {
+        return solvedUsingStateEquation;
+    }
+
+    public void setSolvedUsingStateEquation(boolean solvedUsingStateEquation) {
+        this.solvedUsingStateEquation = solvedUsingStateEquation;
+    }
+
+    public boolean isSolvedUsingSiphonTrap() {
+        return solvedUsingSiphonTrap;
+    }
+
+    public void setSolvedUsingSiphonTrap(boolean solvedUsingSiphonTrap) {
+        this.solvedUsingSiphonTrap = solvedUsingSiphonTrap;
+    }
+
+    private boolean solvedUsingQuerySimplification;
+    private boolean solvedUsingTraceAbstractRefinement;
+    private boolean solvedUsingStateEquation;
+    private boolean solvedUsingSiphonTrap;
+
 	public boolean isCTL = false;
 	public QueryResult(boolean satisfied, BoundednessAnalysisResult boundednessAnalysis, TAPNQuery query, boolean discreteInclusion){
 		this.satisfied = satisfied;

=== modified file 'src/dk/aau/cs/verification/VerificationResult.java'
--- src/dk/aau/cs/verification/VerificationResult.java	2021-12-09 19:54:26 +0000
+++ src/dk/aau/cs/verification/VerificationResult.java	2022-02-07 08:12:13 +0000
@@ -18,10 +18,27 @@
 	private Stats stats;
 	private NameMapping nameMapping;
 	private TTrace secondaryTrace;
-	private boolean isSolvedUsingStateEquation = false;
+
 	private Tuple<TimedArcPetriNet, NameMapping> unfoldedModel;
-	
-	public boolean isQuerySatisfied() {
+    private boolean resolvedUsingSkeletonPreprocessor = false;
+
+    public boolean isSolvedUsingQuerySimplification() {
+        return queryResult.isSolvedUsingQuerySimplification();
+    }
+
+    public boolean isSolvedUsingTraceAbstractRefinement() {
+        return queryResult.isSolvedUsingTraceAbstractRefinement();
+    }
+
+    public boolean isSolvedUsingStateEquation() {
+        return queryResult.isSolvedUsingStateEquation();
+    }
+
+    public boolean isSolvedUsingSiphonTrap() {
+        return queryResult.isSolvedUsingSiphonTrap();
+    }
+
+    public boolean isQuerySatisfied() {
 		return queryResult.isQuerySatisfied();
 	}
 
@@ -32,15 +49,10 @@
 		this.stats = stats;
 		this.rawOutput = rawOutput;
 	}
-
-    public VerificationResult(QueryResult queryResult, TTrace trace, long verificationTime, Stats stats, boolean isSolvedUsingStateEquation){
-        this(queryResult, trace, verificationTime, stats, null);
-        this.isSolvedUsingStateEquation = isSolvedUsingStateEquation;
-    }
 	
 	public VerificationResult(QueryResult queryResult, TTrace trace, long verificationTime, Stats stats, boolean isSolvedUsingStateEquation, String rawOutput, Tuple<TimedArcPetriNet, NameMapping> unfoldedModel){
 		this(queryResult, trace, verificationTime, stats, rawOutput);
-		this.isSolvedUsingStateEquation = isSolvedUsingStateEquation;
+		//this.solvedUsingStateEquation = isSolvedUsingStateEquation; // This was the old value using for both state equation and untimed skeleton check
 		this.unfoldedModel = unfoldedModel;
 	}
 
@@ -111,8 +123,15 @@
 		returnList.sort(new transitionTupleComparator());
 		return returnList;
 	}
-	
-	public static class transitionTupleComparator implements Comparator<Tuple<String,Integer>> {
+
+    public boolean isResolvedUsingSkeletonPreprocessor() {
+        return resolvedUsingSkeletonPreprocessor;
+    }
+    public boolean setResolvedUsingSkeletonAnalysisPreprocessor(boolean b) {
+        return this.resolvedUsingSkeletonPreprocessor = b;
+    }
+
+    public static class transitionTupleComparator implements Comparator<Tuple<String,Integer>> {
 		
 		public int compare(Tuple<String,Integer> tuple1,Tuple<String,Integer> tuple2) {
             return tuple2.value2() - tuple1.value2();
@@ -210,10 +229,6 @@
 		return m;
 	}
 	
-	public boolean isSolvedUsingStateEquation(){
-		return isSolvedUsingStateEquation;
-	}
-	
 	public void addTime(long timeToAdd) {
 		verificationTime += timeToAdd;
 	}

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java	2022-01-28 09:46:10 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java	2022-02-07 08:12:13 +0000
@@ -5,14 +5,33 @@
 import dk.aau.cs.TCTL.TCTLAGNode;
 import dk.aau.cs.TCTL.TCTLEFNode;
 import dk.aau.cs.TCTL.TCTLEGNode;
-import pipe.gui.petrinet.PetriNetTab;
 import dk.aau.cs.io.LoadedModel;
 import dk.aau.cs.io.TapnEngineXmlLoader;
-import dk.aau.cs.model.tapn.*;
+import dk.aau.cs.model.tapn.LocalTimedPlace;
+import dk.aau.cs.model.tapn.TAPNQuery;
+import dk.aau.cs.model.tapn.TimedArcPetriNet;
+import dk.aau.cs.model.tapn.TimedPlace;
 import dk.aau.cs.model.tapn.simulation.TimedArcPetriNetTrace;
-import dk.aau.cs.util.*;
+import dk.aau.cs.util.FormatException;
+import dk.aau.cs.util.Tuple;
+import dk.aau.cs.util.UnsupportedModelException;
+import dk.aau.cs.util.UnsupportedQueryException;
 import dk.aau.cs.verification.*;
+import net.tapaal.Preferences;
+import net.tapaal.TAPAAL;
+import net.tapaal.gui.petrinet.verification.InclusionPlaces;
+import net.tapaal.gui.petrinet.verification.InclusionPlaces.InclusionPlacesOption;
+import net.tapaal.gui.petrinet.verification.TAPNQuery.TraceOption;
+import net.tapaal.gui.petrinet.verification.TAPNQuery.WorkflowMode;
+import net.tapaal.gui.petrinet.verification.UnfoldNet;
+import pipe.gui.Constants;
+import pipe.gui.FileFinder;
+import pipe.gui.MessengerImpl;
+import pipe.gui.TAPAALGUI;
+import pipe.gui.petrinet.PetriNetTab;
+import pipe.gui.petrinet.dataLayer.DataLayer;
 
+import javax.swing.*;
 import java.io.BufferedReader;
 import java.io.File;
 import java.io.IOException;
@@ -20,18 +39,6 @@
 import java.util.ArrayList;
 import java.util.List;
 
-import net.tapaal.Preferences;
-import net.tapaal.TAPAAL;
-import pipe.gui.petrinet.dataLayer.DataLayer;
-import net.tapaal.gui.petrinet.verification.TAPNQuery.TraceOption;
-import net.tapaal.gui.petrinet.verification.TAPNQuery.WorkflowMode;
-import pipe.gui.*;
-import net.tapaal.gui.petrinet.verification.UnfoldNet;
-import net.tapaal.gui.petrinet.verification.InclusionPlaces;
-import net.tapaal.gui.petrinet.verification.InclusionPlaces.InclusionPlacesOption;
-
-import javax.swing.*;
-
 public class VerifyDTAPN implements ModelChecker{
 
 	private static final String NEED_TO_LOCATE_VERIFYDTAPN_MSG = "TAPAAL needs to know the location of the file verifydtapn.\n\n"
@@ -274,9 +281,13 @@
 
                 TimedArcPetriNetTrace tapnTrace = null;
 
-
                 boolean isColored = (lens != null && lens.isColored() || model.value1().parentNetwork().isColored());
-                if(options.traceOption() != TraceOption.NONE && isColored && queryResult != null && queryResult.value1() != null && queryResult.value1().isQuerySatisfied()) {
+                boolean showTrace = ((query.getProperty() instanceof TCTLEFNode && queryResult.value1().isQuerySatisfied()) ||
+                    (query.getProperty() instanceof TCTLAGNode && !queryResult.value1().isQuerySatisfied()) ||
+                    (query.getProperty() instanceof TCTLEGNode && queryResult.value1().isQuerySatisfied()) ||
+                    (query.getProperty() instanceof TCTLAFNode && !queryResult.value1().isQuerySatisfied()));
+
+                if(options.traceOption() != TraceOption.NONE && isColored && showTrace) {
                     TapnEngineXmlLoader tapnLoader = new TapnEngineXmlLoader();
                     File fileOut = new File(options.unfoldedModelPath());
                     File queriesOut = new File(options.unfoldedQueriesPath());
@@ -291,11 +302,7 @@
                             tapnTrace = parseTrace(!errorOutput.contains("Trace:") ? errorOutput : (errorOutput.split("Trace:")[1]), options, model, exportedModel, query, queryResult.value1());
                         }
 
-                        if(tapnTrace == null){
-                            String message = "No trace could be generated.\n\n";
-                            message += "Model checker output:\n" + standardOutput;
-                            messenger.displayWrappedErrorMessage(message,"No trace found");
-                        } else {
+                        if (tapnTrace != null) {
                             int dialogResult = JOptionPane.showConfirmDialog(null, "There is a trace that will be displayed in a new tab on the unfolded net/query.", "Open trace", JOptionPane.OK_CANCEL_OPTION);
                             if (dialogResult == JOptionPane.OK_OPTION) {
                                 newTab = new PetriNetTab(loadedModel.network(), loadedModel.templates(), loadedModel.queries(), new PetriNetTab.TAPNLens(TAPAALGUI.getCurrentTab().getLens().isTimed(), TAPAALGUI.getCurrentTab().getLens().isGame(), false));
@@ -312,6 +319,7 @@
                                 options.setTraceOption(TraceOption.NONE);
                             }
                         }
+
                     } catch (FormatException e) {
                         e.printStackTrace();
                         return null;
@@ -352,8 +360,6 @@
 						(query.getProperty() instanceof TCTLEGNode && !queryResult.isQuerySatisfied()) ||
 						(query.getProperty() instanceof TCTLAFNode && queryResult.isQuerySatisfied())) {
 					return null;
-				} else {
-					messenger.displayErrorMessage("Verifydtapn cannot generate the requested trace for the model. Try another trace option.");
 				}
 			}
 		}

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java	2022-01-28 12:27:29 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java	2022-02-07 08:12:13 +0000
@@ -287,50 +287,55 @@
 
             Tuple<QueryResult, Stats> queryResult = parseQueryResult(standardOutput, model.value1().marking().size() + query.getExtraTokens(), query.getExtraTokens(), query);
 
-            boolean isColored = (lens != null && lens.isColored() || model.value1().parentNetwork().isColored());
-            if (options.traceOption() != TraceOption.NONE && isColored && queryResult != null && queryResult.value1() != null && queryResult.value1().isQuerySatisfied()) {
-                PNMLoader tapnLoader = new PNMLoader();
-                File fileOut = new File(options.unfoldedModelPath());
-                File queriesOut = new File(options.unfoldedQueriesPath());
-                PetriNetTab newTab;
-                LoadedModel loadedModel = null;
-                try {
-                    loadedModel = tapnLoader.load(fileOut);
-                    TAPNComposer newComposer = new TAPNComposer(new MessengerImpl(), true);
-                    model = newComposer.transformModel(loadedModel.network());
-
-                    if (queryResult != null && queryResult.value1() != null) {
-                        tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1(), true);
-                    }
-
-                    if (!(tapnTrace == null)) {
-                        int dialogResult = JOptionPane.showConfirmDialog(null, "There is a trace that will be displayed in a new tab on the unfolded net/query.", "Open trace", JOptionPane.OK_CANCEL_OPTION);
-                        if (dialogResult == JOptionPane.OK_OPTION) {
-                            newTab = new PetriNetTab(loadedModel.network(), loadedModel.templates(), loadedModel.queries(), new PetriNetTab.TAPNLens(TAPAALGUI.getCurrentTab().getLens().isTimed(), TAPAALGUI.getCurrentTab().getLens().isGame(), false));
-
-                            //The query being verified should be the only query
-                            for (net.tapaal.gui.petrinet.verification.TAPNQuery loadedQuery : UnfoldNet.getQueries(queriesOut, loadedModel.network())) {
-                                newTab.setInitialName(loadedQuery.getName() + " - unfolded");
-                                loadedQuery.copyOptions(dataLayerQuery);
-                                newTab.addQuery(loadedQuery);
-                            }
-                            TAPAALGUI.openNewTabFromStream(newTab);
-                        } else {
-                            options.setTraceOption(TraceOption.NONE);
-                        }
-                    }
-                } catch (FormatException e) {
-                    e.printStackTrace();
-                } catch (ThreadDeath d) {
-                    return null;
-                }
-            }
-
             if (queryResult == null || queryResult.value1() == null) {
                 return new VerificationResult<TimedArcPetriNetTrace>(errorOutput + System.getProperty("line.separator") + standardOutput, runner.getRunningTime());
             } else {
+
+                boolean isColored = (lens != null && lens.isColored() || model.value1().parentNetwork().isColored());
+                boolean showTrace = ((query.getProperty() instanceof TCTLEFNode && queryResult.value1().isQuerySatisfied()) ||
+                    (query.getProperty() instanceof TCTLAGNode && !queryResult.value1().isQuerySatisfied()) ||
+                    (query.getProperty() instanceof TCTLEGNode && queryResult.value1().isQuerySatisfied()) ||
+                    (query.getProperty() instanceof TCTLAFNode && !queryResult.value1().isQuerySatisfied()));
+
+                if (options.traceOption() != TraceOption.NONE && isColored && showTrace) {
+                    PNMLoader tapnLoader = new PNMLoader();
+                    File fileOut = new File(options.unfoldedModelPath());
+                    File queriesOut = new File(options.unfoldedQueriesPath());
+                    PetriNetTab newTab;
+                    LoadedModel loadedModel = null;
+                    try {
+                        loadedModel = tapnLoader.load(fileOut);
+                        TAPNComposer newComposer = new TAPNComposer(new MessengerImpl(), true);
+                        model = newComposer.transformModel(loadedModel.network());
+
+                        if (queryResult != null && queryResult.value1() != null) {
+                            tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1());
+                        }
+
+                        if (!(tapnTrace == null)) {
+                            int dialogResult = JOptionPane.showConfirmDialog(null, "There is a trace that will be displayed in a new tab on the unfolded net/query.", "Open trace", JOptionPane.OK_CANCEL_OPTION);
+                            if (dialogResult == JOptionPane.OK_OPTION) {
+                                newTab = new PetriNetTab(loadedModel.network(), loadedModel.templates(), loadedModel.queries(), new PetriNetTab.TAPNLens(TAPAALGUI.getCurrentTab().getLens().isTimed(), TAPAALGUI.getCurrentTab().getLens().isGame(), false));
+
+                                //The query being verified should be the only query
+                                for (net.tapaal.gui.petrinet.verification.TAPNQuery loadedQuery : UnfoldNet.getQueries(queriesOut, loadedModel.network())) {
+                                    newTab.setInitialName(loadedQuery.getName() + " - unfolded");
+                                    loadedQuery.copyOptions(dataLayerQuery);
+                                    newTab.addQuery(loadedQuery);
+                                }
+                                TAPAALGUI.openNewTabFromStream(newTab);
+                            } else {
+                                options.setTraceOption(TraceOption.NONE);
+                            }
+                        }
+                    } catch (FormatException e) {
+                        e.printStackTrace();
+                    } catch (ThreadDeath d) {
+                        return null;
+                    }
+                }
+
                 ctlOutput = queryResult.value1().isCTL;
-                boolean approximationResult = queryResult.value2().discoveredStates() == 0;    // Result is from over-approximation
 
                 if (tapnTrace == null) {
                     if (!errorOutput.contains("Trace") && standardOutput.contains("<trace>")) {
@@ -342,17 +347,16 @@
                         tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1());
                     }
                 }
-                return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, runner.getRunningTime(), queryResult.value2(), approximationResult, standardOutput, model);
+                var result = new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, runner.getRunningTime(), queryResult.value2(), false, standardOutput, model);
+                if (queryResult.value1().isSolvedUsingStateEquation()) {
+
+                }
+                return result;
             }
         }
     }
 
     private TimedArcPetriNetTrace parseTrace(String output, VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, ExportedVerifyTAPNModel exportedModel, TAPNQuery query, QueryResult queryResult) {
-        return parseTrace(output, options, model, exportedModel, query, queryResult, false);
-    }
-    //XXX: this noWarning thinks is a huge hack to avoid warning shown twice for color nets, the warning should not be shown
-    // in this methods in the first case
-    private TimedArcPetriNetTrace parseTrace(String output, VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, ExportedVerifyTAPNModel exportedModel, TAPNQuery query, QueryResult queryResult, boolean noWarning) {
         if (((VerifyTAPNOptions) options).trace() == TraceOption.NONE) return null;
 
         VerifyTAPNTraceParser traceParser = new VerifyTAPNTraceParser(model.value1());
@@ -367,11 +371,6 @@
                     (query.getProperty() instanceof TCTLEGNode && !queryResult.isQuerySatisfied()) ||
                     (query.getProperty() instanceof TCTLAFNode && queryResult.isQuerySatisfied())) {
                     return null;
-                } else {
-                    if (!noWarning) {
-                        String message = "No trace could be generated.\n\n";
-                        messenger.displayWrappedErrorMessage(message, "No trace found");
-                    }
                 }
             }
         }

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPNCTLOutputParser.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPNCTLOutputParser.java	2020-07-13 14:30:00 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPNCTLOutputParser.java	2022-02-07 08:12:13 +0000
@@ -48,6 +48,8 @@
                     result = false;
                     foundResult = true;
                 } else {
+                    parseSolvedMethod(line);
+
                     Matcher matcher = configurationsPattern.matcher(line);
                     if (matcher.find()) {
                         configurtations = Long.parseLong(matcher.group(1));
@@ -86,7 +88,13 @@
 			if(!foundResult) return null;
 
             BoundednessAnalysisResult boundedAnalysis = new BoundednessAnalysisResult(totalTokens, maxUsedTokens, extraTokens);
-            return new Tuple<QueryResult, Stats>(new QueryResult(result, boundedAnalysis, query, false), new Stats(configurtations, markings, edges, processedEdges, processedNEdges, exploredConfigurations));
+            var qr = new QueryResult(result, boundedAnalysis, query, false);
+            qr.setSolvedUsingQuerySimplification(solvedUsingQuerySimplification);
+            qr.setSolvedUsingStateEquation(solvedUsingStateEquation);
+            qr.setSolvedUsingTraceAbstractRefinement(solvedUsingTraceAbstractRefinement);
+            qr.setSolvedUsingSiphonTrap(solvedUsingSiphonTrap);
+
+            return new Tuple<QueryResult, Stats>(qr, new Stats(configurtations, markings, edges, processedEdges, processedNEdges, exploredConfigurations));
 		} catch (Exception e) {
 			e.printStackTrace();
 		}

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOutputParser.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOutputParser.java	2020-07-13 14:30:00 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOutputParser.java	2022-02-07 08:12:13 +0000
@@ -90,6 +90,8 @@
 					result = false;
 					foundResult = true;
 				} else {
+                    parseSolvedMethod(line);
+
 					matcher = discoveredPattern.matcher(line);
 					if(matcher.find()){
 						discovered = Integer.parseInt(matcher.group(1));
@@ -172,7 +174,13 @@
 			if(!foundResult) return null;
 			BoundednessAnalysisResult boundedAnalysis = new BoundednessAnalysisResult(totalTokens, maxUsedTokens, extraTokens);
 			ReductionStats reductionStats = reductionUsed? new ReductionStats(removedTransitions, removedPlaces, ruleA, ruleB, ruleC, ruleD, ruleE, ruleF, ruleG, ruleH, ruleI) : null;
-			return new Tuple<QueryResult, Stats>(new QueryResult(result, boundedAnalysis, query, false), new Stats(discovered, explored, explored, transitionStats, placeBoundStats, reductionStats));
+
+            var qr = new QueryResult(result, boundedAnalysis, query, false);
+            qr.setSolvedUsingQuerySimplification(solvedUsingQuerySimplification);
+            qr.setSolvedUsingStateEquation(solvedUsingStateEquation);
+            qr.setSolvedUsingTraceAbstractRefinement(solvedUsingTraceAbstractRefinement);
+            qr.setSolvedUsingSiphonTrap(solvedUsingSiphonTrap);
+			return new Tuple<QueryResult, Stats>(qr, new Stats(discovered, explored, explored, transitionStats, placeBoundStats, reductionStats));
 		} catch (Exception e) {
 			e.printStackTrace();
 		}

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java	2022-01-28 09:46:10 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java	2022-02-07 08:12:13 +0000
@@ -7,9 +7,14 @@
 import java.util.ArrayList;
 import java.util.List;
 
+import dk.aau.cs.io.LoadedModel;
+import dk.aau.cs.io.TapnEngineXmlLoader;
+import dk.aau.cs.util.FormatException;
 import dk.aau.cs.verification.*;
 import net.tapaal.Preferences;
 import net.tapaal.TAPAAL;
+import net.tapaal.gui.petrinet.verification.UnfoldNet;
+import pipe.gui.TAPAALGUI;
 import pipe.gui.petrinet.PetriNetTab;
 import pipe.gui.petrinet.dataLayer.DataLayer;
 import net.tapaal.gui.petrinet.verification.TAPNQuery.TraceOption;
@@ -32,6 +37,8 @@
 import dk.aau.cs.util.UnsupportedModelException;
 import dk.aau.cs.util.UnsupportedQueryException;
 
+import javax.swing.*;
+
 public class VerifyTAPN implements ModelChecker {
 	private static final String NEED_TO_LOCATE_VERIFYTAPN_MSG = "TAPAAL needs to know the location of the file verifytapn.\n\n"
 		+ "Verifytapn is a part of the TAPAAL distribution and it is\n"
@@ -217,16 +224,21 @@
         }
 		
 		if(((VerifyTAPNOptions)options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model);
-		
-		VerifyTAPNExporter exporter = new VerifyTAPNExporter();
-
-		ExportedVerifyTAPNModel exportedModel = exporter.export(model.value1(), query, null,model.value2(), guiModel, dataLayerQuery);
-
-		if (exportedModel == null) {
-			messenger.displayErrorMessage("There was an error exporting the model");
-		}
-
-		return verify(options, model, exportedModel, query);
+
+        ExportedVerifyTAPNModel exportedModel;
+        if ((lens != null && lens.isColored() || model.value1().parentNetwork().isColored())) {
+            VerifyTAPNExporter exporter = new VerifyTACPNExporter();
+            exportedModel = exporter.export(model.value1(), query, TAPAALGUI.getCurrentTab().getLens(),model.value2(), guiModel, dataLayerQuery);
+        } else {
+            VerifyTAPNExporter exporter = new VerifyTAPNExporter();
+            exportedModel = exporter.export(model.value1(), query, TAPAALGUI.getCurrentTab().getLens(),model.value2(), guiModel, dataLayerQuery);
+        }
+
+        if (exportedModel == null) {
+            messenger.displayErrorMessage("There was an error exporting the model");
+        }
+
+		return verify(options, model, exportedModel, query, dataLayerQuery, lens);
 	}
 
     protected void mapDiscreteInclusionPlacesToNewNames(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model) {
@@ -250,7 +262,7 @@
 		((VerifyTAPNOptions)options).setInclusionPlaces(new InclusionPlaces(InclusionPlacesOption.UserSpecified, inclusionPlaces));
 	}
 
-	protected VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, ExportedVerifyTAPNModel exportedModel, TAPNQuery query) {
+	protected VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, ExportedVerifyTAPNModel exportedModel, TAPNQuery query, net.tapaal.gui.petrinet.verification.TAPNQuery dataLayerQuery,  PetriNetTab.TAPNLens lens) {
 		((VerifyTAPNOptions)options).setTokensInModel(model.value1().marking().size()); // TODO: get rid of me
 		runner = new ProcessRunner(verifytapnpath, createArgumentString(exportedModel.modelFile(), exportedModel.queryFile(), options));
 		runner.run();
@@ -265,8 +277,65 @@
 			if (queryResult == null || queryResult.value1() == null) {
 				return new VerificationResult<TimedArcPetriNetTrace>(errorOutput + System.getProperty("line.separator") + standardOutput, runner.getRunningTime());
 			} else {
-				TimedArcPetriNetTrace tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1());
-				return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, runner.getRunningTime(), queryResult.value2(), standardOutput);
+                TimedArcPetriNetTrace tapnTrace = null;
+
+
+                boolean isColored = (lens != null && lens.isColored() || model.value1().parentNetwork().isColored());
+                boolean showTrace = ((query.getProperty() instanceof TCTLEFNode && queryResult.value1().isQuerySatisfied()) ||
+                    (query.getProperty() instanceof TCTLAGNode && !queryResult.value1().isQuerySatisfied()) ||
+                    (query.getProperty() instanceof TCTLEGNode && queryResult.value1().isQuerySatisfied()) ||
+                    (query.getProperty() instanceof TCTLAFNode && !queryResult.value1().isQuerySatisfied()));
+
+                if(options.traceOption() != TraceOption.NONE && isColored && showTrace) {
+                    TapnEngineXmlLoader tapnLoader = new TapnEngineXmlLoader();
+                    File fileOut = new File(options.unfoldedModelPath());
+                    File queriesOut = new File(options.unfoldedQueriesPath());
+                    PetriNetTab newTab;
+                    LoadedModel loadedModel = null;
+                    try {
+                        loadedModel = tapnLoader.load(fileOut);
+                        TAPNComposer newComposer = new TAPNComposer(new MessengerImpl(), true);
+                        model = newComposer.transformModel(loadedModel.network());
+
+                        if (queryResult != null && queryResult.value1() != null) {
+                            tapnTrace = parseTrace(!errorOutput.contains("Trace:") ? errorOutput : (errorOutput.split("Trace:")[1]), options, model, exportedModel, query, queryResult.value1());
+                        }
+
+                        if (tapnTrace != null) {
+                            int dialogResult = JOptionPane.showConfirmDialog(null, "There is a trace that will be displayed in a new tab on the unfolded net/query.", "Open trace", JOptionPane.OK_CANCEL_OPTION);
+                            if (dialogResult == JOptionPane.OK_OPTION) {
+                                newTab = new PetriNetTab(loadedModel.network(), loadedModel.templates(), loadedModel.queries(), new PetriNetTab.TAPNLens(TAPAALGUI.getCurrentTab().getLens().isTimed(), TAPAALGUI.getCurrentTab().getLens().isGame(), false));
+
+                                //The query being verified should be the only query
+                                for (net.tapaal.gui.petrinet.verification.TAPNQuery loadedQuery : UnfoldNet.getQueries(queriesOut, loadedModel.network())) {
+                                    newTab.setInitialName(loadedQuery.getName() + " - unfolded");
+                                    loadedQuery.copyOptions(dataLayerQuery);
+                                    newTab.addQuery(loadedQuery);
+                                }
+
+                                TAPAALGUI.openNewTabFromStream(newTab);
+                            } else {
+                                options.setTraceOption(TraceOption.NONE);
+                            }
+                        }
+
+                    } catch (FormatException e) {
+                        e.printStackTrace();
+                        return null;
+                    } catch (ThreadDeath d) {
+                        d.printStackTrace();
+                        return null;
+                    } catch (Exception e) {
+                        e.printStackTrace();
+                        return null;
+                    }
+                }
+
+                if (tapnTrace == null) {
+                    tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1());
+                }
+				//return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, runner.getRunningTime(), queryResult.value2(), standardOutput);
+                return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, null, runner.getRunningTime(), queryResult.value2(), false, standardOutput, model);
 			}
 		}
 	}
@@ -276,15 +345,17 @@
 		
 		VerifyTAPNTraceParser traceParser = new VerifyTAPNTraceParser(model.value1());
 		TimedArcPetriNetTrace trace = traceParser.parseTrace(new BufferedReader(new StringReader(output)));
-		
-		if (trace == null) {
-			if (((VerifyTAPNOptions) options).trace() != TraceOption.NONE) {
-				if((query.getProperty() instanceof TCTLEFNode && !queryResult.isQuerySatisfied()) || (query.getProperty() instanceof TCTLAGNode && queryResult.isQuerySatisfied()))
-					return null;
-				else
-					messenger.displayErrorMessage("Verifytapn cannot generate the requested trace for the model. Try another trace option.");
-			}
-		} 
+
+        if (trace == null) {
+            if (((VerifyTAPNOptions) options).trace() != TraceOption.NONE) {
+                if ((query.getProperty() instanceof TCTLEFNode && !queryResult.isQuerySatisfied()) ||
+                    (query.getProperty() instanceof TCTLAGNode && queryResult.isQuerySatisfied()) ||
+                    (query.getProperty() instanceof TCTLEGNode && !queryResult.isQuerySatisfied()) ||
+                    (query.getProperty() instanceof TCTLAFNode && queryResult.isQuerySatisfied())) {
+                    return null;
+                }
+            }
+        }
 		return trace;
 	}
 

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java	2022-01-14 19:03:21 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java	2022-02-07 08:12:13 +0000
@@ -34,7 +34,7 @@
 		File modelFile = createTempFile(".xml");
 		File queryFile;
 		if (query.getCategory() == QueryCategory.CTL || query.getCategory() == QueryCategory.LTL || (lens != null && !lens.isGame() && lens.isColored())) {
-			queryFile = createTempFile(".xml");
+			queryFile = createTempFile(".xml"); // TODO: Remeber to change this back to XML when verifytapn is updated
 		} else {
 			queryFile = createTempFile(".q");
 		}

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java	2022-01-23 12:36:41 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java	2022-02-07 08:12:13 +0000
@@ -1,5 +1,7 @@
 package dk.aau.cs.verification.VerifyTAPN;
 
+import java.io.File;
+import java.io.IOException;
 import java.util.HashMap;
 import java.util.Map;
 
@@ -10,6 +12,7 @@
 import dk.aau.cs.model.tapn.TimedPlace;
 import dk.aau.cs.util.Require;
 import dk.aau.cs.verification.VerificationOptions;
+import pipe.gui.MessengerImpl;
 
 public class VerifyTAPNOptions extends VerificationOptions{
 
@@ -29,9 +32,29 @@
 		this(extraTokens,traceOption, search, symmetry, useStateequationCheck, discreteInclusion, new InclusionPlaces(), enableOverApproximation, enableUnderApproximation, approximationDenominator);
 	}
 
+
+
+
     public VerifyTAPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean symmetry, boolean useStateequationCheck, boolean discreteInclusion, InclusionPlaces inclusionPlaces, boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator) {
         this(extraTokens,traceOption, search, symmetry, useStateequationCheck, discreteInclusion, new InclusionPlaces(), enableOverApproximation, enableUnderApproximation, approximationDenominator, false);
     }
+
+
+    public VerifyTAPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean symmetry, boolean useStateequationCheck, boolean discreteInclusion, InclusionPlaces inclusionPlaces, boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, boolean tarOption, boolean isColor) {
+        this(extraTokens,traceOption, search, symmetry, useStateequationCheck, discreteInclusion, new InclusionPlaces(), enableOverApproximation, enableUnderApproximation, approximationDenominator, tarOption);
+
+        if(isColor && trace() != TraceOption.NONE) // we only force unfolding when traces are involved
+        {
+            try {
+                unfoldedModelPath = File.createTempFile("unfolded-", ".pnml").getAbsolutePath();
+                unfoldedQueriesPath = File.createTempFile("unfoldedQueries-", ".xml").getAbsolutePath();
+            } catch (IOException e) {
+                new MessengerImpl().displayErrorMessage(e.getMessage(), "Error");
+            }
+        }
+    }
+
+
 	
 	public VerifyTAPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean symmetry, boolean useStateEquationCheck, boolean discreteInclusion, InclusionPlaces inclusionPlaces, boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, boolean tarOption) {
 		this.extraTokens = extraTokens;
@@ -75,6 +98,15 @@
 	public String toString() {
 		StringBuilder result = new StringBuilder();
 
+        if(unfoldedModelPath != null && unfoldedQueriesPath != null)
+        {
+            result.append(" --write-unfolded-net ");
+            result.append(unfoldedModelPath);
+            result.append(" --write-unfolded-queries ");
+            result.append(unfoldedQueriesPath);
+            result.append(" ");
+        }
+
 		result.append(kBoundArg());
         result.append(deadTokenArg());
 		result.append(traceMap.get(traceOption));
@@ -106,8 +138,8 @@
 
 	public static Map<TraceOption, String> createTraceOptionsMap() {
 		HashMap<TraceOption, String> map = new HashMap<TraceOption, String>();
-		map.put(TraceOption.SOME, "--trace 1 --xml-trace");
-		map.put(TraceOption.FASTEST, "--trace 2 --xml-trace");
+		map.put(TraceOption.SOME, "--trace 1 ");
+		map.put(TraceOption.FASTEST, "--trace 2 ");
 		map.put(TraceOption.NONE, "");
 
 		return map;
@@ -115,10 +147,10 @@
 
 	private static Map<SearchOption, String> createSearchOptionsMap() {
 		HashMap<SearchOption, String> map = new HashMap<SearchOption, String>();
-		map.put(SearchOption.BFS, "--search-type 0");
-		map.put(SearchOption.DFS, "--search-type 1");
-		map.put(SearchOption.RANDOM, "--search-type 2");
-		map.put(SearchOption.HEURISTIC, "--search-type 3");
+		map.put(SearchOption.BFS, "--search-strategy BFS");
+		map.put(SearchOption.DFS, "--search-strategy DFS");
+		map.put(SearchOption.RANDOM, "--search-strategy RDFS");
+		map.put(SearchOption.HEURISTIC, "--search-strategy MAX-COVER");
 		map.put(SearchOption.DEFAULT, "");
 		return map;
 	}

=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOutputParser.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOutputParser.java	2022-01-09 18:09:13 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOutputParser.java	2022-02-07 08:12:13 +0000
@@ -33,6 +33,27 @@
 		this.extraTokens = extraTokens;
 		this.query = query;
 	}
+
+    private static final String SolvedUsingQuerySimplification_STRING = "Query solved by Query Simplification.";
+    boolean solvedUsingQuerySimplification = false;
+    private static final String solvedUsingTraceAbstractRefinement_STRING = "Solved using Trace Abstraction Refinement";
+    boolean solvedUsingTraceAbstractRefinement = false;
+    private static final String solvedUsingStateEquation_STRING = "Solved using Trace Abstraction Refinement";
+    boolean solvedUsingStateEquation = false;
+    private static final String solvedUsingSiphonTrap_STRING = "Solved using Siphon Trap";
+    boolean solvedUsingSiphonTrap  = false;
+
+    void parseSolvedMethod(String line) {
+        if (line.contains(SolvedUsingQuerySimplification_STRING)) {
+            solvedUsingQuerySimplification = true;
+        } else if (line.contains(solvedUsingTraceAbstractRefinement_STRING)) {
+            solvedUsingTraceAbstractRefinement = true;
+        } else if (line.contains(solvedUsingStateEquation_STRING)) {
+            solvedUsingStateEquation = true;
+        } else if (line.contains(solvedUsingSiphonTrap_STRING)) {
+            solvedUsingSiphonTrap = true;
+        }
+    }
 	
 	public Tuple<QueryResult, Stats> parseOutput(String output) {
 		int discovered = 0;

=== modified file 'src/net/tapaal/gui/petrinet/dialog/QueryDialog.java'
--- src/net/tapaal/gui/petrinet/dialog/QueryDialog.java	2022-01-28 09:46:10 +0000
+++ src/net/tapaal/gui/petrinet/dialog/QueryDialog.java	2022-02-07 08:12:13 +0000
@@ -183,7 +183,7 @@
 	private JCheckBox useTimeDarts;
 	private JCheckBox usePTrie;
 	private JCheckBox useGCD;
-	private JCheckBox useOverApproximation;
+	private JCheckBox skeletonAnalysis;
     private JCheckBox useSiphonTrap;
     private JCheckBox useQueryReduction;
     private JCheckBox useReduction;
@@ -423,7 +423,7 @@
 		boolean timeDarts = useTimeDarts.isSelected();
 		boolean pTrie = usePTrie.isSelected();
 		boolean gcd = useGCD.isSelected();
-		boolean overApproximation = useOverApproximation.isSelected();
+		boolean overApproximation = skeletonAnalysis.isSelected();
 		boolean reduction = useReduction.isSelected();
 
 		TAPNQuery query = new TAPNQuery(
@@ -1395,7 +1395,7 @@
         usePTrie.setSelected(queryToCreateFrom.usePTrie());
         useStubbornReduction.setSelected(queryToCreateFrom.isStubbornReductionEnabled());
         useGCD.setSelected(queryToCreateFrom.useGCD());
-        useOverApproximation.setSelected(queryToCreateFrom.useOverApproximation());
+        skeletonAnalysis.setSelected(queryToCreateFrom.useOverApproximation());
         useReduction.setSelected(queryToCreateFrom.useReduction());
         discreteInclusion.setSelected(queryToCreateFrom.discreteInclusion());
 
@@ -3338,7 +3338,7 @@
         useTimeDarts = new JCheckBox("Use Time Darts");
         useGCD = new JCheckBox("Use GCD");
         usePTrie = new JCheckBox("Use PTrie");
-        useOverApproximation = new JCheckBox("Use untimed state-equations check");
+        skeletonAnalysis = new JCheckBox("Preprocess using skeleton analysis");
         useTraceRefinement = new JCheckBox("Use trace abstraction refinement");
         useTarjan = new JCheckBox("Use Tarjan");
 
@@ -3352,7 +3352,7 @@
         useTimeDarts.setSelected(false);
         useGCD.setSelected(true);
         usePTrie.setSelected(true);
-        useOverApproximation.setSelected(true);
+        skeletonAnalysis.setSelected(true);
         useTraceRefinement.setSelected(false);
         useTarjan.setSelected(true);
 
@@ -3366,7 +3366,7 @@
         useTimeDarts.setToolTipText(TOOL_TIP_TIME_DARTS);
         useGCD.setToolTipText(TOOL_TIP_GCD);
         usePTrie.setToolTipText(TOOL_TIP_PTRIE);
-        useOverApproximation.setToolTipText(TOOL_TIP_OVERAPPROX);
+        skeletonAnalysis.setToolTipText(TOOL_TIP_OVERAPPROX);
         useTraceRefinement.setToolTipText(TOOL_TIP_USE_TRACE_REFINEMENT);
         useTarjan.setToolTipText(TOOL_TIP_USE_TARJAN);
 
@@ -3408,7 +3408,7 @@
         reductionOptionsPanel.add(useStubbornReduction, gbc);
         gbc.gridx = 0;
         gbc.gridy = 3;
-        reductionOptionsPanel.add(useOverApproximation, gbc);
+        reductionOptionsPanel.add(skeletonAnalysis, gbc);
         gbc.gridx = 2;
         gbc.gridy = 1;
         reductionOptionsPanel.add(selectInclusionPlacesButton, gbc);
@@ -3582,13 +3582,13 @@
 
 	private void refreshOverApproximationOption() {
 	    if (queryHasDeadlock() || newProperty.toString().contains("EG") || newProperty.toString().contains("AF")){
-			useOverApproximation.setSelected(false);
-			useOverApproximation.setEnabled(false);
+			skeletonAnalysis.setSelected(false);
+			skeletonAnalysis.setEnabled(false);
 		} else {
-			if(!useOverApproximation.isEnabled()){
-				useOverApproximation.setSelected(true);
+			if(!skeletonAnalysis.isEnabled()){
+				skeletonAnalysis.setSelected(true);
 			}
-			useOverApproximation.setEnabled(true);
+			skeletonAnalysis.setEnabled(true);
 		}
 
         if (lens.isGame()) {

=== modified file 'src/net/tapaal/gui/petrinet/verification/RunVerification.java'
--- src/net/tapaal/gui/petrinet/verification/RunVerification.java	2022-01-09 19:10:28 +0000
+++ src/net/tapaal/gui/petrinet/verification/RunVerification.java	2022-02-07 08:12:13 +0000
@@ -1,38 +1,34 @@
 package net.tapaal.gui.petrinet.verification;
 
-import java.awt.Dialog;
-import java.awt.Dimension;
-import java.awt.GridBagConstraints;
-import java.awt.GridBagLayout;
-import java.awt.Insets;
-import java.awt.Window;
-import java.awt.event.ActionEvent;
-import java.awt.event.ActionListener;
-import java.awt.event.HierarchyEvent;
-import java.awt.event.HierarchyListener;
-import java.io.File;
-import java.util.Comparator;
-import java.util.HashMap;
-import java.util.List;
-
-import javax.swing.*;
-import javax.swing.table.DefaultTableModel;
-import javax.swing.table.TableModel;
-import javax.swing.table.TableRowSorter;
-import pipe.gui.petrinet.PetriNetTab;
 import dk.aau.cs.Messenger;
+import dk.aau.cs.TCTL.TCTLAFNode;
+import dk.aau.cs.TCTL.TCTLAGNode;
+import dk.aau.cs.TCTL.TCTLEFNode;
+import dk.aau.cs.TCTL.TCTLEGNode;
 import dk.aau.cs.model.tapn.TimedArcPetriNet;
 import dk.aau.cs.model.tapn.simulation.TAPNNetworkTrace;
 import dk.aau.cs.util.MemoryMonitor;
 import dk.aau.cs.util.Tuple;
 import dk.aau.cs.util.VerificationCallback;
-import dk.aau.cs.verification.IconSelector;
-import dk.aau.cs.verification.ModelChecker;
-import dk.aau.cs.verification.QueryResult;
-import dk.aau.cs.verification.QueryType;
-import dk.aau.cs.verification.VerificationResult;
+import dk.aau.cs.verification.*;
+import net.tapaal.swinghelpers.GridBagHelper;
+import pipe.gui.TAPAALGUI;
+import pipe.gui.petrinet.PetriNetTab;
 import pipe.gui.petrinet.dataLayer.DataLayer;
-import pipe.gui.TAPAALGUI;
+
+import javax.swing.*;
+import javax.swing.table.DefaultTableModel;
+import javax.swing.table.TableModel;
+import javax.swing.table.TableRowSorter;
+import java.awt.*;
+import java.awt.event.HierarchyEvent;
+import java.awt.event.HierarchyListener;
+import java.io.File;
+import java.util.Comparator;
+import java.util.HashMap;
+import java.util.List;
+
+import static net.tapaal.swinghelpers.GridBagHelper.Anchor.WEST;
 
 public class RunVerification extends RunVerificationBase {	
 	private final IconSelector iconSelector;
@@ -76,10 +72,23 @@
 						JOptionPane.INFORMATION_MESSAGE,
 						iconSelector.getIconFor(result)
 				);
-	
-				if (!reducedNetOpened && result.getTrace() != null) {
-					TAPAALGUI.getAnimator().setTrace(result.getTrace());
-				}
+
+                if (options.traceOption() != TAPNQuery.TraceOption.NONE &&
+                    ((query.getProperty() instanceof TCTLEFNode && result.isQuerySatisfied()) ||
+                    (query.getProperty() instanceof TCTLAGNode && !result.isQuerySatisfied()) ||
+                    (query.getProperty() instanceof TCTLEGNode && result.isQuerySatisfied()) ||
+                    (query.getProperty() instanceof TCTLAFNode && !result.isQuerySatisfied()))) {
+                    // We have a trace to show)
+
+                    if (!reducedNetOpened && result.getTrace() != null) {
+                        TAPAALGUI.getAnimator().setTrace(result.getTrace());
+                    } else {
+                        String message = "A trace exists but could not be generated by the engine.\n\n";
+                        messenger.displayWrappedErrorMessage(message, "No trace generated");
+                    }
+                }
+
+
 			}
 		} else {
 			//Check if the is something like
@@ -121,19 +130,16 @@
             "<html>" + string.replace(System.getProperty("line.separator"), "<br/>") + "</html>";
 	}
 
-	private void displayStats(JPanel panel, String stats, String[] explanations){
+	private int displayStats(JPanel panel, String stats, String[] explanations, int startOffset){
         String[] statsStrings = stats.split(System.getProperty("line.separator"));
+
         for (int i = 0; i < statsStrings.length; i++) {
-            GridBagConstraints gbc = new GridBagConstraints();
-            gbc.gridx = 0;
-            gbc.gridy = i+1;
-            gbc.insets = new Insets(0,0,0,0);
-            gbc.anchor = GridBagConstraints.WEST;
+            GridBagConstraints gbc = GridBagHelper.as(0, i+startOffset, WEST, new Insets(0,0,0,0));
             JLabel statLabel = new JLabel(statsStrings[i]);
             statLabel.setToolTipText(explanations[i]);
             panel.add(statLabel, gbc);
         }
-
+        return startOffset+statsStrings.length;
     }
 
 	private JPanel createStatisticsPanel(final VerificationResult<TAPNNetworkTrace> result, boolean transitionPanel) {
@@ -304,142 +310,121 @@
 
 		// TODO remove this when the engine outputs statistics
 		boolean isCTLQuery = result.getQueryResult().isCTL;
+        int rowOffset = 1;
+		if(modelChecker.supportsStats() && !result.isSolvedUsingQuerySimplification() && !isCTLQuery){
+            rowOffset = displayStats(panel, result.getStatsAsString(), modelChecker.getStatsExplanations(), 1);
 
-		if(modelChecker.supportsStats() && !result.isSolvedUsingStateEquation() && !isCTLQuery){
-            displayStats(panel, result.getStatsAsString(), modelChecker.getStatsExplanations());
             if(!result.getTransitionStatistics().isEmpty()) {
                 if (!result.getTransitionStatistics().isEmpty()) {
                     JButton transitionStatsButton = new JButton("Transition Statistics");
                     transitionStatsButton.addActionListener(arg0 -> JOptionPane.showMessageDialog(panel, createStatisticsPanel(result, true), "Transition Statistics", JOptionPane.INFORMATION_MESSAGE));
-                    gbc = new GridBagConstraints();
-                    gbc.gridx = 0;
-                    gbc.gridy = 4;
-                    gbc.insets = new Insets(10, 0, 10, 0);
-                    gbc.anchor = GridBagConstraints.WEST;
+                    gbc = GridBagHelper.as(0,4, WEST, new Insets(10, 0, 10, 0));
                     panel.add(transitionStatsButton, gbc);
                 }
                 if (!result.getPlaceBoundStatistics().isEmpty()) {
                     JButton placeStatsButton = new JButton("Place-Bound Statistics");
                     placeStatsButton.addActionListener(arg0 -> JOptionPane.showMessageDialog(panel, createStatisticsPanel(result, false), "Place-Bound Statistics", JOptionPane.INFORMATION_MESSAGE));
-                    gbc = new GridBagConstraints();
-                    gbc.gridx = 1;
-                    gbc.gridy = 4;
-                    gbc.insets = new Insets(10, 0, 10, 0);
-                    gbc.anchor = GridBagConstraints.WEST;
+                    gbc = GridBagHelper.as(1,4, WEST, new Insets(10, 0, 10, 0));
                     panel.add(placeStatsButton, gbc);
                 }
             }
 			if(!result.getReductionResultAsString().isEmpty()){
-				JLabel reductionStatsLabel = new JLabel(toHTML(result.getReductionResultAsString()));
-				gbc = new GridBagConstraints();
-				gbc.gridx = 0;
-				gbc.gridy = 6;
-				gbc.insets = new Insets(0,0,20,-90);
-				gbc.anchor = GridBagConstraints.WEST;
 
+                JLabel reductionStatsLabel = new JLabel(toHTML(result.getReductionResultAsString()));
+				gbc = GridBagHelper.as(0,6, WEST, new Insets(0,0,20,-90));
 				panel.add(reductionStatsLabel, gbc);
 
 				if(result.reductionRulesApplied()){
                     JButton openReducedButton = new JButton("Open reduced net");
-                    openReducedButton.addActionListener(new ActionListener() {
-                        public void actionPerformed(ActionEvent e) {
-                            openReducedButton.setEnabled(false);
-                            reducedNetOpened = true;
-
-                            File reducedNetFile = new File(reducedNetFilePath);
-
-                            if(reducedNetFile.exists() && reducedNetFile.isFile() && reducedNetFile.canRead()){
-                                try {
-                                    PetriNetTab reducedNetTab = PetriNetTab.createNewTabFromPNMLFile(reducedNetFile);
-                                    //Ensure that a net was created by the query reduction
-                                    if(reducedNetTab.currentTemplate().guiModel().getPlaces().length  > 0
-                                        || reducedNetTab.currentTemplate().guiModel().getTransitions().length > 0){
-                                        reducedNetTab.setInitialName("reduced-" + TAPAALGUI.getAppGui().getCurrentTabName());
-                                        TAPNQuery convertedQuery = dataLayerQuery.convertPropertyForReducedNet(reducedNetTab.currentTemplate().toString());
-                                        reducedNetTab.addQuery(convertedQuery);
-                                        TAPAALGUI.openNewTabFromStream(reducedNetTab);
-                                    }
-                                } catch (Exception e1){
-                                    JOptionPane.showMessageDialog(TAPAALGUI.getApp(),
-                                        e1.getMessage(),
-                                        "Error loading reduced net file",
-                                        JOptionPane.ERROR_MESSAGE);
+                    openReducedButton.addActionListener(e -> {
+                        openReducedButton.setEnabled(false);
+                        reducedNetOpened = true;
+
+                        File reducedNetFile = new File(reducedNetFilePath);
+
+                        if(reducedNetFile.exists() && reducedNetFile.isFile() && reducedNetFile.canRead()){
+                            try {
+                                PetriNetTab reducedNetTab = PetriNetTab.createNewTabFromPNMLFile(reducedNetFile);
+                                //Ensure that a net was created by the query reduction
+                                if(reducedNetTab.currentTemplate().guiModel().getPlaces().length  > 0
+                                    || reducedNetTab.currentTemplate().guiModel().getTransitions().length > 0){
+                                    reducedNetTab.setInitialName("reduced-" + TAPAALGUI.getAppGui().getCurrentTabName());
+                                    TAPNQuery convertedQuery = dataLayerQuery.convertPropertyForReducedNet(reducedNetTab.currentTemplate().toString());
+                                    reducedNetTab.addQuery(convertedQuery);
+                                    TAPAALGUI.openNewTabFromStream(reducedNetTab);
                                 }
+                            } catch (Exception e1){
+                                JOptionPane.showMessageDialog(TAPAALGUI.getApp(),
+                                    e1.getMessage(),
+                                    "Error loading reduced net file",
+                                    JOptionPane.ERROR_MESSAGE);
                             }
                         }
                     });
 
-                    gbc = new GridBagConstraints();
-                    gbc.gridx = 0;
-                    gbc.gridy = 5;
-                    gbc.insets = new Insets(0,0,10,0);
-                    gbc.anchor = GridBagConstraints.WEST;
+                    gbc = GridBagHelper.as(0,5, WEST, new Insets(0,0,10,0));
                     panel.add(openReducedButton, gbc);
                 }
                 if (!result.getPlaceBoundStatistics().isEmpty()) {
                     JButton placeStatsButton = new JButton("Place-Bound Statistics");
                     placeStatsButton.addActionListener(arg0 -> JOptionPane.showMessageDialog(panel, createStatisticsPanel(result, false), "Place-Bound Statistics", JOptionPane.INFORMATION_MESSAGE));
-                    gbc = new GridBagConstraints();
-                    gbc.gridx = 1;
-                    gbc.gridy = 4;
-                    gbc.insets = new Insets(10, 0, 10, 0);
-                    gbc.anchor = GridBagConstraints.WEST;
+
+                    gbc = GridBagHelper.as(1,4, WEST, new Insets(10, 0, 10, 0));
                     panel.add(placeStatsButton, gbc);
                 }
             }
-
-            if (result.getRawOutput() != null) {
-                JButton showRawQueryButton = new JButton("Show raw query results");
-                showRawQueryButton.addActionListener(arg0 -> JOptionPane.showMessageDialog(panel, createRawQueryPanel(result.getRawOutput()), "Raw query results", JOptionPane.INFORMATION_MESSAGE));
-                gbc = new GridBagConstraints();
-                gbc.gridx = 1;
-                gbc.gridy = 5;
-                gbc.insets = new Insets(0,0,10,0);
-                gbc.anchor = GridBagConstraints.WEST;
-                panel.add(showRawQueryButton, gbc);
-            }
-		} else if (modelChecker.supportsStats() && !result.isSolvedUsingStateEquation() && isCTLQuery){
-            displayStats(panel, result.getCTLStatsAsString(), modelChecker.getStatsExplanations());
-
-		}
-
-		if(result.isSolvedUsingStateEquation()){
-			gbc = new GridBagConstraints();
-			gbc.gridx = 0;
-			gbc.gridy = 6;
-			gbc.insets = new Insets(0,0,15,0);
-			gbc.anchor = GridBagConstraints.WEST;
-			panel.add(new JLabel(toHTML("The query was resolved using state equations.")), gbc);
-		}
+            rowOffset = 6;
+
+		} else if (modelChecker.supportsStats() && !result.isSolvedUsingQuerySimplification() && isCTLQuery){
+            rowOffset = displayStats(panel, result.getCTLStatsAsString(), modelChecker.getStatsExplanations(), 1);
+		}
+
+        if (result.getRawOutput() != null) {
+            JButton showRawQueryButton = new JButton("Show raw query results");
+            showRawQueryButton.addActionListener(arg0 -> JOptionPane.showMessageDialog(panel, createRawQueryPanel(result.getRawOutput()), "Raw query results", JOptionPane.INFORMATION_MESSAGE));
+            gbc = GridBagHelper.as(1, 5, WEST, new Insets(0,0,10,0));
+            panel.add(showRawQueryButton, gbc);
+        }
+
+        if (result.isResolvedUsingSkeletonPreprocessor()) {
+            gbc = GridBagHelper.as(0, rowOffset+1, GridBagHelper.Anchor.WEST, new Insets(0,0,15,0));
+            gbc.gridwidth = 2;
+            panel.add(new JLabel(toHTML("The query was resolved using Skeleton Analysis preprocessing")), gbc);
+        }
+
+
+        gbc = GridBagHelper.as(0, rowOffset+2, WEST, new Insets(0,0,15,0));
+        gbc.gridwidth = 2;
+		if(result.isSolvedUsingQuerySimplification()){
+			panel.add(new JLabel(toHTML("The query was resolved using Query Simplification.")), gbc);
+		} else if (result.isSolvedUsingTraceAbstractRefinement()){
+            panel.add(new JLabel(toHTML("The query was not resolved using Trace Abstraction Refinement.")), gbc);
+        } else if (result.isSolvedUsingStateEquation()) {
+            panel.add(new JLabel(toHTML("The query was resolved using state equations.")), gbc);
+        } else if (result.isSolvedUsingSiphonTrap()) {
+            panel.add(new JLabel(toHTML("The query was resolved using Siphon Trap.")), gbc);
+        }
 		
-		gbc = new GridBagConstraints();
-		gbc.gridx = 0;
-		gbc.gridy = 7;
-		gbc.gridwidth = 2;
-		gbc.anchor = GridBagConstraints.WEST;
+		gbc = GridBagHelper.as(0, rowOffset+3, WEST);
+    	gbc.gridwidth = 2;
 		panel.add(new JLabel(result.getVerificationTimeString()), gbc);
-		
-		gbc = new GridBagConstraints();
-		gbc.gridx = 0;
-		gbc.gridy = 8;
-		gbc.gridwidth = 2;
-		gbc.anchor = GridBagConstraints.WEST;
+
+        gbc = GridBagHelper.as(0, rowOffset+4, WEST);
+        gbc.gridwidth = 2;
 		panel.add(new JLabel("Estimated memory usage: "+MemoryMonitor.getPeakMemory()), gbc);
 		
 		//Show discrete semantics warning if needed
 		QueryResult queryResult = result.getQueryResult();
-		if(((queryResult.hasDeadlock() && queryResult.queryType() == QueryType.EF && !queryResult.isQuerySatisfied()) || 
-                   (queryResult.hasDeadlock() && queryResult.queryType() == QueryType.AG && queryResult.isQuerySatisfied()) || 
-                   (queryResult.queryType() == QueryType.EG && !queryResult.isQuerySatisfied()) || 
-		   (queryResult.queryType() == QueryType.AF && queryResult.isQuerySatisfied())) 
-				&& modelChecker.useDiscreteSemantics()){
-			gbc = new GridBagConstraints();
-			gbc.gridx = 0;
-			gbc.gridy = 11;
-			gbc.gridwidth = 2;
-			gbc.anchor = GridBagConstraints.WEST;
-			panel.add(new JLabel("<html><font color=red>The verification answer is guaranteed for<br/>the discrete semantics only (integer delays).</font></html>"), gbc);
-		}
+        if (((queryResult.hasDeadlock() && queryResult.queryType() == QueryType.EF && !queryResult.isQuerySatisfied()) ||
+            (queryResult.hasDeadlock() && queryResult.queryType() == QueryType.AG && queryResult.isQuerySatisfied()) ||
+            (queryResult.queryType() == QueryType.EG && !queryResult.isQuerySatisfied()) ||
+            (queryResult.queryType() == QueryType.AF && queryResult.isQuerySatisfied()))
+            && modelChecker.useDiscreteSemantics()) {
+
+            gbc = GridBagHelper.as(0, rowOffset+7, WEST);
+            gbc.gridwidth = 2;
+            panel.add(new JLabel("<html><font color=red>The verification answer is guaranteed for<br/>the discrete semantics only (integer delays).</font></html>"), gbc);
+        }
 		
 		return panel;
 	}

=== modified file 'src/net/tapaal/gui/petrinet/verification/RunVerificationBase.java'
--- src/net/tapaal/gui/petrinet/verification/RunVerificationBase.java	2022-01-28 13:29:38 +0000
+++ src/net/tapaal/gui/petrinet/verification/RunVerificationBase.java	2022-02-07 08:12:13 +0000
@@ -107,9 +107,9 @@
                 if (!verifypn.setup()) {
                     messenger.displayInfoMessage("Over-approximation check is skipped because VerifyPN is not available.", "VerifyPN unavailable");
                 } else {
-                    VerificationResult<TimedArcPetriNetTrace> overapprox_result = null;
+                    VerificationResult<TimedArcPetriNetTrace> skeletonAnalysisResult = null;
                     if (dataLayerQuery != null) {
-                        overapprox_result = verifypn.verify(
+                        skeletonAnalysisResult = verifypn.verify(
                             new VerifyPNOptions(
                                 options.extraTokens(),
                                 net.tapaal.gui.petrinet.verification.TAPNQuery.TraceOption.NONE,
@@ -139,7 +139,7 @@
                             dataLayerQuery,
                             null);
                     } else { // TODO: FIX! If datalayer is null then we can't check datalayer's values...
-                        overapprox_result = verifypn.verify(
+                        skeletonAnalysisResult = verifypn.verify(
                             new VerifyPNOptions(
                                 options.extraTokens(),
                                 net.tapaal.gui.petrinet.verification.TAPNQuery.TraceOption.NONE,
@@ -170,18 +170,19 @@
                             null);
                     }
 
-                    if (overapprox_result.getQueryResult() != null) {
-                        if (!overapprox_result.error() && model.isUntimed() || (
-                            (query.queryType() == QueryType.EF && !overapprox_result.getQueryResult().isQuerySatisfied()) ||
-                                (query.queryType() == QueryType.AG && overapprox_result.getQueryResult().isQuerySatisfied()))
+                    if (skeletonAnalysisResult.getQueryResult() != null) {
+                        if (!skeletonAnalysisResult.error() && model.isUntimed() || (
+                            (query.queryType() == QueryType.EF && !skeletonAnalysisResult.getQueryResult().isQuerySatisfied()) ||
+                                (query.queryType() == QueryType.AG && skeletonAnalysisResult.getQueryResult().isQuerySatisfied()))
                         ) {
                             VerificationResult<TAPNNetworkTrace> value = new VerificationResult<TAPNNetworkTrace>(
-                                overapprox_result.getQueryResult(),
-                                decomposeTrace(overapprox_result.getTrace(), transformedModel.value2()),
-                                overapprox_result.verificationTime(),
-                                overapprox_result.stats(),
-                                true
+                                skeletonAnalysisResult.getQueryResult(),
+                                decomposeTrace(skeletonAnalysisResult.getTrace(), transformedModel.value2()),
+                                skeletonAnalysisResult.verificationTime(),
+                                skeletonAnalysisResult.stats(),
+                                skeletonAnalysisResult.getRawOutput()
                             );
+                            value.setResolvedUsingSkeletonAnalysisPreprocessor(true);
                             value.setNameMapping(transformedModel.value2());
                             return value;
                         }

=== modified file 'src/net/tapaal/gui/petrinet/verification/Verifier.java'
--- src/net/tapaal/gui/petrinet/verification/Verifier.java	2022-01-28 13:29:38 +0000
+++ src/net/tapaal/gui/petrinet/verification/Verifier.java	2022-02-07 08:12:13 +0000
@@ -240,7 +240,9 @@
                 query.inclusionPlaces(),
                 query.isOverApproximationEnabled(),
                 query.isUnderApproximationEnabled(),
-                query.approximationDenominator()
+                query.approximationDenominator(),
+                false,
+                isColored
             );
         }
 

=== modified file 'src/net/tapaal/gui/petrinet/verification/VerifyTAPNEngineOptions.java'
--- src/net/tapaal/gui/petrinet/verification/VerifyTAPNEngineOptions.java	2022-01-07 16:58:59 +0000
+++ src/net/tapaal/gui/petrinet/verification/VerifyTAPNEngineOptions.java	2022-02-07 08:12:13 +0000
@@ -19,7 +19,7 @@
             false, //support games
             false, //support EG or AF with net degree > 2
             false, //support for nested quantification
-            false
+            true
         );
     }
 }