diff --git a/prism-tests/bugfixes/deadlock-rewards-issue-29.prism b/prism-tests/bugfixes/deadlock-rewards-issue-29.prism new file mode 100644 index 00000000..767cf4d2 --- /dev/null +++ b/prism-tests/bugfixes/deadlock-rewards-issue-29.prism @@ -0,0 +1,15 @@ +// test case for github issue #29 +// transitions added for deadlock removal should not get rewards + +mdp + +module M1 + s: [0..1] init 0; + + // deadlock for state 1 + [] s=0 -> 1:(s'=1); +endmodule + +rewards "r" + [] true: 2; +endrewards diff --git a/prism-tests/bugfixes/deadlock-rewards-issue-29.prism.mc.props b/prism-tests/bugfixes/deadlock-rewards-issue-29.prism.mc.props new file mode 100644 index 00000000..48b4d57c --- /dev/null +++ b/prism-tests/bugfixes/deadlock-rewards-issue-29.prism.mc.props @@ -0,0 +1,3 @@ +// total reward +// RESULT: 2.0 +R=?[ C ] diff --git a/prism-tests/bugfixes/deadlock-rewards-issue-29.prism.mc.props.args b/prism-tests/bugfixes/deadlock-rewards-issue-29.prism.mc.props.args new file mode 100644 index 00000000..8537dae1 --- /dev/null +++ b/prism-tests/bugfixes/deadlock-rewards-issue-29.prism.mc.props.args @@ -0,0 +1,11 @@ +# As a CTMC +-ctmc -ex +-ctmc -mtbdd +-ctmc -hybrid +-ctmc -sparse + +# As a DTMC +-dtmc -ex +-dtmc -mtbdd +-dtmc -hybrid +-dtmc -sparse diff --git a/prism-tests/bugfixes/deadlock-rewards-issue-29.prism.props b/prism-tests/bugfixes/deadlock-rewards-issue-29.prism.props new file mode 100644 index 00000000..94cd6b76 --- /dev/null +++ b/prism-tests/bugfixes/deadlock-rewards-issue-29.prism.props @@ -0,0 +1,6 @@ +// total reward +// RESULT: 2.0 +Rmax=?[ C ] + +// RESULT: 2.0 +Rmin=?[ C ] diff --git a/prism-tests/bugfixes/deadlock-rewards-issue-29.prism.props.args b/prism-tests/bugfixes/deadlock-rewards-issue-29.prism.props.args new file mode 100644 index 00000000..d1e28394 --- /dev/null +++ b/prism-tests/bugfixes/deadlock-rewards-issue-29.prism.props.args @@ -0,0 +1,4 @@ +-ex +-mtbdd +-hybrid +-sparse diff --git a/prism/src/explicit/rewards/ConstructRewards.java b/prism/src/explicit/rewards/ConstructRewards.java index 0ef9d089..3c4af8aa 100644 --- a/prism/src/explicit/rewards/ConstructRewards.java +++ b/prism/src/explicit/rewards/ConstructRewards.java @@ -174,6 +174,12 @@ public class ConstructRewards if (guard.evaluateBoolean(constantValues, statesList.get(j))) { // Transition reward if (rewStr.getRewardStructItem(i).isTransitionReward()) { + if (mdp.isDeadlockState(j)) { + // As state j is a deadlock state, any outgoing transition + // was added to "fix" the deadlock and thus does not get a reward. + // Skip to next state + continue; + } numChoices = mdp.getNumChoices(j); for (k = 0; k < numChoices; k++) { mdpAction = mdp.getAction(j, k); @@ -275,7 +281,14 @@ public class ConstructRewards if (!allowNegative && rew < 0) throw new PrismException("Reward structure evaluates to " + rew + " at state " + state +", negative rewards not allowed"); rewSimple.addToStateReward(j, rew); + // State-action rewards + if (mdp.isDeadlockState(j)) { + // As state j is a deadlock state, any outgoing transition + // was added to "fix" the deadlock and thus does not get a reward. + // Skip to next state + continue; + } int numChoices = mdp.getNumChoices(j); for (int k = 0; k < numChoices; k++) { rew = modelGen.getStateActionReward(r, state, mdp.getAction(j, k));