From aa11fa528b088071dcaa0c816a363c0fdd0f0b0b Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 27 Jun 2014 13:32:46 +0000
Subject: [PATCH] =?UTF-8?q?Fix=20in=20RelOp=20-=20we=20cannot=20tell=20whe?=
 =?UTF-8?q?ther=20it=20is=20numerical=20without=20the=20bound=20(=3D=20cou?=
 =?UTF-8?q?ld=20be=20=3D=3F=20or=20=3D1=20(in=20theory=20at=20least)).?=

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8626 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/parser/ast/RelOp.java    | 14 --------------
 prism/src/pta/PTAModelChecker.java |  2 +-
 2 files changed, 1 insertion(+), 15 deletions(-)

diff --git a/prism/src/parser/ast/RelOp.java b/prism/src/parser/ast/RelOp.java
index a532c8cc..4608e38c 100644
--- a/prism/src/parser/ast/RelOp.java
+++ b/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=?).
 	 */
diff --git a/prism/src/pta/PTAModelChecker.java b/prism/src/pta/PTAModelChecker.java
index b704416b..785bf8c8 100644
--- a/prism/src/pta/PTAModelChecker.java
+++ b/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();