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()) {