adapted the expression translator

src/main/java/de/tla2b/exceptions/ExpressionTranslationException.java

+package de.tla2b.exceptions;
+
+@SuppressWarnings("serial")
+public class ExpressionTranslationException extends RuntimeException {
+
+	public ExpressionTranslationException(final String message) {
+		super(message);
+	}
+
+}

src/main/java/de/tla2b/global/OperatorTypes.java

+package de.tla2b.global;
+
+import java.util.HashSet;
+import tlc2.tool.ToolGlobals;
+
+public class OperatorTypes implements ToolGlobals, BBuildIns {
+	private static HashSet<Integer> TLA_Predicate_Operators;
+	private static HashSet<Integer> BBuiltIn_Predicate_Operators;
+	static {
+		TLA_Predicate_Operators = new HashSet<Integer>();
+		TLA_Predicate_Operators.add(OPCODE_eq);
+		TLA_Predicate_Operators.add(OPCODE_land);
+		TLA_Predicate_Operators.add(OPCODE_lor);
+		TLA_Predicate_Operators.add(OPCODE_implies);
+		TLA_Predicate_Operators.add(OPCODE_equiv);
+		TLA_Predicate_Operators.add(OPCODE_subseteq);
+		TLA_Predicate_Operators.add(OPCODE_in);
+		TLA_Predicate_Operators.add(OPCODE_notin);
+		TLA_Predicate_Operators.add(OPCODE_neg);// ?
+		TLA_Predicate_Operators.add(OPCODE_cl);
+		TLA_Predicate_Operators.add(OPCODE_dl);
+		TLA_Predicate_Operators.add(OPCODE_lnot);
+		TLA_Predicate_Operators.add(OPCODE_be);
+		TLA_Predicate_Operators.add(OPCODE_bf);
+		TLA_Predicate_Operators.add(OPCODE_noteq);
+
+		BBuiltIn_Predicate_Operators = new HashSet<Integer>();
+		BBuiltIn_Predicate_Operators.add(B_OPCODE_lt);
+		BBuiltIn_Predicate_Operators.add(B_OPCODE_gt);
+		BBuiltIn_Predicate_Operators.add(B_OPCODE_leq);
+		BBuiltIn_Predicate_Operators.add(B_OPCODE_geq);
+		BBuiltIn_Predicate_Operators.add(B_OPCODE_finite);
+		BBuiltIn_Predicate_Operators.add(B_OPCODE_assert);
+	}
+
+	public static boolean tlaOperatorIsPredicate(int opcode) {
+		return TLA_Predicate_Operators.contains(opcode);
+	}
+
+	public static boolean bbuiltInOperatorIsPredicate(int opcode) {
+		return BBuiltIn_Predicate_Operators.contains(opcode);
+	}
+
+}

src/main/java/de/tla2b/output/ASTPrettyPrinter.java

@@ -14,6 +14,7 @@ import de.be4.classicalb.core.parser.node.ADefinitionExpression;
 import de.be4.classicalb.core.parser.node.ADefinitionPredicate;
 import de.be4.classicalb.core.parser.node.AExpressionDefinitionDefinition;
 import de.be4.classicalb.core.parser.node.AFirstProjectionExpression;
+import de.be4.classicalb.core.parser.node.AGeneralSumExpression;
 import de.be4.classicalb.core.parser.node.AIdentifierExpression;
 import de.be4.classicalb.core.parser.node.ALambdaExpression;
 import de.be4.classicalb.core.parser.node.AOperation;
@@ -287,7 +288,6 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
 		}
 	}
 
-
 	private boolean makeBrackets(Node node) {
 		NodeInfo infoNode = getInfo(node);
 		Node parent = node.parent();
@@ -628,8 +628,28 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
 		sb.append(")");
 	}
 
-    public void inAConjunctPredicate(AConjunctPredicate node)
-    {
+	@Override
+	public void caseAGeneralSumExpression(AGeneralSumExpression node) {
+		List<PExpression> copy = new ArrayList<PExpression>(
+				node.getIdentifiers());
+		sb.append("SIGMA(");
+		for (final Iterator<PExpression> iterator = copy.iterator(); iterator
+				.hasNext();) {
+			final PExpression e = iterator.next();
+			e.apply(this);
+
+			if (iterator.hasNext()) {
+				sb.append(", ");
+			}
+		}
+		sb.append(").(");
+		node.getPredicates().apply(this);
+		sb.append("|");
+		node.getExpression().apply(this);
+		sb.append(")");
+	}
+
+	public void inAConjunctPredicate(AConjunctPredicate node) {
 		super.inAConjunctPredicate(node);
 	}
 
@@ -713,7 +733,6 @@ class NodeInfo {
 
 	}
 
-	
 	public NodeInfo(String pre, String beginList, String betweenListElements,
 			String endList, String betweenChildren, String end,
 			Integer precedence, Integer associative) {

src/main/java/de/tla2bAst/BAstCreator.java

@@ -43,6 +43,7 @@ import de.tla2b.config.ValueObj;
 import de.tla2b.exceptions.NotImplementedException;
 import de.tla2b.global.BBuildIns;
 import de.tla2b.global.BBuiltInOPs;
+import de.tla2b.global.OperatorTypes;
 import de.tla2b.global.Priorities;
 import de.tla2b.global.TranslationGlobals;
 import de.tla2b.translation.BMacroHandler;
@@ -77,6 +78,12 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 
 	public Start expressionStart;
 
+	/**
+	 * Creates a B AST node for a TLA expression
+	 * 
+	 * @param moduleNode
+	 * @param specAnalyser
+	 */
 	public BAstCreator(ModuleNode moduleNode, SpecAnalyser specAnalyser) {
 		this.moduleNode = moduleNode;
 		this.specAnalyser = specAnalyser;
@@ -87,10 +94,34 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 
 		ExprNode expr = moduleNode.getOpDefs()[moduleNode.getOpDefs().length - 1]
 				.getBody();
+		System.out.println(expressionIsAPredicate(expr));
+		if (expressionIsAPredicate(expr)) {
+			APredicateParseUnit predicateParseUnit = new APredicateParseUnit();
+			predicateParseUnit.setPredicate(visitExprNodePredicate(expr));
+			expressionStart = new Start(predicateParseUnit, new EOF());
+		} else {
 			AExpressionParseUnit expressionParseUnit = new AExpressionParseUnit();
 			expressionParseUnit.setExpression(visitExprNodeExpression(expr));
 			expressionStart = new Start(expressionParseUnit, new EOF());
 		}
+	}
+
+	private boolean expressionIsAPredicate(ExprNode expr) {
+		if (expr.getKind() == OpApplKind) {
+			OpApplNode opApplNode = (OpApplNode) expr;
+			int kind = opApplNode.getOperator().getKind();
+			if (kind == BuiltInKind) {
+				int opcode = getOpCode(opApplNode.getOperator().getName());
+				return OperatorTypes.tlaOperatorIsPredicate(opcode);
+			} else if (kind == UserDefinedOpKind
+					&& BBuiltInOPs.contains(opApplNode.getOperator().getName())) {
+				int opcode = BBuiltInOPs.getOpcode(opApplNode.getOperator()
+						.getName());
+				return OperatorTypes.bbuiltInOperatorIsPredicate(opcode);
+			}
+		}
+		return false;
+	}
 
 	public BAstCreator(ModuleNode moduleNode, ConfigfileEvaluator conEval,
 			SpecAnalyser specAnalyser,
@@ -1267,6 +1298,20 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 			return new AConvertBoolExpression(pred);
 		}
 
+		case B_OPCODE_setsum: {
+			AGeneralSumExpression sum = new AGeneralSumExpression();
+			String variableName = "t_"; // TODO unused identifier name
+			List<PExpression> exprList = createPexpressionList(createIdentifierNode(variableName));
+			sum.setIdentifiers(exprList);
+			AMemberPredicate memberPredicate = new AMemberPredicate();
+			memberPredicate.setLeft(createIdentifierNode(variableName));
+			memberPredicate
+					.setRight(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
+			sum.setPredicates(memberPredicate);
+			sum.setExpression(createIdentifierNode(variableName));
+			return sum;
+		}
+
 		}
 		throw new RuntimeException(n.getOperator().getName().toString());
 	}
@@ -1667,7 +1712,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 						coupleList.add(pairTable.get(fieldName));
 						couple.setList(coupleList);
 						ASetExtensionExpression set = new ASetExtensionExpression(
-								makePexpressionList(couple));
+								createPexpressionList(couple));
 						rec.setValue(set);
 					} else {
 						AEmptySetExpression emptySet = new AEmptySetExpression();
@@ -1718,7 +1763,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 						.getRep().toString()));
 				AFunctionExpression funcCall = new AFunctionExpression();
 				funcCall.setIdentifier(rcdSelect);
-				funcCall.setParameters(makePexpressionList(new ABooleanTrueExpression()));
+				funcCall.setParameters(createPexpressionList(new ABooleanTrueExpression()));
 				return funcCall;
 			} else {
 				ARecordFieldExpression rcdSelect = new ARecordFieldExpression();
@@ -2484,7 +2529,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
 		return list;
 	}
 
-	public static List<PExpression> makePexpressionList(PExpression expr) {
+	public static List<PExpression> createPexpressionList(PExpression expr) {
 		ArrayList<PExpression> list = new ArrayList<PExpression>();
 		list.add(expr);
 		return list;

src/main/java/de/tla2bAst/ExpressionTranslator.java

@@ -21,6 +21,7 @@ import de.be4.classicalb.core.parser.node.Start;
 import de.tla2b.analysis.SpecAnalyser;
 import de.tla2b.analysis.SymbolRenamer;
 import de.tla2b.analysis.TypeChecker;
+import de.tla2b.exceptions.ExpressionTranslationException;
 import de.tla2b.exceptions.TLA2BException;
 
 public class ExpressionTranslator implements SyntaxTreeConstants {
@@ -46,7 +47,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
 		this.translator = translator;
 	}
 
-	public void parse() throws de.tla2b.exceptions.FrontEndException {
+	public void parse() {
 		String dir = System.getProperty("java.io.tmpdir");
 		ToolIO.setUserDir(dir);
 
@@ -66,9 +67,8 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
 			fw.write(module);
 			fw.close();
 		} catch (IOException e) {
-			throw new de.tla2b.exceptions.FrontEndException(
-					"Can not create file temporary file in directory '" + dir
-							+ "'");
+			throw new ExpressionTranslationException(
+					"Can not create temporary file in directory '" + dir + "'");
 		}
 
 		SpecObj spec = parseModuleWithoutSemanticAnalyse(moduleName, module);
@@ -98,7 +98,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
 			fw.close();
 			tempFile.deleteOnExit();
 		} catch (IOException e) {
-			throw new de.tla2b.exceptions.FrontEndException(e.getMessage());
+			throw new ExpressionTranslationException(e.getMessage());
 		}
 		ToolIO.reset();
 
@@ -108,7 +108,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
 		try {
 			moduleNode = parseModule(moduleName, sb.toString());
 		} catch (de.tla2b.exceptions.FrontEndException e) {
-			throw new de.tla2b.exceptions.FrontEndException(e.getLocalizedMessage());
+			throw new ExpressionTranslationException(e.getLocalizedMessage());
 		}
 	}
 
@@ -133,11 +133,9 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
 		try {
 			tc.start();
 		} catch (TLA2BException e) {
-			// String[] m = ToolIO.getAllMessages();
 			String message = "****TypeError****\n" + e.getLocalizedMessage()
 					+ "\n" + expr + "\n";
-			// System.out.println(message);
-			throw new RuntimeException(message);
+			throw new ExpressionTranslationException(message);
 		}
 
 		SymbolRenamer symRenamer = new SymbolRenamer(moduleNode, specAnalyser);
@@ -209,8 +207,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
 		if (spec.parseErrors.isFailure()) {
 			String message = module + "\n\n";
 			message += allMessagesToString(ToolIO.getAllMessages());
-			// throw new de.tla2b.exceptions.FrontEndException(message, spec);
-			throw new RuntimeException(message);
+			throw new ExpressionTranslationException(message);
 		}
 		return spec;
 	}

src/main/java/de/tla2bAst/Translator.java

@@ -388,12 +388,7 @@ public class Translator implements TranslationGlobals {
 	public static Start translateTlaExpression(String tlaExpression) {
 		ExpressionTranslator expressionTranslator = new ExpressionTranslator(
 				tlaExpression);
-		try {
 		expressionTranslator.parse();
-		} catch (FrontEndException e) {
-			System.out.println(e.getMessage());
-			throw new RuntimeException();
-		}
 		expressionTranslator.translate();
 		return expressionTranslator.getBExpressionParseUnit();
 	}

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

@@ -12,7 +12,7 @@ public class ComplexExpressionTest {
 
 	@Test
 	public void testExcept() throws Exception {
-		compareExpr("bool(a = %u.(u : {3, 4, 5}| u + 1) & x = a <+ {3 |-> 1})",
+		compareExpr("a = %u.(u : {3, 4, 5}| u + 1) & x = a <+ {3 |-> 1}",
 				"a = [u \\in {3,4,5}|-> u + 1] /\\ x = [a EXCEPT ![3] = 1]");
 	}
 
@@ -33,7 +33,7 @@ public class ComplexExpressionTest {
 
 	@Test
 	public void testPrime() throws Exception {
-		compareExpr("bool(x_n = 1)", "x' = 1");
+		compareExpr("x_n = 1", "x' = 1");
 	}
 
 	@Test
@@ -44,7 +44,7 @@ public class ComplexExpressionTest {
 	@Test
 	public void testQuantifier() throws Exception {
 		compareExpr(
-				"bool(#x,z,y.(x : NATURAL & z : NATURAL & y : NATURAL & x = y))",
+				"#x,z,y.(x : NATURAL & z : NATURAL & y : NATURAL & x = y)",
 				"\\E x,z \\in Nat, y \\in Nat: x = y");
 	}
 
@@ -63,7 +63,7 @@ public class ComplexExpressionTest {
 
 	@Test
 	public void testRecord2() throws Exception {
-		compareExpr("bool(r = rec(a:rec(x:1, y:TRUE), b:1) & r2 = rec(a:rec(x:2, y:(r'a)'y), b:r'b))",
+		compareExpr("r = rec(a:rec(x:1, y:TRUE), b:1) & r2 = rec(a:rec(x:2, y:(r'a)'y), b:r'b)",
 				"r = [a |-> [x|->1,y|->TRUE], b |-> 1] "
 						+ "/\\ r2 = [r EXCEPT !.a.x = 2]");
 	}

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

@@ -11,18 +11,29 @@ import static de.tla2b.util.TestUtil.compareExpr;
 public class SimpleExpressionTest {
 
 	@Test
-	public void testSimpleExpr() throws Exception {
+	public void testSimpleExpression() throws Exception {
 		compareExpr("1 + 2", "1 + 2");
 	}
 
+	@Test
+	public void testSimplePredicate() throws Exception {
+		compareExpr("1 = 1", "1 = 1");
+	}
+	
+	@Test
+	public void testSimplePredicate2() throws Exception {
+		compareExpr("1 < 1", "1 < 1");
+	}
+	
+	
 	@Test
 	public void testModulIntegers() throws Exception {
-		compareExpr("bool(-1 : INTEGER)", "-1 \\in Int");
+		compareExpr("-1 : INTEGER", "-1 \\in Int");
 	}
 
 	@Test
 	public void testExist() throws Exception {
-		compareExpr("bool(#a.(a : {1} & 2 > 1))", "\\E a \\in {1}: 2 > 1");
+		compareExpr("#a.(a : {1} & 2 > 1)", "\\E a \\in {1}: 2 > 1");
 	}
 
 	@Test

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

@@ -8,19 +8,21 @@ import static de.tla2b.util.TestUtil.compareExpr;
 
 import org.junit.Test;
 
+import de.tla2b.exceptions.ExpressionTranslationException;
+
 public class TestError {
 
-	@Test(expected = Exception.class)
+	@Test(expected = ExpressionTranslationException.class)
 	public void testParseError() throws Exception {
 		compareExpr(null, "a =");
 	}
 
-	@Test(expected = Exception.class)
+	@Test(expected = ExpressionTranslationException.class)
 	public void testSemanticError() throws Exception {
 		compareExpr(null, "a(1)");
 	}
 
-	@Test(expected = Exception.class)
+	@Test(expected = ExpressionTranslationException.class)
 	public void testTypeError() throws Exception {
 		compareExpr(null, "1 = TRUE");
 	}

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

@@ -22,7 +22,7 @@ public class TestKeywords {
 
 	@Test
 	public void testExcept() throws Exception {
-		compareExpr("bool(x = a <+ {1 |-> 1})", "x = [a EXCEPT ![1] = 1]");
+		compareExpr("x = a <+ {1 |-> 1}", "x = [a EXCEPT ![1] = 1]");
 	}
 
 	@Test
@@ -32,6 +32,6 @@ public class TestKeywords {
 
 	@Test
 	public void testDom() throws Exception {
-		compareExpr("bool(dom_1 = 1)", "dom = 1");
+		compareExpr("dom_1 = 1", "dom = 1");
 	}
 }

src/test/java/de/tla2b/prettyprintb/BBuiltInsTest.java

@@ -6,6 +6,7 @@ package de.tla2b.prettyprintb;
 
 import static de.tla2b.util.TestUtil.compare;
 
+import org.junit.Ignore;
 import org.junit.Test;
 
 public class BBuiltInsTest {
@@ -21,6 +22,19 @@ public class BBuiltInsTest {
 		compare(expected, module);
 	}
 	
+	@Ignore
+	@Test
+	public void testSetSummation() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "EXTENDS TLA2B\n" 
+				+ "ASSUME SetSummation({1,2}) = 3\n"
+				+ "=================================";
+
+		final String expected = "MACHINE Testing\n"
+				+ "PROPERTIES SIGMA(t_).(t_ : {1,2}|t_) = 3 \n" + "END";
+		compare(expected, module);
+	}
+
 	@Test
 	public void testString() throws Exception {
 		final String module = "-------------- MODULE Testing ----------------\n"