From 5b29bd5433c6a5319075a07cd4b58047c1acc56e Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Tue, 28 Jul 2015 12:32:32 +0000
Subject: [PATCH] LTLModelChecker(product MDP): replace second batch of refAlls
 with copies (for newAllDDVars)

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

diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java
index 239ccf88..9b3dc4c3 100644
--- a/prism/src/prism/LTLModelChecker.java
+++ b/prism/src/prism/LTLModelChecker.java
@@ -452,18 +452,16 @@ public class LTLModelChecker extends PrismComponent
 			newVarDDRowVars[before ? i + 1 : i] = varDDRowVars[i].copy();
 			newVarDDColVars[before ? i + 1 : i] = varDDColVars[i].copy();
 		}
-		newAllDDRowVars = new JDDVars();
-		newAllDDColVars = new JDDVars();
 		if (before) {
-			newAllDDRowVars.addVars(daDDRowVars);
-			newAllDDColVars.addVars(daDDColVars);
-			newAllDDRowVars.addVars(allDDRowVars);
-			newAllDDColVars.addVars(allDDColVars);
+			newAllDDRowVars = daDDRowVars.copy();
+			newAllDDColVars = daDDColVars.copy();
+			newAllDDRowVars.copyVarsFrom(allDDRowVars);
+			newAllDDColVars.copyVarsFrom(allDDColVars);
 		} else {
-			newAllDDRowVars.addVars(allDDRowVars);
-			newAllDDColVars.addVars(allDDColVars);
-			newAllDDRowVars.addVars(daDDRowVars);
-			newAllDDColVars.addVars(daDDColVars);
+			newAllDDRowVars = allDDRowVars.copy();
+			newAllDDColVars = allDDColVars.copy();
+			newAllDDRowVars.copyVarsFrom(daDDRowVars);
+			newAllDDColVars.copyVarsFrom(daDDColVars);
 		}
 		newVarList = (VarList) varList.clone();
 		// NB: if DA only has one state, we add an extra dummy state
@@ -471,14 +469,10 @@ public class LTLModelChecker extends PrismComponent
 		newVarList.addVar(before ? 0 : varList.getNumVars(), decl, 1, model.getConstantValues());
 
 		// Extra references (because will get derefed when new model is done with)
-		allDDRowVars.refAll();
-		allDDColVars.refAll();
 		for (i = 0; i < model.getNumModules(); i++) {
 			model.getModuleDDRowVars(i).refAll();
 			model.getModuleDDColVars(i).refAll();
 		}
-		daDDRowVars.refAll();
-		daDDColVars.refAll();
 		model.getAllDDSchedVars().refAll();
 		model.getAllDDSynchVars().refAll();
 		model.getAllDDChoiceVars().refAll();