From 27e1c1e2eb93dbe7bc5ffdb7081b0ddd4e58baed Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Tue, 28 Jul 2015 12:31:03 +0000 Subject: [PATCH] LTLModelChecker(product DTMC): replace second batch of refAlls with copies (for newAllDDVars) git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10435 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 481a8b0e..3b6cd5e8 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -262,18 +262,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 @@ -281,14 +279,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(); // Build transition matrix for product newTrans = buildTransMask(da, labelDDs, allDDRowVars, allDDColVars, daDDRowVars, daDDColVars);