Browse Source

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
master
Joachim Klein 8 years ago
parent
commit
ef197ce5c8
  1. 13
      prism-tests/bugfixes/ctmc-fau-npe.sm
  2. 8
      prism-tests/bugfixes/ctmc-fau-npe.sm.props
  3. 3
      prism-tests/bugfixes/ctmc-fau-npe.sm.props.args
  4. 4
      prism/src/explicit/FastAdaptiveUniformisation.java

13
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

8
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 ];

3
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

4
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);
}
}

Loading…
Cancel
Save