From dc5a8b6f7e2b02093d986a52ee344bc183e40cd0 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 7 Dec 2018 09:00:45 +0100 Subject: [PATCH] Proper DD cleanup after MTBDD engine's Gauss-Seidel exception Due to the change in 98c019b1750cba307054da43ff4135912ea65e9e, the C-level 'Gauss-Seidel not supported' checks of the MTBDD engine get triggered now more often. Before, they would just return, now we actually do the usual DD cleanup there to avoid DD reference leaks. (plus: put breaks in switch statements on separate lines to better see code-flow) --- prism/src/mtbdd/PM_ProbReachReward.cc | 13 +++++++++---- prism/src/mtbdd/PM_ProbReachRewardInterval.cc | 13 +++++++++---- prism/src/mtbdd/PM_ProbUntil.cc | 13 +++++++++---- prism/src/mtbdd/PM_ProbUntilInterval.cc | 13 +++++++++---- prism/src/mtbdd/PM_StochSteadyState.cc | 13 +++++++++---- 5 files changed, 45 insertions(+), 20 deletions(-) diff --git a/prism/src/mtbdd/PM_ProbReachReward.cc b/prism/src/mtbdd/PM_ProbReachReward.cc index d3fb397b..fd1085c9 100644 --- a/prism/src/mtbdd/PM_ProbReachReward.cc +++ b/prism/src/mtbdd/PM_ProbReachReward.cc @@ -105,13 +105,18 @@ jlong __jlongpointer m // 'maybe' states sol = NULL; switch (lin_eq_method) { case LIN_EQ_METHOD_POWER: - sol = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1Power(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(state_rewards), ptr_to_jlong(state_rewards), false)); break; + sol = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1Power(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(state_rewards), ptr_to_jlong(state_rewards), false)); + break; case LIN_EQ_METHOD_JACOBI: - sol = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JOR(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(state_rewards), ptr_to_jlong(state_rewards), false, 1.0)); break; + sol = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JOR(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(state_rewards), ptr_to_jlong(state_rewards), false, 1.0)); + break; case LIN_EQ_METHOD_JOR: - sol = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JOR(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(state_rewards), ptr_to_jlong(state_rewards), false, lin_eq_method_param)); break; + sol = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JOR(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(state_rewards), ptr_to_jlong(state_rewards), false, lin_eq_method_param)); + break; default: - PM_SetErrorMessage("Gauss-Seidel and its variants are currently not supported by the MTBDD engine"); return 0; + // set error message and return NULL pointer after cleanup, below + PM_SetErrorMessage("Gauss-Seidel and its variants are currently not supported by the MTBDD engine"); + break; } // set reward for infinity states to infinity diff --git a/prism/src/mtbdd/PM_ProbReachRewardInterval.cc b/prism/src/mtbdd/PM_ProbReachRewardInterval.cc index 1793faf6..4eee082e 100644 --- a/prism/src/mtbdd/PM_ProbReachRewardInterval.cc +++ b/prism/src/mtbdd/PM_ProbReachRewardInterval.cc @@ -120,13 +120,18 @@ jint flags sol = NULL; switch (lin_eq_method) { case LIN_EQ_METHOD_POWER: - sol = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1PowerInterval(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(state_rewards), ptr_to_jlong(lower), ptr_to_jlong(upper), false, flags)); break; + sol = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1PowerInterval(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(state_rewards), ptr_to_jlong(lower), ptr_to_jlong(upper), false, flags)); + break; case LIN_EQ_METHOD_JACOBI: - sol = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JORInterval(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(state_rewards), ptr_to_jlong(lower), ptr_to_jlong(upper), false, 1.0, flags)); break; + sol = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JORInterval(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(state_rewards), ptr_to_jlong(lower), ptr_to_jlong(upper), false, 1.0, flags)); + break; case LIN_EQ_METHOD_JOR: - sol = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JORInterval(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(state_rewards), ptr_to_jlong(lower), ptr_to_jlong(upper), false, lin_eq_method_param, flags)); break; + sol = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JORInterval(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(state_rewards), ptr_to_jlong(lower), ptr_to_jlong(upper), false, lin_eq_method_param, flags)); + break; default: - PM_SetErrorMessage("Gauss-Seidel and its variants are currently not supported by the MTBDD engine"); return 0; + // set error message and return NULL pointer after cleanup, below + PM_SetErrorMessage("Gauss-Seidel and its variants are currently not supported by the MTBDD engine"); + break; } // set reward for infinity states to infinity diff --git a/prism/src/mtbdd/PM_ProbUntil.cc b/prism/src/mtbdd/PM_ProbUntil.cc index 1650468a..5bd86540 100644 --- a/prism/src/mtbdd/PM_ProbUntil.cc +++ b/prism/src/mtbdd/PM_ProbUntil.cc @@ -85,13 +85,18 @@ jlong __jlongpointer m // 'maybe' states soln = NULL; switch (lin_eq_method) { case LIN_EQ_METHOD_POWER: - soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1Power(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(b), ptr_to_jlong(b), false)); break; + soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1Power(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(b), ptr_to_jlong(b), false)); + break; case LIN_EQ_METHOD_JACOBI: - soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JOR(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(b), ptr_to_jlong(b), false, 1.0)); break; + soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JOR(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(b), ptr_to_jlong(b), false, 1.0)); + break; case LIN_EQ_METHOD_JOR: - soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JOR(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(b), ptr_to_jlong(b), false, lin_eq_method_param)); break; + soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JOR(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(b), ptr_to_jlong(b), false, lin_eq_method_param)); + break; default: - PM_SetErrorMessage("Gauss-Seidel and its variants are currently not supported by the MTBDD engine"); return 0; + // set error message and return NULL pointer after cleanup, below + PM_SetErrorMessage("Gauss-Seidel and its variants are currently not supported by the MTBDD engine"); + break; } // free memory diff --git a/prism/src/mtbdd/PM_ProbUntilInterval.cc b/prism/src/mtbdd/PM_ProbUntilInterval.cc index 52d33a78..c1ace0da 100644 --- a/prism/src/mtbdd/PM_ProbUntilInterval.cc +++ b/prism/src/mtbdd/PM_ProbUntilInterval.cc @@ -104,13 +104,18 @@ jint flags soln = NULL; switch (lin_eq_method) { case LIN_EQ_METHOD_POWER: - soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1PowerInterval(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(b), ptr_to_jlong(lower), ptr_to_jlong(upper), false, flags)); break; + soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1PowerInterval(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(b), ptr_to_jlong(lower), ptr_to_jlong(upper), false, flags)); + break; case LIN_EQ_METHOD_JACOBI: - soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JORInterval(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(b), ptr_to_jlong(lower), ptr_to_jlong(upper), false, 1.0, flags)); break; + soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JORInterval(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(b), ptr_to_jlong(lower), ptr_to_jlong(upper), false, 1.0, flags)); + break; case LIN_EQ_METHOD_JOR: - soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JORInterval(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(b), ptr_to_jlong(lower), ptr_to_jlong(upper), false, lin_eq_method_param, flags)); break; + soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JORInterval(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(b), ptr_to_jlong(lower), ptr_to_jlong(upper), false, lin_eq_method_param, flags)); + break; default: - PM_SetErrorMessage("Gauss-Seidel and its variants are currently not supported by the MTBDD engine"); return 0; + // set error message and return NULL pointer after cleanup, below + PM_SetErrorMessage("Gauss-Seidel and its variants are currently not supported by the MTBDD engine"); + break; } // free memory diff --git a/prism/src/mtbdd/PM_StochSteadyState.cc b/prism/src/mtbdd/PM_StochSteadyState.cc index 0d30316f..9c25d398 100644 --- a/prism/src/mtbdd/PM_StochSteadyState.cc +++ b/prism/src/mtbdd/PM_StochSteadyState.cc @@ -101,13 +101,18 @@ jint num_cvars soln = NULL; switch (lin_eq_method) { case LIN_EQ_METHOD_POWER: - soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1Power(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(b), ptr_to_jlong(init), true)); break; + soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1Power(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(b), ptr_to_jlong(init), true)); + break; case LIN_EQ_METHOD_JACOBI: - soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JOR(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(b), ptr_to_jlong(init), true, 1.0)); break; + soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JOR(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(b), ptr_to_jlong(init), true, 1.0)); + break; case LIN_EQ_METHOD_JOR: - soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JOR(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(b), ptr_to_jlong(init), true, lin_eq_method_param)); break; + soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JOR(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(b), ptr_to_jlong(init), true, lin_eq_method_param)); + break; default: - PM_SetErrorMessage("Gauss-Seidel and its variants are currently not supported by the MTBDD engine"); return 0; + // set error message and return NULL pointer after cleanup, below + PM_SetErrorMessage("Gauss-Seidel and its variants are currently not supported by the MTBDD engine"); + break; } // normalise