diff --git a/src/main/java/de/tla2b/analysis/BOperation.java b/src/main/java/de/tla2b/analysis/BOperation.java
index 3a1c3f3087c0d0876a52d886732a6e0175099cda..84fd88d42721a10cbed92dea3dec427d59a7f4ce 100644
--- a/src/main/java/de/tla2b/analysis/BOperation.java
+++ b/src/main/java/de/tla2b/analysis/BOperation.java
@@ -41,7 +41,7 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
private final ArrayList<OpDeclNode> unchangedVariablesList;
private final ArrayList<ExprOrOpArgNode> guards;
private final ArrayList<ExprOrOpArgNode> beforeAfterPredicates;
- private final LinkedHashMap<SymbolNode, ExprOrOpArgNode> assignments = new LinkedHashMap<SymbolNode, ExprOrOpArgNode>();
+ private final LinkedHashMap<SymbolNode, ExprOrOpArgNode> assignments = new LinkedHashMap<>();
private List<OpDeclNode> anyVariables;
private final SpecAnalyser specAnalyser;
@@ -51,11 +51,11 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
this.node = n;
this.existQuans = existQuans;
this.specAnalyser = specAnalyser;
- this.unchangedVariablesList = new ArrayList<OpDeclNode>();
- this.guards = new ArrayList<ExprOrOpArgNode>();
- this.beforeAfterPredicates = new ArrayList<ExprOrOpArgNode>();
- anyVariables = new ArrayList<OpDeclNode>(Arrays.asList(specAnalyser
- .getModuleNode().getVariableDecls()));
+ this.unchangedVariablesList = new ArrayList<>();
+ this.guards = new ArrayList<>();
+ this.beforeAfterPredicates = new ArrayList<>();
+ anyVariables = new ArrayList<>(Arrays.asList(specAnalyser
+ .getModuleNode().getVariableDecls()));
evalParams();
// System.out.println("Construction B Operation for TLA+ action: " + name);
@@ -68,8 +68,8 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
public AOperation getBOperation(BAstCreator bASTCreator) {
bASTCreator.setUnchangedVariablesNames(unchangedVariables);
AOperation operation = new AOperation();
- List<PExpression> paramList = new ArrayList<PExpression>();
- ArrayList<PPredicate> whereList = new ArrayList<PPredicate>();
+ List<PExpression> paramList = new ArrayList<>();
+ ArrayList<PPredicate> whereList = new ArrayList<>();
for (int j = 0; j < this.getFormalParams().size(); j++) {
paramList.add(bASTCreator.createIdentifierNode(this
.getFormalParams().get(j)));
@@ -81,14 +81,14 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
operation.setOpName(BAstCreator.createTIdentifierLiteral(name));
operation.setParameters(paramList);
- operation.setReturnValues(new ArrayList<PExpression>());
+ operation.setReturnValues(new ArrayList<>());
for (ExprOrOpArgNode g : guards) {
whereList.add(bASTCreator.visitExprOrOpArgNodePredicate(g));
}
- ArrayList<PExpression> leftSideOfAssigment = new ArrayList<PExpression>();
- ArrayList<PExpression> rightSideOfAssigment = new ArrayList<PExpression>();
+ ArrayList<PExpression> leftSideOfAssigment = new ArrayList<>();
+ ArrayList<PExpression> rightSideOfAssigment = new ArrayList<>();
for (Entry<SymbolNode, ExprOrOpArgNode> entry : assignments.entrySet()) {
leftSideOfAssigment.add(bASTCreator.createIdentifierNode(entry
.getKey()));
@@ -96,10 +96,10 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
.visitExprOrOpArgNodeExpression(entry.getValue()));
}
AAssignSubstitution assign = new AAssignSubstitution();
- if (anyVariables.size() > 0) { // ANY x_n WHERE P THEN A END
+ if (!anyVariables.isEmpty()) { // ANY x_n WHERE P THEN A END
AAnySubstitution any = new AAnySubstitution();
any = new AAnySubstitution();
- List<PExpression> anyParams = new ArrayList<PExpression>();
+ List<PExpression> anyParams = new ArrayList<>();
for (OpDeclNode var : anyVariables) {
String varName = var.getName().toString();
String nextName = varName + "_n";
@@ -120,7 +120,7 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
any.setWhere(bASTCreator.createConjunction(whereList));
any.setThen(assign);
operation.setOperationBody(any);
- } else if (whereList.size() > 0) { // SELECT P THEN A END
+ } else if (!whereList.isEmpty()) { // SELECT P THEN A END
ASelectSubstitution select = new ASelectSubstitution();
whereList.addAll(createBeforeAfterPredicates(bASTCreator));
for (ExprOrOpArgNode e : beforeAfterPredicates) {
@@ -134,7 +134,7 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
operation.setOperationBody(block);
}
- if (leftSideOfAssigment.size() > 0) {
+ if (!leftSideOfAssigment.isEmpty()) {
assign.setLhsExpression(leftSideOfAssigment);
assign.setRhsExpressions(rightSideOfAssigment);
} else { // skip
@@ -146,7 +146,7 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
private ArrayList<PPredicate> createBeforeAfterPredicates(
BAstCreator bAstCreator) {
- ArrayList<PPredicate> predicates = new ArrayList<PPredicate>();
+ ArrayList<PPredicate> predicates = new ArrayList<>();
for (ExprOrOpArgNode e : beforeAfterPredicates) {
PPredicate body = null;
if (e instanceof OpApplNode) {
@@ -175,8 +175,8 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
private void findAssignments() {
PrimedVariablesFinder primedVariablesFinder = new PrimedVariablesFinder(
beforeAfterPredicates);
- for (ExprOrOpArgNode node : new ArrayList<ExprOrOpArgNode>(
- beforeAfterPredicates)) {
+ for (ExprOrOpArgNode node : new ArrayList<>(
+ beforeAfterPredicates)) {
if (node instanceof OpApplNode) {
OpApplNode opApplNode = (OpApplNode) node;
if (opApplNode.getOperator().getKind() == BuiltInKind) {
@@ -209,7 +209,7 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
}
}
}
- anyVariables = new ArrayList<OpDeclNode>();
+ anyVariables = new ArrayList<>();
Collections.addAll(anyVariables, specAnalyser.getModuleNode().getVariableDecls());
// for (SymbolNode symbol : primedVariablesFinder.getAllVariables()) {
@@ -241,11 +241,10 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
default: {
if (opApplNode.level < 2) {
guards.add(node); // should we be checking nonLeibnizParams is empty ?
- return;
} else {
beforeAfterPredicates.add(node);
- return;
}
+ return;
}
}
@@ -260,15 +259,14 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
}
private void evalParams() {
- opParams = new ArrayList<String>();
- formalParams = new ArrayList<FormalParamNode>();
- for (int i = 0; i < existQuans.size(); i++) {
- OpApplNode n = existQuans.get(i);
+ opParams = new ArrayList<>();
+ formalParams = new ArrayList<>();
+ for (OpApplNode n : existQuans) {
FormalParamNode[][] params = n.getBdedQuantSymbolLists();
- for (int k = 0; k < params.length; k++) {
- for (int j = 0; j < params[k].length; j++) {
- formalParams.add(params[k][j]);
- opParams.add(params[k][j].getName().toString());
+ for (FormalParamNode[] param : params) {
+ for (int j = 0; j < param.length; j++) {
+ formalParams.add(param[j]);
+ opParams.add(param[j].getName().toString());
}
}
}
@@ -293,7 +291,7 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
}
public ArrayList<OpApplNode> getExistQuans() {
- return new ArrayList<OpApplNode>(existQuans);
+ return new ArrayList<>(existQuans);
}
public ArrayList<String> getOpParams() {
@@ -309,7 +307,7 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
}
private void findUnchangedVariables() {
- unchangedVariables = new ArrayList<String>();
+ unchangedVariables = new ArrayList<>();
findUnchangedVaribalesInSemanticNode(node);
}
@@ -402,9 +400,9 @@ class PrimedVariablesFinder extends AbstractASTVisitor {
private Set<SymbolNode> currentSet;
public PrimedVariablesFinder(ArrayList<ExprOrOpArgNode> list) {
- this.all = new HashSet<SymbolNode>();
- this.twiceUsedVariables = new HashSet<SymbolNode>();
- this.table = new Hashtable<SemanticNode, Set<SymbolNode>>();
+ this.all = new HashSet<>();
+ this.twiceUsedVariables = new HashSet<>();
+ this.table = new Hashtable<>();
for (ExprOrOpArgNode exprOrOpArgNode : list) {
findPrimedVariables(exprOrOpArgNode);
@@ -412,16 +410,13 @@ class PrimedVariablesFinder extends AbstractASTVisitor {
}
public void findPrimedVariables(ExprOrOpArgNode n) {
- currentSet = new HashSet<SymbolNode>();
+ currentSet = new HashSet<>();
this.visitExprOrOpArgNode(n);
table.put(n, currentSet);
}
public void visitBuiltInNode(OpApplNode n) {
- switch (getOpCode(n.getOperator().getName())) {
-
- case OPCODE_prime: // prime
- {
+ if (getOpCode(n.getOperator().getName()) == OPCODE_prime) { // prime
if (n.getArgs()[0] instanceof OpApplNode) {
OpApplNode varNode = (OpApplNode) n.getArgs()[0];
SymbolNode var = varNode.getOperator();
@@ -435,12 +430,7 @@ class PrimedVariablesFinder extends AbstractASTVisitor {
}
}
}
-
- default: {
- super.visitBuiltInNode(n);
- }
-
- }
+ super.visitBuiltInNode(n);
}
public Set<SymbolNode> getTwiceUsedVariables() {
diff --git a/src/main/java/de/tla2b/analysis/InstanceTransformation.java b/src/main/java/de/tla2b/analysis/InstanceTransformation.java
index 5ba34975c652f4dc92abba0cc7264f251b9b7f0f..c5732a49fefc50f663bf30d869f856dc03aede48 100644
--- a/src/main/java/de/tla2b/analysis/InstanceTransformation.java
+++ b/src/main/java/de/tla2b/analysis/InstanceTransformation.java
@@ -9,8 +9,8 @@ import util.UniqueString;
public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
- OpDefNode[] defs;
- Hashtable<String, OpDefNode> defsHash;
+ final OpDefNode[] defs;
+ final Hashtable<String, OpDefNode> defsHash;
private final int substitutionId = 11;
@@ -83,9 +83,9 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
SubstInNode substInNode = (SubstInNode) n;
Subst[] subs = substInNode.getSubsts();
- for (int i = 0; i < subs.length; i++) {
- OpDeclNode op = subs[i].getOp();
- ExprOrOpArgNode expr = subs[i].getExpr();
+ for (Subst sub : subs) {
+ OpDeclNode op = sub.getOp();
+ ExprOrOpArgNode expr = sub.getExpr();
op.setToolObject(substitutionId, expr);
}
return generateNewExprNode(substInNode.getBody(), prefix);
diff --git a/src/main/java/de/tla2b/analysis/PredicateVsExpression.java b/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
index 2d51b7c18ec33f0f456dc116203fbc636bc9bcea..6445fdeb86c3b66685981520ed26ce01440acace 100644
--- a/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
+++ b/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
@@ -1,18 +1,13 @@
package de.tla2b.analysis;
-import java.util.HashMap;
-
import de.tla2b.global.BBuildIns;
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.TranslationGlobals;
-import tla2sany.semantic.ASTConstants;
-import tla2sany.semantic.LetInNode;
-import tla2sany.semantic.ModuleNode;
-import tla2sany.semantic.OpApplNode;
-import tla2sany.semantic.OpDefNode;
-import tla2sany.semantic.SemanticNode;
+import tla2sany.semantic.*;
import tlc2.tool.BuiltInOPs;
+import java.util.HashMap;
+
public class PredicateVsExpression extends BuiltInOPs implements ASTConstants,
BBuildIns, TranslationGlobals {
@@ -27,12 +22,11 @@ public class PredicateVsExpression extends BuiltInOPs implements ASTConstants,
}
public PredicateVsExpression(ModuleNode moduleNode) {
- this.definitionsTypeMap = new HashMap<OpDefNode, PredicateVsExpression.DefinitionType>();
+ this.definitionsTypeMap = new HashMap<>();
OpDefNode[] defs = moduleNode.getOpDefs();
- for (int i = 0; i < defs.length; i++) {
- OpDefNode def = defs[i];
- DefinitionType type = visitSemanticNode(defs[i].getBody());
+ for (OpDefNode def : defs) {
+ DefinitionType type = visitSemanticNode(def.getBody());
definitionsTypeMap.put(def, type);
}
diff --git a/src/main/java/de/tla2b/analysis/RecursiveDefinition.java b/src/main/java/de/tla2b/analysis/RecursiveDefinition.java
index 831537b9293070e9c242f280ec4eee850dbe5cd4..58e07e7d03ca8faaf2e536de40080e515a8b6980 100644
--- a/src/main/java/de/tla2b/analysis/RecursiveDefinition.java
+++ b/src/main/java/de/tla2b/analysis/RecursiveDefinition.java
@@ -18,18 +18,13 @@ public class RecursiveDefinition extends BuiltInOPs{
private void evalRecursiveDefinition() throws NotImplementedException {
if (def.getBody() instanceof OpApplNode) {
OpApplNode o = (OpApplNode) def.getBody();
- switch (getOpCode(o.getOperator().getName())) {
- case OPCODE_ite: { // IF THEN ELSE
+ if (getOpCode(o.getOperator().getName()) == OPCODE_ite) {// IF THEN ELSE
ifThenElse = o;
return;
}
- }
- throw new NotImplementedException(
- "Only IF/THEN/ELSE or CASE constructs are supported at the body of a recursive function.");
- } else {
- throw new NotImplementedException(
- "Only IF/THEN/ELSE or CASE constructs are supported at the body of a recursive function.");
}
+ throw new NotImplementedException(
+ "Only IF/THEN/ELSE or CASE constructs are supported at the body of a recursive function.");
}
public OpDefNode getOpDefNode() {
diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index b6229995ad879c4177f6d5df5361f53dfcf0126a..40b765f9c3a2e3bfeb878de20acffeba0d268a9b 100644
--- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java
+++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
@@ -45,12 +45,12 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
// used to check if a b constant has arguments and is not overriden in the
// configfile
- private ArrayList<BOperation> bOperations = new ArrayList<BOperation>();
- private final ArrayList<ExprNode> inits = new ArrayList<ExprNode>();
+ private ArrayList<BOperation> bOperations = new ArrayList<>();
+ private final ArrayList<ExprNode> inits = new ArrayList<>();
- private Set<OpDefNode> bDefinitionsSet = new HashSet<OpDefNode>();
+ private Set<OpDefNode> bDefinitionsSet = new HashSet<>();
// set of OpDefNodes which will appear in the resulting B Machine
- private Set<OpDefNode> usedDefinitions = new HashSet<OpDefNode>();
+ private Set<OpDefNode> usedDefinitions = new HashSet<>();
// definitions which are used for the type inference algorithm
private final Hashtable<OpDefNode, FormalParamNode[]> letParams = new Hashtable<>();
// additional parameters of an let Operator, these parameters are from the
@@ -65,7 +65,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
private SpecAnalyser(ModuleNode m) {
this.moduleNode = m;
- this.bConstants = new ArrayList<OpDeclNode>();
+ this.bConstants = new ArrayList<>();
}
public static SpecAnalyser createSpecAnalyser(ModuleNode m, ConfigfileEvaluator conEval) {
@@ -91,7 +91,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<String, OpDefNode>();
+ Hashtable<String, OpDefNode> definitions = new Hashtable<>();
for (int i = 0; i < m.getOpDefs().length; i++) {
definitions.put(m.getOpDefs()[i].getName().toString(), m.getOpDefs()[i]);
}
@@ -165,7 +165,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
evalNext();
}
- for (OpDefNode inv : new ArrayList<OpDefNode>(invariants)) {
+ for (OpDefNode inv : new ArrayList<>(invariants)) {
try {
OpApplNode opApplNode = (OpApplNode) inv.getBody();
@@ -199,11 +199,10 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
}
// check if there is B constant with arguments.
- for (int i = 0; i < bConstants.size(); i++) {
- OpDeclNode con = bConstants.get(i);
+ for (OpDeclNode con : bConstants) {
if (con.getArity() > 0) {
throw new ConfigFileErrorException(
- String.format("Constant '%s' must be overriden in the configuration file.", con.getName()));
+ String.format("Constant '%s' must be overriden in the configuration file.", con.getName()));
}
}
findRecursiveConstructs();
@@ -229,14 +228,14 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
}
}
- private void evalNext() throws FrontEndException {
+ private void evalNext() {
if (next != null) {
System.out.println("Using TLA+ Next definition to determine B OPERATIONS");
this.nextExpr = next.getBody();
}
}
- public void evalSpec() throws SemanticErrorException, FrontEndException {
+ public void evalSpec() throws SemanticErrorException {
if (spec != null) {
System.out.println("Using TLA+ Spec to determine B INITIALISATION and OPERATIONS");
processConfigSpec(spec.getBody());
@@ -244,7 +243,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
}
- private void processConfigSpec(ExprNode exprNode) throws SemanticErrorException, FrontEndException {
+ private void processConfigSpec(ExprNode exprNode) throws SemanticErrorException {
if (exprNode instanceof OpApplNode) {
OpApplNode opApp = (OpApplNode) exprNode;
ExprOrOpArgNode[] args = opApp.getArgs();
@@ -266,8 +265,8 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
int opcode = BuiltInOPs.getOpCode(opApp.getOperator().getName());
if (opcode == OPCODE_cl || opcode == OPCODE_land) {
- for (int i = 0; i < args.length; i++) {
- this.processConfigSpec((ExprNode) args[i]);
+ for (ExprOrOpArgNode arg : args) {
+ this.processConfigSpec((ExprNode) arg);
}
return;
}
@@ -276,8 +275,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
SemanticNode boxArg = args[0];
if ((boxArg instanceof OpApplNode)
&& BuiltInOPs.getOpCode(((OpApplNode) boxArg).getOperator().getName()) == OPCODE_sa) {
- ExprNode next = (ExprNode) ((OpApplNode) boxArg).getArgs()[0];
- this.nextExpr = next;
+ this.nextExpr = (ExprNode) ((OpApplNode) boxArg).getArgs()[0];
return;
}
}
@@ -295,7 +293,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
}
private void findRecursiveConstructs() throws NotImplementedException {
- Set<OpDefNode> set = new HashSet<OpDefNode>(usedDefinitions);
+ Set<OpDefNode> set = new HashSet<>(usedDefinitions);
for (OpDefNode def : set) {
if (def.getInRecursive()) {
throw new NotImplementedException("Recursive definitions are currently not supported: " + def.getName()
@@ -305,12 +303,10 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
// recursiveDefinitions.add(rd);
} else if (def.getBody() instanceof OpApplNode) {
OpApplNode o = (OpApplNode) def.getBody();
- switch (getOpCode(o.getOperator().getName())) {
- case OPCODE_rfs: { // recursive Function
+ if (getOpCode(o.getOperator().getName()) == OPCODE_rfs) {// recursive Function
bDefinitionsSet.remove(def);
recursiveFunctions.add(def);
}
- }
}
}
}
@@ -332,7 +328,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
}
public Hashtable<OpDefNode, FormalParamNode[]> getLetParams() {
- return new Hashtable<OpDefNode, FormalParamNode[]>(letParams);
+ return new Hashtable<>(letParams);
}
public ArrayList<String> getDefinitionMacros() {
diff --git a/src/main/java/de/tla2b/analysis/SymbolRenamer.java b/src/main/java/de/tla2b/analysis/SymbolRenamer.java
index bc89947fa4573e7dce11432a95784c41b55b7679..a9cd4c0ed320a0afb92400e7f608cda83b1e4269 100644
--- a/src/main/java/de/tla2b/analysis/SymbolRenamer.java
+++ b/src/main/java/de/tla2b/analysis/SymbolRenamer.java
@@ -126,7 +126,7 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
public SymbolRenamer(ModuleNode moduleNode) {
this.moduleNode = moduleNode;
- usedDefinitions = new HashSet<OpDefNode>();
+ usedDefinitions = new HashSet<>();
OpDefNode[] defs = moduleNode.getOpDefs();
usedDefinitions.add(defs[defs.length - 1]);
}
@@ -153,12 +153,12 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
String newName = getOperatorName(def);
globalNames.add(newName);
def.setToolObject(NEW_NAME, newName);
- usedNamesTable.put(def, new HashSet<String>());
+ usedNamesTable.put(def, new HashSet<>());
}
for (int i = 0; i < moduleNode.getAssumptions().length; i++) {
AssumeNode assumeNode = moduleNode.getAssumptions()[i];
- visitNode(assumeNode.getAssume(), new HashSet<String>());
+ visitNode(assumeNode.getAssume(), new HashSet<>());
}
for (int i = moduleNode.getOpDefs().length - 1; i >= 0; i--) {
@@ -188,12 +188,11 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
// Initialize all local definitions (get a new name, get an empty
// list)
- for (int i = 0; i < defs.length; i++) {
- OpDefNode def = defs[i];
+ for (OpDefNode def : defs) {
String newName = getOperatorName(def);
globalNames.add(newName);
def.setToolObject(NEW_NAME, newName);
- usedNamesTable.put(def, new HashSet<String>(usedNames));
+ usedNamesTable.put(def, new HashSet<>(usedNames));
}
// first visit the IN expression
@@ -269,10 +268,10 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
case OPCODE_be: // \E x \in S : P
{
FormalParamNode[][] params = opApplNode.getBdedQuantSymbolLists();
- Set<String> newUsedNames = new HashSet<String>(usedNames);
- for (int i = 0; i < params.length; i++) {
- for (int j = 0; j < params[i].length; j++) {
- FormalParamNode param = params[i][j];
+ Set<String> newUsedNames = new HashSet<>(usedNames);
+ for (FormalParamNode[] formalParamNodes : params) {
+ for (int j = 0; j < formalParamNodes.length; j++) {
+ FormalParamNode param = formalParamNodes[j];
String paramName = param.getName().toString();
String newName = incName(paramName, usedNames);
param.setToolObject(NEW_NAME, newName);
diff --git a/src/main/java/de/tla2b/analysis/SymbolSorter.java b/src/main/java/de/tla2b/analysis/SymbolSorter.java
index 6d64821a5ee690678a7155e9cf191ebbc5e30ea1..2edb0945ddfd11e7f3931433e27fc7c4abc00153 100644
--- a/src/main/java/de/tla2b/analysis/SymbolSorter.java
+++ b/src/main/java/de/tla2b/analysis/SymbolSorter.java
@@ -33,9 +33,8 @@ public class SymbolSorter {
}
public static Hashtable<String, OpDefNode> getDefsHashTable(OpDefNode[] opDefNodes){
- Hashtable<String, OpDefNode> definitions = new Hashtable<String, OpDefNode>();
- for (int i = 0; i < opDefNodes.length; i++) {
- OpDefNode def = opDefNodes[i];
+ Hashtable<String, OpDefNode> definitions = new Hashtable<>();
+ for (OpDefNode def : opDefNodes) {
// Definition in this module
// if (StandardModules.contains(def.getOriginallyDefinedInModuleNode()
// .getName().toString())
@@ -53,27 +52,15 @@ public class SymbolSorter {
class OpDeclNodeComparator implements Comparator<OpDeclNode> {
public int compare(OpDeclNode a, OpDeclNode b) {
- if (a.getUid() < b.getUid())
- return -1;
- if (a.getUid() > b.getUid())
- return 1;
- return 0;
+ return Integer.compare(a.getUid(), b.getUid());
}
}
class OpDefNodeComparator implements Comparator<OpDefNode> {
public int compare(OpDefNode a, OpDefNode b) {
if (a.getLocation().equals(b.getLocation())) {
- if (a.getSource().getUid() < b.getSource().getUid())
- return -1;
- if (a.getSource().getUid() > b.getSource().getUid())
- return 1;
- return 0;
+ return Integer.compare(a.getSource().getUid(), b.getSource().getUid());
}
- if (a.getUid() < b.getUid())
- return -1;
- if (a.getUid() > b.getUid())
- return 1;
- return 0;
+ return Integer.compare(a.getUid(), b.getUid());
}
}
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index 3b48ec81c3ce4752cb765e4a0bab59982b34b5aa..4f7e1be7ca2c0926716921fc1291d5909952e6b2 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -28,8 +28,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
private final Set<OpDefNode> usedDefinitions;
private final Set<OpDefNode> bDefinitions;
- private final ArrayList<SymbolNode> symbolNodeList = new ArrayList<SymbolNode>();
- private final ArrayList<SemanticNode> tupleNodeList = new ArrayList<SemanticNode>();
+ private final ArrayList<SymbolNode> symbolNodeList = new ArrayList<>();
+ private final ArrayList<SemanticNode> tupleNodeList = new ArrayList<>();
private final ModuleNode moduleNode;
private ArrayList<OpDeclNode> bConstList;
@@ -58,7 +58,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
public TypeChecker(ModuleNode moduleNode, SpecAnalyser specAnalyser) {
this.moduleNode = moduleNode;
this.specAnalyser = specAnalyser;
- Set<OpDefNode> usedDefinitions = new HashSet<OpDefNode>();
+ Set<OpDefNode> usedDefinitions = new HashSet<>();
OpDefNode[] defs = moduleNode.getOpDefs();
// used the last definition of the module
usedDefinitions.add(defs[defs.length - 1]);
@@ -69,8 +69,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
public void start() throws TLA2BException {
OpDeclNode[] cons = moduleNode.getConstantDecls();
- for (int i = 0; i < cons.length; i++) {
- OpDeclNode con = cons[i];
+ for (OpDeclNode con : cons) {
if (constantAssignments != null && constantAssignments.containsKey(con)) {
TLAType t = constantAssignments.get(con).getType();
@@ -86,8 +85,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
OpDeclNode[] vars = moduleNode.getVariableDecls();
- for (int i = 0; i < vars.length; i++) {
- OpDeclNode var = vars[i];
+ for (OpDeclNode var : vars) {
UntypedType u = new UntypedType();
var.setToolObject(TYPE_ID, u);
u.addFollower(var);
@@ -96,9 +94,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
evalDefinitions(moduleNode.getOpDefs());
if (conEval != null) {
- Iterator<Entry<OpDeclNode, OpDefNode>> iter = conEval.getConstantOverrideTable().entrySet().iterator();
- while (iter.hasNext()) {
- Entry<OpDeclNode, OpDefNode> entry = iter.next();
+ for (Entry<OpDeclNode, OpDefNode> entry : conEval.getConstantOverrideTable().entrySet()) {
OpDeclNode con = entry.getKey();
if (!bConstList.contains(con)) {
continue;
@@ -112,7 +108,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
con.setToolObject(TYPE_ID, result);
} catch (UnificationException e) {
throw new TypeErrorException(
- String.format("Expected %s, found %s at constant '%s'.", defType, conType, con.getName()));
+ String.format("Expected %s, found %s at constant '%s'.", defType, conType, con.getName()));
}
}
}
@@ -120,8 +116,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
evalAssumptions(moduleNode.getAssumptions());
if (inits != null) {
- for (int i = 0; i < inits.size(); i++) {
- visitExprNode(inits.get(i), BoolType.getInstance());
+ for (ExprNode init : inits) {
+ visitExprNode(init, BoolType.getInstance());
}
}
@@ -136,25 +132,23 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
private void checkIfAllIdentifiersHaveAType() throws TypeErrorException {
// check if a variable has no type
OpDeclNode[] vars = moduleNode.getVariableDecls();
- for (int i = 0; i < vars.length; i++) {
- OpDeclNode var = vars[i];
+ for (OpDeclNode var : vars) {
TLAType varType = (TLAType) var.getToolObject(TYPE_ID);
if (varType.isUntyped()) {
throw new TypeErrorException(
- "The type of the variable '" + var.getName() + "' can not be inferred: " + varType);
+ "The type of the variable '" + var.getName() + "' can not be inferred: " + varType);
}
}
// check if a constant has no type, only constants which will appear in
// the resulting B Machine are considered
OpDeclNode[] cons = moduleNode.getConstantDecls();
- for (int i = 0; i < cons.length; i++) {
- OpDeclNode con = cons[i];
+ for (OpDeclNode con : cons) {
if (bConstList == null || bConstList.contains(con)) {
TLAType conType = (TLAType) con.getToolObject(TYPE_ID);
if (conType.isUntyped()) {
throw new TypeErrorException(
- "The type of constant " + con.getName() + " is still untyped: " + conType);
+ "The type of constant " + con.getName() + " is still untyped: " + conType);
}
}
}
@@ -177,8 +171,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
private void evalDefinitions(OpDefNode[] opDefs) throws TLA2BException {
- for (int i = 0; i < opDefs.length; i++) {
- OpDefNode def = opDefs[i];
+ for (OpDefNode def : opDefs) {
// Definition in this module
String moduleName1 = def.getOriginallyDefinedInModuleNode().getName().toString();
String moduleName2 = def.getSource().getOriginallyDefinedInModuleNode().getName().toString();
@@ -839,7 +832,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
*/
case OPCODE_cp: // $CartesianProd A \X B \X C as $CartesianProd(A, B, C)
{
- ArrayList<TLAType> list = new ArrayList<TLAType>();
+ ArrayList<TLAType> list = new ArrayList<>();
for (int i = 0; i < n.getArgs().length; i++) {
SetType t = (SetType) visitExprOrOpArgNode(n.getArgs()[i], new SetType(new UntypedType()));
list.add(t.getSubType());
@@ -956,7 +949,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
case OPCODE_uc: {
- List<TLAType> list = new ArrayList<TLAType>();
+ List<TLAType> list = new ArrayList<>();
for (FormalParamNode param : n.getUnbdedQuantSymbols()) {
TLAType paramType = new UntypedType();
symbolNodeList.add(param);
@@ -1096,7 +1089,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
TLAType valueType = visitExprOrOpArgNode(rightside, untyped);
OpApplNode seq = (OpApplNode) leftside;
- LinkedList<ExprOrOpArgNode> list = new LinkedList<ExprOrOpArgNode>();
+ LinkedList<ExprOrOpArgNode> list = new LinkedList<>();
Collections.addAll(list, seq.getArgs());
ExprOrOpArgNode first = list.poll();
@@ -1118,7 +1111,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
TLAType rangeType;
if (domExpr instanceof OpApplNode
&& ((OpApplNode) domExpr).getOperator().getName().toString().equals("$Tuple")) {
- ArrayList<TLAType> domList = new ArrayList<TLAType>();
+ ArrayList<TLAType> domList = new ArrayList<>();
OpApplNode domOpAppl = (OpApplNode) domExpr;
for (int j = 0; j < domOpAppl.getArgs().length; j++) {
TLAType d = visitExprOrOpArgNode(domOpAppl.getArgs()[j], new UntypedType());
@@ -1144,7 +1137,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
private TLAType evalType(LinkedList<ExprOrOpArgNode> list, TLAType valueType) throws TLA2BException {
- if (list.size() == 0) {
+ if (list.isEmpty()) {
return valueType;
}
ExprOrOpArgNode head = list.poll();
@@ -1514,7 +1507,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
SetType set = new SetType(new TupleType(2));
set = (SetType) visitExprOrOpArgNode(n.getArgs()[0], set);
TupleType t = (TupleType) set.getSubType();
- ArrayList<TLAType> list = new ArrayList<TLAType>();
+ ArrayList<TLAType> list = new ArrayList<>();
list.add(t.getTypes().get(1));
list.add(t.getTypes().get(0));
SetType found = new SetType(new TupleType(list));
diff --git a/src/main/java/de/tla2b/analysis/UsedExternalFunctions.java b/src/main/java/de/tla2b/analysis/UsedExternalFunctions.java
index 13144429def5038da832e7ee8c362ae994a0452d..8d31a3b77f3ebf2ee7c5adf8b093cee0f55e9284 100644
--- a/src/main/java/de/tla2b/analysis/UsedExternalFunctions.java
+++ b/src/main/java/de/tla2b/analysis/UsedExternalFunctions.java
@@ -25,7 +25,7 @@ public class UsedExternalFunctions extends AbstractASTVisitor implements BBuildI
public UsedExternalFunctions(ModuleNode moduleNode,
SpecAnalyser specAnalyser) {
- usedExternalFunctions = new HashSet<UsedExternalFunctions.EXTERNAL_FUNCTIONS>();
+ usedExternalFunctions = new HashSet<>();
visitAssumptions(moduleNode.getAssumptions());
@@ -62,12 +62,9 @@ public class UsedExternalFunctions extends AbstractASTVisitor implements BBuildI
@Override
public void visitBBuiltinsNode(OpApplNode n) {
- switch (BBuiltInOPs.getOpcode(n.getOperator().getName())) {
-
- case B_OPCODE_assert: {
+ if (BBuiltInOPs.getOpcode(n.getOperator().getName()) == B_OPCODE_assert) {
usedExternalFunctions.add(EXTERNAL_FUNCTIONS.ASSERT);
}
- }
ExprNode[] in = n.getBdedQuantBounds();
diff --git a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java b/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
index 481b165d9c58295271d4c3f95d7206de9d10476d..c01d402071446518e5d868c2c096c86dc2bf3eac 100644
--- a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
+++ b/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
@@ -4,7 +4,6 @@ import java.util.ArrayList;
import java.util.Enumeration;
import java.util.HashSet;
import java.util.Hashtable;
-import java.util.Iterator;
import java.util.LinkedHashMap;
import java.util.Map;
@@ -40,7 +39,7 @@ public class ConfigfileEvaluator {
private OpDefNode specNode; // SPECIFICATION node, may be null
private OpDefNode nextNode; // NEXT node, may be null
private OpDefNode initNode; // INIT node, may be null
- private final ArrayList<OpDefNode> invariantNodeList = new ArrayList<OpDefNode>();
+ private final ArrayList<OpDefNode> invariantNodeList = new ArrayList<>();
private ArrayList<String> enumeratedSet;
private LinkedHashMap<String, EnumType> enumeratedTypes;
public Hashtable<OpDeclNode, ValueObj> constantAssignments;
@@ -51,7 +50,7 @@ public class ConfigfileEvaluator {
private ArrayList<OpDefNode> operatorModelvalues;
- private final ArrayList<OpDeclNode> bConstantList = new ArrayList<OpDeclNode>();
+ private final ArrayList<OpDeclNode> bConstantList = new ArrayList<>();
// List of constants in the resulting B machine. This list does not contain
// a TLA+ constant if the constant is substituted by a modelvalue with the
// same name (the constant name is moved to an enumerated set) or if the
@@ -69,17 +68,17 @@ public class ConfigfileEvaluator {
this.configAst = configAst;
this.moduleNode = moduleNode;
- definitions = new Hashtable<String, OpDefNode>();
+ definitions = new Hashtable<>();
OpDefNode[] defs = moduleNode.getOpDefs();
- for (int i = 0; i < defs.length; i++) {
- definitions.put(defs[i].getName().toString(), defs[i]);
+ for (OpDefNode def : defs) {
+ definitions.put(def.getName().toString(), def);
}
- constants = new Hashtable<String, OpDeclNode>();
+ constants = new Hashtable<>();
OpDeclNode[] cons = moduleNode.getConstantDecls();
- for (int i = 0; i < cons.length; i++) {
- constants.put(cons[i].getName().toString(), cons[i]);
- bConstantList.add(cons[i]);
+ for (OpDeclNode con : cons) {
+ constants.put(con.getName().toString(), con);
+ bConstantList.add(con);
}
initialize();
@@ -90,15 +89,15 @@ public class ConfigfileEvaluator {
}
private void initialize() {
- this.constantOverrideTable = new Hashtable<OpDeclNode, OpDefNode>();
- this.operatorOverrideTable = new Hashtable<OpDefNode, OpDefNode>();
+ this.constantOverrideTable = new Hashtable<>();
+ this.operatorOverrideTable = new Hashtable<>();
- this.constantAssignments = new Hashtable<OpDeclNode, ValueObj>();
- this.operatorAssignments = new Hashtable<OpDefNode, ValueObj>();
- this.operatorModelvalues = new ArrayList<OpDefNode>();
+ this.constantAssignments = new Hashtable<>();
+ this.operatorAssignments = new Hashtable<>();
+ this.operatorModelvalues = new ArrayList<>();
- this.enumeratedSet = new ArrayList<String>();
- this.enumeratedTypes = new LinkedHashMap<String, EnumType>();
+ this.enumeratedSet = new ArrayList<>();
+ this.enumeratedTypes = new LinkedHashMap<>();
}
public void start() throws ConfigFileErrorException {
@@ -129,7 +128,7 @@ public class ConfigfileEvaluator {
private void evalNext() throws ConfigFileErrorException {
String next = configAst.getNext();
- if (!next.equals("")) {
+ if (!next.isEmpty()) {
if (definitions.containsKey(next)) {
this.nextNode = definitions.get(next);
} else {
@@ -145,7 +144,7 @@ public class ConfigfileEvaluator {
private void evalInit() throws ConfigFileErrorException {
String init = configAst.getInit();
- if (!init.equals("")) {
+ if (!init.isEmpty()) {
if (definitions.containsKey(init)) {
this.initNode = definitions.get(init);
} else {
@@ -162,7 +161,7 @@ public class ConfigfileEvaluator {
private void evalSpec() throws ConfigFileErrorException {
String spec = configAst.getSpec();
- if (!spec.equals("")) {
+ if (!spec.isEmpty()) {
if (definitions.containsKey(spec)) {
this.specNode = definitions.get(spec);
} else {
@@ -199,18 +198,16 @@ public class ConfigfileEvaluator {
*/
@SuppressWarnings("unchecked")
private void evalConstantOrDefOverrides() throws ConfigFileErrorException {
- Iterator<Map.Entry<String, String>> it = configAst.getOverrides()
- .entrySet().iterator();
- while (it.hasNext()) {
- Map.Entry<String, String> entry = it.next();
+ for (Map.Entry<String, String> entry : (Iterable<Map.Entry<String, String>>) configAst.getOverrides()
+ .entrySet()) {
String left = entry.getKey();
String right = entry.getValue();
OpDefNode rightDefNode = definitions.get(right);
if (rightDefNode == null) {
throw new ConfigFileErrorException("Invalid substitution for "
- + left + ".\n Module does not contain definition "
- + right + ".");
+ + left + ".\n Module does not contain definition "
+ + right + ".");
}
if (constants.containsKey(left)) {
@@ -218,12 +215,12 @@ public class ConfigfileEvaluator {
OpDeclNode conNode = constants.get(left);
if (conNode.getArity() != rightDefNode.getArity()) {
throw new ConfigFileErrorException(
- String.format(
- "Invalid substitution for %s.%n Constant %s has %s arguments while %s has %s arguments.",
- left, left, conNode.getArity(), right,
- rightDefNode.getArity()));
+ String.format(
+ "Invalid substitution for %s.%n Constant %s has %s arguments while %s has %s arguments.",
+ left, left, conNode.getArity(), right,
+ rightDefNode.getArity()));
}
- if(conNode.getArity()>0){
+ if (conNode.getArity() > 0) {
bConstantList.remove(conNode);
}
constantOverrideTable.put(conNode, rightDefNode);
@@ -232,10 +229,10 @@ public class ConfigfileEvaluator {
OpDefNode defNode = definitions.get(left);
if (defNode.getArity() != rightDefNode.getArity()) {
throw new ConfigFileErrorException(
- String.format(
- "Invalid substitution for %s.%n Operator %s has %s arguments while %s has %s arguments.",
- left, left, defNode.getArity(), right,
- rightDefNode.getArity()));
+ String.format(
+ "Invalid substitution for %s.%n Operator %s has %s arguments while %s has %s arguments.",
+ left, left, defNode.getArity(), right,
+ rightDefNode.getArity()));
}
operatorOverrideTable.put(defNode, rightDefNode);
@@ -244,7 +241,7 @@ public class ConfigfileEvaluator {
// TLA+
// module
throw new ConfigFileErrorException(
- "Module does not contain the symbol: " + left);
+ "Module does not contain the symbol: " + left);
}
}
}
@@ -359,36 +356,32 @@ public class ConfigfileEvaluator {
ModuleNode mNode = searchModule(moduleName);
Hashtable<String, String> o = configCons.get(moduleName);
- Iterator<Map.Entry<String, String>> it = o.entrySet().iterator();
- while (it.hasNext()) {
- Map.Entry<String, String> entry = it.next();
+ for (Map.Entry<String, String> entry : o.entrySet()) {
String left = entry.getKey();
String right = entry.getValue();
OpDefNode rightDefNode = definitions.get(right);
if (rightDefNode == null) {
throw new ConfigFileErrorException(
- "Invalid substitution for " + left
- + ".\n Module does not contain definition "
- + right + ".");
+ "Invalid substitution for " + left
+ + ".\n Module does not contain definition "
+ + right + ".");
}
OpDefOrDeclNode opDefOrDeclNode = searchDefinitionOrConstant(
- mNode, left);
+ mNode, left);
if (opDefOrDeclNode instanceof OpDefNode) {
// an operator is overridden by another operator
OpDefNode defNode = (OpDefNode) opDefOrDeclNode;
if (defNode.getArity() != rightDefNode.getArity()) {
throw new ConfigFileErrorException(
- String.format(
- "Invalid substitution for %s.%n Operator %s has %s arguments while %s has %s arguments.",
- left, left, defNode.getArity(), right,
- rightDefNode.getArity()));
+ String.format(
+ "Invalid substitution for %s.%n Operator %s has %s arguments while %s has %s arguments.",
+ left, left, defNode.getArity(), right,
+ rightDefNode.getArity()));
}
operatorOverrideTable.put(defNode, rightDefNode);
- }
-
- else {
+ } else {
InstanceNode[] instanceNodes = moduleNode.getInstances();
for (int i = 0; i < instanceNodes.length; i++) {
// if (instanceNodes[i].getModule().getName().toString()
@@ -408,10 +401,10 @@ public class ConfigfileEvaluator {
OpDeclNode conNode = (OpDeclNode) opDefOrDeclNode;
if (conNode.getArity() != rightDefNode.getArity()) {
throw new ConfigFileErrorException(
- String.format(
- "Invalid substitution for %s.%n Constant %s has %s arguments while %s has %s arguments.",
- left, left, conNode.getArity(), right,
- rightDefNode.getArity()));
+ String.format(
+ "Invalid substitution for %s.%n Constant %s has %s arguments while %s has %s arguments.",
+ left, left, conNode.getArity(), right,
+ rightDefNode.getArity()));
}
bConstantList.remove(conNode);
constantOverrideTable.put(conNode, rightDefNode);
@@ -429,9 +422,7 @@ public class ConfigfileEvaluator {
*/
@SuppressWarnings("unchecked")
HashSet<ModuleNode> extendedModules = moduleNode.getExtendedModuleSet();
- for (Iterator<ModuleNode> iterator = extendedModules.iterator(); iterator
- .hasNext();) {
- ModuleNode m = iterator.next();
+ for (ModuleNode m : extendedModules) {
if (m.getName().toString().equals(moduleName)) {
return m;
}
@@ -493,7 +484,7 @@ public class ConfigfileEvaluator {
if (set.elems.elementAt(0).getClass().getName()
.equals("tlc2.value.ModelValue")) {
- EnumType e = new EnumType(new ArrayList<String>());
+ EnumType e = new EnumType(new ArrayList<>());
for (int i = 0; i < set.size(); i++) {
if (set.elems.elementAt(i).getClass().getName()
.equals("tlc2.value.ModelValue")) {
diff --git a/src/main/java/de/tla2b/config/ModuleOverrider.java b/src/main/java/de/tla2b/config/ModuleOverrider.java
index 398d37c42e4f8e53d30118bbd96e15c78853588c..6a52605db990ca3ee9da9df26a5ebec123b1ee4c 100644
--- a/src/main/java/de/tla2b/config/ModuleOverrider.java
+++ b/src/main/java/de/tla2b/config/ModuleOverrider.java
@@ -42,14 +42,13 @@ public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
public void start() {
OpDefNode[] defs = moduleNode.getOpDefs();
- for (int i = 0; i < defs.length; i++) {
- OpDefNode def = defs[i];
+ for (OpDefNode def : defs) {
if (operatorAssignments.containsKey(def)) {
ExprNode oldExpr = def.getBody();
TLCValueNode valueNode;
try {
valueNode = new TLCValueNode(operatorAssignments.get(def),
- oldExpr.getTreeNode());
+ oldExpr.getTreeNode());
} catch (AbortException e) {
throw new RuntimeException();
}
@@ -59,7 +58,7 @@ public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
TLCValueNode valueNode;
try {
valueNode = new TLCValueNode(operatorAssignments.get(def
- .getSource()), oldExpr.getTreeNode());
+ .getSource()), oldExpr.getTreeNode());
} catch (AbortException e) {
throw new RuntimeException();
}
@@ -68,10 +67,10 @@ public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
}
- for (int i = 0; i < defs.length; i++) {
- OpApplNode res = visitExprNode(defs[i].getBody());
+ for (OpDefNode def : defs) {
+ OpApplNode res = visitExprNode(def.getBody());
if (res != null) {
- defs[i].setBody(res);
+ def.setBody(res);
}
}
diff --git a/src/main/java/de/tla2b/global/BBuiltInOPs.java b/src/main/java/de/tla2b/global/BBuiltInOPs.java
index 3fdbfd37c54bf278b69145f31540db4732a4253e..abaad1295f532a60663d6d2ed14709d9ee7e508b 100644
--- a/src/main/java/de/tla2b/global/BBuiltInOPs.java
+++ b/src/main/java/de/tla2b/global/BBuiltInOPs.java
@@ -7,7 +7,7 @@ import util.UniqueString;
public class BBuiltInOPs implements BBuildIns{
private static final Hashtable<UniqueString, Integer> B_Opcode_Table;
static {
- B_Opcode_Table = new Hashtable<UniqueString, Integer>();
+ B_Opcode_Table = new Hashtable<>();
B_Opcode_Table.put(OP_dotdot, B_OPCODE_dotdot);
B_Opcode_Table.put(OP_plus, B_OPCODE_plus);
B_Opcode_Table.put(OP_minus, B_OPCODE_minus);
diff --git a/src/main/java/de/tla2b/global/OperatorTypes.java b/src/main/java/de/tla2b/global/OperatorTypes.java
index 89990f5fbf0d2903486b6afce8b859bb9e861969..e864f01ed8a26dc767c93bd940cc0c41817daff6 100644
--- a/src/main/java/de/tla2b/global/OperatorTypes.java
+++ b/src/main/java/de/tla2b/global/OperatorTypes.java
@@ -7,7 +7,7 @@ public class OperatorTypes implements ToolGlobals, BBuildIns {
private static final HashSet<Integer> TLA_Predicate_Operators;
private static final HashSet<Integer> BBuiltIn_Predicate_Operators;
static {
- TLA_Predicate_Operators = new HashSet<Integer>();
+ TLA_Predicate_Operators = new HashSet<>();
TLA_Predicate_Operators.add(OPCODE_eq);
TLA_Predicate_Operators.add(OPCODE_land);
TLA_Predicate_Operators.add(OPCODE_lor);
@@ -24,7 +24,7 @@ public class OperatorTypes implements ToolGlobals, BBuildIns {
TLA_Predicate_Operators.add(OPCODE_bf);
TLA_Predicate_Operators.add(OPCODE_noteq);
- BBuiltIn_Predicate_Operators = new HashSet<Integer>();
+ BBuiltIn_Predicate_Operators = new HashSet<>();
BBuiltIn_Predicate_Operators.add(B_OPCODE_lt);
BBuiltIn_Predicate_Operators.add(B_OPCODE_gt);
BBuiltIn_Predicate_Operators.add(B_OPCODE_leq);
diff --git a/src/main/java/de/tla2b/output/Indentation.java b/src/main/java/de/tla2b/output/Indentation.java
index 0131b1fae37f6a1f65981949c50381385ed92e56..e2a1e5a7adbc82532dd2251c8494d2e2f5711bc7 100644
--- a/src/main/java/de/tla2b/output/Indentation.java
+++ b/src/main/java/de/tla2b/output/Indentation.java
@@ -21,10 +21,10 @@ import de.be4.classicalb.core.parser.node.Start;
public class Indentation extends DepthFirstAdapter {
- private final Hashtable<Node, Integer> indentation = new Hashtable<Node, Integer>();
- private final HashSet<Node> newlineMiddle = new HashSet<Node>();
- private final HashSet<Node> nodesWithNewlineAtTheEnd = new HashSet<Node>();
- private final HashSet<Node> indentedNodes = new HashSet<Node>();
+ private final Hashtable<Node, Integer> indentation = new Hashtable<>();
+ private final HashSet<Node> newlineMiddle = new HashSet<>();
+ private final HashSet<Node> nodesWithNewlineAtTheEnd = new HashSet<>();
+ private final HashSet<Node> indentedNodes = new HashSet<>();
public final static String INDENT = " ";
public final static String SPACE = " ";
@@ -51,7 +51,7 @@ public class Indentation extends DepthFirstAdapter {
@Override
public void caseASetsMachineClause(ASetsMachineClause node) {
- List<PSet> copy = new ArrayList<PSet>(node.getSetDefinitions());
+ List<PSet> copy = new ArrayList<>(node.getSetDefinitions());
for (PSet e : copy) {
setIndentation(e, getIndentNumber(node) + 1);
addIndentedNode(e);
@@ -61,8 +61,8 @@ public class Indentation extends DepthFirstAdapter {
@Override
public void caseAConstantsMachineClause(AConstantsMachineClause node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<>(
+ node.getIdentifiers());
for (PExpression e : copy) {
setIndentation(e, getIndentNumber(node) + 1);
addIndentedNode(e);
diff --git a/src/main/java/de/tla2b/output/PrologPrinter.java b/src/main/java/de/tla2b/output/PrologPrinter.java
index feb5726e4f54c8b486aeaf64241e8b17ee034b88..0bc44cab976c90e766a4106249df07b164f6899b 100644
--- a/src/main/java/de/tla2b/output/PrologPrinter.java
+++ b/src/main/java/de/tla2b/output/PrologPrinter.java
@@ -20,13 +20,13 @@ import de.prob.prolog.output.PrologTermOutput;
import de.tla2b.types.TLAType;
public class PrologPrinter {
- RecursiveMachineLoader rml;
- BParser bParser;
- String moduleName;
+ final RecursiveMachineLoader rml;
+ final BParser bParser;
+ final String moduleName;
//private final Map<String, SourcePositions> positions = new HashMap<String, SourcePositions>();
private HashSet<PositionedNode> positions;
- private final List<File> files = new ArrayList<File>();
+ private final List<File> files = new ArrayList<>();
private final Hashtable<Node, TLAType> typeTable;
public PrologPrinter(RecursiveMachineLoader rml, BParser bParser,
diff --git a/src/main/java/de/tla2b/translation/BDefinitionsFinder.java b/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
index 2c7cbc86ef19129f6f05c75a5c9e361de82de806..73eef8311426639f9805b4059cf6adde3373caee 100644
--- a/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
+++ b/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
@@ -49,9 +49,7 @@ public class BDefinitionsFinder extends AbstractASTVisitor implements ASTConstan
visitAssumeNode(assume);
}
- for (OpDefNode def : specAnalyser.getInvariants()) {
- bDefinitionsSet.add(def);
- }
+ bDefinitionsSet.addAll(specAnalyser.getInvariants());
for (OpDefNode opDef : specAnalyser.getModuleNode().getOpDefs()) {
String defName = opDef.getName().toString();
diff --git a/src/main/java/de/tla2b/translation/BMacroHandler.java b/src/main/java/de/tla2b/translation/BMacroHandler.java
index d86a71ac14f4112d6f55b877ab0bedd2755a3547..5cf5e0263f6ccf95536b4557449ace9111da4531 100644
--- a/src/main/java/de/tla2b/translation/BMacroHandler.java
+++ b/src/main/java/de/tla2b/translation/BMacroHandler.java
@@ -16,11 +16,11 @@ import de.tla2b.config.ConfigfileEvaluator;
public class BMacroHandler extends AbstractASTVisitor {
- private final Hashtable<FormalParamNode, String> renamingTable = new Hashtable<FormalParamNode, String>();
+ private final Hashtable<FormalParamNode, String> renamingTable = new Hashtable<>();
public BMacroHandler(SpecAnalyser specAnalyser, ConfigfileEvaluator conEval) {
ModuleNode moduleNode = specAnalyser.getModuleNode();
- ArrayList<OpDefNode> bDefs = new ArrayList<OpDefNode>();
+ ArrayList<OpDefNode> bDefs = new ArrayList<>();
for (int i = 0; i < moduleNode.getOpDefs().length; i++) {
OpDefNode def = moduleNode.getOpDefs()[i];
if (specAnalyser.getUsedDefinitions().contains(def)) {
@@ -45,16 +45,16 @@ public class BMacroHandler extends AbstractASTVisitor {
private HashSet<FormalParamNode> definitionParameters;
private HashSet<FormalParamNode> localVariables;
- private final Hashtable<FormalParamNode, Set<FormalParamNode>> parameterContext = new Hashtable<FormalParamNode, Set<FormalParamNode>>();
+ private final Hashtable<FormalParamNode, Set<FormalParamNode>> parameterContext = new Hashtable<>();
@Override
public void visitDefinition(OpDefNode def) {
- definitionParameters = new HashSet<FormalParamNode>();
+ definitionParameters = new HashSet<>();
definitionParameters.addAll(Arrays.asList(def.getParams()));
for (FormalParamNode param : definitionParameters) {
- parameterContext.put(param, new HashSet<FormalParamNode>());
+ parameterContext.put(param, new HashSet<>());
}
- localVariables = new HashSet<FormalParamNode>();
+ localVariables = new HashSet<>();
visitExprNode(def.getBody());
@@ -64,8 +64,8 @@ public class BMacroHandler extends AbstractASTVisitor {
@Override
public void visitAssumeNode(AssumeNode assumeNode) {
- definitionParameters = new HashSet<FormalParamNode>();
- localVariables = new HashSet<FormalParamNode>();
+ definitionParameters = new HashSet<>();
+ localVariables = new HashSet<>();
visitExprNode(assumeNode.getAssume());
@@ -88,9 +88,9 @@ public class BMacroHandler extends AbstractASTVisitor {
{
FormalParamNode[][] params = n.getBdedQuantSymbolLists();
- HashSet<FormalParamNode> set = new HashSet<FormalParamNode>();
- for (int i = 0; i < params.length; i++) {
- Collections.addAll(set, params[i]);
+ HashSet<FormalParamNode> set = new HashSet<>();
+ for (FormalParamNode[] param : params) {
+ Collections.addAll(set, param);
}
localVariables.addAll(set);
ExprNode[] in = n.getBdedQuantBounds();
@@ -113,7 +113,7 @@ public class BMacroHandler extends AbstractASTVisitor {
}
private Set<String> getStringSet(Set<FormalParamNode> set) {
- HashSet<String> stringSet = new HashSet<String>();
+ HashSet<String> stringSet = new HashSet<>();
for (FormalParamNode formalParamNode : set) {
stringSet.add(formalParamNode.getName().toString());
}
@@ -124,7 +124,7 @@ public class BMacroHandler extends AbstractASTVisitor {
private void addToIllegalParams(Set<FormalParamNode> set) {
if (illegalParams == null) {
- illegalParams = new HashSet<FormalParamNode>(set);
+ illegalParams = new HashSet<>(set);
} else {
illegalParams.addAll(set);
}
@@ -133,7 +133,7 @@ public class BMacroHandler extends AbstractASTVisitor {
private Set<FormalParamNode> getContextOfParam(FormalParamNode param) {
Set<FormalParamNode> set = parameterContext.get(param);
if (set == null) {
- set = new HashSet<FormalParamNode>();
+ set = new HashSet<>();
}
return set;
}
@@ -183,7 +183,7 @@ public class BMacroHandler extends AbstractASTVisitor {
}
}
- Set<String> globalNames = new HashSet<String>();
+ final Set<String> globalNames = new HashSet<>();
private Boolean existingName(String name) {
return globalNames.contains(name);
diff --git a/src/main/java/de/tla2b/translation/OperationsFinder.java b/src/main/java/de/tla2b/translation/OperationsFinder.java
index b51bae3c4dd5639d99838a9674c9c0efb12c8a0f..4ecec301bbb0cf4f9fc10f62e850732d647e199f 100644
--- a/src/main/java/de/tla2b/translation/OperationsFinder.java
+++ b/src/main/java/de/tla2b/translation/OperationsFinder.java
@@ -31,11 +31,11 @@ public class OperationsFinder extends AbstractASTVisitor implements
public OperationsFinder(SpecAnalyser specAnalyser) {
this.specAnalyser = specAnalyser;
- this.bOperations = new ArrayList<BOperation>();
+ this.bOperations = new ArrayList<>();
if (specAnalyser.getNext() != null) {
currentName = "Next";
- exists = new ArrayList<OpApplNode>();
+ exists = new ArrayList<>();
visitExprNode(specAnalyser.getNext());
}
}
@@ -97,26 +97,25 @@ public class OperationsFinder extends AbstractASTVisitor implements
{
if (n.getArgs().length == 1) {
visitExprOrOpArgNode(n.getArgs()[0]);
- return;
} else {
String oldName = currentName;
- ArrayList<OpApplNode> oldExists = new ArrayList<OpApplNode>(
- exists);
+ ArrayList<OpApplNode> oldExists = new ArrayList<>(
+ exists);
for (int i = 0; i < n.getArgs().length; i++) {
- exists = new ArrayList<OpApplNode>(oldExists);
+ exists = new ArrayList<>(oldExists);
currentName = oldName + i;
visitExprOrOpArgNode(n.getArgs()[i]);
}
- return;
}
+ return;
}
case OPCODE_lor: { // logical or: split action further
String oldName = currentName;
- ArrayList<OpApplNode> oldExists = new ArrayList<OpApplNode>(exists);
+ ArrayList<OpApplNode> oldExists = new ArrayList<>(exists);
for (int i = 0; i < n.getArgs().length; i++) {
- exists = new ArrayList<OpApplNode>(oldExists);
+ exists = new ArrayList<>(oldExists);
currentName = oldName+ i;
visitExprOrOpArgNode(n.getArgs()[i]);
}
diff --git a/src/main/java/de/tla2b/translation/RecursiveFunctionHandler.java b/src/main/java/de/tla2b/translation/RecursiveFunctionHandler.java
index 62a0c6370dd6fb5d241516e44a1faef78a0bf046..9e99ac9ec91612f5dea5f57a29b360e0be5688c5 100644
--- a/src/main/java/de/tla2b/translation/RecursiveFunctionHandler.java
+++ b/src/main/java/de/tla2b/translation/RecursiveFunctionHandler.java
@@ -21,8 +21,8 @@ public class RecursiveFunctionHandler extends AbstractASTVisitor {
private ArrayList<FormalParamNode> ignoreParamList;
private ArrayList<SymbolNode> externParams;
- private final HashSet<OpApplNode> recursiveFunctions = new HashSet<OpApplNode>();
- private final Hashtable<SemanticNode, ArrayList<SymbolNode>> additionalParamsTable = new Hashtable<SemanticNode, ArrayList<SymbolNode>>();
+ private final HashSet<OpApplNode> recursiveFunctions = new HashSet<>();
+ private final Hashtable<SemanticNode, ArrayList<SymbolNode>> additionalParamsTable = new Hashtable<>();
public RecursiveFunctionHandler(SpecAnalyser specAnalyser) {
for (OpDefNode recFunc : specAnalyser.getRecursiveFunctions()) {
@@ -30,14 +30,14 @@ public class RecursiveFunctionHandler extends AbstractASTVisitor {
recursiveFunctions.add(body);
FormalParamNode[][] params = body.getBdedQuantSymbolLists();
- paramList = new ArrayList<FormalParamNode>();
+ paramList = new ArrayList<>();
FormalParamNode self = body.getUnbdedQuantSymbols()[0];
paramList.add(self);
- for (int i = 0; i < params.length; i++) {
- Collections.addAll(paramList, params[i]);
+ for (FormalParamNode[] param : params) {
+ Collections.addAll(paramList, param);
}
- externParams = new ArrayList<SymbolNode>();
- ignoreParamList = new ArrayList<FormalParamNode>();
+ externParams = new ArrayList<>();
+ ignoreParamList = new ArrayList<>();
visitExprNode(recFunc.getBody());
paramList = null;
additionalParamsTable.put(body, externParams);
@@ -78,9 +78,9 @@ public class RecursiveFunctionHandler extends AbstractASTVisitor {
case OPCODE_soa: // $SetOfAll Represents {e : p1 \in S, p2,p3 \in S2}
{
FormalParamNode[][] params = n.getBdedQuantSymbolLists();
- HashSet<FormalParamNode> set = new HashSet<FormalParamNode>();
- for (int i = 0; i < params.length; i++) {
- Collections.addAll(set, params[i]);
+ HashSet<FormalParamNode> set = new HashSet<>();
+ for (FormalParamNode[] param : params) {
+ Collections.addAll(set, param);
}
ignoreParamList.addAll(set);
ExprNode[] in = n.getBdedQuantBounds();
diff --git a/src/main/java/de/tla2b/types/AbstractHasFollowers.java b/src/main/java/de/tla2b/types/AbstractHasFollowers.java
index d6538265bfefdf8b638e26a08489327d260c1ae9..2df11969f008516b6dc7f0896dc3bed5bdcdeafc 100644
--- a/src/main/java/de/tla2b/types/AbstractHasFollowers.java
+++ b/src/main/java/de/tla2b/types/AbstractHasFollowers.java
@@ -1,6 +1,8 @@
package de.tla2b.types;
import java.util.ArrayList;
+import java.util.List;
+
import tla2sany.semantic.SemanticNode;
public abstract class AbstractHasFollowers extends TLAType {
@@ -9,7 +11,7 @@ public abstract class AbstractHasFollowers extends TLAType {
public AbstractHasFollowers(int t) {
super(t);
- followers = new ArrayList<Object>();
+ followers = new ArrayList<>();
}
public ArrayList<Object> getFollowers() {
@@ -19,8 +21,8 @@ public abstract class AbstractHasFollowers extends TLAType {
public void addFollower(Object o) {
// only (partial) untyped types need follower
if (this.followers != null) {
- for (int i = 0; i < followers.size(); i++) {
- if (followers.get(i) == o)
+ for (Object follower : followers) {
+ if (follower == o)
return;
}
followers.add(o);
@@ -47,9 +49,8 @@ public abstract class AbstractHasFollowers extends TLAType {
protected void setFollowersTo(TLAType newType) {
if (this.followers == null)
return;
- for (int i = 0; i < this.followers.size(); i++) {
-
- Object follower = this.followers.get(i);
+ // avoid concurrent modification:
+ new ArrayList<>(followers).forEach(follower -> {
if (follower instanceof SemanticNode) {
((SemanticNode) follower).setToolObject(5, newType);
if (newType instanceof AbstractHasFollowers) {
@@ -80,12 +81,12 @@ public abstract class AbstractHasFollowers extends TLAType {
((TupleOrFunction) follower).setNewType(this, newType);
} else {
throw new RuntimeException("Unknown follower type: "
- + follower.getClass());
+ + follower.getClass());
}
- }
+ });
}
public boolean hasFollower() {
- return followers.size() != 0;
+ return !followers.isEmpty();
}
}
diff --git a/src/main/java/de/tla2b/types/EnumType.java b/src/main/java/de/tla2b/types/EnumType.java
index 4d2119fba0bc80884d5546d923b16c8afe6b34a7..36c57cba0b9f42e15f2b4dee5ebf334fbbae43fd 100644
--- a/src/main/java/de/tla2b/types/EnumType.java
+++ b/src/main/java/de/tla2b/types/EnumType.java
@@ -9,13 +9,13 @@ import de.tla2b.output.TypeVisitorInterface;
import de.tla2bAst.BAstCreator;
public class EnumType extends AbstractHasFollowers {
- public LinkedHashSet<String> modelvalues;
+ public final LinkedHashSet<String> modelvalues;
public int id;
private boolean noVal = false;
public EnumType(ArrayList<String> enums) {
super(MODELVALUE);
- modelvalues = new LinkedHashSet<String>(enums);
+ modelvalues = new LinkedHashSet<>(enums);
}
public void setNoVal() {
diff --git a/src/main/java/de/tla2b/types/StructOrFunctionType.java b/src/main/java/de/tla2b/types/StructOrFunctionType.java
index 5b921f8187953efd83528728c3a32d49032c00a9..eb559b04825064a00c5cd377582d6ba7cd5646a8 100644
--- a/src/main/java/de/tla2b/types/StructOrFunctionType.java
+++ b/src/main/java/de/tla2b/types/StructOrFunctionType.java
@@ -14,21 +14,19 @@ public class StructOrFunctionType extends AbstractHasFollowers {
public StructOrFunctionType(String name, TLAType type) {
super(STRUCT_OR_FUNCTION);
- types = new LinkedHashMap<String, TLAType>();
+ types = new LinkedHashMap<>();
types.put(name, type);
}
public StructOrFunctionType() {
super(STRUCT_OR_FUNCTION);
- types = new LinkedHashMap<String, TLAType>();
+ types = new LinkedHashMap<>();
}
public void setNewType(TLAType old, TLAType New) {
Set<Entry<String, TLAType>> set = types.entrySet();
- Iterator<Entry<String, TLAType>> iterator = set.iterator();
- while (iterator.hasNext()) {
- Entry<String, TLAType> entry = iterator.next();
+ for (Entry<String, TLAType> entry : set) {
if (entry.getValue() == old) {
String key = entry.getKey();
if (New instanceof AbstractHasFollowers) {
@@ -64,12 +62,10 @@ public class StructOrFunctionType extends AbstractHasFollowers {
return true;
if (o instanceof StructType) {
StructType s = (StructType) o;
- Iterator<String> thisKeys = types.keySet().iterator();
- while (thisKeys.hasNext()) {
- String fieldName = thisKeys.next();
+ for (String fieldName : types.keySet()) {
if (s.getFields().contains(fieldName)) {
if (!this.types.get(fieldName)
- .compare(s.getType(fieldName))) {
+ .compare(s.getType(fieldName))) {
return false;
}
}
@@ -80,12 +76,10 @@ public class StructOrFunctionType extends AbstractHasFollowers {
if (o instanceof StructOrFunctionType) {
StructOrFunctionType s = (StructOrFunctionType) o;
- Iterator<String> thisKeys = types.keySet().iterator();
- while (thisKeys.hasNext()) {
- String fieldName = thisKeys.next();
+ for (String fieldName : types.keySet()) {
if (s.types.containsKey(fieldName)) {
if (!this.types.get(fieldName).compare(
- s.types.get(fieldName))) {
+ s.types.get(fieldName))) {
return false;
}
}
@@ -97,9 +91,7 @@ public class StructOrFunctionType extends AbstractHasFollowers {
@Override
public boolean contains(TLAType o) {
- Iterator<String> thisKeys = types.keySet().iterator();
- while (thisKeys.hasNext()) {
- String fieldName = thisKeys.next();
+ for (String fieldName : types.keySet()) {
TLAType type = this.types.get(fieldName);
if (type.equals(o) || type.contains(o))
return true;
diff --git a/src/main/java/de/tla2b/types/StructType.java b/src/main/java/de/tla2b/types/StructType.java
index 2184cfa21a269600efaf965c1d7e5791fbeea3a8..51120ae9591ddda12cea88893a0075e4f6b3eba7 100644
--- a/src/main/java/de/tla2b/types/StructType.java
+++ b/src/main/java/de/tla2b/types/StructType.java
@@ -25,7 +25,7 @@ public class StructType extends AbstractHasFollowers {
public StructType() {
super(STRUCT);
- types = new LinkedHashMap<String, TLAType>();
+ types = new LinkedHashMap<>();
extensible = false;
incompleteStruct = false;
}
@@ -54,10 +54,8 @@ public class StructType extends AbstractHasFollowers {
public void setNewType(TLAType old, TLAType New) {
Set<Entry<String, TLAType>> set = types.entrySet();
- Iterator<Entry<String, TLAType>> iterator = set.iterator();
- while (iterator.hasNext()) {
- Entry<String, TLAType> entry = iterator.next();
+ for (Entry<String, TLAType> entry : set) {
if (entry.getValue() == old) {
String key = entry.getKey();
if (New instanceof AbstractHasFollowers) {
@@ -71,9 +69,7 @@ public class StructType extends AbstractHasFollowers {
@Override
public boolean isUntyped() {
- Iterator<TLAType> ts = types.values().iterator();
- while (ts.hasNext()) {
- TLAType bType = ts.next();
+ for (TLAType bType : types.values()) {
if (bType.isUntyped())
return true;
}
@@ -93,12 +89,10 @@ public class StructType extends AbstractHasFollowers {
if (o instanceof StructType) {
StructType s = (StructType) o;
- Iterator<String> thisKeys = types.keySet().iterator();
- while (thisKeys.hasNext()) {
- String fieldName = thisKeys.next();
+ for (String fieldName : types.keySet()) {
if (s.types.containsKey(fieldName)) {
if (!this.types.get(fieldName).compare(
- s.types.get(fieldName))) {
+ s.types.get(fieldName))) {
return false;
}
}
@@ -134,9 +128,7 @@ public class StructType extends AbstractHasFollowers {
}
this.extensible = this.extensible || otherStruct.extensible || extendStruct;
- Iterator<String> keys = otherStruct.types.keySet().iterator();
- while (keys.hasNext()) {
- String fieldName = keys.next();
+ for (String fieldName : otherStruct.types.keySet()) {
TLAType sType = otherStruct.types.get(fieldName);
if (this.types.containsKey(fieldName)) {
TLAType res = this.types.get(fieldName).unify(sType);
@@ -160,10 +152,8 @@ public class StructType extends AbstractHasFollowers {
StructType clone = new StructType();
Set<Entry<String, TLAType>> set = this.types.entrySet();
- Iterator<Entry<String, TLAType>> iterator = set.iterator();
- while (iterator.hasNext()) {
- Entry<String, TLAType> entry = iterator.next();
+ for (Entry<String, TLAType> entry : set) {
String field = entry.getKey();
TLAType type = entry.getValue().cloneTLAType();
clone.add(field, type);
@@ -173,20 +163,13 @@ public class StructType extends AbstractHasFollowers {
}
public ArrayList<String> getFields() {
- ArrayList<String> fields = new ArrayList<String>();
- Iterator<String> keys = this.types.keySet().iterator();
- while (keys.hasNext()) {
- String fieldName = keys.next();
- fields.add(fieldName);
- }
+ ArrayList<String> fields = new ArrayList<>(this.types.keySet());
return fields;
}
@Override
public boolean contains(TLAType o) {
- Iterator<TLAType> ts = types.values().iterator();
- while (ts.hasNext()) {
- TLAType bType = ts.next();
+ for (TLAType bType : types.values()) {
if (bType.equals(o) || bType.contains(o))
return true;
}
@@ -213,7 +196,7 @@ public class StructType extends AbstractHasFollowers {
@Override
public PExpression getBNode() {
- List<PRecEntry> recList = new ArrayList<PRecEntry>();
+ List<PRecEntry> recList = new ArrayList<>();
for (Entry<String, TLAType> entry : types.entrySet()) {
ARecEntry rec = new ARecEntry();
rec.setIdentifier(BAstCreator.createIdentifierNode(entry.getKey()));
diff --git a/src/main/java/de/tla2b/types/TupleOrFunction.java b/src/main/java/de/tla2b/types/TupleOrFunction.java
index df6468f3de8a0242c9ed8805f90258e0c1efaa1b..f2fa7a585a1bd0ea8a052317c07bd89bc3254116 100644
--- a/src/main/java/de/tla2b/types/TupleOrFunction.java
+++ b/src/main/java/de/tla2b/types/TupleOrFunction.java
@@ -11,7 +11,7 @@ import de.tla2b.exceptions.UnificationException;
import de.tla2b.output.TypeVisitorInterface;
public class TupleOrFunction extends AbstractHasFollowers {
- private final LinkedHashMap<Integer, TLAType> types = new LinkedHashMap<Integer, TLAType>();
+ private final LinkedHashMap<Integer, TLAType> types = new LinkedHashMap<>();
public TupleOrFunction(Integer index, TLAType type) {
super(TUPLE_OR_FUNCTION);
@@ -75,7 +75,7 @@ public class TupleOrFunction extends AbstractHasFollowers {
} catch (UnificationException e) {
// tuple
boolean isTuple = true;
- ArrayList<TLAType> typeList = new ArrayList<TLAType>();
+ ArrayList<TLAType> typeList = new ArrayList<>();
for (int i = 1; i <= types.keySet().size(); i++) {
if (types.containsKey(i)) {
typeList.add(types.get(i));
@@ -132,7 +132,7 @@ public class TupleOrFunction extends AbstractHasFollowers {
if (index >= 1
&& index <= tupleType.getTypes().size()
&& this.types.get(index).compare(
- tupleType.getTypes().get(index + -1))) {
+ tupleType.getTypes().get(index - 1))) {
} else {
return false;
}
@@ -164,7 +164,7 @@ public class TupleOrFunction extends AbstractHasFollowers {
private static boolean isTupleOrFunction(TupleOrFunction t1,
TupleOrFunction t2) {
- List<TLAType> typeList = new ArrayList<TLAType>();
+ List<TLAType> typeList = new ArrayList<>();
typeList.addAll(t1.types.values());
typeList.addAll(t2.types.values());
return comparable(typeList);
@@ -199,7 +199,7 @@ public class TupleOrFunction extends AbstractHasFollowers {
public TLAType cloneTLAType() {
TupleOrFunction res = new TupleOrFunction();
for (Entry<Integer, TLAType> entry : this.types.entrySet()) {
- res.types.put(Integer.valueOf(entry.getKey().intValue()), entry
+ res.types.put(entry.getKey().intValue(), entry
.getValue().cloneTLAType());
}
return res;
@@ -227,7 +227,7 @@ public class TupleOrFunction extends AbstractHasFollowers {
if (o instanceof TupleType) {
TupleType tupleType = (TupleType) o;
- List<TLAType> typeList = new ArrayList<TLAType>();
+ List<TLAType> typeList = new ArrayList<>();
for (int i = 0; i < tupleType.getTypes().size(); i++) {
if (this.types.containsKey(i + 1)) {
TLAType res = tupleType.getTypes().get(i)
@@ -303,8 +303,8 @@ public class TupleOrFunction extends AbstractHasFollowers {
}
public void setNewType(AbstractHasFollowers oldType, TLAType newType) {
- LinkedHashMap<Integer, TLAType> temp = new LinkedHashMap<Integer, TLAType>(
- types);
+ LinkedHashMap<Integer, TLAType> temp = new LinkedHashMap<>(
+ types);
for (Entry<Integer, TLAType> entry : temp.entrySet()) {
if (entry.getValue().equals(oldType)) {
types.put(entry.getKey(), newType);
@@ -318,7 +318,7 @@ public class TupleOrFunction extends AbstractHasFollowers {
}
public TLAType getFinalType() {
- List<TLAType> list = new ArrayList<TLAType>(this.types.values());
+ List<TLAType> list = new ArrayList<>(this.types.values());
if (comparable(list)) {
FunctionType func = new FunctionType(IntType.getInstance(),
@@ -339,7 +339,7 @@ public class TupleOrFunction extends AbstractHasFollowers {
}
private TLAType update() {
- List<TLAType> list = new ArrayList<TLAType>(this.types.values());
+ List<TLAType> list = new ArrayList<>(this.types.values());
// if (allTyped(list) && comparable(list)) {
// FunctionType func = new FunctionType(IntType.getInstance(),
// new UntypedType());
diff --git a/src/main/java/de/tla2b/types/TupleType.java b/src/main/java/de/tla2b/types/TupleType.java
index b53f6464757d64d175ac5ec391a201975c4c74f0..a5b6ae21a1d9007866da72085977e67c158e2280 100644
--- a/src/main/java/de/tla2b/types/TupleType.java
+++ b/src/main/java/de/tla2b/types/TupleType.java
@@ -18,7 +18,7 @@ public class TupleType extends AbstractHasFollowers {
public TupleType(int size) {
super(TUPLE);
- ArrayList<TLAType> list = new ArrayList<TLAType>();
+ ArrayList<TLAType> list = new ArrayList<>();
for (int i = 0; i < size; i++) {
list.add(new UntypedType());
}
@@ -26,12 +26,12 @@ public class TupleType extends AbstractHasFollowers {
}
public ArrayList<TLAType> getTypes() {
- return new ArrayList<TLAType>(types);
+ return new ArrayList<>(types);
}
public void setTypes(List<TLAType> types) {
this.types = types;
- types = new ArrayList<TLAType>(types);
+ types = new ArrayList<>(types);
for (TLAType tlaType : types) {
if (tlaType instanceof AbstractHasFollowers) {
((AbstractHasFollowers) tlaType).addFollower(this);
@@ -95,7 +95,7 @@ public class TupleType extends AbstractHasFollowers {
@Override
public TLAType cloneTLAType() {
- ArrayList<TLAType> list = new ArrayList<TLAType>();
+ ArrayList<TLAType> list = new ArrayList<>();
for (TLAType tlaType : types) {
list.add(tlaType.cloneTLAType());
}
@@ -146,7 +146,7 @@ public class TupleType extends AbstractHasFollowers {
@Override
public PExpression getBNode() {
- List<PExpression> list = new ArrayList<PExpression>();
+ List<PExpression> list = new ArrayList<>();
for (TLAType t : types) {
list.add(t.getBNode());
}
diff --git a/src/main/java/de/tla2b/util/FileUtils.java b/src/main/java/de/tla2b/util/FileUtils.java
index 374560f2c5a7a673a2f6b6d245ab99723e67d60c..e0c35251a09e3cffae15667eea253573ee206720 100644
--- a/src/main/java/de/tla2b/util/FileUtils.java
+++ b/src/main/java/de/tla2b/util/FileUtils.java
@@ -35,7 +35,7 @@ public class FileUtils {
BufferedReader in = new BufferedReader(new FileReader(fileName));
String str;
while ((str = in.readLine()) != null) {
- res.append(str + "\n");
+ res.append(str).append("\n");
}
in.close();
return res.toString();
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 40317398d2498185668537c9193fb6da0722dc3a..65fafe9fb4e9e6e89c7faf7c94ba066317969c4b 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -27,7 +27,7 @@ public class BAstCreator extends BuiltInOPs
List<PMachineClause> machineClauseList;
ConfigfileEvaluator conEval;
- SpecAnalyser specAnalyser;
+ final SpecAnalyser specAnalyser;
private final PredicateVsExpression predicateVsExpression;
private final BMacroHandler bMacroHandler;
private final RecursiveFunctionHandler recursiveFunctionHandler;
@@ -133,7 +133,7 @@ public class BAstCreator extends BuiltInOPs
return;
ASetsMachineClause setsClause = new ASetsMachineClause();
- ArrayList<EnumType> printed = new ArrayList<EnumType>();
+ ArrayList<EnumType> printed = new ArrayList<>();
OpDeclNode[] cons = moduleNode.getConstantDecls();
for (OpDeclNode con : cons) {
TLAType type = (TLAType) con.getToolObject(TYPE_ID);
@@ -192,7 +192,7 @@ public class BAstCreator extends BuiltInOPs
List<PDefinition> defs = new ArrayList<>(createDefinitionsForExternalFunctions(set));
for (OpDefNode opDefNode : bDefs) {
- List<PExpression> list = new ArrayList<PExpression>();
+ List<PExpression> list = new ArrayList<>();
for (int i = 0; i < opDefNode.getParams().length; i++) {
FormalParamNode p = opDefNode.getParams()[i];
list.add(createIdentifierNode(p));
@@ -406,18 +406,16 @@ public class BAstCreator extends BuiltInOPs
}
}
}
+ AEqualPredicate equal = new AEqualPredicate();
if (isEnum) {
- AEqualPredicate equal = new AEqualPredicate();
equal.setLeft(createIdentifierNode(con));
equal.setRight(createIdentifierNode(((SetType) t).getSubType().toString()));
- propertiesList.add(equal);
} else {
- AEqualPredicate equal = new AEqualPredicate();
equal.setLeft(createIdentifierNode(con));
Value tlcValue = v.getValue();
equal.setRight(createTLCValue(tlcValue));
- propertiesList.add(equal);
}
+ propertiesList.add(equal);
} else {
AMemberPredicate member = new AMemberPredicate();
member.setLeft(createIdentifierNode(con));
@@ -476,7 +474,7 @@ public class BAstCreator extends BuiltInOPs
}
private List<PPredicate> evalRecursiveFunctions() {
- List<PPredicate> propertiesList = new ArrayList<PPredicate>();
+ List<PPredicate> propertiesList = new ArrayList<>();
for (OpDefNode def : specAnalyser.getRecursiveFunctions()) {
AEqualPredicate equals = new AEqualPredicate(createIdentifierNode(def),
visitExprNodeExpression(def.getBody()));
@@ -486,15 +484,15 @@ public class BAstCreator extends BuiltInOPs
}
private List<PPredicate> evalRecursiveDefinitions() {
- List<PPredicate> propertiesList = new ArrayList<PPredicate>();
+ List<PPredicate> propertiesList = new ArrayList<>();
for (RecursiveDefinition recDef : specAnalyser.getRecursiveDefinitions()) {
OpDefNode def = recDef.getOpDefNode();
// TLAType t = (TLAType) def.getToolObject(TYPE_ID);
// OpApplNode ifThenElse = recDef.getIfThenElse();
FormalParamNode[] params = def.getParams();
- ArrayList<PExpression> paramList1 = new ArrayList<PExpression>();
- ArrayList<PPredicate> typeList = new ArrayList<PPredicate>();
+ ArrayList<PExpression> paramList1 = new ArrayList<>();
+ ArrayList<PPredicate> typeList = new ArrayList<>();
// ArrayList<PExpression> paramList2 = new ArrayList<PExpression>();
for (FormalParamNode p : params) {
paramList1.add(createIdentifierNode(p));
@@ -652,7 +650,7 @@ public class BAstCreator extends BuiltInOPs
if (type instanceof FunctionType) {
FunctionType funcType = (FunctionType) type;
PExpression param = visitExprOrOpArgNodeExpression(list.poll());
- List<PExpression> params = new ArrayList<PExpression>();
+ List<PExpression> params = new ArrayList<>();
params.add(param);
AFunctionExpression funCall = new AFunctionExpression();
funCall.setIdentifier(base);
@@ -1115,7 +1113,7 @@ public class BAstCreator extends BuiltInOPs
AMinusOrSetSubtractExpression minus2 = new AMinusOrSetSubtractExpression();
minus2.setLeft(add2);
minus2.setRight(new AIntegerExpression(new TIntegerLiteral("1")));
- ArrayList<PExpression> params = new ArrayList<PExpression>();
+ ArrayList<PExpression> params = new ArrayList<>();
params.add(minus2);
AFunctionExpression func = new AFunctionExpression();
func.setIdentifier(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]));
@@ -1128,7 +1126,7 @@ public class BAstCreator extends BuiltInOPs
case B_OPCODE_assert: {
ADefinitionPredicate pred = new ADefinitionPredicate();
pred.setDefLiteral(new TDefLiteralPredicate("ASSERT_TRUE"));
- ArrayList<PExpression> list = new ArrayList<PExpression>();
+ ArrayList<PExpression> list = new ArrayList<>();
list.add(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]));
list.add(new AStringExpression(new TStringLiteral("Error")));
pred.setParameters(list);
@@ -1201,7 +1199,7 @@ public class BAstCreator extends BuiltInOPs
case OPCODE_cl: // $ConjList
{
- List<PPredicate> list = new ArrayList<PPredicate>();
+ List<PPredicate> list = new ArrayList<>();
for (int i = 0; i < n.getArgs().length; i++) {
list.add(visitExprOrOpArgNodePredicate(n.getArgs()[i]));
}
@@ -1210,7 +1208,7 @@ public class BAstCreator extends BuiltInOPs
case OPCODE_dl: // $DisjList
{
- List<PPredicate> list = new ArrayList<PPredicate>();
+ List<PPredicate> list = new ArrayList<>();
for (int i = 0; i < n.getArgs().length; i++) {
list.add(visitExprOrOpArgNodePredicate(n.getArgs()[i]));
}
@@ -1268,7 +1266,7 @@ public class BAstCreator extends BuiltInOPs
if (n.getArgs().length == 0) {
return new AEmptySetExpression();
} else {
- List<PExpression> list = new ArrayList<PExpression>();
+ List<PExpression> list = new ArrayList<>();
for (int i = 0; i < n.getArgs().length; i++) {
list.add(visitExprOrOpArgNodeExpression(n.getArgs()[i]));
@@ -1329,7 +1327,7 @@ public class BAstCreator extends BuiltInOPs
case OPCODE_sso: { // $SubsetOf Represents {x \in S : P}
FormalParamNode[][] params = n.getBdedQuantSymbolLists();
- List<PExpression> list = new ArrayList<PExpression>();
+ List<PExpression> list = new ArrayList<>();
for (int i = 0; i < params[0].length; i++) {
FormalParamNode p = params[0][i];
list.add(createIdentifierNode(p));
@@ -1345,7 +1343,7 @@ public class BAstCreator extends BuiltInOPs
case OPCODE_soa: { // $SetOfAll Represents {e : p1 \in S, p2,p3 \in S2}
FormalParamNode[][] params = n.getBdedQuantSymbolLists();
List<PExpression> idList = createListOfIdentifier(params);
- List<PPredicate> predList = new ArrayList<PPredicate>();
+ List<PPredicate> predList = new ArrayList<>();
predList.add(visitBoundsOfLocalVariables(n));
final String nameOfTempVariable = "t_";
@@ -1358,7 +1356,7 @@ public class BAstCreator extends BuiltInOPs
exist.setPredicate(createConjunction(predList));
AComprehensionSetExpression compre = new AComprehensionSetExpression();
- List<PExpression> tList = new ArrayList<PExpression>();
+ List<PExpression> tList = new ArrayList<>();
tList.add(createIdentifierNode(nameOfTempVariable));
compre.setIdentifiers(tList);
compre.setPredicates(exist);
@@ -1368,7 +1366,7 @@ public class BAstCreator extends BuiltInOPs
union.setIdentifiers(idList);
union.setPredicates(createConjunction(predList));
ASetExtensionExpression set = new ASetExtensionExpression();
- List<PExpression> list = new ArrayList<PExpression>();
+ List<PExpression> list = new ArrayList<>();
list.add(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
set.setExpressions(list);
union.setExpression(set);
@@ -1380,16 +1378,15 @@ public class BAstCreator extends BuiltInOPs
case OPCODE_fc: // Represents [x \in S |-> e].
case OPCODE_rfs: {
FormalParamNode[][] params = n.getBdedQuantSymbolLists();
- List<PExpression> idList = new ArrayList<PExpression>();
- for (int i = 0; i < params.length; i++) {
- for (int j = 0; j < params[i].length; j++) {
- FormalParamNode p = params[i][j];
+ List<PExpression> idList = new ArrayList<>();
+ for (FormalParamNode[] param : params) {
+ for (FormalParamNode p : param) {
idList.add(createIdentifierNode(p));
}
}
boolean[] isTuple = n.isBdedQuantATuple();
ALambdaExpression lambda = new ALambdaExpression();
- List<PExpression> idList2 = new ArrayList<PExpression>();
+ List<PExpression> idList2 = new ArrayList<>();
for (int i = 0; i < params.length; i++) {
if (isTuple[i] && i > 0) {
StringBuilder sb = new StringBuilder();
@@ -1414,10 +1411,10 @@ public class BAstCreator extends BuiltInOPs
if (recursiveFunctionHandler.isRecursiveFunction(n)) {
ArrayList<SymbolNode> externParams = recursiveFunctionHandler.getAdditionalParams(n);
- if (externParams.size() > 0) {
+ if (!externParams.isEmpty()) {
ALambdaExpression lambda2 = new ALambdaExpression();
- ArrayList<PExpression> shiftedParams = new ArrayList<PExpression>();
- List<PPredicate> predList2 = new ArrayList<PPredicate>();
+ ArrayList<PExpression> shiftedParams = new ArrayList<>();
+ List<PPredicate> predList2 = new ArrayList<>();
for (SymbolNode p : externParams) {
shiftedParams.add(createIdentifierNode(p));
@@ -1446,14 +1443,14 @@ public class BAstCreator extends BuiltInOPs
} else {
AFunctionExpression func = new AFunctionExpression();
func.setIdentifier(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
- List<PExpression> paramList = new ArrayList<PExpression>();
+ List<PExpression> paramList = new ArrayList<>();
ExprOrOpArgNode dom = n.getArgs()[1];
if (dom instanceof OpApplNode
&& ((OpApplNode) dom).getOperator().getName().toString().equals("$Tuple")) {
OpApplNode domOpAppl = (OpApplNode) dom;
if (domOpAppl.getArgs().length == 1) {
- List<PExpression> list = new ArrayList<PExpression>();
+ List<PExpression> list = new ArrayList<>();
list.add(visitExprOrOpArgNodeExpression(domOpAppl.getArgs()[0]));
ASequenceExtensionExpression seq = new ASequenceExtensionExpression(list);
paramList.add(seq);
@@ -1480,7 +1477,7 @@ public class BAstCreator extends BuiltInOPs
visitExprOrOpArgNodeExpression(n.getArgs()[1]));
case OPCODE_tup: { // $Tuple
- List<PExpression> list = new ArrayList<PExpression>();
+ List<PExpression> list = new ArrayList<>();
for (int i = 0; i < n.getArgs().length; i++) {
list.add(visitExprOrOpArgNodeExpression(n.getArgs()[i]));
}
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index bd0efaf09b201e87043bc35572f96a1d3891c82c..2c85ea880d4966e9f983d93dfac905aaec9ac7bd 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -4,7 +4,6 @@ import java.io.BufferedReader;
import java.io.BufferedWriter;
import java.io.File;
import java.io.FileNotFoundException;
-import java.io.FileOutputStream;
import java.io.FileReader;
import java.io.IOException;
import java.io.OutputStreamWriter;
diff --git a/src/test/java/de/tla2b/expression/SimpleExpressionTest.java b/src/test/java/de/tla2b/expression/SimpleExpressionTest.java
index ac8f716bdcd1bae95876e8d82359bec92afb967c..bb9c2e52592ecd813ac30212aedc15a17df5b98f 100644
--- a/src/test/java/de/tla2b/expression/SimpleExpressionTest.java
+++ b/src/test/java/de/tla2b/expression/SimpleExpressionTest.java
@@ -1,6 +1,5 @@
package de.tla2b.expression;
-import org.junit.Ignore;
import org.junit.Test;
import static de.tla2b.util.TestUtil.compareExpr;
diff --git a/src/test/java/de/tla2b/typechecking/BBuiltInsTest.java b/src/test/java/de/tla2b/typechecking/BBuiltInsTest.java
index 477632042a2eeaafe1083335fc8a25f5dd78b6ff..f0847d79f130790b4406c6df0a4b031aaeafaa55 100644
--- a/src/test/java/de/tla2b/typechecking/BBuiltInsTest.java
+++ b/src/test/java/de/tla2b/typechecking/BBuiltInsTest.java
@@ -4,7 +4,6 @@ import static org.junit.Assert.*;
import org.junit.Test;
-import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.exceptions.TypeErrorException;
import de.tla2b.util.TestTypeChecker;
diff --git a/src/test/java/de/tla2b/typechecking/ConfigTest.java b/src/test/java/de/tla2b/typechecking/ConfigTest.java
index 08afa569efd5c3cbe400751ecb32c5e91d9090aa..fbae27a75991e5b4e0714e0a5f8df48247928b9c 100644
--- a/src/test/java/de/tla2b/typechecking/ConfigTest.java
+++ b/src/test/java/de/tla2b/typechecking/ConfigTest.java
@@ -4,7 +4,6 @@ import static org.junit.Assert.assertEquals;
import org.junit.Test;
-import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.util.TestTypeChecker;
import de.tla2b.util.TestUtil;
diff --git a/src/test/java/de/tla2b/typechecking/ConstantTypesTest.java b/src/test/java/de/tla2b/typechecking/ConstantTypesTest.java
index b454878cb39c20d7462937a565b91a395840e8dd..27c2cb966ffed0955f5bfd00d67a01cb4bf7811e 100644
--- a/src/test/java/de/tla2b/typechecking/ConstantTypesTest.java
+++ b/src/test/java/de/tla2b/typechecking/ConstantTypesTest.java
@@ -4,7 +4,6 @@ import static org.junit.Assert.*;
import org.junit.Test;
-import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.exceptions.TypeErrorException;
import de.tla2b.util.TestTypeChecker;
diff --git a/src/test/java/de/tla2b/typechecking/DefinitionsTest.java b/src/test/java/de/tla2b/typechecking/DefinitionsTest.java
index 1eaf7afe62d3df216c98950b5204b5fa842d8588..444012592c452a88c9ccd102e1e0af7205c6a672 100644
--- a/src/test/java/de/tla2b/typechecking/DefinitionsTest.java
+++ b/src/test/java/de/tla2b/typechecking/DefinitionsTest.java
@@ -4,7 +4,6 @@ import static org.junit.Assert.*;
import org.junit.Test;
-import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.util.TestTypeChecker;
import de.tla2b.util.TestUtil;
diff --git a/src/test/java/de/tla2b/typechecking/ExceptTest.java b/src/test/java/de/tla2b/typechecking/ExceptTest.java
index 0eaf918b5c13499807f9deff2e02db77ea7de29e..360d0fdd2f4998c62c811ce11bf3478ce9e34c80 100644
--- a/src/test/java/de/tla2b/typechecking/ExceptTest.java
+++ b/src/test/java/de/tla2b/typechecking/ExceptTest.java
@@ -4,7 +4,6 @@ import static org.junit.Assert.assertEquals;
import org.junit.Test;
-import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.exceptions.TypeErrorException;
import de.tla2b.util.TestTypeChecker;
diff --git a/src/test/java/de/tla2b/typechecking/FunctionTest.java b/src/test/java/de/tla2b/typechecking/FunctionTest.java
index 9fa32603ce9b16128a37ebe0598a319172efc8d1..6102665347ab99be8c467130bc0785cdffd037a0 100644
--- a/src/test/java/de/tla2b/typechecking/FunctionTest.java
+++ b/src/test/java/de/tla2b/typechecking/FunctionTest.java
@@ -4,7 +4,6 @@ import static org.junit.Assert.assertEquals;
import org.junit.Test;
-import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.exceptions.TypeErrorException;
import de.tla2b.util.TestTypeChecker;
diff --git a/src/test/java/de/tla2b/typechecking/LogicOperatorsTest.java b/src/test/java/de/tla2b/typechecking/LogicOperatorsTest.java
index f13ea70fce1c897f84682d84e9cee211214ae4a6..554a2021f33507deef9b900427b1ea95b8147755 100644
--- a/src/test/java/de/tla2b/typechecking/LogicOperatorsTest.java
+++ b/src/test/java/de/tla2b/typechecking/LogicOperatorsTest.java
@@ -4,7 +4,6 @@ import static org.junit.Assert.*;
import org.junit.Test;
-import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.exceptions.TypeErrorException;
import de.tla2b.util.TestTypeChecker;
diff --git a/src/test/java/de/tla2b/typechecking/MiscellaneousConstructsTest.java b/src/test/java/de/tla2b/typechecking/MiscellaneousConstructsTest.java
index 7753c4cc967f7c6b22af288a44125e33eadb7740..e23b5247d1d9e0b92d85dc7e633fcc7674a0e46e 100644
--- a/src/test/java/de/tla2b/typechecking/MiscellaneousConstructsTest.java
+++ b/src/test/java/de/tla2b/typechecking/MiscellaneousConstructsTest.java
@@ -4,7 +4,6 @@ import static org.junit.Assert.assertEquals;
import org.junit.Test;
-import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.util.TestTypeChecker;
import de.tla2b.util.TestUtil;
diff --git a/src/test/java/de/tla2b/typechecking/SetTest.java b/src/test/java/de/tla2b/typechecking/SetTest.java
index 2180c8ae43a43dffca8a6b7eada52511047902f9..dec46415c3bf6e891716a323f5248132e00d87a1 100644
--- a/src/test/java/de/tla2b/typechecking/SetTest.java
+++ b/src/test/java/de/tla2b/typechecking/SetTest.java
@@ -4,7 +4,6 @@ import static org.junit.Assert.*;
import org.junit.Test;
-import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.exceptions.TypeErrorException;
import de.tla2b.util.TestTypeChecker;
diff --git a/src/test/java/de/tla2b/typechecking/StringTest.java b/src/test/java/de/tla2b/typechecking/StringTest.java
index f3cb27dc7d4a2da2c812a35083f8aca96655b114..d6f55367ee980e1f6d851033d68789d00a6ee1d3 100644
--- a/src/test/java/de/tla2b/typechecking/StringTest.java
+++ b/src/test/java/de/tla2b/typechecking/StringTest.java
@@ -4,7 +4,6 @@ import static org.junit.Assert.assertEquals;
import org.junit.Test;
-import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.exceptions.TypeErrorException;
import de.tla2b.util.TestTypeChecker;
diff --git a/src/test/java/de/tla2b/typechecking/StructTest.java b/src/test/java/de/tla2b/typechecking/StructTest.java
index 588094af981fb59dc5caefce33f647e01ba976c1..bffb148b7dde748fc2bb8751d1eaef8a6b090342 100644
--- a/src/test/java/de/tla2b/typechecking/StructTest.java
+++ b/src/test/java/de/tla2b/typechecking/StructTest.java
@@ -4,7 +4,6 @@ import static org.junit.Assert.assertEquals;
import org.junit.Test;
-import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.exceptions.TypeErrorException;
import de.tla2b.util.TestTypeChecker;
diff --git a/src/test/java/de/tla2b/typechecking/TupleTest.java b/src/test/java/de/tla2b/typechecking/TupleTest.java
index ea9facd1a03e95f8dbe8e7ca94a22033bd9ccb74..f418326a0ff6ca0a9d6dc6f9ea6fff13ea649484 100644
--- a/src/test/java/de/tla2b/typechecking/TupleTest.java
+++ b/src/test/java/de/tla2b/typechecking/TupleTest.java
@@ -4,7 +4,6 @@ import static org.junit.Assert.assertEquals;
import org.junit.Test;
-import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.exceptions.TypeErrorException;
import de.tla2b.util.TestTypeChecker;
diff --git a/src/test/java/de/tla2b/typechecking/TupleVsSequenceTest.java b/src/test/java/de/tla2b/typechecking/TupleVsSequenceTest.java
index aa416a420b0aecd0c36a9b12ee5ec2f4b71ac1fb..235215b7d67266284e277dbf0658762b70cfaba4 100644
--- a/src/test/java/de/tla2b/typechecking/TupleVsSequenceTest.java
+++ b/src/test/java/de/tla2b/typechecking/TupleVsSequenceTest.java
@@ -4,7 +4,6 @@ import static org.junit.Assert.assertEquals;
import org.junit.Test;
-import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.exceptions.TypeErrorException;
import de.tla2b.util.TestTypeChecker;
diff --git a/src/test/java/de/tla2b/typechecking/TypeConflictsTest.java b/src/test/java/de/tla2b/typechecking/TypeConflictsTest.java
index 95c0aacce698f5798c4875a342d8708e1346b050..d4e18e6635281a9de681edfb319093338f196c89 100644
--- a/src/test/java/de/tla2b/typechecking/TypeConflictsTest.java
+++ b/src/test/java/de/tla2b/typechecking/TypeConflictsTest.java
@@ -2,7 +2,6 @@ package de.tla2b.typechecking;
import org.junit.Test;
-import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.exceptions.TypeErrorException;
import de.tla2b.util.TestUtil;
diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleFiniteSets.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleFiniteSets.java
index 022bfd3f0f7874e7e440aace10cb20bad04a9b31..ca60a3ccd9dbfcb00b9c0a68adc6671fce508ed8 100644
--- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleFiniteSets.java
+++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleFiniteSets.java
@@ -4,7 +4,6 @@ import static org.junit.Assert.*;
import org.junit.Test;
-import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.exceptions.TypeErrorException;
import de.tla2b.util.TestTypeChecker;
diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleIntegers.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleIntegers.java
index 4a3d5b1c02f45deccfc36d36baffc4574f636bdc..96064e743d18e5f60905b90363c052a3e85f7bb1 100644
--- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleIntegers.java
+++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleIntegers.java
@@ -4,7 +4,6 @@ import static org.junit.Assert.*;
import org.junit.Test;
-import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.exceptions.TypeErrorException;
import de.tla2b.util.TestTypeChecker;
diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java
index 7269878ae5154c4280d28e9f93b78f86ff2c8990..d2cb4faea76bc67d2beb2f0b55f97efee011b133 100644
--- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java
+++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java
@@ -4,7 +4,6 @@ import static org.junit.Assert.assertEquals;
import org.junit.Test;
-import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.exceptions.TypeErrorException;
import de.tla2b.util.TestTypeChecker;
diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java
index 6e56bcbbcd1ba75984168d49feb47835edb02258..73f6fa45ac3d348fd3d618fdfcac4ebdc528654d 100644
--- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java
+++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java
@@ -4,7 +4,6 @@ import de.tla2b.exceptions.TLA2BException;
import de.tla2b.exceptions.TypeErrorException;
import de.tla2b.util.TestTypeChecker;
import de.tla2b.util.TestUtil;
-import org.junit.Ignore;
import org.junit.Test;
import static org.junit.Assert.assertEquals;
diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleSequences.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleSequences.java
index 20c152bba70526cfaa8cef8b568e82802c88cb6e..5b9df09a862ef8716066608374653806bb59f0c0 100644
--- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleSequences.java
+++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleSequences.java
@@ -4,7 +4,6 @@ import static org.junit.Assert.*;
import org.junit.Test;
-import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.exceptions.TypeErrorException;
import de.tla2b.util.TestTypeChecker;
diff --git a/src/test/java/de/tla2b/util/TestTypeChecker.java b/src/test/java/de/tla2b/util/TestTypeChecker.java
index 69a9dda5c2d996aa4757be56c3e52205bed47a66..a71588336f87ac3845f72f337e8d76f9f3b1a805 100644
--- a/src/test/java/de/tla2b/util/TestTypeChecker.java
+++ b/src/test/java/de/tla2b/util/TestTypeChecker.java
@@ -2,7 +2,6 @@ package de.tla2b.util;
import java.util.Hashtable;
-import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.global.TranslationGlobals;
import de.tla2b.types.TLAType;
@@ -22,9 +21,9 @@ public class TestTypeChecker implements TranslationGlobals {
private final Hashtable<String, DefCon> definitions;
public TestTypeChecker() {
- constants = new Hashtable<String, TLAType>();
- variables = new Hashtable<String, TLAType>();
- definitions = new Hashtable<String, DefCon>();
+ constants = new Hashtable<>();
+ variables = new Hashtable<>();
+ definitions = new Hashtable<>();
}
public void startTest(String moduleString, String configString)
@@ -102,12 +101,12 @@ public class TestTypeChecker implements TranslationGlobals {
return definitions.get(defName).getParams().get(paramName).toString();
}
- public class DefCon {
+ public static class DefCon {
private final Hashtable<String, TLAType> parameters;
private TLAType type;
private DefCon(TLAType t) {
- parameters = new Hashtable<String, TLAType>();
+ parameters = new Hashtable<>();
type = t;
}
diff --git a/src/test/java/de/tla2b/util/TestUtil.java b/src/test/java/de/tla2b/util/TestUtil.java
index f3f4186f2ef0c51dd2094079f5bc7b7962068966..cd9752edb130c1045e81c748e7be62c7fc192240 100644
--- a/src/test/java/de/tla2b/util/TestUtil.java
+++ b/src/test/java/de/tla2b/util/TestUtil.java
@@ -27,7 +27,7 @@ public class TestUtil {
File root = new File(path);
File[] list = root.listFiles();
- List<File> files = new ArrayList<File>();
+ List<File> files = new ArrayList<>();
if (list == null) {
return files;
}