Model.export methods for any format, including .umb, .pexp, with attached labels/rewards.

Author: davexparker

prism/src/explicit/Model.java

@@ -40,9 +40,7 @@
 import common.IterableStateSet;
 import common.IteratorTools;
 import explicit.rewards.Rewards;
-import io.DotExporter;
-import io.ModelExportOptions;
-import io.PrismExplicitExporter;
+import io.*;
 import parser.State;
 import parser.Values;
 import parser.VarList;
@@ -426,6 +424,31 @@ default void prob1step(BitSet subset, BitSet u, BitSet v, BitSet result)
 	 */
 	void checkForDeadlocks(BitSet except) throws PrismException;
 
+	/**
+	 * Export to the specified model format.
+	 */
+	default void export(PrismLog out, ModelExportFormat exportFormat) throws PrismException
+	{
+		export(out, new ModelExportOptions(exportFormat));
+	}
+
+	/**
+	 * Export using the specified export options.
+	 */
+	default void export(PrismLog out, ModelExportOptions exportOptions) throws PrismException
+	{
+		// Create a model checker with {@code out} as the log and export to that
+		StateModelChecker mcExport = StateModelChecker.createModelChecker(getModelType());
+		mcExport.setLog(out);
+		// If {@code out} is backed by a real file (as opposed to stdout/the main log),
+		// pass that file through too, since some (e.g. binary) export formats need it
+		File file = null;
+		if (out instanceof PrismFileLog && !((PrismFileLog) out).isStdout()) {
+			file = new File(((PrismFileLog) out).getFileName());
+		}
+		mcExport.exportModel(this, ModelExportTask.fromOptions(file, exportOptions));
+	}
+
 	// Export methods (explicit files)
 
 	/**

prism/src/prism/PrismFileLog.java

@@ -127,6 +127,14 @@ public String getFileName()
 		return stdout ? "stdout" : filename;
 	}
 
+	/**
+	 * Is this log writing to standard output (rather than a file)?
+	 */
+	public boolean isStdout()
+	{
+		return stdout;
+	}
+
 	/**
 	 * Is this log using native code to write to the file?
 	 */