refactored "used definitions" class

build.gradle

@@ -69,6 +69,10 @@ jacocoTestReport {
 //}
 
 
+test { 
+	exclude('testing')
+}
+
 jar { from sourceSets.main.allJava }
 jar	{
 	from configurations.releaseJars.collect { it.isDirectory() ? it : zipTree(it) }

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

@@ -174,8 +174,9 @@ public class AbstractASTVisitor extends BuiltInOPs implements ASTConstants {
 	}
 
 	public void visitUserDefinedNode(OpApplNode n) {
-		ExprOrOpArgNode[] arguments = n.getArgs();
-		for (ExprOrOpArgNode exprOrOpArgNode : arguments) {
+
+		
+		for (ExprOrOpArgNode exprOrOpArgNode : n.getArgs()) {
 			visitExprOrOpArgNode(exprOrOpArgNode);
 		}
 	}

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

@@ -17,8 +17,8 @@ import de.tla2b.exceptions.NotImplementedException;
 import de.tla2b.exceptions.SemanticErrorException;
 import de.tla2b.global.BBuiltInOPs;
 import de.tla2b.global.TranslationGlobals;
+import de.tla2b.translation.UsedDefinitionsFinder;
 import de.tla2b.types.IType;
-
 import tla2sany.semantic.ASTConstants;
 import tla2sany.semantic.AssumeNode;
 import tla2sany.semantic.ExprNode;
@@ -74,7 +74,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 
 	private ArrayList<RecursiveDefinition> recursiveDefinitions = new ArrayList<RecursiveDefinition>();
 
-	private ConfigfileEvaluator conEval;
+	private ConfigfileEvaluator configFileEvaluator;
 
 	private SpecAnalyser(ModuleNode m) {
 		this.moduleNode = m;
@@ -89,7 +89,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 		specAnalyser.next = conEval.getNextNode();
 		specAnalyser.invariants = conEval.getInvariants();
 		specAnalyser.bConstants = conEval.getbConstantList();
-		specAnalyser.conEval = conEval;
+		specAnalyser.configFileEvaluator = conEval;
 
 		return specAnalyser;
 	}
@@ -123,7 +123,11 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 		findOperations();
 
 		findDefinitions();
-		usedDefinitions.addAll(bDefinitionsSet);
+		
+		UsedDefinitionsFinder definitionFinder = new UsedDefinitionsFinder(this);
+		
+		usedDefinitions = definitionFinder.getUsedDefinitions();
+		//usedDefinitions.addAll(bDefinitionsSet);
 
 		// test whether there is a init predicate if there is a variable
 		if (moduleNode.getVariableDecls().length > 0 && inits == null) {
@@ -371,8 +375,8 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 	 */
 
 	private void findDefinitions() throws ConfigFileErrorException {
-		if (conEval != null) {
-			bDefinitionsSet.addAll(conEval.getConstantOverrideTable().values());
+		if (configFileEvaluator != null) {
+			bDefinitionsSet.addAll(configFileEvaluator.getConstantOverrideTable().values());
 		}
 
 		AssumeNode[] assumes = moduleNode.getAssumptions();
@@ -386,6 +390,10 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 			}
 		}
 
+		
+//		if(nextExpr != null){
+//			findDefintionInExprNode(nextExpr, null);
+//		}
 		if (bOperations != null) {
 			for (int i = 0; i < bOperations.size(); i++) {
 				ExprNode node = bOperations.get(i).getNode();
@@ -423,6 +431,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 			findDefintionInExprNode(def.getBody(), null);
 		}
 		
+		//bDefinitionsSet.remove(next);
 	}
 
 	/**
@@ -567,7 +576,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 	 * 
 	 */
 	private void evalRecursiveFunctions() throws NotImplementedException {
-		Set<OpDefNode> set = new HashSet<OpDefNode>(bDefinitionsSet);
+		Set<OpDefNode> set = new HashSet<OpDefNode>(usedDefinitions);
 		for (OpDefNode def : set) {
 			if (def.getInRecursive()) {
 				bDefinitionsSet.remove(def);
@@ -645,4 +654,12 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
 		return this.moduleNode;
 	}
 
+	public ConfigfileEvaluator getConfigFileEvaluator(){
+		return configFileEvaluator;
+	}
+	
+	public ArrayList<OpDefNode> getInvariants(){
+		return invariants;
+	}
+	
 }

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

+package de.tla2b.translation;
+
+import java.util.Collection;
+import java.util.HashSet;
+
+import tla2sany.semantic.ASTConstants;
+import tla2sany.semantic.ModuleNode;
+import tla2sany.semantic.OpApplNode;
+import tla2sany.semantic.OpDefNode;
+import tlc2.tool.ToolGlobals;
+import de.tla2b.analysis.AbstractASTVisitor;
+import de.tla2b.analysis.SpecAnalyser;
+import de.tla2b.global.BBuiltInOPs;
+import de.tla2b.global.TranslationGlobals;
+import de.tla2b.types.IType;
+
+public class UsedDefinitionsFinder extends AbstractASTVisitor implements
+		ASTConstants, ToolGlobals, IType, TranslationGlobals {
+
+	private final HashSet<OpDefNode> usedDefinitions = new HashSet<OpDefNode>();
+	
+	public UsedDefinitionsFinder(SpecAnalyser specAnalyser) {
+		
+		if(specAnalyser.getConfigFileEvaluator() != null){
+			Collection<OpDefNode> cons = specAnalyser.getConfigFileEvaluator().getConstantOverrideTable().values();
+			for (OpDefNode def : cons) {
+				visitExprNode(def.getBody());
+			}
+			Collection<OpDefNode> ops = specAnalyser.getConfigFileEvaluator().getOperatorOverrideTable().values();
+			for (OpDefNode def : cons) {
+				visitExprNode(def.getBody());
+			}
+			usedDefinitions.addAll(cons);
+			usedDefinitions.addAll(ops);
+		}
+		
+		visitAssumptions(specAnalyser.getModuleNode().getAssumptions());
+	
+		
+		if(specAnalyser.getNext() != null){
+			visitExprNode(specAnalyser.getNext());
+		}
+
+		if (specAnalyser.getInits() != null) {
+			for (int i = 0; i < specAnalyser.getInits().size(); i++) {
+				visitExprNode(specAnalyser.getInits().get(i));
+			}
+		}
+	
+		if (specAnalyser.getInvariants() != null) {
+			for (int i = 0; i < specAnalyser.getInvariants().size(); i++) {
+				OpDefNode def = specAnalyser.getInvariants().get(i);
+				usedDefinitions.add(def);
+				visitExprNode(def.getBody());
+			}
+		}
+	}
+
+	public HashSet<OpDefNode> getUsedDefinitions(){
+		return usedDefinitions;
+	}
+	
+	@Override
+	public void visitUserDefinedNode(OpApplNode n) {
+		super.visitUserDefinedNode(n);
+		
+		OpDefNode def = (OpDefNode) n.getOperator();
+		ModuleNode moduleNode = def.getSource()
+				.getOriginallyDefinedInModuleNode();
+		if (moduleNode.getName().toString().equals("TLA2B")) {
+			return;
+		}
+		if (BBuiltInOPs.contains(def.getName())
+				&& STANDARD_MODULES.contains(def.getSource()
+						.getOriginallyDefinedInModuleNode().getName()
+						.toString())) {
+			return;
+		}
+		if (usedDefinitions.add(def)) {
+			visitExprNode(def.getBody());
+		}
+
+
+	}
+}