From f1881a61e006c172fa7718fa3113ae33b31feaf3 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 12 Oct 2018 14:25:58 +0200
Subject: [PATCH] imported patch
 rewardcounter-TemporalBound.hasSameDomain.patch

---
 .../src/parser/ast/TemporalOperatorBound.java | 44 +++++++++++++++++++
 1 file changed, 44 insertions(+)

diff --git a/prism/src/parser/ast/TemporalOperatorBound.java b/prism/src/parser/ast/TemporalOperatorBound.java
index c41bf17e..d6d389f3 100644
--- a/prism/src/parser/ast/TemporalOperatorBound.java
+++ b/prism/src/parser/ast/TemporalOperatorBound.java
@@ -143,6 +143,50 @@ public class TemporalOperatorBound extends ASTElement {
 		return uBoundStrict;
 	}
 
+	/**
+	 * Returns true if this TemporalOperatorBound has the same domain
+	 * as {@other}, in the discrete time setting (step = time bound).
+	 * <br>
+	 * Requires that the reward structure index (for reward bounds)
+	 * has already been resolved, i.e., that {@code setRewardStruct()}
+	 * has been called.
+	 */
+	public boolean hasSameDomainDiscreteTime(TemporalOperatorBound other) {
+		if (boundType == BoundType.REWARD_BOUND) {
+			if (getResolvedRewardStructIndex() == null || other.getResolvedRewardStructIndex() == null) {
+				throw new IllegalStateException("Invalid operation: TemporalOperatorBound.hasSameDomainDiscreteTime() requires that reward structures have already been resolved");
+			}
+			return other.getBoundType() == boundType && getResolvedRewardStructIndex() == other.getResolvedRewardStructIndex();
+		} else {
+			// STEP = TIME = DEFAULT
+			return other.getBoundType() == BoundType.DEFAULT_BOUND ||
+			       other.getBoundType() == BoundType.STEP_BOUND ||
+			       other.getBoundType() == BoundType.TIME_BOUND;
+		}
+	}
+
+	/**
+	 * Returns true if this TemporalOperatorBound has the same domain
+	 * as {@other}, in the continuous time setting (step != time bound).
+ 	 * <br>
+	 * Requires that the reward structure index (for reward bounds)
+	 * has already been resolved, i.e., that {@code setRewardStruct()}
+	 * has been called.
+	 */
+	public boolean hasSameDomainContinuousTime(TemporalOperatorBound other) {
+		if (boundType == BoundType.REWARD_BOUND) {
+			if (getResolvedRewardStructIndex() == null || other.getResolvedRewardStructIndex() == null) {
+				throw new IllegalStateException("Invalid operation: TemporalOperatorBound.hasSameDomainContinuousTime() requires that reward structures have already been resolved");
+			}
+			return other.getBoundType() == boundType && getResolvedRewardStructIndex() == other.getResolvedRewardStructIndex();
+		} else if (boundType == BoundType.TIME_BOUND) {
+			return other.getBoundType() == BoundType.TIME_BOUND ||
+			       other.getBoundType() == BoundType.DEFAULT_BOUND;
+		} else {
+			return other.getBoundType() ==  BoundType.STEP_BOUND;
+		}
+	}
+
 	/**
 	 * Returns true if lower/upper bound are equal and should be displayed as =T
 	 */