From 50c7f12544869b0822d29385d76df81ca70f3a2b Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Mon, 13 Feb 2023 13:00:34 +0100
Subject: [PATCH] add test
Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
src/main/java/de/tla2bAst/ExpressionTranslator.java | 1 +
.../java/de/tla2b/expression/ComplexExpressionTest.java | 7 +++++++
2 files changed, 8 insertions(+)
diff --git a/src/main/java/de/tla2bAst/ExpressionTranslator.java b/src/main/java/de/tla2bAst/ExpressionTranslator.java
index 7dd9bf0..76121df 100644
--- a/src/main/java/de/tla2bAst/ExpressionTranslator.java
+++ b/src/main/java/de/tla2bAst/ExpressionTranslator.java
@@ -216,6 +216,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
searchVarInSyntaxTree(expr);
// this code seems to assume that there is no variable clash between outer and nested variables
+ // I guess the parser will then generate "Multiply-defined symbol ..." errors
for (int i = 0; i < noVariables.size(); i++) {
variables.remove(noVariables.get(i));
}
diff --git a/src/test/java/de/tla2b/expression/ComplexExpressionTest.java b/src/test/java/de/tla2b/expression/ComplexExpressionTest.java
index f8fc9f6..297a8a6 100644
--- a/src/test/java/de/tla2b/expression/ComplexExpressionTest.java
+++ b/src/test/java/de/tla2b/expression/ComplexExpressionTest.java
@@ -84,5 +84,12 @@ public class ComplexExpressionTest {
compareExpr("CHOOSE({x|x:0..100 & x**3 - 20*x**2 + 7*x = 14388})",
"CHOOSE x \\in 0..100: x^3 - 20*x^2 + 7*x = 14388");
}
+ @Test
+ public void testConstraintCHOOSENested() throws Exception {
+ compareExpr("CHOOSE({y|y : 0 .. 100 & y = CHOOSE({x|x : 0 .. 100 & x ** 3 - 20 * x ** 2 + 7 * x = 14388})})",
+ "CHOOSE y \\in 0..100: y = CHOOSE x \\in 0..100: x^3 - 20*x^2 + 7*x = 14388");
+ }
+ // Note that for: CHOOSE x \in 0..100: x = CHOOSE x \in 0..100: x^3 - 20*x^2 + 7*x = 14388
+ // we get an error: Multiply-defined symbol 'x': this definition or declaration conflicts
}
--
GitLab