Skip to content
Snippets Groups Projects
Commit 87f1a9d1 authored by Jan Gruteser's avatar Jan Gruteser
Browse files

add method for constants map

parent ee1b879b
No related branches found
No related tags found
No related merge requests found
Pipeline #148354 passed
......@@ -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);
}
}
......@@ -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
......
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) {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment