From f058cca5dd27f6c3c2adda51ba1fffbc9bd3cabd Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 13 Oct 2017 15:41:19 +0200
Subject: [PATCH] parser.ast.Update: support exact evaluation of update
 expressions

---
 prism/src/parser/ast/Update.java | 27 ++++++++++++++++++++++++++-
 1 file changed, 26 insertions(+), 1 deletion(-)

diff --git a/prism/src/parser/ast/Update.java b/prism/src/parser/ast/Update.java
index 952e1b71..e770b714 100644
--- a/prism/src/parser/ast/Update.java
+++ b/prism/src/parser/ast/Update.java
@@ -29,6 +29,7 @@ package parser.ast;
 import java.util.ArrayList;
 import java.util.BitSet;
 
+import param.BigRational;
 import parser.*;
 import parser.type.*;
 import parser.visitor.*;
@@ -245,15 +246,39 @@ public class Update extends ASTElement
 	 * Apply changes in variables to a provided copy of the State object.
 	 * (i.e. oldState and newState should be equal when passed in) 
 	 * It is assumed that any constants have already been defined.
+	 * <br>
+	 * Arithmetic expressions are evaluated using the default evaluate (i.e., not using exact arithmetic)
 	 * @param oldState Variable values in current state
 	 * @param newState State object to apply changes to
 	 */
 	public void update(State oldState, State newState) throws PrismLangException
+	{
+		update(oldState, newState, false);
+	}
+
+	/**
+	 * Execute this update, based on variable values specified as a State object.
+	 * Apply changes in variables to a provided copy of the State object.
+	 * (i.e. oldState and newState should be equal when passed in)
+	 * It is assumed that any constants have already been defined.
+	 * @param oldState Variable values in current state
+	 * @param newState State object to apply changes to
+	 * @param exact evaluate arithmetic expressions exactly?
+	 */
+	public void update(State oldState, State newState, boolean exact) throws PrismLangException
 	{
 		int i, n;
 		n = exprs.size();
 		for (i = 0; i < n; i++) {
-			newState.setValue(getVarIndex(i), getExpression(i).evaluate(oldState));
+			Object newValue;
+			if (exact) {
+				BigRational r = getExpression(i).evaluateExact(oldState);
+				// cast to Java data type
+				newValue = getExpression(i).getType().castFromBigRational(r);
+			} else {
+				newValue = getExpression(i).evaluate(oldState);
+			}
+			newState.setValue(getVarIndex(i), newValue);
 		}
 	}