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

@@ -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));