From 249f45118cfbf36f44c1ebaf031c9246942a7942 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Tue, 28 Jul 2015 12:30:28 +0000 Subject: [PATCH] LTLModelChecker(product DTMC): simplify handling of daDDVarsCopy parameters git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10433 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/LTLModelChecker.java | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index dd36a0e2..dc1ba773 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -236,10 +236,8 @@ public class LTLModelChecker extends PrismComponent before = false; } - // If passed in var lists are null, create new lists - // (which won't be accessible later in this case) - daDDRowVars = (daDDRowVarsCopy == null) ? new JDDVars() : daDDRowVarsCopy; - daDDColVars = (daDDColVarsCopy == null) ? new JDDVars() : daDDColVarsCopy; + daDDRowVars = new JDDVars(); + daDDColVars = new JDDVars(); // Create the new dd variables newDDVarNames = new Vector(); newDDVarNames.addAll(ddVarNames); @@ -295,6 +293,8 @@ 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); @@ -345,11 +345,14 @@ public class LTLModelChecker extends PrismComponent newStart = JDD.And(model.getStart(), newStart); modelProd.setStart(newStart); - // Reference DA DD vars (if being returned) + // if possible, return copies of the DA DD variables via the method parameters if (daDDRowVarsCopy != null) - daDDRowVarsCopy.refAll(); + daDDRowVarsCopy.copyVarsFrom(daDDRowVars); if (daDDColVarsCopy != null) - daDDColVarsCopy.refAll(); + daDDColVarsCopy.copyVarsFrom(daDDColVars); + + daDDRowVars.derefAll(); + daDDColVars.derefAll(); return modelProd; }