diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 515acc1b..8529ffad 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -441,32 +441,21 @@ public class PrismCL implements PrismModelListener // export results (if required) if (exportresults) { - - mainLog.print("\nExporting results "); - if (exportResultsFormat.equals("matrix")) - mainLog.print("in matrix form "); - if (!exportResultsFilename.equals("stdout")) - mainLog.println("to file \"" + exportResultsFilename + "\"..."); - else - mainLog.println("below:\n"); + ResultsExporter exporter = new ResultsExporter(exportResultsFormat, "string"); + mainLog.print("\nExporting results " + (exportResultsFormat.equals("matrix") ? "in matrix form " : "")); + mainLog.println(exportResultsFilename.equals("stdout") ? "below:\n" : "to file \"" + exportResultsFilename + "\"..."); PrismFileLog tmpLog = new PrismFileLog(exportResultsFilename); if (!tmpLog.ready()) { errorAndExit("Couldn't open file \"" + exportResultsFilename + "\" for output"); } - for (i = 0; i < numPropertiesToCheck; i++) { if (i > 0) tmpLog.println(); if (numPropertiesToCheck > 1) { - if (exportResultsFormat.equals("csv")) - tmpLog.print("\"" + propertiesToCheck.get(i) + ":\"\n"); - else - tmpLog.print(propertiesToCheck.get(i) + ":\n"); + exporter.setProperty(propertiesToCheck.get(i)); } if (!exportResultsFormat.equals("matrix")) { - ResultsExporter exporter = new ResultsExporter(exportResultsFormat, "string"); tmpLog.println(results[i].export(exporter).getExportString()); - //tmpLog.println(results[i].toString(false, sep, sep)); } else { tmpLog.println(results[i].toStringMatrix("\t")); } diff --git a/prism/src/prism/ResultsExporter.java b/prism/src/prism/ResultsExporter.java index 9676a576..a6850c25 100644 --- a/prism/src/prism/ResultsExporter.java +++ b/prism/src/prism/ResultsExporter.java @@ -29,6 +29,7 @@ package prism; import java.util.List; import parser.Values; +import parser.ast.Property; /** * Class to export the results of model checking in various formats. @@ -93,6 +94,7 @@ public class ResultsExporter }; private List constants; + private Property property; private ResultsExportFormat format = ResultsExportFormat.PLAIN; private boolean printHeader; @@ -173,6 +175,11 @@ public class ResultsExporter this.constants = constants; } + public void setProperty(final Property property) + { + this.property = property; + } + /** * Get the exported results as a string (if the destination was specified to be a string). */ @@ -189,17 +196,34 @@ public class ResultsExporter */ public void start() { - String s = ""; + // Reset output string + exportString = ""; + // Prepend property, if present + if (property != null) { + switch (format) { + case PLAIN: + exportString += property.toString() + ":\n"; + break; + case CSV: + exportString += "\"" + property.toString().replaceAll("\"", "\\\"") + "\"\n"; + break; + case COMMENT: + // None - it's printed at the the end in this case + break; + default: + break; + } + } + // Print header, if needed if (printHeader && constants != null) { for (int i = 0; i < constants.size(); i++) { if (i > 0) { - s += separator; + exportString += separator; } - s += constants.get(i).getName(); + exportString += constants.get(i).getName(); } - s += equals + "Result\n"; + exportString += equals + "Result\n"; } - exportString = s; } /** @@ -222,10 +246,15 @@ public class ResultsExporter */ public void end() { + // For "comment" format, print the property at the end, if present + if (property != null && format == ResultsExportFormat.COMMENT) { + exportString += property.toString() + "\n"; + } + // If writing to a string, strip off last \n before returning if (destination == ResultsExportDestination.STRING) { - // Strip off last \n before returning - if (exportString.charAt(exportString.length() - 1) == '\n') + if (exportString.charAt(exportString.length() - 1) == '\n') { exportString = exportString.substring(0, exportString.length() - 1); + } } } }