From 15e1412cfd2fc1ddefbfa25d4747ac4c511bc583 Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Fri, 3 Jan 2025 20:05:19 +0100
Subject: [PATCH] support SetProduct
but not sure if it is used elsewhere (comes from TLA2B module)
---
src/main/java/de/tla2bAst/BAstCreator.java | 13 +++++++++++++
1 file changed, 13 insertions(+)
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 89be2a9..c88eaa6 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -1008,6 +1008,19 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, BBuil
returnNode = sum;
break;
}
+
+ case B_OPCODE_setprod: {
+ AIdentifierExpression variable = createIdentifierNode("t_"); // TODO unused identifier name
+ returnNode = new AGeneralProductExpression(
+ Collections.singletonList(variable.clone()),
+ new AMemberPredicate(
+ variable.clone(),
+ visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0])
+ ),
+ variable.clone()
+ );
+ break;
+ }
}
if (returnNode != null) {
return createPositionedNode(returnNode, opApplNode);
--
GitLab