imported patch min-max--multi-protect-against-explicitMinMax.patch

7 years ago · 774edd1dbf
1 changed files with 3 additions and 0 deletions
--- 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()) {