Merge lp:~tapaal-contributor/tapaal/remove-nongame-queries into lp:tapaal

[Lena Said]

Remove affected queries when changing to game nets

When changing a net from non-game to game, the queries that aren't supported by the game feature is removed

[lp:~tapaal-contributor/tapaal/remove-nongame-queries]

1105. By Lena Said on 2020-08-19

Merge with trunk

[Jiri Srba (srba)]

The exclusion is too restrictive in these checks:
!q.getReductionOption().equals(ReductionOption.VerifyTAPNdiscreteVerification)
+ || !q.getTraceOption().equals(TAPNQuery.TraceOption.NONE)
+ || q.getSearchOption().equals(TAPNQuery.SearchOption.HEURISTIC)
+ || q.isUnderApproximationEnabled()
+ || q.isOverApproximationEnabled()
+ || q.useTimeDarts()
+ || q.useGCD()

These should be changed so that the query is legal (whenever possible).

review: Needs Fixing

[lp:~tapaal-contributor/tapaal/remove-nongame-queries]

1106. By Lena Said on 2020-08-20

Made the checks less restrictive

[Jiri Srba (srba)]

review: Approve

=== modified file 'src/dk/aau/cs/gui/TabContent.java'
--- src/dk/aau/cs/gui/TabContent.java	2020-08-17 08:18:13 +0000
+++ src/dk/aau/cs/gui/TabContent.java	2020-08-20 07:26:16 +0000
@@ -12,6 +12,8 @@
 
 import javax.swing.*;
 import javax.swing.border.BevelBorder;
+
+import dk.aau.cs.TCTL.TCTLAGNode;
 import dk.aau.cs.debug.Logger;
 import dk.aau.cs.gui.components.BugHandledJXMultisplitPane;
 import dk.aau.cs.gui.components.StatisticsPanel;
@@ -23,6 +25,7 @@
 import dk.aau.cs.io.queries.SUMOQueryLoader;
 import dk.aau.cs.io.queries.XMLQueryLoader;
 import dk.aau.cs.model.tapn.*;
+import dk.aau.cs.translations.ReductionOption;
 import dk.aau.cs.util.Require;
 import dk.aau.cs.util.Tuple;
 import dk.aau.cs.verification.NameMapping;
@@ -1566,12 +1569,45 @@
                 }
             } else {
                 TabContent tab = duplicateTab(new TAPNLens(lens.isTimed(), true), "-game");
+                findAndRemoveGameAffectedQueries(tab);
                 guiFrameControllerActions.ifPresent(o -> o.openTab(tab));
             }
             updateFeatureText();
         }
     }
 
+    private void findAndRemoveGameAffectedQueries(TabContent tab){
+        List<TAPNQuery> queriesToRemove = new ArrayList<TAPNQuery>();
+        for (TAPNQuery q : tab.queries()) {
+            if (q.hasUntimedOnlyProperties() || !(q.getProperty() instanceof TCTLAGNode) || !lens.isTimed()) {
+                queriesToRemove.add(q);
+                tab.removeQuery(q);
+            } else {
+                if (!q.getReductionOption().equals(ReductionOption.VerifyTAPNdiscreteVerification)) {
+                    q.setReductionOption(ReductionOption.VerifyTAPNdiscreteVerification);
+                } if (!q.getTraceOption().equals(TAPNQuery.TraceOption.NONE)) {
+                    q.setTraceOption(TAPNQuery.TraceOption.NONE);
+                } if (q.getSearchOption().equals(TAPNQuery.SearchOption.HEURISTIC)) {
+                    q.setSearchOption(TAPNQuery.SearchOption.DFS);
+                } if (q.useTimeDarts()) {
+                    q.setUseTimeDarts(false);
+                } if (q.useGCD()) {
+                    q.setUseGCD(false);
+                } if (q.isOverApproximationEnabled() || q.isUnderApproximationEnabled()) {
+                    q.setUseOverApproximationEnabled(false);
+                    q.setUseUnderApproximationEnabled(false);
+                }
+            }
+        }
+        String message = "The following queries will be removed in the conversion:";
+        for (TAPNQuery q : queriesToRemove) {
+            message += "\n" + q.getName();
+        }
+        if (!queriesToRemove.isEmpty()) {
+            JOptionPane.showMessageDialog(this, message, "Information", JOptionPane.INFORMATION_MESSAGE);
+        }
+    }
+
     public static Split getEditorModelRoot(){
 		return editorModelroot;
 	}

=== modified file 'src/pipe/dataLayer/TAPNQuery.java'
--- src/pipe/dataLayer/TAPNQuery.java	2020-08-17 08:09:43 +0000
+++ src/pipe/dataLayer/TAPNQuery.java	2020-08-20 07:26:16 +0000
@@ -218,7 +218,15 @@
 	public void setUseOverApproximation(boolean useOverApproximation){
 		overApproximation = useOverApproximation;
 	}
-	
+
+    public void setUseOverApproximationEnabled(boolean useOverApproximationEnabled){
+        this.enableOverApproximation = useOverApproximationEnabled;
+    }
+
+    public void setUseUnderApproximationEnabled(boolean useUnderApproximationEnabled){
+        this.enableUnderApproximation = useUnderApproximationEnabled;
+    }
+
 	public void setUseReduction(boolean useReduction){
 		this.useReduction = useReduction;
 	}