From 8c37649ddab27b20cd4e5cd75b25d14415782e78 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Thu, 12 Sep 2024 11:45:26 +0200
Subject: [PATCH] more uses of the verbose flag
Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
.../java/de/tla2b/translation/UsedDefinitionsFinder.java | 3 +++
src/main/java/de/tla2b/util/DebugUtils.java | 5 +++++
src/main/java/de/tla2bAst/BAstCreator.java | 5 +++++
3 files changed, 13 insertions(+)
diff --git a/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java b/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java
index 61609f6..c1ba55c 100644
--- a/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java
+++ b/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java
@@ -5,6 +5,7 @@ import de.tla2b.analysis.AbstractASTVisitor;
import de.tla2b.analysis.SpecAnalyser;
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.TranslationGlobals;
+import de.tla2b.util.DebugUtils;
import tla2sany.semantic.ASTConstants;
import tla2sany.semantic.ModuleNode;
import tla2sany.semantic.OpApplNode;
@@ -60,7 +61,9 @@ public class UsedDefinitionsFinder extends AbstractASTVisitor implements ASTCons
for (OpDefNode opDef : specAnalyser.getModuleNode().getOpDefs()) {
String defName = opDef.getName().toString();
// GOAL, ANIMATION_FUNCTION, ANIMATION_IMGxx, SET_PREF_xxx, etc.
+ // DebugUtils.printDebugMsg("Checking definition: " + defName);
if (Utils.isProBSpecialDefinitionName(defName)) {
+ DebugUtils.printMsg("ProB special definition: " + defName);
usedDefinitions.add(opDef);
}
}
diff --git a/src/main/java/de/tla2b/util/DebugUtils.java b/src/main/java/de/tla2b/util/DebugUtils.java
index 4818ecf..7f78432 100644
--- a/src/main/java/de/tla2b/util/DebugUtils.java
+++ b/src/main/java/de/tla2b/util/DebugUtils.java
@@ -7,6 +7,11 @@ public class DebugUtils {
debugOn = newDebugOn;
}
+ public static void printVeryVerboseMsg(String Msg) {
+ // TODO: turn on using -vv flag
+ // System.out.println(Msg);
+ }
+
public static void printDebugMsg(String Msg) {
if(debugOn) {
System.out.println(Msg);
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 9346e3a..f1edcd5 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -14,6 +14,7 @@ import de.tla2b.global.*;
import de.tla2b.translation.BMacroHandler;
import de.tla2b.translation.RecursiveFunctionHandler;
import de.tla2b.types.*;
+import de.tla2b.util.DebugUtils;
import tla2sany.semantic.*;
import tla2sany.st.Location;
import tlc2.tool.BuiltInOPs;
@@ -178,13 +179,17 @@ public class BAstCreator extends BuiltInOPs
OpDefNode def = moduleNode.getOpDefs()[i];
if (specAnalyser.getBDefinitions().contains(def)) {
if (conEval != null && conEval.getConstantOverrideTable().containsValue(def)) {
+ DebugUtils.printVeryVerboseMsg("Not creating B DEFINITION (in Override Table) " + def.getName() + " " + def);
continue;
}
if (def.getOriginallyDefinedInModuleNode().getName().toString().equals("MC")) {
continue;
}
+ //debugUtils.printVeryVerboseMsg("Creating B DEFINITION " + def.getName() + " " + def);
bDefs.add(def);
+ } else {
+ DebugUtils.printVeryVerboseMsg("Not creating unused B DEFINITION for " + def.getName() + " " + def);
}
}
--
GitLab