add more tests

src/test/java/de/tla2b/examples/MCTest.java

@@ -72,7 +72,7 @@ public class MCTest {
 	
 	@Ignore
 	@Test
-	public void testRecursiveFunciton() throws Exception {
+	public void testRecursiveFunction() throws Exception {
 		String file = "src/test/resources/examples/RecursiveFunction/RecursiveFunction.tla";
 		runModule(file);
 	}

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

@@ -38,6 +38,11 @@ public class ComplexExpressionTest {
 		compareExpr("1 + 2", "LET foo == 1 bar == 2 IN foo + bar ");
 	}
 
+	@Test
+	public void testLetTwoDefsReal() throws Exception {
+		compareExpr("1.0 + 2.0", "LET foo == 1.0 bar == 2.0 IN foo + bar ");
+	}
+
 	@Test
 	public void testPrime() throws Exception {
 		compareExpr("x_n = 1", "x' = 1");

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

@@ -16,6 +16,16 @@ public class TestKeywords {
 		compareExpr("NATURAL", "Nat");
 	}
 
+	@Test
+	public void testInt() throws Exception {
+		compareExpr("INTEGER", "Int");
+	}
+
+	@Test
+	public void testReal() throws Exception {
+		compareExpr("REAL", "Real");
+	}
+
 	@Test
 	public void testExcept() throws Exception {
 		compareExpr("x = a <+ {1 |-> 1}", "x = [a EXCEPT ![1] = 1]");

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

@@ -10,6 +10,13 @@ public class InstanceTest {
 
 	private static final String path = "src/test/resources/typechecking/modules/";
 
+	@Test
+	public void TestCounterReal() throws Exception {
+		TestTypeChecker t = TestUtil.typeCheck(path + "CounterReal.tla");
+		assertEquals("REAL", t.getConstantType("start"));
+		assertEquals("REAL", t.getVariableType("x"));
+	}
+
 	@Test
 	public void TestNamedInstanceCounter() throws Exception {
 		TestTypeChecker t = TestUtil.typeCheck(path + "NamedInstanceCounter.tla");

src/test/resources/typechecking/modules/CounterReal.tla

+-------------------------- MODULE CounterReal -----------------------------
+EXTENDS Reals
+CONSTANTS start
+VARIABLE x
+---------------------------------------------------------------------------
+Init  ==  x = start
+Inc == x' = x + 1.0
+Dec == x' = x - 0.99
+Next  ==  Inc \/ Dec
+===========================================================================