Merge lp:~tapaal-contributor/tapaal/ltl-icon-selection-1997234 into lp:tapaal/3.9
- ltl-icon-selection-1997234
- Merge into 3.9
Proposed by
Lena Ernstsen
Status: | Merged |
---|---|
Approved by: | Jiri Srba |
Approved revision: | 1179 |
Merge reported by: | Jiri Srba |
Merged at revision: | not available |
Proposed branch: | lp:~tapaal-contributor/tapaal/ltl-icon-selection-1997234 |
Merge into: | lp:tapaal/3.9 |
Diff against target: |
310 lines (+112/-32) 9 files modified
src/dk/aau/cs/model/tapn/TAPNQuery.java (+6/-7) src/dk/aau/cs/verification/QueryResult.java (+2/-0) src/dk/aau/cs/verification/QueryType.java (+3/-1) src/dk/aau/cs/verification/Stats.java (+3/-3) src/dk/aau/cs/verification/VerificationResult.java (+16/-0) src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java (+0/-1) src/dk/aau/cs/verification/VerifyTAPN/VerifyPNCTLOutputParser.java (+18/-10) src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java (+28/-8) src/pipe/gui/RunVerification.java (+36/-2) |
To merge this branch: | bzr merge lp:~tapaal-contributor/tapaal/ltl-icon-selection-1997234 |
Related bugs: |
Reviewer | Review Type | Date Requested | Status |
---|---|---|---|
Jiri Srba | Approve | ||
Review via email: mp+435360@code.launchpad.net |
This proposal supersedes a proposal from 2023-01-09.
Commit message
Considers LTL nodes when selecting icons for verification
Description of the change
To post a comment you must log in.
- 1177. By Lena Ernstsen
-
Reverted change to avoid NPE
- 1178. By Lena Ernstsen
-
Added 'show raw query results' button for state equation results
- 1179. By Lena Ernstsen
-
Fixed wrong statistics for CTL queries
Preview Diff
[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1 | === modified file 'src/dk/aau/cs/model/tapn/TAPNQuery.java' | |||
2 | --- src/dk/aau/cs/model/tapn/TAPNQuery.java 2016-04-14 20:09:47 +0000 | |||
3 | +++ src/dk/aau/cs/model/tapn/TAPNQuery.java 2023-01-23 10:20:36 +0000 | |||
4 | @@ -1,9 +1,6 @@ | |||
5 | 1 | package dk.aau.cs.model.tapn; | 1 | package dk.aau.cs.model.tapn; |
6 | 2 | 2 | ||
11 | 3 | import dk.aau.cs.TCTL.TCTLAFNode; | 3 | import dk.aau.cs.TCTL.*; |
8 | 4 | import dk.aau.cs.TCTL.TCTLAbstractProperty; | ||
9 | 5 | import dk.aau.cs.TCTL.TCTLEFNode; | ||
10 | 6 | import dk.aau.cs.TCTL.TCTLEGNode; | ||
12 | 7 | import dk.aau.cs.TCTL.visitors.HasDeadlockVisitor; | 4 | import dk.aau.cs.TCTL.visitors.HasDeadlockVisitor; |
13 | 8 | import dk.aau.cs.verification.QueryType; | 5 | import dk.aau.cs.verification.QueryType; |
14 | 9 | import pipe.dataLayer.TAPNQuery.QueryCategory; | 6 | import pipe.dataLayer.TAPNQuery.QueryCategory; |
15 | @@ -27,9 +24,11 @@ | |||
16 | 27 | } | 24 | } |
17 | 28 | 25 | ||
18 | 29 | public QueryType queryType(){ | 26 | public QueryType queryType(){ |
22 | 30 | if(property instanceof TCTLEFNode) return QueryType.EF; | 27 | if (property instanceof TCTLEFNode) return QueryType.EF; |
23 | 31 | else if(property instanceof TCTLEGNode) return QueryType.EG; | 28 | else if (property instanceof TCTLEGNode) return QueryType.EG; |
24 | 32 | else if(property instanceof TCTLAFNode) return QueryType.AF; | 29 | else if (property instanceof LTLENode) return QueryType.E; |
25 | 30 | else if (property instanceof LTLANode) return QueryType.A; | ||
26 | 31 | else if (property instanceof TCTLAFNode) return QueryType.AF; | ||
27 | 33 | else return QueryType.AG; | 32 | else return QueryType.AG; |
28 | 34 | } | 33 | } |
29 | 35 | 34 | ||
30 | 36 | 35 | ||
31 | === modified file 'src/dk/aau/cs/verification/QueryResult.java' | |||
32 | --- src/dk/aau/cs/verification/QueryResult.java 2020-07-13 13:58:47 +0000 | |||
33 | +++ src/dk/aau/cs/verification/QueryResult.java 2023-01-23 10:20:36 +0000 | |||
34 | @@ -61,6 +61,8 @@ | |||
35 | 61 | || (queryType().equals(QueryType.EG)) // && !isQuerySatisfied()) | 61 | || (queryType().equals(QueryType.EG)) // && !isQuerySatisfied()) |
36 | 62 | || (queryType().equals(QueryType.AF)) // && isQuerySatisfied()) | 62 | || (queryType().equals(QueryType.AF)) // && isQuerySatisfied()) |
37 | 63 | || (queryType().equals(QueryType.AG) && isQuerySatisfied()) | 63 | || (queryType().equals(QueryType.AG) && isQuerySatisfied()) |
38 | 64 | || (queryType().equals(QueryType.A)) | ||
39 | 65 | || (queryType().equals(QueryType.E)) | ||
40 | 64 | || (hasDeadlock() && | 66 | || (hasDeadlock() && |
41 | 65 | (!isQuerySatisfied() && queryType().equals(QueryType.EF)) || | 67 | (!isQuerySatisfied() && queryType().equals(QueryType.EF)) || |
42 | 66 | (isQuerySatisfied() && queryType().equals(QueryType.AG)) | 68 | (isQuerySatisfied() && queryType().equals(QueryType.AG)) |
43 | 67 | 69 | ||
44 | === modified file 'src/dk/aau/cs/verification/QueryType.java' | |||
45 | --- src/dk/aau/cs/verification/QueryType.java 2011-05-21 13:00:05 +0000 | |||
46 | +++ src/dk/aau/cs/verification/QueryType.java 2023-01-23 10:20:36 +0000 | |||
47 | @@ -4,5 +4,7 @@ | |||
48 | 4 | EF, | 4 | EF, |
49 | 5 | EG, | 5 | EG, |
50 | 6 | AF, | 6 | AF, |
52 | 7 | AG | 7 | AG, |
53 | 8 | A, | ||
54 | 9 | E | ||
55 | 8 | } | 10 | } |
56 | 9 | 11 | ||
57 | === modified file 'src/dk/aau/cs/verification/Stats.java' | |||
58 | --- src/dk/aau/cs/verification/Stats.java 2020-07-13 13:58:47 +0000 | |||
59 | +++ src/dk/aau/cs/verification/Stats.java 2023-01-23 10:20:36 +0000 | |||
60 | @@ -137,15 +137,15 @@ | |||
61 | 137 | @Override | 137 | @Override |
62 | 138 | public String toString() { | 138 | public String toString() { |
63 | 139 | StringBuilder buffer = new StringBuilder(); | 139 | StringBuilder buffer = new StringBuilder(); |
65 | 140 | buffer.append("Discovered markings: "); | 140 | buffer.append("Discovered configurations: "); |
66 | 141 | buffer.append(discovered); | 141 | buffer.append(discovered); |
67 | 142 | buffer.append(System.getProperty("line.separator")); | 142 | buffer.append(System.getProperty("line.separator")); |
68 | 143 | 143 | ||
70 | 144 | buffer.append("Explored markings: "); | 144 | buffer.append("Explored configurations: "); |
71 | 145 | buffer.append(explored); | 145 | buffer.append(explored); |
72 | 146 | buffer.append(System.getProperty("line.separator")); | 146 | buffer.append(System.getProperty("line.separator")); |
73 | 147 | 147 | ||
75 | 148 | buffer.append("Stored markings: "); | 148 | buffer.append("Stored configurations: "); |
76 | 149 | buffer.append(stored); | 149 | buffer.append(stored); |
77 | 150 | return buffer.toString(); | 150 | return buffer.toString(); |
78 | 151 | } | 151 | } |
79 | 152 | 152 | ||
80 | === modified file 'src/dk/aau/cs/verification/VerificationResult.java' | |||
81 | --- src/dk/aau/cs/verification/VerificationResult.java 2021-10-13 18:51:36 +0000 | |||
82 | +++ src/dk/aau/cs/verification/VerificationResult.java 2023-01-23 10:20:36 +0000 | |||
83 | @@ -4,6 +4,8 @@ | |||
84 | 4 | import java.util.ArrayList; | 4 | import java.util.ArrayList; |
85 | 5 | import java.util.Comparator; | 5 | import java.util.Comparator; |
86 | 6 | import java.util.List; | 6 | import java.util.List; |
87 | 7 | import java.util.regex.Matcher; | ||
88 | 8 | import java.util.regex.Pattern; | ||
89 | 7 | 9 | ||
90 | 8 | import dk.aau.cs.model.tapn.NetworkMarking; | 10 | import dk.aau.cs.model.tapn.NetworkMarking; |
91 | 9 | import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork; | 11 | import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork; |
92 | @@ -21,6 +23,7 @@ | |||
93 | 21 | private NameMapping nameMapping; | 23 | private NameMapping nameMapping; |
94 | 22 | private TTrace secondaryTrace; | 24 | private TTrace secondaryTrace; |
95 | 23 | private boolean isSolvedUsingStateEquation = false; | 25 | private boolean isSolvedUsingStateEquation = false; |
96 | 26 | private int bound; | ||
97 | 24 | 27 | ||
98 | 25 | public boolean isQuerySatisfied() { | 28 | public boolean isQuerySatisfied() { |
99 | 26 | return queryResult.isQuerySatisfied(); | 29 | return queryResult.isQuerySatisfied(); |
100 | @@ -32,6 +35,15 @@ | |||
101 | 32 | this.verificationTime = verificationTime; | 35 | this.verificationTime = verificationTime; |
102 | 33 | this.stats = stats; | 36 | this.stats = stats; |
103 | 34 | this.rawOutput = rawOutput; | 37 | this.rawOutput = rawOutput; |
104 | 38 | |||
105 | 39 | String[] lines = rawOutput.split(System.getProperty("line.separator")); | ||
106 | 40 | for (String line : lines) { | ||
107 | 41 | Matcher matcher = Pattern.compile("\\s*-k\\s*(\\d+)\\s*").matcher(line); | ||
108 | 42 | if (matcher.find()) { | ||
109 | 43 | this.bound = Integer.parseInt(matcher.group(1)); | ||
110 | 44 | break; | ||
111 | 45 | } | ||
112 | 46 | } | ||
113 | 35 | } | 47 | } |
114 | 36 | 48 | ||
115 | 37 | public VerificationResult(QueryResult queryResult, TTrace trace, long verificationTime, Stats stats, boolean isSolvedUsingStateEquation){ | 49 | public VerificationResult(QueryResult queryResult, TTrace trace, long verificationTime, Stats stats, boolean isSolvedUsingStateEquation){ |
116 | @@ -231,4 +243,8 @@ | |||
117 | 231 | public String getRawOutput() { | 243 | public String getRawOutput() { |
118 | 232 | return rawOutput; | 244 | return rawOutput; |
119 | 233 | } | 245 | } |
120 | 246 | |||
121 | 247 | public int getBound() { | ||
122 | 248 | return bound; | ||
123 | 249 | } | ||
124 | 234 | } | 250 | } |
125 | 235 | 251 | ||
126 | === modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java' | |||
127 | --- src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java 2021-07-16 20:39:22 +0000 | |||
128 | +++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java 2023-01-23 10:20:36 +0000 | |||
129 | @@ -340,7 +340,6 @@ | |||
130 | 340 | tapnTrace = parseTrace(trace, options, model, exportedModel, query, queryResult.value1()); | 340 | tapnTrace = parseTrace(trace, options, model, exportedModel, query, queryResult.value1()); |
131 | 341 | } else { | 341 | } else { |
132 | 342 | tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1()); | 342 | tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1()); |
133 | 343 | |||
134 | 344 | } | 343 | } |
135 | 345 | return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, runner.getRunningTime(), queryResult.value2(), approximationResult, standardOutput); | 344 | return new VerificationResult<TimedArcPetriNetTrace>(queryResult.value1(), tapnTrace, runner.getRunningTime(), queryResult.value2(), approximationResult, standardOutput); |
136 | 346 | } | 345 | } |
137 | 347 | 346 | ||
138 | === modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPNCTLOutputParser.java' | |||
139 | --- src/dk/aau/cs/verification/VerifyTAPN/VerifyPNCTLOutputParser.java 2020-07-13 14:30:00 +0000 | |||
140 | +++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPNCTLOutputParser.java 2023-01-23 10:20:36 +0000 | |||
141 | @@ -13,15 +13,16 @@ | |||
142 | 13 | private static final String Query_IS_NOT_SATISFIED_STRING = "Query is NOT satisfied"; | 13 | private static final String Query_IS_NOT_SATISFIED_STRING = "Query is NOT satisfied"; |
143 | 14 | private static final String Query_IS_SATISFIED_STRING = "Query is satisfied"; | 14 | private static final String Query_IS_SATISFIED_STRING = "Query is satisfied"; |
144 | 15 | 15 | ||
154 | 16 | private static final Pattern configurationsPattern = Pattern.compile("\\s*Configurations:\\s*(\\d+)\\s*"); | 16 | private static final Pattern configurationsPattern = Pattern.compile("\\s*Configurations\\s*:\\s*(\\d+)\\s*"); |
155 | 17 | private static final Pattern markingsPattern = Pattern.compile("\\s*Markings:\\s*(\\d+)\\s*"); | 17 | private static final Pattern markingsPattern = Pattern.compile("\\s*Markings\\s*:\\s*(\\d+)\\s*"); |
156 | 18 | private static final Pattern edgesPattern = Pattern.compile("\\t+Edges:\\s*(\\d+)\\s*"); | 18 | private static final Pattern edgesPattern = Pattern.compile("\\t+Edges\\s*:\\s*(\\d+)\\s*"); |
157 | 19 | 19 | ||
158 | 20 | private static final Pattern processedEdgesPattern = Pattern.compile("\\s*Processed Edges:\\s*(\\d+)\\s*"); | 20 | private static final Pattern processedEdgesPattern = Pattern.compile("\\s*Processed Edges\\s*:\\s*(\\d+)\\s*"); |
159 | 21 | private static final Pattern processedNEdgesPattern = Pattern.compile("\\s*Processed N. Edges:\\s*(\\d+)\\s*"); | 21 | private static final Pattern processedNEdgesPattern = Pattern.compile("\\s*Processed N. Edges\\s*:\\s*(\\d+)\\s*"); |
160 | 22 | private static final Pattern exploredConfigurationsPattern = Pattern.compile("\\s*Explored Configs:\\s*(\\d+)\\s*"); | 22 | private static final Pattern exploredConfigurationsPattern = Pattern.compile("\\s*Explored Configs\\s*:\\s*(\\d+)\\s*"); |
161 | 23 | 23 | ||
162 | 24 | private static final Pattern maxUsedTokensPattern = Pattern.compile("\\s*Max number of tokens found in any reachable marking:\\s*(>)?(\\d+)\\s*"); | 24 | private static final Pattern maxUsedTokensPattern = Pattern.compile("\\s*Max number of tokens found in any reachable marking\\s*:\\s*(>)?(\\d+)\\s*"); |
163 | 25 | private static final Pattern maxTokensPattern = Pattern.compile("\\s*max tokens\\s*:\\s*(>)?(\\d+)\\s*"); | ||
164 | 25 | 26 | ||
165 | 26 | public VerifyPNCTLOutputParser(int totalTokens, int extraTokens, TAPNQuery queryType) { | 27 | public VerifyPNCTLOutputParser(int totalTokens, int extraTokens, TAPNQuery queryType) { |
166 | 27 | super(totalTokens, extraTokens, queryType); | 28 | super(totalTokens, extraTokens, queryType); |
167 | @@ -76,7 +77,14 @@ | |||
168 | 76 | 77 | ||
169 | 77 | matcher = maxUsedTokensPattern.matcher(line); | 78 | matcher = maxUsedTokensPattern.matcher(line); |
170 | 78 | if(matcher.find()){ | 79 | if(matcher.find()){ |
172 | 79 | maxUsedTokens = Integer.parseInt(matcher.group(1)); | 80 | maxUsedTokens += Integer.parseInt(matcher.group(2)); |
173 | 81 | String operator = matcher.group(1) == null ? "" : matcher.group(1); | ||
174 | 82 | if(operator.equals(">")) maxUsedTokens += 1; // Indicate non-k-boundedness by encoding that an extra token was used. | ||
175 | 83 | } | ||
176 | 84 | |||
177 | 85 | matcher = maxTokensPattern.matcher(line); | ||
178 | 86 | if(matcher.find()){ | ||
179 | 87 | maxUsedTokens += Integer.parseInt(matcher.group(2)); | ||
180 | 80 | String operator = matcher.group(1) == null ? "" : matcher.group(1); | 88 | String operator = matcher.group(1) == null ? "" : matcher.group(1); |
181 | 81 | if(operator.equals(">")) maxUsedTokens += 1; // Indicate non-k-boundedness by encoding that an extra token was used. | 89 | if(operator.equals(">")) maxUsedTokens += 1; // Indicate non-k-boundedness by encoding that an extra token was used. |
182 | 82 | } | 90 | } |
183 | 83 | 91 | ||
184 | === modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java' | |||
185 | --- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java 2019-03-22 10:13:18 +0000 | |||
186 | +++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java 2023-01-23 10:20:36 +0000 | |||
187 | @@ -15,27 +15,47 @@ | |||
188 | 15 | switch(result.getQueryResult().queryType()) | 15 | switch(result.getQueryResult().queryType()) |
189 | 16 | { | 16 | { |
190 | 17 | case EF: | 17 | case EF: |
192 | 18 | if(result.isQuerySatisfied()){ | 18 | if (result.isQuerySatisfied()) { |
193 | 19 | return satisfiedIcon; | 19 | return satisfiedIcon; |
195 | 20 | }else if(!result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)){ | 20 | } else if (!result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) { |
196 | 21 | return notSatisfiedIcon; | 21 | return notSatisfiedIcon; |
197 | 22 | } | 22 | } |
198 | 23 | break; | 23 | break; |
199 | 24 | case AG: | 24 | case AG: |
202 | 25 | if(!result.isQuerySatisfied()) return notSatisfiedIcon; | 25 | if (!result.isQuerySatisfied() && result.getBound() >= result.getQueryResult().boundednessAnalysis().usedTokens()) { |
203 | 26 | else if(result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) return satisfiedIcon; | 26 | return notSatisfiedIcon; |
204 | 27 | } else if (result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) { | ||
205 | 28 | return satisfiedIcon; | ||
206 | 29 | } | ||
207 | 27 | break; | 30 | break; |
208 | 28 | case AF: | 31 | case AF: |
210 | 29 | if(!result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)){ | 32 | if (!result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) { |
211 | 30 | return notSatisfiedIcon; | 33 | return notSatisfiedIcon; |
213 | 31 | } else if(result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)){ | 34 | } else if (result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) { |
214 | 32 | return satisfiedIcon; | 35 | return satisfiedIcon; |
215 | 33 | } | 36 | } |
216 | 34 | break; | 37 | break; |
217 | 35 | case EG: | 38 | case EG: |
220 | 36 | if(result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) return satisfiedIcon; | 39 | if (result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) { |
221 | 37 | else if(!result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) return notSatisfiedIcon; | 40 | return satisfiedIcon; |
222 | 41 | } else if (!result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) { | ||
223 | 42 | return notSatisfiedIcon; | ||
224 | 43 | } | ||
225 | 38 | break; | 44 | break; |
226 | 45 | case A: | ||
227 | 46 | if (!result.isQuerySatisfied()) { | ||
228 | 47 | return notSatisfiedIcon; | ||
229 | 48 | } else if (result.isQuerySatisfied() && result.getBound() >= result.getQueryResult().boundednessAnalysis().usedTokens()) { | ||
230 | 49 | return satisfiedIcon; | ||
231 | 50 | } | ||
232 | 51 | break; | ||
233 | 52 | case E: | ||
234 | 53 | if (!result.isQuerySatisfied() && result.getBound() >= result.getQueryResult().boundednessAnalysis().usedTokens()) { | ||
235 | 54 | return notSatisfiedIcon; | ||
236 | 55 | } else if (result.isQuerySatisfied()) { | ||
237 | 56 | return satisfiedIcon; | ||
238 | 57 | } | ||
239 | 58 | break; | ||
240 | 39 | default: | 59 | default: |
241 | 40 | return null; | 60 | return null; |
242 | 41 | } | 61 | } |
243 | 42 | 62 | ||
244 | === modified file 'src/pipe/gui/RunVerification.java' | |||
245 | --- src/pipe/gui/RunVerification.java 2021-10-13 18:51:36 +0000 | |||
246 | +++ src/pipe/gui/RunVerification.java 2023-01-23 10:20:36 +0000 | |||
247 | @@ -298,11 +298,20 @@ | |||
248 | 298 | gbc.anchor = GridBagConstraints.WEST; | 298 | gbc.anchor = GridBagConstraints.WEST; |
249 | 299 | panel.add(new JLabel(toHTML(result.getResultString())), gbc); | 299 | panel.add(new JLabel(toHTML(result.getResultString())), gbc); |
250 | 300 | 300 | ||
251 | 301 | if (result.getBound() < result.getQueryResult().boundednessAnalysis().usedTokens() && | ||
252 | 302 | !result.getQueryResult().toString().toLowerCase().contains("only markings with")) { | ||
253 | 303 | gbc = new GridBagConstraints(); | ||
254 | 304 | gbc.gridx = 0; | ||
255 | 305 | gbc.gridy = 0; | ||
256 | 306 | gbc.gridwidth = 2; | ||
257 | 307 | gbc.anchor = GridBagConstraints.WEST; | ||
258 | 308 | panel.add(new JLabel("<html><br/><br/>Only markings with at most " + result.getBound() + " tokens were explored<br/><br/></html>"), gbc); | ||
259 | 309 | } | ||
260 | 310 | |||
261 | 301 | // TODO remove this when the engine outputs statistics | 311 | // TODO remove this when the engine outputs statistics |
262 | 302 | boolean isCTLQuery = result.getQueryResult().isCTL; | 312 | boolean isCTLQuery = result.getQueryResult().isCTL; |
263 | 303 | 313 | ||
264 | 304 | if(modelChecker.supportsStats() && !result.isSolvedUsingStateEquation() && !isCTLQuery){ | 314 | if(modelChecker.supportsStats() && !result.isSolvedUsingStateEquation() && !isCTLQuery){ |
265 | 305 | |||
266 | 306 | displayStats(panel, result.getStatsAsString(), modelChecker.getStatsExplanations()); | 315 | displayStats(panel, result.getStatsAsString(), modelChecker.getStatsExplanations()); |
267 | 307 | 316 | ||
268 | 308 | if(!result.getTransitionStatistics().isEmpty()){ | 317 | if(!result.getTransitionStatistics().isEmpty()){ |
269 | @@ -383,15 +392,40 @@ | |||
270 | 383 | } else if (modelChecker.supportsStats() && !result.isSolvedUsingStateEquation() && isCTLQuery){ | 392 | } else if (modelChecker.supportsStats() && !result.isSolvedUsingStateEquation() && isCTLQuery){ |
271 | 384 | displayStats(panel, result.getCTLStatsAsString(), modelChecker.getStatsExplanations()); | 393 | displayStats(panel, result.getCTLStatsAsString(), modelChecker.getStatsExplanations()); |
272 | 385 | 394 | ||
273 | 395 | if (result.getRawOutput() != null) { | ||
274 | 396 | JButton showRawQueryButton = new JButton("Show raw query results"); | ||
275 | 397 | showRawQueryButton.addActionListener(arg0 -> { | ||
276 | 398 | JOptionPane.showMessageDialog(panel, createRawQueryPanel(result.getRawOutput()), "Raw query results", JOptionPane.INFORMATION_MESSAGE); | ||
277 | 399 | }); | ||
278 | 400 | gbc = new GridBagConstraints(); | ||
279 | 401 | gbc.gridx = 0; | ||
280 | 402 | gbc.gridy = 4; | ||
281 | 403 | gbc.insets = new Insets(0,0,10,0); | ||
282 | 404 | gbc.anchor = GridBagConstraints.WEST; | ||
283 | 405 | panel.add(showRawQueryButton, gbc); | ||
284 | 406 | } | ||
285 | 386 | } | 407 | } |
286 | 387 | 408 | ||
287 | 388 | if(result.isSolvedUsingStateEquation()){ | 409 | if(result.isSolvedUsingStateEquation()){ |
288 | 389 | gbc = new GridBagConstraints(); | 410 | gbc = new GridBagConstraints(); |
289 | 390 | gbc.gridx = 0; | 411 | gbc.gridx = 0; |
291 | 391 | gbc.gridy = 6; | 412 | gbc.gridy = 4; |
292 | 392 | gbc.insets = new Insets(0,0,15,0); | 413 | gbc.insets = new Insets(0,0,15,0); |
293 | 393 | gbc.anchor = GridBagConstraints.WEST; | 414 | gbc.anchor = GridBagConstraints.WEST; |
294 | 394 | panel.add(new JLabel(toHTML("The query was resolved using state equations.")), gbc); | 415 | panel.add(new JLabel(toHTML("The query was resolved using state equations.")), gbc); |
295 | 416 | |||
296 | 417 | if (result.getRawOutput() != null) { | ||
297 | 418 | JButton showRawQueryButton = new JButton("Show raw query results"); | ||
298 | 419 | showRawQueryButton.addActionListener(arg0 -> { | ||
299 | 420 | JOptionPane.showMessageDialog(panel, createRawQueryPanel(result.getRawOutput()), "Raw query results", JOptionPane.INFORMATION_MESSAGE); | ||
300 | 421 | }); | ||
301 | 422 | gbc = new GridBagConstraints(); | ||
302 | 423 | gbc.gridx = 0; | ||
303 | 424 | gbc.gridy = 5; | ||
304 | 425 | gbc.insets = new Insets(0,0,10,0); | ||
305 | 426 | gbc.anchor = GridBagConstraints.WEST; | ||
306 | 427 | panel.add(showRawQueryButton, gbc); | ||
307 | 428 | } | ||
308 | 395 | } | 429 | } |
309 | 396 | 430 | ||
310 | 397 | gbc = new GridBagConstraints(); | 431 | gbc = new GridBagConstraints(); |
Tested and works fine.