diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java
index 02b5c54a..ef56efbe 100644
--- a/prism/src/explicit/CTMCModelChecker.java
+++ b/prism/src/explicit/CTMCModelChecker.java
@@ -860,6 +860,29 @@ public class CTMCModelChecker extends ProbModelChecker
return createDTMCModelChecker().computeSteadyStateProbs(dtmcEmb, initDist, new SteadyStateBSCCPostProcessor(ctmc));
}
+ /**
+ * Compute steady-state rewards, i.e., R=?[ S ].
+ * @param ctmc the CTMC
+ * @param modelRewards the (state) rewards
+ */
+ public ModelCheckerResult computeSteadyStateRewards(CTMC ctmc, MCRewards modelRewards) throws PrismException
+ {
+ int n = ctmc.getNumStates();
+ double multRewards[] = new double[n];
+
+ for (int i = 0; i < n; i++) {
+ multRewards[i] = modelRewards.getStateReward(i);
+ }
+
+ // We construct the embedded DTMC and do the steady-state computation there
+ mainLog.println("Building embedded DTMC...");
+ DTMC dtmcEmb = ctmc.getImplicitEmbeddedDTMC();
+
+ // compute the steady-state rewards in the embedded DTMC, applying the BSCC value post-processing
+ mainLog.println("Doing steady-state computation in embedded DTMC (with exit-rate weighting for BSCC probabilities)...");
+ return createDTMCModelChecker().computeSteadyStateBackwardsProbs(dtmcEmb, multRewards, new SteadyStateBSCCPostProcessor(ctmc));
+ }
+
/**
* Compute transient probabilities.
* i.e. compute the probability of being in each state at time {@code t},
diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java
index 216920a2..f2c46618 100644
--- a/prism/src/explicit/DTMCModelChecker.java
+++ b/prism/src/explicit/DTMCModelChecker.java
@@ -2308,12 +2308,15 @@ public class DTMCModelChecker extends ProbModelChecker
* of the steady-state probability of being in s'
* multiplied by the corresponding probability in the vector {@code multProbs}.
* If {@code multProbs} is null, it is assumed to be all 1s.
+ *
+ * Note: This method can also be used to compute the steady-state backwards rewards, i.e.,
+ * when mult contains the state rewards for the BSCC states.
* @param dtmc The DTMC
- * @param multProbs Multiplication vector (optional: null means all 1s)
+ * @param mult Multiplication vector, used to weight the steady-state probabilities for BSCC states (optional: null means all 1s)
*/
- public ModelCheckerResult computeSteadyStateBackwardsProbs(DTMC dtmc, double multProbs[]) throws PrismException
+ public ModelCheckerResult computeSteadyStateBackwardsProbs(DTMC dtmc, double mult[]) throws PrismException
{
- return computeSteadyStateBackwardsProbs(dtmc, multProbs, null);
+ return computeSteadyStateBackwardsProbs(dtmc, mult, null);
}
/**
@@ -2322,11 +2325,14 @@ public class DTMCModelChecker extends ProbModelChecker
* of the steady-state probability of being in s'
* multiplied by the corresponding probability in the vector {@code multProbs}.
* If {@code multProbs} is null, it is assumed to be all 1s.
+ *
+ * Note: This method can also be used to compute the steady-state backwards rewards, i.e.,
+ * when mult contains the state rewards for the BSCC states.
* @param dtmc The DTMC
- * @param multProbs Multiplication vector (optional: null means all 1s)
+ * @param mult Multiplication vector, used to weight the steady-state probabilities for BSCC states (optional: null means all 1s)
* @param bsccPostProcessor Post-processor for the values of each BSCC (optional: null means no post-processing)
*/
- public ModelCheckerResult computeSteadyStateBackwardsProbs(DTMC dtmc, double multProbs[], BSCCPostProcessor bsccPostProcessor) throws PrismException
+ public ModelCheckerResult computeSteadyStateBackwardsProbs(DTMC dtmc, double mult[], BSCCPostProcessor bsccPostProcessor) throws PrismException
{
StopWatch watch = new StopWatch().start();
@@ -2341,8 +2347,8 @@ public class DTMCModelChecker extends ProbModelChecker
BitSet notInBSCCs = sccStore.getNotInBSCCs();
int numBSCCs = bsccs.size();
- // Compute steady-state probability for each BSCC...
- double[] probBSCCs = new double[numBSCCs];
+ // Compute steady-state values for each BSCC...
+ double[] valueBSCCs = new double[numBSCCs];
double[] ssProbs = new double[numStates];
for (int b = 0; b < numBSCCs; b++) {
mainLog.println("\nComputing steady state probabilities for BSCC " + (b + 1));
@@ -2352,21 +2358,21 @@ public class DTMCModelChecker extends ProbModelChecker
if (bsccPostProcessor != null) {
bsccPostProcessor.apply(ssProbs, bscc);
}
- // Compute weighted sum of probabilities with multProbs
- probBSCCs[b] = 0.0;
- if (multProbs == null) {
+ // Compute weighted sum of probabilities with mult
+ valueBSCCs[b] = 0.0;
+ if (mult == null) {
for (int i = bscc.nextSetBit(0); i >= 0; i = bscc.nextSetBit(i + 1)) {
- probBSCCs[b] += ssProbs[i];
+ valueBSCCs[b] += ssProbs[i];
}
} else {
for (int i = bscc.nextSetBit(0); i >= 0; i = bscc.nextSetBit(i + 1)) {
- probBSCCs[b] += multProbs[i] * ssProbs[i];
+ valueBSCCs[b] += mult[i] * ssProbs[i];
}
}
- mainLog.print("\nValue for BSCC " + (b + 1) + ": " + probBSCCs[b] + "\n");
+ mainLog.print("\nValue for BSCC " + (b + 1) + ": " + valueBSCCs[b] + "\n");
}
- // Create/initialise prob vector
+ // Create/initialise solution vector
double[] soln = new double[numStates];
for (int i = 0; i < numStates; i++) {
soln[i] = 0.0;
@@ -2378,7 +2384,7 @@ public class DTMCModelChecker extends ProbModelChecker
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))
- soln[i] += probBSCCs[b];
+ soln[i] += valueBSCCs[b];
}
}
@@ -2386,8 +2392,8 @@ public class DTMCModelChecker extends ProbModelChecker
else {
// Compute probabilities of reaching each BSCC...
for (int b = 0; b < numBSCCs; b++) {
- // Skip BSCCs with zero probability
- if (probBSCCs[b] == 0.0)
+ // Skip BSCCs with zero value
+ if (valueBSCCs[b] == 0.0)
continue;
mainLog.println("\nComputing probabilities of reaching BSCC " + (b + 1));
BitSet bscc = bsccs.get(b);
@@ -2395,7 +2401,7 @@ public class DTMCModelChecker extends ProbModelChecker
double[] reachProbs = computeUntilProbs(dtmc, notInBSCCs, bscc).soln;
// Multiply by value for BSCC, add to total
for (int i = 0; i < numStates; i++) {
- soln[i] += reachProbs[i] * probBSCCs[b];
+ soln[i] += reachProbs[i] * valueBSCCs[b];
}
}
}
@@ -2407,6 +2413,23 @@ public class DTMCModelChecker extends ProbModelChecker
return res;
}
+ /**
+ * Compute steady-state rewards, i.e., R=?[ S ].
+ * @param dtmc the DTMC
+ * @param modelRewards the (state) rewards
+ */
+ public ModelCheckerResult computeSteadyStateRewards(DTMC dtmc, MCRewards modelRewards) throws PrismException
+ {
+ int n = dtmc.getNumStates();
+ double multRewards[] = new double[n];
+
+ for (int i = 0; i < n; i++) {
+ multRewards[i] = modelRewards.getStateReward(i);
+ }
+
+ return computeSteadyStateBackwardsProbs(dtmc, multRewards);
+ }
+
/**
* Compute steady-state probabilities for a BSCC
* i.e. compute the long-run probability of being in each state of the BSCC.
diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java
index 96e52277..cf079e9a 100644
--- a/prism/src/explicit/ProbModelChecker.java
+++ b/prism/src/explicit/ProbModelChecker.java
@@ -984,6 +984,9 @@ public class ProbModelChecker extends NonProbModelChecker
rewards = checkRewardTotal(model, modelRewards, exprTemp, minMax);
}
break;
+ case ExpressionTemporal.R_S:
+ rewards = checkRewardSteady(model, modelRewards);
+ break;
default:
throw new PrismNotSupportedException("Explicit engine does not yet handle the " + exprTemp.getOperatorSymbol() + " reward operator");
}
@@ -1109,6 +1112,27 @@ public class ProbModelChecker extends NonProbModelChecker
return StateValues.createFromDoubleArray(res.soln, model);
}
+ /**
+ * Compute expected rewards for a steady-state reward operator.
+ */
+ protected StateValues checkRewardSteady(Model model, Rewards modelRewards) throws PrismException
+ {
+ // Compute/return the rewards
+ ModelCheckerResult res = null;
+ switch (model.getModelType()) {
+ case DTMC:
+ res = ((DTMCModelChecker) this).computeSteadyStateRewards((DTMC) model, (MCRewards) modelRewards);
+ break;
+ case CTMC:
+ res = ((CTMCModelChecker) this).computeSteadyStateRewards((CTMC) model, (MCRewards) modelRewards);
+ break;
+ default:
+ throw new PrismNotSupportedException("Explicit engine does not yet handle the steady-state reward operator for " + model.getModelType() + "s");
+ }
+ result.setStrategy(res.strat);
+ return StateValues.createFromDoubleArray(res.soln, model);
+ }
+
/**
* Compute rewards for a path formula in a reward operator.
*/