From e38ea63e8997f6984bb2fd61eb19f23783fa6286 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 2 Sep 2016 13:03:26 +0000 Subject: [PATCH] Fix U>=t computations for CTMC, explicit engine [with Marcus Daum] The unbounded until computation has to be carried out on the embedded DTMC. Fixes issue prismmodelchecker/prism#9. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11768 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/CTMCModelChecker.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index ff7f36dc..e75417ac 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/prism/src/explicit/CTMCModelChecker.java @@ -180,11 +180,11 @@ public class CTMCModelChecker extends ProbModelChecker // check for special case of lTime == 0, this is actually an unbounded until if (lTime == 0) { // compute probs - res = createDTMCModelChecker().computeUntilProbs((DTMC) model, b1, b2); + res = computeUntilProbs((CTMC)model, b1, b2); probs = StateValues.createFromDoubleArray(res.soln, model); } else { // compute unbounded until probs - tmpRes = createDTMCModelChecker().computeUntilProbs((DTMC) model, b1, b2); + tmpRes = computeUntilProbs((CTMC)model, b1, b2); // compute bounded until probs res = computeTransientBackwardsProbs((CTMC) model, b1, b1, lTime, tmpRes.soln); probs = StateValues.createFromDoubleArray(res.soln, model);