From 01a398bbc04c58b4faf64cb0cd90a18b518126d2 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 16 Feb 2017 18:41:16 +0000 Subject: [PATCH] explicit.DTMCModelChecker.computeTotalRewards: use predecessor-relation-based computations for prob0 Previous behavior available via -noprerel switch. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11978 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/DTMCModelChecker.java | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 8c2343e0..1093f02f 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -368,7 +368,15 @@ public class DTMCModelChecker extends ProbModelChecker mainLog.print("States in non-zero reward BSCCs: " + bsccsNonZero.cardinality()); // Find states with infinite reward (those reach a non-zero reward BSCC with prob > 0) - BitSet inf = prob0(dtmc, null, bsccsNonZero); + BitSet inf; + if (preRel) { + // prob0 using predecessor relation + PredecessorRelation pre = dtmc.getPredecessorRelation(this, true); + inf = prob0(dtmc, null, bsccsNonZero, pre); + } else { + // prob0 using fixed point algorithm + inf = prob0(dtmc, null, bsccsNonZero); + } inf.flip(0, n); int numInf = inf.cardinality(); mainLog.println(", inf=" + numInf + ", maybe=" + (n - numInf));