diff --git a/src/main/java/de/tla2b/analysis/PredicateVsExpression.java b/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
index 2e4c8fe6b168805d46f22813e99a256b1e106a47..a6cf364cd2836e2799cb7a2e6368a65d504f0bcc 100644
--- a/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
+++ b/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
@@ -8,8 +8,6 @@ import tlc2.tool.BuiltInOPs;
import java.util.HashMap;
import java.util.Map;
-import static de.tla2b.global.TranslationGlobals.STANDARD_MODULES;
-
public class PredicateVsExpression extends BuiltInOPs implements BBuildIns {
private final Map<OpDefNode, DefinitionType> definitionsTypeMap = new HashMap<>();
@@ -80,8 +78,7 @@ public class PredicateVsExpression extends BuiltInOPs implements BBuildIns {
private DefinitionType visitUserdefinedOp(OpApplNode s) {
OpDefNode def = (OpDefNode) s.getOperator();
- if (BBuiltInOPs.contains(def.getName())
- && STANDARD_MODULES.contains(def.getSource().getOriginallyDefinedInModuleNode().getName().toString())) {
+ if (BBuiltInOPs.isBBuiltInOp(def)) {
switch (BBuiltInOPs.getOpcode(def.getName())) {
case B_OPCODE_lt: // <
case B_OPCODE_gt: // >
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index bae579cab6bbafcb42dd0f4af91566dbca69da7b..8edc28de13f9f86496cdc60af16780e727aedda1 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -156,12 +156,9 @@ public class TypeChecker extends BuiltInOPs implements BBuildIns, TranslationGlo
private void evalDefinitions(OpDefNode[] opDefs) throws TLA2BException {
for (OpDefNode def : opDefs) {
// Definition in this module
- String moduleName1 = def.getOriginallyDefinedInModuleNode().getName().toString();
- String moduleName2 = def.getSource().getOriginallyDefinedInModuleNode().getName().toString();
-
- if (STANDARD_MODULES.contains(moduleName1) || STANDARD_MODULES.contains(moduleName2)) {
+ String moduleName = def.getOriginallyDefinedInModuleNode().getName().toString();
+ if (STANDARD_MODULES.contains(moduleName) || BBuiltInOPs.isBBuiltInOp(def))
continue;
- }
if (usedDefinitions.contains(def) || bDefinitions.contains(def))
visitOpDefNode(def);
}
@@ -283,8 +280,7 @@ public class TypeChecker extends BuiltInOPs implements BBuildIns, TranslationGlo
OpDefNode def = (OpDefNode) n.getOperator();
// Definition is a BBuilt-in definition
- String sourceModule = def.getSource().getOriginallyDefinedInModuleNode().getName().toString();
- if (BBuiltInOPs.contains(def.getName()) && STANDARD_MODULES.contains(sourceModule)) {
+ if (BBuiltInOPs.isBBuiltInOp(def)) {
return evalBBuiltIns(n, expected);
}
diff --git a/src/main/java/de/tla2b/global/BBuiltInOPs.java b/src/main/java/de/tla2b/global/BBuiltInOPs.java
index 9d17f8e8c1a59960a6309f6a1672d62cba43beec..60633b2122139ca39cb67a2ef673b28e806c3b68 100644
--- a/src/main/java/de/tla2b/global/BBuiltInOPs.java
+++ b/src/main/java/de/tla2b/global/BBuiltInOPs.java
@@ -1,10 +1,13 @@
package de.tla2b.global;
+import tla2sany.semantic.OpDefNode;
import util.UniqueString;
import java.util.HashMap;
import java.util.Map;
+import static de.tla2b.global.TranslationGlobals.STANDARD_MODULES;
+
public class BBuiltInOPs implements BBuildIns {
private static final Map<UniqueString, Integer> B_Opcodes = new HashMap<>();
@@ -61,6 +64,10 @@ public class BBuiltInOPs implements BBuildIns {
return B_Opcodes.containsKey(s);
}
+ public static boolean isBBuiltInOp(OpDefNode def) {
+ return contains(def.getName()) && STANDARD_MODULES.contains(def.getSource().getOriginallyDefinedInModuleNode().getName().toString());
+ }
+
public static int getOpcode(UniqueString s) {
return B_Opcodes.get(s);
}
diff --git a/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java b/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java
index 67b06eb9b81c90c5c5f1e757448b8bfe6cc8be97..a101349b04fa36d66f11782447faea24c861be5a 100644
--- a/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java
+++ b/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java
@@ -14,8 +14,6 @@ import java.util.Collection;
import java.util.HashSet;
import java.util.Set;
-import static de.tla2b.global.TranslationGlobals.STANDARD_MODULES;
-
public class UsedDefinitionsFinder extends AbstractASTVisitor {
private final Set<OpDefNode> usedDefinitions = new HashSet<>();
@@ -82,9 +80,7 @@ public class UsedDefinitionsFinder extends AbstractASTVisitor {
OpDefNode def = (OpDefNode) n.getOperator();
ModuleNode moduleNode = def.getSource().getOriginallyDefinedInModuleNode();
- if (moduleNode.getName().toString().equals("TLA2B"))
- return;
- if (BBuiltInOPs.contains(def.getName()) && STANDARD_MODULES.contains(moduleNode.getName().toString()))
+ if (moduleNode.getName().toString().equals("TLA2B") || BBuiltInOPs.isBBuiltInOp(def))
return;
if (usedDefinitions.add(def)) {
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index e4bdced8e1404706393c91b3d3e70762e0cab20c..89be2a9c2b777b94a45a548c03939788e485a1cb 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -626,8 +626,8 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, BBuil
private PPredicate visitUserdefinedOpPredicate(OpApplNode n) {
OpDefNode def = (OpDefNode) n.getOperator();
- if (BBuiltInOPs.contains(def.getName()) // Operator is a B built-in operator
- && STANDARD_MODULES.contains(def.getSource().getOriginallyDefinedInModuleNode().getName().toString())) {
+ // Operator is a B built-in operator
+ if (BBuiltInOPs.isBBuiltInOp(def)) {
return visitBBuiltInsPredicate(n);
}
if (specAnalyser.getRecursiveFunctions().contains(def)) {
@@ -666,8 +666,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, BBuil
private PExpression visitUserdefinedOpExpression(OpApplNode n) {
OpDefNode def = (OpDefNode) n.getOperator();
// Operator is a B built-in operator
- if (BBuiltInOPs.contains(def.getName())
- && STANDARD_MODULES.contains(def.getSource().getOriginallyDefinedInModuleNode().getName().toString())) {
+ if (BBuiltInOPs.isBBuiltInOp(def)) {
return visitBBuiltInsExpression(n);
}
diff --git a/src/main/java/de/tla2bAst/ExpressionTranslator.java b/src/main/java/de/tla2bAst/ExpressionTranslator.java
index c87b11c4c086d10a95d22698f734ca7f2ef33df1..89e8141eb23b20e2a12ffd723ce8c7adfb402b11 100644
--- a/src/main/java/de/tla2bAst/ExpressionTranslator.java
+++ b/src/main/java/de/tla2bAst/ExpressionTranslator.java
@@ -30,8 +30,6 @@ import java.io.IOException;
import java.util.*;
import java.util.stream.Collectors;
-import static de.tla2b.global.TranslationGlobals.STANDARD_MODULES;
-
public class ExpressionTranslator implements SyntaxTreeConstants {
private final String tlaExpression;
@@ -380,8 +378,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
// nCtx.addSymbolToContext(node.getName(), fromSpec);
// this should be redundant and not necessary:
// TypeChecker.setType(node, TypeChecker.getType(fromSpec));
- } else if (!(BBuiltInOPs.contains(node.getName())
- && STANDARD_MODULES.contains(node.getSource().getOriginallyDefinedInModuleNode().getName().toString()))) {
+ } else if (!BBuiltInOPs.isBBuiltInOp(node)) {
// throw error if def is not included in translation and not a built-in definition
throw new ExpressionTranslationException("Evaluation error:\n"
+ "Definition '" + fromSpec.getName() + "' is not included in the B translation.\n");