TAPAAL

Merge lp:~yrke/tapaal/tapaal-fix-1756865 into lp:tapaal/3.4

  1. tapaal-fix-1756865
  2. Merge into 3.4
Proposed by Kenneth Yrke Jørgensen
Status: Merged
Approved by: Jiri Srba
Approved revision: 953
Merge reported by: Jiri Srba
Merged at revision: not available
Proposed branch: lp:~yrke/tapaal/tapaal-fix-1756865
Merge into: lp:tapaal/3.4
Diff against target: 300 lines (+83/-13)
6 files modified
src/dk/aau/cs/gui/BatchProcessingDialog.java (+48/-2)
src/dk/aau/cs/verification/batchProcessing/BatchProcessingVerificationOptions.java (+13/-3)
src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java (+8/-2)
src/pipe/dataLayer/TAPNQuery.java (+3/-3)
src/pipe/gui/CreateGui.java (+5/-1)
src/pipe/gui/GuiFrame.java (+6/-2)
To merge this branch: bzr merge lp:~yrke/tapaal/tapaal-fix-1756865
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Review via email: mp+342957@code.launchpad.net

Commit message

Fixes bug lp:1756865, SpecialMacHandler not working in Java9

To post a comment you must log in.
Revision history for this message
Jiri Srba (srba) wrote :

The proposal to merge for 3.4 suggests to merge a new feature that should be only
in trunk and not in 3.4. Otherwise it works and on my mac with Java 9 it is usable
(though not pretty). I get the following warnings though, but not related to this fix.

WARNING: An illegal reflective access operation has occurred
WARNING: Illegal reflective access by dk.aau.cs.util.MemoryMonitor (file:/Users/srba/dev/tapaal-fix-1756865/release-version/) to field java.lang.ProcessImpl.pid
WARNING: Please consider reporting this to the maintainers of dk.aau.cs.util.MemoryMonitor
WARNING: Use --illegal-access=warn to enable warnings of further illegal reflective access operations
WARNING: All illegal access operations will be denied in a future release

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 2017-06-07 13:20:08 +0000
3+++ src/dk/aau/cs/gui/BatchProcessingDialog.java 2018-04-10 17:59:18 +0000
4@@ -84,6 +84,7 @@
5 import dk.aau.cs.verification.batchProcessing.BatchProcessingVerificationOptions.ApproximationMethodOption;
6 import dk.aau.cs.verification.batchProcessing.BatchProcessingVerificationOptions.QueryPropertyOption;
7 import dk.aau.cs.verification.batchProcessing.BatchProcessingVerificationOptions.SymmetryOption;
8+import dk.aau.cs.verification.batchProcessing.BatchProcessingVerificationOptions.StubbornReductionOption;
9 import dk.aau.cs.verification.batchProcessing.BatchProcessingVerificationResult;
10 import dk.aau.cs.verification.batchProcessing.BatchProcessingWorker;
11 import dk.aau.cs.verification.batchProcessing.FileChangedEvent;
12@@ -141,9 +142,11 @@
13 private static final String name_Random = "Random search";
14 private static final String name_KeepQueryOption = "Do not override";
15 private static final String name_SEARCHWHOLESTATESPACE = "Search whole state space";
16- private static final String name_EXISTDEADLOCK = "Existence of a deadlock";
17+ private static final String name_EXISTDEADLOCK = "Existence of a deadlock";
18 private static final String name_SYMMETRY = "Yes";
19 private static final String name_NOSYMMETRY = "No";
20+ private static final String name_STUBBORNREUDCTION = "Yes";
21+ private static final String name_NOSTUBBORNREDUCTION = "No";
22 private static final String name_NONE_APPROXIMATION = "None";
23 private static final String name_OVER_APPROXIMATION = "Over-approximation";
24 private static final String name_UNDER_APPROXIMATION = "Under-approximation";
25@@ -164,6 +167,8 @@
26 private final static String TOOL_TIP_SearchOption = "Choose to override the search options in the nets";
27 private final static String TOOL_TIP_SymmetryLabel = null;
28 private final static String TOOL_TIP_SymmetryOption = "Choose to override the symmetry reduction in the nets";
29+ private final static String TOOL_TIP_StubbornReductionLabel = null;
30+ private final static String TOOL_TIP_StubbornReductionOption = "Apply partial order reduction (only for EF and AG queries and when Time Darts are disabled)";
31 private final static String TOOL_TIP_ReductionLabel = null;
32 private final static String TOOL_TIP_ReductionOption = "Choose to override the verification methods in the nets";
33 private final static String TOOL_TIP_TimeoutLabel = null;
34@@ -228,6 +233,7 @@
35 private CustomJSpinner numberOfExtraTokensInNet;
36 private JCheckBox keepQueryCapacity;
37 private JComboBox symmetryOption;
38+ private JComboBox stubbornReductionOption;
39 private JCheckBox noTimeoutCheckbox;
40 private JCheckBox noOOMCheckbox;
41 private CustomJSpinner timeoutValue;
42@@ -506,6 +512,7 @@
43 initQueryPropertyOptionsComponents();
44 initSearchOptionsComponents();
45 initSymmetryOptionsComponents();
46+ initStubbornReductionOptionsComponents();
47 initReductionOptionsComponents();
48 initCapacityComponents();
49 initTimeoutComponents();
50@@ -815,6 +822,31 @@
51 gbc.gridwidth = 2;
52 verificationOptionsPanel.add(symmetryOption, gbc);
53 }
54+
55+ private void initStubbornReductionOptionsComponents() {
56+ JLabel stubbornReductionLabel = new JLabel("Stubborn Reduction:");
57+ stubbornReductionLabel.setToolTipText(TOOL_TIP_StubbornReductionLabel);
58+ GridBagConstraints gbc = new GridBagConstraints();
59+ gbc.gridx = 0;
60+ gbc.gridy = 3;
61+ gbc.insets = new Insets(0, 0, 5, 0);
62+ gbc.anchor = GridBagConstraints.WEST;
63+ verificationOptionsPanel.add(stubbornReductionLabel, gbc);
64+
65+ String[] options = new String[] { name_KeepQueryOption, name_STUBBORNREUDCTION,
66+ name_NOSTUBBORNREDUCTION };
67+ stubbornReductionOption = new JComboBox(options);
68+ stubbornReductionOption.setToolTipText(TOOL_TIP_StubbornReductionOption);
69+
70+ gbc = new GridBagConstraints();
71+ gbc.fill = GridBagConstraints.HORIZONTAL;
72+ gbc.gridx = 1;
73+ gbc.gridy = 3;
74+ gbc.anchor = GridBagConstraints.WEST;
75+ gbc.insets = new Insets(0, 0, 5, 0);
76+ gbc.gridwidth = 2;
77+ verificationOptionsPanel.add(stubbornReductionOption, gbc);
78+ }
79
80 private SearchOption getSearchOption() {
81 if (((String) searchOption.getSelectedItem()).equals(name_DFS))
82@@ -851,7 +883,7 @@
83
84 return new BatchProcessingVerificationOptions(getQueryPropertyOption(),
85 keepQueryCapacity.isSelected(), getNumberOfExtraTokens(),
86- getSearchOption(), getSymmetryOption(), reductionOption,
87+ getSearchOption(), getSymmetryOption(), getStubbornReductionOption(), reductionOption,
88 reductionOptionChooser.isDiscreteInclusion(), reductionOptionChooser.useTimeDartsPTrie(), reductionOptionChooser.useTimeDarts(),
89 reductionOptionChooser.usePTrie(), getApproximationMethodOption(), getApproximationDenominator(), reductionOptionChooser.getChoosenOptions());
90 }
91@@ -869,6 +901,16 @@
92 else
93 return SymmetryOption.KeepQueryOption;
94 }
95+
96+ private StubbornReductionOption getStubbornReductionOption(){
97+ String stubbornReductionString = (String) stubbornReductionOption.getSelectedItem();
98+ if (stubbornReductionString.equals(name_STUBBORNREUDCTION))
99+ return StubbornReductionOption.Yes;
100+ else if (stubbornReductionString.equals(name_NOSTUBBORNREDUCTION))
101+ return StubbornReductionOption.No;
102+ else
103+ return StubbornReductionOption.KeepQueryOption;
104+ }
105
106 private QueryPropertyOption getQueryPropertyOption() {
107 String propertyOptionString = (String) queryPropertyOption.getSelectedItem();
108@@ -1567,6 +1609,10 @@
109 s.append("\n\n");
110 s.append("Symmetry: ");
111 s.append(query.useSymmetry() ? "Yes\n\n" : "No\n\n");
112+
113+ s.append("\n\n");
114+ s.append("Stubborn Reduction: ");
115+ s.append(query.isStubbornReductionEnabled() ? "Yes\n\n" : "No\n\n");
116
117 s.append("Query Property:\n");
118 s.append(query.getProperty().toString());
119
120=== modified file 'src/dk/aau/cs/verification/batchProcessing/BatchProcessingVerificationOptions.java'
121--- src/dk/aau/cs/verification/batchProcessing/BatchProcessingVerificationOptions.java 2014-07-12 14:57:21 +0000
122+++ src/dk/aau/cs/verification/batchProcessing/BatchProcessingVerificationOptions.java 2018-04-10 17:59:18 +0000
123@@ -15,6 +15,10 @@
124 public enum SymmetryOption {
125 KeepQueryOption, Yes, No
126 };
127+
128+ public enum StubbornReductionOption{
129+ KeepQueryOption, Yes, No
130+ };
131
132 public enum ApproximationMethodOption {
133 KeepQueryOption, None, OverApproximation, UnderApproximation
134@@ -25,6 +29,7 @@
135 private SearchOption searchOption;
136 private QueryPropertyOption queryPropertyOption;
137 private SymmetryOption symmetryOption;
138+ private StubbornReductionOption stubbornReductionOption;
139 private ApproximationMethodOption approximationMethodOption;
140 private int approximationDenominator = 0;
141 private boolean keepQueryCapacity;
142@@ -34,13 +39,14 @@
143 private boolean useTimeDart = false;
144 private boolean usePTrie = false;
145
146- public BatchProcessingVerificationOptions(QueryPropertyOption queryPropertyOption, boolean keepQueryCapacity, int capacity, SearchOption searchOption, SymmetryOption symmetryOption, ReductionOption reductionOption, boolean discreteInclusion,
147+ public BatchProcessingVerificationOptions(QueryPropertyOption queryPropertyOption, boolean keepQueryCapacity, int capacity, SearchOption searchOption, SymmetryOption symmetryOption, StubbornReductionOption stubbornReductionOption, ReductionOption reductionOption, boolean discreteInclusion,
148 boolean useTimeDartPTrie, boolean useTimeDart, boolean usePTrie, ApproximationMethodOption approximationMethodOption, int approximationDenominator, List<ReductionOption> reductionOptions) {
149 Require.that(!(reductionOptions == null && reductionOption == ReductionOption.BatchProcessingUserDefinedReductions), "ReductionOption was given as userdefined but a list of reductionoptions was not given");
150 this.searchOption = searchOption;
151 this.reductionOption = reductionOption;
152 this.queryPropertyOption = queryPropertyOption;
153 this.symmetryOption = symmetryOption;
154+ this.stubbornReductionOption = stubbornReductionOption;
155 this.keepQueryCapacity = keepQueryCapacity;
156 this.capacity = capacity;
157 this.discreteInclusion = discreteInclusion;
158@@ -52,9 +58,9 @@
159 this.approximationDenominator = approximationDenominator;
160 }
161
162- public BatchProcessingVerificationOptions(QueryPropertyOption queryPropertyOption, boolean keepQueryCapacity, int capacity, SearchOption searchOption, SymmetryOption symmetryOption, ReductionOption reductionOption, boolean discreteInclusion,
163+ public BatchProcessingVerificationOptions(QueryPropertyOption queryPropertyOption, boolean keepQueryCapacity, int capacity, SearchOption searchOption, SymmetryOption symmetryOption, StubbornReductionOption stubbornReductionOption, ReductionOption reductionOption, boolean discreteInclusion,
164 boolean useTimeDartPTrie, boolean useTimeDart, boolean usePTrie, ApproximationMethodOption approximationMethodOption, int approximationRValue) {
165- this(queryPropertyOption, keepQueryCapacity, capacity, searchOption, symmetryOption, reductionOption, discreteInclusion, useTimeDartPTrie, useTimeDart, usePTrie, approximationMethodOption, approximationRValue, null);
166+ this(queryPropertyOption, keepQueryCapacity, capacity, searchOption, symmetryOption, stubbornReductionOption, reductionOption, discreteInclusion, useTimeDartPTrie, useTimeDart, usePTrie, approximationMethodOption, approximationRValue, null);
167 }
168
169 public boolean isReductionOptionUserdefined(){
170@@ -93,6 +99,10 @@
171 public SymmetryOption symmetry() {
172 return symmetryOption;
173 }
174+
175+ public StubbornReductionOption stubbornReductionOption(){
176+ return stubbornReductionOption;
177+ }
178
179 public boolean KeepCapacityFromQuery() {
180 return keepQueryCapacity;
181
182=== modified file 'src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java'
183--- src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java 2017-12-22 21:19:54 +0000
184+++ src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java 2018-04-10 17:59:18 +0000
185@@ -53,6 +53,7 @@
186 import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNOptions;
187 import dk.aau.cs.verification.batchProcessing.BatchProcessingVerificationOptions.ApproximationMethodOption;
188 import dk.aau.cs.verification.batchProcessing.BatchProcessingVerificationOptions.QueryPropertyOption;
189+import dk.aau.cs.verification.batchProcessing.BatchProcessingVerificationOptions.StubbornReductionOption;
190 import dk.aau.cs.verification.batchProcessing.BatchProcessingVerificationOptions.SymmetryOption;
191 import pipe.dataLayer.TAPNQuery.QueryCategory;
192
193@@ -259,6 +260,7 @@
194 name = query.getName();
195 }
196 boolean symmetry = batchProcessingVerificationOptions.symmetry() == SymmetryOption.KeepQueryOption ? query.useSymmetry() : getSymmetryFromBatchProcessingOptions();
197+ boolean stubbornReduction = batchProcessingVerificationOptions.stubbornReductionOption() == StubbornReductionOption.KeepQueryOption ? query.isStubbornReductionEnabled() : getStubbornReductionFromBatchProcessingOptions();
198 int capacity = batchProcessingVerificationOptions.KeepCapacityFromQuery() ? query.getCapacity() : batchProcessingVerificationOptions.capacity();
199 boolean overApproximation = query.isOverApproximationEnabled();
200 boolean underApproximation = query.isUnderApproximationEnabled();
201@@ -281,12 +283,12 @@
202
203 if(batchProcessingVerificationOptions.queryPropertyOption() == QueryPropertyOption.KeepQueryOption)
204 changedQuery.setActive(query.isActive());
205-
206+
207 changedQuery.setCategory(query.getCategory());
208 changedQuery.setAlgorithmOption(query.getAlgorithmOption());
209 changedQuery.setUseSiphontrap(query.isSiphontrapEnabled());
210 changedQuery.setUseQueryReduction(query.isQueryReductionEnabled());
211- changedQuery.setUseStubbornReduction(query.isStubbornReductionEnabled());
212+ changedQuery.setUseStubbornReduction(stubbornReduction);
213 return changedQuery;
214 }
215
216@@ -296,6 +298,10 @@
217 private boolean getSymmetryFromBatchProcessingOptions() {
218 return batchProcessingVerificationOptions.symmetry() == SymmetryOption.Yes;
219 }
220+
221+ private boolean getStubbornReductionFromBatchProcessingOptions(){
222+ return batchProcessingVerificationOptions.stubbornReductionOption() == StubbornReductionOption.Yes;
223+ }
224
225 private Tuple<TimedArcPetriNet, NameMapping> composeModel(LoadedBatchProcessingModel model) {
226 ITAPNComposer composer = new TAPNComposer(new Messenger(){
227
228=== modified file 'src/pipe/dataLayer/TAPNQuery.java'
229--- src/pipe/dataLayer/TAPNQuery.java 2017-05-17 20:32:38 +0000
230+++ src/pipe/dataLayer/TAPNQuery.java 2018-04-10 17:59:18 +0000
231@@ -192,7 +192,7 @@
232
233 public boolean useSymmetry() {
234 return symmetry;
235- }
236+ }
237
238 public boolean useGCD(){
239 return gcd;
240@@ -278,7 +278,7 @@
241
242 public TAPNQuery(String name, int capacity, TCTLAbstractProperty property,
243 TraceOption traceOption, SearchOption searchOption,
244- ReductionOption reductionOption, boolean symmetry,boolean gcd, boolean timeDart, boolean pTrie, boolean overApproximation, HashTableSize hashTabelSize,
245+ ReductionOption reductionOption, boolean symmetry, boolean gcd, boolean timeDart, boolean pTrie, boolean overApproximation, HashTableSize hashTabelSize,
246 ExtrapolationOption extrapolationOption, WorkflowMode workflow) {
247 this(name, capacity, property, traceOption, searchOption, reductionOption, symmetry, gcd, timeDart, pTrie, overApproximation, false, hashTabelSize, extrapolationOption, new InclusionPlaces());
248 this.setWorkflowMode(workflow);
249@@ -286,7 +286,7 @@
250
251 public TAPNQuery(String name, int capacity, TCTLAbstractProperty property,
252 TraceOption traceOption, SearchOption searchOption,
253- ReductionOption reductionOption, boolean symmetry,boolean gcd, boolean timeDart, boolean pTrie, boolean overApproximation, HashTableSize hashTabelSize,
254+ ReductionOption reductionOption, boolean symmetry, boolean gcd, boolean timeDart, boolean pTrie, boolean overApproximation, HashTableSize hashTabelSize,
255 ExtrapolationOption extrapolationOption, WorkflowMode workflow, long strongSoundnessBound) {
256 this(name, capacity, property, traceOption, searchOption, reductionOption, symmetry, gcd, timeDart, pTrie, overApproximation, hashTabelSize, extrapolationOption, workflow);
257 this.setStrongSoundnessBound(strongSoundnessBound);
258
259=== modified file 'src/pipe/gui/CreateGui.java'
260--- src/pipe/gui/CreateGui.java 2016-10-06 20:08:50 +0000
261+++ src/pipe/gui/CreateGui.java 2018-04-10 17:59:18 +0000
262@@ -122,7 +122,11 @@
263 appGui = new GuiFrame(TAPAAL.getProgramName());
264
265 if (appGui.isMac()){
266- SpecialMacHandler.postprocess();
267+ try {
268+ SpecialMacHandler.postprocess();
269+ } catch (NoClassDefFoundError e) {
270+ //Failed loading special mac handler, ignore and run program without MacOS integration
271+ }
272 }
273
274 Grid.enableGrid();
275
276=== modified file 'src/pipe/gui/GuiFrame.java'
277--- src/pipe/gui/GuiFrame.java 2018-01-13 20:58:46 +0000
278+++ src/pipe/gui/GuiFrame.java 2018-04-10 17:59:18 +0000
279@@ -216,7 +216,11 @@
280 }
281
282 if (isMac()){
283- new SpecialMacHandler();
284+ try {
285+ new SpecialMacHandler();
286+ } catch (NoClassDefFoundError e) {
287+ //Failed loading special mac handler, ignore and run program without MacOS integration
288+ }
289 }
290
291 this.setIconImage(new ImageIcon(Thread.currentThread().getContextClassLoader().getResource(CreateGui.imgPath + "icon.png")).getImage());
292@@ -2456,7 +2460,7 @@
293 buffer.append("TAPAAL GUI and Translations:\n");
294 buffer.append("Mathias Andersen, Sine V. Birch, Joakim Byg, Jakob Dyhr, Louise Foshammer,\nMalte Neve-Graesboell, ");
295 buffer.append("Lasse Jacobsen, Morten Jacobsen, Thomas S. Jacobsen,\nJacob J. Jensen, Peter G. Jensen, ");
296- buffer.append("Mads Johannsen, Kenneth Y. Joergensen,\nMikael H. Moeller, Christoffer Moesgaard, Niels N. Samuelsen, Jiri Srba,\nMathias G. Soerensen and Jakob H. Taankvist\n");
297+ buffer.append("Mads Johannsen, Kenneth Y. Joergensen,\nMikael H. Moeller, Christoffer Moesgaard, Niels N. Samuelsen, Jiri Srba,\nMathias G. Soerensen, Jakob H. Taankvist and Peter H. Taankvist\n");
298 buffer.append("Aalborg University 2009-2018\n\n");
299 buffer.append("TAPAAL Continuous Engine (verifytapn):\n");
300 buffer.append("Alexandre David, Lasse Jacobsen, Morten Jacobsen and Jiri Srba\n");

Subscribers

People subscribed via source and target branches