Merge lp:~tapaal-contributor/tapaal/show-reduced-net-1879130 into lp:tapaal

[Thomas Pedersen]

Add button for opening the reduced net, obtained after applying the structural reduction rules.

Added the place and transition positions to the saved net file, for the engine to preserve these positions in the reduced net.

This code is dependent on https://code.launchpad.net/~tapaal-contributor/verifypn/show-reduced-net for using the place and transition positions.

[Jiri Srba (srba)]

The button should also appear in the query dialog next two "Merge net components".

review: Needs Fixing

[lp:~tapaal-contributor/tapaal/show-reduced-net-1879130]

1070. By Thomas Pedersen <email address hidden> on 2020-10-15

Add option to open reduced net from the query dialog panel

[Thomas Pedersen (tpede16)]

Added the open reduced net button to the query dialog.

The button will close the dialog and run minimal verification before opening the reduced net.

review: Needs Resubmitting

[Kenneth Yrke Jørgensen (yrke)]

review: Approve (code)

[Jiri Srba (srba)]

The reduction gives error when called for timed net. The reduction show option should be available only if the lens says that the new is untimed and non-game.

review: Needs Fixing

[lp:~tapaal-contributor/tapaal/show-reduced-net-1879130]

1071. By Thomas Pedersen <email address hidden> on 2020-10-31

Make button to open reduced net in query dialog only appear for untimed non-game nets

[Thomas Pedersen (tpede16)]

Made the button to open the reduced net from the query dialog only appear if the lens is untimed and non-game

review: Needs Resubmitting

[lp:~tapaal-contributor/tapaal/show-reduced-net-1879130]

1072. By Thomas Pedersen <email address hidden> on 2020-10-31

Added the query to the reduced net

1073. By Thomas Pedersen <email address hidden> on 2020-11-06

Fix query translation for reduced nets

1074. By Thomas Pedersen <email address hidden> on 2020-11-06

Merge with trunk

1075. By Thomas Pedersen <email address hidden> on 2020-11-06

Ensure that a new tab is only opened when a reduced net is created

[Thomas Pedersen (tpede16)]

Transferred the query that produced the reduced net to the tab for the reduced net and ensured that a new tab is only created when there is a reduced net to display.

review: Needs Resubmitting

[Kenneth Yrke Jørgensen (yrke)]

approved, you might consider implementing the changes in the AST as a visitor insted of directly on the AST.

review: Approve (code)

[Jiri Srba (srba)]

Open the alternating bit components example - untime it and verify the query. An exception is raised - works correctly in 3.7.1.

review: Needs Fixing

[lp:~tapaal-contributor/tapaal/show-reduced-net-1879130]

1076. By Thomas Pedersen <email address hidden> on 2020-11-11

Fix getting positional information from multiple components

[Thomas Pedersen (tpede16)]

Fixed getting positions from multiple templates and stopped entering simulation mode after verification if the reduced net is opened.

review: Needs Resubmitting

[Jiri Srba (srba)]

If you run verification and no reduction rules were applicable, the verification answer still offers "Open reduced net" but when you click nothing happens. If no reduction rules are applicable, then the button show not be enabled.

review: Needs Fixing

[Jiri Srba (srba)]

Also, open intro net, untime it and change the query so that Target=2. Now try to show the reduced net - it never opens as the state equations kick in - they should be disabled when you want to see the reduced net.

review: Needs Fixing

[lp:~tapaal-contributor/tapaal/show-reduced-net-1879130]

1077. By Thomas Pedersen <email address hidden> on 2020-11-11

Check if reduction rules are used before creating button to open reduced net

1078. By Thomas Pedersen <email address hidden> on 2020-11-13

Disable query reduction when reduced net is opened from query dialog

[Thomas Pedersen (tpede16)]

Removed the button for opening the reduced net, when no reduction rules are applied.

Disabled query reduction completely when the reduced net is opened from the query dialog. This is dependent on the changes made to verifypn allowing -s OverApprox -q 0 (https://code.launchpad.net/~tapaal-contributor/verifypn/show-reduced-net)

review: Needs Resubmitting

[Jiri Srba (srba)]

Still needs fixing - open intro example and unselect all verification options (Reductions, Siphon etc). They try to open the reduced net, an error appers.

review: Needs Fixing

[lp:~tapaal-contributor/tapaal/show-reduced-net-1879130]

1079. By Thomas Pedersen <email address hidden> on 2020-12-16

Disable open reduced net button when query reductions are disabled

[Jiri Srba (srba)]

Needs to be merged with trunk - there are a few merge conflicts

review: Needs Fixing

[lp:~tapaal-contributor/tapaal/show-reduced-net-1879130]

1080. By Thomas Pedersen <email address hidden> on 2020-12-17

Merge with trunk

[Thomas Pedersen (tpede16)]

Disable the button for opening the reduced net from the query dialog, when structural reductions are disabled and merged with trunk

review: Needs Resubmitting

[Jiri Srba (srba)]

review: Approve

=== modified file 'gradlew' (properties changed: -x to +x)
=== modified file 'src/dk/aau/cs/TCTL/AritmeticOperator.java'
--- src/dk/aau/cs/TCTL/AritmeticOperator.java	2020-08-17 08:09:43 +0000
+++ src/dk/aau/cs/TCTL/AritmeticOperator.java	2020-12-17 21:03:24 +0000
@@ -22,7 +22,11 @@
 		}
 	}
 
-	@Override
+    @Override
+    public void convertForReducedNet(String templateName) {
+    }
+
+    @Override
 	public TCTLAbstractStateProperty copy() {
 		return new AritmeticOperator(operator);
 	}
 
=== modified file 'src/dk/aau/cs/TCTL/TCTLAFNode.java'
--- src/dk/aau/cs/TCTL/TCTLAFNode.java	2020-08-17 08:09:43 +0000
+++ src/dk/aau/cs/TCTL/TCTLAFNode.java	2020-12-17 21:03:24 +0000
@@ -41,7 +41,12 @@
 		return children;
 	}
 
-	@Override
+    @Override
+    public void convertForReducedNet(String templateName) {
+        property.convertForReducedNet(templateName);
+    }
+
+    @Override
 	public boolean equals(Object o) {
 		if (o instanceof TCTLAFNode) {
 			TCTLAFNode node = (TCTLAFNode) o;
 
=== modified file 'src/dk/aau/cs/TCTL/TCTLAGNode.java'
--- src/dk/aau/cs/TCTL/TCTLAGNode.java	2020-08-17 08:09:43 +0000
+++ src/dk/aau/cs/TCTL/TCTLAGNode.java	2020-12-17 21:03:24 +0000
@@ -41,7 +41,12 @@
 		return children;
 	}
 
-	@Override
+    @Override
+    public void convertForReducedNet(String templateName) {
+        property.convertForReducedNet(templateName);
+    }
+
+    @Override
 	public boolean equals(Object o) {
 		if (o instanceof TCTLAGNode) {
 			TCTLAGNode node = (TCTLAGNode) o;
 
=== modified file 'src/dk/aau/cs/TCTL/TCTLAUNode.java'
--- src/dk/aau/cs/TCTL/TCTLAUNode.java	2020-08-17 08:09:43 +0000
+++ src/dk/aau/cs/TCTL/TCTLAUNode.java	2020-12-17 21:03:24 +0000
@@ -58,7 +58,13 @@
 		return children;
 	}
 
-	@Override
+    @Override
+    public void convertForReducedNet(String templateName) {
+        left.convertForReducedNet(templateName);
+        right.convertForReducedNet(templateName);
+    }
+
+    @Override
 	public boolean equals(Object o) {	
 		if (o instanceof TCTLAUNode) {
 			TCTLAUNode node = (TCTLAUNode) o;
 
=== modified file 'src/dk/aau/cs/TCTL/TCTLAXNode.java'
--- src/dk/aau/cs/TCTL/TCTLAXNode.java	2020-08-17 08:09:43 +0000
+++ src/dk/aau/cs/TCTL/TCTLAXNode.java	2020-12-17 21:03:24 +0000
@@ -41,7 +41,12 @@
 		return children;
 	}
 
-	@Override
+    @Override
+    public void convertForReducedNet(String templateName) {
+        property.convertForReducedNet(templateName);
+    }
+
+    @Override
 	public boolean equals(Object o) {
 		if (o instanceof TCTLAXNode) {
 			TCTLAXNode node = (TCTLAXNode) o;
 
=== modified file 'src/dk/aau/cs/TCTL/TCTLAbstractProperty.java'
--- src/dk/aau/cs/TCTL/TCTLAbstractProperty.java	2020-08-17 08:09:43 +0000
+++ src/dk/aau/cs/TCTL/TCTLAbstractProperty.java	2020-12-17 21:03:24 +0000
@@ -51,6 +51,8 @@
 		return children;
 	}
 
+	public abstract void convertForReducedNet(String templateName);
+
 	public abstract void accept(ITCTLVisitor visitor, Object context);
 
 	public abstract boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName);
 
=== modified file 'src/dk/aau/cs/TCTL/TCTLAndListNode.java'
--- src/dk/aau/cs/TCTL/TCTLAndListNode.java	2020-08-17 08:09:43 +0000
+++ src/dk/aau/cs/TCTL/TCTLAndListNode.java	2020-12-17 21:03:24 +0000
@@ -122,7 +122,14 @@
 		return children;
 	}
 
-	@Override
+    @Override
+    public void convertForReducedNet(String templateName) {
+        for (TCTLAbstractProperty property : properties){
+            property.convertForReducedNet(templateName);
+        }
+    }
+
+    @Override
 	public boolean equals(Object o) {
 		if (o instanceof TCTLAndListNode) {
 			TCTLAndListNode node = (TCTLAndListNode) o;
 
=== modified file 'src/dk/aau/cs/TCTL/TCTLAtomicPropositionNode.java'
--- src/dk/aau/cs/TCTL/TCTLAtomicPropositionNode.java	2020-08-17 08:09:43 +0000
+++ src/dk/aau/cs/TCTL/TCTLAtomicPropositionNode.java	2020-12-17 21:03:24 +0000
@@ -67,7 +67,13 @@
 		}
 	}
 
-	@Override
+    @Override
+    public void convertForReducedNet(String templateName) {
+        left.convertForReducedNet(templateName);
+        right.convertForReducedNet(templateName);
+    }
+
+    @Override
 	public String toString() {
 		return left + " " + op + " " + right;
 	}
@@ -88,6 +94,31 @@
         return false;
     }
 
+/*    @Override
+    public StringPosition[] getChildren() {
+        StringPosition[] children = new StringPosition[2];
+
+        int start = 0;
+        int end = 0;
+        boolean leftSimpleProperty = left.isSimpleProperty();
+
+        start = leftSimpleProperty ? 0 : 1;
+        end = start + left.toString().length();
+
+        StringPosition posLeft = new StringPosition(start, end, left);
+
+        start = end + 5 + (right.isSimpleProperty() ? 0 : 1)
+            + (leftSimpleProperty ? 0 : 1);
+
+        end = start + right.toString().length();
+
+        StringPosition posRight = new StringPosition(start, end, right);
+
+        children[0] = posLeft;
+        children[1] = posRight;
+        return children;
+    }*/
+
     @Override
 	public TCTLAbstractProperty findFirstPlaceHolder() {
 		TCTLAbstractProperty rightP = right.findFirstPlaceHolder(); 
 
=== modified file 'src/dk/aau/cs/TCTL/TCTLConstNode.java'
--- src/dk/aau/cs/TCTL/TCTLConstNode.java	2020-08-17 08:09:43 +0000
+++ src/dk/aau/cs/TCTL/TCTLConstNode.java	2020-12-17 21:03:24 +0000
@@ -26,7 +26,12 @@
 		}
 	}
 
-	@Override
+    @Override
+    public void convertForReducedNet(String templateName) {
+
+    }
+
+    @Override
 	public TCTLAbstractStateProperty copy() {
 		return new TCTLConstNode(constant);
 	}
 
=== modified file 'src/dk/aau/cs/TCTL/TCTLDeadlockNode.java'
--- src/dk/aau/cs/TCTL/TCTLDeadlockNode.java	2020-08-17 08:09:43 +0000
+++ src/dk/aau/cs/TCTL/TCTLDeadlockNode.java	2020-12-17 21:03:24 +0000
@@ -18,7 +18,11 @@
 		}
 	}
 
-	@Override
+    @Override
+    public void convertForReducedNet(String templateName) {
+    }
+
+    @Override
 	public void accept(ITCTLVisitor visitor, Object context) {
 		visitor.visit(this, context);
 	}
 
=== modified file 'src/dk/aau/cs/TCTL/TCTLEFNode.java'
--- src/dk/aau/cs/TCTL/TCTLEFNode.java	2020-08-17 08:09:43 +0000
+++ src/dk/aau/cs/TCTL/TCTLEFNode.java	2020-12-17 21:03:24 +0000
@@ -41,7 +41,12 @@
 		return children;
 	}
 
-	@Override
+    @Override
+    public void convertForReducedNet(String templateName) {
+        property.convertForReducedNet(templateName);
+    }
+
+    @Override
 	public boolean equals(Object o) {
 		if (o instanceof TCTLEFNode) {
 			TCTLEFNode node = (TCTLEFNode) o;
 
=== modified file 'src/dk/aau/cs/TCTL/TCTLEGNode.java'
--- src/dk/aau/cs/TCTL/TCTLEGNode.java	2020-08-17 08:09:43 +0000
+++ src/dk/aau/cs/TCTL/TCTLEGNode.java	2020-12-17 21:03:24 +0000
@@ -41,7 +41,12 @@
 		return children;
 	}
 
-	@Override
+    @Override
+    public void convertForReducedNet(String templateName) {
+        property.convertForReducedNet(templateName);
+    }
+
+    @Override
 	public boolean equals(Object o) {
 		if (o instanceof TCTLEGNode) {
 			TCTLEGNode node = (TCTLEGNode) o;
 
=== modified file 'src/dk/aau/cs/TCTL/TCTLEUNode.java'
--- src/dk/aau/cs/TCTL/TCTLEUNode.java	2020-08-17 08:09:43 +0000
+++ src/dk/aau/cs/TCTL/TCTLEUNode.java	2020-12-17 21:03:24 +0000
@@ -58,7 +58,13 @@
 		return children;
 	}
 
-	@Override
+    @Override
+    public void convertForReducedNet(String templateName) {
+        left.convertForReducedNet(templateName);
+        right.convertForReducedNet(templateName);
+    }
+
+    @Override
 	public boolean equals(Object o) {	
 		if (o instanceof TCTLEUNode) {
 			TCTLEUNode node = (TCTLEUNode) o;
 
=== modified file 'src/dk/aau/cs/TCTL/TCTLEXNode.java'
--- src/dk/aau/cs/TCTL/TCTLEXNode.java	2020-08-17 08:09:43 +0000
+++ src/dk/aau/cs/TCTL/TCTLEXNode.java	2020-12-17 21:03:24 +0000
@@ -41,7 +41,12 @@
 		return children;
 	}
 
-	@Override
+    @Override
+    public void convertForReducedNet(String templateName) {
+        property.convertForReducedNet(templateName);
+    }
+
+    @Override
 	public boolean equals(Object o) {
 		if (o instanceof TCTLEXNode) {
 			TCTLEXNode node = (TCTLEXNode) o;
 
=== modified file 'src/dk/aau/cs/TCTL/TCTLFalseNode.java'
--- src/dk/aau/cs/TCTL/TCTLFalseNode.java	2020-08-17 08:09:43 +0000
+++ src/dk/aau/cs/TCTL/TCTLFalseNode.java	2020-12-17 21:03:24 +0000
@@ -18,7 +18,11 @@
 		}
 	}
 
-	@Override
+    @Override
+    public void convertForReducedNet(String templateName) {
+    }
+
+    @Override
 	public void accept(ITCTLVisitor visitor, Object context) {
 		visitor.visit(this, context);
 	}
 
=== modified file 'src/dk/aau/cs/TCTL/TCTLNotNode.java'
--- src/dk/aau/cs/TCTL/TCTLNotNode.java	2020-08-17 08:09:43 +0000
+++ src/dk/aau/cs/TCTL/TCTLNotNode.java	2020-12-17 21:03:24 +0000
@@ -52,7 +52,12 @@
 		return children;
 	}
 
-	@Override
+    @Override
+    public void convertForReducedNet(String templateName) {
+        property.convertForReducedNet(templateName);
+    }
+
+    @Override
 	public TCTLAbstractStateProperty copy() {
 		return new TCTLNotNode(property.copy());
 	}
 
=== modified file 'src/dk/aau/cs/TCTL/TCTLOrListNode.java'
--- src/dk/aau/cs/TCTL/TCTLOrListNode.java	2020-08-17 08:09:43 +0000
+++ src/dk/aau/cs/TCTL/TCTLOrListNode.java	2020-12-17 21:03:24 +0000
@@ -122,7 +122,14 @@
 		return children;
 	}
 
-	@Override
+    @Override
+    public void convertForReducedNet(String templateName) {
+        for(TCTLAbstractProperty property : properties){
+            property.convertForReducedNet(templateName);
+        }
+    }
+
+    @Override
 	public boolean equals(Object o) {
 		if (o instanceof TCTLOrListNode) {
 			TCTLOrListNode node = (TCTLOrListNode) o;
 
=== modified file 'src/dk/aau/cs/TCTL/TCTLPathPlaceHolder.java'
--- src/dk/aau/cs/TCTL/TCTLPathPlaceHolder.java	2020-08-17 08:09:43 +0000
+++ src/dk/aau/cs/TCTL/TCTLPathPlaceHolder.java	2020-12-17 21:03:24 +0000
@@ -49,7 +49,12 @@
 		}
 	}
 
-	@Override
+    @Override
+    public void convertForReducedNet(String templateName) {
+
+    }
+
+    @Override
 	public void accept(ITCTLVisitor visitor, Object context) {
 		visitor.visit(this, context);
 	}
 
=== modified file 'src/dk/aau/cs/TCTL/TCTLPathToStateConverter.java'
--- src/dk/aau/cs/TCTL/TCTLPathToStateConverter.java	2020-08-17 08:09:43 +0000
+++ src/dk/aau/cs/TCTL/TCTLPathToStateConverter.java	2020-12-17 21:03:24 +0000
@@ -37,7 +37,12 @@
 		return children;
 	}
 
-	@Override
+    @Override
+    public void convertForReducedNet(String templateName) {
+        property.convertForReducedNet(templateName);
+    }
+
+    @Override
 	public boolean equals(Object o) {
 		if (o instanceof TCTLEFNode) {
 			TCTLEFNode node = (TCTLEFNode) o;
 
=== modified file 'src/dk/aau/cs/TCTL/TCTLPlaceNode.java'
--- src/dk/aau/cs/TCTL/TCTLPlaceNode.java	2020-08-17 08:09:43 +0000
+++ src/dk/aau/cs/TCTL/TCTLPlaceNode.java	2020-12-17 21:03:24 +0000
@@ -29,7 +29,17 @@
 		}
 	}
 
-	@Override
+    @Override
+    public void convertForReducedNet(String templateName) {
+	    if(template.isEmpty()){
+            place = "Shared_" + place;
+        } else {
+            place = template + "_" + place;
+        }
+        template = templateName;
+    }
+
+    @Override
 	public TCTLAbstractStateProperty copy() {
 		return new TCTLPlaceNode(template, place);
 	}
 
=== modified file 'src/dk/aau/cs/TCTL/TCTLPlusListNode.java'
--- src/dk/aau/cs/TCTL/TCTLPlusListNode.java	2020-08-17 08:09:43 +0000
+++ src/dk/aau/cs/TCTL/TCTLPlusListNode.java	2020-12-17 21:03:24 +0000
@@ -36,7 +36,14 @@
 		}
 	}
 
-	@Override
+    @Override
+    public void convertForReducedNet(String templateName) {
+        for(TCTLAbstractProperty property : terms) {
+            property.convertForReducedNet(templateName);
+        }
+    }
+
+    @Override
 	public TCTLAbstractStateProperty copy() {
 		ArrayList<TCTLAbstractStateProperty> copy = new ArrayList<TCTLAbstractStateProperty>();
 		
 
=== modified file 'src/dk/aau/cs/TCTL/TCTLStatePlaceHolder.java'
--- src/dk/aau/cs/TCTL/TCTLStatePlaceHolder.java	2020-08-17 08:09:43 +0000
+++ src/dk/aau/cs/TCTL/TCTLStatePlaceHolder.java	2020-12-17 21:03:24 +0000
@@ -51,7 +51,11 @@
 		}
 	}
 
-	@Override
+    @Override
+    public void convertForReducedNet(String templateName) {
+    }
+
+    @Override
 	public void accept(ITCTLVisitor visitor, Object context) {
 		visitor.visit(this, context);
 
 
=== modified file 'src/dk/aau/cs/TCTL/TCTLStateToPathConverter.java'
--- src/dk/aau/cs/TCTL/TCTLStateToPathConverter.java	2020-08-17 08:09:43 +0000
+++ src/dk/aau/cs/TCTL/TCTLStateToPathConverter.java	2020-12-17 21:03:24 +0000
@@ -37,7 +37,12 @@
 		return children;
 	}
 
-	@Override
+    @Override
+    public void convertForReducedNet(String templateName) {
+        property.convertForReducedNet(templateName);
+    }
+
+    @Override
 	public boolean equals(Object o) {
 		if (o instanceof TCTLEFNode) {
 			TCTLEFNode node = (TCTLEFNode) o;
 
=== modified file 'src/dk/aau/cs/TCTL/TCTLTermListNode.java'
--- src/dk/aau/cs/TCTL/TCTLTermListNode.java	2020-08-17 08:09:43 +0000
+++ src/dk/aau/cs/TCTL/TCTLTermListNode.java	2020-12-17 21:03:24 +0000
@@ -36,7 +36,14 @@
 		}
 	}
 
-	@Override
+    @Override
+    public void convertForReducedNet(String templateName) {
+        for (TCTLAbstractProperty property : factors) {
+            property.convertForReducedNet(templateName);
+        }
+    }
+
+    @Override
 	public TCTLAbstractStateProperty copy() {
 		ArrayList<TCTLAbstractStateProperty> copy = new ArrayList<TCTLAbstractStateProperty>();
 
 
=== modified file 'src/dk/aau/cs/TCTL/TCTLTransitionNode.java'
--- src/dk/aau/cs/TCTL/TCTLTransitionNode.java	2020-08-17 08:09:43 +0000
+++ src/dk/aau/cs/TCTL/TCTLTransitionNode.java	2020-12-17 21:03:24 +0000
@@ -29,7 +29,13 @@
 		}
 	}
 
-	@Override
+    @Override
+    public void convertForReducedNet(String templateName) {
+        transition = template + "_" + transition;
+        template = templateName;
+    }
+
+    @Override
 	public TCTLAbstractStateProperty copy() {
 		return new TCTLTransitionNode(template, transition);
 	}
 
=== modified file 'src/dk/aau/cs/TCTL/TCTLTrueNode.java'
--- src/dk/aau/cs/TCTL/TCTLTrueNode.java	2020-08-17 08:09:43 +0000
+++ src/dk/aau/cs/TCTL/TCTLTrueNode.java	2020-12-17 21:03:24 +0000
@@ -18,7 +18,11 @@
 		}
 	}
 
-	@Override
+    @Override
+    public void convertForReducedNet(String templateName) {
+    }
+
+    @Override
 	public void accept(ITCTLVisitor visitor, Object context) {
 		visitor.visit(this, context);
 	}
 
=== modified file 'src/dk/aau/cs/verification/VerificationResult.java'
--- src/dk/aau/cs/verification/VerificationResult.java	2020-12-16 21:11:57 +0000
+++ src/dk/aau/cs/verification/VerificationResult.java	2020-12-17 21:03:24 +0000
@@ -180,6 +180,11 @@
 		}
 		return reductionStats.toString();
 	}
+
+	public boolean reductionRulesApplied(){
+        ReductionStats reductionStats = stats.getReductionStats();
+        return (reductionStats.getRemovedPlaces() + reductionStats.getRemovedTrantitions()) > 0;
+    }
 	
 	public NetworkMarking getCoveredMarking(TimedArcPetriNetNetwork model){
 		
 
=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java	2020-12-16 21:11:57 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java	2020-12-17 21:03:24 +0000
@@ -284,7 +284,7 @@
 			if(((VerifyTAPNOptions)options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model);
 			
 			VerifyPNExporter exporter = new VerifyPNExporter();
-			ExportedVerifyTAPNModel exportedModel = exporter.export(model.value1(), query, null);
+			ExportedVerifyTAPNModel exportedModel = exporter.export(model.value1(), query, null, model.value2());
 
 			if (exportedModel == null) {
 				messenger.displayErrorMessage("There was an error exporting the model");
@@ -314,8 +314,9 @@
 			((VerifyTAPNOptions)options).setInclusionPlaces(new InclusionPlaces(InclusionPlacesOption.UserSpecified, inclusionPlaces));
 		}
 
-		private VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, ExportedVerifyTAPNModel exportedModel, TAPNQuery query) {
+		private VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, ExportedVerifyTAPNModel exportedModel, TAPNQuery query) throws IOException {
 			((VerifyTAPNOptions)options).setTokensInModel(model.value1().marking().size()); // TODO: get rid of me
+
 			runner = new ProcessRunner(verifypnpath, createArgumentString(exportedModel.modelFile(), exportedModel.queryFile(), options));
 			runner.run();
 
 
=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java	2020-07-13 13:58:47 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java	2020-12-17 21:03:24 +0000
@@ -4,6 +4,7 @@
 import java.util.Map;
 
 import pipe.dataLayer.TAPNQuery.SearchOption;
+import pipe.dataLayer.TAPNQuery.QueryReductionTime;
 import pipe.dataLayer.TAPNQuery.TraceOption;
 import pipe.dataLayer.TAPNQuery.AlgorithmOption;
 import pipe.dataLayer.TAPNQuery.QueryCategory;
@@ -16,26 +17,28 @@
 	private final QueryCategory queryCategory;
 	private final AlgorithmOption algorithmOption;
 	private boolean useSiphontrap = false; 
-	private boolean useQueryReduction = true; 
+	private QueryReductionTime queryReductionTime;
 	private boolean useStubbornReduction = true;
+	private String pathToReducedNet;
 	
-	public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, ModelReduction modelReduction, 
-		boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, QueryCategory queryCategory, AlgorithmOption algorithmOption,
-		boolean siphontrap, boolean queryReduction, boolean stubbornReduction) {
+	public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, ModelReduction modelReduction,
+                           boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, QueryCategory queryCategory, AlgorithmOption algorithmOption,
+                           boolean siphontrap, QueryReductionTime queryReduction, boolean stubbornReduction, String pathToReducedNet) {
 		super(extraTokens, traceOption, search, true, useOverApproximation, false, new InclusionPlaces(), enableOverApproximation, enableUnderApproximation, approximationDenominator);
 		this.modelReduction = modelReduction;
 		this.queryCategory = queryCategory;
 		this.algorithmOption = algorithmOption;
 		this.useSiphontrap = siphontrap;
-		this.useQueryReduction = queryReduction;
+		this.queryReductionTime = queryReduction;
 		this.useStubbornReduction = stubbornReduction;
+		this.pathToReducedNet = pathToReducedNet;
 	}
 	
-	public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, boolean useModelReduction, 
-		boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, QueryCategory queryCategory, AlgorithmOption algorithmOption,
-		boolean siphontrap, boolean queryReduction, boolean stubbornReduction) {
+	public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, boolean useModelReduction,
+                           boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, QueryCategory queryCategory, AlgorithmOption algorithmOption,
+                           boolean siphontrap, QueryReductionTime queryReduction, boolean stubbornReduction) {
 		this(extraTokens, traceOption, search, useOverApproximation, useModelReduction? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION, enableOverApproximation, 
-			enableUnderApproximation, approximationDenominator,queryCategory, algorithmOption, siphontrap, queryReduction, stubbornReduction);
+			enableUnderApproximation, approximationDenominator,queryCategory, algorithmOption, siphontrap, queryReduction, stubbornReduction, null);
 	}
 
 	@Override
@@ -49,12 +52,16 @@
 		switch(getModelReduction()){
 		case AGGRESSIVE:
 			result.append(" -r 1 ");
+            String writeReducedCMD = " --write-reduced " +pathToReducedNet;
+            result.append(writeReducedCMD);
 			break;
 		case NO_REDUCTION:
 			result.append(" -r 0 ");
 			break;
 		case BOUNDPRESERVING:
 			result.append(" -r 2 ");
+            writeReducedCMD = " --write-reduced " +pathToReducedNet;
+            result.append(writeReducedCMD);
 			break;
 		default:
 			break;			
@@ -67,9 +74,12 @@
 		if (this.useSiphontrap) {
 			result.append(" -a 10 ");
 		}
-		if (!this.useQueryReduction) {
+		if (this.queryReductionTime == QueryReductionTime.NoTime) {
 			result.append(" -q 0 ");
-		}
+		} else if (this.queryReductionTime == QueryReductionTime.ShortestTime) {
+		    //Run query reduction for 1 second, to avoid conflict with -s OverApprox argument, but also still not run the verification.
+		    result.append(" -q 1");
+        }
 		if (!this.useStubbornReduction) {
 			result.append(" -p ");
 		}
 
=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java	2020-12-16 21:11:57 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java	2020-12-17 21:03:24 +0000
@@ -272,7 +272,7 @@
 		if(((VerifyTAPNOptions)options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model);
 		
 		VerifyTAPNExporter exporter = new VerifyTAPNExporter();
-		ExportedVerifyTAPNModel exportedModel = exporter.export(model.value1(), query, null);
+		ExportedVerifyTAPNModel exportedModel = exporter.export(model.value1(), query, null, model.value2());
 
 		if (exportedModel == null) {
 			messenger.displayErrorMessage("There was an error exporting the model");
 
=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java	2020-12-16 21:11:57 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java	2020-12-17 21:03:24 +0000
@@ -278,7 +278,7 @@
         }
 
 		VerifyTAPNExporter exporter = new VerifyTAPNExporter();
-		ExportedVerifyTAPNModel exportedModel = exporter.export(model.value1(), query, CreateGui.getCurrentTab().getLens());
+		ExportedVerifyTAPNModel exportedModel = exporter.export(model.value1(), query, CreateGui.getCurrentTab().getLens(), model.value2());
 
 		if (exportedModel == null) {
 			messenger.displayErrorMessage("There was an error exporting the model");
 
=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java	2020-12-14 17:13:30 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java	2020-12-17 21:03:24 +0000
@@ -4,8 +4,12 @@
 import java.io.FileNotFoundException;
 import java.io.IOException;
 import java.io.PrintStream;
+import java.util.Collection;
+import java.util.List;
 
 import dk.aau.cs.gui.TabContent;
+import dk.aau.cs.verification.NameMapping;
+import pipe.dataLayer.DataLayer;
 import pipe.dataLayer.TAPNQuery.QueryCategory;
 
 import dk.aau.cs.model.tapn.TAPNQuery;
@@ -18,9 +22,14 @@
 import dk.aau.cs.model.tapn.TransportArc;
 
 import dk.aau.cs.TCTL.visitors.CTLQueryVisitor;
+import pipe.gui.CreateGui;
+import pipe.gui.graphicElements.Place;
+import pipe.gui.graphicElements.Transition;
+
+import javax.xml.crypto.Data;
 
 public class VerifyTAPNExporter {
-	public ExportedVerifyTAPNModel export(TimedArcPetriNet model, TAPNQuery query, TabContent.TAPNLens lens) {
+	public ExportedVerifyTAPNModel export(TimedArcPetriNet model, TAPNQuery query, TabContent.TAPNLens lens, NameMapping mapping) {
 		File modelFile = createTempFile(".xml");
 		File queryFile;
 		if (query.getCategory() == QueryCategory.CTL){
@@ -28,19 +37,20 @@
 		} else {
 			queryFile = createTempFile(".q");
 		}
-		
-
-		return export(model, query, modelFile, queryFile, lens);
+
+		return export(model, query, modelFile, queryFile, null, lens, mapping);
+
 	}
 
-	public ExportedVerifyTAPNModel export(TimedArcPetriNet model, TAPNQuery query, File modelFile, File queryFile, TabContent.TAPNLens lens) {
+
+	public ExportedVerifyTAPNModel export(TimedArcPetriNet model, TAPNQuery query, File modelFile, File queryFile, pipe.dataLayer.TAPNQuery dataLayerQuery, TabContent.TAPNLens lens, NameMapping mapping) {
 		if (modelFile == null || queryFile == null)
 			return null;
 
 		try{
 			PrintStream modelStream = new PrintStream(modelFile);
 
-			outputModel(model, modelStream);
+			outputModel(model, modelStream, mapping);
 			modelStream.close();
 
 			PrintStream queryStream = new PrintStream(queryFile);
@@ -62,15 +72,17 @@
 		return new ExportedVerifyTAPNModel(modelFile.getAbsolutePath(), queryFile.getAbsolutePath());
 	}
 	
-	private void outputModel(TimedArcPetriNet model, PrintStream modelStream) {
+	private void outputModel(TimedArcPetriNet model, PrintStream modelStream, NameMapping mapping) {
+        Collection<DataLayer> guiModels = CreateGui.getCurrentTab().getGuiModels().values();
+
 		modelStream.append("<pnml>\n");
 		modelStream.append("<net id=\"" + model.name() + "\" type=\"P/T net\">\n");
 		
 		for(TimedPlace p : model.places())
-			outputPlace(p, modelStream);
+			outputPlace(p, modelStream, guiModels, mapping);
 		
 		for(TimedTransition t : model.transitions())
-			outputTransition(t,modelStream);
+			outputTransition(t,modelStream, guiModels, mapping);
 		
 		for(TimedInputArc inputArc : model.inputArcs())
 			outputInputArc(inputArc, modelStream);
@@ -88,28 +100,63 @@
 		modelStream.append("</pnml>");
 	}
 	
-	private void outputPlace(TimedPlace p, PrintStream modelStream) {
+	private void outputPlace(TimedPlace p, PrintStream modelStream, Collection<DataLayer> guiModels, NameMapping mapping) {
+        //remove the net prefix from the place name
+        String placeName = mapping.map(p.name()).value2();
+        Place guiPlace = null;
+
+        for(DataLayer guiModel : guiModels ){
+            guiPlace = guiModel.getPlaceById(placeName);
+            if(guiPlace != null){
+                break;
+            }
+        }
+
 		modelStream.append("<place ");
 		
 		modelStream.append("id=\"" + p.name() + "\" ");
 		modelStream.append("name=\"" + p.name() + "\" ");
 		modelStream.append("invariant=\"" + p.invariant().toString(false).replace("<", "&lt;") + "\" ");
 		modelStream.append("initialMarking=\"" + p.numberOfTokens() + "\" ");
-		
-		modelStream.append("/>\n");
+        modelStream.append(">\n");
+        outputPosition(modelStream, guiPlace.getPositionX(), guiPlace.getPositionY());
+
+        modelStream.append("</place>\n");
 	}
 
-	private void outputTransition(TimedTransition t, PrintStream modelStream) {
+    private void outputTransition(TimedTransition t, PrintStream modelStream, Collection<DataLayer> guiModels, NameMapping mapping) {
+        //remove the net prefix from the transition name
+	    String transitionName = mapping.map(t.name()).value2();
+        Transition guiTransition = null;
+
+        for(DataLayer guiModel : guiModels){
+	        guiTransition = guiModel.getTransitionById(transitionName);
+	        if(guiTransition != null){
+	            break;
+            }
+        }
+
 		modelStream.append("<transition ");
 
         modelStream.append("player=\"" + (t.isUncontrollable() ? "1" : "0") + "\" ");
         modelStream.append("id=\"" + t.name() + "\" ");
 		modelStream.append("name=\"" + t.name() + "\" ");
-		modelStream.append("urgent=\"" + (t.isUrgent()? "true":"false") + "\"");
-		
-		modelStream.append("/>\n");
+        modelStream.append("urgent=\"" + (t.isUrgent()? "true":"false") + "\"");
+        modelStream.append(">\n");
+        outputPosition(modelStream, guiTransition.getPositionX(), guiTransition.getPositionY());
+
+        modelStream.append("</transition>\n");
 	}
 
+    private void outputPosition(PrintStream modelStream, int positionX, int positionY) {
+        modelStream.append("<graphics>");
+        modelStream.append("<position ");
+        modelStream.append("x=\"" + positionX + "\" ");
+        modelStream.append("y=\"" + positionY + "\" ");
+        modelStream.append("/>");
+        modelStream.append("</graphics>");
+    }
+
 	protected void outputInputArc(TimedInputArc inputArc, PrintStream modelStream) {
 		modelStream.append("<inputArc ");
 		
 
=== modified file 'src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java'
--- src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java	2020-07-13 13:58:47 +0000
+++ src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java	2020-12-17 21:03:24 +0000
@@ -8,6 +8,7 @@
 import pipe.dataLayer.TAPNQuery.SearchOption;
 import pipe.dataLayer.TAPNQuery.TraceOption;
 import pipe.dataLayer.TAPNQuery.WorkflowMode;
+import pipe.dataLayer.TAPNQuery.QueryReductionTime;
 import pipe.gui.CreateGui;
 import pipe.gui.FileFinder;
 import pipe.gui.MessengerImpl;
@@ -307,7 +308,7 @@
 					}
 					long c  = m*B+1;
 					queryToVerify.setStrongSoundnessBound(c);
-					Verifier.runVerifyTAPNVerification(model.network(), queryToVerify, new VerificationCallback() {
+					Verifier.runVerifyTAPNVerification(model.network(), queryToVerify, false, new VerificationCallback() {
 						
 						@Override
 						public void run(VerificationResult<TAPNNetworkTrace> result) {
@@ -575,7 +576,7 @@
 		TAPNQuery queryToVerify = getTAPNQuery(composedModel.value1(),query);
 		queryToVerify.setCategory(query.getCategory());
 		MapQueryToNewNames(queryToVerify, composedModel.value2());
-		
+
 		TAPNQuery clonedQuery = new TAPNQuery(query.getProperty().copy(), queryToVerify.getExtraTokens());
 		clonedQuery.setCategory(query.getCategory());
 		MapQueryToNewNames(clonedQuery, composedModel.value2());
@@ -622,9 +623,9 @@
 			return new VerifyDTAPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), query.useSymmetry(), query.useGCD(), query.useTimeDarts(), query.usePTrie(), false,  query.discreteInclusion(), query.inclusionPlaces(), query.getWorkflowMode(), 0, query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator(), query.isStubbornReductionEnabled());
 		else if(query.getReductionOption() == ReductionOption.VerifyPN || query.getReductionOption() == ReductionOption.VerifyPNApprox || query.getReductionOption() == ReductionOption.VerifyPNReduce)
 			if (batchProcessingVerificationOptions.queryPropertyOption() == QueryPropertyOption.SearchWholeStateSpace){
-			    return new VerifyPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), false, false, false, false, query.approximationDenominator(), QueryCategory.Default, query.getAlgorithmOption(), false, false, false);
+			    return new VerifyPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), false, false, false, false, query.approximationDenominator(), QueryCategory.Default, query.getAlgorithmOption(), false, QueryReductionTime.UnlimitedTime, false);
 			} else {
-			    return new VerifyPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), query.useOverApproximation(), query.useReduction(), query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator(), query.getCategory(), query.getAlgorithmOption(), query.isSiphontrapEnabled(), query.isQueryReductionEnabled(), query.isStubbornReductionEnabled());
+			    return new VerifyPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), query.useOverApproximation(), query.useReduction(), query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator(), query.getCategory(), query.getAlgorithmOption(), query.isSiphontrapEnabled(), query.isQueryReductionEnabled()? QueryReductionTime.UnlimitedTime: QueryReductionTime.NoTime, query.isStubbornReductionEnabled());
 			}
 		else
 			return new VerifytaOptions(TraceOption.NONE, query.getSearchOption(), false, query.getReductionOption(), query.useSymmetry(), false, query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator());
 
=== modified file 'src/net/tapaal/TAPAAL.java'
--- src/net/tapaal/TAPAAL.java	2020-05-21 08:51:39 +0000
+++ src/net/tapaal/TAPAAL.java	2020-12-17 21:03:24 +0000
@@ -148,7 +148,7 @@
 					System.out.println("    | Running query: " + query.getName());
 
 					if(query.getReductionOption() == ReductionOption.VerifyTAPN || query.getReductionOption() == ReductionOption.VerifyTAPNdiscreteVerification || query.getReductionOption() == ReductionOption.VerifyPN) {
-						Verifier.runVerifyTAPNVerification(network, query, new VerificationCallback() {
+						Verifier.runVerifyTAPNVerification(network, query, false, new VerificationCallback() {
 							@Override
 							public void run(VerificationResult<TAPNNetworkTrace> result) {
 
 
=== modified file 'src/pipe/dataLayer/TAPNQuery.java'
--- src/pipe/dataLayer/TAPNQuery.java	2020-08-20 07:26:04 +0000
+++ src/pipe/dataLayer/TAPNQuery.java	2020-12-17 21:03:24 +0000
@@ -16,6 +16,10 @@
 		BFS, DFS, RANDOM, BatchProcessingKeepQueryOption, HEURISTIC, OVERAPPROXIMATE, DEFAULT
 	}
 
+	public enum QueryReductionTime {
+	    NoTime, ShortestTime, UnlimitedTime
+    }
+
 	public enum HashTableSize {
 		MB_4, MB_16, MB_64, MB_256, MB_512
 	}
@@ -430,4 +434,10 @@
         }
         return false;
     }
+
+    public TAPNQuery convertPropertyForReducedNet(String templateName){
+	    TAPNQuery convertedQuery = copy();
+	    convertedQuery.property.convertForReducedNet(templateName);
+        return  convertedQuery;
+    }
 }
 
=== modified file 'src/pipe/gui/Export.java'
--- src/pipe/gui/Export.java	2020-12-14 17:13:30 +0000
+++ src/pipe/gui/Export.java	2020-12-17 21:03:24 +0000
@@ -147,9 +147,9 @@
             i++;
 
             if (lens.isGame() && isDTAPN) {
-                exporter.export(model, new dk.aau.cs.model.tapn.TAPNQuery(query.getProperty(), 0), new File(modelFile), new File(queryFile + i + ".q"), lens);
+                exporter.export(model, new dk.aau.cs.model.tapn.TAPNQuery(query.getProperty(), 0), new File(modelFile), new File(queryFile + i + ".q"), null, lens, transformedModel.value2());
             } else {
-                exporter.export(model, new dk.aau.cs.model.tapn.TAPNQuery(query.getProperty(), 0), new File(modelFile), new File(queryFile + i + ".q"), new TabContent.TAPNLens(true, false));
+                exporter.export(model, new dk.aau.cs.model.tapn.TAPNQuery(query.getProperty(), 0), new File(modelFile), new File(queryFile + i + ".q"), null ,new TabContent.TAPNLens(true, false), transformedModel.value2());
             }
         }
     }
 
=== modified file 'src/pipe/gui/KBoundAnalyzer.java'
--- src/pipe/gui/KBoundAnalyzer.java	2020-07-13 13:58:47 +0000
+++ src/pipe/gui/KBoundAnalyzer.java	2020-12-17 21:03:24 +0000
@@ -52,7 +52,7 @@
 
 	protected VerifyTAPNOptions verificationOptions() {
 		if(modelChecker instanceof VerifyPN){
-			return new VerifyPNOptions(k, TraceOption.NONE, SearchOption.BFS, false, ModelReduction.BOUNDPRESERVING, false, false, 1, QueryCategory.Default, AlgorithmOption.CERTAIN_ZERO, false, false, false);
+			return new VerifyPNOptions(k, TraceOption.NONE, SearchOption.BFS, false, ModelReduction.BOUNDPRESERVING, false, false, 1, QueryCategory.Default, AlgorithmOption.CERTAIN_ZERO, false, pipe.dataLayer.TAPNQuery.QueryReductionTime.UnlimitedTime, false, null);
 		} else if(modelChecker instanceof VerifyTAPN){
 			return new VerifyTAPNOptions(k, TraceOption.NONE, SearchOption.BFS, true, false, true, false, false, 1);
 		} else if(modelChecker instanceof VerifyTAPNDiscreteVerification){
 
=== modified file 'src/pipe/gui/RunVerification.java'
--- src/pipe/gui/RunVerification.java	2020-12-16 21:11:57 +0000
+++ src/pipe/gui/RunVerification.java	2020-12-17 21:03:24 +0000
@@ -6,8 +6,11 @@
 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.List;
 
@@ -15,29 +18,30 @@
 import javax.swing.table.DefaultTableModel;
 import javax.swing.table.TableModel;
 import javax.swing.table.TableRowSorter;
-
+import dk.aau.cs.gui.TabContent;
+import dk.aau.cs.verification.*;
 import dk.aau.cs.Messenger;
 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 pipe.dataLayer.TAPNQuery;
 
 public class RunVerification extends RunVerificationBase {	
 	private final IconSelector iconSelector;
 	private final VerificationCallback callback;
-	public RunVerification(ModelChecker modelChecker, IconSelector selector, Messenger messenger, VerificationCallback callback) {
-		super(modelChecker, messenger);
+	public RunVerification(ModelChecker modelChecker, IconSelector selector, Messenger messenger, VerificationCallback callback, String reducedNetFilePath, boolean reduceNetOnly) {
+		super(modelChecker, messenger, reducedNetFilePath, reduceNetOnly);
 		iconSelector = selector;
 		this.callback = callback;
 	}
+
+    public RunVerification(ModelChecker modelChecker, IconSelector selector, Messenger messenger, VerificationCallback callback) {
+        this(modelChecker, selector, messenger, callback, null, false);
+    }
 	
 	public RunVerification(ModelChecker modelChecker, IconSelector selector, Messenger messenger) {
-		this(modelChecker, selector, messenger, null);
+		this(modelChecker, selector, messenger, null, null, false);
 	}
 
 	@Override
@@ -54,12 +58,14 @@
 						iconSelector.getIconFor(result)
 				);
 	
-				if (result.getTrace() != null) {
+				if (!reducedNetOpened && result.getTrace() != null) {
 					CreateGui.getAnimator().setTrace(result.getTrace());
 				}
 			}
 
-		}else{
+		} else if(reduceNetOnly) {
+            //If the engine is only called to produce a reduced net, it will fail, but no error message should be shown
+        }else{
 			
 			//Check if the is something like 
 			//verifyta: relocation_error:
@@ -116,7 +122,6 @@
 
     }
 
-
 	private JPanel createStatisticsPanel(final VerificationResult<TAPNNetworkTrace> result, boolean transitionPanel) {
 		JPanel headLinePanel = new JPanel(new GridBagLayout());
 		final JPanel fullPanel = new JPanel(new GridBagLayout());
@@ -311,13 +316,46 @@
 			}
 			
 			if(!result.getReductionResultAsString().isEmpty()){
-				JLabel reductionStatsLabet = new JLabel(toHTML(result.getReductionResultAsString()));
+				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;
-				panel.add(reductionStatsLabet, gbc);
+
+				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 {
+                                    TabContent reducedNetTab = TabContent.createNewTabFromPNMLFile(reducedNetFile);
+                                    reducedNetTab.setInitialName("reduced-" + CreateGui.getAppGui().getCurrentTabName());
+                                    TAPNQuery convertedQuery = dataLayerQuery.convertPropertyForReducedNet(reducedNetTab.currentTemplate().toString());
+                                    reducedNetTab.addQuery(convertedQuery);
+                                    CreateGui.openNewTabFromStream(reducedNetTab);
+                                } catch (Exception e1){
+                                    JOptionPane.showMessageDialog(CreateGui.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;
+                    panel.add(openReducedButton, gbc);
+                }
 			}
             if (result.getRawOutput() != null) {
                 JButton showRawQueryButton = new JButton("Show raw query results");
@@ -325,9 +363,9 @@
                         JOptionPane.showMessageDialog(panel, createRawQueryPanel(result.getRawOutput()), "Raw query results", JOptionPane.INFORMATION_MESSAGE);
                 });
                 gbc = new GridBagConstraints();
-                gbc.gridx = 0;
+                gbc.gridx = 1;
                 gbc.gridy = 5;
-                gbc.insets = new Insets(10,0,10,0);
+                gbc.insets = new Insets(0,0,10,0);
                 gbc.anchor = GridBagConstraints.WEST;
                 panel.add(showRawQueryButton, gbc);
             }
 
=== modified file 'src/pipe/gui/RunVerificationBase.java'
--- src/pipe/gui/RunVerificationBase.java	2020-08-27 07:27:30 +0000
+++ src/pipe/gui/RunVerificationBase.java	2020-12-17 21:03:24 +0000
@@ -1,5 +1,6 @@
 package pipe.gui;
 
+import java.io.File;
 import java.util.concurrent.ExecutionException;
 
 import javax.swing.SwingUtilities;
@@ -39,16 +40,25 @@
 	protected TimedArcPetriNetNetwork model;
 	protected TAPNQuery query;
 	protected pipe.dataLayer.TAPNQuery dataLayerQuery;
+	protected String reducedNetFilePath;
+	protected boolean reduceNetOnly;
+	protected boolean reducedNetOpened = false;
 	
 	
 	protected Messenger messenger;
 
-	public RunVerificationBase(ModelChecker modelChecker, Messenger messenger) {
+	public RunVerificationBase(ModelChecker modelChecker, Messenger messenger, String reducedNetFilePath, boolean reduceNetOnly) {
 		super();
 		this.modelChecker = modelChecker;
 		this.messenger = messenger;
+		this.reducedNetFilePath = reducedNetFilePath;
+		this.reduceNetOnly = reduceNetOnly;
 	}
 
+    public RunVerificationBase(ModelChecker modelChecker, Messenger messenger) {
+        this(modelChecker, messenger, null, false);
+    }
+
 	
 	public void execute(VerificationOptions options, TimedArcPetriNetNetwork model, TAPNQuery query, pipe.dataLayer.TAPNQuery dataLayerQuery) {
 		this.model = model;
@@ -110,8 +120,9 @@
 										dataLayerQuery.getCategory(),
 										dataLayerQuery.getAlgorithmOption(),
 										dataLayerQuery.isSiphontrapEnabled(),
-										dataLayerQuery.isQueryReductionEnabled(),
-										dataLayerQuery.isStubbornReductionEnabled()
+										dataLayerQuery.isQueryReductionEnabled()? pipe.dataLayer.TAPNQuery.QueryReductionTime.UnlimitedTime: pipe.dataLayer.TAPNQuery.QueryReductionTime.NoTime,
+										dataLayerQuery.isStubbornReductionEnabled(),
+                                        reducedNetFilePath
 								),
 								transformedModel,
 								clonedQuery
@@ -130,8 +141,9 @@
 										pipe.dataLayer.TAPNQuery.QueryCategory.Default,
 										pipe.dataLayer.TAPNQuery.AlgorithmOption.CERTAIN_ZERO,
 										false,
-										true,
-										false
+                                        pipe.dataLayer.TAPNQuery.QueryReductionTime.UnlimitedTime,
+										false,
+                                        reducedNetFilePath
 								),
 								transformedModel,
 								clonedQuery
 
=== modified file 'src/pipe/gui/Verifier.java'
--- src/pipe/gui/Verifier.java	2020-07-06 11:57:37 +0000
+++ src/pipe/gui/Verifier.java	2020-12-17 21:03:24 +0000
@@ -15,6 +15,9 @@
 import dk.aau.cs.verification.UPPAAL.Verifyta;
 import dk.aau.cs.verification.UPPAAL.VerifytaOptions;
 
+import java.io.File;
+import java.io.IOException;
+
 /**
  * Implementes af class for handling integrated Uppaal Verification
  * 
@@ -24,6 +27,8 @@
  */
 
 public class Verifier {
+    private static File reducedNetTempFile = null;
+
 	private static Verifyta getVerifyta() {
 		Verifyta verifyta = new Verifyta(new FileFinder(), new MessengerImpl());
 		verifyta.setup();
@@ -61,6 +66,10 @@
 		}
 	}
 
+	public static String getReducedNetFilePath() {
+	    return reducedNetTempFile.getAbsolutePath();
+    }
+
 	public static void analyzeKBound(TimedArcPetriNetNetwork tapnNetwork, int k, JSpinner tokensControl) {
 		ModelChecker modelChecker;
 		
@@ -129,10 +138,12 @@
 	public static void runVerifyTAPNVerification(
 			TimedArcPetriNetNetwork tapnNetwork,
 			TAPNQuery query,
+            boolean onlyCreateReducedNet,
 			VerificationCallback callback
 	) {
 		ModelChecker verifytapn = getModelChecker(query);
 
+
 		if (!verifytapn.isCorrectVersion()) {
 			new MessengerImpl().displayErrorMessage(
 					"No "+verifytapn+" specified: The verification is cancelled",
@@ -165,21 +176,53 @@
 					query.isStubbornReductionEnabled()
 			);
 		} else if(query.getReductionOption() == ReductionOption.VerifyPN){
-			verifytapnOptions = new VerifyPNOptions(
-					bound,
-					query.getTraceOption(),
-					query.getSearchOption(),
-					query.useOverApproximation(),
-					query.useReduction()? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION,
-					query.isOverApproximationEnabled(),
-					query.isUnderApproximationEnabled(),
-					query.approximationDenominator(),
-					query.getCategory(),
-					query.getAlgorithmOption(),
-					query.isSiphontrapEnabled(),
-					query.isQueryReductionEnabled(),
-					query.isStubbornReductionEnabled()
-			);
+
+            try {
+                reducedNetTempFile = File.createTempFile("reduced-", ".pnml");
+            } catch (IOException e) {
+                new MessengerImpl().displayErrorMessage(
+                    e.getMessage(),
+                    "Error");
+                return;
+            }
+
+            if (onlyCreateReducedNet) {
+                //These options should disable the verification and only produce the net after applying reduction rules
+                verifytapnOptions = new VerifyPNOptions(
+                    bound,
+                    query.getTraceOption(),
+                    TAPNQuery.SearchOption.OVERAPPROXIMATE,
+                    query.useOverApproximation(),
+                    query.useReduction()? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION,
+                    query.isOverApproximationEnabled(),
+                    query.isUnderApproximationEnabled(),
+                    query.approximationDenominator(),
+                    query.getCategory(),
+                    query.getAlgorithmOption(),
+                    query.isSiphontrapEnabled(),
+                    TAPNQuery.QueryReductionTime.NoTime,
+                    query.isStubbornReductionEnabled(),
+                    reducedNetTempFile.getAbsolutePath()
+                );
+            } else {
+                verifytapnOptions = new VerifyPNOptions(
+                    bound,
+                    query.getTraceOption(),
+                    query.getSearchOption(),
+                    query.useOverApproximation(),
+                    query.useReduction()? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION,
+                    query.isOverApproximationEnabled(),
+                    query.isUnderApproximationEnabled(),
+                    query.approximationDenominator(),
+                    query.getCategory(),
+                    query.getAlgorithmOption(),
+                    query.isSiphontrapEnabled(),
+                    query.isQueryReductionEnabled()? TAPNQuery.QueryReductionTime.UnlimitedTime: TAPNQuery.QueryReductionTime.NoTime,
+                    query.isStubbornReductionEnabled(),
+                    reducedNetTempFile.getAbsolutePath()
+                );
+            }
+
 		} else {
 			verifytapnOptions = new VerifyTAPNOptions(
 					bound,
@@ -200,7 +243,13 @@
 		}
 		
 		if (tapnNetwork != null) {
-			RunVerificationBase thread = new RunVerification(verifytapn, new VerifyTAPNIconSelector(), new MessengerImpl(), callback);
+            RunVerificationBase thread;
+		    if (reducedNetTempFile != null) {
+                 thread = new RunVerification(verifytapn, new VerifyTAPNIconSelector(), new MessengerImpl(), callback, reducedNetTempFile.getAbsolutePath(), onlyCreateReducedNet );
+            } else {
+                thread = new RunVerification(verifytapn, new VerifyTAPNIconSelector(), new MessengerImpl(), callback);
+            }
+
 			RunningVerificationDialog dialog = new RunningVerificationDialog(CreateGui.getApp(), thread);
 			thread.execute(verifytapnOptions, tapnNetwork, new dk.aau.cs.model.tapn.TAPNQuery(query.getProperty(), bound), query);
 			dialog.setVisible(true);
 
=== modified file 'src/pipe/gui/widgets/QueryDialog.java'
--- src/pipe/gui/widgets/QueryDialog.java	2020-12-14 17:13:30 +0000
+++ src/pipe/gui/widgets/QueryDialog.java	2020-12-17 21:03:24 +0000
@@ -17,10 +17,7 @@
 import java.util.Vector;
 
 import javax.swing.*;
-import javax.swing.event.DocumentEvent;
-import javax.swing.event.DocumentListener;
-import javax.swing.event.UndoableEditEvent;
-import javax.swing.event.UndoableEditListener;
+import javax.swing.event.*;
 import javax.swing.text.MutableAttributeSet;
 import javax.swing.text.SimpleAttributeSet;
 import javax.swing.text.StyleConstants;
@@ -70,6 +67,7 @@
 	private static final String EXPORT_VERIFYTAPN_BTN_TEXT = "Export TAPAAL XML";
 	private static final String EXPORT_VERIFYPN_BTN_TEXT = "Export PN XML";
 	private static final String EXPORT_COMPOSED_BTN_TEXT = "Merge net components";
+    private static final String OPEN_REDUCED_BTN_TEXT = "Open reduced net";
 
 	private static final String UPPAAL_SOME_TRACE_STRING = "Some trace       ";
 	private static final String SOME_TRACE_STRING = "Some trace       ";
@@ -183,6 +181,7 @@
 	private JButton saveAndVerifyButton;
 	private JButton saveUppaalXMLButton;
 	private JButton mergeNetComponentsButton;
+	private JButton openReducedNetButton;
 
 	// Private Members
 	private StringPosition currentSelection = null;
@@ -313,6 +312,7 @@
 	private final static String TOOL_TIP_CANCEL_BUTTON = "Cancel the changes made in this dialog.";
 	private final static String TOOL_TIP_SAVE_UPPAAL_BUTTON = "Export an xml file that can be opened in UPPAAL GUI.";
 	private final static String TOOL_TIP_SAVE_COMPOSED_BUTTON = "Export an xml file of composed net and approximated net if enabled";
+	private final static String TOOL_TIP_OPEN_REDUCED_BUTTON = "Open the net produced after applying structural reduction rules";
 	private final static String TOOL_TIP_SAVE_TAPAAL_BUTTON = "Export an xml file that can be used as input for the TAPAAL engine.";
 	private final static String TOOL_TIP_SAVE_PN_BUTTON = "Export an xml file that can be used as input for the untimed Petri net engine.";
 
@@ -676,7 +676,7 @@
             current = ((TCTLStateToPathConverter) current).getProperty();
         }
         if (current instanceof TCTLAtomicPropositionNode) {
-			TCTLAtomicPropositionNode node = (TCTLAtomicPropositionNode) currentSelection.getObject();
+			TCTLAtomicPropositionNode node = (TCTLAtomicPropositionNode) current;
 
 			// bit of a hack to prevent posting edits to the undo manager when
 			// we programmatically change the selection in the atomic proposition comboboxes etc.
@@ -811,11 +811,13 @@
 			saveAndVerifyButton.setEnabled(isQueryOk);
 			saveUppaalXMLButton.setEnabled(isQueryOk);
 			mergeNetComponentsButton.setEnabled(isQueryOk);
+            openReducedNetButton.setEnabled(isQueryOk && useReduction.isSelected());
 		} else {
 			saveButton.setEnabled(false);
 			saveAndVerifyButton.setEnabled(false);
 			saveUppaalXMLButton.setEnabled(false);
 			mergeNetComponentsButton.setEnabled(false);
+            openReducedNetButton.setEnabled(false);
 		}
 	}
 
@@ -1454,9 +1456,12 @@
 		if (lens.isTimed() || lens.isGame()) {
 		    saveUppaalXMLButton.setVisible(advancedView);
 		    overApproximationOptionsPanel.setVisible(advancedView);
+        } else if (!lens.isGame()){
+            openReducedNetButton.setVisible(advancedView);
         }
 		mergeNetComponentsButton.setVisible(advancedView);
 
+
 		if(advancedView){
 			advancedButton.setText("Simple view");
 			advancedButton.setToolTipText(TOOL_TIP_SIMPLE_VIEW_BUTTON);
@@ -2679,6 +2684,13 @@
         if (lens.isTimed() || lens.isGame()) {
             initTimedReductionOptions();
         } else {
+            useReduction.addActionListener(new ActionListener() {
+                @Override
+                public void actionPerformed(ActionEvent actionEvent) {
+                        openReducedNetButton.setEnabled(useReduction.isSelected() && getQueryComment().length() > 0
+                            && !newProperty.containsPlaceHolder());
+                }
+            });
             initUntimedReductionOptions();
         }
 
@@ -2962,6 +2974,10 @@
 			mergeNetComponentsButton = new JButton(EXPORT_COMPOSED_BTN_TEXT);
 			mergeNetComponentsButton.setVisible(false);
 
+			openReducedNetButton = new JButton(OPEN_REDUCED_BTN_TEXT);
+            openReducedNetButton.setVisible(false);
+
+
 			saveUppaalXMLButton = new JButton(EXPORT_UPPAAL_BTN_TEXT);
 			//Only show in advanced mode
 			saveUppaalXMLButton.setVisible(false);
@@ -2972,6 +2988,7 @@
 			cancelButton.setToolTipText(TOOL_TIP_CANCEL_BUTTON);
 			saveUppaalXMLButton.setToolTipText(TOOL_TIP_SAVE_UPPAAL_BUTTON);
 			mergeNetComponentsButton.setToolTipText(TOOL_TIP_SAVE_COMPOSED_BUTTON);
+            openReducedNetButton.setToolTipText(TOOL_TIP_OPEN_REDUCED_BUTTON);
 
 			saveButton.addActionListener(new ActionListener() {
 				public void actionPerformed(ActionEvent evt) {
@@ -2995,7 +3012,7 @@
 						TAPNQuery query = getQuery();
 
 						if(query.getReductionOption() == ReductionOption.VerifyTAPN || query.getReductionOption() == ReductionOption.VerifyTAPNdiscreteVerification || query.getReductionOption() == ReductionOption.VerifyPN)
-							Verifier.runVerifyTAPNVerification(tapnNetwork, query, null);
+							Verifier.runVerifyTAPNVerification(tapnNetwork, query, false, null);
 						else
 							Verifier.runUppaalVerification(tapnNetwork, query);
 					}}
@@ -3049,10 +3066,12 @@
                         }
 						if(reduction == ReductionOption.VerifyTAPN || reduction == ReductionOption.VerifyTAPNdiscreteVerification) {
 							VerifyTAPNExporter exporter = new VerifyTAPNExporter();
-							exporter.export(transformedModel.value1(), clonedQuery, new File(xmlFile), new File(queryFile), lens);
+							exporter.export(transformedModel.value1(), clonedQuery, new File(xmlFile), new File(queryFile), tapnQuery, lens, transformedModel.value2());
+
 						} else if(reduction == ReductionOption.VerifyPN){
 							VerifyPNExporter exporter = new VerifyPNExporter();
-							exporter.export(transformedModel.value1(), clonedQuery, new File(xmlFile), new File(queryFile), lens);
+							exporter.export(transformedModel.value1(), clonedQuery, new File(xmlFile), new File(queryFile), tapnQuery, lens, transformedModel.value2());
+
 						} else {
 							UppaalExporter exporter = new UppaalExporter();
 							try {
@@ -3117,6 +3136,51 @@
 				}
 			});
 
+            openReducedNetButton.addActionListener(new ActionListener() {
+                public void actionPerformed(ActionEvent e) {
+
+
+                    if (checkIfSomeReductionOption()) {
+                        querySaved = true;
+                        // Now if a query is saved and verified, the net is marked as modified
+                        CreateGui.getCurrentTab().setNetChanged(true);
+
+                        TAPNQuery query = getQuery();
+                        if(query.getReductionOption() != ReductionOption.VerifyPN) {
+                            JOptionPane.showMessageDialog(CreateGui.getApp(),
+                                "The selected verification engine does not support application of reduction rules",
+                                "Reduction rules unsupported", JOptionPane.ERROR_MESSAGE);
+                            return;
+                        }
+
+                        exit();
+
+                        Verifier.runVerifyTAPNVerification(tapnNetwork, query,true, null);
+
+                        File reducedNetFile = new File(Verifier.getReducedNetFilePath());
+
+                        if(reducedNetFile.exists() && reducedNetFile.isFile() && reducedNetFile.canRead()){
+                            try {
+                                TabContent reducedNetTab = TabContent.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-" + CreateGui.getAppGui().getCurrentTabName());
+                                    TAPNQuery convertedQuery = query.convertPropertyForReducedNet(reducedNetTab.currentTemplate().toString());
+                                    reducedNetTab.addQuery(convertedQuery);
+                                    CreateGui.openNewTabFromStream(reducedNetTab);
+                                }
+                            } catch (Exception e1){
+                                JOptionPane.showMessageDialog(CreateGui.getApp(),
+                                    e1.getMessage(),
+                                    "Error loading reduced net file",
+                                    JOptionPane.ERROR_MESSAGE);
+                            }
+                        }
+                    }
+                }
+            });
+
 
 		} else if (option == QueryDialogueOption.Export) {
 			saveButton = new JButton("export");
@@ -3133,6 +3197,7 @@
 			JPanel leftButtomPanel = new JPanel(new FlowLayout());
 			JPanel rightButtomPanel = new JPanel(new FlowLayout());
 			leftButtomPanel.add(mergeNetComponentsButton, FlowLayout.LEFT);
+			leftButtomPanel.add(openReducedNetButton, FlowLayout.LEFT);
 			leftButtomPanel.add(saveUppaalXMLButton, FlowLayout.LEFT);
 
 
 
=== modified file 'src/pipe/gui/widgets/QueryPane.java'
--- src/pipe/gui/widgets/QueryPane.java	2020-08-20 07:30:52 +0000
+++ src/pipe/gui/widgets/QueryPane.java	2020-12-17 21:03:24 +0000
@@ -440,7 +440,7 @@
 		
 		if(NumberOfSelectedElements == 1) {
 			if(query.getReductionOption() == ReductionOption.VerifyTAPN || query.getReductionOption() == ReductionOption.VerifyTAPNdiscreteVerification || query.getReductionOption() == ReductionOption.VerifyPN)
-				Verifier.runVerifyTAPNVerification(tabContent.network(), query, null);
+				Verifier.runVerifyTAPNVerification(tabContent.network(), query, false, null);
 			else
 				Verifier.runUppaalVerification(tabContent.network(), query);
 		}
 
=== modified file 'src/pipe/gui/widgets/WorkflowDialog.java'
--- src/pipe/gui/widgets/WorkflowDialog.java	2020-07-20 07:19:51 +0000
+++ src/pipe/gui/widgets/WorkflowDialog.java	2020-12-17 21:03:24 +0000
@@ -1010,7 +1010,7 @@
 						WorkflowMode.WORKFLOW_STRONG_SOUNDNESS,
 						c
 				);
-				Verifier.runVerifyTAPNVerification(model, q, result -> {
+				Verifier.runVerifyTAPNVerification(model, q, false, result -> {
 					if(result.isQuerySatisfied()){
 
 						switch(((TimedTAPNNetworkTrace) result.getTrace()).getTraceType()){
@@ -1115,7 +1115,7 @@
                     ExtrapolationOption.AUTOMATIC,
                     WorkflowMode.WORKFLOW_SOUNDNESS
             );
-            Verifier.runVerifyTAPNVerification(model, q, new VerificationCallback() {
+            Verifier.runVerifyTAPNVerification(model, q, false, new VerificationCallback() {
 
                 @Override
                 public void run(VerificationResult<TAPNNetworkTrace> result) {
@@ -1225,7 +1225,7 @@
                             null,
                             ExtrapolationOption.AUTOMATIC
                     );
-                    Verifier.runVerifyTAPNVerification(model, q, new VerificationCallback() {
+                    Verifier.runVerifyTAPNVerification(model, q, false, new VerificationCallback() {
 
                         @Override
                         public void run(VerificationResult<TAPNNetworkTrace> result) {