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

@@ -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...");

prism/src/prism/Prism.java

@@ -117,6 +117,11 @@ 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; }
 	

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) {