code refactoring

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

@@ -185,8 +185,9 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
 			if (node instanceof OpApplNode) {
 				OpApplNode opApplNode = (OpApplNode) node;
 				if (opApplNode.getOperator().getKind() == BuiltInKind) {
-					switch (getOpCode(opApplNode.getOperator().getName())) {
-					case OPCODE_eq: {
+
+					if (OPCODE_eq == getOpCode(opApplNode.getOperator()
+							.getName())) {
 						ExprOrOpArgNode arg1 = opApplNode.getArgs()[0];
 						try {
 							OpApplNode arg11 = (OpApplNode) arg1;
@@ -204,12 +205,9 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
 
 							}
 						} catch (ClassCastException e) {
-
 						}
-
-					}
-					default:
 					}
+
 				}
 			}
 		}
@@ -263,7 +261,7 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
 			beforeAfterPredicates.add(node);
 			return;
 		}
-		//beforeAfterPredicates.add(node);
+		// beforeAfterPredicates.add(node);
 	}
 
 	private void evalParams() {

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

@@ -14,7 +14,6 @@ import tla2sany.semantic.Context;
 import tla2sany.semantic.ExprNode;
 import tla2sany.semantic.ExprOrOpArgNode;
 import tla2sany.semantic.FormalParamNode;
-import tla2sany.semantic.InstanceNode;
 import tla2sany.semantic.LetInNode;
 import tla2sany.semantic.ModuleNode;
 import tla2sany.semantic.NumeralNode;

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

@@ -20,7 +20,6 @@ import de.tla2b.global.TranslationGlobals;
 import de.tla2b.translation.BDefinitionsFinder;
 import de.tla2b.translation.OperationsFinder;
 import de.tla2b.translation.UsedDefinitionsFinder;
-import de.tla2b.types.IType;
 import tla2sany.semantic.ASTConstants;
 import tla2sany.semantic.ExprNode;
 import tla2sany.semantic.ExprOrOpArgNode;
@@ -43,8 +42,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 
 	private OpDefNode expressionOpdefNode;
 	private Hashtable<String, SymbolNode> namingHashTable = new Hashtable<String, SymbolNode>();
-	
-	
+
 	private final ModuleNode moduleNode;
 	private ExprNode nextExpr;
 
@@ -87,18 +85,16 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 
 		return specAnalyser;
 	}
-	
-	
-	
-	public static SpecAnalyser createSpecAnalyserForTlaExpression(ModuleNode m){
+
+	public static SpecAnalyser createSpecAnalyserForTlaExpression(ModuleNode m) {
 		SpecAnalyser specAnalyser = new SpecAnalyser(m);
-		
-		specAnalyser.expressionOpdefNode = m.getOpDefs()[m.getOpDefs().length-1];
+
+		specAnalyser.expressionOpdefNode = m.getOpDefs()[m.getOpDefs().length - 1];
 		specAnalyser.usedDefinitions.add(specAnalyser.expressionOpdefNode);
 		specAnalyser.bDefinitionsSet.add(specAnalyser.expressionOpdefNode);
 		return specAnalyser;
 	}
-	
+
 	public static SpecAnalyser createSpecAnalyser(ModuleNode m) {
 		SpecAnalyser specAnalyser = new SpecAnalyser(m);
 		Hashtable<String, OpDefNode> definitions = new Hashtable<String, OpDefNode>();
@@ -109,7 +105,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 		specAnalyser.spec = definitions.get("Spec");
 		specAnalyser.init = definitions.get("Init");
 		specAnalyser.next = definitions.get("Next");
-		if(definitions.containsKey("Inv")){
+		if (definitions.containsKey("Inv")) {
 			specAnalyser.invariants.add(definitions.get("Inv"));
 		}
 		// TODO are constant in the right order
@@ -132,27 +128,27 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 		for (OpDefNode inv : new ArrayList<OpDefNode>(invariants)) {
 			try {
 				OpApplNode opApplNode = (OpApplNode) inv.getBody();
-				
+
 				OpDefNode opDefNode = (OpDefNode) opApplNode.getOperator();
-				
-			    if (opDefNode.getKind() == UserDefinedOpKind && !BBuiltInOPs.contains(opDefNode.getName())){
+
+				if (opDefNode.getKind() == UserDefinedOpKind
+						&& !BBuiltInOPs.contains(opDefNode.getName())) {
 					int i = invariants.indexOf(inv);
 					invariants.set(i, opDefNode);
-			    }
+				}
 			} catch (ClassCastException e) {
 			}
 		}
-		
-		
+
 		OperationsFinder operationsFinder = new OperationsFinder(this);
 		bOperations = operationsFinder.getBOperations();
-		
+
 		UsedDefinitionsFinder definitionFinder = new UsedDefinitionsFinder(this);
 		this.usedDefinitions = definitionFinder.getUsedDefinitions();
-		
+
 		BDefinitionsFinder bDefinitionFinder = new BDefinitionsFinder(this);
 		this.bDefinitionsSet = bDefinitionFinder.getBDefinitionsSet();
-		//usedDefinitions.addAll(bDefinitionsSet);
+		// usedDefinitions.addAll(bDefinitionsSet);
 
 		// test whether there is a init predicate if there is a variable
 		if (moduleNode.getVariableDecls().length > 0 && inits == null) {
@@ -170,9 +166,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 			}
 		}
 		findRecursiveConstructs();
-		
-		
-		
+
 		for (OpDeclNode var : moduleNode.getVariableDecls()) {
 			namingHashTable.put(var.getName().toString(), var);
 		}
@@ -182,7 +176,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 		for (OpDefNode def : usedDefinitions) {
 			namingHashTable.put(def.getName().toString(), def);
 		}
-		
+
 	}
 
 	private void evalInit() {
@@ -263,12 +257,12 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 		Set<OpDefNode> set = new HashSet<OpDefNode>(usedDefinitions);
 		for (OpDefNode def : set) {
 			if (def.getInRecursive()) {
-				throw new NotImplementedException("Recursive definitions are currently not supported.");
-//				bDefinitionsSet.remove(def);
-//				RecursiveDefinition rd = new RecursiveDefinition(def);
-//				recursiveDefinitions.add(rd);
-			} else
-			if (def.getBody() instanceof OpApplNode) {
+				throw new NotImplementedException(
+						"Recursive definitions are currently not supported.");
+				// bDefinitionsSet.remove(def);
+				// RecursiveDefinition rd = new RecursiveDefinition(def);
+				// recursiveDefinitions.add(rd);
+			} else if (def.getBody() instanceof OpApplNode) {
 				OpApplNode o = (OpApplNode) def.getBody();
 				switch (getOpCode(o.getOperator().getName())) {
 				case OPCODE_rfs: { // recursive Function
@@ -297,7 +291,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 	}
 
 	public Hashtable<OpDefNode, FormalParamNode[]> getLetParams() {
-		return letParams;
+		return new Hashtable<OpDefNode, FormalParamNode[]>(letParams);
 	}
 
 	public ArrayList<String> getDefinitionMacros() {
@@ -320,24 +314,24 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 		return this.moduleNode;
 	}
 
-	public ConfigfileEvaluator getConfigFileEvaluator(){
+	public ConfigfileEvaluator getConfigFileEvaluator() {
 		return configFileEvaluator;
 	}
-	
-	public ArrayList<OpDefNode> getInvariants(){
+
+	public ArrayList<OpDefNode> getInvariants() {
 		return invariants;
 	}
-	
-	public OpDefNode getInitDef(){
+
+	public OpDefNode getInitDef() {
 		return init;
 	}
-	
-	public OpDefNode getExpressionOpdefNode(){
+
+	public OpDefNode getExpressionOpdefNode() {
 		return expressionOpdefNode;
 	}
-	
-	public SymbolNode getSymbolNodeByName(String name){
+
+	public SymbolNode getSymbolNodeByName(String name) {
 		return namingHashTable.get(name);
 	}
-	
+
 }

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

@@ -45,7 +45,7 @@ import tlc2.tool.BuiltInOPs;
 public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 		TranslationGlobals {
 
-	private final int TEMP_TYPE_ID = 6;
+	private static final int TEMP_TYPE_ID = 6;
 	private int paramId;
 
 	private ArrayList<ExprNode> inits;
@@ -461,14 +461,15 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 			}
 
 			TLAType found = ((TLAType) def.getToolObject(TYPE_ID));
-			if (found == null){
+			if (found == null) {
 				found = new UntypedType();
-			// throw new RuntimeException(def.getName() + " has no type yet!");
+				// throw new RuntimeException(def.getName() +
+				// " has no type yet!");
 			}
-			if(n.getArgs().length != 0){
+			if (n.getArgs().length != 0) {
 				found = found.cloneTLAType();
 			}
-			
+
 			try {
 				found = found.unify(expected);
 			} catch (UnificationException e) {

src/main/java/de/tla2b/output/ASTPrettyPrinter.java

@@ -13,14 +13,12 @@ import de.be4.classicalb.core.parser.node.AConjunctPredicate;
 import de.be4.classicalb.core.parser.node.ADefinitionExpression;
 import de.be4.classicalb.core.parser.node.ADefinitionPredicate;
 import de.be4.classicalb.core.parser.node.AExpressionDefinitionDefinition;
-import de.be4.classicalb.core.parser.node.AFirstProjectionExpression;
 import de.be4.classicalb.core.parser.node.AGeneralSumExpression;
 import de.be4.classicalb.core.parser.node.AIdentifierExpression;
 import de.be4.classicalb.core.parser.node.ALambdaExpression;
 import de.be4.classicalb.core.parser.node.AOperation;
 import de.be4.classicalb.core.parser.node.AOperationsMachineClause;
 import de.be4.classicalb.core.parser.node.APredicateDefinitionDefinition;
-import de.be4.classicalb.core.parser.node.ASecondProjectionExpression;
 import de.be4.classicalb.core.parser.node.ASelectSubstitution;
 import de.be4.classicalb.core.parser.node.Node;
 import de.be4.classicalb.core.parser.node.PExpression;

src/main/java/de/tla2b/translation/BDefinitionsFinder.java

@@ -12,7 +12,6 @@ import de.tla2b.analysis.AbstractASTVisitor;
 import de.tla2b.analysis.BOperation;
 import de.tla2b.analysis.SpecAnalyser;
 import de.tla2b.global.TranslationGlobals;
-import de.tla2b.types.IType;
 
 public class BDefinitionsFinder extends AbstractASTVisitor implements
 		ASTConstants, ToolGlobals, TranslationGlobals {

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

@@ -2,8 +2,6 @@ package de.tla2b.types;
 
 import de.be4.classicalb.core.parser.node.PExpression;
 import de.tla2b.exceptions.UnificationException;
-import de.tla2b.output.TypeVisitorInterface;
-
 
 public abstract class TLAType implements IType {
 	private int kind;

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

@@ -204,7 +204,7 @@ public class TupleOrFunction extends AbstractHasFollowers {
 	public TLAType cloneTLAType() {
 		TupleOrFunction res = new TupleOrFunction();
 		for (Entry<Integer, TLAType> entry : this.types.entrySet()) {
-			res.types.put(new Integer(entry.getKey().intValue()), entry
+			res.types.put(Integer.valueOf(entry.getKey().intValue()), entry
 					.getValue().cloneTLAType());
 		}
 		return res;
@@ -390,14 +390,4 @@ public class TupleOrFunction extends AbstractHasFollowers {
 		}
 		return true;
 	}
-
-	private static boolean allTyped(List<TLAType> typeList) {
-		for (int i = 0; i < typeList.size(); i++) {
-			if (typeList.get(i).isUntyped()) {
-				return false;
-			}
-		}
-		return true;
-	}
-
 }

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

@@ -94,7 +94,6 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 
 		ExprNode expr = moduleNode.getOpDefs()[moduleNode.getOpDefs().length - 1]
 				.getBody();
-		System.out.println(expressionIsAPredicate(expr));
 		if (expressionIsAPredicate(expr)) {
 			APredicateParseUnit predicateParseUnit = new APredicateParseUnit();
 			predicateParseUnit.setPredicate(visitExprNodePredicate(expr));
@@ -832,7 +831,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 		switch (n.getOperator().getKind()) {
 		case VariableDeclKind:
 		case ConstantDeclKind:
-		case FormalParamKind: { // TODO
+		case FormalParamKind: {
 			return new AEqualPredicate(createIdentifierNode(n.getOperator()),
 					new ABooleanTrueExpression());
 		}
@@ -1503,7 +1502,6 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 		case OPCODE_fc: // Represents [x \in S |-> e].
 		case OPCODE_rfs: {
 			FormalParamNode[][] params = n.getBdedQuantSymbolLists();
-			// ExprNode[] bounds = n.getBdedQuantBounds(); TODO
 			List<PExpression> idList = new ArrayList<PExpression>();
 			for (int i = 0; i < params.length; i++) {
 				for (int j = 0; j < params[i].length; j++) {
@@ -1511,9 +1509,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 					idList.add(createIdentifierNode(p));
 				}
 			}
-
 			boolean[] isTuple = n.isBdedQuantATuple();
-
 			ALambdaExpression lambda = new ALambdaExpression();
 			List<PExpression> idList2 = new ArrayList<PExpression>();
 			for (int i = 0; i < params.length; i++) {
@@ -2137,12 +2133,6 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 		return list;
 	}
 
-	private List<PExpression> createIdentifierList(SymbolNode symbolNode) {
-		ArrayList<PExpression> list = new ArrayList<PExpression>();
-		list.add(createIdentifierNode(getName(symbolNode)));
-		return list;
-	}
-
 	private PPredicate visitBuiltInKindPredicate(OpApplNode n) {
 		switch (getOpCode(n.getOperator().getName())) {
 		case OPCODE_land: // \land

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

@@ -137,7 +137,6 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
 					+ "\n" + expr + "\n";
 			throw new ExpressionTranslationException(message);
 		}
-
 		SymbolRenamer symRenamer = new SymbolRenamer(moduleNode, specAnalyser);
 		symRenamer.start();
 		BAstCreator bASTCreator = new BAstCreator(moduleNode, specAnalyser);

src/test/java/de/tla2b/expression/ModuleAndExpressionTest.java

@@ -7,11 +7,12 @@ import org.junit.Test;
 import de.tla2b.exceptions.TypeErrorException;
 
 public class ModuleAndExpressionTest {
+	
 	@Test
 	public void testCon() throws Exception {
 		String module = "---- MODULE Testing ----\n" + "CONSTANTS k \n"
 				+ "ASSUME k = 4" + "===============";
-		compareExprIncludingModel("bool(k = 1)", "k = 1", module);
+		compareExprIncludingModel("k = 1", "k = 1", module);
 	}
 
 	@Test(expected = TypeErrorException.class)

src/test/java/de/tla2b/util/TestTypeChecker.java

@@ -10,7 +10,6 @@ import de.tla2b.exceptions.FrontEndException;
 import de.tla2b.exceptions.TLA2BException;
 import de.tla2b.global.TranslationGlobals;
 import de.tla2b.types.TLAType;
-import de.tla2b.types.TupleOrFunction;
 import de.tla2bAst.Translator;
 import tla2sany.semantic.FormalParamNode;
 import tla2sany.semantic.ModuleNode;

src/test/java/de/tla2b/util/TestUtil.java

@@ -64,7 +64,7 @@ public class TestUtil {
 		Renamer renamer = new Renamer(resultNode);
 		ASTPrettyPrinter aP = new ASTPrettyPrinter(resultNode, renamer);
 		resultNode.apply(aP);
-		System.out.println(aP.getResultString());
+		//System.out.println(aP.getResultString());
 		String bAstString = getAstStringofBExpressionString(bExpr);
 		String result = getAstStringofBExpressionString(aP.getResultString());
 		// String tlaAstString = getTreeAsString(resultNode);
@@ -72,11 +72,16 @@ public class TestUtil {
 	}
 
 	public static void compareExprIncludingModel(String bExpr, String tlaExpr,
-			String moduleString) throws TLA2BException {
+			String moduleString) throws TLA2BException, BException {
 		Translator trans = new Translator(moduleString, null);
 		trans.translate();
-		Start result = trans.translateExpression(tlaExpr);
-		// TODO
+		Start resultNode = trans.translateExpression(tlaExpr);
+		Renamer renamer = new Renamer(resultNode);
+		ASTPrettyPrinter aP = new ASTPrettyPrinter(resultNode, renamer);
+		resultNode.apply(aP);
+		String bAstString = getAstStringofBExpressionString(bExpr);
+		String result = getAstStringofBExpressionString(aP.getResultString());
+		assertEquals(bAstString, result);
 	}
 
 	public static void compare(String bMachine, String tlaModule)