imported patch min-max-new-min-max-check.patch

prism/src/explicit/MinMax.java

@@ -82,6 +82,24 @@ public class MinMax
 		return neg;
 	}
 	
+	public String toString()
+	{
+		if (min) {
+			return "min";
+		} else {
+			return "max";
+		}
+	}
+	
+	public MinMax clone()
+	{
+		MinMax result = new MinMax();
+		result.min = min;
+		result.min1 = min1;
+		result.min2 = min2;
+		return result;
+	}
+	
 	// Utility methods to create instances of this class
 	
 	public static MinMax blank()

prism/src/param/ParamModelChecker.java

@@ -91,6 +91,7 @@ import parser.type.TypeInt;
 import parser.type.TypePathBool;
 import parser.type.TypePathDouble;
 import prism.ModelType;
+import prism.OpRelOpBound;
 import prism.PrismComponent;
 import prism.PrismException;
 import prism.PrismSettings;
@@ -918,7 +919,9 @@ final public class ParamModelChecker extends PrismComponent
 			if (p.compareTo(0) == -1 || p.compareTo(1) == 1)
 				throw new PrismException("Invalid probability bound " + p + " in P operator");
 		}
-		min = relOp.isLowerBound() || relOp.isMin();
+		// Get info from P operator
+		OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues);
+		min = opInfo.getMinMax(modelType).isMin();
 
 		// Compute probabilities
 		if (!expr.getExpression().isSimplePathFormula()) {
@@ -1029,7 +1032,9 @@ final public class ParamModelChecker extends PrismComponent
 			if (r.compareTo(0) == -1)
 				throw new PrismException("Invalid reward bound " + r + " in R[] formula");
 		}
-		min = relOp.isLowerBound() || relOp.isMin();
+		// Get info from R operator
+		OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues);
+		min = opInfo.getMinMax(model.getModelType()).isMin();
 
 		ParamRewardStruct rew = constructRewards(model, rewStruct, constantValues);
 		mainLog.println("Building reward structure...");
@@ -1186,7 +1191,9 @@ final public class ParamModelChecker extends PrismComponent
 			if (p.compareTo(0) == -1 || p.compareTo(1) == 1)
 				throw new PrismException("Invalid probability bound " + p + " in P operator");
 		}
-		min = relOp.isLowerBound() || relOp.isMin();
+		// Get info from SS operator
+		OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues);
+		min = opInfo.getMinMax(modelType).isMin();
 
 		// Compute probabilities
 		probs = checkProbSteadyState(model, expr.getExpression(), min, needStates);

prism/src/parser/ast/ExpressionProb.java

@@ -86,9 +86,9 @@ public class ExpressionProb extends ExpressionQuant
 			double boundVal = getBound().evaluateDouble(constantValues);
 			if (boundVal < 0 || boundVal > 1)
 				throw new PrismLangException("Invalid probability bound " + boundVal + " in P operator");
-			return new OpRelOpBound("P", getRelOp(), boundVal);
+			return new OpRelOpBound("P", minMax, getRelOp(), boundVal);
 		} else {
-			return new OpRelOpBound("P", getRelOp(), null);
+			return new OpRelOpBound("P", minMax, getRelOp(), null);
 		}
 	}
 	
@@ -123,11 +123,15 @@ public class ExpressionProb extends ExpressionQuant
 	{
 		if (getBound() != null)
 			return "Result";
-		else if (getRelOp() == RelOp.MIN)
+		else if (getRelOp() == RelOp.EQ) {
+			if (minMax != null) {
+				if (minMax.isMin()) {
 					return "Minimum probability";
-		else if (getRelOp() == RelOp.MAX)
+				} else {
 					return "Maximum probability";
-		else
+				}
+			}
+		}
 		return "Probability";
 	}
 
@@ -150,6 +154,7 @@ public class ExpressionProb extends ExpressionQuant
 	{
 		ExpressionProb expr = new ExpressionProb();
 		expr.setExpression(getExpression() == null ? null : getExpression().deepCopy());
+		expr.setMinMax(minMax != null ? minMax.clone() : null);
 		expr.setRelOp(getRelOp());
 		expr.setBound(getBound() == null ? null : getBound().deepCopy());
 		expr.setFilter(getFilter() == null ? null : (Filter)getFilter().deepCopy());
@@ -165,7 +170,9 @@ public class ExpressionProb extends ExpressionQuant
 	{
 		String s = "";
 
-		s += "P" + getModifierString() + getRelOp();
+		s += "P" + getModifierString();
+		s += (minMax != null ? minMax : "");
+		s+= getRelOp();
 		s += (getBound() == null) ? "?" : getBound().toString();
 		s += " [ " + getExpression();
 		if (getFilter() != null)

prism/src/parser/ast/ExpressionQuant.java

@@ -26,6 +26,7 @@
 
 package parser.ast;
 
+import explicit.MinMax;
 import parser.Values;
 import prism.OpRelOpBound;
 import prism.PrismException;
@@ -38,6 +39,8 @@ public abstract class ExpressionQuant extends Expression
 {
 	/** Optional "modifier" to specify variants of the P/R/S operator */
 	protected String modifier = null;
+	/** The attached min/max operator, if it exists */
+	protected MinMax minMax = null;
 	/** The attached relational operator (e.g. "<" in "P<0.1"). */
 	protected RelOp relOp = null;
 	/** The attached (probability/reward) bound, as an expression (e.g. "p" in "P<p"). Null if absent (e.g. "P=?"). */
@@ -58,6 +61,23 @@ public abstract class ExpressionQuant extends Expression
 		this.modifier = modifier;
 	}
 
+	public void setMinMax(MinMax minMax)
+	{
+		this.minMax = minMax;
+	}
+	
+	/** Set the attached min/max operator */
+	public void setMinMax(String minMaxString) throws PrismException
+	{
+		if (minMaxString.equals("min")) {
+			minMax = MinMax.min();
+		} else if (minMaxString.equals("max")) {
+			minMax = MinMax.max();
+		} else {
+			throw new PrismException("Min/Max has to be either min or max");
+		}
+	}
+
 	/**
 	 * Set the attached relational operator (e.g. "<" in "P<0.1").
 	 * Uses the enum {@link RelOp}. For example: {@code setRelOp(RelOp.GT);}
@@ -119,6 +139,12 @@ public abstract class ExpressionQuant extends Expression
 		return modifier == null ? "" : "(" + modifier + ")";
 	}
 
+	/** Get the optional MinMax operator */
+	public MinMax getMinMax()
+	{
+		return minMax;
+	}
+
 	/**
 	 * Get the attached relational operator (e.g. "<" in "P<0.1"), as a {@link RelOp}.
 	 */

prism/src/parser/ast/ExpressionReward.java

@@ -197,9 +197,9 @@ public class ExpressionReward extends ExpressionQuant
 	{
 		if (getBound() != null) {
 			double boundValue = getBound().evaluateDouble(constantValues);
-			return new OpRelOpBound("R", getRelOp(), boundValue);
+			return new OpRelOpBound("R", minMax, getRelOp(), boundValue);
 		} else {
-			return new OpRelOpBound("R", getRelOp(), null);
+			return new OpRelOpBound("R", minMax, getRelOp(), null);
 		}
 	}
 	
@@ -246,8 +246,10 @@ public class ExpressionReward extends ExpressionQuant
 		// For R=? properties, use name of reward structure where applicable
 		if (getBound() == null) {
 			String s = "E";
-			if (getRelOp() == RelOp.MIN) s = "Minimum e";
-			else if (getRelOp() == RelOp.MAX) s = "Maximum e";
+			if (minMax != null) {
+				if (minMax.isMin()) s = "Minimum e";
+				else s = "Maximum e";
+			}
 			else s = "E";
 			if (rewardStructIndex instanceof String) {
 				if (rewardStructIndexDiv instanceof String)
@@ -287,6 +289,7 @@ public class ExpressionReward extends ExpressionQuant
 		ExpressionReward expr = new ExpressionReward();
 		expr.setExpression(getExpression() == null ? null : getExpression().deepCopy());
 		expr.setRelOp(getRelOp());
+		expr.setMinMax(minMax == null ? null : minMax.clone() );
 		expr.setBound(getBound() == null ? null : getBound().deepCopy());
 		if (rewardStructIndex != null && rewardStructIndex instanceof Expression) expr.setRewardStructIndex(((Expression)rewardStructIndex).deepCopy());
 		else expr.setRewardStructIndex(rewardStructIndex);
@@ -315,6 +318,7 @@ public class ExpressionReward extends ExpressionQuant
 				else if (rewardStructIndexDiv instanceof String) s += "{\""+rewardStructIndexDiv+"\"}";
 			}
 		}
+		s += (getMinMax()==null) ? "" : getMinMax();
 		s += getRelOp();
 		s += (getBound()==null) ? "?" : getBound().toString();
 		s += " [ " + getExpression();

prism/src/parser/ast/ExpressionSS.java

@@ -80,9 +80,9 @@ public class ExpressionSS extends ExpressionQuant
 			double boundValue = getBound().evaluateDouble(constantValues);
 			if (boundValue < 0 || boundValue > 1)
 				throw new PrismException("Invalid probability bound " + boundValue + " in P operator");
-			return new OpRelOpBound("S", getRelOp(), boundValue);
+			return new OpRelOpBound("S", minMax, getRelOp(), boundValue);
 		} else {
-			return new OpRelOpBound("S", getRelOp(), null);
+			return new OpRelOpBound("S", minMax, getRelOp(), null);
 		}
 	}
 	

prism/src/parser/ast/RelOp.java

@@ -39,19 +39,6 @@ public enum RelOp
 			return (keepStrictness ? LEQ : LT);
 		}
 	},
-	MIN("min=") {
-		@Override
-		public boolean isMin()
-		{
-			return true;
-		}
-
-		@Override
-		public RelOp negate(boolean keepStrictness) throws PrismLangException
-		{
-			return MAX;
-		}
-	},
 	LT("<") {
 		@Override
 		public boolean isUpperBound()
@@ -84,19 +71,6 @@ public enum RelOp
 			return (keepStrictness ? GEQ : GT);
 		}
 	},
-	MAX("max=") {
-		@Override
-		public boolean isMax()
-		{
-			return true;
-		}
-
-		@Override
-		public RelOp negate(boolean keepStrictness) throws PrismLangException
-		{
-			return MIN;
-		}
-	},
 	EQ("=") {
 		@Override
 		public RelOp negate(boolean keepStrictness) throws PrismLangException
@@ -120,7 +94,6 @@ public enum RelOp
 
 	/**
 	 * Returns true if this corresponds to a lower bound (i.e. &gt;, &gt;=).
-	 * NB: "min=?" does not return true for this.
 	 */
 	public boolean isLowerBound()
 	{
@@ -129,7 +102,6 @@ public enum RelOp
 
 	/**
 	 * Returns true if this corresponds to an upper bound (i.e. &lt;, &lt;=).
-	 * NB: "max=?" does not return true for this.
 	 */
 	public boolean isUpperBound()
 	{
@@ -144,22 +116,6 @@ public enum RelOp
 		return false;
 	}
 
-	/**
-	 * Returns true if this corresponds to minimum (min=?).
-	 */
-	public boolean isMin()
-	{
-		return false;
-	}
-
-	/**
-	 * Returns true if this corresponds to maximum (max=?).
-	 */
-	public boolean isMax()
-	{
-		return false;
-	}
-
 	/**
 	 * Returns the negated form of this operator.
 	 * <br>

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)
+		if (modelType.nondeterministic() && e.getRelOp() == RelOp.EQ && 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)
+		if (modelType.nondeterministic() && e.getRelOp() == RelOp.EQ && 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

@@ -42,6 +42,7 @@ import jdd.JDDVars;
 import mtbdd.PrismMTBDD;
 import parser.ast.Expression;
 import parser.ast.RelOp;
+import explicit.MinMax;
 import sparse.NDSparseMatrix;
 import sparse.PrismSparse;
 import acceptance.AcceptanceRabin;
@@ -271,7 +272,7 @@ public class MultiObjModelChecker extends PrismComponent
 									opsAndBounds.getProbStepBound(i), i);
 						}
 					}
-					tmpOpsAndBounds.add(new OpRelOpBound("R", RelOp.MAX, -1.0), Operator.R_MAX, -1.0, -1, opsAndBounds.probSize());
+					tmpOpsAndBounds.add(new OpRelOpBound("R", MinMax.max(), RelOp.EQ, -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,16 +838,21 @@ public class NondetModelChecker extends NonProbModelChecker
 		if (relOp.isStrict()) {
 			throw new PrismException("Multi-objective properties can not use strict inequalities on P/R operators");
 		}
-		Operator op;
-		if (relOp == RelOp.MAX) {
+		Operator op = null;
+		if (relOp == RelOp.EQ) {
+			if (exprQuant.getMinMax() != null) {
+				if (exprQuant.getMinMax().isMax()) {
 					op = (exprProb != null) ? Operator.P_MAX : Operator.R_MAX;
+				} else {
+					op = (exprProb != null) ? Operator.P_MIN : Operator.R_MIN;
+				}
+			}
 		} else if (relOp == RelOp.GEQ) {
 			op = (exprProb != null) ? Operator.P_GE : Operator.R_GE;
-		} else if (relOp == RelOp.MIN) {
-			op = (exprProb != null) ? Operator.P_MIN : Operator.R_MIN;
 		} else if (relOp == RelOp.LEQ) {
 			op = (exprProb != null) ? Operator.P_LE : Operator.R_LE;
-		} else {
+		}
+		if (op == null) {
 			throw new PrismException("Multi-objective properties can only contain P/R operators with max/min=? or lower/upper probability bounds");
 		}
 		// Find bound
@@ -876,7 +881,7 @@ public class NondetModelChecker extends NonProbModelChecker
 		for (JDDNode set : tmpecs)
 			acceptingStates = JDD.Or(acceptingStates, set);
 		targetDDs.add(acceptingStates);
-		OpRelOpBound opInfo = new OpRelOpBound("P", RelOp.GEQ, 0.0);
+		OpRelOpBound opInfo = new OpRelOpBound("P", null, RelOp.GEQ, 0.0);
 		opsAndBounds.add(opInfo, Operator.P_GE, 0.0, -1, -1);
 	}
 

prism/src/prism/OpRelOpBound.java

@@ -36,12 +36,14 @@ public class OpRelOpBound
 {
 	protected String op;
 	protected RelOp relOp;
+	protected MinMax minMax;
 	protected boolean numeric;
 	protected double bound;
 
-	public OpRelOpBound(String op, RelOp relOp, Double boundObject)
+	public OpRelOpBound(String op, MinMax minMax, RelOp relOp, Double boundObject)
 	{
 		this.op = op;
+		this.minMax = minMax;
 		this.relOp = relOp;
 		numeric = (boundObject == null);
 		if (boundObject != null)
@@ -73,6 +75,11 @@ public class OpRelOpBound
 		return bound;
 	}
 
+	public boolean hasExplicitMinMax()
+	{
+		return minMax != null;
+	}
+
 	public boolean isQualitative()
 	{
 		return !isNumeric() && op.equals("P") && (bound == 0 || bound == 1);
@@ -111,7 +118,12 @@ public class OpRelOpBound
 
 	public MinMax getMinMax(ModelType modelType, boolean forAll) throws PrismLangException
 	{
+		if (this.minMax != null) {
+			return this.minMax;
+		}
+
 		MinMax minMax = MinMax.blank();
+
 		if (modelType.nondeterministic()) {
 			if (!(modelType == ModelType.MDP || modelType == ModelType.POMDP || modelType == ModelType.CTMDP)) {
 				throw new PrismLangException("Don't know how to model check " + getTypeOfOperator() + " properties for " + modelType + "s");
@@ -120,7 +132,6 @@ public class OpRelOpBound
 				if (relOp == RelOp.EQ) {
 					throw new PrismLangException("Can't use \"" + op + "=?\" for nondeterministic models; use e.g. \"" + op + "min=?\" or \"" + op + "max=?\"");
 				}
-				minMax = relOp.isMin() ? MinMax.min() : MinMax.max();
 			} else {
 				if (forAll) {
 					minMax = (relOp.isLowerBound() ) ? MinMax.min() : MinMax.max();

prism/src/prism/ProbModelChecker.java

@@ -187,7 +187,7 @@ public class ProbModelChecker extends NonProbModelChecker
 		}
 
 		// Print a warning if Pmin/Pmax used
-		if (opInfo.getRelOp() == RelOp.MIN || opInfo.getRelOp() == RelOp.MAX) {
+		if (opInfo.hasExplicitMinMax()) {
 			mainLog.printWarning("\"Pmin=?\" and \"Pmax=?\" operators are identical to \"P=?\" for DTMCs/CTMCs");
 		}
 
@@ -235,7 +235,7 @@ public class ProbModelChecker extends NonProbModelChecker
 		JDDNode transRewards = getTransitionRewardsByIndexObject(rs, model, constantValues);
 
 		// Print a warning if Rmin/Rmax used
-		if (opInfo.getRelOp() == RelOp.MIN || opInfo.getRelOp() == RelOp.MAX) {
+		if (opInfo.hasExplicitMinMax()) {
 			mainLog.printWarning("\"Rmin=?\" and \"Rmax=?\" operators are identical to \"R=?\" for DTMCs/CTMCs");
 		}
 

prism/src/pta/PTAModelChecker.java

@@ -194,7 +194,9 @@ public class PTAModelChecker extends PrismComponent
 		if (expr.getProb() != null) {
 			throw new PrismException("PTA model checking currently only supports Pmin=? and Pmax=? properties (try the digital clocks engine instead)");
 		}
-		min = relOp.isLowerBound() || relOp.isMin();
+		// Get info from P operator
+		OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues);
+		min = opInfo.getMinMax(ModelType.PTA).isMin();
 
 		// Check this is a F path property (only case allowed at the moment)
 		if (!(expr.getExpression() instanceof ExpressionTemporal))