From 852398415b2eff4ffa7e866099c83a24a2a40036 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Tue, 7 Jul 2015 09:22:03 +0000
Subject: [PATCH] Add R[C] model checking for explicit DTMC model checker too
 (not really testeed much yet).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10215 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/explicit/DTMCModelChecker.java | 63 ++++++++++++++++++++++++
 prism/src/explicit/ProbModelChecker.java | 35 ++++++++++++-
 2 files changed, 96 insertions(+), 2 deletions(-)

diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java
index 128da11d..a524d3a7 100644
--- a/prism/src/explicit/DTMCModelChecker.java
+++ b/prism/src/explicit/DTMCModelChecker.java
@@ -214,6 +214,69 @@ public class DTMCModelChecker extends ProbModelChecker
 		return res;
 	}
 
+	public ModelCheckerResult computeTotalRewards(DTMC dtmc, MCRewards mcRewards) throws PrismException
+	{
+		ModelCheckerResult res = null;
+		int n, numBSCCs = 0;
+		long timer;
+
+		// Switch to a supported method, if necessary
+		if (!(linEqMethod == LinEqMethod.POWER)) {
+			linEqMethod = LinEqMethod.POWER;
+			mainLog.printWarning("Switching to linear equation solution method \"" + linEqMethod.fullName() + "\"");
+		}
+
+		// Store num states
+		n = dtmc.getNumStates();
+
+		// Start total rewards computation
+		timer = System.currentTimeMillis();
+		mainLog.println("\nStarting total reward computation...");
+
+		// Compute bottom strongly connected components (BSCCs)
+		SCCComputer sccComputer = SCCComputer.createSCCComputer(this, dtmc);
+		sccComputer.computeBSCCs();
+		List<BitSet> bsccs = sccComputer.getBSCCs();
+		numBSCCs = bsccs.size();
+
+		// Find BSCCs with non-zero reward
+		BitSet bsccsNonZero = new BitSet();
+		for (int b = 0; b < numBSCCs; b++) {
+			BitSet bscc = bsccs.get(b);
+			for (int i = bscc.nextSetBit(0); i >= 0; i = bscc.nextSetBit(i + 1)) {
+				if (mcRewards.getStateReward(i) > 0) {
+					bsccsNonZero.or(bscc);
+					continue;
+				}
+			}
+		}
+		mainLog.print("States in non-zero reward BSCCs: " + bsccsNonZero.cardinality());
+		
+		// Find states with infinite reward (those reach a non-zero reward BSCC with prob > 0)
+		BitSet inf = prob0(dtmc, null, bsccsNonZero);
+		inf.flip(0, n);
+		int numInf = inf.cardinality();
+		mainLog.println(", inf=" + numInf + ", maybe=" + (n - numInf));
+		
+		// Compute rewards
+		// (do this using the functions for "reward reachability" properties but with no targets)
+		switch (linEqMethod) {
+		case POWER:
+			res = computeReachRewardsValIter(dtmc, mcRewards, new BitSet(), inf, null, null);
+			break;
+		default:
+			throw new PrismException("Unknown linear equation solution method " + linEqMethod.fullName());
+		}
+
+		// Finished total reward computation
+		timer = System.currentTimeMillis() - timer;
+		mainLog.print("Total reward computation");
+		mainLog.println(" took " + timer / 1000.0 + " seconds.");
+
+		// Return results
+		return res;
+	}
+
 	// Steady-state/transient probability computation
 
 	/**
diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java
index cb9f5b66..7a18b7ea 100644
--- a/prism/src/explicit/ProbModelChecker.java
+++ b/prism/src/explicit/ProbModelChecker.java
@@ -894,7 +894,11 @@ public class ProbModelChecker extends NonProbModelChecker
 				rewards = checkRewardInstantaneous(model, modelRewards, exprTemp, minMax);
 				break;
 			case ExpressionTemporal.R_C:
-				rewards = checkRewardCumulative(model, modelRewards, exprTemp, minMax);
+				if (exprTemp.hasBounds()) {
+					rewards = checkRewardCumulative(model, modelRewards, exprTemp, minMax);
+				} else {
+					rewards = checkRewardTotal(model, modelRewards, exprTemp, minMax);
+				}
 				break;
 			default:
 				throw new PrismNotSupportedException("Explicit engine does not yet handle the " + exprTemp.getOperatorSymbol() + " reward operator");
@@ -972,7 +976,7 @@ public class ProbModelChecker extends NonProbModelChecker
 
 		// Check that there is an upper time bound
 		if (expr.getUpperBound() == null) {
-			throw new PrismNotSupportedException("Cumulative reward operator without time bound (C) is only allowed for multi-objective queries");
+			throw new PrismNotSupportedException("This is not a cumulative reward operator");
 		}
 
 		// Get time bound
@@ -1013,6 +1017,33 @@ public class ProbModelChecker extends NonProbModelChecker
 		return StateValues.createFromDoubleArray(res.soln, model);
 	}
 
+	/**
+	 * Compute expected rewards for a total reward operator.
+	 */
+	protected StateValues checkRewardTotal(Model model, Rewards modelRewards, ExpressionTemporal expr, MinMax minMax) throws PrismException
+	{
+		// Check that there is no upper time bound
+		if (expr.getUpperBound() != null) {
+			throw new PrismException("This is not a total reward operator");
+		}
+
+		// Compute/return the rewards
+		ModelCheckerResult res = null;
+		switch (model.getModelType()) {
+		case DTMC:
+			res = ((DTMCModelChecker) this).computeTotalRewards((DTMC) model, (MCRewards) modelRewards);
+			break;
+		case CTMC:
+			break;
+		case MDP:
+			break;
+		default:
+			throw new PrismNotSupportedException("Explicit engine does not yet handle the " + expr.getOperatorSymbol() + " reward operator for " + model.getModelType()
+					+ "s");
+		}
+		return StateValues.createFromDoubleArray(res.soln, model);
+	}
+
 	/**
 	 * Model check an S operator expression and return the values for all states.
 	 */