Merge lp:~tapaal-contributor/tapaal/ltl-icon-selection-1997234 into lp:tapaal
- ltl-icon-selection-1997234
- Merge into trunk
Status: | Superseded |
---|---|
Proposed branch: | lp:~tapaal-contributor/tapaal/ltl-icon-selection-1997234 |
Merge into: | lp:tapaal |
Diff against target: |
493 lines (+145/-47) (has conflicts) 15 files modified
src/dk/aau/cs/model/tapn/TAPNQuery.java (+8/-8) 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/VerifyTAPNExporter.java (+22/-20) src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java (+28/-8) src/net/tapaal/Preferences.java (+17/-0) src/net/tapaal/TAPAAL.java (+1/-1) src/pipe/gui/GuiFrameController.java (+4/-4) src/pipe/gui/Pipe.java (+1/-1) src/pipe/gui/RunVerification.java (+10/-0) src/pipe/gui/widgets/filebrowser/NativeFileBrowser.java (+10/-0) src/pipe/gui/widgets/filebrowser/NativeFileBrowserFallback.java (+20/-0) Text conflict in src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java Text conflict in src/net/tapaal/Preferences.java Text conflict in src/pipe/gui/widgets/filebrowser/NativeFileBrowser.java Text conflict in src/pipe/gui/widgets/filebrowser/NativeFileBrowserFallback.java |
To merge this branch: | bzr merge lp:~tapaal-contributor/tapaal/ltl-icon-selection-1997234 |
Related bugs: |
Reviewer | Review Type | Date Requested | Status |
---|---|---|---|
TAPAAL Reviewers | Pending | ||
Review via email: mp+435359@code.launchpad.net |
This proposal has been superseded by a proposal from 2023-01-09.
Commit message
Considers LTL nodes when selecting icons for verification
Description of the change
- 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
Unmerged revisions
- 1179. By Lena Ernstsen
-
Fixed wrong statistics for CTL queries
- 1178. By Lena Ernstsen
-
Added 'show raw query results' button for state equation results
- 1177. By Lena Ernstsen
-
Reverted change to avoid NPE
- 1176. By Lena Ernstsen
-
Icon selection now considers LTL nodes
- 1175. By <email address hidden>
-
increased version to 3.9.3 and min version of verifypn to 4.2.2
- 1174. By <email address hidden>
-
merged in lp:~tapaal-contributor/tapaal/update-ltl-support-3.9 fixing bug #1983371
- 1173. By <email address hidden>
-
merged in lp:~tapaal-contributor/tapaal/save-file-browser-location-3.9 fixing the remembering of a location when opening a file
- 1172. By Jiri Srba
-
merged in a fix for resting LTL queries
- 1171. By Jiri Srba
-
merged in a bug fix for LTL manual edit of queries ( E .. and .. and ...) did not allow manual edit and removing the last conjunct
- 1170. By Jiri Srba
-
merged in lp:~yrke/tapaal/fix1976494 fixing a problem with copying components that contain environmental transitions
Preview Diff
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-09 11:13:50 +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,10 +24,13 @@ | |||
16 | 27 | } | 24 | } |
17 | 28 | 25 | ||
18 | 29 | public QueryType queryType(){ | 26 | public QueryType queryType(){ |
23 | 30 | if(property instanceof TCTLEFNode) return QueryType.EF; | 27 | if (property instanceof TCTLEFNode) return QueryType.EF; |
24 | 31 | else if(property instanceof TCTLEGNode) return QueryType.EG; | 28 | else if (property instanceof TCTLEGNode) return QueryType.EG; |
25 | 32 | else if(property instanceof TCTLAFNode) return QueryType.AF; | 29 | else if (property instanceof TCTLAFNode) return QueryType.AF; |
26 | 33 | else return QueryType.AG; | 30 | else if (property instanceof TCTLAGNode) return QueryType.AG; |
27 | 31 | else if (property instanceof LTLANode) return QueryType.A; | ||
28 | 32 | else if (property instanceof LTLENode) return QueryType.E; | ||
29 | 33 | else return null; | ||
30 | 34 | } | 34 | } |
31 | 35 | 35 | ||
32 | 36 | public boolean hasDeadlock(){ | 36 | public boolean hasDeadlock(){ |
33 | 37 | 37 | ||
34 | === modified file 'src/dk/aau/cs/verification/QueryResult.java' | |||
35 | --- src/dk/aau/cs/verification/QueryResult.java 2020-07-13 13:58:47 +0000 | |||
36 | +++ src/dk/aau/cs/verification/QueryResult.java 2023-01-09 11:13:50 +0000 | |||
37 | @@ -61,6 +61,8 @@ | |||
38 | 61 | || (queryType().equals(QueryType.EG)) // && !isQuerySatisfied()) | 61 | || (queryType().equals(QueryType.EG)) // && !isQuerySatisfied()) |
39 | 62 | || (queryType().equals(QueryType.AF)) // && isQuerySatisfied()) | 62 | || (queryType().equals(QueryType.AF)) // && isQuerySatisfied()) |
40 | 63 | || (queryType().equals(QueryType.AG) && isQuerySatisfied()) | 63 | || (queryType().equals(QueryType.AG) && isQuerySatisfied()) |
41 | 64 | || (queryType().equals(QueryType.A)) | ||
42 | 65 | || (queryType().equals(QueryType.E)) | ||
43 | 64 | || (hasDeadlock() && | 66 | || (hasDeadlock() && |
44 | 65 | (!isQuerySatisfied() && queryType().equals(QueryType.EF)) || | 67 | (!isQuerySatisfied() && queryType().equals(QueryType.EF)) || |
45 | 66 | (isQuerySatisfied() && queryType().equals(QueryType.AG)) | 68 | (isQuerySatisfied() && queryType().equals(QueryType.AG)) |
46 | 67 | 69 | ||
47 | === modified file 'src/dk/aau/cs/verification/QueryType.java' | |||
48 | --- src/dk/aau/cs/verification/QueryType.java 2011-05-21 13:00:05 +0000 | |||
49 | +++ src/dk/aau/cs/verification/QueryType.java 2023-01-09 11:13:50 +0000 | |||
50 | @@ -4,5 +4,7 @@ | |||
51 | 4 | EF, | 4 | EF, |
52 | 5 | EG, | 5 | EG, |
53 | 6 | AF, | 6 | AF, |
55 | 7 | AG | 7 | AG, |
56 | 8 | A, | ||
57 | 9 | E | ||
58 | 8 | } | 10 | } |
59 | 9 | 11 | ||
60 | === modified file 'src/dk/aau/cs/verification/Stats.java' | |||
61 | --- src/dk/aau/cs/verification/Stats.java 2020-07-13 13:58:47 +0000 | |||
62 | +++ src/dk/aau/cs/verification/Stats.java 2023-01-09 11:13:50 +0000 | |||
63 | @@ -137,15 +137,15 @@ | |||
64 | 137 | @Override | 137 | @Override |
65 | 138 | public String toString() { | 138 | public String toString() { |
66 | 139 | StringBuilder buffer = new StringBuilder(); | 139 | StringBuilder buffer = new StringBuilder(); |
68 | 140 | buffer.append("Discovered markings: "); | 140 | buffer.append("Discovered configurations: "); |
69 | 141 | buffer.append(discovered); | 141 | buffer.append(discovered); |
70 | 142 | buffer.append(System.getProperty("line.separator")); | 142 | buffer.append(System.getProperty("line.separator")); |
71 | 143 | 143 | ||
73 | 144 | buffer.append("Explored markings: "); | 144 | buffer.append("Explored configurations: "); |
74 | 145 | buffer.append(explored); | 145 | buffer.append(explored); |
75 | 146 | buffer.append(System.getProperty("line.separator")); | 146 | buffer.append(System.getProperty("line.separator")); |
76 | 147 | 147 | ||
78 | 148 | buffer.append("Stored markings: "); | 148 | buffer.append("Stored configurations: "); |
79 | 149 | buffer.append(stored); | 149 | buffer.append(stored); |
80 | 150 | return buffer.toString(); | 150 | return buffer.toString(); |
81 | 151 | } | 151 | } |
82 | 152 | 152 | ||
83 | === modified file 'src/dk/aau/cs/verification/VerificationResult.java' | |||
84 | --- src/dk/aau/cs/verification/VerificationResult.java 2021-10-13 18:51:36 +0000 | |||
85 | +++ src/dk/aau/cs/verification/VerificationResult.java 2023-01-09 11:13:50 +0000 | |||
86 | @@ -4,6 +4,8 @@ | |||
87 | 4 | import java.util.ArrayList; | 4 | import java.util.ArrayList; |
88 | 5 | import java.util.Comparator; | 5 | import java.util.Comparator; |
89 | 6 | import java.util.List; | 6 | import java.util.List; |
90 | 7 | import java.util.regex.Matcher; | ||
91 | 8 | import java.util.regex.Pattern; | ||
92 | 7 | 9 | ||
93 | 8 | import dk.aau.cs.model.tapn.NetworkMarking; | 10 | import dk.aau.cs.model.tapn.NetworkMarking; |
94 | 9 | import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork; | 11 | import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork; |
95 | @@ -21,6 +23,7 @@ | |||
96 | 21 | private NameMapping nameMapping; | 23 | private NameMapping nameMapping; |
97 | 22 | private TTrace secondaryTrace; | 24 | private TTrace secondaryTrace; |
98 | 23 | private boolean isSolvedUsingStateEquation = false; | 25 | private boolean isSolvedUsingStateEquation = false; |
99 | 26 | private int bound; | ||
100 | 24 | 27 | ||
101 | 25 | public boolean isQuerySatisfied() { | 28 | public boolean isQuerySatisfied() { |
102 | 26 | return queryResult.isQuerySatisfied(); | 29 | return queryResult.isQuerySatisfied(); |
103 | @@ -32,6 +35,15 @@ | |||
104 | 32 | this.verificationTime = verificationTime; | 35 | this.verificationTime = verificationTime; |
105 | 33 | this.stats = stats; | 36 | this.stats = stats; |
106 | 34 | this.rawOutput = rawOutput; | 37 | this.rawOutput = rawOutput; |
107 | 38 | |||
108 | 39 | String[] lines = rawOutput.split(System.getProperty("line.separator")); | ||
109 | 40 | for (String line : lines) { | ||
110 | 41 | Matcher matcher = Pattern.compile("\\s*-k\\s*(\\d+)\\s*").matcher(line); | ||
111 | 42 | if (matcher.find()) { | ||
112 | 43 | this.bound = Integer.parseInt(matcher.group(1)); | ||
113 | 44 | break; | ||
114 | 45 | } | ||
115 | 46 | } | ||
116 | 35 | } | 47 | } |
117 | 36 | 48 | ||
118 | 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){ |
119 | @@ -231,4 +243,8 @@ | |||
120 | 231 | public String getRawOutput() { | 243 | public String getRawOutput() { |
121 | 232 | return rawOutput; | 244 | return rawOutput; |
122 | 233 | } | 245 | } |
123 | 246 | |||
124 | 247 | public int getBound() { | ||
125 | 248 | return bound; | ||
126 | 249 | } | ||
127 | 234 | } | 250 | } |
128 | 235 | 251 | ||
129 | === modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java' | |||
130 | --- src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java 2021-07-16 20:39:22 +0000 | |||
131 | +++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java 2023-01-09 11:13:50 +0000 | |||
132 | @@ -340,7 +340,6 @@ | |||
133 | 340 | tapnTrace = parseTrace(trace, options, model, exportedModel, query, queryResult.value1()); | 340 | tapnTrace = parseTrace(trace, options, model, exportedModel, query, queryResult.value1()); |
134 | 341 | } else { | 341 | } else { |
135 | 342 | tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1()); | 342 | tapnTrace = parseTrace(errorOutput, options, model, exportedModel, query, queryResult.value1()); |
136 | 343 | |||
137 | 344 | } | 343 | } |
138 | 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); |
139 | 346 | } | 345 | } |
140 | 347 | 346 | ||
141 | === modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java' | |||
142 | --- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java 2021-12-27 08:26:55 +0000 | |||
143 | +++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java 2023-01-09 11:13:50 +0000 | |||
144 | @@ -1,33 +1,21 @@ | |||
145 | 1 | package dk.aau.cs.verification.VerifyTAPN; | 1 | package dk.aau.cs.verification.VerifyTAPN; |
146 | 2 | 2 | ||
154 | 3 | import java.io.File; | 3 | import dk.aau.cs.TCTL.visitors.CTLQueryVisitor; |
148 | 4 | import java.io.FileNotFoundException; | ||
149 | 5 | import java.io.IOException; | ||
150 | 6 | import java.io.PrintStream; | ||
151 | 7 | import java.util.Collection; | ||
152 | 8 | import java.util.List; | ||
153 | 9 | |||
155 | 10 | import dk.aau.cs.TCTL.visitors.LTLQueryVisitor; | 4 | import dk.aau.cs.TCTL.visitors.LTLQueryVisitor; |
156 | 11 | import dk.aau.cs.gui.TabContent; | 5 | import dk.aau.cs.gui.TabContent; |
157 | 6 | import dk.aau.cs.model.tapn.*; | ||
158 | 12 | import dk.aau.cs.verification.NameMapping; | 7 | import dk.aau.cs.verification.NameMapping; |
159 | 13 | import pipe.dataLayer.DataLayer; | 8 | import pipe.dataLayer.DataLayer; |
160 | 14 | import pipe.dataLayer.TAPNQuery.QueryCategory; | 9 | import pipe.dataLayer.TAPNQuery.QueryCategory; |
161 | 15 | |||
162 | 16 | import dk.aau.cs.model.tapn.TAPNQuery; | ||
163 | 17 | import dk.aau.cs.model.tapn.TimedArcPetriNet; | ||
164 | 18 | import dk.aau.cs.model.tapn.TimedInhibitorArc; | ||
165 | 19 | import dk.aau.cs.model.tapn.TimedInputArc; | ||
166 | 20 | import dk.aau.cs.model.tapn.TimedOutputArc; | ||
167 | 21 | import dk.aau.cs.model.tapn.TimedPlace; | ||
168 | 22 | import dk.aau.cs.model.tapn.TimedTransition; | ||
169 | 23 | import dk.aau.cs.model.tapn.TransportArc; | ||
170 | 24 | |||
171 | 25 | import dk.aau.cs.TCTL.visitors.CTLQueryVisitor; | ||
172 | 26 | import pipe.gui.CreateGui; | 10 | import pipe.gui.CreateGui; |
173 | 27 | import pipe.gui.graphicElements.Place; | 11 | import pipe.gui.graphicElements.Place; |
174 | 28 | import pipe.gui.graphicElements.Transition; | 12 | import pipe.gui.graphicElements.Transition; |
175 | 29 | 13 | ||
177 | 30 | import javax.xml.crypto.Data; | 14 | import java.io.File; |
178 | 15 | import java.io.FileNotFoundException; | ||
179 | 16 | import java.io.IOException; | ||
180 | 17 | import java.io.PrintStream; | ||
181 | 18 | import java.util.Collection; | ||
182 | 31 | 19 | ||
183 | 32 | public class VerifyTAPNExporter { | 20 | public class VerifyTAPNExporter { |
184 | 33 | public ExportedVerifyTAPNModel export(TimedArcPetriNet model, TAPNQuery query, TabContent.TAPNLens lens, NameMapping mapping) { | 21 | public ExportedVerifyTAPNModel export(TimedArcPetriNet model, TAPNQuery query, TabContent.TAPNLens lens, NameMapping mapping) { |
185 | @@ -140,9 +128,15 @@ | |||
186 | 140 | 128 | ||
187 | 141 | private void outputTransition(TimedTransition t, PrintStream modelStream, Collection<DataLayer> guiModels, NameMapping mapping) { | 129 | private void outputTransition(TimedTransition t, PrintStream modelStream, Collection<DataLayer> guiModels, NameMapping mapping) { |
188 | 142 | //remove the net prefix from the transition name | 130 | //remove the net prefix from the transition name |
189 | 131 | <<<<<<< TREE | ||
190 | 143 | var m = mapping.map(t.name()); | 132 | var m = mapping.map(t.name()); |
191 | 144 | 133 | ||
192 | 134 | ======= | ||
193 | 135 | var m = mapping.map(t.name()); | ||
194 | 136 | String transitionName; | ||
195 | 137 | >>>>>>> MERGE-SOURCE | ||
196 | 145 | Transition guiTransition = null; | 138 | Transition guiTransition = null; |
197 | 139 | <<<<<<< TREE | ||
198 | 146 | if (m != null) { | 140 | if (m != null) { |
199 | 147 | String transitionName = m.value2(); | 141 | String transitionName = m.value2(); |
200 | 148 | for(DataLayer guiModel : guiModels){ | 142 | for(DataLayer guiModel : guiModels){ |
201 | @@ -150,11 +144,19 @@ | |||
202 | 150 | if(guiTransition != null){ | 144 | if(guiTransition != null){ |
203 | 151 | break; | 145 | break; |
204 | 152 | } | 146 | } |
205 | 147 | ======= | ||
206 | 148 | if (m != null) { | ||
207 | 149 | transitionName = m.value2(); | ||
208 | 150 | for (DataLayer guiModel : guiModels) { | ||
209 | 151 | guiTransition = guiModel.getTransitionById(transitionName); | ||
210 | 152 | if (guiTransition != null) { | ||
211 | 153 | break; | ||
212 | 154 | } | ||
213 | 155 | >>>>>>> MERGE-SOURCE | ||
214 | 153 | } | 156 | } |
215 | 154 | } | 157 | } |
216 | 155 | 158 | ||
217 | 156 | modelStream.append("<transition "); | 159 | modelStream.append("<transition "); |
218 | 157 | |||
219 | 158 | modelStream.append("player=\"" + (t.isUncontrollable() ? "1" : "0") + "\" "); | 160 | modelStream.append("player=\"" + (t.isUncontrollable() ? "1" : "0") + "\" "); |
220 | 159 | modelStream.append("id=\"" + t.name() + "\" "); | 161 | modelStream.append("id=\"" + t.name() + "\" "); |
221 | 160 | modelStream.append("name=\"" + t.name() + "\" "); | 162 | modelStream.append("name=\"" + t.name() + "\" "); |
222 | 161 | 163 | ||
223 | === modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java' | |||
224 | --- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java 2019-03-22 10:13:18 +0000 | |||
225 | +++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java 2023-01-09 11:13:50 +0000 | |||
226 | @@ -15,27 +15,47 @@ | |||
227 | 15 | switch(result.getQueryResult().queryType()) | 15 | switch(result.getQueryResult().queryType()) |
228 | 16 | { | 16 | { |
229 | 17 | case EF: | 17 | case EF: |
231 | 18 | if(result.isQuerySatisfied()){ | 18 | if (result.isQuerySatisfied()) { |
232 | 19 | return satisfiedIcon; | 19 | return satisfiedIcon; |
234 | 20 | }else if(!result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)){ | 20 | } else if (!result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) { |
235 | 21 | return notSatisfiedIcon; | 21 | return notSatisfiedIcon; |
236 | 22 | } | 22 | } |
237 | 23 | break; | 23 | break; |
238 | 24 | case AG: | 24 | case AG: |
241 | 25 | if(!result.isQuerySatisfied()) return notSatisfiedIcon; | 25 | if (!result.isQuerySatisfied() && result.getBound() >= result.getQueryResult().boundednessAnalysis().usedTokens()) { |
242 | 26 | else if(result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) return satisfiedIcon; | 26 | return notSatisfiedIcon; |
243 | 27 | } else if (result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) { | ||
244 | 28 | return satisfiedIcon; | ||
245 | 29 | } | ||
246 | 27 | break; | 30 | break; |
247 | 28 | case AF: | 31 | case AF: |
249 | 29 | if(!result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)){ | 32 | if (!result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) { |
250 | 30 | return notSatisfiedIcon; | 33 | return notSatisfiedIcon; |
252 | 31 | } else if(result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)){ | 34 | } else if (result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) { |
253 | 32 | return satisfiedIcon; | 35 | return satisfiedIcon; |
254 | 33 | } | 36 | } |
255 | 34 | break; | 37 | break; |
256 | 35 | case EG: | 38 | case EG: |
259 | 36 | if(result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) return satisfiedIcon; | 39 | if (result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) { |
260 | 37 | else if(!result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) return notSatisfiedIcon; | 40 | return satisfiedIcon; |
261 | 41 | } else if (!result.isQuerySatisfied() && result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) { | ||
262 | 42 | return notSatisfiedIcon; | ||
263 | 43 | } | ||
264 | 38 | break; | 44 | break; |
265 | 45 | case A: | ||
266 | 46 | if (!result.isQuerySatisfied()) { | ||
267 | 47 | return notSatisfiedIcon; | ||
268 | 48 | } else if (result.isQuerySatisfied() && result.getBound() >= result.getQueryResult().boundednessAnalysis().usedTokens()) { | ||
269 | 49 | return satisfiedIcon; | ||
270 | 50 | } | ||
271 | 51 | break; | ||
272 | 52 | case E: | ||
273 | 53 | if (!result.isQuerySatisfied() && result.getBound() >= result.getQueryResult().boundednessAnalysis().usedTokens()) { | ||
274 | 54 | return notSatisfiedIcon; | ||
275 | 55 | } else if (result.isQuerySatisfied()) { | ||
276 | 56 | return satisfiedIcon; | ||
277 | 57 | } | ||
278 | 58 | break; | ||
279 | 39 | default: | 59 | default: |
280 | 40 | return null; | 60 | return null; |
281 | 41 | } | 61 | } |
282 | 42 | 62 | ||
283 | === modified file 'src/net/tapaal/Preferences.java' | |||
284 | --- src/net/tapaal/Preferences.java 2022-08-01 09:36:08 +0000 | |||
285 | +++ src/net/tapaal/Preferences.java 2023-01-09 11:13:50 +0000 | |||
286 | @@ -329,6 +329,7 @@ | |||
287 | 329 | 329 | ||
288 | 330 | return object; | 330 | return object; |
289 | 331 | } | 331 | } |
290 | 332 | <<<<<<< TREE | ||
291 | 332 | 333 | ||
292 | 333 | public void setFileBrowserLocation(String location) { | 334 | public void setFileBrowserLocation(String location) { |
293 | 334 | final String key = "file.location"; | 335 | final String key = "file.location"; |
294 | @@ -343,4 +344,20 @@ | |||
295 | 343 | public String getFileBrowserLocation() { | 344 | public String getFileBrowserLocation() { |
296 | 344 | return pref.get("file.location", null); | 345 | return pref.get("file.location", null); |
297 | 345 | } | 346 | } |
298 | 347 | ======= | ||
299 | 348 | |||
300 | 349 | public void setFileBrowserLocation(String location) { | ||
301 | 350 | final String key = "file.location"; | ||
302 | 351 | |||
303 | 352 | if (location == null || location.equals("")){ | ||
304 | 353 | pref.remove(key); | ||
305 | 354 | } else { | ||
306 | 355 | pref.put(key, location); | ||
307 | 356 | } | ||
308 | 357 | } | ||
309 | 358 | |||
310 | 359 | public String getFileBrowserLocation() { | ||
311 | 360 | return pref.get("file.location", null); | ||
312 | 361 | } | ||
313 | 362 | >>>>>>> MERGE-SOURCE | ||
314 | 346 | } | 363 | } |
315 | 347 | 364 | ||
316 | === modified file 'src/net/tapaal/TAPAAL.java' | |||
317 | --- src/net/tapaal/TAPAAL.java 2021-11-23 22:09:14 +0000 | |||
318 | +++ src/net/tapaal/TAPAAL.java 2023-01-09 11:13:50 +0000 | |||
319 | @@ -39,7 +39,7 @@ | |||
320 | 39 | public class TAPAAL { | 39 | public class TAPAAL { |
321 | 40 | 40 | ||
322 | 41 | public static final String TOOLNAME = "TAPAAL"; | 41 | public static final String TOOLNAME = "TAPAAL"; |
324 | 42 | public static final String VERSION = "DEV"; | 42 | public static final String VERSION = "3.9.3"; |
325 | 43 | 43 | ||
326 | 44 | public static String getProgramName(){ | 44 | public static String getProgramName(){ |
327 | 45 | return "" + TAPAAL.TOOLNAME + " " + TAPAAL.VERSION; | 45 | return "" + TAPAAL.TOOLNAME + " " + TAPAAL.VERSION; |
328 | 46 | 46 | ||
329 | === modified file 'src/pipe/gui/GuiFrameController.java' | |||
330 | --- src/pipe/gui/GuiFrameController.java 2021-10-17 18:41:49 +0000 | |||
331 | +++ src/pipe/gui/GuiFrameController.java 2023-01-09 11:13:50 +0000 | |||
332 | @@ -248,16 +248,16 @@ | |||
333 | 248 | buffer.append("Lasse Jacobsen, Morten Jacobsen,\nThomas S. Jacobsen, Jacob J. Jensen, Peter G. Jensen, "); | 248 | buffer.append("Lasse Jacobsen, Morten Jacobsen,\nThomas S. Jacobsen, Jacob J. Jensen, Peter G. Jensen, "); |
334 | 249 | buffer.append("Mads Johannsen,\nKenneth Y. Joergensen, Mikael H. Moeller, Christoffer Moesgaard, Kristian Morsing Pedersen,\nThomas Pedersen, Lena Said, Niels N. Samuelsen, Jiri Srba, Mathias G. Soerensen,\nJakob H. Taankvist and Peter H. Taankvist\n"); | 249 | buffer.append("Mads Johannsen,\nKenneth Y. Joergensen, Mikael H. Moeller, Christoffer Moesgaard, Kristian Morsing Pedersen,\nThomas Pedersen, Lena Said, Niels N. Samuelsen, Jiri Srba, Mathias G. Soerensen,\nJakob H. Taankvist and Peter H. Taankvist\n"); |
335 | 250 | 250 | ||
337 | 251 | buffer.append("Aalborg University 2008-2021\n\n"); | 251 | buffer.append("Aalborg University 2008-2022\n\n"); |
338 | 252 | 252 | ||
339 | 253 | buffer.append("TAPAAL Continuous Engine (verifytapn):\n"); | 253 | buffer.append("TAPAAL Continuous Engine (verifytapn):\n"); |
340 | 254 | buffer.append("Alexandre David, Lasse Jacobsen, Morten Jacobsen and Jiri Srba\n"); | 254 | buffer.append("Alexandre David, Lasse Jacobsen, Morten Jacobsen and Jiri Srba\n"); |
342 | 255 | buffer.append("Aalborg University 2011-2021\n\n"); | 255 | buffer.append("Aalborg University 2011-2022\n\n"); |
343 | 256 | 256 | ||
344 | 257 | buffer.append("TAPAAL Discrete Engine (verifydtapn):\n"); | 257 | buffer.append("TAPAAL Discrete Engine (verifydtapn):\n"); |
345 | 258 | buffer.append("Mathias Andersen, Peter G. Jensen, Heine G. Larsen, Jiri Srba,\n"); | 258 | buffer.append("Mathias Andersen, Peter G. Jensen, Heine G. Larsen, Jiri Srba,\n"); |
346 | 259 | buffer.append("Mathias G. Soerensen and Jakob H. Taankvist\n"); | 259 | buffer.append("Mathias G. Soerensen and Jakob H. Taankvist\n"); |
348 | 260 | buffer.append("Aalborg University 2012-2021\n\n"); | 260 | buffer.append("Aalborg University 2012-2022\n\n"); |
349 | 261 | 261 | ||
350 | 262 | buffer.append("TAPAAL Untimed Engine (verifypn):\n"); | 262 | buffer.append("TAPAAL Untimed Engine (verifypn):\n"); |
351 | 263 | buffer.append("Alexander Bilgram, Frederik M. Boenneland, Jakob Dyhr, Peter Fogh, "); | 263 | buffer.append("Alexander Bilgram, Frederik M. Boenneland, Jakob Dyhr, Peter Fogh, "); |
352 | @@ -265,7 +265,7 @@ | |||
353 | 265 | buffer.append("Tobias S. Jepsen, Kenneth Y. Joergensen,\nMads Johannsen, Isabella Kaufmann, "); | 265 | buffer.append("Tobias S. Jepsen, Kenneth Y. Joergensen,\nMads Johannsen, Isabella Kaufmann, "); |
354 | 266 | buffer.append("Andreas H. Klostergaard, Soeren M. Nielsen,\nThomas S. Nielsen, Lars K. Oestergaard, "); | 266 | buffer.append("Andreas H. Klostergaard, Soeren M. Nielsen,\nThomas S. Nielsen, Lars K. Oestergaard, "); |
355 | 267 | buffer.append("Samuel Pastva, Thomas Pedersen, Jiri Srba,\nPeter H. Taankvist, Nikolaj J. Ulrik and Simon M. Virenfeldt\n"); | 267 | buffer.append("Samuel Pastva, Thomas Pedersen, Jiri Srba,\nPeter H. Taankvist, Nikolaj J. Ulrik and Simon M. Virenfeldt\n"); |
357 | 268 | buffer.append("Aalborg University 2014-2021\n\n"); | 268 | buffer.append("Aalborg University 2014-2022\n\n"); |
358 | 269 | 269 | ||
359 | 270 | 270 | ||
360 | 271 | buffer.append("\n"); | 271 | buffer.append("\n"); |
361 | 272 | 272 | ||
362 | === modified file 'src/pipe/gui/Pipe.java' | |||
363 | --- src/pipe/gui/Pipe.java 2021-11-22 16:58:24 +0000 | |||
364 | +++ src/pipe/gui/Pipe.java 2023-01-09 11:13:50 +0000 | |||
365 | @@ -79,7 +79,7 @@ | |||
366 | 79 | public static final String verifytaMinRev = "4.1.19"; | 79 | public static final String verifytaMinRev = "4.1.19"; |
367 | 80 | public static final String verifytapnMinRev = "1.3.1"; | 80 | public static final String verifytapnMinRev = "1.3.1"; |
368 | 81 | public static final String verifydtapnMinRev = "3.5.0"; | 81 | public static final String verifydtapnMinRev = "3.5.0"; |
370 | 82 | public static final String verifypnMinRev = "4.2.1"; | 82 | public static final String verifypnMinRev = "4.2.2"; |
371 | 83 | public static final int AGE_DECIMAL_PRECISION = 5; | 83 | public static final int AGE_DECIMAL_PRECISION = 5; |
372 | 84 | public static final int AGE_PRECISION = AGE_DECIMAL_PRECISION + 4; | 84 | public static final int AGE_PRECISION = AGE_DECIMAL_PRECISION + 4; |
373 | 85 | 85 | ||
374 | 86 | 86 | ||
375 | === modified file 'src/pipe/gui/RunVerification.java' | |||
376 | --- src/pipe/gui/RunVerification.java 2021-10-13 18:51:36 +0000 | |||
377 | +++ src/pipe/gui/RunVerification.java 2023-01-09 11:13:50 +0000 | |||
378 | @@ -298,6 +298,16 @@ | |||
379 | 298 | gbc.anchor = GridBagConstraints.WEST; | 298 | gbc.anchor = GridBagConstraints.WEST; |
380 | 299 | panel.add(new JLabel(toHTML(result.getResultString())), gbc); | 299 | panel.add(new JLabel(toHTML(result.getResultString())), gbc); |
381 | 300 | 300 | ||
382 | 301 | if (result.getBound() < result.getQueryResult().boundednessAnalysis().usedTokens() && | ||
383 | 302 | !result.getQueryResult().toString().toLowerCase().contains("only markings with")) { | ||
384 | 303 | gbc = new GridBagConstraints(); | ||
385 | 304 | gbc.gridx = 0; | ||
386 | 305 | gbc.gridy = 0; | ||
387 | 306 | gbc.gridwidth = 2; | ||
388 | 307 | gbc.anchor = GridBagConstraints.WEST; | ||
389 | 308 | panel.add(new JLabel("<html><br/><br/>Only markings with at most " + result.getBound() + " tokens were explored<br/><br/></html>"), gbc); | ||
390 | 309 | } | ||
391 | 310 | |||
392 | 301 | // TODO remove this when the engine outputs statistics | 311 | // TODO remove this when the engine outputs statistics |
393 | 302 | boolean isCTLQuery = result.getQueryResult().isCTL; | 312 | boolean isCTLQuery = result.getQueryResult().isCTL; |
394 | 303 | 313 | ||
395 | 304 | 314 | ||
396 | === modified file 'src/pipe/gui/widgets/filebrowser/NativeFileBrowser.java' | |||
397 | --- src/pipe/gui/widgets/filebrowser/NativeFileBrowser.java 2022-08-01 09:36:08 +0000 | |||
398 | +++ src/pipe/gui/widgets/filebrowser/NativeFileBrowser.java 2023-01-09 11:13:50 +0000 | |||
399 | @@ -8,6 +8,8 @@ | |||
400 | 8 | import java.util.regex.Pattern; | 8 | import java.util.regex.Pattern; |
401 | 9 | 9 | ||
402 | 10 | import javax.swing.*; | 10 | import javax.swing.*; |
403 | 11 | |||
404 | 12 | import net.tapaal.Preferences; | ||
405 | 11 | import pipe.gui.CreateGui; | 13 | import pipe.gui.CreateGui; |
406 | 12 | import net.tapaal.Preferences; | 14 | import net.tapaal.Preferences; |
407 | 13 | 15 | ||
408 | @@ -73,7 +75,11 @@ | |||
409 | 73 | } | 75 | } |
410 | 74 | 76 | ||
411 | 75 | public File[] openFiles() { | 77 | public File[] openFiles() { |
412 | 78 | <<<<<<< TREE | ||
413 | 76 | if(specifiedPath == null) specifiedPath = Preferences.getInstance().getFileBrowserLocation(); | 79 | if(specifiedPath == null) specifiedPath = Preferences.getInstance().getFileBrowserLocation(); |
414 | 80 | ======= | ||
415 | 81 | if(specifiedPath == null) specifiedPath = Preferences.getInstance().getFileBrowserLocation();; | ||
416 | 82 | >>>>>>> MERGE-SOURCE | ||
417 | 77 | fc.setDirectory(specifiedPath); | 83 | fc.setDirectory(specifiedPath); |
418 | 78 | //This is needed for Windows | 84 | //This is needed for Windows |
419 | 79 | if(optionalExt.equals("")) fc.setFile(ext.equals("")? "":("*."+ext)); | 85 | if(optionalExt.equals("")) fc.setFile(ext.equals("")? "":("*."+ext)); |
420 | @@ -151,7 +157,11 @@ | |||
421 | 151 | //So we make a JFileChooser in which we can control it | 157 | //So we make a JFileChooser in which we can control it |
422 | 152 | if(System.getProperty("os.name").startsWith("Windows")) { | 158 | if(System.getProperty("os.name").startsWith("Windows")) { |
423 | 153 | File selectedDir = null; | 159 | File selectedDir = null; |
424 | 160 | <<<<<<< TREE | ||
425 | 154 | if (specifiedPath == null) specifiedPath = Preferences.getInstance().getFileBrowserLocation(); | 161 | if (specifiedPath == null) specifiedPath = Preferences.getInstance().getFileBrowserLocation(); |
426 | 162 | ======= | ||
427 | 163 | if (specifiedPath == null) specifiedPath = Preferences.getInstance().getFileBrowserLocation();; | ||
428 | 164 | >>>>>>> MERGE-SOURCE | ||
429 | 155 | JFileChooser c = new JFileChooser(specifiedPath); | 165 | JFileChooser c = new JFileChooser(specifiedPath); |
430 | 156 | c.setFileSelectionMode(JFileChooser.DIRECTORIES_ONLY); | 166 | c.setFileSelectionMode(JFileChooser.DIRECTORIES_ONLY); |
431 | 157 | c.setDialogTitle("Choose target directory for export"); | 167 | c.setDialogTitle("Choose target directory for export"); |
432 | 158 | 168 | ||
433 | === modified file 'src/pipe/gui/widgets/filebrowser/NativeFileBrowserFallback.java' | |||
434 | --- src/pipe/gui/widgets/filebrowser/NativeFileBrowserFallback.java 2022-08-01 09:36:08 +0000 | |||
435 | +++ src/pipe/gui/widgets/filebrowser/NativeFileBrowserFallback.java 2023-01-09 11:13:50 +0000 | |||
436 | @@ -77,7 +77,11 @@ | |||
437 | 77 | } | 77 | } |
438 | 78 | 78 | ||
439 | 79 | public File openFile() { | 79 | public File openFile() { |
440 | 80 | <<<<<<< TREE | ||
441 | 80 | if(specifiedPath == null) specifiedPath = Preferences.getInstance().getFileBrowserLocation(); | 81 | if(specifiedPath == null) specifiedPath = Preferences.getInstance().getFileBrowserLocation(); |
442 | 82 | ======= | ||
443 | 83 | if(specifiedPath == null) specifiedPath = Preferences.getInstance().getFileBrowserLocation();; | ||
444 | 84 | >>>>>>> MERGE-SOURCE | ||
445 | 81 | fc.setDirectory(specifiedPath); | 85 | fc.setDirectory(specifiedPath); |
446 | 82 | //This is needed for windows | 86 | //This is needed for windows |
447 | 83 | if(optionalExt.equals("")) fc.setFile(ext.equals("")? "":("*."+ext)); | 87 | if(optionalExt.equals("")) fc.setFile(ext.equals("")? "":("*."+ext)); |
448 | @@ -86,13 +90,21 @@ | |||
449 | 86 | fc.setVisible(true); | 90 | fc.setVisible(true); |
450 | 87 | String selectedFile = fc.getFile(); | 91 | String selectedFile = fc.getFile(); |
451 | 88 | String selectedDir = fc.getDirectory(); | 92 | String selectedDir = fc.getDirectory(); |
452 | 93 | <<<<<<< TREE | ||
453 | 89 | Preferences.getInstance().setFileBrowserLocation(selectedDir); | 94 | Preferences.getInstance().setFileBrowserLocation(selectedDir); |
454 | 95 | ======= | ||
455 | 96 | Preferences.getInstance().setFileBrowserLocation(selectedDir); | ||
456 | 97 | >>>>>>> MERGE-SOURCE | ||
457 | 90 | File file = selectedFile == null? null:new File(selectedDir + selectedFile); | 98 | File file = selectedFile == null? null:new File(selectedDir + selectedFile); |
458 | 91 | return file; | 99 | return file; |
459 | 92 | } | 100 | } |
460 | 93 | 101 | ||
461 | 94 | public File[] openFiles() { | 102 | public File[] openFiles() { |
462 | 103 | <<<<<<< TREE | ||
463 | 95 | if(specifiedPath == null) specifiedPath = Preferences.getInstance().getFileBrowserLocation(); | 104 | if(specifiedPath == null) specifiedPath = Preferences.getInstance().getFileBrowserLocation(); |
464 | 105 | ======= | ||
465 | 106 | if(specifiedPath == null) specifiedPath = Preferences.getInstance().getFileBrowserLocation();; | ||
466 | 107 | >>>>>>> MERGE-SOURCE | ||
467 | 96 | if(new File(specifiedPath).exists()) fileChooser.setCurrentDirectory(new File(specifiedPath)); | 108 | if(new File(specifiedPath).exists()) fileChooser.setCurrentDirectory(new File(specifiedPath)); |
468 | 97 | /*if (lastPath != null) { | 109 | /*if (lastPath != null) { |
469 | 98 | File path = new File(lastPath); | 110 | File path = new File(lastPath); |
470 | @@ -112,7 +124,11 @@ | |||
471 | 112 | 124 | ||
472 | 113 | 125 | ||
473 | 114 | public String saveFile(String suggestedName) { | 126 | public String saveFile(String suggestedName) { |
474 | 127 | <<<<<<< TREE | ||
475 | 115 | if(specifiedPath == null) specifiedPath = Preferences.getInstance().getFileBrowserLocation(); | 128 | if(specifiedPath == null) specifiedPath = Preferences.getInstance().getFileBrowserLocation(); |
476 | 129 | ======= | ||
477 | 130 | if(specifiedPath == null) specifiedPath = Preferences.getInstance().getFileBrowserLocation();; | ||
478 | 131 | >>>>>>> MERGE-SOURCE | ||
479 | 116 | fc.setDirectory(specifiedPath); | 132 | fc.setDirectory(specifiedPath); |
480 | 117 | fc.setFile(suggestedName + (suggestedName.endsWith("."+ext)? "":"."+ext)); | 133 | fc.setFile(suggestedName + (suggestedName.endsWith("."+ext)? "":"."+ext)); |
481 | 118 | fc.setMode(FileDialog.SAVE); | 134 | fc.setMode(FileDialog.SAVE); |
482 | @@ -165,7 +181,11 @@ | |||
483 | 165 | //So we make a JFileChooser in which we can control it | 181 | //So we make a JFileChooser in which we can control it |
484 | 166 | if(System.getProperty("os.name").startsWith("Windows")) { | 182 | if(System.getProperty("os.name").startsWith("Windows")) { |
485 | 167 | File selectedDir = null; | 183 | File selectedDir = null; |
486 | 184 | <<<<<<< TREE | ||
487 | 168 | if (specifiedPath == null) specifiedPath = Preferences.getInstance().getFileBrowserLocation(); | 185 | if (specifiedPath == null) specifiedPath = Preferences.getInstance().getFileBrowserLocation(); |
488 | 186 | ======= | ||
489 | 187 | if (specifiedPath == null) specifiedPath = Preferences.getInstance().getFileBrowserLocation();; | ||
490 | 188 | >>>>>>> MERGE-SOURCE | ||
491 | 169 | JFileChooser c = new JFileChooser(specifiedPath); | 189 | JFileChooser c = new JFileChooser(specifiedPath); |
492 | 170 | c.setFileSelectionMode(JFileChooser.DIRECTORIES_ONLY); | 190 | c.setFileSelectionMode(JFileChooser.DIRECTORIES_ONLY); |
493 | 171 | c.setDialogTitle("Choose target directory for export"); | 191 | c.setDialogTitle("Choose target directory for export"); |