diff --git a/prism-tests/functionality/language/infinite-rates.prism b/prism-tests/functionality/language/infinite-rates.prism new file mode 100644 index 00000000..e84f9078 --- /dev/null +++ b/prism-tests/functionality/language/infinite-rates.prism @@ -0,0 +1,51 @@ +// polling example [IT90] +// gxn/dxp 26/01/00 + +ctmc + +const int N = 2; + +const double mu = 1/0; +const double gamma = 200; +const double lambda = mu/N; + +module server + + s : [1..2]; // station + a : [0..1]; // action: 0=polling, 1=serving + + [loop1a] (s=1)&(a=0) -> gamma : (s'=s+1); + [loop1b] (s=1)&(a=0) -> gamma : (a'=1); + [serve1] (s=1)&(a=1) -> mu : (s'=s+1)&(a'=0); + + [loop2a] (s=2)&(a=0) -> gamma : (s'=1); + [loop2b] (s=2)&(a=0) -> gamma : (a'=1); + [serve2] (s=2)&(a=1) -> mu : (s'=1)&(a'=0); + +endmodule + +module station1 + + s1 : [0..1]; // state of station: 0=empty, 1=full + + [loop1a] (s1=0) -> 1 : (s1'=0); + [] (s1=0) -> lambda : (s1'=1); + [loop1b] (s1=1) -> 1 : (s1'=1); + [serve1] (s1=1) -> 1 : (s1'=0); + +endmodule + +// construct further stations through renaming + +module station2 = station1 [ s1=s2, loop1a=loop2a, loop1b=loop2b, serve1=serve2 ] endmodule +// (cumulative) rewards + +// expected time station 1 is waiting to be served +rewards "waiting" + s1=1 & !(s=1 & a=1) : 1; +endrewards + +// expected number of times station 1 is served +rewards "served" + [serve1] true : 1; +endrewards diff --git a/prism-tests/functionality/language/infinite-rates.prism.props b/prism-tests/functionality/language/infinite-rates.prism.props new file mode 100644 index 00000000..fce966d6 --- /dev/null +++ b/prism-tests/functionality/language/infinite-rates.prism.props @@ -0,0 +1,2 @@ +// RESULT: Error +P=? [ s1=1 ]; diff --git a/prism-tests/functionality/language/infinite-rates.prism.props.args b/prism-tests/functionality/language/infinite-rates.prism.props.args new file mode 100644 index 00000000..68dd9ea4 --- /dev/null +++ b/prism-tests/functionality/language/infinite-rates.prism.props.args @@ -0,0 +1,2 @@ +-s +-ex diff --git a/prism/src/simulator/Updater.java b/prism/src/simulator/Updater.java index 74b60c87..6a6e565a 100644 --- a/prism/src/simulator/Updater.java +++ b/prism/src/simulator/Updater.java @@ -359,8 +359,8 @@ public class Updater extends PrismComponent for (i = 0; i < n; i++) { // Compute probability/rate p = ups.getProbabilityInState(i, state); - // Check for negative/NaN probabilities/rates - if (Double.isNaN(p) || p < 0) { + // Check for non-finite/NaN probabilities/rates + if (!Double.isFinite(p) || p < 0) { String s = modelType.choicesSumToOne() ? "Probability" : "Rate"; s += " is invalid (" + p + ") in state " + state.toString(modulesFile); // Note: we indicate error in whole Updates object because the offending