diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 22130228..14905607 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -466,7 +466,9 @@ public class PrismCL implements PrismModelListener tmpLog.print(propertiesToCheck.get(i) + ":\n"); } if (!exportresultsmatrix) { - tmpLog.println(results[i].toString(false, sep, sep)); + ResultsExporter exporter = new ResultsExporter(exportresultscsv ? "csv" : "plain", "string"); + tmpLog.println(results[i].export(exporter).getExportString()); + //tmpLog.println(results[i].toString(false, sep, sep)); } else { tmpLog.println(results[i].toStringMatrix(sep)); } diff --git a/prism/src/prism/ResultsCollection.java b/prism/src/prism/ResultsCollection.java index a66d185f..2d99e95b 100644 --- a/prism/src/prism/ResultsCollection.java +++ b/prism/src/prism/ResultsCollection.java @@ -263,7 +263,7 @@ public class ResultsCollection for (i = 0; i < rangingConstants.size(); i++) { if (i > 0) s += sep; - s += ((DefinedConstant) rangingConstants.elementAt(i)).getName(); + s += rangingConstants.elementAt(i).getName(); } s += eq + "Result\n"; } @@ -273,6 +273,19 @@ public class ResultsCollection return s; } + /** + * Pass the results to a ResultsExporter. + * For convenience, returns a pointer to the same ResultsExporter passed in + */ + public ResultsExporter export(ResultsExporter exporter) + { + exporter.setConstantsInfo(rangingConstants); + exporter.start(); + root.export(exporter); + exporter.end(); + return exporter; + } + /** * Create string representation of the data for a partial evaluation * @param partial Values for a subset of the constants @@ -462,6 +475,14 @@ public class ResultsCollection return ret; } + /** + * Pass the results to a ResultsExporter. + */ + public void export(ResultsExporter export) + { + exportRec(new Values(), export); + } + public String toStringRec(boolean pv, String sep, String eq, String head) { int i, n; @@ -482,6 +503,15 @@ public class ResultsCollection return res; } + public void exportRec(Values values, ResultsExporter export) + { + int n = constant.getNumSteps(); + for (int i = 0; i < n; i++) { + values.setValue(constant.getName(), constant.getValue(i)); + kids[i].exportRec(values, export); + } + } + /** * Create string representation of the data for a partial evaluation * @param partial Values for a subset of the constants @@ -625,6 +655,11 @@ public class ResultsCollection return head + eq + val + "\n"; } + public void exportRec(Values values, ResultsExporter export) + { + export.exportResult(values, val); + } + public String toStringPartialRec(Values partial, boolean first, boolean pv, String sep, String eq, String head) { return head + eq + val + "\n"; diff --git a/prism/src/prism/ResultsExporter.java b/prism/src/prism/ResultsExporter.java new file mode 100644 index 00000000..9676a576 --- /dev/null +++ b/prism/src/prism/ResultsExporter.java @@ -0,0 +1,231 @@ +//============================================================================== +// +// Copyright (c) 2015- +// Authors: +// * Dave Parker (University of Birmingham/Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package prism; + +import java.util.List; + +import parser.Values; + +/** + * Class to export the results of model checking in various formats. + */ +public class ResultsExporter +{ + // Formats for export + public enum ResultsExportFormat { + PLAIN, CSV, COMMENT; + public String fullName() + { + switch (this) { + case PLAIN: + return "plain text"; + case CSV: + return "CSV"; + case COMMENT: + return "comment"; + default: + return this.toString(); + } + } + + public static ResultsExportFormat parse(String formatName) + { + switch (formatName) { + case "plain": + return ResultsExportFormat.PLAIN; + case "csv": + return ResultsExportFormat.CSV; + case "comment": + return ResultsExportFormat.COMMENT; + default: + // Default to plain if unknown format + return ResultsExportFormat.PLAIN; + } + } + }; + + // Possible destinations for export + public enum ResultsExportDestination { + STRING; + public String fullName() + { + switch (this) { + case STRING: + return "string"; + default: + return this.toString(); + } + } + public static ResultsExportDestination parse(String formatName) + { + switch (formatName) { + case "string": + return ResultsExportDestination.STRING; + default: + // Default to string if unknown format + return ResultsExportDestination.STRING; + } + } + }; + + private List constants; + private ResultsExportFormat format = ResultsExportFormat.PLAIN; + + private boolean printHeader; + private boolean printNames; + private String separator; + private String equals; + + private ResultsExportDestination destination = ResultsExportDestination.STRING; + + private String exportString = ""; + + // Methods to create and set up a ResultsExporter + + public ResultsExporter() + { + setFormat(ResultsExportFormat.PLAIN); + setDestination(ResultsExportDestination.STRING); + } + + public ResultsExporter(ResultsExportFormat format, ResultsExportDestination destination) + { + setFormat(format); + setDestination(destination); + } + + public ResultsExporter(String formatName, String destinationName) + { + setFormatByName(formatName); + setDestinationByName(destinationName); + } + + public void setFormat(ResultsExportFormat format) + { + this.format = format; + switch (format) { + case PLAIN: + printHeader = true; + printNames = false; + separator = "\t"; + equals = "\t"; + break; + case CSV: + printHeader = true; + printNames = false; + separator = ", "; + equals = ", "; + break; + default: + break; + } + } + + public void setFormatByName(String formatName) + { + setFormat(ResultsExportFormat.parse(formatName)); + } + + public void setDestination(ResultsExportDestination destination) + { + this.destination = destination; + } + + public void setDestinationByName(String destinationName) + { + setDestination(ResultsExportDestination.parse(destinationName)); + } + + /*public void setCustomFormat(boolean printHeader, boolean printNames, String separator, String equals) + { + this.printHeader = printHeader; + this.printNames = printNames; + this.separator = separator; + this.equals = equals; + }*/ + + public void setConstantsInfo(final List constants) + { + this.constants = constants; + } + + /** + * Get the exported results as a string (if the destination was specified to be a string). + */ + public String getExportString() + { + return exportString; + } + + // Main interface for the actual export: + // methods to be called by the class that has the results + + /** + * Start the export process. + */ + public void start() + { + String s = ""; + if (printHeader && constants != null) { + for (int i = 0; i < constants.size(); i++) { + if (i > 0) { + s += separator; + } + s += constants.get(i).getName(); + } + s += equals + "Result\n"; + } + exportString = s; + } + + /** + * Export a single result. + */ + public void exportResult(final Values values, final Object result) + { + switch (format) { + case PLAIN: + case CSV: + exportString += values.toString(printNames, separator) + equals + result + "\n"; + break; + case COMMENT: + exportString += "// RESULT (" + values.toString(true, ",") + "): " + result + "\n"; + } + } + + /** + * Finish the export process. + */ + public void end() + { + if (destination == ResultsExportDestination.STRING) { + // Strip off last \n before returning + if (exportString.charAt(exportString.length() - 1) == '\n') + exportString = exportString.substring(0, exportString.length() - 1); + } + } +}