Optimisation for PTA model checking where the initial state is a target - just return 1.

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

prism/src/pta/PTAModelChecker.java

@@ -309,6 +309,12 @@ public class PTAModelChecker extends PrismComponent
 	 */
 	private double computeProbabilisticReachability(BitSet targetLocs, boolean min) throws PrismException
 	{
+		// Catch the special case where the initial state is already a target - just return 1.0 directly
+		if (targetLocs.get(0)) {
+			mainLog.println("Skipping numerical computation since initial state is a target...");
+			return 1.0;
+		}
+		
 		// Determine which method to use for computation
 		String ptaMethod = settings.getString(PrismSettings.PRISM_PTA_METHOD);