s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

explicit: Support computation of R=? [ S ] for DTMCs/CTMCs 

The computation reuses the computeSteadyStateBackwardsProbs() method
used for the computation of S=?[ phi ]. We tweak the variable names
and comments in that method to make clear that the solution values of
a BSCC - after multiplication with the mult array - are not
necessarily probabilities anymore.
accumulation-v4.7
Joachim Klein 8 years ago
committed by Dave Parker
parent
a8aa7f1f15
commit
16240b0eee
3 changed files with 88 additions and 18 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 23
      prism/src/explicit/CTMCModelChecker.java
  2. 59
      prism/src/explicit/DTMCModelChecker.java
  3. 24
      prism/src/explicit/ProbModelChecker.java

23
prism/src/explicit/CTMCModelChecker.java
View File

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

59
prism/src/explicit/DTMCModelChecker.java
View File

@ -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.
* <br>
* 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.
* <br>
* 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.

24
prism/src/explicit/ProbModelChecker.java
View File

@ -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.
*/

Write Preview
Loading…
Cancel
Save