From c9c313e796e8838b6d46a16851159d3b6088a3da Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Tue, 28 Jul 2015 12:30:49 +0000 Subject: [PATCH] LTLModelChecker(product DTMC): replace first batch of daDDVars refAll with copies git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10434 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/LTLModelChecker.java | 16 +++++----------- 1 file changed, 5 insertions(+), 11 deletions(-) diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index dc1ba773..481a8b0e 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -212,7 +212,7 @@ public class LTLModelChecker extends PrismComponent int i, j, n; boolean before; - // Get details of old model + // Get details of old model (no copy, does not need to be cleaned up) varDDRowVars = model.getVarDDRowVars(); varDDColVars = model.getVarDDColVars(); allDDRowVars = model.getAllDDRowVars(); @@ -256,13 +256,11 @@ public class LTLModelChecker extends PrismComponent // Create/populate new lists newVarDDRowVars = new JDDVars[varDDRowVars.length + 1]; newVarDDColVars = new JDDVars[varDDRowVars.length + 1]; - newVarDDRowVars[before ? 0 : varDDRowVars.length] = daDDRowVars; - newVarDDColVars[before ? 0 : varDDColVars.length] = daDDColVars; + newVarDDRowVars[before ? 0 : varDDRowVars.length] = daDDRowVars.copy(); + newVarDDColVars[before ? 0 : varDDColVars.length] = daDDColVars.copy(); for (i = 0; i < varDDRowVars.length; i++) { - newVarDDRowVars[before ? i + 1 : i] = new JDDVars(); - newVarDDColVars[before ? i + 1 : i] = new JDDVars(); - newVarDDRowVars[before ? i + 1 : i].addVars(varDDRowVars[i]); - newVarDDColVars[before ? i + 1 : i].addVars(varDDColVars[i]); + newVarDDRowVars[before ? i + 1 : i] = varDDRowVars[i].copy(); + newVarDDColVars[before ? i + 1 : i] = varDDColVars[i].copy(); } newAllDDRowVars = new JDDVars(); newAllDDColVars = new JDDVars(); @@ -284,8 +282,6 @@ public class LTLModelChecker extends PrismComponent // Extra references (because will get derefed when new model is done with) allDDRowVars.refAll(); - allDDRowVars.refAll(); - allDDColVars.refAll(); allDDColVars.refAll(); for (i = 0; i < model.getNumModules(); i++) { model.getModuleDDRowVars(i).refAll(); @@ -293,8 +289,6 @@ public class LTLModelChecker extends PrismComponent } daDDRowVars.refAll(); daDDColVars.refAll(); - daDDRowVars.refAll(); - daDDColVars.refAll(); // Build transition matrix for product newTrans = buildTransMask(da, labelDDs, allDDRowVars, allDDColVars, daDDRowVars, daDDColVars);