diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index ff2ca246ed57b8709bf958f350831fb88b3bbb0d..1c46459315e57e11436969774b2764af6ab2ade3 100644
--- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java
+++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
@@ -41,6 +41,10 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
private OpDefNode next;
private ArrayList<OpDefNode> invariants = new ArrayList<OpDefNode>();
+ private OpDefNode expressionOpdefNode;
+ private Hashtable<String, SymbolNode> namingHashTable = new Hashtable<String, SymbolNode>();
+
+
private final ModuleNode moduleNode;
private ExprNode nextExpr;
@@ -85,11 +89,13 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
}
+
public static SpecAnalyser createSpecAnalyserForTlaExpression(ModuleNode m){
SpecAnalyser specAnalyser = new SpecAnalyser(m);
- OpDefNode expr = m.getOpDefs()[m.getOpDefs().length-1];
- specAnalyser.usedDefinitions.add(expr);
- specAnalyser.bDefinitionsSet.add(expr);
+
+ specAnalyser.expressionOpdefNode = m.getOpDefs()[m.getOpDefs().length-1];
+ specAnalyser.usedDefinitions.add(specAnalyser.expressionOpdefNode);
+ specAnalyser.bDefinitionsSet.add(specAnalyser.expressionOpdefNode);
return specAnalyser;
}
@@ -161,6 +167,19 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
}
}
findRecursiveConstructs();
+
+
+
+ for (OpDeclNode var : moduleNode.getVariableDecls()) {
+ namingHashTable.put(var.getName().toString(), var);
+ }
+ for (OpDeclNode con : moduleNode.getConstantDecls()) {
+ namingHashTable.put(con.getName().toString(), con);
+ }
+ for (OpDefNode def : usedDefinitions) {
+ namingHashTable.put(def.getName().toString(), def);
+ }
+
}
private void evalInit() {
@@ -309,4 +328,12 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
return init;
}
+ public OpDefNode getExpressionOpdefNode(){
+ return expressionOpdefNode;
+ }
+
+ public SymbolNode getSymbolNodeByName(String name){
+ return namingHashTable.get(name);
+ }
+
}
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index b468d57ba7ca3e6705c7eeaa1015522ee58c9339..1a5ac15125014e0d0f39d01c19e6d3bab2f29766 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -54,7 +54,8 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
// every record node [a |-> 1 .. ] will be added to this List
private ModuleNode moduleNode;
private ArrayList<OpDeclNode> bConstList;
-
+ private SpecAnalyser specAnalyser;
+
private Hashtable<OpDeclNode, ValueObj> constantAssignments;
private ConfigfileEvaluator conEval;
@@ -67,6 +68,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
public TypeChecker(ModuleNode moduleNode, ConfigfileEvaluator conEval,
SpecAnalyser specAnalyser) {
this.moduleNode = moduleNode;
+ this.specAnalyser= specAnalyser;
if (conEval != null) {
this.bConstList = conEval.getbConstantList();
this.constantAssignments = conEval.getConstantAssignments();
@@ -79,9 +81,9 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
paramId = TYPE_ID;
}
- public TypeChecker(ModuleNode moduleNode) {
+ public TypeChecker(ModuleNode moduleNode, SpecAnalyser specAnalyser) {
this.moduleNode = moduleNode;
-
+ this.specAnalyser = specAnalyser;
Set<OpDefNode> usedDefinitions = new HashSet<OpDefNode>();
OpDefNode[] defs = moduleNode.getOpDefs();
// used the last definition of the module
@@ -229,7 +231,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
* @param def
* @throws TLA2BException
*/
- private void visitOpDefNode(OpDefNode def) throws TLA2BException {
+ public void visitOpDefNode(OpDefNode def) throws TLA2BException {
FormalParamNode[] params = def.getParams();
for (int i = 0; i < params.length; i++) {
FormalParamNode p = params[i];
@@ -386,7 +388,15 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
String vName = symbolNode.getName().toString();
TLAType v = (TLAType) symbolNode.getToolObject(TYPE_ID);
if (v == null) {
- throw new RuntimeException(vName + " has no type yet!");
+ SymbolNode var = this.specAnalyser.getSymbolNodeByName(vName);
+ if(var != null){
+ // symbolNode is variable of an expression, e.g. v + 1
+ v = (TLAType) var.getToolObject(TYPE_ID);
+ }else{
+ throw new RuntimeException(vName + " has no type yet!");
+ }
+
+
}
try {
TLAType result = expected.unify(v);
diff --git a/src/main/java/de/tla2b/old/ExpressionTranslatorOld.java b/src/main/java/de/tla2b/old/ExpressionTranslatorOld.java
index 2a545f3cf51a446a8de25b4495fff9dd1e5b3ee7..1799d45af3a59e967e435d975e195db2b4199cfb 100644
--- a/src/main/java/de/tla2b/old/ExpressionTranslatorOld.java
+++ b/src/main/java/de/tla2b/old/ExpressionTranslatorOld.java
@@ -120,7 +120,7 @@ public class ExpressionTranslatorOld implements SyntaxTreeConstants {
ModuleNode moduleNode = parseModule(moduleName, expr);
- TypeChecker tc = new TypeChecker(moduleNode);
+ TypeChecker tc = null;//= new TypeChecker(moduleNode);
try {
tc.start();
} catch (TLA2BException e) {
diff --git a/src/main/java/de/tla2bAst/ExpressionTranslator.java b/src/main/java/de/tla2bAst/ExpressionTranslator.java
index a75e2ab334ebf27b6a4c11d7a4f5a67d41cc2230..a8b8314f2d7c802d3169a2e0cc7dd936fc08a8d7 100644
--- a/src/main/java/de/tla2bAst/ExpressionTranslator.java
+++ b/src/main/java/de/tla2bAst/ExpressionTranslator.java
@@ -17,7 +17,6 @@ import tla2sany.semantic.ModuleNode;
import tla2sany.st.SyntaxTreeConstants;
import tla2sany.st.TreeNode;
import util.ToolIO;
-import de.be4.classicalb.core.parser.node.AExpressionParseUnit;
import de.be4.classicalb.core.parser.node.Start;
import de.tla2b.analysis.SpecAnalyser;
import de.tla2b.analysis.SymbolRenamer;
@@ -25,23 +24,30 @@ import de.tla2b.analysis.TypeChecker;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.old.Tla2BTranslator;
-public class ExpressionTranslator implements SyntaxTreeConstants{
+public class ExpressionTranslator implements SyntaxTreeConstants {
private final String tlaExpression;
private final ArrayList<String> variables = new ArrayList<String>();
private final ArrayList<String> noVariables = new ArrayList<String>();
private Start expressionStart;
+ private ModuleNode moduleNode;
+ private String expr;
+ private Translator translator;
- public Start getBExpressionParseUnit(){
+ public Start getBExpressionParseUnit() {
return expressionStart;
}
-
-
+
public ExpressionTranslator(String tlaExpression) {
this.tlaExpression = tlaExpression;
}
-
- public void start(){
+
+ public ExpressionTranslator(String tlaExpression, Translator translator) {
+ this.tlaExpression = tlaExpression;
+ this.translator = translator;
+ }
+
+ public void parse() {
String dir = System.getProperty("java.io.tmpdir");
ToolIO.setUserDir(dir);
@@ -54,8 +60,8 @@ public class ExpressionTranslator implements SyntaxTreeConstants{
moduleName = tempFile.getName().substring(0,
tempFile.getName().indexOf("."));
- module = "----MODULE " + moduleName + " ----\n"
- + "Expression == " + tlaExpression + "\n====";
+ module = "----MODULE " + moduleName + " ----\n" + "Expression == "
+ + tlaExpression + "\n====";
FileWriter fw = new FileWriter(tempFile);
fw.write(module);
@@ -85,8 +91,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants{
sb.append(" == ");
sb.append(tlaExpression);
sb.append("\n====================");
-
-
+
try {
FileWriter fw = new FileWriter(tempFile);
fw.write(sb.toString());
@@ -97,26 +102,43 @@ public class ExpressionTranslator implements SyntaxTreeConstants{
throw new RuntimeException(e.getMessage());
}
ToolIO.reset();
- expressionStart = translate(moduleName, sb.toString());
- }
-
-
- private static Start translate(String moduleName, String expr) {
- ModuleNode moduleNode = null;
+
+ this.expr = sb.toString();
+
+ this.moduleNode = null;
try {
- moduleNode = parseModule(moduleName, expr);
+ moduleNode = parseModule(moduleName, sb.toString());
} catch (de.tla2b.exceptions.FrontEndException e) {
throw new RuntimeException(e.getLocalizedMessage());
}
+ }
+
+ public Start translateIncludingModel() throws TLA2BException{
+ SpecAnalyser specAnalyser = SpecAnalyser
+ .createSpecAnalyserForTlaExpression(moduleNode);
+ TypeChecker tc = translator.getTypeChecker();
+ tc.visitOpDefNode(specAnalyser.getExpressionOpdefNode());
- SpecAnalyser specAnalyser = SpecAnalyser.createSpecAnalyserForTlaExpression(moduleNode);
- TypeChecker tc = new TypeChecker(moduleNode);
+
+ SymbolRenamer symRenamer = new SymbolRenamer(moduleNode, specAnalyser);
+ symRenamer.start();
+ BAstCreator bASTCreator = new BAstCreator(moduleNode, specAnalyser);
+
+ this.expressionStart = bASTCreator.expressionStart;
+ return this.expressionStart;
+ }
+
+
+ public Start translate() {
+ SpecAnalyser specAnalyser = SpecAnalyser
+ .createSpecAnalyserForTlaExpression(moduleNode);
+ TypeChecker tc = new TypeChecker(moduleNode, specAnalyser);
try {
tc.start();
} catch (TLA2BException e) {
- //String[] m = ToolIO.getAllMessages();
- String message = "****TypeError****\n"
- + e.getLocalizedMessage() + "\n" + expr + "\n";
+ // String[] m = ToolIO.getAllMessages();
+ String message = "****TypeError****\n" + e.getLocalizedMessage()
+ + "\n" + expr + "\n";
// System.out.println(message);
throw new RuntimeException(message);
}
@@ -124,10 +146,11 @@ public class ExpressionTranslator implements SyntaxTreeConstants{
SymbolRenamer symRenamer = new SymbolRenamer(moduleNode, specAnalyser);
symRenamer.start();
BAstCreator bASTCreator = new BAstCreator(moduleNode, specAnalyser);
-
- return bASTCreator.expressionStart;
+
+ this.expressionStart = bASTCreator.expressionStart;
+ return this.expressionStart;
}
-
+
public static ModuleNode parseModule(String moduleName, String module)
throws de.tla2b.exceptions.FrontEndException {
SpecObj spec = new SpecObj(moduleName, null);
@@ -139,9 +162,8 @@ public class ExpressionTranslator implements SyntaxTreeConstants{
}
if (spec.parseErrors.isFailure()) {
- //String[] m = ToolIO.getAllMessages();
- String message = module + "\n\n"
- + spec.parseErrors;
+ // String[] m = ToolIO.getAllMessages();
+ String message = module + "\n\n" + spec.parseErrors;
// System.out.println(spec.parseErrors);
message += Tla2BTranslator.allMessagesToString(ToolIO
.getAllMessages());
@@ -149,7 +171,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants{
}
if (spec.semanticErrors.isFailure()) {
- //String[] m = ToolIO.getAllMessages();
+ // String[] m = ToolIO.getAllMessages();
String message = module + "\n\n" + spec.semanticErrors;
message += Tla2BTranslator.allMessagesToString(ToolIO
.getAllMessages());
@@ -175,14 +197,13 @@ public class ExpressionTranslator implements SyntaxTreeConstants{
}
return n;
}
-
-
+
/**
* @param moduleFileName
* @throws de.tla2b.exceptions.FrontEndException
*/
- private SpecObj parseModuleWithoutSemanticAnalyse(String moduleFileName, String module)
- {
+ private SpecObj parseModuleWithoutSemanticAnalyse(String moduleFileName,
+ String module) {
SpecObj spec = new SpecObj(moduleFileName, null);
try {
@@ -199,14 +220,12 @@ public class ExpressionTranslator implements SyntaxTreeConstants{
String message = module + "\n\n";
message += Tla2BTranslator.allMessagesToString(ToolIO
.getAllMessages());
- //throw new de.tla2b.exceptions.FrontEndException(message, spec);
+ // throw new de.tla2b.exceptions.FrontEndException(message, spec);
throw new RuntimeException(message);
}
return spec;
}
-
-
/**
* @param spec
* @return
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index 1d40375536a6cf5e1172e432d882b2bd5950436f..94a1908996f6c64eb8ef41a66fd7c2a60627b502 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -44,9 +44,14 @@ public class Translator implements TranslationGlobals {
// private String moduleName;
private ModuleNode moduleNode;
private ModelConfig modelConfig;
-
private String bMachineString;
+ private SpecAnalyser specAnalyser;
+ private TypeChecker typechecker;
+
+
+
+
public Translator(String moduleFileName) throws FrontEndException {
this.moduleFileName = moduleFileName;
@@ -181,8 +186,6 @@ public class Translator implements TranslationGlobals {
PredicateVsExpression predicateVsExpression = new PredicateVsExpression(
moduleNode);
- SpecAnalyser specAnalyser;
-
ConfigfileEvaluator conEval = null;
if (modelConfig != null) {
@@ -196,10 +199,10 @@ public class Translator implements TranslationGlobals {
specAnalyser = SpecAnalyser.createSpecAnalyser(moduleNode);
}
specAnalyser.start();
- TypeChecker typechecker = new TypeChecker(moduleNode, conEval,
+ typechecker = new TypeChecker(moduleNode, conEval,
specAnalyser);
typechecker.start();
-
+
SymbolRenamer symRenamer = new SymbolRenamer(moduleNode, specAnalyser);
symRenamer.start();
UsedExternalFunctions usedExternalFunctions = new UsedExternalFunctions(
@@ -271,10 +274,18 @@ public class Translator implements TranslationGlobals {
}
+ public Start translateExpression(String tlaExpression) throws TLA2BException{
+ ExpressionTranslator expressionTranslator = new ExpressionTranslator(tlaExpression, this);
+ expressionTranslator.parse();
+ Start start = expressionTranslator.translateIncludingModel();
+ return start;
+ }
+
public static Start translateTlaExpression(String tlaExpression){
ExpressionTranslator expressionTranslator = new ExpressionTranslator(tlaExpression);
- expressionTranslator.start();
+ expressionTranslator.parse();
+ expressionTranslator.translate();
return expressionTranslator.getBExpressionParseUnit();
}
@@ -290,5 +301,13 @@ public class Translator implements TranslationGlobals {
public ModuleNode getModuleNode() {
return moduleNode;
}
+
+ protected TypeChecker getTypeChecker(){
+ return this.typechecker;
+ }
+ protected SpecAnalyser getSpecAnalyser(){
+ return this.specAnalyser;
+ }
+
}
diff --git a/src/test/java/de/tla2b/expression/ModuleAndExpressionTest.java b/src/test/java/de/tla2b/expression/ModuleAndExpressionTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..f2d2e42a7692eb1b12a0ce6c7cbec0ed84ae4136
--- /dev/null
+++ b/src/test/java/de/tla2b/expression/ModuleAndExpressionTest.java
@@ -0,0 +1,23 @@
+package de.tla2b.expression;
+
+import static de.tla2b.util.TestUtil.compareExprIncludingModel;
+
+import org.junit.Test;
+
+import de.tla2b.exceptions.TypeErrorException;
+
+public class ModuleAndExpressionTest {
+ @Test
+ public void testCon() throws Exception {
+ String module = "---- MODULE Testing ----\n" + "CONSTANTS k \n"
+ + "ASSUME k = 4" + "===============";
+ compareExprIncludingModel("bool(k = 1)", "k = 1", module);
+ }
+
+ @Test(expected = TypeErrorException.class)
+ public void testTypeError() throws Exception {
+ String module = "---- MODULE Testing ----\n" + "CONSTANTS k \n"
+ + "ASSUME k = 4" + "===============";
+ compareExprIncludingModel(null, "k = TRUE", module);
+ }
+}
diff --git a/src/test/java/de/tla2b/util/TestUtil.java b/src/test/java/de/tla2b/util/TestUtil.java
index 231480546d6778bc571a54e4d0fe1af47cd3ca2c..355e27ec1cdbd74aff51486230ef4c46694e5f42 100644
--- a/src/test/java/de/tla2b/util/TestUtil.java
+++ b/src/test/java/de/tla2b/util/TestUtil.java
@@ -74,6 +74,13 @@ public class TestUtil {
assertEquals(bAstString, result);
}
+ public static void compareExprIncludingModel(String bExpr, String tlaExpr, String moduleString) throws TLA2BException{
+ Translator trans = new Translator(moduleString, null);
+ trans.translate();
+ Start result = trans.translateExpression(tlaExpr);
+
+ }
+
public static void compare(String bMachine, String tlaModule) throws BException, TLA2BException{
ToolIO.setMode(ToolIO.TOOL);
diff --git a/src/test/resources/regression/Club/Club_tla.mch b/src/test/resources/regression/Club/Club_tla.mch
index 9c82d40c39c39efff08728f7fcad79c27f4e456c..48809d63bb87ddbfb14d10a01ebebf875dc05eab 100644
--- a/src/test/resources/regression/Club/Club_tla.mch
+++ b/src/test/resources/regression/Club/Club_tla.mch
@@ -1,4 +1,4 @@
-/*@ generated by TLA2B 1.0.7 Fri May 09 15:38:02 CEST 2014 */
+/*@ generated by TLA2B 1.0.7 Fri May 09 16:29:56 CEST 2014 */
MACHINE Club
SETS ENUM1 = {n1, n2, n3}
ABSTRACT_CONSTANTS capacity, NAME, total