Create a new ResultsExporter class, connect it to ResultsCollection and use this from PrismCL (in some cases) to handle -exportresults.

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

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

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

prism/src/prism/ResultsExporter.java

@@ -0,0 +1,231 @@
+//==============================================================================
+//	
+//	Copyright (c) 2015-
+//	Authors:
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (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<DefinedConstant> 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<DefinedConstant> 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);
+		}
+	}
+}