From 31d10dfd1cd913d1a5341172afc094824a811047 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 12 Oct 2018 14:26:01 +0200
Subject: [PATCH] imported patch
 rewardcounter-CounterProduct.getStatesWithAccumulatedRewardInBoundConjunction.patch

---
 prism/src/explicit/CounterProduct.java | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/prism/src/explicit/CounterProduct.java b/prism/src/explicit/CounterProduct.java
index 2904305c..6f09cacc 100644
--- a/prism/src/explicit/CounterProduct.java
+++ b/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