From 0988f0fe132b4532fe53a5955d9eb4024315c2a1 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Thu, 12 Apr 2012 14:02:47 +0000
Subject: [PATCH] New swicth -exportdigital which only does model export once
 for digital clocks (-exportprism does it twice).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4979 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/Prism.java   | 22 +++++++++++++++++++---
 prism/src/prism/PrismCL.java | 11 +++++++++++
 2 files changed, 30 insertions(+), 3 deletions(-)

diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java
index 47467e3b..e0901157 100644
--- a/prism/src/prism/Prism.java
+++ b/prism/src/prism/Prism.java
@@ -120,6 +120,9 @@ public class Prism implements PrismSettingsListener
 	protected File exportPrismFile = null;
 	protected boolean exportPrismConst = false;
 	protected File exportPrismConstFile = null;
+	// Export digital clocks translation PRISM model?
+	protected boolean exportDigital = false;
+	protected File exportDigitalFile = null;
 	// Export target state info?
 	protected boolean exportTarget = false;
 	protected String exportTargetFilename = null;
@@ -462,6 +465,19 @@ public class Prism implements PrismSettingsListener
 		exportPrismConstFile = f;
 	}
 
+	public void setExportDigital(boolean b) throws PrismException
+	{
+		exportDigital = b;
+	}
+
+	/**
+	 * Set file to export digital clocks translation PRISM file to (null = stdout).
+	 */
+	public void setExportDigitalFile(File f) throws PrismException
+	{
+		exportDigitalFile = f;
+	}
+
 	public void setExportTarget(boolean b) throws PrismException
 	{
 		exportTarget = b;
@@ -2406,13 +2422,13 @@ public class Prism implements PrismSettingsListener
 				currentModulesFile.setUndefinedConstants(oldModulesFile.getConstantValues());
 				currentModelType = ModelType.MDP;
 				// If required, export generated PRISM model
-				if (exportPrism) {
+				if (exportDigital) {
 					try {
-						exportPRISMModel(exportPrismFile);
+						exportPRISMModel(exportDigitalFile);
 					}
 					// In case of error, just print a warning
 					catch (FileNotFoundException e) {
-						mainLog.printWarning("PRISM code export failed: Couldn't open file \"" + exportPrismFile + "\" for output");
+						mainLog.printWarning("PRISM code export failed: Couldn't open file \"" + exportDigitalFile + "\" for output");
 					} catch (PrismException e) {
 						mainLog.printWarning("PRISM code export failed: " + e.getMessage());
 					}
diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java
index 82792080..98d29cf8 100644
--- a/prism/src/prism/PrismCL.java
+++ b/prism/src/prism/PrismCL.java
@@ -1159,6 +1159,17 @@ public class PrismCL implements PrismModelListener
 						errorAndExit("No file specified for -" + sw + " switch");
 					}
 				}
+				// export digital clocks translation prism model to file
+				else if (sw.equals("exportdigital")) {
+					if (i < args.length - 1) {
+						String filename = args[++i];
+						File f = (filename.equals("stdout")) ? null : new File(filename);
+						prism.setExportDigital(true);
+						prism.setExportDigitalFile(f);
+					} else {
+						errorAndExit("No file specified for -" + sw + " switch");
+					}
+				}
 				// export reachability target info to file (hidden option)
 				else if (sw.equals("exporttarget")) {
 					if (i < args.length - 1) {