Allow export (but not model checking) of negative rewards

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

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)

prism/src/explicit/StateModelChecker.java

@@ -1603,7 +1603,7 @@ public <Value> void exportStateRewards(Model<Value> model, int r, File file, Mod
 		}
 
 		try (PrismLog out = getPrismLogForFile(file)) {
-			Rewards<Value> modelRewards = constructRewards(model, r);
+			Rewards<Value> modelRewards = constructRewards(model, r, true);
 			PrismExplicitExporter<Value> exporter = new PrismExplicitExporter<>(exportOptions);
 			exporter.exportStateRewards(model, modelRewards, rewardGen.getRewardStructName(r), out);
 		}
@@ -1623,7 +1623,7 @@ public <Value> void exportTransRewards(Model<Value> model, int r, File file, Mod
 		}
 
 		try (PrismLog out = getPrismLogForFile(file)) {
-			Rewards<Value> modelRewards = constructRewards(model, r);
+			Rewards<Value> modelRewards = constructRewards(model, r, true);
 			PrismExplicitExporter<Value> exporter = new PrismExplicitExporter<>(exportOptions);
 			exporter.exportTransRewards(model, modelRewards, rewardGen.getRewardStructName(r), out);
 		}

prism/src/explicit/rewards/ConstructRewards.java

@@ -201,10 +201,10 @@ private <Value> Value getAndCheckStateReward(int s, RewardGenerator<Value> 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> 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");
 		}

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

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).

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

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

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

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) {

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()
 	{