add test to ensure that the GOAL definition is translated

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

@@ -15,16 +15,13 @@ import de.tla2b.analysis.BOperation;
 import de.tla2b.analysis.SpecAnalyser;
 import de.tla2b.global.TranslationGlobals;
 
-public class BDefinitionsFinder extends AbstractASTVisitor implements
-		ASTConstants, ToolGlobals, TranslationGlobals {
-	private final HashSet<OpDefNode> bDefinitionsSet = new HashSet<OpDefNode>();
+public class BDefinitionsFinder extends AbstractASTVisitor implements ASTConstants, ToolGlobals, TranslationGlobals {
+	private final HashSet<OpDefNode> bDefinitionsSet = new HashSet<>();
 
 	public BDefinitionsFinder(SpecAnalyser specAnalyser) {
 		if (specAnalyser.getConfigFileEvaluator() != null) {
-			bDefinitionsSet.addAll(specAnalyser.getConfigFileEvaluator()
-					.getConstantOverrideTable().values());
-			bDefinitionsSet.addAll(specAnalyser.getConfigFileEvaluator()
-					.getOperatorOverrideTable().values());
+			bDefinitionsSet.addAll(specAnalyser.getConfigFileEvaluator().getConstantOverrideTable().values());
+			bDefinitionsSet.addAll(specAnalyser.getConfigFileEvaluator().getOperatorOverrideTable().values());
 		}
 
 		for (BOperation op : specAnalyser.getBOperations()) {
@@ -52,10 +49,19 @@ public class BDefinitionsFinder extends AbstractASTVisitor implements
 			bDefinitionsSet.add(def);
 		}
 
-		HashSet<OpDefNode> temp = new HashSet<OpDefNode>(bDefinitionsSet);
+		HashSet<OpDefNode> temp = new HashSet<>(bDefinitionsSet);
 		for (OpDefNode opDefNode : temp) {
 			visitExprNode(opDefNode.getBody());
 		}
+
+		for (OpDefNode opDef : specAnalyser.getModuleNode().getOpDefs()) {
+			String defName = opDef.getName().toString();
+			// GOAL, ANIMATION_FUNCTION, ANIMATION_IMGxx, SET_PREF_xxx,
+			if (defName.equals("GOAL") || defName.startsWith("ANIMATION_FUNCTION")
+					|| defName.startsWith("ANIMATION_IMG") || defName.startsWith("SET_PREF_")) {
+				bDefinitionsSet.add(opDef);
+			}
+		}
 	}
 
 	public void visitUserDefinedNode(OpApplNode n) {

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

@@ -33,4 +33,22 @@ public class DefinitionsTest {
 				+ "END";
 		compare(expected, module);
 	}
+	
+	@Test
+	public void testGoalDefinition() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "EXTENDS Naturals \n"
+				+ "VARIABLES x, y \n"
+				+ "Init == x = 1 /\\ y = 1 \n"
+				+ "GOAL == 1=1 \n"
+				+ "=================================";
+		
+		final String expected = "MACHINE Testing\n"
+				+ "DEFINITIONS GOAL == 1 = 1;"
+				+ "VARIABLES x, y\n"
+				+ "INVARIANT x : INTEGER & y : INTEGER \n"
+				+ "INITIALISATION  x, y:(x = 1 & y = 1) \n"
+				+ "END";
+		compare(expected, module);
+	}
 }