diff --git a/src/test/java/de/tla2b/expression/ModuleAndExpressionTest.java b/src/test/java/de/tla2b/expression/ModuleAndExpressionTest.java index 46f69d0844030b35f628866d51d520485aac7fc4..32a886b0cc87003aac6b09ca980ffd45f9f28a84 100644 --- a/src/test/java/de/tla2b/expression/ModuleAndExpressionTest.java +++ b/src/test/java/de/tla2b/expression/ModuleAndExpressionTest.java @@ -16,8 +16,18 @@ public class ModuleAndExpressionTest { compareExprIncludingModel("k = 1", "k = 1", module); } + @Test + public void testVar() throws Exception { + String module = "---- MODULE Testing ----\n" + + "VARIABLES v \n" + + "Init == v = 4.0 \n" + + "Next == v' = 5.0" + + "==============="; + compareExprIncludingModel("v = 4.0", "v = 4.0", module); + } + @Test(expected = ExpressionTranslationException.class) - public void testTypeError() throws Exception { + public void testConTypeError() throws Exception { String module = "---- MODULE Testing ----\n" + "CONSTANTS k \n" + "ASSUME k = 4" @@ -25,6 +35,84 @@ public class ModuleAndExpressionTest { compareExprIncludingModel(null, "k = TRUE", module); } + @Test(expected = ExpressionTranslationException.class) + public void testVarTypeError() throws Exception { + String module = "---- MODULE Testing ----\n" + + "VARIABLES v \n" + + "Init == v = 4.0 \n" + + "Next == v' = 5.0" + + "==============="; + compareExprIncludingModel(null, "v = TRUE", module); + } + + @Test + public void testConAdditionalFreeVariable() throws Exception { + String module = "---- MODULE Testing ----\n" + + "CONSTANTS k \n" + + "ASSUME k = 4" + + "==============="; + compareExprIncludingModel("k = s", "k = s", module); + } + + @Test + public void testVarAdditionalFreeVariable() throws Exception { + String module = "---- MODULE Testing ----\n" + + "VARIABLES v \n" + + "Init == v = 4.0 \n" + + "Next == v' = 5.0" + + "==============="; + compareExprIncludingModel("v = s", "v = s", module); + } + + @Test(expected = ExpressionTranslationException.class) + public void testAdditionalFreeVariableError() throws Exception { + String module = "---- MODULE Testing ----\n" + + "CONSTANTS k \n" + + "ASSUME k = 4" + + "==============="; + compareExprIncludingModel(null, "s = TRUE /\\ k = s", module); + } + + @Test + public void testWithDefinitions() throws Exception { + String module = "---- MODULE Testing ----\n" + + "EXTENDS Naturals \n" + + "CONSTANTS k \n" + + "ASSUME k = 4 \n" + + "InnerDef(b) == b*5 \n" + + "HelpDef(a,b) == a+InnerDef(b) \n" + + "Init == 1 = HelpDef(1,1) \n" // to get defs into translated B definitions + + "==============="; + compareExprIncludingModel("HelpDef(k,k)", "HelpDef(k,k)", module); + } + + @Test + public void testWithDefinitionsAndFreeVariables() throws Exception { + String module = "---- MODULE Testing ----\n" + + "EXTENDS Naturals \n" + + "CONSTANTS k \n" + + "ASSUME k = 4 \n" + + "InnerDef(b) == b*5 \n" + + "HelpDef(a,b) == a+InnerDef(b) \n" + + "SecondDef(x) == x \n" + + "Init == 1.0 = SecondDef(1.0) /\\ 1 = HelpDef(1,1) \n" // to get defs into translated B definitions + + "==============="; + compareExprIncludingModel("s = 5 & t = 10 & w : REAL & v = HelpDef(s,t) & w = SecondDef(s)", + "s = 5 /\\ t = 10 /\\ w \\in Real /\\ v = HelpDef(s,t) /\\ w = SecondDef(s)", module); + } + + @Test(expected = ExpressionTranslationException.class) + public void testWithDefinitionError() throws Exception { + String module = "---- MODULE Testing ----\n" + + "EXTENDS Reals \n" + + "CONSTANTS k \n" + + "ASSUME k = 4.0 \n" + + "HelpDef(a,b) == 0.3*a+2.7*b \n" + + "Init == 1.0 = HelpDef(1.0,1.0) \n" // to get defs into translated B definitions + + "==============="; + compareExprIncludingModel(null, "s \\in Int /\\ HelpDef(k,s)", module); + } + @Test public void testReals() throws Exception { String module = "---- MODULE Testing ----\n"