Some fixes in the way comments are displayed when exporting results (+ associated refactoring).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10156 bbc10eb1-c90d-0410-af57-cb519fbb1720

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"));
 				}

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<DefinedConstant> 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);
+			}
 		}
 	}
 }