Implement round function

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:

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}.

prism/src/param/BigRational.java

@@ -55,10 +55,14 @@ public final class BigRational extends Number implements Comparable<BigRational>
 
 	/** 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<BigRational>
 		}
 	}
 
+	/**
+	 * 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}.
 	 * 

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 {

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

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