From 6a1417c6f41d21f4a3c4c362c438083d1c6d4dd4 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 23 Mar 2015 10:15:56 +0000 Subject: [PATCH] Bug fix in explicit engine CTMC until model checking (spotted by Chris Dehnert) (probably due to recent ProbModelChecker refactoring). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9699 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/CTMCModelChecker.java | 28 ++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index d9553805..99e5562c 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/prism/src/explicit/CTMCModelChecker.java @@ -230,6 +230,34 @@ public class CTMCModelChecker extends DTMCModelChecker return super.computeNextProbs(dtmcEmb, target); } + /** + * Compute reachability probabilities. + * i.e. compute the probability of reaching a state in {@code target}. + * @param ctmc The CTMC + * @param target Target states + */ + public ModelCheckerResult computeReachProbs(CTMC ctmc, BitSet target) throws PrismException + { + mainLog.println("Building embedded DTMC..."); + DTMC dtmcEmb = ctmc.buildImplicitEmbeddedDTMC(); + return super.computeReachProbs(dtmcEmb, target); + } + + /** + * Compute until probabilities. + * i.e. compute the probability of reaching a state in {@code target}, + * while remaining in those in @{code remain}. + * @param dtmc The CTMC + * @param remain Remain in these states (optional: null means "all") + * @param target Target states + */ + public ModelCheckerResult computeUntilProbs(CTMC ctmc, BitSet remain, BitSet target) throws PrismException + { + mainLog.println("Building embedded DTMC..."); + DTMC dtmcEmb = ctmc.buildImplicitEmbeddedDTMC(); + return super.computeUntilProbs(dtmcEmb, remain, target); + } + /** * Compute reachability/until probabilities. * i.e. compute the probability of reaching a state in {@code target},