TAPAAL

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

  1. add-tar-option
  2. Merge into trunk
Proposed by Lena Ernstsen
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.
lp:~tapaal-contributor/tapaal/add-tar-option updated
1116. By Lena Ernstsen

Merged lp:tapaal

Revision history for this message
Kenneth Yrke Jørgensen (yrke) :
review: Approve (code)
Revision history for this message
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
lp:~tapaal-contributor/tapaal/add-tar-option updated
1117. By Lena Ernstsen

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

Revision history for this message
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
lp:~tapaal-contributor/tapaal/add-tar-option updated
1118. By Lena Ernstsen

Fixed tar only possible with AG and EF

Revision history for this message
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/verification/VerifyTAPN/VerifyPNOptions.java'
2--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java 2020-10-15 15:44:06 +0000
3+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java 2021-02-22 22:26:13 +0000
4@@ -19,26 +19,28 @@
5 private boolean useSiphontrap = false;
6 private QueryReductionTime queryReductionTime;
7 private boolean useStubbornReduction = true;
8+ private boolean useTarOption;
9 private String pathToReducedNet;
10
11 public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, ModelReduction modelReduction,
12 boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, QueryCategory queryCategory, AlgorithmOption algorithmOption,
13- boolean siphontrap, QueryReductionTime queryReduction, boolean stubbornReduction, String pathToReducedNet) {
14- super(extraTokens, traceOption, search, true, useOverApproximation, false, new InclusionPlaces(), enableOverApproximation, enableUnderApproximation, approximationDenominator);
15+ boolean siphontrap, QueryReductionTime queryReduction, boolean stubbornReduction, String pathToReducedNet, boolean useTarOption) {
16+ super(extraTokens, traceOption, search, true, useOverApproximation, false, new InclusionPlaces(), enableOverApproximation, enableUnderApproximation, approximationDenominator, useTarOption);
17 this.modelReduction = modelReduction;
18 this.queryCategory = queryCategory;
19 this.algorithmOption = algorithmOption;
20 this.useSiphontrap = siphontrap;
21 this.queryReductionTime = queryReduction;
22 this.useStubbornReduction = stubbornReduction;
23+ this.useTarOption = useTarOption;
24 this.pathToReducedNet = pathToReducedNet;
25 }
26-
27+
28 public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, boolean useModelReduction,
29 boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, QueryCategory queryCategory, AlgorithmOption algorithmOption,
30 boolean siphontrap, QueryReductionTime queryReduction, boolean stubbornReduction) {
31 this(extraTokens, traceOption, search, useOverApproximation, useModelReduction? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION, enableOverApproximation,
32- enableUnderApproximation, approximationDenominator,queryCategory, algorithmOption, siphontrap, queryReduction, stubbornReduction, null);
33+ enableUnderApproximation, approximationDenominator,queryCategory, algorithmOption, siphontrap, queryReduction, stubbornReduction, null, false);
34 }
35
36 @Override
37@@ -83,6 +85,9 @@
38 if (!this.useStubbornReduction) {
39 result.append(" -p ");
40 }
41+ if (this.useTarOption) {
42+ result.append(" -tar ");
43+ }
44 return result.toString();
45 }
46
47
48=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java'
49--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java 2020-07-13 13:58:47 +0000
50+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java 2021-02-22 22:26:13 +0000
51@@ -16,6 +16,7 @@
52 protected int tokensInModel;
53 private final boolean symmetry;
54 private final boolean discreteInclusion;
55+ private final boolean tarOption;
56 private InclusionPlaces inclusionPlaces;
57
58 //only used for boundedness analysis
59@@ -27,8 +28,12 @@
60 public VerifyTAPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean symmetry, boolean useStateequationCheck, boolean discreteInclusion, boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator) {
61 this(extraTokens,traceOption, search, symmetry, useStateequationCheck, discreteInclusion, new InclusionPlaces(), enableOverApproximation, enableUnderApproximation, approximationDenominator);
62 }
63+
64+ public VerifyTAPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean symmetry, boolean useStateequationCheck, boolean discreteInclusion, InclusionPlaces inclusionPlaces, boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator) {
65+ this(extraTokens,traceOption, search, symmetry, useStateequationCheck, discreteInclusion, new InclusionPlaces(), enableOverApproximation, enableUnderApproximation, approximationDenominator, false);
66+ }
67
68- public VerifyTAPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean symmetry, boolean useStateEquationCheck, boolean discreteInclusion, InclusionPlaces inclusionPlaces, boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator) {
69+ public VerifyTAPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean symmetry, boolean useStateEquationCheck, boolean discreteInclusion, InclusionPlaces inclusionPlaces, boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, boolean tarOption) {
70 this.extraTokens = extraTokens;
71 this.traceOption = traceOption;
72 searchOption = search;
73@@ -39,6 +44,7 @@
74 this.enabledOverApproximation = enableOverApproximation;
75 this.enabledUnderApproximation = enableUnderApproximation;
76 this.approximationDenominator = approximationDenominator;
77+ this.tarOption = tarOption;
78 }
79
80 public TraceOption trace() {
81
82=== modified file 'src/pipe/dataLayer/TAPNQuery.java'
83--- src/pipe/dataLayer/TAPNQuery.java 2020-11-06 19:41:50 +0000
84+++ src/pipe/dataLayer/TAPNQuery.java 2021-02-22 22:26:13 +0000
85@@ -72,6 +72,7 @@
86 private boolean useSiphontrap = false;
87 private boolean useQueryReduction = true;
88 private boolean useStubbornReduction = true;
89+ private boolean useTarOption = false;
90
91 /**
92 * @param name
93@@ -108,6 +109,14 @@
94 return this.useStubbornReduction;
95 }
96
97+ public boolean isTarOptionEnabled() {
98+ return this.useTarOption;
99+ }
100+
101+ public void setUseTarOption(boolean useTarOption) {
102+ this.useTarOption = useTarOption;
103+ }
104+
105 public int approximationDenominator() {
106 return this.denominator;
107 }
108@@ -361,6 +370,7 @@
109 useSiphontrap = newQuery.isSiphontrapEnabled();
110 useQueryReduction = newQuery.isQueryReductionEnabled();
111 useStubbornReduction = newQuery.isStubbornReductionEnabled();
112+ useTarOption = newQuery.isTarOptionEnabled();
113 }
114
115 public InclusionPlaces inclusionPlaces() {
116
117=== modified file 'src/pipe/gui/KBoundAnalyzer.java'
118--- src/pipe/gui/KBoundAnalyzer.java 2020-10-15 15:44:06 +0000
119+++ src/pipe/gui/KBoundAnalyzer.java 2021-02-22 22:26:13 +0000
120@@ -52,7 +52,7 @@
121
122 protected VerifyTAPNOptions verificationOptions() {
123 if(modelChecker instanceof VerifyPN){
124- 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);
125+ 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);
126 } else if(modelChecker instanceof VerifyTAPN){
127 return new VerifyTAPNOptions(k, TraceOption.NONE, SearchOption.BFS, true, false, true, false, false, 1);
128 } else if(modelChecker instanceof VerifyTAPNDiscreteVerification){
129
130=== modified file 'src/pipe/gui/RunVerificationBase.java'
131--- src/pipe/gui/RunVerificationBase.java 2020-11-11 07:55:24 +0000
132+++ src/pipe/gui/RunVerificationBase.java 2021-02-22 22:26:13 +0000
133@@ -122,7 +122,8 @@
134 dataLayerQuery.isSiphontrapEnabled(),
135 dataLayerQuery.isQueryReductionEnabled()? pipe.dataLayer.TAPNQuery.QueryReductionTime.UnlimitedTime: pipe.dataLayer.TAPNQuery.QueryReductionTime.NoTime,
136 dataLayerQuery.isStubbornReductionEnabled(),
137- reducedNetFilePath
138+ reducedNetFilePath,
139+ dataLayerQuery.isTarOptionEnabled()
140 ),
141 transformedModel,
142 clonedQuery
143@@ -143,7 +144,8 @@
144 false,
145 pipe.dataLayer.TAPNQuery.QueryReductionTime.UnlimitedTime,
146 false,
147- reducedNetFilePath
148+ reducedNetFilePath,
149+ false
150 ),
151 transformedModel,
152 clonedQuery
153
154=== modified file 'src/pipe/gui/Verifier.java'
155--- src/pipe/gui/Verifier.java 2020-11-13 10:08:54 +0000
156+++ src/pipe/gui/Verifier.java 2021-02-22 22:26:13 +0000
157@@ -176,7 +176,6 @@
158 query.isStubbornReductionEnabled()
159 );
160 } else if(query.getReductionOption() == ReductionOption.VerifyPN){
161-
162 try {
163 reducedNetTempFile = File.createTempFile("reduced-", ".pnml");
164 } catch (IOException e) {
165@@ -202,7 +201,8 @@
166 query.isSiphontrapEnabled(),
167 TAPNQuery.QueryReductionTime.NoTime,
168 query.isStubbornReductionEnabled(),
169- reducedNetTempFile.getAbsolutePath()
170+ reducedNetTempFile.getAbsolutePath(),
171+ query.isTarOptionEnabled()
172 );
173 } else {
174 verifytapnOptions = new VerifyPNOptions(
175@@ -219,10 +219,10 @@
176 query.isSiphontrapEnabled(),
177 query.isQueryReductionEnabled()? TAPNQuery.QueryReductionTime.UnlimitedTime: TAPNQuery.QueryReductionTime.NoTime,
178 query.isStubbornReductionEnabled(),
179- reducedNetTempFile.getAbsolutePath()
180+ reducedNetTempFile.getAbsolutePath(),
181+ query.isTarOptionEnabled()
182 );
183 }
184-
185 } else {
186 verifytapnOptions = new VerifyTAPNOptions(
187 bound,
188
189=== modified file 'src/pipe/gui/widgets/QueryDialog.java'
190--- src/pipe/gui/widgets/QueryDialog.java 2020-12-17 21:03:12 +0000
191+++ src/pipe/gui/widgets/QueryDialog.java 2021-02-22 22:26:13 +0000
192@@ -165,6 +165,7 @@
193 private JCheckBox useQueryReduction;
194 private JCheckBox useReduction;
195 private JCheckBox useStubbornReduction;
196+ private JCheckBox useTraceRefinement;
197
198 // Approximation options panel
199 private JPanel overApproximationOptionsPanel;
200@@ -293,6 +294,7 @@
201 private final static String TOOL_TIP_USE_STRUCTURALREDUCTION = "Apply structural reductions to reduce the size of the net.";
202 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.";
203 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.";
204+ private final static String TOOL_TIP_USE_TRACE_REFINEMENT = "Enables Trace Abstraction Refinement for reachability properties";
205
206 //Tool tips for search options panel
207 private final static String TOOL_TIP_HEURISTIC_SEARCH = "<html>Uses a heuristic method in state space exploration.<br />" +
208@@ -322,8 +324,7 @@
209 private final static String TOOL_TIP_APPROXIMATION_METHOD_UNDER = "Approximate by dividing all intervals with the approximation constant and shrinking the intervals.";
210 private final static String TOOL_TIP_APPROXIMATION_CONSTANT = "Choose approximation constant";
211
212- public QueryDialog(EscapableDialog me, QueryDialogueOption option,
213- TAPNQuery queryToCreateFrom, TimedArcPetriNetNetwork tapnNetwork, HashMap<TimedArcPetriNet, DataLayer> guiModels, TabContent.TAPNLens lens) {
214+ public QueryDialog(EscapableDialog me, QueryDialogueOption option, TAPNQuery queryToCreateFrom, TimedArcPetriNetNetwork tapnNetwork, HashMap<TimedArcPetriNet, DataLayer> guiModels, TabContent.TAPNLens lens) {
215 this.tapnNetwork = tapnNetwork;
216 this.guiModels = guiModels;
217 this.lens = lens;
218@@ -442,6 +443,7 @@
219 query.setUseSiphontrap(useSiphonTrap.isSelected());
220 query.setUseQueryReduction(useQueryReduction.isSelected());
221 query.setUseStubbornReduction(useStubbornReduction.isSelected());
222+ query.setUseTarOption(useTraceRefinement.isSelected());
223 return query;
224 }
225
226@@ -1210,8 +1212,15 @@
227 setupSearchOptionsFromQuery(queryToCreateFrom);
228 setupReductionOptionsFromQuery(queryToCreateFrom);
229 setupTraceOptionsFromQuery(queryToCreateFrom);
230+ setupTarOptionsFromQuery(queryToCreateFrom);
231 }
232
233+ private void setupTarOptionsFromQuery(TAPNQuery queryToCreateFrom) {
234+ if (queryToCreateFrom.isTarOptionEnabled()) {
235+ useTraceRefinement.setSelected(true);
236+ }
237+ }
238+
239 private void setupApproximationOptionsFromQuery(TAPNQuery queryToCreateFrom) {
240 if (queryToCreateFrom.isOverApproximationEnabled())
241 overApproximationEnable.setSelected(true);
242@@ -2656,6 +2665,7 @@
243 useGCD = new JCheckBox("Use GCD");
244 usePTrie = new JCheckBox("Use PTrie");
245 useOverApproximation = new JCheckBox("Use untimed state-equations check");
246+ useTraceRefinement = new JCheckBox("Use trace abstraction refinement");
247
248 useReduction.setSelected(true);
249 useSiphonTrap.setSelected(false);
250@@ -2668,6 +2678,7 @@
251 useGCD.setSelected(true);
252 usePTrie.setSelected(true);
253 useOverApproximation.setSelected(true);
254+ useTraceRefinement.setSelected(false);
255
256 useReduction.setToolTipText(TOOL_TIP_USE_STRUCTURALREDUCTION);
257 useSiphonTrap.setToolTipText(TOOL_TIP_USE_SIPHONTRAP);
258@@ -2680,6 +2691,7 @@
259 useGCD.setToolTipText(TOOL_TIP_GCD);
260 usePTrie.setToolTipText(TOOL_TIP_PTRIE);
261 useOverApproximation.setToolTipText(TOOL_TIP_OVERAPPROX);
262+ useTraceRefinement.setToolTipText(TOOL_TIP_USE_TRACE_REFINEMENT);
263
264 if (lens.isTimed() || lens.isGame()) {
265 initTimedReductionOptions();
266@@ -2765,6 +2777,9 @@
267 gbc.gridx = 2;
268 gbc.gridy = 3;
269 reductionOptionsPanel.add(useStubbornReduction, gbc);
270+ gbc.gridx = 3;
271+ gbc.gridy = 0;
272+ reductionOptionsPanel.add(useTraceRefinement, gbc);
273 }
274
275 protected void setEnabledOptionsAccordingToCurrentReduction() {
276@@ -2776,11 +2791,24 @@
277 refreshDiscreteOptions();
278 refreshDiscreteInclusion();
279 refreshOverApproximationOption();
280+ } else if (!lens.isTimed()) {
281+ refreshTraceRefinement();
282 }
283 updateSearchStrategies();
284 refreshExportButtonText();
285 }
286
287+ private void refreshTraceRefinement() {
288+ ReductionOption reduction = getReductionOption();
289+ useTraceRefinement.setEnabled(false);
290+
291+ if (reduction != null && reduction.equals(ReductionOption.VerifyPN) && !hasInhibitorArcs &&
292+ (newProperty.toString().startsWith("AG") || newProperty.toString().startsWith("EF")) &&
293+ !newProperty.hasNestedPathQuantifiers()) {
294+ useTraceRefinement.setEnabled(true);
295+ }
296+ }
297+
298 private void refreshDiscreteInclusion() {
299 ReductionOption reduction = getReductionOption();
300 if(reduction == null){
301
302=== modified file 'src/resources/Example nets/train-level-crossing.tapn'
303--- src/resources/Example nets/train-level-crossing.tapn 2018-07-13 18:16:32 +0000
304+++ src/resources/Example nets/train-level-crossing.tapn 2021-02-22 22:26:13 +0000
305@@ -112,6 +112,6 @@
306 <arcpath arcPointType="false" id="1" xCoord="117" yCoord="147"/>
307 </arc>
308 </net>
309-<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"/>
310+<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"/>
311 <k-bound bound="3"/>
312 </pnml>

Subscribers

People subscribed via source and target branches