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