Extend previous commit (reachability enlarging target) to STPG model checking.

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

prism/src/explicit/STPGModelChecker.java

@@ -31,6 +31,8 @@ import java.util.BitSet;
 import java.util.List;
 import java.util.Map;
 
+import common.IterableBitSet;
+
 import parser.ast.Expression;
 import prism.PrismComponent;
 import prism.PrismException;
@@ -114,7 +116,7 @@ public class STPGModelChecker extends ProbModelChecker
 	/**
 	 * Compute until probabilities.
 	 * i.e. compute the min/max probability of reaching a state in {@code target},
-	 * while remaining in those in @{code remain}.
+	 * while remaining in those in {@code remain}.
 	 * @param stpg The STPG
 	 * @param remain Remain in these states (optional: null means "all")
 	 * @param target Target states
@@ -129,7 +131,7 @@ public class STPGModelChecker extends ProbModelChecker
 	/**
 	 * Compute reachability/until probabilities.
 	 * i.e. compute the min/max probability of reaching a state in {@code target},
-	 * while remaining in those in @{code remain}.
+	 * while remaining in those in {@code remain}.
 	 * @param stpg The STPG
 	 * @param remain Remain in these states (optional: null means "all")
 	 * @param target Target states
@@ -144,7 +146,7 @@ public class STPGModelChecker extends ProbModelChecker
 	{
 		ModelCheckerResult res = null;
 		BitSet no, yes;
-		int i, n, numYes, numNo;
+		int n, numYes, numNo;
 		long timer, timerProb0, timerProb1;
 		boolean genAdv;
 
@@ -168,10 +170,12 @@ public class STPGModelChecker extends ProbModelChecker
 		n = stpg.getNumStates();
 
 		// Optimise by enlarging target set (if more info is available)
-		if (init != null && known != null) {
-			BitSet targetNew = new BitSet(n);
-			for (i = 0; i < n; i++) {
-				targetNew.set(i, target.get(i) || (known.get(i) && init[i] == 1.0));
+		if (init != null && known != null && !known.isEmpty()) {
+			BitSet targetNew = (BitSet) target.clone();
+			for (int i : new IterableBitSet(known)) {
+				if (init[i] == 1.0) {
+					targetNew.set(i);
+				}
 			}
 			target = targetNew;
 		}
@@ -226,7 +230,7 @@ public class STPGModelChecker extends ProbModelChecker
 	/**
 	 * Prob0 precomputation algorithm.
 	 * i.e. determine the states of an STPG which, with min/max probability 0,
-	 * reach a state in {@code target}, while remaining in those in @{code remain}.
+	 * reach a state in {@code target}, while remaining in those in {@code remain}.
 	 * {@code min}=true gives Prob0E, {@code min}=false gives Prob0A. 
 	 * @param stpg The STPG
 	 * @param remain Remain in these states (optional: null means "all")
@@ -299,7 +303,7 @@ public class STPGModelChecker extends ProbModelChecker
 	/**
 	 * Prob1 precomputation algorithm.
 	 * i.e. determine the states of an STPG which, with min/max probability 1,
-	 * reach a state in {@code target}, while remaining in those in @{code remain}.
+	 * reach a state in {@code target}, while remaining in those in {@code remain}.
 	 * @param stpg The STPG
 	 * @param remain Remain in these states (optional: null means "all")
 	 * @param target Target states
@@ -617,7 +621,7 @@ public class STPGModelChecker extends ProbModelChecker
 	/**
 	 * Compute bounded until probabilities.
 	 * i.e. compute the min/max probability of reaching a state in {@code target},
-	 * within k steps, and while remaining in states in @{code remain}.
+	 * within k steps, and while remaining in states in {@code remain}.
 	 * @param stpg The STPG
 	 * @param remain Remain in these states (optional: null means "all")
 	 * @param target Target states
@@ -633,7 +637,7 @@ public class STPGModelChecker extends ProbModelChecker
 	/**
 	 * Compute bounded reachability/until probabilities.
 	 * i.e. compute the min/max probability of reaching a state in {@code target},
-	 * within k steps, and while remaining in states in @{code remain}.
+	 * within k steps, and while remaining in states in {@code remain}.
 	 * @param stpg The STPG
 	 * @param remain Remain in these states (optional: null means "all")
 	 * @param target Target states
@@ -746,7 +750,7 @@ public class STPGModelChecker extends ProbModelChecker
 	{
 		ModelCheckerResult res = null;
 		BitSet inf;
-		int i, n, numTarget, numInf;
+		int n, numTarget, numInf;
 		long timer, timerProb1;
 
 		// Start expected reachability
@@ -761,10 +765,12 @@ public class STPGModelChecker extends ProbModelChecker
 		n = stpg.getNumStates();
 
 		// Optimise by enlarging target set (if more info is available)
-		if (init != null && known != null) {
-			BitSet targetNew = new BitSet(n);
-			for (i = 0; i < n; i++) {
-				targetNew.set(i, target.get(i) || (known.get(i) && init[i] == 0.0));
+		if (init != null && known != null && !known.isEmpty()) {
+			BitSet targetNew = (BitSet) target.clone();
+			for (int i : new IterableBitSet(known)) {
+				if (init[i] == 1.0) {
+					targetNew.set(i);
+				}
 			}
 			target = targetNew;
 		}