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

ModelGenerator2MTBDD: simplify reference handling, use JDDNode.copy(), JDD.DerefArray() 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11821 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 9 years ago
parent
410b38ab30
commit
8b07176df3
1 changed files with 16 additions and 34 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 50
      prism/src/prism/ModelGenerator2MTBDD.java

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

@ -215,22 +215,14 @@ public class ModelGenerator2MTBDD
// deref spare dds // deref spare dds
JDD.Deref(moduleIdentities[0]); JDD.Deref(moduleIdentities[0]);
JDD.Deref(moduleRangeDDs[0]); JDD.Deref(moduleRangeDDs[0]);
for (i = 0; i < numVars; i++) {
JDD.Deref(varIdentities[i]);
JDD.Deref(varRangeDDs[i]);
JDD.Deref(varColRangeDDs[i]);
}
JDD.DerefArray(varIdentities, numVars);
JDD.DerefArray(varRangeDDs, numVars);
JDD.DerefArray(varColRangeDDs, numVars);
JDD.Deref(range); JDD.Deref(range);
if (modelType == ModelType.MDP) { if (modelType == ModelType.MDP) {
for (i = 0; i < ddSynchVars.length; i++) {
JDD.Deref(ddSynchVars[i]);
}
for (i = 0; i < ddSchedVars.length; i++) {
JDD.Deref(ddSchedVars[i]);
}
for (i = 0; i < ddChoiceVars.length; i++) {
JDD.Deref(ddChoiceVars[i]);
}
JDD.DerefArray(ddSynchVars, ddSynchVars.length);
JDD.DerefArray(ddSchedVars, ddSchedVars.length);
JDD.DerefArray(ddChoiceVars, ddChoiceVars.length);
} }
return model; return model;
@ -335,10 +327,8 @@ public class ModelGenerator2MTBDD
if (modelType == ModelType.MDP) { if (modelType == ModelType.MDP) {
for (i = 0; i < ddChoiceVars.length; i++) { for (i = 0; i < ddChoiceVars.length; i++) {
// add to list // add to list
JDD.Ref(ddChoiceVars[i]);
JDD.Ref(ddChoiceVars[i]);
allDDChoiceVars.addVar(ddChoiceVars[i]);
allDDNondetVars.addVar(ddChoiceVars[i]);
allDDChoiceVars.addVar(ddChoiceVars[i].copy());
allDDNondetVars.addVar(ddChoiceVars[i].copy());
} }
} }
} }
@ -365,8 +355,7 @@ public class ModelGenerator2MTBDD
id = JDD.Constant(1); id = JDD.Constant(1);
for (j = 0; j < numVars; j++) { for (j = 0; j < numVars; j++) {
if (varList.getModule(j) == 0) { if (varList.getModule(j) == 0) {
JDD.Ref(varIdentities[j]);
id = JDD.Apply(JDD.TIMES, id, varIdentities[j]);
id = JDD.Apply(JDD.TIMES, id, varIdentities[j].copy());
} }
} }
moduleIdentities[0] = id; moduleIdentities[0] = id;
@ -385,20 +374,16 @@ public class ModelGenerator2MTBDD
varColRangeDDs = new JDDNode[numVars]; varColRangeDDs = new JDDNode[numVars];
for (i = 0; i < numVars; i++) { for (i = 0; i < numVars; i++) {
// obtain range dd by abstracting from identity matrix // obtain range dd by abstracting from identity matrix
JDD.Ref(varIdentities[i]);
varRangeDDs[i] = JDD.SumAbstract(varIdentities[i], varDDColVars[i]);
varRangeDDs[i] = JDD.SumAbstract(varIdentities[i].copy(), varDDColVars[i]);
// obtain range dd by abstracting from identity matrix // obtain range dd by abstracting from identity matrix
JDD.Ref(varIdentities[i]);
varColRangeDDs[i] = JDD.SumAbstract(varIdentities[i], varDDRowVars[i]);
varColRangeDDs[i] = JDD.SumAbstract(varIdentities[i].copy(), varDDRowVars[i]);
// build up range for whole system as we go // build up range for whole system as we go
JDD.Ref(varRangeDDs[i]);
range = JDD.Apply(JDD.TIMES, range, varRangeDDs[i]);
range = JDD.Apply(JDD.TIMES, range, varRangeDDs[i].copy());
} }
// module ranges // module ranges
moduleRangeDDs = new JDDNode[1]; moduleRangeDDs = new JDDNode[1];
// obtain range dd by abstracting from identity matrix // obtain range dd by abstracting from identity matrix
JDD.Ref(moduleIdentities[0]);
moduleRangeDDs[0] = JDD.SumAbstract(moduleIdentities[0], moduleDDColVars[0]);
moduleRangeDDs[0] = JDD.SumAbstract(moduleIdentities[0].copy(), moduleDDColVars[0]);
} }
/** Construct transition matrix and rewards */ /** Construct transition matrix and rewards */
@ -474,8 +459,7 @@ public class ModelGenerator2MTBDD
elem = JDD.Apply(JDD.TIMES, elem, JDD.SetVectorElement(JDD.Constant(0), allDDChoiceVars, i, 1)); elem = JDD.Apply(JDD.TIMES, elem, JDD.SetVectorElement(JDD.Constant(0), allDDChoiceVars, i, 1));
} }
// add it into mtbdds for transition matrix and transition rewards // add it into mtbdds for transition matrix and transition rewards
JDD.Ref(elem);
trans = JDD.Apply(JDD.PLUS, trans, JDD.Apply(JDD.TIMES, JDD.Constant(d), elem));
trans = JDD.Apply(JDD.PLUS, trans, JDD.Apply(JDD.TIMES, JDD.Constant(d), elem.copy()));
// look up action name // look up action name
int k; int k;
if (!(a == null || "".equals(a))) { if (!(a == null || "".equals(a))) {
@ -499,14 +483,12 @@ public class ModelGenerator2MTBDD
transPerAction.add(tmp); transPerAction.add(tmp);
} }
// add element to matrix // add element to matrix
JDD.Ref(elem);
tmp = JDD.Apply(JDD.PLUS, tmp, JDD.Apply(JDD.TIMES, JDD.Constant(d), elem));
tmp = JDD.Apply(JDD.PLUS, tmp, JDD.Apply(JDD.TIMES, JDD.Constant(d), elem.copy()));
transPerAction.set(k, tmp); transPerAction.set(k, tmp);
} }
/// ...for mdps... /// ...for mdps...
else { else {
JDD.Ref(elem);
tmp = JDD.ThereExists(elem, allDDColVars);
tmp = JDD.ThereExists(elem.copy(), allDDColVars);
// use max here because we see multiple transitions for a sinlge choice // use max here because we see multiple transitions for a sinlge choice
transActions = JDD.Apply(JDD.MAX, transActions, JDD.Apply(JDD.TIMES, JDD.Constant(j), tmp)); transActions = JDD.Apply(JDD.MAX, transActions, JDD.Apply(JDD.TIMES, JDD.Constant(j), tmp));
} }

Write Preview
Loading…
Cancel
Save