Merge lp:~ptaank/tapaal/run-multiple-queries- into lp:tapaal
- run-multiple-queries-
- Merge into trunk
Status: | Merged | ||||
---|---|---|---|---|---|
Approved by: | Jiri Srba | ||||
Approved revision: | 960 | ||||
Merged at revision: | 954 | ||||
Proposed branch: | lp:~ptaank/tapaal/run-multiple-queries- | ||||
Merge into: | lp:tapaal | ||||
Diff against target: |
553 lines (+197/-61) 6 files modified
src/dk/aau/cs/gui/BatchProcessingDialog.java (+55/-6) src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java (+9/-1) src/pipe/gui/GuiFrame.java (+25/-10) src/pipe/gui/undo/RemoveQueriesCommand.java (+32/-0) src/pipe/gui/undo/RemoveQueryCommand.java (+0/-22) src/pipe/gui/widgets/QueryPane.java (+76/-22) |
||||
To merge this branch: | bzr merge lp:~ptaank/tapaal/run-multiple-queries- | ||||
Related bugs: |
|
Reviewer | Review Type | Date Requested | Status |
---|---|---|---|
Jiri Srba | Approve | ||
Peter Haahr Taankvist (community) | Needs Resubmitting | ||
Review via email: mp+340078@code.launchpad.net |
This proposal supersedes a proposal from 2018-02-27.
Commit message
Description of the change
Fixed:
The list used for showing the queries is now reset properly after batch processing has been run, so it shows all the original queries.
The 'unnecessary update' is because when the queries are selected, the queries not selected are removed from the net, then the net is saved in the temporary file and batch processing is run, and they are re-added after batchprocessing is closed.
Jiri Srba (srba) wrote : Posted in a previous version of this proposal | # |
Jiri Srba (srba) wrote : | # |
There are two issues before we can merge it to trunk:
1. Once you run multiple queries, the name of the net is changed (some long number is appended) every time you run the multiple queries. After we return from batch processing, the name of the net is still modified.
2. If you have three queries and select only two of them, once you enter the batch processing,
the non-selected query disappears temporarily from the list and reappears after batch processing is closed.
Jiri Srba (srba) wrote : | # |
And I still get this warning:
objc[29737]: Class FIFinderSyncExt
Peter Haahr Taankvist (ptaank) wrote : | # |
As far as I can see it's a problem with high Sierra, and therefore not
something I can do anything about :/
However, most people say it's harmless..
Peter
On 9 Mar 2018 08.25, "Jiri Srba" <email address hidden> wrote:
> And I still get this warning:
>
> objc[29737]: Class FIFinderSyncExt
> /System/
> (0x7fff91849b68) and /System/
> FileProvider.
> viderOverride.
> (0x13eec1cd8). One of the two will be used. Which one is undefined.
> --
> https:/
> queries-
> You are the owner of lp:~ptaank/tapaal/run-multiple-queries-.
>
- 956. By Peter Taankvist <email address hidden>
-
Made new save method for run multiple queries
Peter Haahr Taankvist (ptaank) wrote : | # |
Made new method for saving specifically for when selecting multiple queries in GuiFrame.
Difference from other method: Does not set a new tab name. Does not reset undos and redos.
Deleted some methods which were unnecessary after the creation of the new method.
Jiri Srba (srba) wrote : | # |
Tested and works very nice and as expected, I only found one issue:
Make a new net, do not save it and run multiquery verification. Once finished,
press do "Save" and the temporary file name gets appended to the net. Repeat
the multi query verification, return to the editor and save the net and now again
the file name gets longer with additional random string etc.
Also, it would be nice if in the batch processing the name of the net in the results overview
was without the appended random string (try to hide it somehow).
- 957. By Peter Taankvist <email address hidden>
-
Refactor of save method and modelname fixed in results
Peter Haahr Taankvist (ptaank) wrote : | # |
I refactored the new save method, saveNet, so it is only when you actually save the net that the GUI changes, meaning that it is not affected by running multiple queries.
Made condition that the filename cannot be that of the temporary file.(Very small likelihood that the user names a file that of the temporary file) If it is it uses the name of the current tab.
Jiri Srba (srba) wrote : | # |
Works just fine, just remove please also the tmp file name in Monitor, Net:
It is still shown there.
Jiri Srba (srba) wrote : | # |
And one more problem, the classical batch processing is broken now.
Just load a few models, click verify and nothing happens - the batch processing
does not start.
- 958. By Peter Taankvist <email address hidden>
-
Fix Monitor, net and NullPointerExce
ption
Peter Haahr Taankvist (ptaank) wrote : | # |
Batch processing didn't start because of a Null Pointer Exception which is now handled.
Monitor, Net now shows the current tabname instead of the name of the tempfile
Jiri Srba (srba) wrote : | # |
Tested again and discovered two more issues:
1. The moving up and down of queries using the arrows to the right of the query panel,
as well as sorting the alphabetically is broken in the current version.
2. The batch file dialog does not remember the most recently opened folder
but it should always open in the most recently open one (maybe this issues was already
present in the earlier version of trunk.
Peter Haahr Taankvist (ptaank) wrote : | # |
1. should be fixed now
2. Added lastpath to filebrowser so it opens the same place you were before. (This bug is present in current release)
Jiri Srba (srba) wrote : | # |
Approved as it works as expected now.
Preview Diff
1 | === modified file 'src/dk/aau/cs/gui/BatchProcessingDialog.java' |
2 | --- src/dk/aau/cs/gui/BatchProcessingDialog.java 2018-02-11 13:28:38 +0000 |
3 | +++ src/dk/aau/cs/gui/BatchProcessingDialog.java 2018-04-09 08:31:59 +0000 |
4 | @@ -66,6 +66,7 @@ |
5 | import pipe.gui.widgets.CustomJSpinner; |
6 | import pipe.gui.widgets.EscapableDialog; |
7 | import pipe.gui.widgets.FileBrowser; |
8 | +import pipe.gui.widgets.QueryPane; |
9 | import pipe.gui.widgets.InclusionPlaces.InclusionPlacesOption; |
10 | import dk.aau.cs.gui.components.BatchProcessingResultsTableModel; |
11 | import dk.aau.cs.gui.components.MultiLineAutoWrappingToolTip; |
12 | @@ -241,6 +242,7 @@ |
13 | private JComboBox approximationMethodOption; |
14 | private CustomJSpinner approximationDenominator; |
15 | private JCheckBox approximationDenominatorCheckbox; |
16 | + private JList ListOfQueries; |
17 | |
18 | private Timer timeoutTimer = new Timer(30000, new ActionListener() { |
19 | public void actionPerformed(ActionEvent e) { |
20 | @@ -318,9 +320,16 @@ |
21 | |
22 | static BatchProcessingDialog batchProcessingDialog; |
23 | |
24 | - public static void showBatchProcessingDialog(){ |
25 | + /* ListOfQueries is used throughout the class to check if |
26 | + BatchProcessing was called from QueryPane |
27 | + (should maybe be boolean) |
28 | + */ |
29 | + public static void showBatchProcessingDialog(JList ListOfQueries){ |
30 | + if(ListOfQueries.getModel().getSize() != 0) { |
31 | + batchProcessingDialog = null; |
32 | + } |
33 | if(batchProcessingDialog == null){ |
34 | - batchProcessingDialog = new BatchProcessingDialog(CreateGui.getApp(), "Batch Processing", true); |
35 | + batchProcessingDialog = new BatchProcessingDialog(CreateGui.getApp(), "Batch Processing", true, ListOfQueries); |
36 | batchProcessingDialog.pack(); |
37 | batchProcessingDialog.setPreferredSize(batchProcessingDialog.getSize()); |
38 | //Set the minimum size to 150 less than the preferred, to be consistent with the minimum size of the result panel |
39 | @@ -331,16 +340,24 @@ |
40 | batchProcessingDialog.setVisible(true); |
41 | } |
42 | |
43 | - private BatchProcessingDialog(Frame frame, String title, boolean modal) { |
44 | + private BatchProcessingDialog(Frame frame, String title, boolean modal, JList ListOfQueries) { |
45 | super(frame, title, modal); |
46 | |
47 | addWindowListener(new WindowAdapter() { |
48 | public void windowClosing(WindowEvent we) { |
49 | + if(!(isQueryListEmpty())) { |
50 | + batchProcessingDialog = null; |
51 | + } |
52 | terminateBatchProcessing(); |
53 | } |
54 | }); |
55 | + this.ListOfQueries = ListOfQueries; |
56 | |
57 | initComponents(); |
58 | + //Runs the BatchProcessing if it is called from the QueryPane |
59 | + if(!(isQueryListEmpty())) { |
60 | + process(); |
61 | + } |
62 | } |
63 | |
64 | private void initComponents() { |
65 | @@ -353,6 +370,7 @@ |
66 | initVerificationOptionsPanel(); |
67 | initMonitorPanel(); |
68 | initResultTablePanel(); |
69 | + setFileListToTempFile(); |
70 | |
71 | splitpane = new JSplitPane(JSplitPane.VERTICAL_SPLIT, topPanel, bottomPanel); |
72 | splitpane.setResizeWeight(0); |
73 | @@ -360,6 +378,19 @@ |
74 | splitpane.setContinuousLayout(true); |
75 | setContentPane(splitpane); |
76 | } |
77 | + |
78 | + private void setFileListToTempFile() { |
79 | + if(!(isQueryListEmpty())) { |
80 | + files.add(QueryPane.getTemporaryFile()); |
81 | + } |
82 | + } |
83 | + |
84 | + private boolean isQueryListEmpty() { |
85 | + if(ListOfQueries.getModel().getSize() == 0) |
86 | + return true; |
87 | + else |
88 | + return false; |
89 | + } |
90 | |
91 | private void initFileListPanel() { |
92 | JPanel fileListPanel = new JPanel(new GridBagLayout()); |
93 | @@ -474,10 +505,14 @@ |
94 | gbc.gridheight = 2; |
95 | gbc.insets = new Insets(10, 5, 0, 5); |
96 | topPanel.add(fileListPanel, gbc); |
97 | + //Hides the file list panel if batch processing is run from the tabcomponent |
98 | + if(!(isQueryListEmpty())) { |
99 | + fileListPanel.setVisible(false); |
100 | + } |
101 | } |
102 | |
103 | private void addFiles() { |
104 | - FileBrowser browser = new FileBrowser("Timed-Arc Petri Nets","xml"); |
105 | + FileBrowser browser = new FileBrowser("Timed-Arc Petri Nets","xml", lastPath); |
106 | |
107 | File[] filesArray = browser.openFiles(); |
108 | if (filesArray.length>0) { |
109 | @@ -528,6 +563,10 @@ |
110 | gbc.weightx = 0; |
111 | gbc.insets = new Insets(10, 0, 0, 5); |
112 | topPanel.add(verificationOptionsPanel, gbc); |
113 | + //Hides the verification options if batch processing is run from the tabcomponent |
114 | + if(!(isQueryListEmpty())) { |
115 | + verificationOptionsPanel.setVisible(false); |
116 | + } |
117 | } |
118 | |
119 | private void initQueryPropertyOptionsComponents() { |
120 | @@ -967,6 +1006,11 @@ |
121 | private void exit() { |
122 | terminateBatchProcessing(); |
123 | rootPane.getParent().setVisible(false); |
124 | + //resets batch processing when exiting |
125 | + //if batch processing was called from the tab |
126 | + if(!(isQueryListEmpty())){ |
127 | + batchProcessingDialog = null; |
128 | + } |
129 | } |
130 | |
131 | private void initResultTablePanel() { |
132 | @@ -982,10 +1026,11 @@ |
133 | } |
134 | |
135 | private void exportResults() { |
136 | - String filename = new FileBrowser("CSV file", "csv") |
137 | + String filename = new FileBrowser("CSV file", "csv", lastPath) |
138 | .saveFile("results"); |
139 | if (filename != null) { |
140 | File exportFile = new File(filename); |
141 | + lastPath = exportFile.getParent(); |
142 | BatchProcessingResultsExporter exporter = new BatchProcessingResultsExporter(); |
143 | try { |
144 | exporter.exportToCSV(tableModel.getResults(), |
145 | @@ -1338,7 +1383,11 @@ |
146 | } |
147 | |
148 | public void fireFileChanged(FileChangedEvent e) { |
149 | - fileStatusLabel.setText(e.fileName()); |
150 | + if(!(isQueryListEmpty())) { |
151 | + fileStatusLabel.setText(CreateGui.appGui.getCurrentTabName()); |
152 | + } |
153 | + else |
154 | + fileStatusLabel.setText(e.fileName()); |
155 | } |
156 | |
157 | }); |
158 | |
159 | === modified file 'src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java' |
160 | --- src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java 2018-02-11 13:28:38 +0000 |
161 | +++ src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java 2018-04-09 08:31:59 +0000 |
162 | @@ -8,8 +8,10 @@ |
163 | |
164 | import pipe.dataLayer.TAPNQuery.SearchOption; |
165 | import pipe.dataLayer.TAPNQuery.TraceOption; |
166 | +import pipe.gui.CreateGui; |
167 | import pipe.gui.FileFinderImpl; |
168 | import pipe.gui.MessengerImpl; |
169 | +import pipe.gui.widgets.QueryPane; |
170 | import dk.aau.cs.Messenger; |
171 | import dk.aau.cs.TCTL.TCTLAGNode; |
172 | import dk.aau.cs.TCTL.TCTLEFNode; |
173 | @@ -372,7 +374,13 @@ |
174 | } |
175 | |
176 | private void publishResult(String fileName, pipe.dataLayer.TAPNQuery query, String verificationResult, long verificationTime, Stats stats) { |
177 | - BatchProcessingVerificationResult result = new BatchProcessingVerificationResult(fileName, query, verificationResult, verificationTime, MemoryMonitor.getPeakMemory(), stats); |
178 | + BatchProcessingVerificationResult result; |
179 | + if(QueryPane.getTemporaryFile() != null && fileName.equals(QueryPane.getTemporaryFile().getName())) { |
180 | + //removes numbers from tempFile so it looks good |
181 | + result = new BatchProcessingVerificationResult(CreateGui.appGui.getCurrentTabName(), query, verificationResult, verificationTime, MemoryMonitor.getPeakMemory(), stats); |
182 | + } else { |
183 | + result = new BatchProcessingVerificationResult(fileName, query, verificationResult, verificationTime, MemoryMonitor.getPeakMemory(), stats); |
184 | + } |
185 | publish(result); |
186 | } |
187 | |
188 | |
189 | === modified file 'src/pipe/gui/GuiFrame.java' |
190 | --- src/pipe/gui/GuiFrame.java 2018-02-15 11:31:28 +0000 |
191 | +++ src/pipe/gui/GuiFrame.java 2018-04-09 08:31:59 +0000 |
192 | @@ -25,6 +25,7 @@ |
193 | import java.util.jar.JarFile; |
194 | import javax.swing.Action; |
195 | import javax.swing.BoxLayout; |
196 | +import javax.swing.DefaultListModel; |
197 | import javax.swing.ImageIcon; |
198 | import javax.swing.JCheckBox; |
199 | import javax.swing.JCheckBoxMenuItem; |
200 | @@ -32,6 +33,7 @@ |
201 | import javax.swing.JComponent; |
202 | import javax.swing.JDialog; |
203 | import javax.swing.JFrame; |
204 | +import javax.swing.JList; |
205 | import javax.swing.JMenu; |
206 | import javax.swing.JMenuBar; |
207 | import javax.swing.JMenuItem; |
208 | @@ -77,6 +79,7 @@ |
209 | import pipe.gui.widgets.FileBrowser; |
210 | import pipe.gui.widgets.NewTAPNPanel; |
211 | import pipe.gui.widgets.QueryDialog; |
212 | +import pipe.gui.widgets.QueryPane; |
213 | import pipe.gui.widgets.WorkflowDialog; |
214 | import dk.aau.cs.debug.Logger; |
215 | import dk.aau.cs.gui.BatchProcessingDialog; |
216 | @@ -743,7 +746,7 @@ |
217 | batchProcessing.addActionListener(new ActionListener() { |
218 | public void actionPerformed(ActionEvent arg0) { |
219 | if(checkForSaveAll()){ |
220 | - BatchProcessingDialog.showBatchProcessingDialog(); |
221 | + BatchProcessingDialog.showBatchProcessingDialog(new JList(new DefaultListModel())); |
222 | } |
223 | } |
224 | }); |
225 | @@ -1355,6 +1358,26 @@ |
226 | |
227 | private void saveNet(int index, File outFile) { |
228 | try { |
229 | + saveNet(index, outFile, (List<TAPNQuery>) CreateGui.getTab(index).queries()); |
230 | + |
231 | + CreateGui.setFile(outFile, index); |
232 | + |
233 | + CreateGui.getDrawingSurface(index).setNetChanged(false); |
234 | + appTab.setTitleAt(index, outFile.getName()); |
235 | + if(index == appTab.getSelectedIndex()) setTitle(outFile.getName()); // Change the window title |
236 | + CreateGui.getDrawingSurface(index).getUndoManager().clear(); |
237 | + undoAction.setEnabled(false); |
238 | + redoAction.setEnabled(false); |
239 | + } catch (Exception e) { |
240 | + System.err.println(e); |
241 | + JOptionPane.showMessageDialog(GuiFrame.this, e.toString(), |
242 | + "File Output Error", JOptionPane.ERROR_MESSAGE); |
243 | + return; |
244 | + } |
245 | + } |
246 | + |
247 | + public void saveNet(int index, File outFile, List<TAPNQuery> queries) { |
248 | + try { |
249 | TabContent currentTab = CreateGui.getTab(index); |
250 | NetworkMarking currentMarking = null; |
251 | if(getGUIMode().equals(GUIMode.animation)){ |
252 | @@ -1365,20 +1388,12 @@ |
253 | NetWriter tapnWriter = new TimedArcPetriNetNetworkWriter( |
254 | currentTab.network(), |
255 | currentTab.allTemplates(), |
256 | - currentTab.queries(), |
257 | + queries, |
258 | currentTab.network().constants() |
259 | ); |
260 | |
261 | tapnWriter.savePNML(outFile); |
262 | |
263 | - CreateGui.setFile(outFile, index); |
264 | - |
265 | - CreateGui.getDrawingSurface(index).setNetChanged(false); |
266 | - appTab.setTitleAt(index, outFile.getName()); |
267 | - if(index == appTab.getSelectedIndex()) setTitle(outFile.getName()); // Change the window title |
268 | - CreateGui.getDrawingSurface(index).getUndoManager().clear(); |
269 | - undoAction.setEnabled(false); |
270 | - redoAction.setEnabled(false); |
271 | if(getGUIMode().equals(GUIMode.animation)){ |
272 | currentTab.network().setMarking(currentMarking); |
273 | } |
274 | |
275 | === added file 'src/pipe/gui/undo/RemoveQueriesCommand.java' |
276 | --- src/pipe/gui/undo/RemoveQueriesCommand.java 1970-01-01 00:00:00 +0000 |
277 | +++ src/pipe/gui/undo/RemoveQueriesCommand.java 2018-04-09 08:31:59 +0000 |
278 | @@ -0,0 +1,32 @@ |
279 | +package pipe.gui.undo; |
280 | + |
281 | +import java.util.List; |
282 | + |
283 | +import dk.aau.cs.gui.TabContent; |
284 | +import dk.aau.cs.gui.undo.Command; |
285 | +import pipe.dataLayer.TAPNQuery; |
286 | + |
287 | +public class RemoveQueriesCommand extends Command { |
288 | + |
289 | + private List<TAPNQuery> queriesToRemove; |
290 | + private TabContent tabContent; |
291 | + |
292 | + |
293 | + public RemoveQueriesCommand(List<TAPNQuery> QueriesToRemove, TabContent TabContent) { |
294 | + this.queriesToRemove = QueriesToRemove; |
295 | + this.tabContent = TabContent; |
296 | + } |
297 | + |
298 | + @Override |
299 | + public void redo() { |
300 | + for(TAPNQuery queryToRemove : queriesToRemove) { |
301 | + tabContent.removeQuery(queryToRemove); |
302 | + } |
303 | + } |
304 | + |
305 | + @Override |
306 | + public void undo() { |
307 | + for(TAPNQuery query : queriesToRemove) |
308 | + tabContent.addQuery(query); |
309 | + } |
310 | +} |
311 | |
312 | === removed file 'src/pipe/gui/undo/RemoveQueryCommand.java' |
313 | --- src/pipe/gui/undo/RemoveQueryCommand.java 2011-04-02 16:30:48 +0000 |
314 | +++ src/pipe/gui/undo/RemoveQueryCommand.java 1970-01-01 00:00:00 +0000 |
315 | @@ -1,22 +0,0 @@ |
316 | -package pipe.gui.undo; |
317 | - |
318 | -import pipe.dataLayer.TAPNQuery; |
319 | -import dk.aau.cs.gui.TabContent; |
320 | - |
321 | -public class RemoveQueryCommand extends AddQueryCommand { |
322 | - |
323 | - public RemoveQueryCommand(TAPNQuery query, TabContent tabContent) { |
324 | - super(query, tabContent); |
325 | - } |
326 | - |
327 | - @Override |
328 | - public void redo() { |
329 | - super.undo(); |
330 | - } |
331 | - |
332 | - @Override |
333 | - public void undo() { |
334 | - super.redo(); |
335 | - } |
336 | - |
337 | -} |
338 | |
339 | === modified file 'src/pipe/gui/widgets/QueryPane.java' |
340 | --- src/pipe/gui/widgets/QueryPane.java 2017-06-23 09:03:39 +0000 |
341 | +++ src/pipe/gui/widgets/QueryPane.java 2018-04-09 08:31:59 +0000 |
342 | @@ -11,9 +11,12 @@ |
343 | import java.awt.event.ComponentListener; |
344 | import java.awt.event.MouseAdapter; |
345 | import java.awt.event.MouseEvent; |
346 | +import java.io.File; |
347 | +import java.io.IOException; |
348 | import java.util.ArrayList; |
349 | import java.util.Arrays; |
350 | import java.util.HashSet; |
351 | +import java.util.List; |
352 | |
353 | import javax.swing.BorderFactory; |
354 | import javax.swing.DefaultListCellRenderer; |
355 | @@ -31,17 +34,20 @@ |
356 | import javax.swing.event.ListDataListener; |
357 | import javax.swing.event.ListSelectionEvent; |
358 | import javax.swing.event.ListSelectionListener; |
359 | - |
360 | import pipe.dataLayer.TAPNQuery; |
361 | import pipe.gui.CreateGui; |
362 | +import pipe.gui.GuiFrame; |
363 | +import pipe.gui.MessengerImpl; |
364 | import pipe.gui.Verifier; |
365 | import pipe.gui.graphicElements.PetriNetObject; |
366 | import pipe.gui.graphicElements.tapn.TimedPlaceComponent; |
367 | import pipe.gui.undo.AddQueryCommand; |
368 | -import pipe.gui.undo.RemoveQueryCommand; |
369 | +import pipe.gui.undo.RemoveQueriesCommand; |
370 | import pipe.gui.undo.UndoManager; |
371 | import pipe.gui.widgets.QueryDialog.QueryDialogueOption; |
372 | +import dk.aau.cs.Messenger; |
373 | import dk.aau.cs.debug.Logger; |
374 | +import dk.aau.cs.gui.BatchProcessingDialog; |
375 | import dk.aau.cs.gui.TabContent; |
376 | import dk.aau.cs.gui.TemplateExplorer; |
377 | import dk.aau.cs.gui.undo.Command; |
378 | @@ -59,7 +65,9 @@ |
379 | private JPanel buttonsPanel; |
380 | private DefaultListModel listModel; |
381 | private JList queryList; |
382 | + private List<TAPNQuery> selectedQueries; |
383 | private JScrollPane queryScroller; |
384 | + private Messenger messenger = new MessengerImpl(); |
385 | |
386 | private JButton addQueryButton; |
387 | private JButton editQueryButton; |
388 | @@ -71,14 +79,15 @@ |
389 | private JButton moveUpButton; |
390 | private JButton moveDownButton; |
391 | private JButton sortButton; |
392 | + private static File tempFile; |
393 | |
394 | private static final String toolTipNewQuery = "Create a new query"; |
395 | private static final String toolTipEditQuery="Edit the selected query"; |
396 | private static final String toolTipRemoveQuery="Remove the selected query"; |
397 | private static final String toolTipVerifyQuery="Verify the selected query"; |
398 | private static final String toolTipSortQueries="Sort the queries alphabetically"; |
399 | - private final static String toolTipMoveUp = "Move the selected query up"; |
400 | - private final static String toolTipMoveDown = "Move the selected query down"; |
401 | + private final static String toolTipMoveUp = "Move the selected query up; only one query can be moved at a time"; |
402 | + private final static String toolTipMoveDown = "Move the selected query down; only one query can be moved at a time"; |
403 | |
404 | //private static final String toolTipQueryPane = "Here you can manage queries. Queries can explore properties of the Net."; |
405 | |
406 | @@ -107,7 +116,7 @@ |
407 | |
408 | queryList = new NonsearchableJList(listModel); |
409 | queryList.setCellRenderer(new QueryCellRenderer()); |
410 | - queryList.setSelectionMode(ListSelectionModel.SINGLE_SELECTION); |
411 | + queryList.setSelectionMode(ListSelectionModel.MULTIPLE_INTERVAL_SELECTION); |
412 | queryList.addListSelectionListener(new ListSelectionListener() { |
413 | public void valueChanged(ListSelectionEvent e) { |
414 | if (!(e.getValueIsAdjusting())) { |
415 | @@ -179,13 +188,13 @@ |
416 | removeQueryButton.setEnabled(true); |
417 | } |
418 | int index = queryList.getSelectedIndex(); |
419 | - if(index > 0) |
420 | + if(index > 0 && queryList.getSelectedIndices().length == 1) |
421 | moveUpButton.setEnabled(true); |
422 | else |
423 | moveUpButton.setEnabled(false); |
424 | |
425 | |
426 | - if(index < listModel.size()-1) |
427 | + if(index < listModel.size()-1 && queryList.getSelectedIndices().length == 1) |
428 | moveDownButton.setEnabled(true); |
429 | else |
430 | moveDownButton.setEnabled(false); |
431 | @@ -211,10 +220,12 @@ |
432 | public void actionPerformed(ActionEvent e) { |
433 | int index = queryList.getSelectedIndex(); |
434 | |
435 | - if(index > 0) { |
436 | + if(index > 0 && queryList.getSelectedIndices().length == 1) { |
437 | swapQueries(index, index-1); |
438 | queryList.setSelectedIndex(index-1); |
439 | } |
440 | + else |
441 | + moveUpButton.setEnabled(false); |
442 | } |
443 | }); |
444 | |
445 | @@ -231,10 +242,12 @@ |
446 | public void actionPerformed(ActionEvent e) { |
447 | int index = queryList.getSelectedIndex(); |
448 | |
449 | - if(index < listModel.size()-1) { |
450 | + if(index < listModel.size()-1 && queryList.getSelectedIndices().length == 1) { |
451 | swapQueries(index, index+1); |
452 | queryList.setSelectedIndex(index+1); |
453 | } |
454 | + else |
455 | + moveDownButton.setEnabled(false); |
456 | } |
457 | }); |
458 | |
459 | @@ -272,7 +285,10 @@ |
460 | editQueryButton.setPreferredSize(dimension); |
461 | editQueryButton.addActionListener(new ActionListener() { |
462 | public void actionPerformed(ActionEvent e) { |
463 | - showEditDialog(); |
464 | + if(queryList.getSelectedIndices().length == 1) |
465 | + showEditDialog(); |
466 | + else |
467 | + messenger.displayErrorMessage("It is only possible to edit 1 query at a time. Only verification can be done with multiple queries."); |
468 | } |
469 | }); |
470 | GridBagConstraints gbc = new GridBagConstraints(); |
471 | @@ -302,11 +318,7 @@ |
472 | removeQueryButton.setPreferredSize(dimension); |
473 | removeQueryButton.addActionListener(new ActionListener() { |
474 | public void actionPerformed(ActionEvent e) { |
475 | - TAPNQuery query = (TAPNQuery) queryList.getSelectedValue(); |
476 | - undoManager.addNewEdit(new RemoveQueryCommand(query, tabContent)); |
477 | - if(listModel.getSize() > 0 && query != null){ |
478 | - listModel.remove(queryList.getSelectedIndex()); |
479 | - } |
480 | + removeQueries(); |
481 | } |
482 | }); |
483 | gbc = new GridBagConstraints(); |
484 | @@ -359,6 +371,16 @@ |
485 | listModel.set(currentIndex, listModel.get(newIndex)); |
486 | listModel.set(newIndex, temp); |
487 | } |
488 | + |
489 | + private void removeQueries() { |
490 | + undoManager.addNewEdit(new RemoveQueriesCommand((List<TAPNQuery>) queryList.getSelectedValuesList(), tabContent)); |
491 | + if(listModel.getSize() > 0 && isQueryPossible()){ |
492 | + for(Object o : queryList.getSelectedValuesList()) { |
493 | + listModel.removeElement(o); |
494 | + } |
495 | + updateQueryButtons(); |
496 | + } |
497 | + } |
498 | |
499 | public void showEditDialog() { |
500 | int openCTLDialog = JOptionPane.YES_OPTION; |
501 | @@ -463,13 +485,45 @@ |
502 | |
503 | private void verifyQuery() { |
504 | TAPNQuery query = (TAPNQuery) queryList.getSelectedValue(); |
505 | - |
506 | - if(query.getReductionOption() == ReductionOption.VerifyTAPN || query.getReductionOption() == ReductionOption.VerifyTAPNdiscreteVerification || query.getReductionOption() == ReductionOption.VerifyPN) |
507 | - Verifier.runVerifyTAPNVerification(tabContent.network(), query, null, this.tabContent.getGuiModels()); |
508 | - else |
509 | - Verifier.runUppaalVerification(tabContent.network(), query); |
510 | - } |
511 | - |
512 | + int NumberOfSelectedElements = queryList.getSelectedIndices().length; |
513 | + |
514 | + |
515 | + if(NumberOfSelectedElements == 1) { |
516 | + if(query.getReductionOption() == ReductionOption.VerifyTAPN || query.getReductionOption() == ReductionOption.VerifyTAPNdiscreteVerification || query.getReductionOption() == ReductionOption.VerifyPN) |
517 | + Verifier.runVerifyTAPNVerification(tabContent.network(), query, null, this.tabContent.getGuiModels()); |
518 | + else |
519 | + Verifier.runUppaalVerification(tabContent.network(), query); |
520 | + } |
521 | + else if(NumberOfSelectedElements > 1) { |
522 | + saveNetAndRunBatchProcessing(); |
523 | + } |
524 | + } |
525 | + |
526 | + private void saveNetAndRunBatchProcessing() { |
527 | + getSelectedQueriesForProcessing(); |
528 | + //Saves the net in a temporary file which is used in batchProcessing |
529 | + //File is deleted on exit |
530 | + try { |
531 | + tempFile = File.createTempFile(CreateGui.appGui.getCurrentTabName(), ".xml"); |
532 | + CreateGui.appGui.saveNet(CreateGui.getTab().getSelectedIndex(), tempFile, selectedQueries); |
533 | + BatchProcessingDialog.showBatchProcessingDialog(queryList); |
534 | + tempFile.deleteOnExit(); |
535 | + if(tempFile == null) { |
536 | + throw new IOException(); |
537 | + } |
538 | + }catch(IOException e) { |
539 | + messenger.displayErrorMessage("Creation of temporary file needed for verification failed."); |
540 | + } |
541 | + } |
542 | + |
543 | + private void getSelectedQueriesForProcessing() { |
544 | + selectedQueries = queryList.getSelectedValuesList(); |
545 | + } |
546 | + |
547 | + public static File getTemporaryFile() { |
548 | + return tempFile; |
549 | + } |
550 | + |
551 | public boolean isQueryPossible() { |
552 | return (queryList.getModel().getSize() > 0 ); |
553 | } |
There is still a bug in the branch that returns:
ensionHost is implemented in both /System/ Library/ PrivateFramewor ks/FinderKit. framework/ Versions/ A/FinderKit (0x7fff923fdb68) and /System/ Library/ PrivateFramewor ks/FileProvider .framework/ OverrideBundles /FinderSyncColl aborationFilePr oviderOverride. bundle/ Contents/ MacOS/FinderSyn cCollaborationF ileProviderOver ride (0x133b6dcd8). One of the two will be used. Which one is undefined.
To reproduce:
1. Make new net with just one place
2. Make query called 1 that is EF true
3. Make query called 2 thas is EF false
4. Select both queries and run verify - the query names get refreshed for no reason
5. After you close the batch processing dialog, there are now queries 1, 2, 1, 2
in the list of queries.