diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index 4c8fc556..02b5c54a 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/prism/src/explicit/CTMCModelChecker.java @@ -821,6 +821,25 @@ public class CTMCModelChecker extends ProbModelChecker } + /** + * Compute steady-state probabilities for an S operator, i.e., S=?[ b ]. + * @param ctmc the CTMC + * @param b the satisfaction set of states for the inner state formula of the operators + */ + protected StateValues computeSteadyStateFormula(CTMC ctmc, BitSet b) throws PrismException + { + double multProbs[] = Utils.bitsetToDoubleArray(b, ctmc.getNumStates()); + + // 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 probabilities 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)..."); + ModelCheckerResult res = createDTMCModelChecker().computeSteadyStateBackwardsProbs(dtmcEmb, multProbs, new SteadyStateBSCCPostProcessor(ctmc)); + return StateValues.createFromDoubleArray(res.soln, ctmc); + } + /** * Compute (forwards) steady-state probabilities * i.e. compute the long-run probability of being in each state, diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 1de83d2c..96e52277 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -1210,6 +1210,8 @@ public class ProbModelChecker extends NonProbModelChecker switch (model.getModelType()) { case DTMC: return ((DTMCModelChecker) this).computeSteadyStateFormula((DTMC) model, b); + case CTMC: + return ((CTMCModelChecker) this).computeSteadyStateFormula((CTMC) model, b); default: throw new PrismNotSupportedException("Explicit engine does not yet handle the S operator for " + model.getModelType() + "s"); }