Merge lp:~tapaal-contributor/tapaal/engine-option-matrix-dev into lp:tapaal
- engine-option-matrix-dev
- Merge into trunk
Status: | Merged |
---|---|
Approved by: | Jiri Srba |
Approved revision: | 1084 |
Merged at revision: | 1083 |
Proposed branch: | lp:~tapaal-contributor/tapaal/engine-option-matrix-dev |
Merge into: | lp:tapaal |
Diff against target: |
398 lines (+232/-86) 4 files modified
src/dk/aau/cs/model/tapn/TimedArcPetriNet.java (+9/-4) src/dk/aau/cs/model/tapn/TimedArcPetriNetNetwork.java (+7/-0) src/pipe/gui/EngineSupportOptions.java (+51/-0) src/pipe/gui/widgets/QueryDialog.java (+165/-82) |
To merge this branch: | bzr merge lp:~tapaal-contributor/tapaal/engine-option-matrix-dev |
Related bugs: |
Reviewer | Review Type | Date Requested | Status |
---|---|---|---|
Jiri Srba | Approve | ||
Peter Haahr Taankvist (community) | Needs Resubmitting | ||
Kenneth Yrke Jørgensen | Approve | ||
Review via email: mp+388561@code.launchpad.net |
Commit message
Implement engine option matrix, which tells which engines are available given certain features. This replaces a large if-else tree and makes it easier to extend if the engines start supporting new features.
Description of the change
- 1075. By Peter Taankvist <email address hidden>
-
merge with trunk
Jiri Srba (srba) wrote : | # |
Kenneth, I saw your comments and it was actually me who suggested to add the comments
for the true/false values. I think they are necessary for checking and making sure that
there is not any mistake. In the future, they should get updated should there be any change.
- 1078. By Peter Haahr Taankvist
-
Clean up and making members final/static
- 1079. By Peter Haahr Taankvist
-
Use max function when finding highest degree
Peter Haahr Taankvist (ptaank) wrote : | # |
Made the suggested changes, except for 2 comments. I left some comments in the diff.
Members are now static/final and I use the max function when calculating the highest degree.
Kenneth Yrke Jørgensen (yrke) : | # |
Jiri Srba (srba) wrote : | # |
Open Fisher's protocol from examples and make the query AF true.
This branch offers UPPAAL: Optimized Standard Reduction that should
not be offered - compare with e.g. 3.6.1 released version.
Peter Haahr Taankvist (ptaank) wrote : | # |
Added option for a query with AF or EG and with net degree > 2.
Jiri Srba (srba) wrote : | # |
Please, remove the debugging information like:
4
UPPAAL: Optimized Broadcast Reduction
UPPAAL: Optimised Standard Reduction
4
UPPAAL: Standard Reduction
4
UPPAAL: Broadcast Reduction
4
UPPAAL: Broadcast Degree 2 Reduction
4
...
- 1084. By Peter Haahr Taankvist
-
Remove more debug lines
Jiri Srba (srba) : | # |
Preview Diff
1 | === modified file 'src/dk/aau/cs/model/tapn/TimedArcPetriNet.java' | |||
2 | --- src/dk/aau/cs/model/tapn/TimedArcPetriNet.java 2020-08-10 06:46:22 +0000 | |||
3 | +++ src/dk/aau/cs/model/tapn/TimedArcPetriNet.java 2020-08-14 09:31:36 +0000 | |||
4 | @@ -1,13 +1,10 @@ | |||
5 | 1 | package dk.aau.cs.model.tapn; | 1 | package dk.aau.cs.model.tapn; |
6 | 2 | 2 | ||
10 | 3 | import java.util.ArrayList; | 3 | import java.util.*; |
8 | 4 | import java.util.Arrays; | ||
9 | 5 | import java.util.List; | ||
11 | 6 | 4 | ||
12 | 7 | import dk.aau.cs.model.tapn.Bound.InfBound; | 5 | import dk.aau.cs.model.tapn.Bound.InfBound; |
13 | 8 | import dk.aau.cs.util.IntervalOperations; | 6 | import dk.aau.cs.util.IntervalOperations; |
14 | 9 | import dk.aau.cs.util.Require; | 7 | import dk.aau.cs.util.Require; |
15 | 10 | import java.util.HashSet; | ||
16 | 11 | 8 | ||
17 | 12 | public class TimedArcPetriNet { | 9 | public class TimedArcPetriNet { |
18 | 13 | private String name; | 10 | private String name; |
19 | @@ -371,6 +368,14 @@ | |||
20 | 371 | } | 368 | } |
21 | 372 | return true; | 369 | return true; |
22 | 373 | } | 370 | } |
23 | 371 | |||
24 | 372 | public int getHighestNetDegree(){ | ||
25 | 373 | int currentHighestNetDegree = 0; | ||
26 | 374 | for (TimedTransition t : this.transitions()) { | ||
27 | 375 | currentHighestNetDegree = Collections.max(Arrays.asList(currentHighestNetDegree, t.presetSize(), t.postsetSize())); | ||
28 | 376 | } | ||
29 | 377 | return currentHighestNetDegree; | ||
30 | 378 | } | ||
31 | 374 | 379 | ||
32 | 375 | public boolean isActive() { | 380 | public boolean isActive() { |
33 | 376 | return isActive; | 381 | return isActive; |
34 | 377 | 382 | ||
35 | === modified file 'src/dk/aau/cs/model/tapn/TimedArcPetriNetNetwork.java' | |||
36 | --- src/dk/aau/cs/model/tapn/TimedArcPetriNetNetwork.java 2020-08-04 06:34:24 +0000 | |||
37 | +++ src/dk/aau/cs/model/tapn/TimedArcPetriNetNetwork.java 2020-08-14 09:31:36 +0000 | |||
38 | @@ -505,6 +505,13 @@ | |||
39 | 505 | return composedModel.value1().isDegree2(); | 505 | return composedModel.value1().isDegree2(); |
40 | 506 | } | 506 | } |
41 | 507 | 507 | ||
42 | 508 | public int getHighestNetDegree(){ | ||
43 | 509 | ITAPNComposer composer = new TAPNComposer(new MessengerImpl(), false); | ||
44 | 510 | Tuple<TimedArcPetriNet,NameMapping> composedModel = composer.transformModel(this); | ||
45 | 511 | |||
46 | 512 | return composedModel.value1().getHighestNetDegree(); | ||
47 | 513 | } | ||
48 | 514 | |||
49 | 508 | public boolean isSharedPlaceUsedInTemplates(SharedPlace place) { | 515 | public boolean isSharedPlaceUsedInTemplates(SharedPlace place) { |
50 | 509 | for(TimedArcPetriNet tapn : this.activeTemplates()){ | 516 | for(TimedArcPetriNet tapn : this.activeTemplates()){ |
51 | 510 | for(TimedPlace timedPlace : tapn.places()){ | 517 | for(TimedPlace timedPlace : tapn.places()){ |
52 | 511 | 518 | ||
53 | === added file 'src/pipe/gui/EngineSupportOptions.java' | |||
54 | --- src/pipe/gui/EngineSupportOptions.java 1970-01-01 00:00:00 +0000 | |||
55 | +++ src/pipe/gui/EngineSupportOptions.java 2020-08-14 09:31:36 +0000 | |||
56 | @@ -0,0 +1,51 @@ | |||
57 | 1 | package pipe.gui; | ||
58 | 2 | |||
59 | 3 | import java.util.ArrayList; | ||
60 | 4 | |||
61 | 5 | public class EngineSupportOptions { | ||
62 | 6 | public final String nameString; | ||
63 | 7 | public final boolean supportFastestTrace; | ||
64 | 8 | public final boolean supportDeadlockNetdegree2EForAG; | ||
65 | 9 | public final boolean supportDeadlockWithInhib; | ||
66 | 10 | public final boolean supportWeights; | ||
67 | 11 | public final boolean supportInhibArcs; | ||
68 | 12 | public final boolean supportUrgentTransitions; | ||
69 | 13 | public final boolean supportEGorAF; | ||
70 | 14 | public final boolean supportStrictNets; | ||
71 | 15 | public final boolean supportTimedNets; | ||
72 | 16 | public final boolean supportDeadlockNetdegreeGreaterThan2; | ||
73 | 17 | public final boolean supportGames; | ||
74 | 18 | public final boolean supportEGorAFWithNetDegreeGreaterThan2; | ||
75 | 19 | |||
76 | 20 | public final boolean[] optionsArray; | ||
77 | 21 | public EngineSupportOptions(String nameString, boolean supportFastestTrace, boolean supportDeadlockNetdegree2EForAG, boolean supportDeadlockEGorAF, boolean supportDeadlockWithInhib, | ||
78 | 22 | boolean supportWeights, boolean supportInhibArcs, boolean supportUrgentTransitions, boolean supportEGorAF, boolean supportStrictNets, boolean supportTimedNets, | ||
79 | 23 | boolean supportDeadlockNetdegreeGreaterThan2, boolean supportGames, boolean supportEGorAFWithNetDegreeGreaterThan2){ | ||
80 | 24 | this.nameString = nameString; | ||
81 | 25 | this.supportFastestTrace = supportFastestTrace; | ||
82 | 26 | this.supportDeadlockNetdegree2EForAG = supportDeadlockNetdegree2EForAG; | ||
83 | 27 | this.supportDeadlockWithInhib = supportDeadlockWithInhib; | ||
84 | 28 | this.supportWeights = supportWeights; | ||
85 | 29 | this.supportInhibArcs = supportInhibArcs; | ||
86 | 30 | this.supportUrgentTransitions = supportUrgentTransitions; | ||
87 | 31 | this.supportEGorAF = supportEGorAF; | ||
88 | 32 | this.supportStrictNets = supportStrictNets; | ||
89 | 33 | this.supportTimedNets = supportTimedNets; | ||
90 | 34 | this.supportDeadlockNetdegreeGreaterThan2 = supportDeadlockNetdegreeGreaterThan2; | ||
91 | 35 | this.supportGames = supportGames; | ||
92 | 36 | this.supportEGorAFWithNetDegreeGreaterThan2 = supportEGorAFWithNetDegreeGreaterThan2; | ||
93 | 37 | this.optionsArray = new boolean[]{supportFastestTrace, supportDeadlockNetdegree2EForAG, supportDeadlockEGorAF, supportDeadlockWithInhib, | ||
94 | 38 | supportWeights, supportInhibArcs, supportUrgentTransitions, supportEGorAF, supportStrictNets, supportTimedNets, supportDeadlockNetdegreeGreaterThan2, | ||
95 | 39 | supportGames, supportEGorAFWithNetDegreeGreaterThan2}; | ||
96 | 40 | } | ||
97 | 41 | |||
98 | 42 | public boolean areOptionsSupported(boolean[] queryOptions){ | ||
99 | 43 | for(int i = 0; i < optionsArray.length; i++){ | ||
100 | 44 | if(queryOptions[i] == true && optionsArray[i] != true){ | ||
101 | 45 | return false; | ||
102 | 46 | } | ||
103 | 47 | } | ||
104 | 48 | return true; | ||
105 | 49 | } | ||
106 | 50 | |||
107 | 51 | } | ||
108 | 0 | 52 | ||
109 | === modified file 'src/pipe/gui/widgets/QueryDialog.java' | |||
110 | --- src/pipe/gui/widgets/QueryDialog.java 2020-08-10 06:46:22 +0000 | |||
111 | +++ src/pipe/gui/widgets/QueryDialog.java 2020-08-14 09:31:36 +0000 | |||
112 | @@ -41,10 +41,7 @@ | |||
113 | 41 | import pipe.dataLayer.Template; | 41 | import pipe.dataLayer.Template; |
114 | 42 | import pipe.dataLayer.TAPNQuery.SearchOption; | 42 | import pipe.dataLayer.TAPNQuery.SearchOption; |
115 | 43 | import pipe.dataLayer.TAPNQuery.TraceOption; | 43 | import pipe.dataLayer.TAPNQuery.TraceOption; |
120 | 44 | import pipe.gui.CreateGui; | 44 | import pipe.gui.*; |
117 | 45 | import pipe.gui.MessengerImpl; | ||
118 | 46 | import pipe.gui.Verifier; | ||
119 | 47 | import pipe.gui.Zoomer; | ||
121 | 48 | import dk.aau.cs.TCTL.StringPosition; | 45 | import dk.aau.cs.TCTL.StringPosition; |
122 | 49 | import dk.aau.cs.TCTL.TCTLAFNode; | 46 | import dk.aau.cs.TCTL.TCTLAFNode; |
123 | 50 | import dk.aau.cs.TCTL.TCTLAGNode; | 47 | import dk.aau.cs.TCTL.TCTLAGNode; |
124 | @@ -214,22 +211,139 @@ | |||
125 | 214 | private final HashMap<TimedArcPetriNet, DataLayer> guiModels; | 211 | private final HashMap<TimedArcPetriNet, DataLayer> guiModels; |
126 | 215 | private QueryConstructionUndoManager undoManager; | 212 | private QueryConstructionUndoManager undoManager; |
127 | 216 | private UndoableEditSupport undoSupport; | 213 | private UndoableEditSupport undoSupport; |
130 | 217 | private final boolean isNetDegree2; | 214 | private boolean isNetDegree2; |
131 | 218 | private final boolean hasInhibitorArcs; | 215 | private int highestNetDegree; |
132 | 216 | private boolean hasInhibitorArcs; | ||
133 | 219 | private InclusionPlaces inclusionPlaces; | 217 | private InclusionPlaces inclusionPlaces; |
134 | 220 | private TabContent.TAPNLens lens; | 218 | private TabContent.TAPNLens lens; |
135 | 221 | 219 | ||
144 | 222 | private final String name_verifyTAPN = "TAPAAL: Continous Engine (verifytapn)"; | 220 | private static final String name_verifyTAPN = "TAPAAL: Continous Engine (verifytapn)"; |
145 | 223 | private final String name_COMBI = "UPPAAL: Optimized Broadcast Reduction"; | 221 | private static final String name_COMBI = "UPPAAL: Optimized Broadcast Reduction"; |
146 | 224 | private final String name_OPTIMIZEDSTANDARD = "UPPAAL: Optimised Standard Reduction"; | 222 | private static final String name_OPTIMIZEDSTANDARD = "UPPAAL: Optimised Standard Reduction"; |
147 | 225 | private final String name_STANDARD = "UPPAAL: Standard Reduction"; | 223 | private static final String name_STANDARD = "UPPAAL: Standard Reduction"; |
148 | 226 | private final String name_BROADCAST = "UPPAAL: Broadcast Reduction"; | 224 | private static final String name_BROADCAST = "UPPAAL: Broadcast Reduction"; |
149 | 227 | private final String name_BROADCASTDEG2 = "UPPAAL: Broadcast Degree 2 Reduction"; | 225 | private static final String name_BROADCASTDEG2 = "UPPAAL: Broadcast Degree 2 Reduction"; |
150 | 228 | private final String name_DISCRETE = "TAPAAL: Discrete Engine (verifydtapn)"; | 226 | private static final String name_DISCRETE = "TAPAAL: Discrete Engine (verifydtapn)"; |
151 | 229 | private final String name_UNTIMED = "TAPAAL: Untimed Engine (verifypn)"; | 227 | private static final String name_UNTIMED = "TAPAAL: Untimed Engine (verifypn)"; |
152 | 230 | private boolean userChangedAtomicPropSelection = true; | 228 | private boolean userChangedAtomicPropSelection = true; |
155 | 231 | 229 | //In order: name of engine, support fastest trace, support deadlock with net degree 2 and (EF or AG), support deadlock with EG or AF, support deadlock with inhibitor arcs | |
156 | 232 | private TCTLAbstractProperty newProperty; | 230 | //support weights, support inhibitor arcs, support urgent transitions, support EG or AF, support strict nets, support timed nets/time intervals, support deadlock with net degree > 2 |
157 | 231 | private final static EngineSupportOptions verifyTAPNOptions= new EngineSupportOptions( | ||
158 | 232 | name_verifyTAPN, //name of engine | ||
159 | 233 | false, // support fastest trace | ||
160 | 234 | false, // support deadlock with net degree 2 and (EF or AG) | ||
161 | 235 | false, // support deadlock with EG or AF | ||
162 | 236 | false, // support deadlock with inhibitor arcs | ||
163 | 237 | false, //support weights | ||
164 | 238 | true, //support inhibitor arcs | ||
165 | 239 | false, // support urgent transitions | ||
166 | 240 | false, // support EG or AF | ||
167 | 241 | true, // support strict nets | ||
168 | 242 | true, // support timed nets/time intervals | ||
169 | 243 | false,// support deadlock with net degree > 2 | ||
170 | 244 | false, //support games | ||
171 | 245 | false);//support EG or AF with net degree > 2 | ||
172 | 246 | |||
173 | 247 | private final static EngineSupportOptions UPPAALCombiOptions= new EngineSupportOptions( | ||
174 | 248 | name_COMBI,//name of engine | ||
175 | 249 | false,// support fastest trace | ||
176 | 250 | true,// support deadlock with net degree 2 and (EF or AG) | ||
177 | 251 | false,// support deadlock with EG or AF | ||
178 | 252 | false,// support deadlock with inhibitor arcs | ||
179 | 253 | true, //support weights | ||
180 | 254 | true, //support inhibitor arcs | ||
181 | 255 | true,// support urgent transitions | ||
182 | 256 | true,// support EG or AF | ||
183 | 257 | true,// support strict nets | ||
184 | 258 | true,// support timed nets/time intervals | ||
185 | 259 | false,// support deadlock with net degree > 2 | ||
186 | 260 | false, //support games | ||
187 | 261 | true);//support EG or AF with net degree > 2); | ||
188 | 262 | |||
189 | 263 | private final static EngineSupportOptions UPPAALOptimizedStandardOptions = new EngineSupportOptions( | ||
190 | 264 | name_OPTIMIZEDSTANDARD,//name of engine | ||
191 | 265 | false,// support fastest trace | ||
192 | 266 | false,// support deadlock with net degree 2 and (EF or AG) | ||
193 | 267 | false,// support deadlock with EG or AF | ||
194 | 268 | false,// support deadlock with inhibitor arcs | ||
195 | 269 | false, //support weights | ||
196 | 270 | false, //support inhibitor arcs | ||
197 | 271 | false,// support urgent transitions | ||
198 | 272 | true,// support EG or AF | ||
199 | 273 | true,// support strict nets | ||
200 | 274 | true,// support timed nets/time intervals | ||
201 | 275 | false,// support deadlock with net degree > 2 | ||
202 | 276 | false, //support games | ||
203 | 277 | false);//support EG or AF with net degree > 2); | ||
204 | 278 | |||
205 | 279 | private final static EngineSupportOptions UPPAAALStandardOptions = new EngineSupportOptions( | ||
206 | 280 | name_STANDARD,//name of engine | ||
207 | 281 | false,// support fastest trace | ||
208 | 282 | false,// support deadlock with net degree 2 and (EF or AG) | ||
209 | 283 | false,// support deadlock with EG or AF | ||
210 | 284 | false,// support deadlock with inhibitor arcs | ||
211 | 285 | false, //support weights | ||
212 | 286 | false, //support inhibitor arcs | ||
213 | 287 | false,// support urgent transitions | ||
214 | 288 | false,// support EG or AF | ||
215 | 289 | true,// support strict nets | ||
216 | 290 | true,// support timed nets/time intervals | ||
217 | 291 | false,// support deadlock with net degree > 2 | ||
218 | 292 | false, //support games | ||
219 | 293 | false);//support EG or AF with net degree > 2); | ||
220 | 294 | |||
221 | 295 | private final static EngineSupportOptions UPPAALBroadcastOptions = new EngineSupportOptions( | ||
222 | 296 | name_BROADCAST,//name of engine | ||
223 | 297 | false,// support fastest trace | ||
224 | 298 | true,// support deadlock with net degree 2 and (EF or AG) | ||
225 | 299 | false,// support deadlock with EG or AF | ||
226 | 300 | false,// support deadlock with inhibitor arcs | ||
227 | 301 | false, //support weights | ||
228 | 302 | true, //support inhibitor arcs | ||
229 | 303 | false,// support urgent transitions | ||
230 | 304 | true,// support EG or AF | ||
231 | 305 | true,// support strict nets | ||
232 | 306 | true,// support timed nets/time intervals | ||
233 | 307 | false,// support deadlock with net degree > 2 | ||
234 | 308 | false, //support games | ||
235 | 309 | true);//support EG or AF with net degree > 2); | ||
236 | 310 | |||
237 | 311 | private final static EngineSupportOptions UPPAALBroadcastDegree2Options = new EngineSupportOptions( | ||
238 | 312 | name_BROADCASTDEG2,//name of engine | ||
239 | 313 | false,// support fastest trace | ||
240 | 314 | true,// support deadlock with net degree 2 and (EF or AG) | ||
241 | 315 | false,// support deadlock with EG or AF | ||
242 | 316 | false,// support deadlock with inhibitor arcs | ||
243 | 317 | false, //support weights | ||
244 | 318 | true, //support inhibitor arcs | ||
245 | 319 | false,// support urgent transitions | ||
246 | 320 | true,// support EG or AF | ||
247 | 321 | true,// support strict nets | ||
248 | 322 | true,// support timed nets/time intervals | ||
249 | 323 | false,// support deadlock with net degree > 2 | ||
250 | 324 | false, //support games | ||
251 | 325 | true);//support EG or AF with net degree > 2); | ||
252 | 326 | |||
253 | 327 | private final static EngineSupportOptions verifyDTAPNOptions= new EngineSupportOptions( | ||
254 | 328 | name_DISCRETE,//name of engine | ||
255 | 329 | true,// support fastest trace | ||
256 | 330 | true,// support deadlock with net degree 2 and (EF or AG) | ||
257 | 331 | true,// support deadlock with EG or AF | ||
258 | 332 | true,// support deadlock with inhibitor arcs | ||
259 | 333 | true, //support weights | ||
260 | 334 | true, //support inhibitor arcs | ||
261 | 335 | true,// support urgent transitions | ||
262 | 336 | true,// support EG or AF | ||
263 | 337 | false,// support strict nets | ||
264 | 338 | true,// support timed nets/time intervals | ||
265 | 339 | true,// support deadlock with net degree > 2 | ||
266 | 340 | true, //support games | ||
267 | 341 | true);//support EG or AF with net degree > 2); | ||
268 | 342 | |||
269 | 343 | //private final static EngineSupportOptions verifyPNOptions= new EngineSupportOptions(name_UNTIMED,false, true, true,true,true,true,false,true,false, false, false); | ||
270 | 344 | private final static EngineSupportOptions[] engineSupportOptions = new EngineSupportOptions[]{verifyDTAPNOptions,verifyTAPNOptions,UPPAALCombiOptions,UPPAALOptimizedStandardOptions,UPPAAALStandardOptions,UPPAALBroadcastOptions,UPPAALBroadcastDegree2Options,/*verifyPNOptions*/}; | ||
271 | 345 | |||
272 | 346 | private TCTLAbstractProperty newProperty; | ||
273 | 233 | private JTextField queryName; | 347 | private JTextField queryName; |
274 | 234 | 348 | ||
275 | 235 | private static Boolean advancedView = false; | 349 | private static Boolean advancedView = false; |
276 | @@ -333,6 +447,7 @@ | |||
277 | 333 | newProperty = queryToCreateFrom == null ? new TCTLPathPlaceHolder() : queryToCreateFrom.getProperty(); | 447 | newProperty = queryToCreateFrom == null ? new TCTLPathPlaceHolder() : queryToCreateFrom.getProperty(); |
278 | 334 | rootPane = me.getRootPane(); | 448 | rootPane = me.getRootPane(); |
279 | 335 | isNetDegree2 = tapnNetwork.isDegree2(); | 449 | isNetDegree2 = tapnNetwork.isDegree2(); |
280 | 450 | highestNetDegree = tapnNetwork.getHighestNetDegree(); | ||
281 | 336 | hasInhibitorArcs = tapnNetwork.hasInhibitorArcs(); | 451 | hasInhibitorArcs = tapnNetwork.hasInhibitorArcs(); |
282 | 337 | 452 | ||
283 | 338 | setLayout(new GridBagLayout()); | 453 | setLayout(new GridBagLayout()); |
284 | @@ -707,12 +822,24 @@ | |||
285 | 707 | ArrayList<String> options = new ArrayList<String>(); | 822 | ArrayList<String> options = new ArrayList<String>(); |
286 | 708 | 823 | ||
287 | 709 | disableSymmetryUpdate = true; | 824 | disableSymmetryUpdate = true; |
288 | 825 | //The order here should be the same as in EngineSupportOptions | ||
289 | 826 | boolean[] queryOptions = new boolean[]{fastestTraceRadioButton.isSelected(), | ||
290 | 827 | (queryHasDeadlock() && (getQuantificationSelection().equals("E<>") || getQuantificationSelection().equals("A[]")) && highestNetDegree <= 2), | ||
291 | 828 | (queryHasDeadlock() && (getQuantificationSelection().equals("E[]") || getQuantificationSelection().equals("A<>"))), | ||
292 | 829 | (queryHasDeadlock() && hasInhibitorArcs), | ||
293 | 830 | tapnNetwork.hasWeights(), | ||
294 | 831 | hasInhibitorArcs, | ||
295 | 832 | tapnNetwork.hasUrgentTransitions(), | ||
296 | 833 | (getQuantificationSelection().equals("E[]") || getQuantificationSelection().equals("A<>")), | ||
297 | 834 | //we want to know if it is strict | ||
298 | 835 | !tapnNetwork.isNonStrict(), | ||
299 | 836 | //we want to know if it is timed | ||
300 | 837 | lens.isTimed(), | ||
301 | 838 | (queryHasDeadlock() && highestNetDegree > 2), | ||
302 | 839 | lens.isGame(), | ||
303 | 840 | (getQuantificationSelection().equals("E[]") || getQuantificationSelection().equals("A<>")) && highestNetDegree > 2 | ||
304 | 841 | }; | ||
305 | 710 | 842 | ||
306 | 711 | /* The untimed engine is disabled for now. It is used in the CTL query dialog | ||
307 | 712 | if(!fastestTraceRadioButton.isSelected() && (getQuantificationSelection().equals("E<>") || getQuantificationSelection().equals("A[]") || getQuantificationSelection().equals("")) && tapnNetwork.isUntimed()){ | ||
308 | 713 | options.add(name_UNTIMED); | ||
309 | 714 | } | ||
310 | 715 | */ | ||
311 | 716 | 843 | ||
312 | 717 | if(useTimeDarts != null){ | 844 | if(useTimeDarts != null){ |
313 | 718 | if(hasForcedDisabledTimeDarts){ | 845 | if(hasForcedDisabledTimeDarts){ |
314 | @@ -738,68 +865,24 @@ | |||
315 | 738 | useGCD.setEnabled(true); | 865 | useGCD.setEnabled(true); |
316 | 739 | } | 866 | } |
317 | 740 | 867 | ||
336 | 741 | if (lens.isGame()) { | 868 | if (tapnNetwork.isNonStrict()) { |
337 | 742 | if (tapnNetwork.isNonStrict()) { | 869 | // disable timedarts if liveness and deadlock prop |
338 | 743 | options.add(name_DISCRETE); | 870 | if((getQuantificationSelection().equals("E[]") || |
339 | 744 | } | 871 | getQuantificationSelection().equals("A<>"))){ |
340 | 745 | } else if (fastestTraceRadioButton.isSelected()) { | 872 | if (useTimeDarts != null) { |
341 | 746 | options.add(name_DISCRETE); | 873 | if(useTimeDarts.isSelected()){ |
342 | 747 | } else if (queryHasDeadlock()) { | 874 | hasForcedDisabledTimeDarts = true; |
325 | 748 | if (tapnNetwork.isNonStrict()) { | ||
326 | 749 | options.add(name_DISCRETE); | ||
327 | 750 | // disable timedarts if liveness and deadlock prop | ||
328 | 751 | if((getQuantificationSelection().equals("E[]") || | ||
329 | 752 | getQuantificationSelection().equals("A<>"))){ | ||
330 | 753 | if (useTimeDarts != null) { | ||
331 | 754 | if(useTimeDarts.isSelected()){ | ||
332 | 755 | hasForcedDisabledTimeDarts = true; | ||
333 | 756 | } | ||
334 | 757 | useTimeDarts.setEnabled(false); | ||
335 | 758 | useTimeDarts.setSelected(false); | ||
343 | 759 | } | 875 | } |
387 | 760 | } | 876 | useTimeDarts.setEnabled(false); |
388 | 761 | } | 877 | useTimeDarts.setSelected(false); |
389 | 762 | if (getQuantificationSelection().equals("E<>") || getQuantificationSelection().equals("A[]")) { | 878 | } |
390 | 763 | if (isNetDegree2 && !hasInhibitorArcs) { | 879 | } |
391 | 764 | options.add(name_COMBI); | 880 | } |
392 | 765 | if(!tapnNetwork.hasWeights() && !hasInhibitorArcs) { | 881 | for(EngineSupportOptions engine : engineSupportOptions){ |
393 | 766 | options.addAll(Arrays.asList(name_BROADCAST, name_BROADCASTDEG2)); | 882 | if(engine.areOptionsSupported(queryOptions)){ |
394 | 767 | } | 883 | options.add(engine.nameString); |
395 | 768 | } | 884 | } |
396 | 769 | } | 885 | } |
354 | 770 | |||
355 | 771 | } else if(tapnNetwork.hasWeights()){ | ||
356 | 772 | if(tapnNetwork.isNonStrict()){ | ||
357 | 773 | options.add(name_DISCRETE); | ||
358 | 774 | } | ||
359 | 775 | options.add(name_COMBI); | ||
360 | 776 | } else if(tapnNetwork.hasUrgentTransitions()){ | ||
361 | 777 | if(tapnNetwork.isNonStrict()){ | ||
362 | 778 | options.add(name_DISCRETE); | ||
363 | 779 | } | ||
364 | 780 | options.add(name_COMBI); | ||
365 | 781 | } else if (getQuantificationSelection().equals("E[]") || getQuantificationSelection().equals("A<>")) { | ||
366 | 782 | if(tapnNetwork.isNonStrict()){ | ||
367 | 783 | options.add(name_DISCRETE); | ||
368 | 784 | } | ||
369 | 785 | options.add(name_COMBI); | ||
370 | 786 | if(isNetDegree2 && !hasInhibitorArcs) | ||
371 | 787 | options.addAll(Arrays.asList( name_BROADCAST, name_BROADCASTDEG2, name_OPTIMIZEDSTANDARD)); | ||
372 | 788 | else | ||
373 | 789 | options.addAll(Arrays.asList(name_BROADCAST, name_BROADCASTDEG2)); | ||
374 | 790 | } else if(tapnNetwork.hasInhibitorArcs()) { | ||
375 | 791 | options.add( name_verifyTAPN ); | ||
376 | 792 | if(tapnNetwork.isNonStrict()){ | ||
377 | 793 | options.add(name_DISCRETE); | ||
378 | 794 | } | ||
379 | 795 | options.addAll(Arrays.asList(name_COMBI, name_BROADCAST, name_BROADCASTDEG2 )); | ||
380 | 796 | } else { | ||
381 | 797 | options.add( name_verifyTAPN); | ||
382 | 798 | if(tapnNetwork.isNonStrict()){ | ||
383 | 799 | options.add(name_DISCRETE); | ||
384 | 800 | } | ||
385 | 801 | options.addAll(Arrays.asList(name_COMBI, name_OPTIMIZEDSTANDARD, name_STANDARD, name_BROADCAST, name_BROADCASTDEG2)); | ||
386 | 802 | } | ||
397 | 803 | 886 | ||
398 | 804 | reductionOption.removeAllItems(); | 887 | reductionOption.removeAllItems(); |
399 | 805 | 888 |
In general think it looks good, a sound beginning, but there is defenitly more work that can be done.
Added a few notes to the implementation.