Added exportprod{states,trans} functionality to D/CTMC model checker too.

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

prism/src/prism/ProbModelChecker.java

@@ -617,8 +617,19 @@ public class ProbModelChecker extends NonProbModelChecker
 		modelProduct = mcLtl.constructProductMC(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() + "\"...");
+				modelProduct.exportToFile(Prism.EXPORT_PLAIN, true, new File(prism.getExportProductTransFilename()));
+			} catch (FileNotFoundException e) {
+				mainLog.printWarning("Could not export product transition matrix to file \"" + prism.getExportProductTransFilename() + "\"");
+			}
+		}
+		if (prism.getExportProductStates()) {
+			mainLog.println("\nExporting product state space to file \"" + prism.getExportProductStatesFilename() + "\"...");
+			modelProduct.exportStates(Prism.EXPORT_PLAIN, new PrismFileLog(prism.getExportProductStatesFilename()));
+		}
 
 		// Find accepting maximum end BSCC
 		mainLog.println("\nFinding accepting BSCCs...");