From 2c8f5427b53cbcd18b7cb373df1c2f7bc1cfe922 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 22 Jul 2016 10:36:45 +0000 Subject: [PATCH] Expression: add evaluateExact methods git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11556 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/ast/Expression.java | 90 ++++++++++++++++++++ prism/src/parser/ast/ExpressionBinaryOp.java | 41 +++++++++ prism/src/parser/ast/ExpressionConstant.java | 13 ++- prism/src/parser/ast/ExpressionExists.java | 7 ++ prism/src/parser/ast/ExpressionFilter.java | 7 ++ prism/src/parser/ast/ExpressionForAll.java | 7 ++ prism/src/parser/ast/ExpressionFormula.java | 11 +++ prism/src/parser/ast/ExpressionFunc.java | 87 ++++++++++++++++++- prism/src/parser/ast/ExpressionITE.java | 7 ++ prism/src/parser/ast/ExpressionIdent.java | 9 ++ prism/src/parser/ast/ExpressionLabel.java | 7 ++ prism/src/parser/ast/ExpressionLiteral.java | 7 ++ prism/src/parser/ast/ExpressionProb.java | 7 ++ prism/src/parser/ast/ExpressionProp.java | 7 ++ prism/src/parser/ast/ExpressionReward.java | 7 ++ prism/src/parser/ast/ExpressionSS.java | 7 ++ prism/src/parser/ast/ExpressionStrategy.java | 7 ++ prism/src/parser/ast/ExpressionTemporal.java | 7 ++ prism/src/parser/ast/ExpressionUnaryOp.java | 15 ++++ prism/src/parser/ast/ExpressionVar.java | 12 ++- 20 files changed, 359 insertions(+), 3 deletions(-) diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java index 146e37b5..fecc1ef7 100644 --- a/prism/src/parser/ast/Expression.java +++ b/prism/src/parser/ast/Expression.java @@ -27,6 +27,7 @@ package parser.ast; import jltl2ba.SimpleLTL; +import param.BigRational; import parser.*; import parser.visitor.*; import prism.ModelType; @@ -55,6 +56,12 @@ public abstract class Expression extends ASTElement */ public abstract Object evaluate(EvaluateContext ec) throws PrismLangException; + /** + * Evaluate this expression exactly, return the result as a BigRational. + * Note: assumes that type checking has been done already. + */ + public abstract BigRational evaluateExact(EvaluateContext ec) throws PrismLangException; + /** * Get "name" of the result of this expression (used for y-axis of any graphs plotted) */ @@ -531,6 +538,89 @@ public abstract class Expression extends ASTElement return evaluateBoolean(new EvaluateContextSubstate(constantValues, substate, varMap)); } + + /** + * Evaluate this expression exactly to a BigRational, using no constant or variable values. + * Any typing issues cause an exception (but: we do allow conversion of boolean to 0/1). + * Note: assumes that type checking has been done already. + */ + public BigRational evaluateExact() throws PrismLangException + { + return evaluateExact(new EvaluateContextValues(null, null)); + } + + /** + * Evaluate this expression exactly to a BigRational, based on values for constants (but not variables). + * Any typing issues cause an exception (but: we do allow conversion of boolean to 0/1). + * Constant values are supplied as a Values object. + * Note: assumes that type checking has been done already. + */ + public BigRational evaluateExact(Values constantValues) throws PrismLangException + { + return evaluateExact(new EvaluateContextValues(constantValues, null)); + } + + /** + * Evaluate this expression exactly to a BigRational, based on values for constants/variables. + * Any typing issues cause an exception (but: we do allow conversion of boolean to 0/1). + * Each set of values is supplied as a Values object. + * Note: assumes that type checking has been done already. + */ + public BigRational evaluateExact(Values constantValues, Values varValues) throws PrismLangException + { + return evaluateExact(new EvaluateContextValues(constantValues, varValues)); + } + + /** + * Evaluate this expression exactly to a BigRational, based on values for variables (but not constants). + * Any typing issues cause an exception (but: we do allow conversion of boolean to 0/1). + * Variable values are supplied as a State object, i.e. array of variable values. + * Note: assumes that constants have been evaluated and type checking has been done. + */ + public BigRational evaluateExact(State state) throws PrismLangException + { + return evaluateExact(new EvaluateContextState(state)); + } + + /** + * Evaluate this expression as an integer, based on values for constants/variables. + * Any typing issues cause an exception (but: we do allow conversion of boolean to 0/1). + * Constant values are supplied as a Values object. + * Variable values are supplied as a State object, i.e. array of variable values. + * Note: assumes that type checking has been done. + */ + public BigRational evaluateExact(Values constantValues, State state) throws PrismLangException + { + return evaluateExact(new EvaluateContextState(constantValues, state)); + } + + /** + * Evaluate this expression exactly to a BigRational, based on values for some variables (but not constants). + * Any typing issues cause an exception (but: we do allow conversion of boolean to 0/1). + * Variable values are supplied as a State object, indexed over a subset of all variables, + * and a mapping from indices (over all variables) to this subset (-1 if not in subset). + * If any variables required for evaluation are missing, this will fail with an exception. + * Note: assumes that constants have been evaluated and type checking has been done. + */ + public BigRational evaluateExact(State substate, int[] varMap) throws PrismLangException + { + return evaluateExact(new EvaluateContextSubstate(substate, varMap)); + } + + /** + * Evaluate this expression exactly to a BigRational, based on values for constants and some variables. + * Any typing issues cause an exception (but: we do allow conversion of boolean to 0/1). + * Constant values are supplied as a Values object. + * Variable values are supplied as a State object, indexed over a subset of all variables, + * and a mapping from indices (over all variables) to this subset (-1 if not in subset). + * If any variables required for evaluation are missing, this will fail with an exception. + * Note: assumes that type checking has been done. + */ + public BigRational evaluateExact(Values constantValues, State substate, int[] varMap) throws PrismLangException + { + return evaluateExact(new EvaluateContextSubstate(constantValues, substate, varMap)); + } + // Static constructors for convenience public static ExpressionLiteral True() diff --git a/prism/src/parser/ast/ExpressionBinaryOp.java b/prism/src/parser/ast/ExpressionBinaryOp.java index 52945c7f..5d1d8dc3 100644 --- a/prism/src/parser/ast/ExpressionBinaryOp.java +++ b/prism/src/parser/ast/ExpressionBinaryOp.java @@ -26,6 +26,7 @@ package parser.ast; +import param.BigRational; import parser.EvaluateContext; import parser.type.TypeInt; import parser.visitor.ASTVisitor; @@ -198,6 +199,46 @@ public class ExpressionBinaryOp extends Expression } throw new PrismLangException("Unknown binary operator", this); } + + @Override + public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException + { + BigRational v1 = operand1.evaluateExact(ec); + BigRational v2 = operand2.evaluateExact(ec); + + switch (op) { + case IMPLIES: + return BigRational.from(!v1.toBoolean() || v2.toBoolean()); + case IFF: + return BigRational.from(v1.toBoolean() == v2.toBoolean()); + case OR: + return BigRational.from(v1.toBoolean() || v2.toBoolean()); + case AND: + return BigRational.from(v1.toBoolean() && v2.toBoolean()); + case EQ: + return BigRational.from(v1.equals(v2)); + case NE: + return BigRational.from(!v1.equals(v2)); + case GT: + return BigRational.from(v1.compareTo(v2) > 0); + case GE: + return BigRational.from(v1.equals(v2) || v1.compareTo(v2) > 0); + case LT: + return BigRational.from(v1.compareTo(v2) < 0); + case LE: + return BigRational.from(v1.equals(v2) || v1.compareTo(v2) < 0); + case PLUS: + return v1.add(v2); + case MINUS: + return v1.subtract(v2); + case TIMES: + return v1.multiply(v2); + case DIVIDE: + return v1.divide(v2); + } + throw new PrismLangException("Unknown binary operator", this); + } + @Override public boolean returnsSingleValue() diff --git a/prism/src/parser/ast/ExpressionConstant.java b/prism/src/parser/ast/ExpressionConstant.java index 74d87f1b..db8d0be8 100644 --- a/prism/src/parser/ast/ExpressionConstant.java +++ b/prism/src/parser/ast/ExpressionConstant.java @@ -26,6 +26,7 @@ package parser.ast; +import param.BigRational; import parser.*; import parser.visitor.*; import prism.PrismLangException; @@ -83,7 +84,17 @@ public class ExpressionConstant extends Expression throw new PrismLangException("Could not evaluate constant", this); return res; } - + + @Override + public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException + { + Object res = ec.getConstantValue(name); + if (res == null) + throw new PrismLangException("Could not evaluate constant", this); + + return BigRational.from(res); + } + @Override public boolean returnsSingleValue() { diff --git a/prism/src/parser/ast/ExpressionExists.java b/prism/src/parser/ast/ExpressionExists.java index 118c6b6b..8a1dfbbe 100644 --- a/prism/src/parser/ast/ExpressionExists.java +++ b/prism/src/parser/ast/ExpressionExists.java @@ -26,6 +26,7 @@ package parser.ast; +import param.BigRational; import parser.*; import parser.visitor.*; import prism.PrismLangException; @@ -79,6 +80,12 @@ public class ExpressionExists extends Expression throw new PrismLangException("Cannot evaluate an E operator without a model"); } + @Override + public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException + { + throw new PrismLangException("Cannot evaluate an E operator without a model"); + } + @Override public boolean returnsSingleValue() { diff --git a/prism/src/parser/ast/ExpressionFilter.java b/prism/src/parser/ast/ExpressionFilter.java index 264c0f56..32ccb3b2 100644 --- a/prism/src/parser/ast/ExpressionFilter.java +++ b/prism/src/parser/ast/ExpressionFilter.java @@ -26,6 +26,7 @@ package parser.ast; +import param.BigRational; import parser.*; import parser.type.TypeBool; import parser.visitor.*; @@ -226,6 +227,12 @@ public class ExpressionFilter extends Expression throw new PrismLangException("Cannot evaluate a filter without a model"); } + @Override + public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException + { + throw new PrismLangException("Cannot evaluate a filter without a model"); + } + @Override public boolean returnsSingleValue() { diff --git a/prism/src/parser/ast/ExpressionForAll.java b/prism/src/parser/ast/ExpressionForAll.java index ada2fc90..b2bd76fe 100644 --- a/prism/src/parser/ast/ExpressionForAll.java +++ b/prism/src/parser/ast/ExpressionForAll.java @@ -26,6 +26,7 @@ package parser.ast; +import param.BigRational; import parser.*; import parser.visitor.*; import prism.PrismLangException; @@ -79,6 +80,12 @@ public class ExpressionForAll extends Expression throw new PrismLangException("Cannot evaluate an E operator without a model"); } + @Override + public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException + { + throw new PrismLangException("Cannot evaluate an E operator without a model"); + } + @Override public boolean returnsSingleValue() { diff --git a/prism/src/parser/ast/ExpressionFormula.java b/prism/src/parser/ast/ExpressionFormula.java index 5d1957bd..3f3bb26d 100644 --- a/prism/src/parser/ast/ExpressionFormula.java +++ b/prism/src/parser/ast/ExpressionFormula.java @@ -26,6 +26,7 @@ package parser.ast; +import param.BigRational; import parser.*; import parser.visitor.*; import prism.PrismLangException; @@ -97,6 +98,16 @@ public class ExpressionFormula extends Expression return definition.evaluate(ec); } + @Override + public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException + { + // Should only be called (if at all) after definition has been set + if (definition == null) + throw new PrismLangException("Could not evaluate formula", this); + else + return definition.evaluateExact(ec); + } + @Override public boolean returnsSingleValue() { diff --git a/prism/src/parser/ast/ExpressionFunc.java b/prism/src/parser/ast/ExpressionFunc.java index 5cbf1d97..9367c77d 100644 --- a/prism/src/parser/ast/ExpressionFunc.java +++ b/prism/src/parser/ast/ExpressionFunc.java @@ -28,6 +28,7 @@ package parser.ast; import java.util.ArrayList; +import param.BigRational; import parser.*; import parser.visitor.*; import prism.PrismLangException; @@ -190,6 +191,29 @@ public class ExpressionFunc extends Expression throw new PrismLangException("Unknown function \"" + name + "\"", this); } + @Override + public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException + { + switch (code) { + case MIN: + return evaluateMinExact(ec); + case MAX: + return evaluateMaxExact(ec); + case FLOOR: + return evaluateFloorExact(ec); + case CEIL: + return evaluateCeilExact(ec); + case POW: + return evaluatePowExact(ec); + case MOD: + return evaluateModExact(ec); + case LOG: + return evaluateLogExact(ec); + } + throw new PrismLangException("Unknown function \"" + name + "\"", this); + } + + private Object evaluateMin(EvaluateContext ec) throws PrismLangException { int i, j, n, iMin; @@ -214,6 +238,17 @@ public class ExpressionFunc extends Expression } } + private BigRational evaluateMinExact(EvaluateContext ec) throws PrismLangException + { + BigRational min; + + min = getOperand(0).evaluateExact(ec); + for (int i = 1, n = getNumOperands(); i < n; i++) { + min = min.min(getOperand(i).evaluateExact(ec)); + } + return min; + } + private Object evaluateMax(EvaluateContext ec) throws PrismLangException { int i, j, n, iMax; @@ -238,6 +273,17 @@ public class ExpressionFunc extends Expression } } + private BigRational evaluateMaxExact(EvaluateContext ec) throws PrismLangException + { + BigRational max; + + max = getOperand(0).evaluateExact(ec); + for (int i = 1, n = getNumOperands(); i < n; i++) { + max = max.max(getOperand(i).evaluateExact(ec)); + } + return max; + } + public Object evaluateFloor(EvaluateContext ec) throws PrismLangException { try { @@ -276,6 +322,16 @@ public class ExpressionFunc extends Expression return (int) d; } + public BigRational evaluateCeilExact(EvaluateContext ec) throws PrismLangException + { + return getOperand(0).evaluateExact(ec).ceil(); + } + + public BigRational evaluateFloorExact(EvaluateContext ec) throws PrismLangException + { + return getOperand(0).evaluateExact(ec).floor(); + } + public Object evaluatePow(EvaluateContext ec) throws PrismLangException { try { @@ -307,6 +363,19 @@ public class ExpressionFunc extends Expression return Math.pow(base, exp); } + public BigRational evaluatePowExact(EvaluateContext ec) throws PrismLangException + { + BigRational base = getOperand(0).evaluateExact(ec); + BigRational exp = getOperand(1).evaluateExact(ec); + + try { + int expInt = exp.toInt(); + return base.pow(expInt); + } catch (PrismLangException e) { + throw new PrismLangException("Can not compute pow exactly, as there is a problem with the exponent: " + e.getMessage(), this); + } + } + public Object evaluateMod(EvaluateContext ec) throws PrismLangException { try { @@ -326,7 +395,18 @@ public class ExpressionFunc extends Expression int rem = i % j; return (rem < 0) ? rem + j : rem; } - + + public BigRational evaluateModExact(EvaluateContext ec) throws PrismLangException + { + BigRational a = getOperand(0).evaluateExact(ec); + BigRational b = getOperand(1).evaluateExact(ec); + + if (!a.isInteger() && !b.isInteger()) { + throw new PrismLangException("Can not compute mod for non-integer arguments", this); + } + return new BigRational(a.getNum().mod(b.getNum())); + } + public Object evaluateLog(EvaluateContext ec) throws PrismLangException { try { @@ -342,6 +422,11 @@ public class ExpressionFunc extends Expression return PrismUtils.log(x, b); } + public BigRational evaluateLogExact(EvaluateContext ec) throws PrismLangException + { + throw new PrismLangException("Currently, can not compute log exactly", this); + } + @Override public boolean returnsSingleValue() { diff --git a/prism/src/parser/ast/ExpressionITE.java b/prism/src/parser/ast/ExpressionITE.java index 81bfb6c7..e5586eea 100644 --- a/prism/src/parser/ast/ExpressionITE.java +++ b/prism/src/parser/ast/ExpressionITE.java @@ -26,6 +26,7 @@ package parser.ast; +import param.BigRational; import parser.*; import parser.visitor.*; import prism.PrismLangException; @@ -100,6 +101,12 @@ public class ExpressionITE extends Expression return operand1.evaluateBoolean(ec) ? operand2.evaluate(ec) : operand3.evaluate(ec); } + @Override + public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException + { + return operand1.evaluateExact(ec).toBoolean() ? operand2.evaluateExact(ec) : operand3.evaluateExact(ec); + } + @Override public boolean returnsSingleValue() { diff --git a/prism/src/parser/ast/ExpressionIdent.java b/prism/src/parser/ast/ExpressionIdent.java index 61767826..0385c38a 100644 --- a/prism/src/parser/ast/ExpressionIdent.java +++ b/prism/src/parser/ast/ExpressionIdent.java @@ -26,6 +26,7 @@ package parser.ast; +import param.BigRational; import parser.*; import parser.visitor.*; import prism.PrismLangException; @@ -83,6 +84,14 @@ public class ExpressionIdent extends Expression throw new PrismLangException("Could not evaluate identifier", this); } + @Override + public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException + { + // This should never be called. + // The ExpressionIdent should have been converted to an ExpressionVar/ExpressionConstant/... + throw new PrismLangException("Could not evaluate identifier", this); + } + @Override public boolean returnsSingleValue() { diff --git a/prism/src/parser/ast/ExpressionLabel.java b/prism/src/parser/ast/ExpressionLabel.java index e1e2c718..f1b0323b 100644 --- a/prism/src/parser/ast/ExpressionLabel.java +++ b/prism/src/parser/ast/ExpressionLabel.java @@ -26,6 +26,7 @@ package parser.ast; +import param.BigRational; import parser.*; import parser.visitor.*; import prism.PrismLangException; @@ -85,6 +86,12 @@ public class ExpressionLabel extends Expression throw new PrismLangException("Cannot evaluate labels", this); } + @Override + public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException + { + throw new PrismLangException("Cannot evaluate labels", this); + } + @Override public boolean returnsSingleValue() { diff --git a/prism/src/parser/ast/ExpressionLiteral.java b/prism/src/parser/ast/ExpressionLiteral.java index 9490aad9..71338bf7 100644 --- a/prism/src/parser/ast/ExpressionLiteral.java +++ b/prism/src/parser/ast/ExpressionLiteral.java @@ -26,6 +26,7 @@ package parser.ast; +import param.BigRational; import parser.*; import parser.visitor.*; import prism.PrismLangException; @@ -94,6 +95,12 @@ public class ExpressionLiteral extends Expression return value; } + @Override + public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException + { + return BigRational.from(value); + } + @Override public boolean returnsSingleValue() { diff --git a/prism/src/parser/ast/ExpressionProb.java b/prism/src/parser/ast/ExpressionProb.java index a33bd894..515ce219 100644 --- a/prism/src/parser/ast/ExpressionProb.java +++ b/prism/src/parser/ast/ExpressionProb.java @@ -26,6 +26,7 @@ package parser.ast; +import param.BigRational; import parser.EvaluateContext; import parser.Values; import parser.visitor.ASTVisitor; @@ -111,6 +112,12 @@ public class ExpressionProb extends ExpressionQuant throw new PrismLangException("Cannot evaluate a P operator without a model"); } + @Override + public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException + { + throw new PrismLangException("Cannot evaluate a P operator without a model"); + } + @Override public String getResultName() { diff --git a/prism/src/parser/ast/ExpressionProp.java b/prism/src/parser/ast/ExpressionProp.java index 2dc10475..16f1ced9 100644 --- a/prism/src/parser/ast/ExpressionProp.java +++ b/prism/src/parser/ast/ExpressionProp.java @@ -26,6 +26,7 @@ package parser.ast; +import param.BigRational; import parser.*; import parser.visitor.*; import prism.PrismLangException; @@ -73,6 +74,12 @@ public class ExpressionProp extends Expression throw new PrismLangException("Cannot evaluate property references", this); } + @Override + public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException + { + throw new PrismLangException("Cannot evaluate property references", this); + } + @Override public boolean returnsSingleValue() { diff --git a/prism/src/parser/ast/ExpressionReward.java b/prism/src/parser/ast/ExpressionReward.java index 93b975d9..13694d6b 100644 --- a/prism/src/parser/ast/ExpressionReward.java +++ b/prism/src/parser/ast/ExpressionReward.java @@ -26,6 +26,7 @@ package parser.ast; +import param.BigRational; import parser.EvaluateContext; import parser.Values; import parser.visitor.ASTVisitor; @@ -185,6 +186,12 @@ public class ExpressionReward extends ExpressionQuant throw new PrismLangException("Cannot evaluate an R operator without a model"); } + @Override + public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException + { + throw new PrismLangException("Cannot evaluate an R operator without a model"); + } + @Override public String getResultName() { diff --git a/prism/src/parser/ast/ExpressionSS.java b/prism/src/parser/ast/ExpressionSS.java index 9225be19..5a3bd4b3 100644 --- a/prism/src/parser/ast/ExpressionSS.java +++ b/prism/src/parser/ast/ExpressionSS.java @@ -26,6 +26,7 @@ package parser.ast; +import param.BigRational; import parser.EvaluateContext; import parser.Values; import parser.visitor.ASTVisitor; @@ -105,6 +106,12 @@ public class ExpressionSS extends ExpressionQuant throw new PrismLangException("Cannot evaluate an S operator without a model"); } + @Override + public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException + { + throw new PrismLangException("Cannot evaluate an S operator without a model"); + } + @Override public String getResultName() { diff --git a/prism/src/parser/ast/ExpressionStrategy.java b/prism/src/parser/ast/ExpressionStrategy.java index 152ef477..7062aea9 100644 --- a/prism/src/parser/ast/ExpressionStrategy.java +++ b/prism/src/parser/ast/ExpressionStrategy.java @@ -29,6 +29,7 @@ package parser.ast; import java.util.ArrayList; import java.util.List; +import param.BigRational; import parser.EvaluateContext; import parser.visitor.ASTVisitor; import prism.PrismLangException; @@ -173,6 +174,12 @@ public class ExpressionStrategy extends Expression throw new PrismLangException("Cannot evaluate a " + getOperatorString() + " operator without a model"); } + @Override + public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException + { + throw new PrismLangException("Cannot evaluate a " + getOperatorString() + " operator without a model"); + } + /*@Override public String getResultName() { diff --git a/prism/src/parser/ast/ExpressionTemporal.java b/prism/src/parser/ast/ExpressionTemporal.java index 73a5edac..48221c46 100644 --- a/prism/src/parser/ast/ExpressionTemporal.java +++ b/prism/src/parser/ast/ExpressionTemporal.java @@ -26,6 +26,7 @@ package parser.ast; +import param.BigRational; import parser.EvaluateContext; import parser.visitor.ASTVisitor; import prism.PrismLangException; @@ -223,6 +224,12 @@ public class ExpressionTemporal extends Expression throw new PrismLangException("Cannot evaluate a temporal operator without a path"); } + @Override + public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException + { + throw new PrismLangException("Cannot evaluate a temporal operator without a path"); + } + @Override public boolean returnsSingleValue() { diff --git a/prism/src/parser/ast/ExpressionUnaryOp.java b/prism/src/parser/ast/ExpressionUnaryOp.java index 29eb24b9..793fda1b 100644 --- a/prism/src/parser/ast/ExpressionUnaryOp.java +++ b/prism/src/parser/ast/ExpressionUnaryOp.java @@ -26,6 +26,7 @@ package parser.ast; +import param.BigRational; import parser.*; import parser.visitor.*; import prism.PrismLangException; @@ -118,6 +119,20 @@ public class ExpressionUnaryOp extends Expression throw new PrismLangException("Unknown unary operator", this); } + @Override + public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException + { + switch (op) { + case NOT: + return BigRational.from(!operand.evaluateExact(ec).toBoolean()); + case MINUS: + return operand.evaluateExact().negate(); + case PARENTH: + return operand.evaluateExact(ec); + } + throw new PrismLangException("Unknown unary operator", this); + } + @Override public boolean returnsSingleValue() { diff --git a/prism/src/parser/ast/ExpressionVar.java b/prism/src/parser/ast/ExpressionVar.java index dc1dad34..4e9e98c5 100644 --- a/prism/src/parser/ast/ExpressionVar.java +++ b/prism/src/parser/ast/ExpressionVar.java @@ -26,6 +26,7 @@ package parser.ast; +import param.BigRational; import parser.*; import parser.visitor.*; import prism.PrismLangException; @@ -93,7 +94,16 @@ public class ExpressionVar extends Expression throw new PrismLangException("Could not evaluate variable", this); return res; } - + + @Override + public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException + { + Object res = ec.getVarValue(name, index); + if (res == null) + throw new PrismLangException("Could not evaluate variable", this); + return BigRational.from(res); + } + @Override public boolean returnsSingleValue() {