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

[Peter Haahr Taankvist]

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.

[lp:~tapaal-contributor/tapaal/engine-option-matrix-dev]

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

merge with trunk

[Kenneth Yrke Jørgensen (yrke)]

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

[lp:~tapaal-contributor/tapaal/engine-option-matrix-dev]

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)]

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.

[lp:~tapaal-contributor/tapaal/engine-option-matrix-dev]

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)]

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: Resubmit

[Kenneth Yrke Jørgensen (yrke)]

review: Approve

[lp:~tapaal-contributor/tapaal/engine-option-matrix-dev]

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)]

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

[lp:~tapaal-contributor/tapaal/engine-option-matrix-dev]

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)]

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

review: Resubmit

[Jiri Srba (srba)]

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

[lp:~tapaal-contributor/tapaal/engine-option-matrix-dev]

1084. By Peter Haahr Taankvist on 2020-08-14

Remove more debug lines

[Jiri Srba (srba)]

review: Approve

=== modified file 'src/dk/aau/cs/model/tapn/TimedArcPetriNet.java'
--- src/dk/aau/cs/model/tapn/TimedArcPetriNet.java	2020-08-10 06:46:22 +0000
+++ src/dk/aau/cs/model/tapn/TimedArcPetriNet.java	2020-08-14 09:31:36 +0000
@@ -1,13 +1,10 @@
 package dk.aau.cs.model.tapn;
 
-import java.util.ArrayList;
-import java.util.Arrays;
-import java.util.List;
+import java.util.*;
 
 import dk.aau.cs.model.tapn.Bound.InfBound;
 import dk.aau.cs.util.IntervalOperations;
 import dk.aau.cs.util.Require;
-import java.util.HashSet;
 
 public class TimedArcPetriNet {
 	private String name;
@@ -371,6 +368,14 @@
 		}
 		return true;
 	}
+
+    public int getHighestNetDegree(){
+	    int currentHighestNetDegree = 0;
+        for (TimedTransition t : this.transitions()) {
+            currentHighestNetDegree = Collections.max(Arrays.asList(currentHighestNetDegree, t.presetSize(), t.postsetSize()));
+        }
+        return currentHighestNetDegree;
+    }
 	
 	public boolean isActive() {
 		return isActive;

=== modified file 'src/dk/aau/cs/model/tapn/TimedArcPetriNetNetwork.java'
--- src/dk/aau/cs/model/tapn/TimedArcPetriNetNetwork.java	2020-08-04 06:34:24 +0000
+++ src/dk/aau/cs/model/tapn/TimedArcPetriNetNetwork.java	2020-08-14 09:31:36 +0000
@@ -505,6 +505,13 @@
 		return composedModel.value1().isDegree2();
 	}
 
+    public int getHighestNetDegree(){
+        ITAPNComposer composer = new TAPNComposer(new MessengerImpl(), false);
+        Tuple<TimedArcPetriNet,NameMapping> composedModel = composer.transformModel(this);
+
+        return composedModel.value1().getHighestNetDegree();
+    }
+
 	public boolean isSharedPlaceUsedInTemplates(SharedPlace place) {
 		for(TimedArcPetriNet tapn : this.activeTemplates()){
 			for(TimedPlace timedPlace : tapn.places()){

=== added file 'src/pipe/gui/EngineSupportOptions.java'
--- src/pipe/gui/EngineSupportOptions.java	1970-01-01 00:00:00 +0000
+++ src/pipe/gui/EngineSupportOptions.java	2020-08-14 09:31:36 +0000
@@ -0,0 +1,51 @@
+package pipe.gui;
+
+import java.util.ArrayList;
+
+public class EngineSupportOptions {
+    public final String nameString;
+    public final boolean supportFastestTrace;
+    public final boolean supportDeadlockNetdegree2EForAG;
+    public final boolean supportDeadlockWithInhib;
+    public final boolean supportWeights;
+    public final boolean supportInhibArcs;
+    public final boolean supportUrgentTransitions;
+    public final boolean supportEGorAF;
+    public final boolean supportStrictNets;
+    public final boolean supportTimedNets;
+    public final boolean supportDeadlockNetdegreeGreaterThan2;
+    public final boolean supportGames;
+    public final boolean supportEGorAFWithNetDegreeGreaterThan2;
+
+    public final boolean[] optionsArray;
+    public EngineSupportOptions(String nameString, boolean supportFastestTrace, boolean supportDeadlockNetdegree2EForAG, boolean supportDeadlockEGorAF, boolean supportDeadlockWithInhib,
+                                boolean supportWeights, boolean supportInhibArcs, boolean supportUrgentTransitions, boolean supportEGorAF, boolean supportStrictNets, boolean supportTimedNets,
+                                boolean supportDeadlockNetdegreeGreaterThan2, boolean supportGames, boolean supportEGorAFWithNetDegreeGreaterThan2){
+        this.nameString = nameString;
+        this.supportFastestTrace =  supportFastestTrace;
+        this.supportDeadlockNetdegree2EForAG =  supportDeadlockNetdegree2EForAG;
+        this.supportDeadlockWithInhib =  supportDeadlockWithInhib;
+        this.supportWeights =  supportWeights;
+        this.supportInhibArcs =  supportInhibArcs;
+        this.supportUrgentTransitions =  supportUrgentTransitions;
+        this.supportEGorAF =  supportEGorAF;
+        this.supportStrictNets =  supportStrictNets;
+        this.supportTimedNets = supportTimedNets;
+        this.supportDeadlockNetdegreeGreaterThan2 = supportDeadlockNetdegreeGreaterThan2;
+        this.supportGames = supportGames;
+        this.supportEGorAFWithNetDegreeGreaterThan2 = supportEGorAFWithNetDegreeGreaterThan2;
+        this.optionsArray = new boolean[]{supportFastestTrace, supportDeadlockNetdegree2EForAG, supportDeadlockEGorAF, supportDeadlockWithInhib,
+            supportWeights, supportInhibArcs, supportUrgentTransitions, supportEGorAF, supportStrictNets, supportTimedNets, supportDeadlockNetdegreeGreaterThan2,
+            supportGames, supportEGorAFWithNetDegreeGreaterThan2};
+    }
+
+    public boolean areOptionsSupported(boolean[] queryOptions){
+        for(int i = 0; i < optionsArray.length; i++){
+            if(queryOptions[i] == true && optionsArray[i] != true){
+                return false;
+            }
+        }
+        return true;
+    }
+
+}

=== modified file 'src/pipe/gui/widgets/QueryDialog.java'
--- src/pipe/gui/widgets/QueryDialog.java	2020-08-10 06:46:22 +0000
+++ src/pipe/gui/widgets/QueryDialog.java	2020-08-14 09:31:36 +0000
@@ -41,10 +41,7 @@
 import pipe.dataLayer.Template;
 import pipe.dataLayer.TAPNQuery.SearchOption;
 import pipe.dataLayer.TAPNQuery.TraceOption;
-import pipe.gui.CreateGui;
-import pipe.gui.MessengerImpl;
-import pipe.gui.Verifier;
-import pipe.gui.Zoomer;
+import pipe.gui.*;
 import dk.aau.cs.TCTL.StringPosition;
 import dk.aau.cs.TCTL.TCTLAFNode;
 import dk.aau.cs.TCTL.TCTLAGNode;
@@ -214,22 +211,139 @@
 	private final HashMap<TimedArcPetriNet, DataLayer> guiModels;
 	private QueryConstructionUndoManager undoManager;
 	private UndoableEditSupport undoSupport;
-	private final boolean isNetDegree2;
-	private final boolean hasInhibitorArcs;
+	private boolean isNetDegree2;
+	private int highestNetDegree;
+	private boolean hasInhibitorArcs;
 	private InclusionPlaces inclusionPlaces;
 	private TabContent.TAPNLens lens;
 
-	private final String name_verifyTAPN = "TAPAAL: Continous Engine (verifytapn)";
-	private final String name_COMBI = "UPPAAL: Optimized Broadcast Reduction";
-	private final String name_OPTIMIZEDSTANDARD = "UPPAAL: Optimised Standard Reduction";
-	private final String name_STANDARD = "UPPAAL: Standard Reduction";
-	private final String name_BROADCAST = "UPPAAL: Broadcast Reduction";
-	private final String name_BROADCASTDEG2 = "UPPAAL: Broadcast Degree 2 Reduction";
-	private final String name_DISCRETE = "TAPAAL: Discrete Engine (verifydtapn)";
-	private final String name_UNTIMED = "TAPAAL: Untimed Engine (verifypn)";
+	private static final String name_verifyTAPN = "TAPAAL: Continous Engine (verifytapn)";
+	private static final String name_COMBI = "UPPAAL: Optimized Broadcast Reduction";
+	private static final String name_OPTIMIZEDSTANDARD = "UPPAAL: Optimised Standard Reduction";
+	private static final String name_STANDARD = "UPPAAL: Standard Reduction";
+	private static final String name_BROADCAST = "UPPAAL: Broadcast Reduction";
+	private static final String name_BROADCASTDEG2 = "UPPAAL: Broadcast Degree 2 Reduction";
+	private static final String name_DISCRETE = "TAPAAL: Discrete Engine (verifydtapn)";
+	private static final String name_UNTIMED = "TAPAAL: Untimed Engine (verifypn)";
 	private boolean userChangedAtomicPropSelection = true;
-
-	private TCTLAbstractProperty newProperty;
+	//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
+    //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
+	private final static EngineSupportOptions verifyTAPNOptions= new EngineSupportOptions(
+	    name_verifyTAPN, //name of engine
+        false, //  support fastest trace
+        false, // support deadlock with net degree 2 and (EF or AG)
+        false, //  support deadlock with EG or AF
+        false, // support deadlock with inhibitor arcs
+        false,  //support weights
+        true,  //support inhibitor arcs
+        false, // support urgent transitions
+        false, // support EG or AF
+        true, // support strict nets
+        true, //  support timed nets/time intervals
+        false,// support deadlock with net degree > 2
+        false, //support games
+        false);//support EG or AF with net degree > 2
+
+    private final static EngineSupportOptions UPPAALCombiOptions= new EngineSupportOptions(
+        name_COMBI,//name of engine
+        false,//  support fastest trace
+        true,// support deadlock with net degree 2 and (EF or AG)
+        false,//  support deadlock with EG or AF
+        false,// support deadlock with inhibitor arcs
+        true, //support weights
+        true, //support inhibitor arcs
+        true,// support urgent transitions
+        true,// support EG or AF
+        true,// support strict nets
+        true,//  support timed nets/time intervals
+        false,// support deadlock with net degree > 2
+        false, //support games
+        true);//support EG or AF with net degree > 2);
+
+    private final static EngineSupportOptions UPPAALOptimizedStandardOptions = new EngineSupportOptions(
+        name_OPTIMIZEDSTANDARD,//name of engine
+        false,//  support fastest trace
+        false,// support deadlock with net degree 2 and (EF or AG)
+        false,//  support deadlock with EG or AF
+        false,// support deadlock with inhibitor arcs
+        false, //support weights
+        false, //support inhibitor arcs
+        false,// support urgent transitions
+        true,// support EG or AF
+        true,// support strict nets
+        true,//  support timed nets/time intervals
+        false,// support deadlock with net degree > 2
+        false, //support games
+        false);//support EG or AF with net degree > 2);
+
+    private final static EngineSupportOptions UPPAAALStandardOptions = new EngineSupportOptions(
+        name_STANDARD,//name of engine
+        false,//  support fastest trace
+        false,// support deadlock with net degree 2 and (EF or AG)
+        false,//  support deadlock with EG or AF
+        false,// support deadlock with inhibitor arcs
+        false, //support weights
+        false, //support inhibitor arcs
+        false,// support urgent transitions
+        false,// support EG or AF
+        true,// support strict nets
+        true,//  support timed nets/time intervals
+        false,// support deadlock with net degree > 2
+        false, //support games
+        false);//support EG or AF with net degree > 2);
+
+    private final static EngineSupportOptions UPPAALBroadcastOptions = new EngineSupportOptions(
+        name_BROADCAST,//name of engine
+        false,//  support fastest trace
+        true,// support deadlock with net degree 2 and (EF or AG)
+        false,//  support deadlock with EG or AF
+        false,// support deadlock with inhibitor arcs
+        false, //support weights
+        true, //support inhibitor arcs
+        false,// support urgent transitions
+        true,// support EG or AF
+        true,// support strict nets
+        true,//  support timed nets/time intervals
+        false,// support deadlock with net degree > 2
+        false, //support games
+        true);//support EG or AF with net degree > 2);
+
+    private final static EngineSupportOptions UPPAALBroadcastDegree2Options = new EngineSupportOptions(
+        name_BROADCASTDEG2,//name of engine
+        false,//  support fastest trace
+        true,// support deadlock with net degree 2 and (EF or AG)
+        false,//  support deadlock with EG or AF
+        false,// support deadlock with inhibitor arcs
+        false, //support weights
+        true, //support inhibitor arcs
+        false,// support urgent transitions
+        true,// support EG or AF
+        true,// support strict nets
+        true,//  support timed nets/time intervals
+        false,// support deadlock with net degree > 2
+        false, //support games
+        true);//support EG or AF with net degree > 2);
+
+    private final static EngineSupportOptions verifyDTAPNOptions= new EngineSupportOptions(
+        name_DISCRETE,//name of engine
+        true,//  support fastest trace
+        true,// support deadlock with net degree 2 and (EF or AG)
+        true,//  support deadlock with EG or AF
+        true,// support deadlock with inhibitor arcs
+        true, //support weights
+        true, //support inhibitor arcs
+        true,// support urgent transitions
+        true,// support EG or AF
+        false,// support strict nets
+        true,//  support timed nets/time intervals
+        true,// support deadlock with net degree > 2
+        true, //support games
+        true);//support EG or AF with net degree > 2);
+
+    //private final static EngineSupportOptions verifyPNOptions= new EngineSupportOptions(name_UNTIMED,false, true, true,true,true,true,false,true,false, false, false);
+    private final static EngineSupportOptions[] engineSupportOptions = new EngineSupportOptions[]{verifyDTAPNOptions,verifyTAPNOptions,UPPAALCombiOptions,UPPAALOptimizedStandardOptions,UPPAAALStandardOptions,UPPAALBroadcastOptions,UPPAALBroadcastDegree2Options,/*verifyPNOptions*/};
+
+    private TCTLAbstractProperty newProperty;
 	private JTextField queryName;
 
 	private static Boolean advancedView = false;
@@ -333,6 +447,7 @@
 		newProperty = queryToCreateFrom == null ? new TCTLPathPlaceHolder() : queryToCreateFrom.getProperty();
 		rootPane = me.getRootPane();
 		isNetDegree2 = tapnNetwork.isDegree2();
+		highestNetDegree = tapnNetwork.getHighestNetDegree();
 		hasInhibitorArcs = tapnNetwork.hasInhibitorArcs();
 
 		setLayout(new GridBagLayout());
@@ -707,12 +822,24 @@
 		ArrayList<String> options = new ArrayList<String>();
 		
 		disableSymmetryUpdate = true;
+		//The order here should be the same as in EngineSupportOptions
+        boolean[] queryOptions = new boolean[]{fastestTraceRadioButton.isSelected(),
+            (queryHasDeadlock() && (getQuantificationSelection().equals("E<>") || getQuantificationSelection().equals("A[]")) && highestNetDegree <= 2),
+            (queryHasDeadlock() && (getQuantificationSelection().equals("E[]") || getQuantificationSelection().equals("A<>"))),
+            (queryHasDeadlock() && hasInhibitorArcs),
+            tapnNetwork.hasWeights(),
+            hasInhibitorArcs,
+            tapnNetwork.hasUrgentTransitions(),
+            (getQuantificationSelection().equals("E[]") || getQuantificationSelection().equals("A<>")),
+            //we want to know if it is strict
+            !tapnNetwork.isNonStrict(),
+            //we want to know if it is timed
+            lens.isTimed(),
+            (queryHasDeadlock() && highestNetDegree > 2),
+            lens.isGame(),
+            (getQuantificationSelection().equals("E[]") || getQuantificationSelection().equals("A<>")) && highestNetDegree > 2
+        };
 
-		/* The untimed engine is disabled for now. It is used in the CTL query dialog
-		if(!fastestTraceRadioButton.isSelected() && (getQuantificationSelection().equals("E<>") || getQuantificationSelection().equals("A[]") || getQuantificationSelection().equals("")) && tapnNetwork.isUntimed()){
-			options.add(name_UNTIMED);
-		}
-		*/
 		
 		if(useTimeDarts != null){
 			if(hasForcedDisabledTimeDarts){
@@ -738,68 +865,24 @@
             useGCD.setEnabled(true);     
         }
 
-		if (lens.isGame()) {
-		    if (tapnNetwork.isNonStrict()) {
-		        options.add(name_DISCRETE);
-            }
-        } else if (fastestTraceRadioButton.isSelected()) {
-        	options.add(name_DISCRETE);
-        } else if (queryHasDeadlock()) {
-            if (tapnNetwork.isNonStrict()) {
-                options.add(name_DISCRETE);
-                // disable timedarts if liveness and deadlock prop
-                if((getQuantificationSelection().equals("E[]") || 
-                        getQuantificationSelection().equals("A<>"))){
-                    if (useTimeDarts != null) {
-                    	if(useTimeDarts.isSelected()){
-                    		hasForcedDisabledTimeDarts = true;
-                    	}
-                        useTimeDarts.setEnabled(false);
-                        useTimeDarts.setSelected(false);
+        if (tapnNetwork.isNonStrict()) {
+            // disable timedarts if liveness and deadlock prop
+            if((getQuantificationSelection().equals("E[]") ||
+                getQuantificationSelection().equals("A<>"))){
+                if (useTimeDarts != null) {
+                    if(useTimeDarts.isSelected()){
+                        hasForcedDisabledTimeDarts = true;
                     }
-                }
-            }
-            if (getQuantificationSelection().equals("E<>") || getQuantificationSelection().equals("A[]")) {
-                if (isNetDegree2 && !hasInhibitorArcs) {
-                	options.add(name_COMBI);
-                	if(!tapnNetwork.hasWeights() && !hasInhibitorArcs) {
-                		options.addAll(Arrays.asList(name_BROADCAST, name_BROADCASTDEG2));
-                	}
-                }
-            }
-            
-		} else if(tapnNetwork.hasWeights()){
-			if(tapnNetwork.isNonStrict()){
-				options.add(name_DISCRETE);
-			}
-			options.add(name_COMBI);
-		} else if(tapnNetwork.hasUrgentTransitions()){
-			if(tapnNetwork.isNonStrict()){
-				options.add(name_DISCRETE);
-			}
-			options.add(name_COMBI);
-        } else if (getQuantificationSelection().equals("E[]") || getQuantificationSelection().equals("A<>")) {
-			if(tapnNetwork.isNonStrict()){
-				options.add(name_DISCRETE);
-			}
-			options.add(name_COMBI);
-			if(isNetDegree2 && !hasInhibitorArcs)
-				options.addAll(Arrays.asList( name_BROADCAST, name_BROADCASTDEG2, name_OPTIMIZEDSTANDARD));
-			else
-				options.addAll(Arrays.asList(name_BROADCAST, name_BROADCASTDEG2));
-		} else if(tapnNetwork.hasInhibitorArcs()) {
-			options.add( name_verifyTAPN );
-			if(tapnNetwork.isNonStrict()){
-				options.add(name_DISCRETE);
-			}					
-			options.addAll(Arrays.asList(name_COMBI, name_BROADCAST, name_BROADCASTDEG2 ));
-		} else {
-			options.add( name_verifyTAPN);
-			if(tapnNetwork.isNonStrict()){
-				options.add(name_DISCRETE);
-			}
-			options.addAll(Arrays.asList(name_COMBI, name_OPTIMIZEDSTANDARD, name_STANDARD, name_BROADCAST, name_BROADCASTDEG2));
-		}
+                    useTimeDarts.setEnabled(false);
+                    useTimeDarts.setSelected(false);
+                }
+            }
+        }
+		for(EngineSupportOptions engine : engineSupportOptions){
+		    if(engine.areOptionsSupported(queryOptions)){
+		        options.add(engine.nameString);
+            }
+        }
 
 		reductionOption.removeAllItems();