Aligning with prism-games a bit (explicit reward stuff).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6873 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/rewards/MDPRewardsSimple.java

@@ -41,7 +41,7 @@ public class MDPRewardsSimple implements MDPRewards
 	protected List<Double> stateRewards;
 	/** Transition rewards */
 	protected List<List<Double>> transRewards;
-	
+
 	/**
 	 * Constructor: all zero rewards.
 	 * @param numStates Number of states
@@ -53,9 +53,44 @@ public class MDPRewardsSimple implements MDPRewards
 		stateRewards = null;
 		transRewards = null;
 	}
-	
+
+	/**
+	 * Copy constructor
+	 * @param rews Rewards to copy
+	 */
+	public MDPRewardsSimple(MDPRewardsSimple rews)
+	{
+		numStates = rews.numStates;
+		if (rews.stateRewards == null) {
+			stateRewards = null;
+		} else {
+			stateRewards = new ArrayList<Double>(numStates);
+			for (int i = 0; i < numStates; i++) {
+				stateRewards.add(rews.stateRewards.get(i));
+			}
+		}
+		if (rews.transRewards == null) {
+			transRewards = null;
+		} else {
+			transRewards = new ArrayList<List<Double>>(numStates);
+			for (int i = 0; i < numStates; i++) {
+				List<Double> list = rews.transRewards.get(i);
+				if (list == null) {
+					transRewards.add(null);
+				} else {
+					int n = list.size();
+					List<Double> list2 = new ArrayList<Double>(n);
+					transRewards.add(list2);
+					for (int j = 0; j < n; j++) {
+						list2.add(list.get(j));
+					}
+				}
+			}
+		}
+	}
+
 	// Mutators
-	
+
 	/**
 	 * Set the state reward for state {@code s} to {@code r}.
 	 */
@@ -116,7 +151,7 @@ public class MDPRewardsSimple implements MDPRewards
 	{
 		setTransitionReward(s, i, getTransitionReward(s, i) + r);
 	}
-	
+
 	/**
 	 * Clear all rewards for state s.
 	 */
@@ -127,9 +162,9 @@ public class MDPRewardsSimple implements MDPRewards
 			transRewards.set(s, null);
 		}
 	}
-	
+
 	// Accessors
-	
+
 	@Override
 	public double getStateReward(int s)
 	{
@@ -137,7 +172,7 @@ public class MDPRewardsSimple implements MDPRewards
 			return 0.0;
 		return stateRewards.get(s);
 	}
-	
+
 	@Override
 	public double getTransitionReward(int s, int i)
 	{
@@ -148,7 +183,7 @@ public class MDPRewardsSimple implements MDPRewards
 			return 0.0;
 		return list.get(i);
 	}
-	
+
 	@Override
 	public String toString()
 	{

prism/src/explicit/rewards/STPGRewards.java

@@ -38,14 +38,19 @@ public interface STPGRewards extends Rewards
 	 * Get the state reward for state {@code s}.
 	 */
 	public abstract double getStateReward(int s);
-	
+
 	/**
 	 * Get the transition reward for the {@code i}th choice from state {@code s}.
 	 */
-	public abstract double getTransitionReward(int s, int i); 
-	
+	public abstract double getTransitionReward(int s, int i);
+
 	/**
 	 * Get the transition reward for the {@code i,j}th nested choice from state {@code s}.
 	 */
-	public abstract double getNestedTransitionReward(int s, int i, int j); 
+	public abstract double getNestedTransitionReward(int s, int i, int j);
+
+	/**
+	 * Build an MDPRewards object containing all the same rewards except for the nested ones.
+	 */
+	public abstract MDPRewards buildMDPRewards();
 }

prism/src/explicit/rewards/STPGRewardsSimple.java

@@ -45,7 +45,7 @@ public class STPGRewardsSimple extends MDPRewardsSimple implements STPGRewards
 		// Initially list is just null (denoting all 0)
 		nestedTransRewards = null;
 	}
-	
+
 	// Mutators
 
 	/**
@@ -106,9 +106,9 @@ public class STPGRewardsSimple extends MDPRewardsSimple implements STPGRewards
 			nestedTransRewards.set(s, null);
 		}
 	}
-	
+
 	// Accessors
-	
+
 	@Override
 	public double getNestedTransitionReward(int s, int i, int j)
 	{
@@ -122,7 +122,15 @@ public class STPGRewardsSimple extends MDPRewardsSimple implements STPGRewards
 			return 0.0;
 		return list2.get(j);
 	}
-	
+
+	// Other
+
+	@Override
+	public MDPRewards buildMDPRewards()
+	{
+		return new MDPRewardsSimple(this);
+	}
+
 	@Override
 	public String toString()
 	{

prism/src/explicit/rewards/StateRewards.java

@@ -29,7 +29,7 @@ package explicit.rewards;
 /**
  * Explicit-state storage of just state rewards.
  */
-public abstract class StateRewards implements MCRewards, MDPRewards
+public abstract class StateRewards implements MCRewards, MDPRewards, STPGRewards
 {
 	/**
 	 * Get the state reward for state {@code s}.
@@ -41,4 +41,21 @@ public abstract class StateRewards implements MCRewards, MDPRewards
 	{
 		return 0.0;
 	}
+	
+	@Override
+	public double getNestedTransitionReward(int s, int i, int j)
+	{
+		return 0.0;
+	}
+	
+	@Override
+	public MDPRewards buildMDPRewards()
+	{
+		return deepCopy();
+	}
+	
+	/**
+	 * Perform a deep copy.
+	 */
+	public abstract StateRewards deepCopy();
 }

prism/src/explicit/rewards/StateRewardsConstant.java

@@ -32,7 +32,7 @@ package explicit.rewards;
 public class StateRewardsConstant extends StateRewards
 {
 	protected double stateReward = 0.0;
-	
+
 	/**
 	 * Constructor: all rewards equal to {@code r}
 	 */
@@ -40,12 +40,20 @@ public class StateRewardsConstant extends StateRewards
 	{
 		stateReward = r;
 	}
-	
+
 	// Accessors
-	
+
 	@Override
 	public double getStateReward(int s)
 	{
 		return stateReward;
 	}
+
+	// Other
+
+	@Override
+	public StateRewardsConstant deepCopy()
+	{
+		return new StateRewardsConstant(stateReward);
+	}
 }

prism/src/explicit/rewards/StateRewardsSimple.java

@@ -35,27 +35,40 @@ public class StateRewardsSimple extends StateRewards
 {
 	/** Arraylist of state rewards **/
 	protected ArrayList<Double> stateRewards;
-	
+
 	/**
 	 * Constructor: all zero rewards.
-	 * @param numStates Number of states
 	 */
-	public StateRewardsSimple(int numStates)
+	public StateRewardsSimple()
 	{
-		stateRewards = new ArrayList<Double>(numStates);
-		for (int i = 0; i < numStates; i++)
-			stateRewards.add(0.0);
+		stateRewards = new ArrayList<Double>();
 	}
-	
+
+	/**
+	 * Copy constructor
+	 * @param rews Rewards to copy
+	 */
+	public StateRewardsSimple(StateRewardsSimple rews)
+	{
+		if (rews.stateRewards == null) {
+			stateRewards = null;
+		} else {
+			int n = rews.stateRewards.size();
+			stateRewards = new ArrayList<Double>(n);
+			for (int i = 0; i < n; i++) {
+				stateRewards.add(rews.stateRewards.get(i));
+			}
+		}
+	}
+
 	// Mutators
-	
+
 	/**
 	 * Set the reward for state {@code s} to {@code r}.
 	 */
 	public void setStateReward(int s, double r)
 	{
-		// Nothing to do for zero reward
-		if (r == 0.0)
+		if (r == 0.0 && s >= stateRewards.size())
 			return;
 		// If list not big enough, extend
 		int n = s - stateRewards.size() + 1;
@@ -67,17 +80,24 @@ public class StateRewardsSimple extends StateRewards
 		// Set reward
 		stateRewards.set(s, r);
 	}
-	
+
 	// Accessors
-	
+
 	@Override
 	public double getStateReward(int s)
 	{
 		try {
 			return stateRewards.get(s);
-		}
-		catch (ArrayIndexOutOfBoundsException e) {
+		} catch (ArrayIndexOutOfBoundsException e) {
 			return 0.0;
 		}
 	}
+
+	// Other
+
+	@Override
+	public StateRewardsSimple deepCopy()
+	{
+		return new StateRewardsSimple(this);
+	}
 }