nested except statements

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

@@ -740,7 +740,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 			} else if (list.size() == 1) {
 				found = new FunctionType(IntType.getInstance(), list.get(0));
 			} else {
-				found = new TupleType(list);
+				found = TupleOrFunction.createTupleOrFunctionType(list);
+				//found = new TupleType(list);
 			}
 			try {
 				found = found.unify(expected);
@@ -920,7 +921,6 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 						new SetType(new UntypedType()));
 				list.add(t.getSubType());
 			}
-
 			SetType found = new SetType(new TupleType(list));
 			try {
 				found = found.unify(expected);
@@ -929,6 +929,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 						"Expected %s, found %s at Cartesian Product,%n%s",
 						expected, found, n.getLocation()));
 			}
+			
 			return found;
 		}
 

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;
@@ -25,6 +27,26 @@ public class TupleOrFunction extends AbstractHasFollowers {
 		super(TUPLE_OR_FUNCTION);
 	}
 
+	public static TLAType createTupleOrFunctionType(List<TLAType> list) {
+		if (comparable(list)) {
+			TupleOrFunction tOrF = new TupleOrFunction();
+			tOrF.add(list);
+			return tOrF;
+		} else {
+			return new TupleType(list);
+		}
+	}
+
+	public void add(List<TLAType> list) {
+		for (int i = 0; i < list.size(); i++) {
+			TLAType type = list.get(i);
+			types.put(i + 1, type);
+			if (type instanceof AbstractHasFollowers) {
+				((AbstractHasFollowers) type).addFollower(this);
+			}
+		}
+	}
+
 	public void apply(TypeVisitorInterface visitor) {
 		throw new RuntimeException("Type " + this + " is not a complete type.");
 	}
@@ -37,10 +59,27 @@ public class TupleOrFunction extends AbstractHasFollowers {
 		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(");
-			for (Iterator<Integer> keys = types.keySet().iterator(); keys.hasNext();) {
+				sb.append("(");
+				for (Iterator<Integer> keys = types.keySet().iterator(); keys
+						.hasNext();) {
 					Integer key = keys.next();
 					sb.append(key);
 					sb.append(" : ").append(types.get(key));
@@ -51,32 +90,61 @@ public class TupleOrFunction extends AbstractHasFollowers {
 				throw new RuntimeException("Type " + sb + "is incomplete");
 			}
 
-		return res.toString();
-		
+		}
 
 	}
 
 	@Override
 	public PExpression getBNode() {
-		return null;
+		FunctionType func = new FunctionType();
+		func.setDomain(IntType.getInstance());
+		func.setRange(new UntypedType());
+		FunctionType res;
+		try {
+			res = func.unify(this);
+			return res.getBNode();
+		} 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).getBNode();
+			} else {
+				StringBuilder sb = new StringBuilder();
+				sb.append("(");
+				for (Iterator<Integer> keys = types.keySet().iterator(); keys
+						.hasNext();) {
+					Integer key = keys.next();
+					sb.append(key);
+					sb.append(" : ").append(types.get(key));
+					if (keys.hasNext())
+						sb.append(", ");
+				}
+				sb.append(")");
+				throw new RuntimeException("Type " + sb + "is incomplete");
+			}
+
+		}
+		
 	}
 
 	@Override
 	public boolean compare(TLAType o) {
-		if (this.contains(o) || o.contains(this))
+		if (this.contains(o) || o.contains(this)){
 			return false;
+		}
 		if (o.getKind() == UNTYPED)
 			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;
-				}
-			}
-		}
+
 		if (o instanceof FunctionType) {
 			FunctionType t = (FunctionType) o;
 			if (!t.getDomain().compare(IntType.getInstance())) {
@@ -100,10 +168,51 @@ public class TupleOrFunction extends AbstractHasFollowers {
 			}
 			return true;
 		}
+		if (o instanceof TupleOrFunction) {
+			TupleOrFunction other = (TupleOrFunction) o;
+			if (isTupleOrFunction(this, other)) {
+				return true;
+			}
+
+			try {
+				for (int i = 1; i <= types.keySet().size(); i++) {
+					if (!types.get(i).compare(other.types.get(i))) {
+						return false;
+					}
+				}
+			} catch (Exception e) {
+				return false;
+			}
+
+			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
 		return false;
 	}
 
+	private static boolean isTupleOrFunction(TupleOrFunction t1,
+			TupleOrFunction t2) {
+		List<TLAType> typeList = new ArrayList<TLAType>();
+		typeList.addAll(t1.types.values());
+		typeList.addAll(t2.types.values());
+		if (comparable(typeList)) {
+			return true;
+		}
+		return false;
+	}
+
 	@Override
 	public boolean contains(TLAType o) {
 		for (TLAType type : this.types.values()) {
@@ -161,47 +270,116 @@ public class TupleOrFunction extends AbstractHasFollowers {
 		}
 		if (o instanceof TupleType) {
 			TupleType tupleType = (TupleType) o;
-			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);
+			
+			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));
+					typeList.add(res);
+				}else {
+					typeList.add(tupleType.getTypes().get(i));
+				}
+			}
+			TupleType r = new TupleType(typeList);
+			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) {
+							((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);
 					}
-					TLAType elementOfTuple = tupleType.getTypes()
-							.get(index - 1);
-					elementOfTuple.unify(type);
 				}
-				return tupleType;
+				return this;
 			} else{
-				TLAType range = new UntypedType();
-				for (TLAType type : types.values()) {
-					if (type instanceof AbstractHasFollowers) {
-						((AbstractHasFollowers) type).removeFollower(this);
+				ArrayList<TLAType> list1 = new ArrayList<TLAType>();
+				for (int i = 1; i <= types.keySet().size(); i++) {
+						list1.add(types.get(i));
 				}
-					range = range.unify(type);
+				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));
 				}
-				FunctionType funcType = new FunctionType(IntType.getInstance(),
-						range);
-				return funcType.unify(tupleType);
+				TupleType tuple2 = new TupleType(list2);
+				return tuple1.unify(tuple2);
 			}
+
 		}
+
 		throw new RuntimeException();
 	}
 
-	public void setNewType(AbstractHasFollowers oldType,
-			TLAType newType) {
-		LinkedHashMap<Integer, TLAType> temp = new LinkedHashMap<Integer, TLAType>(types);
+	public void setNewType(AbstractHasFollowers oldType, TLAType newType) {
+		LinkedHashMap<Integer, TLAType> temp = new LinkedHashMap<Integer, TLAType>(
+				types);
 		for (Entry<Integer, TLAType> entry : temp.entrySet()) {
 			if (entry.getValue().equals(oldType)) {
 				types.put(entry.getKey(), newType);
 				if (newType instanceof AbstractHasFollowers) {
-					((AbstractHasFollowers) newType).addFollower(this);;
+					((AbstractHasFollowers) newType).addFollower(this);
+					;
+				}
 			}
 		}
+
 	}
 
+	private static boolean comparable(List<TLAType> typeList) {
+		for (int i = 0; i < typeList.size() - 1; i++) {
+			TLAType t1 = typeList.get(i);
+			for (int j = 1; j < typeList.size(); j++) {
+				TLAType t2 = typeList.get(j);
+				if (!t1.compare(t2))
+					return false; // tuple
+			}
+		}
+		return true;
 	}
 
 }

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

@@ -9,9 +9,9 @@ import de.tla2b.exceptions.UnificationException;
 import de.tla2b.output.TypeVisitorInterface;
 
 public class TupleType extends AbstractHasFollowers {
-	private ArrayList<TLAType> types;
+	private List<TLAType> types;
 
-	public TupleType(ArrayList<TLAType> typeList) {
+	public TupleType(List<TLAType> typeList) {
 		super(TUPLE);
 		setTypes(typeList);
 	}
@@ -29,7 +29,7 @@ public class TupleType extends AbstractHasFollowers {
 		return new ArrayList<TLAType>(types);
 	}
 
-	public void setTypes(ArrayList<TLAType> types) {
+	public void setTypes(List<TLAType> types) {
 		this.types = types;
 		types = new ArrayList<TLAType>(types);
 		for (TLAType tlaType : types) {

src/main/java/de/tla2bAst/BAstCreator.java

@@ -1693,18 +1693,34 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 		{
 			TLAType type = (TLAType) n.getToolObject(TYPE_ID);
 			if (type.getKind() == IType.STRUCT) {
+				StructType structType = (StructType) type;
 				Hashtable<String, PExpression> temp = new Hashtable<String, PExpression>();
 				for (int i = 1; i < n.getArgs().length; i++) {
 					OpApplNode pair = (OpApplNode) n.getArgs()[i];
+
 					ExprOrOpArgNode first = pair.getArgs()[0];
-					ExprOrOpArgNode second = pair.getArgs()[1];
+					ExprOrOpArgNode val = pair.getArgs()[1];
 					OpApplNode seq = (OpApplNode) first;
 
-					PExpression val = visitExprOrOpArgNodeExpression(second);
+					LinkedList<ExprOrOpArgNode> seqList = new LinkedList<ExprOrOpArgNode>();
+					for (int j = 0; j < seq.getArgs().length; j++) {
+						seqList.add(seq.getArgs()[j]);
+					}
 
-					StringNode stringNode = (StringNode) seq.getArgs()[0];
+					PExpression oldRec = visitExprOrOpArgNodeExpression(n
+							.getArgs()[0]);
+					//PExpression val =  visitExprOrOpArgNodeExpression(second);
+					ARecordFieldExpression select = new ARecordFieldExpression();
+					select.setRecord(oldRec);
+					
+					StringNode stringNode = (StringNode) seqList.poll();
 					String fieldName = stringNode.getRep().toString();
-					temp.put(fieldName, val);
+					select.setIdentifier(createIdentifierNode(fieldName));
+					
+					PExpression value = evalExceptValue(select,
+									seqList, structType.getType(fieldName), val);		
+							
+					temp.put(fieldName, value);
 				}
 
 				StructType st = (StructType) type;
@@ -1725,20 +1741,38 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 				}
 				ARecExpression rec = new ARecExpression(list);
 				return rec;
-
 			} else {
-				// FunctionType func = (FunctionType) type;
+				FunctionType func = (FunctionType) type;
 
 				List<PExpression> list = new ArrayList<PExpression>();
 				for (int i = 1; i < n.getArgs().length; i++) {
 					OpApplNode pair = (OpApplNode) n.getArgs()[i];
 
+					ExprOrOpArgNode first = pair.getArgs()[0];
+					ExprOrOpArgNode val = pair.getArgs()[1];
+					OpApplNode seq = (OpApplNode) first;
+
+					LinkedList<ExprOrOpArgNode> seqList = new LinkedList<ExprOrOpArgNode>();
+					for (int j = 0; j < seq.getArgs().length; j++) {
+						seqList.add(seq.getArgs()[j]);
+					}
+
+					PExpression oldFunc = visitExprOrOpArgNodeExpression(n
+							.getArgs()[0]);
+					PExpression firstArg = visitExprOrOpArgNodeExpression(seqList
+							.poll());
+					AFunctionExpression funcApplication = new AFunctionExpression();
+					funcApplication.setIdentifier(oldFunc);
+					List<PExpression> argList = new ArrayList<PExpression>();
+					argList.add(firstArg);
+					funcApplication.setParameters(argList);
+
+					PExpression value = evalExceptValue(funcApplication,
+							seqList, func.getRange(), val);
 					ACoupleExpression couple = new ACoupleExpression();
 					List<PExpression> coupleList = new ArrayList<PExpression>();
-					coupleList.add(visitExprOrOpArgNodeExpression(pair
-							.getArgs()[0]));
-					coupleList.add(visitExprOrOpArgNodeExpression(pair
-							.getArgs()[1]));
+					coupleList.add(firstArg);
+					coupleList.add(value);
 					couple.setList(coupleList);
 					list.add(couple);
 				}
@@ -1800,6 +1834,70 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 		throw new RuntimeException(n.getOperator().getName().toString());
 	}
 
+	private PExpression evalExceptValue(PExpression prefix,
+			LinkedList<ExprOrOpArgNode> seqList, TLAType tlaType,
+			ExprOrOpArgNode val) {
+
+		ExprOrOpArgNode head = seqList.poll();
+		if (head == null) {
+			return visitExprOrOpArgNodeExpression(val);
+		}
+
+		if (tlaType instanceof StructType) {
+			StructType structType = (StructType) tlaType;
+			String field = ((StringNode) head).getRep().toString();
+
+			List<PRecEntry> list = new ArrayList<PRecEntry>();
+			for (int i = 0; i < structType.getFields().size(); i++) {
+				ARecEntry entry = new ARecEntry();
+				String fieldName = structType.getFields().get(i);
+				entry.setIdentifier(createIdentifierNode(fieldName));
+				
+				PExpression value = null;
+				ARecordFieldExpression select = new ARecordFieldExpression();
+				select.setRecord((PExpression)prefix.clone());
+				select.setIdentifier(createIdentifierNode(fieldName));
+				if(fieldName.equals(field)){
+
+					value = evalExceptValue(select, seqList, structType.getType(fieldName),
+							val);
+				}else{
+					value = select;
+				}
+				entry.setValue(value);
+				list.add(entry);
+				
+			}
+			
+			ARecExpression rec = new ARecExpression(list);
+			return rec;
+
+		} else {
+			FunctionType func = (FunctionType) tlaType;
+
+			ACoupleExpression couple = new ACoupleExpression();
+			List<PExpression> coupleList = new ArrayList<PExpression>();
+			coupleList.add(visitExprOrOpArgNodeExpression(head));
+
+			AFunctionExpression funcCall = new AFunctionExpression();
+			funcCall.setIdentifier(prefix);
+			List<PExpression> argList = new ArrayList<PExpression>();
+			argList.add(visitExprOrOpArgNodeExpression(head));
+			funcCall.setParameters(argList);
+			coupleList.add(evalExceptValue(funcCall, seqList, func.getRange(),
+					val));
+			couple.setList(coupleList);
+			List<PExpression> setList = new ArrayList<PExpression>();
+			setList.add(couple);
+			ASetExtensionExpression setExtension = new ASetExtensionExpression(
+					setList);
+			AOverwriteExpression overwrite = new AOverwriteExpression();
+			overwrite.setLeft((PExpression) prefix.clone());
+			overwrite.setRight(setExtension);
+			return overwrite;
+		}
+	}
+
 	private PExpression createProjectionFunction(OpApplNode n, int field,
 			TLAType t) {
 		TupleType tuple = (TupleType) t;

src/test/java/de/tla2b/expression/ComplexExpressionTest.java

@@ -63,7 +63,7 @@ public class ComplexExpressionTest {
 
 	@Test
 	public void testRecord2() throws Exception {
-		compareExpr("bool(r = rec(a:rec(x:1, y:TRUE), b:1) & r2 = rec(a:2, b:r'b))",
+		compareExpr("bool(r = rec(a:rec(x:1, y:TRUE), b:1) & r2 = rec(a:rec(x:2, y:(r'a)'y), b:r'b))",
 				"r = [a |-> [x|->1,y|->TRUE], b |-> 1] "
 						+ "/\\ r2 = [r EXCEPT !.a.x = 2]");
 	}

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

@@ -23,15 +23,61 @@ public class ExceptTest {
 	}
 
 	@Test
-	public void testFunctionExcept2() throws Exception {
+	public void testRecordExcept() throws Exception {
 		final String module = "-------------- MODULE Testing ----------------\n"
 				+ "CONSTANTS k \n"
-				+ "ASSUME k = [k EXCEPT ![TRUE] = 0, ![FALSE] = 0]  \n"
+				+ "ASSUME k = [a |-> 1, b |-> TRUE] /\\ k /= [k EXCEPT !.a = 2, !.b = FALSE]  \n"
 				+ "=================================";
 
 		final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
-				+ "PROPERTIES " + " k : BOOL +-> INTEGER "
-				+ "& k = k <+ {TRUE |-> 0, FALSE |-> 0}" + "END";
+				+ "PROPERTIES "
+				+ "k : struct(a:INTEGER, b:BOOL) & (k = rec(a:1, b:TRUE) & k /= rec(a:2, b:FALSE))" 
+				+ "END";
+		compare(expected, module);
+
+	}
+	
+	@Test
+	public void testRecordFunctionExcept() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "CONSTANTS k \n"
+				+ "ASSUME k = [a |-> <<3>>] /\\ k /= [k EXCEPT !.a[1] = 4]  \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+				+ "PROPERTIES "
+				+ "k : struct(a:INTEGER +-> INTEGER) & (k = rec(a:[3]) & k /= rec(a:k'a <+ {(1,4)})) \n" 
+				+ "END";
+		compare(expected, module);
+
+	}
+	
+	@Test
+	public void testFunctionRecordExcept() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "CONSTANTS k \n"
+				+ "ASSUME k = [i \\in {3,4} |->[a |-> i, b |-> TRUE ] ] /\\ k /= [k EXCEPT ![3].b = FALSE]  \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+				+ "PROPERTIES "
+				+ "k : INTEGER +-> struct(a:INTEGER, b:BOOL) & (k = %(i).(i : {3, 4} | rec(a:i, b:TRUE)) & k /= k <+ {(3,rec(a:k(3)'a, b:FALSE))}) \n" 
+				+ "END";
+		compare(expected, module);
+
+	}
+	
+	@Test
+	public void testRecordExceptNested() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "CONSTANTS k \n"
+				+ "ASSUME k = [a |-> [b |-> 1, c |-> 2]] /\\ k /= [k EXCEPT !.a.b = 2]  \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+				+ "PROPERTIES "
+				+ "k : struct(a:struct(b:INTEGER, c:INTEGER)) & (k = rec(a:rec(b:1, c:2)) & k /= rec(a:rec(b:2, c:(k'a)'c))) \n" 
+				+ "END";
 		compare(expected, module);
 
 	}
@@ -69,4 +115,51 @@ public class ExceptTest {
 		compare(expected, module);
 	}
 	
+	@Test
+	public void testFunctionExcept9() throws Exception {
+		ToolIO.reset();
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "EXTENDS Naturals \n"
+				+ "CONSTANTS k \n"
+				+ "ASSUME k = [i \\in {3,4} |-> <<i, 7>>] /\\ [k EXCEPT ![4] = <<4, 8>>] # [k EXCEPT ![4][2] = 9] \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+				+ "PROPERTIES "
+				+ "k : INTEGER +-> (INTEGER +-> INTEGER) & (k = %(i).(i : {3, 4} | [i,7]) & k <+ {(4,[4,8])} /= k <+ {(4,k(4) <+ {(2,9)})}) \n"
+				+ "END";
+		compare(expected, module);
+	}
+	
+	@Test
+	public void testFunctionExceptNested() throws Exception {
+		ToolIO.reset();
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "EXTENDS Naturals \n"
+				+ "CONSTANTS k \n"
+				+ "ASSUME k = [i \\in {3,4} |-> <<i, 7>>] /\\ k # [k EXCEPT ![4][2] = 8] \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+				+ "PROPERTIES "
+				+ "k : INTEGER +-> (INTEGER +-> INTEGER) & (k = %(i).(i : {3, 4} | [i,7]) & k /= k <+ {(4,k(4) <+ {(2,8)})}) \n"
+				+ "END";
+		compare(expected, module);
+	}
+	
+	@Test
+	public void testFunctionExceptNested2() throws Exception {
+		ToolIO.reset();
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "EXTENDS Naturals \n"
+				+ "CONSTANTS k \n"
+				+ "ASSUME k = [i \\in {3,4} |-> << <<8>> >>] /\\ k # [k EXCEPT ![4][1][1] = 7] \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+				+ "PROPERTIES "
+				+ "k : INTEGER +-> (INTEGER +-> (INTEGER +-> INTEGER)) & (k = %(i).(i : {3, 4} | [[8]]) & k /= k <+ {(4,k(4) <+ {(1,(k(4))(1) <+ {(1,7)})})}) \n"
+				+ "END";
+		compare(expected, module);
+	}
 }

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

@@ -115,4 +115,16 @@ public class TupleTest {
 		compare(expected, module);
 	}
 	
+	@Test
+	public void testDomainOfTuple() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "ASSUME {1,2,3} = DOMAIN <<\"a\", \"b\", \"c\">> \n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n"
+				+ "PROPERTIES {1, 2, 3} = dom([\"a\", \"b\", \"c\"]) \n"
+				+ "END";
+		compare(expected, module);
+	}
+
 }

src/test/java/de/tla2b/typechecking/TupleTest.java

@@ -72,7 +72,7 @@ public class TupleTest {
 				+ "=================================";
 
 		TestTypeChecker t = TestUtil.typeCheckString(module);
-		assertEquals("INTEGER*INTEGER*INTEGER", t.getConstantType("k").toString());
+		assertEquals("POW(INTEGER*INTEGER)", t.getConstantType("k").toString());
 	}
 
 	@Test
@@ -84,7 +84,7 @@ public class TupleTest {
 				+ "ASSUME k = <<1,1>> \n" + "=================================";
 
 		TestTypeChecker t = TestUtil.typeCheckString(module);
-		assertEquals("INTEGER*INTEGER", t.getConstantType("k").toString());
+		assertEquals("POW(INTEGER*INTEGER)", t.getConstantType("k").toString());
 	}
 
 	@Test

src/test/java/de/tla2b/typechecking/TupleVsSequenceTest.java

@@ -59,5 +59,24 @@ public class TupleVsSequenceTest {
 		assertEquals("INTEGER*BOOL", t.getConstantType("c"));
 	}
 	
+	@Test  
+	public void testTupleVsSequence5() throws FrontEndException, TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "CONSTANTS k\n"
+				+ "ASSUME k = <<1,2>> /\\ k \\in {1} \\X {2} \n"
+				+ "=================================";
+		TestTypeChecker t = TestUtil.typeCheckString(module);
+		assertEquals("INTEGER*INTEGER", t.getConstantType("k"));
+	}
+	
+	@Test  
+	public void testTupleVsSequence6() throws FrontEndException, TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "CONSTANTS k\n"
+				+ "ASSUME {k} = {<<x, y>> \\in {1} \\X {2}: TRUE} \n"
+				+ "=================================";
+		TestTypeChecker t = TestUtil.typeCheckString(module);
+		assertEquals("INTEGER*INTEGER", t.getConstantType("k"));
+	}
 	
 }

src/test/resources/regression/Club/Club.prob

-parser_version('2014-03-12 22:57:52.564').
-classical_b('Club',['/Users/hansen/git/tla2bAST/src/test/resources/regression/Club/Club.tla']).
-machine(abstract_machine(1,machine(2),machine_header(3,'Club',[]),[sets(4,[enumerated_set(5,'ENUM1',[identifier(6,n1),identifier(7,n2),identifier(8,n3)])]),constants(9,[identifier(info(10,tla_type(integer)),capacity),identifier(info(11,tla_type(set(modelvalue))),'NAME'),identifier(info(12,tla_type(integer)),total)]),properties(13,conjunct(14,conjunct(15,conjunct(16,conjunct(17,conjunct(18,member(19,identifier(20,capacity),integer_set(21)),equal(22,identifier(23,'NAME'),identifier(24,'ENUM1'))),member(25,identifier(26,total),integer_set(27))),conjunct(28,member(29,identifier(30,capacity),natural_set(31)),equal(32,identifier(33,capacity),integer(34,2)))),greater(35,card(36,identifier(37,'NAME')),identifier(38,capacity))),conjunct(39,member(40,identifier(41,total),natural_set(42)),greater(43,identifier(44,total),integer(45,2))))),variables(46,[identifier(info(47,tla_type(set(modelvalue))),member),identifier(info(48,tla_type(set(modelvalue))),waiting)]),invariant(49,conjunct(50,member(51,identifier(52,member),pow_subset(53,identifier(54,'ENUM1'))),member(55,identifier(56,waiting),pow_subset(57,identifier(58,'ENUM1'))))),initialisation(59,becomes_such(60,[identifier(61,member),identifier(62,waiting)],conjunct(63,equal(64,identifier(65,member),empty_set(66)),equal(67,identifier(68,waiting),empty_set(69))))),operations(70,[operation(71,identifier(71,join_queue),[],[identifier(72,nn)],any(73,[identifier(74,member_n)],conjunct(75,conjunct(76,conjunct(77,conjunct(78,conjunct(79,member(80,identifier(81,nn),identifier(82,'NAME')),not_member(83,identifier(84,nn),identifier(85,member))),not_member(86,identifier(87,nn),identifier(88,waiting))),member(89,identifier(90,member_n),pow_subset(91,identifier(92,'ENUM1')))),less(93,card(94,identifier(95,waiting)),identifier(96,total))),equal(97,identifier(98,member_n),identifier(99,member))),assign(100,[identifier(101,waiting),identifier(102,member)],[union(103,identifier(104,waiting),set_extension(105,[identifier(106,nn)])),identifier(107,member_n)]))),operation(108,identifier(108,join),[],[identifier(109,nn)],select(110,conjunct(111,conjunct(112,conjunct(113,member(114,identifier(115,nn),identifier(116,'NAME')),member(117,identifier(118,nn),identifier(119,waiting))),less(120,card(121,identifier(122,member)),identifier(123,capacity))),less(124,card(125,identifier(126,member)),identifier(127,capacity))),assign(128,[identifier(129,member),identifier(130,waiting)],[union(131,identifier(132,member),set_extension(133,[identifier(134,nn)])),minus_or_set_subtract(135,identifier(136,waiting),set_extension(137,[identifier(138,nn)]))]),[])),operation(139,identifier(139,remove),[],[identifier(140,nn)],any(141,[identifier(142,waiting_n)],conjunct(143,conjunct(144,conjunct(145,member(146,identifier(147,nn),identifier(148,'NAME')),member(149,identifier(150,nn),identifier(151,member))),member(152,identifier(153,waiting_n),pow_subset(154,identifier(155,'ENUM1')))),equal(156,identifier(157,waiting_n),identifier(158,waiting))),assign(159,[identifier(160,member),identifier(161,waiting)],[minus_or_set_subtract(162,identifier(163,member),set_extension(164,[identifier(165,nn)])),identifier(166,waiting_n)])))])])).