From 2ef6a3e2eea6f860892ce617baf57a5c69fe45bc Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 11 Dec 2012 16:39:55 +0000 Subject: [PATCH] Bug fix: computing next probs in explicit engine (was not converted to embedded DTMC). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6173 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/CTMCModelChecker.java | 13 +++++++++++++ 1 file changed, 13 insertions(+) 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},