From 21d663816acf1dd50c194e15a4c2d4a1951bb1d4 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 17 Jul 2015 09:45:17 +0000
Subject: [PATCH] Push lifting of (explicit) reward structures into Reward
 classes.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10354 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/explicit/MDPModelChecker.java       |  2 +-
 prism/src/explicit/Product.java               | 34 -------------------
 prism/src/explicit/rewards/MCRewards.java     |  6 ++++
 .../rewards/MCRewardsFromMDPRewards.java      |  9 +++++
 prism/src/explicit/rewards/MDPRewards.java    | 10 ++++--
 .../explicit/rewards/MDPRewardsSimple.java    | 28 +++++++++++++++
 prism/src/explicit/rewards/Rewards.java       | 11 ++++--
 prism/src/explicit/rewards/StateRewards.java  |  6 ++++
 .../explicit/rewards/StateRewardsArray.java   | 15 ++++++++
 .../rewards/StateRewardsConstant.java         | 11 ++++++
 .../explicit/rewards/StateRewardsSimple.java  | 17 ++++++++++
 11 files changed, 110 insertions(+), 39 deletions(-)

diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java
index e8805dab..dde93e79 100644
--- a/prism/src/explicit/MDPModelChecker.java
+++ b/prism/src/explicit/MDPModelChecker.java
@@ -158,7 +158,7 @@ public class MDPModelChecker extends ProbModelChecker
 		product = mcLtl.constructProductMDP(this, (MDP)model, expr, statesOfInterest, allowedAcceptance);
 		
 		// Adapt reward info to product model
-		productRewards = product.liftFromModel((MDPRewards) modelRewards);
+		productRewards = ((MDPRewards) modelRewards).liftFromModel(product);
 		
 		// Output product, if required
 		if (getExportProductTrans()) {
diff --git a/prism/src/explicit/Product.java b/prism/src/explicit/Product.java
index 74aac87e..b595d98a 100644
--- a/prism/src/explicit/Product.java
+++ b/prism/src/explicit/Product.java
@@ -29,9 +29,6 @@ package explicit;
 
 import java.util.BitSet;
 
-import explicit.rewards.MDPRewards;
-import explicit.rewards.MDPRewardsSimple;
-import explicit.rewards.StateRewardsConstant;
 import parser.type.TypeBool;
 import parser.type.TypeDouble;
 import parser.type.TypeInt;
@@ -145,37 +142,6 @@ public abstract class Product<M extends Model> implements ModelTransformation<M,
 		return result;
 	}
 
-	/**
-	 * Lifts an MDP reward structure over states in the original model to one
-	 * over states in the product model: The rewards for a product state are
-	 * copied from those the parameter for the corresponding original model state.
-	 * It is assumed that the original model in the product was an MDP.
-	 * It is also assume that nondeterministic choices in each state of the product
-	 * are ordered in the same way as in the original model.
-	 * @param mdpRewards an MDPRewards over states of the original model for this product.
-	 */
-	public MDPRewards liftFromModel(MDPRewards mdpRewards)
-	{	
-		MDP productMDP = (MDP)productModel;
-		// Special case: constant state rewards
-		if (mdpRewards instanceof StateRewardsConstant) {
-			return ((StateRewardsConstant) mdpRewards).deepCopy();
-		}
-		// Normal: state and transition rewards
-		else {
-			int numStates = productMDP.getNumStates();
-			MDPRewardsSimple rewSimple = new MDPRewardsSimple(numStates);
-			for (int productState = 0; productState < numStates; productState++) {
-				rewSimple.setStateReward(productState, mdpRewards.getStateReward(getModelState(productState)));
-				int numChoices = productMDP.getNumChoices(productState);
-				for (int i = 0; i < numChoices; i++) {
-					rewSimple.setTransitionReward(productState, i, mdpRewards.getTransitionReward(getModelState(productState), i));
-				}
-			}
-			return rewSimple;
-		}
-	}
-	
 	/**
 	 * Project state values from the product model back to the original model. This function
 	 * assumes that the product model has at most one initial state per state in the original
diff --git a/prism/src/explicit/rewards/MCRewards.java b/prism/src/explicit/rewards/MCRewards.java
index 8d22a546..2b24f03d 100644
--- a/prism/src/explicit/rewards/MCRewards.java
+++ b/prism/src/explicit/rewards/MCRewards.java
@@ -26,6 +26,9 @@
 
 package explicit.rewards;
 
+import explicit.Model;
+import explicit.Product;
+
 /**
  * Classes that provide (read) access to explicit-state rewards for a Markov chain (DTMC/CTMC).
  */
@@ -35,4 +38,7 @@ public interface MCRewards extends Rewards
 	 * Get the state reward for state {@code s}.
 	 */
 	public abstract double getStateReward(int s); 
+
+	@Override
+	public MCRewards liftFromModel(Product<? extends Model> product);
 }
diff --git a/prism/src/explicit/rewards/MCRewardsFromMDPRewards.java b/prism/src/explicit/rewards/MCRewardsFromMDPRewards.java
index 0519e8e8..3ed4642c 100644
--- a/prism/src/explicit/rewards/MCRewardsFromMDPRewards.java
+++ b/prism/src/explicit/rewards/MCRewardsFromMDPRewards.java
@@ -26,6 +26,9 @@
 
 package explicit.rewards;
 
+import explicit.Model;
+import explicit.Product;
+
 
 /**
  * Explicit-state representation of a DTMC rewards structure, constructed (implicitly)
@@ -55,4 +58,10 @@ public class MCRewardsFromMDPRewards implements MCRewards
 		// This works fine for cumulative rewards, but not instantaneous ones
 		return mdpRewards.getStateReward(s) + mdpRewards.getTransitionReward(s, strat[s]);
 	}
+	
+	@Override
+	public MCRewards liftFromModel(Product<? extends Model> product)
+	{
+		throw new UnsupportedOperationException();
+	}
 }
diff --git a/prism/src/explicit/rewards/MDPRewards.java b/prism/src/explicit/rewards/MDPRewards.java
index c7bbfbe5..bf246c11 100644
--- a/prism/src/explicit/rewards/MDPRewards.java
+++ b/prism/src/explicit/rewards/MDPRewards.java
@@ -26,6 +26,9 @@
 
 package explicit.rewards;
 
+import explicit.Model;
+import explicit.Product;
+
 /**
  * Classes that provide (read) access to explicit-state rewards for an MDP.
  */
@@ -35,9 +38,12 @@ public interface MDPRewards 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);
+
+	@Override
+	public MDPRewards liftFromModel(Product<? extends Model> product);
 }
diff --git a/prism/src/explicit/rewards/MDPRewardsSimple.java b/prism/src/explicit/rewards/MDPRewardsSimple.java
index 60010f95..a4c13578 100644
--- a/prism/src/explicit/rewards/MDPRewardsSimple.java
+++ b/prism/src/explicit/rewards/MDPRewardsSimple.java
@@ -29,6 +29,10 @@ package explicit.rewards;
 import java.util.ArrayList;
 import java.util.List;
 
+import explicit.Model;
+import explicit.NondetModel;
+import explicit.Product;
+
 /**
  * Simple explicit-state storage of rewards for an MDP.
  * Like the related class MDPSimple, this is not especially efficient, but mutable (in terms of size).
@@ -184,6 +188,30 @@ public class MDPRewardsSimple implements MDPRewards
 		return list.get(i);
 	}
 
+	// Converters
+	
+	@Override
+	public MDPRewards liftFromModel(Product<? extends Model> product)
+	{
+		Model modelProd = product.getProductModel();
+		int numStatesProd = modelProd.getNumStates();		
+		MDPRewardsSimple rewardsProd = new MDPRewardsSimple(numStatesProd);
+		if (stateRewards != null) {
+			for (int s = 0; s < numStatesProd; s++) {
+				rewardsProd.setStateReward(s, stateRewards.get(product.getModelState(s)));
+			}
+		}
+		if (transRewards != null) {
+			for (int s = 0; s < numStatesProd; s++) {
+				int numChoices = transRewards.get(s).size();
+				for (int i = 0; i < numChoices; i++) {
+					rewardsProd.setTransitionReward(s, i, transRewards.get(product.getModelState(s)).get(i));
+				}
+			}
+		}
+		return rewardsProd;
+	}
+	
 	@Override
 	public String toString()
 	{
diff --git a/prism/src/explicit/rewards/Rewards.java b/prism/src/explicit/rewards/Rewards.java
index 8083d460..06c35a05 100644
--- a/prism/src/explicit/rewards/Rewards.java
+++ b/prism/src/explicit/rewards/Rewards.java
@@ -27,10 +27,17 @@
 
 package explicit.rewards;
 
+import explicit.Model;
+import explicit.Product;
+
 /**
- * A dummy interface implemented by all reward classes.
+ * Interface implemented by all reward classes.
  */
 public interface Rewards
 {
-
+	/**
+	 * Create a new reward structure that lifts this one such that it is defined over states of a
+	 * model that is a product of the one that this reward structure is defined over. 
+	 */
+	public Rewards liftFromModel(Product<? extends Model> product);
 }
diff --git a/prism/src/explicit/rewards/StateRewards.java b/prism/src/explicit/rewards/StateRewards.java
index afeef6a6..8f10aa9b 100644
--- a/prism/src/explicit/rewards/StateRewards.java
+++ b/prism/src/explicit/rewards/StateRewards.java
@@ -26,6 +26,9 @@
 
 package explicit.rewards;
 
+import explicit.Model;
+import explicit.Product;
+
 /**
  * Explicit-state storage of just state rewards.
  */
@@ -54,6 +57,9 @@ public abstract class StateRewards implements MCRewards, MDPRewards, STPGRewards
 		return deepCopy();
 	}
 	
+	@Override
+	public abstract StateRewards liftFromModel(Product<? extends Model> product);
+	
 	/**
 	 * Perform a deep copy.
 	 */
diff --git a/prism/src/explicit/rewards/StateRewardsArray.java b/prism/src/explicit/rewards/StateRewardsArray.java
index 66388468..bc360788 100644
--- a/prism/src/explicit/rewards/StateRewardsArray.java
+++ b/prism/src/explicit/rewards/StateRewardsArray.java
@@ -27,6 +27,7 @@
 package explicit.rewards;
 
 import explicit.Model;
+import explicit.Product;
 
 /**
  * Explicit-state storage of just state rewards (as an array).
@@ -87,6 +88,20 @@ public class StateRewardsArray extends StateRewards
 		return stateRewards[s];
 	}
 	
+	// Converters
+	
+	@Override
+	public StateRewards liftFromModel(Product<? extends Model> product)
+	{
+		Model modelProd = product.getProductModel();
+		int numStatesProd = modelProd.getNumStates();
+		StateRewardsArray rewardsProd = new StateRewardsArray(numStatesProd);
+		for (int s = 0; s < numStatesProd; s++) {
+			rewardsProd.setStateReward(s, stateRewards[product.getModelState(s)]);
+		}
+		return rewardsProd;
+	}
+	
 	// Other
 
 	@Override
diff --git a/prism/src/explicit/rewards/StateRewardsConstant.java b/prism/src/explicit/rewards/StateRewardsConstant.java
index 4de39530..76fee3b5 100644
--- a/prism/src/explicit/rewards/StateRewardsConstant.java
+++ b/prism/src/explicit/rewards/StateRewardsConstant.java
@@ -26,6 +26,9 @@
 
 package explicit.rewards;
 
+import explicit.Model;
+import explicit.Product;
+
 /**
  * Explicit-state storage of constant state rewards.
  */
@@ -49,6 +52,14 @@ public class StateRewardsConstant extends StateRewards
 		return stateReward;
 	}
 
+	// Converters
+	
+	@Override
+	public StateRewards liftFromModel(Product<? extends Model> product)
+	{
+		return deepCopy();
+	}
+	
 	// Other
 
 	@Override
diff --git a/prism/src/explicit/rewards/StateRewardsSimple.java b/prism/src/explicit/rewards/StateRewardsSimple.java
index 28a34e64..5d3d7739 100644
--- a/prism/src/explicit/rewards/StateRewardsSimple.java
+++ b/prism/src/explicit/rewards/StateRewardsSimple.java
@@ -28,6 +28,9 @@ package explicit.rewards;
 
 import java.util.ArrayList;
 
+import explicit.Model;
+import explicit.Product;
+
 /**
  * Explicit-state storage of just state rewards (mutable).
  */
@@ -93,6 +96,20 @@ public class StateRewardsSimple extends StateRewards
 		}
 	}
 
+	// Converters
+	
+	@Override
+	public StateRewards liftFromModel(Product<? extends Model> product)
+	{
+		Model modelProd = product.getProductModel();
+		int numStatesProd = modelProd.getNumStates();
+		StateRewardsSimple rewardsProd = new StateRewardsSimple();
+		for (int s = 0; s < numStatesProd; s++) {
+			rewardsProd.setStateReward(s, getStateReward(product.getModelState(s)));
+		}
+		return rewardsProd;
+	}
+	
 	// Other
 
 	@Override