diff --git a/src/main/java/de/tla2b/analysis/PredicateVsExpression.java b/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
index 615e60b1245f80617cbf25cd7e23e026c6ad871a..672b281128b3a30f391d290d39f87c47b151a701 100644
--- a/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
+++ b/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
@@ -2,16 +2,18 @@ package de.tla2b.analysis;
import de.tla2b.global.BBuildIns;
import de.tla2b.global.BBuiltInOPs;
-import de.tla2b.global.TranslationGlobals;
import tla2sany.semantic.*;
import tlc2.tool.BuiltInOPs;
-import java.util.HashMap;
+import java.util.Arrays;
+import java.util.Map;
+import java.util.stream.Collectors;
-public class PredicateVsExpression extends BuiltInOPs implements ASTConstants,
- BBuildIns, TranslationGlobals {
+import static de.tla2b.global.TranslationGlobals.STANDARD_MODULES;
- private final HashMap<OpDefNode, DefinitionType> definitionsTypeMap;
+public class PredicateVsExpression extends BuiltInOPs implements BBuildIns {
+
+ private final Map<OpDefNode, DefinitionType> definitionsTypeMap;
public enum DefinitionType {
PREDICATE, EXPRESSION
@@ -22,30 +24,22 @@ public class PredicateVsExpression extends BuiltInOPs implements ASTConstants,
}
public PredicateVsExpression(ModuleNode moduleNode) {
- this.definitionsTypeMap = new HashMap<>();
- OpDefNode[] defs = moduleNode.getOpDefs();
-
- for (OpDefNode def : defs) {
- DefinitionType type = visitSemanticNode(def.getBody());
- definitionsTypeMap.put(def, type);
- }
+ this.definitionsTypeMap = Arrays.stream(moduleNode.getOpDefs())
+ .collect(Collectors.toMap(def -> def, def -> visitSemanticNode(def.getBody())));
}
private DefinitionType visitSemanticNode(SemanticNode s) {
switch (s.getKind()) {
- case OpApplKind: {
- return visitOppApplNode((OpApplNode) s);
- }
+ case OpApplKind:
+ return visitOpApplNode((OpApplNode) s);
- case LetInKind: {
- LetInNode letInNode = (LetInNode) s;
- return visitSemanticNode(letInNode.getBody());
- }
+ case LetInKind:
+ return visitSemanticNode(((LetInNode) s).getBody());
}
return DefinitionType.EXPRESSION;
}
- private DefinitionType visitOppApplNode(OpApplNode opApplNode) {
+ private DefinitionType visitOpApplNode(OpApplNode opApplNode) {
int kind = opApplNode.getOperator().getKind();
if (kind == BuiltInKind) {
@@ -63,17 +57,13 @@ public class PredicateVsExpression extends BuiltInOPs implements ASTConstants,
case OPCODE_bf: // \A x \in S : P
case OPCODE_in: // \in
case OPCODE_subseteq: // \subseteq {1,2} <: {1,2,3}
- case OPCODE_unchanged: {
+ case OPCODE_unchanged:
return DefinitionType.PREDICATE;
- }
case OPCODE_ite: // IF THEN ELSE
- {
return visitSemanticNode(opApplNode.getArgs()[1]);
- }
- case OPCODE_case: // CASE p1 -> e1 [] p2 -> e2
- {
+ case OPCODE_case: { // CASE p1 -> e1 [] p2 -> e2
OpApplNode pair = (OpApplNode) opApplNode.getArgs()[0];
return visitSemanticNode(pair.getArgs()[1]);
}
@@ -91,8 +81,7 @@ public class PredicateVsExpression extends BuiltInOPs implements ASTConstants,
private DefinitionType visitUserdefinedOp(OpApplNode s) {
OpDefNode def = (OpDefNode) s.getOperator();
if (BBuiltInOPs.contains(def.getName())
- && STANDARD_MODULES.contains(def.getSource().getOriginallyDefinedInModuleNode().getName().toString())) {
-
+ && STANDARD_MODULES.contains(def.getSource().getOriginallyDefinedInModuleNode().getName().toString())) {
switch (BBuiltInOPs.getOpcode(def.getName())) {
case B_OPCODE_lt: // <
case B_OPCODE_gt: // >
@@ -103,7 +92,6 @@ public class PredicateVsExpression extends BuiltInOPs implements ASTConstants,
default:
return DefinitionType.EXPRESSION;
}
-
}
return getDefinitionType(def);
}
diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index 252d09e62daf21df356e539782a1b080e809f5d1..d2c55237ac925eca3e0d748fa36ea06eb8c42795 100644
--- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java
+++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
@@ -69,7 +69,6 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
public static SpecAnalyser createSpecAnalyserForTlaExpression(ModuleNode m) {
SpecAnalyser specAnalyser = new SpecAnalyser(m);
-
specAnalyser.expressionOpdefNode = m.getOpDefs()[m.getOpDefs().length - 1];
specAnalyser.usedDefinitions.add(specAnalyser.expressionOpdefNode);
specAnalyser.bDefinitionsSet.add(specAnalyser.expressionOpdefNode);
@@ -78,7 +77,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
public static SpecAnalyser createSpecAnalyser(ModuleNode m) {
SpecAnalyser specAnalyser = new SpecAnalyser(m);
- Hashtable<String, OpDefNode> definitions = new Hashtable<>();
+ Map<String, OpDefNode> definitions = new HashMap<>();
for (int i = 0; i < m.getOpDefs().length; i++) {
definitions.put(m.getOpDefs()[i].getName().toString(), m.getOpDefs()[i]);
}
@@ -157,9 +156,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
DebugUtils.printMsg("Detected TLA+ Default Definition " + Name + " for Clause: " + Clause);
}
- public void start()
- throws SemanticErrorException, TLA2BFrontEndException, ConfigFileErrorException, NotImplementedException {
-
+ public void start() throws SemanticErrorException, ConfigFileErrorException, NotImplementedException {
if (spec != null) {
evalSpec();
} else {
@@ -170,7 +167,6 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
for (OpDefNode inv : new ArrayList<>(invariants)) {
try {
OpApplNode opApplNode = (OpApplNode) inv.getBody();
-
OpDefNode opDefNode = (OpDefNode) opApplNode.getOperator();
if (opDefNode.getKind() == UserDefinedOpKind && !BBuiltInOPs.contains(opDefNode.getName())) {
@@ -186,11 +182,8 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
bOperations = new OperationsFinder(this).getBOperations();
DebugUtils.printDebugMsg("Finding used definitions");
- UsedDefinitionsFinder definitionFinder = new UsedDefinitionsFinder(this);
- this.usedDefinitions = definitionFinder.getUsedDefinitions();
-
- BDefinitionsFinder bDefinitionFinder = new BDefinitionsFinder(this);
- this.bDefinitionsSet = bDefinitionFinder.getBDefinitionsSet();
+ this.usedDefinitions = new UsedDefinitionsFinder(this).getUsedDefinitions();
+ this.bDefinitionsSet = new BDefinitionsFinder(this).getBDefinitionsSet();
// usedDefinitions.addAll(bDefinitionsSet);
DebugUtils.printDebugMsg("Computing variable declarations");
diff --git a/src/main/java/de/tla2b/analysis/UsedExternalFunctions.java b/src/main/java/de/tla2b/analysis/UsedExternalFunctions.java
index 6ee67e0f8919dc247cbe2e38927985ba8e1edcf6..80a4a059133a2a152bbabb79dca5225710dd0aa5 100644
--- a/src/main/java/de/tla2b/analysis/UsedExternalFunctions.java
+++ b/src/main/java/de/tla2b/analysis/UsedExternalFunctions.java
@@ -59,8 +59,7 @@ public class UsedExternalFunctions extends AbstractASTVisitor implements BBuildI
usedExternalFunctions.add(EXTERNAL_FUNCTIONS.ASSERT);
}
- ExprNode[] in = n.getBdedQuantBounds();
- for (ExprNode exprNode : in) {
+ for (ExprNode exprNode : n.getBdedQuantBounds()) {
visitExprNode(exprNode);
}
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index a4192f41302cba6de13ea3785ce3d8784a138303..d10764c4cbd79a52daef6fcc34977251f8bd8421 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -176,12 +176,11 @@ public class Translator implements TranslationGlobals {
public Start translate() throws TLA2BException {
InstanceTransformation.run(moduleNode);
- SymbolSorter.sort(moduleNode);
+ SymbolSorter.sort(moduleNode); // what is the benefit of this?
ConfigfileEvaluator conEval = null;
if (modelConfig != null) {
conEval = new ConfigfileEvaluator(modelConfig, moduleNode);
-
ModuleOverrider.run(moduleNode, conEval);
specAnalyser = SpecAnalyser.createSpecAnalyser(moduleNode, conEval);
} else {
@@ -309,6 +308,9 @@ public class Translator implements TranslationGlobals {
return moduleFile;
}
+ /**
+ * external interface (used by prob_java to obtain list, e.g. for ProB2-UI editor)
+ */
public List<File> getModuleFiles() {
return Collections.unmodifiableList(moduleFiles);
}