explicit.DTMC, refactor: provide default implementation for prob0step and prob1step, as well as new single state prob0step, prob1step methods

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

prism/src/explicit/DTMC.java

@@ -28,7 +28,9 @@ package explicit;
 
 import java.util.*;
 import java.util.Map.Entry;
+import java.util.PrimitiveIterator.OfInt;
 
+import common.IterableStateSet;
 import prism.Pair;
 import explicit.rewards.MCRewards;
 
@@ -52,14 +54,68 @@ public interface DTMC extends Model
 	 */
 	public Iterator<Entry<Integer, Pair<Double, Object>>> getTransitionsAndActionsIterator(int s);
 
+	/**
+	 * Perform a single step of precomputation algorithm Prob0 for a single state,
+	 * i.e., for the state {@code s} returns true iff there is a transition from
+	 * {@code s} to a state in {@code u}.
+	 * <br>
+	 * <i>Default implementation</i>: Iterates using {@code getSuccessors()} and performs the check.
+	 * @param s The state in question
+	 * @param u Set of states {@code u}
+	 * @return true iff there is a transition from s to a state in u
+	 */
+	public default boolean prob0step(int s, BitSet u)
+	{
+		for (SuccessorsIterator succ = getSuccessors(s); succ.hasNext(); ) {
+			int t = succ.nextInt();
+			if (u.get(t))
+				return true;
+		}
+		return false;
+	}
+
 	/**
 	 * Perform a single step of precomputation algorithm Prob0, i.e., for states i in {@code subset},
 	 * set bit i of {@code result} iff there is a transition to a state in {@code u}.
+	 * <br>
+	 * <i>Default implementation</i>: Iterate over {@code subset} and use {@code prob0step(s,u)}
+	 * to determine result for {@code s}.
 	 * @param subset Only compute for these states
 	 * @param u Set of states {@code u}
 	 * @param result Store results here
 	 */
-	public void prob0step(BitSet subset, BitSet u, BitSet result);
+	public default void prob0step(BitSet subset, BitSet u, BitSet result)
+	{
+		for (OfInt it = new IterableStateSet(subset, getNumStates()).iterator(); it.hasNext();) {
+			int s = it.nextInt();
+			result.set(s, prob0step(s,u));
+		}
+	}
+
+	/**
+	 * Perform a single step of precomputation algorithm Prob1 for a single state,
+	 * i.e., for states s return true iff there is a transition to a state in
+	 * {@code v} and all transitions go to states in {@code u}.
+	 * @param s The state in question
+	 * @param u Set of states {@code u}
+	 * @param v Set of states {@code v}
+	 * @return true iff there is a transition from s to a state in v and all transitions go to u.
+	 */
+	public default boolean prob1step(int s, BitSet u, BitSet v)
+	{
+		boolean allTransitionsToU = true;
+		boolean hasTransitionToV = false;
+		for (SuccessorsIterator succ = getSuccessors(s); succ.hasNext(); ) {
+			int t = succ.nextInt();
+			if (!u.get(t)) {
+				allTransitionsToU = false;
+				// early abort, as overall result is false
+				break;
+			}
+			hasTransitionToV = hasTransitionToV || v.get(t);
+		}
+		return (allTransitionsToU && hasTransitionToV);
+	}
 
 	/**
 	 * Perform a single step of precomputation algorithm Prob1, i.e., for states i in {@code subset},
@@ -69,7 +125,13 @@ public interface DTMC extends Model
 	 * @param v Set of states {@code v}
 	 * @param result Store results here
 	 */
-	public void prob1step(BitSet subset, BitSet u, BitSet v, BitSet result);
+	public default void prob1step(BitSet subset, BitSet u, BitSet v, BitSet result)
+	{
+		for (OfInt it = new IterableStateSet(subset, getNumStates()).iterator(); it.hasNext();) {
+			int s = it.nextInt();
+			result.set(s, prob1step(s,u,v));
+		}
+	}
 
 	/**
 	 * Do a matrix-vector multiplication for