diff --git a/prism/src/mtbdd/PM_StochBoundedUntil.cc b/prism/src/mtbdd/PM_StochBoundedUntil.cc index 41442dd9..3ea647ff 100644 --- a/prism/src/mtbdd/PM_StochBoundedUntil.cc +++ b/prism/src/mtbdd/PM_StochBoundedUntil.cc @@ -183,7 +183,21 @@ jlong __jlongpointer mu // probs for multiplying // compute poisson probabilities (fox/glynn) PM_PrintToMainLog(env, "\nUniformisation: q.t = %f x %f = %f\n", unif, time, unif * time); fgw = fox_glynn(unif * time, 1.0e-300, 1.0e+300, term_crit_param_unif); - if (fgw.right < 0) { PM_SetErrorMessage("Overflow in Fox-Glynn computation (time bound too big?)"); return 0; } + if (fgw.right < 0) { + PM_SetErrorMessage("Overflow in Fox-Glynn computation (time bound too big?)"); + + if (combine) { + // METHOD 1 + Cudd_RecursiveDeref(ddman, q); + } + else { + // METHOD 2 + Cudd_RecursiveDeref(ddman, r); + Cudd_RecursiveDeref(ddman, d); + } + Cudd_RecursiveDeref(ddman, diags); + return 0; + } for (i = fgw.left; i <= fgw.right; i++) { fgw.weights[i-fgw.left] /= fgw.total_weight; } diff --git a/prism/src/mtbdd/PM_StochCumulReward.cc b/prism/src/mtbdd/PM_StochCumulReward.cc index 6170f246..2498bf0c 100644 --- a/prism/src/mtbdd/PM_StochCumulReward.cc +++ b/prism/src/mtbdd/PM_StochCumulReward.cc @@ -131,7 +131,14 @@ jdouble time // time bound // compute poisson probabilities (fox/glynn) PM_PrintToMainLog(env, "\nUniformisation: q.t = %f x %f = %f\n", unif, time, unif * time); fgw = fox_glynn(unif * time, 1.0e-300, 1.0e+300, term_crit_param_unif); - if (fgw.right < 0) { PM_SetErrorMessage("Overflow in Fox-Glynn computation (time bound too big?)"); return 0; } + if (fgw.right < 0) { + PM_SetErrorMessage("Overflow in Fox-Glynn computation (time bound too big?)"); + Cudd_RecursiveDeref(ddman, q); + Cudd_RecursiveDeref(ddman, diags); + Cudd_RecursiveDeref(ddman, sol); + Cudd_RecursiveDeref(ddman, sum); + return 0; + } for (i = fgw.left; i <= fgw.right; i++) { fgw.weights[i-fgw.left] /= fgw.total_weight; } diff --git a/prism/src/mtbdd/PM_StochTransient.cc b/prism/src/mtbdd/PM_StochTransient.cc index 8d99930b..bf84a833 100644 --- a/prism/src/mtbdd/PM_StochTransient.cc +++ b/prism/src/mtbdd/PM_StochTransient.cc @@ -164,7 +164,24 @@ jdouble time // time // compute poisson probabilities (fox/glynn) PM_PrintToMainLog(env, "\nUniformisation: q.t = %f x %f = %f\n", unif, time, unif * time); fgw = fox_glynn(unif * time, 1.0e-300, 1.0e+300, term_crit_param_unif); - if (fgw.right < 0) { PM_SetErrorMessage("Overflow in Fox-Glynn computation (time bound too big?)"); return 0; } + if (fgw.right < 0) { + PM_SetErrorMessage("Overflow in Fox-Glynn computation (time bound too big?)"); + + if (combine) { + // METHOD 1 + Cudd_RecursiveDeref(ddman, q); + } + else { + // METHOD 2 + Cudd_RecursiveDeref(ddman, r); + Cudd_RecursiveDeref(ddman, d); + } + Cudd_RecursiveDeref(ddman, diags); + // nb: we deref init, even though it is passed in as a param + Cudd_RecursiveDeref(ddman, init); + + return 0; + } for (i = fgw.left; i <= fgw.right; i++) { fgw.weights[i-fgw.left] /= fgw.total_weight; }