From 3bbbf4be9fbce223f66569996aa314895b4d227e Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Thu, 9 Feb 2012 22:51:34 +0000
Subject: [PATCH] Fix (reinstate) exportprism option for digital clocks
 generated model.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4567 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/Prism.java | 18 +++++++++++++-----
 1 file changed, 13 insertions(+), 5 deletions(-)

diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java
index 5630a338..8707c932 100644
--- a/prism/src/prism/Prism.java
+++ b/prism/src/prism/Prism.java
@@ -2235,7 +2235,7 @@ public class Prism implements PrismSettingsListener
 	{
 		Result res = null;
 
-		if (!digital) // TODO: if "non-nested"
+		if (!digital)
 			mainLog.printSeparator();
 		mainLog.println("\nModel checking: " + expr);
 		if (currentDefinedMFConstants != null && currentDefinedMFConstants.getNumValues() > 0)
@@ -2324,10 +2324,18 @@ public class Prism implements PrismSettingsListener
 				currentModulesFile = dc.getNewModulesFile();
 				currentModulesFile.setUndefinedConstants(oldModulesFile.getConstantValues());
 				currentModelType = ModelType.MDP;
-				/*if (exportprism) {
-					
-				}*/
-				//  TODO doPrismLangExports(modulesFileToCheck);
+				// If required, export generated PRISM model
+				if (exportPrism) {
+					try {
+						exportPRISMModel(exportPrismFile);
+					}
+					// In case of error, just print a warning
+					catch (FileNotFoundException e) {
+						mainLog.printWarning("PRISM code export failed: Couldn't open file \"" + exportPrismFile + "\" for output");
+					} catch (PrismException e) {
+						mainLog.printWarning("PRISM code export failed: " + e.getMessage());
+					}
+				}
 				return modelCheck(propertiesFile, expr, definedPFConstants);
 			} finally {
 				digital = false;