From e9518b6448d812b5cd1b3fb06fb5bc8f02d566d3 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Thu, 18 Aug 2011 18:29:09 +0000
Subject: [PATCH] Added -exportprodtrans and -exportprodstates switches.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3508 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/NondetModelChecker.java | 21 ++++++++++--
 prism/src/prism/Prism.java              | 45 +++++++++++++++++++++++--
 prism/src/prism/PrismCL.java            | 18 ++++++++++
 3 files changed, 80 insertions(+), 4 deletions(-)

diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java
index 2173d4a1..5fb332e2 100644
--- a/prism/src/prism/NondetModelChecker.java
+++ b/prism/src/prism/NondetModelChecker.java
@@ -27,6 +27,7 @@
 
 package prism;
 
+import java.io.File;
 import java.io.FileNotFoundException;
 import java.util.*;
 
@@ -449,8 +450,24 @@ public class NondetModelChecker extends NonProbModelChecker
 		modelProduct = mcLtl.constructProductMDP(dra, model, labelDDs, draDDRowVars, draDDColVars);
 		mainLog.println();
 		modelProduct.printTransInfo(mainLog, prism.getExtraDDInfo());
-		// prism.exportStatesToFile(modelProduct, Prism.EXPORT_PLAIN, null);
-		// prism.exportTransToFile(modelProduct, true, Prism.EXPORT_PLAIN, null);
+		// Output product, if required
+		if (prism.getExportProductTrans()) {
+			try {
+				mainLog.println("\nExporting product transition matrix to file \"" + prism.getExportProductTransFilename() + "\"...");
+				prism.exportTransToFile(modelProduct, true, Prism.EXPORT_PLAIN, new File(prism.getExportProductTransFilename()));
+			} catch (FileNotFoundException e) {
+				mainLog.println("\nWarning: Could not export product transition matrix to file \"" + prism.getExportProductTransFilename() + "\"");
+			}
+		}
+		if (prism.getExportProductStates()) {
+			try {
+				mainLog.println("\nExporting product state space to file \"" + prism.getExportProductStatesFilename() + "\"...");
+				prism.exportTransToFile(modelProduct, true, Prism.EXPORT_PLAIN, new File(prism.getExportProductStatesFilename()));
+				prism.exportStatesToFile(modelProduct, Prism.EXPORT_PLAIN, new File(prism.getExportProductStatesFilename()));
+			} catch (FileNotFoundException e) {
+				mainLog.println("\nWarning: Could not export product state space to file \"" + prism.getExportProductStatesFilename() + "\"");
+			}
+		}
 
 		// Find accepting maximum end components
 		mainLog.println("\nFinding accepting end components...");
diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java
index 0d37dccc..38bb5845 100644
--- a/prism/src/prism/Prism.java
+++ b/prism/src/prism/Prism.java
@@ -117,7 +117,12 @@ public class Prism implements PrismSettingsListener
 	// Export target state info?
 	protected boolean exportTarget;
 	protected String exportTargetFilename;
-	
+	// Export product model info?
+	protected boolean exportProductTrans;
+	protected String exportProductTransFilename;
+	protected boolean exportProductStates;
+	protected String exportProductStatesFilename;
+		
 	// A few miscellaneous options (i.e. defunct/hidden/undocumented/etc.)
 	// See constructor below for default values
 	
@@ -208,6 +213,10 @@ public class Prism implements PrismSettingsListener
 		// default values for miscellaneous options 
 		exportTarget = false;
 		exportTargetFilename = null;
+		exportProductTrans = false;
+		exportProductTransFilename = null;
+		exportProductStates = false;
+		exportProductStatesFilename = null;
 		doReach = true;
 		bsccComp = true;
 		checkZeroLoops = false;
@@ -380,6 +389,26 @@ public class Prism implements PrismSettingsListener
 		exportTargetFilename = s;
 	}
 	
+	public void setExportProductTrans(boolean b) throws PrismException
+	{
+		exportProductTrans = b;
+	}
+	
+	public void setExportProductTransFilename(String s) throws PrismException
+	{
+		exportProductTransFilename = s;
+	}
+	
+	public void setExportProductStates(boolean b) throws PrismException
+	{
+		exportProductStates = b;
+	}
+	
+	public void setExportProductStatesFilename(String s) throws PrismException
+	{
+		exportProductStatesFilename = s;
+	}
+	
 	public void setDoReach(boolean b) throws PrismException
 	{
 		doReach = b;
@@ -494,11 +523,23 @@ public class Prism implements PrismSettingsListener
 	// Get methods for miscellaneous options
 	
 	public boolean getExportTarget()
-	{return exportTarget; }
+	{ return exportTarget; }
 	
 	public String getExportTargetFilename()
 	{ return exportTargetFilename; }
 	
+	public boolean getExportProductTrans()
+	{ return exportProductTrans; }
+	
+	public String getExportProductTransFilename()
+	{ return exportProductTransFilename; }
+	
+	public boolean getExportProductStates()
+	{ return exportProductStates; }
+	
+	public String getExportProductStatesFilename()
+	{ return exportProductStatesFilename; }
+	
 	public boolean getDoReach()
 	{ return doReach; }
 	
diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java
index 9d66402a..39ba4df4 100644
--- a/prism/src/prism/PrismCL.java
+++ b/prism/src/prism/PrismCL.java
@@ -1387,6 +1387,24 @@ public class PrismCL
 						errorAndExit("No file specified for -" + sw + " switch");
 					}
 				}
+				// export product transition matrix to file (hidden option)
+				else if (sw.equals("exportprodtrans")) {
+					if (i < args.length - 1) {
+						prism.setExportProductTrans(true);
+						prism.setExportProductTransFilename(args[++i]);
+					} else {
+						errorAndExit("No file specified for -" + sw + " switch");
+					}
+				}
+				// export product states to file (hidden option)
+				else if (sw.equals("exportprodstates")) {
+					if (i < args.length - 1) {
+						prism.setExportProductStates(true);
+						prism.setExportProductStatesFilename(args[++i]);
+					} else {
+						errorAndExit("No file specified for -" + sw + " switch");
+					}
+				}
 				// export model to plain text file (deprecated option so hidden)
 				else if (sw.equals("exportplain")) {
 					if (i < args.length - 1) {