diff --git a/src/main/java/de/tla2b/analysis/PredicateVsExpression.java b/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
index 1a9cfd7c61d8dc0a5c078e4dbf3e09a5a32335d2..615e60b1245f80617cbf25cd7e23e026c6ad871a 100644
--- a/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
+++ b/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: // <
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index 60404782f67d38a7ab2ae3e0281e5a57f7f11435..385d25c60c6f4dfff807080409ae60e7c3fac8c6 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/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 {
diff --git a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java b/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
index 847533e1ec694053ab8e34f74ff29d50f53e2868..aa02a99d16b85952a920b0a6769591c69b33cf80 100644
--- a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
+++ b/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());
}
}
diff --git a/src/main/java/de/tla2b/config/ModuleOverrider.java b/src/main/java/de/tla2b/config/ModuleOverrider.java
index c9aaf30cdbde8a6f57bb59ca70a854bcbb4735d5..86fb68cdaeee4ca4684f445a5944f66e99229927 100644
--- a/src/main/java/de/tla2b/config/ModuleOverrider.java
+++ b/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
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index f45d754c0c26f0b68aa01f8c3b5ec24177820463..86993b0bc448e3b01fe9b6b322426e9518d2a195 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/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) {