s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Refactor: Switch MTBDD variable handling for symbolic models to ModelVariablesDD infrastructure 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11824 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 10 years ago
parent
a69f3d2e3f
commit
3d48780b8d
9 changed files with 109 additions and 152 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 33
      prism/src/prism/ExplicitFiles2MTBDD.java
  2. 29
      prism/src/prism/ExplicitModel2MTBDD.java
  3. 68
      prism/src/prism/LTLModelChecker.java
  4. 5
      prism/src/prism/Model.java
  5. 19
      prism/src/prism/ModelGenerator2MTBDD.java
  6. 69
      prism/src/prism/Modules2MTBDD.java
  7. 11
      prism/src/prism/NondetModel.java
  8. 23
      prism/src/prism/ProbModel.java
  9. 4
      prism/src/prism/StochModel.java

33
prism/src/prism/ExplicitFiles2MTBDD.java
View File

@ -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<String> ddVarNames;
private ModelVariablesDD modelVariables;
// action info
private Vector<String> 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<String>();
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));
}
}
}

29
prism/src/prism/ExplicitModel2MTBDD.java
View File

@ -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<String> ddVarNames;
private ModelVariablesDD modelVariables;
// action info
private Vector<String> 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<String>();
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));
}
}
}

68
prism/src/prism/LTLModelChecker.java
View File

@ -250,19 +250,18 @@ public class LTLModelChecker extends PrismComponent
JDDVars varDDColVars[];
JDDVars allDDRowVars;
JDDVars allDDColVars;
Vector<String> ddVarNames;
VarList varList;
// New (product) model - dds, vars, etc.
JDDNode newTrans, newStart;
JDDVars newVarDDRowVars[], newVarDDColVars[];
JDDVars newAllDDRowVars, newAllDDColVars;
Vector<String> 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<String>();
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<String> ddVarNames;
VarList varList;
// New (product) model - dds, vars, etc.
JDDNode newTrans, newStart;
JDDVars newVarDDRowVars[], newVarDDColVars[];
JDDVars newAllDDRowVars, newAllDDColVars;
Vector<String> 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<String>();
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(),

5
prism/src/prism/Model.java
View File

@ -139,7 +139,10 @@ public interface Model
int getNumDDColVars();
int getNumDDVarsInTrans();
Vector<String> getDDVarNames();
/** Get the information about the model variables */
ModelVariablesDD getModelVariables();
ODDNode getODD();
void setSynchs(List<String> synchs);

19
prism/src/prism/ModelGenerator2MTBDD.java
View File

@ -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<String> ddVarNames;
private ModelVariablesDD modelVariables;
// action info
private Vector<String> 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<String>();
// 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);
}
}
}

69
prism/src/prism/Modules2MTBDD.java
View File

@ -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<String> 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<String>();
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 <numModules; j++) {
v = JDD.Var(ddVarsUsed++);
ddSchedVars[j] = v;
ddVarNames.add(moduleNames[j] + ".s");
ddSchedVars[j] = modelVariables.allocateVariable(moduleNames[j] + ".s");
}
break;

11
prism/src/prism/NondetModel.java
View File

@ -182,9 +182,9 @@ public class NondetModel extends ProbModel
// constructor
public NondetModel(JDDNode tr, JDDNode s, JDDNode sr[], JDDNode trr[], String rsn[], JDDVars arv, JDDVars acv, JDDVars asyv, JDDVars asv, JDDVars achv,
JDDVars andv, Vector<String> 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);
}
}
//------------------------------------------------------------------------------

23
prism/src/prism/ProbModel.java
View File

@ -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<String> 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<String> 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<String> 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();
}
}

4
prism/src/prism/StochModel.java
View File

@ -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<String> 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);
}
}
Write Preview
Loading…
Cancel
Save