TAPAAL

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

  1. save-tar-option
  2. Merge into trunk
Proposed by Lena Ernstsen
Status: Merged
Approved by: Jiri Srba
Approved revision: 1121
Merged at revision: 1120
Proposed branch: lp:~tapaal-contributor/tapaal/save-tar-option
Merge into: lp:tapaal
Diff against target: 150 lines (+35/-3)
7 files modified
src/dk/aau/cs/gui/BatchProcessingDialog.java (+4/-0)
src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java (+3/-1)
src/dk/aau/cs/io/queries/TAPNQueryLoader.java (+15/-0)
src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java (+7/-0)
src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java (+4/-2)
src/pipe/dataLayer/TAPNQuery.java (+1/-0)
src/pipe/gui/widgets/QueryDialog.java (+1/-0)
To merge this branch: bzr merge lp:~tapaal-contributor/tapaal/save-tar-option
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Review via email: mp+399026@code.launchpad.net

Commit message

The trace refinement option is saved in the .tapn file

To post a comment you must log in.
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/gui/BatchProcessingDialog.java'
2--- src/dk/aau/cs/gui/BatchProcessingDialog.java 2020-07-20 07:55:49 +0000
3+++ src/dk/aau/cs/gui/BatchProcessingDialog.java 2021-03-02 20:12:24 +0000
4@@ -1577,6 +1577,10 @@
5 s.append("Stubborn Reduction: ");
6 s.append(query.isStubbornReductionEnabled() ? "Yes\n\n" : "No\n\n");
7
8+ s.append("\n\n");
9+ s.append("Trace Abstract Refinement: ");
10+ s.append(query.isTarOptionEnabled() ? "Yes\n\n" : "No\n\n");
11+
12 s.append("Query Property:\n");
13 s.append(query.getProperty().toString());
14
15
16=== modified file 'src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java'
17--- src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java 2020-08-11 13:25:25 +0000
18+++ src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java 2021-03-02 20:12:24 +0000
19@@ -320,7 +320,8 @@
20 queryElement.setAttribute("enableOverApproximation", "" + query.isOverApproximationEnabled());
21 queryElement.setAttribute("enableUnderApproximation", "" + query.isUnderApproximationEnabled());
22 queryElement.setAttribute("approximationDenominator", "" + query.approximationDenominator());
23- queryElement.setAttribute("useStubbornReduction", "" + query.isStubbornReductionEnabled());
24+ queryElement.setAttribute("useStubbornReduction", "" + query.isStubbornReductionEnabled());
25+ queryElement.setAttribute("useTarOption", "" + query.isTarOptionEnabled());
26
27 return queryElement;
28 }
29@@ -358,6 +359,7 @@
30 queryElement.setAttribute("useSiphonTrapAnalysis", "" + query.isSiphontrapEnabled());
31 queryElement.setAttribute("useQueryReduction", "" + query.isQueryReductionEnabled());
32 queryElement.setAttribute("useStubbornReduction", "" + query.isStubbornReductionEnabled());
33+ queryElement.setAttribute("useTarOption", "" + query.isTarOptionEnabled());
34
35 return queryElement;
36 }
37
38=== modified file 'src/dk/aau/cs/io/queries/TAPNQueryLoader.java'
39--- src/dk/aau/cs/io/queries/TAPNQueryLoader.java 2020-10-31 17:27:18 +0000
40+++ src/dk/aau/cs/io/queries/TAPNQueryLoader.java 2021-03-02 20:12:24 +0000
41@@ -91,6 +91,7 @@
42 boolean siphontrap = getReductionOption(queryElement, "useSiphonTrapAnalysis", false);
43 boolean queryReduction = getReductionOption(queryElement, "useQueryReduction", true);
44 boolean stubborn = getReductionOption(queryElement, "useStubbornReduction", true);
45+ boolean useTar = getTarOption(queryElement, "useTarOption", false);
46
47 TCTLAbstractProperty query;
48 if (queryElement.getElementsByTagName("formula").item(0) != null){
49@@ -107,6 +108,7 @@
50 parsedQuery.setUseSiphontrap(siphontrap);
51 parsedQuery.setUseQueryReduction(queryReduction);
52 parsedQuery.setUseStubbornReduction(stubborn);
53+ parsedQuery.setUseTarOption(useTar);
54 if (parsedQuery.getCategory() == QueryCategory.CTL && algorithmOption != null){
55 parsedQuery.setAlgorithmOption(AlgorithmOption.valueOf(algorithmOption));
56 // RenameTemplateVisitor rt = new RenameTemplateVisitor("",
57@@ -229,6 +231,19 @@
58 }
59 return result;
60 }
61+
62+ private boolean getTarOption(Element queryElement, String attributeName, boolean defaultValue) {
63+ if(!queryElement.hasAttribute(attributeName)){
64+ return defaultValue;
65+ }
66+ boolean result;
67+ try {
68+ result = queryElement.getAttribute(attributeName).equals("true");
69+ } catch(Exception e) {
70+ result = defaultValue;
71+ }
72+ return result;
73+ }
74
75 private int getApproximationValue(Element queryElement, String attributeName, int defaultValue)
76 {
77
78=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java'
79--- src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java 2021-02-07 11:09:51 +0000
80+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java 2021-03-02 20:12:24 +0000
81@@ -43,6 +43,13 @@
82 enableUnderApproximation, approximationDenominator,queryCategory, algorithmOption, siphontrap, queryReduction, stubbornReduction, null, false);
83 }
84
85+ public VerifyPNOptions(int extraTokens, TraceOption traceOption, SearchOption search, boolean useOverApproximation, boolean useModelReduction,
86+ boolean enableOverApproximation, boolean enableUnderApproximation, int approximationDenominator, QueryCategory queryCategory, AlgorithmOption algorithmOption,
87+ boolean siphontrap, QueryReductionTime queryReduction, boolean stubbornReduction, boolean useTarOption) {
88+ this(extraTokens, traceOption, search, useOverApproximation, useModelReduction? ModelReduction.AGGRESSIVE:ModelReduction.NO_REDUCTION, enableOverApproximation,
89+ enableUnderApproximation, approximationDenominator,queryCategory, algorithmOption, siphontrap, queryReduction, stubbornReduction, null, useTarOption);
90+ }
91+
92 @Override
93 public String toString() {
94 StringBuilder result = new StringBuilder();
95
96=== modified file 'src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java'
97--- src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java 2020-10-15 15:44:06 +0000
98+++ src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java 2021-03-02 20:12:24 +0000
99@@ -356,6 +356,7 @@
100 boolean stubbornReduction = batchProcessingVerificationOptions.stubbornReductionOption() == StubbornReductionOption.KeepQueryOption ? query.isStubbornReductionEnabled() : getStubbornReductionFromBatchProcessingOptions();
101 boolean overApproximation = query.isOverApproximationEnabled();
102 boolean underApproximation = query.isUnderApproximationEnabled();
103+ boolean useTar = query.isTarOptionEnabled();
104 int approximationDenominator = query.approximationDenominator();
105 if (batchProcessingVerificationOptions.approximationMethodOption() == ApproximationMethodOption.None) {
106 overApproximation = false;
107@@ -381,6 +382,7 @@
108 changedQuery.setUseSiphontrap(query.isSiphontrapEnabled());
109 changedQuery.setUseQueryReduction(query.isQueryReductionEnabled());
110 changedQuery.setUseStubbornReduction(stubbornReduction);
111+ changedQuery.setUseTarOption(useTar);
112 return changedQuery;
113 } else if (batchProcessingVerificationOptions.queryPropertyOption() == QueryPropertyOption.Soundness) {
114 isSoundnessCheck = true;
115@@ -623,9 +625,9 @@
116 return new VerifyDTAPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), query.useSymmetry(), query.useGCD(), query.useTimeDarts(), query.usePTrie(), false, query.discreteInclusion(), query.inclusionPlaces(), query.getWorkflowMode(), 0, query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator(), query.isStubbornReductionEnabled());
117 else if(query.getReductionOption() == ReductionOption.VerifyPN || query.getReductionOption() == ReductionOption.VerifyPNApprox || query.getReductionOption() == ReductionOption.VerifyPNReduce)
118 if (batchProcessingVerificationOptions.queryPropertyOption() == QueryPropertyOption.SearchWholeStateSpace){
119- return new VerifyPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), false, false, false, false, query.approximationDenominator(), QueryCategory.Default, query.getAlgorithmOption(), false, QueryReductionTime.UnlimitedTime, false);
120+ return new VerifyPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), false, false, false, false, query.approximationDenominator(), QueryCategory.Default, query.getAlgorithmOption(), false, QueryReductionTime.UnlimitedTime, false, query.isTarOptionEnabled());
121 } else {
122- return new VerifyPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), query.useOverApproximation(), query.useReduction(), query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator(), query.getCategory(), query.getAlgorithmOption(), query.isSiphontrapEnabled(), query.isQueryReductionEnabled()? QueryReductionTime.UnlimitedTime: QueryReductionTime.NoTime, query.isStubbornReductionEnabled());
123+ return new VerifyPNOptions(query.getCapacity(), TraceOption.NONE, query.getSearchOption(), query.useOverApproximation(), query.useReduction(), query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator(), query.getCategory(), query.getAlgorithmOption(), query.isSiphontrapEnabled(), query.isQueryReductionEnabled()? QueryReductionTime.UnlimitedTime: QueryReductionTime.NoTime, query.isStubbornReductionEnabled(), query.isTarOptionEnabled());
124 }
125 else
126 return new VerifytaOptions(TraceOption.NONE, query.getSearchOption(), false, query.getReductionOption(), query.useSymmetry(), false, query.isOverApproximationEnabled(), query.isUnderApproximationEnabled(), query.approximationDenominator());
127
128=== modified file 'src/pipe/dataLayer/TAPNQuery.java'
129--- src/pipe/dataLayer/TAPNQuery.java 2021-02-07 11:09:51 +0000
130+++ src/pipe/dataLayer/TAPNQuery.java 2021-03-02 20:12:24 +0000
131@@ -393,6 +393,7 @@
132 copy.setUseSiphontrap(this.isQueryReductionEnabled());
133 copy.setUseQueryReduction(this.isQueryReductionEnabled());
134 copy.setUseStubbornReduction(this.isStubbornReductionEnabled());
135+ copy.setUseTarOption(this.isTarOptionEnabled());
136
137 return copy;
138 }
139
140=== modified file 'src/pipe/gui/widgets/QueryDialog.java'
141--- src/pipe/gui/widgets/QueryDialog.java 2021-02-22 22:26:01 +0000
142+++ src/pipe/gui/widgets/QueryDialog.java 2021-03-02 20:12:24 +0000
143@@ -1292,6 +1292,7 @@
144 useQueryReduction.setSelected(queryToCreateFrom.isQueryReductionEnabled());
145 useStubbornReduction.setSelected(queryToCreateFrom.isStubbornReductionEnabled());
146 useReduction.setSelected(queryToCreateFrom.useReduction());
147+ useTraceRefinement.setSelected(queryToCreateFrom.isTarOptionEnabled());
148 }
149
150 private void setupTraceOptionsFromQuery(TAPNQuery queryToCreateFrom) {

Subscribers

People subscribed via source and target branches