=== 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 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 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 options = new ArrayList(); 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();