Merge lp:~tapaal-contributor/tapaal/add-tar-option into lp:tapaal

Proposed by Lena Said
Status: Merged
Approved by: Jiri Srba
Approved revision: 1118
Merged at revision: 1119
Proposed branch: lp:~tapaal-contributor/tapaal/add-tar-option
Merge into: lp:tapaal
Diff against target: 312 lines (+66/-15)
8 files modified
src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java (+9/-4)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java (+7/-1)
src/pipe/dataLayer/TAPNQuery.java (+10/-0)
src/pipe/gui/KBoundAnalyzer.java (+1/-1)
src/pipe/gui/RunVerificationBase.java (+4/-2)
src/pipe/gui/Verifier.java (+4/-4)
src/pipe/gui/widgets/QueryDialog.java (+30/-2)
src/resources/Example nets/train-level-crossing.tapn (+1/-1)
To merge this branch: bzr merge lp:~tapaal-contributor/tapaal/add-tar-option
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Kenneth Yrke Jørgensen code Approve
Review via email: mp+397624@code.launchpad.net

Commit message

Added -tar option to the query dialog

To post a comment you must log in.
1116. By Lena Said on 2021-02-07

Merged lp:tapaal

review: Approve (code)
Jiri Srba (srba) wrote :

The detection if a query is a reachability query must be improved - tar can only be offered for EF or AG queries that do not contain any other temporal operators.

E.g. for the query

E ((AG true) U false)

the TAR option is offered as well, which should not be the case.

review: Needs Fixing
1117. By Lena Said on 2021-02-19

Only possible to use tar when either 'AG' or 'EF' is chosen

Jiri Srba (srba) wrote :

I just made a simple untimed net and a query:

A (TAPN1.P0 = 1 U (EF TAPN1.P0 = 1))

and it still offers to use the tar option in the query dialog.

review: Needs Fixing
1118. By Lena Said on 2021-02-22

Fixed tar only possible with AG and EF

Jiri Srba (srba) :
review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java 2020-10-15 15:44:06 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java 2021-02-22 22:26:13 +0000
@@ -19,26 +19,28 @@
19 private boolean useSiphontrap = false; 19 private boolean useSiphontrap = false;
20 private QueryReductionTime queryReductionTime;20 private QueryReductionTime queryReductionTime;
21 private boolean useStubbornReduction = true;21 private boolean useStubbornReduction = true;
22 private boolean useTarOption;
22 private String pathToReducedNet;23 private String pathToReducedNet;
23 24
24 public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, ModelReduction modelReduction,25 public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, ModelReduction modelReduction,
25 boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, QueryCategory queryCategory, AlgorithmOption algorithmOption,26 boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, QueryCategory queryCategory, AlgorithmOption algorithmOption,
26 boolean siphontrap, QueryReductionTime queryReduction, boolean stubbornReduction, String pathToReducedNet) {27 boolean siphontrap, QueryReductionTime queryReduction, boolean stubbornReduction, String pathToReducedNet, boolean useTarOption) {
27 super(extraTokens, traceOption, search, true, useOverApproximation, false, new InclusionPlaces(), enableOverApproximation, enableUnderApproximation, approximationDenominator);28 super(extraTokens, traceOption, search, true, useOverApproximation, false, new InclusionPlaces(), enableOverApproximation, enableUnderApproximation, approximationDenominator, useTarOption);
28 this.modelReduction = modelReduction;29 this.modelReduction = modelReduction;
29 this.queryCategory = queryCategory;30 this.queryCategory = queryCategory;
30 this.algorithmOption = algorithmOption;31 this.algorithmOption = algorithmOption;
31 this.useSiphontrap = siphontrap;32 this.useSiphontrap = siphontrap;
32 this.queryReductionTime = queryReduction;33 this.queryReductionTime = queryReduction;
33 this.useStubbornReduction = stubbornReduction;34 this.useStubbornReduction = stubbornReduction;
35 this.useTarOption = useTarOption;
34 this.pathToReducedNet = pathToReducedNet;36 this.pathToReducedNet = pathToReducedNet;
35 }37 }
36 38
37 public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, boolean useModelReduction,39 public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, boolean useModelReduction,
38 boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, QueryCategory queryCategory, AlgorithmOption algorithmOption,40 boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, QueryCategory queryCategory, AlgorithmOption algorithmOption,
39 boolean siphontrap, QueryReductionTime queryReduction, boolean stubbornReduction) {41 boolean siphontrap, QueryReductionTime queryReduction, boolean stubbornReduction) {
40 this(extraTokens, traceOption, search, useOverApproximation, useModelReduction? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION, enableOverApproximation, 42 this(extraTokens, traceOption, search, useOverApproximation, useModelReduction? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION, enableOverApproximation,
41 enableUnderApproximation, approximationDenominator,queryCategory, algorithmOption, siphontrap, queryReduction, stubbornReduction, null);43 enableUnderApproximation, approximationDenominator,queryCategory, algorithmOption, siphontrap, queryReduction, stubbornReduction, null, false);
42 }44 }
4345
44 @Override46 @Override
@@ -83,6 +85,9 @@
83 if (!this.useStubbornReduction) {85 if (!this.useStubbornReduction) {
84 result.append(" -p ");86 result.append(" -p ");
85 }87 }
88 if (this.useTarOption) {
89 result.append(" -tar ");
90 }
86 return result.toString();91 return result.toString();
87 }92 }
8893
8994
=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java 2020-07-13 13:58:47 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java 2021-02-22 22:26:13 +0000
@@ -16,6 +16,7 @@
16 protected int tokensInModel;16 protected int tokensInModel;
17 private final boolean symmetry;17 private final boolean symmetry;
18 private final boolean discreteInclusion;18 private final boolean discreteInclusion;
19 private final boolean tarOption;
19 private InclusionPlaces inclusionPlaces;20 private InclusionPlaces inclusionPlaces;
20 21
21 //only used for boundedness analysis22 //only used for boundedness analysis
@@ -27,8 +28,12 @@
27 public VerifyTAPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean symmetry, boolean useStateequationCheck, boolean discreteInclusion, boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator) {28 public VerifyTAPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean symmetry, boolean useStateequationCheck, boolean discreteInclusion, boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator) {
28 this(extraTokens,traceOption, search, symmetry, useStateequationCheck, discreteInclusion, new InclusionPlaces(), enableOverApproximation, enableUnderApproximation, approximationDenominator);29 this(extraTokens,traceOption, search, symmetry, useStateequationCheck, discreteInclusion, new InclusionPlaces(), enableOverApproximation, enableUnderApproximation, approximationDenominator);
29 }30 }
31
32 public VerifyTAPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean symmetry, boolean useStateequationCheck, boolean discreteInclusion, InclusionPlaces inclusionPlaces, boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator) {
33 this(extraTokens,traceOption, search, symmetry, useStateequationCheck, discreteInclusion, new InclusionPlaces(), enableOverApproximation, enableUnderApproximation, approximationDenominator, false);
34 }
30 35
31 public VerifyTAPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean symmetry, boolean useStateEquationCheck, boolean discreteInclusion, InclusionPlaces inclusionPlaces, boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator) {36 public VerifyTAPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean symmetry, boolean useStateEquationCheck, boolean discreteInclusion, InclusionPlaces inclusionPlaces, boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, boolean tarOption) {
32 this.extraTokens = extraTokens;37 this.extraTokens = extraTokens;
33 this.traceOption = traceOption;38 this.traceOption = traceOption;
34 searchOption = search;39 searchOption = search;
@@ -39,6 +44,7 @@
39 this.enabledOverApproximation = enableOverApproximation;44 this.enabledOverApproximation = enableOverApproximation;
40 this.enabledUnderApproximation = enableUnderApproximation;45 this.enabledUnderApproximation = enableUnderApproximation;
41 this.approximationDenominator = approximationDenominator;46 this.approximationDenominator = approximationDenominator;
47 this.tarOption = tarOption;
42 }48 }
4349
44 public TraceOption trace() {50 public TraceOption trace() {
4551
=== modified file 'src/pipe/dataLayer/TAPNQuery.java'
--- src/pipe/dataLayer/TAPNQuery.java 2020-11-06 19:41:50 +0000
+++ src/pipe/dataLayer/TAPNQuery.java 2021-02-22 22:26:13 +0000
@@ -72,6 +72,7 @@
72 private boolean useSiphontrap = false; 72 private boolean useSiphontrap = false;
73 private boolean useQueryReduction = true; 73 private boolean useQueryReduction = true;
74 private boolean useStubbornReduction = true;74 private boolean useStubbornReduction = true;
75 private boolean useTarOption = false;
7576
76 /**77 /**
77 * @param name78 * @param name
@@ -108,6 +109,14 @@
108 return this.useStubbornReduction;109 return this.useStubbornReduction;
109 }110 }
110111
112 public boolean isTarOptionEnabled() {
113 return this.useTarOption;
114 }
115
116 public void setUseTarOption(boolean useTarOption) {
117 this.useTarOption = useTarOption;
118 }
119
111 public int approximationDenominator() {120 public int approximationDenominator() {
112 return this.denominator;121 return this.denominator;
113 }122 }
@@ -361,6 +370,7 @@
361 useSiphontrap = newQuery.isSiphontrapEnabled();370 useSiphontrap = newQuery.isSiphontrapEnabled();
362 useQueryReduction = newQuery.isQueryReductionEnabled();371 useQueryReduction = newQuery.isQueryReductionEnabled();
363 useStubbornReduction = newQuery.isStubbornReductionEnabled();372 useStubbornReduction = newQuery.isStubbornReductionEnabled();
373 useTarOption = newQuery.isTarOptionEnabled();
364 }374 }
365375
366 public InclusionPlaces inclusionPlaces() {376 public InclusionPlaces inclusionPlaces() {
367377
=== modified file 'src/pipe/gui/KBoundAnalyzer.java'
--- src/pipe/gui/KBoundAnalyzer.java 2020-10-15 15:44:06 +0000
+++ src/pipe/gui/KBoundAnalyzer.java 2021-02-22 22:26:13 +0000
@@ -52,7 +52,7 @@
5252
53 protected VerifyTAPNOptions verificationOptions() {53 protected VerifyTAPNOptions verificationOptions() {
54 if(modelChecker instanceof VerifyPN){54 if(modelChecker instanceof VerifyPN){
55 return new VerifyPNOptions(k, TraceOption.NONE, SearchOption.BFS, false, ModelReduction.BOUNDPRESERVING, false, false, 1, QueryCategory.Default, AlgorithmOption.CERTAIN_ZERO, false, pipe.dataLayer.TAPNQuery.QueryReductionTime.UnlimitedTime, false, null);55 return new VerifyPNOptions(k, TraceOption.NONE, SearchOption.BFS, false, ModelReduction.BOUNDPRESERVING, false, false, 1, QueryCategory.Default, AlgorithmOption.CERTAIN_ZERO, false, pipe.dataLayer.TAPNQuery.QueryReductionTime.UnlimitedTime, false, null, false);
56 } else if(modelChecker instanceof VerifyTAPN){56 } else if(modelChecker instanceof VerifyTAPN){
57 return new VerifyTAPNOptions(k, TraceOption.NONE, SearchOption.BFS, true, false, true, false, false, 1);57 return new VerifyTAPNOptions(k, TraceOption.NONE, SearchOption.BFS, true, false, true, false, false, 1);
58 } else if(modelChecker instanceof VerifyTAPNDiscreteVerification){58 } else if(modelChecker instanceof VerifyTAPNDiscreteVerification){
5959
=== modified file 'src/pipe/gui/RunVerificationBase.java'
--- src/pipe/gui/RunVerificationBase.java 2020-11-11 07:55:24 +0000
+++ src/pipe/gui/RunVerificationBase.java 2021-02-22 22:26:13 +0000
@@ -122,7 +122,8 @@
122 dataLayerQuery.isSiphontrapEnabled(),122 dataLayerQuery.isSiphontrapEnabled(),
123 dataLayerQuery.isQueryReductionEnabled()? pipe.dataLayer.TAPNQuery.QueryReductionTime.UnlimitedTime: pipe.dataLayer.TAPNQuery.QueryReductionTime.NoTime,123 dataLayerQuery.isQueryReductionEnabled()? pipe.dataLayer.TAPNQuery.QueryReductionTime.UnlimitedTime: pipe.dataLayer.TAPNQuery.QueryReductionTime.NoTime,
124 dataLayerQuery.isStubbornReductionEnabled(),124 dataLayerQuery.isStubbornReductionEnabled(),
125 reducedNetFilePath125 reducedNetFilePath,
126 dataLayerQuery.isTarOptionEnabled()
126 ),127 ),
127 transformedModel,128 transformedModel,
128 clonedQuery129 clonedQuery
@@ -143,7 +144,8 @@
143 false,144 false,
144 pipe.dataLayer.TAPNQuery.QueryReductionTime.UnlimitedTime,145 pipe.dataLayer.TAPNQuery.QueryReductionTime.UnlimitedTime,
145 false,146 false,
146 reducedNetFilePath147 reducedNetFilePath,
148 false
147 ),149 ),
148 transformedModel,150 transformedModel,
149 clonedQuery151 clonedQuery
150152
=== modified file 'src/pipe/gui/Verifier.java'
--- src/pipe/gui/Verifier.java 2020-11-13 10:08:54 +0000
+++ src/pipe/gui/Verifier.java 2021-02-22 22:26:13 +0000
@@ -176,7 +176,6 @@
176 query.isStubbornReductionEnabled()176 query.isStubbornReductionEnabled()
177 );177 );
178 } else if(query.getReductionOption() == ReductionOption.VerifyPN){178 } else if(query.getReductionOption() == ReductionOption.VerifyPN){
179
180 try {179 try {
181 reducedNetTempFile = File.createTempFile("reduced-", ".pnml");180 reducedNetTempFile = File.createTempFile("reduced-", ".pnml");
182 } catch (IOException e) {181 } catch (IOException e) {
@@ -202,7 +201,8 @@
202 query.isSiphontrapEnabled(),201 query.isSiphontrapEnabled(),
203 TAPNQuery.QueryReductionTime.NoTime,202 TAPNQuery.QueryReductionTime.NoTime,
204 query.isStubbornReductionEnabled(),203 query.isStubbornReductionEnabled(),
205 reducedNetTempFile.getAbsolutePath()204 reducedNetTempFile.getAbsolutePath(),
205 query.isTarOptionEnabled()
206 );206 );
207 } else {207 } else {
208 verifytapnOptions = new VerifyPNOptions(208 verifytapnOptions = new VerifyPNOptions(
@@ -219,10 +219,10 @@
219 query.isSiphontrapEnabled(),219 query.isSiphontrapEnabled(),
220 query.isQueryReductionEnabled()? TAPNQuery.QueryReductionTime.UnlimitedTime: TAPNQuery.QueryReductionTime.NoTime,220 query.isQueryReductionEnabled()? TAPNQuery.QueryReductionTime.UnlimitedTime: TAPNQuery.QueryReductionTime.NoTime,
221 query.isStubbornReductionEnabled(),221 query.isStubbornReductionEnabled(),
222 reducedNetTempFile.getAbsolutePath()222 reducedNetTempFile.getAbsolutePath(),
223 query.isTarOptionEnabled()
223 );224 );
224 }225 }
225
226 } else {226 } else {
227 verifytapnOptions = new VerifyTAPNOptions(227 verifytapnOptions = new VerifyTAPNOptions(
228 bound,228 bound,
229229
=== modified file 'src/pipe/gui/widgets/QueryDialog.java'
--- src/pipe/gui/widgets/QueryDialog.java 2020-12-17 21:03:12 +0000
+++ src/pipe/gui/widgets/QueryDialog.java 2021-02-22 22:26:13 +0000
@@ -165,6 +165,7 @@
165 private JCheckBox useQueryReduction;165 private JCheckBox useQueryReduction;
166 private JCheckBox useReduction;166 private JCheckBox useReduction;
167 private JCheckBox useStubbornReduction;167 private JCheckBox useStubbornReduction;
168 private JCheckBox useTraceRefinement;
168169
169 // Approximation options panel170 // Approximation options panel
170 private JPanel overApproximationOptionsPanel;171 private JPanel overApproximationOptionsPanel;
@@ -293,6 +294,7 @@
293 private final static String TOOL_TIP_USE_STRUCTURALREDUCTION = "Apply structural reductions to reduce the size of the net.";294 private final static String TOOL_TIP_USE_STRUCTURALREDUCTION = "Apply structural reductions to reduce the size of the net.";
294 private final static String TOOL_TIP_USE_SIPHONTRAP = "For a deadlock query, attempt to prove deadlock-freedom by using siphon-trap analysis via linear programming.";295 private final static String TOOL_TIP_USE_SIPHONTRAP = "For a deadlock query, attempt to prove deadlock-freedom by using siphon-trap analysis via linear programming.";
295 private final static String TOOL_TIP_USE_QUERY_REDUCTION = "Use query rewriting rules and linear programming (state equations) to reduce the size of the query.";296 private final static String TOOL_TIP_USE_QUERY_REDUCTION = "Use query rewriting rules and linear programming (state equations) to reduce the size of the query.";
297 private final static String TOOL_TIP_USE_TRACE_REFINEMENT = "Enables Trace Abstraction Refinement for reachability properties";
296298
297 //Tool tips for search options panel299 //Tool tips for search options panel
298 private final static String TOOL_TIP_HEURISTIC_SEARCH = "<html>Uses a heuristic method in state space exploration.<br />" +300 private final static String TOOL_TIP_HEURISTIC_SEARCH = "<html>Uses a heuristic method in state space exploration.<br />" +
@@ -322,8 +324,7 @@
322 private final static String TOOL_TIP_APPROXIMATION_METHOD_UNDER = "Approximate by dividing all intervals with the approximation constant and shrinking the intervals.";324 private final static String TOOL_TIP_APPROXIMATION_METHOD_UNDER = "Approximate by dividing all intervals with the approximation constant and shrinking the intervals.";
323 private final static String TOOL_TIP_APPROXIMATION_CONSTANT = "Choose approximation constant";325 private final static String TOOL_TIP_APPROXIMATION_CONSTANT = "Choose approximation constant";
324326
325 public QueryDialog(EscapableDialog me, QueryDialogueOption option,327 public QueryDialog(EscapableDialog me, QueryDialogueOption option, TAPNQuery queryToCreateFrom, TimedArcPetriNetNetwork tapnNetwork, HashMap<TimedArcPetriNet, DataLayer> guiModels, TabContent.TAPNLens lens) {
326 TAPNQuery queryToCreateFrom, TimedArcPetriNetNetwork tapnNetwork, HashMap<TimedArcPetriNet, DataLayer> guiModels, TabContent.TAPNLens lens) {
327 this.tapnNetwork = tapnNetwork;328 this.tapnNetwork = tapnNetwork;
328 this.guiModels = guiModels;329 this.guiModels = guiModels;
329 this.lens = lens;330 this.lens = lens;
@@ -442,6 +443,7 @@
442 query.setUseSiphontrap(useSiphonTrap.isSelected());443 query.setUseSiphontrap(useSiphonTrap.isSelected());
443 query.setUseQueryReduction(useQueryReduction.isSelected());444 query.setUseQueryReduction(useQueryReduction.isSelected());
444 query.setUseStubbornReduction(useStubbornReduction.isSelected());445 query.setUseStubbornReduction(useStubbornReduction.isSelected());
446 query.setUseTarOption(useTraceRefinement.isSelected());
445 return query;447 return query;
446 }448 }
447449
@@ -1210,8 +1212,15 @@
1210 setupSearchOptionsFromQuery(queryToCreateFrom);1212 setupSearchOptionsFromQuery(queryToCreateFrom);
1211 setupReductionOptionsFromQuery(queryToCreateFrom);1213 setupReductionOptionsFromQuery(queryToCreateFrom);
1212 setupTraceOptionsFromQuery(queryToCreateFrom);1214 setupTraceOptionsFromQuery(queryToCreateFrom);
1215 setupTarOptionsFromQuery(queryToCreateFrom);
1213 }1216 }
12141217
1218 private void setupTarOptionsFromQuery(TAPNQuery queryToCreateFrom) {
1219 if (queryToCreateFrom.isTarOptionEnabled()) {
1220 useTraceRefinement.setSelected(true);
1221 }
1222 }
1223
1215 private void setupApproximationOptionsFromQuery(TAPNQuery queryToCreateFrom) {1224 private void setupApproximationOptionsFromQuery(TAPNQuery queryToCreateFrom) {
1216 if (queryToCreateFrom.isOverApproximationEnabled())1225 if (queryToCreateFrom.isOverApproximationEnabled())
1217 overApproximationEnable.setSelected(true);1226 overApproximationEnable.setSelected(true);
@@ -2656,6 +2665,7 @@
2656 useGCD = new JCheckBox("Use GCD");2665 useGCD = new JCheckBox("Use GCD");
2657 usePTrie = new JCheckBox("Use PTrie");2666 usePTrie = new JCheckBox("Use PTrie");
2658 useOverApproximation = new JCheckBox("Use untimed state-equations check");2667 useOverApproximation = new JCheckBox("Use untimed state-equations check");
2668 useTraceRefinement = new JCheckBox("Use trace abstraction refinement");
26592669
2660 useReduction.setSelected(true);2670 useReduction.setSelected(true);
2661 useSiphonTrap.setSelected(false);2671 useSiphonTrap.setSelected(false);
@@ -2668,6 +2678,7 @@
2668 useGCD.setSelected(true);2678 useGCD.setSelected(true);
2669 usePTrie.setSelected(true);2679 usePTrie.setSelected(true);
2670 useOverApproximation.setSelected(true);2680 useOverApproximation.setSelected(true);
2681 useTraceRefinement.setSelected(false);
26712682
2672 useReduction.setToolTipText(TOOL_TIP_USE_STRUCTURALREDUCTION);2683 useReduction.setToolTipText(TOOL_TIP_USE_STRUCTURALREDUCTION);
2673 useSiphonTrap.setToolTipText(TOOL_TIP_USE_SIPHONTRAP);2684 useSiphonTrap.setToolTipText(TOOL_TIP_USE_SIPHONTRAP);
@@ -2680,6 +2691,7 @@
2680 useGCD.setToolTipText(TOOL_TIP_GCD);2691 useGCD.setToolTipText(TOOL_TIP_GCD);
2681 usePTrie.setToolTipText(TOOL_TIP_PTRIE);2692 usePTrie.setToolTipText(TOOL_TIP_PTRIE);
2682 useOverApproximation.setToolTipText(TOOL_TIP_OVERAPPROX);2693 useOverApproximation.setToolTipText(TOOL_TIP_OVERAPPROX);
2694 useTraceRefinement.setToolTipText(TOOL_TIP_USE_TRACE_REFINEMENT);
26832695
2684 if (lens.isTimed() || lens.isGame()) {2696 if (lens.isTimed() || lens.isGame()) {
2685 initTimedReductionOptions();2697 initTimedReductionOptions();
@@ -2765,6 +2777,9 @@
2765 gbc.gridx = 2;2777 gbc.gridx = 2;
2766 gbc.gridy = 3;2778 gbc.gridy = 3;
2767 reductionOptionsPanel.add(useStubbornReduction, gbc);2779 reductionOptionsPanel.add(useStubbornReduction, gbc);
2780 gbc.gridx = 3;
2781 gbc.gridy = 0;
2782 reductionOptionsPanel.add(useTraceRefinement, gbc);
2768 }2783 }
27692784
2770 protected void setEnabledOptionsAccordingToCurrentReduction() {2785 protected void setEnabledOptionsAccordingToCurrentReduction() {
@@ -2776,11 +2791,24 @@
2776 refreshDiscreteOptions();2791 refreshDiscreteOptions();
2777 refreshDiscreteInclusion();2792 refreshDiscreteInclusion();
2778 refreshOverApproximationOption();2793 refreshOverApproximationOption();
2794 } else if (!lens.isTimed()) {
2795 refreshTraceRefinement();
2779 }2796 }
2780 updateSearchStrategies();2797 updateSearchStrategies();
2781 refreshExportButtonText();2798 refreshExportButtonText();
2782 }2799 }
27832800
2801 private void refreshTraceRefinement() {
2802 ReductionOption reduction = getReductionOption();
2803 useTraceRefinement.setEnabled(false);
2804
2805 if (reduction != null && reduction.equals(ReductionOption.VerifyPN) && !hasInhibitorArcs &&
2806 (newProperty.toString().startsWith("AG") || newProperty.toString().startsWith("EF")) &&
2807 !newProperty.hasNestedPathQuantifiers()) {
2808 useTraceRefinement.setEnabled(true);
2809 }
2810 }
2811
2784 private void refreshDiscreteInclusion() {2812 private void refreshDiscreteInclusion() {
2785 ReductionOption reduction = getReductionOption();2813 ReductionOption reduction = getReductionOption();
2786 if(reduction == null){2814 if(reduction == null){
27872815
=== modified file 'src/resources/Example nets/train-level-crossing.tapn'
--- src/resources/Example nets/train-level-crossing.tapn 2018-07-13 18:16:32 +0000
+++ src/resources/Example nets/train-level-crossing.tapn 2021-02-22 22:26:13 +0000
@@ -112,6 +112,6 @@
112<arcpath arcPointType="false" id="1" xCoord="117" yCoord="147"/>112<arcpath arcPointType="false" id="1" xCoord="117" yCoord="147"/>
113</arc>113</arc>
114</net>114</net>
115<query active="true" approximationDenominator="2" capacity="5" discreteInclusion="false" enableOverApproximation="false" enableUnderApproximation="false" extrapolationOption="null" gcd="true" hashTableSize="null" inclusionPlaces="*NONE*" name="Crossing is Save" overApproximation="true" pTrie="true" query="AG (!(Train.DangerZone &gt; 0) or TraficLight.Red = 1)" reduction="true" reductionOption="VerifyTAPN" searchOption="HEURISTIC" symmetry="true" timeDarts="true" traceOption="NONE"/>115<query active="true" approximationDenominator="2" capacity="5" discreteInclusion="false" enableOverApproximation="false" enableUnderApproximation="false" extrapolationOption="null" gcd="true" hashTableSize="null" inclusionPlaces="*NONE*" name="Crossing is Safe" overApproximation="true" pTrie="true" query="AG (!(Train.DangerZone &gt; 0) or TraficLight.Red = 1)" reduction="true" reductionOption="VerifyTAPN" searchOption="HEURISTIC" symmetry="true" timeDarts="true" traceOption="NONE"/>
116<k-bound bound="3"/>116<k-bound bound="3"/>
117</pnml>117</pnml>

Subscribers

People subscribed via source and target branches