From b7093533e5720607c051b0c522286657dbc033e2 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Sun, 24 Jul 2016 17:38:52 +0000
Subject: [PATCH] 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 | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/prism/src/pta/PTAModelChecker.java b/prism/src/pta/PTAModelChecker.java
index c89a68d4..93b8af5f 100644
--- a/prism/src/pta/PTAModelChecker.java
+++ b/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);