From 3a236f558ea5b2cc13853a888c4dfed85a306bf7 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Fri, 28 Feb 2020 16:42:14 +0100
Subject: [PATCH] throw exception when no Init found
---
src/main/java/de/tla2bAst/BAstCreator.java | 3 +++
1 file changed, 3 insertions(+)
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index df56ca7..8fd68c5 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);
--
GitLab