Provide method to compute steady state probs for BSCC without explici…

…t post processing

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

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.