minor formatting

src/main/java/de/tla2b/analysis/PredicateVsExpression.java

@@ -29,7 +29,6 @@ public class PredicateVsExpression extends BuiltInOPs implements ASTConstants,
 			DefinitionType type = visitSemanticNode(def.getBody());
 			definitionsTypeMap.put(def, type);
 		}
-
 	}
 
 	private DefinitionType visitSemanticNode(SemanticNode s) {
@@ -42,9 +41,7 @@ public class PredicateVsExpression extends BuiltInOPs implements ASTConstants,
 				LetInNode letInNode = (LetInNode) s;
 				return visitSemanticNode(letInNode.getBody());
 			}
-
 		}
-
 		return DefinitionType.EXPRESSION;
 	}
 
@@ -94,9 +91,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: // <

src/main/java/de/tla2b/analysis/TypeChecker.java

@@ -793,7 +793,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 
 				FunctionType func = new FunctionType(new UntypedType(), new UntypedType());
 				func = (FunctionType) visitExprOrOpArgNode(n.getArgs()[0], func);
-				TLAType res = null;
+				TLAType res;
 				try {
 					res = new SetType(func.getDomain()).unify(expected);
 				} catch (UnificationException e) {
@@ -957,7 +957,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 					setType(param, paramType);
 					list.add(paramType);
 				}
-				TLAType found = null;
+				TLAType found;
 				if (list.size() == 1) {
 					found = list.get(0);
 				} else {
@@ -1063,7 +1063,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 			}
 		}
 
-		TLAType domType = null;
+		TLAType domType;
 		if (domList.size() == 1) {
 			domType = domList.get(0);
 		} else {

src/main/java/de/tla2b/config/ConfigfileEvaluator.java

@@ -104,15 +104,10 @@ public class ConfigfileEvaluator {
 
 		evalInvariants();
 		// check if INVARIANT declarations are valid definitions
-
 		evalConstantOrDefOverrides();
-
 		evalConstantOrOperatorAssignments();
-
 		evalModConOrDefAssignments();
-
 		evalModConOrDefOverrides();
-
 	}
 
 
@@ -127,9 +122,7 @@ public class ConfigfileEvaluator {
 						+ " Module does not contain the definition '"
 						+ next + "'");
 			}
-		} else
-			next = null;
-
+		}
 	}
 
 	private void evalInit() throws ConfigFileErrorException {
@@ -143,10 +136,7 @@ public class ConfigfileEvaluator {
 						+ " Module does not contain the definition '"
 						+ init + "'");
 			}
-		} else {
-			init = null;
 		}
-
 	}
 
 	private void evalSpec() throws ConfigFileErrorException {
@@ -160,8 +150,7 @@ public class ConfigfileEvaluator {
 						+ "Module does not contain the definition '"
 						+ spec + "'");
 			}
-		} else
-			spec = null;
+		}
 	}
 
 	private void evalInvariants() throws ConfigFileErrorException {
@@ -180,7 +169,6 @@ public class ConfigfileEvaluator {
 				}
 			}
 		}
-
 	}
 
 	/**
@@ -303,11 +291,9 @@ public class ConfigfileEvaluator {
 					OpDeclNode c = (OpDeclNode) opDefOrDeclNode;
 					ValueObj valueObj = new ValueObj(symbolValue, symbolType);
 					constantAssignments.put(c, valueObj);
-					/**
-					 * if conValue is a model value and the name of value is the
-					 * same as the name of constants, then the constant
-					 * declaration in the resulting B machine disappears
-					 **/
+					// if conValue is a model value and the name of value is the
+					// same as the name of constants, then the constant
+					// declaration in the resulting B machine disappears
 					if (symbolName.equals(symbolValue.toString())) {
 						bConstantList.remove(c);
 					}
@@ -323,7 +309,6 @@ public class ConfigfileEvaluator {
 					} else if ((symbolType instanceof EnumType)) {
 						operatorModelvalues.add(def);
 					}
-
 				}
 			}
 		}
@@ -332,8 +317,7 @@ public class ConfigfileEvaluator {
 	private void evalModConOrDefOverrides() throws ConfigFileErrorException {
 		// foo <- [Counter] bar or k <- [Counter] bar
 		@SuppressWarnings("unchecked")
-		Hashtable<String, Hashtable<String, String>> configCons = configAst
-			.getModOverrides();
+		Hashtable<String, Hashtable<String, String>> configCons = configAst.getModOverrides();
 		Enumeration<String> moduleNames = configCons.keys();
 		while (moduleNames.hasMoreElements()) {
 			String moduleName = moduleNames.nextElement();
@@ -351,8 +335,7 @@ public class ConfigfileEvaluator {
 							+ ".\n Module does not contain definition "
 							+ right + ".");
 				}
-				OpDefOrDeclNode opDefOrDeclNode = searchDefinitionOrConstant(
-					mNode, left);
+				OpDefOrDeclNode opDefOrDeclNode = searchDefinitionOrConstant(mNode, left);
 
 				if (opDefOrDeclNode instanceof OpDefNode) {
 					// an operator is overridden by another operator
@@ -392,15 +375,12 @@ public class ConfigfileEvaluator {
 					}
 					bConstantList.remove(conNode);
 					constantOverrideTable.put(conNode, rightDefNode);
-
 				}
 			}
-
 		}
 	}
 
-	public ModuleNode searchModule(String moduleName)
-		throws ConfigFileErrorException {
+	public ModuleNode searchModule(String moduleName) throws ConfigFileErrorException {
 		/*
 		 * Search module in extended modules
 		 */
@@ -414,7 +394,6 @@ public class ConfigfileEvaluator {
 		/*
 		 * search module in instanced modules
 		 */
-
 		OpDefNode[] defs = moduleNode.getOpDefs();
 		for (int j = defs.length - 1; j > 0; j--) {
 			OpDefNode def = null;
@@ -434,43 +413,36 @@ public class ConfigfileEvaluator {
 				moduleName));
 	}
 
-	public OpDefOrDeclNode searchDefinitionOrConstant(ModuleNode n,
-	                                                  String defOrConName) throws ConfigFileErrorException {
+	public OpDefOrDeclNode searchDefinitionOrConstant(ModuleNode n, String defOrConName) throws ConfigFileErrorException {
 		for (int i = 0; i < n.getOpDefs().length; i++) {
 			if (n.getOpDefs()[i].getName().toString().equals(defOrConName)) {
 				return n.getOpDefs()[i];
 			}
 		}
 		for (int i = 0; i < n.getConstantDecls().length; i++) {
-			if (n.getConstantDecls()[i].getName().toString()
-				.equals(defOrConName)) {
+			if (n.getConstantDecls()[i].getName().toString().equals(defOrConName)) {
 				return n.getConstantDecls()[i];
 			}
 		}
-		throw new ConfigFileErrorException(
-			"Module does not contain the symbol: " + defOrConName);
+		throw new ConfigFileErrorException("Module does not contain the symbol: " + defOrConName);
 	}
 
 	private TLAType conGetType(Object o) throws ConfigFileErrorException {
 		if (o instanceof IntValue) {
-
 			// IntValue iv = (IntValue) o;
 			return IntType.getInstance();
 		} else if (o.getClass().getName().equals("tlc2.value.impl.SetEnumValue")) {
 			SetEnumValue set = (SetEnumValue) o;
 			SetType t = new SetType(new UntypedType());
 			if (set.isEmpty()) {
-				throw new ConfigFileErrorException(
-					"empty set is not permitted!");
+				throw new ConfigFileErrorException("empty set is not permitted!");
 			}
 			TLAType elemType;
 
-			if (set.elems.elementAt(0).getClass().getName()
-				.equals("tlc2.value.impl.ModelValue")) {
+			if (set.elems.elementAt(0).getClass().getName().equals("tlc2.value.impl.ModelValue")) {
 				EnumType e = new EnumType(new ArrayList<>());
 				for (int i = 0; i < set.size(); i++) {
-					if (set.elems.elementAt(i).getClass().getName()
-						.equals("tlc2.value.impl.ModelValue")) {
+					if (set.elems.elementAt(i).getClass().getName().equals("tlc2.value.impl.ModelValue")) {
 						String mv = set.elems.elementAt(i).toString();
 						if (!enumeratedSet.contains(mv)) {
 							enumeratedSet.add(mv);
@@ -485,9 +457,7 @@ public class ConfigfileEvaluator {
 						}
 
 					} else {
-						throw new ConfigFileErrorException(
-							"Elements of the set must have the same type: "
-								+ o);
+						throw new ConfigFileErrorException("Elements of the set must have the same type: " + o);
 					}
 				}
 				for (String s : e.modelvalues) {
@@ -500,9 +470,7 @@ public class ConfigfileEvaluator {
 					elemType = conGetType(set.elems.elementAt(i));
 					// all Elements have the same Type?
 					if (!t.getSubType().compare(elemType)) {
-						throw new ConfigFileErrorException(
-							"Elements of the set must have the same type: "
-								+ o);
+						throw new ConfigFileErrorException("Elements of the set must have the same type: " + o);
 					}
 				}
 			}
@@ -527,8 +495,7 @@ public class ConfigfileEvaluator {
 		} else if (o.getClass().getName().equals("tlc2.value.impl.BoolValue")) {
 			return BoolType.getInstance();
 		} else {
-			throw new ConfigFileErrorException("Unknown ConstantType: " + o
-				+ " " + o.getClass());
+			throw new ConfigFileErrorException("Unknown ConstantType: " + o + " " + o.getClass());
 		}
 	}
 

src/main/java/de/tla2b/config/ModuleOverrider.java

@@ -114,7 +114,7 @@ public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
 			case ConstantDeclKind: {
 				if (constantOverrideTable.containsKey(s) && s.getArity() > 0) {
 					SymbolNode newOperator = constantOverrideTable.get(s);
-					OpApplNode newNode = null;
+					OpApplNode newNode;
 					try {
 						newNode = new OpApplNode(newOperator, n.getArgs(),
 							n.getTreeNode(), null);
@@ -160,7 +160,7 @@ public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
 					&& !operatorOverrideTable.containsKey(operator))
 					break;
 
-				SymbolNode newOperator = null;
+				SymbolNode newOperator;
 				// IF there are two override statements in the configuration file
 				//(a: Add <- (Rule) Add2, b: R1!Add <- Add3)
 				// TLC uses variant a) overriding the source definition

src/main/java/de/tla2bAst/BAstCreator.java

@@ -144,7 +144,7 @@ public class BAstCreator extends BuiltInOPs
 		for (OpDeclNode con : cons) {
 			TLAType type = (TLAType) con.getToolObject(TYPE_ID);
 
-			EnumType e = null;
+			EnumType e;
 			if (type instanceof SetType) {
 				if (((SetType) type).getSubType() instanceof EnumType) {
 					e = (EnumType) ((SetType) type).getSubType();
@@ -419,7 +419,7 @@ public class BAstCreator extends BuiltInOPs
 			for (Entry<OpDeclNode, OpDefNode> entry : conEval.getConstantOverrideTable().entrySet()) {
 				OpDeclNode con = entry.getKey();
 				OpDefNode generatedDef = entry.getValue();
-				OpDefNode def = null;
+				OpDefNode def;
 				try {
 					OpApplNode opApplNode = (OpApplNode) generatedDef.getBody();
 					if (opApplNode.getKind() == UserDefinedOpKind) {