diff --git a/prism/src/automata/LTL2RabinLibrary.java b/prism/src/automata/LTL2RabinLibrary.java index 4173888c2c..a07b573946 100644 --- a/prism/src/automata/LTL2RabinLibrary.java +++ b/prism/src/automata/LTL2RabinLibrary.java @@ -132,7 +132,7 @@ public static DA getDRAforLTL(Expression ltl, Values co labels = new ArrayList(); ltl.accept(new ASTTraverse() { - public Object visit(ExpressionLabel e) throws PrismLangException + public Object visitNow(ExpressionLabel e) throws PrismLangException { labels.add(e.getName()); return null; @@ -144,7 +144,7 @@ public Object visit(ExpressionLabel e) throws PrismLangException Expression ltl2 = ltl.deepCopy(); ltl2.accept(new ASTTraverseModify() { - public Object visit(ExpressionLabel e) throws PrismLangException + public Object visitNow(ExpressionLabel e) throws PrismLangException { int i = labels.indexOf(e.getName()); //char letter = (char) ('a' + i); diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index 0adf107753..2e06985af8 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -1299,57 +1299,57 @@ public CheckMaximalPropositionalFormulas(StateModelChecker mc, Model model, List this.propBSs = propBSs; } - public Object visit(ExpressionITE e) throws PrismLangException + public Object visitNow(ExpressionITE e) throws PrismLangException { - return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e); + return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visitNow(e); } - public Object visit(ExpressionBinaryOp e) throws PrismLangException + public Object visitNow(ExpressionBinaryOp e) throws PrismLangException { - return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e); + return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visitNow(e); } - public Object visit(ExpressionUnaryOp e) throws PrismLangException + public Object visitNow(ExpressionUnaryOp e) throws PrismLangException { - return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e); + return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visitNow(e); } - public Object visit(ExpressionFunc e) throws PrismLangException + public Object visitNow(ExpressionFunc e) throws PrismLangException { - return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e); + return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visitNow(e); } - public Object visit(ExpressionIdent e) throws PrismLangException + public Object visitNow(ExpressionIdent e) throws PrismLangException { - return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e); + return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visitNow(e); } - public Object visit(ExpressionLiteral e) throws PrismLangException + public Object visitNow(ExpressionLiteral e) throws PrismLangException { - return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e); + return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visitNow(e); } - public Object visit(ExpressionConstant e) throws PrismLangException + public Object visitNow(ExpressionConstant e) throws PrismLangException { - return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e); + return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visitNow(e); } - public Object visit(ExpressionFormula e) throws PrismLangException + public Object visitNow(ExpressionFormula e) throws PrismLangException { - return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e); + return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visitNow(e); } - public Object visit(ExpressionVar e) throws PrismLangException + public Object visitNow(ExpressionVar e) throws PrismLangException { - return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e); + return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visitNow(e); } - public Object visit(ExpressionLabel e) throws PrismLangException + public Object visitNow(ExpressionLabel e) throws PrismLangException { - return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e); + return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visitNow(e); } - public Object visit(ExpressionProp e) throws PrismLangException + public Object visitNow(ExpressionProp e) throws PrismLangException { // Look up property and recurse Property prop = propertiesFile.lookUpPropertyObjectByName(e.getName()); @@ -1360,9 +1360,9 @@ public Object visit(ExpressionProp e) throws PrismLangException } } - public Object visit(ExpressionFilter e) throws PrismLangException + public Object visitNow(ExpressionFilter e) throws PrismLangException { - return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visit(e); + return (e.getType() instanceof TypeBool && e.isProposition()) ? replaceWithLabel(e) : super.visitNow(e); } /** diff --git a/prism/src/parser/BooleanUtils.java b/prism/src/parser/BooleanUtils.java index c75778f5dc..57cbbd430f 100644 --- a/prism/src/parser/BooleanUtils.java +++ b/prism/src/parser/BooleanUtils.java @@ -118,7 +118,7 @@ private static Expression removeImpliesIffAndParentheses(Expression expr) try { exprMod = (Expression) expr.accept(new ASTTraverseModify() { - public Object visit(ExpressionUnaryOp e) throws PrismLangException + public Object visitNow(ExpressionUnaryOp e) throws PrismLangException { // Remove parentheses: (a) if (Expression.isParenth(e)) { @@ -126,10 +126,10 @@ public Object visit(ExpressionUnaryOp e) throws PrismLangException // (a) == a return a; } - return super.visit(e); + return super.visitNow(e); } - public Object visit(ExpressionBinaryOp e) throws PrismLangException + public Object visitNow(ExpressionBinaryOp e) throws PrismLangException { // Remove implication: a => b if (Expression.isImplies(e)) { @@ -145,7 +145,7 @@ public Object visit(ExpressionBinaryOp e) throws PrismLangException // a <=> b == (a | !b) & (!a | b) return Expression.And(Expression.Or(a, Expression.Not(b)), Expression.Or(Expression.Not(a.deepCopy()), b.deepCopy())); } - return super.visit(e); + return super.visitNow(e); } }); } catch (PrismLangException e) { diff --git a/prism/src/parser/PrismParser.java b/prism/src/parser/PrismParser.java index 51c18ffe55..45cd704cdf 100644 --- a/prism/src/parser/PrismParser.java +++ b/prism/src/parser/PrismParser.java @@ -80,7 +80,7 @@ else if (args[0].equals("-expression") || args[0].equals("-e")) { else if (args[0].equals("-ltl") || args[0].equals("-l")) { Expression expr = p.parseSingleLTLFormula(str); expr = (Expression) expr.accept(new ASTTraverseModify() { - public Object visit(ExpressionIdent e) throws PrismLangException + public Object visitNow(ExpressionIdent e) throws PrismLangException { return new parser.ast.ExpressionVar(e.getName(), TypeBool.getInstance()); } @@ -99,7 +99,7 @@ public Object visit(ExpressionIdent e) throws PrismLangException System.out.println("Syntactically co-safe: " + Expression.isCoSafeLTLSyntactic(exprPnf)); } Expression expr2 = (Expression) expr.deepCopy().accept(new ASTTraverseModify() { - public Object visit(ExpressionVar e) throws PrismLangException + public Object visitNow(ExpressionVar e) throws PrismLangException { return new parser.ast.ExpressionLabel(e.getName()); } diff --git a/prism/src/parser/ast/ASTElement.java b/prism/src/parser/ast/ASTElement.java index 8326057509..960f48f9d7 100644 --- a/prism/src/parser/ast/ASTElement.java +++ b/prism/src/parser/ast/ASTElement.java @@ -35,7 +35,7 @@ // Abstract class for PRISM language AST elements -public abstract class ASTElement +public abstract class ASTElement implements Cloneable { // Type - default to null (unknown) protected Type type = null; @@ -186,7 +186,39 @@ public String getEndString() /** * Perform a deep copy. */ - public abstract ASTElement deepCopy(); + public ASTElement deepCopy() + { + try { + return new DeepCopy().copy(this); + } catch (PrismLangException e) { + throw new Error(e); + } + } + + /** + * Perform a deep copy of all internal ASTElements using a deep copy visitor. + * This method is usually called after {@code clone()} and must return the receiver. + * + * @param copier the copy visitor + * @returns the receiver with deep-copied subcomponents + * @throws PrismLangException + * @see #clone() + */ + public abstract ASTElement deepCopy(DeepCopy copier) throws PrismLangException; + + /** + * Perform a shallow copy of the receiver and + * clone all internal container, e.g., lists and vectors, too. + */ + @Override + public ASTElement clone() + { + try { + return (ASTElement) super.clone(); + } catch (CloneNotSupportedException e) { + throw new InternalError("Object#clone is expected to work for Cloneable objects.", e); + } + } // Various methods based on AST traversals (implemented using the visitor // pattern): diff --git a/prism/src/parser/ast/Command.java b/prism/src/parser/ast/Command.java index c1ffb8c3b3..8adc91123f 100644 --- a/prism/src/parser/ast/Command.java +++ b/prism/src/parser/ast/Command.java @@ -137,19 +137,20 @@ public String toString() s += "] " + guard + " -> " + updates; return s; } - - /** - * Perform a deep copy. - */ - public ASTElement deepCopy() + + @Override + public Command deepCopy(DeepCopy copier) throws PrismLangException + { + guard = copier.copy(guard); + updates = copier.copy(updates); + + return this; + } + + @Override + public Command clone() { - Command ret = new Command(); - ret.setSynch(getSynch()); - ret.setSynchIndex(getSynchIndex()); - ret.setGuard(getGuard().deepCopy()); - ret.setUpdates((Updates)getUpdates().deepCopy()); - ret.setPosition(this); - return ret; + return (Command) super.clone(); } } diff --git a/prism/src/parser/ast/ConstantList.java b/prism/src/parser/ast/ConstantList.java index c10f9a04fa..ada68d8d70 100644 --- a/prism/src/parser/ast/ConstantList.java +++ b/prism/src/parser/ast/ConstantList.java @@ -80,7 +80,7 @@ public void addConstant(ExpressionIdent n, Expression c, Type t) types.addElement(t); nameIdents.addElement(n); } - + public void setConstant(int i, Expression c) { constants.setElementAt(c, i); @@ -429,21 +429,28 @@ public String toString() return s; } - - /** - * Perform a deep copy. - */ - public ASTElement deepCopy() + + @Override + public ConstantList deepCopy(DeepCopy copier) throws PrismLangException { - int i, n; - ConstantList ret = new ConstantList(); - n = size(); - for (i = 0; i < n; i++) { - Expression constantNew = (getConstant(i) == null) ? null : getConstant(i).deepCopy(); - ret.addConstant((ExpressionIdent)getConstantNameIdent(i).deepCopy(), constantNew, getConstantType(i)); - } - ret.setPosition(this); - return ret; + copier.copyAll(constants); + copier.copyAll(nameIdents); + + return this; + } + + @SuppressWarnings("unchecked") + @Override + public ConstantList clone() + { + ConstantList clone = (ConstantList) super.clone(); + + clone.constants = (Vector) constants.clone(); + clone.nameIdents = (Vector) nameIdents.clone(); + clone.names = (Vector) names.clone(); + clone.types = (Vector) types.clone(); + + return clone; } } diff --git a/prism/src/parser/ast/Declaration.java b/prism/src/parser/ast/Declaration.java index 7cb5a29ce9..8fb0802270 100644 --- a/prism/src/parser/ast/Declaration.java +++ b/prism/src/parser/ast/Declaration.java @@ -138,17 +138,19 @@ public String toString() return s; } - /** - * Perform a deep copy. - */ @Override - public ASTElement deepCopy() + public Declaration deepCopy(DeepCopy copier) throws PrismLangException + { + declType = copier.copy(declType); + start = copier.copy(start); + + return this; + } + + @Override + public Declaration clone() { - Declaration ret = new Declaration(getName(), (DeclarationType)getDeclType().deepCopy()); - if (getStart() != null) - ret.setStart(getStart().deepCopy()); - ret.setPosition(this); - return ret; + return (Declaration) super.clone(); } } diff --git a/prism/src/parser/ast/DeclarationArray.java b/prism/src/parser/ast/DeclarationArray.java index d79ec97635..1727b67192 100644 --- a/prism/src/parser/ast/DeclarationArray.java +++ b/prism/src/parser/ast/DeclarationArray.java @@ -29,6 +29,7 @@ import parser.type.*; import parser.visitor.ASTVisitor; +import parser.visitor.DeepCopy; import prism.PrismLangException; public class DeclarationArray extends DeclarationType @@ -121,17 +122,19 @@ public String toString() return "array [" + low + ".." + high + "] of " + subtype; } - /** - * Perform a deep copy. - */ @Override - public ASTElement deepCopy() + public DeclarationArray deepCopy(DeepCopy copier) throws PrismLangException + { + low = copier.copy(low); + high = copier.copy(high); + subtype = copier.copy(subtype); + + return this; + } + + @Override + public DeclarationArray clone() { - Expression lowCopy = (low == null) ? null : low.deepCopy(); - Expression highCopy = (high == null) ? null : high.deepCopy(); - DeclarationType subtypeCopy = (DeclarationType) subtype.deepCopy(); - DeclarationArray ret = new DeclarationArray(lowCopy, highCopy, subtypeCopy); - ret.setPosition(this); - return ret; + return (DeclarationArray) super.clone(); } } diff --git a/prism/src/parser/ast/DeclarationBool.java b/prism/src/parser/ast/DeclarationBool.java index 03f0bbeaef..aa9b70b759 100644 --- a/prism/src/parser/ast/DeclarationBool.java +++ b/prism/src/parser/ast/DeclarationBool.java @@ -29,6 +29,7 @@ import parser.type.TypeBool; import parser.visitor.ASTVisitor; +import parser.visitor.DeepCopy; import prism.PrismLangException; public class DeclarationBool extends DeclarationType @@ -75,13 +76,15 @@ public String toString() return "bool"; } - /** - * Perform a deep copy. - */ - public ASTElement deepCopy() + @Override + public DeclarationBool deepCopy(DeepCopy copier) throws PrismLangException + { + return this; + } + + @Override + public DeclarationBool clone() { - DeclarationBool ret = new DeclarationBool(); - ret.setPosition(this); - return ret; + return (DeclarationBool) super.clone(); } } diff --git a/prism/src/parser/ast/DeclarationClock.java b/prism/src/parser/ast/DeclarationClock.java index bbfa9d012e..0b3f3af8b6 100644 --- a/prism/src/parser/ast/DeclarationClock.java +++ b/prism/src/parser/ast/DeclarationClock.java @@ -28,6 +28,7 @@ import parser.type.*; import parser.visitor.ASTVisitor; +import parser.visitor.DeepCopy; import prism.PrismLangException; public class DeclarationClock extends DeclarationType @@ -78,14 +79,15 @@ public String toString() return "clock"; } - /** - * Perform a deep copy. - */ @Override - public ASTElement deepCopy() + public DeclarationClock deepCopy(DeepCopy copier) throws PrismLangException + { + return this; + } + + @Override + public DeclarationClock clone() { - DeclarationClock ret = new DeclarationClock(); - ret.setPosition(this); - return ret; + return (DeclarationClock) super.clone(); } } diff --git a/prism/src/parser/ast/DeclarationInt.java b/prism/src/parser/ast/DeclarationInt.java index 00163bd643..078d02d867 100644 --- a/prism/src/parser/ast/DeclarationInt.java +++ b/prism/src/parser/ast/DeclarationInt.java @@ -29,6 +29,7 @@ import parser.type.*; import parser.visitor.ASTVisitor; +import parser.visitor.DeepCopy; import prism.PrismLangException; public class DeclarationInt extends DeclarationType @@ -106,16 +107,18 @@ public String toString() return "[" + low + ".." + high + "]"; } - /** - * Perform a deep copy. - */ @Override - public ASTElement deepCopy() + public DeclarationInt deepCopy(DeepCopy copier) throws PrismLangException + { + low = copier.copy(low); + high = copier.copy(high); + + return this; + } + + @Override + public DeclarationInt clone() { - Expression lowCopy = (low == null) ? null : low.deepCopy(); - Expression highCopy = (high == null) ? null : high.deepCopy(); - DeclarationInt ret = new DeclarationInt(lowCopy, highCopy); - ret.setPosition(this); - return ret; + return (DeclarationInt) super.clone(); } } diff --git a/prism/src/parser/ast/DeclarationIntUnbounded.java b/prism/src/parser/ast/DeclarationIntUnbounded.java index 0da204f0a4..d9eb775a40 100644 --- a/prism/src/parser/ast/DeclarationIntUnbounded.java +++ b/prism/src/parser/ast/DeclarationIntUnbounded.java @@ -28,6 +28,7 @@ import parser.type.*; import parser.visitor.ASTVisitor; +import parser.visitor.DeepCopy; import prism.PrismLangException; public class DeclarationIntUnbounded extends DeclarationType @@ -78,14 +79,15 @@ public String toString() return "int"; } - /** - * Perform a deep copy. - */ @Override - public ASTElement deepCopy() + public DeclarationIntUnbounded deepCopy(DeepCopy copier) throws PrismLangException + { + return this; + } + + @Override + public DeclarationIntUnbounded clone() { - DeclarationIntUnbounded ret = new DeclarationIntUnbounded(); - ret.setPosition(this); - return ret; + return (DeclarationIntUnbounded) super.clone(); } } diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java index 6569c66629..ccd24cfd73 100644 --- a/prism/src/parser/ast/Expression.java +++ b/prism/src/parser/ast/Expression.java @@ -75,13 +75,20 @@ public String getResultName() * when evaluated during model checking? */ public abstract boolean returnsSingleValue(); - - // Overrided version of deepCopy() from superclass ASTElement (to reduce casting). - /** - * Perform a deep copy. - */ - public abstract Expression deepCopy(); + // Override version of deepCopy() from superclass (to reduce casting). + @Override + public Expression deepCopy() + { + return (Expression) super.deepCopy(); + } + + // Override version of clone() from superclass (to reduce casting). + @Override + public Expression clone() + { + return (Expression) super.clone(); + } // Utility methods: @@ -790,14 +797,8 @@ public static boolean isFunc(Expression expr, int nameCode) */ public static boolean isQuantitative(Expression expr) { - if (expr instanceof ExpressionProb) { - return ((ExpressionProb) expr).getProb() == null; - } - else if (expr instanceof ExpressionReward) { - return ((ExpressionReward) expr).getReward() == null; - } - else if (expr instanceof ExpressionSS) { - return ((ExpressionSS) expr).getProb() == null; + if (expr instanceof ExpressionQuant) { + return ((ExpressionQuant) expr).isQuantitative(); } return false; } diff --git a/prism/src/parser/ast/ExpressionBinaryOp.java b/prism/src/parser/ast/ExpressionBinaryOp.java index 9e78cf6290..5ee234e03d 100644 --- a/prism/src/parser/ast/ExpressionBinaryOp.java +++ b/prism/src/parser/ast/ExpressionBinaryOp.java @@ -30,6 +30,7 @@ import parser.EvaluateContext; import parser.type.TypeInt; import parser.visitor.ASTVisitor; +import parser.visitor.DeepCopy; import prism.PrismLangException; public class ExpressionBinaryOp extends Expression @@ -269,12 +270,18 @@ public Object accept(ASTVisitor v) throws PrismLangException } @Override - public Expression deepCopy() + public ExpressionBinaryOp deepCopy(DeepCopy copier) throws PrismLangException { - ExpressionBinaryOp expr = new ExpressionBinaryOp(op, operand1.deepCopy(), operand2.deepCopy()); - expr.setType(type); - expr.setPosition(this); - return expr; + operand1 = copier.copy(operand1); + operand2 = copier.copy(operand2); + + return this; + } + + @Override + public ExpressionBinaryOp clone() + { + return (ExpressionBinaryOp) super.clone(); } // Standard methods diff --git a/prism/src/parser/ast/ExpressionConstant.java b/prism/src/parser/ast/ExpressionConstant.java index db8d0be871..2b0469d165 100644 --- a/prism/src/parser/ast/ExpressionConstant.java +++ b/prism/src/parser/ast/ExpressionConstant.java @@ -108,13 +108,17 @@ public Object accept(ASTVisitor v) throws PrismLangException { return v.visit(this); } - + + @Override + public ExpressionConstant deepCopy(DeepCopy copier) throws PrismLangException + { + return this; + } + @Override - public Expression deepCopy() + public ExpressionConstant clone() { - Expression ret = new ExpressionConstant(name, type); - ret.setPosition(this); - return ret; + return (ExpressionConstant) super.clone(); } // Standard methods diff --git a/prism/src/parser/ast/ExpressionExists.java b/prism/src/parser/ast/ExpressionExists.java index 8a1dfbbe7c..1e19b5af40 100644 --- a/prism/src/parser/ast/ExpressionExists.java +++ b/prism/src/parser/ast/ExpressionExists.java @@ -99,14 +99,19 @@ public Object accept(ASTVisitor v) throws PrismLangException { return v.visit(this); } - + + @Override + public ExpressionExists deepCopy(DeepCopy copier) throws PrismLangException + { + expression = copier.copy(expression); + + return this; + } + @Override - public Expression deepCopy() + public ExpressionExists clone() { - ExpressionExists expr = new ExpressionExists(expression.deepCopy()); - expr.setType(type); - expr.setPosition(this); - return expr; + return (ExpressionExists) super.clone(); } // Standard methods diff --git a/prism/src/parser/ast/ExpressionFilter.java b/prism/src/parser/ast/ExpressionFilter.java index 32ccb3b2fb..585c9da748 100644 --- a/prism/src/parser/ast/ExpressionFilter.java +++ b/prism/src/parser/ast/ExpressionFilter.java @@ -254,16 +254,19 @@ public Object accept(ASTVisitor v) throws PrismLangException } @Override - public Expression deepCopy() + public ExpressionFilter deepCopy(DeepCopy copier) throws PrismLangException { - ExpressionFilter e; - e = new ExpressionFilter(opName, operand.deepCopy(), filter == null ? null : filter.deepCopy()); - e.setInvisible(invisible); - e.setType(type); - e.setPosition(this); - e.param = this.param; + filter = copier.copy(filter); + operand = copier.copy(operand); - return e; + return this; + + } + + @Override + public ExpressionFilter clone() + { + return (ExpressionFilter) super.clone(); } // Standard methods diff --git a/prism/src/parser/ast/ExpressionForAll.java b/prism/src/parser/ast/ExpressionForAll.java index b2bd76fecb..885b0a5916 100644 --- a/prism/src/parser/ast/ExpressionForAll.java +++ b/prism/src/parser/ast/ExpressionForAll.java @@ -99,14 +99,19 @@ public Object accept(ASTVisitor v) throws PrismLangException { return v.visit(this); } - + + @Override + public ExpressionForAll deepCopy(DeepCopy copier) throws PrismLangException + { + expression = copier.copy(expression); + + return this; + } + @Override - public Expression deepCopy() + public ExpressionForAll clone() { - ExpressionForAll expr = new ExpressionForAll(expression.deepCopy()); - expr.setType(type); - expr.setPosition(this); - return expr; + return (ExpressionForAll) super.clone(); } // Standard methods diff --git a/prism/src/parser/ast/ExpressionFormula.java b/prism/src/parser/ast/ExpressionFormula.java index 3f3bb26d00..b6477bbcf5 100644 --- a/prism/src/parser/ast/ExpressionFormula.java +++ b/prism/src/parser/ast/ExpressionFormula.java @@ -122,14 +122,19 @@ public Object accept(ASTVisitor v) throws PrismLangException { return v.visit(this); } - + + @Override + public ExpressionFormula deepCopy(DeepCopy copier) throws PrismLangException + { + definition = copier.copy(definition); + + return this; + } + @Override - public Expression deepCopy() + public ExpressionFormula clone() { - ExpressionFormula ret = new ExpressionFormula(name); - ret.setDefinition(definition == null ? null : definition.deepCopy()); - ret.setPosition(this); - return ret; + return (ExpressionFormula) super.clone(); } // Standard methods diff --git a/prism/src/parser/ast/ExpressionFunc.java b/prism/src/parser/ast/ExpressionFunc.java index c399be0a52..5b51b8326f 100644 --- a/prism/src/parser/ast/ExpressionFunc.java +++ b/prism/src/parser/ast/ExpressionFunc.java @@ -452,25 +452,26 @@ public Object accept(ASTVisitor v) throws PrismLangException } @Override - public Expression deepCopy() + public ExpressionFunc deepCopy(DeepCopy copier) throws PrismLangException { - int i, n; - ExpressionFunc e; + copier.copyAll(operands); - e = new ExpressionFunc(name); - e.setOldStyle(oldStyle); - n = getNumOperands(); - for (i = 0; i < n; i++) { - e.addOperand((Expression) getOperand(i).deepCopy()); - } - e.setType(type); - e.setPosition(this); + return this; + } - return e; + @SuppressWarnings("unchecked") + @Override + public ExpressionFunc clone() + { + ExpressionFunc clone = (ExpressionFunc) super.clone(); + + clone.operands = (ArrayList) operands.clone(); + + return clone; } - + // Standard methods - + @Override public String toString() { diff --git a/prism/src/parser/ast/ExpressionITE.java b/prism/src/parser/ast/ExpressionITE.java index e5586eea84..a6e2956b96 100644 --- a/prism/src/parser/ast/ExpressionITE.java +++ b/prism/src/parser/ast/ExpressionITE.java @@ -122,12 +122,19 @@ public Object accept(ASTVisitor v) throws PrismLangException } @Override - public Expression deepCopy() + public ExpressionITE deepCopy(DeepCopy copier) throws PrismLangException { - ExpressionITE expr = new ExpressionITE(operand1.deepCopy(), operand2.deepCopy(), operand3.deepCopy()); - expr.setType(type); - expr.setPosition(this); - return expr; + operand1 = copier.copy(operand1); + operand2 = copier.copy(operand2); + operand3 = copier.copy(operand3); + + return this; + } + + @Override + public ExpressionITE clone() + { + return (ExpressionITE) super.clone(); } // Standard methods diff --git a/prism/src/parser/ast/ExpressionIdent.java b/prism/src/parser/ast/ExpressionIdent.java index 0385c38aca..17fbb28506 100644 --- a/prism/src/parser/ast/ExpressionIdent.java +++ b/prism/src/parser/ast/ExpressionIdent.java @@ -106,14 +106,17 @@ public Object accept(ASTVisitor v) throws PrismLangException { return v.visit(this); } - + + @Override + public ExpressionIdent deepCopy(DeepCopy copier) throws PrismLangException + { + return this; + } + @Override - public Expression deepCopy() + public ExpressionIdent clone() { - ExpressionIdent expr = new ExpressionIdent(name); - expr.setType(type); - expr.setPosition(this); - return expr; + return (ExpressionIdent) super.clone(); } // Standard methods diff --git a/prism/src/parser/ast/ExpressionLabel.java b/prism/src/parser/ast/ExpressionLabel.java index f1b0323b39..5f142328e9 100644 --- a/prism/src/parser/ast/ExpressionLabel.java +++ b/prism/src/parser/ast/ExpressionLabel.java @@ -105,14 +105,17 @@ public Object accept(ASTVisitor v) throws PrismLangException { return v.visit(this); } - + + @Override + public ExpressionLabel deepCopy(DeepCopy copier) throws PrismLangException + { + return this; + } + @Override - public Expression deepCopy() + public ExpressionLabel clone() { - ExpressionLabel expr = new ExpressionLabel(name); - expr.setType(type); - expr.setPosition(this); - return expr; + return (ExpressionLabel) super.clone(); } // Standard methods diff --git a/prism/src/parser/ast/ExpressionLiteral.java b/prism/src/parser/ast/ExpressionLiteral.java index 71338bf7ee..81985085d3 100644 --- a/prism/src/parser/ast/ExpressionLiteral.java +++ b/prism/src/parser/ast/ExpressionLiteral.java @@ -116,11 +116,15 @@ public Object accept(ASTVisitor v) throws PrismLangException } @Override - public Expression deepCopy() + public ExpressionLiteral deepCopy(DeepCopy copier) throws PrismLangException { - Expression expr = new ExpressionLiteral(type, value, string); - expr.setPosition(this); - return expr; + return this; + } + + @Override + public ExpressionLiteral clone() + { + return (ExpressionLiteral) super.clone(); } // Standard methods diff --git a/prism/src/parser/ast/ExpressionProb.java b/prism/src/parser/ast/ExpressionProb.java index 515ce219f6..0576139919 100644 --- a/prism/src/parser/ast/ExpressionProb.java +++ b/prism/src/parser/ast/ExpressionProb.java @@ -26,10 +26,9 @@ package parser.ast; -import param.BigRational; -import parser.EvaluateContext; import parser.Values; import parser.visitor.ASTVisitor; +import parser.visitor.DeepCopy; import prism.OpRelOpBound; import prism.PrismLangException; @@ -91,32 +90,8 @@ public OpRelOpBound getRelopBoundInfo(Values constantValues) throws PrismLangExc return new OpRelOpBound("P", getRelOp(), null); } } - - // Methods required for Expression: - - @Override - public boolean isConstant() - { - return false; - } - @Override - public boolean isProposition() - { - return false; - } - - @Override - public Object evaluate(EvaluateContext ec) throws PrismLangException - { - 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"); - } + // Methods required for Expression: @Override public String getResultName() @@ -131,12 +106,6 @@ else if (getRelOp() == RelOp.MAX) return "Probability"; } - @Override - public boolean returnsSingleValue() - { - return false; - } - // Methods required for ASTElement: @Override @@ -146,33 +115,30 @@ public Object accept(ASTVisitor v) throws PrismLangException } @Override - public Expression deepCopy() + public ExpressionProb deepCopy(DeepCopy copier) throws PrismLangException { - ExpressionProb expr = new ExpressionProb(); - expr.setExpression(getExpression() == null ? null : getExpression().deepCopy()); - expr.setRelOp(getRelOp()); - expr.setBound(getBound() == null ? null : getBound().deepCopy()); - expr.setFilter(getFilter() == null ? null : (Filter)getFilter().deepCopy()); - expr.setType(type); - expr.setPosition(this); - return expr; + return (ExpressionProb) super.deepCopy(copier); + } + + @Override + public ExpressionProb clone() + { + return (ExpressionProb) super.clone(); } // Standard methods @Override - public String toString() + protected String operatorToString() { - String s = ""; - - s += "P" + getModifierString() + getRelOp(); - s += (getBound() == null) ? "?" : getBound().toString(); - s += " [ " + getExpression(); - if (getFilter() != null) - s += " " + getFilter(); - s += " ]"; + return "P" + getModifierString(); + } - return s; + @Override + protected String bodyToString() + { + String filter = getFilter() == null ? "" : " " + getFilter(); + return getExpression() + filter; } } diff --git a/prism/src/parser/ast/ExpressionProp.java b/prism/src/parser/ast/ExpressionProp.java index 16f1ced98a..93334fc583 100644 --- a/prism/src/parser/ast/ExpressionProp.java +++ b/prism/src/parser/ast/ExpressionProp.java @@ -95,16 +95,19 @@ public Object accept(ASTVisitor v) throws PrismLangException } @Override - public Expression deepCopy() + public ExpressionProp deepCopy(DeepCopy copier) throws PrismLangException { - ExpressionProp expr = new ExpressionProp(name); - expr.setType(type); - expr.setPosition(this); - return expr; + return this; + } + + @Override + public ExpressionProp clone() + { + return (ExpressionProp) super.clone(); } // Standard methods - + @Override public String toString() { diff --git a/prism/src/parser/ast/ExpressionQuant.java b/prism/src/parser/ast/ExpressionQuant.java index 20d2c9042b..71ebc09e51 100644 --- a/prism/src/parser/ast/ExpressionQuant.java +++ b/prism/src/parser/ast/ExpressionQuant.java @@ -26,9 +26,13 @@ package parser.ast; +import param.BigRational; +import parser.EvaluateContext; import parser.Values; +import parser.visitor.DeepCopy; import prism.OpRelOpBound; import prism.PrismException; +import prism.PrismLangException; /** * Abstract class for representing "quantitative" operators (P,R,S), @@ -161,8 +165,74 @@ public Filter getFilter() return filter; } + // Test methods + + @Override + public boolean isConstant() + { + return false; + } + + @Override + public boolean isProposition() + { + return false; + } + + public boolean isQuantitative() + { + return getBound() == null; + } + + @Override + public boolean returnsSingleValue() + { + return false; + } + + // Methods required for Expression: + + @Override + public Object evaluate(final EvaluateContext ec) throws PrismLangException + { + throw new PrismLangException("Cannot evaluate a quantiative expression without a model"); + } + + @Override + public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException + { + throw new PrismLangException("Cannot evaluate a quantiative expression without a model"); + } + + @Override + public ExpressionQuant deepCopy(DeepCopy copier) throws PrismLangException + { + expression = copier.copy(expression); + bound = copier.copy(bound); + filter = copier.copy(filter); + + return this; + } + // Standard methods - + + @Override + public String toString() + { + return operatorToString() + boundsToString() + " [ " + bodyToString() + " ]"; + } + + protected abstract String operatorToString(); + + protected String boundsToString() + { + String bounds = getBound() == null ? "?" : getBound().toString(); + return getRelOp() + bounds; + } + + protected abstract String bodyToString(); + + @Override public int hashCode() { diff --git a/prism/src/parser/ast/ExpressionReward.java b/prism/src/parser/ast/ExpressionReward.java index 2d6ffb95c8..ad11b83329 100644 --- a/prism/src/parser/ast/ExpressionReward.java +++ b/prism/src/parser/ast/ExpressionReward.java @@ -26,10 +26,9 @@ package parser.ast; -import param.BigRational; -import parser.EvaluateContext; import parser.Values; import parser.visitor.ASTVisitor; +import parser.visitor.DeepCopy; import prism.ModelInfo; import prism.OpRelOpBound; import prism.PrismException; @@ -39,13 +38,13 @@ public class ExpressionReward extends ExpressionQuant { protected Object rewardStructIndex = null; protected Object rewardStructIndexDiv = null; - + // Constructors - + public ExpressionReward() { } - + public ExpressionReward(Expression expression, String relOpString, Expression r) { setExpression(expression); @@ -54,7 +53,7 @@ public ExpressionReward(Expression expression, String relOpString, Expression r) } // Set methods - + public void setRewardStructIndex(Object o) { rewardStructIndex = o; @@ -74,7 +73,7 @@ public void setReward(Expression r) } // Get methods - + public Object getRewardStructIndex() { return rewardStructIndex; @@ -94,7 +93,7 @@ public Expression getReward() } // Other methods - + /** * Get a string describing the type of R operator, e.g. "R=?" or "R<r". */ @@ -172,11 +171,11 @@ public static RewardStruct getRewardStructByIndexObject(Object rsi, ModelInfo mo return modelInfo.getRewardStruct(rewardStructIndex); } - /** * Get info about the operator and bound. * @param constantValues Values for constants in order to evaluate any bound */ + @Override public OpRelOpBound getRelopBoundInfo(Values constantValues) throws PrismException { if (getBound() != null) { @@ -186,32 +185,8 @@ public OpRelOpBound getRelopBoundInfo(Values constantValues) throws PrismExcepti return new OpRelOpBound("R", getRelOp(), null); } } - - // Methods required for Expression: - - @Override - public boolean isConstant() - { - return false; - } - - @Override - public boolean isProposition() - { - return false; - } - - @Override - public Object evaluate(EvaluateContext ec) throws PrismLangException - { - 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"); - } + // Methods required for Expression: @Override public String getResultName() @@ -240,61 +215,57 @@ else if (rewardStructIndexDiv == null) } } + // Methods required for ASTElement: + @Override - public boolean returnsSingleValue() + public Object accept(ASTVisitor v) throws PrismLangException { - return false; + return v.visit(this); } - // Methods required for ASTElement: - @Override - public Object accept(ASTVisitor v) throws PrismLangException + public ExpressionReward deepCopy(DeepCopy copier) throws PrismLangException { - return v.visit(this); + super.deepCopy(copier); + if (rewardStructIndex instanceof Expression) { + rewardStructIndex = copier.copy((Expression) rewardStructIndex); + } + if (rewardStructIndexDiv instanceof Expression) { + rewardStructIndexDiv = copier.copy((Expression) rewardStructIndexDiv); + } + + return this; } @Override - public Expression deepCopy() + public ExpressionReward clone() { - ExpressionReward expr = new ExpressionReward(); - expr.setExpression(getExpression() == null ? null : getExpression().deepCopy()); - expr.setRelOp(getRelOp()); - expr.setBound(getBound() == null ? null : getBound().deepCopy()); - if (rewardStructIndex != null && rewardStructIndex instanceof Expression) expr.setRewardStructIndex(((Expression)rewardStructIndex).deepCopy()); - else expr.setRewardStructIndex(rewardStructIndex); - if (rewardStructIndexDiv != null && rewardStructIndexDiv instanceof Expression) expr.setRewardStructIndexDiv(((Expression)rewardStructIndexDiv).deepCopy()); - else expr.setRewardStructIndexDiv(rewardStructIndexDiv); - expr.setFilter(getFilter() == null ? null : (Filter)getFilter().deepCopy()); - expr.setType(type); - expr.setPosition(this); - return expr; + return (ExpressionReward) super.clone(); } // Standard methods - + @Override - public String toString() + protected String operatorToString() { - String s = ""; - - s += "R" + getModifierString(); + String rewards = ""; if (rewardStructIndex != null) { - if (rewardStructIndex instanceof Expression) s += "{"+rewardStructIndex+"}"; - else if (rewardStructIndex instanceof String) s += "{\""+rewardStructIndex+"\"}"; + if (rewardStructIndex instanceof Expression) rewards += "{"+rewardStructIndex+"}"; + else if (rewardStructIndex instanceof String) rewards += "{\""+rewardStructIndex+"\"}"; if (rewardStructIndexDiv != null) { - s += "/"; - if (rewardStructIndexDiv instanceof Expression) s += "{"+rewardStructIndexDiv+"}"; - else if (rewardStructIndexDiv instanceof String) s += "{\""+rewardStructIndexDiv+"\"}"; + rewards += "/"; + if (rewardStructIndexDiv instanceof Expression) rewards += "{"+rewardStructIndexDiv+"}"; + else if (rewardStructIndexDiv instanceof String) rewards += "{\""+rewardStructIndexDiv+"\"}"; } } - s += getRelOp(); - s += (getBound()==null) ? "?" : getBound().toString(); - s += " [ " + getExpression(); - if (getFilter() != null) s += " "+getFilter(); - s += " ]"; - - return s; + return "R" + getModifierString() + rewards; + } + + @Override + protected String bodyToString() + { + String filter = getFilter() == null ? "" : " " + getFilter(); + return getExpression() + filter; } @Override diff --git a/prism/src/parser/ast/ExpressionSS.java b/prism/src/parser/ast/ExpressionSS.java index 5a3bd4b378..91c700466d 100644 --- a/prism/src/parser/ast/ExpressionSS.java +++ b/prism/src/parser/ast/ExpressionSS.java @@ -26,10 +26,9 @@ package parser.ast; -import param.BigRational; -import parser.EvaluateContext; import parser.Values; import parser.visitor.ASTVisitor; +import parser.visitor.DeepCopy; import prism.OpRelOpBound; import prism.PrismException; import prism.PrismLangException; @@ -37,11 +36,11 @@ public class ExpressionSS extends ExpressionQuant { // Constructors - + public ExpressionSS() { } - + public ExpressionSS(Expression expression, String relOpString, Expression p) { setExpression(expression); @@ -50,7 +49,7 @@ public ExpressionSS(Expression expression, String relOpString, Expression p) } // Set methods - + /** * Set the probability bound. Equivalent to {@code setBound(p)}. */ @@ -60,7 +59,7 @@ public void setProb(Expression p) } // Get methods - + /** * Get the probability bound. Equivalent to {@code getBound()}. */ @@ -74,6 +73,7 @@ public Expression getProb() * Does some checks, e.g., throws an exception if probability is out of range. * @param constantValues Values for constants in order to evaluate any bound */ + @Override public OpRelOpBound getRelopBoundInfo(Values constantValues) throws PrismException { if (getBound() != null) { @@ -85,80 +85,48 @@ public OpRelOpBound getRelopBoundInfo(Values constantValues) throws PrismExcepti return new OpRelOpBound("S", getRelOp(), null); } } - + // Methods required for Expression: - - @Override - public boolean isConstant() - { - return false; - } @Override - public boolean isProposition() - { - return false; - } - - @Override - public Object evaluate(EvaluateContext ec) throws PrismLangException + public String getResultName() { - throw new PrismLangException("Cannot evaluate an S operator without a model"); + return (getBound() == null) ? "Probability" : "Result"; } - @Override - public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException - { - throw new PrismLangException("Cannot evaluate an S operator without a model"); - } + // Methods required for ASTElement: @Override - public String getResultName() + public Object accept(ASTVisitor v) throws PrismLangException { - return (getBound() == null) ? "Probability" : "Result"; + return v.visit(this); } @Override - public boolean returnsSingleValue() + public ExpressionSS deepCopy(DeepCopy copier) throws PrismLangException { - return false; + return (ExpressionSS) super.deepCopy(copier); } - // Methods required for ASTElement: - @Override - public Object accept(ASTVisitor v) throws PrismLangException + public ExpressionSS clone() { - return v.visit(this); + return (ExpressionSS) super.clone(); } + // Standard methods + @Override - public Expression deepCopy() + protected String operatorToString() { - ExpressionSS expr = new ExpressionSS(); - expr.setExpression(getExpression() == null ? null : getExpression().deepCopy()); - expr.setRelOp(getRelOp()); - expr.setBound(getBound() == null ? null : getBound().deepCopy()); - expr.setFilter(getFilter() == null ? null : (Filter)getFilter().deepCopy()); - expr.setType(type); - expr.setPosition(this); - return expr; + return "S" + getModifierString(); } - // Standard methods - @Override - public String toString() + protected String bodyToString() { - String s = ""; - - s += "S" + getModifierString() + getRelOp(); - s += (getBound()==null) ? "?" : getBound().toString(); - s += " [ " + getExpression(); - if (getFilter() != null) s += " "+getFilter(); - s += " ]"; - - return s; + String filter = getFilter() == null ? "" : " " + getFilter(); + return getExpression() + filter; } } diff --git a/prism/src/parser/ast/ExpressionStrategy.java b/prism/src/parser/ast/ExpressionStrategy.java index 7062aea9ef..555302d445 100644 --- a/prism/src/parser/ast/ExpressionStrategy.java +++ b/prism/src/parser/ast/ExpressionStrategy.java @@ -32,6 +32,7 @@ import param.BigRational; import parser.EvaluateContext; import parser.visitor.ASTVisitor; +import parser.visitor.DeepCopy; import prism.PrismLangException; /** @@ -47,7 +48,7 @@ public class ExpressionStrategy extends Expression protected Coalition coalition = new Coalition(); /** Child expression(s) */ - protected List operands = new ArrayList(); + protected ArrayList operands = new ArrayList(); /** Is there just a single operand (P/R operator)? If not, the operand list will be parenthesised. **/ protected boolean singleOperand = false; @@ -201,18 +202,23 @@ public Object accept(ASTVisitor v) throws PrismLangException } @Override - public Expression deepCopy() + public ExpressionStrategy deepCopy(DeepCopy copier) throws PrismLangException { - ExpressionStrategy expr = new ExpressionStrategy(); - expr.setThereExists(isThereExists()); - expr.coalition = new Coalition(coalition); - for (Expression operand : operands) { - expr.addOperand((Expression) operand.deepCopy()); - } - expr.singleOperand = singleOperand; - expr.setType(type); - expr.setPosition(this); - return expr; + copier.copyAll(operands); + + return this; + } + + @SuppressWarnings("unchecked") + @Override + public ExpressionStrategy clone() + { + ExpressionStrategy clone = (ExpressionStrategy) super.clone(); + + clone.coalition = new Coalition(coalition); + clone.operands = (ArrayList) operands.clone(); + + return clone; } // Standard methods diff --git a/prism/src/parser/ast/ExpressionTemporal.java b/prism/src/parser/ast/ExpressionTemporal.java index 528a34d27f..c8aea61a00 100644 --- a/prism/src/parser/ast/ExpressionTemporal.java +++ b/prism/src/parser/ast/ExpressionTemporal.java @@ -29,6 +29,7 @@ import param.BigRational; import parser.EvaluateContext; import parser.visitor.ASTVisitor; +import parser.visitor.DeepCopy; import prism.PrismLangException; public class ExpressionTemporal extends Expression @@ -263,20 +264,20 @@ public Object accept(ASTVisitor v) throws PrismLangException } @Override - public Expression deepCopy() + public ExpressionTemporal deepCopy(DeepCopy copier) throws PrismLangException { - ExpressionTemporal expr = new ExpressionTemporal(); - expr.setOperator(op); - if (operand1 != null) - expr.setOperand1(operand1.deepCopy()); - if (operand2 != null) - expr.setOperand2(operand2.deepCopy()); - expr.setLowerBound(lBound == null ? null : lBound.deepCopy(), lBoundStrict); - expr.setUpperBound(uBound == null ? null : uBound.deepCopy(), uBoundStrict); - expr.equals = equals; - expr.setType(type); - expr.setPosition(this); - return expr; + operand1 = copier.copy(operand1); + operand2 = copier.copy(operand2); + lBound = copier.copy(lBound); + uBound = copier.copy(uBound); + + return this; + } + + @Override + public ExpressionTemporal clone() + { + return (ExpressionTemporal) super.clone(); } // Standard methods diff --git a/prism/src/parser/ast/ExpressionUnaryOp.java b/prism/src/parser/ast/ExpressionUnaryOp.java index 0c48975ff8..cdc2ca73aa 100644 --- a/prism/src/parser/ast/ExpressionUnaryOp.java +++ b/prism/src/parser/ast/ExpressionUnaryOp.java @@ -162,12 +162,17 @@ public Object accept(ASTVisitor v) throws PrismLangException } @Override - public Expression deepCopy() + public ExpressionUnaryOp deepCopy(DeepCopy copier) throws PrismLangException { - ExpressionUnaryOp expr = new ExpressionUnaryOp(op, operand.deepCopy()); - expr.setType(type); - expr.setPosition(this); - return expr; + operand = copier.copy(operand); + + return this; + } + + @Override + public ExpressionUnaryOp clone() + { + return (ExpressionUnaryOp) super.clone(); } // Standard methods diff --git a/prism/src/parser/ast/ExpressionVar.java b/prism/src/parser/ast/ExpressionVar.java index 4e9e98c5fb..a33304fb0f 100644 --- a/prism/src/parser/ast/ExpressionVar.java +++ b/prism/src/parser/ast/ExpressionVar.java @@ -119,12 +119,15 @@ public Object accept(ASTVisitor v) throws PrismLangException } @Override - public Expression deepCopy() + public ExpressionVar deepCopy(DeepCopy copier) throws PrismLangException { - ExpressionVar expr = new ExpressionVar(name, type); - expr.setIndex(index); - expr.setPosition(this); - return expr; + return this; + } + + @Override + public ExpressionVar clone() + { + return (ExpressionVar) super.clone(); } // Standard methods diff --git a/prism/src/parser/ast/Filter.java b/prism/src/parser/ast/Filter.java index b0353ce58b..4a9a0ce575 100644 --- a/prism/src/parser/ast/Filter.java +++ b/prism/src/parser/ast/Filter.java @@ -115,17 +115,19 @@ public String toString() if (maxReq) s += "{max}"; return s; } - - /** - * Perform a deep copy. - */ - public ASTElement deepCopy() + + @Override + public Filter deepCopy(DeepCopy copier) throws PrismLangException + { + expr = copier.copy(expr); + + return this; + } + + @Override + public Filter clone() { - Filter ret = new Filter(expr.deepCopy()); - ret.setMinRequested(minReq); - ret.setMaxRequested(maxReq); - ret.setPosition(this); - return ret; + return (Filter) super.clone(); } } diff --git a/prism/src/parser/ast/ForLoop.java b/prism/src/parser/ast/ForLoop.java index d9120a1dbd..68b6cf7bae 100644 --- a/prism/src/parser/ast/ForLoop.java +++ b/prism/src/parser/ast/ForLoop.java @@ -138,21 +138,21 @@ public String toString() s += ":" + to; return s; } - - /** - * Perform a deep copy. - */ - public ASTElement deepCopy() - { - ForLoop ret = new ForLoop(); - ret.lhs = lhs; - ret.from = from.deepCopy(); - ret.to = to.deepCopy(); - ret.step = step.deepCopy(); - ret.pc = pc; - ret.between = between; - ret.setPosition(this); - return ret; + + @Override + public ForLoop deepCopy(DeepCopy copier) throws PrismLangException + { + from = copier.copy(from); + to = copier.copy(to); + step = copier.copy(step); + + return this; + } + + @Override + public ForLoop clone() + { + return (ForLoop) super.clone(); } } diff --git a/prism/src/parser/ast/FormulaList.java b/prism/src/parser/ast/FormulaList.java index f7cd15501a..3248805e34 100644 --- a/prism/src/parser/ast/FormulaList.java +++ b/prism/src/parser/ast/FormulaList.java @@ -34,7 +34,7 @@ // class to store list of formulas -public class FormulaList extends ASTElement +public class FormulaList extends ASTElement implements Cloneable { // Name/expression pairs to define formulas private Vector names; @@ -155,19 +155,26 @@ public String toString() return s; } - /** - * Perform a deep copy. - */ - public ASTElement deepCopy() + @Override + public FormulaList deepCopy(DeepCopy copier) throws PrismLangException { - int i, n; - FormulaList ret = new FormulaList(); - n = size(); - for (i = 0; i < n; i++) { - ret.addFormula((ExpressionIdent)getFormulaNameIdent(i).deepCopy(), getFormula(i).deepCopy()); - } - ret.setPosition(this); - return ret; + copier.copyAll(formulas); + copier.copyAll(nameIdents); + + return this; + } + + @SuppressWarnings("unchecked") + @Override + public FormulaList clone() + { + FormulaList clone = (FormulaList) super.clone(); + + clone.formulas = (Vector) formulas.clone(); + clone.nameIdents = (Vector) nameIdents.clone(); + clone.names = (Vector) names.clone(); + + return clone; } } diff --git a/prism/src/parser/ast/LabelList.java b/prism/src/parser/ast/LabelList.java index 5dfebec5e9..022f501301 100644 --- a/prism/src/parser/ast/LabelList.java +++ b/prism/src/parser/ast/LabelList.java @@ -31,14 +31,15 @@ import java.util.Vector; import parser.visitor.ASTVisitor; +import parser.visitor.DeepCopy; import prism.PrismLangException; // class to store list of labels -public class LabelList extends ASTElement +public class LabelList extends ASTElement implements Cloneable { // Name/expression pairs to define labels - private List names; + private ArrayList names; private Vector labels; // We also store an ExpressionIdent to match each name. // This is to just to provide positional info. @@ -134,20 +135,27 @@ public String toString() return s; } - - /** - * Perform a deep copy. - */ - public ASTElement deepCopy() + + @Override + public LabelList deepCopy(DeepCopy copier) throws PrismLangException { - int i, n; - LabelList ret = new LabelList(); - n = size(); - for (i = 0; i < n; i++) { - ret.addLabel((ExpressionIdent)getLabelNameIdent(i).deepCopy(), getLabel(i).deepCopy()); - } - ret.setPosition(this); - return ret; + copier.copyAll(labels); + copier.copyAll(nameIdents); + + return this; + } + + @SuppressWarnings("unchecked") + @Override + public LabelList clone() + { + LabelList clone = (LabelList) super.clone(); + + clone.labels = (Vector) labels.clone(); + clone.nameIdents = (Vector) nameIdents.clone(); + clone.names = (ArrayList) names.clone(); + + return clone; } } diff --git a/prism/src/parser/ast/Module.java b/prism/src/parser/ast/Module.java index e604b55749..0ef86781de 100644 --- a/prism/src/parser/ast/Module.java +++ b/prism/src/parser/ast/Module.java @@ -281,28 +281,32 @@ public String toString() return s; } - - /** - * Perform a deep copy. - */ - public ASTElement deepCopy() + + @Override + public Module deepCopy(DeepCopy copier) throws PrismLangException { - int i, n; - Module ret = new Module(name); - if (nameASTElement != null) - ret.setNameASTElement((ExpressionIdent)nameASTElement.deepCopy()); - n = getNumDeclarations(); - for (i = 0; i < n; i++) { - ret.addDeclaration((Declaration)getDeclaration(i).deepCopy()); - } - n = getNumCommands(); - for (i = 0; i < n; i++) { - ret.addCommand((Command)getCommand(i).deepCopy()); + nameASTElement = copier.copy(nameASTElement); + invariant = copier.copy(invariant); + copier.copyAll(decls); + copier.copyAll(commands); + + return this; + } + + @SuppressWarnings("unchecked") + @Override + public Module clone() + { + Module clone = (Module) super.clone(); + + clone.decls = (ArrayList) decls.clone(); + clone.commands = (ArrayList) commands.clone(); + + if (alphabet != null) { + clone.alphabet = (Vector) alphabet.clone(); } - if (invariant != null) - ret.setInvariant(invariant.deepCopy()); - ret.setPosition(this); - return ret; + + return clone; } } diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java index 9faaf5196d..2abb831073 100644 --- a/prism/src/parser/ast/ModulesFile.java +++ b/prism/src/parser/ast/ModulesFile.java @@ -53,7 +53,7 @@ public class ModulesFile extends ASTElement implements ModelInfo private ArrayList systemDefns; // System definitions (system...endsystem constructs) private ArrayList systemDefnNames; // System definition names (system...endsystem constructs) private ArrayList rewardStructs; // Rewards structures - private List rewardStructNames; // Names of reward structures + private ArrayList rewardStructNames; // Names of reward structures private Expression initStates; // Initial states specification // Lists of all identifiers used @@ -1267,57 +1267,59 @@ public String toString() return s; } - /** - * Perform a deep copy. - */ - @SuppressWarnings("unchecked") - public ASTElement deepCopy() - { - int i, n; - ModulesFile ret = new ModulesFile(); - - // Copy ASTElement stuff - ret.setPosition(this); - // Copy type - ret.setModelType(modelType); - // Deep copy main components - ret.setFormulaList((FormulaList) formulaList.deepCopy()); - ret.setLabelList((LabelList) labelList.deepCopy()); - ret.setConstantList((ConstantList) constantList.deepCopy()); - n = getNumGlobals(); - for (i = 0; i < n; i++) { - ret.addGlobal((Declaration) getGlobal(i).deepCopy()); - } - n = getNumModules(); - for (i = 0; i < n; i++) { - ret.addModule((Module) getModule(i).deepCopy()); - } - n = getNumSystemDefns(); - for (i = 0; i < n; i++) { - ret.addSystemDefn(getSystemDefn(i).deepCopy(), getSystemDefnName(i)); - } - n = getNumRewardStructs(); - for (i = 0; i < n; i++) { - ret.addRewardStruct((RewardStruct) getRewardStruct(i).deepCopy()); - } - if (initStates != null) - ret.setInitialStates(initStates.deepCopy()); - // Copy other (generated) info - ret.formulaIdents = (formulaIdents == null) ? null : (Vector)formulaIdents.clone(); - ret.constantIdents = (constantIdents == null) ? null : (Vector)constantIdents.clone(); - ret.varIdents = (varIdents == null) ? null : (Vector)varIdents.clone(); - ret.moduleNames = (moduleNames == null) ? null : moduleNames.clone(); - ret.synchs = (synchs == null) ? null : (Vector)synchs.clone(); - if (varDecls != null) { - ret.varDecls = new Vector(); - for (Declaration d : varDecls) - ret.varDecls.add((Declaration) d.deepCopy()); + @Override + public ModulesFile deepCopy(DeepCopy copier) throws PrismLangException + { + // deep copy main components + formulaList = copier.copy(formulaList); + labelList = copier.copy(labelList); + constantList = copier.copy(constantList); + initStates = copier.copy(initStates); + copier.copyAll(globals); + copier.copyAll(systemDefns); + copier.copyAll(rewardStructs); + copier.copyAll(varDecls); + for (int i = 0, n = getNumModules(); i < n; i++) { + // only change modules and ignore other objects (== null) + if (getModule(i) != null) { + setModule(i, copier.copy(getModule(i))); + } } - ret.varNames = (varNames == null) ? null : (Vector)varNames.clone(); - ret.varTypes = (varTypes == null) ? null : (Vector)varTypes.clone(); - ret.constantValues = (constantValues == null) ? null : new Values(constantValues); - - return ret; + + return this; + } + + @SuppressWarnings("unchecked") + @Override + public ModulesFile clone() + { + ModulesFile clone = (ModulesFile) super.clone(); + + // clone main components + clone.globals = (Vector) globals.clone(); + clone.modules = (Vector) modules.clone(); + clone.systemDefnNames = (ArrayList) systemDefnNames.clone(); + clone.systemDefns = (ArrayList) systemDefns.clone(); + clone.rewardStructs = (ArrayList) rewardStructs.clone(); + clone.rewardStructNames = (ArrayList) rewardStructNames.clone(); + clone.formulaIdents = (Vector) formulaIdents.clone(); + clone.constantIdents = (Vector) constantIdents.clone(); + clone.varIdents = (Vector) varIdents.clone(); + clone.varDecls = (Vector) varDecls.clone(); + clone.varNames = (Vector) varNames.clone(); + clone.varTypes = (Vector) varTypes.clone(); + + // clone other (generated) info + if (constantValues != null) + clone.constantValues = (Values) constantValues.clone(); + if (undefinedConstantValues != null) + clone.undefinedConstantValues = (Values) undefinedConstantValues.clone(); + if (moduleNames != null) + clone.moduleNames = moduleNames.clone(); + if (synchs != null) + clone.synchs = (Vector) synchs.clone(); + + return clone; } } diff --git a/prism/src/parser/ast/PropertiesFile.java b/prism/src/parser/ast/PropertiesFile.java index 050bf4aae7..87891e3260 100644 --- a/prism/src/parser/ast/PropertiesFile.java +++ b/prism/src/parser/ast/PropertiesFile.java @@ -36,7 +36,7 @@ // Class representing parsed properties file/list -public class PropertiesFile extends ASTElement +public class PropertiesFile extends ASTElement implements Cloneable { // Associated ModulesFile (for constants, ...) private ModulesFile modulesFile; @@ -619,30 +619,35 @@ public String toString() return s; } - /** - * Perform a deep copy. - */ + @Override + public PropertiesFile deepCopy(DeepCopy copier) throws PrismLangException + { + // deep copy main components + formulaList = copier.copy(formulaList); + labelList = copier.copy(labelList); + combinedLabelList = copier.copy(combinedLabelList); + constantList = copier.copy(constantList); + copier.copyAll(properties); + + return this; + } + @SuppressWarnings("unchecked") - public ASTElement deepCopy() + @Override + public PropertiesFile clone() { - int i, n; - PropertiesFile ret = new PropertiesFile(modelInfo); - // Copy ASTElement stuff - ret.setPosition(this); - // Deep copy main components - ret.setFormulaList((FormulaList) formulaList.deepCopy()); - ret.setLabelList((LabelList) labelList.deepCopy()); - ret.combinedLabelList = (LabelList) combinedLabelList.deepCopy(); - ret.setConstantList((ConstantList) constantList.deepCopy()); - n = getNumProperties(); - for (i = 0; i < n; i++) { - ret.addProperty((Property) getPropertyObject(i).deepCopy()); - } - // Copy other (generated) info - ret.allIdentsUsed = (allIdentsUsed == null) ? null : (Vector) allIdentsUsed.clone(); - ret.constantValues = (constantValues == null) ? null : new Values(constantValues); + PropertiesFile clone = (PropertiesFile) super.clone(); + + // clone main components + clone.properties = (Vector) properties.clone(); + + // clone other (generated) info + if (allIdentsUsed != null) + clone.allIdentsUsed = (Vector) allIdentsUsed.clone(); + if (constantValues != null) + clone.constantValues = new Values(constantValues); - return ret; + return clone; } } diff --git a/prism/src/parser/ast/Property.java b/prism/src/parser/ast/Property.java index 8469d8d1be..b8bb1ceb33 100644 --- a/prism/src/parser/ast/Property.java +++ b/prism/src/parser/ast/Property.java @@ -581,12 +581,17 @@ public String toString() } @Override - public Property deepCopy() + public Property deepCopy(DeepCopy copier) throws PrismLangException { - Property prop = new Property(expr, name, comment); - prop.setType(type); - prop.setPosition(this); - return prop; + expr = copier.copy(expr); + + return this; + } + + @Override + public Property clone() + { + return (Property) super.clone(); } } diff --git a/prism/src/parser/ast/RenamedModule.java b/prism/src/parser/ast/RenamedModule.java index eb9dc98561..99bfccd30c 100644 --- a/prism/src/parser/ast/RenamedModule.java +++ b/prism/src/parser/ast/RenamedModule.java @@ -183,22 +183,30 @@ public String toString() return s; } - - /** - * Perform a deep copy. - */ - public ASTElement deepCopy() - { - int i, n; - RenamedModule ret = new RenamedModule(name, baseModule); - ret.setNameASTElement((ExpressionIdent)nameASTElement.deepCopy()); - ret.setBaseModuleASTElement((ExpressionIdent)baseModuleASTElement.deepCopy()); - n = oldNames.size(); - for (i = 0; i < n; i++) { - ret.addRename(oldNames.get(i), newNames.get(i)); - } - ret.setPosition(this); - return ret; + + @Override + public RenamedModule deepCopy(DeepCopy copier) throws PrismLangException + { + nameASTElement = copier.copy(nameASTElement); + baseModuleASTElement = copier.copy(baseModuleASTElement); + copier.copyAll(newNameASTElements); + copier.copyAll(oldNameASTElements); + + return this; + } + + @SuppressWarnings("unchecked") + @Override + public RenamedModule clone() + { + RenamedModule clone = (RenamedModule) super.clone(); + + clone.newNameASTElements = (ArrayList) newNameASTElements.clone(); + clone.newNames = (ArrayList) newNames.clone(); + clone.oldNameASTElements = (ArrayList) oldNameASTElements.clone(); + clone.oldNames = (ArrayList) oldNames.clone(); + + return clone; } } diff --git a/prism/src/parser/ast/RewardStruct.java b/prism/src/parser/ast/RewardStruct.java index 67dd2445af..47dd897088 100644 --- a/prism/src/parser/ast/RewardStruct.java +++ b/prism/src/parser/ast/RewardStruct.java @@ -144,21 +144,24 @@ public String toString() return s; } - - /** - * Perform a deep copy. - */ - public ASTElement deepCopy() + + @Override + public RewardStruct deepCopy(DeepCopy copier) throws PrismLangException { - int i, n; - RewardStruct ret = new RewardStruct(); - ret.setName(name); - n = getNumItems(); - for (i = 0; i < n; i++) { - ret.addItem((RewardStructItem)getRewardStructItem(i).deepCopy()); - } - ret.setPosition(this); - return ret; + copier.copyAll(items); + + return this; + } + + @SuppressWarnings("unchecked") + @Override + public RewardStruct clone() + { + RewardStruct clone = (RewardStruct) super.clone(); + + clone.items = (Vector) items.clone(); + + return clone; } } diff --git a/prism/src/parser/ast/RewardStructItem.java b/prism/src/parser/ast/RewardStructItem.java index 0f8af694a4..2ff23376f8 100644 --- a/prism/src/parser/ast/RewardStructItem.java +++ b/prism/src/parser/ast/RewardStructItem.java @@ -138,16 +138,20 @@ public String toString() return s; } - - /** - * Perform a deep copy. - */ - public ASTElement deepCopy() + + @Override + public RewardStructItem deepCopy(DeepCopy copier) throws PrismLangException + { + states = copier.copy(states); + reward = copier.copy(reward); + + return this; + } + + @Override + public RewardStructItem clone() { - RewardStructItem ret = new RewardStructItem(synch, states.deepCopy(), reward.deepCopy()); - ret.setSynchIndex(getSynchIndex()); - ret.setPosition(this); - return ret; + return (RewardStructItem) super.clone(); } } diff --git a/prism/src/parser/ast/SystemBrackets.java b/prism/src/parser/ast/SystemBrackets.java index abd1ceeaea..a6fe663836 100644 --- a/prism/src/parser/ast/SystemBrackets.java +++ b/prism/src/parser/ast/SystemBrackets.java @@ -112,13 +112,19 @@ public String toString() { return "(" + operand + ")"; } - + + @Override + public SystemBrackets deepCopy(DeepCopy copier) throws PrismLangException + { + operand = copier.copy(operand); + + return this; + } + @Override - public SystemDefn deepCopy() + public SystemBrackets clone() { - SystemDefn ret = new SystemBrackets(getOperand().deepCopy()); - ret.setPosition(this); - return ret; + return (SystemBrackets) super.clone(); } } diff --git a/prism/src/parser/ast/SystemDefn.java b/prism/src/parser/ast/SystemDefn.java index e52938dc5c..8e82030df7 100644 --- a/prism/src/parser/ast/SystemDefn.java +++ b/prism/src/parser/ast/SystemDefn.java @@ -30,13 +30,6 @@ public abstract class SystemDefn extends ASTElement { - // Overrided version of deepCopy() from superclass ASTElement (to reduce casting). - - /** - * Perform a deep copy. - */ - public abstract SystemDefn deepCopy(); - // Methods required for SystemDefn (all subclasses should implement): /** diff --git a/prism/src/parser/ast/SystemFullParallel.java b/prism/src/parser/ast/SystemFullParallel.java index 8b4ef70192..73b1101574 100644 --- a/prism/src/parser/ast/SystemFullParallel.java +++ b/prism/src/parser/ast/SystemFullParallel.java @@ -148,18 +148,24 @@ public String toString() return s; } - + @Override - public SystemDefn deepCopy() + public SystemFullParallel deepCopy(DeepCopy copier) throws PrismLangException { - int i, n; - SystemFullParallel ret = new SystemFullParallel(); - n = getNumOperands(); - for (i = 0; i < n; i++) { - ret.addOperand(getOperand(i).deepCopy()); - } - ret.setPosition(this); - return ret; + copier.copyAll(operands); + + return this; + } + + @SuppressWarnings("unchecked") + @Override + public SystemFullParallel clone() + { + SystemFullParallel clone = (SystemFullParallel) super.clone(); + + clone.operands = (Vector) operands.clone(); + + return clone; } } diff --git a/prism/src/parser/ast/SystemHide.java b/prism/src/parser/ast/SystemHide.java index c8931b6534..f9522778b5 100644 --- a/prism/src/parser/ast/SystemHide.java +++ b/prism/src/parser/ast/SystemHide.java @@ -152,18 +152,24 @@ public String toString() return s; } - + @Override - public SystemDefn deepCopy() + public SystemHide deepCopy(DeepCopy copier) throws PrismLangException { - int i, n; - SystemHide ret = new SystemHide(getOperand().deepCopy()); - n = getNumActions(); - for (i = 0; i < n; i++) { - ret.addAction(getAction(i)); - } - ret.setPosition(this); - return ret; + operand = copier.copy(operand); + + return this; + } + + @SuppressWarnings("unchecked") + @Override + public SystemHide clone() + { + SystemHide clone = (SystemHide) super.clone(); + + clone.actions = (Vector) actions.clone(); + + return clone; } } diff --git a/prism/src/parser/ast/SystemInterleaved.java b/prism/src/parser/ast/SystemInterleaved.java index 193a916e8b..76844e9893 100644 --- a/prism/src/parser/ast/SystemInterleaved.java +++ b/prism/src/parser/ast/SystemInterleaved.java @@ -148,18 +148,24 @@ public String toString() return s; } - + @Override - public SystemDefn deepCopy() + public SystemInterleaved deepCopy(DeepCopy copier) throws PrismLangException { - int i, n; - SystemInterleaved ret = new SystemInterleaved(); - n = getNumOperands(); - for (i = 0; i < n; i++) { - ret.addOperand(getOperand(i).deepCopy()); - } - ret.setPosition(this); - return ret; + copier.copyAll(operands); + + return this; + } + + @SuppressWarnings("unchecked") + @Override + public SystemInterleaved clone() + { + SystemInterleaved clone = (SystemInterleaved) super.clone(); + + clone.operands = (Vector) operands.clone(); + + return clone; } } diff --git a/prism/src/parser/ast/SystemModule.java b/prism/src/parser/ast/SystemModule.java index b5d40aa0fb..8e71bb5cd5 100644 --- a/prism/src/parser/ast/SystemModule.java +++ b/prism/src/parser/ast/SystemModule.java @@ -106,13 +106,17 @@ public String toString() { return name; } - + + @Override + public SystemModule deepCopy(DeepCopy copier) throws PrismLangException + { + return this; + } + @Override - public SystemDefn deepCopy() + public SystemModule clone() { - SystemDefn ret = new SystemModule(name); - ret.setPosition(this); - return ret; + return (SystemModule) super.clone(); } } diff --git a/prism/src/parser/ast/SystemParallel.java b/prism/src/parser/ast/SystemParallel.java index 383a242c8c..51d04c540a 100644 --- a/prism/src/parser/ast/SystemParallel.java +++ b/prism/src/parser/ast/SystemParallel.java @@ -167,17 +167,25 @@ public String toString() return s; } - + @Override + public SystemParallel deepCopy(DeepCopy copier) throws PrismLangException + { + operand1 = copier.copy(operand1); + operand2 = copier.copy(operand2); + + return this; + } + @SuppressWarnings("unchecked") - public SystemDefn deepCopy() - { - SystemParallel ret = new SystemParallel(); - ret.setOperand1(getOperand1().deepCopy()); - ret.setOperand2(getOperand2().deepCopy()); - ret.actions = (actions == null) ? null : (Vector)actions.clone(); - ret.setPosition(this); - return ret; + @Override + public SystemParallel clone() + { + SystemParallel clone = (SystemParallel) super.clone(); + + clone.actions = (Vector) actions.clone(); + + return clone; } } diff --git a/prism/src/parser/ast/SystemReference.java b/prism/src/parser/ast/SystemReference.java index 1312ab5b69..cca5dd0d09 100644 --- a/prism/src/parser/ast/SystemReference.java +++ b/prism/src/parser/ast/SystemReference.java @@ -111,13 +111,17 @@ public String toString() { return "\"" + name + "\""; } - + + @Override + public SystemReference deepCopy(DeepCopy copier) throws PrismLangException + { + return this; + } + @Override - public SystemDefn deepCopy() + public SystemReference clone() { - SystemDefn ret = new SystemReference(name); - ret.setPosition(this); - return ret; + return (SystemReference) super.clone(); } } diff --git a/prism/src/parser/ast/SystemRename.java b/prism/src/parser/ast/SystemRename.java index ce03b9c73d..1732cd724e 100644 --- a/prism/src/parser/ast/SystemRename.java +++ b/prism/src/parser/ast/SystemRename.java @@ -197,16 +197,23 @@ public String toString() } @Override - public SystemDefn deepCopy() + public SystemRename deepCopy(DeepCopy copier) throws PrismLangException { - int i, n; - SystemRename ret = new SystemRename(getOperand().deepCopy()); - n = getNumRenames(); - for (i = 0; i < n; i++) { - ret.addRename(getFrom(i), getTo(i)); - } - ret.setPosition(this); - return ret; + operand = copier.copy(operand); + + return this; + } + + @SuppressWarnings("unchecked") + @Override + public SystemRename clone() + { + SystemRename clone = (SystemRename) super.clone(); + + clone.from = (Vector) from.clone(); + clone.to = (Vector) to.clone(); + + return clone; } } diff --git a/prism/src/parser/ast/Update.java b/prism/src/parser/ast/Update.java index 952e1b71f4..67f4ec0fdf 100644 --- a/prism/src/parser/ast/Update.java +++ b/prism/src/parser/ast/Update.java @@ -27,7 +27,6 @@ package parser.ast; import java.util.ArrayList; -import java.util.BitSet; import parser.*; import parser.type.*; @@ -335,21 +334,28 @@ public String toString() return s; } - /** - * Perform a deep copy. - */ - public ASTElement deepCopy() + @Override + public Update deepCopy(DeepCopy copier) throws PrismLangException { - 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)); - } - ret.setPosition(this); - return ret; + copier.copyAll(exprs); + copier.copyAll(varIdents); + + return this; + } + + @SuppressWarnings("unchecked") + @Override + public Update clone() + { + Update clone = (Update) super.clone(); + + clone.indices = (ArrayList) indices.clone(); + clone.vars = (ArrayList) vars.clone(); + clone.exprs = (ArrayList) exprs.clone(); + clone.types = (ArrayList) types.clone(); + clone.varIdents = (ArrayList) varIdents.clone(); + + return clone; } } diff --git a/prism/src/parser/ast/Updates.java b/prism/src/parser/ast/Updates.java index ef92421057..551488281d 100644 --- a/prism/src/parser/ast/Updates.java +++ b/prism/src/parser/ast/Updates.java @@ -148,6 +148,7 @@ public Command getParent() /** * Visitor method. */ + @Override public Object accept(ASTVisitor v) throws PrismLangException { return v.visit(this); @@ -174,23 +175,25 @@ public String toString() return s; } - /** - * Perform a deep copy. - */ - public ASTElement deepCopy() + @Override + public Updates deepCopy(DeepCopy copier) throws PrismLangException { - int i, n; - Expression p; - Updates ret = new Updates(); - n = getNumUpdates(); - for (i = 0; i < n; i++) { - p = getProbability(i); - if (p != null) - p = p.deepCopy(); - ret.addUpdate(p, (Update) getUpdate(i).deepCopy()); - } - ret.setPosition(this); - return ret; + copier.copyAll(probs); + copier.copyAll(updates); + + return this; + } + + @SuppressWarnings("unchecked") + @Override + public Updates clone() + { + Updates clone = (Updates) super.clone(); + + clone.probs = (ArrayList) probs.clone(); + clone.updates = (ArrayList) updates.clone(); + + return clone; } } diff --git a/prism/src/parser/visitor/ASTTraverse.java b/prism/src/parser/visitor/ASTTraverse.java index d8ee27aaf1..992146f24c 100644 --- a/prism/src/parser/visitor/ASTTraverse.java +++ b/prism/src/parser/visitor/ASTTraverse.java @@ -27,21 +27,26 @@ package parser.visitor; import parser.ast.*; +import parser.ast.Module; import prism.PrismLangException; -// Performs a depth-first traversal of an asbtract syntax tree (AST). -// Many traversal-based tasks can be implemented by extending and either: -// (a) overriding defaultVisitPre or defaultVisitPost -// (b) overiding visit for leaf (or other selected) nodes -// See also ASTTraverseModify. - -public class ASTTraverse implements ASTVisitor +/** + * Performs a depth-first traversal of an abstract syntax tree (AST). + * + * Many traversal-based tasks can be implemented by extending and either: + *
    + *
  • overriding defaultVisitPre or defaultVisitPost
    • + *
  • overriding visit for leaf (or other selected) nodes
    • + *
+ * @see ASTTraverseModify + */ +public class ASTTraverse extends DAGVisitor { public void defaultVisitPre(ASTElement e) throws PrismLangException {} public void defaultVisitPost(ASTElement e) throws PrismLangException {} // ----------------------------------------------------------------------------------- public void visitPre(ModulesFile e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ModulesFile e) throws PrismLangException + public Object visitNow(ModulesFile e) throws PrismLangException { visitPre(e); int i, n; @@ -68,7 +73,7 @@ public Object visit(ModulesFile e) throws PrismLangException public void visitPost(ModulesFile e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(PropertiesFile e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(PropertiesFile e) throws PrismLangException + public Object visitNow(PropertiesFile e) throws PrismLangException { visitPre(e); int i, n; @@ -84,7 +89,7 @@ public Object visit(PropertiesFile e) throws PrismLangException public void visitPost(PropertiesFile e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(Property e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(Property e) throws PrismLangException + public Object visitNow(Property e) throws PrismLangException { visitPre(e); if (e.getExpression() != null) e.getExpression().accept(this); @@ -94,7 +99,7 @@ public Object visit(Property e) throws PrismLangException public void visitPost(Property e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(FormulaList e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(FormulaList e) throws PrismLangException + public Object visitNow(FormulaList e) throws PrismLangException { visitPre(e); int i, n; @@ -108,7 +113,7 @@ public Object visit(FormulaList e) throws PrismLangException public void visitPost(FormulaList e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(LabelList e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(LabelList e) throws PrismLangException + public Object visitNow(LabelList e) throws PrismLangException { visitPre(e); int i, n; @@ -122,7 +127,7 @@ public Object visit(LabelList e) throws PrismLangException public void visitPost(LabelList e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ConstantList e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ConstantList e) throws PrismLangException + public Object visitNow(ConstantList e) throws PrismLangException { visitPre(e); int i, n; @@ -136,7 +141,7 @@ public Object visit(ConstantList e) throws PrismLangException public void visitPost(ConstantList e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(Declaration e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(Declaration e) throws PrismLangException + public Object visitNow(Declaration e) throws PrismLangException { visitPre(e); if (e.getDeclType() != null) e.getDeclType().accept(this); @@ -147,7 +152,7 @@ public Object visit(Declaration e) throws PrismLangException public void visitPost(Declaration e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(DeclarationInt e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(DeclarationInt e) throws PrismLangException + public Object visitNow(DeclarationInt e) throws PrismLangException { visitPre(e); if (e.getLow() != null) e.getLow().accept(this); @@ -158,7 +163,7 @@ public Object visit(DeclarationInt e) throws PrismLangException public void visitPost(DeclarationInt e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(DeclarationBool e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(DeclarationBool e) throws PrismLangException + public Object visitNow(DeclarationBool e) throws PrismLangException { visitPre(e); visitPost(e); @@ -167,7 +172,7 @@ public Object visit(DeclarationBool e) throws PrismLangException public void visitPost(DeclarationBool e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(DeclarationArray e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(DeclarationArray e) throws PrismLangException + public Object visitNow(DeclarationArray e) throws PrismLangException { visitPre(e); if (e.getLow() != null) e.getLow().accept(this); @@ -179,7 +184,7 @@ public Object visit(DeclarationArray e) throws PrismLangException public void visitPost(DeclarationArray e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(DeclarationClock e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(DeclarationClock e) throws PrismLangException + public Object visitNow(DeclarationClock e) throws PrismLangException { visitPre(e); visitPost(e); @@ -188,7 +193,7 @@ public Object visit(DeclarationClock e) throws PrismLangException public void visitPost(DeclarationClock e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(DeclarationIntUnbounded e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(DeclarationIntUnbounded e) throws PrismLangException + public Object visitNow(DeclarationIntUnbounded e) throws PrismLangException { visitPre(e); visitPost(e); @@ -196,8 +201,8 @@ public Object visit(DeclarationIntUnbounded e) throws PrismLangException } public void visitPost(DeclarationIntUnbounded e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- - public void visitPre(parser.ast.Module e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(parser.ast.Module e) throws PrismLangException + public void visitPre(Module e) throws PrismLangException { defaultVisitPre(e); } + public Object visitNow(Module e) throws PrismLangException { // Note: a few classes override this method (e.g. SemanticCheck) // so take care to update those versions if changing this method @@ -216,10 +221,10 @@ public Object visit(parser.ast.Module e) throws PrismLangException visitPost(e); return null; } - public void visitPost(parser.ast.Module e) throws PrismLangException { defaultVisitPost(e); } + public void visitPost(Module e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(Command e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(Command e) throws PrismLangException + public Object visitNow(Command e) throws PrismLangException { // Note: a few classes override this method (e.g. SemanticCheck) // so take care to update those versions if changing this method @@ -232,7 +237,7 @@ public Object visit(Command e) throws PrismLangException public void visitPost(Command e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(Updates e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(Updates e) throws PrismLangException + public Object visitNow(Updates e) throws PrismLangException { visitPre(e); int i, n; @@ -247,7 +252,7 @@ public Object visit(Updates e) throws PrismLangException public void visitPost(Updates e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(Update e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(Update e) throws PrismLangException + public Object visitNow(Update e) throws PrismLangException { visitPre(e); int i, n; @@ -261,7 +266,7 @@ public Object visit(Update e) throws PrismLangException public void visitPost(Update e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(RenamedModule e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(RenamedModule e) throws PrismLangException + public Object visitNow(RenamedModule e) throws PrismLangException { visitPre(e); visitPost(e); @@ -270,7 +275,7 @@ public Object visit(RenamedModule e) throws PrismLangException public void visitPost(RenamedModule e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(RewardStruct e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(RewardStruct e) throws PrismLangException + public Object visitNow(RewardStruct e) throws PrismLangException { visitPre(e); int i, n; @@ -284,7 +289,7 @@ public Object visit(RewardStruct e) throws PrismLangException public void visitPost(RewardStruct e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(RewardStructItem e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(RewardStructItem e) throws PrismLangException + public Object visitNow(RewardStructItem e) throws PrismLangException { visitPre(e); e.getStates().accept(this); @@ -295,7 +300,7 @@ public Object visit(RewardStructItem e) throws PrismLangException public void visitPost(RewardStructItem e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(SystemInterleaved e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(SystemInterleaved e) throws PrismLangException + public Object visitNow(SystemInterleaved e) throws PrismLangException { visitPre(e); int i, n = e.getNumOperands(); @@ -308,7 +313,7 @@ public Object visit(SystemInterleaved e) throws PrismLangException public void visitPost(SystemInterleaved e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(SystemFullParallel e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(SystemFullParallel e) throws PrismLangException + public Object visitNow(SystemFullParallel e) throws PrismLangException { visitPre(e); int i, n = e.getNumOperands(); @@ -321,7 +326,7 @@ public Object visit(SystemFullParallel e) throws PrismLangException public void visitPost(SystemFullParallel e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(SystemParallel e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(SystemParallel e) throws PrismLangException + public Object visitNow(SystemParallel e) throws PrismLangException { visitPre(e); e.getOperand1().accept(this); @@ -332,7 +337,7 @@ public Object visit(SystemParallel e) throws PrismLangException public void visitPost(SystemParallel e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(SystemHide e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(SystemHide e) throws PrismLangException + public Object visitNow(SystemHide e) throws PrismLangException { visitPre(e); e.getOperand().accept(this); @@ -342,7 +347,7 @@ public Object visit(SystemHide e) throws PrismLangException public void visitPost(SystemHide e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(SystemRename e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(SystemRename e) throws PrismLangException + public Object visitNow(SystemRename e) throws PrismLangException { visitPre(e); e.getOperand().accept(this); @@ -352,7 +357,7 @@ public Object visit(SystemRename e) throws PrismLangException public void visitPost(SystemRename e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(SystemModule e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(SystemModule e) throws PrismLangException + public Object visitNow(SystemModule e) throws PrismLangException { visitPre(e); visitPost(e); @@ -361,7 +366,7 @@ public Object visit(SystemModule e) throws PrismLangException public void visitPost(SystemModule e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(SystemBrackets e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(SystemBrackets e) throws PrismLangException + public Object visitNow(SystemBrackets e) throws PrismLangException { visitPre(e); e.getOperand().accept(this); @@ -371,7 +376,7 @@ public Object visit(SystemBrackets e) throws PrismLangException public void visitPost(SystemBrackets e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(SystemReference e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(SystemReference e) throws PrismLangException + public Object visitNow(SystemReference e) throws PrismLangException { visitPre(e); visitPost(e); @@ -380,7 +385,7 @@ public Object visit(SystemReference e) throws PrismLangException public void visitPost(SystemReference e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionTemporal e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionTemporal e) throws PrismLangException + public Object visitNow(ExpressionTemporal e) throws PrismLangException { visitPre(e); if (e.getOperand1() != null) e.getOperand1().accept(this); @@ -393,7 +398,7 @@ public Object visit(ExpressionTemporal e) throws PrismLangException public void visitPost(ExpressionTemporal e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionITE e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionITE e) throws PrismLangException + public Object visitNow(ExpressionITE e) throws PrismLangException { visitPre(e); e.getOperand1().accept(this); @@ -405,7 +410,7 @@ public Object visit(ExpressionITE e) throws PrismLangException public void visitPost(ExpressionITE e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionBinaryOp e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionBinaryOp e) throws PrismLangException + public Object visitNow(ExpressionBinaryOp e) throws PrismLangException { visitPre(e); e.getOperand1().accept(this); @@ -416,7 +421,7 @@ public Object visit(ExpressionBinaryOp e) throws PrismLangException public void visitPost(ExpressionBinaryOp e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionUnaryOp e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionUnaryOp e) throws PrismLangException + public Object visitNow(ExpressionUnaryOp e) throws PrismLangException { visitPre(e); e.getOperand().accept(this); @@ -426,7 +431,7 @@ public Object visit(ExpressionUnaryOp e) throws PrismLangException public void visitPost(ExpressionUnaryOp e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionFunc e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionFunc e) throws PrismLangException + public Object visitNow(ExpressionFunc e) throws PrismLangException { visitPre(e); int i, n = e.getNumOperands(); @@ -439,7 +444,7 @@ public Object visit(ExpressionFunc e) throws PrismLangException public void visitPost(ExpressionFunc e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionIdent e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionIdent e) throws PrismLangException + public Object visitNow(ExpressionIdent e) throws PrismLangException { visitPre(e); visitPost(e); @@ -448,7 +453,7 @@ public Object visit(ExpressionIdent e) throws PrismLangException public void visitPost(ExpressionIdent e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionLiteral e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionLiteral e) throws PrismLangException + public Object visitNow(ExpressionLiteral e) throws PrismLangException { visitPre(e); visitPost(e); @@ -457,7 +462,7 @@ public Object visit(ExpressionLiteral e) throws PrismLangException public void visitPost(ExpressionLiteral e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionConstant e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionConstant e) throws PrismLangException + public Object visitNow(ExpressionConstant e) throws PrismLangException { visitPre(e); visitPost(e); @@ -466,7 +471,7 @@ public Object visit(ExpressionConstant e) throws PrismLangException public void visitPost(ExpressionConstant e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionFormula e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionFormula e) throws PrismLangException + public Object visitNow(ExpressionFormula e) throws PrismLangException { visitPre(e); if (e.getDefinition() != null) e.getDefinition().accept(this); @@ -476,7 +481,7 @@ public Object visit(ExpressionFormula e) throws PrismLangException public void visitPost(ExpressionFormula e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionVar e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionVar e) throws PrismLangException + public Object visitNow(ExpressionVar e) throws PrismLangException { visitPre(e); visitPost(e); @@ -485,7 +490,7 @@ public Object visit(ExpressionVar e) throws PrismLangException public void visitPost(ExpressionVar e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionProb e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionProb e) throws PrismLangException + public Object visitNow(ExpressionProb e) throws PrismLangException { visitPre(e); if (e.getProb() != null) e.getProb().accept(this); @@ -497,7 +502,7 @@ public Object visit(ExpressionProb e) throws PrismLangException public void visitPost(ExpressionProb e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionReward e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionReward e) throws PrismLangException + public Object visitNow(ExpressionReward e) throws PrismLangException { visitPre(e); if (e.getRewardStructIndex() != null && e.getRewardStructIndex() instanceof Expression) ((Expression)e.getRewardStructIndex()).accept(this); @@ -511,7 +516,7 @@ public Object visit(ExpressionReward e) throws PrismLangException public void visitPost(ExpressionReward e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionSS e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionSS e) throws PrismLangException + public Object visitNow(ExpressionSS e) throws PrismLangException { visitPre(e); if (e.getProb() != null) e.getProb().accept(this); @@ -523,7 +528,7 @@ public Object visit(ExpressionSS e) throws PrismLangException public void visitPost(ExpressionSS e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionExists e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionExists e) throws PrismLangException + public Object visitNow(ExpressionExists e) throws PrismLangException { visitPre(e); if (e.getExpression() != null) e.getExpression().accept(this); @@ -533,7 +538,7 @@ public Object visit(ExpressionExists e) throws PrismLangException public void visitPost(ExpressionExists e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionForAll e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionForAll e) throws PrismLangException + public Object visitNow(ExpressionForAll e) throws PrismLangException { visitPre(e); if (e.getExpression() != null) e.getExpression().accept(this); @@ -543,7 +548,7 @@ public Object visit(ExpressionForAll e) throws PrismLangException public void visitPost(ExpressionForAll e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionStrategy e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionStrategy e) throws PrismLangException + public Object visitNow(ExpressionStrategy e) throws PrismLangException { visitPre(e); int i, n = e.getNumOperands(); @@ -556,7 +561,7 @@ public Object visit(ExpressionStrategy e) throws PrismLangException public void visitPost(ExpressionStrategy e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionLabel e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionLabel e) throws PrismLangException + public Object visitNow(ExpressionLabel e) throws PrismLangException { visitPre(e); visitPost(e); @@ -565,7 +570,7 @@ public Object visit(ExpressionLabel e) throws PrismLangException public void visitPost(ExpressionLabel e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionProp e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionProp e) throws PrismLangException + public Object visitNow(ExpressionProp e) throws PrismLangException { visitPre(e); visitPost(e); @@ -574,7 +579,7 @@ public Object visit(ExpressionProp e) throws PrismLangException public void visitPost(ExpressionProp e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionFilter e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionFilter e) throws PrismLangException + public Object visitNow(ExpressionFilter e) throws PrismLangException { visitPre(e); if (e.getFilter() != null) e.getFilter().accept(this); @@ -585,7 +590,7 @@ public Object visit(ExpressionFilter e) throws PrismLangException public void visitPost(ExpressionFilter e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(Filter e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(Filter e) throws PrismLangException + public Object visitNow(Filter e) throws PrismLangException { visitPre(e); if (e.getExpression() != null) e.getExpression().accept(this); @@ -595,7 +600,7 @@ public Object visit(Filter e) throws PrismLangException public void visitPost(Filter e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ForLoop e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ForLoop e) throws PrismLangException + public Object visitNow(ForLoop e) throws PrismLangException { visitPre(e); if (e.getFrom() != null) e.getFrom().accept(this); diff --git a/prism/src/parser/visitor/ASTTraverseModify.java b/prism/src/parser/visitor/ASTTraverseModify.java index 96670422f1..68dc9dddc5 100644 --- a/prism/src/parser/visitor/ASTTraverseModify.java +++ b/prism/src/parser/visitor/ASTTraverseModify.java @@ -27,22 +27,28 @@ package parser.visitor; import parser.ast.*; +import parser.ast.Module; import prism.PrismLangException; -// Variant of ASTTraverse. -// Performs a depth-first traversal of an asbtract syntax tree (AST), -// replacing each child node with the object returned by the recursive visit call. -// Like ASTTraverse, many traversal-based tasks can be implemented by extending and either: -// (a) overriding defaultVisitPre or defaultVisitPost -// (b) overiding visit for leaf (or other selected) nodes - -public class ASTTraverseModify implements ASTVisitor +/** + * Variant of ASTTraverse. + * + * Performs a depth-first traversal of an abstract syntax tree (AST), + * replacing each child node with the object returned by the recursive visit call. + * Like ASTTraverse, many traversal-based tasks can be implemented by extending and either: + *
    + *
  • overriding defaultVisitPre or defaultVisitPost
    • + *
  • overriding visit for leaf (or other selected) nodes
    • + *
+ * @see ASTTraverse + */ +public class ASTTraverseModify extends DAGVisitor { public void defaultVisitPre(ASTElement e) throws PrismLangException {} public void defaultVisitPost(ASTElement e) throws PrismLangException {} // ----------------------------------------------------------------------------------- public void visitPre(ModulesFile e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ModulesFile e) throws PrismLangException + public Object visitNow(ModulesFile e) throws PrismLangException { visitPre(e); int i, n; @@ -72,7 +78,7 @@ public Object visit(ModulesFile e) throws PrismLangException public void visitPost(ModulesFile e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(PropertiesFile e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(PropertiesFile e) throws PrismLangException + public Object visitNow(PropertiesFile e) throws PrismLangException { visitPre(e); int i, n; @@ -93,7 +99,7 @@ public void visitPre(Property e) throws PrismLangException defaultVisitPre(e); } - public Object visit(Property e) throws PrismLangException + public Object visitNow(Property e) throws PrismLangException { visitPre(e); if (e.getExpression() != null) @@ -109,7 +115,7 @@ public void visitPost(Property e) throws PrismLangException // ----------------------------------------------------------------------------------- public void visitPre(FormulaList e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(FormulaList e) throws PrismLangException + public Object visitNow(FormulaList e) throws PrismLangException { visitPre(e); int i, n; @@ -123,7 +129,7 @@ public Object visit(FormulaList e) throws PrismLangException public void visitPost(FormulaList e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(LabelList e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(LabelList e) throws PrismLangException + public Object visitNow(LabelList e) throws PrismLangException { visitPre(e); int i, n; @@ -137,7 +143,7 @@ public Object visit(LabelList e) throws PrismLangException public void visitPost(LabelList e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ConstantList e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ConstantList e) throws PrismLangException + public Object visitNow(ConstantList e) throws PrismLangException { visitPre(e); int i, n; @@ -151,7 +157,7 @@ public Object visit(ConstantList e) throws PrismLangException public void visitPost(ConstantList e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(Declaration e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(Declaration e) throws PrismLangException + public Object visitNow(Declaration e) throws PrismLangException { visitPre(e); if (e.getDeclType() != null) e.setDeclType((DeclarationType)e.getDeclType().accept(this)); @@ -162,7 +168,7 @@ public Object visit(Declaration e) throws PrismLangException public void visitPost(Declaration e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(DeclarationInt e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(DeclarationInt e) throws PrismLangException + public Object visitNow(DeclarationInt e) throws PrismLangException { visitPre(e); if (e.getLow() != null) e.setLow((Expression)e.getLow().accept(this)); @@ -173,7 +179,7 @@ public Object visit(DeclarationInt e) throws PrismLangException public void visitPost(DeclarationInt e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(DeclarationBool e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(DeclarationBool e) throws PrismLangException + public Object visitNow(DeclarationBool e) throws PrismLangException { visitPre(e); visitPost(e); @@ -182,7 +188,7 @@ public Object visit(DeclarationBool e) throws PrismLangException public void visitPost(DeclarationBool e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(DeclarationArray e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(DeclarationArray e) throws PrismLangException + public Object visitNow(DeclarationArray e) throws PrismLangException { visitPre(e); if (e.getLow() != null) e.setLow((Expression)e.getLow().accept(this)); @@ -194,7 +200,7 @@ public Object visit(DeclarationArray e) throws PrismLangException public void visitPost(DeclarationArray e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(DeclarationClock e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(DeclarationClock e) throws PrismLangException + public Object visitNow(DeclarationClock e) throws PrismLangException { visitPre(e); visitPost(e); @@ -203,7 +209,7 @@ public Object visit(DeclarationClock e) throws PrismLangException public void visitPost(DeclarationClock e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(DeclarationIntUnbounded e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(DeclarationIntUnbounded e) throws PrismLangException + public Object visitNow(DeclarationIntUnbounded e) throws PrismLangException { visitPre(e); visitPost(e); @@ -211,8 +217,8 @@ public Object visit(DeclarationIntUnbounded e) throws PrismLangException } public void visitPost(DeclarationIntUnbounded e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- - public void visitPre(parser.ast.Module e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(parser.ast.Module e) throws PrismLangException + public void visitPre(Module e) throws PrismLangException { defaultVisitPre(e); } + public Object visitNow(Module e) throws PrismLangException { visitPre(e); int i, n; @@ -232,7 +238,7 @@ public Object visit(parser.ast.Module e) throws PrismLangException public void visitPost(parser.ast.Module e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(Command e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(Command e) throws PrismLangException + public Object visitNow(Command e) throws PrismLangException { visitPre(e); e.setGuard((Expression)(e.getGuard().accept(this))); @@ -243,7 +249,7 @@ public Object visit(Command e) throws PrismLangException public void visitPost(Command e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(Updates e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(Updates e) throws PrismLangException + public Object visitNow(Updates e) throws PrismLangException { visitPre(e); int i, n; @@ -258,7 +264,7 @@ public Object visit(Updates e) throws PrismLangException public void visitPost(Updates e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(Update e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(Update e) throws PrismLangException + public Object visitNow(Update e) throws PrismLangException { visitPre(e); int i, n; @@ -272,7 +278,7 @@ public Object visit(Update e) throws PrismLangException public void visitPost(Update e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(RenamedModule e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(RenamedModule e) throws PrismLangException + public Object visitNow(RenamedModule e) throws PrismLangException { visitPre(e); visitPost(e); @@ -281,7 +287,7 @@ public Object visit(RenamedModule e) throws PrismLangException public void visitPost(RenamedModule e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(RewardStruct e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(RewardStruct e) throws PrismLangException + public Object visitNow(RewardStruct e) throws PrismLangException { visitPre(e); int i, n; @@ -295,7 +301,7 @@ public Object visit(RewardStruct e) throws PrismLangException public void visitPost(RewardStruct e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(RewardStructItem e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(RewardStructItem e) throws PrismLangException + public Object visitNow(RewardStructItem e) throws PrismLangException { visitPre(e); e.setStates((Expression)(e.getStates().accept(this))); @@ -306,7 +312,7 @@ public Object visit(RewardStructItem e) throws PrismLangException public void visitPost(RewardStructItem e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(SystemInterleaved e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(SystemInterleaved e) throws PrismLangException + public Object visitNow(SystemInterleaved e) throws PrismLangException { visitPre(e); int i, n = e.getNumOperands(); @@ -319,7 +325,7 @@ public Object visit(SystemInterleaved e) throws PrismLangException public void visitPost(SystemInterleaved e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(SystemFullParallel e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(SystemFullParallel e) throws PrismLangException + public Object visitNow(SystemFullParallel e) throws PrismLangException { visitPre(e); int i, n = e.getNumOperands(); @@ -332,7 +338,7 @@ public Object visit(SystemFullParallel e) throws PrismLangException public void visitPost(SystemFullParallel e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(SystemParallel e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(SystemParallel e) throws PrismLangException + public Object visitNow(SystemParallel e) throws PrismLangException { visitPre(e); e.setOperand1((SystemDefn)(e.getOperand1().accept(this))); @@ -343,7 +349,7 @@ public Object visit(SystemParallel e) throws PrismLangException public void visitPost(SystemParallel e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(SystemHide e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(SystemHide e) throws PrismLangException + public Object visitNow(SystemHide e) throws PrismLangException { visitPre(e); e.setOperand((SystemDefn)(e.getOperand().accept(this))); @@ -353,7 +359,7 @@ public Object visit(SystemHide e) throws PrismLangException public void visitPost(SystemHide e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(SystemRename e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(SystemRename e) throws PrismLangException + public Object visitNow(SystemRename e) throws PrismLangException { visitPre(e); e.setOperand((SystemDefn)(e.getOperand().accept(this))); @@ -363,7 +369,7 @@ public Object visit(SystemRename e) throws PrismLangException public void visitPost(SystemRename e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(SystemModule e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(SystemModule e) throws PrismLangException + public Object visitNow(SystemModule e) throws PrismLangException { visitPre(e); visitPost(e); @@ -372,7 +378,7 @@ public Object visit(SystemModule e) throws PrismLangException public void visitPost(SystemModule e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(SystemBrackets e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(SystemBrackets e) throws PrismLangException + public Object visitNow(SystemBrackets e) throws PrismLangException { visitPre(e); e.setOperand((SystemDefn)(e.getOperand().accept(this))); @@ -382,7 +388,7 @@ public Object visit(SystemBrackets e) throws PrismLangException public void visitPost(SystemBrackets e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(SystemReference e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(SystemReference e) throws PrismLangException + public Object visitNow(SystemReference e) throws PrismLangException { visitPre(e); visitPost(e); @@ -391,7 +397,7 @@ public Object visit(SystemReference e) throws PrismLangException public void visitPost(SystemReference e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionTemporal e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionTemporal e) throws PrismLangException + public Object visitNow(ExpressionTemporal e) throws PrismLangException { visitPre(e); if (e.getOperand1() != null) e.setOperand1((Expression)(e.getOperand1().accept(this))); @@ -404,7 +410,7 @@ public Object visit(ExpressionTemporal e) throws PrismLangException public void visitPost(ExpressionTemporal e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionITE e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionITE e) throws PrismLangException + public Object visitNow(ExpressionITE e) throws PrismLangException { visitPre(e); e.setOperand1((Expression)(e.getOperand1().accept(this))); @@ -416,7 +422,7 @@ public Object visit(ExpressionITE e) throws PrismLangException public void visitPost(ExpressionITE e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionBinaryOp e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionBinaryOp e) throws PrismLangException + public Object visitNow(ExpressionBinaryOp e) throws PrismLangException { visitPre(e); e.setOperand1((Expression)(e.getOperand1().accept(this))); @@ -427,7 +433,7 @@ public Object visit(ExpressionBinaryOp e) throws PrismLangException public void visitPost(ExpressionBinaryOp e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionUnaryOp e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionUnaryOp e) throws PrismLangException + public Object visitNow(ExpressionUnaryOp e) throws PrismLangException { visitPre(e); e.setOperand((Expression)(e.getOperand().accept(this))); @@ -437,7 +443,7 @@ public Object visit(ExpressionUnaryOp e) throws PrismLangException public void visitPost(ExpressionUnaryOp e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionFunc e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionFunc e) throws PrismLangException + public Object visitNow(ExpressionFunc e) throws PrismLangException { visitPre(e); int i, n = e.getNumOperands(); @@ -450,7 +456,7 @@ public Object visit(ExpressionFunc e) throws PrismLangException public void visitPost(ExpressionFunc e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionIdent e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionIdent e) throws PrismLangException + public Object visitNow(ExpressionIdent e) throws PrismLangException { visitPre(e); visitPost(e); @@ -459,7 +465,7 @@ public Object visit(ExpressionIdent e) throws PrismLangException public void visitPost(ExpressionIdent e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionLiteral e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionLiteral e) throws PrismLangException + public Object visitNow(ExpressionLiteral e) throws PrismLangException { visitPre(e); visitPost(e); @@ -468,7 +474,7 @@ public Object visit(ExpressionLiteral e) throws PrismLangException public void visitPost(ExpressionLiteral e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionConstant e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionConstant e) throws PrismLangException + public Object visitNow(ExpressionConstant e) throws PrismLangException { visitPre(e); visitPost(e); @@ -477,7 +483,7 @@ public Object visit(ExpressionConstant e) throws PrismLangException public void visitPost(ExpressionConstant e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionFormula e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionFormula e) throws PrismLangException + public Object visitNow(ExpressionFormula e) throws PrismLangException { visitPre(e); if (e.getDefinition() != null) e.setDefinition((Expression)(e.getDefinition().accept(this))); @@ -487,7 +493,7 @@ public Object visit(ExpressionFormula e) throws PrismLangException public void visitPost(ExpressionFormula e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionVar e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionVar e) throws PrismLangException + public Object visitNow(ExpressionVar e) throws PrismLangException { visitPre(e); visitPost(e); @@ -496,7 +502,7 @@ public Object visit(ExpressionVar e) throws PrismLangException public void visitPost(ExpressionVar e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionProb e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionProb e) throws PrismLangException + public Object visitNow(ExpressionProb e) throws PrismLangException { visitPre(e); if (e.getProb() != null) e.setProb((Expression)(e.getProb().accept(this))); @@ -508,7 +514,7 @@ public Object visit(ExpressionProb e) throws PrismLangException public void visitPost(ExpressionProb e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionReward e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionReward e) throws PrismLangException + public Object visitNow(ExpressionReward e) throws PrismLangException { visitPre(e); if (e.getRewardStructIndex() != null && e.getRewardStructIndex() instanceof Expression) @@ -524,7 +530,7 @@ public Object visit(ExpressionReward e) throws PrismLangException public void visitPost(ExpressionReward e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionSS e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionSS e) throws PrismLangException + public Object visitNow(ExpressionSS e) throws PrismLangException { visitPre(e); if (e.getProb() != null) e.setProb((Expression)(e.getProb().accept(this))); @@ -536,7 +542,7 @@ public Object visit(ExpressionSS e) throws PrismLangException public void visitPost(ExpressionSS e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionExists e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionExists e) throws PrismLangException + public Object visitNow(ExpressionExists e) throws PrismLangException { visitPre(e); if (e.getExpression() != null) e.setExpression((Expression)(e.getExpression().accept(this))); @@ -546,7 +552,7 @@ public Object visit(ExpressionExists e) throws PrismLangException public void visitPost(ExpressionExists e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionForAll e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionForAll e) throws PrismLangException + public Object visitNow(ExpressionForAll e) throws PrismLangException { visitPre(e); if (e.getExpression() != null) e.setExpression((Expression)(e.getExpression().accept(this))); @@ -556,7 +562,7 @@ public Object visit(ExpressionForAll e) throws PrismLangException public void visitPost(ExpressionForAll e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionStrategy e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionStrategy e) throws PrismLangException + public Object visitNow(ExpressionStrategy e) throws PrismLangException { visitPre(e); int i, n = e.getNumOperands(); @@ -569,7 +575,7 @@ public Object visit(ExpressionStrategy e) throws PrismLangException public void visitPost(ExpressionStrategy e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionLabel e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionLabel e) throws PrismLangException + public Object visitNow(ExpressionLabel e) throws PrismLangException { visitPre(e); visitPost(e); @@ -578,7 +584,7 @@ public Object visit(ExpressionLabel e) throws PrismLangException public void visitPost(ExpressionLabel e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionProp e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionProp e) throws PrismLangException + public Object visitNow(ExpressionProp e) throws PrismLangException { visitPre(e); visitPost(e); @@ -587,7 +593,7 @@ public Object visit(ExpressionProp e) throws PrismLangException public void visitPost(ExpressionProp e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ExpressionFilter e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ExpressionFilter e) throws PrismLangException + public Object visitNow(ExpressionFilter e) throws PrismLangException { visitPre(e); if (e.getFilter() != null) e.setFilter((Expression)(e.getFilter().accept(this))); @@ -598,7 +604,7 @@ public Object visit(ExpressionFilter e) throws PrismLangException public void visitPost(ExpressionFilter e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(ForLoop e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(ForLoop e) throws PrismLangException + public Object visitNow(ForLoop e) throws PrismLangException { visitPre(e); if (e.getFrom() != null) e.setFrom((Expression)(e.getFrom().accept(this))); @@ -610,7 +616,7 @@ public Object visit(ForLoop e) throws PrismLangException public void visitPost(ForLoop e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- public void visitPre(Filter e) throws PrismLangException { defaultVisitPre(e); } - public Object visit(Filter e) throws PrismLangException + public Object visitNow(Filter e) throws PrismLangException { visitPre(e); if (e.getExpression() != null) e.setExpression((Expression)(e.getExpression().accept(this))); @@ -620,4 +626,3 @@ public Object visit(Filter e) throws PrismLangException public void visitPost(Filter e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- } - diff --git a/prism/src/parser/visitor/DAGVisitor.java b/prism/src/parser/visitor/DAGVisitor.java new file mode 100644 index 0000000000..f5e0e286ee --- /dev/null +++ b/prism/src/parser/visitor/DAGVisitor.java @@ -0,0 +1,481 @@ +//============================================================================== +// +// Copyright (c) 2018- +// Authors: +// * Steffen Maercker (TU Dresden) +// +//------------------------------------------------------------------------------ +// +// 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.visitor; + +import java.util.IdentityHashMap; +import java.util.Map; + +import parser.ast.*; +import parser.ast.Module; +import prism.PrismLangException; + +/** + * Performs a depth-first traversal of an abstract syntax tree (AST). + * Each node is visited exactly once, even if the AST is a directed acyclic graph. + *

+ * By default, the implementation uses an identity-based map to identify duplicates. + * However, this can be configured by providing other map types. + * To implement the visiting behavior, subclasses should override {@code visitNow}. + * To visit subsequent nodes, {@code visit} has to be called to ensure that nodes + * are visited only once. + *

+ * @see ASTTraverse + * @see java.util.IdentityHashMap + */ +public abstract class DAGVisitor implements ASTVisitor +{ + protected Map visited; + + /** + * Create and configure a DAG-aware visitor with an IdentityHashMap. + * This is a conservative choice to ensure that nodes are considered + * visited if and only if they are the same object. + * + * @see java.util.IdentityHashMap + */ + protected DAGVisitor() + { + this(new IdentityHashMap<>()); + } + + /** + * Create and configure a DAG-aware visitor. + * If no map is provided, nodes are visited multiple times. + * + * @param visited a map to keep track of duplicates or null + * @see java.util.Map + */ + protected DAGVisitor(Map visited) + { + this.visited = visited; + } + + protected boolean isVisited(T element) + { + return visited != null && visited.containsKey(element); + } + + protected Object getStored(ASTElement element) + { + if (visited != null) { + return visited.get(element); + } + return null; + } + + protected Object store(T element, Object result) + { + if (visited != null) { + visited.put(element, result); + } + return result; + } + + @Override + public Object visit(ModulesFile e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(PropertiesFile e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(Property e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(FormulaList e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(LabelList e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(ConstantList e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(Declaration e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(DeclarationInt e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(DeclarationBool e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(DeclarationArray e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(DeclarationClock e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(DeclarationIntUnbounded e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(Module e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(Command e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(Updates e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(Update e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(RenamedModule e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(RewardStruct e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(RewardStructItem e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(SystemInterleaved e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(SystemFullParallel e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(SystemParallel e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(SystemHide e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(SystemRename e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(SystemModule e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(SystemBrackets e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(SystemReference e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(ExpressionTemporal e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(ExpressionITE e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(ExpressionBinaryOp e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(ExpressionUnaryOp e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(ExpressionFunc e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(ExpressionIdent e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(ExpressionLiteral e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(ExpressionConstant e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(ExpressionFormula e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(ExpressionVar e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(ExpressionProb e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(ExpressionReward e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(ExpressionSS e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(ExpressionExists e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(ExpressionForAll e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(ExpressionStrategy e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(ExpressionLabel e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(ExpressionProp e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(ExpressionFilter e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(Filter e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + @Override + public Object visit(ForLoop e) throws PrismLangException + { + return isVisited(e) ? getStored(e) : store(e, visitNow(e)); + } + + public abstract Object visitNow(ModulesFile e) throws PrismLangException; + + public abstract Object visitNow(PropertiesFile e) throws PrismLangException; + + public abstract Object visitNow(Property e) throws PrismLangException; + + public abstract Object visitNow(FormulaList e) throws PrismLangException; + + public abstract Object visitNow(LabelList e) throws PrismLangException; + + public abstract Object visitNow(ConstantList e) throws PrismLangException; + + public abstract Object visitNow(Declaration e) throws PrismLangException; + + public abstract Object visitNow(DeclarationInt e) throws PrismLangException; + + public abstract Object visitNow(DeclarationBool e) throws PrismLangException; + + public abstract Object visitNow(DeclarationArray e) throws PrismLangException; + + public abstract Object visitNow(DeclarationClock e) throws PrismLangException; + + public abstract Object visitNow(DeclarationIntUnbounded e) throws PrismLangException; + + public abstract Object visitNow(Module e) throws PrismLangException; + + public abstract Object visitNow(Command e) throws PrismLangException; + + public abstract Object visitNow(Updates e) throws PrismLangException; + + public abstract Object visitNow(Update e) throws PrismLangException; + + public abstract Object visitNow(RenamedModule e) throws PrismLangException; + + public abstract Object visitNow(RewardStruct e) throws PrismLangException; + + public abstract Object visitNow(RewardStructItem e) throws PrismLangException; + + public abstract Object visitNow(SystemInterleaved e) throws PrismLangException; + + public abstract Object visitNow(SystemFullParallel e) throws PrismLangException; + + public abstract Object visitNow(SystemParallel e) throws PrismLangException; + + public abstract Object visitNow(SystemHide e) throws PrismLangException; + + public abstract Object visitNow(SystemRename e) throws PrismLangException; + + public abstract Object visitNow(SystemModule e) throws PrismLangException; + + public abstract Object visitNow(SystemBrackets e) throws PrismLangException; + + public abstract Object visitNow(SystemReference e) throws PrismLangException; + + public abstract Object visitNow(ExpressionTemporal e) throws PrismLangException; + + public abstract Object visitNow(ExpressionITE e) throws PrismLangException; + + public abstract Object visitNow(ExpressionBinaryOp e) throws PrismLangException; + + public abstract Object visitNow(ExpressionUnaryOp e) throws PrismLangException; + + public abstract Object visitNow(ExpressionFunc e) throws PrismLangException; + + public abstract Object visitNow(ExpressionIdent e) throws PrismLangException; + + public abstract Object visitNow(ExpressionLiteral e) throws PrismLangException; + + public abstract Object visitNow(ExpressionConstant e) throws PrismLangException; + + public abstract Object visitNow(ExpressionFormula e) throws PrismLangException; + + public abstract Object visitNow(ExpressionVar e) throws PrismLangException; + + public abstract Object visitNow(ExpressionProb e) throws PrismLangException; + + public abstract Object visitNow(ExpressionReward e) throws PrismLangException; + + public abstract Object visitNow(ExpressionSS e) throws PrismLangException; + + public abstract Object visitNow(ExpressionExists e) throws PrismLangException; + + public abstract Object visitNow(ExpressionForAll e) throws PrismLangException; + + public abstract Object visitNow(ExpressionStrategy e) throws PrismLangException; + + public abstract Object visitNow(ExpressionLabel e) throws PrismLangException; + + public abstract Object visitNow(ExpressionProp e) throws PrismLangException; + + public abstract Object visitNow(ExpressionFilter e) throws PrismLangException; + + public abstract Object visitNow(Filter e) throws PrismLangException; + + public abstract Object visitNow(ForLoop e) throws PrismLangException; +} diff --git a/prism/src/parser/visitor/DeepCopy.java b/prism/src/parser/visitor/DeepCopy.java new file mode 100644 index 0000000000..ae08730552 --- /dev/null +++ b/prism/src/parser/visitor/DeepCopy.java @@ -0,0 +1,438 @@ +//============================================================================== +// +// Copyright (c) 2018- +// Authors: +// * Steffen Maercker (TU Dresden) +// * Johannes Kath (TU Dresden) +// +//------------------------------------------------------------------------------ +// +// 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.visitor; + +import java.util.HashMap; +import java.util.List; +import java.util.Vector; + +import parser.ast.*; +import parser.ast.Module; +import prism.PrismLangException; + +/** + * DeepCopy is a visitor that copies an AST with out duplicating nodes. + *

+ * After certain replacements, e.g., formula substitution, + * the AST becomes a directed acyclic graph. + * DeepCopy preserves that structure on copying to prevent + * a (potentially exponential) blowup in the number of nodes. + *

+ *

+ * The implementation uses an equality-based map to identify duplicates. + * For copying it provides the methods {@code copy} and {@copyAll} and relies + * on {@code deepCopy} in ASTElement. + *

+ * @see ASTElement#deepCopy(DeepCopy) + * @see java.util.HashMap + */ +public class DeepCopy extends DAGVisitor +{ + public DeepCopy() + { + super(new HashMap<>()); + } + /** + * Wrapper for {@PrismLangException} to enable usage of {@link List#replaceAll} + * by masking the exception temporarily as RuntimeException; + */ + @SuppressWarnings("serial") + protected class WrappedPrismLangException extends RuntimeException + { + public WrappedPrismLangException(PrismLangException cause) + { + super(cause); + } + + public PrismLangException getCause() + { + return (PrismLangException) super.getCause(); + } + } + + /** + * Copy an ASTElement or null. + * + * @param element the element to be copied or null + * @return copy of the element or null + * @throws PrismLangException + */ + @SuppressWarnings("unchecked") + public T copy(T element) throws PrismLangException + { + return (element == null) ? null :(T) element.accept(this); + } + + /** + * Copy all ASTElements (or null) in the list. + * + * @param list list of elements to be copied + * @return the argument list with all elements copied + * @throws PrismLangException + */ + public List copyAll(List list) throws PrismLangException + { + if (list != null) { + try { + list.replaceAll(d -> copyOrThrow(d)); + } + catch (WrappedPrismLangException e) { + throw e.getCause(); + } + } + return list; + } + + /** + * Copy all ASTElements (or null) in the vector. + * + * @param vect vector of elements to be copied + * @return the argument vector with all elements copied + * @throws PrismLangException + */ + public Vector copyAll(Vector vect) throws PrismLangException + { + if (vect != null) { + try { + vect.replaceAll(d -> copyOrThrow(d)); + } + catch (WrappedPrismLangException e) { + throw e.getCause(); + } + } + return vect; + } + + /** + * Copy an ASTElement and mask PrismLangExpecitons as RuntimeExceptions + * + * @param element the element to be copied + * @return copy of the element + * @throws WrappedPrismLangException if a PrismLangException occurs internally + */ + protected T copyOrThrow(T element) + { + try { + return copy(element); + } catch (PrismLangException e) { + throw new WrappedPrismLangException(e); + } + } + + @Override + public ModulesFile visitNow(ModulesFile e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public PropertiesFile visitNow(PropertiesFile e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public Property visitNow(Property e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public FormulaList visitNow(FormulaList e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public LabelList visitNow(LabelList e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public ConstantList visitNow(ConstantList e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public Declaration visitNow(Declaration e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public DeclarationInt visitNow(DeclarationInt e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public DeclarationBool visitNow(DeclarationBool e) throws PrismLangException + { + return e.clone(); + } + + @Override + public DeclarationArray visitNow(DeclarationArray e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public DeclarationClock visitNow(DeclarationClock e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public DeclarationIntUnbounded visitNow(DeclarationIntUnbounded e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public Module visitNow(Module e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public Command visitNow(Command e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public Updates visitNow(Updates e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public Update visitNow(Update e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public RenamedModule visitNow(RenamedModule e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public RewardStruct visitNow(RewardStruct e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public RewardStructItem visitNow(RewardStructItem e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public SystemInterleaved visitNow(SystemInterleaved e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public SystemFullParallel visitNow(SystemFullParallel e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public SystemParallel visitNow(SystemParallel e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public SystemHide visitNow(SystemHide e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public SystemRename visitNow(SystemRename e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public SystemModule visitNow(SystemModule e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public SystemBrackets visitNow(SystemBrackets e) throws PrismLangException + { + SystemBrackets copy = e.clone(); + + copy.setOperand(copy(copy.getOperand())); + + return copy; + } + + @Override + public SystemReference visitNow(SystemReference e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public ExpressionTemporal visitNow(ExpressionTemporal e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public ExpressionITE visitNow(ExpressionITE e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public ExpressionBinaryOp visitNow(ExpressionBinaryOp e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public ExpressionUnaryOp visitNow(ExpressionUnaryOp e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public ExpressionFunc visitNow(ExpressionFunc e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public ExpressionIdent visitNow(ExpressionIdent e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public ExpressionLiteral visitNow(ExpressionLiteral e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public ExpressionConstant visitNow(ExpressionConstant e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public ExpressionFormula visitNow(ExpressionFormula e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public ExpressionVar visitNow(ExpressionVar e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public ExpressionProb visitNow(ExpressionProb e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public ExpressionReward visitNow(ExpressionReward e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public ExpressionSS visitNow(ExpressionSS e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public ExpressionExists visitNow(ExpressionExists e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public ExpressionForAll visitNow(ExpressionForAll e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public ExpressionStrategy visitNow(ExpressionStrategy e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public ExpressionLabel visitNow(ExpressionLabel e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public ExpressionProp visitNow(ExpressionProp e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public ExpressionFilter visitNow(ExpressionFilter e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public ForLoop visitNow(ForLoop e) throws PrismLangException + { + return e.clone().deepCopy(this); + } + + @Override + public Filter visitNow(Filter e) throws PrismLangException + { + return e.clone().deepCopy(this); + } +} diff --git a/prism/src/parser/visitor/EvaluatePartially.java b/prism/src/parser/visitor/EvaluatePartially.java index 43cb980c22..2f36e26aea 100644 --- a/prism/src/parser/visitor/EvaluatePartially.java +++ b/prism/src/parser/visitor/EvaluatePartially.java @@ -42,7 +42,7 @@ public EvaluatePartially(EvaluateContext ec) this.ec = ec; } - public Object visit(ExpressionConstant e) throws PrismLangException + public Object visitNow(ExpressionConstant e) throws PrismLangException { Object val = ec.getConstantValue(e.getName()); if (val == null) { @@ -52,7 +52,7 @@ public Object visit(ExpressionConstant e) throws PrismLangException } } - public Object visit(ExpressionVar e) throws PrismLangException + public Object visitNow(ExpressionVar e) throws PrismLangException { Object val = ec.getVarValue(e.getName(), e.getIndex()); if (val == null) { diff --git a/prism/src/parser/visitor/ExpandConstants.java b/prism/src/parser/visitor/ExpandConstants.java index 2d999b2fd9..2795cb1f97 100644 --- a/prism/src/parser/visitor/ExpandConstants.java +++ b/prism/src/parser/visitor/ExpandConstants.java @@ -42,7 +42,7 @@ public ExpandConstants(ConstantList constantList) this.constantList = constantList; } - public Object visit(ExpressionConstant e) throws PrismLangException + public Object visitNow(ExpressionConstant e) throws PrismLangException { int i; Type t; diff --git a/prism/src/parser/visitor/ExpandFormulas.java b/prism/src/parser/visitor/ExpandFormulas.java index d7a6caa02c..1980d65ca8 100644 --- a/prism/src/parser/visitor/ExpandFormulas.java +++ b/prism/src/parser/visitor/ExpandFormulas.java @@ -48,7 +48,7 @@ public ExpandFormulas(FormulaList formulaList, boolean replace) this.replace = replace; } - public Object visit(ExpressionFormula e) throws PrismLangException + public Object visitNow(ExpressionFormula e) throws PrismLangException { int i; Type t; diff --git a/prism/src/parser/visitor/ExpandLabels.java b/prism/src/parser/visitor/ExpandLabels.java index 11890e9d08..48977dd4c8 100644 --- a/prism/src/parser/visitor/ExpandLabels.java +++ b/prism/src/parser/visitor/ExpandLabels.java @@ -44,7 +44,7 @@ public ExpandLabels(LabelList labelList) this.labelList = labelList; } - public Object visit(ExpressionLabel e) throws PrismLangException + public Object visitNow(ExpressionLabel e) throws PrismLangException { int i; Type t; diff --git a/prism/src/parser/visitor/ExpandPropRefsAndLabels.java b/prism/src/parser/visitor/ExpandPropRefsAndLabels.java index 9ce3324661..def8e42457 100644 --- a/prism/src/parser/visitor/ExpandPropRefsAndLabels.java +++ b/prism/src/parser/visitor/ExpandPropRefsAndLabels.java @@ -49,7 +49,7 @@ public ExpandPropRefsAndLabels(PropertiesFile propertiesFile, LabelList labelLis this.labelList = labelList; } - public Object visit(ExpressionLabel e) throws PrismLangException + public Object visitNow(ExpressionLabel e) throws PrismLangException { int i; Type t; @@ -84,7 +84,7 @@ public Object visit(ExpressionLabel e) throws PrismLangException return e; } - public Object visit(ExpressionProp e) throws PrismLangException + public Object visitNow(ExpressionProp e) throws PrismLangException { Property prop; Type t; diff --git a/prism/src/parser/visitor/ExpressionTraverseNonNested.java b/prism/src/parser/visitor/ExpressionTraverseNonNested.java index 0fd7f1df22..8922f75ef0 100644 --- a/prism/src/parser/visitor/ExpressionTraverseNonNested.java +++ b/prism/src/parser/visitor/ExpressionTraverseNonNested.java @@ -42,9 +42,9 @@ *
* Subclasses should not override
*
    - *
  • {@code visit(ExpressionProb)}
    • - *
  • {@code visit(ExpressionReward)}
    • - *
  • {@code visit(ExpressionSS)}
    • + *
  • {@code visitNow(ExpressionProb)}
    • + *
  • {@code visitNow(ExpressionReward)}
    • + *
  • {@code visitNow(ExpressionSS)}
    • *
*/ public class ExpressionTraverseNonNested extends ASTTraverse @@ -74,7 +74,7 @@ private boolean inLimit() } @Override - public Object visit(ExpressionProb e) throws PrismLangException + public Object visitNow(ExpressionProb e) throws PrismLangException { currentNesting++; // only visit if we are still in limit @@ -82,13 +82,13 @@ public Object visit(ExpressionProb e) throws PrismLangException currentNesting--; return null; } - Object rv = super.visit(e); + Object rv = super.visitNow(e); currentNesting--; return rv; } @Override - public Object visit(ExpressionReward e) throws PrismLangException + public Object visitNow(ExpressionReward e) throws PrismLangException { currentNesting++; // only visit if we are still in limit @@ -96,13 +96,13 @@ public Object visit(ExpressionReward e) throws PrismLangException currentNesting--; return null; } - Object rv = super.visit(e); + Object rv = super.visitNow(e); currentNesting--; return rv; } @Override - public Object visit(ExpressionSS e) throws PrismLangException + public Object visitNow(ExpressionSS e) throws PrismLangException { currentNesting++; // only visit if we are still in limit @@ -110,7 +110,7 @@ public Object visit(ExpressionSS e) throws PrismLangException currentNesting--; return null; } - Object rv = super.visit(e); + Object rv = super.visitNow(e); currentNesting--; return rv; } diff --git a/prism/src/parser/visitor/FindAllConstants.java b/prism/src/parser/visitor/FindAllConstants.java index 6873c9fe27..1bc03f0925 100644 --- a/prism/src/parser/visitor/FindAllConstants.java +++ b/prism/src/parser/visitor/FindAllConstants.java @@ -41,7 +41,7 @@ public FindAllConstants(ConstantList constantList) this.constantList = constantList; } - public Object visit(ExpressionIdent e) throws PrismLangException + public Object visitNow(ExpressionIdent e) throws PrismLangException { int i; // See if identifier corresponds to a constant diff --git a/prism/src/parser/visitor/FindAllFormulas.java b/prism/src/parser/visitor/FindAllFormulas.java index 394750b31b..07a8df2913 100644 --- a/prism/src/parser/visitor/FindAllFormulas.java +++ b/prism/src/parser/visitor/FindAllFormulas.java @@ -41,7 +41,7 @@ public FindAllFormulas(FormulaList formulaList) this.formulaList = formulaList; } - public Object visit(ExpressionIdent e) throws PrismLangException + public Object visitNow(ExpressionIdent e) throws PrismLangException { int i; // See if identifier corresponds to a formula diff --git a/prism/src/parser/visitor/FindAllPropRefs.java b/prism/src/parser/visitor/FindAllPropRefs.java index 2d62b98f6d..bad61feca9 100644 --- a/prism/src/parser/visitor/FindAllPropRefs.java +++ b/prism/src/parser/visitor/FindAllPropRefs.java @@ -43,7 +43,7 @@ public FindAllPropRefs(ModulesFile mf, PropertiesFile pf) this.pf = pf; } - public Object visit(ExpressionLabel e) throws PrismLangException + public Object visitNow(ExpressionLabel e) throws PrismLangException { String name; Property prop = null; diff --git a/prism/src/parser/visitor/FindAllVars.java b/prism/src/parser/visitor/FindAllVars.java index 5e7c36f13a..cec7f83a77 100644 --- a/prism/src/parser/visitor/FindAllVars.java +++ b/prism/src/parser/visitor/FindAllVars.java @@ -71,7 +71,7 @@ public void visitPost(Update e) throws PrismLangException } } - public Object visit(ExpressionIdent e) throws PrismLangException + public Object visitNow(ExpressionIdent e) throws PrismLangException { int i; // See if identifier corresponds to a variable @@ -89,7 +89,7 @@ public Object visit(ExpressionIdent e) throws PrismLangException } // Also re-compute info for ExpressionVar objects in case variable indices have changed - public Object visit(ExpressionVar e) throws PrismLangException + public Object visitNow(ExpressionVar e) throws PrismLangException { int i; // See if identifier corresponds to a variable diff --git a/prism/src/parser/visitor/ModulesFileSemanticCheck.java b/prism/src/parser/visitor/ModulesFileSemanticCheck.java index 678cea87a4..0d268dcabb 100644 --- a/prism/src/parser/visitor/ModulesFileSemanticCheck.java +++ b/prism/src/parser/visitor/ModulesFileSemanticCheck.java @@ -29,6 +29,7 @@ import java.util.Vector; import parser.ast.*; +import parser.ast.Module; import parser.type.*; import prism.ModelType; import prism.PrismLangException; @@ -92,7 +93,7 @@ public void visitPost(ModulesFile e) throws PrismLangException } } - public Object visit(SystemReference e) throws PrismLangException + public Object visitNow(SystemReference e) throws PrismLangException { // Make sure referenced system exists if (modulesFile.getSystemDefnByName(e.getName()) == null) @@ -100,7 +101,7 @@ public Object visit(SystemReference e) throws PrismLangException return null; } - public Object visit(FormulaList e) throws PrismLangException + public Object visitNow(FormulaList e) throws PrismLangException { // Override - don't need to do any semantic checks on formulas // (they will have been expanded in place, where needed) @@ -180,7 +181,7 @@ public void visitPre(parser.ast.Module e) throws PrismLangException //inModule = e; } - public Object visit(parser.ast.Module e) throws PrismLangException + public Object visitNow(Module e) throws PrismLangException { // Override this so we can keep track of when we are in an invariant visitPre(e); @@ -207,7 +208,7 @@ public void visitPost(parser.ast.Module e) throws PrismLangException //inModule = null; } - public Object visit(Command e) throws PrismLangException + public Object visitNow(Command e) throws PrismLangException { // Override this so we can keep track of when we are in a command visitPre(e); diff --git a/prism/src/parser/visitor/PropertiesSemanticCheck.java b/prism/src/parser/visitor/PropertiesSemanticCheck.java index 2709fced1b..03186ab643 100644 --- a/prism/src/parser/visitor/PropertiesSemanticCheck.java +++ b/prism/src/parser/visitor/PropertiesSemanticCheck.java @@ -78,7 +78,7 @@ public void setModelInfo(ModelInfo modelInfo) } } - public Object visit(FormulaList e) throws PrismLangException + public Object visitNow(FormulaList e) throws PrismLangException { // Override - don't need to do any semantic checks on formulas // (they will have been expanded in place, where needed) diff --git a/prism/src/parser/visitor/ReplaceLabels.java b/prism/src/parser/visitor/ReplaceLabels.java index 5d1d18a0c5..431f001a0b 100644 --- a/prism/src/parser/visitor/ReplaceLabels.java +++ b/prism/src/parser/visitor/ReplaceLabels.java @@ -52,7 +52,7 @@ public ReplaceLabels(String labelFrom, String labelTo) } @Override - public Object visit(ExpressionLabel e) + public Object visitNow(ExpressionLabel e) { if (e.getName() == null) return e; diff --git a/prism/src/parser/visitor/Simplify.java b/prism/src/parser/visitor/Simplify.java index 4e12ac9286..b9b01b3527 100644 --- a/prism/src/parser/visitor/Simplify.java +++ b/prism/src/parser/visitor/Simplify.java @@ -35,7 +35,7 @@ */ public class Simplify extends ASTTraverseModify { - public Object visit(ExpressionBinaryOp e) throws PrismLangException + public Object visitNow(ExpressionBinaryOp e) throws PrismLangException { // Apply recursively e.setOperand1((Expression) (e.getOperand1().accept(this))); @@ -93,13 +93,15 @@ public Object visit(ExpressionBinaryOp e) throws PrismLangException return e.getOperand2(); if (Expression.isDouble(e.getOperand2()) && e.getOperand2().evaluateDouble() == 0.0) { // Need to be careful that type is preserved - e.getOperand1().setType(e.getType()); - return e.getOperand1(); + Expression op = e.getOperand1().clone(); + op.setType(e.getType()); + return op; } if (Expression.isDouble(e.getOperand1()) && e.getOperand1().evaluateDouble() == 0.0) { // Need to be careful that type is preserved - e.getOperand2().setType(e.getType()); - return e.getOperand2(); + Expression op = e.getOperand2().clone(); + op.setType(e.getType()); + return op; } break; case ExpressionBinaryOp.MINUS: @@ -113,8 +115,9 @@ public Object visit(ExpressionBinaryOp e) throws PrismLangException } if (Expression.isDouble(e.getOperand2()) && e.getOperand2().evaluateDouble() == 0.0) { // Need to be careful that type is preserved - e.getOperand1().setType(e.getType()); - return e.getOperand1(); + Expression op = e.getOperand1().clone(); + op.setType(e.getType()); + return op; } if (Expression.isDouble(e.getOperand1()) && e.getOperand1().evaluateDouble() == 0.0) { ExpressionUnaryOp simplified = new ExpressionUnaryOp(ExpressionUnaryOp.MINUS, e.getOperand2()); @@ -130,13 +133,15 @@ public Object visit(ExpressionBinaryOp e) throws PrismLangException return e.getOperand2(); if (Expression.isDouble(e.getOperand2()) && e.getOperand2().evaluateDouble() == 1.0) { // Need to be careful that type is preserved - e.getOperand1().setType(e.getType()); - return e.getOperand1(); + Expression op = e.getOperand1().clone(); + op.setType(e.getType()); + return op; } if (Expression.isDouble(e.getOperand1()) && e.getOperand1().evaluateDouble() == 1.0) { // Need to be careful that type is preserved - e.getOperand2().setType(e.getType()); - return e.getOperand2(); + Expression op = e.getOperand2().clone(); + op.setType(e.getType()); + return op; } if (Expression.isInt(e.getOperand2()) && e.getOperand2().evaluateInt() == 0) { // Need to be careful that type is preserved @@ -159,7 +164,7 @@ public Object visit(ExpressionBinaryOp e) throws PrismLangException return e; } - public Object visit(ExpressionUnaryOp e) throws PrismLangException + public Object visitNow(ExpressionUnaryOp e) throws PrismLangException { // Apply recursively e.setOperand((Expression) (e.getOperand().accept(this))); @@ -174,7 +179,7 @@ public Object visit(ExpressionUnaryOp e) throws PrismLangException return e; } - public Object visit(ExpressionITE e) throws PrismLangException + public Object visitNow(ExpressionITE e) throws PrismLangException { // Apply recursively e.setOperand1((Expression) (e.getOperand1().accept(this))); @@ -194,7 +199,7 @@ public Object visit(ExpressionITE e) throws PrismLangException return e; } - public Object visit(ExpressionFunc e) throws PrismLangException + public Object visitNow(ExpressionFunc e) throws PrismLangException { int i, n; boolean literal; @@ -218,7 +223,7 @@ public Object visit(ExpressionFunc e) throws PrismLangException return e; } - public Object visit(ExpressionFormula e) throws PrismLangException + public Object visitNow(ExpressionFormula e) throws PrismLangException { // If formula has an attached definition, just replace it with that return e.getDefinition() != null ? e.getDefinition() : e; diff --git a/prism/src/parser/visitor/TypeCheck.java b/prism/src/parser/visitor/TypeCheck.java index 65a114ba63..f70b2e2ab4 100644 --- a/prism/src/parser/visitor/TypeCheck.java +++ b/prism/src/parser/visitor/TypeCheck.java @@ -584,7 +584,7 @@ public void visitPost(ExpressionProp e) throws PrismLangException { // Recursively type check referenced property // (may not have been done yet, e.g. because that property appears later than the current one in a PropertiesFile) - // (NB: recursive check not triggered in visit() method because PropertiesFile not available there) + // (NB: recursive check not triggered in visitNow() method because PropertiesFile not available there) // However, if a PropertiesFile is not available *and* we have a type stored already, don't recompute // (in case typeCheck() is called by getType() later without passing a PropertieFile) if (propertiesFile == null) { diff --git a/prism/src/pta/DigitalClocks.java b/prism/src/pta/DigitalClocks.java index 6eff8fe011..16a5150f61 100644 --- a/prism/src/pta/DigitalClocks.java +++ b/prism/src/pta/DigitalClocks.java @@ -30,6 +30,7 @@ import parser.*; import parser.ast.*; +import parser.ast.Module; import parser.type.*; import parser.visitor.*; import prism.*; @@ -127,7 +128,7 @@ public void translate(ModulesFile modulesFile, PropertiesFile propertiesFile, Ex for (RewardStruct rs : modulesFile.getRewardStructs()) { rs.accept(new ASTTraverseModify() { - public Object visit(ExpressionVar e) throws PrismLangException + public Object visitNow(ExpressionVar e) throws PrismLangException { if (e.getType() instanceof TypeClock) { throw new PrismLangException("Reward structures cannot contain references to clocks", e); @@ -164,7 +165,7 @@ public Object visit(ExpressionVar e) throws PrismLangException // Change all clock variable declarations to bounded integers mf = (ModulesFile) mf.accept(new ASTTraverseModify() { - public Object visit(Declaration e) throws PrismLangException + public Object visitNow(Declaration e) throws PrismLangException { if (e.getDeclType() instanceof DeclarationClock) { int cMax = cci.getScaledClockMax(e.getName()); @@ -184,7 +185,7 @@ public Object visit(Declaration e) throws PrismLangException allInVariants = null; mf = (ModulesFile) mf.accept(new ASTTraverseModify() { - public Object visit(parser.ast.Module e) throws PrismLangException + public Object visitNow(Module e) throws PrismLangException { Command timeCommand; Updates ups; @@ -202,7 +203,7 @@ public Object visit(parser.ast.Module e) throws PrismLangException // Replace all clocks x with x+1 in invariant invar = (Expression) invar.accept(new ASTTraverseModify() { - public Object visit(ExpressionVar e) throws PrismLangException + public Object visitNow(ExpressionVar e) throws PrismLangException { if (e.getType() instanceof TypeClock) { return Expression.Plus(e, Expression.Int(1)); @@ -247,7 +248,7 @@ public Object visit(ExpressionVar e) throws PrismLangException asttm = new ASTTraverseModify() { // Resets - public Object visit(Update e) throws PrismLangException + public Object visitNow(Update e) throws PrismLangException { int i, n; ExpressionFunc exprFunc; @@ -269,7 +270,7 @@ public Object visit(Update e) throws PrismLangException } // Variable accesses - public Object visit(ExpressionVar e) throws PrismLangException + public Object visitNow(ExpressionVar e) throws PrismLangException { if (e.getType() instanceof TypeClock) { e.setType(TypeInt.getInstance()); diff --git a/prism/src/pta/PTAModelChecker.java b/prism/src/pta/PTAModelChecker.java index 93b8af5f8c..73e68cb064 100644 --- a/prism/src/pta/PTAModelChecker.java +++ b/prism/src/pta/PTAModelChecker.java @@ -119,7 +119,7 @@ public Result check(Expression expr) throws PrismException // (do this before modifications below for better error reporting) expr.accept(new ASTTraverseModify() { - public Object visit(ExpressionVar e) throws PrismLangException + public Object visitNow(ExpressionVar e) throws PrismLangException { if (e.getType() instanceof TypeClock) { throw new PrismLangException("Properties cannot contain references to clocks (try the digital clocks engine instead)", e);