From 1539fc766cd80ab6363e4e8710ea36ef1bd97aab Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 10 Jun 2013 09:21:19 +0000 Subject: [PATCH] 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 --- .../explicit/rewards/MDPRewardsSimple.java | 51 ++++++++++++++++--- prism/src/explicit/rewards/STPGRewards.java | 13 +++-- .../explicit/rewards/STPGRewardsSimple.java | 16 ++++-- prism/src/explicit/rewards/StateRewards.java | 19 ++++++- .../rewards/StateRewardsConstant.java | 14 +++-- .../explicit/rewards/StateRewardsSimple.java | 48 ++++++++++++----- 6 files changed, 127 insertions(+), 34 deletions(-) diff --git a/prism/src/explicit/rewards/MDPRewardsSimple.java b/prism/src/explicit/rewards/MDPRewardsSimple.java index afcdda24..60010f95 100644 --- a/prism/src/explicit/rewards/MDPRewardsSimple.java +++ b/prism/src/explicit/rewards/MDPRewardsSimple.java @@ -41,7 +41,7 @@ public class MDPRewardsSimple implements MDPRewards protected List stateRewards; /** Transition rewards */ protected List> 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(numStates); + for (int i = 0; i < numStates; i++) { + stateRewards.add(rews.stateRewards.get(i)); + } + } + if (rews.transRewards == null) { + transRewards = null; + } else { + transRewards = new ArrayList>(numStates); + for (int i = 0; i < numStates; i++) { + List list = rews.transRewards.get(i); + if (list == null) { + transRewards.add(null); + } else { + int n = list.size(); + List list2 = new ArrayList(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() { diff --git a/prism/src/explicit/rewards/STPGRewards.java b/prism/src/explicit/rewards/STPGRewards.java index 8a06797d..a828c282 100644 --- a/prism/src/explicit/rewards/STPGRewards.java +++ b/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(); } diff --git a/prism/src/explicit/rewards/STPGRewardsSimple.java b/prism/src/explicit/rewards/STPGRewardsSimple.java index 9475475f..cc164645 100644 --- a/prism/src/explicit/rewards/STPGRewardsSimple.java +++ b/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() { diff --git a/prism/src/explicit/rewards/StateRewards.java b/prism/src/explicit/rewards/StateRewards.java index 9e404e38..afeef6a6 100644 --- a/prism/src/explicit/rewards/StateRewards.java +++ b/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(); } diff --git a/prism/src/explicit/rewards/StateRewardsConstant.java b/prism/src/explicit/rewards/StateRewardsConstant.java index d254fdcd..4de39530 100644 --- a/prism/src/explicit/rewards/StateRewardsConstant.java +++ b/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); + } } diff --git a/prism/src/explicit/rewards/StateRewardsSimple.java b/prism/src/explicit/rewards/StateRewardsSimple.java index 4b7a0e93..28a34e64 100644 --- a/prism/src/explicit/rewards/StateRewardsSimple.java +++ b/prism/src/explicit/rewards/StateRewardsSimple.java @@ -35,27 +35,40 @@ public class StateRewardsSimple extends StateRewards { /** Arraylist of state rewards **/ protected ArrayList stateRewards; - + /** * Constructor: all zero rewards. - * @param numStates Number of states */ - public StateRewardsSimple(int numStates) + public StateRewardsSimple() { - stateRewards = new ArrayList(numStates); - for (int i = 0; i < numStates; i++) - stateRewards.add(0.0); + stateRewards = new ArrayList(); } - + + /** + * 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(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); + } }