TAPAAL

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

  1. cpn-solvedBy
  2. Merge into cpn-gui-dev
Proposed by Kenneth Yrke Jørgensen
Status: Merged
Approved by: Jiri Srba
Approved revision: 1576
Merged at revision: 1581
Proposed branch: lp:~tapaal-contributor/tapaal/cpn-solvedBy
Merge into: lp:~tapaal-contributor/tapaal/cpn-gui-dev
Diff against target: 375 lines (+33/-55)
9 files modified
src/dk/aau/cs/approximation/ApproximationWorker.java (+22/-22)
src/dk/aau/cs/verification/QueryResult.java (+0/-9)
src/dk/aau/cs/verification/UPPAAL/UppaalIconSelector.java (+1/-1)
src/dk/aau/cs/verification/VerificationResult.java (+0/-4)
src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java (+1/-2)
src/dk/aau/cs/verification/VerifyTAPN/VerifyPNCTLOutputParser.java (+0/-1)
src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOutputParser.java (+0/-1)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOutputParser.java (+1/-5)
src/net/tapaal/gui/petrinet/verification/RunVerification.java (+8/-10)
To merge this branch: bzr merge lp:~tapaal-contributor/tapaal/cpn-solvedBy
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Review via email: mp+415019@code.launchpad.net
To post a comment you must log in.
Revision history for this message
Kenneth Yrke Jørgensen (yrke) wrote :

Made the following changes:

Renamed untimed state equation to preproces using skeleton analysis, and result is displayed independently from general state equation.

Not will report the solution method (if output by engine)
  - query reduction
  - TAR

lp:~tapaal-contributor/tapaal/cpn-solvedBy updated
1575. By Kenneth Yrke Jørgensen

Fixed placement of show raw query btn and fixed detection of solved siphon-trap.

Also removed old solved by state-equation (covered by query simplification)

1576. By Kenneth Yrke Jørgensen

Updated skeleton analysis text

Revision history for this message
Jiri Srba (srba) :
review: Approve
lp:~tapaal-contributor/tapaal/cpn-solvedBy updated
1577. By Kenneth Yrke Jørgensen

Merged cpn branch into solvedBy

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'src/dk/aau/cs/approximation/ApproximationWorker.java'
2--- src/dk/aau/cs/approximation/ApproximationWorker.java 2022-01-28 12:08:30 +0000
3+++ src/dk/aau/cs/approximation/ApproximationWorker.java 2022-02-08 09:07:46 +0000
4@@ -82,7 +82,7 @@
5 decomposeTrace(result.getSecondaryTrace(), nameMapping, netNetwork),
6 result.verificationTime(),
7 result.stats(),
8- result.isSolvedUsingStateEquation(),
9+ false,
10 result.getUnfoldedModel());
11 toReturn.setNameMapping(transformedModel.value2());
12
13@@ -103,7 +103,7 @@
14 decomposeTrace(approxResult.getSecondaryTrace(), nameMapping, netNetwork),
15 approxResult.verificationTime(),
16 approxResult.stats(),
17- approxResult.isSolvedUsingStateEquation(),
18+ false,
19 approxResult.getUnfoldedModel());
20 toReturn.setNameMapping(nameMapping);
21
22@@ -151,7 +151,7 @@
23 decomposeTrace(result.getSecondaryTrace(), nameMapping, netNetwork),
24 approxResult.verificationTime() + result.verificationTime(),
25 approxResult.stats(),
26- approxResult.isSolvedUsingStateEquation(),
27+ false,
28 approxResult.getUnfoldedModel());
29 toReturn.setNameMapping(nameMapping);
30
31@@ -176,7 +176,7 @@
32 decomposeTrace(approxResult.getSecondaryTrace(), nameMapping, netNetwork),
33 approxResult.verificationTime(),
34 approxResult.stats(),
35- approxResult.isSolvedUsingStateEquation(),
36+ false,
37 approxResult.getUnfoldedModel());
38 toReturn.setNameMapping(nameMapping);
39
40@@ -196,7 +196,7 @@
41 decomposeTrace(approxResult.getSecondaryTrace(), nameMapping, netNetwork),
42 approxResult.verificationTime(),
43 approxResult.stats(),
44- approxResult.isSolvedUsingStateEquation(),
45+ false,
46 approxResult.getUnfoldedModel());
47 toReturn.setNameMapping(nameMapping);
48
49@@ -231,7 +231,7 @@
50 decomposeTrace(result.getSecondaryTrace(), nameMapping, netNetwork),
51 result.verificationTime(),
52 result.stats(),
53- result.isSolvedUsingStateEquation(),
54+ false,
55 result.getUnfoldedModel());
56 toReturn.setNameMapping(nameMapping);
57
58@@ -252,7 +252,7 @@
59 decomposeTrace(result.getSecondaryTrace(), nameMapping, netNetwork),
60 result.verificationTime(),
61 result.stats(),
62- result.isSolvedUsingStateEquation(),
63+ false,
64 result.getUnfoldedModel());
65 toReturn.setNameMapping(nameMapping);
66
67@@ -271,7 +271,7 @@
68 decomposeTrace(approxResult.getSecondaryTrace(), nameMapping, netNetwork),
69 approxResult.verificationTime(),
70 approxResult.stats(),
71- result.isSolvedUsingStateEquation(),
72+ false,
73 result.getUnfoldedModel());
74 toReturn.setNameMapping(nameMapping);
75
76@@ -323,7 +323,7 @@
77 decomposeTrace(result.getSecondaryTrace(), nameMapping, netNetwork),
78 approxResult.verificationTime() + result.verificationTime(),
79 approxResult.stats(),
80- approxResult.isSolvedUsingStateEquation(),
81+ false,
82 approxResult.getUnfoldedModel());
83 toReturn.setNameMapping(transformedModel.value2());
84 }
85@@ -342,7 +342,7 @@
86 decomposeTrace(approxResult.getSecondaryTrace(), nameMapping, netNetwork),
87 approxResult.verificationTime(),
88 approxResult.stats(),
89- approxResult.isSolvedUsingStateEquation(),
90+ false,
91 approxResult.getUnfoldedModel());
92 toReturn.setNameMapping(nameMapping);
93 }
94@@ -359,7 +359,7 @@
95 decomposeTrace(result.getSecondaryTrace(), nameMapping, netNetwork),
96 result.verificationTime(),
97 result.stats(),
98- result.isSolvedUsingStateEquation(),
99+ false,
100 result.getRawOutput(),
101 result.getUnfoldedModel());
102 toReturn.setNameMapping(nameMapping);
103@@ -428,7 +428,7 @@
104 verificationResult.getSecondaryTrace(),
105 verificationResult.verificationTime(),
106 verificationResult.stats(),
107- verificationResult.isSolvedUsingStateEquation(),
108+ false,
109 verificationResult.getUnfoldedModel());
110 value.setNameMapping(composedModel.value2());
111 } else {
112@@ -446,7 +446,7 @@
113 decomposeTrace(approxResult.getSecondaryTrace(), nameMapping, netNetwork),
114 approxResult.verificationTime(),
115 approxResult.stats(),
116- verificationResult.isSolvedUsingStateEquation(),
117+ false,
118 verificationResult.getUnfoldedModel());
119 valueNetwork.setNameMapping(nameMapping);
120
121@@ -488,7 +488,7 @@
122 approxResult.getSecondaryTrace(),
123 approxResult.verificationTime() + verificationResult.verificationTime(),
124 approxResult.stats(),
125- verificationResult.isSolvedUsingStateEquation(),
126+ false,
127 verificationResult.getUnfoldedModel());
128 value.setNameMapping(composedModel.value2());
129 }
130@@ -508,7 +508,7 @@
131 verificationResult.getSecondaryTrace(),
132 verificationResult.verificationTime(),
133 verificationResult.stats(),
134- verificationResult.isSolvedUsingStateEquation(),
135+ false,
136 verificationResult.getUnfoldedModel());
137 value.setNameMapping(composedModel.value2());
138 }
139@@ -525,7 +525,7 @@
140 verificationResult.getSecondaryTrace(),
141 verificationResult.verificationTime(),
142 verificationResult.stats(),
143- verificationResult.isSolvedUsingStateEquation(),
144+ false,
145 verificationResult.getUnfoldedModel());
146 value.setNameMapping(composedModel.value2());
147 }
148@@ -544,7 +544,7 @@
149 verificationResult.getSecondaryTrace(),
150 verificationResult.verificationTime(),
151 verificationResult.stats(),
152- verificationResult.isSolvedUsingStateEquation(),
153+ false,
154 verificationResult.getUnfoldedModel());
155 value.setNameMapping(composedModel.value2());
156 }
157@@ -562,7 +562,7 @@
158 verificationResult.getSecondaryTrace(),
159 verificationResult.verificationTime(),
160 verificationResult.stats(),
161- verificationResult.isSolvedUsingStateEquation(),
162+ false,
163 verificationResult.getUnfoldedModel());
164 value.setNameMapping(composedModel.value2());
165
166@@ -584,7 +584,7 @@
167 decomposeTrace(approxResult.getSecondaryTrace(), nameMapping, netNetwork),
168 approxResult.verificationTime(),
169 approxResult.stats(),
170- approxResult.isSolvedUsingStateEquation(),
171+ false,
172 verificationResult.getUnfoldedModel());
173 valueNetwork.setNameMapping(nameMapping);
174
175@@ -631,7 +631,7 @@
176 verificationResult.getSecondaryTrace(),
177 verificationResult.verificationTime() + approxResult.verificationTime(),
178 verificationResult.stats(),
179- verificationResult.isSolvedUsingStateEquation(),
180+ false,
181 verificationResult.getUnfoldedModel());
182 value.setNameMapping(composedModel.value2());
183 }
184@@ -646,7 +646,7 @@
185 verificationResult.getSecondaryTrace(),
186 verificationResult.verificationTime(),
187 verificationResult.stats(),
188- verificationResult.isSolvedUsingStateEquation(),
189+ false,
190 verificationResult.getUnfoldedModel());
191 value.setNameMapping(composedModel.value2());
192 }
193@@ -660,7 +660,7 @@
194 verificationResult.getSecondaryTrace(),
195 verificationResult.verificationTime(),
196 verificationResult.stats(),
197- verificationResult.isSolvedUsingStateEquation(),
198+ false,
199 verificationResult.getUnfoldedModel());
200 value.setNameMapping(composedModel.value2());
201 }
202
203=== modified file 'src/dk/aau/cs/verification/QueryResult.java'
204--- src/dk/aau/cs/verification/QueryResult.java 2022-02-02 14:59:29 +0000
205+++ src/dk/aau/cs/verification/QueryResult.java 2022-02-08 09:07:46 +0000
206@@ -26,14 +26,6 @@
207 this.solvedUsingTraceAbstractRefinement = solvedUsingTraceAbstractRefinement;
208 }
209
210- public boolean isSolvedUsingStateEquation() {
211- return solvedUsingStateEquation;
212- }
213-
214- public void setSolvedUsingStateEquation(boolean solvedUsingStateEquation) {
215- this.solvedUsingStateEquation = solvedUsingStateEquation;
216- }
217-
218 public boolean isSolvedUsingSiphonTrap() {
219 return solvedUsingSiphonTrap;
220 }
221@@ -44,7 +36,6 @@
222
223 private boolean solvedUsingQuerySimplification;
224 private boolean solvedUsingTraceAbstractRefinement;
225- private boolean solvedUsingStateEquation;
226 private boolean solvedUsingSiphonTrap;
227
228 public boolean isCTL = false;
229
230=== modified file 'src/dk/aau/cs/verification/UPPAAL/UppaalIconSelector.java'
231--- src/dk/aau/cs/verification/UPPAAL/UppaalIconSelector.java 2020-04-18 15:55:51 +0000
232+++ src/dk/aau/cs/verification/UPPAAL/UppaalIconSelector.java 2022-02-08 09:07:46 +0000
233@@ -11,7 +11,7 @@
234 @Override
235 public ImageIcon getIconFor(VerificationResult<?> result){
236 if (result.getQueryResult().isApproximationInconclusive()) return rerunIcon;
237- if(result.isSolvedUsingStateEquation()) return result.isQuerySatisfied()? satisfiedIcon:notSatisfiedIcon; // If we got a result from over-approximation, this is always conclusive.
238+ if(result.isResolvedUsingSkeletonPreprocessor()) return result.isQuerySatisfied()? satisfiedIcon:notSatisfiedIcon; // If we got a result from over-approximation, this is always conclusive.
239 if(result.getQueryResult().hasDeadlock()) return inconclusiveIcon;
240
241 switch(result.getQueryResult().queryType())
242
243=== modified file 'src/dk/aau/cs/verification/VerificationResult.java'
244--- src/dk/aau/cs/verification/VerificationResult.java 2022-02-02 14:59:29 +0000
245+++ src/dk/aau/cs/verification/VerificationResult.java 2022-02-08 09:07:46 +0000
246@@ -30,10 +30,6 @@
247 return queryResult.isSolvedUsingTraceAbstractRefinement();
248 }
249
250- public boolean isSolvedUsingStateEquation() {
251- return queryResult.isSolvedUsingStateEquation();
252- }
253-
254 public boolean isSolvedUsingSiphonTrap() {
255 return queryResult.isSolvedUsingSiphonTrap();
256 }
257
258=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java'
259--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java 2022-02-08 08:56:59 +0000
260+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java 2022-02-08 09:07:46 +0000
261@@ -347,10 +347,9 @@
262 tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1());
263 }
264 }
265+
266 var result = new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, runner.getRunningTime(), queryResult.value2(), false, standardOutput + "\n\n" + errorOutput, model);
267- if (queryResult.value1().isSolvedUsingStateEquation()) {
268
269- }
270 return result;
271 }
272 }
273
274=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPNCTLOutputParser.java'
275--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPNCTLOutputParser.java 2022-02-02 14:59:29 +0000
276+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPNCTLOutputParser.java 2022-02-08 09:07:46 +0000
277@@ -90,7 +90,6 @@
278 BoundednessAnalysisResult boundedAnalysis = new BoundednessAnalysisResult(totalTokens, maxUsedTokens, extraTokens);
279 var qr = new QueryResult(result, boundedAnalysis, query, false);
280 qr.setSolvedUsingQuerySimplification(solvedUsingQuerySimplification);
281- qr.setSolvedUsingStateEquation(solvedUsingStateEquation);
282 qr.setSolvedUsingTraceAbstractRefinement(solvedUsingTraceAbstractRefinement);
283 qr.setSolvedUsingSiphonTrap(solvedUsingSiphonTrap);
284
285
286=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOutputParser.java'
287--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOutputParser.java 2022-02-02 14:59:29 +0000
288+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOutputParser.java 2022-02-08 09:07:46 +0000
289@@ -177,7 +177,6 @@
290
291 var qr = new QueryResult(result, boundedAnalysis, query, false);
292 qr.setSolvedUsingQuerySimplification(solvedUsingQuerySimplification);
293- qr.setSolvedUsingStateEquation(solvedUsingStateEquation);
294 qr.setSolvedUsingTraceAbstractRefinement(solvedUsingTraceAbstractRefinement);
295 qr.setSolvedUsingSiphonTrap(solvedUsingSiphonTrap);
296 return new Tuple<QueryResult, Stats>(qr, new Stats(discovered, explored, explored, transitionStats, placeBoundStats, reductionStats));
297
298=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOutputParser.java'
299--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOutputParser.java 2022-02-02 14:59:29 +0000
300+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOutputParser.java 2022-02-08 09:07:46 +0000
301@@ -38,9 +38,7 @@
302 boolean solvedUsingQuerySimplification = false;
303 private static final String solvedUsingTraceAbstractRefinement_STRING = "Solved using Trace Abstraction Refinement";
304 boolean solvedUsingTraceAbstractRefinement = false;
305- private static final String solvedUsingStateEquation_STRING = "Solved using Trace Abstraction Refinement";
306- boolean solvedUsingStateEquation = false;
307- private static final String solvedUsingSiphonTrap_STRING = "Solved using Siphon Trap";
308+ private static final String solvedUsingSiphonTrap_STRING = "Query solved by Siphon-Trap Analysis.";
309 boolean solvedUsingSiphonTrap = false;
310
311 void parseSolvedMethod(String line) {
312@@ -48,8 +46,6 @@
313 solvedUsingQuerySimplification = true;
314 } else if (line.contains(solvedUsingTraceAbstractRefinement_STRING)) {
315 solvedUsingTraceAbstractRefinement = true;
316- } else if (line.contains(solvedUsingStateEquation_STRING)) {
317- solvedUsingStateEquation = true;
318 } else if (line.contains(solvedUsingSiphonTrap_STRING)) {
319 solvedUsingSiphonTrap = true;
320 }
321
322=== modified file 'src/net/tapaal/gui/petrinet/verification/RunVerification.java'
323--- src/net/tapaal/gui/petrinet/verification/RunVerification.java 2022-02-03 12:31:00 +0000
324+++ src/net/tapaal/gui/petrinet/verification/RunVerification.java 2022-02-08 09:07:46 +0000
325@@ -382,34 +382,32 @@
326 if (result.getRawOutput() != null) {
327 JButton showRawQueryButton = new JButton("Show raw query results");
328 showRawQueryButton.addActionListener(arg0 -> JOptionPane.showMessageDialog(panel, createRawQueryPanel(result.getRawOutput()), "Raw query results", JOptionPane.INFORMATION_MESSAGE));
329- gbc = GridBagHelper.as(1, 5, WEST, new Insets(0,0,10,0));
330+ gbc = GridBagHelper.as(1, rowOffset+1, WEST, new Insets(0,0,10,0));
331 panel.add(showRawQueryButton, gbc);
332 }
333
334 if (result.isResolvedUsingSkeletonPreprocessor()) {
335- gbc = GridBagHelper.as(0, rowOffset+1, GridBagHelper.Anchor.WEST, new Insets(0,0,15,0));
336+ gbc = GridBagHelper.as(0, rowOffset+2, GridBagHelper.Anchor.WEST, new Insets(0,0,15,0));
337 gbc.gridwidth = 2;
338- panel.add(new JLabel(toHTML("The query was resolved using Skeleton Analysis preprocessing")), gbc);
339+ panel.add(new JLabel(toHTML("The query was answered by Skeleton Analysis preprocessing.")), gbc);
340 }
341
342
343- gbc = GridBagHelper.as(0, rowOffset+2, WEST, new Insets(0,0,15,0));
344+ gbc = GridBagHelper.as(0, rowOffset+3, WEST, new Insets(0,0,15,0));
345 gbc.gridwidth = 2;
346 if(result.isSolvedUsingQuerySimplification()){
347 panel.add(new JLabel(toHTML("The query was resolved using Query Simplification.")), gbc);
348 } else if (result.isSolvedUsingTraceAbstractRefinement()){
349- panel.add(new JLabel(toHTML("The query was not resolved using Trace Abstraction Refinement.")), gbc);
350- } else if (result.isSolvedUsingStateEquation()) {
351- panel.add(new JLabel(toHTML("The query was resolved using state equations.")), gbc);
352+ panel.add(new JLabel(toHTML("The query was resolved using Trace Abstraction Refinement.")), gbc);
353 } else if (result.isSolvedUsingSiphonTrap()) {
354 panel.add(new JLabel(toHTML("The query was resolved using Siphon Trap.")), gbc);
355 }
356
357- gbc = GridBagHelper.as(0, rowOffset+3, WEST);
358+ gbc = GridBagHelper.as(0, rowOffset+4, WEST);
359 gbc.gridwidth = 2;
360 panel.add(new JLabel(result.getVerificationTimeString()), gbc);
361
362- gbc = GridBagHelper.as(0, rowOffset+4, WEST);
363+ gbc = GridBagHelper.as(0, rowOffset+5, WEST);
364 gbc.gridwidth = 2;
365 panel.add(new JLabel("Estimated memory usage: "+MemoryMonitor.getPeakMemory()), gbc);
366
367@@ -421,7 +419,7 @@
368 (queryResult.queryType() == QueryType.AF && queryResult.isQuerySatisfied()))
369 && modelChecker.useDiscreteSemantics()) {
370
371- gbc = GridBagHelper.as(0, rowOffset+7, WEST);
372+ gbc = GridBagHelper.as(0, rowOffset+8, WEST);
373 gbc.gridwidth = 2;
374 panel.add(new JLabel("<html><font color=red>The verification answer is guaranteed for<br/>the discrete semantics only (integer delays).</font></html>"), gbc);
375 }

Subscribers

People subscribed via source and target branches

to all changes: