diff --git a/prism/src/parser/ast/Update.java b/prism/src/parser/ast/Update.java index e770b714..6682ac20 100644 --- a/prism/src/parser/ast/Update.java +++ b/prism/src/parser/ast/Update.java @@ -2,7 +2,7 @@ // // Copyright (c) 2002- // Authors: -// * Dave Parker (University of Oxford, formerly University of Birmingham) +// * Dave Parker (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)&(x'=x+1) */ -public class Update extends ASTElement +public class Update extends ASTElement implements Iterable { - // Lists of variable/expression pairs (and types) - private ArrayList vars; - private ArrayList exprs; - private ArrayList types; - // We also store an ExpressionIdent to match each variable. - // This is to just to provide positional info. - private ArrayList varIdents; - // The indices of each variable in the model to which it belongs - private ArrayList indices; + // Individual elements of update + private ArrayList elements; + // Parent Updates object private Updates parent; @@ -57,11 +54,7 @@ public class Update extends ASTElement */ public Update() { - vars = new ArrayList(); - exprs = new ArrayList(); - types = new ArrayList(); - varIdents = new ArrayList(); - indices = new ArrayList(); + 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 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"; + } + } } //------------------------------------------------------------------------------ diff --git a/prism/src/parser/ast/UpdateElement.java b/prism/src/parser/ast/UpdateElement.java new file mode 100644 index 00000000..1ac33342 --- /dev/null +++ b/prism/src/parser/ast/UpdateElement.java @@ -0,0 +1,220 @@ +//============================================================================== +// +// Copyright (c) 2018 +// Authors: +// * Dave Parker (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() + ")"; + } +} diff --git a/prism/src/parser/visitor/ASTTraverse.java b/prism/src/parser/visitor/ASTTraverse.java index d8ee27aa..2e7598c8 100644 --- a/prism/src/parser/visitor/ASTTraverse.java +++ b/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 { diff --git a/prism/src/parser/visitor/ASTTraverseModify.java b/prism/src/parser/visitor/ASTTraverseModify.java index 96670422..1453fd14 100644 --- a/prism/src/parser/visitor/ASTTraverseModify.java +++ b/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 { diff --git a/prism/src/parser/visitor/ASTVisitor.java b/prism/src/parser/visitor/ASTVisitor.java index a5702ef3..67be47cc 100644 --- a/prism/src/parser/visitor/ASTVisitor.java +++ b/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;