diff --git a/src/main/java/de/tla2b/exceptions/ExpressionTranslationException.java b/src/main/java/de/tla2b/exceptions/ExpressionTranslationException.java
new file mode 100644
index 0000000000000000000000000000000000000000..ff7f014ccd7c835419c8c3f3787f64f186edcce2
--- /dev/null
+++ b/src/main/java/de/tla2b/exceptions/ExpressionTranslationException.java
@@ -0,0 +1,10 @@
+package de.tla2b.exceptions;
+
+@SuppressWarnings("serial")
+public class ExpressionTranslationException extends RuntimeException {
+
+ public ExpressionTranslationException(final String message) {
+ super(message);
+ }
+
+}
diff --git a/src/main/java/de/tla2b/global/OperatorTypes.java b/src/main/java/de/tla2b/global/OperatorTypes.java
new file mode 100644
index 0000000000000000000000000000000000000000..1bcfec469c48935cd8093899ee92c27e19049ebf
--- /dev/null
+++ b/src/main/java/de/tla2b/global/OperatorTypes.java
@@ -0,0 +1,44 @@
+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);
+ }
+
+}
diff --git a/src/main/java/de/tla2b/output/ASTPrettyPrinter.java b/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
index b326af6fd755c316eaba117f7041fb7b3b304ca1..1f899732e529be0521edc516dc31f776a2c77db8 100644
--- a/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
+++ b/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;
@@ -45,7 +46,7 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
public ASTPrettyPrinter(Start start, Renamer renamer) {
this.renamer = renamer;
-
+
this.indentation = new Indentation(start);
}
@@ -219,7 +220,7 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
put("AComprehensionSetExpression", "{", "", ",", "", " | ", "}");
put("AFirstProjectionExpression", "prj1(", null, null, null, ", ", ")");
-
+
put("ASecondProjectionExpression", "prj2(", null, null, null, ", ", ")");
}
@@ -263,7 +264,7 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
builder.append(node.getClass().getSimpleName());
builder.append("(");
}
-
+
@Override
public void defaultCase(final Node node) {
super.defaultCase(node);
@@ -287,7 +288,6 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
}
}
-
private boolean makeBrackets(Node node) {
NodeInfo infoNode = getInfo(node);
Node parent = node.parent();
@@ -335,7 +335,7 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
@Override
public void betweenChildren(final Node node) {
builder.append(',');
- if(indentation.printNewLineInTheMiddle(node)){
+ if (indentation.printNewLineInTheMiddle(node)) {
sb.append("\n");
}
sb.append(getInfo(node).betweenChildren);
@@ -627,11 +627,31 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
node.getExpression().apply(this);
sb.append(")");
}
-
- public void inAConjunctPredicate(AConjunctPredicate node)
- {
- super.inAConjunctPredicate(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) {
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 31c2924d0d31f95c3f1ba4213c6008ca0668c922..f906e9975fc3e71cf1860d303c3d6815790f4f99 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/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,9 +94,33 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
ExprNode expr = moduleNode.getOpDefs()[moduleNode.getOpDefs().length - 1]
.getBody();
- AExpressionParseUnit expressionParseUnit = new AExpressionParseUnit();
- expressionParseUnit.setExpression(visitExprNodeExpression(expr));
- expressionStart = new Start(expressionParseUnit, new EOF());
+ 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,
@@ -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;
diff --git a/src/main/java/de/tla2bAst/ExpressionTranslator.java b/src/main/java/de/tla2bAst/ExpressionTranslator.java
index e809a791fe9f40815e08cb89d3a252bacfe71017..c4da22f1a9cd49d128de74efce430749868897e3 100644
--- a/src/main/java/de/tla2bAst/ExpressionTranslator.java
+++ b/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;
}
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index 5a1c46ebf1b5904c785bbdb30acf92d4b2105276..76f539e8fe35bdc55b0e414554cb7d7c6cb48092 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/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.parse();
expressionTranslator.translate();
return expressionTranslator.getBExpressionParseUnit();
}
diff --git a/src/test/java/de/tla2b/expression/ComplexExpressionTest.java b/src/test/java/de/tla2b/expression/ComplexExpressionTest.java
index ccc38c61511de05d74f5ab996669b8b9f815f36c..f57db27b211a273e7ed565699818078b24d50456 100644
--- a/src/test/java/de/tla2b/expression/ComplexExpressionTest.java
+++ b/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]");
}
diff --git a/src/test/java/de/tla2b/expression/SimpleExpressionTest.java b/src/test/java/de/tla2b/expression/SimpleExpressionTest.java
index 4afcbc73c6d4cbdd69570c07eb91f9df79f5e2b1..e8eecb4c5f0dd24caf04611daa976867c81776e3 100644
--- a/src/test/java/de/tla2b/expression/SimpleExpressionTest.java
+++ b/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
diff --git a/src/test/java/de/tla2b/expression/TestError.java b/src/test/java/de/tla2b/expression/TestError.java
index a63773f9d92b122b522eba50f8d82cb1b94d6bff..104ff1b69f85845fe761399e9bb0f953a54d830d 100644
--- a/src/test/java/de/tla2b/expression/TestError.java
+++ b/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");
}
diff --git a/src/test/java/de/tla2b/expression/TestKeywords.java b/src/test/java/de/tla2b/expression/TestKeywords.java
index db85231832b2b358946152e32466f75fe8b176f1..ef4ecec88e4e24cc4e4f0c2e01a457188a49354f 100644
--- a/src/test/java/de/tla2b/expression/TestKeywords.java
+++ b/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");
}
}
diff --git a/src/test/java/de/tla2b/prettyprintb/BBuiltInsTest.java b/src/test/java/de/tla2b/prettyprintb/BBuiltInsTest.java
index c434d8a2e7ebe96935e192726fc320d38c8d74db..6570544fcfa7d43fe7e756b1ea4538d322cf58e6 100644
--- a/src/test/java/de/tla2b/prettyprintb/BBuiltInsTest.java
+++ b/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 {
@@ -20,6 +21,19 @@ public class BBuiltInsTest {
+ "PROPERTIES TRUE : BOOL \n" + "END";
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 {