From a2aee2fa364d13ca8bf10e1be3356a373a42610b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffen=20M=C3=A4rcker?= Date: Wed, 16 May 2018 10:45:43 +0200 Subject: [PATCH] Implement round function --- prism/src/explicit/StateModelChecker.java | 1 + prism/src/explicit/StateValues.java | 22 ++++++++++ prism/src/param/BigRational.java | 18 ++++++++ prism/src/parser/ast/ExpressionFunc.java | 53 +++++++++++++++++------ prism/src/parser/visitor/TypeCheck.java | 2 + prism/src/prism/StateModelChecker.java | 10 +++++ 6 files changed, 93 insertions(+), 13 deletions(-) diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index 0adf1077..ea173be7 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -738,6 +738,7 @@ public class StateModelChecker extends PrismComponent return checkExpressionFuncNary(model, expr, statesOfInterest); case ExpressionFunc.FLOOR: case ExpressionFunc.CEIL: + case ExpressionFunc.ROUND: return checkExpressionFuncUnary(model, expr, statesOfInterest); case ExpressionFunc.POW: case ExpressionFunc.MOD: diff --git a/prism/src/explicit/StateValues.java b/prism/src/explicit/StateValues.java index 56663ba4..f0566de1 100644 --- a/prism/src/explicit/StateValues.java +++ b/prism/src/explicit/StateValues.java @@ -1014,6 +1014,9 @@ public class StateValues implements StateVector case ExpressionFunc.CEIL: ceil(); break; + case ExpressionFunc.ROUND: + round(); + break; default: throw new PrismException("Unknown unary function"); } @@ -1057,6 +1060,25 @@ public class StateValues implements StateVector } } + /** + * Modify the vector by applying 'round'. + */ + public void round() throws PrismException + { + if (type instanceof TypeInt) { + // Nothing to do + } else if (type instanceof TypeDouble) { + valuesI = new int[size]; + type = TypeInt.getInstance(); + for (int i = 0; i < size; i++) { + valuesI[i] = ExpressionFunc.evaluateRound(valuesD[i]); + } + valuesD = null; + } else { + throw new PrismException("Function round cannot be applied to Boolean vectors"); + } + } + /** * Modify the vector by applying (binary or N-ary) function {@code op} with second operand {@code sv}, * where {@code op} refers to the codes in {@link parser.ast.ExpressionFunc}. diff --git a/prism/src/param/BigRational.java b/prism/src/param/BigRational.java index f1f7b748..1939ec8d 100644 --- a/prism/src/param/BigRational.java +++ b/prism/src/param/BigRational.java @@ -55,10 +55,14 @@ public final class BigRational extends Number implements Comparable /** the BigRational "1" */ public final static BigRational ONE = new BigRational(BigInteger.ONE); + /** the BigRational "2" */ + public final static BigRational TWO = new BigRational(BigInteger.valueOf(2)); /** the BigRational "-1" */ public final static BigRational MONE = new BigRational(BigInteger.ONE).negate(); /** the BigRational "0" */ public final static BigRational ZERO = new BigRational(BigInteger.ZERO); + /** the BigRational "1/2" */ + public final static BigRational HALF = ONE.divide(TWO); /** the BigRational "infinity" */ public final static BigRational INF = new BigRational(BigInteger.ONE, BigInteger.ZERO); /** the BigRational "-infinity" */ @@ -807,6 +811,20 @@ public final class BigRational extends Number implements Comparable } } + /** + * Return round(value), i.e., the integer closest to value with + * ties rounding towards positive infinity. + * @throws PrismLangException for special values (NaN, infinity) + */ + public BigRational round() throws PrismLangException + { + if (isSpecial()) { + throw new PrismLangException("Can not compute round of " + this); + } + + return this.add(HALF).floor(); + } + /** * Returns larger value of {@code this} and {@code other}. * diff --git a/prism/src/parser/ast/ExpressionFunc.java b/prism/src/parser/ast/ExpressionFunc.java index b6cece35..a8f3be7d 100644 --- a/prism/src/parser/ast/ExpressionFunc.java +++ b/prism/src/parser/ast/ExpressionFunc.java @@ -42,15 +42,16 @@ public class ExpressionFunc extends Expression public static final int MAX = 1; public static final int FLOOR = 2; public static final int CEIL = 3; - public static final int POW = 4; - public static final int MOD = 5; - public static final int LOG = 6; - public static final int MULTI = 7; + public static final int ROUND = 4; + public static final int POW = 5; + public static final int MOD = 6; + public static final int LOG = 7; + public static final int MULTI = 8; // Built-in function names - public static final String names[] = { "min", "max", "floor", "ceil", "pow", "mod", "log", "multi" }; + public static final String names[] = { "min", "max", "floor", "ceil", "round", "pow", "mod", "log", "multi"}; // Min/max function arities - public static final int minArities[] = { 2, 2, 1, 1, 2, 2, 2, 1 }; - public static final int maxArities[] = { -1, -1, 1, 1, 2, 2, 2, -1 }; + public static final int minArities[] = { 2, 2, 1, 1, 1, 2, 2, 2, 1 }; + public static final int maxArities[] = { -1, -1, 1, 1, 1, 2, 2, 2, -1 }; // Function name private String name = ""; @@ -181,6 +182,8 @@ public class ExpressionFunc extends Expression return evaluateFloor(ec); case CEIL: return evaluateCeil(ec); + case ROUND: + return evaluateRound(ec); case POW: return evaluatePow(ec); case MOD: @@ -203,6 +206,8 @@ public class ExpressionFunc extends Expression return evaluateFloorExact(ec); case CEIL: return evaluateCeilExact(ec); + case ROUND: + return evaluateRoundExact(ec); case POW: return evaluatePowExact(ec); case MOD: @@ -314,16 +319,28 @@ public class ExpressionFunc extends Expression public static int evaluateCeil(double arg) throws PrismLangException { - double d = Math.ceil(arg); // Check for NaN or +/-inf, otherwise possible errors lost in cast to int - if (Double.isNaN(d) || Double.isInfinite(d)) - throw new PrismLangException("Cannot take ceil() of " + d); - return (int) d; + if (Double.isNaN(arg) || Double.isInfinite(arg)) + throw new PrismLangException("Cannot take ceil() of " + arg); + return (int) Math.ceil(arg); } - public BigRational evaluateCeilExact(EvaluateContext ec) throws PrismLangException + public Integer evaluateRound(EvaluateContext ec) throws PrismLangException { - return getOperand(0).evaluateExact(ec).ceil(); + try { + return evaluateRound(getOperand(0).evaluateDouble(ec)); + } catch (PrismLangException e) { + e.setASTElement(this); + throw e; + } + } + + public static int evaluateRound(double arg) throws PrismLangException + { + // Check for NaN, otherwise possible errors lost in cast to int + if (Double.isNaN(arg)) + throw new PrismLangException("Cannot take round() of " + arg); + return (int) Math.round(arg); } public BigRational evaluateFloorExact(EvaluateContext ec) throws PrismLangException @@ -331,6 +348,16 @@ public class ExpressionFunc extends Expression return getOperand(0).evaluateExact(ec).floor(); } + public BigRational evaluateCeilExact(EvaluateContext ec) throws PrismLangException + { + return getOperand(0).evaluateExact(ec).ceil(); + } + + public BigRational evaluateRoundExact(EvaluateContext ec) throws PrismLangException + { + return getOperand(0).evaluateExact(ec).round(); + } + public Object evaluatePow(EvaluateContext ec) throws PrismLangException { try { diff --git a/prism/src/parser/visitor/TypeCheck.java b/prism/src/parser/visitor/TypeCheck.java index 65a114ba..4b8eb9d3 100644 --- a/prism/src/parser/visitor/TypeCheck.java +++ b/prism/src/parser/visitor/TypeCheck.java @@ -353,6 +353,7 @@ public class TypeCheck extends ASTTraverse case ExpressionFunc.MAX: case ExpressionFunc.FLOOR: case ExpressionFunc.CEIL: + case ExpressionFunc.ROUND: case ExpressionFunc.POW: case ExpressionFunc.LOG: // All operands must be ints or doubles @@ -405,6 +406,7 @@ public class TypeCheck extends ASTTraverse break; case ExpressionFunc.FLOOR: case ExpressionFunc.CEIL: + case ExpressionFunc.ROUND: case ExpressionFunc.MOD: // Resulting type is always int e.setType(TypeInt.getInstance()); diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index 739d4742..f9ac59eb 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/prism/src/prism/StateModelChecker.java @@ -745,6 +745,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker return checkExpressionFuncNary(expr, statesOfInterest); case ExpressionFunc.FLOOR: case ExpressionFunc.CEIL: + case ExpressionFunc.ROUND: return checkExpressionFuncUnary(expr, statesOfInterest); case ExpressionFunc.POW: case ExpressionFunc.MOD: @@ -785,6 +786,10 @@ public class StateModelChecker extends PrismComponent implements ModelChecker // NB: Ceil result kept as double, so don't need to check if operand is NaN dd1 = JDD.MonadicApply(JDD.CEIL, dd1); break; + case ExpressionFunc.ROUND: + // NB: Round result kept as double, so don't need to check if operand is NaN + dd1 = JDD.MonadicApply(JDD.FLOOR, JDD.Plus(dd1, JDD.Constant(0.5))); + break; } return new StateValuesMTBDD(dd1, model); } @@ -803,6 +808,11 @@ public class StateModelChecker extends PrismComponent implements ModelChecker for (i = 0; i < n; i++) dv1.setElement(i, Math.ceil(dv1.getElement(i))); break; + case ExpressionFunc.ROUND: + // NB: Round result kept as double, so don't need to check if operand is NaN + for (i = 0; i < n; i++) + dv1.setElement(i, Math.round(dv1.getElement(i))); + break; } return new StateValuesDV(dv1, model); }