diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index d6b95999760eeba2c58de4f731b04554db89021a..b4045036922b7b4e64094de2e3e3350312cc58a0 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -2,7 +2,6 @@ package de.tla2b.analysis;
import de.tla2b.config.ConfigfileEvaluator;
import de.tla2b.config.TLCValueNode;
-import de.tla2b.config.ValueObj;
import de.tla2b.exceptions.*;
import de.tla2b.global.BBuildIns;
import de.tla2b.global.BBuiltInOPs;
@@ -31,7 +30,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
private List<OpDeclNode> bConstList;
private final SpecAnalyser specAnalyser;
- private Map<OpDeclNode, ValueObj> constantAssignments;
+ private Map<OpDeclNode, TLCValueNode> constantAssignments;
private ConfigfileEvaluator conEval;
diff --git a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java b/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
index d80af5c6fe2d97476cc76808cb98995fe9661e98..22f6dbdbc91615541e1c583aaedb776b48db2c39 100644
--- a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
+++ b/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
@@ -35,9 +35,9 @@ public class ConfigfileEvaluator {
private final List<OpDefNode> invariantNodeList = new ArrayList<>();
private final List<String> enumeratedSet = new ArrayList<>();
private final Map<String, EnumType> enumeratedTypes = new LinkedHashMap<>();
- private final Map<OpDeclNode, ValueObj> constantAssignments = new HashMap<>();
- // k = 1, the ValueObj describes the right side of the assignment and contains its type
- private final Map<OpDefNode, ValueObj> operatorAssignments = new HashMap<>(); // def = 1
+ private final Map<OpDeclNode, TLCValueNode> constantAssignments = new HashMap<>();
+ // k = 1, the ValueNode describes the right side of the assignment and contains its type
+ private final Map<OpDefNode, TLCValueNode> operatorAssignments = new HashMap<>(); // def = 1
private final List<OpDefNode> operatorModelvalues = new ArrayList<>();
@@ -72,8 +72,12 @@ public class ConfigfileEvaluator {
evalInvariants(); // check if INVARIANT declarations are valid definitions
evalConstantOrDefOverrides();
- evalConstantOrOperatorAssignments();
- evalModConOrDefAssignments();
+ try {
+ evalConstantOrOperatorAssignments();
+ evalModConOrDefAssignments();
+ } catch (AbortException e) {
+ throw new RuntimeException(e);
+ }
evalModConOrDefOverrides();
}
@@ -151,7 +155,7 @@ public class ConfigfileEvaluator {
}
}
- private void evalConstantOrOperatorAssignments() throws ConfigFileErrorException {
+ private void evalConstantOrOperatorAssignments() throws ConfigFileErrorException, AbortException {
Vect<?> configCons = configAst.getConstants();
// iterate over all constant or operator assignments in the config file
// k = 1 or def = 1
@@ -162,7 +166,7 @@ public class ConfigfileEvaluator {
TLAType symbolType = conGetType(symbol.lastElement());
if (constants.containsKey(symbolName)) {
OpDeclNode c = constants.get(symbolName);
- constantAssignments.put(c, new ValueObj(symbolValue, symbolType));
+ constantAssignments.put(c, new TLCValueNode(symbolValue, symbolType, null));
// if conValue is a model value and the name of the value is the
// same as the name of constants, then the constant declaration
// in the resulting B machine disappears
@@ -171,7 +175,7 @@ public class ConfigfileEvaluator {
}
} else if (definitions.containsKey(symbolName)) {
OpDefNode def = definitions.get(symbolName);
- operatorAssignments.put(def, new ValueObj(symbolValue, symbolType));
+ operatorAssignments.put(def, new TLCValueNode(symbolValue, symbolType, def.getBody().getTreeNode()));
if (symbolType instanceof SetType && ((SetType) symbolType).getSubType() instanceof EnumType) {
operatorModelvalues.add(def);
@@ -185,7 +189,7 @@ public class ConfigfileEvaluator {
}
}
- private void evalModConOrDefAssignments() throws ConfigFileErrorException {
+ private void evalModConOrDefAssignments() throws ConfigFileErrorException, AbortException {
// TODO: seems like there are no tests for this
// example: val = [Counter] 7
@SuppressWarnings("unchecked")
@@ -201,12 +205,11 @@ public class ConfigfileEvaluator {
Value symbolValue = (Value) assignment.elementAt(1);
TLAType symbolType = conGetType(symbolValue);
- ValueObj valueObj = new ValueObj(symbolValue, symbolType);
if (opDefOrDeclNode instanceof OpDeclNode) {
// TODO test whether c is a extended constant
// Instanced constants must be overridden in the instance statement
OpDeclNode c = (OpDeclNode) opDefOrDeclNode;
- constantAssignments.put(c, valueObj);
+ constantAssignments.put(c, new TLCValueNode(symbolValue, symbolType, c.getTreeNode()));
// if conValue is a model value and the name of value is the same as the name of constants,
// then the constant declaration in the resulting B machine disappears
String symbolName = opDefOrDeclNode.getName().toString();
@@ -215,7 +218,7 @@ public class ConfigfileEvaluator {
}
} else {
OpDefNode def = (OpDefNode) opDefOrDeclNode;
- operatorAssignments.put(def, valueObj);
+ operatorAssignments.put(def, new TLCValueNode(symbolValue, symbolType, def.getBody().getTreeNode()));
if (symbolType instanceof SetType) {
if (((SetType) symbolType).getSubType() instanceof EnumType) {
@@ -415,11 +418,11 @@ public class ConfigfileEvaluator {
return this.invariantNodeList;
}
- public Map<OpDeclNode, ValueObj> getConstantAssignments() {
+ public Map<OpDeclNode, TLCValueNode> getConstantAssignments() {
return this.constantAssignments;
}
- public Map<OpDefNode, ValueObj> getOperatorAssignments() {
+ public Map<OpDefNode, TLCValueNode> getOperatorAssignments() {
return this.operatorAssignments;
}
diff --git a/src/main/java/de/tla2b/config/ModuleOverrider.java b/src/main/java/de/tla2b/config/ModuleOverrider.java
index 123230d196aabdd036582c382fbe0be12dce7e34..4fa75efadb6bb329971f40331069e778a064bf00 100644
--- a/src/main/java/de/tla2b/config/ModuleOverrider.java
+++ b/src/main/java/de/tla2b/config/ModuleOverrider.java
@@ -10,7 +10,7 @@ public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
private final ModuleNode moduleNode;
private final Map<OpDeclNode, OpDefNode> constantOverrideTable;
private final Map<OpDefNode, OpDefNode> operatorOverrideTable;
- private final Map<OpDefNode, ValueObj> operatorAssignments;
+ private final Map<OpDefNode, TLCValueNode> operatorAssignments;
private ModuleOverrider(ModuleNode moduleNode, ConfigfileEvaluator conEval) {
this.moduleNode = moduleNode;
@@ -27,23 +27,9 @@ public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
OpDefNode[] defs = moduleNode.getOpDefs();
for (OpDefNode def : defs) {
if (operatorAssignments.containsKey(def)) {
- ExprNode oldExpr = def.getBody();
- TLCValueNode valueNode;
- try {
- valueNode = new TLCValueNode(operatorAssignments.get(def), oldExpr.getTreeNode());
- } catch (AbortException e) {
- throw new RuntimeException();
- }
- def.setBody(valueNode);
+ def.setBody(operatorAssignments.get(def));
} else if (operatorAssignments.containsKey(def.getSource())) {
- ExprNode oldExpr = def.getBody();
- TLCValueNode valueNode;
- try {
- valueNode = new TLCValueNode(operatorAssignments.get(def.getSource()), oldExpr.getTreeNode());
- } catch (AbortException e) {
- throw new RuntimeException();
- }
- def.setBody(valueNode);
+ def.setBody(operatorAssignments.get(def.getSource()));
}
}
diff --git a/src/main/java/de/tla2b/config/TLCValueNode.java b/src/main/java/de/tla2b/config/TLCValueNode.java
index 329d2c513863984abfdca53eedfc041f91b5cdd6..3a5515c11f5e69cece4e210aeb26f41790a6197f 100644
--- a/src/main/java/de/tla2b/config/TLCValueNode.java
+++ b/src/main/java/de/tla2b/config/TLCValueNode.java
@@ -12,10 +12,10 @@ public class TLCValueNode extends NumeralNode implements TranslationGlobals {
private final Value value;
private final TLAType type;
- public TLCValueNode(ValueObj valObj, TreeNode stn) throws AbortException {
+ public TLCValueNode(Value value, TLAType type, TreeNode stn) throws AbortException {
super("1337", stn);
- this.value = valObj.getValue();
- this.type = valObj.getType();
+ this.value = value;
+ this.type = type;
}
public String toString2() {
diff --git a/src/main/java/de/tla2b/config/ValueObj.java b/src/main/java/de/tla2b/config/ValueObj.java
deleted file mode 100644
index b649f7348c4f49d1c8ddb2877ca88a653d3179f0..0000000000000000000000000000000000000000
--- a/src/main/java/de/tla2b/config/ValueObj.java
+++ /dev/null
@@ -1,22 +0,0 @@
-package de.tla2b.config;
-
-import de.tla2b.types.TLAType;
-import tlc2.value.impl.Value;
-
-public class ValueObj {
- private final Value value;
- private final TLAType type;
-
- public ValueObj(Value value, TLAType t) {
- this.value = value;
- this.type = t;
- }
-
- public Value getValue() {
- return value;
- }
-
- public TLAType getType() {
- return type;
- }
-}
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 5356fce79f3ed0705bcac0b6f51af4abe62292c9..96df6c1cf117b958914af8a2dabed14197773f91 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -9,7 +9,7 @@ import de.tla2b.analysis.*;
import de.tla2b.analysis.PredicateVsExpression.DefinitionType;
import de.tla2b.analysis.UsedExternalFunctions.EXTERNAL_FUNCTIONS;
import de.tla2b.config.ConfigfileEvaluator;
-import de.tla2b.config.ValueObj;
+import de.tla2b.config.TLCValueNode;
import de.tla2b.exceptions.NotImplementedException;
import de.tla2b.global.*;
import de.tla2b.translation.BMacroHandler;
@@ -333,7 +333,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, BBuil
propertiesList.addAll(evalRecursiveFunctions());
for (OpDeclNode con : bConstants) {
if (conEval != null && conEval.getConstantAssignments().containsKey(con) && bConstants.contains(con)) {
- ValueObj v = conEval.getConstantAssignments().get(con);
+ TLCValueNode v = conEval.getConstantAssignments().get(con);
TLAType t = v.getType();
AEqualPredicate equal = new AEqualPredicate();