From 16bbd0b24b8f4353d97511568c8846a06020e208 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Wed, 14 Sep 2016 20:32:24 +0000
Subject: [PATCH] Prism: reset currentModel and currentModelExpl to null in
 clearBuiltModel()

Generally, as soon as clearBuiltModel is called, the models should not be
touched anymore. In doBuildModel, keep the null assignments for the
model storage variable for the unused engine.


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

diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java
index 782a3d96..64f73aa0 100644
--- a/prism/src/prism/Prism.java
+++ b/prism/src/prism/Prism.java
@@ -1689,8 +1689,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		currentModelType = currentModulesFile == null ? null : currentModulesFile.getModelType();
 		currentModelInfo = currentModulesFile;
 		currentDefinedMFConstants = null;
-		currentModel = null;
-		currentModelExpl = null;
 
 		// Print basic model info
 		mainLog.println("\nType:        " + currentModulesFile.getModelType());
@@ -1736,8 +1734,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		currentModelType = currentModelGenerator == null ? null : currentModelGenerator.getModelType();
 		currentModelInfo = currentModelGenerator;
 		currentDefinedMFConstants = null;
-		currentModel = null;
-		currentModelExpl = null;
 
 		// Print basic model info
 		mainLog.println("\nGenerator:   " + currentModelGenerator.getClass().getName());
@@ -1768,9 +1764,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		if (currentModelGenerator != null) {
 			currentModelGenerator.setSomeUndefinedConstants(definedMFConstants);
 		}
-		// Reset dependent info
-		currentModel = null;
-		currentModelExpl = null;
 
 		// If required, export parsed PRISM model, with constants expanded
 		if (exportPrismConst) {
@@ -1804,7 +1797,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		currentModelType = currentModulesFile == null ? null : currentModulesFile.getModelType();
 		currentModelInfo = currentModulesFile;
 		currentDefinedMFConstants = null;
-		currentModelExpl = null;
 	}
 
 	/**
@@ -1824,7 +1816,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		// Reset dependent info
 		currentModelType = currentModel == null ? null : currentModel.getModelType();
 		currentDefinedMFConstants = null;
-		currentModelExpl = null;
 	}
 
 	/**
@@ -1854,8 +1845,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		currentModelType = currentModulesFile == null ? null : currentModulesFile.getModelType();
 		currentModelInfo = currentModulesFile;
 		currentDefinedMFConstants = null;
-		currentModel = null;
-		currentModelExpl = null;
 
 		return currentModulesFile;
 	}
@@ -2909,8 +2898,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 				currentModelType = ModelType.MDP;
 				currentModelGenerator = new ModulesFileModelGenerator(currentModulesFile, this);
 				clearBuiltModel();
-				currentModel = null;
-				currentModelExpl = null;
 				// If required, export generated PRISM model
 				if (exportDigital) {
 					try {
@@ -3610,13 +3597,16 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 
 	/**
 	 * Clear the built model if needed (free/deallocate memory etc)
+	 * <br>
+	 * Resets {@code currentModel} and {@code currentModelExpl} to {@code null}.
 	 */
 	private void clearBuiltModel()
 	{
-		if (currentModel != null)
+		if (currentModel != null) {
 			currentModel.clear();
-		/*if (currentModelExpl != null)
-			currentModelExpl.clear();*/
+			currentModel = null;
+		}
+		currentModelExpl = null;
 	}
 
 	/**