instantaneous and cumulative rewards for explicit engine for dtmcs and ctmcs

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6616 bbc10eb1-c90d-0410-af57-cb519fbb1720
13 years ago · 1f5a901890
2 changed files with 371 additions and 0 deletions
--- a/prism/src/explicit/CTMCModelChecker.java
+++ b/prism/src/explicit/CTMCModelChecker.java
@ -384,6 +384,232 @@ public class CTMCModelChecker extends DTMCModelChecker
 		return res;
 	}

+	/**
+	 * Perform cumulative reward computation.
+	 * Compute, for each state of {@ctmc}, the expected rewards accumulated until {@code t}
+	 * when starting in this state and using reward structure {@code mcRewards}.
+	 * @param ctmc The CTMC
+	 * @param mcRewards The rewards
+	 * @param t Time bound
+	 */
+	@Override
+	public ModelCheckerResult computeCumulativeRewards(DTMC dtmc, MCRewards mcRewards, double t) throws PrismException
+	{
+		ModelCheckerResult res = null;
+		int i, n, iters;
+		double soln[], soln2[], tmpsoln[], sum[];
+		long timer;
+		// Fox-Glynn stuff
+		FoxGlynn fg;
+		int left, right;
+		double q, qt, acc, weights[], totalWeight;
+
+		// Optimisation: If t = 0, this is easy.
+		if (t == 0) {
+			res = new ModelCheckerResult();
+			res.soln = new double[dtmc.getNumStates()];
+			return res;
+		}
+
+		// Start backwards transient computation
+		timer = System.currentTimeMillis();
+		mainLog.println("Starting backwards cumulative rewards computation...");
+
+		CTMC ctmc = (CTMC) dtmc;
+
+		// Store num states
+		n = ctmc.getNumStates();
+
+		// Get uniformisation rate; do Fox-Glynn
+		q = ctmc.getDefaultUniformisationRate();
+		qt = q * t;
+		mainLog.println("\nUniformisation: q.t = " + q + " x " + t + " = " + qt);
+		acc = termCritParam / 8.0;
+		fg = new FoxGlynn(qt, 1e-300, 1e+300, acc);
+		left = fg.getLeftTruncationPoint();
+		right = fg.getRightTruncationPoint();
+		if (right < 0) {
+			throw new PrismException("Overflow in Fox-Glynn computation (time bound too big?)");
+		}
+		weights = fg.getWeights();
+		totalWeight = fg.getTotalWeight();
+		for (i = left; i <= right; i++) {
+			weights[i - left] /= totalWeight;
+		}
+
+		// modify the poisson probabilities to what we need for this computation
+		// first make the kth value equal to the sum of the values for 0...k
+		for (i = left+1; i <= right; i++) {
+			weights[i - left] += weights[i - 1 - left];
+		}
+		// then subtract from 1 and divide by uniformisation constant (q) to give mixed poisson probabilities
+		for (i = left; i <= right; i++) {
+			weights[i - left] = (1 - weights[i - left]) / q;
+		}
+		mainLog.println("Fox-Glynn (" + acc + "): left = " + left + ", right = " + right);
+
+		// Build (implicit) uniformised DTMC
+		dtmc = ctmc.buildImplicitUniformisedDTMC(q);
+
+		// Create solution vector(s)
+		soln = new double[n];
+		soln2 = new double[n];
+
+		// Initialise solution vectors.
+		for (i = 0; i < n; i++)
+			soln[i] = mcRewards.getStateReward(i);
+
+		// do 0th element of summation (doesn't require any matrix powers)
+		sum = new double[n];
+		if (left == 0) {
+			for (i = 0; i < n; i++)
+				sum[i] += weights[0] * soln[i];
+		} else {
+			for (i = 0; i < n; i++)
+				sum[i] += soln[i] / q;
+		}
+
+		// Start iterations
+		iters = 1;
+		while (iters <= right) {
+			// Matrix-vector multiply
+			dtmc.mvMult(soln, soln2, null, false);
+			// Swap vectors for next iter
+			tmpsoln = soln;
+			soln = soln2;
+			soln2 = tmpsoln;
+			// Add to sum
+			if (iters >= left) {
+				for (i = 0; i < n; i++)
+					sum[i] += weights[iters - left] * soln[i];
+			} else {
+				for (i = 0; i < n; i++)
+					sum[i] += soln[i] / q;
+			}
+			iters++;
+		}
+
+		// Finished backwards transient computation
+		timer = System.currentTimeMillis() - timer;
+		mainLog.print("Backwards transient cumulative rewards computation");
+		mainLog.println(" took " + iters + " iters and " + timer / 1000.0 + " seconds.");
+
+		// Return results
+		res = new ModelCheckerResult();
+		res.soln = sum;
+		res.lastSoln = soln2;
+		res.numIters = iters;
+		res.timeTaken = timer / 1000.0;
+		res.timePre = 0.0;
+		return res;
+	}
+
+	/**
+	 * Perform instantaneous reward computation.
+	 * Compute, for each state of {@ctmc}, the expected rewards at time {@code t}
+	 * when starting in this state and using reward structure {@code mcRewards}.
+	 * @param ctmc The CTMC
+	 * @param mcRewards The rewards
+	 * @param t Time bound
+	 */
+	@Override
+	public ModelCheckerResult computeInstantaneousRewards(DTMC dtmc, MCRewards mcRewards, double t) throws PrismException
+	{
+		ModelCheckerResult res = null;
+		int i, n, iters;
+		double soln[], soln2[], tmpsoln[], sum[];
+		long timer;
+		// Fox-Glynn stuff
+		FoxGlynn fg;
+		int left, right;
+		double q, qt, acc, weights[], totalWeight;
+
+		// Store num states
+		n = dtmc.getNumStates();
+
+		// Optimisation: If t = 0, this is easy.
+		if (t == 0) {
+			res = new ModelCheckerResult();
+			res.soln = new double[dtmc.getNumStates()];
+			for (i = 0; i < n; i++)
+				res.soln[i] = mcRewards.getStateReward(i);
+			return res;
+		}
+
+		// Start backwards transient computation
+		timer = System.currentTimeMillis();
+		mainLog.println("Starting backwards instantaneous rewards computation...");
+
+		CTMC ctmc = (CTMC) dtmc;
+
+		// Get uniformisation rate; do Fox-Glynn
+		q = ctmc.getDefaultUniformisationRate();
+		qt = q * t;
+		mainLog.println("\nUniformisation: q.t = " + q + " x " + t + " = " + qt);
+		acc = termCritParam / 8.0;
+		fg = new FoxGlynn(qt, 1e-300, 1e+300, acc);
+		left = fg.getLeftTruncationPoint();
+		right = fg.getRightTruncationPoint();
+		if (right < 0) {
+			throw new PrismException("Overflow in Fox-Glynn computation (time bound too big?)");
+		}
+		weights = fg.getWeights();
+		totalWeight = fg.getTotalWeight();
+		for (i = left; i <= right; i++) {
+			weights[i - left] /= totalWeight;
+		}
+
+		mainLog.println("Fox-Glynn (" + acc + "): left = " + left + ", right = " + right);
+
+		// Build (implicit) uniformised DTMC
+		dtmc = ctmc.buildImplicitUniformisedDTMC(q);
+
+		// Create solution vector(s)
+		soln = new double[n];
+		soln2 = new double[n];
+
+		// Initialise solution vectors.
+		for (i = 0; i < n; i++)
+			soln[i] = mcRewards.getStateReward(i);
+
+		// do 0th element of summation (doesn't require any matrix powers)
+		sum = new double[n];
+		if (left == 0)
+			for (i = 0; i < n; i++)
+				sum[i] += weights[0] * soln[i];
+
+		// Start iterations
+		iters = 1;
+		while (iters <= right) {
+			// Matrix-vector multiply
+			dtmc.mvMult(soln, soln2, null, false);
+			// Swap vectors for next iter
+			tmpsoln = soln;
+			soln = soln2;
+			soln2 = tmpsoln;
+			// Add to sum
+			if (iters >= left) {
+				for (i = 0; i < n; i++)
+					sum[i] += weights[iters - left] * soln[i];
+			}
+			iters++;
+		}
+
+		// Finished backwards transient computation
+		timer = System.currentTimeMillis() - timer;
+		mainLog.print("Backwards transient instantaneous rewards computation");
+		mainLog.println(" took " + iters + " iters and " + timer / 1000.0 + " seconds.");
+
+		// Return results
+		res = new ModelCheckerResult();
+		res.soln = sum;
+		res.lastSoln = soln2;
+		res.numIters = iters;
+		res.timeTaken = timer / 1000.0;
+		res.timePre = 0.0;
+		return res;
+	}
+
 	/**
 	 * Compute expected reachability rewards.
 	 * @param dtmc The CTMC
--- a/prism/src/explicit/DTMCModelChecker.java
+++ b/prism/src/explicit/DTMCModelChecker.java
@ -196,6 +196,12 @@ public class DTMCModelChecker extends ProbModelChecker
 			case ExpressionTemporal.R_F:
 				rewards = checkRewardReach(model, modelRewards, exprTemp);
 				break;
+			case ExpressionTemporal.R_I:
+				rewards = checkRewardInstantaneous(model, modelRewards, exprTemp);
+				break;
+			case ExpressionTemporal.R_C:
+				rewards = checkRewardCumulative(model, modelRewards, exprTemp);
+				break;
 			default:
 				throw new PrismException("Explicit engine does not yet handle the " + exprTemp.getOperatorSymbol() + " operator in the R operator");
 			}
@ -229,6 +235,145 @@ public class DTMCModelChecker extends ProbModelChecker
 		return rewards;
 	}

+	/**
+	 * Compute rewards for an instantaneous reward operator.
+	 */
+	protected StateValues checkRewardInstantaneous(Model model, MCRewards modelRewards, ExpressionTemporal expr) throws PrismException
+	{
+		StateValues rewards = null;
+		ModelCheckerResult res = null;
+
+		// get time bound
+		double t = expr.getUpperBound().evaluateDouble(constantValues);
+
+		// print out some info about num states
+		// mainLog.print("\nb = " + JDD.GetNumMintermsString(b1,
+		// allDDRowVars.n()));
+
+		res = computeInstantaneousRewards((DTMC) model, modelRewards, t);
+		rewards = StateValues.createFromDoubleArray(res.soln, model);
+
+		return rewards;
+	}
+
+	/**
+	 * Compute rewards for a cumulative reward operator.
+	 */
+	protected StateValues checkRewardCumulative(Model model, MCRewards modelRewards, ExpressionTemporal expr) throws PrismException
+	{
+		StateValues rewards = null;
+		ModelCheckerResult res = null;
+
+		// get time bound
+		double t = expr.getUpperBound().evaluateDouble(constantValues);
+
+		// print out some info about num states
+		// mainLog.print("\nb = " + JDD.GetNumMintermsString(b1,
+		// allDDRowVars.n()));
+
+		res = computeCumulativeRewards((DTMC) model, modelRewards, t);
+		rewards = StateValues.createFromDoubleArray(res.soln, model);
+
+		return rewards;
+	}
+
+	public ModelCheckerResult computeInstantaneousRewards(DTMC dtmc, MCRewards mcRewards, double t) 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();
+
+		// Start backwards transient computation
+		timer = System.currentTimeMillis();
+		mainLog.println("Starting backwards instantaneous rewards computation...");
+
+		// Create solution vector(s)
+		soln = new double[n];
+		soln2 = new double[n];
+
+		// Initialise solution vectors.
+		for (i = 0; i < n; i++)
+			soln[i] = mcRewards.getStateReward(i);
+
+		// Start iterations
+		for (iters = 0; iters < right; iters++) {
+			// Matrix-vector multiply
+			dtmc.mvMult(soln, soln2, null, false);
+			// Swap vectors for next iter
+			tmpsoln = soln;
+			soln = soln2;
+			soln2 = tmpsoln;
+			iters++;
+		}
+
+		// Finished backwards transient computation
+		timer = System.currentTimeMillis() - timer;
+		mainLog.print("Backwards transient instantaneous rewards computation");
+		mainLog.println(" took " + iters + " iters and " + timer / 1000.0 + " seconds.");
+
+		// Return results
+		res = new ModelCheckerResult();
+		res.soln = soln;
+		res.lastSoln = soln2;
+		res.numIters = iters;
+		res.timeTaken = timer / 1000.0;
+		res.timePre = 0.0;
+		return res;
+	}
+
+	public ModelCheckerResult computeCumulativeRewards(DTMC dtmc, MCRewards mcRewards, double t) 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();
+
+		// Start backwards transient computation
+		timer = System.currentTimeMillis();
+		mainLog.println("Starting backwards cumulative rewards computation...");
+
+		// Create solution vector(s)
+		soln = new double[n];
+		soln2 = new double[n];
+
+		// Start iterations
+		for (iters = 0; iters < right; iters++) {
+			// Matrix-vector multiply plus adding rewards
+			dtmc.mvMult(soln, soln2, null, false);
+			for (i = 0; i < n; i++) {
+				soln2[i] += mcRewards.getStateReward(i);
+			}
+			// Swap vectors for next iter
+			tmpsoln = soln;
+			soln = soln2;
+			soln2 = tmpsoln;
+			iters++;
+		}
+
+		// Finished backwards transient computation
+		timer = System.currentTimeMillis() - timer;
+		mainLog.print("Backwards cumulative rewards computation");
+		mainLog.println(" took " + iters + " iters and " + timer / 1000.0 + " seconds.");
+
+		// Return results
+		res = new ModelCheckerResult();
+		res.soln = soln;
+		res.lastSoln = soln2;
+		res.numIters = iters;
+		res.timeTaken = timer / 1000.0;
+		res.timePre = 0.0;
+		return res;
+	}
+
 	/**
 	 * Compute steady-state probabilities for an S operator.
 	 */