From e5b7f3297b82bf1c2f43dabe9a7d8a4e458a992b Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Wed, 6 Jul 2016 11:49:09 +0000 Subject: [PATCH] Symbolic engines: Clear ODD when clearing the model (fix memory leak) Previously, the ODD data structure (for mapping between reachable states and their index) on the C side was not deallocated when the model was cleared. Closes https://sourceforge.net/p/prism-mc/bugs/9/ git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11468 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/NondetModel.java | 5 ++++- prism/src/prism/ProbModel.java | 16 ++++++++++++++-- 2 files changed, 18 insertions(+), 3 deletions(-) diff --git a/prism/src/prism/NondetModel.java b/prism/src/prism/NondetModel.java index 51736cf1..f6ba9b0f 100644 --- a/prism/src/prism/NondetModel.java +++ b/prism/src/prism/NondetModel.java @@ -213,7 +213,10 @@ public class NondetModel extends ProbModel // work out number of reachable states numStates = JDD.GetNumMinterms(reach, allDDRowVars.n()); - // build odd + // build odd, clear old one + if (odd != null) { + ODDUtils.ClearODD(odd); + } odd = ODDUtils.BuildODD(reach, allDDRowVars); } diff --git a/prism/src/prism/ProbModel.java b/prism/src/prism/ProbModel.java index 5d968c50..4686c1f9 100644 --- a/prism/src/prism/ProbModel.java +++ b/prism/src/prism/ProbModel.java @@ -505,7 +505,10 @@ public class ProbModel implements Model // work out number of reachable states numStates = Math.pow(2, allDDRowVars.n()); - // build odd + // build odd, clear old one + if (odd != null) { + ODDUtils.ClearODD(odd); + } odd = ODDUtils.BuildODD(reach, allDDRowVars); } @@ -522,7 +525,10 @@ public class ProbModel implements Model // work out number of reachable states numStates = JDD.GetNumMinterms(reach, allDDRowVars.n()); - // build odd + // build odd, clear old one + if (odd != null) { + ODDUtils.ClearODD(odd); + } odd = ODDUtils.BuildODD(reach, allDDRowVars); } @@ -928,5 +934,11 @@ public class ProbModel implements Model JDD.Deref(transPerAction[i]); } } + + if (odd != null) { + // clear ODD + ODDUtils.ClearODD(odd); + odd = null; + } } }