From a025ae2e075060f665aab9f36708ea905be6a3db Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Sun, 13 Dec 2015 00:18:41 +0000
Subject: [PATCH] Add model checking of R[C] operator for CTMCs.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11041 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/explicit/CTMCModelChecker.java | 22 +++++++++++++++
 prism/src/explicit/ProbModelChecker.java |  1 +
 prism/src/prism/StochModelChecker.java   | 35 +++++++++++++++++++++++-
 3 files changed, 57 insertions(+), 1 deletion(-)

diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java
index 11d8e36b..639558fe 100644
--- a/prism/src/explicit/CTMCModelChecker.java
+++ b/prism/src/explicit/CTMCModelChecker.java
@@ -560,6 +560,28 @@ public class CTMCModelChecker extends ProbModelChecker
 		return res;
 	}
 
+	/**
+	 * Compute expected total rewards.
+	 * @param ctmc The CTMC
+	 * @param mcRewards The rewards
+	 * @param target Target states
+	 */
+	public ModelCheckerResult computeTotalRewards(CTMC ctmc, MCRewards mcRewards) throws PrismException
+	{
+		int i, n;
+		// Build embedded DTMC
+		mainLog.println("Building embedded DTMC...");
+		DTMC dtmcEmb = ctmc.getImplicitEmbeddedDTMC();
+		// Convert rewards
+		n = ctmc.getNumStates();
+		StateRewardsArray rewEmb = new StateRewardsArray(n);
+		for (i = 0; i < n; i++) {
+			rewEmb.setStateReward(i, mcRewards.getStateReward(i) / ctmc.getExitRate(i));
+		}
+		// Do computation on DTMC
+		return createDTMCModelChecker().computeTotalRewards(dtmcEmb, rewEmb);
+	}
+
 	/**
 	 * Perform instantaneous reward computation.
 	 * Compute, for each state of {@ctmc}, the expected rewards at time {@code t}
diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java
index a5492480..da30ec0f 100644
--- a/prism/src/explicit/ProbModelChecker.java
+++ b/prism/src/explicit/ProbModelChecker.java
@@ -1021,6 +1021,7 @@ public class ProbModelChecker extends NonProbModelChecker
 			res = ((DTMCModelChecker) this).computeTotalRewards((DTMC) model, (MCRewards) modelRewards);
 			break;
 		case CTMC:
+			res = ((CTMCModelChecker) this).computeTotalRewards((CTMC) model, (MCRewards) modelRewards);
 			break;
 		case MDP:
 			break;
diff --git a/prism/src/prism/StochModelChecker.java b/prism/src/prism/StochModelChecker.java
index a2e4ac01..66af2465 100644
--- a/prism/src/prism/StochModelChecker.java
+++ b/prism/src/prism/StochModelChecker.java
@@ -553,6 +553,39 @@ public class StochModelChecker extends ProbModelChecker
 		return rewards;
 	}
 
+	// compute total rewards
+
+	protected StateValues computeTotalRewards(JDDNode tr, JDDNode tr01, JDDNode sr, JDDNode trr) throws PrismException
+	{
+		JDDNode diags, emb, srNew;
+		StateValues rewards = null;
+
+		// Compute embedded Markov chain
+		JDD.Ref(tr);
+		diags = JDD.SumAbstract(tr, allDDColVars);
+		JDD.Ref(tr);
+		JDD.Ref(diags);
+		emb = JDD.Apply(JDD.DIVIDE, trans, diags);
+		mainLog.println("\nDiagonals vector: " + JDD.GetInfoString(diags, allDDRowVars.n()));
+		mainLog.println("Embedded Markov chain: " + JDD.GetInfoString(emb, allDDRowVars.n() * 2));
+
+		// Convert rewards
+		JDD.Ref(sr);
+		JDD.Ref(diags);
+		srNew = JDD.Apply(JDD.DIVIDE, sr, diags);
+
+		// And then use superclass (ProbModelChecker)
+		// to compute rewards
+		rewards = super.computeTotalRewards(emb, tr01, srNew, trr);
+
+		// derefs
+		JDD.Deref(diags);
+		JDD.Deref(emb);
+		JDD.Deref(srNew);
+
+		return rewards;
+	}
+	
 	// compute rewards for reach reward
 
 	protected StateValues computeReachRewards(JDDNode tr, JDDNode tr01, JDDNode sr, JDDNode trr, JDDNode b)
@@ -576,7 +609,7 @@ public class StochModelChecker extends ProbModelChecker
 		srNew = JDD.Apply(JDD.DIVIDE, sr, diags);
 
 		// And then use superclass (ProbModelChecker)
-		// to compute probabilities
+		// to compute rewards
 		rewards = super.computeReachRewards(emb, tr01, srNew, trr, b);
 
 		// derefs