imported patch rewardcounter-CounterProduct.getStatesWithAccumulatedRewardInBoundConjunction.patch

prism/src/explicit/CounterProduct.java

@@ -28,6 +28,7 @@ package explicit;
 
 import java.util.ArrayList;
 import java.util.BitSet;
+import java.util.List;
 
 import common.SafeCast;
 
@@ -157,6 +158,20 @@ public class CounterProduct<M extends Model> extends ProductWithProductStates<M>
 	}
 
 
+	/**
+	 * Get the states in the product DTMC inside the conjunction of integer bounds,
+	 * given as a List of IntegerBounds.
+	 */
+	BitSet getStatesWithAccumulatedRewardInBoundConjunction(List<IntegerBound> bounds) {
+		BitSet result = new BitSet();
+		for (int r=0; r<=limit; r++) {
+			if (IntegerBound.isInBoundForConjunction(bounds, r)) {
+				result.or(getStatesWithAccumulatedReward(r));
+			}
+		}
+		return result;
+	}
+
 	/**
 	 * Generate the product of a DTMC with an accumulated reward counter.
 	 * The counter has the range [0,limit], with saturation semantics for accumulated