From c7c8c8a7ff0f46b8a310e3cf9d483250ac45fa7c Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Thu, 16 Feb 2017 18:40:06 +0000
Subject: [PATCH] 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 | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

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;