explicit.DTMCModelChecker.computeReachRewards: use predecessor-relation-based computation for prob1

Previous behavior available using -noprerel switch.


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11977 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/DTMCModelChecker.java

@@ -1269,7 +1269,14 @@ public class DTMCModelChecker extends ProbModelChecker
 
 		// Precomputation (not optional)
 		timerProb1 = System.currentTimeMillis();
+		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;