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

Proposed by Thomas Pedersen
Status: Merged
Approved by: Jiri Srba
Approved revision: 1080
Merged at revision: 1117
Proposed branch: lp:~tapaal-contributor/tapaal/show-reduced-net-1879130
Merge into: lp:tapaal
Diff against target: 1488 lines (+515/-113)
43 files modified
src/dk/aau/cs/TCTL/AritmeticOperator.java (+5/-1)
src/dk/aau/cs/TCTL/TCTLAFNode.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLAGNode.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLAUNode.java (+7/-1)
src/dk/aau/cs/TCTL/TCTLAXNode.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLAbstractProperty.java (+2/-0)
src/dk/aau/cs/TCTL/TCTLAndListNode.java (+8/-1)
src/dk/aau/cs/TCTL/TCTLAtomicPropositionNode.java (+32/-1)
src/dk/aau/cs/TCTL/TCTLConstNode.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLDeadlockNode.java (+5/-1)
src/dk/aau/cs/TCTL/TCTLEFNode.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLEGNode.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLEUNode.java (+7/-1)
src/dk/aau/cs/TCTL/TCTLEXNode.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLFalseNode.java (+5/-1)
src/dk/aau/cs/TCTL/TCTLNotNode.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLOrListNode.java (+8/-1)
src/dk/aau/cs/TCTL/TCTLPathPlaceHolder.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLPathToStateConverter.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLPlaceNode.java (+11/-1)
src/dk/aau/cs/TCTL/TCTLPlusListNode.java (+8/-1)
src/dk/aau/cs/TCTL/TCTLStatePlaceHolder.java (+5/-1)
src/dk/aau/cs/TCTL/TCTLStateToPathConverter.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLTermListNode.java (+8/-1)
src/dk/aau/cs/TCTL/TCTLTransitionNode.java (+7/-1)
src/dk/aau/cs/TCTL/TCTLTrueNode.java (+5/-1)
src/dk/aau/cs/verification/VerificationResult.java (+5/-0)
src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java (+3/-2)
src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java (+21/-11)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java (+1/-1)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java (+1/-1)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java (+63/-16)
src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java (+5/-4)
src/net/tapaal/TAPAAL.java (+1/-1)
src/pipe/dataLayer/TAPNQuery.java (+10/-0)
src/pipe/gui/Export.java (+2/-2)
src/pipe/gui/KBoundAnalyzer.java (+1/-1)
src/pipe/gui/RunVerification.java (+54/-16)
src/pipe/gui/RunVerificationBase.java (+17/-5)
src/pipe/gui/Verifier.java (+65/-16)
src/pipe/gui/widgets/QueryDialog.java (+73/-8)
src/pipe/gui/widgets/QueryPane.java (+1/-1)
src/pipe/gui/widgets/WorkflowDialog.java (+3/-3)
To merge this branch: bzr merge lp:~tapaal-contributor/tapaal/show-reduced-net-1879130
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Thomas Pedersen (community) Needs Resubmitting
Kenneth Yrke Jørgensen code Approve
Review via email: mp+390961@code.launchpad.net

Commit message

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.

To post a comment you must log in.
Jiri Srba (srba) wrote :

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

review: Needs Fixing
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) wrote :

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
review: Approve (code)
Jiri Srba (srba) wrote :

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
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) wrote :

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
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) wrote :

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) wrote :

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) wrote :

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
1076. By Thomas Pedersen <email address hidden> on 2020-11-11

Fix getting positional information from multiple components

Thomas Pedersen (tpede16) wrote :

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) wrote :

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) wrote :

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
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) wrote :

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) wrote :

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
1079. By Thomas Pedersen <email address hidden> on 2020-12-16

Disable open reduced net button when query reductions are disabled

Jiri Srba (srba) wrote :

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

review: Needs Fixing
1080. By Thomas Pedersen <email address hidden> on 2020-12-17

Merge with trunk

Thomas Pedersen (tpede16) wrote :

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

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
=== 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 @@
22 }22 }
23 }23 }
2424
25 @Override25 @Override
26 public void convertForReducedNet(String templateName) {
27 }
28
29 @Override
26 public TCTLAbstractStateProperty copy() {30 public TCTLAbstractStateProperty copy() {
27 return new AritmeticOperator(operator);31 return new AritmeticOperator(operator);
28 }32 }
2933
=== 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 @@
41 return children;41 return children;
42 }42 }
4343
44 @Override44 @Override
45 public void convertForReducedNet(String templateName) {
46 property.convertForReducedNet(templateName);
47 }
48
49 @Override
45 public boolean equals(Object o) {50 public boolean equals(Object o) {
46 if (o instanceof TCTLAFNode) {51 if (o instanceof TCTLAFNode) {
47 TCTLAFNode node = (TCTLAFNode) o;52 TCTLAFNode node = (TCTLAFNode) o;
4853
=== 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 @@
41 return children;41 return children;
42 }42 }
4343
44 @Override44 @Override
45 public void convertForReducedNet(String templateName) {
46 property.convertForReducedNet(templateName);
47 }
48
49 @Override
45 public boolean equals(Object o) {50 public boolean equals(Object o) {
46 if (o instanceof TCTLAGNode) {51 if (o instanceof TCTLAGNode) {
47 TCTLAGNode node = (TCTLAGNode) o;52 TCTLAGNode node = (TCTLAGNode) o;
4853
=== 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 @@
58 return children;58 return children;
59 }59 }
6060
61 @Override61 @Override
62 public void convertForReducedNet(String templateName) {
63 left.convertForReducedNet(templateName);
64 right.convertForReducedNet(templateName);
65 }
66
67 @Override
62 public boolean equals(Object o) { 68 public boolean equals(Object o) {
63 if (o instanceof TCTLAUNode) {69 if (o instanceof TCTLAUNode) {
64 TCTLAUNode node = (TCTLAUNode) o;70 TCTLAUNode node = (TCTLAUNode) o;
6571
=== 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 @@
41 return children;41 return children;
42 }42 }
4343
44 @Override44 @Override
45 public void convertForReducedNet(String templateName) {
46 property.convertForReducedNet(templateName);
47 }
48
49 @Override
45 public boolean equals(Object o) {50 public boolean equals(Object o) {
46 if (o instanceof TCTLAXNode) {51 if (o instanceof TCTLAXNode) {
47 TCTLAXNode node = (TCTLAXNode) o;52 TCTLAXNode node = (TCTLAXNode) o;
4853
=== 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 @@
51 return children;51 return children;
52 }52 }
5353
54 public abstract void convertForReducedNet(String templateName);
55
54 public abstract void accept(ITCTLVisitor visitor, Object context);56 public abstract void accept(ITCTLVisitor visitor, Object context);
5557
56 public abstract boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName);58 public abstract boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName);
5759
=== 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 @@
122 return children;122 return children;
123 }123 }
124124
125 @Override125 @Override
126 public void convertForReducedNet(String templateName) {
127 for (TCTLAbstractProperty property : properties){
128 property.convertForReducedNet(templateName);
129 }
130 }
131
132 @Override
126 public boolean equals(Object o) {133 public boolean equals(Object o) {
127 if (o instanceof TCTLAndListNode) {134 if (o instanceof TCTLAndListNode) {
128 TCTLAndListNode node = (TCTLAndListNode) o;135 TCTLAndListNode node = (TCTLAndListNode) o;
129136
=== 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 @@
67 }67 }
68 }68 }
6969
70 @Override70 @Override
71 public void convertForReducedNet(String templateName) {
72 left.convertForReducedNet(templateName);
73 right.convertForReducedNet(templateName);
74 }
75
76 @Override
71 public String toString() {77 public String toString() {
72 return left + " " + op + " " + right;78 return left + " " + op + " " + right;
73 }79 }
@@ -88,6 +94,31 @@
88 return false;94 return false;
89 }95 }
9096
97/* @Override
98 public StringPosition[] getChildren() {
99 StringPosition[] children = new StringPosition[2];
100
101 int start = 0;
102 int end = 0;
103 boolean leftSimpleProperty = left.isSimpleProperty();
104
105 start = leftSimpleProperty ? 0 : 1;
106 end = start + left.toString().length();
107
108 StringPosition posLeft = new StringPosition(start, end, left);
109
110 start = end + 5 + (right.isSimpleProperty() ? 0 : 1)
111 + (leftSimpleProperty ? 0 : 1);
112
113 end = start + right.toString().length();
114
115 StringPosition posRight = new StringPosition(start, end, right);
116
117 children[0] = posLeft;
118 children[1] = posRight;
119 return children;
120 }*/
121
91 @Override122 @Override
92 public TCTLAbstractProperty findFirstPlaceHolder() {123 public TCTLAbstractProperty findFirstPlaceHolder() {
93 TCTLAbstractProperty rightP = right.findFirstPlaceHolder(); 124 TCTLAbstractProperty rightP = right.findFirstPlaceHolder();
94125
=== 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 @@
26 }26 }
27 }27 }
2828
29 @Override29 @Override
30 public void convertForReducedNet(String templateName) {
31
32 }
33
34 @Override
30 public TCTLAbstractStateProperty copy() {35 public TCTLAbstractStateProperty copy() {
31 return new TCTLConstNode(constant);36 return new TCTLConstNode(constant);
32 }37 }
3338
=== 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 @@
18 }18 }
19 }19 }
2020
21 @Override21 @Override
22 public void convertForReducedNet(String templateName) {
23 }
24
25 @Override
22 public void accept(ITCTLVisitor visitor, Object context) {26 public void accept(ITCTLVisitor visitor, Object context) {
23 visitor.visit(this, context);27 visitor.visit(this, context);
24 }28 }
2529
=== 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 @@
41 return children;41 return children;
42 }42 }
4343
44 @Override44 @Override
45 public void convertForReducedNet(String templateName) {
46 property.convertForReducedNet(templateName);
47 }
48
49 @Override
45 public boolean equals(Object o) {50 public boolean equals(Object o) {
46 if (o instanceof TCTLEFNode) {51 if (o instanceof TCTLEFNode) {
47 TCTLEFNode node = (TCTLEFNode) o;52 TCTLEFNode node = (TCTLEFNode) o;
4853
=== 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 @@
41 return children;41 return children;
42 }42 }
4343
44 @Override44 @Override
45 public void convertForReducedNet(String templateName) {
46 property.convertForReducedNet(templateName);
47 }
48
49 @Override
45 public boolean equals(Object o) {50 public boolean equals(Object o) {
46 if (o instanceof TCTLEGNode) {51 if (o instanceof TCTLEGNode) {
47 TCTLEGNode node = (TCTLEGNode) o;52 TCTLEGNode node = (TCTLEGNode) o;
4853
=== 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 @@
58 return children;58 return children;
59 }59 }
6060
61 @Override61 @Override
62 public void convertForReducedNet(String templateName) {
63 left.convertForReducedNet(templateName);
64 right.convertForReducedNet(templateName);
65 }
66
67 @Override
62 public boolean equals(Object o) { 68 public boolean equals(Object o) {
63 if (o instanceof TCTLEUNode) {69 if (o instanceof TCTLEUNode) {
64 TCTLEUNode node = (TCTLEUNode) o;70 TCTLEUNode node = (TCTLEUNode) o;
6571
=== 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 @@
41 return children;41 return children;
42 }42 }
4343
44 @Override44 @Override
45 public void convertForReducedNet(String templateName) {
46 property.convertForReducedNet(templateName);
47 }
48
49 @Override
45 public boolean equals(Object o) {50 public boolean equals(Object o) {
46 if (o instanceof TCTLEXNode) {51 if (o instanceof TCTLEXNode) {
47 TCTLEXNode node = (TCTLEXNode) o;52 TCTLEXNode node = (TCTLEXNode) o;
4853
=== 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 @@
18 }18 }
19 }19 }
2020
21 @Override21 @Override
22 public void convertForReducedNet(String templateName) {
23 }
24
25 @Override
22 public void accept(ITCTLVisitor visitor, Object context) {26 public void accept(ITCTLVisitor visitor, Object context) {
23 visitor.visit(this, context);27 visitor.visit(this, context);
24 }28 }
2529
=== 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 @@
52 return children;52 return children;
53 }53 }
5454
55 @Override55 @Override
56 public void convertForReducedNet(String templateName) {
57 property.convertForReducedNet(templateName);
58 }
59
60 @Override
56 public TCTLAbstractStateProperty copy() {61 public TCTLAbstractStateProperty copy() {
57 return new TCTLNotNode(property.copy());62 return new TCTLNotNode(property.copy());
58 }63 }
5964
=== 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 @@
122 return children;122 return children;
123 }123 }
124124
125 @Override125 @Override
126 public void convertForReducedNet(String templateName) {
127 for(TCTLAbstractProperty property : properties){
128 property.convertForReducedNet(templateName);
129 }
130 }
131
132 @Override
126 public boolean equals(Object o) {133 public boolean equals(Object o) {
127 if (o instanceof TCTLOrListNode) {134 if (o instanceof TCTLOrListNode) {
128 TCTLOrListNode node = (TCTLOrListNode) o;135 TCTLOrListNode node = (TCTLOrListNode) o;
129136
=== 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 @@
49 }49 }
50 }50 }
5151
52 @Override52 @Override
53 public void convertForReducedNet(String templateName) {
54
55 }
56
57 @Override
53 public void accept(ITCTLVisitor visitor, Object context) {58 public void accept(ITCTLVisitor visitor, Object context) {
54 visitor.visit(this, context);59 visitor.visit(this, context);
55 }60 }
5661
=== 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 @@
37 return children;37 return children;
38 }38 }
3939
40 @Override40 @Override
41 public void convertForReducedNet(String templateName) {
42 property.convertForReducedNet(templateName);
43 }
44
45 @Override
41 public boolean equals(Object o) {46 public boolean equals(Object o) {
42 if (o instanceof TCTLEFNode) {47 if (o instanceof TCTLEFNode) {
43 TCTLEFNode node = (TCTLEFNode) o;48 TCTLEFNode node = (TCTLEFNode) o;
4449
=== 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 @@
29 }29 }
30 }30 }
3131
32 @Override32 @Override
33 public void convertForReducedNet(String templateName) {
34 if(template.isEmpty()){
35 place = "Shared_" + place;
36 } else {
37 place = template + "_" + place;
38 }
39 template = templateName;
40 }
41
42 @Override
33 public TCTLAbstractStateProperty copy() {43 public TCTLAbstractStateProperty copy() {
34 return new TCTLPlaceNode(template, place);44 return new TCTLPlaceNode(template, place);
35 }45 }
3646
=== 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 @@
36 }36 }
37 }37 }
3838
39 @Override39 @Override
40 public void convertForReducedNet(String templateName) {
41 for(TCTLAbstractProperty property : terms) {
42 property.convertForReducedNet(templateName);
43 }
44 }
45
46 @Override
40 public TCTLAbstractStateProperty copy() {47 public TCTLAbstractStateProperty copy() {
41 ArrayList<TCTLAbstractStateProperty> copy = new ArrayList<TCTLAbstractStateProperty>();48 ArrayList<TCTLAbstractStateProperty> copy = new ArrayList<TCTLAbstractStateProperty>();
42 49
4350
=== 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 @@
51 }51 }
52 }52 }
5353
54 @Override54 @Override
55 public void convertForReducedNet(String templateName) {
56 }
57
58 @Override
55 public void accept(ITCTLVisitor visitor, Object context) {59 public void accept(ITCTLVisitor visitor, Object context) {
56 visitor.visit(this, context);60 visitor.visit(this, context);
5761
5862
=== 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 @@
37 return children;37 return children;
38 }38 }
3939
40 @Override40 @Override
41 public void convertForReducedNet(String templateName) {
42 property.convertForReducedNet(templateName);
43 }
44
45 @Override
41 public boolean equals(Object o) {46 public boolean equals(Object o) {
42 if (o instanceof TCTLEFNode) {47 if (o instanceof TCTLEFNode) {
43 TCTLEFNode node = (TCTLEFNode) o;48 TCTLEFNode node = (TCTLEFNode) o;
4449
=== 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 @@
36 }36 }
37 }37 }
3838
39 @Override39 @Override
40 public void convertForReducedNet(String templateName) {
41 for (TCTLAbstractProperty property : factors) {
42 property.convertForReducedNet(templateName);
43 }
44 }
45
46 @Override
40 public TCTLAbstractStateProperty copy() {47 public TCTLAbstractStateProperty copy() {
41 ArrayList<TCTLAbstractStateProperty> copy = new ArrayList<TCTLAbstractStateProperty>();48 ArrayList<TCTLAbstractStateProperty> copy = new ArrayList<TCTLAbstractStateProperty>();
4249
4350
=== 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 @@
29 }29 }
30 }30 }
3131
32 @Override32 @Override
33 public void convertForReducedNet(String templateName) {
34 transition = template + "_" + transition;
35 template = templateName;
36 }
37
38 @Override
33 public TCTLAbstractStateProperty copy() {39 public TCTLAbstractStateProperty copy() {
34 return new TCTLTransitionNode(template, transition);40 return new TCTLTransitionNode(template, transition);
35 }41 }
3642
=== 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 @@
18 }18 }
19 }19 }
2020
21 @Override21 @Override
22 public void convertForReducedNet(String templateName) {
23 }
24
25 @Override
22 public void accept(ITCTLVisitor visitor, Object context) {26 public void accept(ITCTLVisitor visitor, Object context) {
23 visitor.visit(this, context);27 visitor.visit(this, context);
24 }28 }
2529
=== 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 @@
180 }180 }
181 return reductionStats.toString();181 return reductionStats.toString();
182 }182 }
183
184 public boolean reductionRulesApplied(){
185 ReductionStats reductionStats = stats.getReductionStats();
186 return (reductionStats.getRemovedPlaces() + reductionStats.getRemovedTrantitions()) > 0;
187 }
183 188
184 public NetworkMarking getCoveredMarking(TimedArcPetriNetNetwork model){189 public NetworkMarking getCoveredMarking(TimedArcPetriNetNetwork model){
185 190
186191
=== 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 @@
284 if(((VerifyTAPNOptions)options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model);284 if(((VerifyTAPNOptions)options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model);
285 285
286 VerifyPNExporter exporter = new VerifyPNExporter();286 VerifyPNExporter exporter = new VerifyPNExporter();
287 ExportedVerifyTAPNModel exportedModel = exporter.export(model.value1(), query, null);287 ExportedVerifyTAPNModel exportedModel = exporter.export(model.value1(), query, null, model.value2());
288288
289 if (exportedModel == null) {289 if (exportedModel == null) {
290 messenger.displayErrorMessage("There was an error exporting the model");290 messenger.displayErrorMessage("There was an error exporting the model");
@@ -314,8 +314,9 @@
314 ((VerifyTAPNOptions)options).setInclusionPlaces(new InclusionPlaces(InclusionPlacesOption.UserSpecified, inclusionPlaces));314 ((VerifyTAPNOptions)options).setInclusionPlaces(new InclusionPlaces(InclusionPlacesOption.UserSpecified, inclusionPlaces));
315 }315 }
316316
317 private VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, ExportedVerifyTAPNModel exportedModel, TAPNQuery query) {317 private VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, ExportedVerifyTAPNModel exportedModel, TAPNQuery query) throws IOException {
318 ((VerifyTAPNOptions)options).setTokensInModel(model.value1().marking().size()); // TODO: get rid of me318 ((VerifyTAPNOptions)options).setTokensInModel(model.value1().marking().size()); // TODO: get rid of me
319
319 runner = new ProcessRunner(verifypnpath, createArgumentString(exportedModel.modelFile(), exportedModel.queryFile(), options));320 runner = new ProcessRunner(verifypnpath, createArgumentString(exportedModel.modelFile(), exportedModel.queryFile(), options));
320 runner.run();321 runner.run();
321322
322323
=== 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 @@
4import java.util.Map;4import java.util.Map;
55
6import pipe.dataLayer.TAPNQuery.SearchOption;6import pipe.dataLayer.TAPNQuery.SearchOption;
7import pipe.dataLayer.TAPNQuery.QueryReductionTime;
7import pipe.dataLayer.TAPNQuery.TraceOption;8import pipe.dataLayer.TAPNQuery.TraceOption;
8import pipe.dataLayer.TAPNQuery.AlgorithmOption;9import pipe.dataLayer.TAPNQuery.AlgorithmOption;
9import pipe.dataLayer.TAPNQuery.QueryCategory;10import pipe.dataLayer.TAPNQuery.QueryCategory;
@@ -16,26 +17,28 @@
16 private final QueryCategory queryCategory;17 private final QueryCategory queryCategory;
17 private final AlgorithmOption algorithmOption;18 private final AlgorithmOption algorithmOption;
18 private boolean useSiphontrap = false; 19 private boolean useSiphontrap = false;
19 private boolean useQueryReduction = true; 20 private QueryReductionTime queryReductionTime;
20 private boolean useStubbornReduction = true;21 private boolean useStubbornReduction = true;
22 private String pathToReducedNet;
21 23
22 public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, ModelReduction modelReduction, 24 public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, ModelReduction modelReduction,
23 boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, QueryCategory queryCategory, AlgorithmOption algorithmOption,25 boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, QueryCategory queryCategory, AlgorithmOption algorithmOption,
24 boolean siphontrap, boolean queryReduction, boolean stubbornReduction) {26 boolean siphontrap, QueryReductionTime queryReduction, boolean stubbornReduction, String pathToReducedNet) {
25 super(extraTokens, traceOption, search, true, useOverApproximation, false, new InclusionPlaces(), enableOverApproximation, enableUnderApproximation, approximationDenominator);27 super(extraTokens, traceOption, search, true, useOverApproximation, false, new InclusionPlaces(), enableOverApproximation, enableUnderApproximation, approximationDenominator);
26 this.modelReduction = modelReduction;28 this.modelReduction = modelReduction;
27 this.queryCategory = queryCategory;29 this.queryCategory = queryCategory;
28 this.algorithmOption = algorithmOption;30 this.algorithmOption = algorithmOption;
29 this.useSiphontrap = siphontrap;31 this.useSiphontrap = siphontrap;
30 this.useQueryReduction = queryReduction;32 this.queryReductionTime = queryReduction;
31 this.useStubbornReduction = stubbornReduction;33 this.useStubbornReduction = stubbornReduction;
34 this.pathToReducedNet = pathToReducedNet;
32 }35 }
33 36
34 public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, boolean useModelReduction, 37 public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, boolean useModelReduction,
35 boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, QueryCategory queryCategory, AlgorithmOption algorithmOption,38 boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, QueryCategory queryCategory, AlgorithmOption algorithmOption,
36 boolean siphontrap, boolean queryReduction, boolean stubbornReduction) {39 boolean siphontrap, QueryReductionTime queryReduction, boolean stubbornReduction) {
37 this(extraTokens, traceOption, search, useOverApproximation, useModelReduction? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION, enableOverApproximation, 40 this(extraTokens, traceOption, search, useOverApproximation, useModelReduction? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION, enableOverApproximation,
38 enableUnderApproximation, approximationDenominator,queryCategory, algorithmOption, siphontrap, queryReduction, stubbornReduction);41 enableUnderApproximation, approximationDenominator,queryCategory, algorithmOption, siphontrap, queryReduction, stubbornReduction, null);
39 }42 }
4043
41 @Override44 @Override
@@ -49,12 +52,16 @@
49 switch(getModelReduction()){52 switch(getModelReduction()){
50 case AGGRESSIVE:53 case AGGRESSIVE:
51 result.append(" -r 1 ");54 result.append(" -r 1 ");
55 String writeReducedCMD = " --write-reduced " +pathToReducedNet;
56 result.append(writeReducedCMD);
52 break;57 break;
53 case NO_REDUCTION:58 case NO_REDUCTION:
54 result.append(" -r 0 ");59 result.append(" -r 0 ");
55 break;60 break;
56 case BOUNDPRESERVING:61 case BOUNDPRESERVING:
57 result.append(" -r 2 ");62 result.append(" -r 2 ");
63 writeReducedCMD = " --write-reduced " +pathToReducedNet;
64 result.append(writeReducedCMD);
58 break;65 break;
59 default:66 default:
60 break; 67 break;
@@ -67,9 +74,12 @@
67 if (this.useSiphontrap) {74 if (this.useSiphontrap) {
68 result.append(" -a 10 ");75 result.append(" -a 10 ");
69 }76 }
70 if (!this.useQueryReduction) {77 if (this.queryReductionTime == QueryReductionTime.NoTime) {
71 result.append(" -q 0 ");78 result.append(" -q 0 ");
72 }79 } else if (this.queryReductionTime == QueryReductionTime.ShortestTime) {
80 //Run query reduction for 1 second, to avoid conflict with -s OverApprox argument, but also still not run the verification.
81 result.append(" -q 1");
82 }
73 if (!this.useStubbornReduction) {83 if (!this.useStubbornReduction) {
74 result.append(" -p ");84 result.append(" -p ");
75 }85 }
7686
=== 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 @@
272 if(((VerifyTAPNOptions)options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model);272 if(((VerifyTAPNOptions)options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model);
273 273
274 VerifyTAPNExporter exporter = new VerifyTAPNExporter();274 VerifyTAPNExporter exporter = new VerifyTAPNExporter();
275 ExportedVerifyTAPNModel exportedModel = exporter.export(model.value1(), query, null);275 ExportedVerifyTAPNModel exportedModel = exporter.export(model.value1(), query, null, model.value2());
276276
277 if (exportedModel == null) {277 if (exportedModel == null) {
278 messenger.displayErrorMessage("There was an error exporting the model");278 messenger.displayErrorMessage("There was an error exporting the model");
279279
=== 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 @@
278 }278 }
279279
280 VerifyTAPNExporter exporter = new VerifyTAPNExporter();280 VerifyTAPNExporter exporter = new VerifyTAPNExporter();
281 ExportedVerifyTAPNModel exportedModel = exporter.export(model.value1(), query, CreateGui.getCurrentTab().getLens());281 ExportedVerifyTAPNModel exportedModel = exporter.export(model.value1(), query, CreateGui.getCurrentTab().getLens(), model.value2());
282282
283 if (exportedModel == null) {283 if (exportedModel == null) {
284 messenger.displayErrorMessage("There was an error exporting the model");284 messenger.displayErrorMessage("There was an error exporting the model");
285285
=== 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 @@
4import java.io.FileNotFoundException;4import java.io.FileNotFoundException;
5import java.io.IOException;5import java.io.IOException;
6import java.io.PrintStream;6import java.io.PrintStream;
7import java.util.Collection;
8import java.util.List;
79
8import dk.aau.cs.gui.TabContent;10import dk.aau.cs.gui.TabContent;
11import dk.aau.cs.verification.NameMapping;
12import pipe.dataLayer.DataLayer;
9import pipe.dataLayer.TAPNQuery.QueryCategory;13import pipe.dataLayer.TAPNQuery.QueryCategory;
1014
11import dk.aau.cs.model.tapn.TAPNQuery;15import dk.aau.cs.model.tapn.TAPNQuery;
@@ -18,9 +22,14 @@
18import dk.aau.cs.model.tapn.TransportArc;22import dk.aau.cs.model.tapn.TransportArc;
1923
20import dk.aau.cs.TCTL.visitors.CTLQueryVisitor;24import dk.aau.cs.TCTL.visitors.CTLQueryVisitor;
25import pipe.gui.CreateGui;
26import pipe.gui.graphicElements.Place;
27import pipe.gui.graphicElements.Transition;
28
29import javax.xml.crypto.Data;
2130
22public class VerifyTAPNExporter {31public class VerifyTAPNExporter {
23 public ExportedVerifyTAPNModel export(TimedArcPetriNet model, TAPNQuery query, TabContent.TAPNLens lens) {32 public ExportedVerifyTAPNModel export(TimedArcPetriNet model, TAPNQuery query, TabContent.TAPNLens lens, NameMapping mapping) {
24 File modelFile = createTempFile(".xml");33 File modelFile = createTempFile(".xml");
25 File queryFile;34 File queryFile;
26 if (query.getCategory() == QueryCategory.CTL){35 if (query.getCategory() == QueryCategory.CTL){
@@ -28,19 +37,20 @@
28 } else {37 } else {
29 queryFile = createTempFile(".q");38 queryFile = createTempFile(".q");
30 }39 }
31 40
3241 return export(model, query, modelFile, queryFile, null, lens, mapping);
33 return export(model, query, modelFile, queryFile, lens);42
34 }43 }
3544
36 public ExportedVerifyTAPNModel export(TimedArcPetriNet model, TAPNQuery query, File modelFile, File queryFile, TabContent.TAPNLens lens) {45
46 public ExportedVerifyTAPNModel export(TimedArcPetriNet model, TAPNQuery query, File modelFile, File queryFile, pipe.dataLayer.TAPNQuery dataLayerQuery, TabContent.TAPNLens lens, NameMapping mapping) {
37 if (modelFile == null || queryFile == null)47 if (modelFile == null || queryFile == null)
38 return null;48 return null;
3949
40 try{50 try{
41 PrintStream modelStream = new PrintStream(modelFile);51 PrintStream modelStream = new PrintStream(modelFile);
4252
43 outputModel(model, modelStream);53 outputModel(model, modelStream, mapping);
44 modelStream.close();54 modelStream.close();
4555
46 PrintStream queryStream = new PrintStream(queryFile);56 PrintStream queryStream = new PrintStream(queryFile);
@@ -62,15 +72,17 @@
62 return new ExportedVerifyTAPNModel(modelFile.getAbsolutePath(), queryFile.getAbsolutePath());72 return new ExportedVerifyTAPNModel(modelFile.getAbsolutePath(), queryFile.getAbsolutePath());
63 }73 }
64 74
65 private void outputModel(TimedArcPetriNet model, PrintStream modelStream) {75 private void outputModel(TimedArcPetriNet model, PrintStream modelStream, NameMapping mapping) {
76 Collection<DataLayer> guiModels = CreateGui.getCurrentTab().getGuiModels().values();
77
66 modelStream.append("<pnml>\n");78 modelStream.append("<pnml>\n");
67 modelStream.append("<net id=\"" + model.name() + "\" type=\"P/T net\">\n");79 modelStream.append("<net id=\"" + model.name() + "\" type=\"P/T net\">\n");
68 80
69 for(TimedPlace p : model.places())81 for(TimedPlace p : model.places())
70 outputPlace(p, modelStream);82 outputPlace(p, modelStream, guiModels, mapping);
71 83
72 for(TimedTransition t : model.transitions())84 for(TimedTransition t : model.transitions())
73 outputTransition(t,modelStream);85 outputTransition(t,modelStream, guiModels, mapping);
74 86
75 for(TimedInputArc inputArc : model.inputArcs())87 for(TimedInputArc inputArc : model.inputArcs())
76 outputInputArc(inputArc, modelStream);88 outputInputArc(inputArc, modelStream);
@@ -88,28 +100,63 @@
88 modelStream.append("</pnml>");100 modelStream.append("</pnml>");
89 }101 }
90 102
91 private void outputPlace(TimedPlace p, PrintStream modelStream) {103 private void outputPlace(TimedPlace p, PrintStream modelStream, Collection<DataLayer> guiModels, NameMapping mapping) {
104 //remove the net prefix from the place name
105 String placeName = mapping.map(p.name()).value2();
106 Place guiPlace = null;
107
108 for(DataLayer guiModel : guiModels ){
109 guiPlace = guiModel.getPlaceById(placeName);
110 if(guiPlace != null){
111 break;
112 }
113 }
114
92 modelStream.append("<place ");115 modelStream.append("<place ");
93 116
94 modelStream.append("id=\"" + p.name() + "\" ");117 modelStream.append("id=\"" + p.name() + "\" ");
95 modelStream.append("name=\"" + p.name() + "\" ");118 modelStream.append("name=\"" + p.name() + "\" ");
96 modelStream.append("invariant=\"" + p.invariant().toString(false).replace("<", "&lt;") + "\" ");119 modelStream.append("invariant=\"" + p.invariant().toString(false).replace("<", "&lt;") + "\" ");
97 modelStream.append("initialMarking=\"" + p.numberOfTokens() + "\" ");120 modelStream.append("initialMarking=\"" + p.numberOfTokens() + "\" ");
98 121 modelStream.append(">\n");
99 modelStream.append("/>\n");122 outputPosition(modelStream, guiPlace.getPositionX(), guiPlace.getPositionY());
123
124 modelStream.append("</place>\n");
100 }125 }
101126
102 private void outputTransition(TimedTransition t, PrintStream modelStream) {127 private void outputTransition(TimedTransition t, PrintStream modelStream, Collection<DataLayer> guiModels, NameMapping mapping) {
128 //remove the net prefix from the transition name
129 String transitionName = mapping.map(t.name()).value2();
130 Transition guiTransition = null;
131
132 for(DataLayer guiModel : guiModels){
133 guiTransition = guiModel.getTransitionById(transitionName);
134 if(guiTransition != null){
135 break;
136 }
137 }
138
103 modelStream.append("<transition ");139 modelStream.append("<transition ");
104140
105 modelStream.append("player=\"" + (t.isUncontrollable() ? "1" : "0") + "\" ");141 modelStream.append("player=\"" + (t.isUncontrollable() ? "1" : "0") + "\" ");
106 modelStream.append("id=\"" + t.name() + "\" ");142 modelStream.append("id=\"" + t.name() + "\" ");
107 modelStream.append("name=\"" + t.name() + "\" ");143 modelStream.append("name=\"" + t.name() + "\" ");
108 modelStream.append("urgent=\"" + (t.isUrgent()? "true":"false") + "\"");144 modelStream.append("urgent=\"" + (t.isUrgent()? "true":"false") + "\"");
109 145 modelStream.append(">\n");
110 modelStream.append("/>\n");146 outputPosition(modelStream, guiTransition.getPositionX(), guiTransition.getPositionY());
147
148 modelStream.append("</transition>\n");
111 }149 }
112150
151 private void outputPosition(PrintStream modelStream, int positionX, int positionY) {
152 modelStream.append("<graphics>");
153 modelStream.append("<position ");
154 modelStream.append("x=\"" + positionX + "\" ");
155 modelStream.append("y=\"" + positionY + "\" ");
156 modelStream.append("/>");
157 modelStream.append("</graphics>");
158 }
159
113 protected void outputInputArc(TimedInputArc inputArc, PrintStream modelStream) {160 protected void outputInputArc(TimedInputArc inputArc, PrintStream modelStream) {
114 modelStream.append("<inputArc ");161 modelStream.append("<inputArc ");
115 162
116163
=== 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 @@
8import pipe.dataLayer.TAPNQuery.SearchOption;8import pipe.dataLayer.TAPNQuery.SearchOption;
9import pipe.dataLayer.TAPNQuery.TraceOption;9import pipe.dataLayer.TAPNQuery.TraceOption;
10import pipe.dataLayer.TAPNQuery.WorkflowMode;10import pipe.dataLayer.TAPNQuery.WorkflowMode;
11import pipe.dataLayer.TAPNQuery.QueryReductionTime;
11import pipe.gui.CreateGui;12import pipe.gui.CreateGui;
12import pipe.gui.FileFinder;13import pipe.gui.FileFinder;
13import pipe.gui.MessengerImpl;14import pipe.gui.MessengerImpl;
@@ -307,7 +308,7 @@
307 }308 }
308 long c = m*B+1;309 long c = m*B+1;
309 queryToVerify.setStrongSoundnessBound(c);310 queryToVerify.setStrongSoundnessBound(c);
310 Verifier.runVerifyTAPNVerification(model.network(), queryToVerify, new VerificationCallback() {311 Verifier.runVerifyTAPNVerification(model.network(), queryToVerify, false, new VerificationCallback() {
311 312
312 @Override313 @Override
313 public void run(VerificationResult<TAPNNetworkTrace> result) {314 public void run(VerificationResult<TAPNNetworkTrace> result) {
@@ -575,7 +576,7 @@
575 TAPNQuery queryToVerify = getTAPNQuery(composedModel.value1(),query);576 TAPNQuery queryToVerify = getTAPNQuery(composedModel.value1(),query);
576 queryToVerify.setCategory(query.getCategory());577 queryToVerify.setCategory(query.getCategory());
577 MapQueryToNewNames(queryToVerify, composedModel.value2());578 MapQueryToNewNames(queryToVerify, composedModel.value2());
578 579
579 TAPNQuery clonedQuery = new TAPNQuery(query.getProperty().copy(), queryToVerify.getExtraTokens());580 TAPNQuery clonedQuery = new TAPNQuery(query.getProperty().copy(), queryToVerify.getExtraTokens());
580 clonedQuery.setCategory(query.getCategory());581 clonedQuery.setCategory(query.getCategory());
581 MapQueryToNewNames(clonedQuery, composedModel.value2());582 MapQueryToNewNames(clonedQuery, composedModel.value2());
@@ -622,9 +623,9 @@
622 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());623 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());
623 else if(query.getReductionOption() == ReductionOption.VerifyPN || query.getReductionOption() == ReductionOption.VerifyPNApprox || query.getReductionOption() == ReductionOption.VerifyPNReduce)624 else if(query.getReductionOption() == ReductionOption.VerifyPN || query.getReductionOption() == ReductionOption.VerifyPNApprox || query.getReductionOption() == ReductionOption.VerifyPNReduce)
624 if (batchProcessingVerificationOptions.queryPropertyOption() == QueryPropertyOption.SearchWholeStateSpace){625 if (batchProcessingVerificationOptions.queryPropertyOption() == QueryPropertyOption.SearchWholeStateSpace){
625 return new VerifyPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), false, false, false, false, query.approximationDenominator(), QueryCategory.Default, query.getAlgorithmOption(), false, false, false);626 return new VerifyPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), false, false, false, false, query.approximationDenominator(), QueryCategory.Default, query.getAlgorithmOption(), false, QueryReductionTime.UnlimitedTime, false);
626 } else {627 } else {
627 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());628 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());
628 }629 }
629 else630 else
630 return new VerifytaOptions(TraceOption.NONE, query.getSearchOption(), false, query.getReductionOption(), query.useSymmetry(), false, query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator());631 return new VerifytaOptions(TraceOption.NONE, query.getSearchOption(), false, query.getReductionOption(), query.useSymmetry(), false, query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator());
631632
=== 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 @@
148 System.out.println(" | Running query: " + query.getName());148 System.out.println(" | Running query: " + query.getName());
149149
150 if(query.getReductionOption() == ReductionOption.VerifyTAPN || query.getReductionOption() == ReductionOption.VerifyTAPNdiscreteVerification || query.getReductionOption() == ReductionOption.VerifyPN) {150 if(query.getReductionOption() == ReductionOption.VerifyTAPN || query.getReductionOption() == ReductionOption.VerifyTAPNdiscreteVerification || query.getReductionOption() == ReductionOption.VerifyPN) {
151 Verifier.runVerifyTAPNVerification(network, query, new VerificationCallback() {151 Verifier.runVerifyTAPNVerification(network, query, false, new VerificationCallback() {
152 @Override152 @Override
153 public void run(VerificationResult<TAPNNetworkTrace> result) {153 public void run(VerificationResult<TAPNNetworkTrace> result) {
154154
155155
=== 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 @@
16 BFS, DFS, RANDOM, BatchProcessingKeepQueryOption, HEURISTIC, OVERAPPROXIMATE, DEFAULT16 BFS, DFS, RANDOM, BatchProcessingKeepQueryOption, HEURISTIC, OVERAPPROXIMATE, DEFAULT
17 }17 }
1818
19 public enum QueryReductionTime {
20 NoTime, ShortestTime, UnlimitedTime
21 }
22
19 public enum HashTableSize {23 public enum HashTableSize {
20 MB_4, MB_16, MB_64, MB_256, MB_51224 MB_4, MB_16, MB_64, MB_256, MB_512
21 }25 }
@@ -430,4 +434,10 @@
430 }434 }
431 return false;435 return false;
432 }436 }
437
438 public TAPNQuery convertPropertyForReducedNet(String templateName){
439 TAPNQuery convertedQuery = copy();
440 convertedQuery.property.convertForReducedNet(templateName);
441 return convertedQuery;
442 }
433}443}
434444
=== 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 @@
147 i++;147 i++;
148148
149 if (lens.isGame() && isDTAPN) {149 if (lens.isGame() && isDTAPN) {
150 exporter.export(model, new dk.aau.cs.model.tapn.TAPNQuery(query.getProperty(), 0), new File(modelFile), new File(queryFile + i + ".q"), lens);150 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());
151 } else {151 } else {
152 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));152 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());
153 }153 }
154 }154 }
155 }155 }
156156
=== 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 @@
5252
53 protected VerifyTAPNOptions verificationOptions() {53 protected VerifyTAPNOptions verificationOptions() {
54 if(modelChecker instanceof VerifyPN){54 if(modelChecker instanceof VerifyPN){
55 return new VerifyPNOptions(k, TraceOption.NONE, SearchOption.BFS, false, ModelReduction.BOUNDPRESERVING, false, false, 1, QueryCategory.Default, AlgorithmOption.CERTAIN_ZERO, false, false, false);55 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);
56 } else if(modelChecker instanceof VerifyTAPN){56 } else if(modelChecker instanceof VerifyTAPN){
57 return new VerifyTAPNOptions(k, TraceOption.NONE, SearchOption.BFS, true, false, true, false, false, 1);57 return new VerifyTAPNOptions(k, TraceOption.NONE, SearchOption.BFS, true, false, true, false, false, 1);
58 } else if(modelChecker instanceof VerifyTAPNDiscreteVerification){58 } else if(modelChecker instanceof VerifyTAPNDiscreteVerification){
5959
=== 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 @@
6import java.awt.GridBagLayout;6import java.awt.GridBagLayout;
7import java.awt.Insets;7import java.awt.Insets;
8import java.awt.Window;8import java.awt.Window;
9import java.awt.event.ActionEvent;
10import java.awt.event.ActionListener;
9import java.awt.event.HierarchyEvent;11import java.awt.event.HierarchyEvent;
10import java.awt.event.HierarchyListener;12import java.awt.event.HierarchyListener;
13import java.io.File;
11import java.util.Comparator;14import java.util.Comparator;
12import java.util.List;15import java.util.List;
1316
@@ -15,29 +18,30 @@
15import javax.swing.table.DefaultTableModel;18import javax.swing.table.DefaultTableModel;
16import javax.swing.table.TableModel;19import javax.swing.table.TableModel;
17import javax.swing.table.TableRowSorter;20import javax.swing.table.TableRowSorter;
1821import dk.aau.cs.gui.TabContent;
22import dk.aau.cs.verification.*;
19import dk.aau.cs.Messenger;23import dk.aau.cs.Messenger;
20import dk.aau.cs.model.tapn.simulation.TAPNNetworkTrace;24import dk.aau.cs.model.tapn.simulation.TAPNNetworkTrace;
21import dk.aau.cs.util.MemoryMonitor;25import dk.aau.cs.util.MemoryMonitor;
22import dk.aau.cs.util.Tuple;26import dk.aau.cs.util.Tuple;
23import dk.aau.cs.util.VerificationCallback;27import dk.aau.cs.util.VerificationCallback;
24import dk.aau.cs.verification.IconSelector;28import pipe.dataLayer.TAPNQuery;
25import dk.aau.cs.verification.ModelChecker;
26import dk.aau.cs.verification.QueryResult;
27import dk.aau.cs.verification.QueryType;
28import dk.aau.cs.verification.VerificationResult;
2929
30public class RunVerification extends RunVerificationBase { 30public class RunVerification extends RunVerificationBase {
31 private final IconSelector iconSelector;31 private final IconSelector iconSelector;
32 private final VerificationCallback callback;32 private final VerificationCallback callback;
33 public RunVerification(ModelChecker modelChecker, IconSelector selector, Messenger messenger, VerificationCallback callback) {33 public RunVerification(ModelChecker modelChecker, IconSelector selector, Messenger messenger, VerificationCallback callback, String reducedNetFilePath, boolean reduceNetOnly) {
34 super(modelChecker, messenger);34 super(modelChecker, messenger, reducedNetFilePath, reduceNetOnly);
35 iconSelector = selector;35 iconSelector = selector;
36 this.callback = callback;36 this.callback = callback;
37 }37 }
38
39 public RunVerification(ModelChecker modelChecker, IconSelector selector, Messenger messenger, VerificationCallback callback) {
40 this(modelChecker, selector, messenger, callback, null, false);
41 }
38 42
39 public RunVerification(ModelChecker modelChecker, IconSelector selector, Messenger messenger) {43 public RunVerification(ModelChecker modelChecker, IconSelector selector, Messenger messenger) {
40 this(modelChecker, selector, messenger, null);44 this(modelChecker, selector, messenger, null, null, false);
41 }45 }
4246
43 @Override47 @Override
@@ -54,12 +58,14 @@
54 iconSelector.getIconFor(result)58 iconSelector.getIconFor(result)
55 );59 );
56 60
57 if (result.getTrace() != null) {61 if (!reducedNetOpened && result.getTrace() != null) {
58 CreateGui.getAnimator().setTrace(result.getTrace());62 CreateGui.getAnimator().setTrace(result.getTrace());
59 }63 }
60 }64 }
6165
62 }else{66 } else if(reduceNetOnly) {
67 //If the engine is only called to produce a reduced net, it will fail, but no error message should be shown
68 }else{
63 69
64 //Check if the is something like 70 //Check if the is something like
65 //verifyta: relocation_error:71 //verifyta: relocation_error:
@@ -116,7 +122,6 @@
116122
117 }123 }
118124
119
120 private JPanel createStatisticsPanel(final VerificationResult<TAPNNetworkTrace> result, boolean transitionPanel) {125 private JPanel createStatisticsPanel(final VerificationResult<TAPNNetworkTrace> result, boolean transitionPanel) {
121 JPanel headLinePanel = new JPanel(new GridBagLayout());126 JPanel headLinePanel = new JPanel(new GridBagLayout());
122 final JPanel fullPanel = new JPanel(new GridBagLayout());127 final JPanel fullPanel = new JPanel(new GridBagLayout());
@@ -311,13 +316,46 @@
311 }316 }
312 317
313 if(!result.getReductionResultAsString().isEmpty()){318 if(!result.getReductionResultAsString().isEmpty()){
314 JLabel reductionStatsLabet = new JLabel(toHTML(result.getReductionResultAsString()));319 JLabel reductionStatsLabel = new JLabel(toHTML(result.getReductionResultAsString()));
315 gbc = new GridBagConstraints();320 gbc = new GridBagConstraints();
316 gbc.gridx = 0;321 gbc.gridx = 0;
317 gbc.gridy = 6;322 gbc.gridy = 6;
318 gbc.insets = new Insets(0,0,20,-90);323 gbc.insets = new Insets(0,0,20,-90);
319 gbc.anchor = GridBagConstraints.WEST;324 gbc.anchor = GridBagConstraints.WEST;
320 panel.add(reductionStatsLabet, gbc);325
326 panel.add(reductionStatsLabel, gbc);
327
328 if(result.reductionRulesApplied()){
329 JButton openReducedButton = new JButton("Open reduced net");
330 openReducedButton.addActionListener(new ActionListener() {
331 public void actionPerformed(ActionEvent e) {
332 openReducedButton.setEnabled(false);
333 reducedNetOpened = true;
334 File reducedNetFile = new File(reducedNetFilePath);
335
336 if(reducedNetFile.exists() && reducedNetFile.isFile() && reducedNetFile.canRead()){
337 try {
338 TabContent reducedNetTab = TabContent.createNewTabFromPNMLFile(reducedNetFile);
339 reducedNetTab.setInitialName("reduced-" + CreateGui.getAppGui().getCurrentTabName());
340 TAPNQuery convertedQuery = dataLayerQuery.convertPropertyForReducedNet(reducedNetTab.currentTemplate().toString());
341 reducedNetTab.addQuery(convertedQuery);
342 CreateGui.openNewTabFromStream(reducedNetTab);
343 } catch (Exception e1){
344 JOptionPane.showMessageDialog(CreateGui.getApp(),
345 e1.getMessage(),
346 "Error loading reduced net file",
347 JOptionPane.ERROR_MESSAGE);
348 }
349 }
350 }
351 });
352 gbc = new GridBagConstraints();
353 gbc.gridx = 0;
354 gbc.gridy = 5;
355 gbc.insets = new Insets(0,0,10,0);
356 gbc.anchor = GridBagConstraints.WEST;
357 panel.add(openReducedButton, gbc);
358 }
321 }359 }
322 if (result.getRawOutput() != null) {360 if (result.getRawOutput() != null) {
323 JButton showRawQueryButton = new JButton("Show raw query results");361 JButton showRawQueryButton = new JButton("Show raw query results");
@@ -325,9 +363,9 @@
325 JOptionPane.showMessageDialog(panel, createRawQueryPanel(result.getRawOutput()), "Raw query results", JOptionPane.INFORMATION_MESSAGE);363 JOptionPane.showMessageDialog(panel, createRawQueryPanel(result.getRawOutput()), "Raw query results", JOptionPane.INFORMATION_MESSAGE);
326 });364 });
327 gbc = new GridBagConstraints();365 gbc = new GridBagConstraints();
328 gbc.gridx = 0;366 gbc.gridx = 1;
329 gbc.gridy = 5;367 gbc.gridy = 5;
330 gbc.insets = new Insets(10,0,10,0);368 gbc.insets = new Insets(0,0,10,0);
331 gbc.anchor = GridBagConstraints.WEST;369 gbc.anchor = GridBagConstraints.WEST;
332 panel.add(showRawQueryButton, gbc);370 panel.add(showRawQueryButton, gbc);
333 }371 }
334372
=== 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 @@
1package pipe.gui;1package pipe.gui;
22
3import java.io.File;
3import java.util.concurrent.ExecutionException;4import java.util.concurrent.ExecutionException;
45
5import javax.swing.SwingUtilities;6import javax.swing.SwingUtilities;
@@ -39,16 +40,25 @@
39 protected TimedArcPetriNetNetwork model;40 protected TimedArcPetriNetNetwork model;
40 protected TAPNQuery query;41 protected TAPNQuery query;
41 protected pipe.dataLayer.TAPNQuery dataLayerQuery;42 protected pipe.dataLayer.TAPNQuery dataLayerQuery;
43 protected String reducedNetFilePath;
44 protected boolean reduceNetOnly;
45 protected boolean reducedNetOpened = false;
42 46
43 47
44 protected Messenger messenger;48 protected Messenger messenger;
4549
46 public RunVerificationBase(ModelChecker modelChecker, Messenger messenger) {50 public RunVerificationBase(ModelChecker modelChecker, Messenger messenger, String reducedNetFilePath, boolean reduceNetOnly) {
47 super();51 super();
48 this.modelChecker = modelChecker;52 this.modelChecker = modelChecker;
49 this.messenger = messenger;53 this.messenger = messenger;
54 this.reducedNetFilePath = reducedNetFilePath;
55 this.reduceNetOnly = reduceNetOnly;
50 }56 }
5157
58 public RunVerificationBase(ModelChecker modelChecker, Messenger messenger) {
59 this(modelChecker, messenger, null, false);
60 }
61
52 62
53 public void execute(VerificationOptions options, TimedArcPetriNetNetwork model, TAPNQuery query, pipe.dataLayer.TAPNQuery dataLayerQuery) {63 public void execute(VerificationOptions options, TimedArcPetriNetNetwork model, TAPNQuery query, pipe.dataLayer.TAPNQuery dataLayerQuery) {
54 this.model = model;64 this.model = model;
@@ -110,8 +120,9 @@
110 dataLayerQuery.getCategory(),120 dataLayerQuery.getCategory(),
111 dataLayerQuery.getAlgorithmOption(),121 dataLayerQuery.getAlgorithmOption(),
112 dataLayerQuery.isSiphontrapEnabled(),122 dataLayerQuery.isSiphontrapEnabled(),
113 dataLayerQuery.isQueryReductionEnabled(),123 dataLayerQuery.isQueryReductionEnabled()? pipe.dataLayer.TAPNQuery.QueryReductionTime.UnlimitedTime: pipe.dataLayer.TAPNQuery.QueryReductionTime.NoTime,
114 dataLayerQuery.isStubbornReductionEnabled()124 dataLayerQuery.isStubbornReductionEnabled(),
125 reducedNetFilePath
115 ),126 ),
116 transformedModel,127 transformedModel,
117 clonedQuery128 clonedQuery
@@ -130,8 +141,9 @@
130 pipe.dataLayer.TAPNQuery.QueryCategory.Default,141 pipe.dataLayer.TAPNQuery.QueryCategory.Default,
131 pipe.dataLayer.TAPNQuery.AlgorithmOption.CERTAIN_ZERO,142 pipe.dataLayer.TAPNQuery.AlgorithmOption.CERTAIN_ZERO,
132 false,143 false,
133 true,144 pipe.dataLayer.TAPNQuery.QueryReductionTime.UnlimitedTime,
134 false145 false,
146 reducedNetFilePath
135 ),147 ),
136 transformedModel,148 transformedModel,
137 clonedQuery149 clonedQuery
138150
=== 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 @@
15import dk.aau.cs.verification.UPPAAL.Verifyta;15import dk.aau.cs.verification.UPPAAL.Verifyta;
16import dk.aau.cs.verification.UPPAAL.VerifytaOptions;16import dk.aau.cs.verification.UPPAAL.VerifytaOptions;
1717
18import java.io.File;
19import java.io.IOException;
20
18/**21/**
19 * Implementes af class for handling integrated Uppaal Verification22 * Implementes af class for handling integrated Uppaal Verification
20 * 23 *
@@ -24,6 +27,8 @@
24 */27 */
2528
26public class Verifier {29public class Verifier {
30 private static File reducedNetTempFile = null;
31
27 private static Verifyta getVerifyta() {32 private static Verifyta getVerifyta() {
28 Verifyta verifyta = new Verifyta(new FileFinder(), new MessengerImpl());33 Verifyta verifyta = new Verifyta(new FileFinder(), new MessengerImpl());
29 verifyta.setup();34 verifyta.setup();
@@ -61,6 +66,10 @@
61 }66 }
62 }67 }
6368
69 public static String getReducedNetFilePath() {
70 return reducedNetTempFile.getAbsolutePath();
71 }
72
64 public static void analyzeKBound(TimedArcPetriNetNetwork tapnNetwork, int k, JSpinner tokensControl) {73 public static void analyzeKBound(TimedArcPetriNetNetwork tapnNetwork, int k, JSpinner tokensControl) {
65 ModelChecker modelChecker;74 ModelChecker modelChecker;
66 75
@@ -129,10 +138,12 @@
129 public static void runVerifyTAPNVerification(138 public static void runVerifyTAPNVerification(
130 TimedArcPetriNetNetwork tapnNetwork,139 TimedArcPetriNetNetwork tapnNetwork,
131 TAPNQuery query,140 TAPNQuery query,
141 boolean onlyCreateReducedNet,
132 VerificationCallback callback142 VerificationCallback callback
133 ) {143 ) {
134 ModelChecker verifytapn = getModelChecker(query);144 ModelChecker verifytapn = getModelChecker(query);
135145
146
136 if (!verifytapn.isCorrectVersion()) {147 if (!verifytapn.isCorrectVersion()) {
137 new MessengerImpl().displayErrorMessage(148 new MessengerImpl().displayErrorMessage(
138 "No "+verifytapn+" specified: The verification is cancelled",149 "No "+verifytapn+" specified: The verification is cancelled",
@@ -165,21 +176,53 @@
165 query.isStubbornReductionEnabled()176 query.isStubbornReductionEnabled()
166 );177 );
167 } else if(query.getReductionOption() == ReductionOption.VerifyPN){178 } else if(query.getReductionOption() == ReductionOption.VerifyPN){
168 verifytapnOptions = new VerifyPNOptions(179
169 bound,180 try {
170 query.getTraceOption(),181 reducedNetTempFile = File.createTempFile("reduced-", ".pnml");
171 query.getSearchOption(),182 } catch (IOException e) {
172 query.useOverApproximation(),183 new MessengerImpl().displayErrorMessage(
173 query.useReduction()? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION,184 e.getMessage(),
174 query.isOverApproximationEnabled(),185 "Error");
175 query.isUnderApproximationEnabled(),186 return;
176 query.approximationDenominator(),187 }
177 query.getCategory(),188
178 query.getAlgorithmOption(),189 if (onlyCreateReducedNet) {
179 query.isSiphontrapEnabled(),190 //These options should disable the verification and only produce the net after applying reduction rules
180 query.isQueryReductionEnabled(),191 verifytapnOptions = new VerifyPNOptions(
181 query.isStubbornReductionEnabled()192 bound,
182 );193 query.getTraceOption(),
194 TAPNQuery.SearchOption.OVERAPPROXIMATE,
195 query.useOverApproximation(),
196 query.useReduction()? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION,
197 query.isOverApproximationEnabled(),
198 query.isUnderApproximationEnabled(),
199 query.approximationDenominator(),
200 query.getCategory(),
201 query.getAlgorithmOption(),
202 query.isSiphontrapEnabled(),
203 TAPNQuery.QueryReductionTime.NoTime,
204 query.isStubbornReductionEnabled(),
205 reducedNetTempFile.getAbsolutePath()
206 );
207 } else {
208 verifytapnOptions = new VerifyPNOptions(
209 bound,
210 query.getTraceOption(),
211 query.getSearchOption(),
212 query.useOverApproximation(),
213 query.useReduction()? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION,
214 query.isOverApproximationEnabled(),
215 query.isUnderApproximationEnabled(),
216 query.approximationDenominator(),
217 query.getCategory(),
218 query.getAlgorithmOption(),
219 query.isSiphontrapEnabled(),
220 query.isQueryReductionEnabled()? TAPNQuery.QueryReductionTime.UnlimitedTime: TAPNQuery.QueryReductionTime.NoTime,
221 query.isStubbornReductionEnabled(),
222 reducedNetTempFile.getAbsolutePath()
223 );
224 }
225
183 } else {226 } else {
184 verifytapnOptions = new VerifyTAPNOptions(227 verifytapnOptions = new VerifyTAPNOptions(
185 bound,228 bound,
@@ -200,7 +243,13 @@
200 }243 }
201 244
202 if (tapnNetwork != null) {245 if (tapnNetwork != null) {
203 RunVerificationBase thread = new RunVerification(verifytapn, new VerifyTAPNIconSelector(), new MessengerImpl(), callback);246 RunVerificationBase thread;
247 if (reducedNetTempFile != null) {
248 thread = new RunVerification(verifytapn, new VerifyTAPNIconSelector(), new MessengerImpl(), callback, reducedNetTempFile.getAbsolutePath(), onlyCreateReducedNet );
249 } else {
250 thread = new RunVerification(verifytapn, new VerifyTAPNIconSelector(), new MessengerImpl(), callback);
251 }
252
204 RunningVerificationDialog dialog = new RunningVerificationDialog(CreateGui.getApp(), thread);253 RunningVerificationDialog dialog = new RunningVerificationDialog(CreateGui.getApp(), thread);
205 thread.execute(verifytapnOptions, tapnNetwork, new dk.aau.cs.model.tapn.TAPNQuery(query.getProperty(), bound), query);254 thread.execute(verifytapnOptions, tapnNetwork, new dk.aau.cs.model.tapn.TAPNQuery(query.getProperty(), bound), query);
206 dialog.setVisible(true);255 dialog.setVisible(true);
207256
=== 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 @@
17import java.util.Vector;17import java.util.Vector;
1818
19import javax.swing.*;19import javax.swing.*;
20import javax.swing.event.DocumentEvent;20import javax.swing.event.*;
21import javax.swing.event.DocumentListener;
22import javax.swing.event.UndoableEditEvent;
23import javax.swing.event.UndoableEditListener;
24import javax.swing.text.MutableAttributeSet;21import javax.swing.text.MutableAttributeSet;
25import javax.swing.text.SimpleAttributeSet;22import javax.swing.text.SimpleAttributeSet;
26import javax.swing.text.StyleConstants;23import javax.swing.text.StyleConstants;
@@ -70,6 +67,7 @@
70 private static final String EXPORT_VERIFYTAPN_BTN_TEXT = "Export TAPAAL XML";67 private static final String EXPORT_VERIFYTAPN_BTN_TEXT = "Export TAPAAL XML";
71 private static final String EXPORT_VERIFYPN_BTN_TEXT = "Export PN XML";68 private static final String EXPORT_VERIFYPN_BTN_TEXT = "Export PN XML";
72 private static final String EXPORT_COMPOSED_BTN_TEXT = "Merge net components";69 private static final String EXPORT_COMPOSED_BTN_TEXT = "Merge net components";
70 private static final String OPEN_REDUCED_BTN_TEXT = "Open reduced net";
7371
74 private static final String UPPAAL_SOME_TRACE_STRING = "Some trace ";72 private static final String UPPAAL_SOME_TRACE_STRING = "Some trace ";
75 private static final String SOME_TRACE_STRING = "Some trace ";73 private static final String SOME_TRACE_STRING = "Some trace ";
@@ -183,6 +181,7 @@
183 private JButton saveAndVerifyButton;181 private JButton saveAndVerifyButton;
184 private JButton saveUppaalXMLButton;182 private JButton saveUppaalXMLButton;
185 private JButton mergeNetComponentsButton;183 private JButton mergeNetComponentsButton;
184 private JButton openReducedNetButton;
186185
187 // Private Members186 // Private Members
188 private StringPosition currentSelection = null;187 private StringPosition currentSelection = null;
@@ -313,6 +312,7 @@
313 private final static String TOOL_TIP_CANCEL_BUTTON = "Cancel the changes made in this dialog.";312 private final static String TOOL_TIP_CANCEL_BUTTON = "Cancel the changes made in this dialog.";
314 private final static String TOOL_TIP_SAVE_UPPAAL_BUTTON = "Export an xml file that can be opened in UPPAAL GUI.";313 private final static String TOOL_TIP_SAVE_UPPAAL_BUTTON = "Export an xml file that can be opened in UPPAAL GUI.";
315 private final static String TOOL_TIP_SAVE_COMPOSED_BUTTON = "Export an xml file of composed net and approximated net if enabled";314 private final static String TOOL_TIP_SAVE_COMPOSED_BUTTON = "Export an xml file of composed net and approximated net if enabled";
315 private final static String TOOL_TIP_OPEN_REDUCED_BUTTON = "Open the net produced after applying structural reduction rules";
316 private final static String TOOL_TIP_SAVE_TAPAAL_BUTTON = "Export an xml file that can be used as input for the TAPAAL engine.";316 private final static String TOOL_TIP_SAVE_TAPAAL_BUTTON = "Export an xml file that can be used as input for the TAPAAL engine.";
317 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.";317 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.";
318318
@@ -676,7 +676,7 @@
676 current = ((TCTLStateToPathConverter) current).getProperty();676 current = ((TCTLStateToPathConverter) current).getProperty();
677 }677 }
678 if (current instanceof TCTLAtomicPropositionNode) {678 if (current instanceof TCTLAtomicPropositionNode) {
679 TCTLAtomicPropositionNode node = (TCTLAtomicPropositionNode) currentSelection.getObject();679 TCTLAtomicPropositionNode node = (TCTLAtomicPropositionNode) current;
680680
681 // bit of a hack to prevent posting edits to the undo manager when681 // bit of a hack to prevent posting edits to the undo manager when
682 // we programmatically change the selection in the atomic proposition comboboxes etc.682 // we programmatically change the selection in the atomic proposition comboboxes etc.
@@ -811,11 +811,13 @@
811 saveAndVerifyButton.setEnabled(isQueryOk);811 saveAndVerifyButton.setEnabled(isQueryOk);
812 saveUppaalXMLButton.setEnabled(isQueryOk);812 saveUppaalXMLButton.setEnabled(isQueryOk);
813 mergeNetComponentsButton.setEnabled(isQueryOk);813 mergeNetComponentsButton.setEnabled(isQueryOk);
814 openReducedNetButton.setEnabled(isQueryOk && useReduction.isSelected());
814 } else {815 } else {
815 saveButton.setEnabled(false);816 saveButton.setEnabled(false);
816 saveAndVerifyButton.setEnabled(false);817 saveAndVerifyButton.setEnabled(false);
817 saveUppaalXMLButton.setEnabled(false);818 saveUppaalXMLButton.setEnabled(false);
818 mergeNetComponentsButton.setEnabled(false);819 mergeNetComponentsButton.setEnabled(false);
820 openReducedNetButton.setEnabled(false);
819 }821 }
820 }822 }
821823
@@ -1454,9 +1456,12 @@
1454 if (lens.isTimed() || lens.isGame()) {1456 if (lens.isTimed() || lens.isGame()) {
1455 saveUppaalXMLButton.setVisible(advancedView);1457 saveUppaalXMLButton.setVisible(advancedView);
1456 overApproximationOptionsPanel.setVisible(advancedView);1458 overApproximationOptionsPanel.setVisible(advancedView);
1459 } else if (!lens.isGame()){
1460 openReducedNetButton.setVisible(advancedView);
1457 }1461 }
1458 mergeNetComponentsButton.setVisible(advancedView);1462 mergeNetComponentsButton.setVisible(advancedView);
14591463
1464
1460 if(advancedView){1465 if(advancedView){
1461 advancedButton.setText("Simple view");1466 advancedButton.setText("Simple view");
1462 advancedButton.setToolTipText(TOOL_TIP_SIMPLE_VIEW_BUTTON);1467 advancedButton.setToolTipText(TOOL_TIP_SIMPLE_VIEW_BUTTON);
@@ -2679,6 +2684,13 @@
2679 if (lens.isTimed() || lens.isGame()) {2684 if (lens.isTimed() || lens.isGame()) {
2680 initTimedReductionOptions();2685 initTimedReductionOptions();
2681 } else {2686 } else {
2687 useReduction.addActionListener(new ActionListener() {
2688 @Override
2689 public void actionPerformed(ActionEvent actionEvent) {
2690 openReducedNetButton.setEnabled(useReduction.isSelected() && getQueryComment().length() > 0
2691 && !newProperty.containsPlaceHolder());
2692 }
2693 });
2682 initUntimedReductionOptions();2694 initUntimedReductionOptions();
2683 }2695 }
26842696
@@ -2962,6 +2974,10 @@
2962 mergeNetComponentsButton = new JButton(EXPORT_COMPOSED_BTN_TEXT);2974 mergeNetComponentsButton = new JButton(EXPORT_COMPOSED_BTN_TEXT);
2963 mergeNetComponentsButton.setVisible(false);2975 mergeNetComponentsButton.setVisible(false);
29642976
2977 openReducedNetButton = new JButton(OPEN_REDUCED_BTN_TEXT);
2978 openReducedNetButton.setVisible(false);
2979
2980
2965 saveUppaalXMLButton = new JButton(EXPORT_UPPAAL_BTN_TEXT);2981 saveUppaalXMLButton = new JButton(EXPORT_UPPAAL_BTN_TEXT);
2966 //Only show in advanced mode2982 //Only show in advanced mode
2967 saveUppaalXMLButton.setVisible(false);2983 saveUppaalXMLButton.setVisible(false);
@@ -2972,6 +2988,7 @@
2972 cancelButton.setToolTipText(TOOL_TIP_CANCEL_BUTTON);2988 cancelButton.setToolTipText(TOOL_TIP_CANCEL_BUTTON);
2973 saveUppaalXMLButton.setToolTipText(TOOL_TIP_SAVE_UPPAAL_BUTTON);2989 saveUppaalXMLButton.setToolTipText(TOOL_TIP_SAVE_UPPAAL_BUTTON);
2974 mergeNetComponentsButton.setToolTipText(TOOL_TIP_SAVE_COMPOSED_BUTTON);2990 mergeNetComponentsButton.setToolTipText(TOOL_TIP_SAVE_COMPOSED_BUTTON);
2991 openReducedNetButton.setToolTipText(TOOL_TIP_OPEN_REDUCED_BUTTON);
29752992
2976 saveButton.addActionListener(new ActionListener() {2993 saveButton.addActionListener(new ActionListener() {
2977 public void actionPerformed(ActionEvent evt) {2994 public void actionPerformed(ActionEvent evt) {
@@ -2995,7 +3012,7 @@
2995 TAPNQuery query = getQuery();3012 TAPNQuery query = getQuery();
29963013
2997 if(query.getReductionOption() == ReductionOption.VerifyTAPN || query.getReductionOption() == ReductionOption.VerifyTAPNdiscreteVerification || query.getReductionOption() == ReductionOption.VerifyPN)3014 if(query.getReductionOption() == ReductionOption.VerifyTAPN || query.getReductionOption() == ReductionOption.VerifyTAPNdiscreteVerification || query.getReductionOption() == ReductionOption.VerifyPN)
2998 Verifier.runVerifyTAPNVerification(tapnNetwork, query, null);3015 Verifier.runVerifyTAPNVerification(tapnNetwork, query, false, null);
2999 else3016 else
3000 Verifier.runUppaalVerification(tapnNetwork, query);3017 Verifier.runUppaalVerification(tapnNetwork, query);
3001 }}3018 }}
@@ -3049,10 +3066,12 @@
3049 }3066 }
3050 if(reduction == ReductionOption.VerifyTAPN || reduction == ReductionOption.VerifyTAPNdiscreteVerification) {3067 if(reduction == ReductionOption.VerifyTAPN || reduction == ReductionOption.VerifyTAPNdiscreteVerification) {
3051 VerifyTAPNExporter exporter = new VerifyTAPNExporter();3068 VerifyTAPNExporter exporter = new VerifyTAPNExporter();
3052 exporter.export(transformedModel.value1(), clonedQuery, new File(xmlFile), new File(queryFile), lens);3069 exporter.export(transformedModel.value1(), clonedQuery, new File(xmlFile), new File(queryFile), tapnQuery, lens, transformedModel.value2());
3070
3053 } else if(reduction == ReductionOption.VerifyPN){3071 } else if(reduction == ReductionOption.VerifyPN){
3054 VerifyPNExporter exporter = new VerifyPNExporter();3072 VerifyPNExporter exporter = new VerifyPNExporter();
3055 exporter.export(transformedModel.value1(), clonedQuery, new File(xmlFile), new File(queryFile), lens);3073 exporter.export(transformedModel.value1(), clonedQuery, new File(xmlFile), new File(queryFile), tapnQuery, lens, transformedModel.value2());
3074
3056 } else {3075 } else {
3057 UppaalExporter exporter = new UppaalExporter();3076 UppaalExporter exporter = new UppaalExporter();
3058 try {3077 try {
@@ -3117,6 +3136,51 @@
3117 }3136 }
3118 });3137 });
31193138
3139 openReducedNetButton.addActionListener(new ActionListener() {
3140 public void actionPerformed(ActionEvent e) {
3141
3142
3143 if (checkIfSomeReductionOption()) {
3144 querySaved = true;
3145 // Now if a query is saved and verified, the net is marked as modified
3146 CreateGui.getCurrentTab().setNetChanged(true);
3147
3148 TAPNQuery query = getQuery();
3149 if(query.getReductionOption() != ReductionOption.VerifyPN) {
3150 JOptionPane.showMessageDialog(CreateGui.getApp(),
3151 "The selected verification engine does not support application of reduction rules",
3152 "Reduction rules unsupported", JOptionPane.ERROR_MESSAGE);
3153 return;
3154 }
3155
3156 exit();
3157
3158 Verifier.runVerifyTAPNVerification(tapnNetwork, query,true, null);
3159
3160 File reducedNetFile = new File(Verifier.getReducedNetFilePath());
3161
3162 if(reducedNetFile.exists() && reducedNetFile.isFile() && reducedNetFile.canRead()){
3163 try {
3164 TabContent reducedNetTab = TabContent.createNewTabFromPNMLFile(reducedNetFile);
3165 //Ensure that a net was created by the query reduction
3166 if(reducedNetTab.currentTemplate().guiModel().getPlaces().length > 0
3167 || reducedNetTab.currentTemplate().guiModel().getTransitions().length > 0){
3168 reducedNetTab.setInitialName("reduced-" + CreateGui.getAppGui().getCurrentTabName());
3169 TAPNQuery convertedQuery = query.convertPropertyForReducedNet(reducedNetTab.currentTemplate().toString());
3170 reducedNetTab.addQuery(convertedQuery);
3171 CreateGui.openNewTabFromStream(reducedNetTab);
3172 }
3173 } catch (Exception e1){
3174 JOptionPane.showMessageDialog(CreateGui.getApp(),
3175 e1.getMessage(),
3176 "Error loading reduced net file",
3177 JOptionPane.ERROR_MESSAGE);
3178 }
3179 }
3180 }
3181 }
3182 });
3183
31203184
3121 } else if (option == QueryDialogueOption.Export) {3185 } else if (option == QueryDialogueOption.Export) {
3122 saveButton = new JButton("export");3186 saveButton = new JButton("export");
@@ -3133,6 +3197,7 @@
3133 JPanel leftButtomPanel = new JPanel(new FlowLayout());3197 JPanel leftButtomPanel = new JPanel(new FlowLayout());
3134 JPanel rightButtomPanel = new JPanel(new FlowLayout());3198 JPanel rightButtomPanel = new JPanel(new FlowLayout());
3135 leftButtomPanel.add(mergeNetComponentsButton, FlowLayout.LEFT);3199 leftButtomPanel.add(mergeNetComponentsButton, FlowLayout.LEFT);
3200 leftButtomPanel.add(openReducedNetButton, FlowLayout.LEFT);
3136 leftButtomPanel.add(saveUppaalXMLButton, FlowLayout.LEFT);3201 leftButtomPanel.add(saveUppaalXMLButton, FlowLayout.LEFT);
31373202
31383203
31393204
=== 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 @@
440 440
441 if(NumberOfSelectedElements == 1) {441 if(NumberOfSelectedElements == 1) {
442 if(query.getReductionOption() == ReductionOption.VerifyTAPN || query.getReductionOption() == ReductionOption.VerifyTAPNdiscreteVerification || query.getReductionOption() == ReductionOption.VerifyPN)442 if(query.getReductionOption() == ReductionOption.VerifyTAPN || query.getReductionOption() == ReductionOption.VerifyTAPNdiscreteVerification || query.getReductionOption() == ReductionOption.VerifyPN)
443 Verifier.runVerifyTAPNVerification(tabContent.network(), query, null);443 Verifier.runVerifyTAPNVerification(tabContent.network(), query, false, null);
444 else444 else
445 Verifier.runUppaalVerification(tabContent.network(), query);445 Verifier.runUppaalVerification(tabContent.network(), query);
446 }446 }
447447
=== 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 @@
1010 WorkflowMode.WORKFLOW_STRONG_SOUNDNESS,1010 WorkflowMode.WORKFLOW_STRONG_SOUNDNESS,
1011 c1011 c
1012 );1012 );
1013 Verifier.runVerifyTAPNVerification(model, q, result -> {1013 Verifier.runVerifyTAPNVerification(model, q, false, result -> {
1014 if(result.isQuerySatisfied()){1014 if(result.isQuerySatisfied()){
10151015
1016 switch(((TimedTAPNNetworkTrace) result.getTrace()).getTraceType()){1016 switch(((TimedTAPNNetworkTrace) result.getTrace()).getTraceType()){
@@ -1115,7 +1115,7 @@
1115 ExtrapolationOption.AUTOMATIC,1115 ExtrapolationOption.AUTOMATIC,
1116 WorkflowMode.WORKFLOW_SOUNDNESS1116 WorkflowMode.WORKFLOW_SOUNDNESS
1117 );1117 );
1118 Verifier.runVerifyTAPNVerification(model, q, new VerificationCallback() {1118 Verifier.runVerifyTAPNVerification(model, q, false, new VerificationCallback() {
11191119
1120 @Override1120 @Override
1121 public void run(VerificationResult<TAPNNetworkTrace> result) {1121 public void run(VerificationResult<TAPNNetworkTrace> result) {
@@ -1225,7 +1225,7 @@
1225 null,1225 null,
1226 ExtrapolationOption.AUTOMATIC1226 ExtrapolationOption.AUTOMATIC
1227 );1227 );
1228 Verifier.runVerifyTAPNVerification(model, q, new VerificationCallback() {1228 Verifier.runVerifyTAPNVerification(model, q, false, new VerificationCallback() {
12291229
1230 @Override1230 @Override
1231 public void run(VerificationResult<TAPNNetworkTrace> result) {1231 public void run(VerificationResult<TAPNNetworkTrace> result) {

Subscribers

People subscribed via source and target branches