diff --git a/src/main/java/de/tla2b/TLA2B.java b/src/main/java/de/tla2b/TLA2B.java
index 82f3ecf5619c3b67fd630433143ad605b17decfe..cc760f0792776d84848ab5b766a84ed47beadf90 100644
--- a/src/main/java/de/tla2b/TLA2B.java
+++ b/src/main/java/de/tla2b/TLA2B.java
@@ -19,7 +19,7 @@ public class TLA2B implements TranslationGlobals {
private String mainFile;
- private static boolean error = false;
+ private static final boolean error = false;
public static boolean hasError() {
return error;
diff --git a/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java b/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java
index d8d94aff6ebde8098560ffcbf079e2360697edfd..075a1503bd5d0a8aae15cf83d51f329662d8020c 100644
--- a/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java
+++ b/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java
@@ -70,7 +70,6 @@ public class AbstractASTVisitor extends BuiltInOPs implements ASTConstants {
}
case LetInKind: {
visitLetInNode((LetInNode) node);
- return;
}
}
}
@@ -99,10 +98,8 @@ public class AbstractASTVisitor extends BuiltInOPs implements ASTConstants {
case UserDefinedOpKind: {
if (BBuiltInOPs.contains(node.getOperator().getName())) {
visitBBuiltinsNode(node);
- return;
} else {
visitUserDefinedNode(node);
- return;
}
}
@@ -155,7 +152,6 @@ public class AbstractASTVisitor extends BuiltInOPs implements ASTConstants {
public void visitStubstInNode(SubstInNode n) {
visitExprNode(n.getBody());
- return;
}
public void visitUserDefinedNode(OpApplNode n) {
diff --git a/src/main/java/de/tla2b/analysis/BOperation.java b/src/main/java/de/tla2b/analysis/BOperation.java
index 3edbe00a488ffde83e9c51728684a86028f25fd4..3a1c3f3087c0d0876a52d886732a6e0175099cda 100644
--- a/src/main/java/de/tla2b/analysis/BOperation.java
+++ b/src/main/java/de/tla2b/analysis/BOperation.java
@@ -1,13 +1,7 @@
package de.tla2b.analysis;
-import java.util.ArrayList;
-import java.util.Arrays;
-import java.util.HashSet;
-import java.util.Hashtable;
-import java.util.LinkedHashMap;
-import java.util.List;
+import java.util.*;
import java.util.Map.Entry;
-import java.util.Set;
import de.be4.classicalb.core.parser.node.AAnySubstitution;
import de.be4.classicalb.core.parser.node.AAssignSubstitution;
@@ -47,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 LinkedHashMap<SymbolNode, ExprOrOpArgNode> assignments = new LinkedHashMap<SymbolNode, ExprOrOpArgNode>();
+ private final LinkedHashMap<SymbolNode, ExprOrOpArgNode> assignments = new LinkedHashMap<SymbolNode, ExprOrOpArgNode>();
private List<OpDeclNode> anyVariables;
private final SpecAnalyser specAnalyser;
@@ -216,9 +210,7 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
}
}
anyVariables = new ArrayList<OpDeclNode>();
- for (OpDeclNode var : specAnalyser.getModuleNode().getVariableDecls()) {
- anyVariables.add(var);
- }
+ Collections.addAll(anyVariables, specAnalyser.getModuleNode().getVariableDecls());
// for (SymbolNode symbol : primedVariablesFinder.getAllVariables()) {
// anyVariables.add((OpDeclNode) symbol);
@@ -261,10 +253,8 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
}
if (node.level < 2) {
guards.add(node);
- return;
} else {
beforeAfterPredicates.add(node);
- return;
}
// beforeAfterPredicates.add(node);
}
@@ -338,7 +328,6 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
case SubstInKind: {
SubstInNode substInNode = (SubstInNode) node;
findUnchangedVaribalesInSemanticNode(substInNode.getBody());
- return;
}
}
}
@@ -350,7 +339,6 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
&& !BBuiltInOPs.contains(n.getOperator().getName())) {
OpDefNode def = (OpDefNode) n.getOperator();
findUnchangedVaribalesInSemanticNode(def.getBody());
- return;
} else if (kind == BuiltInKind) {
int opcode = BuiltInOPs.getOpCode(n.getOperator().getName());
switch (opcode) {
diff --git a/src/main/java/de/tla2b/analysis/InstanceTransformation.java b/src/main/java/de/tla2b/analysis/InstanceTransformation.java
index 6b59d16f92e052463ae11ae46043782fa0dfe62d..5ba34975c652f4dc92abba0cc7264f251b9b7f0f 100644
--- a/src/main/java/de/tla2b/analysis/InstanceTransformation.java
+++ b/src/main/java/de/tla2b/analysis/InstanceTransformation.java
@@ -11,29 +11,27 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
OpDefNode[] defs;
Hashtable<String, OpDefNode> defsHash;
- private int substitutionId = 11;
+ private final int substitutionId = 11;
public InstanceTransformation(ModuleNode moduleNode) {
defs = moduleNode.getOpDefs();
- defsHash = new Hashtable<String, OpDefNode>();
- for (int i = 0; i < defs.length; i++) {
- OpDefNode def = defs[i];
+ defsHash = new Hashtable<>();
+ for (OpDefNode def : defs) {
defsHash.put(def.getName().toString(), def);
}
}
public void start() {
- for (int i = 0; i < defs.length; i++) {
- OpDefNode def = defs[i];
+ for (OpDefNode def : defs) {
if (def.getSource() != def
- && !BBuiltInOPs.contains(def.getSource().getName())) {
+ && !BBuiltInOPs.contains(def.getSource().getName())) {
// instance
String defName = def.getName().toString();
if (def.getBody() instanceof SubstInNode) {
String prefix = defName.substring(0,
- defName.lastIndexOf('!') + 1);
+ defName.lastIndexOf('!') + 1);
def.setParams(generateNewParams(def.getParams()));
ExprNode body;
try {
diff --git a/src/main/java/de/tla2b/analysis/RecursiveDefinition.java b/src/main/java/de/tla2b/analysis/RecursiveDefinition.java
index 09b5d7a270664808036d270024beb186bc8bf68e..831537b9293070e9c242f280ec4eee850dbe5cd4 100644
--- a/src/main/java/de/tla2b/analysis/RecursiveDefinition.java
+++ b/src/main/java/de/tla2b/analysis/RecursiveDefinition.java
@@ -7,7 +7,7 @@ import de.tla2b.exceptions.NotImplementedException;
public class RecursiveDefinition extends BuiltInOPs{
- private OpDefNode def;
+ private final OpDefNode def;
private OpApplNode ifThenElse;
public RecursiveDefinition(OpDefNode def) throws NotImplementedException{
diff --git a/src/main/java/de/tla2b/analysis/RecursiveFunktion.java b/src/main/java/de/tla2b/analysis/RecursiveFunktion.java
index 70c18ffc5af4a3e2e9d4229af27d1d27ab817915..f516fa5d52cccfe0cfc602d91a55581cf966bd01 100644
--- a/src/main/java/de/tla2b/analysis/RecursiveFunktion.java
+++ b/src/main/java/de/tla2b/analysis/RecursiveFunktion.java
@@ -7,8 +7,8 @@ import tlc2.tool.BuiltInOPs;
public class RecursiveFunktion extends BuiltInOPs {
- private OpDefNode def;
- private OpApplNode rfs;
+ private final OpDefNode def;
+ private final OpApplNode rfs;
private OpApplNode ifThenElse;
public RecursiveFunktion(OpDefNode n, OpApplNode rfs)
diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index cd3b7a1e353f59642f0c1a59524efe387aeadc49..b6229995ad879c4177f6d5df5361f53dfcf0126a 100644
--- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java
+++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
@@ -36,7 +36,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
private ArrayList<OpDefNode> invariants = new ArrayList<>();
private OpDefNode expressionOpdefNode;
- private Hashtable<String, SymbolNode> namingHashTable = new Hashtable<>();
+ private final Hashtable<String, SymbolNode> namingHashTable = new Hashtable<>();
private final ModuleNode moduleNode;
private ExprNode nextExpr;
@@ -46,20 +46,20 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
// configfile
private ArrayList<BOperation> bOperations = new ArrayList<BOperation>();
- private ArrayList<ExprNode> inits = new ArrayList<ExprNode>();
+ private final ArrayList<ExprNode> inits = new ArrayList<ExprNode>();
private Set<OpDefNode> bDefinitionsSet = new HashSet<OpDefNode>();
// set of OpDefNodes which will appear in the resulting B Machine
private Set<OpDefNode> usedDefinitions = new HashSet<OpDefNode>();
// definitions which are used for the type inference algorithm
- private Hashtable<OpDefNode, FormalParamNode[]> letParams = new Hashtable<>();
+ private final Hashtable<OpDefNode, FormalParamNode[]> letParams = new Hashtable<>();
// additional parameters of an let Operator, these parameters are from the
// surrounding operator
- private ArrayList<String> definitionMacros = new ArrayList<>();
+ private final ArrayList<String> definitionMacros = new ArrayList<>();
- private ArrayList<OpDefNode> recursiveFunctions = new ArrayList<>();
+ private final ArrayList<OpDefNode> recursiveFunctions = new ArrayList<>();
- private ArrayList<RecursiveDefinition> recursiveDefinitions = new ArrayList<>();
+ private final ArrayList<RecursiveDefinition> recursiveDefinitions = new ArrayList<>();
private ConfigfileEvaluator configFileEvaluator;
diff --git a/src/main/java/de/tla2b/analysis/SymbolRenamer.java b/src/main/java/de/tla2b/analysis/SymbolRenamer.java
index d2892f66af1c836355711c0c7f0457e76d2fed90..49a2f800aea6e492b2681c9d881d083e09060666 100644
--- a/src/main/java/de/tla2b/analysis/SymbolRenamer.java
+++ b/src/main/java/de/tla2b/analysis/SymbolRenamer.java
@@ -113,11 +113,11 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
BBUILTIN_OPERATOR.put("..", "dot2");
}
- private ModuleNode moduleNode;
- private Set<OpDefNode> usedDefinitions;
+ private final ModuleNode moduleNode;
+ private final Set<OpDefNode> usedDefinitions;
- private Set<String> globalNames = new HashSet<String>();
- private Hashtable<OpDefNode, Set<String>> usedNamesTable = new Hashtable<OpDefNode, Set<String>>();
+ private final Set<String> globalNames = new HashSet<String>();
+ private final Hashtable<OpDefNode, Set<String>> usedNamesTable = new Hashtable<OpDefNode, Set<String>>();
public SymbolRenamer(ModuleNode moduleNode, SpecAnalyser specAnalyser) {
this.moduleNode = moduleNode;
@@ -330,10 +330,7 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
}
private Boolean existingName(String name) {
- if (globalNames.contains(name) || KEYWORDS.contains(name)) {
- return true;
- } else
- return false;
+ return globalNames.contains(name) || KEYWORDS.contains(name);
}
private String incName(String name) {
diff --git a/src/main/java/de/tla2b/analysis/SymbolSorter.java b/src/main/java/de/tla2b/analysis/SymbolSorter.java
index b68f74ccdb412d1e86218f19a7f92eb597256928..6d64821a5ee690678a7155e9cf191ebbc5e30ea1 100644
--- a/src/main/java/de/tla2b/analysis/SymbolSorter.java
+++ b/src/main/java/de/tla2b/analysis/SymbolSorter.java
@@ -9,7 +9,7 @@ import tla2sany.semantic.OpDeclNode;
import tla2sany.semantic.OpDefNode;
public class SymbolSorter {
- private ModuleNode moduleNode;
+ private final ModuleNode moduleNode;
public SymbolSorter(ModuleNode moduleNode) {
this.moduleNode = moduleNode;
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index 82c94f4caf48870bf7741a63c957769fe326cf61..582bd30151e28908743a9184d04de6c6105c7966 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -2,7 +2,6 @@ package de.tla2b.analysis;
import java.util.*;
import java.util.Map.Entry;
-import java.util.stream.Collectors;
import de.tla2b.config.ConfigfileEvaluator;
import de.tla2b.config.TLCValueNode;
@@ -29,12 +28,12 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
private final Set<OpDefNode> usedDefinitions;
private final Set<OpDefNode> bDefinitions;
- private ArrayList<SymbolNode> symbolNodeList = new ArrayList<SymbolNode>();
- private ArrayList<SemanticNode> tupleNodeList = new ArrayList<SemanticNode>();
+ private final ArrayList<SymbolNode> symbolNodeList = new ArrayList<SymbolNode>();
+ private final ArrayList<SemanticNode> tupleNodeList = new ArrayList<SemanticNode>();
- private ModuleNode moduleNode;
+ private final ModuleNode moduleNode;
private ArrayList<OpDeclNode> bConstList;
- private SpecAnalyser specAnalyser;
+ private final SpecAnalyser specAnalyser;
private Hashtable<OpDeclNode, ValueObj> constantAssignments;
@@ -195,11 +194,10 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
public void visitOpDefNode(OpDefNode def) throws TLA2BException {
FormalParamNode[] params = def.getParams();
- for (int i = 0; i < params.length; i++) {
- FormalParamNode p = params[i];
+ for (FormalParamNode p : params) {
if (p.getArity() > 0) {
throw new FrontEndException(String.format("TLA2B do not support 2nd-order operators: '%s'%n %s ",
- def.getName(), def.getLocation()));
+ def.getName(), def.getLocation()));
}
UntypedType u = new UntypedType();
p.setToolObject(paramId, u);
@@ -437,7 +435,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
p.setToolObject(TEMP_TYPE_ID, pType);
}
- if (found.isUntyped() || untyped || def.getInRecursive() == false) {
+ if (found.isUntyped() || untyped || !def.getInRecursive()) {
// evaluate the body of the definition again
paramId = TEMP_TYPE_ID;
found = visitExprNode(def.getBody(), found);
@@ -660,12 +658,12 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
* Tuple: Tuple as Function 1..n to Set (Sequence)
*/
case OPCODE_tup: { // $Tuple
- ArrayList<TLAType> list = new ArrayList<TLAType>();
+ ArrayList<TLAType> list = new ArrayList<>();
for (int i = 0; i < n.getArgs().length; i++) {
list.add(visitExprOrOpArgNode(n.getArgs()[i], new UntypedType()));
}
- TLAType found = null;
- if (list.size() == 0) {
+ TLAType found;
+ if (list.isEmpty()) {
found = new FunctionType(IntType.getInstance(), new UntypedType());
} else if (list.size() == 1) {
found = new FunctionType(IntType.getInstance(), list.get(0));
@@ -744,7 +742,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
TLAType domType;
ExprOrOpArgNode dom = n.getArgs()[1];
if (dom instanceof OpApplNode && ((OpApplNode) dom).getOperator().getName().toString().equals("$Tuple")) {
- ArrayList<TLAType> domList = new ArrayList<TLAType>();
+ ArrayList<TLAType> domList = new ArrayList<>();
OpApplNode domOpAppl = (OpApplNode) dom;
for (int i = 0; i < domOpAppl.getArgs().length; i++) {
TLAType d = visitExprOrOpArgNode(domOpAppl.getArgs()[i], new UntypedType());
@@ -1009,11 +1007,11 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
throw new NotImplementedException(
- "Not supported Operator: " + n.getOperator().getName().toString() + "\n" + n.getLocation());
+ "Not supported Operator: " + n.getOperator().getName() + "\n" + n.getLocation());
}
private TLAType evalBoundedVariables(OpApplNode n) throws TLA2BException {
- ArrayList<TLAType> domList = new ArrayList<TLAType>();
+ ArrayList<TLAType> domList = new ArrayList<>();
FormalParamNode[][] params = n.getBdedQuantSymbolLists();
ExprNode[] bounds = n.getBdedQuantBounds();
for (int i = 0; i < bounds.length; i++) {
@@ -1099,9 +1097,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
OpApplNode seq = (OpApplNode) leftside;
LinkedList<ExprOrOpArgNode> list = new LinkedList<ExprOrOpArgNode>();
- for (int j = 0; j < seq.getArgs().length; j++) {
- list.add(seq.getArgs()[j]);
- }
+ Collections.addAll(list, seq.getArgs());
ExprOrOpArgNode first = list.poll();
if (first instanceof StringNode) {
@@ -1343,7 +1339,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return set_of_seq;
}
- case B_OPCODE_len: { // lengh of the sequence
+ case B_OPCODE_len: { // length of the sequence
try {
IntType.getInstance().unify(expected);
} catch (UnificationException e) {
diff --git a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java b/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
index e72441c8016361fa97d27f96ac6037be93a612b4..481b165d9c58295271d4c3f95d7206de9d10476d 100644
--- a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
+++ b/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
@@ -10,13 +10,7 @@ import java.util.Map;
import de.tla2b.exceptions.ConfigFileErrorException;
import de.tla2b.exceptions.UnificationException;
-import de.tla2b.types.BoolType;
-import de.tla2b.types.EnumType;
-import de.tla2b.types.IntType;
-import de.tla2b.types.SetType;
-import de.tla2b.types.StringType;
-import de.tla2b.types.TLAType;
-import de.tla2b.types.UntypedType;
+import de.tla2b.types.*;
import tla2sany.semantic.InstanceNode;
import tla2sany.semantic.ModuleNode;
import tla2sany.semantic.OpDeclNode;
@@ -491,7 +485,7 @@ public class ConfigfileEvaluator {
} else if (o.getClass().getName().equals("tlc2.value.SetEnumValue")) {
SetEnumValue set = (SetEnumValue) o;
SetType t = new SetType(new UntypedType());
- if (set.size() == 0) {
+ if (set.isEmpty()) {
throw new ConfigFileErrorException(
"empty set is not permitted!");
}
@@ -522,9 +516,8 @@ public class ConfigfileEvaluator {
+ o);
}
}
- Iterator<String> it = e.modelvalues.iterator();
- while (it.hasNext()) {
- enumeratedTypes.put(it.next(), e);
+ for (String s : e.modelvalues) {
+ enumeratedTypes.put(s, e);
}
elemType = e;
} else {
@@ -546,7 +539,7 @@ public class ConfigfileEvaluator {
ModelValue mv = (ModelValue) o;
if (!enumeratedSet.contains(mv.toString())) {
enumeratedSet.add(mv.toString());
- ArrayList<String> temp = new ArrayList<String>();
+ ArrayList<String> temp = new ArrayList<>();
temp.add(mv.toString());
EnumType e = new EnumType(temp);
enumeratedTypes.put(mv.toString(), e);
diff --git a/src/main/java/de/tla2b/config/ModuleOverrider.java b/src/main/java/de/tla2b/config/ModuleOverrider.java
index aff07f2fc3dbced2458aa15790da202f44fb5042..398d37c42e4f8e53d30118bbd96e15c78853588c 100644
--- a/src/main/java/de/tla2b/config/ModuleOverrider.java
+++ b/src/main/java/de/tla2b/config/ModuleOverrider.java
@@ -17,10 +17,10 @@ import tlc2.tool.BuiltInOPs;
public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
- private ModuleNode moduleNode;
- private Hashtable<OpDeclNode, OpDefNode> constantOverrideTable;
- private Hashtable<OpDefNode, OpDefNode> operatorOverrideTable;
- private Hashtable<OpDefNode, ValueObj> operatorAssignments;
+ private final ModuleNode moduleNode;
+ private final Hashtable<OpDeclNode, OpDefNode> constantOverrideTable;
+ private final Hashtable<OpDefNode, OpDefNode> operatorOverrideTable;
+ private final Hashtable<OpDefNode, ValueObj> operatorAssignments;
public ModuleOverrider(ModuleNode moduleNode,
Hashtable<OpDeclNode, OpDefNode> constantOverrideTable,
diff --git a/src/main/java/de/tla2b/config/TLCValueNode.java b/src/main/java/de/tla2b/config/TLCValueNode.java
index 41f08c3760624a5250f5b622a74f8e0ed28973af..45e06860fe8d0258a5f66b92cd8e9d4e38a55f16 100644
--- a/src/main/java/de/tla2b/config/TLCValueNode.java
+++ b/src/main/java/de/tla2b/config/TLCValueNode.java
@@ -9,8 +9,8 @@ import tlc2.value.Value;
public class TLCValueNode extends NumeralNode implements TranslationGlobals {
- private Value value;
- private TLAType type;
+ private final Value value;
+ private final TLAType type;
public TLCValueNode(ValueObj valObj, TreeNode stn) throws AbortException {
super("1337", stn);
diff --git a/src/main/java/de/tla2b/global/BBuildIns.java b/src/main/java/de/tla2b/global/BBuildIns.java
index 40a6b50eb1c708872cbcccd22d9dcfda20a33242..424a955054e5ce6ee35789b465adb49852430dd4 100644
--- a/src/main/java/de/tla2b/global/BBuildIns.java
+++ b/src/main/java/de/tla2b/global/BBuildIns.java
@@ -3,134 +3,134 @@ package de.tla2b.global;
import util.UniqueString;
public interface BBuildIns {
- public static final UniqueString OP_dotdot = UniqueString
+ UniqueString OP_dotdot = UniqueString
.uniqueStringOf("..");
- public static final UniqueString OP_plus = UniqueString.uniqueStringOf("+");
- public static final UniqueString OP_minus = UniqueString
+ UniqueString OP_plus = UniqueString.uniqueStringOf("+");
+ UniqueString OP_minus = UniqueString
.uniqueStringOf("-");
- public static final UniqueString OP_times = UniqueString
+ UniqueString OP_times = UniqueString
.uniqueStringOf("*");
- public static final UniqueString OP_div = UniqueString
+ UniqueString OP_div = UniqueString
.uniqueStringOf("\\div");
- public static final UniqueString OP_mod = UniqueString.uniqueStringOf("%");
- public static final UniqueString OP_exp = UniqueString.uniqueStringOf("^");
+ UniqueString OP_mod = UniqueString.uniqueStringOf("%");
+ UniqueString OP_exp = UniqueString.uniqueStringOf("^");
- public static final UniqueString OP_uminus = UniqueString
+ UniqueString OP_uminus = UniqueString
.uniqueStringOf("-.");
- public static final UniqueString OP_lt = UniqueString.uniqueStringOf("<");
- public static final UniqueString OP_leq = UniqueString
+ UniqueString OP_lt = UniqueString.uniqueStringOf("<");
+ UniqueString OP_leq = UniqueString
.uniqueStringOf("\\leq");
- public static final UniqueString OP_gt = UniqueString.uniqueStringOf(">");
- public static final UniqueString OP_geq = UniqueString
+ UniqueString OP_gt = UniqueString.uniqueStringOf(">");
+ UniqueString OP_geq = UniqueString
.uniqueStringOf("\\geq");
- public static final UniqueString OP_nat = UniqueString
+ UniqueString OP_nat = UniqueString
.uniqueStringOf("Nat");
- public static final UniqueString OP_int = UniqueString
+ UniqueString OP_int = UniqueString
.uniqueStringOf("Int");
UniqueString OP_real = UniqueString
.uniqueStringOf("Real");
- public static final UniqueString OP_bool = UniqueString
+ UniqueString OP_bool = UniqueString
.uniqueStringOf("BOOLEAN");
- public static final UniqueString OP_true = UniqueString
+ UniqueString OP_true = UniqueString
.uniqueStringOf("TRUE");
- public static final UniqueString OP_false = UniqueString
+ UniqueString OP_false = UniqueString
.uniqueStringOf("FALSE");
- public static final UniqueString OP_string = UniqueString
+ UniqueString OP_string = UniqueString
.uniqueStringOf("STRING");
// Sets
- public static final UniqueString OP_card = UniqueString
+ UniqueString OP_card = UniqueString
.uniqueStringOf("Cardinality");
- public static final UniqueString OP_finite = UniqueString
+ UniqueString OP_finite = UniqueString
.uniqueStringOf("IsFiniteSet");
// Sequences
- public static final UniqueString OP_len = UniqueString
+ UniqueString OP_len = UniqueString
.uniqueStringOf("Len");
- public static final UniqueString OP_append = UniqueString
+ UniqueString OP_append = UniqueString
.uniqueStringOf("Append");
- public static final UniqueString OP_seq = UniqueString
+ UniqueString OP_seq = UniqueString
.uniqueStringOf("Seq");
- public static final UniqueString OP_head = UniqueString
+ UniqueString OP_head = UniqueString
.uniqueStringOf("Head");
- public static final UniqueString OP_tail = UniqueString
+ UniqueString OP_tail = UniqueString
.uniqueStringOf("Tail");
- public static final UniqueString OP_subseq = UniqueString
+ UniqueString OP_subseq = UniqueString
.uniqueStringOf("SubSeq");
- public static final UniqueString OP_conc = UniqueString
+ UniqueString OP_conc = UniqueString
.uniqueStringOf("\\o");
//TLA2B
- public static final UniqueString OP_min = UniqueString
+ UniqueString OP_min = UniqueString
.uniqueStringOf("MinOfSet");
- public static final UniqueString OP_max = UniqueString
+ UniqueString OP_max = UniqueString
.uniqueStringOf("MaxOfSet");
- public static final UniqueString OP_setprod = UniqueString
+ UniqueString OP_setprod = UniqueString
.uniqueStringOf("SetProduct");
- public static final UniqueString OP_setsum = UniqueString
+ UniqueString OP_setsum = UniqueString
.uniqueStringOf("SetSummation");
- public static final UniqueString OP_permseq = UniqueString
+ UniqueString OP_permseq = UniqueString
.uniqueStringOf("PermutedSequences");
//BBuildIns
- public static final UniqueString OP_pow1 = UniqueString
+ UniqueString OP_pow1 = UniqueString
.uniqueStringOf("POW1");
//Relations
- public static final UniqueString OP_rel_inverse = UniqueString
+ UniqueString OP_rel_inverse = UniqueString
.uniqueStringOf("rel_inverse");
//TLC
- public static final UniqueString OP_assert = UniqueString
+ UniqueString OP_assert = UniqueString
.uniqueStringOf("Assert");
- public static final int B_OPCODE_dotdot = 1;
- public static final int B_OPCODE_plus = 2;
- public static final int B_OPCODE_minus = 3;
- public static final int B_OPCODE_times = 4;
- public static final int B_OPCODE_div = 5;
- public static final int B_OPCODE_exp = 6;
- public static final int B_OPCODE_uminus = 7;
- public static final int B_OPCODE_mod = 8;
+ int B_OPCODE_dotdot = 1;
+ int B_OPCODE_plus = 2;
+ int B_OPCODE_minus = 3;
+ int B_OPCODE_times = 4;
+ int B_OPCODE_div = 5;
+ int B_OPCODE_exp = 6;
+ int B_OPCODE_uminus = 7;
+ int B_OPCODE_mod = 8;
- public static final int B_OPCODE_lt = B_OPCODE_mod + 1;
- public static final int B_OPCODE_leq = B_OPCODE_mod + 2;
- public static final int B_OPCODE_gt = B_OPCODE_mod + 3;
- public static final int B_OPCODE_geq = B_OPCODE_mod + 4;
+ int B_OPCODE_lt = B_OPCODE_mod + 1;
+ int B_OPCODE_leq = B_OPCODE_mod + 2;
+ int B_OPCODE_gt = B_OPCODE_mod + 3;
+ int B_OPCODE_geq = B_OPCODE_mod + 4;
- public static final int B_OPCODE_nat = B_OPCODE_geq + 1;
- public static final int B_OPCODE_bool = B_OPCODE_geq + 2;
- public static final int B_OPCODE_true = B_OPCODE_geq + 3;
- public static final int B_OPCODE_false = B_OPCODE_geq + 4;
- public static final int B_OPCODE_int = B_OPCODE_geq + 5;
- public static final int B_OPCODE_string = B_OPCODE_geq + 6;
+ int B_OPCODE_nat = B_OPCODE_geq + 1;
+ int B_OPCODE_bool = B_OPCODE_geq + 2;
+ int B_OPCODE_true = B_OPCODE_geq + 3;
+ int B_OPCODE_false = B_OPCODE_geq + 4;
+ int B_OPCODE_int = B_OPCODE_geq + 5;
+ int B_OPCODE_string = B_OPCODE_geq + 6;
- public static final int B_OPCODE_finite = B_OPCODE_string + 1;
- public static final int B_OPCODE_card = B_OPCODE_string + 2;
+ int B_OPCODE_finite = B_OPCODE_string + 1;
+ int B_OPCODE_card = B_OPCODE_string + 2;
- public static final int B_OPCODE_len = B_OPCODE_card + 1;
- public static final int B_OPCODE_append = B_OPCODE_card + 2;
- public static final int B_OPCODE_seq = B_OPCODE_card + 3;
- public static final int B_OPCODE_head = B_OPCODE_card + 4;
- public static final int B_OPCODE_tail = B_OPCODE_card + 5;
- public static final int B_OPCODE_subseq = B_OPCODE_card + 6;
- public static final int B_OPCODE_conc = B_OPCODE_card + 7;
+ int B_OPCODE_len = B_OPCODE_card + 1;
+ int B_OPCODE_append = B_OPCODE_card + 2;
+ int B_OPCODE_seq = B_OPCODE_card + 3;
+ int B_OPCODE_head = B_OPCODE_card + 4;
+ int B_OPCODE_tail = B_OPCODE_card + 5;
+ int B_OPCODE_subseq = B_OPCODE_card + 6;
+ int B_OPCODE_conc = B_OPCODE_card + 7;
- public static final int B_OPCODE_min = B_OPCODE_conc + 1;
- public static final int B_OPCODE_max = B_OPCODE_conc + 2;
- public static final int B_OPCODE_setprod = B_OPCODE_conc + 3;
- public static final int B_OPCODE_setsum = B_OPCODE_conc + 4;
- public static final int B_OPCODE_permseq = B_OPCODE_conc + 5;
+ int B_OPCODE_min = B_OPCODE_conc + 1;
+ int B_OPCODE_max = B_OPCODE_conc + 2;
+ int B_OPCODE_setprod = B_OPCODE_conc + 3;
+ int B_OPCODE_setsum = B_OPCODE_conc + 4;
+ int B_OPCODE_permseq = B_OPCODE_conc + 5;
- public static final int B_OPCODE_pow1 = B_OPCODE_permseq + 1;
+ int B_OPCODE_pow1 = B_OPCODE_permseq + 1;
- public static final int B_OPCODE_rel_inverse = B_OPCODE_pow1 + 1;
+ int B_OPCODE_rel_inverse = B_OPCODE_pow1 + 1;
- public static final int B_OPCODE_assert = B_OPCODE_rel_inverse + 1;
+ int B_OPCODE_assert = B_OPCODE_rel_inverse + 1;
int B_OPCODE_real = B_OPCODE_assert + 1;
}
diff --git a/src/main/java/de/tla2b/global/OperatorTypes.java b/src/main/java/de/tla2b/global/OperatorTypes.java
index 1bcfec469c48935cd8093899ee92c27e19049ebf..89990f5fbf0d2903486b6afce8b859bb9e861969 100644
--- a/src/main/java/de/tla2b/global/OperatorTypes.java
+++ b/src/main/java/de/tla2b/global/OperatorTypes.java
@@ -4,8 +4,8 @@ import java.util.HashSet;
import tlc2.tool.ToolGlobals;
public class OperatorTypes implements ToolGlobals, BBuildIns {
- private static HashSet<Integer> TLA_Predicate_Operators;
- private static HashSet<Integer> BBuiltIn_Predicate_Operators;
+ 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.add(OPCODE_eq);
diff --git a/src/main/java/de/tla2b/global/Priorities.java b/src/main/java/de/tla2b/global/Priorities.java
index 7d176b60cdb4d2ecebbb7c1db4009826f05218d2..071f11d0bcab3da5733e8a0a40f182f882fc9b66 100644
--- a/src/main/java/de/tla2b/global/Priorities.java
+++ b/src/main/java/de/tla2b/global/Priorities.java
@@ -1,64 +1,64 @@
package de.tla2b.global;
public interface Priorities {
- public static final int P_max = 300;
+ int P_max = 300;
- public static final int P_record_acc = 250;
- public static final int P_uminus = 210;
- public static final int P_exp = 200;
+ int P_record_acc = 250;
+ int P_uminus = 210;
+ int P_exp = 200;
- public static final int P_times = 190;
- public static final int P_div = 190;
- public static final int P_mod = 190;
+ int P_times = 190;
+ int P_div = 190;
+ int P_mod = 190;
- public static final int P_plus = 180;
- public static final int P_minus = 180;
- public static final int P_setdiff = 180;
+ int P_plus = 180;
+ int P_minus = 180;
+ int P_setdiff = 180;
- public static final int P_dotdot = 170;
+ int P_dotdot = 170;
- public static final int P_maplet = 160;
+ int P_maplet = 160;
- public static final int P_take_first = 160;
- public static final int P_drop_last = 160;
- public static final int P_conc = 160;
+ int P_take_first = 160;
+ int P_drop_last = 160;
+ int P_conc = 160;
- public static final int P_intersect = 140;
- public static final int P_union = 140;
+ int P_intersect = 140;
+ int P_union = 140;
- public static final int P_append = 130;
+ int P_append = 130;
- public static final int P_total_f = 125;
+ int P_total_f = 125;
- public static final int P_comma = 115;
+ int P_comma = 115;
- public static final int P_rel_overriding = 90;
+ int P_rel_overriding = 90;
- public static final int P_in = 60;
- public static final int P_notin = 60;
- public static final int P_subseteq = 60;
+ int P_in = 60;
+ int P_notin = 60;
+ int P_subseteq = 60;
- public static final int P_equals = 50;
- public static final int P_noteq = 50;
- public static final int P_gt = 50;
- public static final int P_lt = 50;
- public static final int P_leq = 50;
- public static final int P_geq = 50;
+ int P_equals = 50;
+ int P_noteq = 50;
+ int P_gt = 50;
+ int P_lt = 50;
+ int P_leq = 50;
+ int P_geq = 50;
- public static final int P_equiv = 60;
+ int P_equiv = 60;
- public static final int P_and = 40;
- public static final int P_or = 40;
+ int P_and = 40;
+ int P_or = 40;
- public static final int P_implies = 30;
+ int P_implies = 30;
- public static final int P_min = 0;
+ int P_min = 0;
diff --git a/src/main/java/de/tla2b/global/TranslationGlobals.java b/src/main/java/de/tla2b/global/TranslationGlobals.java
index 981b611acfda0d2fe369cd03684d5159d7a18811..9a4ce27180efaa35ee560ef77160f7fdd541eafc 100644
--- a/src/main/java/de/tla2b/global/TranslationGlobals.java
+++ b/src/main/java/de/tla2b/global/TranslationGlobals.java
@@ -6,25 +6,25 @@ import java.util.Arrays;
import tla2sany.semantic.FrontEnd;
public interface TranslationGlobals {
- final String VERSION_NUMBER = VersionHelper.VERSION;
+ String VERSION_NUMBER = VersionHelper.VERSION;
- final int TLCValueKind = 100;
+ int TLCValueKind = 100;
- final int USED = FrontEnd.getToolId();
- final int OVERRIDE_SUBSTITUTION_ID = 17;
- final int CONSTANT_OBJECT = 18;
- final int DEF_OBJECT = 19;
- final int PRINT_DEFINITION = 11;
- final int TYPE_ID = 5;
- final int EXCEPT_BASE = 6;
- final int LET_PARAMS_ID = 13;
- final int NEW_NAME = 20;
+ int USED = FrontEnd.getToolId();
+ int OVERRIDE_SUBSTITUTION_ID = 17;
+ int CONSTANT_OBJECT = 18;
+ int DEF_OBJECT = 19;
+ int PRINT_DEFINITION = 11;
+ int TYPE_ID = 5;
+ int EXCEPT_BASE = 6;
+ int LET_PARAMS_ID = 13;
+ int NEW_NAME = 20;
- final int SUBSTITUTE_PARAM = 29;
- final int TUPLE = 30;
+ int SUBSTITUTE_PARAM = 29;
+ int TUPLE = 30;
- final String CHOOSE = " CHOOSE(X) == \"a member of X\"; EXTERNAL_FUNCTION_CHOOSE(T) == (POW(T)-->T)";
- final String IF_THEN_ELSE = " IF_THEN_ELSE(P, a, b) == (%t_.(t_ = TRUE & P = TRUE | a )\\/%t_.(t_= TRUE & not(P= TRUE) | b ))(TRUE)";
+ String CHOOSE = " CHOOSE(X) == \"a member of X\"; EXTERNAL_FUNCTION_CHOOSE(T) == (POW(T)-->T)";
+ String IF_THEN_ELSE = " IF_THEN_ELSE(P, a, b) == (%t_.(t_ = TRUE & P = TRUE | a )\\/%t_.(t_= TRUE & not(P= TRUE) | b ))(TRUE)";
ArrayList<String> STANDARD_MODULES = new ArrayList<>(
Arrays.asList("Naturals", "FiniteSets", "Integers", "Reals",
diff --git a/src/main/java/de/tla2b/output/Indentation.java b/src/main/java/de/tla2b/output/Indentation.java
index 4fd9dd92d9746785f54e3aa5df06cf64f9b8c9fa..0131b1fae37f6a1f65981949c50381385ed92e56 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 Hashtable<Node, Integer> indentation = new Hashtable<Node, Integer>();
- private HashSet<Node> newlineMiddle = new HashSet<Node>();
- private HashSet<Node> nodesWithNewlineAtTheEnd = new HashSet<Node>();
- private HashSet<Node> indentedNodes = new HashSet<Node>();
+ 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>();
public final static String INDENT = " ";
public final static String SPACE = " ";
diff --git a/src/main/java/de/tla2b/output/TlaTypePrinter.java b/src/main/java/de/tla2b/output/TlaTypePrinter.java
index 5d5fc8c51e5ec5233fcb1b8d90c68895f0df74be..94e2ffe2811c4eb4028cf9d70a72e08debb0b156 100644
--- a/src/main/java/de/tla2b/output/TlaTypePrinter.java
+++ b/src/main/java/de/tla2b/output/TlaTypePrinter.java
@@ -40,14 +40,13 @@ public class TlaTypePrinter implements PositionPrinter, TypeVisitorInterface {
final Integer id = nodeIds.lookup(node);
if (positions != null && positions.contains(node)) {
- PositionedNode pNode = (PositionedNode) node;
pout.openTerm("pos", true);
pout.printNumber(id == null ? -1 : id);
pout.printNumber(nodeIds.lookupFileNumber(node));
- pout.printNumber(pNode.getStartPos().getLine());
- pout.printNumber(pNode.getStartPos().getPos());
- pout.printNumber(pNode.getEndPos().getLine());
- pout.printNumber(pNode.getEndPos().getPos());
+ pout.printNumber(node.getStartPos().getLine());
+ pout.printNumber(node.getStartPos().getPos());
+ pout.printNumber(node.getEndPos().getLine());
+ pout.printNumber(node.getEndPos().getPos());
pout.closeTerm();
} else {
if (id == null) {
diff --git a/src/main/java/de/tla2b/translation/BMacroHandler.java b/src/main/java/de/tla2b/translation/BMacroHandler.java
index a6c3cc12a54fdd11937ec3755cbe44585e147c63..d86a71ac14f4112d6f55b877ab0bedd2755a3547 100644
--- a/src/main/java/de/tla2b/translation/BMacroHandler.java
+++ b/src/main/java/de/tla2b/translation/BMacroHandler.java
@@ -1,10 +1,6 @@
package de.tla2b.translation;
-import java.util.ArrayList;
-import java.util.Arrays;
-import java.util.HashSet;
-import java.util.Hashtable;
-import java.util.Set;
+import java.util.*;
import tla2sany.semantic.AssumeNode;
import tla2sany.semantic.ExprNode;
@@ -94,10 +90,7 @@ public class BMacroHandler extends AbstractASTVisitor {
FormalParamNode[][] params = n.getBdedQuantSymbolLists();
HashSet<FormalParamNode> set = new HashSet<FormalParamNode>();
for (int i = 0; i < params.length; i++) {
- for (int j = 0; j < params[i].length; j++) {
- FormalParamNode param = params[i][j];
- set.add(param);
- }
+ Collections.addAll(set, params[i]);
}
localVariables.addAll(set);
ExprNode[] in = n.getBdedQuantBounds();
@@ -113,7 +106,6 @@ public class BMacroHandler extends AbstractASTVisitor {
}
default: {
super.visitBuiltInNode(n);
- return;
}
}
@@ -194,10 +186,7 @@ public class BMacroHandler extends AbstractASTVisitor {
Set<String> globalNames = new HashSet<String>();
private Boolean existingName(String name) {
- if (globalNames.contains(name)) {
- return true;
- } else
- return false;
+ return globalNames.contains(name);
}
private String incName(String name, Set<String> tempSet) {
diff --git a/src/main/java/de/tla2b/translation/OperationsFinder.java b/src/main/java/de/tla2b/translation/OperationsFinder.java
index dbe48dcef54b934433d1eb5a7a156e2439e4997e..b51bae3c4dd5639d99838a9674c9c0efb12c8a0f 100644
--- a/src/main/java/de/tla2b/translation/OperationsFinder.java
+++ b/src/main/java/de/tla2b/translation/OperationsFinder.java
@@ -67,7 +67,6 @@ public class OperationsFinder extends AbstractASTVisitor implements
case LetInKind: {
// we do not visit the local definitions
visitExprNode(((LetInNode) n).getBody());
- return;
}
}
}
@@ -161,8 +160,7 @@ public class OperationsFinder extends AbstractASTVisitor implements
return;
}
throw new RuntimeException(String.format(
- "Expected an action at '%s' :%n%s", n.getOperator().getName()
- .toString(), n.getLocation().toString()));
+ "Expected an action at '%s' :%n%s", n.getOperator().getName(), n.getLocation().toString()));
}
diff --git a/src/main/java/de/tla2b/translation/RecursiveFunctionHandler.java b/src/main/java/de/tla2b/translation/RecursiveFunctionHandler.java
index 73ec0d76a979e1896369e3063cc8670519b81fdf..62a0c6370dd6fb5d241516e44a1faef78a0bf046 100644
--- a/src/main/java/de/tla2b/translation/RecursiveFunctionHandler.java
+++ b/src/main/java/de/tla2b/translation/RecursiveFunctionHandler.java
@@ -1,6 +1,7 @@
package de.tla2b.translation;
import java.util.ArrayList;
+import java.util.Collections;
import java.util.HashSet;
import java.util.Hashtable;
@@ -20,8 +21,8 @@ public class RecursiveFunctionHandler extends AbstractASTVisitor {
private ArrayList<FormalParamNode> ignoreParamList;
private ArrayList<SymbolNode> externParams;
- private HashSet<OpApplNode> recursiveFunctions = new HashSet<OpApplNode>();
- private Hashtable<SemanticNode, ArrayList<SymbolNode>> additionalParamsTable = new Hashtable<SemanticNode, ArrayList<SymbolNode>>();
+ private final HashSet<OpApplNode> recursiveFunctions = new HashSet<OpApplNode>();
+ private final Hashtable<SemanticNode, ArrayList<SymbolNode>> additionalParamsTable = new Hashtable<SemanticNode, ArrayList<SymbolNode>>();
public RecursiveFunctionHandler(SpecAnalyser specAnalyser) {
for (OpDefNode recFunc : specAnalyser.getRecursiveFunctions()) {
@@ -33,9 +34,7 @@ public class RecursiveFunctionHandler extends AbstractASTVisitor {
FormalParamNode self = body.getUnbdedQuantSymbols()[0];
paramList.add(self);
for (int i = 0; i < params.length; i++) {
- for (int j = 0; j < params[i].length; j++) {
- paramList.add(params[i][j]);
- }
+ Collections.addAll(paramList, params[i]);
}
externParams = new ArrayList<SymbolNode>();
ignoreParamList = new ArrayList<FormalParamNode>();
@@ -81,10 +80,7 @@ public class RecursiveFunctionHandler extends AbstractASTVisitor {
FormalParamNode[][] params = n.getBdedQuantSymbolLists();
HashSet<FormalParamNode> set = new HashSet<FormalParamNode>();
for (int i = 0; i < params.length; i++) {
- for (int j = 0; j < params[i].length; j++) {
- FormalParamNode param = params[i][j];
- set.add(param);
- }
+ Collections.addAll(set, params[i]);
}
ignoreParamList.addAll(set);
ExprNode[] in = n.getBdedQuantBounds();
@@ -99,7 +95,6 @@ public class RecursiveFunctionHandler extends AbstractASTVisitor {
}
default: {
super.visitBuiltInNode(n);
- return;
}
}
diff --git a/src/main/java/de/tla2b/types/AbstractHasFollowers.java b/src/main/java/de/tla2b/types/AbstractHasFollowers.java
index 2d64796587d753656fb8daa56e6bb7706172d783..d6538265bfefdf8b638e26a08489327d260c1ae9 100644
--- a/src/main/java/de/tla2b/types/AbstractHasFollowers.java
+++ b/src/main/java/de/tla2b/types/AbstractHasFollowers.java
@@ -86,9 +86,6 @@ public abstract class AbstractHasFollowers extends TLAType {
}
public boolean hasFollower() {
- if (followers.size() == 0) {
- return false;
- } else
- return true;
+ return followers.size() != 0;
}
}
diff --git a/src/main/java/de/tla2b/types/BoolType.java b/src/main/java/de/tla2b/types/BoolType.java
index 79636ee3f312a7d551cd83d0572d69c06f2d72a9..f901cd0543114cc4e3dd9d39aaae5bd1f41a55aa 100644
--- a/src/main/java/de/tla2b/types/BoolType.java
+++ b/src/main/java/de/tla2b/types/BoolType.java
@@ -7,7 +7,7 @@ import de.tla2b.output.TypeVisitorInterface;
public class BoolType extends TLAType {
- private static BoolType instance = new BoolType();
+ private static final BoolType instance = new BoolType();
private BoolType() {
super(BOOL);
@@ -29,10 +29,7 @@ public class BoolType extends TLAType {
@Override
public boolean compare(TLAType o) {
- if (o.getKind() == UNTYPED || o.getKind() == BOOL)
- return true;
- else
- return false;
+ return o.getKind() == UNTYPED || o.getKind() == BOOL;
}
@Override
@@ -65,4 +62,4 @@ public class BoolType extends TLAType {
t.caseBoolType(this);
}
-}
\ No newline at end of file
+}
diff --git a/src/main/java/de/tla2b/types/EnumType.java b/src/main/java/de/tla2b/types/EnumType.java
index ba7496d97f386a4300afb215338ee09270930b01..4d2119fba0bc80884d5546d923b16c8afe6b34a7 100644
--- a/src/main/java/de/tla2b/types/EnumType.java
+++ b/src/main/java/de/tla2b/types/EnumType.java
@@ -37,10 +37,7 @@ public class EnumType extends AbstractHasFollowers {
@Override
public boolean compare(TLAType o) {
- if (o.getKind() == UNTYPED || o.getKind() == MODELVALUE)
- return true;
- else
- return false;
+ return o.getKind() == UNTYPED || o.getKind() == MODELVALUE;
}
@Override
diff --git a/src/main/java/de/tla2b/types/FunctionType.java b/src/main/java/de/tla2b/types/FunctionType.java
index c25fd7fac0287076f4e580233abeaf52e5cb63e8..b061b51ad6d9eee4af03eb90e6cae0198c70e538 100644
--- a/src/main/java/de/tla2b/types/FunctionType.java
+++ b/src/main/java/de/tla2b/types/FunctionType.java
@@ -93,10 +93,10 @@ public class FunctionType extends AbstractHasFollowers {
return this;
}
if (other instanceof TupleType) {
- return (FunctionType) other.unify(this);
+ return other.unify(this);
}
if (other instanceof TupleOrFunction) {
- return (FunctionType) other.unify(this);
+ return other.unify(this);
}
throw new RuntimeException();
diff --git a/src/main/java/de/tla2b/types/IntType.java b/src/main/java/de/tla2b/types/IntType.java
index f6f2d0619bf006c582276229c6b0239eb6af8835..bdde67f2f04d0c63a2f87b574ae33f7f9f8d36ce 100644
--- a/src/main/java/de/tla2b/types/IntType.java
+++ b/src/main/java/de/tla2b/types/IntType.java
@@ -7,7 +7,7 @@ import de.tla2b.output.TypeVisitorInterface;
public class IntType extends TLAType {
- private static IntType instance = new IntType();
+ private static final IntType instance = new IntType();
private IntType() {
super(INTEGER);
@@ -29,10 +29,7 @@ public class IntType extends TLAType {
@Override
public boolean compare(TLAType o) {
- if (o.getKind() == UNTYPED || o.getKind() == INTEGER)
- return true;
- else
- return false;
+ return o.getKind() == UNTYPED || o.getKind() == INTEGER;
}
@Override
@@ -65,4 +62,4 @@ public class IntType extends TLAType {
visitor.caseIntegerType(this);
}
-}
\ No newline at end of file
+}
diff --git a/src/main/java/de/tla2b/types/ModelValueType.java b/src/main/java/de/tla2b/types/ModelValueType.java
index b9c6697d9f9050dcc5ac81a9f44dc0fd2411fa87..9607031cc4fbb27ac2d9b1c5e38820927bdbb406 100644
--- a/src/main/java/de/tla2b/types/ModelValueType.java
+++ b/src/main/java/de/tla2b/types/ModelValueType.java
@@ -6,7 +6,7 @@ import de.tla2b.output.TypeVisitorInterface;
public class ModelValueType extends TLAType {
- private static ModelValueType instance = new ModelValueType();
+ private static final ModelValueType instance = new ModelValueType();
private ModelValueType() {
super(MODELVALUE);
@@ -29,10 +29,7 @@ public class ModelValueType extends TLAType {
@Override
public boolean compare(TLAType o) {
- if (o.getKind() == UNTYPED || o.getKind() == MODELVALUE)
- return true;
- else
- return false;
+ return o.getKind() == UNTYPED || o.getKind() == MODELVALUE;
}
@Override
@@ -65,4 +62,4 @@ public class ModelValueType extends TLAType {
public void apply(TypeVisitorInterface visitor) {
visitor.caseModelValueType(this);
}
-}
\ No newline at end of file
+}
diff --git a/src/main/java/de/tla2b/types/StringType.java b/src/main/java/de/tla2b/types/StringType.java
index 2450686343f7bcf9a5813a15fc77cac361076cf3..e88d0ed9a87c68c49f3e0aa47a8ed6dcf861854c 100644
--- a/src/main/java/de/tla2b/types/StringType.java
+++ b/src/main/java/de/tla2b/types/StringType.java
@@ -11,7 +11,7 @@ public class StringType extends TLAType {
super(STRING);
}
- private static StringType instance = new StringType();
+ private static final StringType instance = new StringType();
public static StringType getInstance() {
return instance;
diff --git a/src/main/java/de/tla2b/types/StructOrFunctionType.java b/src/main/java/de/tla2b/types/StructOrFunctionType.java
index 992894174753b4131cf217a16bb095def97aeff6..5b921f8187953efd83528728c3a32d49032c00a9 100644
--- a/src/main/java/de/tla2b/types/StructOrFunctionType.java
+++ b/src/main/java/de/tla2b/types/StructOrFunctionType.java
@@ -10,7 +10,7 @@ import de.tla2b.exceptions.UnificationException;
import de.tla2b.output.TypeVisitorInterface;
public class StructOrFunctionType extends AbstractHasFollowers {
- private LinkedHashMap<String, TLAType> types;
+ private final LinkedHashMap<String, TLAType> types;
public StructOrFunctionType(String name, TLAType type) {
super(STRUCT_OR_FUNCTION);
diff --git a/src/main/java/de/tla2b/types/StructType.java b/src/main/java/de/tla2b/types/StructType.java
index b97a85700868c2e414391927c98f6943c9fc8e8b..2184cfa21a269600efaf965c1d7e5791fbeea3a8 100644
--- a/src/main/java/de/tla2b/types/StructType.java
+++ b/src/main/java/de/tla2b/types/StructType.java
@@ -19,7 +19,7 @@ import de.tla2b.output.TypeVisitorInterface;
import de.tla2bAst.BAstCreator;
public class StructType extends AbstractHasFollowers {
- private LinkedHashMap<String, TLAType> types;
+ private final LinkedHashMap<String, TLAType> types;
private boolean extensible;
private boolean incompleteStruct;
@@ -126,17 +126,9 @@ public class StructType extends AbstractHasFollowers {
if (this.incompleteStruct && otherStruct.incompleteStruct) {
extendStruct = false;
} else if (this.incompleteStruct) {
- if (otherStruct.types.keySet().containsAll(this.types.keySet())) {
- extendStruct = false;
- } else {
- extendStruct = true;
- }
+ extendStruct = !otherStruct.types.keySet().containsAll(this.types.keySet());
} else if (otherStruct.incompleteStruct) {
- if (this.types.keySet().containsAll(otherStruct.types.keySet())) {
- extendStruct = false;
- } else {
- extendStruct = true;
- }
+ extendStruct = !this.types.keySet().containsAll(otherStruct.types.keySet());
} else {
extendStruct = !otherStruct.types.keySet().equals(this.types.keySet());
}
diff --git a/src/main/java/de/tla2b/types/TLAType.java b/src/main/java/de/tla2b/types/TLAType.java
index 790c2b1b3ab6922badde0f037e286496efc45917..c51156890a0bcd8a6da8c01568abeddff6756aa4 100644
--- a/src/main/java/de/tla2b/types/TLAType.java
+++ b/src/main/java/de/tla2b/types/TLAType.java
@@ -4,7 +4,7 @@ import de.be4.classicalb.core.parser.node.PExpression;
import de.tla2b.exceptions.UnificationException;
public abstract class TLAType implements IType {
- private int kind;
+ private final int kind;
public TLAType(int t) {
this.kind = t;
@@ -30,8 +30,8 @@ public abstract class TLAType implements IType {
public TLAType unityAll(TLAType[] types) throws UnificationException{
TLAType current = this;
- for (int i = 0; i < types.length; i++) {
- current = current.unify(types[i]);
+ for (TLAType type : types) {
+ current = current.unify(type);
}
return current;
}
diff --git a/src/main/java/de/tla2b/types/TupleOrFunction.java b/src/main/java/de/tla2b/types/TupleOrFunction.java
index 301800d8fdb7c538cde5a5abcc653a9a6e4c29c6..df6468f3de8a0242c9ed8805f90258e0c1efaa1b 100644
--- a/src/main/java/de/tla2b/types/TupleOrFunction.java
+++ b/src/main/java/de/tla2b/types/TupleOrFunction.java
@@ -77,7 +77,7 @@ public class TupleOrFunction extends AbstractHasFollowers {
boolean isTuple = true;
ArrayList<TLAType> typeList = new ArrayList<TLAType>();
for (int i = 1; i <= types.keySet().size(); i++) {
- if (types.keySet().contains(i)) {
+ if (types.containsKey(i)) {
typeList.add(types.get(i));
} else {
isTuple = false;
@@ -167,10 +167,7 @@ public class TupleOrFunction extends AbstractHasFollowers {
List<TLAType> typeList = new ArrayList<TLAType>();
typeList.addAll(t1.types.values());
typeList.addAll(t2.types.values());
- if (comparable(typeList)) {
- return true;
- }
- return false;
+ return comparable(typeList);
}
@Override
@@ -195,11 +192,7 @@ public class TupleOrFunction extends AbstractHasFollowers {
FunctionType func = new FunctionType();
func.setDomain(IntType.getInstance());
func.setRange(new UntypedType());
- if (func.compare(this)) {
- return false;
- } else {
- return true;
- }
+ return !func.compare(this);
}
@Override
@@ -317,7 +310,6 @@ public class TupleOrFunction extends AbstractHasFollowers {
types.put(entry.getKey(), newType);
if (newType instanceof AbstractHasFollowers) {
((AbstractHasFollowers) newType).addFollower(this);
- ;
}
}
}
diff --git a/src/main/java/de/tla2b/types/UntypedType.java b/src/main/java/de/tla2b/types/UntypedType.java
index fc746ed1e1890e36763d6c182dea46527850b4f8..56dc71d652e496db0f687f441740d9400ca3c037 100644
--- a/src/main/java/de/tla2b/types/UntypedType.java
+++ b/src/main/java/de/tla2b/types/UntypedType.java
@@ -22,10 +22,7 @@ public class UntypedType extends AbstractHasFollowers {
@Override
public boolean compare(TLAType o){
- if(o.contains(this)){
- return false;
- }
- return true;
+ return !o.contains(this);
}
@Override
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index ff61c9d6cfeca5fc4f26268a1855ce50269aa0a5..76c9d52b54d11dbcecd22d3197db1c47f5ec3eac 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -1,14 +1,7 @@
package de.tla2bAst;
-import java.util.ArrayList;
-import java.util.Arrays;
-import java.util.HashSet;
-import java.util.Hashtable;
-import java.util.Iterator;
-import java.util.LinkedList;
-import java.util.List;
+import java.util.*;
import java.util.Map.Entry;
-import java.util.Set;
import tla2sany.semantic.*;
import tla2sany.st.Location;
@@ -59,14 +52,14 @@ public class BAstCreator extends BuiltInOPs
private List<OpDeclNode> bConstants;
- private ModuleNode moduleNode;
+ private final ModuleNode moduleNode;
private UsedExternalFunctions usedExternalFunctions;
- private Definitions bDefinitions = new Definitions();
+ private final Definitions bDefinitions = new Definitions();
private Start start;
- private final Hashtable<Node, TLAType> typeTable = new Hashtable<Node, TLAType>();
- private final HashSet<PositionedNode> sourcePosition = new HashSet<PositionedNode>();
+ private final Hashtable<Node, TLAType> typeTable = new Hashtable<>();
+ private final HashSet<PositionedNode> sourcePosition = new HashSet<>();
private List<String> toplevelUnchangedVariableNames = new ArrayList<>();
public Start expressionStart;
@@ -129,7 +122,7 @@ public class BAstCreator extends BuiltInOPs
this.bConstants = Arrays.asList(moduleNode.getConstantDecls());
}
- machineClauseList = new ArrayList<PMachineClause>();
+ machineClauseList = new ArrayList<>();
AAbstractMachineParseUnit aAbstractMachineParseUnit = new AAbstractMachineParseUnit();
aAbstractMachineParseUnit.setVariant(new AMachineMachineVariant());
@@ -139,7 +132,7 @@ public class BAstCreator extends BuiltInOPs
aAbstractMachineParseUnit.setHeader(machineHeader);
createSetsClause();
- createDefintionClause();
+ createDefinitionClause();
createAbstractConstantsClause();
createConstantsClause();
createPropertyClause();
@@ -154,14 +147,14 @@ public class BAstCreator extends BuiltInOPs
}
private void createSetsClause() {
- if (conEval == null || conEval.getEnumerationSet() == null || conEval.getEnumerationSet().size() == 0)
+ if (conEval == null || conEval.getEnumerationSet() == null || conEval.getEnumerationSet().isEmpty())
return;
ASetsMachineClause setsClause = new ASetsMachineClause();
ArrayList<EnumType> printed = new ArrayList<EnumType>();
OpDeclNode[] cons = moduleNode.getConstantDecls();
- for (int i = 0; i < cons.length; i++) {
- TLAType type = (TLAType) cons[i].getToolObject(TYPE_ID);
+ for (OpDeclNode con : cons) {
+ TLAType type = (TLAType) con.getToolObject(TYPE_ID);
EnumType e = null;
if (type instanceof SetType) {
@@ -179,14 +172,14 @@ public class BAstCreator extends BuiltInOPs
}
}
- ArrayList<PSet> sets = new ArrayList<PSet>();
+ ArrayList<PSet> sets = new ArrayList<>();
for (int i = 0; i < printed.size(); i++) {
AEnumeratedSetSet eSet = new AEnumeratedSetSet();
printed.get(i).id = i + 1;
eSet.setIdentifier(createTIdentifierLiteral("ENUM" + (i + 1)));
- List<PExpression> list = new ArrayList<PExpression>();
- for (Iterator<String> iterator = printed.get(i).modelvalues.iterator(); iterator.hasNext();) {
- list.add(createIdentifierNode(iterator.next()));
+ List<PExpression> list = new ArrayList<>();
+ for (String s : printed.get(i).modelvalues) {
+ list.add(createIdentifierNode(s));
}
eSet.setElements(list);
sets.add(eSet);
@@ -196,8 +189,8 @@ public class BAstCreator extends BuiltInOPs
}
- private void createDefintionClause() {
- ArrayList<OpDefNode> bDefs = new ArrayList<OpDefNode>();
+ private void createDefinitionClause() {
+ ArrayList<OpDefNode> bDefs = new ArrayList<>();
for (int i = 0; i < moduleNode.getOpDefs().length; i++) {
OpDefNode def = moduleNode.getOpDefs()[i];
if (specAnalyser.getBDefinitions().contains(def)) {
@@ -213,10 +206,8 @@ public class BAstCreator extends BuiltInOPs
}
- List<PDefinition> defs = new ArrayList<PDefinition>();
-
Set<EXTERNAL_FUNCTIONS> set = usedExternalFunctions.getUsedExternalFunctions();
- defs.addAll(createDefinitionsForExternalFunctions(set));
+ List<PDefinition> defs = new ArrayList<>(createDefinitionsForExternalFunctions(set));
for (OpDefNode opDefNode : bDefs) {
List<PExpression> list = new ArrayList<PExpression>();
@@ -263,7 +254,7 @@ public class BAstCreator extends BuiltInOPs
}
private ArrayList<PDefinition> createDefinitionsForExternalFunctions(Set<EXTERNAL_FUNCTIONS> set) {
- ArrayList<PDefinition> list = new ArrayList<PDefinition>();
+ ArrayList<PDefinition> list = new ArrayList<>();
if (set.contains(UsedExternalFunctions.EXTERNAL_FUNCTIONS.CHOOSE)) {
AExpressionDefinitionDefinition def1 = new AExpressionDefinitionDefinition();
@@ -283,7 +274,7 @@ public class BAstCreator extends BuiltInOPs
if (set.contains(UsedExternalFunctions.EXTERNAL_FUNCTIONS.ASSERT)) {
APredicateDefinitionDefinition def1 = new APredicateDefinitionDefinition();
def1.setName(new TDefLiteralPredicate("ASSERT_TRUE"));
- ArrayList<PExpression> params = new ArrayList<PExpression>();
+ ArrayList<PExpression> params = new ArrayList<>();
params.add(createIdentifierNode("P"));
params.add(createIdentifierNode("Msg"));
def1.setParameters(params);
@@ -293,7 +284,7 @@ public class BAstCreator extends BuiltInOPs
AExpressionDefinitionDefinition def2 = new AExpressionDefinitionDefinition();
def2.setName(new TIdentifierLiteral("EXTERNAL_PREDICATE_ASSERT_TRUE"));
- def2.setParameters(new ArrayList<PExpression>());
+ def2.setParameters(new ArrayList<>());
AMultOrCartExpression cart = new AMultOrCartExpression();
cart.setLeft(new ABoolSetExpression());
cart.setRight(new AStringSetExpression());
@@ -305,13 +296,12 @@ public class BAstCreator extends BuiltInOPs
private void createOperationsClause() {
ArrayList<BOperation> bOperations = specAnalyser.getBOperations();
- if (bOperations == null || bOperations.size() == 0) {
+ if (bOperations == null || bOperations.isEmpty()) {
return;
}
- List<POperation> opList = new ArrayList<POperation>();
- for (int i = 0; i < bOperations.size(); i++) {
- BOperation op = bOperations.get(i);
+ List<POperation> opList = new ArrayList<>();
+ for (BOperation op : bOperations) {
opList.add(op.getBOperation(this));
}
@@ -323,14 +313,14 @@ public class BAstCreator extends BuiltInOPs
OpDeclNode[] vars = moduleNode.getVariableDecls();
if (vars.length == 0)
return;
- List<PExpression> varList = new ArrayList<PExpression>();
- for (int i = 0; i < vars.length; i++) {
- varList.add(createIdentifierNode(vars[i]));
+ List<PExpression> varList = new ArrayList<>();
+ for (OpDeclNode var : vars) {
+ varList.add(createIdentifierNode(var));
}
ABecomesSuchSubstitution becomes = new ABecomesSuchSubstitution();
becomes.setIdentifiers(varList);
- List<PPredicate> predList = new ArrayList<PPredicate>();
+ List<PPredicate> predList = new ArrayList<>();
for (ExprNode node : specAnalyser.getInits()) {
predList.add(visitExprNodePredicate(node));
}
@@ -344,8 +334,8 @@ public class BAstCreator extends BuiltInOPs
private void createVariableClause() {
List<OpDeclNode> bVariables = Arrays.asList(moduleNode.getVariableDecls());
- if (bVariables.size() > 0) {
- List<PExpression> list = new ArrayList<PExpression>();
+ if (!bVariables.isEmpty()) {
+ List<PExpression> list = new ArrayList<>();
for (OpDeclNode opDeclNode : bVariables) {
AIdentifierExpression id = createPositionedNode(
@@ -360,7 +350,7 @@ public class BAstCreator extends BuiltInOPs
}
private void createAbstractConstantsClause() {
- List<PExpression> constantsList = new ArrayList<PExpression>();
+ List<PExpression> constantsList = new ArrayList<>();
for (RecursiveDefinition recDef : specAnalyser.getRecursiveDefinitions()) {
AIdentifierExpression id = createPositionedNode(
@@ -378,7 +368,7 @@ public class BAstCreator extends BuiltInOPs
typeTable.put(id, type);
}
- if (constantsList.size() > 0) {
+ if (!constantsList.isEmpty()) {
AAbstractConstantsMachineClause abstractConstantsClause = new AAbstractConstantsMachineClause(
constantsList);
machineClauseList.add(abstractConstantsClause);
@@ -393,7 +383,7 @@ public class BAstCreator extends BuiltInOPs
bConstants = Arrays.asList(moduleNode.getConstantDecls());
}
- List<PExpression> constantsList = new ArrayList<PExpression>();
+ List<PExpression> constantsList = new ArrayList<>();
for (OpDeclNode opDeclNode : bConstants) {
AIdentifierExpression id = createPositionedNode(
new AIdentifierExpression(createTIdentifierLiteral(getName(opDeclNode))), opDeclNode);
@@ -401,7 +391,7 @@ public class BAstCreator extends BuiltInOPs
TLAType type = (TLAType) opDeclNode.getToolObject(TYPE_ID);
typeTable.put(id, type);
}
- if (constantsList.size() > 0) {
+ if (!constantsList.isEmpty()) {
AConstantsMachineClause constantsClause = new AConstantsMachineClause(constantsList);
machineClauseList.add(constantsClause);
}
@@ -416,7 +406,7 @@ public class BAstCreator extends BuiltInOPs
}
private void createPropertyClause() {
- List<PPredicate> propertiesList = new ArrayList<PPredicate>();
+ List<PPredicate> propertiesList = new ArrayList<>();
propertiesList.addAll(evalRecursiveDefinitions());
propertiesList.addAll(evalRecursiveFunctions());
for (OpDeclNode con : bConstants) {
@@ -456,9 +446,7 @@ public class BAstCreator extends BuiltInOPs
}
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();
OpDefNode generatedDef = entry.getValue();
OpDefNode def = null;
@@ -481,7 +469,7 @@ public class BAstCreator extends BuiltInOPs
}
AssumeNode[] assumes = moduleNode.getAssumptions();
- List<PPredicate> assertionList = new ArrayList<PPredicate>();
+ List<PPredicate> assertionList = new ArrayList<>();
for (AssumeNode assumeNode : assumes) {
ThmOrAssumpDefNode def = assumeNode.getDef();
if (def != null) {
@@ -492,12 +480,12 @@ public class BAstCreator extends BuiltInOPs
propertiesList.add(visitAssumeNode(assumeNode));
}
}
- if (propertiesList.size() > 0) {
+ if (!propertiesList.isEmpty()) {
APropertiesMachineClause propertiesClause = new APropertiesMachineClause();
propertiesClause.setPredicates(createConjunction(propertiesList));
machineClauseList.add(propertiesClause);
}
- if (assertionList.size() > 0) {
+ if (!assertionList.isEmpty()) {
AAssertionsMachineClause assertionClause = new AAssertionsMachineClause();
assertionClause.setPredicates(assertionList);
machineClauseList.add(assertionClause);
@@ -561,7 +549,7 @@ public class BAstCreator extends BuiltInOPs
return new AIntegerExpression(new TIntegerLiteral(tlcValue.toString()));
case SETENUMVALUE: {
SetEnumValue s = (SetEnumValue) tlcValue;
- ArrayList<PExpression> list = new ArrayList<PExpression>();
+ ArrayList<PExpression> list = new ArrayList<>();
for (int i = 0; i < s.elems.size(); i++) {
Value v = s.elems.elementAt(i);
list.add(createTLCValue(v));
@@ -584,12 +572,12 @@ public class BAstCreator extends BuiltInOPs
private void createInvariantClause() {
OpDeclNode[] vars = moduleNode.getVariableDecls();
- List<PPredicate> predList = new ArrayList<PPredicate>();
- for (int i = 0; i < vars.length; i++) {
- TLAType varType = (TLAType) vars[i].getToolObject(TYPE_ID);
+ List<PPredicate> predList = new ArrayList<>();
+ for (OpDeclNode var : vars) {
+ TLAType varType = (TLAType) var.getToolObject(TYPE_ID);
AMemberPredicate member = new AMemberPredicate();
- member.setLeft(createIdentifierNode(vars[i]));
+ member.setLeft(createIdentifierNode(var));
member.setRight(varType.getBNode());
predList.add(member);
@@ -612,7 +600,7 @@ public class BAstCreator extends BuiltInOPs
}
}
- if (predList.size() > 0) {
+ if (!predList.isEmpty()) {
AInvariantMachineClause invClause = new AInvariantMachineClause(createConjunction(predList));
machineClauseList.add(invClause);
}
@@ -631,7 +619,8 @@ public class BAstCreator extends BuiltInOPs
LetInNode letInNode = (LetInNode) exprNode;
return visitExprNodePredicate(letInNode.getBody());
}
- case NumeralKind: {
+ case NumeralKind:
+ case DecimalKind: {
throw new RuntimeException();
}
default:
@@ -659,10 +648,7 @@ public class BAstCreator extends BuiltInOPs
AtNode at = (AtNode) exprNode;
TLAType type = (TLAType) at.getExceptRef().getToolObject(TYPE_ID);
OpApplNode seq = at.getAtModifier();
- LinkedList<ExprOrOpArgNode> list = new LinkedList<ExprOrOpArgNode>();
- for (int j = 0; j < seq.getArgs().length; j++) {
- list.add(seq.getArgs()[j]);
- }
+ LinkedList<ExprOrOpArgNode> list = new LinkedList<>(Arrays.asList(seq.getArgs()));
// PExpression base = visitExprNodeExpression(at.getAtBase());
PExpression base = (PExpression) at.getExceptComponentRef().getToolObject(EXCEPT_BASE);
return evalAtNode(list, type, base.clone());
@@ -678,7 +664,7 @@ public class BAstCreator extends BuiltInOPs
}
private PExpression evalAtNode(LinkedList<ExprOrOpArgNode> list, TLAType type, PExpression base) {
- if (list.size() == 0) {
+ if (list.isEmpty()) {
return base;
}
if (type instanceof FunctionType) {
@@ -740,10 +726,10 @@ public class BAstCreator extends BuiltInOPs
if (recursiveFunctionHandler.isRecursiveFunction(param)) {
ArrayList<SymbolNode> list = recursiveFunctionHandler.getAdditionalParams(param);
- if (list.size() > 0) {
+ if (!list.isEmpty()) {
AFunctionExpression call = new AFunctionExpression();
call.setIdentifier(createIdentifierNode(param));
- ArrayList<PExpression> params = new ArrayList<PExpression>();
+ ArrayList<PExpression> params = new ArrayList<>();
for (SymbolNode symbolNode : list) {
params.add(createIdentifierNode(symbolNode));
}
@@ -756,14 +742,14 @@ public class BAstCreator extends BuiltInOPs
if (tuple.length == 1) {
AFunctionExpression functionCall = new AFunctionExpression();
functionCall.setIdentifier(createIdentifierNode(n.getOperator()));
- List<PExpression> paramList = new ArrayList<PExpression>();
+ List<PExpression> paramList = new ArrayList<>();
paramList.add(new AIntegerExpression(new TIntegerLiteral("1")));
functionCall.setParameters(paramList);
return functionCall;
} else {
StringBuilder sb = new StringBuilder();
- List<TLAType> typeList = new ArrayList<TLAType>();
+ List<TLAType> typeList = new ArrayList<>();
int number = -1;
for (int j = 0; j < tuple.length; j++) {
FormalParamNode p = tuple[j];
@@ -776,8 +762,7 @@ public class BAstCreator extends BuiltInOPs
}
TupleType tupleType = new TupleType(typeList);
PExpression id = createIdentifierNode(sb.toString());
- PExpression prj = createProjectionFunction(id, number, tupleType);
- return prj;
+ return createProjectionFunction(id, number, tupleType);
}
}
return createIdentifierNode(n.getOperator());
@@ -804,7 +789,7 @@ public class BAstCreator extends BuiltInOPs
return new AEqualPredicate(createIdentifierNode(def), new ABooleanTrueExpression());
}
if (Arrays.asList(moduleNode.getOpDefs()).contains(def)) {
- List<PExpression> params = new ArrayList<PExpression>();
+ List<PExpression> params = new ArrayList<>();
for (int i = 0; i < n.getArgs().length; i++) {
params.add(visitExprOrOpArgNodeExpression(n.getArgs()[i]));
}
@@ -825,8 +810,7 @@ public class BAstCreator extends BuiltInOPs
FormalParamNode param = params[i];
param.setToolObject(SUBSTITUTE_PARAM, n.getArgs()[i]);
}
- PPredicate result = visitExprNodePredicate(def.getBody());
- return result;
+ return visitExprNodePredicate(def.getBody());
}
}
@@ -844,10 +828,10 @@ public class BAstCreator extends BuiltInOPs
if (specAnalyser.getRecursiveFunctions().contains(def)) {
ArrayList<SymbolNode> list = recursiveFunctionHandler.getAdditionalParams(def);
- if (list.size() > 0) {
+ if (!list.isEmpty()) {
AFunctionExpression call = new AFunctionExpression();
call.setIdentifier(createIdentifierNode(def));
- ArrayList<PExpression> params = new ArrayList<PExpression>();
+ ArrayList<PExpression> params = new ArrayList<>();
for (SymbolNode symbolNode : list) {
params.add(createIdentifierNode(symbolNode));
}
@@ -859,7 +843,7 @@ public class BAstCreator extends BuiltInOPs
}
if (Arrays.asList(moduleNode.getOpDefs()).contains(def)) {
- List<PExpression> params = new ArrayList<PExpression>();
+ List<PExpression> params = new ArrayList<>();
for (int i = 0; i < n.getArgs().length; i++) {
params.add(visitExprOrOpArgNodeExpression(n.getArgs()[i]));
}
@@ -875,7 +859,7 @@ public class BAstCreator extends BuiltInOPs
name = getName(entry.getKey());
}
}
- if (params.size() == 0) {
+ if (params.isEmpty()) {
return createIdentifierNode(name);
} else {
AFunctionExpression funcCall = new AFunctionExpression();
@@ -903,8 +887,7 @@ public class BAstCreator extends BuiltInOPs
FormalParamNode param = params[i];
param.setToolObject(SUBSTITUTE_PARAM, n.getArgs()[i]);
}
- PExpression result = visitExprNodeExpression(def.getBody());
- return result;
+ return visitExprNodeExpression(def.getBody());
}
}
@@ -951,7 +934,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]));
if (opApplNode.getArgs()[1] instanceof StringNode) {
StringNode stringNode = (StringNode) opApplNode.getArgs()[1];
@@ -1467,7 +1450,7 @@ public class BAstCreator extends BuiltInOPs
case OPCODE_fa: { // f[1]
TLAType t = (TLAType) n.getArgs()[0].getToolObject(TYPE_ID);
- if (t != null && t instanceof TupleType) {
+ if (t instanceof TupleType) {
NumeralNode num = (NumeralNode) n.getArgs()[1];
int field = num.val();
PExpression pair = visitExprOrOpArgNodeExpression(n.getArgs()[0]);
@@ -1725,9 +1708,7 @@ public class BAstCreator extends BuiltInOPs
OpApplNode seq = (OpApplNode) first;
LinkedList<ExprOrOpArgNode> seqList = new LinkedList<ExprOrOpArgNode>();
- for (int j = 0; j < seq.getArgs().length; j++) {
- seqList.add(seq.getArgs()[j]);
- }
+ Collections.addAll(seqList, seq.getArgs());
pair.setToolObject(EXCEPT_BASE, res.clone());
res = evalExceptValue(res.clone(), seqList, structType, val);
@@ -1746,9 +1727,7 @@ public class BAstCreator extends BuiltInOPs
OpApplNode seq = (OpApplNode) first;
LinkedList<ExprOrOpArgNode> seqList = new LinkedList<ExprOrOpArgNode>();
- for (int j = 0; j < seq.getArgs().length; j++) {
- seqList.add(seq.getArgs()[j]);
- }
+ Collections.addAll(seqList, seq.getArgs());
pair.setToolObject(EXCEPT_BASE, res.clone());
res = evalExceptValue(res.clone(), seqList, func, val);
@@ -1801,7 +1780,7 @@ public class BAstCreator extends BuiltInOPs
}
- throw new NotImplementedException("Missing support for operator: " + n.getOperator().getName().toString());
+ throw new NotImplementedException("Missing support for operator: " + n.getOperator().getName());
}
private List<PExpression> createListOfIdentifier(FormalParamNode[][] params) {
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index a9e9bf1445e84bd7ee38676feb28f07d43183b2c..0677795fa451dbf448aaa68b0d137e0823079268 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -10,6 +10,7 @@ import java.io.IOException;
import java.io.OutputStreamWriter;
import java.io.PrintWriter;
import java.io.UnsupportedEncodingException;
+import java.nio.charset.StandardCharsets;
import java.util.Hashtable;
import de.be4.classicalb.core.parser.BParser;
@@ -130,7 +131,7 @@ public class Translator implements TranslationGlobals {
try {
configFile.createNewFile();
BufferedWriter out = new BufferedWriter(
- new OutputStreamWriter(new FileOutputStream(configFile), "UTF-8"));
+ new OutputStreamWriter(new FileOutputStream(configFile), StandardCharsets.UTF_8));
try {
out.write(configString);
} finally {
@@ -150,7 +151,7 @@ public class Translator implements TranslationGlobals {
try {
moduleFile = new File("temp/" + moduleName + ".tla");
moduleFile.createNewFile();
- BufferedWriter out = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(moduleFile), "UTF-8"));
+ BufferedWriter out = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(moduleFile), StandardCharsets.UTF_8));
try {
out.write(moduleString);
} finally {
@@ -264,7 +265,7 @@ public class Translator implements TranslationGlobals {
try {
probFile.createNewFile();
} catch (IOException e) {
- System.err.println(String.format("Could not create File %s.", probFile.getName()));
+ System.err.printf("Could not create File %s.%n", probFile.getName());
System.exit(-1);
}
@@ -315,7 +316,7 @@ public class Translator implements TranslationGlobals {
try {
machineFile.createNewFile();
} catch (IOException e) {
- System.err.println(String.format("Could not create File %s.", machineFile.getName()));
+ System.err.printf("Could not create File %s.%n", machineFile.getName());
System.exit(-1);
}
@@ -325,7 +326,7 @@ public class Translator implements TranslationGlobals {
String result = "/*@ generated by TLA2B " + VERSION_NUMBER + " */\n" + pp.getPrettyPrint();
try {
- BufferedWriter out = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(machineFile), "UTF-8"));
+ BufferedWriter out = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(machineFile), StandardCharsets.UTF_8));
try {
out.write(result);
} finally {
diff --git a/src/test/java/de/tla2b/typechecking/BBuiltInsTest.java b/src/test/java/de/tla2b/typechecking/BBuiltInsTest.java
index 1268d5f5b32d94bb4f94ede9217c85b2f538d1ce..477632042a2eeaafe1083335fc8a25f5dd78b6ff 100644
--- a/src/test/java/de/tla2b/typechecking/BBuiltInsTest.java
+++ b/src/test/java/de/tla2b/typechecking/BBuiltInsTest.java
@@ -18,7 +18,7 @@ public class BBuiltInsTest {
* BOOLEAN
*/
@Test
- public void testBoolean() throws FrontEndException, TLA2BException {
+ public void testBoolean() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k = BOOLEAN \n"
@@ -28,7 +28,7 @@ public class BBuiltInsTest {
}
@Test (expected = TypeErrorException.class)
- public void testBooleanException() throws FrontEndException, TLA2BException {
+ public void testBooleanException() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME 1 \\in BOOLEAN \n"
@@ -42,7 +42,7 @@ public class BBuiltInsTest {
* String
*/
@Test
- public void testString() throws FrontEndException, TLA2BException {
+ public void testString() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k = STRING \n"
@@ -52,7 +52,7 @@ public class BBuiltInsTest {
}
@Test (expected = TypeErrorException.class)
- public void testUnifyErrorString() throws FrontEndException, TLA2BException {
+ public void testUnifyErrorString() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME 1 = STRING \n"
@@ -64,7 +64,7 @@ public class BBuiltInsTest {
* Bool value: TRUE, FALSE
*/
@Test
- public void testBoolValue() throws FrontEndException, TLA2BException {
+ public void testBoolValue() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k = TRUE \n"
@@ -74,7 +74,7 @@ public class BBuiltInsTest {
}
@Test (expected = TypeErrorException.class)
- public void testUnifyErrorBoolValue() throws FrontEndException, TLA2BException {
+ public void testUnifyErrorBoolValue() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "ASSUME 1 = TRUE \n"
+ "=================================";
diff --git a/src/test/java/de/tla2b/typechecking/ConfigTest.java b/src/test/java/de/tla2b/typechecking/ConfigTest.java
index 8729051e5ca00dccb747c3441df2736ec0cda80e..08afa569efd5c3cbe400751ecb32c5e91d9090aa 100644
--- a/src/test/java/de/tla2b/typechecking/ConfigTest.java
+++ b/src/test/java/de/tla2b/typechecking/ConfigTest.java
@@ -13,16 +13,16 @@ import de.tla2b.util.TestUtil;
public class ConfigTest {
@Test
- public void TestConAssignment() throws FrontEndException, TLA2BException {
+ public void TestConAssignment() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n" + "=================================";
final String config = "CONSTANTS k = 1";
TestTypeChecker t = TestUtil.typeCheckString(module, config);
- assertEquals("INTEGER", t.getConstantType("k").toString());
+ assertEquals("INTEGER", t.getConstantType("k"));
}
@Test
- public void TestConOverride() throws FrontEndException, TLA2BException {
+ public void TestConOverride() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "foo == 1\n"
@@ -30,7 +30,7 @@ public class ConfigTest {
+ "=================================";
final String config = "CONSTANTS k <- foo";
TestTypeChecker t = TestUtil.typeCheckString(module, config);
- assertEquals("INTEGER", t.getConstantType("k2").toString());
+ assertEquals("INTEGER", t.getConstantType("k2"));
}
// TODO DefOverriding
diff --git a/src/test/java/de/tla2b/typechecking/ConstantTypesTest.java b/src/test/java/de/tla2b/typechecking/ConstantTypesTest.java
index 26544543bfad5b9905baa4b1a1955248b37d6968..b454878cb39c20d7462937a565b91a395840e8dd 100644
--- a/src/test/java/de/tla2b/typechecking/ConstantTypesTest.java
+++ b/src/test/java/de/tla2b/typechecking/ConstantTypesTest.java
@@ -14,7 +14,7 @@ import de.tla2b.util.TestUtil;
public class ConstantTypesTest {
@Test
- public void test1() throws FrontEndException, TLA2BException {
+ public void test1() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "ASSUME k = 1 /\\ k2 = k\n"
@@ -25,7 +25,7 @@ public class ConstantTypesTest {
}
@Test
- public void test2() throws FrontEndException, TLA2BException {
+ public void test2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "ASSUME k = k2 /\\ k = 1\n"
@@ -37,7 +37,7 @@ public class ConstantTypesTest {
}
@Test
- public void test3() throws FrontEndException, TLA2BException {
+ public void test3() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3 \n"
+ "ASSUME k = k2 /\\ k = k3 /\\ k3 = 1\n"
@@ -49,7 +49,7 @@ public class ConstantTypesTest {
}
@Test
- public void worstCaseUnification() throws FrontEndException, TLA2BException {
+ public void worstCaseUnification() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS a, b, c, d, e, f, g, h \n"
+ "ASSUME a = b \n"
@@ -74,14 +74,14 @@ public class ConstantTypesTest {
}
@Test(expected = TypeErrorException.class)
- public void prime() throws FrontEndException, TLA2BException {
+ public void prime() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "Next == 1' = 1 \n" + "=================================";
TestUtil.typeCheckString(module);
}
@Test(expected = TypeErrorException.class)
- public void prime2() throws FrontEndException, TLA2BException {
+ public void prime2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k\n"
+ "foo == k' = 1 \n"
@@ -90,7 +90,7 @@ public class ConstantTypesTest {
}
@Test
- public void ifThenElse() throws FrontEndException, TLA2BException {
+ public void ifThenElse() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2\n"
+ "ASSUME k = IF 1 = 1 THEN k2 ELSE 1 \n"
diff --git a/src/test/java/de/tla2b/typechecking/DefinitionsTest.java b/src/test/java/de/tla2b/typechecking/DefinitionsTest.java
index 336fe4fce12414cbadc6588eb5848d5c388c98bb..1eaf7afe62d3df216c98950b5204b5fa842d8588 100644
--- a/src/test/java/de/tla2b/typechecking/DefinitionsTest.java
+++ b/src/test/java/de/tla2b/typechecking/DefinitionsTest.java
@@ -16,7 +16,7 @@ public class DefinitionsTest {
* Definition: foo(a,b) == e
*/
@Test
- public void testDefinition() throws FrontEndException, TLA2BException {
+ public void testDefinition() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "foo(a,b) == a = 1 /\\ b = TRUE \n"
+ "Next == foo(1,TRUE) \n"
@@ -28,7 +28,7 @@ public class DefinitionsTest {
}
@Test
- public void testDefinition2() throws FrontEndException, TLA2BException {
+ public void testDefinition2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "foo(a,b) == a = k /\\ b = k2 \n"
@@ -44,7 +44,7 @@ public class DefinitionsTest {
}
@Test
- public void testDefinition3() throws FrontEndException, TLA2BException {
+ public void testDefinition3() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "foo == k \n"
@@ -56,7 +56,7 @@ public class DefinitionsTest {
}
@Test
- public void testDefinition4() throws FrontEndException, TLA2BException {
+ public void testDefinition4() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "foo(var, value) == var = value \n"
@@ -73,7 +73,7 @@ public class DefinitionsTest {
*/
@Test
- public void testDefinitionCall() throws FrontEndException, TLA2BException {
+ public void testDefinitionCall() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "foo(a) == TRUE \n"
+ "bar == foo(1) \n"
@@ -85,7 +85,7 @@ public class DefinitionsTest {
}
@Test
- public void testDefinitionCall2() throws FrontEndException, TLA2BException {
+ public void testDefinitionCall2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "foo(a) == a \n"
+ "bar == foo(1) \n"
@@ -99,7 +99,7 @@ public class DefinitionsTest {
}
@Test
- public void testDefinitionCall3() throws FrontEndException, TLA2BException {
+ public void testDefinitionCall3() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "foo(a) == a \n"
@@ -116,7 +116,7 @@ public class DefinitionsTest {
}
@Test
- public void testDefinitionCall4() throws FrontEndException, TLA2BException {
+ public void testDefinitionCall4() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "foo(a,b) == a \\cup b \n"
@@ -133,7 +133,7 @@ public class DefinitionsTest {
}
@Test
- public void testDefinitionCall5() throws FrontEndException, TLA2BException {
+ public void testDefinitionCall5() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "foo(a,b) == a = b \n"
@@ -146,7 +146,7 @@ public class DefinitionsTest {
}
@Test
- public void testDefinitionCall6() throws FrontEndException, TLA2BException {
+ public void testDefinitionCall6() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "foo(a,b) == a = b \n"
@@ -163,7 +163,7 @@ public class DefinitionsTest {
}
@Test
- public void testDefinitionCall7() throws FrontEndException, TLA2BException {
+ public void testDefinitionCall7() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3 \n"
+ "foo(a,b) == a \\cup b \n"
@@ -182,7 +182,7 @@ public class DefinitionsTest {
}
@Test
- public void testDefinitionCall8() throws FrontEndException, TLA2BException {
+ public void testDefinitionCall8() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "foo(a) == k = a \n"
@@ -199,7 +199,7 @@ public class DefinitionsTest {
}
@Test
- public void testDefinitionCall9() throws FrontEndException, TLA2BException {
+ public void testDefinitionCall9() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "foo(a,b) == a = b \n"
@@ -214,7 +214,7 @@ public class DefinitionsTest {
}
@Test
- public void testDefinitionCall10() throws FrontEndException, TLA2BException {
+ public void testDefinitionCall10() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "foo(a,b) == a= 1 /\\ b = TRUE \n"
+ "ASSUME foo(1, TRUE) \n"
diff --git a/src/test/java/de/tla2b/typechecking/ExceptTest.java b/src/test/java/de/tla2b/typechecking/ExceptTest.java
index ea2965af27279deb98ae04bf96c8be0284978e64..0eaf918b5c13499807f9deff2e02db77ea7de29e 100644
--- a/src/test/java/de/tla2b/typechecking/ExceptTest.java
+++ b/src/test/java/de/tla2b/typechecking/ExceptTest.java
@@ -14,7 +14,7 @@ import de.tla2b.util.TestUtil;
public class ExceptTest {
@Test
- public void testFunction() throws FrontEndException, TLA2BException {
+ public void testFunction() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "ASSUME k = [k2 EXCEPT ![TRUE] = 0] \n"
@@ -26,7 +26,7 @@ public class ExceptTest {
}
@Test
- public void testFunctionRecord() throws FrontEndException, TLA2BException {
+ public void testFunctionRecord() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
+ "CONSTANTS k, k2 \n"
@@ -39,7 +39,7 @@ public class ExceptTest {
}
@Test
- public void testFunctionRecord2() throws FrontEndException, TLA2BException {
+ public void testFunctionRecord2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
+ "CONSTANTS k, k2 \n"
@@ -51,19 +51,18 @@ public class ExceptTest {
}
@Test
- public void testRecord() throws FrontEndException, TLA2BException {
+ public void testRecord() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
+ "CONSTANTS k \n"
+ "ASSUME k = [k EXCEPT !.a = 2, !.b = TRUE] \n"
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("struct(a:INTEGER,b:BOOL)", t.getConstantType("k")
- .toString());
+ assertEquals("struct(a:INTEGER,b:BOOL)", t.getConstantType("k"));
}
@Test (expected = TypeErrorException.class)
- public void testRecordOrFunction() throws FrontEndException, TLA2BException {
+ public void testRecordOrFunction() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
+ "CONSTANTS a, b \n"
diff --git a/src/test/java/de/tla2b/typechecking/FunctionTest.java b/src/test/java/de/tla2b/typechecking/FunctionTest.java
index 8b528b41e9bb063fbd8ce3a60149fe978ea169cb..9fa32603ce9b16128a37ebe0598a319172efc8d1 100644
--- a/src/test/java/de/tla2b/typechecking/FunctionTest.java
+++ b/src/test/java/de/tla2b/typechecking/FunctionTest.java
@@ -18,8 +18,8 @@ public class FunctionTest {
*/
@Test
- public void testSimpleFunctionConstructor() throws FrontEndException,
- TLA2BException {
+ public void testSimpleFunctionConstructor() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
+ "CONSTANTS k \n"
@@ -30,8 +30,8 @@ public class FunctionTest {
}
@Test
- public void testFunctionConstructor() throws FrontEndException,
- TLA2BException {
+ public void testFunctionConstructor() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, S \n"
+ "ASSUME k = [x \\in S |-> x = k2] /\\ k2 = 1 \n"
@@ -43,57 +43,53 @@ public class FunctionTest {
}
@Test
- public void testFunctionConstructorTwoVariables() throws FrontEndException,
- TLA2BException {
+ public void testFunctionConstructorTwoVariables() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k = [x,y \\in {1} |-> TRUE] \n"
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("POW(INTEGER*INTEGER*BOOL)", t.getConstantType("k")
- .toString());
+ assertEquals("POW(INTEGER*INTEGER*BOOL)", t.getConstantType("k"));
}
@Test
- public void testFunctionConstructor2() throws FrontEndException,
- TLA2BException {
+ public void testFunctionConstructor2() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k = [<<x,y>> \\in {<<1,TRUE>>} |-> TRUE] \n"
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("POW(INTEGER*BOOL*BOOL)", t.getConstantType("k")
- .toString());
+ assertEquals("POW(INTEGER*BOOL*BOOL)", t.getConstantType("k"));
}
@Test
- public void testFunctionConstructor6() throws FrontEndException,
- TLA2BException {
+ public void testFunctionConstructor6() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k = [x \\in {1}, <<y,z>> \\in {<<1,TRUE>>} |-> TRUE] \n"
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("POW(INTEGER*(INTEGER*BOOL)*BOOL)", t.getConstantType("k")
- .toString());
+ assertEquals("POW(INTEGER*(INTEGER*BOOL)*BOOL)", t.getConstantType("k"));
}
@Test
public void testFunctionConstructorTwoVariables2()
- throws FrontEndException, TLA2BException {
+ throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k = [x \\in {1}, y \\in BOOLEAN |-> TRUE] \n"
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("POW(INTEGER*BOOL*BOOL)", t.getConstantType("k")
- .toString());
+ assertEquals("POW(INTEGER*BOOL*BOOL)", t.getConstantType("k"));
}
@Test(expected = TypeErrorException.class)
- public void testFunctionConstructorFail() throws FrontEndException,
- TLA2BException {
+ public void testFunctionConstructorFail() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k = [<<x,y>> \\in {1} |-> TRUE] \n"
@@ -102,8 +98,8 @@ public class FunctionTest {
}
@Test (expected = TypeErrorException.class)
- public void testFunctionConstructorFail2() throws FrontEndException,
- TLA2BException {
+ public void testFunctionConstructorFail2() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k = [<<x,y,z>> \\in ({1} \\times {1}) |-> TRUE] \n"
@@ -112,8 +108,8 @@ public class FunctionTest {
}
@Test
- public void testFunctionConstructor3() throws FrontEndException,
- TLA2BException {
+ public void testFunctionConstructor3() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, S, S2 \n"
+ "ASSUME k = [x,y \\in S, z \\in S2 |-> z] /\\ S = BOOLEAN /\\ S2 = {1} \n"
@@ -125,8 +121,8 @@ public class FunctionTest {
}
@Test
- public void testFunctionConstructor4() throws FrontEndException,
- TLA2BException {
+ public void testFunctionConstructor4() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, S, S2 \n"
+ "ASSUME [x \\in S |-> k] = [x \\in S2 |-> x=k2] /\\ k2 = 1 \n"
@@ -139,8 +135,8 @@ public class FunctionTest {
}
@Test
- public void testFunctionConstructor5() throws FrontEndException,
- TLA2BException {
+ public void testFunctionConstructor5() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS S, S2 \n"
+ "ASSUME [x \\in S, y \\in S2 |-> 1] = [x,y \\in {1} |-> 1] \n"
@@ -151,8 +147,8 @@ public class FunctionTest {
}
@Test(expected = TypeErrorException.class)
- public void testFunctionConstructorException() throws FrontEndException,
- TLA2BException {
+ public void testFunctionConstructorException() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, S, S2 \n"
+ "ASSUME [x \\in S, y \\in S2 |-> 1] = [x \\in {1} |-> 1] \n"
@@ -164,8 +160,8 @@ public class FunctionTest {
* recursive Function
*/
@Test
- public void testRecursiveFunction() throws FrontEndException,
- TLA2BException {
+ public void testRecursiveFunction() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
+ "CONSTANTS k, k2, k3 \n"
@@ -183,7 +179,7 @@ public class FunctionTest {
*/
@Test
- public void testFunctionCall() throws FrontEndException, TLA2BException {
+ public void testFunctionCall() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
+ "CONSTANTS k \n"
@@ -193,7 +189,7 @@ public class FunctionTest {
}
@Test
- public void testFunctionCall2() throws FrontEndException, TLA2BException {
+ public void testFunctionCall2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
+ "CONSTANTS k \n"
@@ -204,22 +200,21 @@ public class FunctionTest {
}
@Test
- public void testFunctionCall3() throws FrontEndException, TLA2BException {
+ public void testFunctionCall3() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3, S \n"
+ "ASSUME k[k2,TRUE] = k3 \n"
+ "ASSUME k = [x \\in {1}, y \\in S |-> 1]\n"
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("POW(INTEGER*BOOL*INTEGER)", t.getConstantType("k")
- .toString());
+ assertEquals("POW(INTEGER*BOOL*INTEGER)", t.getConstantType("k"));
assertEquals("INTEGER", t.getConstantType("k2"));
assertEquals("INTEGER", t.getConstantType("k3"));
assertEquals("POW(BOOL)", t.getConstantType("S"));
}
@Test
- public void testFunctionCall4() throws FrontEndException, TLA2BException {
+ public void testFunctionCall4() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k[(TRUE /\\ TRUE)] = 2 \n"
@@ -229,8 +224,8 @@ public class FunctionTest {
}
@Test(expected = TypeErrorException.class)
- public void testFunctionCallException() throws FrontEndException,
- TLA2BException {
+ public void testFunctionCallException() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3, S \n"
+ "ASSUME k = [x \\in {1} |-> 1]\n"
@@ -243,28 +238,26 @@ public class FunctionTest {
* Domain
*/
@Test
- public void testDomain() throws FrontEndException, TLA2BException {
+ public void testDomain() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "ASSUME k = [x \\in {1}, y \\in BOOLEAN |-> 1]\n"
+ "ASSUME k2 = DOMAIN k \n"
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("POW(INTEGER*BOOL*INTEGER)", t.getConstantType("k")
- .toString());
+ assertEquals("POW(INTEGER*BOOL*INTEGER)", t.getConstantType("k"));
assertEquals("POW(INTEGER*BOOL)", t.getConstantType("k2"));
}
@Test
- public void testDomain2() throws FrontEndException, TLA2BException {
+ public void testDomain2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "ASSUME k = [x \\in {1}, y \\in BOOLEAN |-> 1]\n"
+ "ASSUME k2 = DOMAIN k \n"
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("POW(INTEGER*BOOL*INTEGER)", t.getConstantType("k")
- .toString());
+ assertEquals("POW(INTEGER*BOOL*INTEGER)", t.getConstantType("k"));
assertEquals("POW(INTEGER*BOOL)", t.getConstantType("k2"));
}
@@ -272,7 +265,7 @@ public class FunctionTest {
* Set of Function
*/
@Test
- public void testSetOfFunction() throws FrontEndException, TLA2BException {
+ public void testSetOfFunction() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k = [BOOLEAN -> {1}] \n"
@@ -282,7 +275,7 @@ public class FunctionTest {
}
@Test
- public void testSetOfFunction2() throws FrontEndException, TLA2BException {
+ public void testSetOfFunction2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS S, S2 \n"
+ "ASSUME [x \\in BOOLEAN |-> 1] \\in [S -> S2] \n"
@@ -293,8 +286,8 @@ public class FunctionTest {
}
@Test(expected = TypeErrorException.class)
- public void testSetOfFunctionException() throws FrontEndException,
- TLA2BException {
+ public void testSetOfFunctionException() throws
+ TLA2BException {
/*
* A set of tuple is not a function in TLA+
*/
@@ -309,7 +302,7 @@ public class FunctionTest {
* Except
*/
@Test
- public void testFunctionExcept() throws FrontEndException, TLA2BException {
+ public void testFunctionExcept() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "ASSUME k = [k2 EXCEPT ![TRUE] = 0] \n"
@@ -322,32 +315,28 @@ public class FunctionTest {
}
@Test
- public void testFunctionExcept2() throws FrontEndException, TLA2BException {
+ public void testFunctionExcept2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3 \n"
+ "ASSUME k = [k2 EXCEPT ![TRUE,1] = k3] /\\ k3 = 1 \n"
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("POW(BOOL*INTEGER*INTEGER)", t.getConstantType("k")
- .toString());
- assertEquals("POW(BOOL*INTEGER*INTEGER)", t.getConstantType("k2")
- .toString());
+ assertEquals("POW(BOOL*INTEGER*INTEGER)", t.getConstantType("k"));
+ assertEquals("POW(BOOL*INTEGER*INTEGER)", t.getConstantType("k2"));
assertEquals("INTEGER", t.getConstantType("k3"));
}
@Test
- public void testFunctionExcept3() throws FrontEndException, TLA2BException {
+ public void testFunctionExcept3() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3, k4, k5 \n"
+ "ASSUME k = [k2 EXCEPT ![k3,k4] = k5]\n"
+ "ASSUME k2 = [x \\in {1}, y \\in BOOLEAN |-> 1]"
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("POW(INTEGER*BOOL*INTEGER)", t.getConstantType("k")
- .toString());
- assertEquals("POW(INTEGER*BOOL*INTEGER)", t.getConstantType("k2")
- .toString());
+ assertEquals("POW(INTEGER*BOOL*INTEGER)", t.getConstantType("k"));
+ assertEquals("POW(INTEGER*BOOL*INTEGER)", t.getConstantType("k2"));
assertEquals("INTEGER", t.getConstantType("k3"));
assertEquals("BOOL", t.getConstantType("k4"));
assertEquals("INTEGER", t.getConstantType("k5"));
@@ -355,37 +344,35 @@ public class FunctionTest {
}
@Test
- public void testFunctionExcept4() throws FrontEndException, TLA2BException {
+ public void testFunctionExcept4() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3, k4, k5 \n"
+ "ASSUME k = [k2 EXCEPT ![k3,k4] = k5]\n"
+ "ASSUME k = [x \\in {1}, y \\in BOOLEAN |-> 1]"
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("POW(INTEGER*BOOL*INTEGER)", t.getConstantType("k")
- .toString());
- assertEquals("POW(INTEGER*BOOL*INTEGER)", t.getConstantType("k2")
- .toString());
+ assertEquals("POW(INTEGER*BOOL*INTEGER)", t.getConstantType("k"));
+ assertEquals("POW(INTEGER*BOOL*INTEGER)", t.getConstantType("k2"));
assertEquals("INTEGER", t.getConstantType("k3"));
assertEquals("BOOL", t.getConstantType("k4"));
assertEquals("INTEGER", t.getConstantType("k5"));
}
@Test
- public void testFunctionExcept6() throws FrontEndException, TLA2BException {
+ public void testFunctionExcept6() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3, k4\n"
+ "ASSUME k = [k2 EXCEPT ![k3] = k4, ![1] = TRUE ]\n"
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("POW(INTEGER*BOOL)", t.getConstantType("k").toString());
- assertEquals("POW(INTEGER*BOOL)", t.getConstantType("k2").toString());
+ assertEquals("POW(INTEGER*BOOL)", t.getConstantType("k"));
+ assertEquals("POW(INTEGER*BOOL)", t.getConstantType("k2"));
assertEquals("INTEGER", t.getConstantType("k3"));
assertEquals("BOOL", t.getConstantType("k4"));
}
@Test
- public void testFunctionExcept5() throws FrontEndException, TLA2BException {
+ public void testFunctionExcept5() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "ASSUME k = [k2 EXCEPT ![1][1] = 2]\n"
@@ -398,7 +385,7 @@ public class FunctionTest {
}
@Test
- public void testFunctionExcept7() throws FrontEndException, TLA2BException {
+ public void testFunctionExcept7() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "ASSUME k = [k2 EXCEPT ![<<1,2>>] = 2]\n"
@@ -412,7 +399,7 @@ public class FunctionTest {
*/
@Test
- public void testAt2() throws FrontEndException, TLA2BException {
+ public void testAt2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2,k3 \n"
+ "ASSUME k = [k2 EXCEPT ![1] = TRUE, ![2] = @=k3] \n"
@@ -423,7 +410,7 @@ public class FunctionTest {
}
@Test(expected = TypeErrorException.class)
- public void testAtException() throws FrontEndException, TLA2BException {
+ public void testAtException() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "ASSUME k = [k2 EXCEPT ![1] = TRUE, ![2] = @=1] \n"
diff --git a/src/test/java/de/tla2b/typechecking/InstanceTest.java b/src/test/java/de/tla2b/typechecking/InstanceTest.java
index b7f851f0f8f91b6a9c5567ddb4f25010d2819bb5..0c6ab195279eb77e8958d30baea33310d9301ff3 100644
--- a/src/test/java/de/tla2b/typechecking/InstanceTest.java
+++ b/src/test/java/de/tla2b/typechecking/InstanceTest.java
@@ -8,7 +8,7 @@ import de.tla2b.util.TestUtil;
public class InstanceTest {
- private static String path = "src/test/resources/typechecking/modules/";
+ private static final String path = "src/test/resources/typechecking/modules/";
@Test
public void TestNamedInstanceCounter() throws Exception {
diff --git a/src/test/java/de/tla2b/typechecking/LogicOperatorsTest.java b/src/test/java/de/tla2b/typechecking/LogicOperatorsTest.java
index 1a0910f6cfa75633bf896d4067e98e3815b768fd..f13ea70fce1c897f84682d84e9cee211214ae4a6 100644
--- a/src/test/java/de/tla2b/typechecking/LogicOperatorsTest.java
+++ b/src/test/java/de/tla2b/typechecking/LogicOperatorsTest.java
@@ -17,25 +17,25 @@ public class LogicOperatorsTest {
* equality and disequality: =, #,
*/
@Test
- public void testEquality() throws FrontEndException, TLA2BException {
+ public void testEquality() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2\n"
+ "ASSUME k = (k2 = 1)\n"
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("BOOL", t.getConstantType("k").toString());
- assertEquals("INTEGER", t.getConstantType("k2").toString());
+ assertEquals("BOOL", t.getConstantType("k"));
+ assertEquals("INTEGER", t.getConstantType("k2"));
}
@Test (expected = TypeErrorException.class)
- public void testEqualityError() throws FrontEndException, TLA2BException {
+ public void testEqualityError() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "ASSUME 1 = TRUE\n"
+ "=================================";
TestUtil.typeCheckString(module);
}
@Test (expected = TypeErrorException.class)
- public void testEqualityError2() throws FrontEndException, TLA2BException {
+ public void testEqualityError2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "ASSUME 1 = (1=1)\n"
+ "=================================";
@@ -48,20 +48,20 @@ public class LogicOperatorsTest {
* Logic Operators: \neg, \lnot, \land, \cl, \lor, \dl, \equiv, =>
*/
@Test
- public void testLogicOperators() throws FrontEndException, TLA2BException {
+ public void testLogicOperators() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3\n"
+ "ASSUME k = (k2 \\land k3) \n"
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("BOOL", t.getConstantType("k").toString());
- assertEquals("BOOL", t.getConstantType("k2").toString());
- assertEquals("BOOL", t.getConstantType("k3").toString());
+ assertEquals("BOOL", t.getConstantType("k"));
+ assertEquals("BOOL", t.getConstantType("k2"));
+ assertEquals("BOOL", t.getConstantType("k3"));
}
@Test (expected = TypeErrorException.class)
- public void testLogicOperatorsError() throws FrontEndException, TLA2BException {
+ public void testLogicOperatorsError() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3\n"
+ "ASSUME 1 = (k2 \\land k3) \n"
@@ -75,19 +75,19 @@ public class LogicOperatorsTest {
@Test
- public void testQuantification() throws FrontEndException, TLA2BException {
+ public void testQuantification() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, S\n"
+ "ASSUME k = (\\A x \\in S : x = k2) /\\ k2 = 1 \n"
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("BOOL", t.getConstantType("k").toString());
- assertEquals("INTEGER", t.getConstantType("k2").toString());
- assertEquals("POW(INTEGER)", t.getConstantType("S").toString());
+ assertEquals("BOOL", t.getConstantType("k"));
+ assertEquals("INTEGER", t.getConstantType("k2"));
+ assertEquals("POW(INTEGER)", t.getConstantType("S"));
}
@Test(expected = TypeErrorException.class)
- public void testQuantificationException() throws FrontEndException, TLA2BException {
+ public void testQuantificationException() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "ASSUME \\A <<x,y>> \\in {1} : TRUE \n"
+ "=================================";
diff --git a/src/test/java/de/tla2b/typechecking/MiscellaneousConstructsTest.java b/src/test/java/de/tla2b/typechecking/MiscellaneousConstructsTest.java
index 4a66162a0787e8729c50409e9638c1c4e60f8d8f..7753c4cc967f7c6b22af288a44125e33eadb7740 100644
--- a/src/test/java/de/tla2b/typechecking/MiscellaneousConstructsTest.java
+++ b/src/test/java/de/tla2b/typechecking/MiscellaneousConstructsTest.java
@@ -16,7 +16,7 @@ public class MiscellaneousConstructsTest {
* IF THEN ELSE
*/
@Test
- public void testIfThenElse() throws FrontEndException, TLA2BException {
+ public void testIfThenElse() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3, k4 \n"
+ "ASSUME k = (IF k2 THEN k3 ELSE k4) /\\ k4 = 1 \n"
@@ -33,7 +33,7 @@ public class MiscellaneousConstructsTest {
* IF THEN ELSE
*/
@Test
- public void testCase() throws FrontEndException, TLA2BException {
+ public void testCase() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3, e1, e2 \n"
+ "ASSUME k = (CASE k2 -> e1 [] k3 -> e2) /\\ e2 = 1 \n"
@@ -47,7 +47,7 @@ public class MiscellaneousConstructsTest {
}
@Test
- public void testCase2() throws FrontEndException, TLA2BException {
+ public void testCase2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3, e1, e2, e3 \n"
+ "ASSUME k = (CASE k2 -> e1 [] k3 -> e2 [] OTHER -> e3) /\\ e2 = 1 \n"
@@ -65,7 +65,7 @@ public class MiscellaneousConstructsTest {
* LET d == exp IN e
*/
@Test
- public void testLetIn() throws FrontEndException, TLA2BException {
+ public void testLetIn() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3 \n"
+ "ASSUME k = (LET d == k2 IN d = k3) /\\ k2 = 1 \n"
@@ -77,7 +77,7 @@ public class MiscellaneousConstructsTest {
}
@Test
- public void testLetIn2() throws FrontEndException, TLA2BException {
+ public void testLetIn2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3 \n"
+ "ASSUME k = (LET d == k2 d2 == k3 IN d = d2) /\\ k2 = 1 \n"
@@ -89,7 +89,7 @@ public class MiscellaneousConstructsTest {
}
@Test
- public void testLetIn3() throws FrontEndException, TLA2BException {
+ public void testLetIn3() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3, k4 \n"
+ "ASSUME k = (LET d(a,b) == a=k2/\\b=k3 IN d(1,k4)) /\\ k4 = TRUE \n"
@@ -102,7 +102,7 @@ public class MiscellaneousConstructsTest {
}
@Test
- public void testBoundedChoose() throws FrontEndException, TLA2BException {
+ public void testBoundedChoose() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k = CHOOSE x \\in {1}: TRUE \n"
@@ -112,7 +112,7 @@ public class MiscellaneousConstructsTest {
}
@Test
- public void testUnboundedChoose() throws FrontEndException, TLA2BException {
+ public void testUnboundedChoose() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k = CHOOSE x : x = 1 \n"
@@ -122,7 +122,7 @@ public class MiscellaneousConstructsTest {
}
@Test
- public void testUnboundedChooseTuple() throws FrontEndException, TLA2BException {
+ public void testUnboundedChooseTuple() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k = CHOOSE <<a,b>> : <<a,b>> = <<1,TRUE>> \n"
@@ -132,7 +132,7 @@ public class MiscellaneousConstructsTest {
}
@Test
- public void testBoundedChooseTuple() throws FrontEndException, TLA2BException {
+ public void testBoundedChooseTuple() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k = CHOOSE <<a,b>> \\in {<<1,TRUE>>}: TRUE \n"
diff --git a/src/test/java/de/tla2b/typechecking/SetTest.java b/src/test/java/de/tla2b/typechecking/SetTest.java
index a59047473a3fad2d6ef11df3fc185dfae920739a..2180c8ae43a43dffca8a6b7eada52511047902f9 100644
--- a/src/test/java/de/tla2b/typechecking/SetTest.java
+++ b/src/test/java/de/tla2b/typechecking/SetTest.java
@@ -17,7 +17,7 @@ public class SetTest {
*/
@Test
- public void testSetEnumeration() throws FrontEndException, TLA2BException {
+ public void testSetEnumeration() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3\n"
+ "ASSUME k = {k2, k3} /\\ k3 = 1\n"
@@ -31,7 +31,7 @@ public class SetTest {
}
@Test
- public void testSetEnumeration2() throws FrontEndException, TLA2BException {
+ public void testSetEnumeration2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3\n"
+ "ASSUME k = {k2, k3} /\\ k = {1}\n"
@@ -44,7 +44,7 @@ public class SetTest {
}
@Test
- public void testSetEnumeration3() throws FrontEndException, TLA2BException {
+ public void testSetEnumeration3() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3\n"
+ "ASSUME k = {k2,{k3}} /\\ k3 = 1\n"
@@ -57,7 +57,7 @@ public class SetTest {
}
@Test
- public void testSetEnumeration4() throws FrontEndException, TLA2BException {
+ public void testSetEnumeration4() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2\n"
+ "ASSUME k = {{1},{k2}}\n"
@@ -69,8 +69,8 @@ public class SetTest {
}
@Test(expected = TypeErrorException.class)
- public void testSetEnumerationException() throws FrontEndException,
- TLA2BException {
+ public void testSetEnumerationException() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2\n"
+ "ASSUME k = {1, TRUE}\n"
@@ -80,8 +80,8 @@ public class SetTest {
}
@Test(expected = TypeErrorException.class)
- public void testSetEnumerationException2() throws FrontEndException,
- TLA2BException {
+ public void testSetEnumerationException2() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2\n"
+ "ASSUME 1 = {1, 2}\n"
@@ -93,7 +93,7 @@ public class SetTest {
* Element of: \in, \notin
*/
@Test
- public void testElementOfSet() throws FrontEndException, TLA2BException {
+ public void testElementOfSet() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2\n"
+ "ASSUME k \\in {k2} /\\ k2 = 1 \n"
@@ -104,7 +104,7 @@ public class SetTest {
}
@Test
- public void testElementOfSet2() throws FrontEndException, TLA2BException {
+ public void testElementOfSet2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2\n"
+ "ASSUME k \\in {k2} /\\ k = 1 \n"
@@ -115,7 +115,7 @@ public class SetTest {
}
@Test
- public void testElementOfSet3() throws FrontEndException, TLA2BException {
+ public void testElementOfSet3() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k \\in {<<TRUE>>}\n"
@@ -126,8 +126,8 @@ public class SetTest {
}
@Test(expected = TypeErrorException.class)
- public void testElementOfSetError() throws FrontEndException,
- TLA2BException {
+ public void testElementOfSetError() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "ASSUME 1 = (1 \\in {1}) \n"
+ "=================================";
@@ -135,8 +135,8 @@ public class SetTest {
}
@Test(expected = TypeErrorException.class)
- public void testElementOfSetError2() throws FrontEndException,
- TLA2BException {
+ public void testElementOfSetError2() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "ASSUME 1 \\in 1 \n" + "=================================";
TestUtil.typeCheckString(module);
@@ -146,7 +146,7 @@ public class SetTest {
* set operators like difference, union, intersection
*/
@Test
- public void testSetOperators() throws FrontEndException, TLA2BException {
+ public void testSetOperators() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3\n"
+ "ASSUME k = (k2 \\cup k3) /\\ k3 = {1} \n"
@@ -158,7 +158,7 @@ public class SetTest {
}
@Test
- public void testSetOperators2() throws FrontEndException, TLA2BException {
+ public void testSetOperators2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2\n"
+ "ASSUME k = (k \\cup k2) /\\ k2 = {1} \n"
@@ -169,8 +169,8 @@ public class SetTest {
}
@Test(expected = TypeErrorException.class)
- public void testSetOperatorsException() throws FrontEndException,
- TLA2BException {
+ public void testSetOperatorsException() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2\n"
+ "ASSUME 1 = k \\cup k2 \n"
@@ -179,8 +179,8 @@ public class SetTest {
}
@Test(expected = TypeErrorException.class)
- public void testSetOperatorsException2() throws FrontEndException,
- TLA2BException {
+ public void testSetOperatorsException2() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k\n"
+ "ASSUME k = {1} \\cup {TRUE} \n"
@@ -192,7 +192,7 @@ public class SetTest {
* set constructor: {x \in S : p}.
*/
@Test
- public void testSubsetOf() throws FrontEndException, TLA2BException {
+ public void testSubsetOf() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, S\n"
+ "ASSUME k = {x \\in S : x = 1} \n"
@@ -203,7 +203,7 @@ public class SetTest {
}
@Test
- public void testSubsetOf2() throws FrontEndException, TLA2BException {
+ public void testSubsetOf2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2\n"
+ "ASSUME k = {x \\in {TRUE} : x = k2} \n"
@@ -214,7 +214,7 @@ public class SetTest {
}
@Test
- public void testSubsetOf3() throws FrontEndException, TLA2BException {
+ public void testSubsetOf3() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, S, k2\n"
+ "ASSUME k = {x \\in S : x = k2} /\\ k2 = TRUE \n"
@@ -226,7 +226,7 @@ public class SetTest {
}
@Test
- public void testSubsetOf4() throws FrontEndException, TLA2BException {
+ public void testSubsetOf4() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, S\n"
+ "ASSUME k = {x \\in S : TRUE} /\\ k = {TRUE} \n"
@@ -237,8 +237,8 @@ public class SetTest {
}
@Test (expected = TypeErrorException.class)
- public void testSubsetOfException() throws FrontEndException,
- TLA2BException {
+ public void testSubsetOfException() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k\n"
+ "ASSUME k = {<<x,y>> \\in {TRUE} : TRUE} \n"
@@ -247,8 +247,8 @@ public class SetTest {
}
@Test(expected = TypeErrorException.class)
- public void testSubsetOfException2() throws FrontEndException,
- TLA2BException {
+ public void testSubsetOfException2() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k\n"
+ "ASSUME k = {x \\in 1 : TRUE} \n"
@@ -257,8 +257,8 @@ public class SetTest {
}
@Test (expected = TypeErrorException.class)
- public void testSubsetOfException3() throws FrontEndException,
- TLA2BException {
+ public void testSubsetOfException3() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k\n"
+ "ASSUME k = {x \\in {} : 1 = 1} \n"
@@ -267,8 +267,8 @@ public class SetTest {
}
@Test
- public void testSubsetOfTuple() throws FrontEndException,
- TLA2BException {
+ public void testSubsetOfTuple() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k\n"
+ "ASSUME k = {<<x,y>> \\in {1} \\times {TRUE} : TRUE} \n"
@@ -278,8 +278,8 @@ public class SetTest {
}
@Test
- public void testSubsetOfTuple2() throws FrontEndException,
- TLA2BException {
+ public void testSubsetOfTuple2() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, S, S2\n"
+ "ASSUME k = {<<x,y>> \\in S \\times S2 : x = 1 /\\ y = TRUE} \n"
@@ -291,8 +291,8 @@ public class SetTest {
}
@Test
- public void testSubsetOfTuple3() throws FrontEndException,
- TLA2BException {
+ public void testSubsetOfTuple3() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, S\n"
+ "ASSUME k = {<<x,y>> \\in S : x = 1 /\\ y = TRUE} \n"
@@ -306,7 +306,7 @@ public class SetTest {
* set constructor: {e : x \in S}
*/
@Test
- public void testSetOfAll() throws FrontEndException, TLA2BException {
+ public void testSetOfAll() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, S, k2\n"
+ "ASSUME k = {x = k2 : x \\in S} /\\ k2 = 1 \n"
@@ -318,7 +318,7 @@ public class SetTest {
}
@Test
- public void testSetOfAll2() throws FrontEndException, TLA2BException {
+ public void testSetOfAll2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, S\n"
+ "ASSUME k = {{x} : x \\in S} /\\ S = {1} \n"
@@ -329,7 +329,7 @@ public class SetTest {
}
@Test
- public void testSetOfAll3() throws FrontEndException, TLA2BException {
+ public void testSetOfAll3() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, S, k2\n"
+ "ASSUME k = { x = y /\\ y = k2 : x,y \\in S} /\\ k2 = 1 \n"
@@ -341,7 +341,7 @@ public class SetTest {
}
@Test
- public void testSetOfAll4() throws FrontEndException, TLA2BException {
+ public void testSetOfAll4() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, S, S2, k2, k3\n"
+ "ASSUME k = { x = k2 /\\ y /\\ z = k3 : x \\in S, y,z \\in S2 } /\\ k2 = TRUE \n"
@@ -354,8 +354,8 @@ public class SetTest {
}
@Test(expected = TypeErrorException.class)
- public void testSetOfAllException() throws FrontEndException,
- TLA2BException {
+ public void testSetOfAllException() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, S\n"
+ "ASSUME 1 = {x : x \\in S} \n"
@@ -364,8 +364,8 @@ public class SetTest {
}
@Test(expected = TypeErrorException.class)
- public void testSetOfAllException2() throws FrontEndException,
- TLA2BException {
+ public void testSetOfAllException2() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, S\n"
+ "ASSUME k = {x : x \\in 1} \n"
@@ -374,8 +374,8 @@ public class SetTest {
}
@Test(expected = TypeErrorException.class)
- public void testSetOfAllException3() throws FrontEndException,
- TLA2BException {
+ public void testSetOfAllException3() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, S\n"
+ "ASSUME k = {x : <<x,y>> \\in S} \n"
@@ -387,7 +387,7 @@ public class SetTest {
* SUBSET: conforms POW in B
*/
@Test
- public void testSubset() throws FrontEndException, TLA2BException {
+ public void testSubset() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "ASSUME k = SUBSET k2 /\\ k2 = 1 \n"
@@ -398,7 +398,7 @@ public class SetTest {
}
@Test
- public void testSubset2() throws FrontEndException, TLA2BException {
+ public void testSubset2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "ASSUME k = SUBSET k2 /\\ k = {1} \n"
@@ -409,7 +409,7 @@ public class SetTest {
}
@Test(expected = TypeErrorException.class)
- public void testSubsetException() throws FrontEndException, TLA2BException {
+ public void testSubsetException() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME 1 = SUBSET k \n"
@@ -421,7 +421,7 @@ public class SetTest {
* UNION
*/
@Test
- public void testUnion() throws FrontEndException, TLA2BException {
+ public void testUnion() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "ASSUME k = UNION k2 /\\ k = {1} \n"
@@ -432,7 +432,7 @@ public class SetTest {
}
@Test
- public void testUnion2() throws FrontEndException, TLA2BException {
+ public void testUnion2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "ASSUME k = UNION k2 /\\ k2 = {{1},{2}} \n"
@@ -443,7 +443,7 @@ public class SetTest {
}
@Test(expected = TypeErrorException.class)
- public void testUnionException() throws FrontEndException, TLA2BException {
+ public void testUnionException() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "ASSUME k = UNION k2 /\\ k = 1 \n"
@@ -452,7 +452,7 @@ public class SetTest {
}
@Test(expected = TypeErrorException.class)
- public void testUnionException2() throws FrontEndException, TLA2BException {
+ public void testUnionException2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "ASSUME k = UNION k2 /\\ k2 = {1,2} \n"
@@ -464,7 +464,7 @@ public class SetTest {
* Subseteq: subset or equal
*/
@Test
- public void testSubseteq() throws FrontEndException, TLA2BException {
+ public void testSubseteq() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3 \n"
+ "ASSUME k = (k2 \\subseteq k3) /\\ k3 = {1} \n"
@@ -476,8 +476,8 @@ public class SetTest {
}
@Test(expected = TypeErrorException.class)
- public void testSubseteqException() throws FrontEndException,
- TLA2BException {
+ public void testSubseteqException() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "ASSUME k = (k2 \\subseteq 1) \n"
@@ -486,8 +486,8 @@ public class SetTest {
}
@Test(expected = TypeErrorException.class)
- public void testSubseteqException2() throws FrontEndException,
- TLA2BException {
+ public void testSubseteqException2() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "ASSUME 1 = (k \\subseteq k2) \n"
diff --git a/src/test/java/de/tla2b/typechecking/StringTest.java b/src/test/java/de/tla2b/typechecking/StringTest.java
index 4e25488b91a5a8d5222718e21e474e0a4ab18fc2..f3cb27dc7d4a2da2c812a35083f8aca96655b114 100644
--- a/src/test/java/de/tla2b/typechecking/StringTest.java
+++ b/src/test/java/de/tla2b/typechecking/StringTest.java
@@ -18,17 +18,17 @@ public class StringTest {
*/
@Test
- public void testAString() throws FrontEndException, TLA2BException {
+ public void testAString() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k = \"abc\" \n"
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("STRING", t.getConstantType("k").toString());
+ assertEquals("STRING", t.getConstantType("k"));
}
@Test (expected = TypeErrorException.class)
- public void testAStringException() throws FrontEndException, TLA2BException {
+ public void testAStringException() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "ASSUME 1 = \"abc\" \n"
+ "=================================";
@@ -36,7 +36,7 @@ public class StringTest {
}
@Test
- public void testStringAsSequence() throws FrontEndException, TLA2BException {
+ public void testStringAsSequence() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "ASSUME \"a\" \\o \"bc\" = \"abc\" \n"
@@ -45,7 +45,7 @@ public class StringTest {
}
@Test
- public void testStringAsSequence2() throws FrontEndException, TLA2BException {
+ public void testStringAsSequence2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "ASSUME SubSeq(\"abc\",1,1) = \"a\" \n"
@@ -54,7 +54,7 @@ public class StringTest {
}
@Test
- public void testStringAsSequence3() throws FrontEndException, TLA2BException {
+ public void testStringAsSequence3() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "ASSUME Len(\"abc\") = 3 \n"
@@ -67,17 +67,17 @@ public class StringTest {
* STRING
*/
@Test
- public void testString() throws FrontEndException, TLA2BException {
+ public void testString() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k = STRING \n"
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("POW(STRING)", t.getConstantType("k").toString());
+ assertEquals("POW(STRING)", t.getConstantType("k"));
}
@Test (expected = TypeErrorException.class)
- public void testStringException() throws FrontEndException, TLA2BException {
+ public void testStringException() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "ASSUME 1 = STRING \n"
+ "=================================";
diff --git a/src/test/java/de/tla2b/typechecking/StructTest.java b/src/test/java/de/tla2b/typechecking/StructTest.java
index ab8b8af6bfd6d2cced3cb462805c5e5006fb3ec0..588094af981fb59dc5caefce33f647e01ba976c1 100644
--- a/src/test/java/de/tla2b/typechecking/StructTest.java
+++ b/src/test/java/de/tla2b/typechecking/StructTest.java
@@ -20,7 +20,7 @@ public class StructTest {
* Set of Records: [L1 : e1, L2 : e2]
*/
@Test
- public void testStruct() throws FrontEndException, TLA2BException {
+ public void testStruct() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k = [a : {1}, b : BOOLEAN] \n"
@@ -30,7 +30,7 @@ public class StructTest {
}
@Test
- public void testStruct2() throws FrontEndException, TLA2BException {
+ public void testStruct2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3 \n"
@@ -43,7 +43,7 @@ public class StructTest {
}
@Test
- public void testStruct3() throws FrontEndException, TLA2BException {
+ public void testStruct3() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "ASSUME [a : {1}, b : BOOLEAN] = [a : k, b : k2] \n"
@@ -54,7 +54,7 @@ public class StructTest {
}
@Test(expected = TypeErrorException.class)
- public void testStructException() throws FrontEndException, TLA2BException {
+ public void testStructException() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME 1 = [a : 1, b : TRUE] \n"
@@ -63,7 +63,7 @@ public class StructTest {
}
@Test(expected = TypeErrorException.class)
- public void testStructException2() throws FrontEndException, TLA2BException {
+ public void testStructException2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "ASSUME [a : {1}, b : BOOLEAN] = [a : BOOLEAN, b : BOOLEAN] \n"
+ "=================================";
@@ -71,7 +71,7 @@ public class StructTest {
}
@Test(expected = TypeErrorException.class)
- public void testStructException3() throws FrontEndException, TLA2BException {
+ public void testStructException3() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "ASSUME [aa : {1}, b : BOOLEAN] = [a : {1}, b : BOOLEAN] \n"
@@ -85,7 +85,7 @@ public class StructTest {
*/
@Test
- public void testRecord() throws FrontEndException, TLA2BException {
+ public void testRecord() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k = [a |-> 1, b |-> TRUE] \n"
@@ -96,7 +96,7 @@ public class StructTest {
}
@Test
- public void testRecord2() throws FrontEndException, TLA2BException {
+ public void testRecord2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3 \n"
+ "ASSUME k = [a |-> k2, b |-> k3] /\\ k2 = 1 /\\ k3 = TRUE \n"
@@ -106,7 +106,7 @@ public class StructTest {
}
@Test(expected = TypeErrorException.class)
- public void testRecordException() throws FrontEndException, TLA2BException {
+ public void testRecordException() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "ASSUME 1 = [b |-> 1, a |-> TRUE] \n"
+ "=================================";
@@ -114,7 +114,7 @@ public class StructTest {
}
@Test
- public void testRecord3() throws FrontEndException, TLA2BException {
+ public void testRecord3() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "ASSUME [a |-> k, b |-> k2] \\in [a: {1}, b: BOOLEAN] \n"
@@ -129,7 +129,7 @@ public class StructTest {
*/
@Test
- public void testRecordSelect() throws FrontEndException, TLA2BException {
+ public void testRecordSelect() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "ASSUME k = [a |-> 1, b |-> TRUE] /\\ k2 = k.a \n"
@@ -140,7 +140,7 @@ public class StructTest {
}
@Test
- public void testRecordSelect2() throws FrontEndException, TLA2BException {
+ public void testRecordSelect2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "ASSUME k2 = k.a /\\ k = [a |-> 1, b |-> TRUE] \n"
@@ -151,7 +151,7 @@ public class StructTest {
}
@Test
- public void testRecordSelect3() throws FrontEndException, TLA2BException {
+ public void testRecordSelect3() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3 \n"
+ "ASSUME k = [a |-> k2, b |-> k3] /\\ k.a = 1 /\\ k.b = TRUE \n"
@@ -164,7 +164,7 @@ public class StructTest {
}
@Test
- public void testRecordSelect4() throws FrontEndException, TLA2BException {
+ public void testRecordSelect4() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3 \n"
+ "ASSUME k \\in [a : k2, b : k3] /\\ k.a = 1 /\\ k.b = TRUE \n"
@@ -176,8 +176,8 @@ public class StructTest {
}
@Test
- public void testRecordSelectException3() throws FrontEndException,
- TLA2BException {
+ public void testRecordSelectException3() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k = [a |-> 1] /\\ TRUE = k.b \n"
@@ -186,7 +186,7 @@ public class StructTest {
}
@Test
- public void testRecordSelect5() throws FrontEndException, TLA2BException {
+ public void testRecordSelect5() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME 1 = k.a /\\ TRUE = k.b /\\ k = [a |-> 1] \n"
@@ -196,8 +196,8 @@ public class StructTest {
}
@Test(expected = TypeErrorException.class)
- public void testRecordSelectException() throws FrontEndException,
- TLA2BException {
+ public void testRecordSelectException() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME TRUE = k.a /\\ k = [a |-> 1] \n"
@@ -206,8 +206,8 @@ public class StructTest {
}
@Test(expected = TypeErrorException.class)
- public void testRecordSelectException4() throws FrontEndException,
- TLA2BException {
+ public void testRecordSelectException4() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
@@ -221,7 +221,7 @@ public class StructTest {
*/
@Test
- public void testRecordExcept() throws FrontEndException, TLA2BException {
+ public void testRecordExcept() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3, k4 \n"
+ "ASSUME k = [a|-> k2, b|-> k3] /\\ k4 = [k EXCEPT !.a = 1, !.b = TRUE]\n"
@@ -234,7 +234,7 @@ public class StructTest {
}
@Test
- public void testRecordExcept2() throws FrontEndException, TLA2BException {
+ public void testRecordExcept2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "ASSUME k.a = 1/\\ k2 = [k EXCEPT !.a = 1, !.b = TRUE] /\\ k2 = [a|->2, b |-> FALSE]\n"
@@ -249,7 +249,7 @@ public class StructTest {
*/
@Test
- public void testRecordExceptAt() throws FrontEndException, TLA2BException {
+ public void testRecordExceptAt() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3 \n"
+ "ASSUME k = [a|-> TRUE] /\\ k2 = [k EXCEPT !.a = @ = k3]\n"
@@ -261,8 +261,8 @@ public class StructTest {
}
@Test(expected = TypeErrorException.class)
- public void testRecordExceptAtException() throws FrontEndException,
- TLA2BException {
+ public void testRecordExceptAtException() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3 \n"
+ "ASSUME k = [a|-> TRUE] /\\ k2 = [k EXCEPT !.a = @ = 1]\n"
@@ -271,8 +271,8 @@ public class StructTest {
}
@Test (expected = TypeErrorException.class)
- public void testRecord5() throws FrontEndException,
- TLA2BException {
+ public void testRecord5() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "ASSUME k = [k EXCEPT !.a = 1] /\\ k ={k2} \n"
diff --git a/src/test/java/de/tla2b/typechecking/TupleTest.java b/src/test/java/de/tla2b/typechecking/TupleTest.java
index 1317d15f0914dbbd41c64add817489aa294d2492..ea9facd1a03e95f8dbe8e7ca94a22033bd9ccb74 100644
--- a/src/test/java/de/tla2b/typechecking/TupleTest.java
+++ b/src/test/java/de/tla2b/typechecking/TupleTest.java
@@ -14,7 +14,7 @@ import de.tla2b.util.TestUtil;
public class TupleTest {
@Test
- public void testSimpleTuple() throws FrontEndException, TLA2BException {
+ public void testSimpleTuple() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
+ "CONSTANTS k \n"
@@ -22,12 +22,12 @@ public class TupleTest {
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("INTEGER*BOOL", t.getConstantType("k").toString());
+ assertEquals("INTEGER*BOOL", t.getConstantType("k"));
}
@Test
- public void testTupleFunctionCall() throws FrontEndException, TLA2BException {
+ public void testTupleFunctionCall() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
+ "CONSTANTS k \n"
@@ -35,11 +35,11 @@ public class TupleTest {
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("BOOL", t.getConstantType("k").toString());
+ assertEquals("BOOL", t.getConstantType("k"));
}
@Test
- public void testTupleFunctionCall2() throws FrontEndException, TLA2BException {
+ public void testTupleFunctionCall2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
+ "CONSTANTS k \n"
@@ -47,11 +47,11 @@ public class TupleTest {
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("STRING", t.getConstantType("k").toString());
+ assertEquals("STRING", t.getConstantType("k"));
}
@Test
- public void testTuple3Components() throws FrontEndException, TLA2BException {
+ public void testTuple3Components() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
+ "CONSTANTS k \n"
@@ -59,11 +59,11 @@ public class TupleTest {
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("INTEGER*BOOL*INTEGER", t.getConstantType("k").toString());
+ assertEquals("INTEGER*BOOL*INTEGER", t.getConstantType("k"));
}
@Test
- public void testTuple3Components2() throws FrontEndException, TLA2BException {
+ public void testTuple3Components2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
+ "CONSTANTS k \n"
@@ -71,23 +71,23 @@ public class TupleTest {
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("POW(INTEGER*INTEGER)", t.getConstantType("k").toString());
+ assertEquals("POW(INTEGER*INTEGER)", t.getConstantType("k"));
}
@Test
- public void testTupleComponentsOfTheSameType() throws FrontEndException,
- TLA2BException {
+ public void testTupleComponentsOfTheSameType() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
+ "CONSTANTS k \n"
+ "ASSUME k = <<1,1>> \n" + "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("POW(INTEGER*INTEGER)", t.getConstantType("k").toString());
+ assertEquals("POW(INTEGER*INTEGER)", t.getConstantType("k"));
}
@Test
- public void testTuple1() throws FrontEndException, TLA2BException {
+ public void testTuple1() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
+ "CONSTANTS k, k2 \n"
@@ -95,12 +95,12 @@ public class TupleTest {
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("INTEGER*BOOL", t.getConstantType("k").toString());
- assertEquals("BOOL", t.getConstantType("k2").toString());
+ assertEquals("INTEGER*BOOL", t.getConstantType("k"));
+ assertEquals("BOOL", t.getConstantType("k2"));
}
@Test
- public void testCartesianProduct() throws FrontEndException, TLA2BException {
+ public void testCartesianProduct() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
+ "CONSTANTS k \n"
@@ -108,23 +108,23 @@ public class TupleTest {
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("POW(INTEGER*BOOL)", t.getConstantType("k").toString());
+ assertEquals("POW(INTEGER*BOOL)", t.getConstantType("k"));
}
@Test
- public void testTupleSingleElement() throws FrontEndException,
- TLA2BException {
+ public void testTupleSingleElement() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k = <<TRUE>> \n"
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("POW(INTEGER*BOOL)", t.getConstantType("k").toString());
+ assertEquals("POW(INTEGER*BOOL)", t.getConstantType("k"));
}
@Test(expected = TypeErrorException.class)
- public void testTuple2Elements() throws FrontEndException, TLA2BException {
+ public void testTuple2Elements() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3 \n"
+ "ASSUME k = <<k2, k3>> /\\ k3 = TRUE \n"
@@ -134,21 +134,20 @@ public class TupleTest {
}
@Test
- public void testUnifyTuple3() throws FrontEndException, TLA2BException {
+ public void testUnifyTuple3() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2, k3 \n"
+ "ASSUME k = <<k2, <<k3>> >> /\\ k3 = TRUE /\\ k2 = 1\n"
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("INTEGER*POW(INTEGER*BOOL)", t.getConstantType("k")
- .toString());
- assertEquals("INTEGER", t.getConstantType("k2").toString());
- assertEquals("BOOL", t.getConstantType("k3").toString());
+ assertEquals("INTEGER*POW(INTEGER*BOOL)", t.getConstantType("k"));
+ assertEquals("INTEGER", t.getConstantType("k2"));
+ assertEquals("BOOL", t.getConstantType("k3"));
}
@Test(expected = TypeErrorException.class)
- public void testUnifyTuple4() throws FrontEndException, TLA2BException {
+ public void testUnifyTuple4() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k \\in <<TRUE>>\n"
@@ -161,31 +160,31 @@ public class TupleTest {
* Cartesian Product
*/
@Test
- public void testCartesianProduct2() throws FrontEndException,
- TLA2BException {
+ public void testCartesianProduct2() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k = BOOLEAN \\X {1} \n"
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("POW(BOOL*INTEGER)", t.getConstantType("k").toString());
+ assertEquals("POW(BOOL*INTEGER)", t.getConstantType("k"));
}
@Test
- public void testCartesianProduct3() throws FrontEndException,
- TLA2BException {
+ public void testCartesianProduct3() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k, k2 \n"
+ "ASSUME BOOLEAN \\X {1} = k \\X k2 \n"
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("POW(BOOL)", t.getConstantType("k").toString());
- assertEquals("POW(INTEGER)", t.getConstantType("k2").toString());
+ assertEquals("POW(BOOL)", t.getConstantType("k"));
+ assertEquals("POW(INTEGER)", t.getConstantType("k2"));
}
@Test(expected = TypeErrorException.class)
- public void testCartesianProductException() throws FrontEndException,
- TLA2BException {
+ public void testCartesianProductException() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k = BOOLEAN \\X 1 \n"
diff --git a/src/test/java/de/tla2b/typechecking/TupleVsSequenceTest.java b/src/test/java/de/tla2b/typechecking/TupleVsSequenceTest.java
index 02e16b398acbd42d35aa85c9286a32319c525e2a..aa416a420b0aecd0c36a9b12ee5ec2f4b71ac1fb 100644
--- a/src/test/java/de/tla2b/typechecking/TupleVsSequenceTest.java
+++ b/src/test/java/de/tla2b/typechecking/TupleVsSequenceTest.java
@@ -14,7 +14,7 @@ import de.tla2b.util.TestUtil;
public class TupleVsSequenceTest {
@Test
- public void testTupleVsSequence() throws FrontEndException, TLA2BException {
+ public void testTupleVsSequence() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k \n"
@@ -25,7 +25,7 @@ public class TupleVsSequenceTest {
}
@Test
- public void testTupleVsSequence2() throws FrontEndException, TLA2BException {
+ public void testTupleVsSequence2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k, k2 \n"
@@ -37,7 +37,7 @@ public class TupleVsSequenceTest {
}
@Test
- public void testTupleVsSequence3() throws FrontEndException, TLA2BException {
+ public void testTupleVsSequence3() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS a, b, c\n"
+ "ASSUME <<1,2,3,4>> = <<a,b,c>> \n"
@@ -49,7 +49,7 @@ public class TupleVsSequenceTest {
}
@Test
- public void testTupleVsSequence4() throws FrontEndException, TLA2BException {
+ public void testTupleVsSequence4() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS a, b, c\n"
+ "ASSUME a = 1 /\\ b = TRUE /\\ c = <<a,b>>\n"
@@ -61,7 +61,7 @@ public class TupleVsSequenceTest {
}
@Test
- public void testTupleVsSequence5() throws FrontEndException, TLA2BException {
+ public void testTupleVsSequence5() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k\n"
+ "ASSUME k = <<1,2>> /\\ k \\in {1} \\X {2} \n"
@@ -72,7 +72,7 @@ public class TupleVsSequenceTest {
@Test
- public void testTupleVsSequence6() throws FrontEndException, TLA2BException {
+ public void testTupleVsSequence6() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k\n"
+ "ASSUME {k} = {<<x, y>> \\in {1} \\X {2}: TRUE} \n"
@@ -82,7 +82,7 @@ public class TupleVsSequenceTest {
}
@Test (expected = TypeErrorException.class)
- public void testTupleVsSequence7() throws FrontEndException, TLA2BException {
+ public void testTupleVsSequence7() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "ASSUME 1 = <<1,TRUE>>[3] \n"
+ "=================================";
diff --git a/src/test/java/de/tla2b/typechecking/TypeConflictsTest.java b/src/test/java/de/tla2b/typechecking/TypeConflictsTest.java
index 6101e46cf12e5b820411c5da345403de720ad3b5..95c0aacce698f5798c4875a342d8708e1346b050 100644
--- a/src/test/java/de/tla2b/typechecking/TypeConflictsTest.java
+++ b/src/test/java/de/tla2b/typechecking/TypeConflictsTest.java
@@ -11,7 +11,7 @@ import de.tla2b.util.TestUtil;
public class TypeConflictsTest {
@Test(expected = TypeErrorException.class)
- public void testTypeConflict1() throws FrontEndException, TLA2BException {
+ public void testTypeConflict1() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k = {k} \n"
@@ -21,7 +21,7 @@ public class TypeConflictsTest {
}
@Test(expected = TypeErrorException.class)
- public void testTypeConflict2() throws FrontEndException, TLA2BException {
+ public void testTypeConflict2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME {k} = k \n"
@@ -31,7 +31,7 @@ public class TypeConflictsTest {
}
@Test(expected = TypeErrorException.class)
- public void testTypeConflict3() throws FrontEndException, TLA2BException {
+ public void testTypeConflict3() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME {{k}} = k \n"
@@ -41,7 +41,7 @@ public class TypeConflictsTest {
}
@Test(expected = TypeErrorException.class)
- public void testTypeConflict4() throws FrontEndException, TLA2BException {
+ public void testTypeConflict4() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k = [a |-> k] \n"
@@ -51,7 +51,7 @@ public class TypeConflictsTest {
}
@Test(expected = TypeErrorException.class)
- public void testTypeConflict5() throws FrontEndException, TLA2BException {
+ public void testTypeConflict5() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Integers \n"
+ "CONSTANTS k \n"
@@ -62,7 +62,7 @@ public class TypeConflictsTest {
}
@Test(expected = TypeErrorException.class)
- public void testTypeConflict6() throws FrontEndException, TLA2BException {
+ public void testTypeConflict6() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS a,b \n"
+ "ASSUME a = [x|->1] /\\ b = [y|->a, x|->1] /\\ a=b \n"
diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleFiniteSets.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleFiniteSets.java
index cd85ccc8e8500d21cea921301c740f93b27cd821..022bfd3f0f7874e7e440aace10cb20bad04a9b31 100644
--- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleFiniteSets.java
+++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleFiniteSets.java
@@ -17,7 +17,7 @@ public class TestModuleFiniteSets {
* IsFiniteSet
*/
@Test
- public void unifyIsFiniteSet() throws FrontEndException, TLA2BException {
+ public void unifyIsFiniteSet() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS FiniteSets \n"
+ "CONSTANTS k \n"
@@ -28,7 +28,7 @@ public class TestModuleFiniteSets {
}
@Test
- public void unifyIsFiniteSet2() throws FrontEndException, TLA2BException {
+ public void unifyIsFiniteSet2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS FiniteSets \n"
+ "CONSTANTS k, k2 \n"
@@ -41,7 +41,7 @@ public class TestModuleFiniteSets {
}
@Test
- public void unifyIsFiniteSet3() throws FrontEndException, TLA2BException {
+ public void unifyIsFiniteSet3() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS FiniteSets \n"
+ "CONSTANTS k \n"
@@ -52,7 +52,7 @@ public class TestModuleFiniteSets {
}
@Test(expected = TypeErrorException.class)
- public void unifyErrorIsFiniteSet() throws FrontEndException, TLA2BException {
+ public void unifyErrorIsFiniteSet() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS FiniteSets \n"
+ "ASSUME IsFiniteSet(1)\n"
@@ -61,7 +61,7 @@ public class TestModuleFiniteSets {
}
@Test(expected = TypeErrorException.class)
- public void unifyErrorIsFiniteSet2() throws FrontEndException, TLA2BException {
+ public void unifyErrorIsFiniteSet2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS FiniteSets \n"
+ "ASSUME 1 = IsFiniteSet({1})\n"
@@ -73,7 +73,7 @@ public class TestModuleFiniteSets {
* Cardinality
*/
@Test
- public void unifyCardinality() throws FrontEndException, TLA2BException {
+ public void unifyCardinality() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS FiniteSets \n"
+ "CONSTANTS k \n"
@@ -84,7 +84,7 @@ public class TestModuleFiniteSets {
}
@Test
- public void unifyCardinality2() throws FrontEndException, TLA2BException {
+ public void unifyCardinality2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS FiniteSets \n"
+ "CONSTANTS k, k2 \n"
@@ -96,7 +96,7 @@ public class TestModuleFiniteSets {
}
@Test(expected = TypeErrorException.class)
- public void unifyErrorCardinality() throws FrontEndException, TLA2BException {
+ public void unifyErrorCardinality() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS FiniteSets \n"
+ "ASSUME Cardinality(1)\n"
@@ -105,7 +105,7 @@ public class TestModuleFiniteSets {
}
@Test(expected = TypeErrorException.class)
- public void unifyErrorCardinality2() throws FrontEndException, TLA2BException {
+ public void unifyErrorCardinality2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS FiniteSets \n"
+ "ASSUME TRUE = Cardinality({1})\n"
diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleIntegers.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleIntegers.java
index ea50115d366dd14ef89ec64608aab877816b9bf4..4a3d5b1c02f45deccfc36d36baffc4574f636bdc 100644
--- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleIntegers.java
+++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleIntegers.java
@@ -17,7 +17,7 @@ public class TestModuleIntegers {
* Int
*/
@Test
- public void unifyInt() throws FrontEndException, TLA2BException {
+ public void unifyInt() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Integers \n"
+ "CONSTANTS k \n"
@@ -27,7 +27,7 @@ public class TestModuleIntegers {
}
@Test(expected = TypeErrorException.class)
- public void unifyErrorInt() throws FrontEndException, TLA2BException {
+ public void unifyErrorInt() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Integers \n"
+ "ASSUME TRUE \\in Int \n"
@@ -40,7 +40,7 @@ public class TestModuleIntegers {
* unary minus: -x
*/
@Test
- public void unifyUnaryMinus() throws FrontEndException, TLA2BException {
+ public void unifyUnaryMinus() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Integers \n"
+ "CONSTANTS k, k2 \n"
@@ -52,7 +52,7 @@ public class TestModuleIntegers {
}
@Test(expected = TypeErrorException.class)
- public void unifyErrorUnaryMinus() throws FrontEndException, TLA2BException {
+ public void unifyErrorUnaryMinus() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Integers \n"
+ "ASSUME TRUE = -1 \n"
diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java
index b7807acd24d497cefe906e97d8a3e141523e5173..505bb324f6de888248b7ec1c5c56602860f7bcb2 100644
--- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java
+++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java
@@ -17,8 +17,8 @@ public class TestModuleNaturals {
* Relational operators: >, <, <=, >=
*/
@Test
- public void testRelationalOperators() throws FrontEndException,
- TLA2BException {
+ public void testRelationalOperators() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
+ "CONSTANTS k, k2, k3 \n"
@@ -31,8 +31,8 @@ public class TestModuleNaturals {
}
@Test(expected = TypeErrorException.class)
- public void testRelationalOperatorsException() throws FrontEndException,
- TLA2BException {
+ public void testRelationalOperatorsException() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
+ "CONSTANTS k, k2 \n"
@@ -44,8 +44,8 @@ public class TestModuleNaturals {
* Arithmetic operator: +, -, *, /, mod, exp
*/
@Test
- public void testArithmeticOperators() throws FrontEndException,
- TLA2BException {
+ public void testArithmeticOperators() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
+ "CONSTANTS k, k2, k3 \n"
@@ -58,8 +58,8 @@ public class TestModuleNaturals {
}
@Test(expected = TypeErrorException.class)
- public void testArithmeticOperatorsException() throws FrontEndException,
- TLA2BException {
+ public void testArithmeticOperatorsException() throws
+ TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
+ "CONSTANTS k, k2 \n"
@@ -73,7 +73,7 @@ public class TestModuleNaturals {
*/
@Test
- public void testDotDot() throws FrontEndException, TLA2BException {
+ public void testDotDot() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
+ "CONSTANTS k, k2, k3 \n"
@@ -86,7 +86,7 @@ public class TestModuleNaturals {
}
@Test(expected = TypeErrorException.class)
- public void testDotDotException() throws FrontEndException, TLA2BException {
+ public void testDotDotException() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
+ "CONSTANTS k2, k3 \n"
@@ -99,7 +99,7 @@ public class TestModuleNaturals {
* Nat
*/
@Test
- public void testNat() throws FrontEndException, TLA2BException {
+ public void testNat() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
+ "CONSTANTS k \n"
@@ -109,7 +109,7 @@ public class TestModuleNaturals {
}
@Test(expected = TypeErrorException.class)
- public void unifyErrorNat() throws FrontEndException, TLA2BException {
+ public void unifyErrorNat() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
+ "ASSUME TRUE \\in Nat \n"
diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleSequences.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleSequences.java
index d5973ef2e6b56824ae5f750b6e7be69d126afacd..20c152bba70526cfaa8cef8b568e82802c88cb6e 100644
--- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleSequences.java
+++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleSequences.java
@@ -17,7 +17,7 @@ public class TestModuleSequences {
* Seq(S): The set of all sequences of elements in S.
*/
@Test
- public void testSeq() throws FrontEndException, TLA2BException {
+ public void testSeq() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k \n"
@@ -28,7 +28,7 @@ public class TestModuleSequences {
}
@Test
- public void testSeq2() throws FrontEndException, TLA2BException {
+ public void testSeq2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k \n"
@@ -41,7 +41,7 @@ public class TestModuleSequences {
@Test (expected = TypeErrorException.class)
- public void testSeqException() throws FrontEndException, TLA2BException {
+ public void testSeqException() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "ASSUME 1 = Seq({1}) \n"
@@ -50,7 +50,7 @@ public class TestModuleSequences {
}
@Test (expected = TypeErrorException.class)
- public void testSeqException2() throws FrontEndException, TLA2BException {
+ public void testSeqException2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k \n"
@@ -64,7 +64,7 @@ public class TestModuleSequences {
* Len(S)
*/
@Test
- public void testLen() throws FrontEndException, TLA2BException {
+ public void testLen() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k \n"
@@ -75,7 +75,7 @@ public class TestModuleSequences {
}
@Test (expected = TypeErrorException.class)
- public void testLenException() throws FrontEndException, TLA2BException {
+ public void testLenException() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k \n"
@@ -85,7 +85,7 @@ public class TestModuleSequences {
}
@Test (expected = TypeErrorException.class)
- public void testLenException2() throws FrontEndException, TLA2BException {
+ public void testLenException2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k \n"
@@ -95,7 +95,7 @@ public class TestModuleSequences {
}
@Test (expected = TypeErrorException.class)
- public void testUnifyErrorLen2() throws FrontEndException, TLA2BException {
+ public void testUnifyErrorLen2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k \n"
@@ -109,7 +109,7 @@ public class TestModuleSequences {
* s \o s2 - concatenation of s and s2
*/
@Test
- public void testUnifyConcatenation() throws FrontEndException, TLA2BException {
+ public void testUnifyConcatenation() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k, k2 \n"
@@ -121,7 +121,7 @@ public class TestModuleSequences {
}
@Test
- public void testUnifyConcatenation2() throws FrontEndException, TLA2BException {
+ public void testUnifyConcatenation2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k, k2 \n"
@@ -133,7 +133,7 @@ public class TestModuleSequences {
}
@Test
- public void testUnifyConcatenation3() throws FrontEndException, TLA2BException {
+ public void testUnifyConcatenation3() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k, k2, k3 \n"
@@ -146,7 +146,7 @@ public class TestModuleSequences {
}
@Test (expected = TypeErrorException.class)
- public void testUnifyErrorConcatenation() throws FrontEndException, TLA2BException {
+ public void testUnifyErrorConcatenation() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k, k2 \n"
@@ -156,7 +156,7 @@ public class TestModuleSequences {
}
@Test (expected = TypeErrorException.class)
- public void testUnifyErrorConcatenation2() throws FrontEndException, TLA2BException {
+ public void testUnifyErrorConcatenation2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k, k2 \n"
@@ -166,7 +166,7 @@ public class TestModuleSequences {
}
@Test (expected = TypeErrorException.class)
- public void testUnifyErrorConcatenation3() throws FrontEndException, TLA2BException {
+ public void testUnifyErrorConcatenation3() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k, k2 \n"
@@ -180,7 +180,7 @@ public class TestModuleSequences {
* Append(s, e)
*/
@Test
- public void testUnifyAppend() throws FrontEndException, TLA2BException {
+ public void testUnifyAppend() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k, k2, k3 \n"
@@ -194,7 +194,7 @@ public class TestModuleSequences {
}
@Test
- public void testUnifyAppend2() throws FrontEndException, TLA2BException {
+ public void testUnifyAppend2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k, k2, k3 \n"
@@ -208,7 +208,7 @@ public class TestModuleSequences {
}
@Test
- public void testUnifyAppend3() throws FrontEndException, TLA2BException {
+ public void testUnifyAppend3() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k, k2 \n"
@@ -222,7 +222,7 @@ public class TestModuleSequences {
@Test (expected = TypeErrorException.class)
- public void testUnifyErrorAppend() throws FrontEndException, TLA2BException {
+ public void testUnifyErrorAppend() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k, k2, k3 \n"
@@ -237,7 +237,7 @@ public class TestModuleSequences {
* Head(s): the first element of the seq
*/
@Test
- public void testUnifyHead() throws FrontEndException, TLA2BException {
+ public void testUnifyHead() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k, k2 \n"
@@ -249,7 +249,7 @@ public class TestModuleSequences {
}
@Test
- public void testUnifyHead2() throws FrontEndException, TLA2BException {
+ public void testUnifyHead2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k, k2 \n"
@@ -261,7 +261,7 @@ public class TestModuleSequences {
}
@Test (expected = TypeErrorException.class)
- public void testUnifyErrorHead() throws FrontEndException, TLA2BException {
+ public void testUnifyErrorHead() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k \n"
@@ -274,7 +274,7 @@ public class TestModuleSequences {
* Tail(s): the sequence without the first element
*/
@Test
- public void testUnifyTail() throws FrontEndException, TLA2BException {
+ public void testUnifyTail() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k, k2 \n"
@@ -286,7 +286,7 @@ public class TestModuleSequences {
}
@Test
- public void testUnifyTail2() throws FrontEndException, TLA2BException {
+ public void testUnifyTail2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k, k2 \n"
@@ -299,7 +299,7 @@ public class TestModuleSequences {
}
@Test (expected = TypeErrorException.class)
- public void testUnifyErrorTail() throws FrontEndException, TLA2BException {
+ public void testUnifyErrorTail() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k \n"
@@ -312,7 +312,7 @@ public class TestModuleSequences {
* SubSeq(s,m,n): The sequence <<s[m], s[m+1], ... , s[n]>>
*/
@Test
- public void testUnifySubSeq() throws FrontEndException, TLA2BException {
+ public void testUnifySubSeq() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k, k2, m, n \n"
@@ -326,7 +326,7 @@ public class TestModuleSequences {
}
@Test
- public void testUnifySubSeq2() throws FrontEndException, TLA2BException {
+ public void testUnifySubSeq2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k, k2, m, n \n"
@@ -340,7 +340,7 @@ public class TestModuleSequences {
}
@Test (expected = TypeErrorException.class)
- public void testUnifyErrorSubSeq() throws FrontEndException, TLA2BException {
+ public void testUnifyErrorSubSeq() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Sequences \n"
+ "CONSTANTS k, k2, m, n \n"
diff --git a/src/test/java/de/tla2b/util/TestTypeChecker.java b/src/test/java/de/tla2b/util/TestTypeChecker.java
index 0610c0addd9e6a05336b07da2bd5069f7c681818..69a9dda5c2d996aa4757be56c3e52205bed47a66 100644
--- a/src/test/java/de/tla2b/util/TestTypeChecker.java
+++ b/src/test/java/de/tla2b/util/TestTypeChecker.java
@@ -17,9 +17,9 @@ public class TestTypeChecker implements TranslationGlobals {
public ModuleNode moduleNode;
public final int toolId = 5;
- private Hashtable<String, TLAType> constants;
- private Hashtable<String, TLAType> variables;
- private Hashtable<String, DefCon> definitions;
+ private final Hashtable<String, TLAType> constants;
+ private final Hashtable<String, TLAType> variables;
+ private final Hashtable<String, DefCon> definitions;
public TestTypeChecker() {
constants = new Hashtable<String, TLAType>();
@@ -28,7 +28,7 @@ public class TestTypeChecker implements TranslationGlobals {
}
public void startTest(String moduleString, String configString)
- throws FrontEndException, TLA2BException {
+ throws TLA2BException {
Translator translator = new Translator(moduleString, configString);
translator.translate();
moduleNode = translator.getModuleNode();
@@ -36,7 +36,7 @@ public class TestTypeChecker implements TranslationGlobals {
}
public void start(String moduleFileName)
- throws FrontEndException, TLA2BException {
+ throws TLA2BException {
Translator translator = new Translator(moduleFileName);
translator.translate();
moduleNode = translator.getModuleNode();
@@ -103,7 +103,7 @@ public class TestTypeChecker implements TranslationGlobals {
}
public class DefCon {
- private Hashtable<String, TLAType> parameters;
+ private final Hashtable<String, TLAType> parameters;
private TLAType type;
private DefCon(TLAType t) {