Merge lp:~tapaal-contributor/tapaal/boundedness-check into lp:tapaal
- boundedness-check
- Merge into trunk
Proposed by
Lena Ernstsen
Status: | Merged | ||||
---|---|---|---|---|---|
Merged at revision: | 1140 | ||||
Proposed branch: | lp:~tapaal-contributor/tapaal/boundedness-check | ||||
Merge into: | lp:tapaal | ||||
Diff against target: |
311 lines (+118/-33) 5 files modified
src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java (+2/-1) src/pipe/gui/KBoundAnalyzer.java (+66/-15) src/pipe/gui/RunKBoundAnalysis.java (+29/-6) src/pipe/gui/RunVerification.java (+3/-2) src/pipe/gui/RunVerificationBase.java (+18/-9) |
||||
To merge this branch: | bzr merge lp:~tapaal-contributor/tapaal/boundedness-check | ||||
Related bugs: |
|
Reviewer | Review Type | Date Requested | Status |
---|---|---|---|
Jiri Srba | Needs Fixing | ||
Review via email: mp+407668@code.launchpad.net |
Commit message
Boundedness check for verifypn uses different query and minimizing extra tokens is optional
Description of the change
To post a comment you must log in.
Preview Diff
[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1 | === modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java' | |||
2 | --- src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java 2021-03-02 16:02:35 +0000 | |||
3 | +++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java 2021-08-25 10:24:16 +0000 | |||
4 | @@ -84,7 +84,8 @@ | |||
5 | 84 | result.append(" -a 10 "); | 84 | result.append(" -a 10 "); |
6 | 85 | } | 85 | } |
7 | 86 | if (this.queryReductionTime == QueryReductionTime.NoTime) { | 86 | if (this.queryReductionTime == QueryReductionTime.NoTime) { |
9 | 87 | result.append(" -q 0 "); | 87 | result.append( |
10 | 88 | " -q 0 "); | ||
11 | 88 | } else if (this.queryReductionTime == QueryReductionTime.ShortestTime) { | 89 | } else if (this.queryReductionTime == QueryReductionTime.ShortestTime) { |
12 | 89 | //Run query reduction for 1 second, to avoid conflict with -s OverApprox argument, but also still not run the verification. | 90 | //Run query reduction for 1 second, to avoid conflict with -s OverApprox argument, but also still not run the verification. |
13 | 90 | result.append(" -q 1"); | 91 | result.append(" -q 1"); |
14 | 91 | 92 | ||
15 | === modified file 'src/pipe/gui/KBoundAnalyzer.java' | |||
16 | --- src/pipe/gui/KBoundAnalyzer.java 2021-02-07 11:09:51 +0000 | |||
17 | +++ src/pipe/gui/KBoundAnalyzer.java 2021-08-25 10:24:16 +0000 | |||
18 | @@ -2,15 +2,18 @@ | |||
19 | 2 | 2 | ||
20 | 3 | import javax.swing.JSpinner; | 3 | import javax.swing.JSpinner; |
21 | 4 | 4 | ||
22 | 5 | import dk.aau.cs.TCTL.*; | ||
23 | 6 | import dk.aau.cs.model.tapn.TimedArcPetriNet; | ||
24 | 7 | import dk.aau.cs.model.tapn.TimedPlace; | ||
25 | 8 | import dk.aau.cs.util.Tuple; | ||
26 | 9 | import dk.aau.cs.verification.NameMapping; | ||
27 | 10 | import dk.aau.cs.verification.TAPNComposer; | ||
28 | 5 | import pipe.dataLayer.TAPNQuery.SearchOption; | 11 | import pipe.dataLayer.TAPNQuery.SearchOption; |
29 | 6 | import pipe.dataLayer.TAPNQuery.TraceOption; | 12 | import pipe.dataLayer.TAPNQuery.TraceOption; |
30 | 7 | import pipe.dataLayer.TAPNQuery.AlgorithmOption; | 13 | import pipe.dataLayer.TAPNQuery.AlgorithmOption; |
31 | 8 | import pipe.dataLayer.TAPNQuery.QueryCategory; | 14 | import pipe.dataLayer.TAPNQuery.QueryCategory; |
32 | 9 | import pipe.gui.widgets.RunningVerificationDialog; | 15 | import pipe.gui.widgets.RunningVerificationDialog; |
33 | 10 | import dk.aau.cs.Messenger; | 16 | import dk.aau.cs.Messenger; |
34 | 11 | import dk.aau.cs.TCTL.TCTLAGNode; | ||
35 | 12 | import dk.aau.cs.TCTL.TCTLAbstractProperty; | ||
36 | 13 | import dk.aau.cs.TCTL.TCTLTrueNode; | ||
37 | 14 | import dk.aau.cs.model.tapn.TAPNQuery; | 17 | import dk.aau.cs.model.tapn.TAPNQuery; |
38 | 15 | import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork; | 18 | import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork; |
39 | 16 | import dk.aau.cs.verification.ModelChecker; | 19 | import dk.aau.cs.verification.ModelChecker; |
40 | @@ -22,6 +25,8 @@ | |||
41 | 22 | import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNDiscreteVerification; | 25 | import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNDiscreteVerification; |
42 | 23 | import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNOptions; | 26 | import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNOptions; |
43 | 24 | 27 | ||
44 | 28 | import java.util.ArrayList; | ||
45 | 29 | |||
46 | 25 | public class KBoundAnalyzer { | 30 | public class KBoundAnalyzer { |
47 | 26 | protected TimedArcPetriNetNetwork tapnNetwork; | 31 | protected TimedArcPetriNetNetwork tapnNetwork; |
48 | 27 | protected int k; | 32 | protected int k; |
49 | @@ -40,16 +45,24 @@ | |||
50 | 40 | } | 45 | } |
51 | 41 | 46 | ||
52 | 42 | public void analyze() { | 47 | public void analyze() { |
61 | 43 | TAPNQuery query = getBoundednessQuery(); | 48 | analyze(verificationOptions()); |
54 | 44 | VerifyTAPNOptions options = verificationOptions(); | ||
55 | 45 | |||
56 | 46 | RunKBoundAnalysis analyzer = new RunKBoundAnalysis(modelChecker, messenger, spinner); | ||
57 | 47 | RunningVerificationDialog dialog = new RunningVerificationDialog(CreateGui.getApp(), analyzer); | ||
58 | 48 | |||
59 | 49 | analyzer.execute(options, tapnNetwork, query, null); | ||
60 | 50 | dialog.setVisible(true); | ||
62 | 51 | } | 49 | } |
63 | 52 | 50 | ||
64 | 51 | public void analyze(VerifyTAPNOptions options) { | ||
65 | 52 | TAPNQuery query; | ||
66 | 53 | if (modelChecker instanceof VerifyPN) { | ||
67 | 54 | query = getPNBoundednessQuery(); | ||
68 | 55 | } else { | ||
69 | 56 | query = getBoundednessQuery(); | ||
70 | 57 | } | ||
71 | 58 | |||
72 | 59 | RunKBoundAnalysis analyzer = new RunKBoundAnalysis(modelChecker, messenger, spinner); | ||
73 | 60 | RunningVerificationDialog dialog = new RunningVerificationDialog(CreateGui.getApp(), analyzer); | ||
74 | 61 | |||
75 | 62 | analyzer.execute(options, tapnNetwork, query, null); | ||
76 | 63 | dialog.setVisible(true); | ||
77 | 64 | } | ||
78 | 65 | |||
79 | 53 | protected VerifyTAPNOptions verificationOptions() { | 66 | protected VerifyTAPNOptions verificationOptions() { |
80 | 54 | if(modelChecker instanceof VerifyPN){ | 67 | if(modelChecker instanceof VerifyPN){ |
81 | 55 | return new VerifyPNOptions(k, TraceOption.NONE, SearchOption.BFS, false, ModelReduction.BOUNDPRESERVING, false, false, 1, QueryCategory.Default, AlgorithmOption.CERTAIN_ZERO, false, pipe.dataLayer.TAPNQuery.QueryReductionTime.UnlimitedTime, false, null, false); | 68 | return new VerifyPNOptions(k, TraceOption.NONE, SearchOption.BFS, false, ModelReduction.BOUNDPRESERVING, false, false, 1, QueryCategory.Default, AlgorithmOption.CERTAIN_ZERO, false, pipe.dataLayer.TAPNQuery.QueryReductionTime.UnlimitedTime, false, null, false); |
82 | @@ -62,10 +75,48 @@ | |||
83 | 62 | } | 75 | } |
84 | 63 | 76 | ||
85 | 64 | protected TAPNQuery getBoundednessQuery() { | 77 | protected TAPNQuery getBoundednessQuery() { |
90 | 65 | TCTLAbstractProperty property = null; | 78 | TCTLAbstractProperty property = new TCTLAGNode(new TCTLTrueNode()); |
87 | 66 | |||
88 | 67 | property = new TCTLAGNode(new TCTLTrueNode()); | ||
89 | 68 | |||
91 | 69 | return new TAPNQuery(property, k); | 79 | return new TAPNQuery(property, k); |
92 | 70 | } | 80 | } |
93 | 81 | |||
94 | 82 | protected TAPNQuery getPNBoundednessQuery() { | ||
95 | 83 | int totalTokens = k + tapnNetwork.marking().size(); | ||
96 | 84 | |||
97 | 85 | TCTLAtomicPropositionNode child = new TCTLAtomicPropositionNode(new TCTLTermListNode(getFactors()), "<=", new TCTLConstNode(totalTokens)); | ||
98 | 86 | TCTLAbstractProperty property = new TCTLAGNode(child); | ||
99 | 87 | |||
100 | 88 | TAPNQuery query = new TAPNQuery(property, k); | ||
101 | 89 | query.setCategory(QueryCategory.CTL); | ||
102 | 90 | |||
103 | 91 | return query; | ||
104 | 92 | } | ||
105 | 93 | |||
106 | 94 | private ArrayList<TCTLAbstractStateProperty> getFactors() { | ||
107 | 95 | TimedArcPetriNet net = mergeNetComponents(); | ||
108 | 96 | ArrayList<TCTLAbstractStateProperty> factors = new ArrayList<>(); | ||
109 | 97 | |||
110 | 98 | tapnNetwork.sharedPlaces().forEach(o -> { | ||
111 | 99 | if (net.getPlaceByName(o.name()) != null && !net.getPlaceByName(o.name()).name().contains("Shared_")) { | ||
112 | 100 | net.getPlaceByName(o.name()).setName("Shared_" + o.name()); | ||
113 | 101 | } | ||
114 | 102 | }); | ||
115 | 103 | tapnNetwork.allTemplates().forEach(o -> o.places().forEach(x -> { | ||
116 | 104 | if (net.getPlaceByName(x.name()) != null) net.getPlaceByName(x.name()).setName(o.name() + "_" + x.name()); | ||
117 | 105 | })); | ||
118 | 106 | |||
119 | 107 | for (TimedPlace place : net.places()) { | ||
120 | 108 | factors.add(new TCTLPlaceNode(place.name())); | ||
121 | 109 | factors.add(new AritmeticOperator("+")); | ||
122 | 110 | } | ||
123 | 111 | if (factors.get(factors.size()-1) instanceof AritmeticOperator) factors.remove(factors.size()-1); | ||
124 | 112 | |||
125 | 113 | return factors; | ||
126 | 114 | } | ||
127 | 115 | |||
128 | 116 | private TimedArcPetriNet mergeNetComponents() { | ||
129 | 117 | TAPNComposer composer = new TAPNComposer(new MessengerImpl(), CreateGui.getCurrentTab().getGuiModels(), true, true); | ||
130 | 118 | Tuple<TimedArcPetriNet, NameMapping> transformedModel = composer.transformModel(tapnNetwork); | ||
131 | 119 | |||
132 | 120 | return transformedModel.value1(); | ||
133 | 121 | } | ||
134 | 71 | } | 122 | } |
135 | 72 | 123 | ||
136 | === modified file 'src/pipe/gui/RunKBoundAnalysis.java' | |||
137 | --- src/pipe/gui/RunKBoundAnalysis.java 2020-05-27 12:59:31 +0000 | |||
138 | +++ src/pipe/gui/RunKBoundAnalysis.java 2021-08-25 10:24:16 +0000 | |||
139 | @@ -4,33 +4,47 @@ | |||
140 | 4 | import javax.swing.JSpinner; | 4 | import javax.swing.JSpinner; |
141 | 5 | 5 | ||
142 | 6 | import dk.aau.cs.Messenger; | 6 | import dk.aau.cs.Messenger; |
143 | 7 | import dk.aau.cs.verification.VerifyTAPN.VerifyPN; | ||
144 | 7 | import net.tapaal.resourcemanager.ResourceManager; | 8 | import net.tapaal.resourcemanager.ResourceManager; |
145 | 8 | import dk.aau.cs.model.tapn.simulation.TAPNNetworkTrace; | 9 | import dk.aau.cs.model.tapn.simulation.TAPNNetworkTrace; |
146 | 9 | import dk.aau.cs.verification.Boundedness; | 10 | import dk.aau.cs.verification.Boundedness; |
147 | 10 | import dk.aau.cs.verification.ModelChecker; | 11 | import dk.aau.cs.verification.ModelChecker; |
148 | 11 | import dk.aau.cs.verification.VerificationResult; | 12 | import dk.aau.cs.verification.VerificationResult; |
149 | 12 | 13 | ||
150 | 14 | import java.util.ArrayList; | ||
151 | 15 | |||
152 | 13 | public class RunKBoundAnalysis extends RunVerificationBase { | 16 | public class RunKBoundAnalysis extends RunVerificationBase { |
153 | 14 | 17 | ||
154 | 15 | private final JSpinner spinner; | 18 | private final JSpinner spinner; |
155 | 16 | 19 | ||
156 | 17 | public RunKBoundAnalysis(ModelChecker modelChecker, Messenger messenger,JSpinner spinner) { | 20 | public RunKBoundAnalysis(ModelChecker modelChecker, Messenger messenger,JSpinner spinner) { |
158 | 18 | super(modelChecker, messenger); | 21 | super(modelChecker, messenger, spinner); |
159 | 19 | this.spinner = spinner; | 22 | this.spinner = spinner; |
160 | 20 | } | 23 | } |
161 | 21 | 24 | ||
162 | 22 | @Override | 25 | @Override |
164 | 23 | protected void showResult(VerificationResult<TAPNNetworkTrace> result) { | 26 | protected boolean showResult(VerificationResult<TAPNNetworkTrace> result) { |
165 | 24 | if(result != null && !result.error()) { | 27 | if(result != null && !result.error()) { |
166 | 25 | if (!result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) { | 28 | if (!result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) { |
167 | 26 | JOptionPane.showMessageDialog(CreateGui.getApp(), | 29 | JOptionPane.showMessageDialog(CreateGui.getApp(), |
168 | 27 | getAnswerNotBoundedString(), "Analysis Result", | 30 | getAnswerNotBoundedString(), "Analysis Result", |
169 | 28 | JOptionPane.INFORMATION_MESSAGE); | 31 | JOptionPane.INFORMATION_MESSAGE); |
170 | 29 | } else { | 32 | } else { |
175 | 30 | spinner.setValue(result.getQueryResult().boundednessAnalysis().usedTokens() - result.getQueryResult().boundednessAnalysis().tokensInNet()); | 33 | if (modelChecker instanceof VerifyPN && !result.getRawOutput().contains("max tokens:")) { |
176 | 31 | JOptionPane.showMessageDialog(CreateGui.getApp(), | 34 | Object[] options = {"Ok", "Minimize extra tokens"}; |
177 | 32 | getAnswerBoundedString(), "Analysis Result", | 35 | int answer = JOptionPane.showOptionDialog(CreateGui.getApp(), |
178 | 33 | JOptionPane.INFORMATION_MESSAGE, ResourceManager.satisfiedIcon()); | 36 | getPNAnswerBoundedString(), "Analysis Result,", |
179 | 37 | JOptionPane.OK_CANCEL_OPTION, JOptionPane.INFORMATION_MESSAGE, | ||
180 | 38 | ResourceManager.satisfiedIcon(), options, JOptionPane.OK_OPTION); | ||
181 | 39 | return answer != JOptionPane.OK_OPTION; | ||
182 | 40 | } else if (modelChecker instanceof VerifyPN) { | ||
183 | 41 | spinner.setValue(result.getQueryResult().boundednessAnalysis().usedTokens() - result.getQueryResult().boundednessAnalysis().tokensInNet()); | ||
184 | 42 | } else { | ||
185 | 43 | spinner.setValue(result.getQueryResult().boundednessAnalysis().usedTokens() - result.getQueryResult().boundednessAnalysis().tokensInNet()); | ||
186 | 44 | JOptionPane.showMessageDialog(CreateGui.getApp(), | ||
187 | 45 | getAnswerBoundedString(), "Analysis Result", | ||
188 | 46 | JOptionPane.INFORMATION_MESSAGE, ResourceManager.satisfiedIcon()); | ||
189 | 47 | } | ||
190 | 34 | } | 48 | } |
191 | 35 | } else { | 49 | } else { |
192 | 36 | String message = "An error occured during the verification." + | 50 | String message = "An error occured during the verification." + |
193 | @@ -40,6 +54,7 @@ | |||
194 | 40 | 54 | ||
195 | 41 | messenger.displayWrappedErrorMessage(message,"Error during verification"); | 55 | messenger.displayWrappedErrorMessage(message,"Error during verification"); |
196 | 42 | } | 56 | } |
197 | 57 | return false; | ||
198 | 43 | } | 58 | } |
199 | 44 | 59 | ||
200 | 45 | protected String getAnswerNotBoundedString() { | 60 | protected String getAnswerNotBoundedString() { |
201 | @@ -58,4 +73,12 @@ | |||
202 | 58 | + "The number of extra tokens was automatically lowered to the\n" | 73 | + "The number of extra tokens was automatically lowered to the\n" |
203 | 59 | + "minimum number of tokens needed for an exact analysis."; | 74 | + "minimum number of tokens needed for an exact analysis."; |
204 | 60 | } | 75 | } |
205 | 76 | |||
206 | 77 | protected String getPNAnswerBoundedString() { | ||
207 | 78 | return "The net with the specified extra number of tokens is bounded.\n\n" | ||
208 | 79 | + "This means that the analysis will be exact and always give \n" | ||
209 | 80 | + "the correct answer.\n\n" | ||
210 | 81 | + "The number of extra tokens can be lowered to the minimum number\n" | ||
211 | 82 | + "of tokens needed for an exact analysis."; | ||
212 | 83 | } | ||
213 | 61 | } | 84 | } |
214 | 62 | 85 | ||
215 | === modified file 'src/pipe/gui/RunVerification.java' | |||
216 | --- src/pipe/gui/RunVerification.java 2021-02-22 22:56:50 +0000 | |||
217 | +++ src/pipe/gui/RunVerification.java 2021-08-25 10:24:16 +0000 | |||
218 | @@ -31,7 +31,7 @@ | |||
219 | 31 | private final IconSelector iconSelector; | 31 | private final IconSelector iconSelector; |
220 | 32 | private final VerificationCallback callback; | 32 | private final VerificationCallback callback; |
221 | 33 | public RunVerification(ModelChecker modelChecker, IconSelector selector, Messenger messenger, VerificationCallback callback, String reducedNetFilePath, boolean reduceNetOnly) { | 33 | public RunVerification(ModelChecker modelChecker, IconSelector selector, Messenger messenger, VerificationCallback callback, String reducedNetFilePath, boolean reduceNetOnly) { |
223 | 34 | super(modelChecker, messenger, reducedNetFilePath, reduceNetOnly); | 34 | super(modelChecker, messenger, reducedNetFilePath, reduceNetOnly, null); |
224 | 35 | iconSelector = selector; | 35 | iconSelector = selector; |
225 | 36 | this.callback = callback; | 36 | this.callback = callback; |
226 | 37 | } | 37 | } |
227 | @@ -45,7 +45,7 @@ | |||
228 | 45 | } | 45 | } |
229 | 46 | 46 | ||
230 | 47 | @Override | 47 | @Override |
232 | 48 | protected void showResult(VerificationResult<TAPNNetworkTrace> result) { | 48 | protected boolean showResult(VerificationResult<TAPNNetworkTrace> result) { |
233 | 49 | if (result != null && !result.error()) { | 49 | if (result != null && !result.error()) { |
234 | 50 | if(callback != null){ | 50 | if(callback != null){ |
235 | 51 | callback.run(result); | 51 | callback.run(result); |
236 | @@ -98,6 +98,7 @@ | |||
237 | 98 | messenger.displayWrappedErrorMessage(message,"Error during verification"); | 98 | messenger.displayWrappedErrorMessage(message,"Error during verification"); |
238 | 99 | 99 | ||
239 | 100 | } | 100 | } |
240 | 101 | return false; | ||
241 | 101 | } | 102 | } |
242 | 102 | 103 | ||
243 | 103 | private String toHTML(String string){ | 104 | private String toHTML(String string){ |
244 | 104 | 105 | ||
245 | === modified file 'src/pipe/gui/RunVerificationBase.java' | |||
246 | --- src/pipe/gui/RunVerificationBase.java 2021-02-07 11:09:51 +0000 | |||
247 | +++ src/pipe/gui/RunVerificationBase.java 2021-08-25 10:24:16 +0000 | |||
248 | @@ -3,9 +3,9 @@ | |||
249 | 3 | import java.io.File; | 3 | import java.io.File; |
250 | 4 | import java.util.concurrent.ExecutionException; | 4 | import java.util.concurrent.ExecutionException; |
251 | 5 | 5 | ||
254 | 6 | import javax.swing.SwingUtilities; | 6 | import javax.swing.*; |
253 | 7 | import javax.swing.SwingWorker; | ||
255 | 8 | 7 | ||
256 | 8 | import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNOptions; | ||
257 | 9 | import pipe.dataLayer.TAPNQuery.SearchOption; | 9 | import pipe.dataLayer.TAPNQuery.SearchOption; |
258 | 10 | import dk.aau.cs.Messenger; | 10 | import dk.aau.cs.Messenger; |
259 | 11 | import dk.aau.cs.TCTL.visitors.RenameAllPlacesVisitor; | 11 | import dk.aau.cs.TCTL.visitors.RenameAllPlacesVisitor; |
260 | @@ -43,20 +43,25 @@ | |||
261 | 43 | protected String reducedNetFilePath; | 43 | protected String reducedNetFilePath; |
262 | 44 | protected boolean reduceNetOnly; | 44 | protected boolean reduceNetOnly; |
263 | 45 | protected boolean reducedNetOpened = false; | 45 | protected boolean reducedNetOpened = false; |
266 | 46 | 46 | protected JSpinner spinner; | |
267 | 47 | 47 | ||
268 | 48 | protected Messenger messenger; | 48 | protected Messenger messenger; |
269 | 49 | 49 | ||
271 | 50 | public RunVerificationBase(ModelChecker modelChecker, Messenger messenger, String reducedNetFilePath, boolean reduceNetOnly) { | 50 | public RunVerificationBase(ModelChecker modelChecker, Messenger messenger, String reducedNetFilePath, boolean reduceNetOnly, JSpinner spinner) { |
272 | 51 | super(); | 51 | super(); |
273 | 52 | this.modelChecker = modelChecker; | 52 | this.modelChecker = modelChecker; |
274 | 53 | this.messenger = messenger; | 53 | this.messenger = messenger; |
275 | 54 | this.reducedNetFilePath = reducedNetFilePath; | 54 | this.reducedNetFilePath = reducedNetFilePath; |
276 | 55 | this.reduceNetOnly = reduceNetOnly; | 55 | this.reduceNetOnly = reduceNetOnly; |
278 | 56 | } | 56 | this.spinner = spinner; |
279 | 57 | } | ||
280 | 57 | 58 | ||
281 | 58 | public RunVerificationBase(ModelChecker modelChecker, Messenger messenger) { | 59 | public RunVerificationBase(ModelChecker modelChecker, Messenger messenger) { |
283 | 59 | this(modelChecker, messenger, null, false); | 60 | this(modelChecker, messenger, null, false, null); |
284 | 61 | } | ||
285 | 62 | |||
286 | 63 | public RunVerificationBase(ModelChecker modelChecker, Messenger messenger, JSpinner spinner) { | ||
287 | 64 | this(modelChecker, messenger, null, false, spinner); | ||
288 | 60 | } | 65 | } |
289 | 61 | 66 | ||
290 | 62 | 67 | ||
291 | @@ -212,8 +217,12 @@ | |||
292 | 212 | return; | 217 | return; |
293 | 213 | } | 218 | } |
294 | 214 | firePropertyChange("state", StateValue.PENDING, StateValue.DONE); | 219 | firePropertyChange("state", StateValue.PENDING, StateValue.DONE); |
295 | 215 | showResult(result); | ||
296 | 216 | 220 | ||
297 | 221 | if (showResult(result) && spinner != null) { | ||
298 | 222 | options = new VerifyPNOptions(options.extraTokens(), pipe.dataLayer.TAPNQuery.TraceOption.NONE, SearchOption.BFS, false, ModelReduction.BOUNDPRESERVING, false, false, 1, pipe.dataLayer.TAPNQuery.QueryCategory.Default, pipe.dataLayer.TAPNQuery.AlgorithmOption.CERTAIN_ZERO, false, pipe.dataLayer.TAPNQuery.QueryReductionTime.NoTime, false, null, false); | ||
299 | 223 | KBoundAnalyzer optimizer = new KBoundAnalyzer(model, options.extraTokens(), modelChecker, new MessengerImpl(), spinner); | ||
300 | 224 | optimizer.analyze((VerifyTAPNOptions) options); | ||
301 | 225 | } | ||
302 | 217 | } else { | 226 | } else { |
303 | 218 | modelChecker.kill(); | 227 | modelChecker.kill(); |
304 | 219 | messenger.displayInfoMessage("Verification was interrupted by the user. No result found!", "Verification Cancelled"); | 228 | messenger.displayInfoMessage("Verification was interrupted by the user. No result found!", "Verification Cancelled"); |
305 | @@ -231,5 +240,5 @@ | |||
306 | 231 | }); | 240 | }); |
307 | 232 | } | 241 | } |
308 | 233 | 242 | ||
310 | 234 | protected abstract void showResult(VerificationResult<TAPNNetworkTrace> result); | 243 | protected abstract boolean showResult(VerificationResult<TAPNNetworkTrace> result); |
311 | 235 | } | 244 | } |
Open the game-harddisk example and check for boundedness, it is broken.