diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index df56ca78ed9a5a59304c8fd8a1a9eda9660311ee..8fd68c51165e6f64439e3c02abda855ebdef76cd 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -348,6 +348,9 @@ public class BAstCreator extends BuiltInOPs
 		for (ExprNode node : specAnalyser.getInits()) {
 			predList.add(visitExprNodePredicate(node));
 		}
+		if (predList.isEmpty()) {
+			throw new NotImplementedException("Could not find a definition of Init.");
+		}
 		becomes.setPredicate(createConjunction(predList));
 		AInitialisationMachineClause initClause = new AInitialisationMachineClause(becomes);
 		machineClauseList.add(initClause);