TAPAAL

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

  1. show-reduced-net-1879130
  2. Merge into trunk
Proposed by Thomas Pedersen on 2020-09-18
Status: Merged
Approved by: Jiri Srba on 2020-12-18
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 2020-09-18 Approve on 2020-12-18
Thomas Pedersen (community) Resubmit on 2020-12-17
Kenneth Yrke Jørgensen code Approve on 2020-11-09
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
lp:~tapaal-contributor/tapaal/show-reduced-net-1879130 updated on 2020-10-15
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: Resubmit
Kenneth Yrke Jørgensen (yrke) :
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
lp:~tapaal-contributor/tapaal/show-reduced-net-1879130 updated on 2020-10-31
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: Resubmit
lp:~tapaal-contributor/tapaal/show-reduced-net-1879130 updated on 2020-11-06
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: Resubmit
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
lp:~tapaal-contributor/tapaal/show-reduced-net-1879130 updated on 2020-11-11
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: Resubmit
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
lp:~tapaal-contributor/tapaal/show-reduced-net-1879130 updated on 2020-11-13
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: Resubmit
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
lp:~tapaal-contributor/tapaal/show-reduced-net-1879130 updated on 2020-12-16
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
lp:~tapaal-contributor/tapaal/show-reduced-net-1879130 updated on 2020-12-17
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: Resubmit
Jiri Srba (srba) :
review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'gradlew' (properties changed: -x to +x)
2=== modified file 'src/dk/aau/cs/TCTL/AritmeticOperator.java'
3--- src/dk/aau/cs/TCTL/AritmeticOperator.java 2020-08-17 08:09:43 +0000
4+++ src/dk/aau/cs/TCTL/AritmeticOperator.java 2020-12-17 21:03:24 +0000
5@@ -22,7 +22,11 @@
6 }
7 }
8
9- @Override
10+ @Override
11+ public void convertForReducedNet(String templateName) {
12+ }
13+
14+ @Override
15 public TCTLAbstractStateProperty copy() {
16 return new AritmeticOperator(operator);
17 }
18
19=== modified file 'src/dk/aau/cs/TCTL/TCTLAFNode.java'
20--- src/dk/aau/cs/TCTL/TCTLAFNode.java 2020-08-17 08:09:43 +0000
21+++ src/dk/aau/cs/TCTL/TCTLAFNode.java 2020-12-17 21:03:24 +0000
22@@ -41,7 +41,12 @@
23 return children;
24 }
25
26- @Override
27+ @Override
28+ public void convertForReducedNet(String templateName) {
29+ property.convertForReducedNet(templateName);
30+ }
31+
32+ @Override
33 public boolean equals(Object o) {
34 if (o instanceof TCTLAFNode) {
35 TCTLAFNode node = (TCTLAFNode) o;
36
37=== modified file 'src/dk/aau/cs/TCTL/TCTLAGNode.java'
38--- src/dk/aau/cs/TCTL/TCTLAGNode.java 2020-08-17 08:09:43 +0000
39+++ src/dk/aau/cs/TCTL/TCTLAGNode.java 2020-12-17 21:03:24 +0000
40@@ -41,7 +41,12 @@
41 return children;
42 }
43
44- @Override
45+ @Override
46+ public void convertForReducedNet(String templateName) {
47+ property.convertForReducedNet(templateName);
48+ }
49+
50+ @Override
51 public boolean equals(Object o) {
52 if (o instanceof TCTLAGNode) {
53 TCTLAGNode node = (TCTLAGNode) o;
54
55=== modified file 'src/dk/aau/cs/TCTL/TCTLAUNode.java'
56--- src/dk/aau/cs/TCTL/TCTLAUNode.java 2020-08-17 08:09:43 +0000
57+++ src/dk/aau/cs/TCTL/TCTLAUNode.java 2020-12-17 21:03:24 +0000
58@@ -58,7 +58,13 @@
59 return children;
60 }
61
62- @Override
63+ @Override
64+ public void convertForReducedNet(String templateName) {
65+ left.convertForReducedNet(templateName);
66+ right.convertForReducedNet(templateName);
67+ }
68+
69+ @Override
70 public boolean equals(Object o) {
71 if (o instanceof TCTLAUNode) {
72 TCTLAUNode node = (TCTLAUNode) o;
73
74=== modified file 'src/dk/aau/cs/TCTL/TCTLAXNode.java'
75--- src/dk/aau/cs/TCTL/TCTLAXNode.java 2020-08-17 08:09:43 +0000
76+++ src/dk/aau/cs/TCTL/TCTLAXNode.java 2020-12-17 21:03:24 +0000
77@@ -41,7 +41,12 @@
78 return children;
79 }
80
81- @Override
82+ @Override
83+ public void convertForReducedNet(String templateName) {
84+ property.convertForReducedNet(templateName);
85+ }
86+
87+ @Override
88 public boolean equals(Object o) {
89 if (o instanceof TCTLAXNode) {
90 TCTLAXNode node = (TCTLAXNode) o;
91
92=== modified file 'src/dk/aau/cs/TCTL/TCTLAbstractProperty.java'
93--- src/dk/aau/cs/TCTL/TCTLAbstractProperty.java 2020-08-17 08:09:43 +0000
94+++ src/dk/aau/cs/TCTL/TCTLAbstractProperty.java 2020-12-17 21:03:24 +0000
95@@ -51,6 +51,8 @@
96 return children;
97 }
98
99+ public abstract void convertForReducedNet(String templateName);
100+
101 public abstract void accept(ITCTLVisitor visitor, Object context);
102
103 public abstract boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName);
104
105=== modified file 'src/dk/aau/cs/TCTL/TCTLAndListNode.java'
106--- src/dk/aau/cs/TCTL/TCTLAndListNode.java 2020-08-17 08:09:43 +0000
107+++ src/dk/aau/cs/TCTL/TCTLAndListNode.java 2020-12-17 21:03:24 +0000
108@@ -122,7 +122,14 @@
109 return children;
110 }
111
112- @Override
113+ @Override
114+ public void convertForReducedNet(String templateName) {
115+ for (TCTLAbstractProperty property : properties){
116+ property.convertForReducedNet(templateName);
117+ }
118+ }
119+
120+ @Override
121 public boolean equals(Object o) {
122 if (o instanceof TCTLAndListNode) {
123 TCTLAndListNode node = (TCTLAndListNode) o;
124
125=== modified file 'src/dk/aau/cs/TCTL/TCTLAtomicPropositionNode.java'
126--- src/dk/aau/cs/TCTL/TCTLAtomicPropositionNode.java 2020-08-17 08:09:43 +0000
127+++ src/dk/aau/cs/TCTL/TCTLAtomicPropositionNode.java 2020-12-17 21:03:24 +0000
128@@ -67,7 +67,13 @@
129 }
130 }
131
132- @Override
133+ @Override
134+ public void convertForReducedNet(String templateName) {
135+ left.convertForReducedNet(templateName);
136+ right.convertForReducedNet(templateName);
137+ }
138+
139+ @Override
140 public String toString() {
141 return left + " " + op + " " + right;
142 }
143@@ -88,6 +94,31 @@
144 return false;
145 }
146
147+/* @Override
148+ public StringPosition[] getChildren() {
149+ StringPosition[] children = new StringPosition[2];
150+
151+ int start = 0;
152+ int end = 0;
153+ boolean leftSimpleProperty = left.isSimpleProperty();
154+
155+ start = leftSimpleProperty ? 0 : 1;
156+ end = start + left.toString().length();
157+
158+ StringPosition posLeft = new StringPosition(start, end, left);
159+
160+ start = end + 5 + (right.isSimpleProperty() ? 0 : 1)
161+ + (leftSimpleProperty ? 0 : 1);
162+
163+ end = start + right.toString().length();
164+
165+ StringPosition posRight = new StringPosition(start, end, right);
166+
167+ children[0] = posLeft;
168+ children[1] = posRight;
169+ return children;
170+ }*/
171+
172 @Override
173 public TCTLAbstractProperty findFirstPlaceHolder() {
174 TCTLAbstractProperty rightP = right.findFirstPlaceHolder();
175
176=== modified file 'src/dk/aau/cs/TCTL/TCTLConstNode.java'
177--- src/dk/aau/cs/TCTL/TCTLConstNode.java 2020-08-17 08:09:43 +0000
178+++ src/dk/aau/cs/TCTL/TCTLConstNode.java 2020-12-17 21:03:24 +0000
179@@ -26,7 +26,12 @@
180 }
181 }
182
183- @Override
184+ @Override
185+ public void convertForReducedNet(String templateName) {
186+
187+ }
188+
189+ @Override
190 public TCTLAbstractStateProperty copy() {
191 return new TCTLConstNode(constant);
192 }
193
194=== modified file 'src/dk/aau/cs/TCTL/TCTLDeadlockNode.java'
195--- src/dk/aau/cs/TCTL/TCTLDeadlockNode.java 2020-08-17 08:09:43 +0000
196+++ src/dk/aau/cs/TCTL/TCTLDeadlockNode.java 2020-12-17 21:03:24 +0000
197@@ -18,7 +18,11 @@
198 }
199 }
200
201- @Override
202+ @Override
203+ public void convertForReducedNet(String templateName) {
204+ }
205+
206+ @Override
207 public void accept(ITCTLVisitor visitor, Object context) {
208 visitor.visit(this, context);
209 }
210
211=== modified file 'src/dk/aau/cs/TCTL/TCTLEFNode.java'
212--- src/dk/aau/cs/TCTL/TCTLEFNode.java 2020-08-17 08:09:43 +0000
213+++ src/dk/aau/cs/TCTL/TCTLEFNode.java 2020-12-17 21:03:24 +0000
214@@ -41,7 +41,12 @@
215 return children;
216 }
217
218- @Override
219+ @Override
220+ public void convertForReducedNet(String templateName) {
221+ property.convertForReducedNet(templateName);
222+ }
223+
224+ @Override
225 public boolean equals(Object o) {
226 if (o instanceof TCTLEFNode) {
227 TCTLEFNode node = (TCTLEFNode) o;
228
229=== modified file 'src/dk/aau/cs/TCTL/TCTLEGNode.java'
230--- src/dk/aau/cs/TCTL/TCTLEGNode.java 2020-08-17 08:09:43 +0000
231+++ src/dk/aau/cs/TCTL/TCTLEGNode.java 2020-12-17 21:03:24 +0000
232@@ -41,7 +41,12 @@
233 return children;
234 }
235
236- @Override
237+ @Override
238+ public void convertForReducedNet(String templateName) {
239+ property.convertForReducedNet(templateName);
240+ }
241+
242+ @Override
243 public boolean equals(Object o) {
244 if (o instanceof TCTLEGNode) {
245 TCTLEGNode node = (TCTLEGNode) o;
246
247=== modified file 'src/dk/aau/cs/TCTL/TCTLEUNode.java'
248--- src/dk/aau/cs/TCTL/TCTLEUNode.java 2020-08-17 08:09:43 +0000
249+++ src/dk/aau/cs/TCTL/TCTLEUNode.java 2020-12-17 21:03:24 +0000
250@@ -58,7 +58,13 @@
251 return children;
252 }
253
254- @Override
255+ @Override
256+ public void convertForReducedNet(String templateName) {
257+ left.convertForReducedNet(templateName);
258+ right.convertForReducedNet(templateName);
259+ }
260+
261+ @Override
262 public boolean equals(Object o) {
263 if (o instanceof TCTLEUNode) {
264 TCTLEUNode node = (TCTLEUNode) o;
265
266=== modified file 'src/dk/aau/cs/TCTL/TCTLEXNode.java'
267--- src/dk/aau/cs/TCTL/TCTLEXNode.java 2020-08-17 08:09:43 +0000
268+++ src/dk/aau/cs/TCTL/TCTLEXNode.java 2020-12-17 21:03:24 +0000
269@@ -41,7 +41,12 @@
270 return children;
271 }
272
273- @Override
274+ @Override
275+ public void convertForReducedNet(String templateName) {
276+ property.convertForReducedNet(templateName);
277+ }
278+
279+ @Override
280 public boolean equals(Object o) {
281 if (o instanceof TCTLEXNode) {
282 TCTLEXNode node = (TCTLEXNode) o;
283
284=== modified file 'src/dk/aau/cs/TCTL/TCTLFalseNode.java'
285--- src/dk/aau/cs/TCTL/TCTLFalseNode.java 2020-08-17 08:09:43 +0000
286+++ src/dk/aau/cs/TCTL/TCTLFalseNode.java 2020-12-17 21:03:24 +0000
287@@ -18,7 +18,11 @@
288 }
289 }
290
291- @Override
292+ @Override
293+ public void convertForReducedNet(String templateName) {
294+ }
295+
296+ @Override
297 public void accept(ITCTLVisitor visitor, Object context) {
298 visitor.visit(this, context);
299 }
300
301=== modified file 'src/dk/aau/cs/TCTL/TCTLNotNode.java'
302--- src/dk/aau/cs/TCTL/TCTLNotNode.java 2020-08-17 08:09:43 +0000
303+++ src/dk/aau/cs/TCTL/TCTLNotNode.java 2020-12-17 21:03:24 +0000
304@@ -52,7 +52,12 @@
305 return children;
306 }
307
308- @Override
309+ @Override
310+ public void convertForReducedNet(String templateName) {
311+ property.convertForReducedNet(templateName);
312+ }
313+
314+ @Override
315 public TCTLAbstractStateProperty copy() {
316 return new TCTLNotNode(property.copy());
317 }
318
319=== modified file 'src/dk/aau/cs/TCTL/TCTLOrListNode.java'
320--- src/dk/aau/cs/TCTL/TCTLOrListNode.java 2020-08-17 08:09:43 +0000
321+++ src/dk/aau/cs/TCTL/TCTLOrListNode.java 2020-12-17 21:03:24 +0000
322@@ -122,7 +122,14 @@
323 return children;
324 }
325
326- @Override
327+ @Override
328+ public void convertForReducedNet(String templateName) {
329+ for(TCTLAbstractProperty property : properties){
330+ property.convertForReducedNet(templateName);
331+ }
332+ }
333+
334+ @Override
335 public boolean equals(Object o) {
336 if (o instanceof TCTLOrListNode) {
337 TCTLOrListNode node = (TCTLOrListNode) o;
338
339=== modified file 'src/dk/aau/cs/TCTL/TCTLPathPlaceHolder.java'
340--- src/dk/aau/cs/TCTL/TCTLPathPlaceHolder.java 2020-08-17 08:09:43 +0000
341+++ src/dk/aau/cs/TCTL/TCTLPathPlaceHolder.java 2020-12-17 21:03:24 +0000
342@@ -49,7 +49,12 @@
343 }
344 }
345
346- @Override
347+ @Override
348+ public void convertForReducedNet(String templateName) {
349+
350+ }
351+
352+ @Override
353 public void accept(ITCTLVisitor visitor, Object context) {
354 visitor.visit(this, context);
355 }
356
357=== modified file 'src/dk/aau/cs/TCTL/TCTLPathToStateConverter.java'
358--- src/dk/aau/cs/TCTL/TCTLPathToStateConverter.java 2020-08-17 08:09:43 +0000
359+++ src/dk/aau/cs/TCTL/TCTLPathToStateConverter.java 2020-12-17 21:03:24 +0000
360@@ -37,7 +37,12 @@
361 return children;
362 }
363
364- @Override
365+ @Override
366+ public void convertForReducedNet(String templateName) {
367+ property.convertForReducedNet(templateName);
368+ }
369+
370+ @Override
371 public boolean equals(Object o) {
372 if (o instanceof TCTLEFNode) {
373 TCTLEFNode node = (TCTLEFNode) o;
374
375=== modified file 'src/dk/aau/cs/TCTL/TCTLPlaceNode.java'
376--- src/dk/aau/cs/TCTL/TCTLPlaceNode.java 2020-08-17 08:09:43 +0000
377+++ src/dk/aau/cs/TCTL/TCTLPlaceNode.java 2020-12-17 21:03:24 +0000
378@@ -29,7 +29,17 @@
379 }
380 }
381
382- @Override
383+ @Override
384+ public void convertForReducedNet(String templateName) {
385+ if(template.isEmpty()){
386+ place = "Shared_" + place;
387+ } else {
388+ place = template + "_" + place;
389+ }
390+ template = templateName;
391+ }
392+
393+ @Override
394 public TCTLAbstractStateProperty copy() {
395 return new TCTLPlaceNode(template, place);
396 }
397
398=== modified file 'src/dk/aau/cs/TCTL/TCTLPlusListNode.java'
399--- src/dk/aau/cs/TCTL/TCTLPlusListNode.java 2020-08-17 08:09:43 +0000
400+++ src/dk/aau/cs/TCTL/TCTLPlusListNode.java 2020-12-17 21:03:24 +0000
401@@ -36,7 +36,14 @@
402 }
403 }
404
405- @Override
406+ @Override
407+ public void convertForReducedNet(String templateName) {
408+ for(TCTLAbstractProperty property : terms) {
409+ property.convertForReducedNet(templateName);
410+ }
411+ }
412+
413+ @Override
414 public TCTLAbstractStateProperty copy() {
415 ArrayList<TCTLAbstractStateProperty> copy = new ArrayList<TCTLAbstractStateProperty>();
416
417
418=== modified file 'src/dk/aau/cs/TCTL/TCTLStatePlaceHolder.java'
419--- src/dk/aau/cs/TCTL/TCTLStatePlaceHolder.java 2020-08-17 08:09:43 +0000
420+++ src/dk/aau/cs/TCTL/TCTLStatePlaceHolder.java 2020-12-17 21:03:24 +0000
421@@ -51,7 +51,11 @@
422 }
423 }
424
425- @Override
426+ @Override
427+ public void convertForReducedNet(String templateName) {
428+ }
429+
430+ @Override
431 public void accept(ITCTLVisitor visitor, Object context) {
432 visitor.visit(this, context);
433
434
435=== modified file 'src/dk/aau/cs/TCTL/TCTLStateToPathConverter.java'
436--- src/dk/aau/cs/TCTL/TCTLStateToPathConverter.java 2020-08-17 08:09:43 +0000
437+++ src/dk/aau/cs/TCTL/TCTLStateToPathConverter.java 2020-12-17 21:03:24 +0000
438@@ -37,7 +37,12 @@
439 return children;
440 }
441
442- @Override
443+ @Override
444+ public void convertForReducedNet(String templateName) {
445+ property.convertForReducedNet(templateName);
446+ }
447+
448+ @Override
449 public boolean equals(Object o) {
450 if (o instanceof TCTLEFNode) {
451 TCTLEFNode node = (TCTLEFNode) o;
452
453=== modified file 'src/dk/aau/cs/TCTL/TCTLTermListNode.java'
454--- src/dk/aau/cs/TCTL/TCTLTermListNode.java 2020-08-17 08:09:43 +0000
455+++ src/dk/aau/cs/TCTL/TCTLTermListNode.java 2020-12-17 21:03:24 +0000
456@@ -36,7 +36,14 @@
457 }
458 }
459
460- @Override
461+ @Override
462+ public void convertForReducedNet(String templateName) {
463+ for (TCTLAbstractProperty property : factors) {
464+ property.convertForReducedNet(templateName);
465+ }
466+ }
467+
468+ @Override
469 public TCTLAbstractStateProperty copy() {
470 ArrayList<TCTLAbstractStateProperty> copy = new ArrayList<TCTLAbstractStateProperty>();
471
472
473=== modified file 'src/dk/aau/cs/TCTL/TCTLTransitionNode.java'
474--- src/dk/aau/cs/TCTL/TCTLTransitionNode.java 2020-08-17 08:09:43 +0000
475+++ src/dk/aau/cs/TCTL/TCTLTransitionNode.java 2020-12-17 21:03:24 +0000
476@@ -29,7 +29,13 @@
477 }
478 }
479
480- @Override
481+ @Override
482+ public void convertForReducedNet(String templateName) {
483+ transition = template + "_" + transition;
484+ template = templateName;
485+ }
486+
487+ @Override
488 public TCTLAbstractStateProperty copy() {
489 return new TCTLTransitionNode(template, transition);
490 }
491
492=== modified file 'src/dk/aau/cs/TCTL/TCTLTrueNode.java'
493--- src/dk/aau/cs/TCTL/TCTLTrueNode.java 2020-08-17 08:09:43 +0000
494+++ src/dk/aau/cs/TCTL/TCTLTrueNode.java 2020-12-17 21:03:24 +0000
495@@ -18,7 +18,11 @@
496 }
497 }
498
499- @Override
500+ @Override
501+ public void convertForReducedNet(String templateName) {
502+ }
503+
504+ @Override
505 public void accept(ITCTLVisitor visitor, Object context) {
506 visitor.visit(this, context);
507 }
508
509=== modified file 'src/dk/aau/cs/verification/VerificationResult.java'
510--- src/dk/aau/cs/verification/VerificationResult.java 2020-12-16 21:11:57 +0000
511+++ src/dk/aau/cs/verification/VerificationResult.java 2020-12-17 21:03:24 +0000
512@@ -180,6 +180,11 @@
513 }
514 return reductionStats.toString();
515 }
516+
517+ public boolean reductionRulesApplied(){
518+ ReductionStats reductionStats = stats.getReductionStats();
519+ return (reductionStats.getRemovedPlaces() + reductionStats.getRemovedTrantitions()) > 0;
520+ }
521
522 public NetworkMarking getCoveredMarking(TimedArcPetriNetNetwork model){
523
524
525=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java'
526--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java 2020-12-16 21:11:57 +0000
527+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java 2020-12-17 21:03:24 +0000
528@@ -284,7 +284,7 @@
529 if(((VerifyTAPNOptions)options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model);
530
531 VerifyPNExporter exporter = new VerifyPNExporter();
532- ExportedVerifyTAPNModel exportedModel = exporter.export(model.value1(), query, null);
533+ ExportedVerifyTAPNModel exportedModel = exporter.export(model.value1(), query, null, model.value2());
534
535 if (exportedModel == null) {
536 messenger.displayErrorMessage("There was an error exporting the model");
537@@ -314,8 +314,9 @@
538 ((VerifyTAPNOptions)options).setInclusionPlaces(new InclusionPlaces(InclusionPlacesOption.UserSpecified, inclusionPlaces));
539 }
540
541- private VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, ExportedVerifyTAPNModel exportedModel, TAPNQuery query) {
542+ private VerificationResult<TimedArcPetriNetTrace> verify(VerificationOptions options, Tuple<TimedArcPetriNet, NameMapping> model, ExportedVerifyTAPNModel exportedModel, TAPNQuery query) throws IOException {
543 ((VerifyTAPNOptions)options).setTokensInModel(model.value1().marking().size()); // TODO: get rid of me
544+
545 runner = new ProcessRunner(verifypnpath, createArgumentString(exportedModel.modelFile(), exportedModel.queryFile(), options));
546 runner.run();
547
548
549=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java'
550--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java 2020-07-13 13:58:47 +0000
551+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java 2020-12-17 21:03:24 +0000
552@@ -4,6 +4,7 @@
553 import java.util.Map;
554
555 import pipe.dataLayer.TAPNQuery.SearchOption;
556+import pipe.dataLayer.TAPNQuery.QueryReductionTime;
557 import pipe.dataLayer.TAPNQuery.TraceOption;
558 import pipe.dataLayer.TAPNQuery.AlgorithmOption;
559 import pipe.dataLayer.TAPNQuery.QueryCategory;
560@@ -16,26 +17,28 @@
561 private final QueryCategory queryCategory;
562 private final AlgorithmOption algorithmOption;
563 private boolean useSiphontrap = false;
564- private boolean useQueryReduction = true;
565+ private QueryReductionTime queryReductionTime;
566 private boolean useStubbornReduction = true;
567+ private String pathToReducedNet;
568
569- public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, ModelReduction modelReduction,
570- boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, QueryCategory queryCategory, AlgorithmOption algorithmOption,
571- boolean siphontrap, boolean queryReduction, boolean stubbornReduction) {
572+ public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, ModelReduction modelReduction,
573+ boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, QueryCategory queryCategory, AlgorithmOption algorithmOption,
574+ boolean siphontrap, QueryReductionTime queryReduction, boolean stubbornReduction, String pathToReducedNet) {
575 super(extraTokens, traceOption, search, true, useOverApproximation, false, new InclusionPlaces(), enableOverApproximation, enableUnderApproximation, approximationDenominator);
576 this.modelReduction = modelReduction;
577 this.queryCategory = queryCategory;
578 this.algorithmOption = algorithmOption;
579 this.useSiphontrap = siphontrap;
580- this.useQueryReduction = queryReduction;
581+ this.queryReductionTime = queryReduction;
582 this.useStubbornReduction = stubbornReduction;
583+ this.pathToReducedNet = pathToReducedNet;
584 }
585
586- public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, boolean useModelReduction,
587- boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, QueryCategory queryCategory, AlgorithmOption algorithmOption,
588- boolean siphontrap, boolean queryReduction, boolean stubbornReduction) {
589+ public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, boolean useModelReduction,
590+ boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, QueryCategory queryCategory, AlgorithmOption algorithmOption,
591+ boolean siphontrap, QueryReductionTime queryReduction, boolean stubbornReduction) {
592 this(extraTokens, traceOption, search, useOverApproximation, useModelReduction? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION, enableOverApproximation,
593- enableUnderApproximation, approximationDenominator,queryCategory, algorithmOption, siphontrap, queryReduction, stubbornReduction);
594+ enableUnderApproximation, approximationDenominator,queryCategory, algorithmOption, siphontrap, queryReduction, stubbornReduction, null);
595 }
596
597 @Override
598@@ -49,12 +52,16 @@
599 switch(getModelReduction()){
600 case AGGRESSIVE:
601 result.append(" -r 1 ");
602+ String writeReducedCMD = " --write-reduced " +pathToReducedNet;
603+ result.append(writeReducedCMD);
604 break;
605 case NO_REDUCTION:
606 result.append(" -r 0 ");
607 break;
608 case BOUNDPRESERVING:
609 result.append(" -r 2 ");
610+ writeReducedCMD = " --write-reduced " +pathToReducedNet;
611+ result.append(writeReducedCMD);
612 break;
613 default:
614 break;
615@@ -67,9 +74,12 @@
616 if (this.useSiphontrap) {
617 result.append(" -a 10 ");
618 }
619- if (!this.useQueryReduction) {
620+ if (this.queryReductionTime == QueryReductionTime.NoTime) {
621 result.append(" -q 0 ");
622- }
623+ } else if (this.queryReductionTime == QueryReductionTime.ShortestTime) {
624+ //Run query reduction for 1 second, to avoid conflict with -s OverApprox argument, but also still not run the verification.
625+ result.append(" -q 1");
626+ }
627 if (!this.useStubbornReduction) {
628 result.append(" -p ");
629 }
630
631=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java'
632--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java 2020-12-16 21:11:57 +0000
633+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java 2020-12-17 21:03:24 +0000
634@@ -272,7 +272,7 @@
635 if(((VerifyTAPNOptions)options).discreteInclusion()) mapDiscreteInclusionPlacesToNewNames(options, model);
636
637 VerifyTAPNExporter exporter = new VerifyTAPNExporter();
638- ExportedVerifyTAPNModel exportedModel = exporter.export(model.value1(), query, null);
639+ ExportedVerifyTAPNModel exportedModel = exporter.export(model.value1(), query, null, model.value2());
640
641 if (exportedModel == null) {
642 messenger.displayErrorMessage("There was an error exporting the model");
643
644=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java'
645--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java 2020-12-16 21:11:57 +0000
646+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java 2020-12-17 21:03:24 +0000
647@@ -278,7 +278,7 @@
648 }
649
650 VerifyTAPNExporter exporter = new VerifyTAPNExporter();
651- ExportedVerifyTAPNModel exportedModel = exporter.export(model.value1(), query, CreateGui.getCurrentTab().getLens());
652+ ExportedVerifyTAPNModel exportedModel = exporter.export(model.value1(), query, CreateGui.getCurrentTab().getLens(), model.value2());
653
654 if (exportedModel == null) {
655 messenger.displayErrorMessage("There was an error exporting the model");
656
657=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java'
658--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java 2020-12-14 17:13:30 +0000
659+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java 2020-12-17 21:03:24 +0000
660@@ -4,8 +4,12 @@
661 import java.io.FileNotFoundException;
662 import java.io.IOException;
663 import java.io.PrintStream;
664+import java.util.Collection;
665+import java.util.List;
666
667 import dk.aau.cs.gui.TabContent;
668+import dk.aau.cs.verification.NameMapping;
669+import pipe.dataLayer.DataLayer;
670 import pipe.dataLayer.TAPNQuery.QueryCategory;
671
672 import dk.aau.cs.model.tapn.TAPNQuery;
673@@ -18,9 +22,14 @@
674 import dk.aau.cs.model.tapn.TransportArc;
675
676 import dk.aau.cs.TCTL.visitors.CTLQueryVisitor;
677+import pipe.gui.CreateGui;
678+import pipe.gui.graphicElements.Place;
679+import pipe.gui.graphicElements.Transition;
680+
681+import javax.xml.crypto.Data;
682
683 public class VerifyTAPNExporter {
684- public ExportedVerifyTAPNModel export(TimedArcPetriNet model, TAPNQuery query, TabContent.TAPNLens lens) {
685+ public ExportedVerifyTAPNModel export(TimedArcPetriNet model, TAPNQuery query, TabContent.TAPNLens lens, NameMapping mapping) {
686 File modelFile = createTempFile(".xml");
687 File queryFile;
688 if (query.getCategory() == QueryCategory.CTL){
689@@ -28,19 +37,20 @@
690 } else {
691 queryFile = createTempFile(".q");
692 }
693-
694-
695- return export(model, query, modelFile, queryFile, lens);
696+
697+ return export(model, query, modelFile, queryFile, null, lens, mapping);
698+
699 }
700
701- public ExportedVerifyTAPNModel export(TimedArcPetriNet model, TAPNQuery query, File modelFile, File queryFile, TabContent.TAPNLens lens) {
702+
703+ public ExportedVerifyTAPNModel export(TimedArcPetriNet model, TAPNQuery query, File modelFile, File queryFile, pipe.dataLayer.TAPNQuery dataLayerQuery, TabContent.TAPNLens lens, NameMapping mapping) {
704 if (modelFile == null || queryFile == null)
705 return null;
706
707 try{
708 PrintStream modelStream = new PrintStream(modelFile);
709
710- outputModel(model, modelStream);
711+ outputModel(model, modelStream, mapping);
712 modelStream.close();
713
714 PrintStream queryStream = new PrintStream(queryFile);
715@@ -62,15 +72,17 @@
716 return new ExportedVerifyTAPNModel(modelFile.getAbsolutePath(), queryFile.getAbsolutePath());
717 }
718
719- private void outputModel(TimedArcPetriNet model, PrintStream modelStream) {
720+ private void outputModel(TimedArcPetriNet model, PrintStream modelStream, NameMapping mapping) {
721+ Collection<DataLayer> guiModels = CreateGui.getCurrentTab().getGuiModels().values();
722+
723 modelStream.append("<pnml>\n");
724 modelStream.append("<net id=\"" + model.name() + "\" type=\"P/T net\">\n");
725
726 for(TimedPlace p : model.places())
727- outputPlace(p, modelStream);
728+ outputPlace(p, modelStream, guiModels, mapping);
729
730 for(TimedTransition t : model.transitions())
731- outputTransition(t,modelStream);
732+ outputTransition(t,modelStream, guiModels, mapping);
733
734 for(TimedInputArc inputArc : model.inputArcs())
735 outputInputArc(inputArc, modelStream);
736@@ -88,28 +100,63 @@
737 modelStream.append("</pnml>");
738 }
739
740- private void outputPlace(TimedPlace p, PrintStream modelStream) {
741+ private void outputPlace(TimedPlace p, PrintStream modelStream, Collection<DataLayer> guiModels, NameMapping mapping) {
742+ //remove the net prefix from the place name
743+ String placeName = mapping.map(p.name()).value2();
744+ Place guiPlace = null;
745+
746+ for(DataLayer guiModel : guiModels ){
747+ guiPlace = guiModel.getPlaceById(placeName);
748+ if(guiPlace != null){
749+ break;
750+ }
751+ }
752+
753 modelStream.append("<place ");
754
755 modelStream.append("id=\"" + p.name() + "\" ");
756 modelStream.append("name=\"" + p.name() + "\" ");
757 modelStream.append("invariant=\"" + p.invariant().toString(false).replace("<", "&lt;") + "\" ");
758 modelStream.append("initialMarking=\"" + p.numberOfTokens() + "\" ");
759-
760- modelStream.append("/>\n");
761+ modelStream.append(">\n");
762+ outputPosition(modelStream, guiPlace.getPositionX(), guiPlace.getPositionY());
763+
764+ modelStream.append("</place>\n");
765 }
766
767- private void outputTransition(TimedTransition t, PrintStream modelStream) {
768+ private void outputTransition(TimedTransition t, PrintStream modelStream, Collection<DataLayer> guiModels, NameMapping mapping) {
769+ //remove the net prefix from the transition name
770+ String transitionName = mapping.map(t.name()).value2();
771+ Transition guiTransition = null;
772+
773+ for(DataLayer guiModel : guiModels){
774+ guiTransition = guiModel.getTransitionById(transitionName);
775+ if(guiTransition != null){
776+ break;
777+ }
778+ }
779+
780 modelStream.append("<transition ");
781
782 modelStream.append("player=\"" + (t.isUncontrollable() ? "1" : "0") + "\" ");
783 modelStream.append("id=\"" + t.name() + "\" ");
784 modelStream.append("name=\"" + t.name() + "\" ");
785- modelStream.append("urgent=\"" + (t.isUrgent()? "true":"false") + "\"");
786-
787- modelStream.append("/>\n");
788+ modelStream.append("urgent=\"" + (t.isUrgent()? "true":"false") + "\"");
789+ modelStream.append(">\n");
790+ outputPosition(modelStream, guiTransition.getPositionX(), guiTransition.getPositionY());
791+
792+ modelStream.append("</transition>\n");
793 }
794
795+ private void outputPosition(PrintStream modelStream, int positionX, int positionY) {
796+ modelStream.append("<graphics>");
797+ modelStream.append("<position ");
798+ modelStream.append("x=\"" + positionX + "\" ");
799+ modelStream.append("y=\"" + positionY + "\" ");
800+ modelStream.append("/>");
801+ modelStream.append("</graphics>");
802+ }
803+
804 protected void outputInputArc(TimedInputArc inputArc, PrintStream modelStream) {
805 modelStream.append("<inputArc ");
806
807
808=== modified file 'src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java'
809--- src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java 2020-07-13 13:58:47 +0000
810+++ src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java 2020-12-17 21:03:24 +0000
811@@ -8,6 +8,7 @@
812 import pipe.dataLayer.TAPNQuery.SearchOption;
813 import pipe.dataLayer.TAPNQuery.TraceOption;
814 import pipe.dataLayer.TAPNQuery.WorkflowMode;
815+import pipe.dataLayer.TAPNQuery.QueryReductionTime;
816 import pipe.gui.CreateGui;
817 import pipe.gui.FileFinder;
818 import pipe.gui.MessengerImpl;
819@@ -307,7 +308,7 @@
820 }
821 long c = m*B+1;
822 queryToVerify.setStrongSoundnessBound(c);
823- Verifier.runVerifyTAPNVerification(model.network(), queryToVerify, new VerificationCallback() {
824+ Verifier.runVerifyTAPNVerification(model.network(), queryToVerify, false, new VerificationCallback() {
825
826 @Override
827 public void run(VerificationResult<TAPNNetworkTrace> result) {
828@@ -575,7 +576,7 @@
829 TAPNQuery queryToVerify = getTAPNQuery(composedModel.value1(),query);
830 queryToVerify.setCategory(query.getCategory());
831 MapQueryToNewNames(queryToVerify, composedModel.value2());
832-
833+
834 TAPNQuery clonedQuery = new TAPNQuery(query.getProperty().copy(), queryToVerify.getExtraTokens());
835 clonedQuery.setCategory(query.getCategory());
836 MapQueryToNewNames(clonedQuery, composedModel.value2());
837@@ -622,9 +623,9 @@
838 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());
839 else if(query.getReductionOption() == ReductionOption.VerifyPN || query.getReductionOption() == ReductionOption.VerifyPNApprox || query.getReductionOption() == ReductionOption.VerifyPNReduce)
840 if (batchProcessingVerificationOptions.queryPropertyOption() == QueryPropertyOption.SearchWholeStateSpace){
841- return new VerifyPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), false, false, false, false, query.approximationDenominator(), QueryCategory.Default, query.getAlgorithmOption(), false, false, false);
842+ return new VerifyPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), false, false, false, false, query.approximationDenominator(), QueryCategory.Default, query.getAlgorithmOption(), false, QueryReductionTime.UnlimitedTime, false);
843 } else {
844- 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());
845+ 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());
846 }
847 else
848 return new VerifytaOptions(TraceOption.NONE, query.getSearchOption(), false, query.getReductionOption(), query.useSymmetry(), false, query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator());
849
850=== modified file 'src/net/tapaal/TAPAAL.java'
851--- src/net/tapaal/TAPAAL.java 2020-05-21 08:51:39 +0000
852+++ src/net/tapaal/TAPAAL.java 2020-12-17 21:03:24 +0000
853@@ -148,7 +148,7 @@
854 System.out.println(" | Running query: " + query.getName());
855
856 if(query.getReductionOption() == ReductionOption.VerifyTAPN || query.getReductionOption() == ReductionOption.VerifyTAPNdiscreteVerification || query.getReductionOption() == ReductionOption.VerifyPN) {
857- Verifier.runVerifyTAPNVerification(network, query, new VerificationCallback() {
858+ Verifier.runVerifyTAPNVerification(network, query, false, new VerificationCallback() {
859 @Override
860 public void run(VerificationResult<TAPNNetworkTrace> result) {
861
862
863=== modified file 'src/pipe/dataLayer/TAPNQuery.java'
864--- src/pipe/dataLayer/TAPNQuery.java 2020-08-20 07:26:04 +0000
865+++ src/pipe/dataLayer/TAPNQuery.java 2020-12-17 21:03:24 +0000
866@@ -16,6 +16,10 @@
867 BFS, DFS, RANDOM, BatchProcessingKeepQueryOption, HEURISTIC, OVERAPPROXIMATE, DEFAULT
868 }
869
870+ public enum QueryReductionTime {
871+ NoTime, ShortestTime, UnlimitedTime
872+ }
873+
874 public enum HashTableSize {
875 MB_4, MB_16, MB_64, MB_256, MB_512
876 }
877@@ -430,4 +434,10 @@
878 }
879 return false;
880 }
881+
882+ public TAPNQuery convertPropertyForReducedNet(String templateName){
883+ TAPNQuery convertedQuery = copy();
884+ convertedQuery.property.convertForReducedNet(templateName);
885+ return convertedQuery;
886+ }
887 }
888
889=== modified file 'src/pipe/gui/Export.java'
890--- src/pipe/gui/Export.java 2020-12-14 17:13:30 +0000
891+++ src/pipe/gui/Export.java 2020-12-17 21:03:24 +0000
892@@ -147,9 +147,9 @@
893 i++;
894
895 if (lens.isGame() && isDTAPN) {
896- exporter.export(model, new dk.aau.cs.model.tapn.TAPNQuery(query.getProperty(), 0), new File(modelFile), new File(queryFile + i + ".q"), lens);
897+ 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());
898 } else {
899- 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));
900+ 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());
901 }
902 }
903 }
904
905=== modified file 'src/pipe/gui/KBoundAnalyzer.java'
906--- src/pipe/gui/KBoundAnalyzer.java 2020-07-13 13:58:47 +0000
907+++ src/pipe/gui/KBoundAnalyzer.java 2020-12-17 21:03:24 +0000
908@@ -52,7 +52,7 @@
909
910 protected VerifyTAPNOptions verificationOptions() {
911 if(modelChecker instanceof VerifyPN){
912- return new VerifyPNOptions(k, TraceOption.NONE, SearchOption.BFS, false, ModelReduction.BOUNDPRESERVING, false, false, 1, QueryCategory.Default, AlgorithmOption.CERTAIN_ZERO, false, false, false);
913+ 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);
914 } else if(modelChecker instanceof VerifyTAPN){
915 return new VerifyTAPNOptions(k, TraceOption.NONE, SearchOption.BFS, true, false, true, false, false, 1);
916 } else if(modelChecker instanceof VerifyTAPNDiscreteVerification){
917
918=== modified file 'src/pipe/gui/RunVerification.java'
919--- src/pipe/gui/RunVerification.java 2020-12-16 21:11:57 +0000
920+++ src/pipe/gui/RunVerification.java 2020-12-17 21:03:24 +0000
921@@ -6,8 +6,11 @@
922 import java.awt.GridBagLayout;
923 import java.awt.Insets;
924 import java.awt.Window;
925+import java.awt.event.ActionEvent;
926+import java.awt.event.ActionListener;
927 import java.awt.event.HierarchyEvent;
928 import java.awt.event.HierarchyListener;
929+import java.io.File;
930 import java.util.Comparator;
931 import java.util.List;
932
933@@ -15,29 +18,30 @@
934 import javax.swing.table.DefaultTableModel;
935 import javax.swing.table.TableModel;
936 import javax.swing.table.TableRowSorter;
937-
938+import dk.aau.cs.gui.TabContent;
939+import dk.aau.cs.verification.*;
940 import dk.aau.cs.Messenger;
941 import dk.aau.cs.model.tapn.simulation.TAPNNetworkTrace;
942 import dk.aau.cs.util.MemoryMonitor;
943 import dk.aau.cs.util.Tuple;
944 import dk.aau.cs.util.VerificationCallback;
945-import dk.aau.cs.verification.IconSelector;
946-import dk.aau.cs.verification.ModelChecker;
947-import dk.aau.cs.verification.QueryResult;
948-import dk.aau.cs.verification.QueryType;
949-import dk.aau.cs.verification.VerificationResult;
950+import pipe.dataLayer.TAPNQuery;
951
952 public class RunVerification extends RunVerificationBase {
953 private final IconSelector iconSelector;
954 private final VerificationCallback callback;
955- public RunVerification(ModelChecker modelChecker, IconSelector selector, Messenger messenger, VerificationCallback callback) {
956- super(modelChecker, messenger);
957+ public RunVerification(ModelChecker modelChecker, IconSelector selector, Messenger messenger, VerificationCallback callback, String reducedNetFilePath, boolean reduceNetOnly) {
958+ super(modelChecker, messenger, reducedNetFilePath, reduceNetOnly);
959 iconSelector = selector;
960 this.callback = callback;
961 }
962+
963+ public RunVerification(ModelChecker modelChecker, IconSelector selector, Messenger messenger, VerificationCallback callback) {
964+ this(modelChecker, selector, messenger, callback, null, false);
965+ }
966
967 public RunVerification(ModelChecker modelChecker, IconSelector selector, Messenger messenger) {
968- this(modelChecker, selector, messenger, null);
969+ this(modelChecker, selector, messenger, null, null, false);
970 }
971
972 @Override
973@@ -54,12 +58,14 @@
974 iconSelector.getIconFor(result)
975 );
976
977- if (result.getTrace() != null) {
978+ if (!reducedNetOpened && result.getTrace() != null) {
979 CreateGui.getAnimator().setTrace(result.getTrace());
980 }
981 }
982
983- }else{
984+ } else if(reduceNetOnly) {
985+ //If the engine is only called to produce a reduced net, it will fail, but no error message should be shown
986+ }else{
987
988 //Check if the is something like
989 //verifyta: relocation_error:
990@@ -116,7 +122,6 @@
991
992 }
993
994-
995 private JPanel createStatisticsPanel(final VerificationResult<TAPNNetworkTrace> result, boolean transitionPanel) {
996 JPanel headLinePanel = new JPanel(new GridBagLayout());
997 final JPanel fullPanel = new JPanel(new GridBagLayout());
998@@ -311,13 +316,46 @@
999 }
1000
1001 if(!result.getReductionResultAsString().isEmpty()){
1002- JLabel reductionStatsLabet = new JLabel(toHTML(result.getReductionResultAsString()));
1003+ JLabel reductionStatsLabel = new JLabel(toHTML(result.getReductionResultAsString()));
1004 gbc = new GridBagConstraints();
1005 gbc.gridx = 0;
1006 gbc.gridy = 6;
1007 gbc.insets = new Insets(0,0,20,-90);
1008 gbc.anchor = GridBagConstraints.WEST;
1009- panel.add(reductionStatsLabet, gbc);
1010+
1011+ panel.add(reductionStatsLabel, gbc);
1012+
1013+ if(result.reductionRulesApplied()){
1014+ JButton openReducedButton = new JButton("Open reduced net");
1015+ openReducedButton.addActionListener(new ActionListener() {
1016+ public void actionPerformed(ActionEvent e) {
1017+ openReducedButton.setEnabled(false);
1018+ reducedNetOpened = true;
1019+ File reducedNetFile = new File(reducedNetFilePath);
1020+
1021+ if(reducedNetFile.exists() && reducedNetFile.isFile() && reducedNetFile.canRead()){
1022+ try {
1023+ TabContent reducedNetTab = TabContent.createNewTabFromPNMLFile(reducedNetFile);
1024+ reducedNetTab.setInitialName("reduced-" + CreateGui.getAppGui().getCurrentTabName());
1025+ TAPNQuery convertedQuery = dataLayerQuery.convertPropertyForReducedNet(reducedNetTab.currentTemplate().toString());
1026+ reducedNetTab.addQuery(convertedQuery);
1027+ CreateGui.openNewTabFromStream(reducedNetTab);
1028+ } catch (Exception e1){
1029+ JOptionPane.showMessageDialog(CreateGui.getApp(),
1030+ e1.getMessage(),
1031+ "Error loading reduced net file",
1032+ JOptionPane.ERROR_MESSAGE);
1033+ }
1034+ }
1035+ }
1036+ });
1037+ gbc = new GridBagConstraints();
1038+ gbc.gridx = 0;
1039+ gbc.gridy = 5;
1040+ gbc.insets = new Insets(0,0,10,0);
1041+ gbc.anchor = GridBagConstraints.WEST;
1042+ panel.add(openReducedButton, gbc);
1043+ }
1044 }
1045 if (result.getRawOutput() != null) {
1046 JButton showRawQueryButton = new JButton("Show raw query results");
1047@@ -325,9 +363,9 @@
1048 JOptionPane.showMessageDialog(panel, createRawQueryPanel(result.getRawOutput()), "Raw query results", JOptionPane.INFORMATION_MESSAGE);
1049 });
1050 gbc = new GridBagConstraints();
1051- gbc.gridx = 0;
1052+ gbc.gridx = 1;
1053 gbc.gridy = 5;
1054- gbc.insets = new Insets(10,0,10,0);
1055+ gbc.insets = new Insets(0,0,10,0);
1056 gbc.anchor = GridBagConstraints.WEST;
1057 panel.add(showRawQueryButton, gbc);
1058 }
1059
1060=== modified file 'src/pipe/gui/RunVerificationBase.java'
1061--- src/pipe/gui/RunVerificationBase.java 2020-08-27 07:27:30 +0000
1062+++ src/pipe/gui/RunVerificationBase.java 2020-12-17 21:03:24 +0000
1063@@ -1,5 +1,6 @@
1064 package pipe.gui;
1065
1066+import java.io.File;
1067 import java.util.concurrent.ExecutionException;
1068
1069 import javax.swing.SwingUtilities;
1070@@ -39,16 +40,25 @@
1071 protected TimedArcPetriNetNetwork model;
1072 protected TAPNQuery query;
1073 protected pipe.dataLayer.TAPNQuery dataLayerQuery;
1074+ protected String reducedNetFilePath;
1075+ protected boolean reduceNetOnly;
1076+ protected boolean reducedNetOpened = false;
1077
1078
1079 protected Messenger messenger;
1080
1081- public RunVerificationBase(ModelChecker modelChecker, Messenger messenger) {
1082+ public RunVerificationBase(ModelChecker modelChecker, Messenger messenger, String reducedNetFilePath, boolean reduceNetOnly) {
1083 super();
1084 this.modelChecker = modelChecker;
1085 this.messenger = messenger;
1086+ this.reducedNetFilePath = reducedNetFilePath;
1087+ this.reduceNetOnly = reduceNetOnly;
1088 }
1089
1090+ public RunVerificationBase(ModelChecker modelChecker, Messenger messenger) {
1091+ this(modelChecker, messenger, null, false);
1092+ }
1093+
1094
1095 public void execute(VerificationOptions options, TimedArcPetriNetNetwork model, TAPNQuery query, pipe.dataLayer.TAPNQuery dataLayerQuery) {
1096 this.model = model;
1097@@ -110,8 +120,9 @@
1098 dataLayerQuery.getCategory(),
1099 dataLayerQuery.getAlgorithmOption(),
1100 dataLayerQuery.isSiphontrapEnabled(),
1101- dataLayerQuery.isQueryReductionEnabled(),
1102- dataLayerQuery.isStubbornReductionEnabled()
1103+ dataLayerQuery.isQueryReductionEnabled()? pipe.dataLayer.TAPNQuery.QueryReductionTime.UnlimitedTime: pipe.dataLayer.TAPNQuery.QueryReductionTime.NoTime,
1104+ dataLayerQuery.isStubbornReductionEnabled(),
1105+ reducedNetFilePath
1106 ),
1107 transformedModel,
1108 clonedQuery
1109@@ -130,8 +141,9 @@
1110 pipe.dataLayer.TAPNQuery.QueryCategory.Default,
1111 pipe.dataLayer.TAPNQuery.AlgorithmOption.CERTAIN_ZERO,
1112 false,
1113- true,
1114- false
1115+ pipe.dataLayer.TAPNQuery.QueryReductionTime.UnlimitedTime,
1116+ false,
1117+ reducedNetFilePath
1118 ),
1119 transformedModel,
1120 clonedQuery
1121
1122=== modified file 'src/pipe/gui/Verifier.java'
1123--- src/pipe/gui/Verifier.java 2020-07-06 11:57:37 +0000
1124+++ src/pipe/gui/Verifier.java 2020-12-17 21:03:24 +0000
1125@@ -15,6 +15,9 @@
1126 import dk.aau.cs.verification.UPPAAL.Verifyta;
1127 import dk.aau.cs.verification.UPPAAL.VerifytaOptions;
1128
1129+import java.io.File;
1130+import java.io.IOException;
1131+
1132 /**
1133 * Implementes af class for handling integrated Uppaal Verification
1134 *
1135@@ -24,6 +27,8 @@
1136 */
1137
1138 public class Verifier {
1139+ private static File reducedNetTempFile = null;
1140+
1141 private static Verifyta getVerifyta() {
1142 Verifyta verifyta = new Verifyta(new FileFinder(), new MessengerImpl());
1143 verifyta.setup();
1144@@ -61,6 +66,10 @@
1145 }
1146 }
1147
1148+ public static String getReducedNetFilePath() {
1149+ return reducedNetTempFile.getAbsolutePath();
1150+ }
1151+
1152 public static void analyzeKBound(TimedArcPetriNetNetwork tapnNetwork, int k, JSpinner tokensControl) {
1153 ModelChecker modelChecker;
1154
1155@@ -129,10 +138,12 @@
1156 public static void runVerifyTAPNVerification(
1157 TimedArcPetriNetNetwork tapnNetwork,
1158 TAPNQuery query,
1159+ boolean onlyCreateReducedNet,
1160 VerificationCallback callback
1161 ) {
1162 ModelChecker verifytapn = getModelChecker(query);
1163
1164+
1165 if (!verifytapn.isCorrectVersion()) {
1166 new MessengerImpl().displayErrorMessage(
1167 "No "+verifytapn+" specified: The verification is cancelled",
1168@@ -165,21 +176,53 @@
1169 query.isStubbornReductionEnabled()
1170 );
1171 } else if(query.getReductionOption() == ReductionOption.VerifyPN){
1172- verifytapnOptions = new VerifyPNOptions(
1173- bound,
1174- query.getTraceOption(),
1175- query.getSearchOption(),
1176- query.useOverApproximation(),
1177- query.useReduction()? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION,
1178- query.isOverApproximationEnabled(),
1179- query.isUnderApproximationEnabled(),
1180- query.approximationDenominator(),
1181- query.getCategory(),
1182- query.getAlgorithmOption(),
1183- query.isSiphontrapEnabled(),
1184- query.isQueryReductionEnabled(),
1185- query.isStubbornReductionEnabled()
1186- );
1187+
1188+ try {
1189+ reducedNetTempFile = File.createTempFile("reduced-", ".pnml");
1190+ } catch (IOException e) {
1191+ new MessengerImpl().displayErrorMessage(
1192+ e.getMessage(),
1193+ "Error");
1194+ return;
1195+ }
1196+
1197+ if (onlyCreateReducedNet) {
1198+ //These options should disable the verification and only produce the net after applying reduction rules
1199+ verifytapnOptions = new VerifyPNOptions(
1200+ bound,
1201+ query.getTraceOption(),
1202+ TAPNQuery.SearchOption.OVERAPPROXIMATE,
1203+ query.useOverApproximation(),
1204+ query.useReduction()? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION,
1205+ query.isOverApproximationEnabled(),
1206+ query.isUnderApproximationEnabled(),
1207+ query.approximationDenominator(),
1208+ query.getCategory(),
1209+ query.getAlgorithmOption(),
1210+ query.isSiphontrapEnabled(),
1211+ TAPNQuery.QueryReductionTime.NoTime,
1212+ query.isStubbornReductionEnabled(),
1213+ reducedNetTempFile.getAbsolutePath()
1214+ );
1215+ } else {
1216+ verifytapnOptions = new VerifyPNOptions(
1217+ bound,
1218+ query.getTraceOption(),
1219+ query.getSearchOption(),
1220+ query.useOverApproximation(),
1221+ query.useReduction()? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION,
1222+ query.isOverApproximationEnabled(),
1223+ query.isUnderApproximationEnabled(),
1224+ query.approximationDenominator(),
1225+ query.getCategory(),
1226+ query.getAlgorithmOption(),
1227+ query.isSiphontrapEnabled(),
1228+ query.isQueryReductionEnabled()? TAPNQuery.QueryReductionTime.UnlimitedTime: TAPNQuery.QueryReductionTime.NoTime,
1229+ query.isStubbornReductionEnabled(),
1230+ reducedNetTempFile.getAbsolutePath()
1231+ );
1232+ }
1233+
1234 } else {
1235 verifytapnOptions = new VerifyTAPNOptions(
1236 bound,
1237@@ -200,7 +243,13 @@
1238 }
1239
1240 if (tapnNetwork != null) {
1241- RunVerificationBase thread = new RunVerification(verifytapn, new VerifyTAPNIconSelector(), new MessengerImpl(), callback);
1242+ RunVerificationBase thread;
1243+ if (reducedNetTempFile != null) {
1244+ thread = new RunVerification(verifytapn, new VerifyTAPNIconSelector(), new MessengerImpl(), callback, reducedNetTempFile.getAbsolutePath(), onlyCreateReducedNet );
1245+ } else {
1246+ thread = new RunVerification(verifytapn, new VerifyTAPNIconSelector(), new MessengerImpl(), callback);
1247+ }
1248+
1249 RunningVerificationDialog dialog = new RunningVerificationDialog(CreateGui.getApp(), thread);
1250 thread.execute(verifytapnOptions, tapnNetwork, new dk.aau.cs.model.tapn.TAPNQuery(query.getProperty(), bound), query);
1251 dialog.setVisible(true);
1252
1253=== modified file 'src/pipe/gui/widgets/QueryDialog.java'
1254--- src/pipe/gui/widgets/QueryDialog.java 2020-12-14 17:13:30 +0000
1255+++ src/pipe/gui/widgets/QueryDialog.java 2020-12-17 21:03:24 +0000
1256@@ -17,10 +17,7 @@
1257 import java.util.Vector;
1258
1259 import javax.swing.*;
1260-import javax.swing.event.DocumentEvent;
1261-import javax.swing.event.DocumentListener;
1262-import javax.swing.event.UndoableEditEvent;
1263-import javax.swing.event.UndoableEditListener;
1264+import javax.swing.event.*;
1265 import javax.swing.text.MutableAttributeSet;
1266 import javax.swing.text.SimpleAttributeSet;
1267 import javax.swing.text.StyleConstants;
1268@@ -70,6 +67,7 @@
1269 private static final String EXPORT_VERIFYTAPN_BTN_TEXT = "Export TAPAAL XML";
1270 private static final String EXPORT_VERIFYPN_BTN_TEXT = "Export PN XML";
1271 private static final String EXPORT_COMPOSED_BTN_TEXT = "Merge net components";
1272+ private static final String OPEN_REDUCED_BTN_TEXT = "Open reduced net";
1273
1274 private static final String UPPAAL_SOME_TRACE_STRING = "Some trace ";
1275 private static final String SOME_TRACE_STRING = "Some trace ";
1276@@ -183,6 +181,7 @@
1277 private JButton saveAndVerifyButton;
1278 private JButton saveUppaalXMLButton;
1279 private JButton mergeNetComponentsButton;
1280+ private JButton openReducedNetButton;
1281
1282 // Private Members
1283 private StringPosition currentSelection = null;
1284@@ -313,6 +312,7 @@
1285 private final static String TOOL_TIP_CANCEL_BUTTON = "Cancel the changes made in this dialog.";
1286 private final static String TOOL_TIP_SAVE_UPPAAL_BUTTON = "Export an xml file that can be opened in UPPAAL GUI.";
1287 private final static String TOOL_TIP_SAVE_COMPOSED_BUTTON = "Export an xml file of composed net and approximated net if enabled";
1288+ private final static String TOOL_TIP_OPEN_REDUCED_BUTTON = "Open the net produced after applying structural reduction rules";
1289 private final static String TOOL_TIP_SAVE_TAPAAL_BUTTON = "Export an xml file that can be used as input for the TAPAAL engine.";
1290 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.";
1291
1292@@ -676,7 +676,7 @@
1293 current = ((TCTLStateToPathConverter) current).getProperty();
1294 }
1295 if (current instanceof TCTLAtomicPropositionNode) {
1296- TCTLAtomicPropositionNode node = (TCTLAtomicPropositionNode) currentSelection.getObject();
1297+ TCTLAtomicPropositionNode node = (TCTLAtomicPropositionNode) current;
1298
1299 // bit of a hack to prevent posting edits to the undo manager when
1300 // we programmatically change the selection in the atomic proposition comboboxes etc.
1301@@ -811,11 +811,13 @@
1302 saveAndVerifyButton.setEnabled(isQueryOk);
1303 saveUppaalXMLButton.setEnabled(isQueryOk);
1304 mergeNetComponentsButton.setEnabled(isQueryOk);
1305+ openReducedNetButton.setEnabled(isQueryOk && useReduction.isSelected());
1306 } else {
1307 saveButton.setEnabled(false);
1308 saveAndVerifyButton.setEnabled(false);
1309 saveUppaalXMLButton.setEnabled(false);
1310 mergeNetComponentsButton.setEnabled(false);
1311+ openReducedNetButton.setEnabled(false);
1312 }
1313 }
1314
1315@@ -1454,9 +1456,12 @@
1316 if (lens.isTimed() || lens.isGame()) {
1317 saveUppaalXMLButton.setVisible(advancedView);
1318 overApproximationOptionsPanel.setVisible(advancedView);
1319+ } else if (!lens.isGame()){
1320+ openReducedNetButton.setVisible(advancedView);
1321 }
1322 mergeNetComponentsButton.setVisible(advancedView);
1323
1324+
1325 if(advancedView){
1326 advancedButton.setText("Simple view");
1327 advancedButton.setToolTipText(TOOL_TIP_SIMPLE_VIEW_BUTTON);
1328@@ -2679,6 +2684,13 @@
1329 if (lens.isTimed() || lens.isGame()) {
1330 initTimedReductionOptions();
1331 } else {
1332+ useReduction.addActionListener(new ActionListener() {
1333+ @Override
1334+ public void actionPerformed(ActionEvent actionEvent) {
1335+ openReducedNetButton.setEnabled(useReduction.isSelected() && getQueryComment().length() > 0
1336+ && !newProperty.containsPlaceHolder());
1337+ }
1338+ });
1339 initUntimedReductionOptions();
1340 }
1341
1342@@ -2962,6 +2974,10 @@
1343 mergeNetComponentsButton = new JButton(EXPORT_COMPOSED_BTN_TEXT);
1344 mergeNetComponentsButton.setVisible(false);
1345
1346+ openReducedNetButton = new JButton(OPEN_REDUCED_BTN_TEXT);
1347+ openReducedNetButton.setVisible(false);
1348+
1349+
1350 saveUppaalXMLButton = new JButton(EXPORT_UPPAAL_BTN_TEXT);
1351 //Only show in advanced mode
1352 saveUppaalXMLButton.setVisible(false);
1353@@ -2972,6 +2988,7 @@
1354 cancelButton.setToolTipText(TOOL_TIP_CANCEL_BUTTON);
1355 saveUppaalXMLButton.setToolTipText(TOOL_TIP_SAVE_UPPAAL_BUTTON);
1356 mergeNetComponentsButton.setToolTipText(TOOL_TIP_SAVE_COMPOSED_BUTTON);
1357+ openReducedNetButton.setToolTipText(TOOL_TIP_OPEN_REDUCED_BUTTON);
1358
1359 saveButton.addActionListener(new ActionListener() {
1360 public void actionPerformed(ActionEvent evt) {
1361@@ -2995,7 +3012,7 @@
1362 TAPNQuery query = getQuery();
1363
1364 if(query.getReductionOption() == ReductionOption.VerifyTAPN || query.getReductionOption() == ReductionOption.VerifyTAPNdiscreteVerification || query.getReductionOption() == ReductionOption.VerifyPN)
1365- Verifier.runVerifyTAPNVerification(tapnNetwork, query, null);
1366+ Verifier.runVerifyTAPNVerification(tapnNetwork, query, false, null);
1367 else
1368 Verifier.runUppaalVerification(tapnNetwork, query);
1369 }}
1370@@ -3049,10 +3066,12 @@
1371 }
1372 if(reduction == ReductionOption.VerifyTAPN || reduction == ReductionOption.VerifyTAPNdiscreteVerification) {
1373 VerifyTAPNExporter exporter = new VerifyTAPNExporter();
1374- exporter.export(transformedModel.value1(), clonedQuery, new File(xmlFile), new File(queryFile), lens);
1375+ exporter.export(transformedModel.value1(), clonedQuery, new File(xmlFile), new File(queryFile), tapnQuery, lens, transformedModel.value2());
1376+
1377 } else if(reduction == ReductionOption.VerifyPN){
1378 VerifyPNExporter exporter = new VerifyPNExporter();
1379- exporter.export(transformedModel.value1(), clonedQuery, new File(xmlFile), new File(queryFile), lens);
1380+ exporter.export(transformedModel.value1(), clonedQuery, new File(xmlFile), new File(queryFile), tapnQuery, lens, transformedModel.value2());
1381+
1382 } else {
1383 UppaalExporter exporter = new UppaalExporter();
1384 try {
1385@@ -3117,6 +3136,51 @@
1386 }
1387 });
1388
1389+ openReducedNetButton.addActionListener(new ActionListener() {
1390+ public void actionPerformed(ActionEvent e) {
1391+
1392+
1393+ if (checkIfSomeReductionOption()) {
1394+ querySaved = true;
1395+ // Now if a query is saved and verified, the net is marked as modified
1396+ CreateGui.getCurrentTab().setNetChanged(true);
1397+
1398+ TAPNQuery query = getQuery();
1399+ if(query.getReductionOption() != ReductionOption.VerifyPN) {
1400+ JOptionPane.showMessageDialog(CreateGui.getApp(),
1401+ "The selected verification engine does not support application of reduction rules",
1402+ "Reduction rules unsupported", JOptionPane.ERROR_MESSAGE);
1403+ return;
1404+ }
1405+
1406+ exit();
1407+
1408+ Verifier.runVerifyTAPNVerification(tapnNetwork, query,true, null);
1409+
1410+ File reducedNetFile = new File(Verifier.getReducedNetFilePath());
1411+
1412+ if(reducedNetFile.exists() && reducedNetFile.isFile() && reducedNetFile.canRead()){
1413+ try {
1414+ TabContent reducedNetTab = TabContent.createNewTabFromPNMLFile(reducedNetFile);
1415+ //Ensure that a net was created by the query reduction
1416+ if(reducedNetTab.currentTemplate().guiModel().getPlaces().length > 0
1417+ || reducedNetTab.currentTemplate().guiModel().getTransitions().length > 0){
1418+ reducedNetTab.setInitialName("reduced-" + CreateGui.getAppGui().getCurrentTabName());
1419+ TAPNQuery convertedQuery = query.convertPropertyForReducedNet(reducedNetTab.currentTemplate().toString());
1420+ reducedNetTab.addQuery(convertedQuery);
1421+ CreateGui.openNewTabFromStream(reducedNetTab);
1422+ }
1423+ } catch (Exception e1){
1424+ JOptionPane.showMessageDialog(CreateGui.getApp(),
1425+ e1.getMessage(),
1426+ "Error loading reduced net file",
1427+ JOptionPane.ERROR_MESSAGE);
1428+ }
1429+ }
1430+ }
1431+ }
1432+ });
1433+
1434
1435 } else if (option == QueryDialogueOption.Export) {
1436 saveButton = new JButton("export");
1437@@ -3133,6 +3197,7 @@
1438 JPanel leftButtomPanel = new JPanel(new FlowLayout());
1439 JPanel rightButtomPanel = new JPanel(new FlowLayout());
1440 leftButtomPanel.add(mergeNetComponentsButton, FlowLayout.LEFT);
1441+ leftButtomPanel.add(openReducedNetButton, FlowLayout.LEFT);
1442 leftButtomPanel.add(saveUppaalXMLButton, FlowLayout.LEFT);
1443
1444
1445
1446=== modified file 'src/pipe/gui/widgets/QueryPane.java'
1447--- src/pipe/gui/widgets/QueryPane.java 2020-08-20 07:30:52 +0000
1448+++ src/pipe/gui/widgets/QueryPane.java 2020-12-17 21:03:24 +0000
1449@@ -440,7 +440,7 @@
1450
1451 if(NumberOfSelectedElements == 1) {
1452 if(query.getReductionOption() == ReductionOption.VerifyTAPN || query.getReductionOption() == ReductionOption.VerifyTAPNdiscreteVerification || query.getReductionOption() == ReductionOption.VerifyPN)
1453- Verifier.runVerifyTAPNVerification(tabContent.network(), query, null);
1454+ Verifier.runVerifyTAPNVerification(tabContent.network(), query, false, null);
1455 else
1456 Verifier.runUppaalVerification(tabContent.network(), query);
1457 }
1458
1459=== modified file 'src/pipe/gui/widgets/WorkflowDialog.java'
1460--- src/pipe/gui/widgets/WorkflowDialog.java 2020-07-20 07:19:51 +0000
1461+++ src/pipe/gui/widgets/WorkflowDialog.java 2020-12-17 21:03:24 +0000
1462@@ -1010,7 +1010,7 @@
1463 WorkflowMode.WORKFLOW_STRONG_SOUNDNESS,
1464 c
1465 );
1466- Verifier.runVerifyTAPNVerification(model, q, result -> {
1467+ Verifier.runVerifyTAPNVerification(model, q, false, result -> {
1468 if(result.isQuerySatisfied()){
1469
1470 switch(((TimedTAPNNetworkTrace) result.getTrace()).getTraceType()){
1471@@ -1115,7 +1115,7 @@
1472 ExtrapolationOption.AUTOMATIC,
1473 WorkflowMode.WORKFLOW_SOUNDNESS
1474 );
1475- Verifier.runVerifyTAPNVerification(model, q, new VerificationCallback() {
1476+ Verifier.runVerifyTAPNVerification(model, q, false, new VerificationCallback() {
1477
1478 @Override
1479 public void run(VerificationResult<TAPNNetworkTrace> result) {
1480@@ -1225,7 +1225,7 @@
1481 null,
1482 ExtrapolationOption.AUTOMATIC
1483 );
1484- Verifier.runVerifyTAPNVerification(model, q, new VerificationCallback() {
1485+ Verifier.runVerifyTAPNVerification(model, q, false, new VerificationCallback() {
1486
1487 @Override
1488 public void run(VerificationResult<TAPNNetworkTrace> result) {

Subscribers

People subscribed via source and target branches