From 3d4225dd0e8ff5d0c9d503f12336dbaf7f675caf Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Mon, 13 Feb 2023 12:53:21 +0100
Subject: [PATCH] fix issue 293 involving evaluation of CHOOSE expressions
by detecting quantified variables
Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
.../de/tla2bAst/ExpressionTranslator.java | 21 ++++++++++++++++---
.../expression/ComplexExpressionTest.java | 10 +++++++++
2 files changed, 28 insertions(+), 3 deletions(-)
diff --git a/src/main/java/de/tla2bAst/ExpressionTranslator.java b/src/main/java/de/tla2bAst/ExpressionTranslator.java
index 7fd7ee8..7dd9bf0 100644
--- a/src/main/java/de/tla2bAst/ExpressionTranslator.java
+++ b/src/main/java/de/tla2bAst/ExpressionTranslator.java
@@ -214,7 +214,8 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
TreeNode n_operatorDefintion = n_body.heirs()[0];
TreeNode expr = n_operatorDefintion.heirs()[2];
searchVarInSyntaxTree(expr);
-
+
+ // this code seems to assume that there is no variable clash between outer and nested variables
for (int i = 0; i < noVariables.size(); i++) {
variables.remove(noVariables.get(i));
}
@@ -273,10 +274,23 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
noVariables.add(treeNode.heirs()[0].getImage());
break;
}
- case N_UnboundQuant: {
+ case N_UnboundQuant: { // TOOD: check: is this an unbounded quantifier with infinite domain or a quantifier that does not hide the quantified variables?
TreeNode[] children = treeNode.heirs();
for (int i = 1; i < children.length - 2; i = i + 2) {
- // System.out.println(children[i].getImage());
+ // System.out.println("N_UnboundQuant: "+children[i].getImage());
+ }
+ searchVarInSyntaxTree(treeNode.heirs()[children.length - 1]);
+ break;
+ }
+ case N_UnboundOrBoundChoose: { // not sure the format is the same as N_QuantBound
+ TreeNode[] children = treeNode.heirs();
+ for (int i = 1; i < children.length - 2; i = i + 2) {
+ String boundedVar = children[i].getImage();
+ // typically children[i+1] is N_MaybeBound
+ if (!noVariables.contains(boundedVar)) {
+ noVariables.add(boundedVar);
+ //System.out.println("CHOOSE quantified variable: " + boundedVar);
+ }
}
searchVarInSyntaxTree(treeNode.heirs()[children.length - 1]);
break;
@@ -287,6 +301,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
String boundedVar = children[i].getImage();
if (!noVariables.contains(boundedVar)) {
noVariables.add(boundedVar);
+ // System.out.println("N_QuantBound: locally quantified variable" + boundedVar);
}
}
searchVarInSyntaxTree(treeNode.heirs()[children.length - 1]);
diff --git a/src/test/java/de/tla2b/expression/ComplexExpressionTest.java b/src/test/java/de/tla2b/expression/ComplexExpressionTest.java
index 37d5b33..f8fc9f6 100644
--- a/src/test/java/de/tla2b/expression/ComplexExpressionTest.java
+++ b/src/test/java/de/tla2b/expression/ComplexExpressionTest.java
@@ -74,5 +74,15 @@ public class ComplexExpressionTest {
"r = [a |-> [x|->1,y|->TRUE], b |-> 1] "
+ "/\\ r2 = [r EXCEPT !.a.x = 2]");
}
+ @Test
+ public void testConstraint1() throws Exception {
+ compareExpr("x**3 - 20*x**2 + 7*x = 14388",
+ "x^3 - 20*x^2 + 7*x = 14388");
+ }
+ @Test
+ public void testConstraintCHOOSE() throws Exception {
+ 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");
+ }
}
--
GitLab