diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 7eeed4e2..8c2343e0 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -1269,7 +1269,14 @@ public class DTMCModelChecker extends ProbModelChecker // Precomputation (not optional) timerProb1 = System.currentTimeMillis(); - inf = prob1(dtmc, null, target); + if (preRel) { + // prob1 via predecessor relation + PredecessorRelation pre = dtmc.getPredecessorRelation(this, true); + inf = prob1(dtmc, null, target, pre); + } else { + // prob1 via fixed-point algorithm + inf = prob1(dtmc, null, target); + } inf.flip(0, n); timerProb1 = System.currentTimeMillis() - timerProb1;