From 7328789e4f636a0f8e9f3ab9de62fdf302e396e2 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 25 Oct 2018 15:56:23 +0200 Subject: [PATCH] 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. --- prism/src/prism/NondetModelChecker.java | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 6bc674cb..3f317cb2 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -2057,7 +2057,11 @@ public class NondetModelChecker extends NonProbModelChecker } if (doIntervalIteration) { 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(), transformed.getTransActions(), transformed.getSynchs(), @@ -2077,7 +2081,11 @@ public class NondetModelChecker extends NonProbModelChecker } } else { 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(), transformed.getTransActions(), transformed.getSynchs(),