diff --git a/prism/src/prism/ExplicitFiles2MTBDD.java b/prism/src/prism/ExplicitFiles2MTBDD.java index 936ac088..8d8e290f 100644 --- a/prism/src/prism/ExplicitFiles2MTBDD.java +++ b/prism/src/prism/ExplicitFiles2MTBDD.java @@ -98,8 +98,9 @@ public class ExplicitFiles2MTBDD private JDDNode[] ddSynchVars; // individual dd vars for synchronising actions private JDDNode[] ddSchedVars; // individual dd vars for scheduling non-det. private JDDNode[] ddChoiceVars; // individual dd vars for local non-det. - // names for all dd vars used - private Vector ddVarNames; + + private ModelVariablesDD modelVariables; + // action info private Vector synchs; // list of action names private JDDNode transActions; // dd for transition action labels (MDPs) @@ -130,7 +131,8 @@ public class ExplicitFiles2MTBDD varList = modulesFile.createVarList(); numVars = varList.getNumVars(); this.numStates = numStates; - + modelVariables = new ModelVariablesDD(); + // Build states list, if info is available if (statesFile != null) { readStatesFromFile(); @@ -259,14 +261,14 @@ public class ExplicitFiles2MTBDD // create new Model object to be returned if (modelType == ModelType.DTMC) { - model = new ProbModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, ddVarNames, numModules, + model = new ProbModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, modelVariables, numModules, moduleNames, moduleDDRowVars, moduleDDColVars, numVars, varList, varDDRowVars, varDDColVars, constantValues); } else if (modelType == ModelType.MDP) { model = new NondetModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, allDDSynchVars, - allDDSchedVars, allDDChoiceVars, allDDNondetVars, ddVarNames, numModules, moduleNames, moduleDDRowVars, moduleDDColVars, numVars, varList, + allDDSchedVars, allDDChoiceVars, allDDNondetVars, modelVariables, numModules, moduleNames, moduleDDRowVars, moduleDDColVars, numVars, varList, varDDRowVars, varDDColVars, constantValues); } else if (modelType == ModelType.CTMC) { - model = new StochModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, ddVarNames, numModules, + model = new StochModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, modelVariables, numModules, moduleNames, moduleDDRowVars, moduleDDColVars, numVars, varList, varDDRowVars, varDDColVars, constantValues); } // set action info @@ -372,11 +374,11 @@ public class ExplicitFiles2MTBDD */ private void allocateDDVars() { - JDDNode v, vr, vc; int i, j, n; - int ddVarsUsed = 0; - ddVarNames = new Vector(); + modelVariables = new ModelVariablesDD(); + + // create arrays/etc. first // nondeterministic variables @@ -398,9 +400,7 @@ public class ExplicitFiles2MTBDD // allocate nondeterministic variables if (modelType == ModelType.MDP) { for (i = 0; i < maxNumChoices; i++) { - v = JDD.Var(ddVarsUsed++); - ddChoiceVars[i] = v; - ddVarNames.add("l" + i); + ddChoiceVars[i] = modelVariables.allocateVariable("l" + i); } } @@ -414,14 +414,9 @@ public class ExplicitFiles2MTBDD // add pairs of variables (row/col) for (j = 0; j < n; j++) { // new dd row variable - vr = JDD.Var(ddVarsUsed++); + varDDRowVars[i].addVar(modelVariables.allocateVariable(varList.getName(i) + "." + j)); // new dd col variable - vc = JDD.Var(ddVarsUsed++); - varDDRowVars[i].addVar(vr); - varDDColVars[i].addVar(vc); - // add names to list - ddVarNames.add(varList.getName(i) + "." + j); - ddVarNames.add(varList.getName(i) + "'." + j); + varDDColVars[i].addVar(modelVariables.allocateVariable(varList.getName(i) + "'." + j)); } } } diff --git a/prism/src/prism/ExplicitModel2MTBDD.java b/prism/src/prism/ExplicitModel2MTBDD.java index 5eab016e..cde9f70b 100644 --- a/prism/src/prism/ExplicitModel2MTBDD.java +++ b/prism/src/prism/ExplicitModel2MTBDD.java @@ -84,8 +84,9 @@ public class ExplicitModel2MTBDD private JDDNode[] ddSynchVars; // individual dd vars for synchronising actions private JDDNode[] ddSchedVars; // individual dd vars for scheduling non-det. private JDDNode[] ddChoiceVars; // individual dd vars for local non-det. - // names for all dd vars used - private Vector ddVarNames; + + private ModelVariablesDD modelVariables; + // action info private Vector synchs; // list of action names private JDDNode transActions; // dd for transition action labels (MDPs) @@ -188,14 +189,14 @@ public class ExplicitModel2MTBDD // Create new Model object to be returned if (modelType == ModelType.DTMC) { - model = new ProbModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, ddVarNames, numModules, + model = new ProbModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, modelVariables, numModules, moduleNames, moduleDDRowVars, moduleDDColVars, numVars, varList, varDDRowVars, varDDColVars, constantValues); } else if (modelType == ModelType.MDP) { model = new NondetModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, allDDSynchVars, - allDDSchedVars, allDDChoiceVars, allDDNondetVars, ddVarNames, numModules, moduleNames, moduleDDRowVars, moduleDDColVars, numVars, varList, + allDDSchedVars, allDDChoiceVars, allDDNondetVars, modelVariables, numModules, moduleNames, moduleDDRowVars, moduleDDColVars, numVars, varList, varDDRowVars, varDDColVars, constantValues); } else if (modelType == ModelType.CTMC) { - model = new StochModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, ddVarNames, numModules, + model = new StochModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, modelVariables, numModules, moduleNames, moduleDDRowVars, moduleDDColVars, numVars, varList, varDDRowVars, varDDColVars, constantValues); } // Set action info @@ -256,11 +257,10 @@ public class ExplicitModel2MTBDD private void allocateDDVars() { - JDDNode v, vr, vc; int i, j, n; - int ddVarsUsed = 0; - ddVarNames = new Vector(); + modelVariables = new ModelVariablesDD(); + // create arrays/etc. first // nondeterministic variables @@ -282,9 +282,7 @@ public class ExplicitModel2MTBDD // allocate nondeterministic variables if (modelType == ModelType.MDP) { for (i = 0; i < maxNumChoices; i++) { - v = JDD.Var(ddVarsUsed++); - ddChoiceVars[i] = v; - ddVarNames.add("l" + i); + ddChoiceVars[i] = modelVariables.allocateVariable("l" + i); } } @@ -298,14 +296,9 @@ public class ExplicitModel2MTBDD // add pairs of variables (row/col) for (j = 0; j < n; j++) { // new dd row variable - vr = JDD.Var(ddVarsUsed++); + varDDRowVars[i].addVar(modelVariables.allocateVariable(varList.getName(i) + "." + j)); // new dd col variable - vc = JDD.Var(ddVarsUsed++); - varDDRowVars[i].addVar(vr); - varDDColVars[i].addVar(vc); - // add names to list - ddVarNames.add(varList.getName(i) + "." + j); - ddVarNames.add(varList.getName(i) + "'." + j); + varDDColVars[i].addVar(modelVariables.allocateVariable(varList.getName(i) + "'." + j)); } } } diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index a98a2e39..b70297a1 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -250,19 +250,18 @@ public class LTLModelChecker extends PrismComponent JDDVars varDDColVars[]; JDDVars allDDRowVars; JDDVars allDDColVars; - Vector ddVarNames; VarList varList; // New (product) model - dds, vars, etc. JDDNode newTrans, newStart; JDDVars newVarDDRowVars[], newVarDDColVars[]; JDDVars newAllDDRowVars, newAllDDColVars; - Vector newDDVarNames; + ModelVariablesDD newModelVariables; VarList newVarList; String daVar; // DA stuff JDDVars daDDRowVars, daDDColVars; // Misc - int i, j, n; + int i, n; boolean before; // Get details of old model (no copy, does not need to be cleaned up) @@ -270,7 +269,6 @@ public class LTLModelChecker extends PrismComponent varDDColVars = model.getVarDDColVars(); allDDRowVars = model.getAllDDRowVars(); allDDColVars = model.getAllDDColVars(); - ddVarNames = model.getDDVarNames(); varList = model.getVarList(); // Create a (new, unique) name for the variable that will represent DA states @@ -279,33 +277,25 @@ public class LTLModelChecker extends PrismComponent daVar = "_" + daVar; } + newModelVariables = model.getModelVariables().copy(); + // See how many new dd vars will be needed for DA // and whether there is room to put them before rather than after the existing vars // (if DA only has one state, we add an extra dummy state) n = (int) Math.ceil(PrismUtils.log2(da.size())); n = Math.max(n, 1); - before = true; - if (allDDRowVars.getMinVarIndex() - 1 < 2 * n) { - before = false; - } - + before = newModelVariables.canPrependExtraStateVariable(n); + daDDRowVars = new JDDVars(); daDDColVars = new JDDVars(); // Create the new dd variables - newDDVarNames = new Vector(); - newDDVarNames.addAll(ddVarNames); - j = before ? allDDRowVars.getMinVarIndex() - 2 * n : model.getAllDDColVars().getMaxVarIndex() + 1; + JDDVars daVars = newModelVariables.allocateExtraStateVariable(n, daVar, before); + for (i = 0; i < n; i++) { - daDDRowVars.addVar(JDD.Var(j++)); - daDDColVars.addVar(JDD.Var(j++)); - if (!before) { - newDDVarNames.add(""); - newDDVarNames.add(""); - } - newDDVarNames.set(j - 2, daVar + "." + i); - newDDVarNames.set(j - 1, daVar + "'." + i); + daDDRowVars.addVar(daVars.getVar(2*i)); + daDDColVars.addVar(daVars.getVar(2*i+1)); } - + // Create/populate new lists newVarDDRowVars = new JDDVars[varDDRowVars.length + 1]; newVarDDColVars = new JDDVars[varDDRowVars.length + 1]; @@ -356,8 +346,8 @@ public class LTLModelChecker extends PrismComponent new JDDNode[0], new JDDNode[0], new String[0], // New list of all row/col vars newAllDDRowVars, newAllDDColVars, - // New list of var names - newDDVarNames, + // New model variables + newModelVariables, // Module info (unchanged) model.getNumModules(), model.getModuleNames(), @@ -440,13 +430,12 @@ public class LTLModelChecker extends PrismComponent JDDVars varDDColVars[]; JDDVars allDDRowVars; JDDVars allDDColVars; - Vector ddVarNames; VarList varList; // New (product) model - dds, vars, etc. JDDNode newTrans, newStart; JDDVars newVarDDRowVars[], newVarDDColVars[]; JDDVars newAllDDRowVars, newAllDDColVars; - Vector newDDVarNames; + ModelVariablesDD newModelVariables; VarList newVarList; String daVar; // DA stuff @@ -460,7 +449,6 @@ public class LTLModelChecker extends PrismComponent varDDColVars = model.getVarDDColVars(); allDDRowVars = model.getAllDDRowVars(); allDDColVars = model.getAllDDColVars(); - ddVarNames = model.getDDVarNames(); varList = model.getVarList(); // Create a (new, unique) name for the variable that will represent DA states @@ -469,33 +457,25 @@ public class LTLModelChecker extends PrismComponent daVar = "_" + daVar; } + newModelVariables = model.getModelVariables().copy(); + // See how many new dd vars will be needed for DA // and whether there is room to put them before rather than after the existing vars // (if DA only has one state, we add an extra dummy state) n = (int) Math.ceil(PrismUtils.log2(da.size())); n = Math.max(n, 1); - before = true; - if ((allDDRowVars.getMinVarIndex() - model.getAllDDNondetVars().getMaxVarIndex()) - 1 < 2 * n) { - before = false; - } + before = newModelVariables.canPrependExtraStateVariable(n); daDDRowVars = new JDDVars(); daDDColVars = new JDDVars(); // Create the new dd variables - newDDVarNames = new Vector(); - newDDVarNames.addAll(ddVarNames); - j = before ? allDDRowVars.getMinVarIndex() - 2 * n : model.getAllDDColVars().getMaxVarIndex() + 1; + JDDVars daVars = newModelVariables.allocateExtraStateVariable(n, daVar, before); + for (i = 0; i < n; i++) { - daDDRowVars.addVar(JDD.Var(j++)); - daDDColVars.addVar(JDD.Var(j++)); - if (!before) { - newDDVarNames.add(""); - newDDVarNames.add(""); - } - newDDVarNames.set(j - 2, daVar + "." + i); - newDDVarNames.set(j - 1, daVar + "'." + i); + daDDRowVars.addVar(daVars.getVar(2*i)); + daDDColVars.addVar(daVars.getVar(2*i+1)); } - + // Create/populate new lists newVarDDRowVars = new JDDVars[varDDRowVars.length + 1]; newVarDDColVars = new JDDVars[varDDRowVars.length + 1]; @@ -553,8 +533,8 @@ public class LTLModelChecker extends PrismComponent model.getAllDDSynchVars().copy(), model.getAllDDChoiceVars().copy(), model.getAllDDNondetVars().copy(), - // New list of var names - newDDVarNames, + // New model variables + newModelVariables, // Module info (unchanged) model.getNumModules(), model.getModuleNames(), diff --git a/prism/src/prism/Model.java b/prism/src/prism/Model.java index bee31e5b..a1ec0227 100644 --- a/prism/src/prism/Model.java +++ b/prism/src/prism/Model.java @@ -139,7 +139,10 @@ public interface Model int getNumDDColVars(); int getNumDDVarsInTrans(); Vector getDDVarNames(); - + + /** Get the information about the model variables */ + ModelVariablesDD getModelVariables(); + ODDNode getODD(); void setSynchs(List synchs); diff --git a/prism/src/prism/ModelGenerator2MTBDD.java b/prism/src/prism/ModelGenerator2MTBDD.java index 6e647e24..9b1af81e 100644 --- a/prism/src/prism/ModelGenerator2MTBDD.java +++ b/prism/src/prism/ModelGenerator2MTBDD.java @@ -84,8 +84,9 @@ public class ModelGenerator2MTBDD private JDDNode[] ddSynchVars; // individual dd vars for synchronising actions private JDDNode[] ddSchedVars; // individual dd vars for scheduling non-det. private JDDNode[] ddChoiceVars; // individual dd vars for local non-det. - // names for all dd vars used - private Vector ddVarNames; + + private ModelVariablesDD modelVariables; + // action info private Vector synchs; // list of action names private JDDNode transActions; // dd for transition action labels (MDPs) @@ -114,6 +115,7 @@ public class ModelGenerator2MTBDD varList = modelGen.createVarList(); numLabels = modelGen.getNumLabels(); numVars = varList.getNumVars(); + modelVariables = new ModelVariablesDD(); numRewardStructs = modelGen.getNumRewardStructs(); rewardStructNames = modelGen.getRewardStructNames().toArray(new String[0]); return buildModel(); @@ -176,14 +178,14 @@ public class ModelGenerator2MTBDD // create new Model object to be returned if (modelType == ModelType.DTMC) { - model = new ProbModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, ddVarNames, numModules, + model = new ProbModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, modelVariables, numModules, moduleNames, moduleDDRowVars, moduleDDColVars, numVars, varList, varDDRowVars, varDDColVars, constantValues); } else if (modelType == ModelType.MDP) { model = new NondetModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, allDDSynchVars, - allDDSchedVars, allDDChoiceVars, allDDNondetVars, ddVarNames, numModules, moduleNames, moduleDDRowVars, moduleDDColVars, numVars, varList, + allDDSchedVars, allDDChoiceVars, allDDNondetVars, modelVariables, numModules, moduleNames, moduleDDRowVars, moduleDDColVars, numVars, varList, varDDRowVars, varDDColVars, constantValues); } else if (modelType == ModelType.CTMC) { - model = new StochModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, ddVarNames, numModules, + model = new StochModel(trans, start, stateRewardsArray, transRewardsArray, rewardStructNames, allDDRowVars, allDDColVars, modelVariables, numModules, moduleNames, moduleDDRowVars, moduleDDColVars, numVars, varList, varDDRowVars, varDDColVars, constantValues); } // set action info @@ -237,7 +239,6 @@ public class ModelGenerator2MTBDD JDDNode v, vr, vc; int i, j, n; int ddVarsUsed = 0; - ddVarNames = new Vector(); // create arrays/etc. first @@ -262,7 +263,7 @@ public class ModelGenerator2MTBDD for (i = 0; i < maxNumChoices; i++) { v = JDD.Var(ddVarsUsed++); ddChoiceVars[i] = v; - ddVarNames.add("l" + i); + modelVariables.allocateVariable("l" + i); } } @@ -282,8 +283,8 @@ public class ModelGenerator2MTBDD varDDRowVars[i].addVar(vr); varDDColVars[i].addVar(vc); // add names to list - ddVarNames.add(varList.getName(i) + "." + j); - ddVarNames.add(varList.getName(i) + "'." + j); + modelVariables.allocateVariable(varList.getName(i) + "." + j); + modelVariables.allocateVariable(varList.getName(i) + "'." + j); } } } diff --git a/prism/src/prism/Modules2MTBDD.java b/prism/src/prism/Modules2MTBDD.java index c5768926..bc3a2329 100644 --- a/prism/src/prism/Modules2MTBDD.java +++ b/prism/src/prism/Modules2MTBDD.java @@ -104,8 +104,9 @@ public class Modules2MTBDD private JDDNode[] ddSynchVars; // individual dd vars for synchronising actions private JDDNode[] ddSchedVars; // individual dd vars for scheduling non-det. private JDDNode[] ddChoiceVars; // individual dd vars for local non-det. - // names for all dd vars used - private Vector ddVarNames; + + private ModelVariablesDD modelVariables; + // flags for keeping track of which variables have been used private boolean[] varsUsed; @@ -250,18 +251,18 @@ public class Modules2MTBDD // create new Model object to be returned if (modelType == ModelType.DTMC) { - model = new ProbModel(trans, start, stateRewards, transRewards, rewardStructNames, allDDRowVars, allDDColVars, ddVarNames, + model = new ProbModel(trans, start, stateRewards, transRewards, rewardStructNames, allDDRowVars, allDDColVars, modelVariables, numModules, moduleNames, moduleDDRowVars, moduleDDColVars, numVars, varList, varDDRowVars, varDDColVars, constantValues); } else if (modelType == ModelType.MDP) { model = new NondetModel(trans, start, stateRewards, transRewards, rewardStructNames, allDDRowVars, allDDColVars, - allDDSynchVars, allDDSchedVars, allDDChoiceVars, allDDNondetVars, ddVarNames, + allDDSynchVars, allDDSchedVars, allDDChoiceVars, allDDNondetVars, modelVariables, numModules, moduleNames, moduleDDRowVars, moduleDDColVars, numVars, varList, varDDRowVars, varDDColVars, constantValues); } else if (modelType == ModelType.CTMC) { - model = new StochModel(trans, start, stateRewards, transRewards, rewardStructNames, allDDRowVars, allDDColVars, ddVarNames, + model = new StochModel(trans, start, stateRewards, transRewards, rewardStructNames, allDDRowVars, allDDColVars, modelVariables, numModules, moduleNames, moduleDDRowVars, moduleDDColVars, numVars, varList, varDDRowVars, varDDColVars, constantValues); } @@ -336,11 +337,10 @@ public class Modules2MTBDD private void allocateDDVars() { - JDDNode v, vr, vc; int i, j, m, n, last; - int ddVarsUsed = 0; - ddVarNames = new Vector(); - + + modelVariables = new ModelVariablesDD(); + switch (prism.getOrdering()) { case 1: @@ -377,9 +377,7 @@ public class Modules2MTBDD if (modelType == ModelType.MDP) { // allocate vars for (i = 0; i < numSynchs; i++) { - v = JDD.Var(ddVarsUsed++); - ddSynchVars[i] = v; - ddVarNames.add(synchs.elementAt(i)+".a"); + ddSynchVars[i] = modelVariables.allocateVariable(synchs.elementAt(i)+".a"); } } @@ -387,9 +385,7 @@ public class Modules2MTBDD if (modelType == ModelType.MDP) { // allocate vars for (i = 0; i < numModules; i++) { - v = JDD.Var(ddVarsUsed++); - ddSchedVars[i] = v; - ddVarNames.add(moduleNames[i] + ".s"); + ddSchedVars[i] = modelVariables.allocateVariable(moduleNames[i] + ".s"); } } @@ -397,19 +393,15 @@ public class Modules2MTBDD if (modelType == ModelType.MDP) { m = ddChoiceVars.length; for (i = 0; i < m; i++) { - v = JDD.Var(ddVarsUsed++); - ddChoiceVars[i] = v; - ddVarNames.add("l" + i); + ddChoiceVars[i] = modelVariables.allocateVariable("l" + i); } } // create a gap in the dd variables // this allows to prepend additionl row/col vars, e.g. for constructing // a product model when doing LTL model checking - for (i = 0; i < 20; i++) { - ddVarsUsed++; - ddVarNames.add(""); - } + modelVariables.preallocateExtraStateVariables(20); + // allocate dd variables for module variables (i.e. rows/cols) // go through all vars in order (incl. global variables) @@ -421,14 +413,9 @@ public class Modules2MTBDD // add pairs of variables (row/col) for (j = 0; j < n; j++) { // new dd row variable - vr = JDD.Var(ddVarsUsed++); + varDDRowVars[i].addVar(modelVariables.allocateVariable(varList.getName(i) + "." + j)); // new dd col variable - vc = JDD.Var(ddVarsUsed++); - varDDRowVars[i].addVar(vr); - varDDColVars[i].addVar(vc); - // add names to list - ddVarNames.add(varList.getName(i) + "." + j); - ddVarNames.add(varList.getName(i) + "'." + j); + varDDColVars[i].addVar(modelVariables.allocateVariable(varList.getName(i) + "'." + j)); } } @@ -465,9 +452,7 @@ public class Modules2MTBDD // allocate synchronizing action variables if (modelType == ModelType.MDP) { for (i = 0; i < numSynchs; i++) { - v = JDD.Var(ddVarsUsed++); - ddSynchVars[i] = v; - ddVarNames.add(synchs.elementAt(i)+".a"); + ddSynchVars[i] = modelVariables.allocateVariable(synchs.elementAt(i)+".a"); } } @@ -475,9 +460,7 @@ public class Modules2MTBDD if (modelType == ModelType.MDP) { m = ddChoiceVars.length; for (i = 0; i < m; i++) { - v = JDD.Var(ddVarsUsed++); - ddChoiceVars[i] = v; - ddVarNames.add("l" + i); + ddChoiceVars[i] = modelVariables.allocateVariable("l" + i); } } @@ -491,9 +474,7 @@ public class Modules2MTBDD if ((modelType == ModelType.MDP) && (last != varList.getModule(i))) { // add scheduling dd var(s) (may do multiple ones here if modules have no vars) for (j = last+1; j <= varList.getModule(i); j++) { - v = JDD.Var(ddVarsUsed++); - ddSchedVars[j] = v; - ddVarNames.add(moduleNames[j] + ".s"); + ddSchedVars[j] = modelVariables.allocateVariable(moduleNames[j] + ".s"); } // change 'last' last = varList.getModule(i); @@ -504,19 +485,13 @@ public class Modules2MTBDD n = varList.getRangeLogTwo(i); // add pairs of variables (row/col) for (j = 0; j < n; j++) { - vr = JDD.Var(ddVarsUsed++); - vc = JDD.Var(ddVarsUsed++); - varDDRowVars[i].addVar(vr); - varDDColVars[i].addVar(vc); - ddVarNames.add(varList.getName(i) + "." + j); - ddVarNames.add(varList.getName(i) + "'." + j); + varDDRowVars[i].addVar(modelVariables.allocateVariable(varList.getName(i) + "." + j)); + varDDColVars[i].addVar(modelVariables.allocateVariable(varList.getName(i) + "'." + j)); } } // add any remaining scheduling dd var(s) (happens if some modules have no vars) if (modelType == ModelType.MDP) for (j = last+1; j ddvn, int nm, String[] mn, JDDVars[] mrv, JDDVars[] mcv, int nv, VarList vl, JDDVars[] vrv, JDDVars[] vcv, Values cv) + JDDVars andv, ModelVariablesDD mvdd, int nm, String[] mn, JDDVars[] mrv, JDDVars[] mcv, int nv, VarList vl, JDDVars[] vrv, JDDVars[] vcv, Values cv) { - super(tr, s, sr, trr, rsn, arv, acv, ddvn, nm, mn, mrv, mcv, nv, vl, vrv, vcv, cv); + super(tr, s, sr, trr, rsn, arv, acv, mvdd, nm, mn, mrv, mcv, nv, vl, vrv, vcv, cv); allDDSynchVars = asyv; allDDSchedVars = asv; @@ -327,16 +327,16 @@ public class NondetModel extends ProbModel n = allDDNondetVars.getNumVars(); for (i = 0; i < n; i++) { j = allDDNondetVars.getVarIndex(i); - log.print(" " + j + ":" + ddVarNames.get(j)); + log.print(" " + j + ":" + getDDVarNames().get(j)); } log.println(); log.print("DD vars (r/c):"); n = allDDRowVars.getNumVars(); for (i = 0; i < n; i++) { j = allDDRowVars.getVarIndex(i); - log.print(" " + j + ":" + ddVarNames.get(j)); + log.print(" " + j + ":" + getDDVarNames().get(j)); j = allDDColVars.getVarIndex(i); - log.print(" " + j + ":" + ddVarNames.get(j)); + log.print(" " + j + ":" + getDDVarNames().get(j)); } log.println(); log.print(getTransName() + " terminals: " + JDD.GetTerminalsAndNumbersString(trans, getNumDDVarsInTrans()) + "\n"); @@ -455,6 +455,7 @@ public class NondetModel extends ProbModel if (transReln != null) JDD.Deref(transReln); } + } //------------------------------------------------------------------------------ diff --git a/prism/src/prism/ProbModel.java b/prism/src/prism/ProbModel.java index f4d94587..cef47c55 100644 --- a/prism/src/prism/ProbModel.java +++ b/prism/src/prism/ProbModel.java @@ -83,8 +83,8 @@ public class ProbModel implements Model protected JDDVars[] moduleDDColVars; // dd vars for each module (cols) protected JDDVars allDDRowVars; // all dd vars (rows) protected JDDVars allDDColVars; // all dd vars (cols) - // names for all dd vars used - protected Vector ddVarNames; + + protected ModelVariablesDD modelVariables; /** * A map from label to state set, optionally storing a state set @@ -390,7 +390,13 @@ public class ProbModel implements Model public Vector getDDVarNames() { - return ddVarNames; + return modelVariables.getDDVarNames(); + } + + @Override + public ModelVariablesDD getModelVariables() + { + return modelVariables; } public ODDNode getODD() @@ -410,7 +416,7 @@ public class ProbModel implements Model // constructor - public ProbModel(JDDNode tr, JDDNode s, JDDNode sr[], JDDNode trr[], String rsn[], JDDVars arv, JDDVars acv, Vector ddvn, int nm, String[] mn, + public ProbModel(JDDNode tr, JDDNode s, JDDNode sr[], JDDNode trr[], String rsn[], JDDVars arv, JDDVars acv, ModelVariablesDD mvdd, int nm, String[] mn, JDDVars[] mrv, JDDVars[] mcv, int nv, VarList vl, JDDVars[] vrv, JDDVars[] vcv, Values cv) { int i; @@ -424,7 +430,7 @@ public class ProbModel implements Model rewardStructNames = rsn; allDDRowVars = arv; allDDColVars = acv; - ddVarNames = ddvn; + modelVariables = mvdd; numModules = nm; moduleNames = mn; moduleDDRowVars = mrv; @@ -753,9 +759,9 @@ public class ProbModel implements Model n = allDDRowVars.getNumVars(); for (i = 0; i < n; i++) { j = allDDRowVars.getVarIndex(i); - log.print(" " + j + ":" + ddVarNames.get(j)); + log.print(" " + j + ":" + getDDVarNames().get(j)); j = allDDColVars.getVarIndex(i); - log.print(" " + j + ":" + ddVarNames.get(j)); + log.print(" " + j + ":" + getDDVarNames().get(j)); } log.println(); log.print(getTransName() + " terminals: " + JDD.GetTerminalsAndNumbersString(trans, getNumDDVarsInTrans()) + "\n"); @@ -1015,6 +1021,9 @@ public class ProbModel implements Model ODDUtils.ClearODD(odd); odd = null; } + + if (modelVariables != null) + modelVariables.clear(); } } diff --git a/prism/src/prism/StochModel.java b/prism/src/prism/StochModel.java index a15fad48..6e7a466a 100644 --- a/prism/src/prism/StochModel.java +++ b/prism/src/prism/StochModel.java @@ -56,9 +56,9 @@ public class StochModel extends ProbModel // constructor public StochModel(JDDNode tr, JDDNode s, JDDNode sr[], JDDNode trr[], String rsn[], JDDVars arv, JDDVars acv, - Vector ddvn, int nm, String[] mn, JDDVars[] mrv, JDDVars[] mcv, int nv, VarList vl, JDDVars[] vrv, + ModelVariablesDD mvdd, int nm, String[] mn, JDDVars[] mrv, JDDVars[] mcv, int nv, VarList vl, JDDVars[] vrv, JDDVars[] vcv, Values cv) { - super(tr, s, sr, trr, rsn, arv, acv, ddvn, nm, mn, mrv, mcv, nv, vl, vrv, vcv, cv); + super(tr, s, sr, trr, rsn, arv, acv, mvdd, nm, mn, mrv, mcv, nv, vl, vrv, vcv, cv); } }