From ef197ce5c83b67eaff0f7ee4901786e807c81b02 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 9 Jul 2018 15:47:58 +0200 Subject: [PATCH] Fix NPE in fast adaptive uniformisation (cumulative reward, transition rewards without action name) The action object attached to a transition can be null (internal action), leading to a null pointer exception when trying to call the toString method. + test case --- prism-tests/bugfixes/ctmc-fau-npe.sm | 13 +++++++++++++ prism-tests/bugfixes/ctmc-fau-npe.sm.props | 8 ++++++++ prism-tests/bugfixes/ctmc-fau-npe.sm.props.args | 3 +++ prism/src/explicit/FastAdaptiveUniformisation.java | 4 ++-- 4 files changed, 26 insertions(+), 2 deletions(-) create mode 100644 prism-tests/bugfixes/ctmc-fau-npe.sm create mode 100644 prism-tests/bugfixes/ctmc-fau-npe.sm.props create mode 100644 prism-tests/bugfixes/ctmc-fau-npe.sm.props.args diff --git a/prism-tests/bugfixes/ctmc-fau-npe.sm b/prism-tests/bugfixes/ctmc-fau-npe.sm new file mode 100644 index 00000000..74bd1e9b --- /dev/null +++ b/prism-tests/bugfixes/ctmc-fau-npe.sm @@ -0,0 +1,13 @@ +// test for null-pointer exception fix in fast adaptive uniformisation (cumulative reward operator) + +ctmc + +module m1 + s: [0..1] init 0; + + [] s=0 -> 2:(s'=1); +endmodule + +rewards "steps" + [] true : 1; +endrewards diff --git a/prism-tests/bugfixes/ctmc-fau-npe.sm.props b/prism-tests/bugfixes/ctmc-fau-npe.sm.props new file mode 100644 index 00000000..900417a5 --- /dev/null +++ b/prism-tests/bugfixes/ctmc-fau-npe.sm.props @@ -0,0 +1,8 @@ +const double T; + +// RESULT (T=1): 0.8646645498740888 +// RESULT (T=2): 0.9816832980524708 +// RESULT (T=3): 0.9975207981483099 +// RESULT (T=4): 0.9996641287431798 +// RESULT (T=5): 0.9999538916843567 +R=? [ C<=T ]; diff --git a/prism-tests/bugfixes/ctmc-fau-npe.sm.props.args b/prism-tests/bugfixes/ctmc-fau-npe.sm.props.args new file mode 100644 index 00000000..8485aa75 --- /dev/null +++ b/prism-tests/bugfixes/ctmc-fau-npe.sm.props.args @@ -0,0 +1,3 @@ +-const T=1:1:5 -transientmethod unif +-const T=1:1:5 -transientmethod fau + diff --git a/prism/src/explicit/FastAdaptiveUniformisation.java b/prism/src/explicit/FastAdaptiveUniformisation.java index 1ac54a85..7f041c01 100644 --- a/prism/src/explicit/FastAdaptiveUniformisation.java +++ b/prism/src/explicit/FastAdaptiveUniformisation.java @@ -1271,11 +1271,11 @@ public final class FastAdaptiveUniformisation extends PrismComponent for (int j = 0; j < numChoices; j++) { int numTransitions = modelGen.getNumTransitions(j); for (int k = 0; k < numTransitions; k++) { - String tAction = modelGen.getTransitionAction(j, k).toString(); + Object tAction = modelGen.getTransitionAction(j, k); if (tAction == null) { tAction = ""; } - if (tAction.equals(action)) { + if (tAction.toString().equals(action)) { sumReward += reward * modelGen.getTransitionProbability(j, k); } }