diff --git a/prism/src/parser/ast/ExpressionProb.java b/prism/src/parser/ast/ExpressionProb.java index 5254a0b0..c3032c47 100644 --- a/prism/src/parser/ast/ExpressionProb.java +++ b/prism/src/parser/ast/ExpressionProb.java @@ -123,7 +123,7 @@ public class ExpressionProb extends ExpressionQuant { if (getBound() != null) return "Result"; - else if (getRelOp() == RelOp.EQ) { + else if (getRelOp() == RelOp.COMPUTE_VALUES) { if (minMax != null) { if (minMax.isMin()) { return "Minimum probability"; diff --git a/prism/src/parser/ast/RelOp.java b/prism/src/parser/ast/RelOp.java index 4c112798..a3aef3cf 100644 --- a/prism/src/parser/ast/RelOp.java +++ b/prism/src/parser/ast/RelOp.java @@ -71,7 +71,7 @@ public enum RelOp return (keepStrictness ? GEQ : GT); } }, - EQ("=") { + COMPUTE_VALUES("=") { @Override public RelOp negate(boolean keepStrictness) throws PrismLangException { diff --git a/prism/src/parser/visitor/CheckValid.java b/prism/src/parser/visitor/CheckValid.java index 549bc34c..11310fb0 100644 --- a/prism/src/parser/visitor/CheckValid.java +++ b/prism/src/parser/visitor/CheckValid.java @@ -99,13 +99,13 @@ public class CheckValid extends ASTTraverse public void visitPost(ExpressionProb e) throws PrismLangException { - if (modelType.nondeterministic() && e.getRelOp() == RelOp.EQ && e.getMinMax() == null) + if (modelType.nondeterministic() && e.getRelOp() == RelOp.COMPUTE_VALUES && e.getMinMax() == null) throw new PrismLangException("Can't use \"P=?\" for nondeterministic models; use \"Pmin=?\" or \"Pmax=?\""); } public void visitPost(ExpressionReward e) throws PrismLangException { - if (modelType.nondeterministic() && e.getRelOp() == RelOp.EQ && e.getMinMax() == null) + if (modelType.nondeterministic() && e.getRelOp() == RelOp.COMPUTE_VALUES && e.getMinMax() == null) throw new PrismLangException("Can't use \"R=?\" for nondeterministic models; use \"Rmin=?\" or \"Rmax=?\""); if (e.getRewardStructIndexDiv() != null) throw new PrismLangException("No support for ratio reward objectives yet"); diff --git a/prism/src/prism/MultiObjModelChecker.java b/prism/src/prism/MultiObjModelChecker.java index 8fd4a5da..a9fa0506 100644 --- a/prism/src/prism/MultiObjModelChecker.java +++ b/prism/src/prism/MultiObjModelChecker.java @@ -272,7 +272,7 @@ public class MultiObjModelChecker extends PrismComponent opsAndBounds.getProbStepBound(i), i); } } - tmpOpsAndBounds.add(new OpRelOpBound("R", MinMax.max(), RelOp.EQ, -1.0), Operator.R_MAX, -1.0, -1, opsAndBounds.probSize()); + tmpOpsAndBounds.add(new OpRelOpBound("R", MinMax.max(), RelOp.COMPUTE_VALUES, -1.0), Operator.R_MAX, -1.0, -1, opsAndBounds.probSize()); ArrayList tmprewards = new ArrayList(1); tmprewards.add(rtarget); diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index ade0ea76..638fc3d4 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -838,7 +838,7 @@ 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.EQ) { + if (relOp == RelOp.COMPUTE_VALUES) { if (exprQuant.getMinMax() != null) { if (exprQuant.getMinMax().isMax()) { op = (exprProb != null) ? Operator.P_MAX : Operator.R_MAX; diff --git a/prism/src/prism/OpRelOpBound.java b/prism/src/prism/OpRelOpBound.java index dbc33a5e..17e14aa0 100644 --- a/prism/src/prism/OpRelOpBound.java +++ b/prism/src/prism/OpRelOpBound.java @@ -103,7 +103,7 @@ public class OpRelOpBound throw new PrismLangException("Don't know how to model check " + getTypeOfOperator() + " properties for " + modelType + "s"); } if (isNumeric()) { - if (relOp == RelOp.EQ) { + if (relOp == RelOp.COMPUTE_VALUES) { throw new PrismLangException("Can't use \"" + op + "=?\" for nondeterministic models; use e.g. \"" + op + "min=?\" or \"" + op + "max=?\""); } } else {