Fix in RelOp - we cannot tell whether it is numerical without the bound (= could be =? or =1 (in theory at least)).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8626 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/parser/ast/RelOp.java

@@ -74,20 +74,6 @@ public enum RelOp {
 		}
 	}
 
-	/**
-	 * Returns true if this is numerical (e.g. min=?, max=?).
-	 */
-	public boolean isNumerical()
-	{
-		switch (this) {
-		case MIN:
-		case MAX:
-			return true;
-		default:
-			return false;
-		}
-	}
-
 	/**
 	 * Returns true if this corresponds to minimum (min=?).
 	 */

prism/src/pta/PTAModelChecker.java

@@ -191,7 +191,7 @@ public class PTAModelChecker extends PrismComponent
 
 		// Check whether Pmin=? or Pmax=? (only two cases allowed)
 		RelOp relOp = expr.getRelOp();
-		if (!relOp.isNumerical()) {
+		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();