From 25b65c4f26d7d868b3def416a71cc59998d81d8d Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Thu, 21 Oct 2010 11:36:36 +0000
Subject: [PATCH] Added -exportprismconst switch.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2178 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/NOTES                  |  3 +++
 prism/src/prism/PrismCL.java | 46 ++++++++++++++++++++++++++++++++----
 2 files changed, 44 insertions(+), 5 deletions(-)

diff --git a/prism/NOTES b/prism/NOTES
index 843b6da1..fe544269 100644
--- a/prism/NOTES
+++ b/prism/NOTES
@@ -16,6 +16,9 @@ PTAs:
 * non-zeno checks?
 * Sort VarList (two types - before and after constants evaluated). Need for simulator too.
 
+Sim(?):
+* Auto x100 in GUI sim doesn't stop on even simple loops
+
 =======================================================
 
 TODO (before public release)
diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java
index e82bb5af..6e70d7fc 100644
--- a/prism/src/prism/PrismCL.java
+++ b/prism/src/prism/PrismCL.java
@@ -58,6 +58,7 @@ public class PrismCL
 	private boolean exportbsccs = false;
 	private boolean exportresults = false;
 	private boolean exportprism = false;
+	private boolean exportprismconst = false;
 	private boolean exportPlainDeprecated = false;
 	private int exportType = Prism.EXPORT_PLAIN;
 	private boolean exportordered = true;
@@ -97,6 +98,7 @@ public class PrismCL
 	private String exportResultsFilename = null;
 	private String exportTransientFilename = null;
 	private String exportPrismFilename = null;
+	private String exportPrismConstFilename = null;
 	private String simpathFilename = null;
 
 	// logs
@@ -230,13 +232,37 @@ public class PrismCL
 
 			// output final prism model here if required
 			if (exportprism) {
+				mainLog.print("\nExporting parsed PRISM file ");
+				if (!exportPrismFilename.equals("stdout"))
+					mainLog.println("to file \"" + exportPrismFilename + "\"...");
+				else
+					mainLog.println("below:");
+				PrismFileLog tmpLog = new PrismFileLog(exportPrismFilename);
+				if (!tmpLog.ready()) {
+					errorAndExit("Couldn't open file \"" + exportPrismFilename + "\" for output");
+				}
+				tmpLog.print(modulesFile.toString());
+			}
+			if (exportprismconst) {
+				mainLog.print("\nExporting parsed PRISM file (with constant expansion) ");
+				if (!exportPrismConstFilename.equals("stdout"))
+					mainLog.println("to file \"" + exportPrismConstFilename + "\"...");
+				else
+					mainLog.println("below:");
+				PrismFileLog tmpLog = new PrismFileLog(exportPrismConstFilename);
+				if (!tmpLog.ready()) {
+					errorAndExit("Couldn't open file \"" + exportPrismConstFilename + "\" for output");
+				}
+				ModulesFile mfTmp = (ModulesFile) modulesFile.deepCopy();
 				try {
-					FileWriter writer = new FileWriter(exportPrismFilename);
-					writer.write(modulesFile.toString());
-					writer.close();
-				} catch (IOException e) {
-					error("Could not export PRISM model to file \"" + exportPrismFilename + "\"");
+					mfTmp = (ModulesFile) mfTmp.replaceConstants(modulesFile.getConstantValues());
+					mfTmp = (ModulesFile) mfTmp.replaceConstants(definedMFConstants);
+					// NB: Don't use simplify() here because doesn't work for the purposes of printing out
+					// (e.g. loss of parethenses causes precedence problems)
+				} catch (PrismLangException e) {
+					error(e.getMessage());
 				}
+				tmpLog.print(mfTmp.toString());
 			}
 
 			// decide if model construction is necessary
@@ -1019,6 +1045,15 @@ public class PrismCL
 						errorAndExit("No file specified for -" + sw + " switch");
 					}
 				}
+				// export prism model to file (with consts expanded)
+				else if (sw.equals("exportprismconst")) {
+					if (i < args.length - 1) {
+						exportprismconst = true;
+						exportPrismConstFilename = args[++i];
+					} else {
+						errorAndExit("No file specified for -" + sw + " switch");
+					}
+				}
 				// export adversary to file
 				else if (sw.equals("exportadv")) {
 					if (i < args.length - 1) {
@@ -1742,6 +1777,7 @@ public class PrismCL
 		mainLog.println("-exportbsccs <file> ............ Compute and export all BSCCs of the model");
 		mainLog.println("-exporttransient <file> ........ Export transient probabilities to a file");
 		mainLog.println("-exportprism <file> ............ Export final PRISM model to a file");
+		mainLog.println("-exportprismconst <file> ....... Export final PRISM model with expanded constants to a file");
 		mainLog.println();
 		mainLog.println("-mtbdd (or -m) ................. Use the MTBDD engine");
 		mainLog.println("-sparse (or -s) ................ Use the Sparse engine");