From 774edd1dbf82df5d8ac00ff3eab171d1397b47b8 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 12 Oct 2018 14:26:19 +0200
Subject: [PATCH] imported patch
 min-max--multi-protect-against-explicitMinMax.patch

---
 prism/src/prism/NondetModelChecker.java | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java
index df754bc2..099b2b4b 100644
--- a/prism/src/prism/NondetModelChecker.java
+++ b/prism/src/prism/NondetModelChecker.java
@@ -839,6 +839,9 @@ public class NondetModelChecker extends NonProbModelChecker
 			throw new PrismException("Multi-objective properties can not use strict inequalities on P/R operators");
 		}
 		Operator op = null;
+		if (relOp != RelOp.COMPUTE_VALUES && opInfo.hasExplicitMinMax()) {
+			throw new PrismException("Multi-objective properties can not contain P/R operators with max/min and bounds");
+		}
 		if (relOp == RelOp.COMPUTE_VALUES) {
 			if (exprQuant.getMinMax() != null) {
 				if (exprQuant.getMinMax().isMax()) {