diff --git a/src/main/java/de/tla2b/analysis/InstanceTransformation.java b/src/main/java/de/tla2b/analysis/InstanceTransformation.java index e26cb2c0f0d6e4af9b627402e11b738fd9ca94a2..d2b8e6092f39ea833b02cf8f300e59c88a9500dc 100644 --- a/src/main/java/de/tla2b/analysis/InstanceTransformation.java +++ b/src/main/java/de/tla2b/analysis/InstanceTransformation.java @@ -1,6 +1,7 @@ package de.tla2b.analysis; import de.tla2b.global.BBuiltInOPs; +import de.tla2b.util.TlaUtils; import tla2sany.semantic.*; import tlc2.tool.BuiltInOPs; import util.UniqueString; @@ -25,7 +26,7 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants { private InstanceTransformation(ModuleNode moduleNode) { this.defs = moduleNode.getOpDefs(); - this.defsHash = SymbolSorter.getDefsMap(defs); + this.defsHash = TlaUtils.getOpDefsMap(defs); } public static void run(ModuleNode moduleNode) { diff --git a/src/main/java/de/tla2b/analysis/SymbolSorter.java b/src/main/java/de/tla2b/analysis/SymbolSorter.java index db0def3155deaff623d0de76976f88ed912228bf..234ec55312d167b0d7b419a86b90f68fccc536e2 100644 --- a/src/main/java/de/tla2b/analysis/SymbolSorter.java +++ b/src/main/java/de/tla2b/analysis/SymbolSorter.java @@ -6,8 +6,6 @@ import tla2sany.semantic.OpDefNode; import java.util.Arrays; import java.util.Comparator; -import java.util.HashMap; -import java.util.Map; public class SymbolSorter { @@ -27,22 +25,6 @@ public class SymbolSorter { public static void sortOpDefNodes(OpDefNode[] opDefNodes) { Arrays.sort(opDefNodes, new OpDefNodeComparator()); } - - public static Map<String, OpDefNode> getDefsMap(OpDefNode[] opDefNodes) { - Map<String, OpDefNode> definitions = new HashMap<>(); - for (OpDefNode def : opDefNodes) { - // Definition in this module -// if (StandardModules.contains(def.getOriginallyDefinedInModuleNode() -// .getName().toString()) -// || StandardModules.contains(def.getSource() -// .getOriginallyDefinedInModuleNode().getName() -// .toString())) { -// continue; -// } - definitions.put(def.getName().toString(), def); - } - return definitions; - } } class OpDeclNodeComparator implements Comparator<OpDeclNode> { diff --git a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java b/src/main/java/de/tla2b/config/ConfigfileEvaluator.java index aa02a99d16b85952a920b0a6769591c69b33cf80..73e9bbf21a3c217ac4cc86c1b8a0a478d89698cc 100644 --- a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java +++ b/src/main/java/de/tla2b/config/ConfigfileEvaluator.java @@ -3,6 +3,7 @@ package de.tla2b.config; import de.tla2b.exceptions.ConfigFileErrorException; import de.tla2b.exceptions.UnificationException; import de.tla2b.types.*; +import de.tla2b.util.TlaUtils; import tla2sany.semantic.*; import tlc2.tool.impl.ModelConfig; import tlc2.util.Vect; @@ -57,12 +58,7 @@ public class ConfigfileEvaluator { public ConfigfileEvaluator(ModelConfig configAst, ModuleNode moduleNode) { this.configAst = configAst; this.moduleNode = moduleNode; - - definitions = new HashMap<>(); - OpDefNode[] defs = moduleNode.getOpDefs(); - for (OpDefNode def : defs) { - definitions.put(def.getName().toString(), def); - } + this.definitions = TlaUtils.getOpDefsMap(moduleNode.getOpDefs()); constants = new HashMap<>(); OpDeclNode[] cons = moduleNode.getConstantDecls();