From 5c16d48e32754ddcee47d9103796f977e8cc2dba Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@cs.uni-duesseldorf.de>
Date: Wed, 25 Sep 2019 15:02:06 +0200
Subject: [PATCH] also support Invariant and Invariants as default
in addition to Inv
---
src/main/java/de/tla2b/analysis/SpecAnalyser.java | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index 5e17ba3..6d04504 100644
--- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java
+++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
@@ -104,6 +104,10 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
specAnalyser.next = definitions.get("Next");
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")) {
+ specAnalyser.invariants.add(definitions.get("Invariants"));
}
// TODO are constant in the right order
--
GitLab