Browse Source

Support for CSV file result export from GUI.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4139 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 14 years ago
parent
commit
23bee5f9b9
  1. 1
      prism/CHANGELOG.txt
  2. 79
      prism/src/userinterface/properties/GUIMultiProperties.java
  3. 17
      prism/src/userinterface/properties/computation/ExportResultsThread.java

1
prism/CHANGELOG.txt

@ -14,6 +14,7 @@ Changes:
Ongoing changes: Ongoing changes:
* CSV format for results export (GUI, not CL yet)
* Handling of verbosity/warnings in log * Handling of verbosity/warnings in log
* Properties can be named, by prefixing with "name":, and reference each other * Properties can be named, by prefixing with "name":, and reference each other
* CTL AG/EF * CTL AG/EF

79
prism/src/userinterface/properties/GUIMultiProperties.java

@ -83,7 +83,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
// GUI // GUI
private GUIPrismFileFilter propsFilter[]; private GUIPrismFileFilter propsFilter[];
private GUIPrismFileFilter textFilter[];
private GUIPrismFileFilter resultsFilter[];
private JMenu propMenu; private JMenu propMenu;
private JPopupMenu propertiesPopup, constantsPopup, labelsPopup, experimentPopup; private JPopupMenu propertiesPopup, constantsPopup, labelsPopup, experimentPopup;
private GUIExperimentTable experiments; private GUIExperimentTable experiments;
@ -92,7 +92,8 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
private JLabel fileLabel; private JLabel fileLabel;
private Vector clipboardVector; private Vector clipboardVector;
private Action newProps, openProps, saveProps, savePropsAs, insertProps, verifySelected, newProperty, editProperty, newConstant, removeConstant, newLabel, private Action newProps, openProps, saveProps, savePropsAs, insertProps, verifySelected, newProperty, editProperty, newConstant, removeConstant, newLabel,
removeLabel, newExperiment, deleteExperiment, stopExperiment, viewResults, plotResults, exportResultsText, exportResultsMatrix,simulate, details;
removeLabel, newExperiment, deleteExperiment, stopExperiment, viewResults, plotResults,
exportResultsListText, exportResultsListCSV, exportResultsMatrixText, exportResultsMatrixCSV, simulate, details;
// Current properties // Current properties
private GUIPropertiesList propList; private GUIPropertiesList propList;
@ -603,8 +604,10 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
plotResults.setEnabled(false); plotResults.setEnabled(false);
} }
// exportResults: enabled if at least one experiment is selected // exportResults: enabled if at least one experiment is selected
exportResultsText.setEnabled(experiments.getSelectedRowCount() > 0);
exportResultsMatrix.setEnabled(experiments.getSelectedRowCount() > 0);
exportResultsListText.setEnabled(experiments.getSelectedRowCount() > 0);
exportResultsListCSV.setEnabled(experiments.getSelectedRowCount() > 0);
exportResultsMatrixText.setEnabled(experiments.getSelectedRowCount() > 0);
exportResultsMatrixCSV.setEnabled(experiments.getSelectedRowCount() > 0);
} }
public int doModificationCheck() public int doModificationCheck()
@ -999,7 +1002,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
} }
public void a_exportResults(boolean exportMatrix)
public void a_exportResults(boolean exportMatrix, String sep)
{ {
GUIExperiment exps[]; GUIExperiment exps[];
int i, n, inds[]; int i, n, inds[];
@ -1013,9 +1016,9 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
for (i = 0; i < n; i++) for (i = 0; i < n; i++)
exps[i] = experiments.getExperiment(inds[i]); exps[i] = experiments.getExperiment(inds[i]);
// get filename to save // get filename to save
if (showSaveFileDialog(textFilter, textFilter[0]) == JFileChooser.APPROVE_OPTION) {
if (showSaveFileDialog(resultsFilter, sep.equals(", ") ? resultsFilter[1] : resultsFilter[0]) == JFileChooser.APPROVE_OPTION) {
File file = getChooserFile(); File file = getChooserFile();
Thread t = new ExportResultsThread(this, exps, file, exportMatrix);
Thread t = new ExportResultsThread(this, exps, file, exportMatrix, sep);
t.setPriority(Thread.NORM_PRIORITY); t.setPriority(Thread.NORM_PRIORITY);
t.start(); t.start();
} }
@ -1558,9 +1561,11 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
propsFilter[0] = new GUIPrismFileFilter("PRISM properties (*.pctl, *.csl)"); propsFilter[0] = new GUIPrismFileFilter("PRISM properties (*.pctl, *.csl)");
propsFilter[0].addExtension("pctl"); propsFilter[0].addExtension("pctl");
propsFilter[0].addExtension("csl"); propsFilter[0].addExtension("csl");
textFilter = new GUIPrismFileFilter[1];
textFilter[0] = new GUIPrismFileFilter("Plain text files (*.txt)");
textFilter[0].addExtension("txt");
resultsFilter = new GUIPrismFileFilter[2];
resultsFilter[0] = new GUIPrismFileFilter("Plain text files (*.txt)");
resultsFilter[0].addExtension("txt");
resultsFilter[1] = new GUIPrismFileFilter("Comma-separated values (*.csv)");
resultsFilter[1].addExtension("csv");
} }
private void createPopups() private void createPopups()
@ -1605,8 +1610,10 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
JMenu exportResultsMenu = new JMenu("Export results"); JMenu exportResultsMenu = new JMenu("Export results");
exportResultsMenu.setMnemonic('E'); exportResultsMenu.setMnemonic('E');
exportResultsMenu.setIcon(GUIPrism.getIconFromImage("smallExport.png")); exportResultsMenu.setIcon(GUIPrism.getIconFromImage("smallExport.png"));
exportResultsMenu.add(exportResultsText);
exportResultsMenu.add(exportResultsMatrix);
exportResultsMenu.add(exportResultsListText);
exportResultsMenu.add(exportResultsListCSV);
exportResultsMenu.add(exportResultsMatrixText);
exportResultsMenu.add(exportResultsMatrixCSV);
experimentPopup.add(exportResultsMenu); experimentPopup.add(exportResultsMenu);
} }
@ -1846,29 +1853,53 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
plotResults.putValue(Action.NAME, "Plot results"); plotResults.putValue(Action.NAME, "Plot results");
plotResults.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileGraph.png")); plotResults.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileGraph.png"));
exportResultsText = new AbstractAction()
exportResultsListText = new AbstractAction()
{ {
public void actionPerformed(ActionEvent e) public void actionPerformed(ActionEvent e)
{ {
a_exportResults(false);
a_exportResults(false, "\t");
} }
}; };
exportResultsText.putValue(Action.LONG_DESCRIPTION, "Export the results of this experiment to a text file");
exportResultsText.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_T));
exportResultsText.putValue(Action.NAME, "Text");
exportResultsText.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileText.png"));
exportResultsListText.putValue(Action.LONG_DESCRIPTION, "Export the results of this experiment to a text file");
exportResultsListText.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_L));
exportResultsListText.putValue(Action.NAME, "List (text)");
exportResultsListText.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileText.png"));
exportResultsMatrix = new AbstractAction()
exportResultsListCSV = new AbstractAction()
{ {
public void actionPerformed(ActionEvent e) public void actionPerformed(ActionEvent e)
{ {
a_exportResults(true);
a_exportResults(false, ", ");
} }
}; };
exportResultsMatrix.putValue(Action.LONG_DESCRIPTION, "Export the results of this experiment to a file in matrix form");
exportResultsMatrix.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_M));
exportResultsMatrix.putValue(Action.NAME, "Matrix");
exportResultsMatrix.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileText.png"));
exportResultsListCSV.putValue(Action.LONG_DESCRIPTION, "Export the results of this experiment to a CSV file");
exportResultsListCSV.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_L));
exportResultsListCSV.putValue(Action.NAME, "List (CSV)");
exportResultsListCSV.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallMatrix.png"));
exportResultsMatrixText = new AbstractAction()
{
public void actionPerformed(ActionEvent e)
{
a_exportResults(true, "\t");
}
};
exportResultsMatrixText.putValue(Action.LONG_DESCRIPTION, "Export the results of this experiment to a file in matrix form");
exportResultsMatrixText.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_M));
exportResultsMatrixText.putValue(Action.NAME, "Matrix (text)");
exportResultsMatrixText.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileText.png"));
exportResultsMatrixCSV = new AbstractAction()
{
public void actionPerformed(ActionEvent e)
{
a_exportResults(true, ", ");
}
};
exportResultsMatrixCSV.putValue(Action.LONG_DESCRIPTION, "Export the results of this experiment to a file in matrix form");
exportResultsMatrixCSV.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_M));
exportResultsMatrixCSV.putValue(Action.NAME, "Matrix (CSV)");
exportResultsMatrixCSV.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallMatrix.png"));
stopExperiment = new AbstractAction() stopExperiment = new AbstractAction()
{ {

17
prism/src/userinterface/properties/computation/ExportResultsThread.java

@ -39,6 +39,7 @@ public class ExportResultsThread extends Thread
private File f; private File f;
private Exception saveError; private Exception saveError;
private boolean exportMatrix; // export in matrix form? private boolean exportMatrix; // export in matrix form?
private String sep; // string separating items
/** Creates a new instance of ExportResultsThread */ /** Creates a new instance of ExportResultsThread */
public ExportResultsThread(GUIMultiProperties parent, GUIExperiment exp, File f) public ExportResultsThread(GUIMultiProperties parent, GUIExperiment exp, File f)
@ -48,6 +49,7 @@ public class ExportResultsThread extends Thread
this.exps[0] = exp; this.exps[0] = exp;
this.f = f; this.f = f;
this.exportMatrix = false; this.exportMatrix = false;
this.sep = " ";
} }
/** Creates a new instance of ExportResultsThread */ /** Creates a new instance of ExportResultsThread */
@ -57,15 +59,17 @@ public class ExportResultsThread extends Thread
this.exps = exps; this.exps = exps;
this.f = f; this.f = f;
this.exportMatrix = false; this.exportMatrix = false;
this.sep = " ";
} }
/** Creates a new instance of ExportResultsThread */ /** Creates a new instance of ExportResultsThread */
public ExportResultsThread(GUIMultiProperties parent, GUIExperiment exps[], File f, boolean exportMatrix)
public ExportResultsThread(GUIMultiProperties parent, GUIExperiment exps[], File f, boolean exportMatrix, String sep)
{ {
this.parent = parent; this.parent = parent;
this.exps = exps; this.exps = exps;
this.f = f; this.f = f;
this.exportMatrix = exportMatrix; this.exportMatrix = exportMatrix;
this.sep = sep;
} }
public void run() public void run()
@ -86,11 +90,16 @@ public class ExportResultsThread extends Thread
n = exps.length; n = exps.length;
for (i = 0; i < n; i++) { for (i = 0; i < n; i++) {
if (i > 0) out.print("\n"); if (i > 0) out.print("\n");
if (!exportMatrix) {
if (n > 1) {
if (sep.equals(", "))
out.print("\"" + exps[i].getPropertyString() + ":\"\n");
else
out.print(exps[i].getPropertyString() + ":\n"); out.print(exps[i].getPropertyString() + ":\n");
out.print(exps[i].getResults().toString(false, " ", " "));
}
if (!exportMatrix) {
out.print(exps[i].getResults().toString(false, sep, sep));
} else { } else {
out.print(exps[i].getResults().toStringMatrix("\t"));
out.print(exps[i].getResults().toStringMatrix(sep));
} }
} }
out.flush(); out.flush();

Loading…
Cancel
Save