From 05ebcc88ca75605f58cb63c7496aef25be36e492 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Fri, 28 Feb 2020 16:42:01 +0100
Subject: [PATCH] also allow TypeInv as invariant definition
---
src/main/java/de/tla2b/analysis/SpecAnalyser.java | 2 ++
1 file changed, 2 insertions(+)
diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index abaadca..ff52783 100644
--- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java
+++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
@@ -124,6 +124,8 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
specAnalyser.invariants.add(definitions.get("Invariant"));
} else if (definitions.containsKey("Invariants")) {
specAnalyser.invariants.add(definitions.get("Invariants"));
+ } else if (definitions.containsKey("TypeInv")) {
+ specAnalyser.invariants.add(definitions.get("TypeInv"));
}
// TODO are constant in the right order
--
GitLab