diff --git a/src/test/java/de/tla2b/examples/MCTest.java b/src/test/java/de/tla2b/examples/MCTest.java index 2526a1f777133bd672c92330aab3c79508a1b0a6..756380b790ec1d90c3c245c6d1ddf8ff55214ac0 100644 --- a/src/test/java/de/tla2b/examples/MCTest.java +++ b/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); } diff --git a/src/test/java/de/tla2b/expression/ComplexExpressionTest.java b/src/test/java/de/tla2b/expression/ComplexExpressionTest.java index 297a8a6009d517428ab436029148616c7860bcbf..520e759a17698f586c904b6d9819546809c7844a 100644 --- a/src/test/java/de/tla2b/expression/ComplexExpressionTest.java +++ b/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"); diff --git a/src/test/java/de/tla2b/expression/TestKeywords.java b/src/test/java/de/tla2b/expression/TestKeywords.java index 0f38543d041f25d136987d85bafc163c369bd31b..393fec6719c554237f5f1c20577654950839b674 100644 --- a/src/test/java/de/tla2b/expression/TestKeywords.java +++ b/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]"); diff --git a/src/test/java/de/tla2b/typechecking/InstanceTest.java b/src/test/java/de/tla2b/typechecking/InstanceTest.java index 0c6ab195279eb77e8958d30baea33310d9301ff3..159380b7acc1d548d65d5f274d069b7699c596eb 100644 --- a/src/test/java/de/tla2b/typechecking/InstanceTest.java +++ b/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"); diff --git a/src/test/resources/typechecking/modules/CounterReal.tla b/src/test/resources/typechecking/modules/CounterReal.tla new file mode 100644 index 0000000000000000000000000000000000000000..3631b5857d8ef0d687ea9bf57b1dcb2d0b5400f4 --- /dev/null +++ b/src/test/resources/typechecking/modules/CounterReal.tla @@ -0,0 +1,10 @@ +-------------------------- MODULE CounterReal ----------------------------- +EXTENDS Reals +CONSTANTS start +VARIABLE x +--------------------------------------------------------------------------- +Init == x = start +Inc == x' = x + 1.0 +Dec == x' = x - 0.99 +Next == Inc \/ Dec +===========================================================================