From cfe571140093cc85a832ca10ab23c4d4cdc7796f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Steffen=20M=C3=A4rcker?= <maercker@tcs.inf.tu-dresden.de>
Date: Fri, 9 Mar 2018 12:21:16 +0100
Subject: [PATCH 1/8] [Java 9] Fix clash with Module from Java 9

---
 prism/src/parser/visitor/ASTTraverse.java              | 3 ++-
 prism/src/parser/visitor/ASTTraverseModify.java        | 1 +
 prism/src/parser/visitor/ModulesFileSemanticCheck.java | 1 +
 prism/src/pta/DigitalClocks.java                       | 1 +
 4 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/prism/src/parser/visitor/ASTTraverse.java b/prism/src/parser/visitor/ASTTraverse.java
index d8ee27aaf1..7a162858a1 100644
--- a/prism/src/parser/visitor/ASTTraverse.java
+++ b/prism/src/parser/visitor/ASTTraverse.java
@@ -27,6 +27,7 @@
 package parser.visitor;
 
 import parser.ast.*;
+import parser.ast.Module;
 import prism.PrismLangException;
 
 // Performs a depth-first traversal of an asbtract syntax tree (AST).
@@ -216,7 +217,7 @@ 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
diff --git a/prism/src/parser/visitor/ASTTraverseModify.java b/prism/src/parser/visitor/ASTTraverseModify.java
index 96670422f1..3e098bc3a4 100644
--- a/prism/src/parser/visitor/ASTTraverseModify.java
+++ b/prism/src/parser/visitor/ASTTraverseModify.java
@@ -27,6 +27,7 @@
 package parser.visitor;
 
 import parser.ast.*;
+import parser.ast.Module;
 import prism.PrismLangException;
 
 // Variant of ASTTraverse.
diff --git a/prism/src/parser/visitor/ModulesFileSemanticCheck.java b/prism/src/parser/visitor/ModulesFileSemanticCheck.java
index 678cea87a4..89fa7b370a 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;
diff --git a/prism/src/pta/DigitalClocks.java b/prism/src/pta/DigitalClocks.java
index 6eff8fe011..551dcf6e75 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.*;

From 50a0446c3ded14cac5f43387d298f646fecc388e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Steffen=20M=C3=A4rcker?= <maercker@tcs.inf.tu-dresden.de>
Date: Fri, 9 Mar 2018 12:21:16 +0100
Subject: [PATCH 2/8] Refactor ExpressionQuant hierarchy

---
 prism/src/parser/ast/Expression.java       | 10 +--
 prism/src/parser/ast/ExpressionProb.java   | 54 +++-----------
 prism/src/parser/ast/ExpressionQuant.java  | 66 ++++++++++++++++-
 prism/src/parser/ast/ExpressionReward.java | 83 +++++++---------------
 prism/src/parser/ast/ExpressionSS.java     | 68 +++++-------------
 5 files changed, 120 insertions(+), 161 deletions(-)

diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java
index 6569c66629..fd8b752708 100644
--- a/prism/src/parser/ast/Expression.java
+++ b/prism/src/parser/ast/Expression.java
@@ -790,14 +790,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/ExpressionProb.java b/prism/src/parser/ast/ExpressionProb.java
index 515ce219f6..17f659a151 100644
--- a/prism/src/parser/ast/ExpressionProb.java
+++ b/prism/src/parser/ast/ExpressionProb.java
@@ -26,8 +26,6 @@
 
 package parser.ast;
 
-import param.BigRational;
-import parser.EvaluateContext;
 import parser.Values;
 import parser.visitor.ASTVisitor;
 import prism.OpRelOpBound;
@@ -91,32 +89,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 +105,6 @@ else if (getRelOp() == RelOp.MAX)
 			return "Probability";
 	}
 
-	@Override
-	public boolean returnsSingleValue()
-	{
-		return false;
-	}
-
 	// Methods required for ASTElement:
 
 	@Override
@@ -146,7 +114,7 @@ public Object accept(ASTVisitor v) throws PrismLangException
 	}
 
 	@Override
-	public Expression deepCopy()
+	public ExpressionProb deepCopy()
 	{
 		ExpressionProb expr = new ExpressionProb();
 		expr.setExpression(getExpression() == null ? null : getExpression().deepCopy());
@@ -161,18 +129,16 @@ public Expression deepCopy()
 	// 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/ExpressionQuant.java b/prism/src/parser/ast/ExpressionQuant.java
index 20d2c9042b..14bff7bb9c 100644
--- a/prism/src/parser/ast/ExpressionQuant.java
+++ b/prism/src/parser/ast/ExpressionQuant.java
@@ -26,9 +26,12 @@
 
 package parser.ast;
 
+import param.BigRational;
+import parser.EvaluateContext;
 import parser.Values;
 import prism.OpRelOpBound;
 import prism.PrismException;
+import prism.PrismLangException;
 
 /**
  * Abstract class for representing "quantitative" operators (P,R,S),
@@ -161,8 +164,69 @@ 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");
+	}
+
+	// Methods required for ASTElement:
+
+	@Override
+	public abstract ExpressionQuant deepCopy();
+
 	// 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..73785c4090 100644
--- a/prism/src/parser/ast/ExpressionReward.java
+++ b/prism/src/parser/ast/ExpressionReward.java
@@ -26,8 +26,6 @@
 
 package parser.ast;
 
-import param.BigRational;
-import parser.EvaluateContext;
 import parser.Values;
 import parser.visitor.ASTVisitor;
 import prism.ModelInfo;
@@ -39,13 +37,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);
@@ -74,7 +72,7 @@ public void setReward(Expression r)
 	}
 
 	// Get methods
-	
+
 	public Object getRewardStructIndex()
 	{
 		return rewardStructIndex;
@@ -94,7 +92,7 @@ public Expression getReward()
 	}
 
 	// Other methods
-	
+
 	/**
 	 * Get a string describing the type of R operator, e.g. "R=?" or "R&lt;r".
 	 */
@@ -172,11 +170,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 +184,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,14 +214,8 @@ else if (rewardStructIndexDiv == null)
 		}
 	}
 
-	@Override
-	public boolean returnsSingleValue()
-	{
-		return false;
-	}
-
 	// Methods required for ASTElement:
-	
+
 	@Override
 	public Object accept(ASTVisitor v) throws PrismLangException
 	{
@@ -255,7 +223,7 @@ public Object accept(ASTVisitor v) throws PrismLangException
 	}
 
 	@Override
-	public Expression deepCopy()
+	public ExpressionReward deepCopy()
 	{
 		ExpressionReward expr = new ExpressionReward();
 		expr.setExpression(getExpression() == null ? null : getExpression().deepCopy());
@@ -272,29 +240,28 @@ public Expression deepCopy()
 	}
 
 	// 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..0fdf6812b4 100644
--- a/prism/src/parser/ast/ExpressionSS.java
+++ b/prism/src/parser/ast/ExpressionSS.java
@@ -26,8 +26,6 @@
 
 package parser.ast;
 
-import param.BigRational;
-import parser.EvaluateContext;
 import parser.Values;
 import parser.visitor.ASTVisitor;
 import prism.OpRelOpBound;
@@ -37,11 +35,11 @@
 public class ExpressionSS extends ExpressionQuant
 {
 	// Constructors
-	
+
 	public ExpressionSS()
 	{
 	}
-	
+
 	public ExpressionSS(Expression expression, String relOpString, Expression p)
 	{
 		setExpression(expression);
@@ -50,7 +48,7 @@ public ExpressionSS(Expression expression, String relOpString, Expression p)
 	}
 
 	// Set methods
-	
+
 	/**
 	 * Set the probability bound. Equivalent to {@code setBound(p)}.
 	 */
@@ -60,7 +58,7 @@ public void setProb(Expression p)
 	}
 
 	// Get methods
-	
+
 	/**
 	 * Get the probability bound. Equivalent to {@code getBound()}.
 	 */
@@ -74,6 +72,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,32 +84,8 @@ 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
-	{
-		throw new PrismLangException("Cannot evaluate an S operator without a model");
-	}
 
-	@Override
-	public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException
-	{
-		throw new PrismLangException("Cannot evaluate an S operator without a model");
-	}
+	// Methods required for Expression:
 
 	@Override
 	public String getResultName()
@@ -118,14 +93,8 @@ public String getResultName()
 		return (getBound() == null) ? "Probability" : "Result";
 	}
 
-	@Override
-	public boolean returnsSingleValue()
-	{
-		return false;
-	}
-
 	// Methods required for ASTElement:
-	
+
 	@Override
 	public Object accept(ASTVisitor v) throws PrismLangException
 	{
@@ -133,7 +102,7 @@ public Object accept(ASTVisitor v) throws PrismLangException
 	}
 
 	@Override
-	public Expression deepCopy()
+	public ExpressionSS deepCopy()
 	{
 		ExpressionSS expr = new ExpressionSS();
 		expr.setExpression(getExpression() == null ? null : getExpression().deepCopy());
@@ -146,19 +115,18 @@ public Expression deepCopy()
 	}
 
 	// Standard methods
-	
+
+	@Override
+	protected String operatorToString()
+	{
+		return "S" + getModifierString();
+	}
+
 	@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;
 	}
 }
 

From 72416e1f2ad8195b730775f6efeb4375c6d38fe3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Steffen=20M=C3=A4rcker?= <maercker@tcs.inf.tu-dresden.de>
Date: Fri, 9 Mar 2018 12:21:16 +0100
Subject: [PATCH 3/8] Improve comments in ASTTraverse and ASTTraverseModify

---
 prism/src/parser/visitor/ASTTraverse.java     | 16 ++++++++++------
 .../src/parser/visitor/ASTTraverseModify.java | 19 ++++++++++++-------
 2 files changed, 22 insertions(+), 13 deletions(-)

diff --git a/prism/src/parser/visitor/ASTTraverse.java b/prism/src/parser/visitor/ASTTraverse.java
index 7a162858a1..412d50085e 100644
--- a/prism/src/parser/visitor/ASTTraverse.java
+++ b/prism/src/parser/visitor/ASTTraverse.java
@@ -30,12 +30,16 @@
 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.
-
+/**
+ *  Performs a depth-first traversal of an abstract syntax tree (AST).
+ *
+ * Many traversal-based tasks can be implemented by extending and either:
+ * <ul>
+ * <li>overriding defaultVisitPre or defaultVisitPost</li>
+ * <li>overriding visit for leaf (or other selected) nodes</li>
+ * </ul>
+ * @see ASTTraverseModify
+ */
 public class ASTTraverse implements ASTVisitor
 {
 	public void defaultVisitPre(ASTElement e) throws PrismLangException {}
diff --git a/prism/src/parser/visitor/ASTTraverseModify.java b/prism/src/parser/visitor/ASTTraverseModify.java
index 3e098bc3a4..81aed92414 100644
--- a/prism/src/parser/visitor/ASTTraverseModify.java
+++ b/prism/src/parser/visitor/ASTTraverseModify.java
@@ -30,13 +30,18 @@
 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
-
+/**
+ *  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:
+ * <ul>
+ * <li>overriding defaultVisitPre or defaultVisitPost</li>
+ * <li>overriding visit for leaf (or other selected) nodes</li>
+ * </ul>
+ * @see ASTTraverse
+ */
 public class ASTTraverseModify implements ASTVisitor
 {
 	public void defaultVisitPre(ASTElement e) throws PrismLangException {}

From 98228f0b1e3a87ed423acf69ef0152a17e06d7ab Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Steffen=20M=C3=A4rcker?= <maercker@tcs.inf.tu-dresden.de>
Date: Fri, 9 Mar 2018 17:57:24 +0100
Subject: [PATCH 4/8] [DAG-visit] Implement DAG-aware visitor

After certain replacements, e.g., formula substitution, the AST becomes a directed acyclic graph.
Most often it is not required to visit a node of this DAG multiply times.
The new class DAGVisitor keeps track of the nodes already seen and visits each node only once.

The class DAGVisitor is inserted between ASTVisitor and ASTTraverse and ASTTraverseModify
without changing the behavior of their subclasses.
---
 prism/src/parser/visitor/ASTTraverse.java     | 100 ++--
 .../src/parser/visitor/ASTTraverseModify.java | 101 ++--
 prism/src/parser/visitor/DAGVisitor.java      | 481 ++++++++++++++++++
 3 files changed, 581 insertions(+), 101 deletions(-)
 create mode 100644 prism/src/parser/visitor/DAGVisitor.java

diff --git a/prism/src/parser/visitor/ASTTraverse.java b/prism/src/parser/visitor/ASTTraverse.java
index 412d50085e..992146f24c 100644
--- a/prism/src/parser/visitor/ASTTraverse.java
+++ b/prism/src/parser/visitor/ASTTraverse.java
@@ -40,13 +40,13 @@
  * </ul>
  * @see ASTTraverseModify
  */
-public class ASTTraverse implements ASTVisitor
+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;
@@ -73,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;
@@ -89,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);
@@ -99,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;
@@ -113,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;
@@ -127,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;
@@ -141,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);
@@ -152,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);
@@ -163,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);
@@ -172,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);
@@ -184,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);
@@ -193,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);
@@ -201,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
@@ -224,7 +224,7 @@ public Object visit(parser.ast.Module e) throws PrismLangException
 	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
@@ -237,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;
@@ -252,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;
@@ -266,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);
@@ -275,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;
@@ -289,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);
@@ -300,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();
@@ -313,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();
@@ -326,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);
@@ -337,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);
@@ -347,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);
@@ -357,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);
@@ -366,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);
@@ -376,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);
@@ -385,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);
@@ -398,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);
@@ -410,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);
@@ -421,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);
@@ -431,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();
@@ -444,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);
@@ -453,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);
@@ -462,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);
@@ -471,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);
@@ -481,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);
@@ -490,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);
@@ -502,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);
@@ -516,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);
@@ -528,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);
@@ -538,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);
@@ -548,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();
@@ -561,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);
@@ -570,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);
@@ -579,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);
@@ -590,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);
@@ -600,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 81aed92414..68dc9dddc5 100644
--- a/prism/src/parser/visitor/ASTTraverseModify.java
+++ b/prism/src/parser/visitor/ASTTraverseModify.java
@@ -42,13 +42,13 @@
  * </ul>
  * @see ASTTraverse
  */
-public class ASTTraverseModify implements ASTVisitor
+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;
@@ -78,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;
@@ -99,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)
@@ -115,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;
@@ -129,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;
@@ -143,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;
@@ -157,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));
@@ -168,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));
@@ -179,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);
@@ -188,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));
@@ -200,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);
@@ -209,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);
@@ -217,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;
@@ -238,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)));
@@ -249,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;
@@ -264,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;
@@ -278,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);
@@ -287,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;
@@ -301,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)));
@@ -312,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();
@@ -325,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();
@@ -338,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)));
@@ -349,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)));
@@ -359,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)));
@@ -369,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);
@@ -378,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)));
@@ -388,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);
@@ -397,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)));
@@ -410,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)));
@@ -422,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)));
@@ -433,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)));
@@ -443,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();
@@ -456,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);
@@ -465,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);
@@ -474,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);
@@ -483,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)));
@@ -493,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);
@@ -502,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)));
@@ -514,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)
@@ -530,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)));
@@ -542,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)));
@@ -552,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)));
@@ -562,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();
@@ -575,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);
@@ -584,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);
@@ -593,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)));
@@ -604,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)));
@@ -616,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)));
@@ -626,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 <maercker@tcs.inf.tu-dresden.de> (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.
+ * <p>
+ * 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.
+ * </p>
+ * @see ASTTraverse
+ * @see java.util.IdentityHashMap
+ */
+public abstract class DAGVisitor implements ASTVisitor
+{
+	protected Map<ASTElement, Object> 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<ASTElement, Object> visited)
+	{
+		this.visited = visited;
+	}
+
+	protected <T extends ASTElement> 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 <T extends ASTElement> 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;
+}

From 48a14d196c6cf4f9908977d7de4956a27b8f5b91 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Steffen=20M=C3=A4rcker?= <maercker@tcs.inf.tu-dresden.de>
Date: Fri, 9 Mar 2018 18:03:23 +0100
Subject: [PATCH 5/8] [DAG-visit] Adapt existing visitors to be DAG-aware

Rename the method visit to visitNow in existing visitor classes.
This makes them traverse the AST without visiting nodes multiple times.
---
 prism/src/automata/LTL2RabinLibrary.java      |  4 +-
 prism/src/explicit/StateModelChecker.java     | 46 +++++++++----------
 prism/src/parser/BooleanUtils.java            |  8 ++--
 prism/src/parser/PrismParser.java             |  4 +-
 .../src/parser/visitor/EvaluatePartially.java |  4 +-
 prism/src/parser/visitor/ExpandConstants.java |  2 +-
 prism/src/parser/visitor/ExpandFormulas.java  |  2 +-
 prism/src/parser/visitor/ExpandLabels.java    |  2 +-
 .../visitor/ExpandPropRefsAndLabels.java      |  4 +-
 .../visitor/ExpressionTraverseNonNested.java  | 18 ++++----
 .../src/parser/visitor/FindAllConstants.java  |  2 +-
 prism/src/parser/visitor/FindAllFormulas.java |  2 +-
 prism/src/parser/visitor/FindAllPropRefs.java |  2 +-
 prism/src/parser/visitor/FindAllVars.java     |  4 +-
 .../visitor/ModulesFileSemanticCheck.java     |  8 ++--
 .../visitor/PropertiesSemanticCheck.java      |  2 +-
 prism/src/parser/visitor/ReplaceLabels.java   |  2 +-
 prism/src/parser/visitor/Simplify.java        | 10 ++--
 prism/src/parser/visitor/TypeCheck.java       |  2 +-
 prism/src/pta/DigitalClocks.java              | 12 ++---
 prism/src/pta/PTAModelChecker.java            |  2 +-
 21 files changed, 71 insertions(+), 71 deletions(-)

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<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);
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/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 @@
  * <br/>
  * Subclasses should not override<br/>
  * <ul>
- *  <li>{@code visit(ExpressionProb)}</li>
- *  <li>{@code visit(ExpressionReward)}</li>
- *  <li>{@code visit(ExpressionSS)}</li>
+ *  <li>{@code visitNow(ExpressionProb)}</li>
+ *  <li>{@code visitNow(ExpressionReward)}</li>
+ *  <li>{@code visitNow(ExpressionSS)}</li>
  * </ul>
  */
 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 89fa7b370a..0d268dcabb 100644
--- a/prism/src/parser/visitor/ModulesFileSemanticCheck.java
+++ b/prism/src/parser/visitor/ModulesFileSemanticCheck.java
@@ -93,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)
@@ -101,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)
@@ -181,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);
@@ -208,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..99064ebb9c 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)));
@@ -159,7 +159,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 +174,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 +194,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 +218,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 551dcf6e75..16a5150f61 100644
--- a/prism/src/pta/DigitalClocks.java
+++ b/prism/src/pta/DigitalClocks.java
@@ -128,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);
@@ -165,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());
@@ -185,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;
@@ -203,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));
@@ -248,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;
@@ -270,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);

From 7be5c42ad9c04a3393fc5fe83488ad448fbd04a8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Steffen=20M=C3=A4rcker?= <maercker@tcs.inf.tu-dresden.de>
Date: Mon, 12 Mar 2018 17:56:21 +0100
Subject: [PATCH 6/8] [DAG-copy] Make ASTElements cloneable

Implement Object#clone to support shallow copies of ASTElements.
Overrides should take care to also clone inner container types, such as lists and vectors.
---
 prism/src/parser/ast/ASTElement.java          | 16 ++++++++-
 prism/src/parser/ast/Command.java             |  6 ++++
 prism/src/parser/ast/ConstantList.java        | 16 ++++++++-
 prism/src/parser/ast/Declaration.java         |  6 ++++
 prism/src/parser/ast/DeclarationArray.java    |  6 ++++
 prism/src/parser/ast/DeclarationBool.java     |  6 ++++
 prism/src/parser/ast/DeclarationClock.java    |  6 ++++
 prism/src/parser/ast/DeclarationInt.java      |  6 ++++
 .../parser/ast/DeclarationIntUnbounded.java   |  6 ++++
 prism/src/parser/ast/Expression.java          |  2 +-
 prism/src/parser/ast/ExpressionBinaryOp.java  |  6 ++++
 prism/src/parser/ast/ExpressionConstant.java  |  6 ++++
 prism/src/parser/ast/ExpressionExists.java    |  6 ++++
 prism/src/parser/ast/ExpressionFilter.java    |  6 ++++
 prism/src/parser/ast/ExpressionForAll.java    |  6 ++++
 prism/src/parser/ast/ExpressionFormula.java   |  6 ++++
 prism/src/parser/ast/ExpressionFunc.java      | 15 ++++++--
 prism/src/parser/ast/ExpressionITE.java       |  6 ++++
 prism/src/parser/ast/ExpressionIdent.java     |  6 ++++
 prism/src/parser/ast/ExpressionLabel.java     |  6 ++++
 prism/src/parser/ast/ExpressionLiteral.java   |  6 ++++
 prism/src/parser/ast/ExpressionProb.java      |  6 ++++
 prism/src/parser/ast/ExpressionProp.java      |  8 ++++-
 prism/src/parser/ast/ExpressionQuant.java     |  5 ---
 prism/src/parser/ast/ExpressionReward.java    |  8 ++++-
 prism/src/parser/ast/ExpressionSS.java        |  6 ++++
 prism/src/parser/ast/ExpressionStrategy.java  | 14 +++++++-
 prism/src/parser/ast/ExpressionTemporal.java  |  6 ++++
 prism/src/parser/ast/ExpressionUnaryOp.java   |  6 ++++
 prism/src/parser/ast/ExpressionVar.java       |  6 ++++
 prism/src/parser/ast/Filter.java              |  6 ++++
 prism/src/parser/ast/ForLoop.java             |  6 ++++
 prism/src/parser/ast/FormulaList.java         | 15 +++++++-
 prism/src/parser/ast/LabelList.java           | 17 +++++++--
 prism/src/parser/ast/Module.java              | 16 +++++++++
 prism/src/parser/ast/ModulesFile.java         | 35 ++++++++++++++++++-
 prism/src/parser/ast/PropertiesFile.java      | 20 ++++++++++-
 prism/src/parser/ast/Property.java            |  6 ++++
 prism/src/parser/ast/RenamedModule.java       | 14 ++++++++
 prism/src/parser/ast/RewardStruct.java        | 11 ++++++
 prism/src/parser/ast/RewardStructItem.java    |  6 ++++
 prism/src/parser/ast/SystemBrackets.java      |  6 ++++
 prism/src/parser/ast/SystemFullParallel.java  | 11 ++++++
 prism/src/parser/ast/SystemHide.java          | 11 ++++++
 prism/src/parser/ast/SystemInterleaved.java   | 11 ++++++
 prism/src/parser/ast/SystemModule.java        |  6 ++++
 prism/src/parser/ast/SystemParallel.java      | 11 ++++++
 prism/src/parser/ast/SystemReference.java     |  6 ++++
 prism/src/parser/ast/SystemRename.java        | 12 +++++++
 prism/src/parser/ast/Update.java              | 16 ++++++++-
 prism/src/parser/ast/Updates.java             | 13 +++++++
 51 files changed, 452 insertions(+), 19 deletions(-)

diff --git a/prism/src/parser/ast/ASTElement.java b/prism/src/parser/ast/ASTElement.java
index 8326057509..6e28bbbb1b 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;
@@ -188,6 +188,20 @@ public String getEndString()
 	 */
 	public abstract ASTElement deepCopy();
 
+	/**
+	 * 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..02c9a8bd20 100644
--- a/prism/src/parser/ast/Command.java
+++ b/prism/src/parser/ast/Command.java
@@ -151,6 +151,12 @@ public ASTElement deepCopy()
 		ret.setPosition(this);
 		return ret;
 	}
+
+	@Override
+	public Command clone()
+	{
+		return (Command) super.clone();
+	}
 }
 
 //------------------------------------------------------------------------------
diff --git a/prism/src/parser/ast/ConstantList.java b/prism/src/parser/ast/ConstantList.java
index c10f9a04fa..74d69db63c 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);
@@ -445,6 +445,20 @@ public ASTElement deepCopy()
 		ret.setPosition(this);
 		return ret;
 	}
+
+@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;
+	}
 }
 
 //------------------------------------------------------------------------------
diff --git a/prism/src/parser/ast/Declaration.java b/prism/src/parser/ast/Declaration.java
index 7cb5a29ce9..d3b7761ba4 100644
--- a/prism/src/parser/ast/Declaration.java
+++ b/prism/src/parser/ast/Declaration.java
@@ -150,6 +150,12 @@ public ASTElement deepCopy()
 		ret.setPosition(this);
 		return ret;
 	}
+
+	@Override
+	public Declaration clone()
+	{
+		return (Declaration) super.clone();
+	}
 }
 
 // ------------------------------------------------------------------------------
diff --git a/prism/src/parser/ast/DeclarationArray.java b/prism/src/parser/ast/DeclarationArray.java
index d79ec97635..584263d53b 100644
--- a/prism/src/parser/ast/DeclarationArray.java
+++ b/prism/src/parser/ast/DeclarationArray.java
@@ -134,4 +134,10 @@ public ASTElement deepCopy()
 		ret.setPosition(this);
 		return ret;
 	}
+
+	@Override
+	public DeclarationArray clone()
+	{
+		return (DeclarationArray) super.clone();
+	}
 }
diff --git a/prism/src/parser/ast/DeclarationBool.java b/prism/src/parser/ast/DeclarationBool.java
index 03f0bbeaef..451190b0c7 100644
--- a/prism/src/parser/ast/DeclarationBool.java
+++ b/prism/src/parser/ast/DeclarationBool.java
@@ -84,4 +84,10 @@ public ASTElement deepCopy()
 		ret.setPosition(this);
 		return ret;
 	}
+
+	@Override
+	public DeclarationBool clone()
+	{
+		return (DeclarationBool) super.clone();
+	}
 }
diff --git a/prism/src/parser/ast/DeclarationClock.java b/prism/src/parser/ast/DeclarationClock.java
index bbfa9d012e..9ea03639c8 100644
--- a/prism/src/parser/ast/DeclarationClock.java
+++ b/prism/src/parser/ast/DeclarationClock.java
@@ -88,4 +88,10 @@ public ASTElement deepCopy()
 		ret.setPosition(this);
 		return ret;
 	}
+
+	@Override
+	public DeclarationClock clone()
+	{
+		return (DeclarationClock) super.clone();
+	}
 }
diff --git a/prism/src/parser/ast/DeclarationInt.java b/prism/src/parser/ast/DeclarationInt.java
index 00163bd643..6529a4583b 100644
--- a/prism/src/parser/ast/DeclarationInt.java
+++ b/prism/src/parser/ast/DeclarationInt.java
@@ -118,4 +118,10 @@ public ASTElement deepCopy()
 		ret.setPosition(this);
 		return ret;
 	}
+
+	@Override
+	public DeclarationInt clone()
+	{
+		return (DeclarationInt) super.clone();
+	}
 }
diff --git a/prism/src/parser/ast/DeclarationIntUnbounded.java b/prism/src/parser/ast/DeclarationIntUnbounded.java
index 0da204f0a4..24aae8cdff 100644
--- a/prism/src/parser/ast/DeclarationIntUnbounded.java
+++ b/prism/src/parser/ast/DeclarationIntUnbounded.java
@@ -88,4 +88,10 @@ public ASTElement deepCopy()
 		ret.setPosition(this);
 		return ret;
 	}
+
+	@Override
+	public DeclarationIntUnbounded clone()
+	{
+		return (DeclarationIntUnbounded) super.clone();
+	}
 }
diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java
index fd8b752708..d71125bcfd 100644
--- a/prism/src/parser/ast/Expression.java
+++ b/prism/src/parser/ast/Expression.java
@@ -76,7 +76,7 @@ public String getResultName()
 	 */
 	public abstract boolean returnsSingleValue();
 	
-	// Overrided version of deepCopy() from superclass ASTElement (to reduce casting).
+	// Override version of deepCopy() from superclass ASTElement (to reduce casting).
 
 	/**
 	 * Perform a deep copy.
diff --git a/prism/src/parser/ast/ExpressionBinaryOp.java b/prism/src/parser/ast/ExpressionBinaryOp.java
index 9e78cf6290..4e2de8c36a 100644
--- a/prism/src/parser/ast/ExpressionBinaryOp.java
+++ b/prism/src/parser/ast/ExpressionBinaryOp.java
@@ -277,6 +277,12 @@ public Expression deepCopy()
 		return expr;
 	}
 
+	@Override
+	public ExpressionBinaryOp clone()
+	{
+		return (ExpressionBinaryOp) super.clone();
+	}
+
 	// Standard methods
 	
 	@Override
diff --git a/prism/src/parser/ast/ExpressionConstant.java b/prism/src/parser/ast/ExpressionConstant.java
index db8d0be871..64cc303a8b 100644
--- a/prism/src/parser/ast/ExpressionConstant.java
+++ b/prism/src/parser/ast/ExpressionConstant.java
@@ -116,6 +116,12 @@ public Expression deepCopy()
 		ret.setPosition(this);
 		return ret;
 	}
+
+	@Override
+	public ExpressionConstant clone()
+	{
+		return (ExpressionConstant) super.clone();
+	}
 	
 	// Standard methods
 	
diff --git a/prism/src/parser/ast/ExpressionExists.java b/prism/src/parser/ast/ExpressionExists.java
index 8a1dfbbe7c..b3d3780190 100644
--- a/prism/src/parser/ast/ExpressionExists.java
+++ b/prism/src/parser/ast/ExpressionExists.java
@@ -109,6 +109,12 @@ public Expression deepCopy()
 		return expr;
 	}
 
+	@Override
+	public ExpressionExists clone()
+	{
+		return (ExpressionExists) super.clone();
+	}
+
 	// Standard methods
 	
 	@Override
diff --git a/prism/src/parser/ast/ExpressionFilter.java b/prism/src/parser/ast/ExpressionFilter.java
index 32ccb3b2fb..e026e7305f 100644
--- a/prism/src/parser/ast/ExpressionFilter.java
+++ b/prism/src/parser/ast/ExpressionFilter.java
@@ -265,6 +265,12 @@ public Expression deepCopy()
 
 		return e;
 	}
+
+	@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..815b31e4d9 100644
--- a/prism/src/parser/ast/ExpressionForAll.java
+++ b/prism/src/parser/ast/ExpressionForAll.java
@@ -109,6 +109,12 @@ public Expression deepCopy()
 		return expr;
 	}
 
+	@Override
+	public ExpressionForAll clone()
+	{
+		return (ExpressionForAll) super.clone();
+	}
+
 	// Standard methods
 	
 	@Override
diff --git a/prism/src/parser/ast/ExpressionFormula.java b/prism/src/parser/ast/ExpressionFormula.java
index 3f3bb26d00..9c5529fda5 100644
--- a/prism/src/parser/ast/ExpressionFormula.java
+++ b/prism/src/parser/ast/ExpressionFormula.java
@@ -132,6 +132,12 @@ public Expression deepCopy()
 		return ret;
 	}
 
+	@Override
+	public ExpressionFormula clone()
+	{
+		return (ExpressionFormula) super.clone();
+	}
+
 	// Standard methods
 	
 	@Override
diff --git a/prism/src/parser/ast/ExpressionFunc.java b/prism/src/parser/ast/ExpressionFunc.java
index c399be0a52..4f89d83786 100644
--- a/prism/src/parser/ast/ExpressionFunc.java
+++ b/prism/src/parser/ast/ExpressionFunc.java
@@ -468,9 +468,20 @@ public Expression deepCopy()
 
 		return e;
 	}
-	
+
+	@SuppressWarnings("unchecked")
+	@Override
+	public ExpressionFunc clone()
+	{
+		ExpressionFunc clone = (ExpressionFunc) super.clone();
+
+		clone.operands = (ArrayList<Expression>) 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..c16344bfbb 100644
--- a/prism/src/parser/ast/ExpressionITE.java
+++ b/prism/src/parser/ast/ExpressionITE.java
@@ -130,6 +130,12 @@ public Expression deepCopy()
 		return expr;
 	}
 
+	@Override
+	public ExpressionITE clone()
+	{
+		return (ExpressionITE) super.clone();
+	}
+
 	// Standard methods
 	
 	@Override
diff --git a/prism/src/parser/ast/ExpressionIdent.java b/prism/src/parser/ast/ExpressionIdent.java
index 0385c38aca..f4606bd832 100644
--- a/prism/src/parser/ast/ExpressionIdent.java
+++ b/prism/src/parser/ast/ExpressionIdent.java
@@ -116,6 +116,12 @@ public Expression deepCopy()
 		return expr;
 	}
 
+	@Override
+	public ExpressionIdent clone()
+	{
+		return (ExpressionIdent) super.clone();
+	}
+
 	// Standard methods
 	
 	@Override
diff --git a/prism/src/parser/ast/ExpressionLabel.java b/prism/src/parser/ast/ExpressionLabel.java
index f1b0323b39..b03bcb7105 100644
--- a/prism/src/parser/ast/ExpressionLabel.java
+++ b/prism/src/parser/ast/ExpressionLabel.java
@@ -115,6 +115,12 @@ public Expression deepCopy()
 		return expr;
 	}
 
+	@Override
+	public ExpressionLabel clone()
+	{
+		return (ExpressionLabel) super.clone();
+	}
+
 	// Standard methods
 
 	@Override
diff --git a/prism/src/parser/ast/ExpressionLiteral.java b/prism/src/parser/ast/ExpressionLiteral.java
index 71338bf7ee..749a018e8d 100644
--- a/prism/src/parser/ast/ExpressionLiteral.java
+++ b/prism/src/parser/ast/ExpressionLiteral.java
@@ -123,6 +123,12 @@ public Expression deepCopy()
 		return expr;
 	}
 
+	@Override
+	public ExpressionLiteral clone()
+	{
+		return (ExpressionLiteral) super.clone();
+	}
+
 	// Standard methods
 	
 	@Override
diff --git a/prism/src/parser/ast/ExpressionProb.java b/prism/src/parser/ast/ExpressionProb.java
index 17f659a151..adc433c144 100644
--- a/prism/src/parser/ast/ExpressionProb.java
+++ b/prism/src/parser/ast/ExpressionProb.java
@@ -126,6 +126,12 @@ public ExpressionProb deepCopy()
 		return expr;
 	}
 
+	@Override
+	public ExpressionProb clone()
+	{
+		return (ExpressionProb) super.clone();
+	}
+
 	// Standard methods
 
 	@Override
diff --git a/prism/src/parser/ast/ExpressionProp.java b/prism/src/parser/ast/ExpressionProp.java
index 16f1ced98a..1dea56cc45 100644
--- a/prism/src/parser/ast/ExpressionProp.java
+++ b/prism/src/parser/ast/ExpressionProp.java
@@ -103,8 +103,14 @@ public Expression deepCopy()
 		return expr;
 	}
 
+	@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 14bff7bb9c..efbd021bef 100644
--- a/prism/src/parser/ast/ExpressionQuant.java
+++ b/prism/src/parser/ast/ExpressionQuant.java
@@ -203,11 +203,6 @@ public BigRational evaluateExact(EvaluateContext ec) throws PrismLangException
 		throw new PrismLangException("Cannot evaluate a quantiative expression without a model");
 	}
 
-	// Methods required for ASTElement:
-
-	@Override
-	public abstract ExpressionQuant deepCopy();
-
 	// Standard methods
 
 	@Override
diff --git a/prism/src/parser/ast/ExpressionReward.java b/prism/src/parser/ast/ExpressionReward.java
index 73785c4090..20a90404c3 100644
--- a/prism/src/parser/ast/ExpressionReward.java
+++ b/prism/src/parser/ast/ExpressionReward.java
@@ -52,7 +52,7 @@ public ExpressionReward(Expression expression, String relOpString, Expression r)
 	}
 
 	// Set methods
-	
+
 	public void setRewardStructIndex(Object o)
 	{
 		rewardStructIndex = o;
@@ -239,6 +239,12 @@ public ExpressionReward deepCopy()
 		return expr;
 	}
 
+	@Override
+	public ExpressionReward clone()
+	{
+		return (ExpressionReward) super.clone();
+	}
+
 	// Standard methods
 
 	@Override
diff --git a/prism/src/parser/ast/ExpressionSS.java b/prism/src/parser/ast/ExpressionSS.java
index 0fdf6812b4..2fc195bce4 100644
--- a/prism/src/parser/ast/ExpressionSS.java
+++ b/prism/src/parser/ast/ExpressionSS.java
@@ -114,6 +114,12 @@ public ExpressionSS deepCopy()
 		return expr;
 	}
 
+	@Override
+	public ExpressionSS clone()
+	{
+		return (ExpressionSS) super.clone();
+	}
+
 	// Standard methods
 
 	@Override
diff --git a/prism/src/parser/ast/ExpressionStrategy.java b/prism/src/parser/ast/ExpressionStrategy.java
index 7062aea9ef..a1bbe91f9e 100644
--- a/prism/src/parser/ast/ExpressionStrategy.java
+++ b/prism/src/parser/ast/ExpressionStrategy.java
@@ -47,7 +47,7 @@ public class ExpressionStrategy extends Expression
 	protected Coalition coalition = new Coalition(); 
 	
 	/** Child expression(s) */
-	protected List<Expression> operands = new ArrayList<Expression>();
+	protected ArrayList<Expression> operands = new ArrayList<Expression>();
 	
 	/** Is there just a single operand (P/R operator)? If not, the operand list will be parenthesised. **/
 	protected boolean singleOperand = false;
@@ -215,6 +215,18 @@ public Expression deepCopy()
 		return expr;
 	}
 
+	@SuppressWarnings("unchecked")
+	@Override
+	public ExpressionStrategy clone()
+	{
+		ExpressionStrategy clone = (ExpressionStrategy) super.clone();
+
+		clone.coalition = new Coalition(coalition);
+		clone.operands  = (ArrayList<Expression>) operands.clone();
+
+		return clone;
+	}
+
 	// Standard methods
 
 	@Override
diff --git a/prism/src/parser/ast/ExpressionTemporal.java b/prism/src/parser/ast/ExpressionTemporal.java
index 528a34d27f..dd27d7340a 100644
--- a/prism/src/parser/ast/ExpressionTemporal.java
+++ b/prism/src/parser/ast/ExpressionTemporal.java
@@ -279,6 +279,12 @@ public Expression deepCopy()
 		return expr;
 	}
 
+	@Override
+	public ExpressionTemporal clone()
+	{
+		return (ExpressionTemporal) super.clone();
+	}
+
 	// Standard methods
 
 	@Override
diff --git a/prism/src/parser/ast/ExpressionUnaryOp.java b/prism/src/parser/ast/ExpressionUnaryOp.java
index 0c48975ff8..bb43414fcd 100644
--- a/prism/src/parser/ast/ExpressionUnaryOp.java
+++ b/prism/src/parser/ast/ExpressionUnaryOp.java
@@ -170,6 +170,12 @@ public Expression deepCopy()
 		return expr;
 	}
 
+	@Override
+	public ExpressionUnaryOp clone()
+	{
+		return (ExpressionUnaryOp) super.clone();
+	}
+
 	// Standard methods
 
 	@Override
diff --git a/prism/src/parser/ast/ExpressionVar.java b/prism/src/parser/ast/ExpressionVar.java
index 4e9e98c5fb..a4b67446c8 100644
--- a/prism/src/parser/ast/ExpressionVar.java
+++ b/prism/src/parser/ast/ExpressionVar.java
@@ -127,6 +127,12 @@ public Expression deepCopy()
 		return expr;
 	}
 
+	@Override
+	public ExpressionVar clone()
+	{
+		return (ExpressionVar) super.clone();
+	}
+
 	// Standard methods
 	
 	@Override
diff --git a/prism/src/parser/ast/Filter.java b/prism/src/parser/ast/Filter.java
index b0353ce58b..4494ebc108 100644
--- a/prism/src/parser/ast/Filter.java
+++ b/prism/src/parser/ast/Filter.java
@@ -127,6 +127,12 @@ public ASTElement deepCopy()
 		ret.setPosition(this);
 		return ret;
 	}
+
+	@Override
+	public Filter clone()
+	{
+		return (Filter) super.clone();
+	}
 }
 
 //------------------------------------------------------------------------------
diff --git a/prism/src/parser/ast/ForLoop.java b/prism/src/parser/ast/ForLoop.java
index d9120a1dbd..7ccdabad69 100644
--- a/prism/src/parser/ast/ForLoop.java
+++ b/prism/src/parser/ast/ForLoop.java
@@ -154,6 +154,12 @@ public ASTElement deepCopy()
 		ret.setPosition(this);
 		return ret;
 	}
+
+	@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..b7ccc01a0f 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<String> names;
@@ -169,6 +169,19 @@ public ASTElement deepCopy()
 		ret.setPosition(this);
 		return ret;
 	}
+
+	@SuppressWarnings("unchecked")
+	@Override
+	public FormulaList clone()
+	{
+		FormulaList clone = (FormulaList) super.clone();
+
+		clone.formulas   = (Vector<Expression>)      formulas.clone();
+		clone.nameIdents = (Vector<ExpressionIdent>) nameIdents.clone();
+		clone.names      = (Vector<String>)          names.clone();
+
+		return clone;
+	}
 }
 
 // ------------------------------------------------------------------------------
diff --git a/prism/src/parser/ast/LabelList.java b/prism/src/parser/ast/LabelList.java
index 5dfebec5e9..3a69466659 100644
--- a/prism/src/parser/ast/LabelList.java
+++ b/prism/src/parser/ast/LabelList.java
@@ -35,10 +35,10 @@
 
 // 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<String> names;
+	private ArrayList<String> names;
 	private Vector<Expression> labels;
 	// We also store an ExpressionIdent to match each name.
 	// This is to just to provide positional info.
@@ -149,6 +149,19 @@ public ASTElement deepCopy()
 		ret.setPosition(this);
 		return ret;
 	}
+
+	@SuppressWarnings("unchecked")
+	@Override
+	public LabelList clone()
+	{
+		LabelList clone = (LabelList) super.clone();
+
+		clone.labels     = (Vector<Expression>)      labels.clone();
+		clone.nameIdents = (Vector<ExpressionIdent>) nameIdents.clone();
+		clone.names      = (ArrayList<String>)       names.clone();
+
+		return clone;
+	}
 }
 
 //------------------------------------------------------------------------------
diff --git a/prism/src/parser/ast/Module.java b/prism/src/parser/ast/Module.java
index e604b55749..e998d83082 100644
--- a/prism/src/parser/ast/Module.java
+++ b/prism/src/parser/ast/Module.java
@@ -304,6 +304,22 @@ public ASTElement deepCopy()
 		ret.setPosition(this);
 		return ret;
 	}
+
+	@SuppressWarnings("unchecked")
+	@Override
+	public Module clone()
+	{
+		Module clone = (Module) super.clone();
+
+		clone.decls    = (ArrayList<Declaration>) decls.clone();
+		clone.commands = (ArrayList<Command>) commands.clone();
+
+		if (alphabet != null) {
+			clone.alphabet = (Vector<String>) alphabet.clone();
+		}
+
+		return clone;
+	}
 }
 
 //------------------------------------------------------------------------------
diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java
index 9faaf5196d..70c7e3cdd9 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<SystemDefn> systemDefns; // System definitions (system...endsystem constructs)
 	private ArrayList<String> systemDefnNames; // System definition names (system...endsystem constructs)
 	private ArrayList<RewardStruct> rewardStructs; // Rewards structures
-	private List<String> rewardStructNames; // Names of reward structures
+	private ArrayList<String> rewardStructNames; // Names of reward structures
 	private Expression initStates; // Initial states specification
 
 	// Lists of all identifiers used
@@ -1319,6 +1319,39 @@ public ASTElement deepCopy()
 		
 		return ret;
 	}
+
+	@SuppressWarnings("unchecked")
+	@Override
+	public ModulesFile clone()
+	{
+		ModulesFile clone = (ModulesFile) super.clone();
+
+		// clone main components
+		clone.globals           = (Vector<Declaration>) globals.clone();
+		clone.modules           = (Vector<Object>) modules.clone();
+		clone.systemDefnNames   = (ArrayList<String>) systemDefnNames.clone();
+		clone.systemDefns       = (ArrayList<SystemDefn>) systemDefns.clone();
+		clone.rewardStructs     = (ArrayList<RewardStruct>) rewardStructs.clone();
+		clone.rewardStructNames = (ArrayList<String>) rewardStructNames.clone();
+		clone.formulaIdents     = (Vector<String>) formulaIdents.clone();
+		clone.constantIdents    = (Vector<String>) constantIdents.clone();
+		clone.varIdents         = (Vector<String>) varIdents.clone();
+		clone.varDecls          = (Vector<Declaration>) varDecls.clone();
+		clone.varNames          = (Vector<String>) varNames.clone();
+		clone.varTypes          = (Vector<Type>) 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<String>) synchs.clone();
+
+		return clone;
+	}
 }
 
 // ------------------------------------------------------------------------------
diff --git a/prism/src/parser/ast/PropertiesFile.java b/prism/src/parser/ast/PropertiesFile.java
index 050bf4aae7..5a39512cd2 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;
@@ -644,6 +644,24 @@ public ASTElement deepCopy()
 
 		return ret;
 	}
+
+	@SuppressWarnings("unchecked")
+	@Override
+	public PropertiesFile clone()
+	{
+		PropertiesFile clone = (PropertiesFile) super.clone();
+
+		// clone main components
+		clone.properties = (Vector<Property>) properties.clone();
+
+		// clone other (generated) info
+		if (allIdentsUsed != null)
+			clone.allIdentsUsed = (Vector<String>) allIdentsUsed.clone();
+		if (constantValues != null)
+			clone.constantValues = new Values(constantValues);
+
+		return clone;
+	}
 }
 
 //------------------------------------------------------------------------------
diff --git a/prism/src/parser/ast/Property.java b/prism/src/parser/ast/Property.java
index 8469d8d1be..2c99042a16 100644
--- a/prism/src/parser/ast/Property.java
+++ b/prism/src/parser/ast/Property.java
@@ -588,6 +588,12 @@ public Property deepCopy()
 		prop.setPosition(this);
 		return prop;
 	}
+
+	@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..82661dd721 100644
--- a/prism/src/parser/ast/RenamedModule.java
+++ b/prism/src/parser/ast/RenamedModule.java
@@ -200,6 +200,20 @@ public ASTElement deepCopy()
 		ret.setPosition(this);
 		return ret;
 	}
+
+	@SuppressWarnings("unchecked")
+	@Override
+	public RenamedModule clone()
+	{
+		RenamedModule clone = (RenamedModule) super.clone();
+
+		clone.newNameASTElements = (ArrayList<ExpressionIdent>) newNameASTElements.clone();
+		clone.newNames           = (ArrayList<String>) newNames.clone();
+		clone.oldNameASTElements = (ArrayList<ExpressionIdent>) oldNameASTElements.clone();
+		clone.oldNames           = (ArrayList<String>) oldNames.clone();
+		
+		return clone;
+	}
 }
 
 //------------------------------------------------------------------------------
diff --git a/prism/src/parser/ast/RewardStruct.java b/prism/src/parser/ast/RewardStruct.java
index 67dd2445af..358b18dd75 100644
--- a/prism/src/parser/ast/RewardStruct.java
+++ b/prism/src/parser/ast/RewardStruct.java
@@ -160,6 +160,17 @@ public ASTElement deepCopy()
 		ret.setPosition(this);
 		return ret;
 	}
+
+	@SuppressWarnings("unchecked")
+	@Override
+	public RewardStruct clone()
+	{
+		RewardStruct clone = (RewardStruct) super.clone();
+		
+		clone.items = (Vector<RewardStructItem>) items.clone();
+
+		return clone;
+	}
 }
 
 //------------------------------------------------------------------------------
diff --git a/prism/src/parser/ast/RewardStructItem.java b/prism/src/parser/ast/RewardStructItem.java
index 0f8af694a4..9b2a73b7f9 100644
--- a/prism/src/parser/ast/RewardStructItem.java
+++ b/prism/src/parser/ast/RewardStructItem.java
@@ -149,6 +149,12 @@ public ASTElement deepCopy()
 		ret.setPosition(this);
 		return ret;
 	}
+
+	@Override
+	public RewardStructItem clone()
+	{
+		return (RewardStructItem) super.clone();
+	}
 }
 
 //------------------------------------------------------------------------------
diff --git a/prism/src/parser/ast/SystemBrackets.java b/prism/src/parser/ast/SystemBrackets.java
index abd1ceeaea..0b5651d3af 100644
--- a/prism/src/parser/ast/SystemBrackets.java
+++ b/prism/src/parser/ast/SystemBrackets.java
@@ -120,6 +120,12 @@ public SystemDefn deepCopy()
 		ret.setPosition(this);
 		return ret;
 	}
+
+	@Override
+	public SystemBrackets clone()
+	{
+		return (SystemBrackets) super.clone();
+	}
 }
 
 //------------------------------------------------------------------------------
diff --git a/prism/src/parser/ast/SystemFullParallel.java b/prism/src/parser/ast/SystemFullParallel.java
index 8b4ef70192..6a64ccda04 100644
--- a/prism/src/parser/ast/SystemFullParallel.java
+++ b/prism/src/parser/ast/SystemFullParallel.java
@@ -161,6 +161,17 @@ public SystemDefn deepCopy()
 		ret.setPosition(this);
 		return ret;
 	}
+
+	@SuppressWarnings("unchecked")
+	@Override
+	public SystemFullParallel clone()
+	{
+		SystemFullParallel clone = (SystemFullParallel) super.clone();
+
+		clone.operands = (Vector<SystemDefn>) operands.clone();
+
+		return clone;
+	}
 }
 
 //------------------------------------------------------------------------------
diff --git a/prism/src/parser/ast/SystemHide.java b/prism/src/parser/ast/SystemHide.java
index c8931b6534..1186315a5f 100644
--- a/prism/src/parser/ast/SystemHide.java
+++ b/prism/src/parser/ast/SystemHide.java
@@ -165,6 +165,17 @@ public SystemDefn deepCopy()
 		ret.setPosition(this);
 		return ret;
 	}
+
+	@SuppressWarnings("unchecked")
+	@Override
+	public SystemHide clone()
+	{
+		SystemHide clone = (SystemHide) super.clone();
+
+		clone.actions = (Vector<String>) actions.clone();
+
+		return clone;
+	}
 }
 
 //------------------------------------------------------------------------------
diff --git a/prism/src/parser/ast/SystemInterleaved.java b/prism/src/parser/ast/SystemInterleaved.java
index 193a916e8b..cd9bf2f50e 100644
--- a/prism/src/parser/ast/SystemInterleaved.java
+++ b/prism/src/parser/ast/SystemInterleaved.java
@@ -161,6 +161,17 @@ public SystemDefn deepCopy()
 		ret.setPosition(this);
 		return ret;
 	}
+
+	@SuppressWarnings("unchecked")
+	@Override
+	public SystemInterleaved clone()
+	{
+		SystemInterleaved clone = (SystemInterleaved) super.clone();
+
+		clone.operands = (Vector<SystemDefn>) operands.clone();
+
+		return clone;
+	}
 }
 
 //------------------------------------------------------------------------------
diff --git a/prism/src/parser/ast/SystemModule.java b/prism/src/parser/ast/SystemModule.java
index b5d40aa0fb..5556f0e48d 100644
--- a/prism/src/parser/ast/SystemModule.java
+++ b/prism/src/parser/ast/SystemModule.java
@@ -114,6 +114,12 @@ public SystemDefn deepCopy()
 		ret.setPosition(this);
 		return ret;
 	}
+
+	@Override
+	public SystemModule clone()
+	{
+		return (SystemModule) super.clone();
+	}
 }
 
 //------------------------------------------------------------------------------
diff --git a/prism/src/parser/ast/SystemParallel.java b/prism/src/parser/ast/SystemParallel.java
index 383a242c8c..1f7d8073d4 100644
--- a/prism/src/parser/ast/SystemParallel.java
+++ b/prism/src/parser/ast/SystemParallel.java
@@ -179,6 +179,17 @@ public SystemDefn deepCopy()
 		ret.setPosition(this);
 		return ret;
 	}
+
+	@SuppressWarnings("unchecked")
+	@Override
+	public SystemParallel clone()
+	{
+		SystemParallel clone = (SystemParallel) super.clone();
+
+		clone.actions = (Vector<String>) actions.clone();
+
+		return clone;
+	}
 }
 
 //------------------------------------------------------------------------------
diff --git a/prism/src/parser/ast/SystemReference.java b/prism/src/parser/ast/SystemReference.java
index 1312ab5b69..856e75243a 100644
--- a/prism/src/parser/ast/SystemReference.java
+++ b/prism/src/parser/ast/SystemReference.java
@@ -119,6 +119,12 @@ public SystemDefn deepCopy()
 		ret.setPosition(this);
 		return ret;
 	}
+
+	@Override
+	public SystemReference clone()
+	{
+		return (SystemReference) super.clone();
+	}
 }
 
 //------------------------------------------------------------------------------
diff --git a/prism/src/parser/ast/SystemRename.java b/prism/src/parser/ast/SystemRename.java
index ce03b9c73d..ee5e155c7a 100644
--- a/prism/src/parser/ast/SystemRename.java
+++ b/prism/src/parser/ast/SystemRename.java
@@ -208,6 +208,18 @@ public SystemDefn deepCopy()
 		ret.setPosition(this);
 		return ret;
 	}
+
+	@SuppressWarnings("unchecked")
+	@Override
+	public SystemRename clone()
+	{
+		SystemRename clone = (SystemRename) super.clone();
+
+		clone.from = (Vector<String>) from.clone();
+		clone.to   = (Vector<String>) to.clone();
+
+		return clone;
+	}
 }
 
 //------------------------------------------------------------------------------
diff --git a/prism/src/parser/ast/Update.java b/prism/src/parser/ast/Update.java
index 952e1b71f4..1cf6a897c5 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.*;
@@ -351,6 +350,21 @@ public ASTElement deepCopy()
 		ret.setPosition(this);
 		return ret;
 	}
+
+	@SuppressWarnings("unchecked")
+	@Override
+	public Update clone()
+	{
+		Update clone = (Update) super.clone();
+
+		clone.indices   = (ArrayList<Integer>) indices.clone();
+		clone.vars      = (ArrayList<String>) vars.clone();
+		clone.exprs     = (ArrayList<Expression>) exprs.clone();
+		clone.types     = (ArrayList<Type>) types.clone();
+		clone.varIdents = (ArrayList<ExpressionIdent>) varIdents.clone();
+
+		return clone;
+	}
 }
 
 //------------------------------------------------------------------------------
diff --git a/prism/src/parser/ast/Updates.java b/prism/src/parser/ast/Updates.java
index ef92421057..950316f724 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);
@@ -192,6 +193,18 @@ public ASTElement deepCopy()
 		ret.setPosition(this);
 		return ret;
 	}
+
+	@SuppressWarnings("unchecked")
+	@Override
+	public Updates clone()
+	{
+		Updates clone = (Updates) super.clone();
+
+		clone.probs   = (ArrayList<Expression>) probs.clone();
+		clone.updates = (ArrayList<Update>) updates.clone();
+
+		return clone;
+	}
 }
 
 //------------------------------------------------------------------------------

From 802a5a6e296d84838ad7688910680e5773fedd27 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Steffen=20M=C3=A4rcker?= <maercker@tcs.inf.tu-dresden.de>
Date: Mon, 12 Mar 2018 18:07:16 +0100
Subject: [PATCH 7/8] [DAG-copy] Implement deep-copying the AST without
 unfolding the DAG

After certain replacements, e.g., formula substitution, the AST becomes a directed acyclic graph.
On copying wewant to preserve this structure.
The identification of duplicates is non-local since duplicates may appear everywhere in the AST/DAG.

The implementation introduces a new visitor to keep track of duplicate nodes
and makes copying a two-step process:
1. Cloning a node and its internal container types via Object::clone
2. Deep-copying AST child nodes using the visitor
---
 prism/src/parser/ast/ASTElement.java          |  20 +-
 prism/src/parser/ast/Command.java             |  19 +-
 prism/src/parser/ast/ConstantList.java        |  23 +-
 prism/src/parser/ast/Declaration.java         |  14 +-
 prism/src/parser/ast/DeclarationArray.java    |  17 +-
 prism/src/parser/ast/DeclarationBool.java     |  11 +-
 prism/src/parser/ast/DeclarationClock.java    |  10 +-
 prism/src/parser/ast/DeclarationInt.java      |  15 +-
 .../parser/ast/DeclarationIntUnbounded.java   |  10 +-
 prism/src/parser/ast/Expression.java          |   9 +-
 prism/src/parser/ast/ExpressionBinaryOp.java  |  11 +-
 prism/src/parser/ast/ExpressionConstant.java  |   8 +-
 prism/src/parser/ast/ExpressionExists.java    |  11 +-
 prism/src/parser/ast/ExpressionFilter.java    |  13 +-
 prism/src/parser/ast/ExpressionForAll.java    |  11 +-
 prism/src/parser/ast/ExpressionFormula.java   |  11 +-
 prism/src/parser/ast/ExpressionFunc.java      |  16 +-
 prism/src/parser/ast/ExpressionITE.java       |  11 +-
 prism/src/parser/ast/ExpressionIdent.java     |   9 +-
 prism/src/parser/ast/ExpressionLabel.java     |   9 +-
 prism/src/parser/ast/ExpressionLiteral.java   |   6 +-
 prism/src/parser/ast/ExpressionProb.java      |  12 +-
 prism/src/parser/ast/ExpressionProp.java      |   7 +-
 prism/src/parser/ast/ExpressionQuant.java     |  11 +
 prism/src/parser/ast/ExpressionReward.java    |  24 +-
 prism/src/parser/ast/ExpressionSS.java        |  12 +-
 prism/src/parser/ast/ExpressionStrategy.java  |  16 +-
 prism/src/parser/ast/ExpressionTemporal.java  |  21 +-
 prism/src/parser/ast/ExpressionUnaryOp.java   |   9 +-
 prism/src/parser/ast/ExpressionVar.java       |   7 +-
 prism/src/parser/ast/Filter.java              |  16 +-
 prism/src/parser/ast/ForLoop.java             |  24 +-
 prism/src/parser/ast/FormulaList.java         |  18 +-
 prism/src/parser/ast/LabelList.java           |  21 +-
 prism/src/parser/ast/Module.java              |  30 +-
 prism/src/parser/ast/ModulesFile.java         |  69 +--
 prism/src/parser/ast/PropertiesFile.java      |  31 +-
 prism/src/parser/ast/Property.java            |   9 +-
 prism/src/parser/ast/RenamedModule.java       |  26 +-
 prism/src/parser/ast/RewardStruct.java        |  20 +-
 prism/src/parser/ast/RewardStructItem.java    |  16 +-
 prism/src/parser/ast/SystemBrackets.java      |  10 +-
 prism/src/parser/ast/SystemDefn.java          |   7 -
 prism/src/parser/ast/SystemFullParallel.java  |  15 +-
 prism/src/parser/ast/SystemHide.java          |  15 +-
 prism/src/parser/ast/SystemInterleaved.java   |  15 +-
 prism/src/parser/ast/SystemModule.java        |   8 +-
 prism/src/parser/ast/SystemParallel.java      |  17 +-
 prism/src/parser/ast/SystemReference.java     |   8 +-
 prism/src/parser/ast/SystemRename.java        |  13 +-
 prism/src/parser/ast/Update.java              |  20 +-
 prism/src/parser/ast/Updates.java             |  22 +-
 prism/src/parser/visitor/DeepCopy.java        | 438 ++++++++++++++++++
 53 files changed, 742 insertions(+), 509 deletions(-)
 create mode 100644 prism/src/parser/visitor/DeepCopy.java

diff --git a/prism/src/parser/ast/ASTElement.java b/prism/src/parser/ast/ASTElement.java
index 6e28bbbb1b..960f48f9d7 100644
--- a/prism/src/parser/ast/ASTElement.java
+++ b/prism/src/parser/ast/ASTElement.java
@@ -186,7 +186,25 @@ 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
diff --git a/prism/src/parser/ast/Command.java b/prism/src/parser/ast/Command.java
index 02c9a8bd20..8adc91123f 100644
--- a/prism/src/parser/ast/Command.java
+++ b/prism/src/parser/ast/Command.java
@@ -137,19 +137,14 @@ public String toString()
 		s += "] " + guard + " -> " + updates;
 		return s;
 	}
-	
-	/**
-	 * Perform a deep copy.
-	 */
-	public ASTElement deepCopy()
+
+	@Override
+	public Command deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		Command ret = new Command();
-		ret.setSynch(getSynch());
-		ret.setSynchIndex(getSynchIndex());
-		ret.setGuard(getGuard().deepCopy());
-		ret.setUpdates((Updates)getUpdates().deepCopy());
-		ret.setPosition(this);
-		return ret;
+		guard   = copier.copy(guard);
+		updates = copier.copy(updates);
+
+		return this;
 	}
 
 	@Override
diff --git a/prism/src/parser/ast/ConstantList.java b/prism/src/parser/ast/ConstantList.java
index 74d69db63c..ada68d8d70 100644
--- a/prism/src/parser/ast/ConstantList.java
+++ b/prism/src/parser/ast/ConstantList.java
@@ -429,24 +429,17 @@ 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")
+	@SuppressWarnings("unchecked")
 	@Override
 	public ConstantList clone()
 	{
diff --git a/prism/src/parser/ast/Declaration.java b/prism/src/parser/ast/Declaration.java
index d3b7761ba4..8fb0802270 100644
--- a/prism/src/parser/ast/Declaration.java
+++ b/prism/src/parser/ast/Declaration.java
@@ -138,17 +138,13 @@ public String toString()
 		return s;
 	}
 
-	/**
-	 * Perform a deep copy.
-	 */
 	@Override
-	public ASTElement deepCopy()
+	public Declaration deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		Declaration ret = new Declaration(getName(), (DeclarationType)getDeclType().deepCopy());
-		if (getStart() != null)
-			ret.setStart(getStart().deepCopy());
-		ret.setPosition(this);
-		return ret;
+		declType = copier.copy(declType);
+		start    = copier.copy(start);
+
+		return this;
 	}
 
 	@Override
diff --git a/prism/src/parser/ast/DeclarationArray.java b/prism/src/parser/ast/DeclarationArray.java
index 584263d53b..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,18 +122,14 @@ public String toString()
 		return "array [" + low + ".." + high + "] of " + subtype;
 	}
 
-	/**
-	 * Perform a deep copy.
-	 */
 	@Override
-	public ASTElement deepCopy()
+	public DeclarationArray deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		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;
+		low     = copier.copy(low);
+		high    = copier.copy(high);
+		subtype = copier.copy(subtype);
+
+		return this;
 	}
 
 	@Override
diff --git a/prism/src/parser/ast/DeclarationBool.java b/prism/src/parser/ast/DeclarationBool.java
index 451190b0c7..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,14 +76,10 @@ public String toString()
 		return "bool";
 	}
 
-	/**
-	 * Perform a deep copy.
-	 */
-	public ASTElement deepCopy()
+	@Override
+	public DeclarationBool deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		DeclarationBool ret = new DeclarationBool();
-		ret.setPosition(this);
-		return ret;
+		return this;
 	}
 
 	@Override
diff --git a/prism/src/parser/ast/DeclarationClock.java b/prism/src/parser/ast/DeclarationClock.java
index 9ea03639c8..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,15 +79,10 @@ public String toString()
 		return "clock";
 	}
 
-	/**
-	 * Perform a deep copy.
-	 */
 	@Override
-	public ASTElement deepCopy()
+	public DeclarationClock deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		DeclarationClock ret = new DeclarationClock();
-		ret.setPosition(this);
-		return ret;
+		return this;
 	}
 
 	@Override
diff --git a/prism/src/parser/ast/DeclarationInt.java b/prism/src/parser/ast/DeclarationInt.java
index 6529a4583b..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,17 +107,13 @@ public String toString()
 		return "[" + low + ".." + high + "]";
 	}
 
-	/**
-	 * Perform a deep copy.
-	 */
 	@Override
-	public ASTElement deepCopy()
+	public DeclarationInt deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		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;
+		low = copier.copy(low);
+		high = copier.copy(high);
+
+		return this;
 	}
 
 	@Override
diff --git a/prism/src/parser/ast/DeclarationIntUnbounded.java b/prism/src/parser/ast/DeclarationIntUnbounded.java
index 24aae8cdff..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,15 +79,10 @@ public String toString()
 		return "int";
 	}
 
-	/**
-	 * Perform a deep copy.
-	 */
 	@Override
-	public ASTElement deepCopy()
+	public DeclarationIntUnbounded deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		DeclarationIntUnbounded ret = new DeclarationIntUnbounded();
-		ret.setPosition(this);
-		return ret;
+		return this;
 	}
 
 	@Override
diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java
index d71125bcfd..0e52491b53 100644
--- a/prism/src/parser/ast/Expression.java
+++ b/prism/src/parser/ast/Expression.java
@@ -78,10 +78,11 @@ public String getResultName()
 	
 	// Override version of deepCopy() from superclass ASTElement (to reduce casting).
 
-	/**
-	 * Perform a deep copy.
-	 */
-	public abstract Expression deepCopy();
+	@Override
+	public Expression deepCopy()
+	{
+		return (Expression) super.deepCopy();
+	}
 
 	// Utility methods:
 
diff --git a/prism/src/parser/ast/ExpressionBinaryOp.java b/prism/src/parser/ast/ExpressionBinaryOp.java
index 4e2de8c36a..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,12 @@ 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
diff --git a/prism/src/parser/ast/ExpressionConstant.java b/prism/src/parser/ast/ExpressionConstant.java
index 64cc303a8b..2b0469d165 100644
--- a/prism/src/parser/ast/ExpressionConstant.java
+++ b/prism/src/parser/ast/ExpressionConstant.java
@@ -108,13 +108,11 @@ public Object accept(ASTVisitor v) throws PrismLangException
 	{
 		return v.visit(this);
 	}
-	
+
 	@Override
-	public Expression deepCopy()
+	public ExpressionConstant deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		Expression ret = new ExpressionConstant(name, type);
-		ret.setPosition(this);
-		return ret;
+		return this;
 	}
 
 	@Override
diff --git a/prism/src/parser/ast/ExpressionExists.java b/prism/src/parser/ast/ExpressionExists.java
index b3d3780190..1e19b5af40 100644
--- a/prism/src/parser/ast/ExpressionExists.java
+++ b/prism/src/parser/ast/ExpressionExists.java
@@ -99,14 +99,13 @@ public Object accept(ASTVisitor v) throws PrismLangException
 	{
 		return v.visit(this);
 	}
-	
+
 	@Override
-	public Expression deepCopy()
+	public ExpressionExists deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		ExpressionExists expr = new ExpressionExists(expression.deepCopy());
-		expr.setType(type);
-		expr.setPosition(this);
-		return expr;
+		expression = copier.copy(expression);
+
+		return this;
 	}
 
 	@Override
diff --git a/prism/src/parser/ast/ExpressionFilter.java b/prism/src/parser/ast/ExpressionFilter.java
index e026e7305f..585c9da748 100644
--- a/prism/src/parser/ast/ExpressionFilter.java
+++ b/prism/src/parser/ast/ExpressionFilter.java
@@ -254,16 +254,13 @@ 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 this;
 
-		return e;
 	}
 
 	@Override
diff --git a/prism/src/parser/ast/ExpressionForAll.java b/prism/src/parser/ast/ExpressionForAll.java
index 815b31e4d9..885b0a5916 100644
--- a/prism/src/parser/ast/ExpressionForAll.java
+++ b/prism/src/parser/ast/ExpressionForAll.java
@@ -99,14 +99,13 @@ public Object accept(ASTVisitor v) throws PrismLangException
 	{
 		return v.visit(this);
 	}
-	
+
 	@Override
-	public Expression deepCopy()
+	public ExpressionForAll deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		ExpressionForAll expr = new ExpressionForAll(expression.deepCopy());
-		expr.setType(type);
-		expr.setPosition(this);
-		return expr;
+		expression = copier.copy(expression);
+
+		return this;
 	}
 
 	@Override
diff --git a/prism/src/parser/ast/ExpressionFormula.java b/prism/src/parser/ast/ExpressionFormula.java
index 9c5529fda5..b6477bbcf5 100644
--- a/prism/src/parser/ast/ExpressionFormula.java
+++ b/prism/src/parser/ast/ExpressionFormula.java
@@ -122,14 +122,13 @@ public Object accept(ASTVisitor v) throws PrismLangException
 	{
 		return v.visit(this);
 	}
-		
+
 	@Override
-	public Expression deepCopy()
+	public ExpressionFormula deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		ExpressionFormula ret = new ExpressionFormula(name);
-		ret.setDefinition(definition == null ? null : definition.deepCopy());
-		ret.setPosition(this);
-		return ret;
+		definition = copier.copy(definition);
+
+		return this;
 	}
 
 	@Override
diff --git a/prism/src/parser/ast/ExpressionFunc.java b/prism/src/parser/ast/ExpressionFunc.java
index 4f89d83786..5b51b8326f 100644
--- a/prism/src/parser/ast/ExpressionFunc.java
+++ b/prism/src/parser/ast/ExpressionFunc.java
@@ -452,21 +452,11 @@ public Object accept(ASTVisitor v) throws PrismLangException
 	}
 
 	@Override
-	public Expression deepCopy()
+	public ExpressionFunc deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		int i, n;
-		ExpressionFunc e;
-
-		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);
+		copier.copyAll(operands);
 
-		return e;
+		return this;
 	}
 
 	@SuppressWarnings("unchecked")
diff --git a/prism/src/parser/ast/ExpressionITE.java b/prism/src/parser/ast/ExpressionITE.java
index c16344bfbb..a6e2956b96 100644
--- a/prism/src/parser/ast/ExpressionITE.java
+++ b/prism/src/parser/ast/ExpressionITE.java
@@ -122,12 +122,13 @@ 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
diff --git a/prism/src/parser/ast/ExpressionIdent.java b/prism/src/parser/ast/ExpressionIdent.java
index f4606bd832..17fbb28506 100644
--- a/prism/src/parser/ast/ExpressionIdent.java
+++ b/prism/src/parser/ast/ExpressionIdent.java
@@ -106,14 +106,11 @@ public Object accept(ASTVisitor v) throws PrismLangException
 	{
 		return v.visit(this);
 	}
-	
+
 	@Override
-	public Expression deepCopy()
+	public ExpressionIdent deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		ExpressionIdent expr = new ExpressionIdent(name);
-		expr.setType(type);
-		expr.setPosition(this);
-		return expr;
+		return this;
 	}
 
 	@Override
diff --git a/prism/src/parser/ast/ExpressionLabel.java b/prism/src/parser/ast/ExpressionLabel.java
index b03bcb7105..5f142328e9 100644
--- a/prism/src/parser/ast/ExpressionLabel.java
+++ b/prism/src/parser/ast/ExpressionLabel.java
@@ -105,14 +105,11 @@ public Object accept(ASTVisitor v) throws PrismLangException
 	{
 		return v.visit(this);
 	}
-	
+
 	@Override
-	public Expression deepCopy()
+	public ExpressionLabel deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		ExpressionLabel expr = new ExpressionLabel(name);
-		expr.setType(type);
-		expr.setPosition(this);
-		return expr;
+		return this;
 	}
 
 	@Override
diff --git a/prism/src/parser/ast/ExpressionLiteral.java b/prism/src/parser/ast/ExpressionLiteral.java
index 749a018e8d..81985085d3 100644
--- a/prism/src/parser/ast/ExpressionLiteral.java
+++ b/prism/src/parser/ast/ExpressionLiteral.java
@@ -116,11 +116,9 @@ 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
diff --git a/prism/src/parser/ast/ExpressionProb.java b/prism/src/parser/ast/ExpressionProb.java
index adc433c144..0576139919 100644
--- a/prism/src/parser/ast/ExpressionProb.java
+++ b/prism/src/parser/ast/ExpressionProb.java
@@ -28,6 +28,7 @@
 
 import parser.Values;
 import parser.visitor.ASTVisitor;
+import parser.visitor.DeepCopy;
 import prism.OpRelOpBound;
 import prism.PrismLangException;
 
@@ -114,16 +115,9 @@ public Object accept(ASTVisitor v) throws PrismLangException
 	}
 
 	@Override
-	public ExpressionProb 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
diff --git a/prism/src/parser/ast/ExpressionProp.java b/prism/src/parser/ast/ExpressionProp.java
index 1dea56cc45..93334fc583 100644
--- a/prism/src/parser/ast/ExpressionProp.java
+++ b/prism/src/parser/ast/ExpressionProp.java
@@ -95,12 +95,9 @@ 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
diff --git a/prism/src/parser/ast/ExpressionQuant.java b/prism/src/parser/ast/ExpressionQuant.java
index efbd021bef..71ebc09e51 100644
--- a/prism/src/parser/ast/ExpressionQuant.java
+++ b/prism/src/parser/ast/ExpressionQuant.java
@@ -29,6 +29,7 @@
 import param.BigRational;
 import parser.EvaluateContext;
 import parser.Values;
+import parser.visitor.DeepCopy;
 import prism.OpRelOpBound;
 import prism.PrismException;
 import prism.PrismLangException;
@@ -203,6 +204,16 @@ 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
diff --git a/prism/src/parser/ast/ExpressionReward.java b/prism/src/parser/ast/ExpressionReward.java
index 20a90404c3..ad11b83329 100644
--- a/prism/src/parser/ast/ExpressionReward.java
+++ b/prism/src/parser/ast/ExpressionReward.java
@@ -28,6 +28,7 @@
 
 import parser.Values;
 import parser.visitor.ASTVisitor;
+import parser.visitor.DeepCopy;
 import prism.ModelInfo;
 import prism.OpRelOpBound;
 import prism.PrismException;
@@ -223,20 +224,17 @@ public Object accept(ASTVisitor v) throws PrismLangException
 	}
 
 	@Override
-	public ExpressionReward deepCopy()
+	public ExpressionReward deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		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;
+		super.deepCopy(copier);
+		if (rewardStructIndex instanceof Expression) {
+			rewardStructIndex = copier.copy((Expression) rewardStructIndex);
+		}
+		if (rewardStructIndexDiv instanceof Expression) {
+			rewardStructIndexDiv = copier.copy((Expression) rewardStructIndexDiv);
+		}
+
+		return this;
 	}
 
 	@Override
diff --git a/prism/src/parser/ast/ExpressionSS.java b/prism/src/parser/ast/ExpressionSS.java
index 2fc195bce4..91c700466d 100644
--- a/prism/src/parser/ast/ExpressionSS.java
+++ b/prism/src/parser/ast/ExpressionSS.java
@@ -28,6 +28,7 @@
 
 import parser.Values;
 import parser.visitor.ASTVisitor;
+import parser.visitor.DeepCopy;
 import prism.OpRelOpBound;
 import prism.PrismException;
 import prism.PrismLangException;
@@ -102,16 +103,9 @@ public Object accept(ASTVisitor v) throws PrismLangException
 	}
 
 	@Override
-	public ExpressionSS deepCopy()
+	public ExpressionSS deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		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 (ExpressionSS) super.deepCopy(copier);
 	}
 
 	@Override
diff --git a/prism/src/parser/ast/ExpressionStrategy.java b/prism/src/parser/ast/ExpressionStrategy.java
index a1bbe91f9e..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;
 
 /**
@@ -201,18 +202,11 @@ 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")
diff --git a/prism/src/parser/ast/ExpressionTemporal.java b/prism/src/parser/ast/ExpressionTemporal.java
index dd27d7340a..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,14 @@ 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
diff --git a/prism/src/parser/ast/ExpressionUnaryOp.java b/prism/src/parser/ast/ExpressionUnaryOp.java
index bb43414fcd..cdc2ca73aa 100644
--- a/prism/src/parser/ast/ExpressionUnaryOp.java
+++ b/prism/src/parser/ast/ExpressionUnaryOp.java
@@ -162,12 +162,11 @@ 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
diff --git a/prism/src/parser/ast/ExpressionVar.java b/prism/src/parser/ast/ExpressionVar.java
index a4b67446c8..a33304fb0f 100644
--- a/prism/src/parser/ast/ExpressionVar.java
+++ b/prism/src/parser/ast/ExpressionVar.java
@@ -119,12 +119,9 @@ 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
diff --git a/prism/src/parser/ast/Filter.java b/prism/src/parser/ast/Filter.java
index 4494ebc108..4a9a0ce575 100644
--- a/prism/src/parser/ast/Filter.java
+++ b/prism/src/parser/ast/Filter.java
@@ -115,17 +115,13 @@ public String toString()
 		if (maxReq) s += "{max}";
 		return s;
 	}
-	
-	/**
-	 * Perform a deep copy.
-	 */
-	public ASTElement deepCopy()
+
+	@Override
+	public Filter deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		Filter ret = new Filter(expr.deepCopy());
-		ret.setMinRequested(minReq);
-		ret.setMaxRequested(maxReq);
-		ret.setPosition(this);
-		return ret;
+		expr = copier.copy(expr);
+
+		return this;
 	}
 
 	@Override
diff --git a/prism/src/parser/ast/ForLoop.java b/prism/src/parser/ast/ForLoop.java
index 7ccdabad69..68b6cf7bae 100644
--- a/prism/src/parser/ast/ForLoop.java
+++ b/prism/src/parser/ast/ForLoop.java
@@ -138,21 +138,15 @@ 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
diff --git a/prism/src/parser/ast/FormulaList.java b/prism/src/parser/ast/FormulaList.java
index b7ccc01a0f..3248805e34 100644
--- a/prism/src/parser/ast/FormulaList.java
+++ b/prism/src/parser/ast/FormulaList.java
@@ -155,19 +155,13 @@ 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")
diff --git a/prism/src/parser/ast/LabelList.java b/prism/src/parser/ast/LabelList.java
index 3a69466659..022f501301 100644
--- a/prism/src/parser/ast/LabelList.java
+++ b/prism/src/parser/ast/LabelList.java
@@ -31,6 +31,7 @@
 import java.util.Vector;
 
 import parser.visitor.ASTVisitor;
+import parser.visitor.DeepCopy;
 import prism.PrismLangException;
 
 // class to store list of labels
@@ -134,20 +135,14 @@ 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")
diff --git a/prism/src/parser/ast/Module.java b/prism/src/parser/ast/Module.java
index e998d83082..0ef86781de 100644
--- a/prism/src/parser/ast/Module.java
+++ b/prism/src/parser/ast/Module.java
@@ -281,28 +281,16 @@ 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());
-		}
-		if (invariant != null)
-			ret.setInvariant(invariant.deepCopy());
-		ret.setPosition(this);
-		return ret;
+		nameASTElement = copier.copy(nameASTElement);
+		invariant      = copier.copy(invariant);
+		copier.copyAll(decls);
+		copier.copyAll(commands);
+
+		return this;
 	}
 
 	@SuppressWarnings("unchecked")
diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java
index 70c7e3cdd9..2abb831073 100644
--- a/prism/src/parser/ast/ModulesFile.java
+++ b/prism/src/parser/ast/ModulesFile.java
@@ -1267,57 +1267,26 @@ 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<String>)formulaIdents.clone();
-		ret.constantIdents = (constantIdents == null) ? null : (Vector<String>)constantIdents.clone();
-		ret.varIdents = (varIdents == null) ? null : (Vector<String>)varIdents.clone();
-		ret.moduleNames = (moduleNames == null) ? null : moduleNames.clone();
-		ret.synchs = (synchs == null) ? null : (Vector<String>)synchs.clone();
-		if (varDecls != null) {
-			ret.varDecls = new Vector<Declaration>();
-			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<String>)varNames.clone();
-		ret.varTypes = (varTypes == null) ? null : (Vector<Type>)varTypes.clone();
-		ret.constantValues = (constantValues == null) ? null : new Values(constantValues);
-		
-		return ret;
+
+		return this;
 	}
 
 	@SuppressWarnings("unchecked")
diff --git a/prism/src/parser/ast/PropertiesFile.java b/prism/src/parser/ast/PropertiesFile.java
index 5a39512cd2..87891e3260 100644
--- a/prism/src/parser/ast/PropertiesFile.java
+++ b/prism/src/parser/ast/PropertiesFile.java
@@ -619,30 +619,17 @@ public String toString()
 		return s;
 	}
 
-	/**
-	 * Perform a deep copy.
-	 */
-	@SuppressWarnings("unchecked")
-	public ASTElement deepCopy()
+	@Override
+	public PropertiesFile deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		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<String>) allIdentsUsed.clone();
-		ret.constantValues = (constantValues == null) ? null : new Values(constantValues);
+		// deep copy main components
+		formulaList       = copier.copy(formulaList);
+		labelList         = copier.copy(labelList);
+		combinedLabelList = copier.copy(combinedLabelList);
+		constantList      = copier.copy(constantList);
+		copier.copyAll(properties);
 
-		return ret;
+		return this;
 	}
 
 	@SuppressWarnings("unchecked")
diff --git a/prism/src/parser/ast/Property.java b/prism/src/parser/ast/Property.java
index 2c99042a16..b8bb1ceb33 100644
--- a/prism/src/parser/ast/Property.java
+++ b/prism/src/parser/ast/Property.java
@@ -581,12 +581,11 @@ 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
diff --git a/prism/src/parser/ast/RenamedModule.java b/prism/src/parser/ast/RenamedModule.java
index 82661dd721..99bfccd30c 100644
--- a/prism/src/parser/ast/RenamedModule.java
+++ b/prism/src/parser/ast/RenamedModule.java
@@ -183,22 +183,16 @@ 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")
diff --git a/prism/src/parser/ast/RewardStruct.java b/prism/src/parser/ast/RewardStruct.java
index 358b18dd75..47dd897088 100644
--- a/prism/src/parser/ast/RewardStruct.java
+++ b/prism/src/parser/ast/RewardStruct.java
@@ -144,21 +144,13 @@ 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")
diff --git a/prism/src/parser/ast/RewardStructItem.java b/prism/src/parser/ast/RewardStructItem.java
index 9b2a73b7f9..2ff23376f8 100644
--- a/prism/src/parser/ast/RewardStructItem.java
+++ b/prism/src/parser/ast/RewardStructItem.java
@@ -138,16 +138,14 @@ public String toString()
 		
 		return s;
 	}
-	
-	/**
-	 * Perform a deep copy.
-	 */
-	public ASTElement deepCopy()
+
+	@Override
+	public RewardStructItem deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		RewardStructItem ret = new RewardStructItem(synch, states.deepCopy(), reward.deepCopy());
-		ret.setSynchIndex(getSynchIndex());
-		ret.setPosition(this);
-		return ret;
+		states = copier.copy(states);
+		reward = copier.copy(reward);
+
+		return this;
 	}
 
 	@Override
diff --git a/prism/src/parser/ast/SystemBrackets.java b/prism/src/parser/ast/SystemBrackets.java
index 0b5651d3af..a6fe663836 100644
--- a/prism/src/parser/ast/SystemBrackets.java
+++ b/prism/src/parser/ast/SystemBrackets.java
@@ -112,13 +112,13 @@ public String toString()
 	{
 		return "(" + operand + ")";
 	}
-	
+
 	@Override
-	public SystemDefn deepCopy()
+	public SystemBrackets deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		SystemDefn ret = new SystemBrackets(getOperand().deepCopy());
-		ret.setPosition(this);
-		return ret;
+		operand = copier.copy(operand);
+
+		return this;
 	}
 
 	@Override
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 6a64ccda04..73b1101574 100644
--- a/prism/src/parser/ast/SystemFullParallel.java
+++ b/prism/src/parser/ast/SystemFullParallel.java
@@ -148,18 +148,13 @@ 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")
diff --git a/prism/src/parser/ast/SystemHide.java b/prism/src/parser/ast/SystemHide.java
index 1186315a5f..f9522778b5 100644
--- a/prism/src/parser/ast/SystemHide.java
+++ b/prism/src/parser/ast/SystemHide.java
@@ -152,18 +152,13 @@ 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")
diff --git a/prism/src/parser/ast/SystemInterleaved.java b/prism/src/parser/ast/SystemInterleaved.java
index cd9bf2f50e..76844e9893 100644
--- a/prism/src/parser/ast/SystemInterleaved.java
+++ b/prism/src/parser/ast/SystemInterleaved.java
@@ -148,18 +148,13 @@ 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")
diff --git a/prism/src/parser/ast/SystemModule.java b/prism/src/parser/ast/SystemModule.java
index 5556f0e48d..8e71bb5cd5 100644
--- a/prism/src/parser/ast/SystemModule.java
+++ b/prism/src/parser/ast/SystemModule.java
@@ -106,13 +106,11 @@ public String toString()
 	{
 		return name;
 	}
-	
+
 	@Override
-	public SystemDefn deepCopy()
+	public SystemModule deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		SystemDefn ret = new SystemModule(name);
-		ret.setPosition(this);
-		return ret;
+		return this;
 	}
 
 	@Override
diff --git a/prism/src/parser/ast/SystemParallel.java b/prism/src/parser/ast/SystemParallel.java
index 1f7d8073d4..51d04c540a 100644
--- a/prism/src/parser/ast/SystemParallel.java
+++ b/prism/src/parser/ast/SystemParallel.java
@@ -167,17 +167,14 @@ public String toString()
 		
 		return s;
 	}
-	
+
 	@Override
-	@SuppressWarnings("unchecked")
-	public SystemDefn deepCopy()
-	{
-		SystemParallel ret = new SystemParallel();
-		ret.setOperand1(getOperand1().deepCopy());
-		ret.setOperand2(getOperand2().deepCopy());
-		ret.actions = (actions == null) ? null : (Vector<String>)actions.clone();
-		ret.setPosition(this);
-		return ret;
+	public SystemParallel deepCopy(DeepCopy copier) throws PrismLangException
+	{
+		operand1 = copier.copy(operand1);
+		operand2 = copier.copy(operand2);
+
+		return this;
 	}
 
 	@SuppressWarnings("unchecked")
diff --git a/prism/src/parser/ast/SystemReference.java b/prism/src/parser/ast/SystemReference.java
index 856e75243a..cca5dd0d09 100644
--- a/prism/src/parser/ast/SystemReference.java
+++ b/prism/src/parser/ast/SystemReference.java
@@ -111,13 +111,11 @@ public String toString()
 	{
 		return "\"" + name + "\"";
 	}
-	
+
 	@Override
-	public SystemDefn deepCopy()
+	public SystemReference deepCopy(DeepCopy copier) throws PrismLangException
 	{
-		SystemDefn ret = new SystemReference(name);
-		ret.setPosition(this);
-		return ret;
+		return this;
 	}
 
 	@Override
diff --git a/prism/src/parser/ast/SystemRename.java b/prism/src/parser/ast/SystemRename.java
index ee5e155c7a..1732cd724e 100644
--- a/prism/src/parser/ast/SystemRename.java
+++ b/prism/src/parser/ast/SystemRename.java
@@ -197,16 +197,11 @@ 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")
diff --git a/prism/src/parser/ast/Update.java b/prism/src/parser/ast/Update.java
index 1cf6a897c5..67f4ec0fdf 100644
--- a/prism/src/parser/ast/Update.java
+++ b/prism/src/parser/ast/Update.java
@@ -334,21 +334,13 @@ 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")
diff --git a/prism/src/parser/ast/Updates.java b/prism/src/parser/ast/Updates.java
index 950316f724..551488281d 100644
--- a/prism/src/parser/ast/Updates.java
+++ b/prism/src/parser/ast/Updates.java
@@ -175,23 +175,13 @@ 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")
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 <maercker@tcs.inf.tu-dresden.de> (TU Dresden)
+//	* Johannes Kath <s1799679@mail.zih.tu-dresden.de> (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.
+ * <p>
+ * 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.
+ * </p>
+ * <p>
+ * 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.
+ * </p>
+ * @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 extends ASTElement> 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 <T extends ASTElement> List<T> copyAll(List<T> 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 <T extends ASTElement> Vector<T> copyAll(Vector<T> 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 extends ASTElement> 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);
+	}
+}

From 1f5d7ed34849cf8c37bd82f14bc61007b9638e65 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Steffen=20M=C3=A4rcker?= <maercker@tcs.inf.tu-dresden.de>
Date: Mon, 3 Dec 2018 09:20:35 +0100
Subject: [PATCH 8/8] [DAG-copy] Fix for uncareful type change in simplify
 visitor

---
 prism/src/parser/ast/Expression.java   | 10 ++++++++--
 prism/src/parser/visitor/Simplify.java | 25 +++++++++++++++----------
 2 files changed, 23 insertions(+), 12 deletions(-)

diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java
index 0e52491b53..ccd24cfd73 100644
--- a/prism/src/parser/ast/Expression.java
+++ b/prism/src/parser/ast/Expression.java
@@ -75,15 +75,21 @@ public String getResultName()
 	 * when evaluated during model checking?
 	 */
 	public abstract boolean returnsSingleValue();
-	
-	// Override version of deepCopy() from superclass ASTElement (to reduce casting).
 
+	// 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:
 
 	/**
diff --git a/prism/src/parser/visitor/Simplify.java b/prism/src/parser/visitor/Simplify.java
index 99064ebb9c..b9b01b3527 100644
--- a/prism/src/parser/visitor/Simplify.java
+++ b/prism/src/parser/visitor/Simplify.java
@@ -93,13 +93,15 @@ public Object visitNow(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 visitNow(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 visitNow(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