Fixed some bugs handling tuples

src/main/java/de/tla2b/analysis/AbstractASTVisitor.java

@@ -117,7 +117,7 @@ public class AbstractASTVisitor extends BuiltInOPs implements ASTConstants {
 
 	}
 
-	private void visitBBuiltinsNode(OpApplNode n) {
+	public void visitBBuiltinsNode(OpApplNode n) {
 		ExprNode[] in = n.getBdedQuantBounds();
 		for (ExprNode exprNode : in) {
 			visitExprNode(exprNode);

src/main/java/de/tla2b/analysis/BOperation.java

@@ -83,7 +83,7 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
 		}
 		for (int j = 0; j < this.getExistQuans().size(); j++) {
 			OpApplNode o = this.getExistQuans().get(j);
-			whereList.add(bASTCreator.visitBounded(o));
+			whereList.add(bASTCreator.visitBoundsOfLocalVariables(o));
 		}
 
 		operation.setOpName(BAstCreator.createTIdentifierLiteral(name));

src/main/java/de/tla2b/analysis/SpecAnalyser.java

@@ -109,6 +109,9 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 		specAnalyser.spec = definitions.get("Spec");
 		specAnalyser.init = definitions.get("Init");
 		specAnalyser.next = definitions.get("Next");
+		if(definitions.containsKey("Inv")){
+			specAnalyser.invariants.add(definitions.get("Inv"));
+		}
 		// TODO are constant in the right order
 
 		specAnalyser.bConstants.addAll(Arrays.asList(m.getConstantDecls()));

src/main/java/de/tla2b/analysis/TypeChecker.java

@@ -36,6 +36,7 @@ import tla2sany.semantic.NumeralNode;
 import tla2sany.semantic.OpApplNode;
 import tla2sany.semantic.OpDeclNode;
 import tla2sany.semantic.OpDefNode;
+import tla2sany.semantic.SemanticNode;
 import tla2sany.semantic.StringNode;
 import tla2sany.semantic.SymbolNode;
 import tlc2.tool.BuiltInOPs;
@@ -50,8 +51,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 	private ExprNode nextExpr;
 	private Set<OpDefNode> usedDefinitions;
 
-	private ArrayList<OpApplNode> recList = new ArrayList<OpApplNode>();
-	// every record node [a |-> 1 .. ] will be added to this List
+	private ArrayList<SymbolNode> symbolNodeList = new ArrayList<SymbolNode>();
+	private ArrayList<SemanticNode> tupleNodeList = new ArrayList<SemanticNode>();
+
 	private ModuleNode moduleNode;
 	private ArrayList<OpDeclNode> bConstList;
 	private SpecAnalyser specAnalyser;
@@ -158,7 +160,13 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 			visitExprNode(nextExpr, BoolType.getInstance());
 		}
 
+		checkIfAllIdentifiersHaveAType();
+
+	}
+
+	private void checkIfAllIdentifiersHaveAType() throws TypeErrorException {
 		// check if a variable has no type
+		OpDeclNode[] vars = moduleNode.getVariableDecls();
 		for (int i = 0; i < vars.length; i++) {
 			OpDeclNode var = vars[i];
 			TLAType varType = (TLAType) var.getToolObject(TYPE_ID);
@@ -170,6 +178,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 
 		// check if a constant has no type, only constants which will appear in
 		// the resulting B Machine are considered
+		OpDeclNode[] cons = moduleNode.getConstantDecls();
 		for (int i = 0; i < cons.length; i++) {
 			OpDeclNode con = cons[i];
 			if (bConstList == null || bConstList.contains(con)) {
@@ -181,30 +190,19 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 			}
 		}
 
-		evalRecList();
+		for (SymbolNode symbol : symbolNodeList) {
+			TLAType type = (TLAType) symbol.getToolObject(TYPE_ID);
+			if (type.isUntyped()) {
+				throw new TypeErrorException("Symbol '" + symbol.getName()
+						+ "' has no type.\n" + symbol.getLocation());
 			}
-
-	/**
-	 * 
-	 */
-	private void evalRecList() {
-		for (int i = 0; i < recList.size(); i++) {
-			OpApplNode n = recList.get(i);
-			StructType struct = (StructType) n.getToolObject(TYPE_ID);
-			ArrayList<String> fieldNames = new ArrayList<String>();
-			ExprOrOpArgNode[] args = n.getArgs();
-			for (int j = 0; j < args.length; j++) {
-				OpApplNode pair = (OpApplNode) args[j];
-				StringNode stringNode = (StringNode) pair.getArgs()[0];
-				fieldNames.add(stringNode.getRep().toString());
-			}
-			for (int j = 0; j < struct.getFields().size(); j++) {
-				String fieldName = struct.getFields().get(j);
-				if (!fieldNames.contains(fieldName)
-						&& struct.getType(fieldName).getKind() == IType.MODELVALUE) {
-					EnumType e = (EnumType) struct.getType(fieldName);
-					e.setNoVal();
 		}
+
+		for (SemanticNode tuple : tupleNodeList) {
+			TLAType type = (TLAType) tuple.getToolObject(TYPE_ID);
+			if (type instanceof TupleOrFunction) {
+				TupleOrFunction tOrF = (TupleOrFunction) type;
+				tOrF.getFinalType();
 			}
 		}
 
@@ -423,6 +421,10 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 			if (t == null) {
 				t = (TLAType) symbolNode.getToolObject(TYPE_ID);
 			}
+			
+			if(t == null){
+				throw new RuntimeException();
+			}
 			try {
 				TLAType result = expected.unify(t);
 				symbolNode.setToolObject(paramId, result);
@@ -751,6 +753,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 						n.getLocation()));
 			}
 			n.setToolObject(TYPE_ID, found);
+			tupleNodeList.add(n);
 			if (found instanceof AbstractHasFollowers) {
 				((AbstractHasFollowers) found).addFollower(n);
 			}
@@ -765,6 +768,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 		{
 
 			FormalParamNode recFunc = n.getUnbdedQuantSymbols()[0];
+			symbolNodeList.add(recFunc);
 			FunctionType recType = new FunctionType();
 			recFunc.setToolObject(TYPE_ID, recType);
 			recType.addFollower(recFunc);
@@ -825,10 +829,19 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 							new UntypedType());
 					domList.add(d);
 				}
+
+				if (domList.size() == 1) { // one-tuple
+					domType = new FunctionType(IntType.getInstance(),
+							domList.get(0));
+					FunctionType func = new FunctionType(domType, expected);
+					TLAType res = visitExprOrOpArgNode(n.getArgs()[0], func);
+					return ((FunctionType) res).getRange();
+				} else {
 					domType = new TupleType(domList);
 					FunctionType func = new FunctionType(domType, expected);
 					TLAType res = visitExprOrOpArgNode(n.getArgs()[0], func);
 					return ((FunctionType) res).getRange();
+				}
 			} else {
 				ExprOrOpArgNode arg = n.getArgs()[1];
 				if (arg instanceof NumeralNode) {
@@ -838,10 +851,14 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 					u.addFollower(n);
 					TupleOrFunction tupleOrFunc = new TupleOrFunction(
 							num.val(), u);
-					TLAType funcOrTuple = visitExprOrOpArgNode(n.getArgs()[0], tupleOrFunc);
+
+					TLAType funcOrTuple = visitExprOrOpArgNode(n.getArgs()[0],
+							tupleOrFunc);
 					n.getArgs()[0].setToolObject(TYPE_ID, funcOrTuple);
+					tupleNodeList.add(n.getArgs()[0]);
 					if (funcOrTuple instanceof AbstractHasFollowers) {
-						((AbstractHasFollowers) funcOrTuple).addFollower(n.getArgs()[0]);
+						((AbstractHasFollowers) funcOrTuple).addFollower(n
+								.getArgs()[0]);
 					}
 
 					TLAType found = (TLAType) n.getToolObject(TYPE_ID);
@@ -849,7 +866,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 						found = found.unify(expected);
 					} catch (UnificationException e) {
 						throw new TypeErrorException("Expected '" + expected
-								+ "', found '" + found + "'.\n" + n.getLocation());
+								+ "', found '" + found + "'.\n"
+								+ n.getLocation());
 					}
 					return found;
 				}
@@ -905,7 +923,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 		/**********************************************************************
 		 * Except
 		 **********************************************************************/
-		case OPCODE_exc: // Except
+		case OPCODE_exc: // $Except
 		{
 			return evalExcept(n, expected);
 		}
@@ -980,7 +998,6 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 			n.setToolObject(TYPE_ID, found);
 			found.addFollower(n);
 
-			recList.add(n);
 			return found;
 
 		}
@@ -1002,8 +1019,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 						"Struct has no field %s with type %s: %s%n%s",
 						fieldName, r.getType(fieldName), r, n.getLocation()));
 			}
-			n.setToolObject(TYPE_ID, r);
-			r.addFollower(n);
+			n.getArgs()[0].setToolObject(TYPE_ID, r);
+			r.addFollower(n.getArgs()[0]);
 			return r.getType(fieldName);
 		}
 
@@ -1045,6 +1062,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 		case OPCODE_uc: {
 			TLAType found = new UntypedType();
 			FormalParamNode x = n.getUnbdedQuantSymbols()[0];
+			symbolNodeList.add(x);
 			x.setToolObject(TYPE_ID, found);
 			((AbstractHasFollowers) found).addFollower(x);
 			visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
@@ -1079,6 +1097,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 						found, n.getLocation()));
 			}
 			FormalParamNode x = n.getBdedQuantSymbolLists()[0][0];
+			symbolNodeList.add(x);
 			x.setToolObject(TYPE_ID, found);
 			if (found instanceof AbstractHasFollowers) {
 				((AbstractHasFollowers) found).addFollower(x);
@@ -1113,37 +1132,38 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 			TLAType subType = boundType.getSubType();
 
 			if (n.isBdedQuantATuple()[i]) {
-				if (subType instanceof TupleType) {
-					domList.add(subType);
-					TupleType t = (TupleType) subType;
-					if (params[i].length != t.getTypes().size()) {
-						throw new TypeErrorException("Expected tuple with "
-								+ params[i].length
-								+ " components, found tuple with "
-								+ t.getTypes().size() + " components.\n"
-								+ bounds[i].getLocation());
-					}
-					for (int j = 0; j < params[i].length; j++) {
-						FormalParamNode p = params[i][j];
-						TLAType paramType = t.getTypes().get(j);
-						p.setToolObject(TYPE_ID, paramType);
-						if (paramType instanceof AbstractHasFollowers) {
-							((AbstractHasFollowers) paramType).addFollower(p);
+				if (params[i].length == 1) {
+					FormalParamNode p = params[i][0];
+					FunctionType expected = new FunctionType(
+							IntType.getInstance(), new UntypedType());
+					try {
+						expected = expected.unify(subType);
+					} catch (UnificationException e) {
+						throw new TypeErrorException(String.format(
+								"Expected %s, found %s at parameter %s,%n%s",
+								expected, subType, p.getName().toString(),
+								bounds[i].getLocation()));
 					}
+					domList.add(expected);
+					symbolNodeList.add(p);
+					p.setToolObject(TYPE_ID, expected.getRange());
+					if (expected.getRange() instanceof AbstractHasFollowers) {
+						((AbstractHasFollowers) expected.getRange())
+								.addFollower(p);
 					}
-				} else if (subType instanceof UntypedType) {
+				} else {
 					TupleType tuple = new TupleType(params[i].length);
 					try {
 						tuple = (TupleType) tuple.unify(subType);
 					} catch (UnificationException e) {
 						throw new TypeErrorException(String.format(
-								"Expected %s, found %s ,%n%s", tuple, subType,
-								n.getLocation()));
+								"Expected %s, found %s at tuple,%n%s", tuple,
+								subType, bounds[i].getLocation()));
 					}
-
 					domList.add(tuple);
 					for (int j = 0; j < params[i].length; j++) {
 						FormalParamNode p = params[i][j];
+						symbolNodeList.add(p);
 						TLAType paramType = tuple.getTypes().get(j);
 						p.setToolObject(TYPE_ID, paramType);
 						if (paramType instanceof AbstractHasFollowers) {
@@ -1151,15 +1171,14 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 						}
 					}
 
-				} else {
-					throw new TypeErrorException("Expected tuple, found '"
-							+ subType + "'.\n" + bounds[i].getLocation());
 				}
+
 			} else {
 				// is not a tuple: all parameter have the same type
 				for (int j = 0; j < params[i].length; j++) {
 					domList.add(subType);
 					FormalParamNode p = params[i][j];
+					symbolNodeList.add(p);
 					p.setToolObject(TYPE_ID, subType);
 					if (subType instanceof AbstractHasFollowers) {
 						((AbstractHasFollowers) subType).addFollower(p);
@@ -1236,6 +1255,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 						domList.add(d);
 					}
 					domType = new TupleType(domList);
+					domExpr.setToolObject(TYPE_ID, domType); // store type
 				} else {
 					domType = visitExprOrOpArgNode(domExpr, new UntypedType());
 				}
@@ -1635,6 +1655,17 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 								.getOperator().getName(), n.getLocation()));
 			}
 
+		case B_OPCODE_assert: {
+			try {
+				BoolType.getInstance().unify(expected);
+				return BoolType.getInstance();
+			} catch (Exception e) {
+				throw new TypeErrorException(String.format(
+						"Expected %s, found BOOL at '%s',%n%s", expected, n
+								.getOperator().getName(), n.getLocation()));
+			}
+		}
+
 		default: {
 			throw new NotImplementedException(n.getOperator().getName()
 					.toString());

src/main/java/de/tla2b/analysis/UsedExternalFunctions.java

@@ -3,16 +3,18 @@ package de.tla2b.analysis;
 import java.util.HashSet;
 import java.util.Set;
 
+import de.tla2b.global.BBuildIns;
+import de.tla2b.global.BBuiltInOPs;
 import tla2sany.semantic.ExprNode;
 import tla2sany.semantic.ExprOrOpArgNode;
 import tla2sany.semantic.ModuleNode;
 import tla2sany.semantic.OpApplNode;
 import tla2sany.semantic.OpDefNode;
 
-public class UsedExternalFunctions extends AbstractASTVisitor {
+public class UsedExternalFunctions extends AbstractASTVisitor implements BBuildIns{
 
 	public enum EXTERNAL_FUNCTIONS {
-		CHOOSE
+		CHOOSE, ASSERT
 	}
 
 	private final Set<EXTERNAL_FUNCTIONS> usedExternalFunctions;
@@ -58,4 +60,25 @@ public class UsedExternalFunctions extends AbstractASTVisitor {
 		}
 	}
 	
+	@Override
+	public void visitBBuiltinsNode(OpApplNode n) {
+		switch (BBuiltInOPs.getOpcode(n.getOperator().getName())) {
+		
+		case B_OPCODE_assert: {
+			usedExternalFunctions.add(EXTERNAL_FUNCTIONS.ASSERT);
+		}
+		}
+		
+		
+		ExprNode[] in = n.getBdedQuantBounds();
+		for (ExprNode exprNode : in) {
+			visitExprNode(exprNode);
+		}
+
+		ExprOrOpArgNode[] arguments = n.getArgs();
+		for (ExprOrOpArgNode exprOrOpArgNode : arguments) {
+			visitExprOrOpArgNode(exprOrOpArgNode);
+		}
+	}
+
 }

src/main/java/de/tla2b/global/BBuildIns.java

@@ -81,6 +81,10 @@ public interface BBuildIns {
 	public static final UniqueString OP_rel_inverse = UniqueString
 			.uniqueStringOf("rel_inverse");
 	
+	//TLC
+	public static final UniqueString OP_assert = UniqueString
+	.uniqueStringOf("Assert");
+	
 	public static final int B_OPCODE_dotdot = 1;
 	public static final int B_OPCODE_plus = 2;
 	public static final int B_OPCODE_minus = 3;
@@ -123,4 +127,6 @@ public interface BBuildIns {
 	
 	
 	public static final int B_OPCODE_rel_inverse = B_OPCODE_pow1 + 1;
+	
+	public static final int B_OPCODE_assert = B_OPCODE_rel_inverse + 1;
 }

src/main/java/de/tla2b/global/BBuiltInOPs.java

@@ -51,7 +51,7 @@ public class BBuiltInOPs implements BBuildIns{
 		//relations
 		B_Opcode_Table.put(OP_rel_inverse, B_OPCODE_rel_inverse);
 		
-		
+		B_Opcode_Table.put(OP_assert, B_OPCODE_assert);
 	}
 	
 	public static boolean contains(UniqueString s){

src/main/java/de/tla2b/global/TranslationGlobals.java

@@ -20,10 +20,12 @@ public interface TranslationGlobals {
 	final int DEF_OBJECT = 19;
 	final int PRINT_DEFINITION = 11;
 	final int TYPE_ID = 5;
+	final int EXCEPT_BASE = 6;
 	final int LET_PARAMS_ID = 13;
 	final int NEW_NAME = 20;
 	
 	final int SUBSTITUTE_PARAM = 29;
+	final int TUPLE = 30;
 
 	final String CHOOSE = " CHOOSE(X) == \"a member of X\"; EXTERNAL_FUNCTION_CHOOSE(T) == (POW(T)-->T)";
 	final String IF_THEN_ELSE = " IF_THEN_ELSE(P, a, b) == (%t_.(t_ = TRUE & P = TRUE | a )\\/%t_.(t_= TRUE & not(P= TRUE) | b ))(TRUE)";

src/main/java/de/tla2b/output/ASTPrettyPrinter.java

@@ -9,6 +9,7 @@ import de.be4.classicalb.core.parser.analysis.ExtendedDFAdapter;
 import de.be4.classicalb.core.parser.node.AAbstractMachineParseUnit;
 import de.be4.classicalb.core.parser.node.AAnySubstitution;
 import de.be4.classicalb.core.parser.node.ABecomesSuchSubstitution;
+import de.be4.classicalb.core.parser.node.AConjunctPredicate;
 import de.be4.classicalb.core.parser.node.ADefinitionExpression;
 import de.be4.classicalb.core.parser.node.ADefinitionPredicate;
 import de.be4.classicalb.core.parser.node.AExpressionDefinitionDefinition;
@@ -33,6 +34,7 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
 	private final StringBuilder builder = new StringBuilder();
 	private final StringBuilder sb = new StringBuilder();
 	private Renamer renamer;
+	private final Indentation indentation;
 
 	private static final int no = 0;
 	private static final int left = 1;
@@ -41,11 +43,14 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
 
 	private final static Hashtable<String, NodeInfo> infoTable = new Hashtable<String, NodeInfo>();
 
-	public ASTPrettyPrinter(Renamer renamer) {
+	public ASTPrettyPrinter(Start start, Renamer renamer) {
 		this.renamer = renamer;
+		
+		this.indentation = new Indentation(start);
 	}
 
-	public ASTPrettyPrinter() {
+	public ASTPrettyPrinter(Start start) {
+		this.indentation = new Indentation(start);
 	}
 
 	private static void putInfixOperator(String nodeName, String symbol,
@@ -251,7 +256,6 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
 
 	@Override
 	public void defaultIn(final Node node) {
-		super.defaultIn(node);
 		if (makeBrackets(node)) {
 			sb.append("(");
 		}
@@ -260,6 +264,30 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
 		builder.append("(");
 	}
 	
+	@Override
+	public void defaultCase(final Node node) {
+		super.defaultCase(node);
+		if (node instanceof Token) {
+			builder.append(((Token) node).getText());
+
+			sb.append(((Token) node).getText());
+		} else {
+			builder.append(node.toString());
+			sb.append(node.toString());
+		}
+
+	}
+
+	@Override
+	public void defaultOut(final Node node) {
+		builder.append(")");
+		sb.append(getInfo(node).end);
+		if (makeBrackets(node)) {
+			sb.append(")");
+		}
+	}
+
+
 	private boolean makeBrackets(Node node) {
 		NodeInfo infoNode = getInfo(node);
 		Node parent = node.parent();
@@ -287,40 +315,15 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
 
 	}
 
-	@Override
-	public void defaultCase(final Node node) {
-		super.defaultCase(node);
-		if (node instanceof Token) {
-			builder.append(((Token) node).getText());
-
-			sb.append(((Token) node).getText());
-		} else {
-			builder.append(node.toString());
-			sb.append(node.toString());
-		}
-
-	}
-
-	@Override
-	public void defaultOut(final Node node) {
-		super.defaultOut(node);
-		builder.append(")");
-		sb.append(getInfo(node).end);
-		if (makeBrackets(node)) {
-			sb.append(")");
-		}
-	}
-
-	@Override
 	public void beginList(final Node parent) {
 		builder.append('[');
 		sb.append(getInfo(parent).beginList);
 	}
 
 	@Override
-	public void betweenListElements(final Node parent) {
+	public void betweenListElements(final Node node) {
 		builder.append(',');
-		sb.append(getInfo(parent).betweenListElements);
+		sb.append(getInfo(node).betweenListElements);
 	}
 
 	@Override
@@ -330,9 +333,12 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
 	}
 
 	@Override
-	public void betweenChildren(final Node parent) {
+	public void betweenChildren(final Node node) {
 		builder.append(',');
-		sb.append(getInfo(parent).betweenChildren);
+		if(indentation.printNewLineInTheMiddle(node)){
+			sb.append("\n");
+		}
+		sb.append(getInfo(node).betweenChildren);
 	}
 
 	@Override
@@ -622,6 +628,11 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
 		sb.append(")");
 	}
 	
+    public void inAConjunctPredicate(AConjunctPredicate node)
+    {
+    	super.inAConjunctPredicate(node);
+    }
+
 }
 
 class NodeInfo {
@@ -702,6 +713,7 @@ class NodeInfo {
 
 	}
 
+	
 	public NodeInfo(String pre, String beginList, String betweenListElements,
 			String endList, String betweenChildren, String end,
 			Integer precedence, Integer associative) {

src/main/java/de/tla2b/output/Indentation.java

+package de.tla2b.output;
+
+import java.util.HashSet;
+import java.util.Hashtable;
+
+import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
+import de.be4.classicalb.core.parser.node.AConjunctPredicate;
+import de.be4.classicalb.core.parser.node.APredicateDefinitionDefinition;
+import de.be4.classicalb.core.parser.node.APropertiesMachineClause;
+import de.be4.classicalb.core.parser.node.Node;
+import de.be4.classicalb.core.parser.node.Start;
+
+public class Indentation extends DepthFirstAdapter {
+
+	private Hashtable<Node, Integer> indentation = new Hashtable<Node, Integer>();
+	private HashSet<Node> newlineMiddle = new HashSet<Node>();
+
+	public Indentation(Start start) {
+		start.apply(this);
+	}
+
+	public void inAPropertiesMachineClause(APropertiesMachineClause node) {
+		indentation.put(node.getPredicates(), 0);
+	}
+
+	@Override
+	public void inAConjunctPredicate(AConjunctPredicate node) {
+		Integer indent = indentation.get(node);
+		if (indent != null) {
+			indentation.put(node.getLeft(), indent);
+			indentation.put(node.getRight(), indent);
+
+			newlineMiddle.add(node);
+
+		}
+	}
+
+    public void inAPredicateDefinitionDefinition(APredicateDefinitionDefinition node)
+    {
+    	indentation.put(node.getRhs(), 0);
+    }
+	
+	
+	public boolean printNewLineInTheMiddle(Node node) {
+		return newlineMiddle.contains(node);
+	}
+
+	public Integer getIndent(Node node) {
+		Integer res = indentation.get(node);
+		if (res == null) {
+			res = 0;
+		}
+		return res;
+	}
+}

src/main/java/de/tla2b/translation/OperationsFinder.java

@@ -102,7 +102,7 @@ public class OperationsFinder extends AbstractASTVisitor implements
 
 				for (int i = 0; i < n.getArgs().length; i++) {
 					exists = new ArrayList<OpApplNode>(oldExists);
-					currentName = oldName;
+					currentName = oldName + i;
 					visitExprOrOpArgNode(n.getArgs()[i]);
 				}
 				return;
@@ -114,7 +114,7 @@ public class OperationsFinder extends AbstractASTVisitor implements
 
 			for (int i = 0; i < n.getArgs().length; i++) {
 				exists = new ArrayList<OpApplNode>(oldExists);
-				currentName = oldName;
+				currentName = oldName+ i;
 				visitExprOrOpArgNode(n.getArgs()[i]);
 			}
 			return;

src/main/java/de/tla2b/types/TupleOrFunction.java

 package de.tla2b.types;
 
 import java.util.ArrayList;
-import java.util.Collections;
 import java.util.Iterator;
 import java.util.LinkedHashMap;
 import java.util.List;
 import java.util.Map.Entry;
 
 import de.be4.classicalb.core.parser.node.PExpression;
-import de.tla2b.exceptions.TypeErrorException;
 import de.tla2b.exceptions.UnificationException;
 import de.tla2b.output.TypeVisitorInterface;
 
@@ -28,13 +26,9 @@ public class TupleOrFunction extends AbstractHasFollowers {
 	}
 
 	public static TLAType createTupleOrFunctionType(List<TLAType> list) {
-		if (comparable(list)) {
 		TupleOrFunction tOrF = new TupleOrFunction();
 		tOrF.add(list);
-			return tOrF;
-		} else {
-			return new TupleType(list);
-		}
+		return tOrF.update();
 	}
 
 	public void add(List<TLAType> list) {
@@ -53,33 +47,11 @@ public class TupleOrFunction extends AbstractHasFollowers {
 
 	@Override
 	public String toString() {
-		FunctionType func = new FunctionType();
-		func.setDomain(IntType.getInstance());
-		func.setRange(new UntypedType());
-		FunctionType res;
-		try {
-			res = func.unify(this);
-			return res.toString();
-		} catch (UnificationException e) {
-			// tuple
-			boolean isTuple = true;
-			ArrayList<TLAType> typeList = new ArrayList<TLAType>();
-			for (int i = 1; i <= types.keySet().size(); i++) {
-				if (types.keySet().contains(i)) {
-					typeList.add(types.get(i));
-				} else {
-					isTuple = false;
-					break;
-				}
-			}
 
-			if (isTuple) {
-				return new TupleType(typeList).toString();
-			} else {
 		StringBuilder sb = new StringBuilder();
+		sb.append("TupleOrFunction");
 		sb.append("(");
-				for (Iterator<Integer> keys = types.keySet().iterator(); keys
-						.hasNext();) {
+		for (Iterator<Integer> keys = types.keySet().iterator(); keys.hasNext();) {
 			Integer key = keys.next();
 			sb.append(key);
 			sb.append(" : ").append(types.get(key));
@@ -87,11 +59,8 @@ public class TupleOrFunction extends AbstractHasFollowers {
 				sb.append(", ");
 		}
 		sb.append(")");
-				throw new RuntimeException("Type " + sb + "is incomplete");
-			}
-
-		}
-
+		return sb.toString();
+		// throw new RuntimeException("Type " + sb + "is incomplete");
 	}
 
 	@Override
@@ -187,18 +156,7 @@ public class TupleOrFunction extends AbstractHasFollowers {
 			return true;
 		}
 
-//		if (o instanceof TupleOrFunction) {
-//			TupleOrFunction t = (TupleOrFunction) o;
-//			for (Entry<Integer, TLAType> entry : types.entrySet()) {
-//				if (t.types.containsKey(entry.getKey())
-//						&& entry.getValue()
-//								.compare(t.types.get(entry.getKey()))) {
-//					return false;
-//				}
-//			}
-//		}
-		
-		// this type is not comparable with all other types
+		// this type is not comparable to all other types
 		return false;
 	}
 
@@ -225,6 +183,9 @@ public class TupleOrFunction extends AbstractHasFollowers {
 
 	@Override
 	public boolean isUntyped() {
+//		if (complete == false) {
+//			return true;
+//		}
 		for (TLAType type : types.values()) {
 			if (type.isUntyped())
 				return true;
@@ -274,7 +235,8 @@ public class TupleOrFunction extends AbstractHasFollowers {
 			List<TLAType> typeList = new ArrayList<TLAType>();
 			for (int i = 0; i < tupleType.getTypes().size(); i++) {
 				if (this.types.containsKey(i + 1)) {
-					TLAType res = tupleType.getTypes().get(i).unify(this.types.get(i+1));
+					TLAType res = tupleType.getTypes().get(i)
+							.unify(this.types.get(i + 1));
 					typeList.add(res);
 				} else {
 					typeList.add(tupleType.getTypes().get(i));
@@ -284,71 +246,61 @@ public class TupleOrFunction extends AbstractHasFollowers {
 			this.setFollowersTo(r);
 			tupleType.setFollowersTo(r);
 			return r;
-			
-//			int max = Collections.max(types.keySet());
-//			if (max <= tupleType.getTypes().size()) {
-//				for (Entry<Integer, TLAType> entry : this.types.entrySet()) {
-//					int index = entry.getKey();
-//					TLAType type = entry.getValue();
-//					if (type instanceof AbstractHasFollowers) {
-//						((AbstractHasFollowers) type).removeFollower(this);
-//					}
-//					TLAType elementOfTuple = tupleType.getTypes()
-//							.get(index - 1);
-//					elementOfTuple.unify(type);
-//				}
-//				return tupleType;
-//			} else {
-//				TLAType range = new UntypedType();
-//				for (TLAType type : types.values()) {
-//					if (type instanceof AbstractHasFollowers) {
-//						((AbstractHasFollowers) type).removeFollower(this);
-//					}
-//					range = range.unify(type);
-//				}
-//				FunctionType funcType = new FunctionType(IntType.getInstance(),
-//						range);
-//				return funcType.unify(tupleType);
-//			}
 		}
 
 		if (o instanceof TupleOrFunction) {
 			TupleOrFunction other = (TupleOrFunction) o;
-			if (isTupleOrFunction(this, other)) {
-				for (Integer i : this.types.keySet()) {
-					if (other.types.containsKey(i)) {
-						TLAType res = this.types.get(i).unify(
-								other.types.get(i));
-						if (res instanceof AbstractHasFollowers) {
+			for (Integer i : other.types.keySet()) {
+				if(this.types.containsKey(i)){
+					TLAType res = other.types.get(i).unify(this.types.get(i));
+					if(res instanceof AbstractHasFollowers)
 						((AbstractHasFollowers) res).addFollower(this);
-						}
 					this.types.put(i, res);
-					}
-				}
-				for (Integer i : other.types.keySet()) {
-					if (!this.types.containsKey(i)) {
+				}else{
 					TLAType res = other.types.get(i);
-						if (res instanceof AbstractHasFollowers) {
+					if(res instanceof AbstractHasFollowers)
 						((AbstractHasFollowers) res).addFollower(this);
-						}
 					this.types.put(i, res);
 				}
-				}
-				return this;
-			} else{
-				ArrayList<TLAType> list1 = new ArrayList<TLAType>();
-				for (int i = 1; i <= types.keySet().size(); i++) {
-						list1.add(types.get(i));
-				}
-				TupleType tuple1 = new TupleType(list1);
 				
-				ArrayList<TLAType> list2 = new ArrayList<TLAType>();
-				for (int i = 1; i <= other.types.keySet().size(); i++) {
-						list2.add(other.types.get(i));
-				}
-				TupleType tuple2 = new TupleType(list2);
-				return tuple1.unify(tuple2);
 			}
+			other.setFollowersTo(this);
+			return this;
+			//			if (isTupleOrFunction(this, other)) {
+//				for (Integer i : this.types.keySet()) {
+//					if (other.types.containsKey(i)) {
+//						TLAType res = this.types.get(i).unify(
+//								other.types.get(i));
+//						if (res instanceof AbstractHasFollowers) {
+//							((AbstractHasFollowers) res).addFollower(this);
+//						}
+//						this.types.put(i, res);
+//					}
+//				}
+//				for (Integer i : other.types.keySet()) {
+//					if (!this.types.containsKey(i)) {
+//						TLAType res = other.types.get(i);
+//						if (res instanceof AbstractHasFollowers) {
+//							((AbstractHasFollowers) res).addFollower(this);
+//						}
+//						this.types.put(i, res);
+//					}
+//				}
+//				return this;
+//			} else {
+//				ArrayList<TLAType> list1 = new ArrayList<TLAType>();
+//				for (int i = 1; i <= types.keySet().size(); i++) {
+//					list1.add(types.get(i));
+//				}
+//				TupleType tuple1 = new TupleType(list1);
+//
+//				ArrayList<TLAType> list2 = new ArrayList<TLAType>();
+//				for (int i = 1; i <= other.types.keySet().size(); i++) {
+//					list2.add(other.types.get(i));
+//				}
+//				TupleType tuple2 = new TupleType(list2);
+//				return tuple1.unify(tuple2);
+//			}
 
 		}
 
@@ -370,6 +322,62 @@ public class TupleOrFunction extends AbstractHasFollowers {
 
 	}
 
+	public TLAType getFinalType() {
+		List<TLAType> list = new ArrayList<TLAType>(this.types.values());
+
+		if (comparable(list)) {
+			FunctionType func = new FunctionType(IntType.getInstance(),
+					new UntypedType());
+			try {
+				func = func.unify(this);
+				this.setFollowersTo(func);
+				return func;
+			} catch (UnificationException e) {
+				throw new RuntimeException();
+			}
+		} else {
+			TupleType tuple = new TupleType(list);
+			this.setFollowersTo(tuple);
+			return tuple;
+		}
+
+	}
+
+	private TLAType update() {
+		List<TLAType> list = new ArrayList<TLAType>(this.types.values());
+		// if (allTyped(list) && comparable(list)) {
+		// FunctionType func = new FunctionType(IntType.getInstance(),
+		// new UntypedType());
+		// try {
+		// func = func.unify(this);
+		// this.setFollowersTo(func);
+		// return func;
+		// } catch (UnificationException e) {
+		// throw new RuntimeException();
+		// }
+		// } else
+		if (!comparable(list)) {
+			TupleType tuple = new TupleType(list);
+			this.setFollowersTo(tuple);
+			return tuple;
+
+			// boolean isTuple = true;
+			// ArrayList<TLAType> typeList = new ArrayList<TLAType>();
+			// for (int i = 1; i <= types.keySet().size(); i++) {
+			// if (types.keySet().contains(i)) {
+			// typeList.add(types.get(i));
+			// } else {
+			// isTuple = false;
+			// break;
+			// }
+			// }
+			//
+			// if (isTuple) {
+			// return new TupleType(typeList).toString();
+		}
+		return this;
+	}
+
 	private static boolean comparable(List<TLAType> typeList) {
 		for (int i = 0; i < typeList.size() - 1; i++) {
 			TLAType t1 = typeList.get(i);
@@ -382,4 +390,13 @@ public class TupleOrFunction extends AbstractHasFollowers {
 		return true;
 	}
 
+	private static boolean allTyped(List<TLAType> typeList) {
+		for (int i = 0; i < typeList.size(); i++) {
+			if (typeList.get(i).isUntyped()) {
+				return false;
+			}
+		}
+		return true;
+	}
+
 }

src/main/java/de/tla2b/types/TupleType.java

@@ -59,39 +59,15 @@ public class TupleType extends AbstractHasFollowers {
 		if (o instanceof TupleType) {
 			TupleType t = (TupleType) o;
 			if (this.types.size() != t.types.size()) {
-				for (int i = 0; i < t.types.size(); i++) {
-					if (!compareToAll(t.types.get(i))) {
 				return false;
 			}
-				}
-				// both are sequences with different lengths
-				return true;
-			}
 			for (int i = 0; i < types.size(); i++) {
 				if (!types.get(i).compare(t.types.get(i)))
 					return false;
 			}
 			return true;
 		}
-		if (o instanceof FunctionType) {
-			// TODO
-			FunctionType func = (FunctionType) o;
-			if (!(func.getDomain() instanceof IntType)) {
-				return false;
-			}
-			TLAType range = func.getRange();
-			for (int i = 0; i < types.size(); i++) {
-				if (types.get(i).compare(range)) {
-					continue;
-				} else {
-					return false;
-				}
-			}
-			if (!compareToAll(range)) {
-				return false;
-			}
-			return true;
-		}
+
 		if (o instanceof TupleOrFunction) {
 			return o.compare(this);
 		}
@@ -99,18 +75,6 @@ public class TupleType extends AbstractHasFollowers {
 		return false;
 	}
 
-	private boolean compareToAll(TLAType other) {
-		for (int i = 0; i < types.size(); i++) {
-			for (int j = i + 1; j < types.size(); j++) {
-				if (!types.get(i).compare(types.get(j)))
-					return false;
-			}
-			if (!types.get(i).compare(other))
-				return false;
-		}
-		return true;
-	}
-
 	@Override
 	public boolean contains(TLAType o) {
 		for (TLAType tlaType : types) {
@@ -149,16 +113,7 @@ public class TupleType extends AbstractHasFollowers {
 		}
 		if (o instanceof TupleType) {
 			TupleType tuple = (TupleType) o;
-			if (this.types.size() != tuple.types.size()) {
-				TLAType t = types.get(0);
-				for (int i = 1; i < types.size(); i++) {
-					t = t.unify(types.get(i));
-				}
-				for (int i = 0; i < tuple.types.size(); i++) {
-					t = t.unify(tuple.types.get(i));
-				}
-				return new FunctionType(IntType.getInstance(), t);
-			} else {
+
 			for (int i = 0; i < types.size(); i++) {
 				TLAType res = types.get(i).unify(tuple.types.get(i));
 				types.set(i, res);
@@ -167,25 +122,7 @@ public class TupleType extends AbstractHasFollowers {
 			}
 			return this;
 		}
-		}
-		if (o instanceof FunctionType) {
-			// TODO
-			if (compareToAll(new UntypedType())) {
-				// Function
-				TLAType t = types.get(0);
-				for (int i = 1; i < types.size(); i++) {
-					t = t.unify(types.get(i));
-				}
-				FunctionType func = new FunctionType(IntType.getInstance(), t);
-				this.setFollowersTo(func);
-				return func.unify(o);
-			} else {
-				TLAType res = types.get(1).unify(((FunctionType) o).getRange());
-				types.set(1, res);
-				return this;
-			}
 
-		}
 		if (o instanceof TupleOrFunction) {
 			return o.unify(this);
 		}

src/main/java/de/tla2bAst/Translator.java

@@ -308,7 +308,7 @@ public class Translator implements TranslationGlobals {
 		}
 
 		Renamer renamer = new Renamer(BAst);
-		ASTPrettyPrinter aP = new ASTPrettyPrinter(renamer);
+		ASTPrettyPrinter aP = new ASTPrettyPrinter(BAst, renamer);
 		BAst.apply(aP);
 		StringBuilder result = aP.getResultAsStringbuilder();
 		result.insert(0, "/*@ generated by TLA2B " + VERSION + " " + new Date()

src/test/java/de/tla2b/prettyprintb/ExampleFilesTest.java

@@ -36,7 +36,7 @@ public class ExampleFilesTest extends AbstractParseModuleTest {
 		Start start = t.translate();
 		String resultTree = TestUtil.getTreeAsString(start);
 		
-		ASTPrettyPrinter aP = new ASTPrettyPrinter();
+		ASTPrettyPrinter aP = new ASTPrettyPrinter(start);
 		start.apply(aP);
 		System.out.println(aP.getResultString());
 

src/test/java/de/tla2b/prettyprintb/ExceptTest.java

@@ -17,8 +17,25 @@ public class ExceptTest {
 				+ "=================================";
 
 		final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
-				+ "PROPERTIES " + " k : BOOL +-> INTEGER "
-				+ "& k = k <+ {TRUE |-> 0, FALSE |-> 0}" + "END";
+				+ "PROPERTIES " 
+				+ "k : BOOL +-> INTEGER & k = (k <+ {(TRUE,0)}) <+ {(FALSE,0)} \n "
+				+ "END";
+		compare(expected, module);
+	}
+	
+	@Test
+	public void testFunctionExcept2() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "EXTENDS Naturals \n"
+				+ "CONSTANTS k, k2 \n"
+				+ "ASSUME k = [i \\in {3} |-> i] /\\ k2 = [k EXCEPT ![3] = @+1, ![3] = @+1]  \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n" 
+				+ "CONSTANTS k, k2\n"
+				+ "PROPERTIES " 
+				+ "(k : INTEGER +-> INTEGER & k2 : INTEGER +-> INTEGER) & (k = %(i).(i : {3} | i) & k2 = (k <+ {(3,k(3) + 1)}) <+ {(3,(k <+ {(3,k(3) + 1)})(3) + 1)}) \n "
+				+ "END";
 		compare(expected, module);
 	}
 
@@ -36,6 +53,21 @@ public class ExceptTest {
 				+ "END";
 		compare(expected, module);
 	}
+	
+	@Test
+	public void testFunctionTuple() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "EXTENDS Naturals \n"
+				+ "CONSTANTS k \n"
+				+ "ASSUME k = [i \\in {3,4}, j \\in {5,6} |-> i+j] /\\ k # [k EXCEPT ![3,5] = 1]  \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+				+ "PROPERTIES " 
+				+ "k : INTEGER * INTEGER +-> INTEGER & (k = %(i, j).(i : {3, 4} & j : {5, 6} | i + j) & k /= k <+ {((3,5),1)}) \n" 
+				+ "END";
+		compare(expected, module);
+	}
 	@Test
 	public void testNestedFunctionAt() throws Exception {
 		final String module = "-------------- MODULE Testing ----------------\n"
@@ -60,7 +92,7 @@ public class ExceptTest {
 
 		final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
 				+ "PROPERTIES "
-				+ "k : struct(a:INTEGER, b:BOOL) & (k = rec(a:1, b:TRUE) & k /= rec(a:2, b:FALSE))" 
+				+ "k : struct(a:INTEGER, b:BOOL) & (k = rec(a:1, b:TRUE) & k /= rec(a:rec(a:2, b:k'b)'a, b:FALSE)) \n" 
 				+ "END";
 		compare(expected, module);
 
@@ -70,13 +102,13 @@ public class ExceptTest {
 	public void testRecordAt() throws Exception {
 		final String module = "-------------- MODULE Testing ----------------\n"
 				+ "EXTENDS Naturals \n"
-				+ "CONSTANTS k \n"
-				+ "ASSUME k = [a |-> 1, b |-> TRUE] /\\ k /= [k EXCEPT !.a = @ + 1]  \n"
+				+ "CONSTANTS k, k2 \n"
+				+ "ASSUME k = [a |-> 1, b |-> 1] /\\ k2 = [k EXCEPT !.b = @ + 1, !.b = @ + 1]  \n"
 				+ "=================================";
 
-		final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+		final String expected = "MACHINE Testing\n" + "CONSTANTS k, k2\n"
 				+ "PROPERTIES "
-				+ "k : struct(a:INTEGER, b:BOOL) & (k = rec(a:1, b:TRUE) & k /= rec(a:k'a + 1, b:k'b)) \n" 
+				+ "(k : struct(a:INTEGER, b:INTEGER) & k2 : struct(a:INTEGER, b:INTEGER)) & (k = rec(a:1, b:1) & k2 = rec(a:rec(a:k'a, b:k'b + 1)'a, b:rec(a:k'a, b:k'b + 1)'b + 1)) \n" 
 				+ "END";
 		compare(expected, module);
 

src/test/java/de/tla2b/prettyprintb/ExternelFunctionsTest.java

+package de.tla2b.prettyprintb;
+
+import static de.tla2b.util.TestUtil.compare;
+
+import org.junit.Test;
+
+public class ExternelFunctionsTest {
+
+	
+	@Test
+	public void testAssert() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "EXTENDS TLC \n"
+				+ "ASSUME Assert(TRUE, \"abc\") \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n"
+				+ "DEFINITIONS "
+				+ "ASSERT_TRUE(P, Msg) == 1 = 1; \n"
+				+ "EXTERNAL_PREDICATE_ASSERT_TRUE == BOOL * STRING; \n"
+				+ "PROPERTIES ASSERT_TRUE(TRUE, \"abc\") \n" 
+				+ "END";
+		compare(expected, module);
+	}
+}

src/test/java/de/tla2b/prettyprintb/FunctionTest.java

@@ -53,6 +53,51 @@ public class FunctionTest {
 		compare(expected, module);
 	}
 	
+	@Test
+	public void testFunctionConstructor4() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "EXTENDS Naturals \n"
+				+ "CONSTANTS k\n"
+				+ "ASSUME k = [<<x,y>> \\in {1} \\X {2} |-> x + y] \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n"
+				+ "CONSTANTS k\n"
+				+ "PROPERTIES k : INTEGER * INTEGER +-> INTEGER & k = %(x, y).((x,y) : {1} * {2} | x + y) \n"
+				+ "END";
+		compare(expected, module);
+	}
+	
+	@Test
+	public void testFunctionConstructorTuple() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "EXTENDS Naturals \n"
+				+ "CONSTANTS k\n"
+				+ "ASSUME k = [a \\in {1}, <<b,c>> \\in {2} \\X {3} |-> a + b + c] \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n"
+				+ "CONSTANTS k\n"
+				+ "PROPERTIES k : INTEGER * (INTEGER * INTEGER) +-> INTEGER  & k = %(a, bc).(a : {1} & bc : {2} * {3} | (a + prj1(INTEGER, INTEGER)(bc)) + prj2(INTEGER, INTEGER)(bc)) \n"
+				+ "END";
+		compare(expected, module);
+	}
+	
+	@Test
+	public void testFunctionConstructorSequence() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "EXTENDS Naturals \n"
+				+ "CONSTANTS k\n"
+				+ "ASSUME k = [<<a>> \\in {<<1>>}, <<b,c>> \\in {2} \\X {3} |-> a + b + c] \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n"
+				+ "CONSTANTS k\n"
+				+ "PROPERTIES k : (INTEGER +-> INTEGER) * (INTEGER * INTEGER) +-> INTEGER  & k = %(a, bc).(a : {[1]} & bc : {2} * {3} | (a(1) + prj1(INTEGER, INTEGER)(bc)) + prj2(INTEGER, INTEGER)(bc)) \n"
+				+ "END";
+		compare(expected, module);
+	}
+
 	/**********************************************************************
 	 * recursive Function
 	 **********************************************************************/

src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java

@@ -137,6 +137,39 @@ public class LogicOperatorsTest {
 		compare(expected, module);
 	}
 	
+	@Test
+	public void testExistentialQuantifierSequence() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "ASSUME \\E <<x>> \\in {<<1>>} : x = 1 \n"
+				+ "=================================";
+		final String expected = "MACHINE Testing\n"
+				+ "PROPERTIES #x.([x] : {[1]} & x = 1) \n"
+				+ "END";
+		compare(expected, module);
+	}
+	
+	@Test
+	public void testExistentialQuantifierTuple() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "ASSUME \\E <<a,b>> \\in {<<1,TRUE>>} : a = 1 /\\ b = TRUE  \n"
+				+ "=================================";
+		final String expected = "MACHINE Testing\n"
+				+ "PROPERTIES #(a,b).((a,b) : {(1,TRUE)} & (a = 1 & b = TRUE)) \n"
+				+ "END";
+		compare(expected, module);
+	}
+	
+	@Test
+	public void testExistentialQuantifierAll() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "ASSUME \\E <<a,b>> \\in {<<1,TRUE>>}, <<c>> \\in {<<3>>}, d,e \\in {TRUE}:  a= 1 /\\ b = TRUE /\\ c = 3 /\\ d = TRUE /\\ e  \n"
+				+ "=================================";
+		final String expected = "MACHINE Testing\n"
+				+ "PROPERTIES #(a,b,c,d,e).(((((a,b) : {(1,TRUE)} & [c] : {[3]}) & d : {TRUE}) & e : {TRUE}) & ((((a = 1 & b = TRUE) & c = 3) & d = TRUE) & e = TRUE)) \n"
+				+ "END";
+		compare(expected, module);
+	}
+
 	@Test
 	public void testQuantifier() throws Exception {
 		final String module = "-------------- MODULE Testing ----------------\n"