Browse Source

prism.NondetModelChecker: Fix potential memory leak when using -exportstrat and interval iteration

When the model has to be transformed (Pmax-quotienting) to apply interval iteration, we currently don't support strategy generation and thus have to properly deallocate the strategy array that has been prepared.
accumulation-v4.7
Joachim Klein 7 years ago
parent
commit
7328789e4f
  1. 12
      prism/src/prism/NondetModelChecker.java

12
prism/src/prism/NondetModelChecker.java

@ -2057,7 +2057,11 @@ public class NondetModelChecker extends NonProbModelChecker
} }
if (doIntervalIteration) { if (doIntervalIteration) {
if (transform != null) { if (transform != null) {
strat = null; // strategy generation with the quotient not yet supported
// strategy generation with the quotient not yet supported
if (strat != null) {
strat.clear();
strat = null;
}
probsDV = PrismSparse.NondetUntilInterval(transformed.getTrans(), probsDV = PrismSparse.NondetUntilInterval(transformed.getTrans(),
transformed.getTransActions(), transformed.getTransActions(),
transformed.getSynchs(), transformed.getSynchs(),
@ -2077,7 +2081,11 @@ public class NondetModelChecker extends NonProbModelChecker
} }
} else { } else {
if (transform != null) { if (transform != null) {
strat = null; // strategy generation with the quotient not yet supported
// strategy generation with the quotient not yet supported
if (strat != null) {
strat.clear();
strat = null;
}
probsDV = PrismSparse.NondetUntil(transformed.getTrans(), probsDV = PrismSparse.NondetUntil(transformed.getTrans(),
transformed.getTransActions(), transformed.getTransActions(),
transformed.getSynchs(), transformed.getSynchs(),

Loading…
Cancel
Save