fix a few typos

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

@@ -61,7 +61,7 @@ public class AbstractASTVisitor extends BuiltInOPs implements ASTConstants {
 				return;
 			}
 			case SubstInKind: {
-				visitStubstInNode((SubstInNode) node);
+				visitSubstInNode((SubstInNode) node);
 				return;
 			}
 			case AtNodeKind: { // @
@@ -150,7 +150,7 @@ public class AbstractASTVisitor extends BuiltInOPs implements ASTConstants {
 	public void visitAtNode(AtNode n) {
 	}
 
-	public void visitStubstInNode(SubstInNode n) {
+	public void visitSubstInNode(SubstInNode n) {
 		visitExprNode(n.getBody());
 	}
 

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

@@ -80,7 +80,6 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
 		AAssignSubstitution assign = new AAssignSubstitution();
 		if (!anyVariables.isEmpty()) { // ANY x_n WHERE P THEN A END
 			AAnySubstitution any = new AAnySubstitution();
-			any = new AAnySubstitution();
 			List<PExpression> anyParams = new ArrayList<>();
 			for (OpDeclNode var : anyVariables) {
 				String varName = var.getName().toString();
@@ -290,10 +289,10 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
 
 	private void findUnchangedVariables() {
 		unchangedVariables = new ArrayList<>();
-		findUnchangedVaribalesInSemanticNode(node);
+		findUnchangedVariablesInSemanticNode(node);
 	}
 
-	private void findUnchangedVaribalesInSemanticNode(SemanticNode node) {
+	private void findUnchangedVariablesInSemanticNode(SemanticNode node) {
 		switch (node.getKind()) {
 			case OpApplKind: {
 				findUnchangedVariablesInOpApplNode((OpApplNode) node);
@@ -301,13 +300,13 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
 			}
 			case LetInKind: {
 				LetInNode letNode = (LetInNode) node;
-				findUnchangedVaribalesInSemanticNode(letNode.getBody());
+				findUnchangedVariablesInSemanticNode(letNode.getBody());
 				return;
 			}
 
 			case SubstInKind: {
 				SubstInNode substInNode = (SubstInNode) node;
-				findUnchangedVaribalesInSemanticNode(substInNode.getBody());
+				findUnchangedVariablesInSemanticNode(substInNode.getBody());
 			}
 		}
 	}
@@ -318,14 +317,14 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
 		if (kind == UserDefinedOpKind
 			&& !BBuiltInOPs.contains(n.getOperator().getName())) {
 			OpDefNode def = (OpDefNode) n.getOperator();
-			findUnchangedVaribalesInSemanticNode(def.getBody());
+			findUnchangedVariablesInSemanticNode(def.getBody());
 		} else if (kind == BuiltInKind) {
 			int opcode = BuiltInOPs.getOpCode(n.getOperator().getName());
 			switch (opcode) {
 				case OPCODE_land: // \land
 				case OPCODE_cl: { // $ConjList
 					for (int i = 0; i < n.getArgs().length; i++) {
-						findUnchangedVaribalesInSemanticNode(n.getArgs()[i]);
+						findUnchangedVariablesInSemanticNode(n.getArgs()[i]);
 					}
 					return;
 				}

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

@@ -29,7 +29,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
 	private ExprNode nextExpr;
 
 	private ArrayList<OpDeclNode> bConstants;
-	// used to check if a b constant has arguments and is not overriden in the
+	// used to check if a b constant has arguments and is not overridden in the
 	// configfile
 
 	private ArrayList<BOperation> bOperations = new ArrayList<>();
@@ -40,7 +40,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
 	private Set<OpDefNode> usedDefinitions = new HashSet<>();
 	// definitions which are used for the type inference algorithm
 	private final Hashtable<OpDefNode, FormalParamNode[]> letParams = new Hashtable<>();
-	// additional parameters of an let Operator, these parameters are from the
+	// additional parameters of a let Operator, these parameters are from the
 	// surrounding operator
 	private final ArrayList<String> definitionMacros = new ArrayList<>();
 
@@ -199,7 +199,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
 		// usedDefinitions.addAll(bDefinitionsSet);
 
 		DebugMsg("Computing variable declarations");
-		// test whether there is a init predicate if there is a variable
+		// test whether there is an init predicate if there is a variable
 		if (moduleNode.getVariableDecls().length > 0 && inits == null) {
 			throw new SemanticErrorException("No initial predicate is defined.");
 		}
@@ -208,7 +208,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
 		for (OpDeclNode con : bConstants) {
 			if (con.getArity() > 0) {
 				throw new ConfigFileErrorException(
-					String.format("Constant '%s' must be overriden in the configuration file.", con.getName()));
+					String.format("Constant '%s' must be overridden in the configuration file.", con.getName()));
 			}
 		}
 		findRecursiveConstructs();

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

@@ -23,7 +23,7 @@ public class ConfigfileEvaluator {
 	private ModelConfig configAst;
 	private ModuleNode moduleNode;
 	private Hashtable<String, OpDefNode> definitions;
-	// Hashtable of all definitons in module
+	// Hashtable of all definitions in module
 	private Hashtable<String, OpDeclNode> constants;
 	// Hashtable of all constants in the module
 
@@ -45,7 +45,7 @@ public class ConfigfileEvaluator {
 	// List of constants in the resulting B machine. This list does not contain
 	// a TLA+ constant if the constant is substituted by a modelvalue with the
 	// same name (the constant name is moved to an enumerated set) or if the
-	// constants has arguments and is overriden by an operator
+	// constants has arguments and is overridden by an operator
 	public Hashtable<OpDefNode, OpDefNode> operatorOverrideTable;
 	// This table contains mappings for operators which are overridden in the
 	// configuration file
@@ -125,7 +125,7 @@ public class ConfigfileEvaluator {
 			} else {
 				throw new ConfigFileErrorException(
 					"Invalid declaration of the next state predicate."
-						+ " Module does not contain the defintion '"
+						+ " Module does not contain the definition '"
 						+ next + "'");
 			}
 		} else
@@ -141,7 +141,7 @@ public class ConfigfileEvaluator {
 			} else {
 				throw new ConfigFileErrorException(
 					"Invalid declaration of the initialisation predicate."
-						+ " Module does not contain the defintion '"
+						+ " Module does not contain the definition '"
 						+ init + "'");
 			}
 		} else {
@@ -158,7 +158,7 @@ public class ConfigfileEvaluator {
 			} else {
 				throw new ConfigFileErrorException(
 					"Invalid declaration of the specification predicate."
-						+ "Module does not contain the defintion '"
+						+ "Module does not contain the definition '"
 						+ spec + "'");
 			}
 		} else
@@ -185,12 +185,10 @@ public class ConfigfileEvaluator {
 	}
 
 	/**
-	 * Represents a override statement in the configuration file: k &lt;- def
+	 * Represents an override statement in the configuration file: k &lt;- def
 	 */
-	@SuppressWarnings("unchecked")
 	private void evalConstantOrDefOverrides() throws ConfigFileErrorException {
-		for (Map.Entry<String, String> entry : (Iterable<Map.Entry<String, String>>) configAst.getOverrides()
-			.entrySet()) {
+		for (Map.Entry<String, String> entry : configAst.getOverrides().entrySet()) {
 			String left = entry.getKey();
 			String right = entry.getValue();
 
@@ -228,9 +226,7 @@ public class ConfigfileEvaluator {
 
 				operatorOverrideTable.put(defNode, rightDefNode);
 			} else {
-				// every constants in the configuration file must appear in the
-				// TLA+
-				// module
+				// every constant in the configuration file must appear in the TLA+ module
 				throw new ConfigFileErrorException(
 					"Module does not contain the symbol: " + left);
 			}
@@ -275,9 +271,7 @@ public class ConfigfileEvaluator {
 				}
 
 			} else {
-				// every constants or operator in the configuration file must
-				// appear in the TLA+
-				// module
+				// every constant or operator in the configuration file must appear in the TLA+ module
 				throw new ConfigFileErrorException(
 					"Module does not contain the symbol: " + symbolName);
 			}
@@ -378,13 +372,13 @@ public class ConfigfileEvaluator {
 						// if (instanceNodes[i].getModule().getName().toString()
 						// .equals(moduleName)) {
 						// /*
-						// * A constant overridden in a instanced module make
-						// * no sence. Such a constant will be overridden by
+						// * A constant overridden in an instanced module make
+						// * no sense. Such a constant will be overridden by
 						// * the instance statement
 						// */
 						// throw new ConfigFileErrorException(
 						// String.format(
-						// "Invalid substitution for constant '%s' of module '%s'.%n A Constant of an instanced module can not be overriden.",
+						// "Invalid substitution for constant '%s' of module '%s'.%n A Constant of an instanced module can not be overridden.",
 						// left, mNode.getName().toString()));
 						// }
 					}
@@ -411,7 +405,6 @@ public class ConfigfileEvaluator {
 		/*
 		 * Search module in extended modules
 		 */
-		@SuppressWarnings("unchecked")
 		HashSet<ModuleNode> extendedModules = moduleNode.getExtendedModuleSet();
 		for (ModuleNode m : extendedModules) {
 			if (m.getName().toString().equals(moduleName)) {
@@ -535,7 +528,7 @@ public class ConfigfileEvaluator {
 		} else if (o.getClass().getName().equals("tlc2.value.impl.BoolValue")) {
 			return BoolType.getInstance();
 		} else {
-			throw new ConfigFileErrorException("Unkown ConstantType: " + o
+			throw new ConfigFileErrorException("Unknown ConstantType: " + o
 				+ " " + o.getClass());
 		}
 	}

src/main/java/de/tla2b/types/FunctionType.java

@@ -142,8 +142,8 @@ public class FunctionType extends AbstractHasFollowers {
 			range.getBNode());
 	}
 
-	public void apply(TypeVisitorInterface vistor) {
-		vistor.caseFunctionType(this);
+	public void apply(TypeVisitorInterface visitor) {
+		visitor.caseFunctionType(this);
 	}
 
 }

src/main/java/de/tla2b/util/FileUtils.java

@@ -7,10 +7,10 @@ import java.io.IOException;
 
 public class FileUtils {
 
-	public static String removeExtention(String filePath) {
+	public static String removeExtension(String filePath) {
 		File f = new File(filePath);
 
-		// if it's a directory, don't remove the extention
+		// if it's a directory, don't remove the extension
 		if (f.isDirectory())
 			return filePath;
 

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

@@ -23,8 +23,6 @@ import tlc2.value.impl.*;
 import java.util.*;
 import java.util.Map.Entry;
 
-import static tlc2.value.ValueConstants.*;
-
 public class BAstCreator extends BuiltInOPs
 	implements TranslationGlobals, ASTConstants, BBuildIns, Priorities, ValueConstants {
 
@@ -764,7 +762,7 @@ public class BAstCreator extends BuiltInOPs
 		if (BBuiltInOPs.contains(def.getName()) // Operator is a B built-in
 			// operator
 			&& STANDARD_MODULES.contains(def.getSource().getOriginallyDefinedInModuleNode().getName().toString())) {
-			return visitBBuitInsPredicate(n);
+			return visitBBuiltInsPredicate(n);
 		}
 		if (specAnalyser.getRecursiveFunctions().contains(def)) {
 			return new AEqualPredicate(createIdentifierNode(def), new ABooleanTrueExpression());
@@ -804,7 +802,7 @@ public class BAstCreator extends BuiltInOPs
 		// Operator is a B built-in operator
 		if (BBuiltInOPs.contains(def.getName())
 			&& STANDARD_MODULES.contains(def.getSource().getOriginallyDefinedInModuleNode().getName().toString())) {
-			return visitBBuitInsExpression(n);
+			return visitBBuiltInsExpression(n);
 		}
 
 		if (specAnalyser.getRecursiveFunctions().contains(def)) {
@@ -873,7 +871,7 @@ public class BAstCreator extends BuiltInOPs
 
 	}
 
-	private PPredicate visitBBuitInsPredicate(OpApplNode opApplNode) {
+	private PPredicate visitBBuiltInsPredicate(OpApplNode opApplNode) {
 		PPredicate returnNode = null;
 		switch (BBuiltInOPs.getOpcode(opApplNode.getOperator().getName())) {
 			case B_OPCODE_lt: // <
@@ -936,7 +934,7 @@ public class BAstCreator extends BuiltInOPs
 		}
 	}
 
-	private PExpression visitBBuitInsExpression(OpApplNode opApplNode) {
+	private PExpression visitBBuiltInsExpression(OpApplNode opApplNode) {
 		PExpression returnNode = null;
 		switch (BBuiltInOPs.getOpcode(opApplNode.getOperator().getName())) {
 			case B_OPCODE_bool: // BOOLEAN
@@ -1279,7 +1277,7 @@ public class BAstCreator extends BuiltInOPs
 			}
 
 			case 0: {
-				return visitBBuitInsExpression(n);
+				return visitBBuiltInsExpression(n);
 			}
 
 			case OPCODE_setdiff: // set difference
@@ -1335,46 +1333,47 @@ public class BAstCreator extends BuiltInOPs
 					FormalParamNode p = params[0][i];
 					list.add(createIdentifierNode(p));
 				}
-				AComprehensionSetExpression compre = new AComprehensionSetExpression();
-				compre.setIdentifiers(list);
-				PPredicate typing = visitBoundsOfFunctionsVariables(n);
-				AConjunctPredicate conj = new AConjunctPredicate(typing, visitExprOrOpArgNodePredicate(n.getArgs()[0]));
-				compre.setPredicates(conj);
-				return compre;
+				return new AComprehensionSetExpression(
+					list,
+					new AConjunctPredicate(
+						visitBoundsOfFunctionsVariables(n),
+						visitExprOrOpArgNodePredicate(n.getArgs()[0])
+					)
+				);
 			}
 
 			case OPCODE_soa: { // $SetOfAll Represents {e : p1 \in S, p2,p3 \in S2}
 				FormalParamNode[][] params = n.getBdedQuantSymbolLists();
 				List<PExpression> idList = createListOfIdentifier(params);
 				List<PPredicate> predList = new ArrayList<>();
-
 				predList.add(visitBoundsOfLocalVariables(n));
-				final String nameOfTempVariable = "t_";
-				AEqualPredicate equals = new AEqualPredicate();
-				equals.setLeft(createIdentifierNode(nameOfTempVariable));
-				equals.setRight(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
+
+				// currently not used:
+				/* final String nameOfTempVariable = "t_";
+
+				AEqualPredicate equals = new AEqualPredicate(
+					createIdentifierNode(nameOfTempVariable),
+					visitExprOrOpArgNodeExpression(n.getArgs()[0])
+				);
 				// predList.add(equals);
-				AExistsPredicate exist = new AExistsPredicate();
-				exist.setIdentifiers(idList);
-				exist.setPredicate(createConjunction(predList));
+				AExistsPredicate exist = new AExistsPredicate(
+					idList,
+					createConjunction(predList)
+				);
 
 				AComprehensionSetExpression compre = new AComprehensionSetExpression();
 				List<PExpression> tList = new ArrayList<>();
 				tList.add(createIdentifierNode(nameOfTempVariable));
 				compre.setIdentifiers(tList);
-				compre.setPredicates(exist);
+				compre.setPredicates(exist);*/
 
 				// UNION(p1,p2,p3).(P | {e})
-				AQuantifiedUnionExpression union = new AQuantifiedUnionExpression();
-				union.setIdentifiers(idList);
-				union.setPredicates(createConjunction(predList));
-				ASetExtensionExpression set = new ASetExtensionExpression();
-				List<PExpression> list = new ArrayList<>();
-				list.add(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
-				set.setExpressions(list);
-				union.setExpression(set);
-
-				return union;
+				return new AQuantifiedUnionExpression(
+					idList,
+					createConjunction(predList),
+					new ASetExtensionExpression(
+						Collections.singletonList(visitExprOrOpArgNodeExpression(n.getArgs()[0])))
+				);
 			}
 
 			case OPCODE_nrfs:
@@ -2188,7 +2187,7 @@ public class BAstCreator extends BuiltInOPs
 				break;
 			}
 			case 0:
-				return visitBBuitInsPredicate(n);
+				return visitBBuiltInsPredicate(n);
 			default:
 				throw new NotImplementedException(n.getOperator().getName().toString());
 		}

src/main/java/de/tla2bAst/ExpressionTranslator.java

@@ -151,7 +151,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
 		try {
 			SANY.frontEndMain(spec, moduleName, ToolIO.out);
 		} catch (FrontEndException e) {
-			// Error in Frontend, should never happens
+			// Error in Frontend, should never happen
 			throw new de.tla2b.exceptions.FrontEndException(
 				"Frontend error! This should never happen.", spec);
 		}
@@ -206,7 +206,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
 	}
 
 	private void evalVariables(SpecObj spec, String moduleName) {
-		ParseUnit p = (ParseUnit) spec.parseUnitContext.get(moduleName);
+		ParseUnit p = spec.parseUnitContext.get(moduleName);
 		TreeNode n_module = p.getParseTree();
 		TreeNode n_body = n_module.heirs()[2];
 		TreeNode n_operatorDefintion = n_body.heirs()[0];
@@ -276,7 +276,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
 				break;
 			}
 			case
-				N_UnboundQuant: { // TOOD: check: is this an unbounded quantifier with infinite domain or a quantifier that does not hide the quantified variables?
+				N_UnboundQuant: { // TODO: check: is this an unbounded quantifier with infinite domain or a quantifier that does not hide the quantified variables?
 				TreeNode[] children = treeNode.heirs();
 				for (int i = 1; i < children.length - 2; i = i + 2) {
 					// System.out.println("N_UnboundQuant: "+children[i].getImage());

src/main/java/de/tla2bAst/Translator.java

@@ -59,7 +59,7 @@ public class Translator implements TranslationGlobals {
 	}
 
 	private void findConfigFile() {
-		String configFileName = FileUtils.removeExtention(moduleFile.getAbsolutePath());
+		String configFileName = FileUtils.removeExtension(moduleFile.getAbsolutePath());
 		configFileName = configFileName + ".cfg";
 		configFile = new File(configFileName);
 		if (!configFile.exists()) {
@@ -235,7 +235,7 @@ public class Translator implements TranslationGlobals {
 	}
 
 	public void createProbFile() {
-		String fileName = FileUtils.removeExtention(moduleFile.getAbsolutePath());
+		String fileName = FileUtils.removeExtension(moduleFile.getAbsolutePath());
 		fileName = fileName + ".prob";
 		File probFile;
 		probFile = new File(fileName);
@@ -252,7 +252,7 @@ public class Translator implements TranslationGlobals {
 			bParser.getDefinitions().addDefinitions(getBDefinitions());
 			final RecursiveMachineLoader rml = parseAllMachines(getBAST(), getModuleFile(), bParser);
 
-			String moduleName = FileUtils.removeExtention(moduleFile.getName());
+			String moduleName = FileUtils.removeExtension(moduleFile.getName());
 			PrologPrinter prologPrinter = new PrologPrinter(rml, bParser, moduleFile, moduleName, typeTable);
 			prologPrinter.setPositions(bAstCreator.getSourcePositions());
 
@@ -268,7 +268,7 @@ public class Translator implements TranslationGlobals {
 	}
 
 	public void createMachineFile() {
-		String bFile = FileUtils.removeExtention(moduleFile.getAbsolutePath());
+		String bFile = FileUtils.removeExtension(moduleFile.getAbsolutePath());
 		bFile = bFile + "_tla.txt";
 
 		File machineFile;

src/test/java/de/tla2b/prettyprintb/ExternelFunctionsTest.java → src/test/java/de/tla2b/prettyprintb/ExternalFunctionsTest.java

@@ -4,7 +4,7 @@ import org.junit.Test;
 
 import static de.tla2b.util.TestUtil.compare;
 
-public class ExternelFunctionsTest {
+public class ExternalFunctionsTest {
 
 
 	@Test

src/test/java/de/tla2b/prettyprintb/SetsTest.java

@@ -104,7 +104,7 @@ public class SetsTest {
 	 * Subseteq: subset or equal
 	 */
 	@Test
-	public void testSubsteq() throws Exception {
+	public void testSubseteq() throws Exception {
 		final String module = "-------------- MODULE Testing ----------------\n"
 			+ "ASSUME TRUE = ({1} \\subseteq {1,2}) \n"
 			+ "=================================";

src/test/java/de/tla2b/typechecking/OpArgTest.java

@@ -10,7 +10,7 @@ import static org.junit.Assert.assertEquals;
 public class OpArgTest {
 
 	@Test
-	public void TestConOverridenByLessOp() throws Exception {
+	public void TestConOverriddenByLessOp() throws Exception {
 		final String module = "-------------- MODULE Testing ----------------\n"
 			+ "EXTENDS Naturals \n"
 			+ "CONSTANTS k(_,_), k2 \n"
@@ -21,7 +21,7 @@ public class OpArgTest {
 	}
 
 	@Test(expected = ConfigFileErrorException.class)
-	public void TestOverridenConstantWrongArityException() throws Exception {
+	public void TestOverriddenConstantWrongArityException() throws Exception {
 		final String module = "-------------- MODULE Testing ----------------\n"
 			+ "CONSTANTS k(_,_) \n"
 			+ "def == TRUE /\\ FALSE \n"
@@ -31,7 +31,7 @@ public class OpArgTest {
 	}
 
 	@Test(expected = ConfigFileErrorException.class)
-	public void TestOverridenDefWrongArityException() throws Exception {
+	public void TestOverriddenDefWrongArityException() throws Exception {
 		final String module = "-------------- MODULE Testing ----------------\n"
 			+ "foo(a, b) == a /\\ b  \n"
 			+ "def == TRUE /\\ FALSE \n"
@@ -42,7 +42,7 @@ public class OpArgTest {
 	}
 
 	@Test
-	public void TestOverridenByDef() throws Exception {
+	public void TestOverriddenByDef() throws Exception {
 		final String module = "-------------- MODULE Testing ----------------\n"
 			+ "CONSTANTS k(_,_), k2 \n"
 			+ "def(a,b) == a /\\ b \n"