diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index 5d3862c1..dff63be3 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/prism/src/explicit/CTMCModelChecker.java @@ -201,6 +201,19 @@ public class CTMCModelChecker extends DTMCModelChecker // Numerical computation functions + /** + * Compute next=state probabilities. + * i.e. compute the probability of being in a state in {@code target} in the next step. + * @param dtmc The DTMC + * @param target Target states + */ + public ModelCheckerResult computeNextProbs(DTMC dtmc, BitSet target) throws PrismException + { + mainLog.println("Building embedded DTMC..."); + DTMC dtmcEmb = ((CTMC) dtmc).buildImplicitEmbeddedDTMC(); + return super.computeNextProbs(dtmcEmb, target); + } + /** * Compute reachability/until probabilities. * i.e. compute the probability of reaching a state in {@code target},