First version of -exportvector <file> switch for the command-line.

Exports the value of a model checked property for all states as a vector.
If <file> is "stdout", this is displayed to the log instead of a file.
Currently, only works for a single property: if there is more than one,
then the file gets overwritten each time a property is checked.

Also fixes a bug in the underlying mechanism for storing results vectors
in the explicit engine (within Results objects).

prism-tests/functionality/export/vector/exportvector.prism

@@ -0,0 +1,11 @@
+dtmc
+
+const int N;
+
+module M
+
+	x : [-N..N] init 0;
+	
+	[] true -> 0.5:(x'=max(x-1,-N)) + 0.5:(x'=min(x+1,N));
+
+endmodule

prism-tests/functionality/export/vector/exportvector.prism.args

@@ -0,0 +1,4 @@
+-ex
+#-m
+-s
+-h

prism-tests/functionality/export/vector/exportvector.prism.props

@@ -0,0 +1,2 @@
+// RESULT: 1.0
+P=? [ F<=3 x=0 ];

prism-tests/functionality/export/vector/exportvector.prism.props.args

@@ -0,0 +1 @@
+-const N=3 -exportvector exportvector.prism.props.txt

prism-tests/functionality/export/vector/exportvector.prism.props.txt

@@ -0,0 +1,7 @@
+0.125
+0.25
+0.625
+1.0
+0.625
+0.25
+0.125

prism/src/explicit/StateModelChecker.java

@@ -572,7 +572,6 @@ public class StateModelChecker extends PrismComponent
 
 		// Clean up
 		//vals.clear();
-		result.setVector(vals);
 
 		// Return result
 		return result;

prism/src/prism/PrismCL.java

@@ -86,6 +86,7 @@ public class PrismCL implements PrismModelListener
 	private boolean exportresults = false;
 	private boolean exportresultsmatrix = false;
 	private String exportResultsFormat = "plain";
+	private boolean exportvector = false;
 	private boolean exportPlainDeprecated = false;
 	private boolean exportModelNoBasename = false;
 	private int exportType = Prism.EXPORT_PLAIN;
@@ -140,6 +141,7 @@ public class PrismCL implements PrismModelListener
 	private String exportBSCCsFilename = null;
 	private String exportMECsFilename = null;
 	private String exportResultsFilename = null;
+	private String exportVectorFilename = null;
 	private String exportSteadyStateFilename = null;
 	private String exportTransientFilename = null;
 	private String exportStratFilename = null;
@@ -446,6 +448,24 @@ public class PrismCL implements PrismModelListener
 							}
 						}
 
+						// if a results vector was stored, and we need to export it, do so
+						if (exportvector && res.getVector() != null) {
+							mainLog.print("\nExporting vector of results for all states ");
+							mainLog.println(exportVectorFilename.equals("stdout") ? "below:" : "to file \"" + exportVectorFilename + "\"...");
+							PrismFileLog tmpLog = new PrismFileLog(exportVectorFilename);
+							if (!tmpLog.ready()) {
+								errorAndExit("Couldn't open file \"" + exportVectorFilename + "\" for output");
+							}
+							boolean toStdout = exportVectorFilename.equals("stdout");
+							try {
+								res.getVector().print(tmpLog, false, false, toStdout, toStdout);
+							} catch (PrismException e) {
+								error(e.getMessage());
+							}
+							res.getVector().clear();
+							tmpLog.close();
+						}
+						
 						// if required, check result against expected value
 						if (test) {
 							doResultTest(propertiesToCheck.get(j), res);
@@ -1360,6 +1380,16 @@ public class PrismCL implements PrismModelListener
 						errorAndExit("No file/options specified for -" + sw + " switch");
 					}
 				}
+				// export vector of results
+				else if (sw.equals("exportvector")) {
+					if (i < args.length - 1) {
+						exportvector = true;
+						exportVectorFilename = args[++i];
+						prism.setStoreVector(true);
+					} else {
+						errorAndExit("No file specified for -" + sw + " switch");
+					}
+				}
 				// export model to explicit file(s)
 				else if (sw.equals("exportmodel")) {
 					if (i < args.length - 1) {

prism/src/prism/StateVector.java

@@ -45,4 +45,9 @@ public interface StateVector
 	 * Clear the vector, i.e. free any used memory.
 	 */
 	public void clear();
+	
+	/**
+	 * Print vector to a log/file (non-zero/non-false entries only).
+	 */
+	public void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates, boolean printIndices) throws PrismException;
 }