diff --git a/prism-tests/functionality/language/negative-rewards.prism b/prism-tests/functionality/language/negative-rewards.prism index 273fd8548..462c3c7a6 100644 --- a/prism-tests/functionality/language/negative-rewards.prism +++ b/prism-tests/functionality/language/negative-rewards.prism @@ -19,6 +19,6 @@ module die endmodule rewards "coin_flips" - s<7 : 2; + //s<7 : 2; s<7 : 1-2; endrewards diff --git a/prism/etc/scripts/prism-log-extract b/prism/etc/scripts/prism-log-extract index 78f4596bc..7cea2229e 100755 --- a/prism/etc/scripts/prism-log-extract +++ b/prism/etc/scripts/prism-log-extract @@ -110,19 +110,20 @@ def grep_for_info_file(logFile, fields): info['log_file'] = os.path.basename(logFile) # For other fields, we parse the log line_num = 1 - for line in open(logFile, 'r').readlines(): - # We assume the first line printed out is the tool name - if line_num == 1: - info['prog_name'] = line.strip() - # For most fields, a regexp is used to grep the log - for field in fields: - field_details = get_field_details(field) - if 'regexp' in field_details and (info[field] == '' or ('match' in field_details and field_details['match'] == 'last')): - regexp = field_details['regexp'] - m = re.search(regexp, line) - if not m is None: - info[field] = m.group(1) - line_num = line_num + 1 + with open(logFile, 'r') as f: + for line in f: + # We assume the first line printed out is the tool name + if line_num == 1: + info['prog_name'] = line.strip() + # For most fields, a regexp is used to grep the log + for field in fields: + field_details = get_field_details(field) + if 'regexp' in field_details and (info[field] == '' or ('match' in field_details and field_details['match'] == 'last')): + regexp = field_details['regexp'] + m = re.search(regexp, line) + if not m is None: + info[field] = m.group(1) + line_num = line_num + 1 # Some field processing based on type for field in info.keys(): field_details = get_field_details(field) diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index 49b85eb0c..e2126f4c5 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -1603,7 +1603,7 @@ public void exportStateRewards(Model model, int r, File file, Mod } try (PrismLog out = getPrismLogForFile(file)) { - Rewards modelRewards = constructRewards(model, r); + Rewards modelRewards = constructRewards(model, r, true); PrismExplicitExporter exporter = new PrismExplicitExporter<>(exportOptions); exporter.exportStateRewards(model, modelRewards, rewardGen.getRewardStructName(r), out); } @@ -1623,7 +1623,7 @@ public void exportTransRewards(Model model, int r, File file, Mod } try (PrismLog out = getPrismLogForFile(file)) { - Rewards modelRewards = constructRewards(model, r); + Rewards modelRewards = constructRewards(model, r, true); PrismExplicitExporter exporter = new PrismExplicitExporter<>(exportOptions); exporter.exportTransRewards(model, modelRewards, rewardGen.getRewardStructName(r), out); } diff --git a/prism/src/explicit/rewards/ConstructRewards.java b/prism/src/explicit/rewards/ConstructRewards.java index b739297c1..a5ee8bc83 100644 --- a/prism/src/explicit/rewards/ConstructRewards.java +++ b/prism/src/explicit/rewards/ConstructRewards.java @@ -201,10 +201,10 @@ private Value getAndCheckStateReward(int s, RewardGenerator rewar if (rewardGen.isRewardLookupSupported(RewardLookup.BY_STATE)) { State state = statesList.get(s); stateIndex = state; - rew = rewardGen.getStateReward(r, state); + rew = rewardGen.getStateReward(r, state, allowNegative); } else if (rewardGen.isRewardLookupSupported(RewardLookup.BY_STATE_INDEX)) { stateIndex = s; - rew = rewardGen.getStateReward(r, s); + rew = rewardGen.getStateReward(r, s, allowNegative); } else { throw new PrismException("Unknown reward lookup mechanism for reward generator"); } @@ -228,10 +228,10 @@ private Value getAndCheckStateActionReward(int s, Object action, RewardG if (rewardGen.isRewardLookupSupported(RewardLookup.BY_STATE)) { State state = statesList.get(s); stateIndex = state; - rew = rewardGen.getStateActionReward(r, state, action); + rew = rewardGen.getStateActionReward(r, state, action, allowNegative); } else if (rewardGen.isRewardLookupSupported(RewardLookup.BY_STATE_INDEX)) { stateIndex = s; - rew = rewardGen.getStateActionReward(r, s, action); + rew = rewardGen.getStateActionReward(r, s, action, allowNegative); } else { throw new PrismException("Unknown reward lookup mechanism for reward generator"); } diff --git a/prism/src/explicit/rewards/Rewards2RewardGenerator.java b/prism/src/explicit/rewards/Rewards2RewardGenerator.java index 638e66322..4f6044d5c 100644 --- a/prism/src/explicit/rewards/Rewards2RewardGenerator.java +++ b/prism/src/explicit/rewards/Rewards2RewardGenerator.java @@ -30,6 +30,7 @@ import parser.State; import prism.Evaluator; import prism.PrismException; +import prism.PrismLangException; import prism.RewardGenerator; import prism.RewardInfo; @@ -116,7 +117,7 @@ public boolean isRewardLookupSupported(RewardLookup lookup) } @Override - public Value getStateReward(int r, State state) throws PrismException + public Value getStateReward(int r, State state, boolean allowNegative) throws PrismException { if (statesList == null) { throw new PrismException("Reward lookup by State not possible since state list is missing"); @@ -125,13 +126,17 @@ public Value getStateReward(int r, State state) throws PrismException if (s == -1) { throw new PrismException("Unknown state " + state); } - return getStateReward(r, s); + return getStateReward(r, s, allowNegative); } @Override - public Value getStateReward(int r, int s) throws PrismException + public Value getStateReward(int r, int s, boolean allowNegative) throws PrismException { - return getRewardObject(r).getStateReward(s); + Value rew = getRewardObject(r).getStateReward(s); + if (!allowNegative && !eval.geq(rew, eval.zero())) { + throw new PrismException("Reward is negative (" + rew + ") at state " + s); + } + return rew; } @Override diff --git a/prism/src/prism/RewardGenerator.java b/prism/src/prism/RewardGenerator.java index 53f943a74..523e97c91 100644 --- a/prism/src/prism/RewardGenerator.java +++ b/prism/src/prism/RewardGenerator.java @@ -83,11 +83,27 @@ public default boolean isRewardLookupSupported(RewardLookup lookup) * Only available if {@link #isRewardLookupSupported(RewardLookup)} returns true for {@code RewardLookup.BY_STATE)}. * If a reward structure has no state rewards, you can indicate this by implementing * the method {@link #rewardStructHasStateRewards(int)}, which may improve efficiency - * and/or allow use of algorithms/implementations that do not support state rewards rewards. + * and/or allow use of algorithms/implementations that do not support state rewards. * @param r The index of the reward structure to use * @param state The state in which to evaluate the rewards */ public default Value getStateReward(int r, State state) throws PrismException + { + return getStateReward(r, state, false); + } + + /** + * Get the state reward of the {@code r}th reward structure for state {@code state} + * ({@code r} is indexed from 0, not from 1 like at the user (property language) level). + * Only available if {@link #isRewardLookupSupported(RewardLookup)} returns true for {@code RewardLookup.BY_STATE)}. + * If a reward structure has no state rewards, you can indicate this by implementing + * the method {@link #rewardStructHasStateRewards(int)}, which may improve efficiency + * and/or allow use of algorithms/implementations that do not support state rewards. + * @param r The index of the reward structure to use + * @param state The state in which to evaluate the rewards + * @param allowNegative Whether to allow negative rewards + */ + public default Value getStateReward(int r, State state, boolean allowNegative) throws PrismException { // Default implementation: error if not supported, or bad index if (!isRewardLookupSupported(RewardLookup.BY_STATE)) { @@ -99,7 +115,7 @@ public default Value getStateReward(int r, State state) throws PrismException // Otherwise, if reward is not defined, that's an error throw new PrismException("Reward has not been defined"); } - + /** * Get the state-action reward of the {@code r}th reward structure for state {@code state} and action {@code action} * ({@code r} is indexed from 0, not from 1 like at the user (property language) level). @@ -112,6 +128,23 @@ public default Value getStateReward(int r, State state) throws PrismException * @param action The outgoing action label */ public default Value getStateActionReward(int r, State state, Object action) throws PrismException + { + return getStateActionReward(r, state, action, false); + } + + /** + * Get the state-action reward of the {@code r}th reward structure for state {@code state} and action {@code action} + * ({@code r} is indexed from 0, not from 1 like at the user (property language) level). + * Only available if {@link #isRewardLookupSupported(RewardLookup)} returns true for {@code RewardLookup.BY_STATE)}. + * If a reward structure has no transition rewards, you can indicate this by implementing + * the method {@link #rewardStructHasTransitionRewards(int)}, which may improve efficiency + * and/or allow use of algorithms/implementations that do not support transition rewards. + * @param r The index of the reward structure to use + * @param state The state in which to evaluate the rewards + * @param action The outgoing action label + * @param allowNegative Whether to allow negative rewards + */ + public default Value getStateActionReward(int r, State state, Object action, boolean allowNegative) throws PrismException { // Default implementation: error if not supported, or bad index if (!isRewardLookupSupported(RewardLookup.BY_STATE)) { @@ -123,7 +156,7 @@ public default Value getStateActionReward(int r, State state, Object action) thr // Otherwise, if reward is not defined, that's an error throw new PrismException("Reward has not been defined"); } - + /** * Get the state reward of the {@code r}th reward structure for state {@code s} * ({@code r} is indexed from 0, not from 1 like at the user (property language) level). @@ -135,6 +168,22 @@ public default Value getStateActionReward(int r, State state, Object action) thr * @param s The index of the state in which to evaluate the rewards */ public default Value getStateReward(int r, int s) throws PrismException + { + return getStateReward(r, s, false); + } + + /** + * Get the state reward of the {@code r}th reward structure for state {@code s} + * ({@code r} is indexed from 0, not from 1 like at the user (property language) level). + * Only available if {@link #isRewardLookupSupported(RewardLookup)} returns true for {@code RewardLookup.BY_STATE_INDEX)}. + * If a reward structure has no state rewards, you can indicate this by implementing + * the method {@link #rewardStructHasStateRewards(int)}, which may improve efficiency + * and/or allow use of algorithms/implementations that do not support state rewards. + * @param r The index of the reward structure to use + * @param s The index of the state in which to evaluate the rewards + * @param allowNegative Whether to allow negative rewards + */ + public default Value getStateReward(int r, int s, boolean allowNegative) throws PrismException { // Default implementation: error if not supported, or bad index if (!isRewardLookupSupported(RewardLookup.BY_STATE_INDEX)) { @@ -159,6 +208,23 @@ public default Value getStateReward(int r, int s) throws PrismException * @param action The outgoing action label */ public default Value getStateActionReward(int r, int s, Object action) throws PrismException + { + return getStateActionReward(r, s, action, false); + } + + /** + * Get the state-action reward of the {@code r}th reward structure for state {@code s} and action {@code action} + * ({@code r} is indexed from 0, not from 1 like at the user (property language) level). + * Only available if {@link #isRewardLookupSupported(RewardLookup)} returns true for {@code RewardLookup.BY_STATE_INDEX)}. + * If a reward structure has no transition rewards, you can indicate this by implementing + * the method {@link #rewardStructHasTransitionRewards(int)}, which may improve efficiency + * and/or allow use of algorithms/implementations that do not support transition rewards. + * @param r The index of the reward structure to use + * @param s The index of the state in which to evaluate the rewards + * @param action The outgoing action label + * @param allowNegative Whether to allow negative rewards + */ + public default Value getStateActionReward(int r, int s, Object action, boolean allowNegative) throws PrismException { // Default implementation: error if not supported, or bad index if (!isRewardLookupSupported(RewardLookup.BY_STATE_INDEX)) { @@ -170,7 +236,7 @@ public default Value getStateActionReward(int r, int s, Object action) throws Pr // Otherwise, if reward is not defined, that's an error throw new PrismException("Reward has not been defined"); } - + /** * Get a {@link RewardStruct} object representing the {@code r}th reward structure * ({@code r} is indexed from 0, not from 1 like at the user (property language) level). diff --git a/prism/src/simulator/ModulesFileModelGenerator.java b/prism/src/simulator/ModulesFileModelGenerator.java index 1cb266522..ded00e49d 100644 --- a/prism/src/simulator/ModulesFileModelGenerator.java +++ b/prism/src/simulator/ModulesFileModelGenerator.java @@ -720,7 +720,7 @@ public boolean rewardStructHasTransitionRewards(int i) } @Override - public Value getStateReward(int r, State state) throws PrismException + public Value getStateReward(int r, State state, boolean allowNegative) throws PrismException { RewardStruct rewStr = modulesFile.getRewardStruct(r); int n = rewStr.getNumItems(); @@ -739,8 +739,8 @@ public Value getStateReward(int r, State state) throws PrismException if (!eval.isFinite(rew)) { throw new PrismLangException("Reward structure is not finite at state " + state, rewStr.getReward(i)); } - if (!eval.geq(rew, eval.zero())) { - throw new PrismLangException("Reward structure is negative + (" + rew + ") at state " + state, originalModulesFile.getRewardStruct(r).getReward(i)); + if (!allowNegative && !eval.geq(rew, eval.zero())) { + throw new PrismLangException("Reward structure is negative (" + rew + ") at state " + state, originalModulesFile.getRewardStruct(r).getReward(i)); } } d = eval.add(d, rew); @@ -751,7 +751,7 @@ public Value getStateReward(int r, State state) throws PrismException } @Override - public Value getStateActionReward(int r, State state, Object action) throws PrismException + public Value getStateActionReward(int r, State state, Object action, boolean allowNegative) throws PrismException { RewardStruct rewStr = modulesFile.getRewardStruct(r); int n = rewStr.getNumItems(); @@ -772,8 +772,8 @@ public Value getStateActionReward(int r, State state, Object action) throws Pris if (!eval.isFinite(rew)) { throw new PrismLangException("Reward structure is not finite at state " + state, rewStr.getReward(i)); } - if (!eval.geq(rew, eval.zero())) { - throw new PrismLangException("Reward structure is negative + (" + rew + ") at state " + state, originalModulesFile.getRewardStruct(r).getReward(i)); + if (!allowNegative && !eval.geq(rew, eval.zero())) { + throw new PrismLangException("Reward structure is negative (" + rew + ") at state " + state, originalModulesFile.getRewardStruct(r).getReward(i)); } } d = eval.add(d, rew); diff --git a/prism/src/symbolic/build/Modules2MTBDD.java b/prism/src/symbolic/build/Modules2MTBDD.java index 64e4a23e0..6a8399501 100644 --- a/prism/src/symbolic/build/Modules2MTBDD.java +++ b/prism/src/symbolic/build/Modules2MTBDD.java @@ -2114,12 +2114,12 @@ private void computeRewards(SystemDDs sysDDs) throws PrismException s += "\nIf this is the case, try strengthening the predicate."; throw new PrismLangException(s, rs.getRewardStructItem(i)); } - if (dmin < 0) { + /*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)); - } + }*/ // add to state rewards stateRewards[j] = JDD.Plus(stateRewards[j], item); } @@ -2160,12 +2160,12 @@ private void computeRewards(SystemDDs sysDDs) throws PrismException s += "\nIf this is the case, try strengthening the predicate."; throw new PrismLangException(s, rs.getRewardStructItem(i)); } - if (dmin < 0) { + /*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)); - } + }*/ // add result to rewards compDDs.rewards[j] = JDD.Plus(compDDs.rewards[j], item); } diff --git a/prism/src/symbolic/comp/NondetModelChecker.java b/prism/src/symbolic/comp/NondetModelChecker.java index 356f312a0..434a791e9 100644 --- a/prism/src/symbolic/comp/NondetModelChecker.java +++ b/prism/src/symbolic/comp/NondetModelChecker.java @@ -343,7 +343,9 @@ protected StateValues checkExpressionReward(ExpressionReward expr, boolean forAl // Get rewards Object rs = expr.getRewardStructIndex(); JDDNode stateRewards = getStateRewardsByIndexObject(rs, model, constantValues); + checkNegativeRewards(stateRewards, "State"); JDDNode transRewards = getTransitionRewardsByIndexObject(rs, model, constantValues); + checkNegativeRewards(transRewards, "Transition"); // Compute rewards StateValues rewards = null; @@ -791,7 +793,9 @@ protected void extractInfoFromMultiObjectiveOperand(ExpressionQuant exprQuant, O throw new PrismNotSupportedException("Multi-objective model checking does not support state rewards; please convert to transition rewards"); } // Add transition rewards to list - transRewardsList.add(getTransitionRewardsByIndexObject(rs, model, constantValues)); + JDDNode transRewards = getTransitionRewardsByIndexObject(rs, model, constantValues); + checkNegativeRewards(transRewards, "Transition"); + transRewardsList.add(transRewards); } // Check that the temporal/reward operator is supported, and store step bounds if present diff --git a/prism/src/symbolic/comp/ProbModelChecker.java b/prism/src/symbolic/comp/ProbModelChecker.java index 9f37e4efa..fa2d642eb 100644 --- a/prism/src/symbolic/comp/ProbModelChecker.java +++ b/prism/src/symbolic/comp/ProbModelChecker.java @@ -251,7 +251,9 @@ protected StateValues checkExpressionReward(ExpressionReward expr, JDDNode state // Get rewards Object rs = expr.getRewardStructIndex(); JDDNode stateRewards = getStateRewardsByIndexObject(rs, model, constantValues); + checkNegativeRewards(stateRewards, "State"); JDDNode transRewards = getTransitionRewardsByIndexObject(rs, model, constantValues); + checkNegativeRewards(transRewards, "Transition"); // Print a warning if Rmin/Rmax used if (opInfo.getRelOp() == RelOp.MIN || opInfo.getRelOp() == RelOp.MAX) { diff --git a/prism/src/symbolic/comp/StateModelChecker.java b/prism/src/symbolic/comp/StateModelChecker.java index 6cc906ca0..0059e2604 100644 --- a/prism/src/symbolic/comp/StateModelChecker.java +++ b/prism/src/symbolic/comp/StateModelChecker.java @@ -1657,6 +1657,20 @@ public JDDNode getTransitionRewardsByIndexObject(Object rs, Model model, Values return transRewards; } + /** + * Check that rewards contained in an MTBDD are non-negative. + * Throws an exception (with explanatory message) if negative rewards are found. + * @param rewards The rewards MTBDD to check + * @param rewardType A string describing the type of rewards: "State" or "Transition" + */ + public void checkNegativeRewards(JDDNode rewards, String rewardType) throws PrismException + { + double rmin = JDD.FindMin(rewards); + if (rmin < 0) { + throw new PrismException(rewardType + " rewards are negative (" + rmin + ") for some states"); + } + } + @Override public Values getConstantValues() {