From 533d7d94256c30fe3e4a261396a9d4195926583c Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 19 Feb 2010 23:12:20 +0000
Subject: [PATCH] Bugfixes: loops (esp. bounded until) in explicit mc.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1756 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/explicit/MDP.java  | 38 +++++++++++++++++++++---------------
 prism/src/explicit/STPG.java | 19 ++++++++++--------
 2 files changed, 33 insertions(+), 24 deletions(-)

diff --git a/prism/src/explicit/MDP.java b/prism/src/explicit/MDP.java
index 36539356..18b3c6f6 100644
--- a/prism/src/explicit/MDP.java
+++ b/prism/src/explicit/MDP.java
@@ -423,14 +423,17 @@ public class MDP extends Model
 	 */
 	public void mvMultMinMax(double vect[], boolean min, double result[], BitSet subset, boolean complement)
 	{
-		int s = -1;
-		while (s < numStates) {
-			// Pick next state
-			s = (subset == null) ? s + 1 : complement ? subset.nextClearBit(s + 1) : subset.nextSetBit(s + 1);
-			if (s < 0)
-				break;
-			// Do operation
-			result[s] = mvMultMinMaxSingle(s, vect, min);
+		int s;
+		// Loop depends on subset/complement arguments
+		if (subset == null) {
+			for (s = 0; s < numStates; s++)
+				result[s] = mvMultMinMaxSingle(s, vect, min);
+		} else if (complement) {
+			for (s = subset.nextClearBit(0); s < numStates; s = subset.nextClearBit(s + 1))
+				result[s] = mvMultMinMaxSingle(s, vect, min);
+		} else {
+			for (s = subset.nextSetBit(0); s >= 0; s = subset.nextSetBit(s + 1))
+				result[s] = mvMultMinMaxSingle(s, vect, min);
 		}
 	}
 
@@ -516,14 +519,17 @@ public class MDP extends Model
 	 */
 	public void mvMultRewMinMax(double vect[], boolean min, double result[], BitSet subset, boolean complement)
 	{
-		int s = -1;
-		while (s < numStates) {
-			// Pick next state
-			s = (subset == null) ? s + 1 : complement ? subset.nextClearBit(s + 1) : subset.nextSetBit(s + 1);
-			if (s < 0)
-				break;
-			// Do operation
-			result[s] = mvMultRewMinMaxSingle(s, vect, min);
+		int s;
+		// Loop depends on subset/complement arguments
+		if (subset == null) {
+			for (s = 0; s < numStates; s++)
+				result[s] = mvMultRewMinMaxSingle(s, vect, min);
+		} else if (complement) {
+			for (s = subset.nextClearBit(0); s < numStates; s = subset.nextClearBit(s + 1))
+				result[s] = mvMultRewMinMaxSingle(s, vect, min);
+		} else {
+			for (s = subset.nextSetBit(0); s >= 0; s = subset.nextSetBit(s + 1))
+				result[s] = mvMultRewMinMaxSingle(s, vect, min);
 		}
 	}
 
diff --git a/prism/src/explicit/STPG.java b/prism/src/explicit/STPG.java
index 621c5243..0030e91f 100644
--- a/prism/src/explicit/STPG.java
+++ b/prism/src/explicit/STPG.java
@@ -452,14 +452,17 @@ public class STPG extends Model
 	public void mvMultMinMax(double vect[], boolean min1, boolean min2, double result[], BitSet subset,
 			boolean complement)
 	{
-		int s = -1;
-		while (s < numStates) {
-			// Pick next state
-			s = (subset == null) ? s + 1 : complement ? subset.nextClearBit(s + 1) : subset.nextSetBit(s + 1);
-			if (s < 0)
-				break;
-			// Do operation
-			result[s] = mvMultMinMaxSingle(s, vect, min1, min2);
+		int s;
+		// Loop depends on subset/complement arguments
+		if (subset == null) {
+			for (s = 0; s < numStates; s++)
+				result[s] = mvMultMinMaxSingle(s, vect, min1, min2);
+		} else if (complement) {
+			for (s = subset.nextClearBit(0); s < numStates; s = subset.nextClearBit(s + 1))
+				result[s] = mvMultMinMaxSingle(s, vect, min1, min2);
+		} else {
+			for (s = subset.nextSetBit(0); s >= 0; s = subset.nextSetBit(s + 1))
+				result[s] = mvMultMinMaxSingle(s, vect, min1, min2);
 		}
 	}