From 189275bed4677d31981544b206897477b2c1e447 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Mon, 28 Aug 2017 12:45:47 +0200
Subject: [PATCH] param.StateEliminator: provide variant of
 collectStatesBackward() that only returns the reachable predecessors

---
 prism/src/param/StateEliminator.java | 21 +++++++++++++++++++--
 1 file changed, 19 insertions(+), 2 deletions(-)

diff --git a/prism/src/param/StateEliminator.java b/prism/src/param/StateEliminator.java
index 3a02b16d..ee8a2e3e 100644
--- a/prism/src/param/StateEliminator.java
+++ b/prism/src/param/StateEliminator.java
@@ -124,10 +124,23 @@ final class StateEliminator {
 	 * Orders states so that states near target states are eliminated first.
 	 * States which do not reach target states are eliminated last. In case
 	 * there are no target states, the order is arbitrary
+	 */
+	private int[] collectStatesBackward()
+	{
+		return collectStatesBackward(false);
+	}
+
+	/**
+	 * Orders states so that states near target states are eliminated first.
+	 * States which do not reach target states are eliminated last. In case
+	 * there are no target states, the order is arbitrary
+	 * <br>
+	 * If {@code onlyStatesReachingTarget} is true, only the states that
+	 * can reach the target states will be returned.
 	 * 
 	 * @return list of states in requested order
 	 */
-	private int[] collectStatesBackward()
+	private int[] collectStatesBackward(boolean onlyStatesReachingTarget)
 	{
 		int[] states = new int[pmc.getNumStates()];
 		BitSet seen = new BitSet(pmc.getNumStates());
@@ -155,7 +168,11 @@ final class StateEliminator {
 			}
 			current = next;
 		}
-		
+
+		if (onlyStatesReachingTarget) {
+			return states;
+		}
+
 		/* might not find all states when doing as above,
 		 * so add missing ones */
 		HashSet<Integer> allStates = new HashSet<Integer>();