imported patch min-max-min-max-2.patch

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";

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
 		{

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");

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<JDDNode> tmprewards = new ArrayList<JDDNode>(1);
 					tmprewards.add(rtarget);

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;

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 {