imported patch ex-dtmc-weights-rewards-has-positive-negative.patch

prism/src/explicit/DTMCModelChecker.java

@@ -1413,6 +1413,18 @@ public class DTMCModelChecker extends ProbModelChecker
 				{
 					return false;
 				}
+
+				@Override
+				public boolean hasPositiveRewards()
+				{
+					return true;
+				}
+
+				@Override
+				public boolean hasNegativeRewards()
+				{
+					return false;
+				}
 			};
 			upperBound = DijkstraSweepMPI.computeUpperBound(this, mdp, mdpRewards, target, unknown);
 			method = "Dijkstra Sweep MPI";

prism/src/explicit/ZeroRewardECQuotient.java

@@ -165,6 +165,18 @@ public class ZeroRewardECQuotient
 			{
 				return rewards.hasTransitionRewards();
 			}
+
+			@Override
+			public boolean hasPositiveRewards()
+			{
+				return rewards.hasPositiveRewards();
+			}
+
+			@Override
+			public boolean hasNegativeRewards()
+			{
+				return rewards.hasNegativeRewards();
+			}
 		};
 
 		if (debug) {

prism/src/explicit/rewards/MCRewardsFromMDPRewards.java

@@ -71,4 +71,17 @@ public class MCRewardsFromMDPRewards implements MCRewards
 		// only state rewards
 		return false;
 	}
+
+	@Override
+	public boolean hasPositiveRewards()
+	{
+		return mdpRewards.hasPositiveRewards();
+	}
+
+	@Override
+	public boolean hasNegativeRewards()
+	{
+		return mdpRewards.hasNegativeRewards();
+	}
+
 }

prism/src/explicit/rewards/MDPRewardsSimple.java

@@ -45,6 +45,11 @@ public class MDPRewardsSimple implements MDPRewards
 	/** Transition rewards */
 	protected List<List<Double>> transRewards;
 
+	/** Flag: has positive rewards */
+	protected boolean hasPositiveRewards = false;
+	/** Flag: has negative rewards */
+	protected boolean hasNegativeRewards = false;
+
 	/**
 	 * Constructor: all zero rewards.
 	 * @param numStates Number of states
@@ -90,6 +95,8 @@ public class MDPRewardsSimple implements MDPRewards
 				}
 			}
 		}
+		this.hasPositiveRewards = rews.hasPositiveRewards;
+		this.hasNegativeRewards = rews.hasNegativeRewards;
 	}
 
 	// Mutators
@@ -107,6 +114,7 @@ public class MDPRewardsSimple implements MDPRewards
 		}
 		// Set reward
 		stateRewards.set(s, r);
+		updateFlags(r);
 	}
 
 	/**
@@ -145,6 +153,7 @@ public class MDPRewardsSimple implements MDPRewards
 		}
 		// Set reward
 		list.set(i, r);
+		updateFlags(r);
 	}
 
 	/**
@@ -165,6 +174,19 @@ public class MDPRewardsSimple implements MDPRewards
 			transRewards.set(s, null);
 		}
 	}
+	
+	/**
+	 * Update the flags for positive / negative rewards by taking
+	 * value r into account.
+	 */
+	protected void updateFlags(double r)
+	{
+		if (r > 0) {
+			hasPositiveRewards = true;
+		} else if (r < 0) {
+			hasNegativeRewards = true;
+		}
+	}
 
 	// Accessors
 
@@ -225,4 +247,17 @@ public class MDPRewardsSimple implements MDPRewards
 	{
 		return transRewards != null;
 	}
+
+	@Override
+	public boolean hasPositiveRewards()
+	{
+		return hasPositiveRewards;
+	}
+
+	@Override
+	public boolean hasNegativeRewards()
+	{
+		return hasNegativeRewards;
+	}
+
 }

prism/src/explicit/rewards/Rewards.java

@@ -43,4 +43,23 @@ public interface Rewards
 
 	/** Returns true if this reward structure has transition rewards */
 	public boolean hasTransitionRewards();
+
+	/**
+	 * Returns true if this reward structure has positive (>0) rewards.
+	 * <br>
+	 * Note: This information is best-effort. E.g., a reward structure that
+	 * contained a positive reward at some time, which was later on overwritten
+	 * may still return true.
+	 */
+	public boolean hasPositiveRewards();
+
+	/**
+	 * Returns true if this reward structure has negative (&lt;0) rewards.
+	 * <br>
+	 * Note: This information is best-effort. E.g., a reward structure that
+	 * contained a positive reward at some time, which was later on overwritten
+	 * may still return true.
+	 */
+	public boolean hasNegativeRewards();
+
 }

prism/src/explicit/rewards/STPGRewardsSimple.java

@@ -108,6 +108,7 @@ public class STPGRewardsSimple extends MDPRewardsSimple implements STPGRewards
 		}
 		// Set reward
 		list2.set(j, r);
+		updateFlags(r);
 	}
 
 	/**

prism/src/explicit/rewards/StateRewardsArray.java

@@ -37,6 +37,11 @@ public class StateRewardsArray extends StateRewards
 	/** Array of state rewards **/
 	protected double stateRewards[] = null;
 	
+	/** Flag: has positive rewards */
+	protected boolean hasPositiveRewards = false;
+	/** Flag: has negative rewards */
+	protected boolean hasNegativeRewards = false;
+	
 	/**
 	 * Constructor: all zero rewards.
 	 * @param numStates Number of states
@@ -60,6 +65,8 @@ public class StateRewardsArray extends StateRewards
 		for (int i = 0; i < numStates; i++) {
 			stateRewards[i] = rews.stateRewards[i];
 		}
+		hasPositiveRewards = rews.hasPositiveRewards;
+		hasNegativeRewards = rews.hasNegativeRewards;
 	}
 
 	// Mutators
@@ -70,6 +77,7 @@ public class StateRewardsArray extends StateRewards
 	public void setStateReward(int s, double r)
 	{
 		stateRewards[s] = r;
+		updateFlags(r);
 	}
 	
 	/**
@@ -77,9 +85,24 @@ public class StateRewardsArray extends StateRewards
 	 */
 	public void addToStateReward(int s, double r)
 	{
-		stateRewards[s] += r;
+		double v;
+		v = stateRewards[s] += r;
+		updateFlags(v);
 	}
-	
+
+	/**
+	 * Update the flags for positive / negative rewards by taking
+	 * value r into account.
+	 */
+	private void updateFlags(double r)
+	{
+		if (r > 0) {
+			hasPositiveRewards = true;
+		} else if (r < 0) {
+			hasNegativeRewards = true;
+		}
+	}
+
 	// Accessors
 	
 	@Override
@@ -87,7 +110,19 @@ public class StateRewardsArray extends StateRewards
 	{
 		return stateRewards[s];
 	}
-	
+
+	@Override
+	public boolean hasPositiveRewards()
+	{
+		return hasPositiveRewards;
+	}
+
+	@Override
+	public boolean hasNegativeRewards()
+	{
+		return hasNegativeRewards;
+	}
+
 	// Converters
 	
 	@Override

prism/src/explicit/rewards/StateRewardsConstant.java

@@ -67,4 +67,16 @@ public class StateRewardsConstant extends StateRewards
 	{
 		return new StateRewardsConstant(stateReward);
 	}
+
+	@Override
+	public boolean hasPositiveRewards()
+	{
+		return stateReward > 0;
+	}
+
+	@Override
+	public boolean hasNegativeRewards()
+	{
+		return stateReward < 0;
+	}
 }

prism/src/explicit/rewards/StateRewardsSimple.java

@@ -39,6 +39,11 @@ public class StateRewardsSimple extends StateRewards
 	/** Arraylist of state rewards **/
 	protected ArrayList<Double> stateRewards;
 
+	/** Flag: has positive rewards */
+	protected boolean hasPositiveRewards = false;
+	/** Flag: has negative rewards */
+	protected boolean hasNegativeRewards = false;
+
 	/**
 	 * Constructor: all zero rewards.
 	 */
@@ -62,6 +67,8 @@ public class StateRewardsSimple extends StateRewards
 				stateRewards.add(rews.stateRewards.get(i));
 			}
 		}
+		hasPositiveRewards = rews.hasPositiveRewards;
+		hasNegativeRewards = rews.hasNegativeRewards;
 	}
 
 	// Mutators
@@ -82,6 +89,20 @@ public class StateRewardsSimple extends StateRewards
 		}
 		// Set reward
 		stateRewards.set(s, r);
+		updateFlags(r);
+	}
+
+	/**
+	 * Update the flags for positive / negative rewards by taking
+	 * value r into account.
+	 */
+	private void updateFlags(double r)
+	{
+		if (r > 0) {
+			hasPositiveRewards = true;
+		} else if (r < 0) {
+			hasNegativeRewards = true;
+		}
 	}
 
 	// Accessors
@@ -96,6 +117,18 @@ public class StateRewardsSimple extends StateRewards
 		}
 	}
 
+	@Override
+	public boolean hasPositiveRewards()
+	{
+		return hasPositiveRewards;
+	}
+
+	@Override
+	public boolean hasNegativeRewards()
+	{
+		return hasNegativeRewards;
+	}
+
 	// Converters
 	
 	@Override