Browse Source

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

tud-infrastructure-2018-10-12
Joachim Klein 7 years ago
parent
commit
12174ee937
  1. 3
      prism/src/prism/NondetModelChecker.java

3
prism/src/prism/NondetModelChecker.java

@ -838,6 +838,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()) {

Loading…
Cancel
Save