From 2bcdab29a59617a65456eb15dadafd5feea5393d Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 21 Jul 2017 13:12:10 +0000
Subject: [PATCH] explicit.NondetModel: provide default
 successorsSafeAndCanReach methods

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12088 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/explicit/NondetModel.java | 40 +++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)

diff --git a/prism/src/explicit/NondetModel.java b/prism/src/explicit/NondetModel.java
index a9abb9fc..d4cb72bd 100644
--- a/prism/src/explicit/NondetModel.java
+++ b/prism/src/explicit/NondetModel.java
@@ -92,6 +92,21 @@ public interface NondetModel extends Model
 		return someSuccessorsMatch(s, i, set::get);
 	}
 
+	/**
+	 * Check the successor states from choice {@code i} of state {@code s}:
+	 * Return {@code true} iff all successors are contained in {@code u}
+	 * (remain in a "safe" region) and at least one is contained in {@code v}
+	 * (can reach the region defined by v).
+	 * @param s The state to check
+	 * @param i Choice index
+	 * @param u The BitSet that all successors have to be in
+	 * @param v The BitSet that some successors have to be in
+	 */
+	public default boolean successorsSafeAndCanReach(int s, int i, BitSet u, BitSet v)
+	{
+		return successorsSafeAndCanReach(s, i, u::get, v::get);
+	}
+
 	/**
 	 * Check if all the successor states from choice {@code i} of state {@code s} match the predicate.
 	 * @param s The state to check
@@ -136,6 +151,31 @@ public interface NondetModel extends Model
 		return false;
 	}
 
+	/**
+	 * Check the successor states from choice {@code i} of state {@code s}:
+	 * Return {@code true} iff all successors match the predicate {@code u}
+	 * (remain in a "safe" region) and at least one matches predicate {@code v}
+	 * (can reach the region defined by v).
+	 * @param s The state to check
+	 * @param i Choice index
+	 * @param u The first predicate (all successors have to match)
+	 * @param v The second predicate (some successors have to match)
+	 */
+	public default boolean successorsSafeAndCanReach(int s, int i, IntPredicate u, IntPredicate v)
+	{
+		SuccessorsIterator it = getSuccessors(s, i);
+		boolean hadTransitionToV = false;
+		while (it.hasNext()) {
+			int t = it.nextInt();
+			if (!u.test(t))
+				return false;
+			if (!hadTransitionToV) {
+				hadTransitionToV = v.test(t);
+			}
+		}
+		return hadTransitionToV;
+	}
+
 	/**
 	 * Get an iterator over the successor states from choice {@code i} of state {@code s}.
 	 * @param s The state