From bfe888031e3f41380693a9e07df47d6707236e47 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 11 Sep 2020 11:56:46 +0100 Subject: [PATCH] Consistent treatment of illegal rewards in symbolic/explicit engines. Both types of engine now disallow negative/infinite/NaN rewards. Symbolic engines will mostly still not detect the presence of NaN due to the way that CUDD deals with this. Regression tests also added. --- .../language/infinite-rewards.prism | 23 +++++++++++ .../language/infinite-rewards.prism.props | 2 + .../infinite-rewards.prism.props.args | 2 + .../functionality/language/nan-rewards.prism | 23 +++++++++++ .../language/nan-rewards.prism.props | 2 + .../language/nan-rewards.prism.props.args | 2 + .../language/negative-rewards.prism | 24 +++++++++++ .../language/negative-rewards.prism.props | 2 + .../negative-rewards.prism.props.args | 2 + .../explicit/rewards/ConstructRewards.java | 8 ++-- prism/src/prism/Modules2MTBDD.java | 40 ++++++++++++++++--- .../simulator/ModulesFileModelGenerator.java | 22 ++++++++-- 12 files changed, 138 insertions(+), 14 deletions(-) create mode 100644 prism-tests/functionality/language/infinite-rewards.prism create mode 100644 prism-tests/functionality/language/infinite-rewards.prism.props create mode 100644 prism-tests/functionality/language/infinite-rewards.prism.props.args create mode 100644 prism-tests/functionality/language/nan-rewards.prism create mode 100644 prism-tests/functionality/language/nan-rewards.prism.props create mode 100644 prism-tests/functionality/language/nan-rewards.prism.props.args create mode 100644 prism-tests/functionality/language/negative-rewards.prism create mode 100644 prism-tests/functionality/language/negative-rewards.prism.props create mode 100644 prism-tests/functionality/language/negative-rewards.prism.props.args diff --git a/prism-tests/functionality/language/infinite-rewards.prism b/prism-tests/functionality/language/infinite-rewards.prism new file mode 100644 index 00000000..d92331ea --- /dev/null +++ b/prism-tests/functionality/language/infinite-rewards.prism @@ -0,0 +1,23 @@ +dtmc + +module die + + // local state + s : [0..7] init 0; + // value of the die + d : [0..6] init 0; + + [] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2); + [] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4); + [] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6); + [] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1); + [] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3); + [] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5); + [] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6); + [] s=7 -> (s'=7); + +endmodule + +rewards "coin_flips" + s<7 : s/0; +endrewards diff --git a/prism-tests/functionality/language/infinite-rewards.prism.props b/prism-tests/functionality/language/infinite-rewards.prism.props new file mode 100644 index 00000000..62b51c61 --- /dev/null +++ b/prism-tests/functionality/language/infinite-rewards.prism.props @@ -0,0 +1,2 @@ +// RESULT: Error +R=? [F s=7]; diff --git a/prism-tests/functionality/language/infinite-rewards.prism.props.args b/prism-tests/functionality/language/infinite-rewards.prism.props.args new file mode 100644 index 00000000..68dd9ea4 --- /dev/null +++ b/prism-tests/functionality/language/infinite-rewards.prism.props.args @@ -0,0 +1,2 @@ +-s +-ex diff --git a/prism-tests/functionality/language/nan-rewards.prism b/prism-tests/functionality/language/nan-rewards.prism new file mode 100644 index 00000000..204d8b5c --- /dev/null +++ b/prism-tests/functionality/language/nan-rewards.prism @@ -0,0 +1,23 @@ +dtmc + +module die + + // local state + s : [0..7] init 0; + // value of the die + d : [0..6] init 0; + + [] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2); + [] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4); + [] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6); + [] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1); + [] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3); + [] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5); + [] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6); + [] s=7 -> (s'=7); + +endmodule + +rewards "coin_flips" + s<7 : 0/0; +endrewards diff --git a/prism-tests/functionality/language/nan-rewards.prism.props b/prism-tests/functionality/language/nan-rewards.prism.props new file mode 100644 index 00000000..62b51c61 --- /dev/null +++ b/prism-tests/functionality/language/nan-rewards.prism.props @@ -0,0 +1,2 @@ +// RESULT: Error +R=? [F s=7]; diff --git a/prism-tests/functionality/language/nan-rewards.prism.props.args b/prism-tests/functionality/language/nan-rewards.prism.props.args new file mode 100644 index 00000000..295a4c43 --- /dev/null +++ b/prism-tests/functionality/language/nan-rewards.prism.props.args @@ -0,0 +1,2 @@ +#-s +-ex diff --git a/prism-tests/functionality/language/negative-rewards.prism b/prism-tests/functionality/language/negative-rewards.prism new file mode 100644 index 00000000..273fd854 --- /dev/null +++ b/prism-tests/functionality/language/negative-rewards.prism @@ -0,0 +1,24 @@ +dtmc + +module die + + // local state + s : [0..7] init 0; + // value of the die + d : [0..6] init 0; + + [] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2); + [] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4); + [] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6); + [] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1); + [] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3); + [] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5); + [] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6); + [] s=7 -> (s'=7); + +endmodule + +rewards "coin_flips" + s<7 : 2; + s<7 : 1-2; +endrewards diff --git a/prism-tests/functionality/language/negative-rewards.prism.props b/prism-tests/functionality/language/negative-rewards.prism.props new file mode 100644 index 00000000..62b51c61 --- /dev/null +++ b/prism-tests/functionality/language/negative-rewards.prism.props @@ -0,0 +1,2 @@ +// RESULT: Error +R=? [F s=7]; diff --git a/prism-tests/functionality/language/negative-rewards.prism.props.args b/prism-tests/functionality/language/negative-rewards.prism.props.args new file mode 100644 index 00000000..68dd9ea4 --- /dev/null +++ b/prism-tests/functionality/language/negative-rewards.prism.props.args @@ -0,0 +1,2 @@ +-s +-ex diff --git a/prism/src/explicit/rewards/ConstructRewards.java b/prism/src/explicit/rewards/ConstructRewards.java index fc7378c4..d1e7913a 100644 --- a/prism/src/explicit/rewards/ConstructRewards.java +++ b/prism/src/explicit/rewards/ConstructRewards.java @@ -454,8 +454,8 @@ public class ConstructRewards extends PrismComponent private void checkStateReward(double rew, Object stateIndex, ASTElement ast) throws PrismException { String error = null; - if (Double.isNaN(rew)) { - error = "State reward evaluates to NaN"; + if (!Double.isFinite(rew)) { + error = "State reward is not finite"; } else if (!allowNegative && rew < 0) { error = "State reward is negative (" + rew + ")"; } @@ -483,8 +483,8 @@ public class ConstructRewards extends PrismComponent private void checkTransitionReward(double rew, Object stateIndex, ASTElement ast) throws PrismException { String error = null; - if (Double.isNaN(rew)) { - error = "Transition reward evaluates to NaN"; + if (!Double.isFinite(rew)) { + error = "Transition reward is not finite"; } else if (!allowNegative && rew < 0) { error = "Transition reward is negative (" + rew + ")"; } diff --git a/prism/src/prism/Modules2MTBDD.java b/prism/src/prism/Modules2MTBDD.java index 8bba2dee..c0164430 100644 --- a/prism/src/prism/Modules2MTBDD.java +++ b/prism/src/prism/Modules2MTBDD.java @@ -1968,9 +1968,23 @@ public class Modules2MTBDD if (synch == null) { // restrict rewards to relevant states item = JDD.Apply(JDD.TIMES, states, rewards); - // check for negative rewards - if ((d = JDD.FindMin(item)) < 0) { - s = "Reward structure item contains negative rewards (" + d + ")."; + // check for infinite/NaN/negative rewards + double dmin = JDD.FindMin(item); + double dmax = JDD.FindMax(item); + if (!Double.isFinite(dmin)) { + s = "Reward structure item contains non-finite rewards (" + dmin + ")."; + s += "\nNote that these may correspond to states which are unreachable."; + s += "\nIf this is the case, try strengthening the predicate."; + throw new PrismLangException(s, rs.getRewardStructItem(i)); + } + if (!Double.isFinite(dmax)) { + s = "Reward structure item contains non-finite rewards (" + dmax + ")."; + s += "\nNote that these may correspond to states which are unreachable."; + s += "\nIf this is the case, try strengthening the predicate."; + throw new PrismLangException(s, rs.getRewardStructItem(i)); + } + if (dmin < 0) { + s = "Reward structure item contains negative rewards (" + dmin + ")."; s += "\nNote that these may correspond to states which are unreachable."; s += "\nIf this is the case, try strengthening the predicate."; throw new PrismLangException(s, rs.getRewardStructItem(i)); @@ -2001,9 +2015,23 @@ public class Modules2MTBDD item = JDD.Apply(JDD.TIMES, item, states); // multiply by reward values item = JDD.Apply(JDD.TIMES, item, rewards); - // check for negative rewards - if ((d = JDD.FindMin(item)) < 0) { - s = "Reward structure item contains negative rewards (" + d + ")."; + // check for infinite/NaN/negative rewards + double dmin = JDD.FindMin(item); + double dmax = JDD.FindMax(item); + if (!Double.isFinite(dmin)) { + s = "Reward structure item contains non-finite rewards (" + dmin + ")."; + s += "\nNote that these may correspond to states which are unreachable."; + s += "\nIf this is the case, try strengthening the predicate."; + throw new PrismLangException(s, rs.getRewardStructItem(i)); + } + if (!Double.isFinite(dmax)) { + s = "Reward structure item contains non-finite rewards (" + dmax + ")."; + s += "\nNote that these may correspond to states which are unreachable."; + s += "\nIf this is the case, try strengthening the predicate."; + throw new PrismLangException(s, rs.getRewardStructItem(i)); + } + if (dmin < 0) { + s = "Reward structure item contains negative rewards (" + dmin + ")."; s += "\nNote that these may correspond to states which are unreachable."; s += "\nIf this is the case, try strengthening the predicate."; throw new PrismLangException(s, rs.getRewardStructItem(i)); diff --git a/prism/src/simulator/ModulesFileModelGenerator.java b/prism/src/simulator/ModulesFileModelGenerator.java index 4a0626ea..2aed6b77 100644 --- a/prism/src/simulator/ModulesFileModelGenerator.java +++ b/prism/src/simulator/ModulesFileModelGenerator.java @@ -415,8 +415,15 @@ public class ModulesFileModelGenerator implements ModelGenerator, RewardGenerato Expression guard = rewStr.getStates(i); if (guard.evaluateBoolean(modulesFile.getConstantValues(), state)) { double rew = rewStr.getReward(i).evaluateDouble(modulesFile.getConstantValues(), state); - if (Double.isNaN(rew)) - throw new PrismLangException("Reward structure evaluates to NaN at state " + state, rewStr.getReward(i)); + // Check reward is finite/non-negative (would be checked at model construction time, + // but more fine grained error reporting can be done here) + // Note use of original model since modulesFile may have been simplified + if (!Double.isFinite(rew)) { + throw new PrismLangException("Reward structure is not finite at state " + state, originalModulesFile.getRewardStruct(r).getReward(i)); + } + if (rew < 0) { + throw new PrismLangException("Reward structure is negative + (" + rew + ") at state " + state, originalModulesFile.getRewardStruct(r).getReward(i)); + } d += rew; } } @@ -437,8 +444,15 @@ public class ModulesFileModelGenerator implements ModelGenerator, RewardGenerato if (action == null ? (cmdAction.isEmpty()) : action.equals(cmdAction)) { if (guard.evaluateBoolean(modulesFile.getConstantValues(), state)) { double rew = rewStr.getReward(i).evaluateDouble(modulesFile.getConstantValues(), state); - if (Double.isNaN(rew)) - throw new PrismLangException("Reward structure evaluates to NaN at state " + state, rewStr.getReward(i)); + // Check reward is finite/non-negative (would be checked at model construction time, + // but more fine grained error reporting can be done here) + // Note use of original model since modulesFile may have been simplified + if (!Double.isFinite(rew)) { + throw new PrismLangException("Reward structure is not finite at state " + state, originalModulesFile.getRewardStruct(r).getReward(i)); + } + if (rew < 0) { + throw new PrismLangException("Reward structure is negative + (" + rew + ") at state " + state, originalModulesFile.getRewardStruct(r).getReward(i)); + } d += rew; } }