From 76fd3b5e80560219997480dda9be9120e1291ac6 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Sun, 24 Jul 2016 17:13:16 +0000
Subject: [PATCH] Bug fix for time-bounded probabilistic reachability in PTAs
 where the initial location is already a target (reported by Joachim Klein,
 Linda Leuschner).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11569 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/pta/PTAModelChecker.java | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/prism/src/pta/PTAModelChecker.java b/prism/src/pta/PTAModelChecker.java
index d17bda7b..507ed4fc 100644
--- a/prism/src/pta/PTAModelChecker.java
+++ b/prism/src/pta/PTAModelChecker.java
@@ -290,8 +290,12 @@ public class PTAModelChecker extends PrismComponent
 			}
 		}
 		// Re-generate set of target locations
+		// (newly added target location, plus initial location (always 0) is this is a target)
 		targetLocsNew = new BitSet(pta.getNumLocations());
 		targetLocsNew.set(newTargetLoc);
+		if (targetLocs.get(0)) {
+			targetLocsNew.set(0);
+		}
 
 		return targetLocsNew;
 	}