Browse Source

LTLModelChecker(product MDP): replace first batch of daDDVars refAll with copies

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10438 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 11 years ago
parent
commit
f6536e356f
  1. 14
      prism/src/prism/LTLModelChecker.java

14
prism/src/prism/LTLModelChecker.java

@ -446,13 +446,11 @@ public class LTLModelChecker extends PrismComponent
// Create/populate new lists // Create/populate new lists
newVarDDRowVars = new JDDVars[varDDRowVars.length + 1]; newVarDDRowVars = new JDDVars[varDDRowVars.length + 1];
newVarDDColVars = new JDDVars[varDDRowVars.length + 1]; newVarDDColVars = new JDDVars[varDDRowVars.length + 1];
newVarDDRowVars[before ? 0 : varDDRowVars.length] = daDDRowVars;
newVarDDColVars[before ? 0 : varDDColVars.length] = daDDColVars;
newVarDDRowVars[before ? 0 : varDDRowVars.length] = daDDRowVars.copy();
newVarDDColVars[before ? 0 : varDDColVars.length] = daDDColVars.copy();
for (i = 0; i < varDDRowVars.length; i++) { for (i = 0; i < varDDRowVars.length; i++) {
newVarDDRowVars[before ? i + 1 : i] = new JDDVars();
newVarDDColVars[before ? i + 1 : i] = new JDDVars();
newVarDDRowVars[before ? i + 1 : i].addVars(varDDRowVars[i]);
newVarDDColVars[before ? i + 1 : i].addVars(varDDColVars[i]);
newVarDDRowVars[before ? i + 1 : i] = varDDRowVars[i].copy();
newVarDDColVars[before ? i + 1 : i] = varDDColVars[i].copy();
} }
newAllDDRowVars = new JDDVars(); newAllDDRowVars = new JDDVars();
newAllDDColVars = new JDDVars(); newAllDDColVars = new JDDVars();
@ -474,8 +472,6 @@ public class LTLModelChecker extends PrismComponent
// Extra references (because will get derefed when new model is done with) // Extra references (because will get derefed when new model is done with)
allDDRowVars.refAll(); allDDRowVars.refAll();
allDDRowVars.refAll();
allDDColVars.refAll();
allDDColVars.refAll(); allDDColVars.refAll();
for (i = 0; i < model.getNumModules(); i++) { for (i = 0; i < model.getNumModules(); i++) {
model.getModuleDDRowVars(i).refAll(); model.getModuleDDRowVars(i).refAll();
@ -483,8 +479,6 @@ public class LTLModelChecker extends PrismComponent
} }
daDDRowVars.refAll(); daDDRowVars.refAll();
daDDColVars.refAll(); daDDColVars.refAll();
daDDRowVars.refAll();
daDDColVars.refAll();
model.getAllDDSchedVars().refAll(); model.getAllDDSchedVars().refAll();
model.getAllDDSynchVars().refAll(); model.getAllDDSynchVars().refAll();
model.getAllDDChoiceVars().refAll(); model.getAllDDChoiceVars().refAll();

Loading…
Cancel
Save