Merge lp:~tapaal-contributor/tapaal/save-tar-option into lp:tapaal
- save-tar-option
- Merge into trunk
Proposed by
Lena Ernstsen
Status: | Merged |
---|---|
Approved by: | Jiri Srba |
Approved revision: | 1121 |
Merged at revision: | 1120 |
Proposed branch: | lp:~tapaal-contributor/tapaal/save-tar-option |
Merge into: | lp:tapaal |
Diff against target: |
150 lines (+35/-3) 7 files modified
src/dk/aau/cs/gui/BatchProcessingDialog.java (+4/-0) src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java (+3/-1) src/dk/aau/cs/io/queries/TAPNQueryLoader.java (+15/-0) src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java (+7/-0) src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java (+4/-2) src/pipe/dataLayer/TAPNQuery.java (+1/-0) src/pipe/gui/widgets/QueryDialog.java (+1/-0) |
To merge this branch: | bzr merge lp:~tapaal-contributor/tapaal/save-tar-option |
Related bugs: |
Reviewer | Review Type | Date Requested | Status |
---|---|---|---|
Jiri Srba | Approve | ||
Review via email: mp+399026@code.launchpad.net |
Commit message
The trace refinement option is saved in the .tapn file
Description of the change
To post a comment you must log in.
Revision history for this message
Jiri Srba (srba) : | # |
review:
Approve
Preview Diff
[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1 | === modified file 'src/dk/aau/cs/gui/BatchProcessingDialog.java' | |||
2 | --- src/dk/aau/cs/gui/BatchProcessingDialog.java 2020-07-20 07:55:49 +0000 | |||
3 | +++ src/dk/aau/cs/gui/BatchProcessingDialog.java 2021-03-02 20:12:24 +0000 | |||
4 | @@ -1577,6 +1577,10 @@ | |||
5 | 1577 | s.append("Stubborn Reduction: "); | 1577 | s.append("Stubborn Reduction: "); |
6 | 1578 | s.append(query.isStubbornReductionEnabled() ? "Yes\n\n" : "No\n\n"); | 1578 | s.append(query.isStubbornReductionEnabled() ? "Yes\n\n" : "No\n\n"); |
7 | 1579 | 1579 | ||
8 | 1580 | s.append("\n\n"); | ||
9 | 1581 | s.append("Trace Abstract Refinement: "); | ||
10 | 1582 | s.append(query.isTarOptionEnabled() ? "Yes\n\n" : "No\n\n"); | ||
11 | 1583 | |||
12 | 1580 | s.append("Query Property:\n"); | 1584 | s.append("Query Property:\n"); |
13 | 1581 | s.append(query.getProperty().toString()); | 1585 | s.append(query.getProperty().toString()); |
14 | 1582 | 1586 | ||
15 | 1583 | 1587 | ||
16 | === modified file 'src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java' | |||
17 | --- src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java 2020-08-11 13:25:25 +0000 | |||
18 | +++ src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java 2021-03-02 20:12:24 +0000 | |||
19 | @@ -320,7 +320,8 @@ | |||
20 | 320 | queryElement.setAttribute("enableOverApproximation", "" + query.isOverApproximationEnabled()); | 320 | queryElement.setAttribute("enableOverApproximation", "" + query.isOverApproximationEnabled()); |
21 | 321 | queryElement.setAttribute("enableUnderApproximation", "" + query.isUnderApproximationEnabled()); | 321 | queryElement.setAttribute("enableUnderApproximation", "" + query.isUnderApproximationEnabled()); |
22 | 322 | queryElement.setAttribute("approximationDenominator", "" + query.approximationDenominator()); | 322 | queryElement.setAttribute("approximationDenominator", "" + query.approximationDenominator()); |
24 | 323 | queryElement.setAttribute("useStubbornReduction", "" + query.isStubbornReductionEnabled()); | 323 | queryElement.setAttribute("useStubbornReduction", "" + query.isStubbornReductionEnabled()); |
25 | 324 | queryElement.setAttribute("useTarOption", "" + query.isTarOptionEnabled()); | ||
26 | 324 | 325 | ||
27 | 325 | return queryElement; | 326 | return queryElement; |
28 | 326 | } | 327 | } |
29 | @@ -358,6 +359,7 @@ | |||
30 | 358 | queryElement.setAttribute("useSiphonTrapAnalysis", "" + query.isSiphontrapEnabled()); | 359 | queryElement.setAttribute("useSiphonTrapAnalysis", "" + query.isSiphontrapEnabled()); |
31 | 359 | queryElement.setAttribute("useQueryReduction", "" + query.isQueryReductionEnabled()); | 360 | queryElement.setAttribute("useQueryReduction", "" + query.isQueryReductionEnabled()); |
32 | 360 | queryElement.setAttribute("useStubbornReduction", "" + query.isStubbornReductionEnabled()); | 361 | queryElement.setAttribute("useStubbornReduction", "" + query.isStubbornReductionEnabled()); |
33 | 362 | queryElement.setAttribute("useTarOption", "" + query.isTarOptionEnabled()); | ||
34 | 361 | 363 | ||
35 | 362 | return queryElement; | 364 | return queryElement; |
36 | 363 | } | 365 | } |
37 | 364 | 366 | ||
38 | === modified file 'src/dk/aau/cs/io/queries/TAPNQueryLoader.java' | |||
39 | --- src/dk/aau/cs/io/queries/TAPNQueryLoader.java 2020-10-31 17:27:18 +0000 | |||
40 | +++ src/dk/aau/cs/io/queries/TAPNQueryLoader.java 2021-03-02 20:12:24 +0000 | |||
41 | @@ -91,6 +91,7 @@ | |||
42 | 91 | boolean siphontrap = getReductionOption(queryElement, "useSiphonTrapAnalysis", false); | 91 | boolean siphontrap = getReductionOption(queryElement, "useSiphonTrapAnalysis", false); |
43 | 92 | boolean queryReduction = getReductionOption(queryElement, "useQueryReduction", true); | 92 | boolean queryReduction = getReductionOption(queryElement, "useQueryReduction", true); |
44 | 93 | boolean stubborn = getReductionOption(queryElement, "useStubbornReduction", true); | 93 | boolean stubborn = getReductionOption(queryElement, "useStubbornReduction", true); |
45 | 94 | boolean useTar = getTarOption(queryElement, "useTarOption", false); | ||
46 | 94 | 95 | ||
47 | 95 | TCTLAbstractProperty query; | 96 | TCTLAbstractProperty query; |
48 | 96 | if (queryElement.getElementsByTagName("formula").item(0) != null){ | 97 | if (queryElement.getElementsByTagName("formula").item(0) != null){ |
49 | @@ -107,6 +108,7 @@ | |||
50 | 107 | parsedQuery.setUseSiphontrap(siphontrap); | 108 | parsedQuery.setUseSiphontrap(siphontrap); |
51 | 108 | parsedQuery.setUseQueryReduction(queryReduction); | 109 | parsedQuery.setUseQueryReduction(queryReduction); |
52 | 109 | parsedQuery.setUseStubbornReduction(stubborn); | 110 | parsedQuery.setUseStubbornReduction(stubborn); |
53 | 111 | parsedQuery.setUseTarOption(useTar); | ||
54 | 110 | if (parsedQuery.getCategory() == QueryCategory.CTL && algorithmOption != null){ | 112 | if (parsedQuery.getCategory() == QueryCategory.CTL && algorithmOption != null){ |
55 | 111 | parsedQuery.setAlgorithmOption(AlgorithmOption.valueOf(algorithmOption)); | 113 | parsedQuery.setAlgorithmOption(AlgorithmOption.valueOf(algorithmOption)); |
56 | 112 | // RenameTemplateVisitor rt = new RenameTemplateVisitor("", | 114 | // RenameTemplateVisitor rt = new RenameTemplateVisitor("", |
57 | @@ -229,6 +231,19 @@ | |||
58 | 229 | } | 231 | } |
59 | 230 | return result; | 232 | return result; |
60 | 231 | } | 233 | } |
61 | 234 | |||
62 | 235 | private boolean getTarOption(Element queryElement, String attributeName, boolean defaultValue) { | ||
63 | 236 | if(!queryElement.hasAttribute(attributeName)){ | ||
64 | 237 | return defaultValue; | ||
65 | 238 | } | ||
66 | 239 | boolean result; | ||
67 | 240 | try { | ||
68 | 241 | result = queryElement.getAttribute(attributeName).equals("true"); | ||
69 | 242 | } catch(Exception e) { | ||
70 | 243 | result = defaultValue; | ||
71 | 244 | } | ||
72 | 245 | return result; | ||
73 | 246 | } | ||
74 | 232 | 247 | ||
75 | 233 | private int getApproximationValue(Element queryElement, String attributeName, int defaultValue) | 248 | private int getApproximationValue(Element queryElement, String attributeName, int defaultValue) |
76 | 234 | { | 249 | { |
77 | 235 | 250 | ||
78 | === modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java' | |||
79 | --- src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java 2021-02-07 11:09:51 +0000 | |||
80 | +++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java 2021-03-02 20:12:24 +0000 | |||
81 | @@ -43,6 +43,13 @@ | |||
82 | 43 | enableUnderApproximation, approximationDenominator,queryCategory, algorithmOption, siphontrap, queryReduction, stubbornReduction, null, false); | 43 | enableUnderApproximation, approximationDenominator,queryCategory, algorithmOption, siphontrap, queryReduction, stubbornReduction, null, false); |
83 | 44 | } | 44 | } |
84 | 45 | 45 | ||
85 | 46 | public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, boolean useModelReduction, | ||
86 | 47 | boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, QueryCategory queryCategory, AlgorithmOption algorithmOption, | ||
87 | 48 | boolean siphontrap, QueryReductionTime queryReduction, boolean stubbornReduction, boolean useTarOption) { | ||
88 | 49 | this(extraTokens, traceOption, search, useOverApproximation, useModelReduction? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION, enableOverApproximation, | ||
89 | 50 | enableUnderApproximation, approximationDenominator,queryCategory, algorithmOption, siphontrap, queryReduction, stubbornReduction, null, useTarOption); | ||
90 | 51 | } | ||
91 | 52 | |||
92 | 46 | @Override | 53 | @Override |
93 | 47 | public String toString() { | 54 | public String toString() { |
94 | 48 | StringBuilder result = new StringBuilder(); | 55 | StringBuilder result = new StringBuilder(); |
95 | 49 | 56 | ||
96 | === modified file 'src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java' | |||
97 | --- src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java 2020-10-15 15:44:06 +0000 | |||
98 | +++ src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java 2021-03-02 20:12:24 +0000 | |||
99 | @@ -356,6 +356,7 @@ | |||
100 | 356 | boolean stubbornReduction = batchProcessingVerificationOptions.stubbornReductionOption() == StubbornReductionOption.KeepQueryOption ? query.isStubbornReductionEnabled() : getStubbornReductionFromBatchProcessingOptions(); | 356 | boolean stubbornReduction = batchProcessingVerificationOptions.stubbornReductionOption() == StubbornReductionOption.KeepQueryOption ? query.isStubbornReductionEnabled() : getStubbornReductionFromBatchProcessingOptions(); |
101 | 357 | boolean overApproximation = query.isOverApproximationEnabled(); | 357 | boolean overApproximation = query.isOverApproximationEnabled(); |
102 | 358 | boolean underApproximation = query.isUnderApproximationEnabled(); | 358 | boolean underApproximation = query.isUnderApproximationEnabled(); |
103 | 359 | boolean useTar = query.isTarOptionEnabled(); | ||
104 | 359 | int approximationDenominator = query.approximationDenominator(); | 360 | int approximationDenominator = query.approximationDenominator(); |
105 | 360 | if (batchProcessingVerificationOptions.approximationMethodOption() == ApproximationMethodOption.None) { | 361 | if (batchProcessingVerificationOptions.approximationMethodOption() == ApproximationMethodOption.None) { |
106 | 361 | overApproximation = false; | 362 | overApproximation = false; |
107 | @@ -381,6 +382,7 @@ | |||
108 | 381 | changedQuery.setUseSiphontrap(query.isSiphontrapEnabled()); | 382 | changedQuery.setUseSiphontrap(query.isSiphontrapEnabled()); |
109 | 382 | changedQuery.setUseQueryReduction(query.isQueryReductionEnabled()); | 383 | changedQuery.setUseQueryReduction(query.isQueryReductionEnabled()); |
110 | 383 | changedQuery.setUseStubbornReduction(stubbornReduction); | 384 | changedQuery.setUseStubbornReduction(stubbornReduction); |
111 | 385 | changedQuery.setUseTarOption(useTar); | ||
112 | 384 | return changedQuery; | 386 | return changedQuery; |
113 | 385 | } else if (batchProcessingVerificationOptions.queryPropertyOption() == QueryPropertyOption.Soundness) { | 387 | } else if (batchProcessingVerificationOptions.queryPropertyOption() == QueryPropertyOption.Soundness) { |
114 | 386 | isSoundnessCheck = true; | 388 | isSoundnessCheck = true; |
115 | @@ -623,9 +625,9 @@ | |||
116 | 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()); | 625 | 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()); |
117 | 624 | else if(query.getReductionOption() == ReductionOption.VerifyPN || query.getReductionOption() == ReductionOption.VerifyPNApprox || query.getReductionOption() == ReductionOption.VerifyPNReduce) | 626 | else if(query.getReductionOption() == ReductionOption.VerifyPN || query.getReductionOption() == ReductionOption.VerifyPNApprox || query.getReductionOption() == ReductionOption.VerifyPNReduce) |
118 | 625 | if (batchProcessingVerificationOptions.queryPropertyOption() == QueryPropertyOption.SearchWholeStateSpace){ | 627 | if (batchProcessingVerificationOptions.queryPropertyOption() == QueryPropertyOption.SearchWholeStateSpace){ |
120 | 626 | return new VerifyPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), false, false, false, false, query.approximationDenominator(), QueryCategory.Default, query.getAlgorithmOption(), false, QueryReductionTime.UnlimitedTime, false); | 628 | return new VerifyPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), false, false, false, false, query.approximationDenominator(), QueryCategory.Default, query.getAlgorithmOption(), false, QueryReductionTime.UnlimitedTime, false, query.isTarOptionEnabled()); |
121 | 627 | } else { | 629 | } else { |
123 | 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()); | 630 | 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(), query.isTarOptionEnabled()); |
124 | 629 | } | 631 | } |
125 | 630 | else | 632 | else |
126 | 631 | return new VerifytaOptions(TraceOption.NONE, query.getSearchOption(), false, query.getReductionOption(), query.useSymmetry(), false, query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator()); | 633 | return new VerifytaOptions(TraceOption.NONE, query.getSearchOption(), false, query.getReductionOption(), query.useSymmetry(), false, query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator()); |
127 | 632 | 634 | ||
128 | === modified file 'src/pipe/dataLayer/TAPNQuery.java' | |||
129 | --- src/pipe/dataLayer/TAPNQuery.java 2021-02-07 11:09:51 +0000 | |||
130 | +++ src/pipe/dataLayer/TAPNQuery.java 2021-03-02 20:12:24 +0000 | |||
131 | @@ -393,6 +393,7 @@ | |||
132 | 393 | copy.setUseSiphontrap(this.isQueryReductionEnabled()); | 393 | copy.setUseSiphontrap(this.isQueryReductionEnabled()); |
133 | 394 | copy.setUseQueryReduction(this.isQueryReductionEnabled()); | 394 | copy.setUseQueryReduction(this.isQueryReductionEnabled()); |
134 | 395 | copy.setUseStubbornReduction(this.isStubbornReductionEnabled()); | 395 | copy.setUseStubbornReduction(this.isStubbornReductionEnabled()); |
135 | 396 | copy.setUseTarOption(this.isTarOptionEnabled()); | ||
136 | 396 | 397 | ||
137 | 397 | return copy; | 398 | return copy; |
138 | 398 | } | 399 | } |
139 | 399 | 400 | ||
140 | === modified file 'src/pipe/gui/widgets/QueryDialog.java' | |||
141 | --- src/pipe/gui/widgets/QueryDialog.java 2021-02-22 22:26:01 +0000 | |||
142 | +++ src/pipe/gui/widgets/QueryDialog.java 2021-03-02 20:12:24 +0000 | |||
143 | @@ -1292,6 +1292,7 @@ | |||
144 | 1292 | useQueryReduction.setSelected(queryToCreateFrom.isQueryReductionEnabled()); | 1292 | useQueryReduction.setSelected(queryToCreateFrom.isQueryReductionEnabled()); |
145 | 1293 | useStubbornReduction.setSelected(queryToCreateFrom.isStubbornReductionEnabled()); | 1293 | useStubbornReduction.setSelected(queryToCreateFrom.isStubbornReductionEnabled()); |
146 | 1294 | useReduction.setSelected(queryToCreateFrom.useReduction()); | 1294 | useReduction.setSelected(queryToCreateFrom.useReduction()); |
147 | 1295 | useTraceRefinement.setSelected(queryToCreateFrom.isTarOptionEnabled()); | ||
148 | 1295 | } | 1296 | } |
149 | 1296 | 1297 | ||
150 | 1297 | private void setupTraceOptionsFromQuery(TAPNQuery queryToCreateFrom) { | 1298 | private void setupTraceOptionsFromQuery(TAPNQuery queryToCreateFrom) { |