diff --git a/src/main/java/de/tla2bAst/ExpressionTranslator.java b/src/main/java/de/tla2bAst/ExpressionTranslator.java index 7dd9bf0d99e0a2a15f0d1fdd3330a4ef0237641c..76121dfee6cfb553dfe400205b6c53faa28cae61 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 f8fc9f6308008663eb7f55d70bab8254b94b40c9..297a8a6009d517428ab436029148616c7860bcbf 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 }