From 2cc923719e5b4bf8bae6d8bf8268fb0305bb7876 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 19 Dec 2008 12:36:39 +0000 Subject: [PATCH] Bug fix: Detection of error when Fox-Glynn value computation overflows. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@902 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/CHANGELOG.txt | 11 ++++++++++- prism/src/hybrid/PH_StochBoundedUntil.cc | 5 +++++ prism/src/hybrid/PH_StochCumulReward.cc | 5 +++++ prism/src/hybrid/PH_StochTransient.cc | 5 +++++ prism/src/mtbdd/PM_StochBoundedUntil.cc | 1 + prism/src/mtbdd/PM_StochCumulReward.cc | 1 + prism/src/mtbdd/PM_StochTransient.cc | 1 + prism/src/sparse/PS_StochBoundedUntil.cc | 5 +++++ prism/src/sparse/PS_StochCumulReward.cc | 5 +++++ prism/src/sparse/PS_StochTransient.cc | 5 +++++ 10 files changed, 43 insertions(+), 1 deletion(-) diff --git a/prism/CHANGELOG.txt b/prism/CHANGELOG.txt index 11b38fee..f29e0b17 100644 --- a/prism/CHANGELOG.txt +++ b/prism/CHANGELOG.txt @@ -7,11 +7,20 @@ of the main changes in each public release, see the file VERSIONS.txt. Ongoing changes: * LTL model checking for MDPs +* CTL model checking -Latest changes (reverse chronological): +Latest changes (reverse chronological): +[correct wrt svn rev 901] +* Improvements to memory handling, especially in sparse/hybrid engines +* Updated JFreeChart library +* Multiple -const switches allowed at command-line +* Efficiency improvements to precomputation algorithms +* Added symmetry reduction functionality +* New -exportbsccs option * Expanded property specification language * Initial state info for explicit import is now via -importlabels +* Added prism2html/prism2latex scripts * Transient probabilities computation for DTMCs * Sparse/hybrid versions of instantaneous reward properties (R=?[I=k]) for DTMCs * Added weak until (W) and release (R) to properties language diff --git a/prism/src/hybrid/PH_StochBoundedUntil.cc b/prism/src/hybrid/PH_StochBoundedUntil.cc index 2168a242..a9e4b73d 100644 --- a/prism/src/hybrid/PH_StochBoundedUntil.cc +++ b/prism/src/hybrid/PH_StochBoundedUntil.cc @@ -208,6 +208,7 @@ jlong __jlongpointer mu // probs for multiplying // compute poisson probabilities (fox/glynn) PH_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) throw "Overflow in Fox-Glynn computation (time bound too big?)"; for (i = fgw.left; i <= fgw.right; i++) { fgw.weights[i-fgw.left] /= fgw.total_weight; } @@ -316,6 +317,10 @@ jlong __jlongpointer mu // probs for multiplying PH_SetErrorMessage("Out of memory"); if (sum) delete[] sum; sum = 0; + } catch (const char *err) { + PH_SetErrorMessage(err); + if (sum) delete sum; + sum = 0; } // free memory diff --git a/prism/src/hybrid/PH_StochCumulReward.cc b/prism/src/hybrid/PH_StochCumulReward.cc index 70483059..db7cbe18 100644 --- a/prism/src/hybrid/PH_StochCumulReward.cc +++ b/prism/src/hybrid/PH_StochCumulReward.cc @@ -206,6 +206,7 @@ jdouble time // time bound // compute poisson probabilities (fox/glynn) PH_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) throw "Overflow in Fox-Glynn computation (time bound too big?)"; for (i = fgw.left; i <= fgw.right; i++) { fgw.weights[i-fgw.left] /= fgw.total_weight; } @@ -330,6 +331,10 @@ jdouble time // time bound PH_SetErrorMessage("Out of memory"); if (sum) delete[] sum; sum = 0; + } catch (const char *err) { + PH_SetErrorMessage(err); + if (sum) delete sum; + sum = 0; } // free memory diff --git a/prism/src/hybrid/PH_StochTransient.cc b/prism/src/hybrid/PH_StochTransient.cc index d7a99be1..dc79eb25 100644 --- a/prism/src/hybrid/PH_StochTransient.cc +++ b/prism/src/hybrid/PH_StochTransient.cc @@ -187,6 +187,7 @@ jdouble time // time bound // compute poisson probabilities (fox/glynn) PH_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) throw "Overflow in Fox-Glynn computation (time bound too big?)"; for (i = fgw.left; i <= fgw.right; i++) { fgw.weights[i-fgw.left] /= fgw.total_weight; } @@ -295,6 +296,10 @@ jdouble time // time bound PH_SetErrorMessage("Out of memory"); if (sum) delete[] sum; sum = 0; + } catch (const char *err) { + PH_SetErrorMessage(err); + if (sum) delete sum; + sum = 0; } // free memory diff --git a/prism/src/mtbdd/PM_StochBoundedUntil.cc b/prism/src/mtbdd/PM_StochBoundedUntil.cc index c9a09b00..381efd11 100644 --- a/prism/src/mtbdd/PM_StochBoundedUntil.cc +++ b/prism/src/mtbdd/PM_StochBoundedUntil.cc @@ -183,6 +183,7 @@ 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; } 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 8a6b5514..2fc223bc 100644 --- a/prism/src/mtbdd/PM_StochCumulReward.cc +++ b/prism/src/mtbdd/PM_StochCumulReward.cc @@ -131,6 +131,7 @@ 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; } 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 81ab204d..a50e0269 100644 --- a/prism/src/mtbdd/PM_StochTransient.cc +++ b/prism/src/mtbdd/PM_StochTransient.cc @@ -164,6 +164,7 @@ jint 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; } for (i = fgw.left; i <= fgw.right; i++) { fgw.weights[i-fgw.left] /= fgw.total_weight; } diff --git a/prism/src/sparse/PS_StochBoundedUntil.cc b/prism/src/sparse/PS_StochBoundedUntil.cc index 5c2b517f..9b2a8a51 100644 --- a/prism/src/sparse/PS_StochBoundedUntil.cc +++ b/prism/src/sparse/PS_StochBoundedUntil.cc @@ -196,6 +196,7 @@ jlong __jlongpointer mu // probs for multiplying // compute poisson probabilities (fox/glynn) PS_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) throw "Overflow in Fox-Glynn computation (time bound too big?)"; for (i = fgw.left; i <= fgw.right; i++) { fgw.weights[i-fgw.left] /= fgw.total_weight; } @@ -341,6 +342,10 @@ jlong __jlongpointer mu // probs for multiplying PS_SetErrorMessage("Out of memory"); if (sum) delete sum; sum = 0; + } catch (const char *err) { + PS_SetErrorMessage(err); + if (sum) delete sum; + sum = 0; } // free memory diff --git a/prism/src/sparse/PS_StochCumulReward.cc b/prism/src/sparse/PS_StochCumulReward.cc index 6068eb96..675c3140 100644 --- a/prism/src/sparse/PS_StochCumulReward.cc +++ b/prism/src/sparse/PS_StochCumulReward.cc @@ -194,6 +194,7 @@ jdouble time // time bound // compute poisson probabilities (fox/glynn) PS_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) throw "Overflow in Fox-Glynn computation (time bound too big?)"; for (i = fgw.left; i <= fgw.right; i++) { fgw.weights[i-fgw.left] /= fgw.total_weight; } @@ -354,6 +355,10 @@ jdouble time // time bound PS_SetErrorMessage("Out of memory"); if (sum) delete[] sum; sum = 0; + } catch (const char *err) { + PS_SetErrorMessage(err); + if (sum) delete sum; + sum = 0; } // free memory diff --git a/prism/src/sparse/PS_StochTransient.cc b/prism/src/sparse/PS_StochTransient.cc index dfe4c5fc..3665c0fd 100644 --- a/prism/src/sparse/PS_StochTransient.cc +++ b/prism/src/sparse/PS_StochTransient.cc @@ -174,6 +174,7 @@ jdouble time // time bound // compute poisson probabilities (fox/glynn) PS_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) throw "Overflow in Fox-Glynn computation (time bound too big?)"; for (i = fgw.left; i <= fgw.right; i++) { fgw.weights[i-fgw.left] /= fgw.total_weight; } @@ -319,6 +320,10 @@ jdouble time // time bound PS_SetErrorMessage("Out of memory"); if (sum) delete[] sum; sum = 0; + } catch (const char *err) { + PS_SetErrorMessage(err); + if (sum) delete sum; + sum = 0; } // free memory