From 00cf8d22dda46ae2577340f2c0e7027370cbc1b3 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Fri, 28 Feb 2020 16:32:28 +0100
Subject: [PATCH] allow a few more variations of Init, Spec and Next

---
 .../java/de/tla2b/analysis/SpecAnalyser.java  | 26 ++++++++++++++++---
 1 file changed, 23 insertions(+), 3 deletions(-)

diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index 73b9a01..abaadca 100644
--- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java
+++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
@@ -95,11 +95,31 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
 		for (int i = 0; i < m.getOpDefs().length; i++) {
 			definitions.put(m.getOpDefs()[i].getName().toString(), m.getOpDefs()[i]);
 		}
-		specAnalyser.spec = definitions.get("Spec");
-		specAnalyser.init = definitions.get("Init");
-		specAnalyser.next = definitions.get("Next");
+		
+		if (definitions.containsKey("Spec")) {
+			specAnalyser.spec = definitions.get("Spec");
+		} else if (definitions.containsKey("SPEC")) {
+			specAnalyser.spec = definitions.get("SPEC");
+		}
+		
+		if (definitions.containsKey("Init")) {
+			specAnalyser.init = definitions.get("Init");
+		} else if (definitions.containsKey("INIT")) {
+			specAnalyser.init = definitions.get("INIT");
+		} else if (definitions.containsKey("Initialisation")) {
+			specAnalyser.init = definitions.get("Initialisation");
+		}
+		
+		if (definitions.containsKey("Next")) {
+			specAnalyser.next = definitions.get("Next");
+		} else if (definitions.containsKey("NEXT")) {
+			specAnalyser.next = definitions.get("NEXT");
+		}
+		
 		if (definitions.containsKey("Inv")) {
 			specAnalyser.invariants.add(definitions.get("Inv"));
+		} else if (definitions.containsKey("INV")) {
+			specAnalyser.invariants.add(definitions.get("INV"));
 		} else if (definitions.containsKey("Invariant")) {
 			specAnalyser.invariants.add(definitions.get("Invariant"));
 		} else if (definitions.containsKey("Invariants")) {
-- 
GitLab