Split Update into individual UpdateElement objects and make it iterable over.

prism/src/parser/ast/Update.java

@@ -2,7 +2,7 @@
 //	
 //	Copyright (c) 2002-
 //	Authors:
-//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham)
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
 //	
 //------------------------------------------------------------------------------
 //	
@@ -27,28 +27,25 @@
 package parser.ast;
 
 import java.util.ArrayList;
-import java.util.BitSet;
-
-import param.BigRational;
-import parser.*;
-import parser.type.*;
-import parser.visitor.*;
+import java.util.Iterator;
+import java.util.stream.Collectors;
+
+import parser.EvaluateContextSubstate;
+import parser.State;
+import parser.Values;
+import parser.VarList;
+import parser.type.Type;
+import parser.visitor.ASTVisitor;
 import prism.PrismLangException;
 
 /**
  * Class to store a single update, i.e. a list of assignments of variables to expressions, e.g. (s'=1)&amp;(x'=x+1)
  */
-public class Update extends ASTElement
+public class Update extends ASTElement implements Iterable<UpdateElement>
 {
-	// Lists of variable/expression pairs (and types)
-	private ArrayList<String> vars;
-	private ArrayList<Expression> exprs;
-	private ArrayList<Type> types;
-	// We also store an ExpressionIdent to match each variable.
-	// This is to just to provide positional info.
-	private ArrayList<ExpressionIdent> varIdents;
-	// The indices of each variable in the model to which it belongs
-	private ArrayList<Integer> indices;
+	// Individual elements of update
+	private ArrayList<UpdateElement> elements;
+
 	// Parent Updates object
 	private Updates parent;
 
@@ -57,11 +54,7 @@ public class Update extends ASTElement
 	 */
 	public Update()
 	{
-		vars = new ArrayList<String>();
-		exprs = new ArrayList<Expression>();
-		types = new ArrayList<Type>();
-		varIdents = new ArrayList<ExpressionIdent>();
-		indices = new ArrayList<Integer>();
+		elements = new ArrayList<>();
 	}
 
 	// Set methods
@@ -73,11 +66,23 @@ public class Update extends ASTElement
 	 */
 	public void addElement(ExpressionIdent v, Expression e)
 	{
-		vars.add(v.getName());
-		exprs.add(e);
-		types.add(null); // Type currently unknown
-		varIdents.add(v);
-		indices.add(-1); // Index currently unknown
+		elements.add(new UpdateElement(v, e));
+	}
+
+	/**
+	 * Add a variable assignment (encoded as an UpdateElement) to this update.
+	 */
+	public void addElement(UpdateElement e)
+	{
+		elements.add(e);
+	}
+
+	/**
+	 * Set the ith variable assignment (encoded as an UpdateElement) to this update.
+	 */
+	public void setElement(int i, UpdateElement e)
+	{
+		elements.set(i, e);
 	}
 
 	/**
@@ -87,8 +92,7 @@ public class Update extends ASTElement
 	 */
 	public void setVar(int i, ExpressionIdent v)
 	{
-		vars.set(i, v.getName());
-		varIdents.set(i, v);
+		elements.get(i).setVarIdent(v);
 	}
 
 	/**
@@ -98,7 +102,7 @@ public class Update extends ASTElement
 	 */
 	public void setExpression(int i, Expression e)
 	{
-		exprs.set(i, e);
+		elements.get(i).setExpression(e);
 	}
 
 	/**
@@ -108,7 +112,7 @@ public class Update extends ASTElement
 	 */
 	public void setType(int i, Type t)
 	{
-		types.set(i, t);
+		elements.get(i).setType(t);
 	}
 
 	/**
@@ -118,7 +122,7 @@ public class Update extends ASTElement
 	 */
 	public void setVarIndex(int i, int index)
 	{
-		indices.set(i, index);
+		elements.get(i).setVarIndex(index);
 	}
 
 	/**
@@ -136,15 +140,21 @@ public class Update extends ASTElement
 	 */
 	public int getNumElements()
 	{
-		return vars.size();
+		return elements.size();
 	}
 
+	/** Get the update element (individual assignment) with the given index. */
+	public UpdateElement getElement(int index)
+	{
+		return elements.get(index);
+	}
+	
 	/**
 	 * Get the name of the {@code i}th variable in this update.
 	 */
 	public String getVar(int i)
 	{
-		return vars.get(i);
+		return elements.get(i).getVar();
 	}
 
 	/**
@@ -152,7 +162,7 @@ public class Update extends ASTElement
 	 */
 	public Expression getExpression(int i)
 	{
-		return exprs.get(i);
+		return elements.get(i).getExpression();
 	}
 
 	/**
@@ -160,7 +170,7 @@ public class Update extends ASTElement
 	 */
 	public Type getType(int i)
 	{
-		return types.get(i);
+		return elements.get(i).getType();
 	}
 
 	/**
@@ -168,7 +178,7 @@ public class Update extends ASTElement
 	 */
 	public ExpressionIdent getVarIdent(int i)
 	{
-		return varIdents.get(i);
+		return elements.get(i).getVarIdent();
 	}
 
 	/**
@@ -176,7 +186,7 @@ public class Update extends ASTElement
 	 */
 	public int getVarIndex(int i)
 	{
-		return indices.get(i);
+		return elements.get(i).getVarIndex();
 	}
 
 	/**
@@ -196,13 +206,8 @@ public class Update extends ASTElement
 	 */
 	public Values update(Values constantValues, Values oldValues) throws PrismLangException
 	{
-		int i, n;
-		Values res;
-		res = new Values(oldValues);
-		n = exprs.size();
-		for (i = 0; i < n; i++) {
-			res.setValue(getVar(i), getExpression(i).evaluate(constantValues, oldValues));
-		}
+		Values res = new Values(oldValues);
+		update(constantValues, oldValues, res);
 		return res;
 	}
 
@@ -216,10 +221,8 @@ public class Update extends ASTElement
 	 */
 	public void update(Values constantValues, Values oldValues, Values newValues) throws PrismLangException
 	{
-		int i, n;
-		n = exprs.size();
-		for (i = 0; i < n; i++) {
-			newValues.setValue(getVar(i), getExpression(i).evaluate(constantValues, oldValues));
+		for (UpdateElement e : this) {
+			e.update(constantValues, oldValues, newValues);
 		}
 	}
 
@@ -231,13 +234,8 @@ public class Update extends ASTElement
 	 */
 	public State update(State oldState) throws PrismLangException
 	{
-		int i, n;
-		State res;
-		res = new State(oldState);
-		n = exprs.size();
-		for (i = 0; i < n; i++) {
-			res.setValue(getVarIndex(i), getExpression(i).evaluate(oldState));
-		}
+		State res = new State(oldState);
+		update(oldState, res);
 		return res;
 	}
 
@@ -267,18 +265,8 @@ public class Update extends ASTElement
 	 */
 	public void update(State oldState, State newState, boolean exact) throws PrismLangException
 	{
-		int i, n;
-		n = exprs.size();
-		for (i = 0; i < n; i++) {
-			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);
+		for (UpdateElement e : this) {
+			e.update(oldState, newState, exact);
 		}
 	}
 
@@ -298,7 +286,7 @@ public class Update extends ASTElement
 	public void updatePartially(State oldState, State newState, int[] varMap) throws PrismLangException
 	{
 		int i, j, n;
-		n = exprs.size();
+		n = elements.size();
 		for (i = 0; i < n; i++) {
 			j = varMap[getVarIndex(i)];
 			if (j != -1) {
@@ -314,68 +302,53 @@ public class Update extends ASTElement
 	 */
 	public State checkUpdate(State oldState, VarList varList) throws PrismLangException
 	{
-		int i, n, valNew;
 		State res;
 		res = new State(oldState);
-		n = exprs.size();
-		for (i = 0; i < n; i++) {
-			valNew = varList.encodeToInt(i, getExpression(i).evaluate(oldState));
-			if (valNew < varList.getLow(i) || valNew > varList.getHigh(i))
-				throw new PrismLangException("Value of variable " + getVar(i) + " overflows", getExpression(i));
+		for (UpdateElement e : this) {
+			e.checkUpdate(oldState, varList);
 		}
 		return res;
 	}
 
 	// Methods required for ASTElement:
 
-	/**
-	 * Visitor method.
-	 */
+	@Override
 	public Object accept(ASTVisitor v) throws PrismLangException
 	{
 		return v.visit(this);
 	}
 
-	/**
-	 * Convert to string.
-	 */
-	public String toString()
-	{
-		int i, n;
-		String s = "";
-
-		n = exprs.size();
-		// normal case
-		if (n > 0) {
-			for (i = 0; i < n - 1; i++) {
-				s = s + "(" + vars.get(i) + "'=" + exprs.get(i) + ") & ";
-			}
-			s = s + "(" + vars.get(n - 1) + "'=" + exprs.get(n - 1) + ")";
-		}
-		// special (empty) case
-		else {
-			s = "true";
-		}
-
-		return s;
-	}
-
-	/**
-	 * Perform a deep copy.
-	 */
+	@Override
 	public ASTElement deepCopy()
 	{
-		int i, n;
 		Update ret = new Update();
-		n = getNumElements();
-		for (i = 0; i < n; i++) {
-			ret.addElement((ExpressionIdent) getVarIdent(i).deepCopy(), getExpression(i).deepCopy());
-			ret.setType(i, getType(i));
-			ret.setVarIndex(i, getVarIndex(i));
+		for (UpdateElement e : this) {
+			ret.addElement(e.deepCopy());
 		}
 		ret.setPosition(this);
 		return ret;
 	}
+	
+	// Other methods:
+	
+	@Override
+	public Iterator<UpdateElement> iterator()
+	{
+		return elements.iterator();
+	}
+	
+	@Override
+	public String toString()
+	{
+		// Normal case
+		if (elements.size() > 0) {
+			return elements.stream().map(UpdateElement::toString).collect(Collectors.joining(" & "));
+		}
+		// Special (empty) case
+		else {
+			return "true";
+		}
+	}
 }
 
 //------------------------------------------------------------------------------

prism/src/parser/ast/UpdateElement.java

@@ -0,0 +1,220 @@
+//==============================================================================
+//	
+//	Copyright (c) 2018
+//	Authors:
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package parser.ast;
+
+import param.BigRational;
+import parser.State;
+import parser.Values;
+import parser.VarList;
+import parser.type.Type;
+import parser.visitor.ASTVisitor;
+import prism.PrismLangException;
+
+/**
+ * Class to store a single element of an Update, i.e. a single assignment (e.g. s'=1)
+ */
+public class UpdateElement extends ASTElement
+{
+	/** The variable that is assigned to */
+	private String var;
+	/** The expression for the assignment value */
+	private Expression expr;
+	/** The type of the assignment (initially empty / unknown) */
+	private Type type;
+	/** The identifier expression for the variable (for position information, etc) */
+	private ExpressionIdent ident;
+	/** The variable index (initially unknown, i.e., -1) */
+	private int index;
+
+	/** Constructor */
+	public UpdateElement(ExpressionIdent v, Expression e)
+	{
+		var = v.getName();
+		expr = e;
+		type = null; // Type currently unknown
+		ident = v;
+		index = -1; // Index currently unknown
+	}
+
+	/** Shallow copy constructor */
+	public UpdateElement(UpdateElement other)
+	{
+		var = other.var;
+		expr = other.expr;
+		type = other.type;
+		ident = other.ident;
+		index = other.index;
+	}
+
+	// Getters
+
+	/** Get the name of the variable that is the assignment target */
+	public String getVar()
+	{
+		return var;
+	}
+
+	/** Get the update expression */
+	public Expression getExpression()
+	{
+		return expr;
+	}
+
+	/** Get the type of the update */
+	public Type getType()
+	{
+		return type;
+	}
+
+	/** Get the ExpressionIdent corresponding to the variable name (for position information) */
+	public ExpressionIdent getVarIdent()
+	{
+		return ident;
+	}
+
+	/** Set the name of the variable that is the assignment target */
+	public void setVar(String var)
+	{
+		this.var = var;
+	}
+
+	/** Get the variable index for the variable that is the assignment target */
+	public int getVarIndex()
+	{
+		return index;
+	}
+
+	// Setters
+	
+	/** Set the update expression */
+	public void setExpression(Expression expr)
+	{
+		this.expr = expr;
+	}
+
+	/** Set the type of the update */
+	public void setType(Type type)
+	{
+		this.type = type;
+	}
+
+	/** Set the ExpressionIdent corresponding to the variable name (for position information) */
+	public void setVarIdent(ExpressionIdent ident)
+	{
+		this.ident = ident;
+		this.var = ident.getName();
+	}
+
+	/** Set the variable index for the variable that is the assignment target */
+	public void setVarIndex(int index)
+	{
+		this.index = index;
+	}
+
+	/**
+	 * Execute this update element, based on variable values specified as a Values object,
+	 * applying changes in variables to a second Values object. 
+	 * Values of any constants should also be provided.
+	 * @param constantValues Values for constants
+	 * @param oldValues Variable values in current state
+	 * @param newValues Values object to apply changes to
+	 */
+	public void update(Values constantValues, Values oldValues, Values newValues) throws PrismLangException
+	{
+		newValues.setValue(var, expr.evaluate(constantValues, oldValues));
+	}
+
+	/**
+	 * Execute this update element, based on variable values specified as a State object.
+	 * 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
+	 */
+	public void update(State oldState, State newState) throws PrismLangException
+	{
+		update(oldState, newState, false);
+	}
+
+	/**
+	 * Execute this update element, based on variable values specified as a State object.
+	 * 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
+	{
+		Object newValue;
+		if (exact) {
+			BigRational r = expr.evaluateExact(oldState);
+			// cast to Java data type
+			newValue = expr.getType().castFromBigRational(r);
+		} else {
+			newValue = expr.evaluate(oldState);
+		}
+		newState.setValue(index, newValue);
+	}
+	
+	/**
+	 * Check whether this update (from a particular state) would cause any errors, mainly variable overflows.
+	 * Variable ranges are specified in the passed in VarList.
+	 * Throws an exception if such an error occurs.
+	 */
+	public void checkUpdate(State oldState, VarList varList) throws PrismLangException
+	{
+		int valNew;
+		valNew = varList.encodeToInt(index, expr.evaluate(oldState));
+		if (valNew < varList.getLow(index) || valNew > varList.getHigh(index))
+			throw new PrismLangException("Value of variable " + var + " overflows", expr);
+	}
+
+
+	// Methods required for ASTElement:
+
+	@Override
+	public Object accept(ASTVisitor v) throws PrismLangException
+	{
+		return v.visit(this);
+	}
+
+	@Override
+	public UpdateElement deepCopy()
+	{
+		UpdateElement result = new UpdateElement((ExpressionIdent)ident.deepCopy(), expr.deepCopy());
+		result.type = type;
+		result.index = index;
+		return result;
+	}
+	
+	// Other methods:
+	
+	@Override
+	public String toString()
+	{
+		return "(" + getVar() + "'=" + getExpression() + ")";		
+	}
+}

prism/src/parser/visitor/ASTTraverse.java

@@ -253,13 +253,22 @@ public class ASTTraverse implements ASTVisitor
 		int i, n;
 		n = e.getNumElements();
 		for (i = 0; i < n; i++) {
-			if (e.getExpression(i) != null) e.getExpression(i).accept(this);
+			if (e.getElement(i) != null) e.getElement(i).accept(this);
 		}
 		visitPost(e);
 		return null;
 	}
 	public void visitPost(Update e) throws PrismLangException { defaultVisitPost(e); }
 	// -----------------------------------------------------------------------------------
+	public void visitPre(UpdateElement e) throws PrismLangException { defaultVisitPre(e); }
+	public Object visit(UpdateElement e) throws PrismLangException
+	{
+		visitPre(e);
+		if (e.getExpression() != null) e.getExpression().accept(this);
+		return null;
+	}
+	public void visitPost(UpdateElement e) throws PrismLangException { defaultVisitPost(e); }
+	// -----------------------------------------------------------------------------------
 	public void visitPre(RenamedModule e) throws PrismLangException { defaultVisitPre(e); }
 	public Object visit(RenamedModule e) throws PrismLangException
 	{

prism/src/parser/visitor/ASTTraverseModify.java

@@ -264,13 +264,23 @@ public class ASTTraverseModify implements ASTVisitor
 		int i, n;
 		n = e.getNumElements();
 		for (i = 0; i < n; i++) {
-			if (e.getExpression(i) != null) e.setExpression(i, (Expression)(e.getExpression(i).accept(this)));
+			if (e.getElement(i) != null) e.setElement(i, (UpdateElement)(e.getElement(i).accept(this)));
 		}
 		visitPost(e);
 		return e;
 	}
 	public void visitPost(Update e) throws PrismLangException { defaultVisitPost(e); }
 	// -----------------------------------------------------------------------------------
+	public void visitPre(UpdateElement e) throws PrismLangException { defaultVisitPre(e); }
+	public Object visit(UpdateElement e) throws PrismLangException
+	{
+		visitPre(e);
+		if (e.getExpression() != null) e.setExpression((Expression)(e.getExpression().accept(this)));
+		visitPost(e);
+		return e;
+	}
+	public void visitPost(UpdateElement e) throws PrismLangException { defaultVisitPost(e); }
+	// -----------------------------------------------------------------------------------
 	public void visitPre(RenamedModule e) throws PrismLangException { defaultVisitPre(e); }
 	public Object visit(RenamedModule e) throws PrismLangException
 	{

prism/src/parser/visitor/ASTVisitor.java

@@ -48,6 +48,7 @@ public interface ASTVisitor
 	public Object visit(Command e) throws PrismLangException;
 	public Object visit(Updates e) throws PrismLangException;
 	public Object visit(Update e) throws PrismLangException;
+	public Object visit(UpdateElement e) throws PrismLangException;
 	public Object visit(RenamedModule e) throws PrismLangException;
 	public Object visit(RewardStruct e) throws PrismLangException;
 	public Object visit(RewardStructItem e) throws PrismLangException;