diff --git a/src/main/java/de/tlc4b/analysis/Typechecker.java b/src/main/java/de/tlc4b/analysis/Typechecker.java
index cb927d6fdc779ae337b5f8c3e630f146dc3ad94a..fbd148e46a278a4a89e0098c23ada8e08db5d6e6 100644
--- a/src/main/java/de/tlc4b/analysis/Typechecker.java
+++ b/src/main/java/de/tlc4b/analysis/Typechecker.java
@@ -1294,42 +1294,10 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
 		setType(node.getExpression(), new UntypedType());
 		node.getExpression().apply(this);
 
-
 		BType found = new SetType(getType(node.getExpression()));
 
 		BType expected = getType(node);
-		try {
-			found.unify(expected, this);
-		} catch (UnificationException e) {
-			throw new TypeErrorException("Excepted '" + expected + "' , found "
-					+ found + "'");
-		}
-		
-		
-//		List<PExpression> copy = new ArrayList<PExpression>(
-//				node.getIdentifiers());
-//		for (PExpression e : copy) {
-//			AIdentifierExpression v = (AIdentifierExpression) e;
-//			UntypedType u = new UntypedType();
-//			setType(v, u);
-//		}
-//		
-//		setType(node.getPredicates(), BoolType.getInstance());
-//		node.getPredicates().apply(this);
-//		
-//		setType(node.getExpression(), new UntypedType());
-//		node.getExpression().apply(this);
-//		
-//		BType expr = getType(node.getExpression());
-//		System.out.println(getType(node.getExpression()));
-//
-//		BType expected = getType(node);
-//		SetType set = new SetType(getType(node.getExpression()));
-//		unify(expected, set, node);
-//		BType type = getType(node);
-//		System.out.println(getType(node));
-
-
+		unify(expected, found, node);
 	}
 
 	public static BType makePair(ArrayList<BType> list) {
@@ -1863,7 +1831,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
 			setType(e, new UntypedType());
 			e.apply(this);
 		}
-		
+
 		for (PExpression e : copy) {
 			list.add(getType(e));
 		}
@@ -2175,7 +2143,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
 		} catch (UnificationException e) {
 			throw new TypeErrorException("Excepted '" + expected + "' , found "
 					+ found + "' at " + node.getClass().getSimpleName() + "\n "
-					+ node.getStartPos());
+					+ node.getStartPos() + ":" + node.getEndPos());
 		}
 	}
 
diff --git a/src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java b/src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java
index 1207e8b7afc1262e68606c1a8f7c6066ba1df5bb..707137ddf5faacb71e98fe298ef49aea0e5c5d49 100644
--- a/src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java
+++ b/src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java
@@ -3,9 +3,11 @@ package de.tlc4b.analysis.transformation;
 import java.util.ArrayList;
 import java.util.Hashtable;
 import java.util.LinkedList;
+import java.util.Set;
 
 import de.be4.classicalb.core.parser.Utils;
 import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
+import de.be4.classicalb.core.parser.node.ABooleanTrueExpression;
 import de.be4.classicalb.core.parser.node.AComprehensionSetExpression;
 import de.be4.classicalb.core.parser.node.AConjunctPredicate;
 import de.be4.classicalb.core.parser.node.ACoupleExpression;
@@ -14,12 +16,30 @@ import de.be4.classicalb.core.parser.node.AEqualPredicate;
 import de.be4.classicalb.core.parser.node.AEventBComprehensionSetExpression;
 import de.be4.classicalb.core.parser.node.AIdentifierExpression;
 import de.be4.classicalb.core.parser.node.AMemberPredicate;
+import de.be4.classicalb.core.parser.node.Node;
 import de.be4.classicalb.core.parser.node.PExpression;
 import de.be4.classicalb.core.parser.node.PPredicate;
 import de.be4.classicalb.core.parser.node.Start;
-
+import de.tlc4b.util.UtilMethods;
+
+/**
+ * This class performs an AST transformation on set comprehension nodes. For
+ * example the expression {a,b| a = b & b : 1..10} will be replaced by the
+ * Event-B set comprehension {b. b : 1..10 | b |-> b}. Moreover, if the parent
+ * of a set comprehension is a domain expression, this will also be used for the
+ * optimization, e.g. {a,b| a = b + 1 & b : 1..10} will be replaced by {b. b :
+ * 1..10 | b + 1}
+ * 
+ * @author hansen
+ * 
+ */
 public class SetComprehensionOptimizer extends DepthFirstAdapter {
 
+	/**
+	 * The method called by the translator.
+	 * 
+	 * @param start
+	 */
 	public static void optimizeSetComprehensions(Start start) {
 		SetComprehensionOptimizer optimizer = new SetComprehensionOptimizer();
 		start.apply(optimizer);
@@ -27,63 +47,6 @@ public class SetComprehensionOptimizer extends DepthFirstAdapter {
 
 	@Override
 	public void caseAComprehensionSetExpression(AComprehensionSetExpression node) {
-		if (node.parent() instanceof ADomainExpression) {
-			LinkedList<PExpression> identifiers = node.getIdentifiers();
-
-			final ArrayList<String> list = new ArrayList<String>();
-			final AIdentifierExpression last = (AIdentifierExpression) identifiers
-					.getLast();
-			for (int i = 0; i < identifiers.size() - 1; i++) {
-				AIdentifierExpression id = (AIdentifierExpression) identifiers
-						.get(i);
-				String name = Utils.getIdentifierAsString(id.getIdentifier());
-				list.add(name);
-			}
-
-			Hashtable<String, PExpression> values = new Hashtable<String, PExpression>();
-			ArrayList<AEqualPredicate> equalList = new ArrayList<AEqualPredicate>();
-			analysePredicate(node.getPredicates(), list, values, equalList);
-
-			if (values.keySet().containsAll(list)) {
-				// delete nodes
-				new NodesRemover(node.getPredicates(), equalList, values);
-
-				AEventBComprehensionSetExpression eventBcomprehension = new AEventBComprehensionSetExpression();
-				ArrayList<PExpression> ids = new ArrayList<PExpression>();
-				ids.add(last);
-				eventBcomprehension.setIdentifiers(ids);
-
-				ACoupleExpression couple = new ACoupleExpression();
-
-				ArrayList<PExpression> exprs = new ArrayList<PExpression>();
-				for (int i = 0; i < list.size(); i++) {
-					exprs.add(values.get(list.get(i)));
-				}
-				couple.setList(exprs);
-				eventBcomprehension.setExpression(couple);
-
-				AMemberPredicate member = new AMemberPredicate();
-				member.setLeft((AIdentifierExpression) last.clone());
-				AComprehensionSetExpression compre = new AComprehensionSetExpression();
-				ArrayList<PExpression> ids2 = new ArrayList<PExpression>();
-				ids2.add((AIdentifierExpression) last.clone());
-				compre.setIdentifiers(ids2);
-				compre.setPredicates(node.getPredicates());
-				member.setRight(compre);
-				eventBcomprehension.setPredicates(member);
-
-				node.parent().replaceBy(eventBcomprehension);
-
-				eventBcomprehension.apply(this);
-			}
-		}
-
-		if (node.parent() != null)
-			testGeneric(node);
-
-	}
-
-	private void testGeneric(AComprehensionSetExpression node) {
 		final LinkedList<PExpression> identifiers = node.getIdentifiers();
 		final ArrayList<String> list = new ArrayList<String>();
 		final Hashtable<String, AIdentifierExpression> identifierTable = new Hashtable<String, AIdentifierExpression>();
@@ -98,67 +61,118 @@ public class SetComprehensionOptimizer extends DepthFirstAdapter {
 		Hashtable<String, PExpression> values = new Hashtable<String, PExpression>();
 		ArrayList<AEqualPredicate> equalList = new ArrayList<AEqualPredicate>();
 		analysePredicate(node.getPredicates(), list, values, equalList);
-		if (values.size() > 0 && list.size()-values.size() > 0) {
+
+		ArrayList<ADomainExpression> parentDomainExprsList = collectParentDomainExpression(node
+				.parent());
+
+		// The set comprehension will be optimized if there is an equal node (
+		// {x,y| x =
+		// 1..} ) or the parent node is a domain expression (dom({..})).
+		// There must be less equal nodes than quantified variables, otherwise
+		// there
+		// is no remaining variable to be quantified.
+		// Moreover, the TLA+ syntax is restricted to non-nested tuples in a set
+		// comprehension ({v : <<a,b>> \in S}.
+		// Hence, there must be at most two remaining variables.
+		// If these conditions are not fulfilled, the AST transformation will
+		// not be applied.
+		// However, other optimization techniques may be applicable.
+
+		if ((values.size() > 0 || parentDomainExprsList.size() > 0)
+				&& values.size() < list.size()
+				&& list.size() - values.size() <= 2) {
+
 			// delete nodes
 			new NodesRemover(node.getPredicates(), equalList, values);
 
-			AEventBComprehensionSetExpression eventBcomprehension = new AEventBComprehensionSetExpression();
+			int max = Math.min(list.size() - 1, parentDomainExprsList.size());
+			int exprCount = list.size() - max;
+
+			// {ids. ids2 \in {ids3 \in S: P } | exprs}
 			ArrayList<PExpression> ids = new ArrayList<PExpression>();
 			ArrayList<PExpression> ids2 = new ArrayList<PExpression>();
 			ArrayList<PExpression> ids3 = new ArrayList<PExpression>();
-			for (String p : list) {
-				if (!values.containsKey(p)) {
-					PExpression clone = (PExpression) identifierTable.get(p)
+			ArrayList<PExpression> exprs = new ArrayList<PExpression>();
+			for (int i = 0; i < list.size(); i++) {
+				String name = list.get(i);
+
+				// expression list
+				if (i < exprCount) {
+					if (values.containsKey(name)) {
+						exprs.add(values.get(name));
+					} else {
+						PExpression clone = (PExpression) identifierTable.get(
+								name).clone();
+						exprs.add(clone);
+					}
+				}
+
+				// remaining quantified variables
+				if (!values.containsKey(name)) {
+					PExpression clone = (PExpression) identifierTable.get(name)
 							.clone();
 					ids.add(clone);
-					PExpression clone2 = (PExpression) identifierTable.get(p)
-							.clone();
+					PExpression clone2 = (PExpression) identifierTable
+							.get(name).clone();
 					ids2.add(clone2);
-					PExpression clone3 = (PExpression) identifierTable.get(p)
-							.clone();
+					PExpression clone3 = (PExpression) identifierTable
+							.get(name).clone();
 					ids3.add(clone3);
 				}
 			}
-			eventBcomprehension.setIdentifiers(ids);
 
+			AEventBComprehensionSetExpression eventBcomprehension = new AEventBComprehensionSetExpression();
 			ACoupleExpression couple = new ACoupleExpression();
-			ArrayList<PExpression> exprs = new ArrayList<PExpression>();
-			for (int i = 0; i < list.size(); i++) {
-				String name = list.get(i);
-				if (values.containsKey(name)) {
-					exprs.add(values.get(name));
-				} else {
-					PExpression clone = (PExpression) identifierTable.get(name)
-							.clone();
-					exprs.add(clone);
-				}
-
-			}
 			couple.setList(exprs);
 			eventBcomprehension.setExpression(couple);
-
 			AMemberPredicate member = new AMemberPredicate();
-			if (ids2.size() > 1) {
-				ACoupleExpression couple2 = new ACoupleExpression();
-				couple2.setList(ids2);
-				member.setLeft(couple2);
-			} else {
+			AComprehensionSetExpression compre = new AComprehensionSetExpression();
+			eventBcomprehension.setIdentifiers(ids);
+			if (ids.size() == 1) {
 				member.setLeft(ids2.get(0));
+			} else {
+				ACoupleExpression couple2 = new ACoupleExpression(ids2);
+				member.setLeft(couple2);
 			}
-
-			AComprehensionSetExpression compre = new AComprehensionSetExpression();
 			compre.setIdentifiers(ids3);
 			compre.setPredicates(node.getPredicates());
 			member.setRight(compre);
-			eventBcomprehension.setPredicates(member);
 
+			eventBcomprehension.setPredicates(member);
 			node.replaceBy(eventBcomprehension);
+			// eventBcomprehension.apply(this);
+		}
+
+	}
 
-			eventBcomprehension.apply(this);
+	/**
+	 * This method collects all {@link ADomainExpression} which are direct
+	 * parents of the the set comprehension. For example the set comprehension
+	 * in k = dom(dom({a,b,c| ..}) has 2 preceding dom expression. All preceding
+	 * dom expression nodes are collected in the parameter domExprList.
+	 * 
+	 * @param node
+	 * @return
+	 */
+
+	private ArrayList<ADomainExpression> collectParentDomainExpression(Node node) {
+		if (node instanceof ADomainExpression) {
+			ArrayList<ADomainExpression> domExprList = collectParentDomainExpression(node
+					.parent());
+			domExprList.set(0, (ADomainExpression) node); // prepend the node
+			return domExprList;
+		} else {
+			return new ArrayList<ADomainExpression>();
 		}
 
 	}
 
+	private void setSourcePosition(AComprehensionSetExpression from,
+			AEventBComprehensionSetExpression to) {
+		to.setStartPos(from.getStartPos());
+		to.setEndPos(from.getEndPos());
+	}
+
 	private void analysePredicate(PPredicate predicate, ArrayList<String> list,
 			Hashtable<String, PExpression> values,
 			ArrayList<AEqualPredicate> equalList) {
@@ -172,16 +186,10 @@ public class SetComprehensionOptimizer extends DepthFirstAdapter {
 				AIdentifierExpression id = (AIdentifierExpression) equal
 						.getLeft();
 				String name = Utils.getIdentifierAsString(id.getIdentifier());
-				if (list.contains(name) && !values.containsKey(name)) {
-					if (equal.getRight() instanceof AIdentifierExpression) {
-						AIdentifierExpression id2 = (AIdentifierExpression) equal
-								.getRight();
-						String name2 = Utils.getIdentifierAsString(id2
-								.getIdentifier());
-						if (values.containsKey(name2)){
-							return;
-						}
-					}
+
+				if (list.contains(name)
+						&& !DependenciesDetector.expressionContainsIdentifier(
+								equal.getRight(), values.keySet())) {
 					equalList.add(equal);
 					values.put(name, equal.getRight());
 				}
@@ -190,21 +198,42 @@ public class SetComprehensionOptimizer extends DepthFirstAdapter {
 				AIdentifierExpression id = (AIdentifierExpression) equal
 						.getRight();
 				String name = Utils.getIdentifierAsString(id.getIdentifier());
-				if (list.contains(name) && !values.containsKey(name)) {
-					if (equal.getLeft() instanceof AIdentifierExpression) {
-						AIdentifierExpression id2 = (AIdentifierExpression) equal
-								.getLeft();
-						String name2 = Utils.getIdentifierAsString(id2
-								.getIdentifier());
-						if (values.contains(name2))
-							return;
-					}
+				if (list.contains(name)
+						&& !DependenciesDetector.expressionContainsIdentifier(
+								equal.getLeft(), values.keySet())) {
 					equalList.add(equal);
 					values.put(name, equal.getLeft());
 				}
 			}
 
 		}
+
+	}
+
+	static class DependenciesDetector extends DepthFirstAdapter {
+		private final Set<String> names;
+		private boolean hasDependency = false;
+
+		private DependenciesDetector(Set<String> names) {
+			this.names = names;
+		}
+
+		@Override
+		public void caseAIdentifierExpression(AIdentifierExpression node) {
+			String name = Utils.getIdentifierAsString(node.getIdentifier());
+			if (names.contains(name)) {
+				hasDependency = true;
+			}
+		}
+
+		static boolean expressionContainsIdentifier(PExpression node,
+				Set<String> names) {
+			DependenciesDetector dependenciesDetector = new DependenciesDetector(
+					names);
+			node.apply(dependenciesDetector);
+			return dependenciesDetector.hasDependency;
+		}
+
 	}
 
 	class NodesRemover extends DepthFirstAdapter {
diff --git a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
index fce8f8737b857ee8df52fbd4913d5d7747082458..22c1f092d7f58bc24a2b507d8a7441509d644d60 100644
--- a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
+++ b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
@@ -10,6 +10,7 @@ import java.util.Set;
 import de.be4.classicalb.core.parser.Utils;
 import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
 import de.be4.classicalb.core.parser.node.AAnySubstitution;
+import de.be4.classicalb.core.parser.node.AAssertionsMachineClause;
 import de.be4.classicalb.core.parser.node.ABecomesSuchSubstitution;
 import de.be4.classicalb.core.parser.node.AComprehensionSetExpression;
 import de.be4.classicalb.core.parser.node.AConjunctPredicate;
@@ -45,6 +46,7 @@ import de.be4.classicalb.core.parser.node.PPredicate;
 import de.be4.classicalb.core.parser.node.Start;
 import de.be4.ltl.core.parser.node.AExistsLtl;
 import de.be4.ltl.core.parser.node.AForallLtl;
+import de.tlc4b.TLC4BGlobals;
 import de.tlc4b.analysis.MachineContext;
 import de.tlc4b.analysis.Typechecker;
 import de.tlc4b.btypes.BType;
@@ -162,7 +164,8 @@ public class TypeRestrictor extends DepthFirstAdapter {
 		for (Node param : list) {
 			set.add((PExpression) param);
 		}
-		createRestrictedTypeofLocalVariables(new HashSet<PExpression>(set), false);
+		createRestrictedTypeofLocalVariables(new HashSet<PExpression>(set),
+				false);
 	}
 
 	@Override
@@ -175,7 +178,8 @@ public class TypeRestrictor extends DepthFirstAdapter {
 		for (Node con : machineContext.getConstants().values()) {
 			set.add((PExpression) con);
 		}
-		createRestrictedTypeofLocalVariables(new HashSet<PExpression>(set), false);
+		createRestrictedTypeofLocalVariables(new HashSet<PExpression>(set),
+				false);
 	}
 
 	public void analyseDisjunktionPredicate(PPredicate node, HashSet<Node> list) {
@@ -190,7 +194,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
 
 	private void analysePredicate(Node n, HashSet<Node> list,
 			HashSet<Node> ignoreList) {
-		
+
 		if (removedNodes.contains(n))
 			return;
 
@@ -223,22 +227,22 @@ public class TypeRestrictor extends DepthFirstAdapter {
 				removedNodes.add(n);
 			}
 			// detecting couples, e.g. (a,b) = (1,3)
-//			if (left instanceof ACoupleExpression) {
-//				ACoupleExpression couple = (ACoupleExpression) left;
-//				PExpression first = couple.getList().get(0);
-//				Node r_first = machineContext.getReferenceNode(first);
-//				PExpression second = couple.getList().get(0);
-//				Node r_second = machineContext.getReferenceNode(second);
-//
-//				if (list.contains(r_first) && list.contains(r_second)
-//						&& isAConstantExpression(right, list, ignoreList)) {
-//					ArrayList<PExpression> element = new ArrayList<PExpression>();
-//					element.add(right);
-//					putRestrictedTypeOfTuple(r_right,
-//							new ASetExtensionExpression(element));
-//					removedNodes.add(n);
-//				}
-//			}
+			// if (left instanceof ACoupleExpression) {
+			// ACoupleExpression couple = (ACoupleExpression) left;
+			// PExpression first = couple.getList().get(0);
+			// Node r_first = machineContext.getReferenceNode(first);
+			// PExpression second = couple.getList().get(0);
+			// Node r_second = machineContext.getReferenceNode(second);
+			//
+			// if (list.contains(r_first) && list.contains(r_second)
+			// && isAConstantExpression(right, list, ignoreList)) {
+			// ArrayList<PExpression> element = new ArrayList<PExpression>();
+			// element.add(right);
+			// putRestrictedTypeOfTuple(r_right,
+			// new ASetExtensionExpression(element));
+			// removedNodes.add(n);
+			// }
+			// }
 
 			return;
 		}
@@ -343,8 +347,8 @@ public class TypeRestrictor extends DepthFirstAdapter {
 		AImplicationPredicate implication = (AImplicationPredicate) node
 				.getImplication();
 		analysePredicate(implication.getLeft(), list, new HashSet<Node>());
-		createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
-				node.getIdentifiers()), false);
+		createRestrictedTypeofLocalVariables(
+				new HashSet<PExpression>(node.getIdentifiers()), false);
 	}
 
 	@Override
@@ -356,8 +360,8 @@ public class TypeRestrictor extends DepthFirstAdapter {
 			list.add(e);
 		}
 		analysePredicate(node.getPredicate(), list, new HashSet<Node>());
-		createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
-				node.getIdentifiers()), false);
+		createRestrictedTypeofLocalVariables(
+				new HashSet<PExpression>(node.getIdentifiers()), false);
 	}
 
 	@Override
@@ -369,8 +373,8 @@ public class TypeRestrictor extends DepthFirstAdapter {
 			list.add(e);
 		}
 		analysePredicate(node.getPredicates(), list, new HashSet<Node>());
-		createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
-				node.getIdentifiers()), false);
+		createRestrictedTypeofLocalVariables(
+				new HashSet<PExpression>(node.getIdentifiers()), false);
 	}
 
 	@Override
@@ -383,8 +387,8 @@ public class TypeRestrictor extends DepthFirstAdapter {
 			list.add(e);
 		}
 		analysePredicate(node.getPredicates(), list, new HashSet<Node>());
-		createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
-				node.getIdentifiers()), false);
+		createRestrictedTypeofLocalVariables(
+				new HashSet<PExpression>(node.getIdentifiers()), false);
 	}
 
 	@Override
@@ -396,8 +400,8 @@ public class TypeRestrictor extends DepthFirstAdapter {
 			list.add(e);
 		}
 		analysePredicate(node.getPredicates(), list, new HashSet<Node>());
-		createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
-				node.getIdentifiers()), false);
+		createRestrictedTypeofLocalVariables(
+				new HashSet<PExpression>(node.getIdentifiers()), false);
 	}
 
 	@Override
@@ -409,8 +413,8 @@ public class TypeRestrictor extends DepthFirstAdapter {
 			list.add(e);
 		}
 		analysePredicate(node.getPredicate(), list, new HashSet<Node>());
-		createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
-				node.getIdentifiers()), false);
+		createRestrictedTypeofLocalVariables(
+				new HashSet<PExpression>(node.getIdentifiers()), false);
 	}
 
 	public void inAGeneralSumExpression(AGeneralSumExpression node) {
@@ -421,8 +425,8 @@ public class TypeRestrictor extends DepthFirstAdapter {
 			list.add(e);
 		}
 		analysePredicate(node.getPredicates(), list, new HashSet<Node>());
-		createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
-				node.getIdentifiers()), false);
+		createRestrictedTypeofLocalVariables(
+				new HashSet<PExpression>(node.getIdentifiers()), false);
 	}
 
 	public void inAGeneralProductExpression(AGeneralProductExpression node) {
@@ -433,8 +437,8 @@ public class TypeRestrictor extends DepthFirstAdapter {
 			list.add(e);
 		}
 		analysePredicate(node.getPredicates(), list, new HashSet<Node>());
-		createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
-				node.getIdentifiers()), false);
+		createRestrictedTypeofLocalVariables(
+				new HashSet<PExpression>(node.getIdentifiers()), false);
 	}
 
 	private Hashtable<Node, HashSet<PExpression>> expectedIdentifieListTable = new Hashtable<Node, HashSet<PExpression>>();
@@ -493,8 +497,8 @@ public class TypeRestrictor extends DepthFirstAdapter {
 		}
 		list.addAll(getExpectedIdentifier(node));
 		analysePredicate(node.getWhere(), list, new HashSet<Node>());
-		createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
-				node.getIdentifiers()), false);
+		createRestrictedTypeofLocalVariables(
+				new HashSet<PExpression>(node.getIdentifiers()), false);
 	}
 
 	@Override
@@ -507,8 +511,8 @@ public class TypeRestrictor extends DepthFirstAdapter {
 		}
 		list.addAll(getExpectedIdentifier(node));
 		analysePredicate(node.getPredicate(), list, new HashSet<Node>());
-		createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
-				node.getIdentifiers()), false);
+		createRestrictedTypeofLocalVariables(
+				new HashSet<PExpression>(node.getIdentifiers()), false);
 	}
 
 	private Hashtable<Node, Node> variablesHashTable;
@@ -527,15 +531,18 @@ public class TypeRestrictor extends DepthFirstAdapter {
 				variablesHashTable.put(ref, e);
 			}
 			analysePredicate(node.getPredicate(), list, new HashSet<Node>());
-			createRestrictedTypeofLocalVariables(new HashSet<PExpression>(copy), false);
+			createRestrictedTypeofLocalVariables(
+					new HashSet<PExpression>(copy), false);
 		}
 	}
 
-	private void createRestrictedTypeofLocalVariables(Set<PExpression> copy, boolean constant) {
-		//TODO if constant is true, only constant expressions should be used to restrict the type.
-		//This is required by the TLC model checker when checking an LTL formula.
-		
-		
+	private void createRestrictedTypeofLocalVariables(Set<PExpression> copy,
+			boolean constant) {
+		// TODO if constant is true, only constant expressions should be used to
+		// restrict the type.
+		// This is required by the TLC model checker when checking an LTL
+		// formula.
+
 		for (PExpression e : copy) {
 			PExpression tree = null;
 			ArrayList<Node> restrictedList = restrictedNodeTable.get(e);
@@ -579,6 +586,17 @@ public class TypeRestrictor extends DepthFirstAdapter {
 		}
 	}
 
+	@Override
+	public void caseAAssertionsMachineClause(AAssertionsMachineClause node) {
+		if (TLC4BGlobals.isAssertion()) {
+			List<PPredicate> copy = new ArrayList<PPredicate>(
+					node.getPredicates());
+			for (PPredicate e : copy) {
+				e.apply(this);
+			}
+		}
+	}
+
 	public void addRemoveNode(Node node) {
 		this.removedNodes.add(node);
 	}
diff --git a/src/main/java/de/tlc4b/util/UtilMethods.java b/src/main/java/de/tlc4b/util/UtilMethods.java
new file mode 100644
index 0000000000000000000000000000000000000000..822c4696c748bbdfe656f0ec5e260d0a2af4307d
--- /dev/null
+++ b/src/main/java/de/tlc4b/util/UtilMethods.java
@@ -0,0 +1,18 @@
+package de.tlc4b.util;
+
+import java.util.ArrayList;
+
+import de.be4.classicalb.core.parser.node.AIdentifierExpression;
+import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
+
+public class UtilMethods {
+
+	public static AIdentifierExpression createAIdentifierExpression(String name) {
+		TIdentifierLiteral literal = new TIdentifierLiteral(name);
+		ArrayList<TIdentifierLiteral> idList = new ArrayList<TIdentifierLiteral>();
+		idList.add(literal);
+		AIdentifierExpression id = new AIdentifierExpression(idList);
+		return id;
+	}
+	
+}
diff --git a/src/test/java/de/tlc4b/analysis/SetComprehensionOptimizerTest.java b/src/test/java/de/tlc4b/analysis/SetComprehensionOptimizerTest.java
index d433d16336656001e289cb83c27c71ccefbce8f5..fd97378d87bfebf1053080b4906985bb9daa5444 100644
--- a/src/test/java/de/tlc4b/analysis/SetComprehensionOptimizerTest.java
+++ b/src/test/java/de/tlc4b/analysis/SetComprehensionOptimizerTest.java
@@ -9,23 +9,69 @@ public class SetComprehensionOptimizerTest {
 	@Test
 	public void testSetComprehension1() throws Exception {
 		String machine = "MACHINE test\n"
-				+ "CONSTANTS k \n"
-				+ "PROPERTIES k = {x,y | x : 1..10 & y = x + 1} \n" + "END";
+				+ "PROPERTIES {x,y | x : 1..10 & y = x + 1} /= {} \n" + "END";
 		String expected = "---- MODULE test----\n" 
 				+ "EXTENDS Naturals\n"
-				+ "k == {<<x, x + 1>>: x \\in {x \\in ((1 .. 10)): TRUE}} \n"
+				+ "ASSUME {<<x, x + 1>>: x \\in {x \\in ((1 .. 10)): TRUE}} # {} \n"
 				+ "======";
 		compare(expected, machine);
 	}
 	
+	/**
+	 * The type restrictor will simplify the expression.
+	 * @throws Exception
+	 */
 	@Test
-	public void testSetComprehension2() throws Exception {
+	public void testNotOptimized() throws Exception {
 		String machine = "MACHINE test\n"
-				+ "CONSTANTS k \n"
-				+ "PROPERTIES k = {x,y|  x : 1..10 & x = y & y = x} \n" + "END";
+				+ "PROPERTIES {x,y | x = 1 & y = 2} /= {} \n" + "END";
+		String expected = "---- MODULE test----\n" 
+				+ "ASSUME {<<x, y>> \\in (({1}) \\times ({2})): TRUE} # {} \n"
+				+ "======";
+		compare(expected, machine);
+	}
+	
+	@Test
+	public void testSetComprehension3() throws Exception {
+		String machine = "MACHINE test\n"
+				+ "PROPERTIES {x,y|  x : 1..10 & x = y & y = x} /= {} \n" + "END";
 		String expected = "---- MODULE test----\n" 
 				+ "EXTENDS Naturals\n"
-				+ "k == {<<x, x + 1>>: x \\in {x \\in ((1 .. 10)): TRUE}} \n"
+				+ "ASSUME {<<y, y>>: y \\in {y \\in ((1 .. 10)): y = y}} # {} \n"
+				+ "======";
+		compare(expected, machine);
+	}
+	
+	@Test
+	public void testSetComprehension4() throws Exception {
+		String machine = "MACHINE test\n"
+				+ "PROPERTIES {x,y,c| c : {TRUE} & x : 1..2 & x = y+1 & y = x-1} /= {} \n" 
+				+ "END";
+		String expected = "---- MODULE test----\n" 
+				+ "EXTENDS Integers\n"
+				+ "ASSUME {<<<<y + 1, y>>, c>>: <<y, c>> \\in {<<y, c>> \\in ((Int) \\times ({TRUE})): y + 1 \\in (1 .. 2) /\\ y = (y + 1) - 1}} # {} \n"
+				+ "======";
+		compare(expected, machine);
+	}
+	
+	@Test
+	public void testSetComprehension5() throws Exception {
+		String machine = "MACHINE test\n"
+				+ "PROPERTIES {x,y| x : 1..2 & y : 1..100 & x = y} /= {} \n" + "END";
+		String expected = "---- MODULE test----\n" 
+				+ "EXTENDS Naturals\n"
+				+ "ASSUME {<<y, y>>: y \\in {y \\in ((1 .. 2) \\cap (1 .. 100)): TRUE}} # {} \n"
+				+ "======";
+		compare(expected, machine);
+	}
+	
+	@Test
+	public void testSetComprehension6() throws Exception {
+		String machine = "MACHINE test\n"
+				+ "PROPERTIES {a,b,c,d| a = b & b : {1} & c : {1} & d : {1}} /= {} \n" + "END";
+		String expected = "---- MODULE test----\n" 
+				+ "EXTENDS Integers\n"
+				+ "ASSUME {<<<<<<t_[1], t_[2]>>, t_[3]>>, t_[4]>>: t_ \\in {<<a, b, c, d>> \\in (Int) \\times ({1}) \\times ({1}) \\times ({1}): a = b}} # {} \n"
 				+ "======";
 		compare(expected, machine);
 	}
diff --git a/src/test/java/de/tlc4b/util/TestUtil.java b/src/test/java/de/tlc4b/util/TestUtil.java
index 24349b05707627582c0b4fa163cbfe28f6f0fbef..98c72910345f0544885f5199646a7defc6d3396a 100644
--- a/src/test/java/de/tlc4b/util/TestUtil.java
+++ b/src/test/java/de/tlc4b/util/TestUtil.java
@@ -31,16 +31,15 @@ public class TestUtil {
 		Translator b2tlaTranslator = new Translator(machine);
 		b2tlaTranslator.translate();
 		System.out.println(b2tlaTranslator.getModuleString());
-		/**
-		 * create standard modules BBuildins
-		 */
+		
+		//TODO  create standard modules BBuildins
+		 
 
 		String moduleName = b2tlaTranslator.getMachineName();
 		String str1 = translateTLA2B(moduleName,
 				b2tlaTranslator.getModuleString());
 
 		String str2 = translateTLA2B(moduleName, expectedModule);
-
 		// StringBuilder sb1 = de.tla2b.translation.Tla2BTranslator
 		// .translateString(name, b2tlaTranslator.getModuleString(), null);
 		// StringBuilder sb2 = de.tla2b.translation.Tla2BTranslator
diff --git a/src/test/java/testing/Testing.java b/src/test/java/testing/Testing.java
index cf4fe083d022b67c76aba76e714df63deacea7e8..1ab3f574a914e47edc92e757d40305c715098c42 100644
--- a/src/test/java/testing/Testing.java
+++ b/src/test/java/testing/Testing.java
@@ -30,15 +30,18 @@ public class Testing extends AbstractParseMachineTest{
 
 	@Test
 	public void testRunTLC() throws Exception {
-		String[] a = new String[] { machine.getPath()};
-		TLC4B.main(a);
-		//assertEquals(error, B2TLA.test(a,false));
+		if (!machine.getName().contains("Mch2")) {
+			return;
+		}
+		
+		String[] a = new String[] { machine.getPath() };
+		TLC4B.test(a, false);
 	}
 
 	@Config
 	public static Configuration getConfig() {
 		final ArrayList<TestPair> list = new ArrayList<TestPair>();
-		list.add(new TestPair(NoError, "./src/test/resources/Testing"));
+		list.add(new TestPair(NoError, "/Users/hansen/git/thales/EngineeringRules-Generic/"));
 		return getConfiguration(list);
 	}
 }