From ce528b848d8d27963883f9fe6c2658dc2fe85701 Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Fri, 20 Dec 2024 08:59:59 +0100
Subject: [PATCH] =?UTF-8?q?don=E2=80=99t=20ignore=20MC=20definitions=20if?=
=?UTF-8?q?=20they=20are=20used?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
fixes public_examples/TLA/book-specs/AddSeq.toolbox/AddSeq_implements_Add/MC.tla
---
src/main/java/de/tla2bAst/BAstCreator.java | 6 +++++-
1 file changed, 5 insertions(+), 1 deletion(-)
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 95a92df..50ac77d 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -186,7 +186,11 @@ public class BAstCreator extends BuiltInOPs
DebugUtils.printVeryVerboseMsg("Not creating B DEFINITION (in Override Table) " + def.getName() + " " + def);
continue;
}
- if (def.getOriginallyDefinedInModuleNode().getName().toString().equals("MC")) {
+ if (def.getOriginallyDefinedInModuleNode().getName().toString().equals("MC")
+ && !specAnalyser.getUsedDefinitions().contains(def)) {
+ // don't skip MC definitions if they are used
+ // TODO: check if this is correct (see invariant check for MC below)
+ DebugUtils.printDebugMsg("Skipping MC definition: " + def.getName());
continue;
}
//debugUtils.printVeryVerboseMsg("Creating B DEFINITION " + def.getName() + " " + def);
--
GitLab