minor changes

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]);
 				}
@@ -92,7 +82,6 @@ public class PredicateVsExpression extends BuiltInOPs implements ASTConstants,
 		OpDefNode def = (OpDefNode) s.getOperator();
 		if (BBuiltInOPs.contains(def.getName())
 				&& 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);
 	}

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");

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);
 		}
 

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);
 	}