From 526b0e7d8d658ad37561bf97307305aa91104108 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 15 Sep 2016 10:55:41 +0000 Subject: [PATCH] ModelGenerator2MTBDD: fix use of ModelVariablesDD, actually allocate variables via ModelVariablesDD git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11829 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/ModelGenerator2MTBDD.java | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) diff --git a/prism/src/prism/ModelGenerator2MTBDD.java b/prism/src/prism/ModelGenerator2MTBDD.java index 9b1af81e..febcfa87 100644 --- a/prism/src/prism/ModelGenerator2MTBDD.java +++ b/prism/src/prism/ModelGenerator2MTBDD.java @@ -236,9 +236,8 @@ public class ModelGenerator2MTBDD */ private void allocateDDVars() { - JDDNode v, vr, vc; + JDDNode vr, vc; int i, j, n; - int ddVarsUsed = 0; // create arrays/etc. first @@ -261,9 +260,7 @@ public class ModelGenerator2MTBDD // allocate nondeterministic variables if (modelType == ModelType.MDP) { for (i = 0; i < maxNumChoices; i++) { - v = JDD.Var(ddVarsUsed++); - ddChoiceVars[i] = v; - modelVariables.allocateVariable("l" + i); + ddChoiceVars[i] = modelVariables.allocateVariable("l" + i); } } @@ -277,14 +274,11 @@ public class ModelGenerator2MTBDD // add pairs of variables (row/col) for (j = 0; j < n; j++) { // new dd row variable - vr = JDD.Var(ddVarsUsed++); + vr = modelVariables.allocateVariable(varList.getName(i) + "." + j); // new dd col variable - vc = JDD.Var(ddVarsUsed++); + vc = modelVariables.allocateVariable(varList.getName(i) + "'." + j); varDDRowVars[i].addVar(vr); varDDColVars[i].addVar(vc); - // add names to list - modelVariables.allocateVariable(varList.getName(i) + "." + j); - modelVariables.allocateVariable(varList.getName(i) + "'." + j); } } }