s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

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
master
Dave Parker 17 years ago
parent
6232c4caa6
commit
2cc923719e
10 changed files with 43 additions and 1 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 11
      prism/CHANGELOG.txt
  2. 5
      prism/src/hybrid/PH_StochBoundedUntil.cc
  3. 5
      prism/src/hybrid/PH_StochCumulReward.cc
  4. 5
      prism/src/hybrid/PH_StochTransient.cc
  5. 1
      prism/src/mtbdd/PM_StochBoundedUntil.cc
  6. 1
      prism/src/mtbdd/PM_StochCumulReward.cc
  7. 1
      prism/src/mtbdd/PM_StochTransient.cc
  8. 5
      prism/src/sparse/PS_StochBoundedUntil.cc
  9. 5
      prism/src/sparse/PS_StochCumulReward.cc
  10. 5
      prism/src/sparse/PS_StochTransient.cc

11
prism/CHANGELOG.txt
View File

@ -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):
[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

5
prism/src/hybrid/PH_StochBoundedUntil.cc
View File

@ -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

5
prism/src/hybrid/PH_StochCumulReward.cc
View File

@ -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

5
prism/src/hybrid/PH_StochTransient.cc
View File

@ -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

1
prism/src/mtbdd/PM_StochBoundedUntil.cc
View File

@ -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;
}

1
prism/src/mtbdd/PM_StochCumulReward.cc
View File

@ -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;
}

1
prism/src/mtbdd/PM_StochTransient.cc
View File

@ -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;
}

5
prism/src/sparse/PS_StochBoundedUntil.cc
View File

@ -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

5
prism/src/sparse/PS_StochCumulReward.cc
View File

@ -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

5
prism/src/sparse/PS_StochTransient.cc
View File

@ -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

Write Preview
Loading…
Cancel
Save