From 87f1a9d1abd51cc3e6c2bc69429cce2a43739030 Mon Sep 17 00:00:00 2001 From: Jan Gruteser <jan.gruteser@hhu.de> Date: Mon, 23 Dec 2024 16:44:12 +0100 Subject: [PATCH] add method for constants map --- .../java/de/tla2b/analysis/SpecAnalyser.java | 17 +++++++---------- .../de/tla2b/config/ConfigfileEvaluator.java | 8 ++------ src/main/java/de/tla2b/util/TlaUtils.java | 9 +++++++++ 3 files changed, 18 insertions(+), 16 deletions(-) diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java index d2c5523..648f92e 100644 --- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java +++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java @@ -2,7 +2,6 @@ package de.tla2b.analysis; import de.tla2b.config.ConfigfileEvaluator; import de.tla2b.exceptions.ConfigFileErrorException; -import de.tla2b.exceptions.TLA2BFrontEndException; import de.tla2b.exceptions.NotImplementedException; import de.tla2b.exceptions.SemanticErrorException; import de.tla2b.global.BBuiltInOPs; @@ -11,6 +10,7 @@ import de.tla2b.translation.BDefinitionsFinder; import de.tla2b.translation.OperationsFinder; import de.tla2b.translation.UsedDefinitionsFinder; import de.tla2b.util.DebugUtils; +import de.tla2b.util.TlaUtils; import tla2sany.semantic.*; import tlc2.tool.BuiltInOPs; import tlc2.tool.ToolGlobals; @@ -24,7 +24,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal private List<OpDefNode> invariants = new ArrayList<>(); private OpDefNode expressionOpdefNode; - private final Hashtable<String, SymbolNode> namingHashTable = new Hashtable<>(); + private final Map<String, SymbolNode> namingMap = new HashMap<>(); private final ModuleNode moduleNode; private ExprNode nextExpr; @@ -202,17 +202,14 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal findRecursiveConstructs(); for (OpDeclNode var : moduleNode.getVariableDecls()) { - namingHashTable.put(var.getName().toString(), var); + namingMap.put(var.getName().toString(), var); } DebugUtils.printMsg("Number of variables detected: " + moduleNode.getVariableDecls().length); - for (OpDeclNode con : moduleNode.getConstantDecls()) { - namingHashTable.put(con.getName().toString(), con); - } + + namingMap.putAll(TlaUtils.getConstantsMap(moduleNode.getConstantDecls())); DebugUtils.printMsg("Number of constants detected: " + moduleNode.getConstantDecls().length); - for (OpDefNode def : usedDefinitions) { - namingHashTable.put(def.getName().toString(), def); - } + namingMap.putAll(TlaUtils.getOpDefsMap(usedDefinitions.toArray(new OpDefNode[0]))); } private void evalInit() { @@ -362,7 +359,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal } public SymbolNode getSymbolNodeByName(String name) { - return namingHashTable.get(name); + return namingMap.get(name); } } diff --git a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java b/src/main/java/de/tla2b/config/ConfigfileEvaluator.java index 6d1d487..e866378 100644 --- a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java +++ b/src/main/java/de/tla2b/config/ConfigfileEvaluator.java @@ -56,12 +56,8 @@ public class ConfigfileEvaluator { this.configAst = configAst; this.moduleNode = moduleNode; this.definitions = TlaUtils.getOpDefsMap(moduleNode.getOpDefs()); - - this.constants = new HashMap<>(); - for (OpDeclNode con : moduleNode.getConstantDecls()) { - this.constants.put(con.getName().toString(), con); - this.bConstantList.add(con); - } + this.constants = TlaUtils.getConstantsMap(moduleNode.getConstantDecls()); + this.bConstantList.addAll(constants.values()); this.nextNode = evalPredicate(configAst.getNext(), "next state"); // check if NEXT declaration is a valid definition this.initNode = evalPredicate(configAst.getInit(), "initialisation"); // check if INIT declaration is a valid definition diff --git a/src/main/java/de/tla2b/util/TlaUtils.java b/src/main/java/de/tla2b/util/TlaUtils.java index cf53a4d..44d0275 100644 --- a/src/main/java/de/tla2b/util/TlaUtils.java +++ b/src/main/java/de/tla2b/util/TlaUtils.java @@ -1,5 +1,6 @@ package de.tla2b.util; +import tla2sany.semantic.OpDeclNode; import tla2sany.semantic.OpDefNode; import java.util.HashMap; @@ -7,6 +8,14 @@ import java.util.Map; public class TlaUtils { + public static Map<String, OpDeclNode> getConstantsMap(OpDeclNode[] constantNodes) { + Map<String, OpDeclNode> constants = new HashMap<>(); + for (OpDeclNode con : constantNodes) { + constants.put(con.getName().toString(), con); + } + return constants; + } + public static Map<String, OpDefNode> getOpDefsMap(OpDefNode[] opDefNodes) { Map<String, OpDefNode> definitions = new HashMap<>(); for (OpDefNode def : opDefNodes) { -- GitLab