From b840d7f3a33b45276222497b4385fb834ebc4943 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Thu, 9 Feb 2012 23:10:59 +0000
Subject: [PATCH] Make sure Prism takes care of clear()ing models.

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

diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java
index 8707c932..c3ec154d 100644
--- a/prism/src/prism/Prism.java
+++ b/prism/src/prism/Prism.java
@@ -1400,6 +1400,8 @@ public class Prism implements PrismSettingsListener
 		currentModelSource = ModelSource.PRISM_MODEL;
 		// Store PRISM model
 		currentModulesFile = modulesFile;
+		// Clear any existing built model(s)
+		clearBuiltModel();
 		// Reset dependent info
 		currentModelType = currentModulesFile == null ? null : currentModulesFile.getModelType();
 		currentDefinedMFConstants = null;
@@ -1444,6 +1446,8 @@ public class Prism implements PrismSettingsListener
 		if (currentDefinedMFConstants != null && currentDefinedMFConstants.equals(definedMFConstants))
 			return;
 
+		// Clear any existing built model(s)
+		clearBuiltModel();
 		// Store constants here and in ModulesFile
 		currentDefinedMFConstants = definedMFConstants;
 		currentModulesFile.setUndefinedConstants(definedMFConstants);
@@ -1474,6 +1478,8 @@ public class Prism implements PrismSettingsListener
 	public void loadPRISMModelAndBuiltModel(ModulesFile modulesFile, Model model)
 	{
 		currentModelSource = ModelSource.PRISM_MODEL;
+		// Clear any existing built model(s)
+		clearBuiltModel();
 		// Store model info
 		currentModulesFile = modulesFile;
 		currentModel = model;
@@ -1492,6 +1498,8 @@ public class Prism implements PrismSettingsListener
 	public void loadBuiltModel(Model model)
 	{
 		currentModelSource = ModelSource.BUILT_MODEL;
+		// Clear any existing built model(s)
+		clearBuiltModel();
 		// Store model info
 		currentModulesFile = null;
 		currentModel = model;
@@ -1512,6 +1520,8 @@ public class Prism implements PrismSettingsListener
 	public ModulesFile loadModelFromExplicitFiles(File statesFile, File transFile, File labelsFile, ModelType typeOverride) throws PrismException
 	{
 		currentModelSource = ModelSource.EXPLICIT_FILES;
+		// Clear any existing built model(s)
+		clearBuiltModel();
 		// Create ExplicitFiles2MTBDD object and build state space
 		expf2mtbdd = new ExplicitFiles2MTBDD(this, statesFile, transFile, labelsFile, typeOverride);
 		currentModulesFile = expf2mtbdd.buildStates();
@@ -1611,6 +1621,9 @@ public class Prism implements PrismSettingsListener
 	{
 		long l; // timer
 
+		// Clear any existing built model(s)
+		clearBuiltModel();
+		
 		try {
 			if (currentModulesFile == null)
 				throw new PrismException("There is no currently loaded PRISM model to build");
@@ -2677,15 +2690,14 @@ public class Prism implements PrismSettingsListener
 	}
 
 	/**
-	 * Clear the built model (free/deallocate memory etc)
+	 * Clear the built model if needed (free/deallocate memory etc)
 	 */
-	public void clearBuiltModel()
+	private void clearBuiltModel()
 	{
 		if (currentModel != null)
 			currentModel.clear();
-		// TODO: if (currentModelExpl != null)
-		//currentModelExpl.clear();
-		loadBuiltModel(null);
+		/*if (currentModelExpl != null)
+			currentModelExpl.clear();*/
 	}
 
 	/**
@@ -2702,6 +2714,8 @@ public class Prism implements PrismSettingsListener
 	 */
 	public void closeDown(boolean check)
 	{
+		// Clear any built model(s)
+		clearBuiltModel();
 		// Close down engines
 		PrismMTBDD.closeDown();
 		PrismSparse.closeDown();
diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java
index 97a301ee..c7ff6fb1 100644
--- a/prism/src/prism/PrismCL.java
+++ b/prism/src/prism/PrismCL.java
@@ -345,9 +345,6 @@ public class PrismCL
 				}
 			}
 			
-			// clear model
-			prism.clearBuiltModel();
-
 			// iterate to next model
 			undefinedMFConstants.iterateModel();
 			for (j = 0; j < numPropertiesToCheck; j++) {