From 7dd036ec1ca215d17e72d47e6447c619383f91eb Mon Sep 17 00:00:00 2001 From: Michael Leuschel <leuschel@uni-duesseldorf.de> Date: Thu, 12 Sep 2024 11:37:22 +0200 Subject: [PATCH] start using verbose command-line flag Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de> --- src/main/java/de/tla2b/TLA2B.java | 4 ++- .../java/de/tla2b/analysis/SpecAnalyser.java | 29 +++++++++---------- src/main/java/de/tla2b/util/DebugUtils.java | 21 ++++++++++++++ 3 files changed, 37 insertions(+), 17 deletions(-) create mode 100644 src/main/java/de/tla2b/util/DebugUtils.java diff --git a/src/main/java/de/tla2b/TLA2B.java b/src/main/java/de/tla2b/TLA2B.java index b41976d..64d28f8 100644 --- a/src/main/java/de/tla2b/TLA2B.java +++ b/src/main/java/de/tla2b/TLA2B.java @@ -6,6 +6,7 @@ import de.tla2b.exceptions.TLA2BException; import de.tla2b.global.TranslationGlobals; import de.tla2bAst.Translator; import org.apache.commons.cli.*; +import de.tla2b.util.DebugUtils; public class TLA2B implements TranslationGlobals { public final static String VERSION = "version"; @@ -25,6 +26,7 @@ public class TLA2B implements TranslationGlobals { try { CommandLine line = parser.parse(options, args); String[] remainingArgs = line.getArgs(); + DebugUtils.setDebugMode(line.hasOption(VERBOSE)); if (line.hasOption(VERSION)) { System.out.println("TLA2B version: " + VERSION_NUMBER); } @@ -77,7 +79,7 @@ public class TLA2B implements TranslationGlobals { private static Options getCommandlineOptions() { Options options = new Options(); options.addOption(VERSION, false, "prints the current version of TLA2B"); - options.addOption(VERBOSE, false, "makes output more verbose (not used yet)"); + options.addOption(VERBOSE, false, "makes output more verbose"); Option config = Option.builder("config") .argName("file") diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java index d2468c3..82103bb 100644 --- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java +++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java @@ -10,6 +10,7 @@ import de.tla2b.global.TranslationGlobals; import de.tla2b.translation.BDefinitionsFinder; import de.tla2b.translation.OperationsFinder; import de.tla2b.translation.UsedDefinitionsFinder; +import de.tla2b.util.DebugUtils; import tla2sany.semantic.*; import tlc2.tool.BuiltInOPs; import tlc2.tool.ToolGlobals; @@ -143,6 +144,8 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal } else if (definitions.containsKey("IndInv")) { specAnalyser.invariants.add(definitions.get("IndInv")); ClausefDetected("IndInv", "INVARIANTS"); + } else { + System.out.println("No default Invariant detected"); } // TODO are constant in the right order @@ -152,13 +155,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal } public static void ClausefDetected(String Name, String Clause) { - // TODO: use -verbose OPTION from command line - System.out.println("Detected TLA+ Default Definition " + Name + " for Clause: " + Clause); - } - - public static void DebugMsg(String Msg) { - // TODO: use -verbose OPTION from command line - System.out.println(Msg); + DebugUtils.printMsg("Detected TLA+ Default Definition " + Name + " for Clause: " + Clause); } public void start() @@ -180,17 +177,17 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal if (opDefNode.getKind() == UserDefinedOpKind && !BBuiltInOPs.contains(opDefNode.getName())) { int i = invariants.indexOf(inv); invariants.set(i, opDefNode); - DebugMsg("Adding invariant " + i); + DebugUtils.printDebugMsg("Adding invariant " + i); } } catch (ClassCastException e) { } } - DebugMsg("Detecting OPERATIONS from disjunctions"); + DebugUtils.printDebugMsg("Detecting OPERATIONS from disjunctions"); OperationsFinder operationsFinder = new OperationsFinder(this); bOperations = operationsFinder.getBOperations(); - DebugMsg("Finding used definitions"); + DebugUtils.printDebugMsg("Finding used definitions"); UsedDefinitionsFinder definitionFinder = new UsedDefinitionsFinder(this); this.usedDefinitions = definitionFinder.getUsedDefinitions(); @@ -198,7 +195,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal this.bDefinitionsSet = bDefinitionFinder.getBDefinitionsSet(); // usedDefinitions.addAll(bDefinitionsSet); - DebugMsg("Computing variable declarations"); + DebugUtils.printDebugMsg("Computing variable declarations"); // test whether there is an init predicate if there is a variable if (moduleNode.getVariableDecls().length > 0 && inits == null) { throw new SemanticErrorException("No initial predicate is defined."); @@ -216,11 +213,11 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal for (OpDeclNode var : moduleNode.getVariableDecls()) { namingHashTable.put(var.getName().toString(), var); } - DebugMsg("Number of variables detected: " + moduleNode.getVariableDecls().length); + DebugUtils.printMsg("Number of variables detected: " + moduleNode.getVariableDecls().length); for (OpDeclNode con : moduleNode.getConstantDecls()) { namingHashTable.put(con.getName().toString(), con); } - DebugMsg("Number of constants detected: " + moduleNode.getConstantDecls().length); + DebugUtils.printMsg("Number of constants detected: " + moduleNode.getConstantDecls().length); for (OpDefNode def : usedDefinitions) { namingHashTable.put(def.getName().toString(), def); } @@ -229,21 +226,21 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal private void evalInit() { if (init != null) { - System.out.println("Using TLA+ Init definition to determine B INITIALISATION"); + DebugUtils.printMsg("Using TLA+ Init definition to determine B INITIALISATION"); inits.add(init.getBody()); } } private void evalNext() { if (next != null) { - System.out.println("Using TLA+ Next definition to determine B OPERATIONS"); + DebugUtils.printMsg("Using TLA+ Next definition to determine B OPERATIONS"); this.nextExpr = next.getBody(); } } public void evalSpec() throws SemanticErrorException { if (spec != null) { - System.out.println("Using TLA+ Spec to determine B INITIALISATION and OPERATIONS"); + DebugUtils.printMsg("Using TLA+ Spec to determine B INITIALISATION and OPERATIONS"); processConfigSpec(spec.getBody()); } diff --git a/src/main/java/de/tla2b/util/DebugUtils.java b/src/main/java/de/tla2b/util/DebugUtils.java new file mode 100644 index 0000000..4818ecf --- /dev/null +++ b/src/main/java/de/tla2b/util/DebugUtils.java @@ -0,0 +1,21 @@ +package de.tla2b.util; + +public class DebugUtils { + private static boolean debugOn; + + public static void setDebugMode(boolean newDebugOn) { + debugOn = newDebugOn; + } + + public static void printDebugMsg(String Msg) { + if(debugOn) { + System.out.println(Msg); + } + } + + public static void printMsg(String Msg) { + // TODO: turn off using silent flag + System.out.println(Msg); + } + +} -- GitLab