add tuple and except Test

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

@@ -4,6 +4,7 @@ import de.tla2b.exceptions.TLA2BException;
 import de.tla2b.exceptions.TypeErrorException;
 import de.tla2b.util.TestTypeChecker;
 import de.tla2b.util.TestUtil;
+import org.junit.Ignore;
 import org.junit.Test;
 
 import static org.junit.Assert.assertEquals;
@@ -31,8 +32,7 @@ public class ExceptTest {
 			+ "ASSUME k = [k EXCEPT ![1] = [a|-> 1, b |-> TRUE], ![1].b = k2 ] "
 			+ "=================================";
 		TestTypeChecker t = TestUtil.typeCheckString(module);
-		assertEquals("POW(INTEGER*struct(a:INTEGER,b:BOOL))",
-			t.getConstantType("k"));
+		assertEquals("POW(INTEGER*struct(a:INTEGER,b:BOOL))", t.getConstantType("k"));
 		assertEquals("BOOL", t.getConstantType("k2"));
 	}
 
@@ -44,8 +44,7 @@ public class ExceptTest {
 			+ "ASSUME k = [k EXCEPT ![1].a = 2, ![1].b = k2 ] /\\ k2 = TRUE \n"
 			+ "=================================";
 		TestTypeChecker t = TestUtil.typeCheckString(module);
-		assertEquals("POW(INTEGER*struct(a:INTEGER,b:BOOL))",
-			t.getConstantType("k"));
+		assertEquals("POW(INTEGER*struct(a:INTEGER,b:BOOL))", t.getConstantType("k"));
 	}
 
 	@Test
@@ -126,6 +125,19 @@ public class ExceptTest {
 		assertEquals("INTEGER", t.getConstantType("k"));
 	}
 
+	@Ignore
+	@Test
+	public void testRecordAtExcept() throws TLA2BException {
+		// TODO: implement in Typechecker
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "CONSTANTS k, k2 \n"
+				+ "ASSUME k = <<[x |-> TRUE], FALSE>> /\\ k2 = [k EXCEPT ![1].x = ~@] \n"
+				+ "=================================";
+		TestTypeChecker t = TestUtil.typeCheckString(module);
+		assertEquals("struct(x:BOOL)*BOOL", t.getConstantType("k"));
+		assertEquals("struct(x:BOOL)*BOOL", t.getConstantType("k2"));
+	}
+
 	@Test
 	public void testAtTuple() throws Exception {
 		final String module = "-------------- MODULE Testing ----------------\n"
@@ -139,5 +151,4 @@ public class ExceptTest {
 		assertEquals("POW(INTEGER*(INTEGER*STRING))", t.getConstantType("k2"));
 	}
 
-
 }

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

@@ -73,8 +73,7 @@ public class TupleTest {
 	}
 
 	@Test
-	public void testTupleComponentsOfTheSameType() throws
-		TLA2BException {
+	public void testTupleComponentsOfTheSameType() throws TLA2BException {
 		final String module = "-------------- MODULE Testing ----------------\n"
 			+ "EXTENDS Naturals \n"
 			+ "CONSTANTS k \n"
@@ -110,8 +109,7 @@ public class TupleTest {
 	}
 
 	@Test
-	public void testTupleSingleElement() throws
-		TLA2BException {
+	public void testTupleSingleElement() throws TLA2BException {
 		final String module = "-------------- MODULE Testing ----------------\n"
 			+ "CONSTANTS k \n"
 			+ "ASSUME k = <<TRUE>> \n"
@@ -158,8 +156,7 @@ public class TupleTest {
 	 * Cartesian Product
 	 */
 	@Test
-	public void testCartesianProduct2() throws
-		TLA2BException {
+	public void testCartesianProduct2() throws TLA2BException {
 		final String module = "-------------- MODULE Testing ----------------\n"
 			+ "CONSTANTS k \n"
 			+ "ASSUME k = BOOLEAN \\X {1} \n"
@@ -169,8 +166,7 @@ public class TupleTest {
 	}
 
 	@Test
-	public void testCartesianProduct3() throws
-		TLA2BException {
+	public void testCartesianProduct3() throws TLA2BException {
 		final String module = "-------------- MODULE Testing ----------------\n"
 			+ "CONSTANTS k, k2 \n"
 			+ "ASSUME BOOLEAN \\X {1} = k \\X k2 \n"
@@ -181,8 +177,7 @@ public class TupleTest {
 	}
 
 	@Test (expected = TypeErrorException.class)
-	public void testCartesianProductException() throws
-		TLA2BException {
+	public void testCartesianProductException() throws TLA2BException {
 		final String module = "-------------- MODULE Testing ----------------\n"
 			+ "CONSTANTS k \n"
 			+ "ASSUME k = BOOLEAN \\X 1 \n"
@@ -190,4 +185,14 @@ public class TupleTest {
 		TestUtil.typeCheckString(module);
 	}
 
+	@Test
+	public void testTupleWithRecord() throws TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "CONSTANTS k \n"
+				+ "ASSUME k = <<[x |-> TRUE, y |-> 5], FALSE>> \n"
+				+ "=================================";
+		TestTypeChecker t = TestUtil.typeCheckString(module);
+		assertEquals("struct(x:BOOL,y:INTEGER)*BOOL", t.getConstantType("k"));
+	}
+
 }