From 28b741819df40ccb7ffd9be25dc6b1464b6376ff Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Sun, 5 Feb 2017 23:42:46 +0000
Subject: [PATCH] Optimise computation of expected instantaenous rewards
 (R[I=k]) for DTMCs when the value is only required for one state (explicit
 engine).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11975 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/explicit/DTMCModelChecker.java | 39 ++++++++++++++++++++++--
 prism/src/explicit/ProbModelChecker.java | 11 +++----
 2 files changed, 41 insertions(+), 9 deletions(-)

diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java
index cf068750..7eeed4e2 100644
--- a/prism/src/explicit/DTMCModelChecker.java
+++ b/prism/src/explicit/DTMCModelChecker.java
@@ -201,13 +201,21 @@ public class DTMCModelChecker extends ProbModelChecker
 		return rewards;
 	}
 	
-	public ModelCheckerResult computeInstantaneousRewards(DTMC dtmc, MCRewards mcRewards, double t) throws PrismException
+	public ModelCheckerResult computeInstantaneousRewards(DTMC dtmc, MCRewards mcRewards, int k, BitSet statesOfInterest) throws PrismException
+	{
+		if (statesOfInterest.cardinality() == 1) {
+			return computeInstantaneousRewardsForwards(dtmc, mcRewards, k, statesOfInterest.nextSetBit(0));
+		} else {
+			return computeInstantaneousRewardsBackwards(dtmc, mcRewards, k);
+		}
+	}
+	
+	public ModelCheckerResult computeInstantaneousRewardsBackwards(DTMC dtmc, MCRewards mcRewards, int k) throws PrismException
 	{
 		ModelCheckerResult res = null;
 		int i, n, iters;
 		double soln[], soln2[], tmpsoln[];
 		long timer;
-		int right = (int) t;
 
 		// Store num states
 		n = dtmc.getNumStates();
@@ -225,7 +233,7 @@ public class DTMCModelChecker extends ProbModelChecker
 			soln[i] = mcRewards.getStateReward(i);
 
 		// Start iterations
-		for (iters = 0; iters < right; iters++) {
+		for (iters = 0; iters < k; iters++) {
 			// Matrix-vector multiply
 			dtmc.mvMult(soln, soln2, null, false);
 			// Swap vectors for next iter
@@ -249,6 +257,31 @@ public class DTMCModelChecker extends ProbModelChecker
 		return res;
 	}
 
+	public ModelCheckerResult computeInstantaneousRewardsForwards(DTMC dtmc, MCRewards mcRewards, int k, int stateOfInterest) throws PrismException
+	{
+		// Build a point probability distribution for the required state  
+		double[] initDist = new double[dtmc.getNumStates()];
+		initDist[stateOfInterest] = 1.0;
+		
+		// Compute (forward) transient probabilities
+		ModelCheckerResult res = computeTransientProbs(dtmc, k, initDist);
+		
+		// Compute expected value (from initial state)
+		int n = dtmc.getNumStates();
+		double avg = 0.0;
+		for (int i = 0; i < n; i++) {
+			avg += res.soln[i] *= mcRewards.getStateReward(i);
+		}
+
+		// Reuse vector/result storage
+		for (int i = 0; i < n; i++) {
+			res.soln[i] = 0.0;
+		}
+		res.soln[stateOfInterest] = avg;
+		
+		return res;
+	}
+	
 	public ModelCheckerResult computeCumulativeRewards(DTMC dtmc, MCRewards mcRewards, double t) throws PrismException
 	{
 		ModelCheckerResult res = null;
diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java
index 4ed031a4..23026ac9 100644
--- a/prism/src/explicit/ProbModelChecker.java
+++ b/prism/src/explicit/ProbModelChecker.java
@@ -954,7 +954,7 @@ public class ProbModelChecker extends NonProbModelChecker
 			ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
 			switch (exprTemp.getOperator()) {
 			case ExpressionTemporal.R_I:
-				rewards = checkRewardInstantaneous(model, modelRewards, exprTemp, minMax);
+				rewards = checkRewardInstantaneous(model, modelRewards, exprTemp, minMax, statesOfInterest);
 				break;
 			case ExpressionTemporal.R_C:
 				if (exprTemp.hasBounds()) {
@@ -979,18 +979,17 @@ public class ProbModelChecker extends NonProbModelChecker
 	/**
 	 * Compute rewards for an instantaneous reward operator.
 	 */
-	protected StateValues checkRewardInstantaneous(Model model, Rewards modelRewards, ExpressionTemporal expr, MinMax minMax) throws PrismException
+	protected StateValues checkRewardInstantaneous(Model model, Rewards modelRewards, ExpressionTemporal expr, MinMax minMax, BitSet statesOfInterest) throws PrismException
 	{
-		// Get time bound
-		double t = expr.getUpperBound().evaluateDouble(constantValues);
-
 		// Compute/return the rewards
 		ModelCheckerResult res = null;
 		switch (model.getModelType()) {
 		case DTMC:
-			res = ((DTMCModelChecker) this).computeInstantaneousRewards((DTMC) model, (MCRewards) modelRewards, t);
+			int k = expr.getUpperBound().evaluateInt(constantValues);
+			res = ((DTMCModelChecker) this).computeInstantaneousRewards((DTMC) model, (MCRewards) modelRewards, k, statesOfInterest);
 			break;
 		case CTMC:
+			double t = expr.getUpperBound().evaluateDouble(constantValues);
 			res = ((CTMCModelChecker) this).computeInstantaneousRewards((CTMC) model, (MCRewards) modelRewards, t);
 			break;
 		default: