From a96a70b06ad3e49230fda5c5db5647f96efd0815 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Thu, 17 Dec 2015 13:21:18 +0100
Subject: [PATCH] translating all necessary TLA+ definitions
---
.../de/tla2b/translation/BDefinitionsFinder.java | 12 ++++++++++--
1 file changed, 10 insertions(+), 2 deletions(-)
diff --git a/src/main/java/de/tla2b/translation/BDefinitionsFinder.java b/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
index 93351e8..3c98c6c 100644
--- a/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
+++ b/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
@@ -1,9 +1,11 @@
package de.tla2b.translation;
+import java.util.ArrayList;
import java.util.HashSet;
import tla2sany.semantic.ASTConstants;
import tla2sany.semantic.AssumeNode;
+import tla2sany.semantic.ExprNode;
import tla2sany.semantic.ExprOrOpArgNode;
import tla2sany.semantic.OpApplNode;
import tla2sany.semantic.OpDefNode;
@@ -27,6 +29,13 @@ public class BDefinitionsFinder extends AbstractASTVisitor implements
for (BOperation op : specAnalyser.getBOperations()) {
visitExprNode(op.getNode());
+ ArrayList<OpApplNode> existQuans = op.getExistQuans();
+ for (OpApplNode opApplNode : existQuans) {
+ ExprNode[] bdedQuantBounds = opApplNode.getBdedQuantBounds();
+ for (ExprNode exprNode : bdedQuantBounds) {
+ visitExprNode(exprNode);
+ }
+ }
}
if (specAnalyser.getInits() != null) {
@@ -43,7 +52,6 @@ public class BDefinitionsFinder extends AbstractASTVisitor implements
bDefinitionsSet.add(def);
}
-
HashSet<OpDefNode> temp = new HashSet<OpDefNode>(bDefinitionsSet);
for (OpDefNode opDefNode : temp) {
visitExprNode(opDefNode.getBody());
@@ -52,7 +60,7 @@ public class BDefinitionsFinder extends AbstractASTVisitor implements
public void visitUserDefinedNode(OpApplNode n) {
OpDefNode def = (OpDefNode) n.getOperator();
- if(bDefinitionsSet.add(def)){
+ if (bDefinitionsSet.add(def)) {
visitExprNode(def.getBody());
}
for (ExprOrOpArgNode exprOrOpArgNode : n.getArgs()) {
--
GitLab