40
40
import javax.swing.JSeparator;
41
41
import javax.swing.JSplitPane;
42
42
import javax.swing.JTable;
43
import javax.swing.ListCellRenderer;
44
43
import javax.swing.ListSelectionModel;
45
44
import javax.swing.SwingConstants;
46
45
import javax.swing.SwingWorker.StateValue;
49
48
import javax.swing.border.Border;
50
49
import javax.swing.event.ChangeEvent;
51
50
import javax.swing.event.ChangeListener;
52
import javax.swing.event.ListSelectionEvent;
53
import javax.swing.event.ListSelectionListener;
54
51
import javax.swing.event.TableModelEvent;
55
52
import javax.swing.event.TableModelListener;
56
53
import javax.swing.table.TableCellRenderer;
60
57
import pipe.dataLayer.TAPNQuery;
61
58
import pipe.dataLayer.TAPNQuery.SearchOption;
62
59
import pipe.gui.CreateGui;
63
import pipe.gui.widgets.CustomJSpinner;
60
import net.tapaal.swinghelpers.CustomJSpinner;
64
61
import pipe.gui.widgets.EscapableDialog;
65
62
import pipe.gui.widgets.filebrowser.FileBrowser;
66
63
import pipe.gui.widgets.QueryPane;
217
214
private JButton addFilesButton;
218
215
private JButton clearFilesButton;
219
216
private JButton removeFileButton;
220
private JList fileList;
221
private DefaultListModel listModel;
217
private JList<File> fileList;
218
private DefaultListModel<File> listModel;
223
220
private JLabel statusLabel;
224
221
private JLabel fileStatusLabel;
230
227
private JLabel memory;
231
228
private long startTimeMs = 0;
233
private JComboBox searchOption;
230
private JComboBox<String> searchOption;
234
231
private JButton exportButton;
235
232
private JButton closeButton;
236
private JComboBox queryPropertyOption;
233
private JComboBox<String> queryPropertyOption;
237
234
private JPanel verificationOptionsPanel;
238
235
private CustomJSpinner numberOfExtraTokensInNet;
239
236
private JCheckBox keepQueryCapacity;
240
private JComboBox symmetryOption;
241
private JComboBox stubbornReductionOption;
237
private JComboBox<String> symmetryOption;
238
private JComboBox<String> stubbornReductionOption;
242
239
private JCheckBox noTimeoutCheckbox;
243
240
private JCheckBox noOOMCheckbox;
244
241
private CustomJSpinner timeoutValue;
245
242
private CustomJSpinner oomValue;
246
private JComboBox approximationMethodOption;
243
private JComboBox<String> approximationMethodOption;
247
244
private CustomJSpinner approximationDenominator;
248
245
private JCheckBox approximationDenominatorCheckbox;
249
private JList ListOfQueries;
246
private JList<TAPNQuery> ListOfQueries;
251
private Timer timeoutTimer = new Timer(30000, new ActionListener() {
252
public void actionPerformed(ActionEvent e) {
253
timeoutCurrentVerificationTask();
248
private Timer timeoutTimer = new Timer(30000, e -> timeoutCurrentVerificationTask());
257
250
private BatchProcessingResultsTableModel tableModel;
328
321
BatchProcessing was called from QueryPane
329
322
(should maybe be boolean)
331
public static void showBatchProcessingDialog(JList ListOfQueries){
324
public static void showBatchProcessingDialog(JList<TAPNQuery> ListOfQueries){
332
325
if(ListOfQueries.getModel().getSize() != 0) {
333
326
batchProcessingDialog = null;
344
337
batchProcessingDialog.setVisible(true);
347
private BatchProcessingDialog(Frame frame, String title, boolean modal, JList ListOfQueries) {
340
private BatchProcessingDialog(Frame frame, String title, boolean modal, JList<TAPNQuery> ListOfQueries) {
348
341
super(frame, title, modal);
350
343
addWindowListener(new WindowAdapter() {
416
fileList.addListSelectionListener(new ListSelectionListener() {
418
public void valueChanged(ListSelectionEvent e) {
419
if (!(e.getValueIsAdjusting())) {
420
if (fileList.getSelectedIndex() == -1) {
421
removeFileButton.setEnabled(false);
423
removeFileButton.setEnabled(true);
406
fileList.addListSelectionListener(e -> {
407
if (!(e.getValueIsAdjusting())) {
408
if (fileList.getSelectedIndex() == -1) {
409
removeFileButton.setEnabled(false);
411
removeFileButton.setEnabled(true);
447
434
addFilesButton = new JButton("Add models");
448
435
addFilesButton.setToolTipText(TOOL_TIP_AddFilesButton);
449
addFilesButton.addActionListener(new ActionListener() {
450
public void actionPerformed(ActionEvent arg0) {
436
addFilesButton.addActionListener(arg0 -> addFiles());
455
438
gbc = new GridBagConstraints();
456
439
gbc.anchor = GridBagConstraints.NORTHWEST;
463
446
removeFileButton = new JButton("Remove models");
464
447
removeFileButton.setToolTipText(TOOL_TIP_RemoveFilesButton);
465
448
removeFileButton.setEnabled(false);
466
removeFileButton.addActionListener(new ActionListener() {
468
public void actionPerformed(ActionEvent arg0) {
469
removeSelectedFiles();
449
removeFileButton.addActionListener(arg0 -> removeSelectedFiles());
472
450
gbc = new GridBagConstraints();
479
457
clearFilesButton = new JButton("Clear");
480
458
clearFilesButton.setToolTipText(TOOL_TIP_ClearFilesButton);
481
459
clearFilesButton.setEnabled(false);
482
clearFilesButton.addActionListener(new ActionListener() {
484
public void actionPerformed(ActionEvent e) {
460
clearFilesButton.addActionListener(e -> {
490
465
gbc = new GridBagConstraints();
894
869
private SearchOption getSearchOption() {
895
if (((String) searchOption.getSelectedItem()).equals(name_DFS))
870
if (searchOption.getSelectedItem().equals(name_DFS))
896
871
return SearchOption.DFS;
897
else if (((String) searchOption.getSelectedItem()).equals(name_Random))
872
else if (searchOption.getSelectedItem().equals(name_Random))
898
873
return SearchOption.RANDOM;
899
else if (((String) searchOption.getSelectedItem())
874
else if (searchOption.getSelectedItem()
900
875
.equals(name_HEURISTIC))
901
876
return SearchOption.HEURISTIC;
902
else if (((String) searchOption.getSelectedItem()).equals(name_BFS))
877
else if (searchOption.getSelectedItem().equals(name_BFS))
903
878
return SearchOption.BFS;
905
880
return SearchOption.BatchProcessingKeepQueryOption;
958
933
private QueryPropertyOption getQueryPropertyOption() {
959
934
String propertyOptionString = (String) queryPropertyOption.getSelectedItem();
960
if (propertyOptionString.equals(name_SEARCHWHOLESTATESPACE))
961
return QueryPropertyOption.SearchWholeStateSpace;
962
else if (propertyOptionString.equals(name_EXISTDEADLOCK))
963
return QueryPropertyOption.ExistDeadlock;
964
else if (propertyOptionString.equals(name_STRONGSOUNDNESS))
965
return QueryPropertyOption.StrongSoundness;
966
else if (propertyOptionString.equals(name_SOUNDNESS))
967
return QueryPropertyOption.Soundness;
969
return QueryPropertyOption.KeepQueryOption;
935
switch (propertyOptionString) {
936
case name_SEARCHWHOLESTATESPACE:
937
return QueryPropertyOption.SearchWholeStateSpace;
938
case name_EXISTDEADLOCK:
939
return QueryPropertyOption.ExistDeadlock;
940
case name_STRONGSOUNDNESS:
941
return QueryPropertyOption.StrongSoundness;
943
return QueryPropertyOption.Soundness;
945
return QueryPropertyOption.KeepQueryOption;
972
949
private ApproximationMethodOption getApproximationMethodOption() {
973
950
String ApproximationMethodOptionString = (String) approximationMethodOption.getSelectedItem();
974
if(ApproximationMethodOptionString.equals(name_OVER_APPROXIMATION)) {
975
return ApproximationMethodOption.OverApproximation;
976
} else if (ApproximationMethodOptionString.equals(name_UNDER_APPROXIMATION)) {
977
return ApproximationMethodOption.UnderApproximation;
978
} else if (ApproximationMethodOptionString.equals(name_NONE_APPROXIMATION)) {
979
return ApproximationMethodOption.None;
981
return ApproximationMethodOption.KeepQueryOption;
951
switch (ApproximationMethodOptionString) {
952
case name_OVER_APPROXIMATION:
953
return ApproximationMethodOption.OverApproximation;
954
case name_UNDER_APPROXIMATION:
955
return ApproximationMethodOption.UnderApproximation;
956
case name_NONE_APPROXIMATION:
957
return ApproximationMethodOption.None;
959
return ApproximationMethodOption.KeepQueryOption;
1036
1014
private void exportResults() {
1037
String filename = FileBrowser.constructor("CSV file", "csv", lastPath)
1038
.saveFile("results");
1015
String filename = FileBrowser.constructor("CSV file", "csv", lastPath).saveFile("results");
1039
1017
if (filename != null) {
1040
1018
File exportFile = new File(filename);
1041
1019
lastPath = exportFile.getParent();
1042
1020
BatchProcessingResultsExporter exporter = new BatchProcessingResultsExporter();
1044
exporter.exportToCSV(tableModel.getResults(),
1022
exporter.exportToCSV(tableModel.getResults(), exportFile);
1046
1023
} catch (Exception e1) {
1047
1024
JOptionPane.showMessageDialog(
1048
1025
CreateGui.getApp(),
1049
1026
"An error occurred while trying to export the results. Please try again",
1050
1027
"Error Exporting Results",
1051
JOptionPane.ERROR_MESSAGE);
1028
JOptionPane.ERROR_MESSAGE
1052
1030
e1.printStackTrace();
1064
1042
closeButton = new JButton("Close");
1065
1043
closeButton.setToolTipText(TOOL_TIP_CloseButton);
1066
closeButton.addActionListener(new ActionListener() {
1067
public void actionPerformed(ActionEvent e) {
1044
closeButton.addActionListener(e -> exit());
1071
1046
gbc = new GridBagConstraints();
1084
1059
Integer.MAX_VALUE); // disable tooltips disappearing
1085
1060
ToolTipManager.sharedInstance().setInitialDelay(200);
1086
1061
return new MultiLineAutoWrappingToolTip();
1089
1064
ResultTableCellRenderer renderer = new ResultTableCellRenderer(true);
1090
1065
table.getColumnModel().getColumn(0).setMinWidth(70);
1097
1072
table.getColumn("Verification Time").setCellRenderer(renderer);
1098
1073
table.getColumn("Memory Usage").setCellRenderer(renderer);
1100
tableModel.addTableModelListener(new TableModelListener() {
1101
public void tableChanged(TableModelEvent e) {
1102
if (e.getType() == TableModelEvent.INSERT) {
1103
table.scrollRectToVisible(table.getCellRect(e.getLastRow(),
1104
e.getLastRow(), true));
1075
tableModel.addTableModelListener(e -> {
1076
if (e.getType() == TableModelEvent.INSERT) {
1077
table.scrollRectToVisible(table.getCellRect(e.getLastRow(), e.getLastRow(), true));
1116
1088
table.setRowSorter(sorter);
1118
1090
JScrollPane scrollPane = new JScrollPane(table);
1120
.setVerticalScrollBarPolicy(JScrollPane.VERTICAL_SCROLLBAR_AS_NEEDED);
1122
.setHorizontalScrollBarPolicy(JScrollPane.HORIZONTAL_SCROLLBAR_AS_NEEDED);
1091
scrollPane.setVerticalScrollBarPolicy(JScrollPane.VERTICAL_SCROLLBAR_AS_NEEDED);
1092
scrollPane.setHorizontalScrollBarPolicy(JScrollPane.HORIZONTAL_SCROLLBAR_AS_NEEDED);
1123
1093
Dimension scrollPanePrefDims = new Dimension(850, 250);
1124
1094
//Set the minimum size to 150 lets than the preferred, to be consistat with theh minimum size of the window
1125
1095
Dimension scrollPaneMinDims = new Dimension(850, 250-150);
1277
1247
cancelButton.setPreferredSize(new java.awt.Dimension(85, 25));
1279
1249
cancelButton.setEnabled(false);
1280
cancelButton.addActionListener(new ActionListener() {
1250
cancelButton.addActionListener(e -> {
1251
terminateBatchProcessing();
1252
fileStatusLabel.setText("");
1253
statusLabel.setText("Batch processing cancelled");
1282
public void actionPerformed(ActionEvent e) {
1283
terminateBatchProcessing();
1284
fileStatusLabel.setText("");
1285
statusLabel.setText("Batch processing cancelled");
1289
1257
gbc = new GridBagConstraints();
1300
1268
skipFileButton.setPreferredSize(new java.awt.Dimension(85, 25));
1302
1270
skipFileButton.setEnabled(false);
1303
skipFileButton.addActionListener(new ActionListener() {
1271
skipFileButton.addActionListener(e -> skipCurrentFile());
1305
public void actionPerformed(ActionEvent e) {
1309
1273
gbc = new GridBagConstraints();
1334
1298
public void propertyChange(PropertyChangeEvent evt) {
1335
1299
if (evt.getPropertyName().equals("state")) {
1336
if ((StateValue) evt.getNewValue() == StateValue.DONE) {
1300
if (evt.getNewValue() == StateValue.DONE) {
1337
1301
enableButtons();
1338
1302
cancelButton.setEnabled(false);
1339
1303
skipFileButton.setEnabled(false);
1342
1306
stopMemoryTimer();
1343
1307
timeoutTimer.stop();
1344
} else if ((StateValue) evt.getNewValue() == StateValue.STARTED) {
1308
} else if (evt.getNewValue() == StateValue.STARTED) {
1345
1309
disableButtonsDuringProcessing();
1346
1310
cancelButton.setEnabled(true);
1347
1311
skipFileButton.setEnabled(true);
1371
1335
startTimeMs = System.currentTimeMillis();
1374
public void fireVerificationTaskComplete(
1375
VerificationTaskCompleteEvent e) {
1376
if (timer.isRunning())
1338
public void fireVerificationTaskComplete(VerificationTaskCompleteEvent e) {
1339
if (timer.isRunning()) {
1378
1342
stopMemoryTimer();
1379
if (timeoutTimer.isRunning())
1343
if (timeoutTimer.isRunning()) {
1380
1344
timeoutTimer.stop();
1381
1346
int tasksCompleted = e.verificationTasksCompleted();
1382
1347
progressLabel.setText(e.verificationTasksCompleted()
1383
1348
+ " verification task"
1491
1456
// Custom cell renderer for the Query Column of the result table display the
1492
1457
// property of the query
1493
private class ResultTableCellRenderer extends JLabel implements
1458
private class ResultTableCellRenderer extends JLabel implements TableCellRenderer {
1495
1459
private static final long serialVersionUID = 3054497986242852099L;
1496
1460
Border unselectedBorder = null;
1497
1461
Border selectedBorder = null;
1501
1465
this.isBordered = isBordered;
1504
public Component getTableCellRendererComponent(JTable table,
1505
Object value, boolean isSelected, boolean hasFocus, int row,
1468
public Component getTableCellRendererComponent(JTable table, Object value, boolean isSelected, boolean hasFocus, int row, int column) {
1507
1469
if (isBordered) {
1508
1470
if (isSelected) {
1509
1471
setBackground(table.getSelectionBackground());
1543
1505
setForeground(table.getForeground());
1544
1506
if (unselectedBorder == null) {
1545
unselectedBorder = BorderFactory.createMatteBorder(2,
1546
5, 2, 5, table.getBackground());
1507
unselectedBorder = BorderFactory.createMatteBorder(2, 5, 2, 5, table.getBackground());
1548
1509
setBorder(unselectedBorder);
1560
1521
setToolTipText(generateTooltipTextFromQuery(newQuery));
1561
1522
setText(newQuery.getName());
1562
} else if (table.getColumnName(column).equals(
1563
"Verification Time")
1523
} else if (table.getColumnName(column).equals("Verification Time")
1564
1524
|| table.getColumnName(column).equals("Method")
1565
1525
|| table.getColumnName(column).equals("Memory Usage")) {
1566
1526
setText(value.toString());
1579
1539
setToolTipText(result != null ? generateMemoryToolTipText(result)
1580
1540
: value.toString());
1582
setToolTipText(result != null ? generateReductionString(result
1583
.query()) : value.toString());
1542
setToolTipText(result != null ? generateReductionString(result.query()) : value.toString());
1585
1544
setToolTipText(value.toString());
1586
1545
setText(value.toString());
1596
private String generateStatsToolTipText(
1597
BatchProcessingVerificationResult result) {
1555
private String generateStatsToolTipText(BatchProcessingVerificationResult result) {
1598
1556
StringBuilder s = new StringBuilder();
1599
1557
s.append("Verification Time: ");
1600
1558
s.append((result.verificationTimeInMs() / 1000.0));
1608
1566
return s.toString();
1611
private String generateMemoryToolTipText(
1612
BatchProcessingVerificationResult result) {
1569
private String generateMemoryToolTipText(BatchProcessingVerificationResult result) {
1613
1570
StringBuilder s = new StringBuilder();
1614
1571
s.append("Peak memory usage (estimate): ");
1615
1572
s.append(result.verificationMemory());
1760
1717
chooseReductionOptions = new JButton(STATUS_TEXT_DONT_OVERRIDE);
1761
1718
chooseReductionOptions.setToolTipText(TOOL_TIP_ReductionOption);
1762
chooseReductionOptions.addActionListener(new ActionListener() {
1763
public void actionPerformed(ActionEvent arg0) {
1764
//reductionOptionDialog.setOverride(true);
1765
reductionOptionDialog.setVisible(true);
1719
chooseReductionOptions.addActionListener(arg0 -> {
1720
//reductionOptionDialog.setOverride(true);
1721
reductionOptionDialog.setVisible(true);
1768
1723
this.add(chooseReductionOptions);
added
removed
src/dk/aau/cs/gui/BatchProcessingDialog.java
