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