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

Proposed by Lena Said on 2020-08-18
Status: Merged
Approved by: Jiri Srba on 2020-08-24
Approved revision: 1106
Merged at revision: 1085
Proposed branch: lp:~tapaal-contributor/tapaal/remove-nongame-queries
Merge into: lp:tapaal
Diff against target: 87 lines (+45/-1)
2 files modified
src/dk/aau/cs/gui/TabContent.java (+36/-0)
src/pipe/dataLayer/TAPNQuery.java (+9/-1)
To merge this branch: bzr merge lp:~tapaal-contributor/tapaal/remove-nongame-queries
Reviewer Review Type Date Requested Status
Jiri Srba 2020-08-18 Approve on 2020-08-24
Review via email: mp+389467@code.launchpad.net

Commit message

Remove affected queries when changing to game nets

Description of the change

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

To post a comment you must log in.
1105. By Lena Said on 2020-08-19

Merge with trunk

Jiri Srba (srba) wrote :

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
1106. By Lena Said on 2020-08-20

Made the checks less restrictive

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/gui/TabContent.java'
2--- src/dk/aau/cs/gui/TabContent.java 2020-08-17 08:18:13 +0000
3+++ src/dk/aau/cs/gui/TabContent.java 2020-08-20 07:26:16 +0000
4@@ -12,6 +12,8 @@
5
6 import javax.swing.*;
7 import javax.swing.border.BevelBorder;
8+
9+import dk.aau.cs.TCTL.TCTLAGNode;
10 import dk.aau.cs.debug.Logger;
11 import dk.aau.cs.gui.components.BugHandledJXMultisplitPane;
12 import dk.aau.cs.gui.components.StatisticsPanel;
13@@ -23,6 +25,7 @@
14 import dk.aau.cs.io.queries.SUMOQueryLoader;
15 import dk.aau.cs.io.queries.XMLQueryLoader;
16 import dk.aau.cs.model.tapn.*;
17+import dk.aau.cs.translations.ReductionOption;
18 import dk.aau.cs.util.Require;
19 import dk.aau.cs.util.Tuple;
20 import dk.aau.cs.verification.NameMapping;
21@@ -1566,12 +1569,45 @@
22 }
23 } else {
24 TabContent tab = duplicateTab(new TAPNLens(lens.isTimed(), true), "-game");
25+ findAndRemoveGameAffectedQueries(tab);
26 guiFrameControllerActions.ifPresent(o -> o.openTab(tab));
27 }
28 updateFeatureText();
29 }
30 }
31
32+ private void findAndRemoveGameAffectedQueries(TabContent tab){
33+ List<TAPNQuery> queriesToRemove = new ArrayList<TAPNQuery>();
34+ for (TAPNQuery q : tab.queries()) {
35+ if (q.hasUntimedOnlyProperties() || !(q.getProperty() instanceof TCTLAGNode) || !lens.isTimed()) {
36+ queriesToRemove.add(q);
37+ tab.removeQuery(q);
38+ } else {
39+ if (!q.getReductionOption().equals(ReductionOption.VerifyTAPNdiscreteVerification)) {
40+ q.setReductionOption(ReductionOption.VerifyTAPNdiscreteVerification);
41+ } if (!q.getTraceOption().equals(TAPNQuery.TraceOption.NONE)) {
42+ q.setTraceOption(TAPNQuery.TraceOption.NONE);
43+ } if (q.getSearchOption().equals(TAPNQuery.SearchOption.HEURISTIC)) {
44+ q.setSearchOption(TAPNQuery.SearchOption.DFS);
45+ } if (q.useTimeDarts()) {
46+ q.setUseTimeDarts(false);
47+ } if (q.useGCD()) {
48+ q.setUseGCD(false);
49+ } if (q.isOverApproximationEnabled() || q.isUnderApproximationEnabled()) {
50+ q.setUseOverApproximationEnabled(false);
51+ q.setUseUnderApproximationEnabled(false);
52+ }
53+ }
54+ }
55+ String message = "The following queries will be removed in the conversion:";
56+ for (TAPNQuery q : queriesToRemove) {
57+ message += "\n" + q.getName();
58+ }
59+ if (!queriesToRemove.isEmpty()) {
60+ JOptionPane.showMessageDialog(this, message, "Information", JOptionPane.INFORMATION_MESSAGE);
61+ }
62+ }
63+
64 public static Split getEditorModelRoot(){
65 return editorModelroot;
66 }
67
68=== modified file 'src/pipe/dataLayer/TAPNQuery.java'
69--- src/pipe/dataLayer/TAPNQuery.java 2020-08-17 08:09:43 +0000
70+++ src/pipe/dataLayer/TAPNQuery.java 2020-08-20 07:26:16 +0000
71@@ -218,7 +218,15 @@
72 public void setUseOverApproximation(boolean useOverApproximation){
73 overApproximation = useOverApproximation;
74 }
75-
76+
77+ public void setUseOverApproximationEnabled(boolean useOverApproximationEnabled){
78+ this.enableOverApproximation = useOverApproximationEnabled;
79+ }
80+
81+ public void setUseUnderApproximationEnabled(boolean useUnderApproximationEnabled){
82+ this.enableUnderApproximation = useUnderApproximationEnabled;
83+ }
84+
85 public void setUseReduction(boolean useReduction){
86 this.useReduction = useReduction;
87 }

Subscribers

People subscribed via source and target branches