Do not unfold the AST on deep-copying

prism/src/automata/LTL2RabinLibrary.java

@@ -132,7 +132,7 @@ public static DA<BitSet, AcceptanceRabin> getDRAforLTL(Expression ltl, Values co
 		labels = new ArrayList<String>();
 		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);

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);
 		}
 
 		/**

prism/src/parser/BooleanUtils.java

@@ -118,18 +118,18 @@ 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)) {
 						Expression a = (Expression) (e.getOperand().accept(this));
 						// (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) {

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());
                                         }

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):

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();
 	}
 }
 

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<Expression>)      constants.clone();
+		clone.nameIdents = (Vector<ExpressionIdent>) nameIdents.clone();
+		clone.names      = (Vector<String>)          names.clone();
+		clone.types      = (Vector<Type>)            types.clone();
+
+		return clone;
 	}
 }
 

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();
 	}
 }
 

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();
 	}
 }

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();
 	}
 }