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

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