diff --git a/prism/src/parser/ast/Coalition.java b/prism/src/parser/ast/Coalition.java
index 9fb13ab5..c20ca656 100644
--- a/prism/src/parser/ast/Coalition.java
+++ b/prism/src/parser/ast/Coalition.java
@@ -143,4 +143,34 @@ public class Coalition
 	{
 		return allPlayers ? "*" : PrismUtils.joinString(players, ",");
 	}
+
+	@Override
+	public int hashCode()
+	{
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + (allPlayers ? 1231 : 1237);
+		result = prime * result + ((players == null) ? 0 : players.hashCode());
+		return result;
+	}
+
+	@Override
+	public boolean equals(Object obj)
+	{
+		if (this == obj)
+			return true;
+		if (obj == null)
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		Coalition other = (Coalition) obj;
+		if (allPlayers != other.allPlayers)
+			return false;
+		if (players == null) {
+			if (other.players != null)
+				return false;
+		} else if (!players.equals(other.players))
+			return false;
+		return true;
+	}
 }
diff --git a/prism/src/parser/ast/ExpressionBinaryOp.java b/prism/src/parser/ast/ExpressionBinaryOp.java
index 02cc52bb..52945c7f 100644
--- a/prism/src/parser/ast/ExpressionBinaryOp.java
+++ b/prism/src/parser/ast/ExpressionBinaryOp.java
@@ -26,10 +26,10 @@
 
 package parser.ast;
 
-import parser.*;
-import parser.visitor.*;
+import parser.EvaluateContext;
+import parser.type.TypeInt;
+import parser.visitor.ASTVisitor;
 import prism.PrismLangException;
-import parser.type.*;
 
 public class ExpressionBinaryOp extends Expression
 {
@@ -213,6 +213,17 @@ public class ExpressionBinaryOp extends Expression
 		return v.visit(this);
 	}
 
+	@Override
+	public Expression deepCopy()
+	{
+		ExpressionBinaryOp expr = new ExpressionBinaryOp(op, operand1.deepCopy(), operand2.deepCopy());
+		expr.setType(type);
+		expr.setPosition(this);
+		return expr;
+	}
+
+	// Standard methods
+	
 	@Override
 	public String toString()
 	{
@@ -220,12 +231,38 @@ public class ExpressionBinaryOp extends Expression
 	}
 
 	@Override
-	public Expression deepCopy()
+	public int hashCode()
 	{
-		ExpressionBinaryOp expr = new ExpressionBinaryOp(op, operand1.deepCopy(), operand2.deepCopy());
-		expr.setType(type);
-		expr.setPosition(this);
-		return expr;
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + op;
+		result = prime * result + ((operand1 == null) ? 0 : operand1.hashCode());
+		result = prime * result + ((operand2 == null) ? 0 : operand2.hashCode());
+		return result;
+	}
+	@Override
+	public boolean equals(Object obj)
+	{
+		if (this == obj)
+			return true;
+		if (obj == null)
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		ExpressionBinaryOp other = (ExpressionBinaryOp) obj;
+		if (op != other.op)
+			return false;
+		if (operand1 == null) {
+			if (other.operand1 != null)
+				return false;
+		} else if (!operand1.equals(other.operand1))
+			return false;
+		if (operand2 == null) {
+			if (other.operand2 != null)
+				return false;
+		} else if (!operand2.equals(other.operand2))
+			return false;
+		return true;
 	}
 }
 
diff --git a/prism/src/parser/ast/ExpressionConstant.java b/prism/src/parser/ast/ExpressionConstant.java
index 820dbe52..74d87f1b 100644
--- a/prism/src/parser/ast/ExpressionConstant.java
+++ b/prism/src/parser/ast/ExpressionConstant.java
@@ -33,7 +33,7 @@ import parser.type.*;
 
 public class ExpressionConstant extends Expression
 {
-	String name;
+	protected String name;
 	
 	// Constructors
 	
@@ -98,6 +98,16 @@ public class ExpressionConstant extends Expression
 		return v.visit(this);
 	}
 	
+	@Override
+	public Expression deepCopy()
+	{
+		Expression ret = new ExpressionConstant(name, type);
+		ret.setPosition(this);
+		return ret;
+	}
+	
+	// Standard methods
+	
 	@Override
 	public String toString()
 	{
@@ -105,11 +115,30 @@ public class ExpressionConstant extends Expression
 	}
 
 	@Override
-	public Expression deepCopy()
+	public int hashCode()
 	{
-		Expression ret = new ExpressionConstant(name, type);
-		ret.setPosition(this);
-		return ret;
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + ((name == null) ? 0 : name.hashCode());
+		return result;
+	}
+
+	@Override
+	public boolean equals(Object obj)
+	{
+		if (this == obj)
+			return true;
+		if (obj == null)
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		ExpressionConstant other = (ExpressionConstant) obj;
+		if (name == null) {
+			if (other.name != null)
+				return false;
+		} else if (!name.equals(other.name))
+			return false;
+		return true;
 	}
 }
 
diff --git a/prism/src/parser/ast/ExpressionExists.java b/prism/src/parser/ast/ExpressionExists.java
index ebdc22c9..118c6b6b 100644
--- a/prism/src/parser/ast/ExpressionExists.java
+++ b/prism/src/parser/ast/ExpressionExists.java
@@ -32,7 +32,7 @@ import prism.PrismLangException;
 
 public class ExpressionExists extends Expression
 {
-	Expression expression = null;
+	protected Expression expression = null;
 	
 	// Constructors
 	
@@ -93,6 +93,17 @@ public class ExpressionExists extends Expression
 		return v.visit(this);
 	}
 	
+	@Override
+	public Expression deepCopy()
+	{
+		ExpressionExists expr = new ExpressionExists(expression.deepCopy());
+		expr.setType(type);
+		expr.setPosition(this);
+		return expr;
+	}
+
+	// Standard methods
+	
 	@Override
 	public String toString()
 	{
@@ -104,12 +115,30 @@ public class ExpressionExists extends Expression
 	}
 
 	@Override
-	public Expression deepCopy()
+	public int hashCode()
 	{
-		ExpressionExists expr = new ExpressionExists(expression.deepCopy());
-		expr.setType(type);
-		expr.setPosition(this);
-		return expr;
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + ((expression == null) ? 0 : expression.hashCode());
+		return result;
+	}
+
+	@Override
+	public boolean equals(Object obj)
+	{
+		if (this == obj)
+			return true;
+		if (obj == null)
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		ExpressionExists other = (ExpressionExists) obj;
+		if (expression == null) {
+			if (other.expression != null)
+				return false;
+		} else if (!expression.equals(other.expression))
+			return false;
+		return true;
 	}
 }
 
diff --git a/prism/src/parser/ast/ExpressionFilter.java b/prism/src/parser/ast/ExpressionFilter.java
index f963c7fd..42ee6ebc 100644
--- a/prism/src/parser/ast/ExpressionFilter.java
+++ b/prism/src/parser/ast/ExpressionFilter.java
@@ -225,6 +225,21 @@ public class ExpressionFilter extends Expression
 		return v.visit(this);
 	}
 
+	@Override
+	public Expression deepCopy()
+	{
+		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;
+
+		return e;
+	}
+	
+	// Standard methods
+	
 	@Override
 	public String toString()
 	{
@@ -239,20 +254,59 @@ public class ExpressionFilter extends Expression
 	}
 
 	@Override
-	public Expression deepCopy()
+	public int hashCode()
 	{
-		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;
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + (explanationEnabled ? 1231 : 1237);
+		result = prime * result + ((filter == null) ? 0 : filter.hashCode());
+		result = prime * result + (invisible ? 1231 : 1237);
+		result = prime * result + ((opName == null) ? 0 : opName.hashCode());
+		result = prime * result + ((opType == null) ? 0 : opType.hashCode());
+		result = prime * result + ((operand == null) ? 0 : operand.hashCode());
+		result = prime * result + (param ? 1231 : 1237);
+		result = prime * result + (storeVector ? 1231 : 1237);
+		return result;
+	}
 
-		return e;
+	@Override
+	public boolean equals(Object obj)
+	{
+		if (this == obj)
+			return true;
+		if (obj == null)
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		ExpressionFilter other = (ExpressionFilter) obj;
+		if (explanationEnabled != other.explanationEnabled)
+			return false;
+		if (filter == null) {
+			if (other.filter != null)
+				return false;
+		} else if (!filter.equals(other.filter))
+			return false;
+		if (invisible != other.invisible)
+			return false;
+		if (opName == null) {
+			if (other.opName != null)
+				return false;
+		} else if (!opName.equals(other.opName))
+			return false;
+		if (opType != other.opType)
+			return false;
+		if (operand == null) {
+			if (other.operand != null)
+				return false;
+		} else if (!operand.equals(other.operand))
+			return false;
+		if (param != other.param)
+			return false;
+		if (storeVector != other.storeVector)
+			return false;
+		return true;
 	}
 	
-	// Utility methods
-	
 	/**
 	 * Wrap a "default" ExpressionFilter around an Expression representing a property to be model checked,
 	 * in order to pick out a single value (the final result of model checking) from a vector of values for all states.
diff --git a/prism/src/parser/ast/ExpressionForAll.java b/prism/src/parser/ast/ExpressionForAll.java
index d2bd7833..ada2fc90 100644
--- a/prism/src/parser/ast/ExpressionForAll.java
+++ b/prism/src/parser/ast/ExpressionForAll.java
@@ -32,7 +32,7 @@ import prism.PrismLangException;
 
 public class ExpressionForAll extends Expression
 {
-	Expression expression = null;
+	protected Expression expression = null;
 	
 	// Constructors
 	
@@ -93,6 +93,17 @@ public class ExpressionForAll extends Expression
 		return v.visit(this);
 	}
 	
+	@Override
+	public Expression deepCopy()
+	{
+		ExpressionForAll expr = new ExpressionForAll(expression.deepCopy());
+		expr.setType(type);
+		expr.setPosition(this);
+		return expr;
+	}
+
+	// Standard methods
+	
 	@Override
 	public String toString()
 	{
@@ -104,12 +115,30 @@ public class ExpressionForAll extends Expression
 	}
 
 	@Override
-	public Expression deepCopy()
+	public int hashCode()
 	{
-		ExpressionForAll expr = new ExpressionForAll(expression.deepCopy());
-		expr.setType(type);
-		expr.setPosition(this);
-		return expr;
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + ((expression == null) ? 0 : expression.hashCode());
+		return result;
+	}
+
+	@Override
+	public boolean equals(Object obj)
+	{
+		if (this == obj)
+			return true;
+		if (obj == null)
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		ExpressionForAll other = (ExpressionForAll) obj;
+		if (expression == null) {
+			if (other.expression != null)
+				return false;
+		} else if (!expression.equals(other.expression))
+			return false;
+		return true;
 	}
 }
 
diff --git a/prism/src/parser/ast/ExpressionFormula.java b/prism/src/parser/ast/ExpressionFormula.java
index 7791b804..5d1957bd 100644
--- a/prism/src/parser/ast/ExpressionFormula.java
+++ b/prism/src/parser/ast/ExpressionFormula.java
@@ -32,8 +32,8 @@ import prism.PrismLangException;
 
 public class ExpressionFormula extends Expression
 {
-	String name;
-	Expression definition;
+	protected String name;
+	protected Expression definition;
 	
 	// Constructors
 	
@@ -112,6 +112,17 @@ public class ExpressionFormula extends Expression
 		return v.visit(this);
 	}
 		
+	@Override
+	public Expression deepCopy()
+	{
+		ExpressionFormula ret = new ExpressionFormula(name);
+		ret.setDefinition(definition == null ? null : definition.deepCopy());
+		ret.setPosition(this);
+		return ret;
+	}
+
+	// Standard methods
+	
 	@Override
 	public String toString()
 	{
@@ -119,12 +130,36 @@ public class ExpressionFormula extends Expression
 	}
 
 	@Override
-	public Expression deepCopy()
+	public int hashCode()
 	{
-		ExpressionFormula ret = new ExpressionFormula(name);
-		ret.setDefinition(definition == null ? null : definition.deepCopy());
-		ret.setPosition(this);
-		return ret;
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + ((definition == null) ? 0 : definition.hashCode());
+		result = prime * result + ((name == null) ? 0 : name.hashCode());
+		return result;
+	}
+
+	@Override
+	public boolean equals(Object obj)
+	{
+		if (this == obj)
+			return true;
+		if (obj == null)
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		ExpressionFormula other = (ExpressionFormula) obj;
+		if (definition == null) {
+			if (other.definition != null)
+				return false;
+		} else if (!definition.equals(other.definition))
+			return false;
+		if (name == null) {
+			if (other.name != null)
+				return false;
+		} else if (!name.equals(other.name))
+			return false;
+		return true;
 	}
 }
 
diff --git a/prism/src/parser/ast/ExpressionFunc.java b/prism/src/parser/ast/ExpressionFunc.java
index 1f3f6bdb..5cbf1d97 100644
--- a/prism/src/parser/ast/ExpressionFunc.java
+++ b/prism/src/parser/ast/ExpressionFunc.java
@@ -363,6 +363,26 @@ public class ExpressionFunc extends Expression
 		return v.visit(this);
 	}
 
+	@Override
+	public Expression deepCopy()
+	{
+		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);
+
+		return e;
+	}
+	
+	// Standard methods
+	
 	@Override
 	public String toString()
 	{
@@ -388,21 +408,42 @@ public class ExpressionFunc extends Expression
 	}
 
 	@Override
-	public Expression deepCopy()
+	public int hashCode()
 	{
-		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);
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + code;
+		result = prime * result + ((name == null) ? 0 : name.hashCode());
+		result = prime * result + (oldStyle ? 1231 : 1237);
+		result = prime * result + ((operands == null) ? 0 : operands.hashCode());
+		return result;
+	}
 
-		return e;
+	@Override
+	public boolean equals(Object obj)
+	{
+		if (this == obj)
+			return true;
+		if (obj == null)
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		ExpressionFunc other = (ExpressionFunc) obj;
+		if (code != other.code)
+			return false;
+		if (name == null) {
+			if (other.name != null)
+				return false;
+		} else if (!name.equals(other.name))
+			return false;
+		if (oldStyle != other.oldStyle)
+			return false;
+		if (operands == null) {
+			if (other.operands != null)
+				return false;
+		} else if (!operands.equals(other.operands))
+			return false;
+		return true;
 	}
 }
 
diff --git a/prism/src/parser/ast/ExpressionITE.java b/prism/src/parser/ast/ExpressionITE.java
index de5d2ee8..81bfb6c7 100644
--- a/prism/src/parser/ast/ExpressionITE.java
+++ b/prism/src/parser/ast/ExpressionITE.java
@@ -114,6 +114,17 @@ public class ExpressionITE extends Expression
 		return v.visit(this);
 	}
 
+	@Override
+	public Expression deepCopy()
+	{
+		ExpressionITE expr = new ExpressionITE(operand1.deepCopy(), operand2.deepCopy(), operand3.deepCopy());
+		expr.setType(type);
+		expr.setPosition(this);
+		return expr;
+	}
+
+	// Standard methods
+	
 	@Override
 	public String toString()
 	{
@@ -121,12 +132,42 @@ public class ExpressionITE extends Expression
 	}
 
 	@Override
-	public Expression deepCopy()
+	public int hashCode()
 	{
-		ExpressionITE expr = new ExpressionITE(operand1.deepCopy(), operand2.deepCopy(), operand3.deepCopy());
-		expr.setType(type);
-		expr.setPosition(this);
-		return expr;
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + ((operand1 == null) ? 0 : operand1.hashCode());
+		result = prime * result + ((operand2 == null) ? 0 : operand2.hashCode());
+		result = prime * result + ((operand3 == null) ? 0 : operand3.hashCode());
+		return result;
+	}
+
+	@Override
+	public boolean equals(Object obj)
+	{
+		if (this == obj)
+			return true;
+		if (obj == null)
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		ExpressionITE other = (ExpressionITE) obj;
+		if (operand1 == null) {
+			if (other.operand1 != null)
+				return false;
+		} else if (!operand1.equals(other.operand1))
+			return false;
+		if (operand2 == null) {
+			if (other.operand2 != null)
+				return false;
+		} else if (!operand2.equals(other.operand2))
+			return false;
+		if (operand3 == null) {
+			if (other.operand3 != null)
+				return false;
+		} else if (!operand3.equals(other.operand3))
+			return false;
+		return true;
 	}
 }
 
diff --git a/prism/src/parser/ast/ExpressionIdent.java b/prism/src/parser/ast/ExpressionIdent.java
index b43bc6bd..61767826 100644
--- a/prism/src/parser/ast/ExpressionIdent.java
+++ b/prism/src/parser/ast/ExpressionIdent.java
@@ -32,7 +32,7 @@ import prism.PrismLangException;
 
 public class ExpressionIdent extends Expression
 {
-	String name;
+	protected String name;
 	
 	// Constructors
 	
@@ -98,6 +98,17 @@ public class ExpressionIdent extends Expression
 		return v.visit(this);
 	}
 	
+	@Override
+	public Expression deepCopy()
+	{
+		ExpressionIdent expr = new ExpressionIdent(name);
+		expr.setType(type);
+		expr.setPosition(this);
+		return expr;
+	}
+
+	// Standard methods
+	
 	@Override
 	public String toString()
 	{
@@ -105,12 +116,30 @@ public class ExpressionIdent extends Expression
 	}
 
 	@Override
-	public Expression deepCopy()
+	public int hashCode()
 	{
-		ExpressionIdent expr = new ExpressionIdent(name);
-		expr.setType(type);
-		expr.setPosition(this);
-		return expr;
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + ((name == null) ? 0 : name.hashCode());
+		return result;
+	}
+
+	@Override
+	public boolean equals(Object obj)
+	{
+		if (this == obj)
+			return true;
+		if (obj == null)
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		ExpressionIdent other = (ExpressionIdent) obj;
+		if (name == null) {
+			if (other.name != null)
+				return false;
+		} else if (!name.equals(other.name))
+			return false;
+		return true;
 	}
 }
 
diff --git a/prism/src/parser/ast/ExpressionLabel.java b/prism/src/parser/ast/ExpressionLabel.java
index 299e13d3..fac2e3e5 100644
--- a/prism/src/parser/ast/ExpressionLabel.java
+++ b/prism/src/parser/ast/ExpressionLabel.java
@@ -83,6 +83,17 @@ public class ExpressionLabel extends Expression
 		return v.visit(this);
 	}
 	
+	@Override
+	public Expression deepCopy()
+	{
+		ExpressionLabel expr = new ExpressionLabel(name);
+		expr.setType(type);
+		expr.setPosition(this);
+		return expr;
+	}
+
+	// Standard methods
+
 	@Override
 	public String toString()
 	{
@@ -90,12 +101,30 @@ public class ExpressionLabel extends Expression
 	}
 
 	@Override
-	public Expression deepCopy()
+	public int hashCode()
 	{
-		ExpressionLabel expr = new ExpressionLabel(name);
-		expr.setType(type);
-		expr.setPosition(this);
-		return expr;
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + ((name == null) ? 0 : name.hashCode());
+		return result;
+	}
+
+	@Override
+	public boolean equals(Object obj)
+	{
+		if (this == obj)
+			return true;
+		if (obj == null)
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		ExpressionLabel other = (ExpressionLabel) obj;
+		if (name == null) {
+			if (other.name != null)
+				return false;
+		} else if (!name.equals(other.name))
+			return false;
+		return true;
 	}
 }
 
diff --git a/prism/src/parser/ast/ExpressionLiteral.java b/prism/src/parser/ast/ExpressionLiteral.java
index 5e3ed2de..9490aad9 100644
--- a/prism/src/parser/ast/ExpressionLiteral.java
+++ b/prism/src/parser/ast/ExpressionLiteral.java
@@ -107,6 +107,16 @@ public class ExpressionLiteral extends Expression
 	{
 		return v.visit(this);
 	}
+
+	@Override
+	public Expression deepCopy()
+	{
+		Expression expr = new ExpressionLiteral(type, value, string);
+		expr.setPosition(this);
+		return expr;
+	}
+
+	// Standard methods
 	
 	@Override
 	public String toString()
@@ -115,11 +125,36 @@ public class ExpressionLiteral extends Expression
 	}
 
 	@Override
-	public Expression deepCopy()
+	public int hashCode()
 	{
-		Expression expr = new ExpressionLiteral(type, value, string);
-		expr.setPosition(this);
-		return expr;
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + ((string == null) ? 0 : string.hashCode());
+		result = prime * result + ((value == null) ? 0 : value.hashCode());
+		return result;
+	}
+
+	@Override
+	public boolean equals(Object obj)
+	{
+		if (this == obj)
+			return true;
+		if (obj == null)
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		ExpressionLiteral other = (ExpressionLiteral) obj;
+		if (string == null) {
+			if (other.string != null)
+				return false;
+		} else if (!string.equals(other.string))
+			return false;
+		if (value == null) {
+			if (other.value != null)
+				return false;
+		} else if (!value.equals(other.value))
+			return false;
+		return true;
 	}
 }
 
diff --git a/prism/src/parser/ast/ExpressionProb.java b/prism/src/parser/ast/ExpressionProb.java
index 2224d157..ddbb724a 100644
--- a/prism/src/parser/ast/ExpressionProb.java
+++ b/prism/src/parser/ast/ExpressionProb.java
@@ -139,6 +139,21 @@ public class ExpressionProb extends ExpressionQuant
 		return v.visit(this);
 	}
 
+	@Override
+	public Expression deepCopy()
+	{
+		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;
+	}
+
+	// Standard methods
+
 	@Override
 	public String toString()
 	{
@@ -153,19 +168,6 @@ public class ExpressionProb extends ExpressionQuant
 
 		return s;
 	}
-
-	@Override
-	public Expression deepCopy()
-	{
-		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;
-	}
 }
 
 //------------------------------------------------------------------------------
diff --git a/prism/src/parser/ast/ExpressionProp.java b/prism/src/parser/ast/ExpressionProp.java
index d3e11037..2dc10475 100644
--- a/prism/src/parser/ast/ExpressionProp.java
+++ b/prism/src/parser/ast/ExpressionProp.java
@@ -86,6 +86,17 @@ public class ExpressionProp extends Expression
 	{
 		return v.visit(this);
 	}
+
+	@Override
+	public Expression deepCopy()
+	{
+		ExpressionProp expr = new ExpressionProp(name);
+		expr.setType(type);
+		expr.setPosition(this);
+		return expr;
+	}
+
+	// Standard methods
 	
 	@Override
 	public String toString()
@@ -94,12 +105,30 @@ public class ExpressionProp extends Expression
 	}
 
 	@Override
-	public Expression deepCopy()
+	public int hashCode()
 	{
-		ExpressionProp expr = new ExpressionProp(name);
-		expr.setType(type);
-		expr.setPosition(this);
-		return expr;
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + ((name == null) ? 0 : name.hashCode());
+		return result;
+	}
+
+	@Override
+	public boolean equals(Object obj)
+	{
+		if (this == obj)
+			return true;
+		if (obj == null)
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		ExpressionProp other = (ExpressionProp) obj;
+		if (name == null) {
+			if (other.name != null)
+				return false;
+		} else if (!name.equals(other.name))
+			return false;
+		return true;
 	}
 }
 
diff --git a/prism/src/parser/ast/ExpressionQuant.java b/prism/src/parser/ast/ExpressionQuant.java
index 6142cc2e..20d2c904 100644
--- a/prism/src/parser/ast/ExpressionQuant.java
+++ b/prism/src/parser/ast/ExpressionQuant.java
@@ -160,6 +160,56 @@ public abstract class ExpressionQuant extends Expression
 	{
 		return filter;
 	}
+
+	// Standard methods
+	
+	@Override
+	public int hashCode()
+	{
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + ((bound == null) ? 0 : bound.hashCode());
+		result = prime * result + ((expression == null) ? 0 : expression.hashCode());
+		result = prime * result + ((filter == null) ? 0 : filter.hashCode());
+		result = prime * result + ((modifier == null) ? 0 : modifier.hashCode());
+		result = prime * result + ((relOp == null) ? 0 : relOp.hashCode());
+		return result;
+	}
+
+	@Override
+	public boolean equals(Object obj)
+	{
+		if (this == obj)
+			return true;
+		if (obj == null)
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		ExpressionQuant other = (ExpressionQuant) obj;
+		if (bound == null) {
+			if (other.bound != null)
+				return false;
+		} else if (!bound.equals(other.bound))
+			return false;
+		if (expression == null) {
+			if (other.expression != null)
+				return false;
+		} else if (!expression.equals(other.expression))
+			return false;
+		if (filter == null) {
+			if (other.filter != null)
+				return false;
+		} else if (!filter.equals(other.filter))
+			return false;
+		if (modifier == null) {
+			if (other.modifier != null)
+				return false;
+		} else if (!modifier.equals(other.modifier))
+			return false;
+		if (relOp != other.relOp)
+			return false;
+		return true;
+	}
 }
 
 //------------------------------------------------------------------------------
diff --git a/prism/src/parser/ast/ExpressionReward.java b/prism/src/parser/ast/ExpressionReward.java
index 052acb25..192c8fe2 100644
--- a/prism/src/parser/ast/ExpressionReward.java
+++ b/prism/src/parser/ast/ExpressionReward.java
@@ -224,6 +224,25 @@ public class ExpressionReward extends ExpressionQuant
 	{
 		return v.visit(this);
 	}
+
+	@Override
+	public Expression deepCopy()
+	{
+		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;
+	}
+
+	// Standard methods
 	
 	@Override
 	public String toString()
@@ -250,20 +269,36 @@ public class ExpressionReward extends ExpressionQuant
 	}
 
 	@Override
-	public Expression deepCopy()
+	public int hashCode()
 	{
-		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;
+		final int prime = 31;
+		int result = super.hashCode();
+		result = prime * result + ((rewardStructIndex == null) ? 0 : rewardStructIndex.hashCode());
+		result = prime * result + ((rewardStructIndexDiv == null) ? 0 : rewardStructIndexDiv.hashCode());
+		return result;
+	}
+
+	@Override
+	public boolean equals(Object obj)
+	{
+		if (this == obj)
+			return true;
+		if (!super.equals(obj))
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		ExpressionReward other = (ExpressionReward) obj;
+		if (rewardStructIndex == null) {
+			if (other.rewardStructIndex != null)
+				return false;
+		} else if (!rewardStructIndex.equals(other.rewardStructIndex))
+			return false;
+		if (rewardStructIndexDiv == null) {
+			if (other.rewardStructIndexDiv != null)
+				return false;
+		} else if (!rewardStructIndexDiv.equals(other.rewardStructIndexDiv))
+			return false;
+		return true;
 	}
 }
 
diff --git a/prism/src/parser/ast/ExpressionSS.java b/prism/src/parser/ast/ExpressionSS.java
index 280fd860..9225be19 100644
--- a/prism/src/parser/ast/ExpressionSS.java
+++ b/prism/src/parser/ast/ExpressionSS.java
@@ -124,6 +124,21 @@ public class ExpressionSS extends ExpressionQuant
 	{
 		return v.visit(this);
 	}
+
+	@Override
+	public Expression deepCopy()
+	{
+		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;
+	}
+
+	// Standard methods
 	
 	@Override
 	public String toString()
@@ -138,19 +153,6 @@ public class ExpressionSS extends ExpressionQuant
 		
 		return s;
 	}
-
-	@Override
-	public Expression deepCopy()
-	{
-		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;
-	}
 }
 
 //------------------------------------------------------------------------------
diff --git a/prism/src/parser/ast/ExpressionStrategy.java b/prism/src/parser/ast/ExpressionStrategy.java
index fba1c45b..77c00b9f 100644
--- a/prism/src/parser/ast/ExpressionStrategy.java
+++ b/prism/src/parser/ast/ExpressionStrategy.java
@@ -161,6 +161,20 @@ public class ExpressionStrategy extends Expression
 		return v.visit(this);
 	}
 
+	@Override
+	public Expression deepCopy()
+	{
+		ExpressionStrategy expr = new ExpressionStrategy();
+		expr.setThereExists(isThereExists());
+		expr.coalition = new Coalition(coalition);
+		expr.setExpression(expression == null ? null : expression.deepCopy());
+		expr.setType(type);
+		expr.setPosition(this);
+		return expr;
+	}
+
+	// Standard methods
+
 	@Override
 	public String toString()
 	{
@@ -173,14 +187,38 @@ public class ExpressionStrategy extends Expression
 	}
 
 	@Override
-	public Expression deepCopy()
+	public int hashCode()
 	{
-		ExpressionStrategy expr = new ExpressionStrategy();
-		expr.setThereExists(isThereExists());
-		expr.coalition = new Coalition(coalition);
-		expr.setExpression(expression == null ? null : expression.deepCopy());
-		expr.setType(type);
-		expr.setPosition(this);
-		return expr;
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + ((coalition == null) ? 0 : coalition.hashCode());
+		result = prime * result + ((expression == null) ? 0 : expression.hashCode());
+		result = prime * result + (thereExists ? 1231 : 1237);
+		return result;
+	}
+
+	@Override
+	public boolean equals(Object obj)
+	{
+		if (this == obj)
+			return true;
+		if (obj == null)
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		ExpressionStrategy other = (ExpressionStrategy) obj;
+		if (coalition == null) {
+			if (other.coalition != null)
+				return false;
+		} else if (!coalition.equals(other.coalition))
+			return false;
+		if (expression == null) {
+			if (other.expression != null)
+				return false;
+		} else if (!expression.equals(other.expression))
+			return false;
+		if (thereExists != other.thereExists)
+			return false;
+		return true;
 	}
 }
diff --git a/prism/src/parser/ast/ExpressionTemporal.java b/prism/src/parser/ast/ExpressionTemporal.java
index 6cfa3030..73a5edac 100644
--- a/prism/src/parser/ast/ExpressionTemporal.java
+++ b/prism/src/parser/ast/ExpressionTemporal.java
@@ -237,6 +237,25 @@ public class ExpressionTemporal extends Expression
 		return v.visit(this);
 	}
 
+	@Override
+	public Expression deepCopy()
+	{
+		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;
+	}
+
+	// Standard methods
+
 	@Override
 	public String toString()
 	{
@@ -267,20 +286,60 @@ public class ExpressionTemporal extends Expression
 	}
 
 	@Override
-	public Expression deepCopy()
+	public int hashCode()
 	{
-		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;
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + (equals ? 1231 : 1237);
+		result = prime * result + ((lBound == null) ? 0 : lBound.hashCode());
+		result = prime * result + (lBoundStrict ? 1231 : 1237);
+		result = prime * result + op;
+		result = prime * result + ((operand1 == null) ? 0 : operand1.hashCode());
+		result = prime * result + ((operand2 == null) ? 0 : operand2.hashCode());
+		result = prime * result + ((uBound == null) ? 0 : uBound.hashCode());
+		result = prime * result + (uBoundStrict ? 1231 : 1237);
+		return result;
+	}
+
+	@Override
+	public boolean equals(Object obj)
+	{
+		if (this == obj)
+			return true;
+		if (obj == null)
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		ExpressionTemporal other = (ExpressionTemporal) obj;
+		if (equals != other.equals)
+			return false;
+		if (lBound == null) {
+			if (other.lBound != null)
+				return false;
+		} else if (!lBound.equals(other.lBound))
+			return false;
+		if (lBoundStrict != other.lBoundStrict)
+			return false;
+		if (op != other.op)
+			return false;
+		if (operand1 == null) {
+			if (other.operand1 != null)
+				return false;
+		} else if (!operand1.equals(other.operand1))
+			return false;
+		if (operand2 == null) {
+			if (other.operand2 != null)
+				return false;
+		} else if (!operand2.equals(other.operand2))
+			return false;
+		if (uBound == null) {
+			if (other.uBound != null)
+				return false;
+		} else if (!uBound.equals(other.uBound))
+			return false;
+		if (uBoundStrict != other.uBoundStrict)
+			return false;
+		return true;
 	}
 
 	// Other useful methods
diff --git a/prism/src/parser/ast/ExpressionUnaryOp.java b/prism/src/parser/ast/ExpressionUnaryOp.java
index 4a2f0bbe..29eb24b9 100644
--- a/prism/src/parser/ast/ExpressionUnaryOp.java
+++ b/prism/src/parser/ast/ExpressionUnaryOp.java
@@ -132,6 +132,17 @@ public class ExpressionUnaryOp extends Expression
 		return v.visit(this);
 	}
 
+	@Override
+	public Expression deepCopy()
+	{
+		ExpressionUnaryOp expr = new ExpressionUnaryOp(op, operand.deepCopy());
+		expr.setType(type);
+		expr.setPosition(this);
+		return expr;
+	}
+
+	// Standard methods
+
 	@Override
 	public String toString()
 	{
@@ -142,12 +153,33 @@ public class ExpressionUnaryOp extends Expression
 	}
 
 	@Override
-	public Expression deepCopy()
+	public int hashCode()
 	{
-		ExpressionUnaryOp expr = new ExpressionUnaryOp(op, operand.deepCopy());
-		expr.setType(type);
-		expr.setPosition(this);
-		return expr;
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + op;
+		result = prime * result + ((operand == null) ? 0 : operand.hashCode());
+		return result;
+	}
+
+	@Override
+	public boolean equals(Object obj)
+	{
+		if (this == obj)
+			return true;
+		if (obj == null)
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		ExpressionUnaryOp other = (ExpressionUnaryOp) obj;
+		if (op != other.op)
+			return false;
+		if (operand == null) {
+			if (other.operand != null)
+				return false;
+		} else if (!operand.equals(other.operand))
+			return false;
+		return true;
 	}
 }
 
diff --git a/prism/src/parser/ast/ExpressionVar.java b/prism/src/parser/ast/ExpressionVar.java
index d6e2edcc..dc1dad34 100644
--- a/prism/src/parser/ast/ExpressionVar.java
+++ b/prism/src/parser/ast/ExpressionVar.java
@@ -107,6 +107,17 @@ public class ExpressionVar extends Expression
 	{
 		return v.visit(this);
 	}
+
+	@Override
+	public Expression deepCopy()
+	{
+		ExpressionVar expr = new ExpressionVar(name, type);
+		expr.setIndex(index);
+		expr.setPosition(this);
+		return expr;
+	}
+
+	// Standard methods
 	
 	@Override
 	public String toString()
@@ -115,12 +126,33 @@ public class ExpressionVar extends Expression
 	}
 
 	@Override
-	public Expression deepCopy()
+	public int hashCode()
 	{
-		ExpressionVar expr = new ExpressionVar(name, type);
-		expr.setIndex(index);
-		expr.setPosition(this);
-		return expr;
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + index;
+		result = prime * result + ((name == null) ? 0 : name.hashCode());
+		return result;
+	}
+
+	@Override
+	public boolean equals(Object obj)
+	{
+		if (this == obj)
+			return true;
+		if (obj == null)
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		ExpressionVar other = (ExpressionVar) obj;
+		if (index != other.index)
+			return false;
+		if (name == null) {
+			if (other.name != null)
+				return false;
+		} else if (!name.equals(other.name))
+			return false;
+		return true;
 	}
 }