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

@@ -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}

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;

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