Collecting all B definitions to make the recursive machine loader happy

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

@@ -105,6 +105,7 @@ import de.be4.classicalb.core.parser.node.AStringExpression;
 import de.be4.classicalb.core.parser.node.AStringSetExpression;
 import de.be4.classicalb.core.parser.node.AStructExpression;
 import de.be4.classicalb.core.parser.node.ASubsetPredicate;
+import de.be4.classicalb.core.parser.node.ASubstitutionDefinitionDefinition;
 import de.be4.classicalb.core.parser.node.ATailExpression;
 import de.be4.classicalb.core.parser.node.ATotalFunctionExpression;
 import de.be4.classicalb.core.parser.node.AUnaryMinusExpression;
@@ -271,16 +272,11 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 			}
 
 		}
-		Set<EXTERNAL_FUNCTIONS> set = usedExternalFunctions
-				.getUsedExternalFunctions();
-
-		if (bDefs.size() == 0 && set.size() == 0) {
-			return;
-		}
 
-		ADefinitionsMachineClause defClause = new ADefinitionsMachineClause();
 		List<PDefinition> defs = new ArrayList<PDefinition>();
 
+		Set<EXTERNAL_FUNCTIONS> set = usedExternalFunctions
+				.getUsedExternalFunctions();
 		defs.addAll(createDefinitionsForExternalFunctions(set));
 
 		for (OpDefNode opDefNode : bDefs) {
@@ -299,7 +295,6 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 				d.setParameters(list);
 				d.setRhs(visitExprNodePredicate(opDefNode.getBody()));
 				defs.add(d);
-				bDefinitions.addDefinition(d, Definitions.Type.Expression);
 			} else {
 				AExpressionDefinitionDefinition d = new AExpressionDefinitionDefinition();
 				d.setName(new TIdentifierLiteral(opDefNode.getName().toString()));
@@ -307,12 +302,31 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 				d.setParameters(list);
 				d.setRhs(visitExprNodeExpression(opDefNode.getBody()));
 				defs.add(d);
-				bDefinitions.addDefinition(d, Definitions.Type.Expression);
 			}
 
 		}
+
+		if (defs.size() > 0) {
+			ADefinitionsMachineClause defClause = new ADefinitionsMachineClause();
 			defClause.setDefinitions(defs);
 			machineClauseList.add(defClause);
+			for (PDefinition def : defs) {
+				if (def instanceof AExpressionDefinitionDefinition) {
+					bDefinitions.addDefinition(
+							(AExpressionDefinitionDefinition) def,
+							Definitions.Type.Expression);
+				} else if (def instanceof APredicateDefinitionDefinition) {
+					bDefinitions.addDefinition(
+							(APredicateDefinitionDefinition) def,
+							Definitions.Type.Predicate);
+				} else {
+					bDefinitions.addDefinition(
+							(ASubstitutionDefinitionDefinition) def,
+							Definitions.Type.Substitution);
+				}
+			}
+		}
+
 	}
 
 	private ArrayList<PDefinition> createDefinitionsForExternalFunctions(

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

@@ -210,7 +210,6 @@ public class Translator {
 				specAnalyser, usedExternalFunctions, predicateVsExpression);
 
 		this.bDefinitions = bAstCreator.getBDefinitions();
-
 		return bAstCreator.getStartNode();
 	}
 

src/test/java/de/tla2b/examples/MCTest.java

@@ -55,6 +55,7 @@ public class MCTest {
 		runModule(file);
 	}
 	
+	
 	@Test
 	public void testChannel() throws Exception {
 		String file = "src/test/resources/examples/Channel/Channel.tla";