diff --git a/src/test/java/de/tla2b/expression/SimpleExpressionTest.java b/src/test/java/de/tla2b/expression/SimpleExpressionTest.java index 391b8cda47a117a3d0e5fba55795a918f8f160bc..91b392a433c89380439c603ed948a4fdd4ce534c 100644 --- a/src/test/java/de/tla2b/expression/SimpleExpressionTest.java +++ b/src/test/java/de/tla2b/expression/SimpleExpressionTest.java @@ -1,5 +1,6 @@ package de.tla2b.expression; +import org.junit.Ignore; import org.junit.Test; import static de.tla2b.util.TestUtil.compareExpr; @@ -26,6 +27,13 @@ public class SimpleExpressionTest { compareExpr("-1 : INTEGER", "-1 \\in Int"); } + // FIXME: real_set(none) vs identifier(none,'Real') + @Ignore + @Test + public void testModulReals() throws Exception { + compareExpr("1 : REAL", "1 \\in Real"); + } + @Test public void testExist() throws Exception { compareExpr("#a.(a : {1} & 2 > 1)", "\\E a \\in {1}: 2 > 1"); diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java index 505bb324f6de888248b7ec1c5c56602860f7bcb2..7269878ae5154c4280d28e9f93b78f86ff2c8990 100644 --- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java +++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java @@ -27,7 +27,7 @@ public class TestModuleNaturals { TestTypeChecker t = TestUtil.typeCheckString(module); assertEquals("BOOL", t.getConstantType("k")); assertEquals("INTEGER", t.getConstantType("k2")); - assertEquals("INTEGER", t.getConstantType("k2")); + assertEquals("INTEGER", t.getConstantType("k3")); } @Test(expected = TypeErrorException.class) diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java new file mode 100644 index 0000000000000000000000000000000000000000..928def9cb3c902a05d9dc6e192b8bdb5866cd241 --- /dev/null +++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java @@ -0,0 +1,143 @@ +package de.tla2b.typechecking.standardmodules; + +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; + + +public class TestModuleReals { + + /* + * Real + */ + @Test + public void unifyReal() throws TLA2BException { + final String module = "-------------- MODULE Testing ----------------\n" + + "EXTENDS Reals \n" + + "CONSTANTS k \n" + + "ASSUME k = Real \n" + "================================="; + TestTypeChecker t = TestUtil.typeCheckString(module); + assertEquals("POW(REAL)", t.getConstantType("k")); + } + + @Test(expected = TypeErrorException.class) + public void unifyErrorReal() throws TLA2BException { + final String module = "-------------- MODULE Testing ----------------\n" + + "EXTENDS Reals \n" + + "ASSUME TRUE \\in Real \n" + + "================================="; + + TestUtil.typeCheckString(module); + } + + // FIXME: support: + @Ignore + /* + * unary minus: -x + */ + @Test + public void unifyUnaryMinusReal() throws TLA2BException { + final String module = "-------------- MODULE Testing ----------------\n" + + "EXTENDS Reals \n" + + "CONSTANTS k, k2 \n" + + "ASSUME k = -k2 \n" + "================================="; + + TestTypeChecker t = TestUtil.typeCheckString(module); + assertEquals("REAL", t.getConstantType("k")); + assertEquals("REAL", t.getConstantType("k2")); + } + + @Test(expected = TypeErrorException.class) + public void unifyErrorUnaryMinusReal() throws TLA2BException { + final String module = "-------------- MODULE Testing ----------------\n" + + "EXTENDS Reals \n" + + "ASSUME TRUE = -1.0 \n" + + "================================="; + TestUtil.typeCheckString(module); + } + + @Test(expected = TypeErrorException.class) + public void testRelationalOperatorsException1() throws + TLA2BException { + final String module = "-------------- MODULE Testing ----------------\n" + + "EXTENDS Reals \n" + + "CONSTANTS k, k2 \n" + + "ASSUME 1.0 = (2 > 1) \n" + "================================="; + TestUtil.typeCheckString(module); + } + + @Test(expected = TypeErrorException.class) + public void testRelationalOperatorsException2() throws + TLA2BException { + final String module = "-------------- MODULE Testing ----------------\n" + + "EXTENDS Reals \n" + + "CONSTANTS k, k2 \n" + + "ASSUME 1.0 = (2.0 > 1) \n" + "================================="; + TestUtil.typeCheckString(module); + } + + @Test(expected = TypeErrorException.class) + public void testRelationalOperatorsException3() throws + TLA2BException { + final String module = "-------------- MODULE Testing ----------------\n" + + "EXTENDS Reals \n" + + "CONSTANTS k, k2 \n" + + "ASSUME 1.0 = (2.0 > 1.0) \n" + "================================="; + TestUtil.typeCheckString(module); + } + + @Test + public void testArithmeticOperators() throws TLA2BException { + final String module = "-------------- MODULE Testing ----------------\n" + + "EXTENDS Naturals \n" + + "ASSUME 2.0 = 1.0 + 1.0 \n" + + "================================="; + TestUtil.typeCheckString(module); + } + + @Test(expected = TypeErrorException.class) + public void testArithmeticOperatorsException1() throws TLA2BException { + final String module = "-------------- MODULE Testing ----------------\n" + + "EXTENDS Naturals \n" + + "ASSUME TRUE = 1.0 + 1.0 \n" + + "================================="; + TestUtil.typeCheckString(module); + } + + @Test(expected = TypeErrorException.class) + public void testArithmeticOperatorsException2() throws TLA2BException { + final String module = "-------------- MODULE Testing ----------------\n" + + "EXTENDS Naturals \n" + + "ASSUME 2.0 = 1.0 + 1 \n" + + "================================="; + TestUtil.typeCheckString(module); + } + + @Test(expected = TypeErrorException.class) + public void testArithmeticOperatorsException3() throws TLA2BException { + final String module = "-------------- MODULE Testing ----------------\n" + + "EXTENDS Naturals \n" + + "ASSUME 2 = 1.0 + 1.0 \n" + + "================================="; + TestUtil.typeCheckString(module); + } + + /* + * Interval operator: x .. y + */ + + @Test(expected = TypeErrorException.class) + public void testDotDotReal() throws TLA2BException { + final String module = "-------------- MODULE Testing ----------------\n" + + "EXTENDS Naturals \n" + + "CONSTANTS k \n" + + "ASSUME k = 1.0 .. 3.0 \n" + + "================================="; + TestUtil.typeCheckString(module); + } +}