Merge lp:~tapaal-contributor/tapaal/engine-option-matrix-dev into lp:tapaal

Proposed by Peter Haahr Taankvist on 2020-08-03
Status: Merged
Approved by: Jiri Srba on 2020-08-14
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
Reviewer Review Type Date Requested Status
Jiri Srba 2020-08-03 Approve on 2020-08-14
Peter Haahr Taankvist (community) Needs Resubmitting on 2020-08-13
Kenneth Yrke Jørgensen 2020-08-03 Approve on 2020-08-06
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.

To post a comment you must log in.
1075. By Peter Taankvist <email address hidden> on 2020-08-04

merge with trunk

Kenneth Yrke Jørgensen (yrke) wrote :

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.

review: Needs Fixing
1076. By Peter Taankvist <email address hidden> on 2020-08-04

merge with trunk

1077. By Peter Taankvist <email address hidden> on 2020-08-04

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 on 2020-08-05

Clean up and making members final/static

1079. By Peter Haahr Taankvist on 2020-08-05

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.

review: Needs Resubmitting
review: Approve
1080. By Peter Taankvist <email address hidden> on 2020-08-10

add game as option for the engines and merge with trunk

1081. By Peter Taankvist <email address hidden> on 2020-08-11

Merge with trunk

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.

review: Needs Fixing
1082. By Peter Taankvist <email address hidden> on 2020-08-13

Add EngineOption for EG or AF with net degree > 2

1083. By Peter Taankvist <email address hidden> on 2020-08-13

Remove debug lines

Peter Haahr Taankvist (ptaank) wrote :

Added option for a query with AF or EG and with net degree > 2.

review: Needs Resubmitting
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
...

review: Needs Fixing
1084. By Peter Haahr Taankvist on 2020-08-14

Remove more debug lines

Jiri Srba (srba) :
review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'src/dk/aau/cs/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 package dk.aau.cs.model.tapn;
6
7-import java.util.ArrayList;
8-import java.util.Arrays;
9-import java.util.List;
10+import java.util.*;
11
12 import dk.aau.cs.model.tapn.Bound.InfBound;
13 import dk.aau.cs.util.IntervalOperations;
14 import dk.aau.cs.util.Require;
15-import java.util.HashSet;
16
17 public class TimedArcPetriNet {
18 private String name;
19@@ -371,6 +368,14 @@
20 }
21 return true;
22 }
23+
24+ public int getHighestNetDegree(){
25+ int currentHighestNetDegree = 0;
26+ for (TimedTransition t : this.transitions()) {
27+ currentHighestNetDegree = Collections.max(Arrays.asList(currentHighestNetDegree, t.presetSize(), t.postsetSize()));
28+ }
29+ return currentHighestNetDegree;
30+ }
31
32 public boolean isActive() {
33 return isActive;
34
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 return composedModel.value1().isDegree2();
40 }
41
42+ public int getHighestNetDegree(){
43+ ITAPNComposer composer = new TAPNComposer(new MessengerImpl(), false);
44+ Tuple<TimedArcPetriNet,NameMapping> composedModel = composer.transformModel(this);
45+
46+ return composedModel.value1().getHighestNetDegree();
47+ }
48+
49 public boolean isSharedPlaceUsedInTemplates(SharedPlace place) {
50 for(TimedArcPetriNet tapn : this.activeTemplates()){
51 for(TimedPlace timedPlace : tapn.places()){
52
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+package pipe.gui;
58+
59+import java.util.ArrayList;
60+
61+public class EngineSupportOptions {
62+ public final String nameString;
63+ public final boolean supportFastestTrace;
64+ public final boolean supportDeadlockNetdegree2EForAG;
65+ public final boolean supportDeadlockWithInhib;
66+ public final boolean supportWeights;
67+ public final boolean supportInhibArcs;
68+ public final boolean supportUrgentTransitions;
69+ public final boolean supportEGorAF;
70+ public final boolean supportStrictNets;
71+ public final boolean supportTimedNets;
72+ public final boolean supportDeadlockNetdegreeGreaterThan2;
73+ public final boolean supportGames;
74+ public final boolean supportEGorAFWithNetDegreeGreaterThan2;
75+
76+ public final boolean[] optionsArray;
77+ public EngineSupportOptions(String nameString, boolean supportFastestTrace, boolean supportDeadlockNetdegree2EForAG, boolean supportDeadlockEGorAF, boolean supportDeadlockWithInhib,
78+ boolean supportWeights, boolean supportInhibArcs, boolean supportUrgentTransitions, boolean supportEGorAF, boolean supportStrictNets, boolean supportTimedNets,
79+ boolean supportDeadlockNetdegreeGreaterThan2, boolean supportGames, boolean supportEGorAFWithNetDegreeGreaterThan2){
80+ this.nameString = nameString;
81+ this.supportFastestTrace = supportFastestTrace;
82+ this.supportDeadlockNetdegree2EForAG = supportDeadlockNetdegree2EForAG;
83+ this.supportDeadlockWithInhib = supportDeadlockWithInhib;
84+ this.supportWeights = supportWeights;
85+ this.supportInhibArcs = supportInhibArcs;
86+ this.supportUrgentTransitions = supportUrgentTransitions;
87+ this.supportEGorAF = supportEGorAF;
88+ this.supportStrictNets = supportStrictNets;
89+ this.supportTimedNets = supportTimedNets;
90+ this.supportDeadlockNetdegreeGreaterThan2 = supportDeadlockNetdegreeGreaterThan2;
91+ this.supportGames = supportGames;
92+ this.supportEGorAFWithNetDegreeGreaterThan2 = supportEGorAFWithNetDegreeGreaterThan2;
93+ this.optionsArray = new boolean[]{supportFastestTrace, supportDeadlockNetdegree2EForAG, supportDeadlockEGorAF, supportDeadlockWithInhib,
94+ supportWeights, supportInhibArcs, supportUrgentTransitions, supportEGorAF, supportStrictNets, supportTimedNets, supportDeadlockNetdegreeGreaterThan2,
95+ supportGames, supportEGorAFWithNetDegreeGreaterThan2};
96+ }
97+
98+ public boolean areOptionsSupported(boolean[] queryOptions){
99+ for(int i = 0; i < optionsArray.length; i++){
100+ if(queryOptions[i] == true && optionsArray[i] != true){
101+ return false;
102+ }
103+ }
104+ return true;
105+ }
106+
107+}
108
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 import pipe.dataLayer.Template;
114 import pipe.dataLayer.TAPNQuery.SearchOption;
115 import pipe.dataLayer.TAPNQuery.TraceOption;
116-import pipe.gui.CreateGui;
117-import pipe.gui.MessengerImpl;
118-import pipe.gui.Verifier;
119-import pipe.gui.Zoomer;
120+import pipe.gui.*;
121 import dk.aau.cs.TCTL.StringPosition;
122 import dk.aau.cs.TCTL.TCTLAFNode;
123 import dk.aau.cs.TCTL.TCTLAGNode;
124@@ -214,22 +211,139 @@
125 private final HashMap<TimedArcPetriNet, DataLayer> guiModels;
126 private QueryConstructionUndoManager undoManager;
127 private UndoableEditSupport undoSupport;
128- private final boolean isNetDegree2;
129- private final boolean hasInhibitorArcs;
130+ private boolean isNetDegree2;
131+ private int highestNetDegree;
132+ private boolean hasInhibitorArcs;
133 private InclusionPlaces inclusionPlaces;
134 private TabContent.TAPNLens lens;
135
136- private final String name_verifyTAPN = "TAPAAL: Continous Engine (verifytapn)";
137- private final String name_COMBI = "UPPAAL: Optimized Broadcast Reduction";
138- private final String name_OPTIMIZEDSTANDARD = "UPPAAL: Optimised Standard Reduction";
139- private final String name_STANDARD = "UPPAAL: Standard Reduction";
140- private final String name_BROADCAST = "UPPAAL: Broadcast Reduction";
141- private final String name_BROADCASTDEG2 = "UPPAAL: Broadcast Degree 2 Reduction";
142- private final String name_DISCRETE = "TAPAAL: Discrete Engine (verifydtapn)";
143- private final String name_UNTIMED = "TAPAAL: Untimed Engine (verifypn)";
144+ private static final String name_verifyTAPN = "TAPAAL: Continous Engine (verifytapn)";
145+ private static final String name_COMBI = "UPPAAL: Optimized Broadcast Reduction";
146+ private static final String name_OPTIMIZEDSTANDARD = "UPPAAL: Optimised Standard Reduction";
147+ private static final String name_STANDARD = "UPPAAL: Standard Reduction";
148+ private static final String name_BROADCAST = "UPPAAL: Broadcast Reduction";
149+ private static final String name_BROADCASTDEG2 = "UPPAAL: Broadcast Degree 2 Reduction";
150+ private static final String name_DISCRETE = "TAPAAL: Discrete Engine (verifydtapn)";
151+ private static final String name_UNTIMED = "TAPAAL: Untimed Engine (verifypn)";
152 private boolean userChangedAtomicPropSelection = true;
153-
154- private TCTLAbstractProperty newProperty;
155+ //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+ //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+ private final static EngineSupportOptions verifyTAPNOptions= new EngineSupportOptions(
158+ name_verifyTAPN, //name of engine
159+ false, // support fastest trace
160+ false, // support deadlock with net degree 2 and (EF or AG)
161+ false, // support deadlock with EG or AF
162+ false, // support deadlock with inhibitor arcs
163+ false, //support weights
164+ true, //support inhibitor arcs
165+ false, // support urgent transitions
166+ false, // support EG or AF
167+ true, // support strict nets
168+ true, // support timed nets/time intervals
169+ false,// support deadlock with net degree > 2
170+ false, //support games
171+ false);//support EG or AF with net degree > 2
172+
173+ private final static EngineSupportOptions UPPAALCombiOptions= new EngineSupportOptions(
174+ name_COMBI,//name of engine
175+ false,// support fastest trace
176+ true,// support deadlock with net degree 2 and (EF or AG)
177+ false,// support deadlock with EG or AF
178+ false,// support deadlock with inhibitor arcs
179+ true, //support weights
180+ true, //support inhibitor arcs
181+ true,// support urgent transitions
182+ true,// support EG or AF
183+ true,// support strict nets
184+ true,// support timed nets/time intervals
185+ false,// support deadlock with net degree > 2
186+ false, //support games
187+ true);//support EG or AF with net degree > 2);
188+
189+ private final static EngineSupportOptions UPPAALOptimizedStandardOptions = new EngineSupportOptions(
190+ name_OPTIMIZEDSTANDARD,//name of engine
191+ false,// support fastest trace
192+ false,// support deadlock with net degree 2 and (EF or AG)
193+ false,// support deadlock with EG or AF
194+ false,// support deadlock with inhibitor arcs
195+ false, //support weights
196+ false, //support inhibitor arcs
197+ false,// support urgent transitions
198+ true,// support EG or AF
199+ true,// support strict nets
200+ true,// support timed nets/time intervals
201+ false,// support deadlock with net degree > 2
202+ false, //support games
203+ false);//support EG or AF with net degree > 2);
204+
205+ private final static EngineSupportOptions UPPAAALStandardOptions = new EngineSupportOptions(
206+ name_STANDARD,//name of engine
207+ false,// support fastest trace
208+ false,// support deadlock with net degree 2 and (EF or AG)
209+ false,// support deadlock with EG or AF
210+ false,// support deadlock with inhibitor arcs
211+ false, //support weights
212+ false, //support inhibitor arcs
213+ false,// support urgent transitions
214+ false,// support EG or AF
215+ true,// support strict nets
216+ true,// support timed nets/time intervals
217+ false,// support deadlock with net degree > 2
218+ false, //support games
219+ false);//support EG or AF with net degree > 2);
220+
221+ private final static EngineSupportOptions UPPAALBroadcastOptions = new EngineSupportOptions(
222+ name_BROADCAST,//name of engine
223+ false,// support fastest trace
224+ true,// support deadlock with net degree 2 and (EF or AG)
225+ false,// support deadlock with EG or AF
226+ false,// support deadlock with inhibitor arcs
227+ false, //support weights
228+ true, //support inhibitor arcs
229+ false,// support urgent transitions
230+ true,// support EG or AF
231+ true,// support strict nets
232+ true,// support timed nets/time intervals
233+ false,// support deadlock with net degree > 2
234+ false, //support games
235+ true);//support EG or AF with net degree > 2);
236+
237+ private final static EngineSupportOptions UPPAALBroadcastDegree2Options = new EngineSupportOptions(
238+ name_BROADCASTDEG2,//name of engine
239+ false,// support fastest trace
240+ true,// support deadlock with net degree 2 and (EF or AG)
241+ false,// support deadlock with EG or AF
242+ false,// support deadlock with inhibitor arcs
243+ false, //support weights
244+ true, //support inhibitor arcs
245+ false,// support urgent transitions
246+ true,// support EG or AF
247+ true,// support strict nets
248+ true,// support timed nets/time intervals
249+ false,// support deadlock with net degree > 2
250+ false, //support games
251+ true);//support EG or AF with net degree > 2);
252+
253+ private final static EngineSupportOptions verifyDTAPNOptions= new EngineSupportOptions(
254+ name_DISCRETE,//name of engine
255+ true,// support fastest trace
256+ true,// support deadlock with net degree 2 and (EF or AG)
257+ true,// support deadlock with EG or AF
258+ true,// support deadlock with inhibitor arcs
259+ true, //support weights
260+ true, //support inhibitor arcs
261+ true,// support urgent transitions
262+ true,// support EG or AF
263+ false,// support strict nets
264+ true,// support timed nets/time intervals
265+ true,// support deadlock with net degree > 2
266+ true, //support games
267+ true);//support EG or AF with net degree > 2);
268+
269+ //private final static EngineSupportOptions verifyPNOptions= new EngineSupportOptions(name_UNTIMED,false, true, true,true,true,true,false,true,false, false, false);
270+ private final static EngineSupportOptions[] engineSupportOptions = new EngineSupportOptions[]{verifyDTAPNOptions,verifyTAPNOptions,UPPAALCombiOptions,UPPAALOptimizedStandardOptions,UPPAAALStandardOptions,UPPAALBroadcastOptions,UPPAALBroadcastDegree2Options,/*verifyPNOptions*/};
271+
272+ private TCTLAbstractProperty newProperty;
273 private JTextField queryName;
274
275 private static Boolean advancedView = false;
276@@ -333,6 +447,7 @@
277 newProperty = queryToCreateFrom == null ? new TCTLPathPlaceHolder() : queryToCreateFrom.getProperty();
278 rootPane = me.getRootPane();
279 isNetDegree2 = tapnNetwork.isDegree2();
280+ highestNetDegree = tapnNetwork.getHighestNetDegree();
281 hasInhibitorArcs = tapnNetwork.hasInhibitorArcs();
282
283 setLayout(new GridBagLayout());
284@@ -707,12 +822,24 @@
285 ArrayList<String> options = new ArrayList<String>();
286
287 disableSymmetryUpdate = true;
288+ //The order here should be the same as in EngineSupportOptions
289+ boolean[] queryOptions = new boolean[]{fastestTraceRadioButton.isSelected(),
290+ (queryHasDeadlock() && (getQuantificationSelection().equals("E<>") || getQuantificationSelection().equals("A[]")) && highestNetDegree <= 2),
291+ (queryHasDeadlock() && (getQuantificationSelection().equals("E[]") || getQuantificationSelection().equals("A<>"))),
292+ (queryHasDeadlock() && hasInhibitorArcs),
293+ tapnNetwork.hasWeights(),
294+ hasInhibitorArcs,
295+ tapnNetwork.hasUrgentTransitions(),
296+ (getQuantificationSelection().equals("E[]") || getQuantificationSelection().equals("A<>")),
297+ //we want to know if it is strict
298+ !tapnNetwork.isNonStrict(),
299+ //we want to know if it is timed
300+ lens.isTimed(),
301+ (queryHasDeadlock() && highestNetDegree > 2),
302+ lens.isGame(),
303+ (getQuantificationSelection().equals("E[]") || getQuantificationSelection().equals("A<>")) && highestNetDegree > 2
304+ };
305
306- /* The untimed engine is disabled for now. It is used in the CTL query dialog
307- if(!fastestTraceRadioButton.isSelected() && (getQuantificationSelection().equals("E<>") || getQuantificationSelection().equals("A[]") || getQuantificationSelection().equals("")) && tapnNetwork.isUntimed()){
308- options.add(name_UNTIMED);
309- }
310- */
311
312 if(useTimeDarts != null){
313 if(hasForcedDisabledTimeDarts){
314@@ -738,68 +865,24 @@
315 useGCD.setEnabled(true);
316 }
317
318- if (lens.isGame()) {
319- if (tapnNetwork.isNonStrict()) {
320- options.add(name_DISCRETE);
321- }
322- } else if (fastestTraceRadioButton.isSelected()) {
323- options.add(name_DISCRETE);
324- } else if (queryHasDeadlock()) {
325- if (tapnNetwork.isNonStrict()) {
326- options.add(name_DISCRETE);
327- // disable timedarts if liveness and deadlock prop
328- if((getQuantificationSelection().equals("E[]") ||
329- getQuantificationSelection().equals("A<>"))){
330- if (useTimeDarts != null) {
331- if(useTimeDarts.isSelected()){
332- hasForcedDisabledTimeDarts = true;
333- }
334- useTimeDarts.setEnabled(false);
335- useTimeDarts.setSelected(false);
336+ if (tapnNetwork.isNonStrict()) {
337+ // disable timedarts if liveness and deadlock prop
338+ if((getQuantificationSelection().equals("E[]") ||
339+ getQuantificationSelection().equals("A<>"))){
340+ if (useTimeDarts != null) {
341+ if(useTimeDarts.isSelected()){
342+ hasForcedDisabledTimeDarts = true;
343 }
344- }
345- }
346- if (getQuantificationSelection().equals("E<>") || getQuantificationSelection().equals("A[]")) {
347- if (isNetDegree2 && !hasInhibitorArcs) {
348- options.add(name_COMBI);
349- if(!tapnNetwork.hasWeights() && !hasInhibitorArcs) {
350- options.addAll(Arrays.asList(name_BROADCAST, name_BROADCASTDEG2));
351- }
352- }
353- }
354-
355- } else if(tapnNetwork.hasWeights()){
356- if(tapnNetwork.isNonStrict()){
357- options.add(name_DISCRETE);
358- }
359- options.add(name_COMBI);
360- } else if(tapnNetwork.hasUrgentTransitions()){
361- if(tapnNetwork.isNonStrict()){
362- options.add(name_DISCRETE);
363- }
364- options.add(name_COMBI);
365- } else if (getQuantificationSelection().equals("E[]") || getQuantificationSelection().equals("A<>")) {
366- if(tapnNetwork.isNonStrict()){
367- options.add(name_DISCRETE);
368- }
369- options.add(name_COMBI);
370- if(isNetDegree2 && !hasInhibitorArcs)
371- options.addAll(Arrays.asList( name_BROADCAST, name_BROADCASTDEG2, name_OPTIMIZEDSTANDARD));
372- else
373- options.addAll(Arrays.asList(name_BROADCAST, name_BROADCASTDEG2));
374- } else if(tapnNetwork.hasInhibitorArcs()) {
375- options.add( name_verifyTAPN );
376- if(tapnNetwork.isNonStrict()){
377- options.add(name_DISCRETE);
378- }
379- options.addAll(Arrays.asList(name_COMBI, name_BROADCAST, name_BROADCASTDEG2 ));
380- } else {
381- options.add( name_verifyTAPN);
382- if(tapnNetwork.isNonStrict()){
383- options.add(name_DISCRETE);
384- }
385- options.addAll(Arrays.asList(name_COMBI, name_OPTIMIZEDSTANDARD, name_STANDARD, name_BROADCAST, name_BROADCASTDEG2));
386- }
387+ useTimeDarts.setEnabled(false);
388+ useTimeDarts.setSelected(false);
389+ }
390+ }
391+ }
392+ for(EngineSupportOptions engine : engineSupportOptions){
393+ if(engine.areOptionsSupported(queryOptions)){
394+ options.add(engine.nameString);
395+ }
396+ }
397
398 reductionOption.removeAllItems();
399

Subscribers

People subscribed via source and target branches