Translating an expression associated to module

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);
+	}
+	
 }

src/main/java/de/tla2b/analysis/TypeChecker.java

@@ -54,6 +54,7 @@ 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;
 
@@ -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,8 +388,16 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
 			String vName = symbolNode.getName().toString();
 			TLAType v = (TLAType) symbolNode.getToolObject(TYPE_ID);
 			if (v == null) {
+				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);
 				symbolNode.setToolObject(TYPE_ID, result);

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) {

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;
@@ -31,17 +30,24 @@ public class ExpressionTranslator implements SyntaxTreeConstants{
 	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() {
 		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);
@@ -86,7 +92,6 @@ public class ExpressionTranslator implements SyntaxTreeConstants{
 		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());
-	}
 		
+		this.expr = sb.toString();
 		
-	private static Start translate(String moduleName, String expr) {
-		ModuleNode moduleNode = null;
+		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 message = "****TypeError****\n" + e.getLocalizedMessage()
+					+ "\n" + expr + "\n";
 			// System.out.println(message);
 			throw new RuntimeException(message);
 		}
@@ -125,7 +147,8 @@ public class ExpressionTranslator implements SyntaxTreeConstants{
 		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)
@@ -140,8 +163,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants{
 
 		if (spec.parseErrors.isFailure()) {
 			// String[] m = ToolIO.getAllMessages();
-			String message = module + "\n\n"
-					+ spec.parseErrors;
+			String message = module + "\n\n" + spec.parseErrors;
 			// System.out.println(spec.parseErrors);
 			message += Tla2BTranslator.allMessagesToString(ToolIO
 					.getAllMessages());
@@ -176,13 +198,12 @@ 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 {
@@ -205,8 +226,6 @@ public class ExpressionTranslator implements SyntaxTreeConstants{
 		return spec;
 	}
 
-	
-
 	/**
 	 * @param spec
 	 * @return

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,7 +199,7 @@ 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();
 		
@@ -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();
 	}
 	
@@ -291,4 +302,12 @@ public class Translator implements TranslationGlobals {
 		return moduleNode;
 	}
 	
+	protected TypeChecker getTypeChecker(){
+		return this.typechecker;
+	}
+
+	protected SpecAnalyser getSpecAnalyser(){
+		return this.specAnalyser;
+	}
+	
 }

src/test/java/de/tla2b/expression/ModuleAndExpressionTest.java

+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);
+	}
+}

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);

src/test/resources/regression/Club/Club_tla.mch

-/*@ 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