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

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

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11820 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 10 years ago
parent
4340969f70
commit
410b38ab30
1 changed files with 36 additions and 73 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. 109
      prism/src/prism/Modules2MTBDD.java

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

@ -310,32 +310,20 @@ public class Modules2MTBDD
// deref spare dds
globalDDRowVars.derefAll();
globalDDColVars.derefAll();
for (i = 0; i < numModules; i++) {
JDD.Deref(moduleIdentities[i]);
JDD.Deref(moduleRangeDDs[i]);
}
for (i = 0; i < numVars; i++) {
JDD.Deref(varIdentities[i]);
JDD.Deref(varRangeDDs[i]);
JDD.Deref(varColRangeDDs[i]);
}
JDD.DerefArray(moduleIdentities, numModules);
JDD.DerefArray(moduleRangeDDs, numModules);
JDD.DerefArray(varIdentities, numVars);
JDD.DerefArray(varRangeDDs, numVars);
JDD.DerefArray(varColRangeDDs, numVars);
JDD.Deref(range);
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);
}
if (doSymmetry) {
JDD.Deref(symm);
for (i = 0; i < numSymmModules-1; i++) {
JDD.Deref(nonSymms[i]);
}
JDD.DerefArray(nonSymms, numSymmModules-1);
}
expr2mtbdd.clearDummyModel();
@ -598,26 +586,20 @@ public class Modules2MTBDD
// go thru all syncronising action vars
for (i = 0; i < ddSynchVars.length; i++) {
// add to list
JDD.Ref(ddSynchVars[i]);
JDD.Ref(ddSynchVars[i]);
allDDSynchVars.addVar(ddSynchVars[i]);
allDDNondetVars.addVar(ddSynchVars[i]);
allDDSynchVars.addVar(ddSynchVars[i].copy());
allDDNondetVars.addVar(ddSynchVars[i].copy());
}
// go thru all scheduler nondet vars
for (i = 0; i < ddSchedVars.length; i++) {
// add to list
JDD.Ref(ddSchedVars[i]);
JDD.Ref(ddSchedVars[i]);
allDDSchedVars.addVar(ddSchedVars[i]);
allDDNondetVars.addVar(ddSchedVars[i]);
allDDSchedVars.addVar(ddSchedVars[i].copy());
allDDNondetVars.addVar(ddSchedVars[i].copy());
}
// go thru all local nondet vars
for (i = 0; i < ddChoiceVars.length; i++) {
// 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());
}
}
}
@ -646,8 +628,7 @@ public class Modules2MTBDD
id = JDD.Constant(1);
for (j = 0; j < numVars; j++) {
if (varList.getModule(j) == i) {
JDD.Ref(varIdentities[j]);
id = JDD.Apply(JDD.TIMES, id, varIdentities[j]);
id = JDD.Apply(JDD.TIMES, id, varIdentities[j].copy());
}
}
moduleIdentities[i] = id;
@ -668,21 +649,17 @@ public class Modules2MTBDD
varColRangeDDs = new JDDNode[numVars];
for (i = 0; i < numVars; i++) {
// 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
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
JDD.Ref(varRangeDDs[i]);
range = JDD.Apply(JDD.TIMES, range, varRangeDDs[i]);
range = JDD.Apply(JDD.TIMES, range, varRangeDDs[i].copy());
}
// module ranges
moduleRangeDDs = new JDDNode[numModules];
for (i = 0; i < numModules; i++) {
// obtain range dd by abstracting from identity matrix
JDD.Ref(moduleIdentities[i]);
moduleRangeDDs[i] = JDD.SumAbstract(moduleIdentities[i], moduleDDColVars[i]);
moduleRangeDDs[i] = JDD.SumAbstract(moduleIdentities[i].copy(), moduleDDColVars[i]);
}
}
@ -715,8 +692,7 @@ public class Modules2MTBDD
// for dtmcs, need to normalise each row to remove local nondeterminism
if (modelType == ModelType.DTMC) {
// divide each row by row sum
JDD.Ref(trans);
tmp = JDD.SumAbstract(trans, allDDColVars);
tmp = JDD.SumAbstract(trans.copy(), allDDColVars);
trans = JDD.Apply(JDD.DIVIDE, trans, tmp);
}
}
@ -783,8 +759,7 @@ public class Modules2MTBDD
// independent bit
tmp = JDD.Constant(1);
for (i = 0; i < numSynchs; i++) {
JDD.Ref(ddSynchVars[i]);
tmp = JDD.And(tmp, JDD.Not(ddSynchVars[i]));
tmp = JDD.And(tmp, JDD.Not(ddSynchVars[i].copy()));
}
sysDDs.ind.trans = JDD.Apply(JDD.TIMES, tmp, sysDDs.ind.trans);
//JDD.Ref(tmp);
@ -793,12 +768,11 @@ public class Modules2MTBDD
for (i = 0; i < numSynchs; i++) {
tmp = JDD.Constant(1);
for (j = 0; j < numSynchs; j++) {
JDD.Ref(ddSynchVars[j]);
if (j == i) {
tmp = JDD.And(tmp, ddSynchVars[j]);
tmp = JDD.And(tmp, ddSynchVars[j].copy());
}
else {
tmp = JDD.And(tmp, JDD.Not(ddSynchVars[j]));
tmp = JDD.And(tmp, JDD.Not(ddSynchVars[j].copy()));
}
}
sysDDs.synchs[i].trans = JDD.Apply(JDD.TIMES, tmp, sysDDs.synchs[i].trans);
@ -813,14 +787,12 @@ public class Modules2MTBDD
// now, for all model types, transition matrix can be built by summing over all actions
// also build transition rewards at the same time
n = modulesFile.getNumRewardStructs();
JDD.Ref(sysDDs.ind.trans);
trans = sysDDs.ind.trans;
trans = sysDDs.ind.trans.copy();
for (j = 0; j < n; j++) {
transRewards[j] = sysDDs.ind.rewards[j];
}
for (i = 0; i < numSynchs; i++) {
JDD.Ref(sysDDs.synchs[i].trans);
trans = JDD.Apply(JDD.PLUS, trans, sysDDs.synchs[i].trans);
trans = JDD.Apply(JDD.PLUS, trans, sysDDs.synchs[i].trans.copy());
for (j = 0; j < n; j++) {
transRewards[j] = JDD.Apply(JDD.PLUS, transRewards[j], sysDDs.synchs[i].rewards[j]);
}
@ -833,20 +805,17 @@ public class Modules2MTBDD
if (modelType != ModelType.MDP) {
n = modulesFile.getNumRewardStructs();
for (j = 0; j < n; j++) {
JDD.Ref(trans);
transRewards[j] = JDD.Apply(JDD.DIVIDE, transRewards[j], trans);
transRewards[j] = JDD.Apply(JDD.DIVIDE, transRewards[j], trans.copy());
}
}
// For MDPs, we take a copy of the DDs used to construct the part
// of the transition matrix that corresponds to each action
if (modelType == ModelType.MDP && storeTransParts) {
JDD.Ref(sysDDs.ind.trans);
transInd = JDD.ThereExists(JDD.GreaterThan(sysDDs.ind.trans, 0), allDDColVars);
transInd = JDD.ThereExists(JDD.GreaterThan(sysDDs.ind.trans.copy(), 0), allDDColVars);
transSynch = new JDDNode[numSynchs];
for (i = 0; i < numSynchs; i++) {
JDD.Ref(sysDDs.synchs[i].trans);
transSynch[i] = JDD.ThereExists(JDD.GreaterThan(sysDDs.synchs[i].trans, 0), allDDColVars);
transSynch[i] = JDD.ThereExists(JDD.GreaterThan(sysDDs.synchs[i].trans.copy(), 0), allDDColVars);
}
}
@ -874,8 +843,7 @@ public class Modules2MTBDD
//tmp = JDD.ThereExists(JDD.GreaterThan(sysDDs.ind.trans, 0), allDDColVars);
//transActions = JDD.Apply(JDD.PLUS, transActions, JDD.Apply(JDD.TIMES, tmp, JDD.Constant(1)));
for (i = 0; i < numSynchs; i++) {
JDD.Ref(sysDDs.synchs[i].trans);
tmp = JDD.ThereExists(JDD.GreaterThan(sysDDs.synchs[i].trans, 0), allDDColVars);
tmp = JDD.ThereExists(JDD.GreaterThan(sysDDs.synchs[i].trans.copy(), 0), allDDColVars);
transActions = JDD.Apply(JDD.PLUS, transActions, JDD.Apply(JDD.TIMES, tmp, JDD.Constant(1+i)));
}
break;
@ -883,11 +851,9 @@ public class Modules2MTBDD
case CTMC:
// Just reference DDs and copy them to new array
transPerAction = new JDDNode[numSynchs + 1];
JDD.Ref(sysDDs.ind.trans);
transPerAction[0] = sysDDs.ind.trans;
transPerAction[0] = sysDDs.ind.trans.copy();
for (i = 0; i < numSynchs; i++) {
JDD.Ref(sysDDs.synchs[i].trans);
transPerAction[i + 1] = sysDDs.synchs[i].trans;
transPerAction[i + 1] = sysDDs.synchs[i].trans.copy();
}
break;
}
@ -970,8 +936,7 @@ public class Modules2MTBDD
sysDDs.synchs[i] = translateModule(m, module, synch, synchMin[i]);
}
// store identity matrix
JDD.Ref(moduleIdentities[m]);
sysDDs.id = moduleIdentities[m];
sysDDs.id = moduleIdentities[m].copy();
// store synchs used
sysDDs.allSynchs.addAll(module.getAllSynchs());
@ -1568,11 +1533,9 @@ public class Modules2MTBDD
}
// deref guards/updates
for (l = 0; l < numCommands; l++) {
JDD.Deref(guardDDs[l]);
JDD.Deref(upDDs[l]);
//JDD.Deref(rewDDs[l]);
}
JDD.DerefArray(guardDDs, numCommands);
JDD.DerefArray(upDDs, numCommands);
//JDD.DerefArray(rewDDs, numCommands);
return compDDs;
}

Write Preview
Loading…
Cancel
Save