diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index ef56efbef3..a41c889a57 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/prism/src/explicit/CTMCModelChecker.java @@ -860,6 +860,18 @@ public ModelCheckerResult computeSteadyStateProbs(CTMC ctmc, double initDist[]) return createDTMCModelChecker().computeSteadyStateProbs(dtmcEmb, initDist, new SteadyStateBSCCPostProcessor(ctmc)); } + /** + * @see DTMCModelChecker#computeSteadyStateProbsForBSCC(DTMC, BitSet, double[], BSCCPostProcessor) + */ + public ModelCheckerResult computeSteadyStateProbsForBSCC(CTMC ctmc, BitSet states, double result[]) throws PrismException + { + // We construct the embedded DTMC and do the steady-state computation there + mainLog.println("Building embedded DTMC..."); + DTMC dtmcEmb = ctmc.getImplicitEmbeddedDTMC(); + + return createDTMCModelChecker().computeSteadyStateProbsForBSCC(dtmcEmb, states, result, new SteadyStateBSCCPostProcessor(ctmc)); + } + /** * Compute steady-state rewards, i.e., R=?[ S ]. * @param ctmc the CTMC diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index f94496029b..5df7221eaf 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -2421,6 +2421,14 @@ public ModelCheckerResult computeSteadyStateRewards(DTMC dtmc, MCRewards modelRe return computeSteadyStateBackwardsProbs(dtmc, multRewards); } + /** + * @see DTMCModelChecker#computeSteadyStateProbsForBSCC(DTMC, BitSet, double[], BSCCPostProcessor) + */ + public ModelCheckerResult computeSteadyStateProbsForBSCC(DTMC dtmc, BitSet states, double result[]) throws PrismException + { + return computeSteadyStateProbsForBSCC(dtmc, states, result, null); + } + /** * Compute steady-state probabilities for a BSCC * i.e. compute the long-run probability of being in each state of the BSCC.