From 632c959a94f1f79c704a4b4c38f4b2fdf36e371a Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 12 Jul 2019 00:03:55 +0100
Subject: [PATCH] Tidy up code to call digital clocks: should generalise to
 other models better.

---
 prism/src/prism/Prism.java | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java
index 97504abf..a79ba8b0 100644
--- a/prism/src/prism/Prism.java
+++ b/prism/src/prism/Prism.java
@@ -3039,12 +3039,9 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 			try {
 				DigitalClocks dc = new DigitalClocks(this);
 				dc.translate(oldModulesFile, propertiesFile, expr);
-				currentModulesFile = dc.getNewModulesFile();
+				loadPRISMModel(dc.getNewModulesFile());
 				// evaluate constants (use exact evaluation if we are in exact computation mode)
 				currentModulesFile.setUndefinedConstants(oldModulesFile.getConstantValues(), settings.getBoolean(PrismSettings.PRISM_EXACT_ENABLED));
-				currentModelType = ModelType.MDP;
-				currentModelGenerator = new ModulesFileModelGenerator(currentModulesFile, this);
-				clearBuiltModel();
 				// If required, export generated PRISM model
 				if (exportDigital) {
 					try {
@@ -3061,7 +3058,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 			} finally {
 				digital = false;
 				currentModulesFile = oldModulesFile;
-				currentModelType = ModelType.PTA;
+				currentModelType = oldModulesFile.getModelType();
 				clearBuiltModel();
 				currentModel = null;
 				currentModelExpl = null;