From 6daac6fec2374f6638f3d94eea88978886d75347 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 12 Oct 2018 14:25:59 +0200 Subject: [PATCH] imported patch rewardcounter-IntegerBounds.getMaximalInterestingValueForConjunction.patch --- prism/src/prism/IntegerBound.java | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/prism/src/prism/IntegerBound.java b/prism/src/prism/IntegerBound.java index f9d746da..4bd87b38 100644 --- a/prism/src/prism/IntegerBound.java +++ b/prism/src/prism/IntegerBound.java @@ -26,6 +26,8 @@ package prism; +import java.util.List; + import parser.Values; import parser.ast.ExpressionTemporal; import parser.ast.TemporalOperatorBound; @@ -249,6 +251,25 @@ public class IntegerBound } } + + /** + * Returns the maximal interesting value when considering the conjunction of {@code bounds}. + * @param bounds list of bounds + * @return the maximum over the maximal interesting values of {@code bounds} + */ + public static int getMaximalInterestingValueForConjunction(List bounds) { + int saturation = 0; + + for (IntegerBound bound : bounds) { + int bound_saturation = bound.getMaximalInterestingValue(); + if (bound_saturation > saturation) { + saturation = bound_saturation; + } + } + + return saturation; + } + public static void main(String args[]) { System.out.println(new IntegerBound(1, true, 3, false));