From 812da0921a8f6ad2ce93521440ec66345be59ac1 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Wed, 18 Jun 2014 13:51:16 +0200
Subject: [PATCH] Fixed some bugs handling tuples
---
.../de/tla2b/analysis/AbstractASTVisitor.java | 2 +-
.../java/de/tla2b/analysis/BOperation.java | 2 +-
.../java/de/tla2b/analysis/SpecAnalyser.java | 3 +
.../java/de/tla2b/analysis/TypeChecker.java | 157 +++---
.../tla2b/analysis/UsedExternalFunctions.java | 27 +-
src/main/java/de/tla2b/global/BBuildIns.java | 6 +
.../java/de/tla2b/global/BBuiltInOPs.java | 2 +-
.../de/tla2b/global/TranslationGlobals.java | 2 +
.../de/tla2b/output/ASTPrettyPrinter.java | 76 +--
.../java/de/tla2b/output/Indentation.java | 55 ++
.../tla2b/translation/OperationsFinder.java | 4 +-
.../java/de/tla2b/types/TupleOrFunction.java | 263 +++++-----
src/main/java/de/tla2b/types/TupleType.java | 81 +--
src/main/java/de/tla2bAst/BAstCreator.java | 478 +++++++++++-------
src/main/java/de/tla2bAst/Translator.java | 2 +-
.../tla2b/prettyprintb/ExampleFilesTest.java | 2 +-
.../de/tla2b/prettyprintb/ExceptTest.java | 46 +-
.../prettyprintb/ExternelFunctionsTest.java | 25 +
.../de/tla2b/prettyprintb/FunctionTest.java | 45 ++
.../prettyprintb/LogicOperatorsTest.java | 33 ++
.../java/de/tla2b/prettyprintb/SetsTest.java | 50 +-
.../java/de/tla2b/prettyprintb/TupleTest.java | 16 +
.../de/tla2b/typechecking/ExceptTest.java | 12 +
.../de/tla2b/typechecking/FunctionTest.java | 3 +-
.../java/de/tla2b/typechecking/TupleTest.java | 1 -
.../java/de/tla2b/util/TestTypeChecker.java | 16 +-
src/test/java/de/tla2b/util/TestUtil.java | 44 +-
.../Modules/InvariantExpression.tla | 6 +
28 files changed, 907 insertions(+), 552 deletions(-)
create mode 100644 src/main/java/de/tla2b/output/Indentation.java
create mode 100644 src/test/java/de/tla2b/prettyprintb/ExternelFunctionsTest.java
create mode 100644 src/test/resources/regression/Modules/InvariantExpression.tla
diff --git a/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java b/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java
index c606330..d94b611 100644
--- a/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java
+++ b/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java
@@ -117,7 +117,7 @@ public class AbstractASTVisitor extends BuiltInOPs implements ASTConstants {
}
- private void visitBBuiltinsNode(OpApplNode n) {
+ public void visitBBuiltinsNode(OpApplNode n) {
ExprNode[] in = n.getBdedQuantBounds();
for (ExprNode exprNode : in) {
visitExprNode(exprNode);
diff --git a/src/main/java/de/tla2b/analysis/BOperation.java b/src/main/java/de/tla2b/analysis/BOperation.java
index fddcb1f..fec96cc 100644
--- a/src/main/java/de/tla2b/analysis/BOperation.java
+++ b/src/main/java/de/tla2b/analysis/BOperation.java
@@ -83,7 +83,7 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
}
for (int j = 0; j < this.getExistQuans().size(); j++) {
OpApplNode o = this.getExistQuans().get(j);
- whereList.add(bASTCreator.visitBounded(o));
+ whereList.add(bASTCreator.visitBoundsOfLocalVariables(o));
}
operation.setOpName(BAstCreator.createTIdentifierLiteral(name));
diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index c28f195..eebb4d1 100644
--- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java
+++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
@@ -109,6 +109,9 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
specAnalyser.spec = definitions.get("Spec");
specAnalyser.init = definitions.get("Init");
specAnalyser.next = definitions.get("Next");
+ if(definitions.containsKey("Inv")){
+ specAnalyser.invariants.add(definitions.get("Inv"));
+ }
// TODO are constant in the right order
specAnalyser.bConstants.addAll(Arrays.asList(m.getConstantDecls()));
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index f15ee18..4549a4e 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -36,6 +36,7 @@ import tla2sany.semantic.NumeralNode;
import tla2sany.semantic.OpApplNode;
import tla2sany.semantic.OpDeclNode;
import tla2sany.semantic.OpDefNode;
+import tla2sany.semantic.SemanticNode;
import tla2sany.semantic.StringNode;
import tla2sany.semantic.SymbolNode;
import tlc2.tool.BuiltInOPs;
@@ -50,8 +51,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
private ExprNode nextExpr;
private Set<OpDefNode> usedDefinitions;
- private ArrayList<OpApplNode> recList = new ArrayList<OpApplNode>();
- // every record node [a |-> 1 .. ] will be added to this List
+ private ArrayList<SymbolNode> symbolNodeList = new ArrayList<SymbolNode>();
+ private ArrayList<SemanticNode> tupleNodeList = new ArrayList<SemanticNode>();
+
private ModuleNode moduleNode;
private ArrayList<OpDeclNode> bConstList;
private SpecAnalyser specAnalyser;
@@ -158,7 +160,13 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
visitExprNode(nextExpr, BoolType.getInstance());
}
+ checkIfAllIdentifiersHaveAType();
+
+ }
+
+ private void checkIfAllIdentifiersHaveAType() throws TypeErrorException {
// check if a variable has no type
+ OpDeclNode[] vars = moduleNode.getVariableDecls();
for (int i = 0; i < vars.length; i++) {
OpDeclNode var = vars[i];
TLAType varType = (TLAType) var.getToolObject(TYPE_ID);
@@ -170,6 +178,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
// check if a constant has no type, only constants which will appear in
// the resulting B Machine are considered
+ OpDeclNode[] cons = moduleNode.getConstantDecls();
for (int i = 0; i < cons.length; i++) {
OpDeclNode con = cons[i];
if (bConstList == null || bConstList.contains(con)) {
@@ -181,30 +190,19 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
}
- evalRecList();
- }
+ for (SymbolNode symbol : symbolNodeList) {
+ TLAType type = (TLAType) symbol.getToolObject(TYPE_ID);
+ if (type.isUntyped()) {
+ throw new TypeErrorException("Symbol '" + symbol.getName()
+ + "' has no type.\n" + symbol.getLocation());
+ }
+ }
- /**
- *
- */
- private void evalRecList() {
- for (int i = 0; i < recList.size(); i++) {
- OpApplNode n = recList.get(i);
- StructType struct = (StructType) n.getToolObject(TYPE_ID);
- ArrayList<String> fieldNames = new ArrayList<String>();
- ExprOrOpArgNode[] args = n.getArgs();
- for (int j = 0; j < args.length; j++) {
- OpApplNode pair = (OpApplNode) args[j];
- StringNode stringNode = (StringNode) pair.getArgs()[0];
- fieldNames.add(stringNode.getRep().toString());
- }
- for (int j = 0; j < struct.getFields().size(); j++) {
- String fieldName = struct.getFields().get(j);
- if (!fieldNames.contains(fieldName)
- && struct.getType(fieldName).getKind() == IType.MODELVALUE) {
- EnumType e = (EnumType) struct.getType(fieldName);
- e.setNoVal();
- }
+ for (SemanticNode tuple : tupleNodeList) {
+ TLAType type = (TLAType) tuple.getToolObject(TYPE_ID);
+ if (type instanceof TupleOrFunction) {
+ TupleOrFunction tOrF = (TupleOrFunction) type;
+ tOrF.getFinalType();
}
}
@@ -423,6 +421,10 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
if (t == null) {
t = (TLAType) symbolNode.getToolObject(TYPE_ID);
}
+
+ if(t == null){
+ throw new RuntimeException();
+ }
try {
TLAType result = expected.unify(t);
symbolNode.setToolObject(paramId, result);
@@ -741,7 +743,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = new FunctionType(IntType.getInstance(), list.get(0));
} else {
found = TupleOrFunction.createTupleOrFunctionType(list);
- //found = new TupleType(list);
+ // found = new TupleType(list);
}
try {
found = found.unify(expected);
@@ -751,6 +753,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
n.getLocation()));
}
n.setToolObject(TYPE_ID, found);
+ tupleNodeList.add(n);
if (found instanceof AbstractHasFollowers) {
((AbstractHasFollowers) found).addFollower(n);
}
@@ -765,6 +768,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
{
FormalParamNode recFunc = n.getUnbdedQuantSymbols()[0];
+ symbolNodeList.add(recFunc);
FunctionType recType = new FunctionType();
recFunc.setToolObject(TYPE_ID, recType);
recType.addFollower(recFunc);
@@ -825,10 +829,19 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
new UntypedType());
domList.add(d);
}
- domType = new TupleType(domList);
- FunctionType func = new FunctionType(domType, expected);
- TLAType res = visitExprOrOpArgNode(n.getArgs()[0], func);
- return ((FunctionType) res).getRange();
+
+ if (domList.size() == 1) { // one-tuple
+ domType = new FunctionType(IntType.getInstance(),
+ domList.get(0));
+ FunctionType func = new FunctionType(domType, expected);
+ TLAType res = visitExprOrOpArgNode(n.getArgs()[0], func);
+ return ((FunctionType) res).getRange();
+ } else {
+ domType = new TupleType(domList);
+ FunctionType func = new FunctionType(domType, expected);
+ TLAType res = visitExprOrOpArgNode(n.getArgs()[0], func);
+ return ((FunctionType) res).getRange();
+ }
} else {
ExprOrOpArgNode arg = n.getArgs()[1];
if (arg instanceof NumeralNode) {
@@ -838,18 +851,23 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
u.addFollower(n);
TupleOrFunction tupleOrFunc = new TupleOrFunction(
num.val(), u);
- TLAType funcOrTuple = visitExprOrOpArgNode(n.getArgs()[0], tupleOrFunc);
+
+ TLAType funcOrTuple = visitExprOrOpArgNode(n.getArgs()[0],
+ tupleOrFunc);
n.getArgs()[0].setToolObject(TYPE_ID, funcOrTuple);
- if(funcOrTuple instanceof AbstractHasFollowers){
- ((AbstractHasFollowers) funcOrTuple).addFollower(n.getArgs()[0]);
+ tupleNodeList.add(n.getArgs()[0]);
+ if (funcOrTuple instanceof AbstractHasFollowers) {
+ ((AbstractHasFollowers) funcOrTuple).addFollower(n
+ .getArgs()[0]);
}
-
+
TLAType found = (TLAType) n.getToolObject(TYPE_ID);
try {
found = found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException("Expected '" + expected
- + "', found '" + found + "'.\n" + n.getLocation());
+ + "', found '" + found + "'.\n"
+ + n.getLocation());
}
return found;
}
@@ -905,7 +923,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
/**********************************************************************
* Except
**********************************************************************/
- case OPCODE_exc: // Except
+ case OPCODE_exc: // $Except
{
return evalExcept(n, expected);
}
@@ -929,7 +947,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
"Expected %s, found %s at Cartesian Product,%n%s",
expected, found, n.getLocation()));
}
-
+
return found;
}
@@ -980,7 +998,6 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
n.setToolObject(TYPE_ID, found);
found.addFollower(n);
- recList.add(n);
return found;
}
@@ -1002,8 +1019,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
"Struct has no field %s with type %s: %s%n%s",
fieldName, r.getType(fieldName), r, n.getLocation()));
}
- n.setToolObject(TYPE_ID, r);
- r.addFollower(n);
+ n.getArgs()[0].setToolObject(TYPE_ID, r);
+ r.addFollower(n.getArgs()[0]);
return r.getType(fieldName);
}
@@ -1045,6 +1062,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
case OPCODE_uc: {
TLAType found = new UntypedType();
FormalParamNode x = n.getUnbdedQuantSymbols()[0];
+ symbolNodeList.add(x);
x.setToolObject(TYPE_ID, found);
((AbstractHasFollowers) found).addFollower(x);
visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
@@ -1079,6 +1097,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found, n.getLocation()));
}
FormalParamNode x = n.getBdedQuantSymbolLists()[0][0];
+ symbolNodeList.add(x);
x.setToolObject(TYPE_ID, found);
if (found instanceof AbstractHasFollowers) {
((AbstractHasFollowers) found).addFollower(x);
@@ -1113,37 +1132,38 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
TLAType subType = boundType.getSubType();
if (n.isBdedQuantATuple()[i]) {
- if (subType instanceof TupleType) {
- domList.add(subType);
- TupleType t = (TupleType) subType;
- if (params[i].length != t.getTypes().size()) {
- throw new TypeErrorException("Expected tuple with "
- + params[i].length
- + " components, found tuple with "
- + t.getTypes().size() + " components.\n"
- + bounds[i].getLocation());
+ if (params[i].length == 1) {
+ FormalParamNode p = params[i][0];
+ FunctionType expected = new FunctionType(
+ IntType.getInstance(), new UntypedType());
+ try {
+ expected = expected.unify(subType);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(String.format(
+ "Expected %s, found %s at parameter %s,%n%s",
+ expected, subType, p.getName().toString(),
+ bounds[i].getLocation()));
}
- for (int j = 0; j < params[i].length; j++) {
- FormalParamNode p = params[i][j];
- TLAType paramType = t.getTypes().get(j);
- p.setToolObject(TYPE_ID, paramType);
- if (paramType instanceof AbstractHasFollowers) {
- ((AbstractHasFollowers) paramType).addFollower(p);
- }
+ domList.add(expected);
+ symbolNodeList.add(p);
+ p.setToolObject(TYPE_ID, expected.getRange());
+ if (expected.getRange() instanceof AbstractHasFollowers) {
+ ((AbstractHasFollowers) expected.getRange())
+ .addFollower(p);
}
- } else if (subType instanceof UntypedType) {
+ } else {
TupleType tuple = new TupleType(params[i].length);
try {
tuple = (TupleType) tuple.unify(subType);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found %s ,%n%s", tuple, subType,
- n.getLocation()));
+ "Expected %s, found %s at tuple,%n%s", tuple,
+ subType, bounds[i].getLocation()));
}
-
domList.add(tuple);
for (int j = 0; j < params[i].length; j++) {
FormalParamNode p = params[i][j];
+ symbolNodeList.add(p);
TLAType paramType = tuple.getTypes().get(j);
p.setToolObject(TYPE_ID, paramType);
if (paramType instanceof AbstractHasFollowers) {
@@ -1151,15 +1171,14 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
}
- } else {
- throw new TypeErrorException("Expected tuple, found '"
- + subType + "'.\n" + bounds[i].getLocation());
}
+
} else {
// is not a tuple: all parameter have the same type
for (int j = 0; j < params[i].length; j++) {
domList.add(subType);
FormalParamNode p = params[i][j];
+ symbolNodeList.add(p);
p.setToolObject(TYPE_ID, subType);
if (subType instanceof AbstractHasFollowers) {
((AbstractHasFollowers) subType).addFollower(p);
@@ -1236,6 +1255,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
domList.add(d);
}
domType = new TupleType(domList);
+ domExpr.setToolObject(TYPE_ID, domType); // store type
} else {
domType = visitExprOrOpArgNode(domExpr, new UntypedType());
}
@@ -1635,6 +1655,17 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
.getOperator().getName(), n.getLocation()));
}
+ case B_OPCODE_assert: {
+ try {
+ BoolType.getInstance().unify(expected);
+ return BoolType.getInstance();
+ } catch (Exception e) {
+ throw new TypeErrorException(String.format(
+ "Expected %s, found BOOL at '%s',%n%s", expected, n
+ .getOperator().getName(), n.getLocation()));
+ }
+ }
+
default: {
throw new NotImplementedException(n.getOperator().getName()
.toString());
diff --git a/src/main/java/de/tla2b/analysis/UsedExternalFunctions.java b/src/main/java/de/tla2b/analysis/UsedExternalFunctions.java
index 97576a9..1314442 100644
--- a/src/main/java/de/tla2b/analysis/UsedExternalFunctions.java
+++ b/src/main/java/de/tla2b/analysis/UsedExternalFunctions.java
@@ -3,16 +3,18 @@ package de.tla2b.analysis;
import java.util.HashSet;
import java.util.Set;
+import de.tla2b.global.BBuildIns;
+import de.tla2b.global.BBuiltInOPs;
import tla2sany.semantic.ExprNode;
import tla2sany.semantic.ExprOrOpArgNode;
import tla2sany.semantic.ModuleNode;
import tla2sany.semantic.OpApplNode;
import tla2sany.semantic.OpDefNode;
-public class UsedExternalFunctions extends AbstractASTVisitor {
+public class UsedExternalFunctions extends AbstractASTVisitor implements BBuildIns{
public enum EXTERNAL_FUNCTIONS {
- CHOOSE
+ CHOOSE, ASSERT
}
private final Set<EXTERNAL_FUNCTIONS> usedExternalFunctions;
@@ -57,5 +59,26 @@ public class UsedExternalFunctions extends AbstractASTVisitor {
}
}
}
+
+ @Override
+ public void visitBBuiltinsNode(OpApplNode n) {
+ switch (BBuiltInOPs.getOpcode(n.getOperator().getName())) {
+
+ case B_OPCODE_assert: {
+ usedExternalFunctions.add(EXTERNAL_FUNCTIONS.ASSERT);
+ }
+ }
+
+
+ ExprNode[] in = n.getBdedQuantBounds();
+ for (ExprNode exprNode : in) {
+ visitExprNode(exprNode);
+ }
+
+ ExprOrOpArgNode[] arguments = n.getArgs();
+ for (ExprOrOpArgNode exprOrOpArgNode : arguments) {
+ visitExprOrOpArgNode(exprOrOpArgNode);
+ }
+ }
}
diff --git a/src/main/java/de/tla2b/global/BBuildIns.java b/src/main/java/de/tla2b/global/BBuildIns.java
index 7a6e238..f30e02b 100644
--- a/src/main/java/de/tla2b/global/BBuildIns.java
+++ b/src/main/java/de/tla2b/global/BBuildIns.java
@@ -81,6 +81,10 @@ public interface BBuildIns {
public static final UniqueString OP_rel_inverse = UniqueString
.uniqueStringOf("rel_inverse");
+ //TLC
+ public static final UniqueString OP_assert = UniqueString
+ .uniqueStringOf("Assert");
+
public static final int B_OPCODE_dotdot = 1;
public static final int B_OPCODE_plus = 2;
public static final int B_OPCODE_minus = 3;
@@ -123,4 +127,6 @@ public interface BBuildIns {
public static final int B_OPCODE_rel_inverse = B_OPCODE_pow1 + 1;
+
+ public static final int B_OPCODE_assert = B_OPCODE_rel_inverse + 1;
}
diff --git a/src/main/java/de/tla2b/global/BBuiltInOPs.java b/src/main/java/de/tla2b/global/BBuiltInOPs.java
index b3d770a..ad48af3 100644
--- a/src/main/java/de/tla2b/global/BBuiltInOPs.java
+++ b/src/main/java/de/tla2b/global/BBuiltInOPs.java
@@ -51,7 +51,7 @@ public class BBuiltInOPs implements BBuildIns{
//relations
B_Opcode_Table.put(OP_rel_inverse, B_OPCODE_rel_inverse);
-
+ B_Opcode_Table.put(OP_assert, B_OPCODE_assert);
}
public static boolean contains(UniqueString s){
diff --git a/src/main/java/de/tla2b/global/TranslationGlobals.java b/src/main/java/de/tla2b/global/TranslationGlobals.java
index 692bdd5..d0af064 100644
--- a/src/main/java/de/tla2b/global/TranslationGlobals.java
+++ b/src/main/java/de/tla2b/global/TranslationGlobals.java
@@ -20,10 +20,12 @@ public interface TranslationGlobals {
final int DEF_OBJECT = 19;
final int PRINT_DEFINITION = 11;
final int TYPE_ID = 5;
+ final int EXCEPT_BASE = 6;
final int LET_PARAMS_ID = 13;
final int NEW_NAME = 20;
final int SUBSTITUTE_PARAM = 29;
+ final int TUPLE = 30;
final String CHOOSE = " CHOOSE(X) == \"a member of X\"; EXTERNAL_FUNCTION_CHOOSE(T) == (POW(T)-->T)";
final String IF_THEN_ELSE = " IF_THEN_ELSE(P, a, b) == (%t_.(t_ = TRUE & P = TRUE | a )\\/%t_.(t_= TRUE & not(P= TRUE) | b ))(TRUE)";
diff --git a/src/main/java/de/tla2b/output/ASTPrettyPrinter.java b/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
index c19d2f6..b326af6 100644
--- a/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
+++ b/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
@@ -9,6 +9,7 @@ import de.be4.classicalb.core.parser.analysis.ExtendedDFAdapter;
import de.be4.classicalb.core.parser.node.AAbstractMachineParseUnit;
import de.be4.classicalb.core.parser.node.AAnySubstitution;
import de.be4.classicalb.core.parser.node.ABecomesSuchSubstitution;
+import de.be4.classicalb.core.parser.node.AConjunctPredicate;
import de.be4.classicalb.core.parser.node.ADefinitionExpression;
import de.be4.classicalb.core.parser.node.ADefinitionPredicate;
import de.be4.classicalb.core.parser.node.AExpressionDefinitionDefinition;
@@ -33,6 +34,7 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
private final StringBuilder builder = new StringBuilder();
private final StringBuilder sb = new StringBuilder();
private Renamer renamer;
+ private final Indentation indentation;
private static final int no = 0;
private static final int left = 1;
@@ -41,11 +43,14 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
private final static Hashtable<String, NodeInfo> infoTable = new Hashtable<String, NodeInfo>();
- public ASTPrettyPrinter(Renamer renamer) {
+ public ASTPrettyPrinter(Start start, Renamer renamer) {
this.renamer = renamer;
+
+ this.indentation = new Indentation(start);
}
- public ASTPrettyPrinter() {
+ public ASTPrettyPrinter(Start start) {
+ this.indentation = new Indentation(start);
}
private static void putInfixOperator(String nodeName, String symbol,
@@ -251,7 +256,6 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
@Override
public void defaultIn(final Node node) {
- super.defaultIn(node);
if (makeBrackets(node)) {
sb.append("(");
}
@@ -259,6 +263,30 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
builder.append(node.getClass().getSimpleName());
builder.append("(");
}
+
+ @Override
+ public void defaultCase(final Node node) {
+ super.defaultCase(node);
+ if (node instanceof Token) {
+ builder.append(((Token) node).getText());
+
+ sb.append(((Token) node).getText());
+ } else {
+ builder.append(node.toString());
+ sb.append(node.toString());
+ }
+
+ }
+
+ @Override
+ public void defaultOut(final Node node) {
+ builder.append(")");
+ sb.append(getInfo(node).end);
+ if (makeBrackets(node)) {
+ sb.append(")");
+ }
+ }
+
private boolean makeBrackets(Node node) {
NodeInfo infoNode = getInfo(node);
@@ -287,40 +315,15 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
}
- @Override
- public void defaultCase(final Node node) {
- super.defaultCase(node);
- if (node instanceof Token) {
- builder.append(((Token) node).getText());
-
- sb.append(((Token) node).getText());
- } else {
- builder.append(node.toString());
- sb.append(node.toString());
- }
-
- }
-
- @Override
- public void defaultOut(final Node node) {
- super.defaultOut(node);
- builder.append(")");
- sb.append(getInfo(node).end);
- if (makeBrackets(node)) {
- sb.append(")");
- }
- }
-
- @Override
public void beginList(final Node parent) {
builder.append('[');
sb.append(getInfo(parent).beginList);
}
@Override
- public void betweenListElements(final Node parent) {
+ public void betweenListElements(final Node node) {
builder.append(',');
- sb.append(getInfo(parent).betweenListElements);
+ sb.append(getInfo(node).betweenListElements);
}
@Override
@@ -330,9 +333,12 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
}
@Override
- public void betweenChildren(final Node parent) {
+ public void betweenChildren(final Node node) {
builder.append(',');
- sb.append(getInfo(parent).betweenChildren);
+ if(indentation.printNewLineInTheMiddle(node)){
+ sb.append("\n");
+ }
+ sb.append(getInfo(node).betweenChildren);
}
@Override
@@ -621,6 +627,11 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
node.getExpression().apply(this);
sb.append(")");
}
+
+ public void inAConjunctPredicate(AConjunctPredicate node)
+ {
+ super.inAConjunctPredicate(node);
+ }
}
@@ -702,6 +713,7 @@ 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/tla2b/output/Indentation.java b/src/main/java/de/tla2b/output/Indentation.java
new file mode 100644
index 0000000..55e950d
--- /dev/null
+++ b/src/main/java/de/tla2b/output/Indentation.java
@@ -0,0 +1,55 @@
+package de.tla2b.output;
+
+import java.util.HashSet;
+import java.util.Hashtable;
+
+import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
+import de.be4.classicalb.core.parser.node.AConjunctPredicate;
+import de.be4.classicalb.core.parser.node.APredicateDefinitionDefinition;
+import de.be4.classicalb.core.parser.node.APropertiesMachineClause;
+import de.be4.classicalb.core.parser.node.Node;
+import de.be4.classicalb.core.parser.node.Start;
+
+public class Indentation extends DepthFirstAdapter {
+
+ private Hashtable<Node, Integer> indentation = new Hashtable<Node, Integer>();
+ private HashSet<Node> newlineMiddle = new HashSet<Node>();
+
+ public Indentation(Start start) {
+ start.apply(this);
+ }
+
+ public void inAPropertiesMachineClause(APropertiesMachineClause node) {
+ indentation.put(node.getPredicates(), 0);
+ }
+
+ @Override
+ public void inAConjunctPredicate(AConjunctPredicate node) {
+ Integer indent = indentation.get(node);
+ if (indent != null) {
+ indentation.put(node.getLeft(), indent);
+ indentation.put(node.getRight(), indent);
+
+ newlineMiddle.add(node);
+
+ }
+ }
+
+ public void inAPredicateDefinitionDefinition(APredicateDefinitionDefinition node)
+ {
+ indentation.put(node.getRhs(), 0);
+ }
+
+
+ public boolean printNewLineInTheMiddle(Node node) {
+ return newlineMiddle.contains(node);
+ }
+
+ public Integer getIndent(Node node) {
+ Integer res = indentation.get(node);
+ if (res == null) {
+ res = 0;
+ }
+ return res;
+ }
+}
diff --git a/src/main/java/de/tla2b/translation/OperationsFinder.java b/src/main/java/de/tla2b/translation/OperationsFinder.java
index cf92e6b..05fd928 100644
--- a/src/main/java/de/tla2b/translation/OperationsFinder.java
+++ b/src/main/java/de/tla2b/translation/OperationsFinder.java
@@ -102,7 +102,7 @@ public class OperationsFinder extends AbstractASTVisitor implements
for (int i = 0; i < n.getArgs().length; i++) {
exists = new ArrayList<OpApplNode>(oldExists);
- currentName = oldName;
+ currentName = oldName + i;
visitExprOrOpArgNode(n.getArgs()[i]);
}
return;
@@ -114,7 +114,7 @@ public class OperationsFinder extends AbstractASTVisitor implements
for (int i = 0; i < n.getArgs().length; i++) {
exists = new ArrayList<OpApplNode>(oldExists);
- currentName = oldName;
+ currentName = oldName+ i;
visitExprOrOpArgNode(n.getArgs()[i]);
}
return;
diff --git a/src/main/java/de/tla2b/types/TupleOrFunction.java b/src/main/java/de/tla2b/types/TupleOrFunction.java
index cf32443..2ef5303 100644
--- a/src/main/java/de/tla2b/types/TupleOrFunction.java
+++ b/src/main/java/de/tla2b/types/TupleOrFunction.java
@@ -1,14 +1,12 @@
package de.tla2b.types;
import java.util.ArrayList;
-import java.util.Collections;
import java.util.Iterator;
import java.util.LinkedHashMap;
import java.util.List;
import java.util.Map.Entry;
import de.be4.classicalb.core.parser.node.PExpression;
-import de.tla2b.exceptions.TypeErrorException;
import de.tla2b.exceptions.UnificationException;
import de.tla2b.output.TypeVisitorInterface;
@@ -28,13 +26,9 @@ public class TupleOrFunction extends AbstractHasFollowers {
}
public static TLAType createTupleOrFunctionType(List<TLAType> list) {
- if (comparable(list)) {
- TupleOrFunction tOrF = new TupleOrFunction();
- tOrF.add(list);
- return tOrF;
- } else {
- return new TupleType(list);
- }
+ TupleOrFunction tOrF = new TupleOrFunction();
+ tOrF.add(list);
+ return tOrF.update();
}
public void add(List<TLAType> list) {
@@ -53,45 +47,20 @@ public class TupleOrFunction extends AbstractHasFollowers {
@Override
public String toString() {
- FunctionType func = new FunctionType();
- func.setDomain(IntType.getInstance());
- func.setRange(new UntypedType());
- FunctionType res;
- try {
- res = func.unify(this);
- return res.toString();
- } catch (UnificationException e) {
- // tuple
- boolean isTuple = true;
- ArrayList<TLAType> typeList = new ArrayList<TLAType>();
- for (int i = 1; i <= types.keySet().size(); i++) {
- if (types.keySet().contains(i)) {
- typeList.add(types.get(i));
- } else {
- isTuple = false;
- break;
- }
- }
-
- if (isTuple) {
- return new TupleType(typeList).toString();
- } else {
- StringBuilder sb = new StringBuilder();
- sb.append("(");
- for (Iterator<Integer> keys = types.keySet().iterator(); keys
- .hasNext();) {
- Integer key = keys.next();
- sb.append(key);
- sb.append(" : ").append(types.get(key));
- if (keys.hasNext())
- sb.append(", ");
- }
- sb.append(")");
- throw new RuntimeException("Type " + sb + "is incomplete");
- }
+ StringBuilder sb = new StringBuilder();
+ sb.append("TupleOrFunction");
+ sb.append("(");
+ for (Iterator<Integer> keys = types.keySet().iterator(); keys.hasNext();) {
+ Integer key = keys.next();
+ sb.append(key);
+ sb.append(" : ").append(types.get(key));
+ if (keys.hasNext())
+ sb.append(", ");
}
-
+ sb.append(")");
+ return sb.toString();
+ // throw new RuntimeException("Type " + sb + "is incomplete");
}
@Override
@@ -134,12 +103,12 @@ public class TupleOrFunction extends AbstractHasFollowers {
}
}
-
+
}
@Override
public boolean compare(TLAType o) {
- if (this.contains(o) || o.contains(this)){
+ if (this.contains(o) || o.contains(this)) {
return false;
}
if (o.getKind() == UNTYPED)
@@ -186,19 +155,8 @@ public class TupleOrFunction extends AbstractHasFollowers {
return true;
}
-
-// if (o instanceof TupleOrFunction) {
-// TupleOrFunction t = (TupleOrFunction) o;
-// for (Entry<Integer, TLAType> entry : types.entrySet()) {
-// if (t.types.containsKey(entry.getKey())
-// && entry.getValue()
-// .compare(t.types.get(entry.getKey()))) {
-// return false;
-// }
-// }
-// }
-
- // this type is not comparable with all other types
+
+ // this type is not comparable to all other types
return false;
}
@@ -225,6 +183,9 @@ public class TupleOrFunction extends AbstractHasFollowers {
@Override
public boolean isUntyped() {
+// if (complete == false) {
+// return true;
+// }
for (TLAType type : types.values()) {
if (type.isUntyped())
return true;
@@ -270,13 +231,14 @@ public class TupleOrFunction extends AbstractHasFollowers {
}
if (o instanceof TupleType) {
TupleType tupleType = (TupleType) o;
-
+
List<TLAType> typeList = new ArrayList<TLAType>();
for (int i = 0; i < tupleType.getTypes().size(); i++) {
- if(this.types.containsKey(i+1)){
- TLAType res = tupleType.getTypes().get(i).unify(this.types.get(i+1));
+ if (this.types.containsKey(i + 1)) {
+ TLAType res = tupleType.getTypes().get(i)
+ .unify(this.types.get(i + 1));
typeList.add(res);
- }else {
+ } else {
typeList.add(tupleType.getTypes().get(i));
}
}
@@ -284,71 +246,61 @@ public class TupleOrFunction extends AbstractHasFollowers {
this.setFollowersTo(r);
tupleType.setFollowersTo(r);
return r;
-
-// int max = Collections.max(types.keySet());
-// if (max <= tupleType.getTypes().size()) {
-// for (Entry<Integer, TLAType> entry : this.types.entrySet()) {
-// int index = entry.getKey();
-// TLAType type = entry.getValue();
-// if (type instanceof AbstractHasFollowers) {
-// ((AbstractHasFollowers) type).removeFollower(this);
-// }
-// TLAType elementOfTuple = tupleType.getTypes()
-// .get(index - 1);
-// elementOfTuple.unify(type);
-// }
-// return tupleType;
-// } else {
-// TLAType range = new UntypedType();
-// for (TLAType type : types.values()) {
-// if (type instanceof AbstractHasFollowers) {
-// ((AbstractHasFollowers) type).removeFollower(this);
-// }
-// range = range.unify(type);
-// }
-// FunctionType funcType = new FunctionType(IntType.getInstance(),
-// range);
-// return funcType.unify(tupleType);
-// }
}
if (o instanceof TupleOrFunction) {
TupleOrFunction other = (TupleOrFunction) o;
- if (isTupleOrFunction(this, other)) {
- for (Integer i : this.types.keySet()) {
- if (other.types.containsKey(i)) {
- TLAType res = this.types.get(i).unify(
- other.types.get(i));
- if (res instanceof AbstractHasFollowers) {
- ((AbstractHasFollowers) res).addFollower(this);
- }
- this.types.put(i, res);
- }
+ for (Integer i : other.types.keySet()) {
+ if(this.types.containsKey(i)){
+ TLAType res = other.types.get(i).unify(this.types.get(i));
+ if(res instanceof AbstractHasFollowers)
+ ((AbstractHasFollowers) res).addFollower(this);
+ this.types.put(i, res);
+ }else{
+ TLAType res = other.types.get(i);
+ if(res instanceof AbstractHasFollowers)
+ ((AbstractHasFollowers) res).addFollower(this);
+ this.types.put(i, res);
}
- for (Integer i : other.types.keySet()) {
- if (!this.types.containsKey(i)) {
- TLAType res = other.types.get(i);
- if (res instanceof AbstractHasFollowers) {
- ((AbstractHasFollowers) res).addFollower(this);
- }
- this.types.put(i, res);
- }
- }
- return this;
- } else{
- ArrayList<TLAType> list1 = new ArrayList<TLAType>();
- for (int i = 1; i <= types.keySet().size(); i++) {
- list1.add(types.get(i));
- }
- TupleType tuple1 = new TupleType(list1);
- ArrayList<TLAType> list2 = new ArrayList<TLAType>();
- for (int i = 1; i <= other.types.keySet().size(); i++) {
- list2.add(other.types.get(i));
- }
- TupleType tuple2 = new TupleType(list2);
- return tuple1.unify(tuple2);
}
+ other.setFollowersTo(this);
+ return this;
+ // if (isTupleOrFunction(this, other)) {
+// for (Integer i : this.types.keySet()) {
+// if (other.types.containsKey(i)) {
+// TLAType res = this.types.get(i).unify(
+// other.types.get(i));
+// if (res instanceof AbstractHasFollowers) {
+// ((AbstractHasFollowers) res).addFollower(this);
+// }
+// this.types.put(i, res);
+// }
+// }
+// for (Integer i : other.types.keySet()) {
+// if (!this.types.containsKey(i)) {
+// TLAType res = other.types.get(i);
+// if (res instanceof AbstractHasFollowers) {
+// ((AbstractHasFollowers) res).addFollower(this);
+// }
+// this.types.put(i, res);
+// }
+// }
+// return this;
+// } else {
+// ArrayList<TLAType> list1 = new ArrayList<TLAType>();
+// for (int i = 1; i <= types.keySet().size(); i++) {
+// list1.add(types.get(i));
+// }
+// TupleType tuple1 = new TupleType(list1);
+//
+// ArrayList<TLAType> list2 = new ArrayList<TLAType>();
+// for (int i = 1; i <= other.types.keySet().size(); i++) {
+// list2.add(other.types.get(i));
+// }
+// TupleType tuple2 = new TupleType(list2);
+// return tuple1.unify(tuple2);
+// }
}
@@ -370,6 +322,62 @@ public class TupleOrFunction extends AbstractHasFollowers {
}
+ public TLAType getFinalType() {
+ List<TLAType> list = new ArrayList<TLAType>(this.types.values());
+
+ if (comparable(list)) {
+ FunctionType func = new FunctionType(IntType.getInstance(),
+ new UntypedType());
+ try {
+ func = func.unify(this);
+ this.setFollowersTo(func);
+ return func;
+ } catch (UnificationException e) {
+ throw new RuntimeException();
+ }
+ } else {
+ TupleType tuple = new TupleType(list);
+ this.setFollowersTo(tuple);
+ return tuple;
+ }
+
+ }
+
+ private TLAType update() {
+ List<TLAType> list = new ArrayList<TLAType>(this.types.values());
+ // if (allTyped(list) && comparable(list)) {
+ // FunctionType func = new FunctionType(IntType.getInstance(),
+ // new UntypedType());
+ // try {
+ // func = func.unify(this);
+ // this.setFollowersTo(func);
+ // return func;
+ // } catch (UnificationException e) {
+ // throw new RuntimeException();
+ // }
+ // } else
+ if (!comparable(list)) {
+ TupleType tuple = new TupleType(list);
+ this.setFollowersTo(tuple);
+ return tuple;
+
+ // boolean isTuple = true;
+ // ArrayList<TLAType> typeList = new ArrayList<TLAType>();
+ // for (int i = 1; i <= types.keySet().size(); i++) {
+ // if (types.keySet().contains(i)) {
+ // typeList.add(types.get(i));
+ // } else {
+ // isTuple = false;
+ // break;
+ // }
+ // }
+ //
+ // if (isTuple) {
+ // return new TupleType(typeList).toString();
+ }
+ return this;
+ }
+
private static boolean comparable(List<TLAType> typeList) {
for (int i = 0; i < typeList.size() - 1; i++) {
TLAType t1 = typeList.get(i);
@@ -382,4 +390,13 @@ public class TupleOrFunction extends AbstractHasFollowers {
return true;
}
+ private static boolean allTyped(List<TLAType> typeList) {
+ for (int i = 0; i < typeList.size(); i++) {
+ if (typeList.get(i).isUntyped()) {
+ return false;
+ }
+ }
+ return true;
+ }
+
}
diff --git a/src/main/java/de/tla2b/types/TupleType.java b/src/main/java/de/tla2b/types/TupleType.java
index 7e2d45e..3fb67ed 100644
--- a/src/main/java/de/tla2b/types/TupleType.java
+++ b/src/main/java/de/tla2b/types/TupleType.java
@@ -59,39 +59,15 @@ public class TupleType extends AbstractHasFollowers {
if (o instanceof TupleType) {
TupleType t = (TupleType) o;
if (this.types.size() != t.types.size()) {
- for (int i = 0; i < t.types.size(); i++) {
- if (!compareToAll(t.types.get(i))) {
- return false;
- }
- }
- // both are sequences with different lengths
- return true;
- }
- for (int i = 0; i < types.size(); i++) {
- if (!types.get(i).compare(t.types.get(i)))
- return false;
- }
- return true;
- }
- if (o instanceof FunctionType) {
- // TODO
- FunctionType func = (FunctionType) o;
- if (!(func.getDomain() instanceof IntType)) {
return false;
}
- TLAType range = func.getRange();
for (int i = 0; i < types.size(); i++) {
- if (types.get(i).compare(range)) {
- continue;
- } else {
+ if (!types.get(i).compare(t.types.get(i)))
return false;
- }
- }
- if (!compareToAll(range)) {
- return false;
}
return true;
}
+
if (o instanceof TupleOrFunction) {
return o.compare(this);
}
@@ -99,18 +75,6 @@ public class TupleType extends AbstractHasFollowers {
return false;
}
- private boolean compareToAll(TLAType other) {
- for (int i = 0; i < types.size(); i++) {
- for (int j = i + 1; j < types.size(); j++) {
- if (!types.get(i).compare(types.get(j)))
- return false;
- }
- if (!types.get(i).compare(other))
- return false;
- }
- return true;
- }
-
@Override
public boolean contains(TLAType o) {
for (TLAType tlaType : types) {
@@ -149,43 +113,16 @@ public class TupleType extends AbstractHasFollowers {
}
if (o instanceof TupleType) {
TupleType tuple = (TupleType) o;
- if (this.types.size() != tuple.types.size()) {
- TLAType t = types.get(0);
- for (int i = 1; i < types.size(); i++) {
- t = t.unify(types.get(i));
- }
- for (int i = 0; i < tuple.types.size(); i++) {
- t = t.unify(tuple.types.get(i));
- }
- return new FunctionType(IntType.getInstance(), t);
- } else {
- for (int i = 0; i < types.size(); i++) {
- TLAType res = types.get(i).unify(tuple.types.get(i));
- types.set(i, res);
- if (res instanceof AbstractHasFollowers)
- ((AbstractHasFollowers) res).addFollower(this);
- }
- return this;
+
+ for (int i = 0; i < types.size(); i++) {
+ TLAType res = types.get(i).unify(tuple.types.get(i));
+ types.set(i, res);
+ if (res instanceof AbstractHasFollowers)
+ ((AbstractHasFollowers) res).addFollower(this);
}
+ return this;
}
- if (o instanceof FunctionType) {
- // TODO
- if (compareToAll(new UntypedType())) {
- // Function
- TLAType t = types.get(0);
- for (int i = 1; i < types.size(); i++) {
- t = t.unify(types.get(i));
- }
- FunctionType func = new FunctionType(IntType.getInstance(), t);
- this.setFollowersTo(func);
- return func.unify(o);
- } else {
- TLAType res = types.get(1).unify(((FunctionType) o).getRange());
- types.set(1, res);
- return this;
- }
- }
if (o instanceof TupleOrFunction) {
return o.unify(this);
}
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 1f92618..106aa3e 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -276,6 +276,28 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
def2.setRhs(total);
list.add(def2);
}
+ if (set.contains(UsedExternalFunctions.EXTERNAL_FUNCTIONS.ASSERT)) {
+ APredicateDefinitionDefinition def1 = new APredicateDefinitionDefinition();
+ def1.setName(new TDefLiteralPredicate("ASSERT_TRUE"));
+ ArrayList<PExpression> params = new ArrayList<PExpression>();
+ params.add(createIdentifierNode("P"));
+ params.add(createIdentifierNode("Msg"));
+ def1.setParameters(params);
+ def1.setRhs(new AEqualPredicate(new AIntegerExpression(
+ new TIntegerLiteral("1")), new AIntegerExpression(
+ new TIntegerLiteral("1"))));
+ list.add(def1);
+
+ AExpressionDefinitionDefinition def2 = new AExpressionDefinitionDefinition();
+ def2.setName(new TIdentifierLiteral(
+ "EXTERNAL_PREDICATE_ASSERT_TRUE"));
+ def2.setParameters(new ArrayList<PExpression>());
+ AMultOrCartExpression cart = new AMultOrCartExpression();
+ cart.setLeft(new ABoolSetExpression());
+ cart.setRight(new AStringSetExpression());
+ def2.setRhs(cart);
+ list.add(def2);
+ }
return list;
}
@@ -299,7 +321,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
for (int j = 0; j < op.getExistQuans().size(); j++) {
OpApplNode o = op.getExistQuans().get(j);
- whereList.add(visitBounded(o));
+ whereList.add(visitBoundsOfLocalVariables(o));
}
AOperation operation = new AOperation();
@@ -362,6 +384,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
any.setThen(assign);
operation.setOperationBody(any);
// opList.add(operation);
+
opList.add(op.getBOperation(this));
}
@@ -653,16 +676,22 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
predList.add(member);
}
- if (conEval != null) {
- for (OpDefNode def : conEval.getInvariants()) {
- if (def.getOriginallyDefinedInModuleNode().getName().toString()
- .equals("MC")) {
- predList.add(visitExprNodePredicate(def.getBody()));
- } else {
+ for (OpDefNode def : specAnalyser.getInvariants()) {
+ if (def.getOriginallyDefinedInModuleNode().getName().toString()
+ .equals("MC")) {
+ predList.add(visitExprNodePredicate(def.getBody()));
+ } else {
+ if (predicateVsExpression.getDefinitionType(def) == DefinitionType.PREDICATE) {
ADefinitionPredicate defPred = new ADefinitionPredicate();
defPred.setDefLiteral(new TDefLiteralPredicate(getName(def)));
predList.add(defPred);
+ } else {
+ ADefinitionExpression defExpr = new ADefinitionExpression();
+ defExpr.setDefLiteral(new TIdentifierLiteral(getName(def)));
+ predList.add(new AEqualPredicate(defExpr,
+ new ABooleanTrueExpression()));
}
+
}
}
@@ -723,9 +752,11 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
for (int j = 0; j < seq.getArgs().length; j++) {
list.add(seq.getArgs()[j]);
}
- PExpression base = visitExprNodeExpression(at.getAtBase());
- return evalAtNode(list, type, base);
+ // PExpression base = visitExprNodeExpression(at.getAtBase());
+ PExpression base = (PExpression) at.getExceptComponentRef()
+ .getToolObject(EXCEPT_BASE);
+ return evalAtNode(list, type, (PExpression) base.clone());
}
case LetInKind: {
@@ -740,10 +771,10 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
private PExpression evalAtNode(LinkedList<ExprOrOpArgNode> list,
TLAType type, PExpression base) {
- if(list.size() == 0){
+ if (list.size() == 0) {
return base;
}
-
+
if (type instanceof FunctionType) {
FunctionType funcType = (FunctionType) type;
PExpression param = visitExprOrOpArgNodeExpression(list.poll());
@@ -760,7 +791,8 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
select.setRecord(base);
StringNode stringNode = (StringNode) list.poll();
String fieldName = stringNode.getRep().toString();
- select.setIdentifier(createIdentifierNode(fieldName)); // TODO renamed
+ select.setIdentifier(createIdentifierNode(fieldName)); // TODO
+ // renamed
return evalAtNode(list, structType.getType(fieldName), select);
}
}
@@ -769,7 +801,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
switch (n.getOperator().getKind()) {
case VariableDeclKind:
case ConstantDeclKind:
- case FormalParamKind: {
+ case FormalParamKind: { // TODO
return new AEqualPredicate(createIdentifierNode(n.getOperator()),
new ABooleanTrueExpression());
}
@@ -797,25 +829,59 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
FormalParamNode param = (FormalParamNode) n.getOperator();
ExprOrOpArgNode e = (ExprOrOpArgNode) param
.getToolObject(SUBSTITUTE_PARAM);
- if (e == null) {
- if (recursiveFunctionHandler.isRecursiveFunction(param)) {
- ArrayList<SymbolNode> list = recursiveFunctionHandler
- .getAdditionalParams(param);
- if (list.size() > 0) {
- AFunctionExpression call = new AFunctionExpression();
- call.setIdentifier(createIdentifierNode(param));
- ArrayList<PExpression> params = new ArrayList<PExpression>();
- for (SymbolNode symbolNode : list) {
- params.add(createIdentifierNode(symbolNode));
+ if (e != null) {
+ return visitExprOrOpArgNodeExpression(e);
+ }
+
+ if (recursiveFunctionHandler.isRecursiveFunction(param)) {
+ ArrayList<SymbolNode> list = recursiveFunctionHandler
+ .getAdditionalParams(param);
+ if (list.size() > 0) {
+ AFunctionExpression call = new AFunctionExpression();
+ call.setIdentifier(createIdentifierNode(param));
+ ArrayList<PExpression> params = new ArrayList<PExpression>();
+ for (SymbolNode symbolNode : list) {
+ params.add(createIdentifierNode(symbolNode));
+ }
+ call.setParameters(params);
+ return call;
+ }
+ }
+
+ FormalParamNode[] tuple = (FormalParamNode[]) param
+ .getToolObject(TUPLE);
+ if (tuple != null) {
+ if (tuple.length == 1) {
+ AFunctionExpression functionCall = new AFunctionExpression();
+ functionCall.setIdentifier(createIdentifierNode(n
+ .getOperator()));
+ List<PExpression> paramList = new ArrayList<PExpression>();
+ paramList.add(new AIntegerExpression(new TIntegerLiteral(
+ "1")));
+ functionCall.setParameters(paramList);
+ return functionCall;
+ } else {
+
+ StringBuilder sb = new StringBuilder();
+ List<TLAType> typeList = new ArrayList<TLAType>();
+ int number = -1;
+ for (int j = 0; j < tuple.length; j++) {
+ FormalParamNode p = tuple[j];
+ sb.append(p.getName().toString());
+ TLAType type = (TLAType) p.getToolObject(TYPE_ID);
+ typeList.add(type);
+ if (p == param) {
+ number = j + 1;
}
- call.setParameters(params);
- return call;
}
+ TupleType tupleType = new TupleType(typeList);
+ PExpression id = createIdentifierNode(sb.toString());
+ PExpression prj = createProjectionFunction(id, number,
+ tupleType);
+ return prj;
}
- return createIdentifierNode(n.getOperator());
- } else {
- return visitExprOrOpArgNodeExpression(e);
}
+ return createIdentifierNode(n.getOperator());
}
@@ -990,6 +1056,22 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
return new AEqualPredicate(new ABooleanFalseExpression(),
new ABooleanTrueExpression());
+ case B_OPCODE_assert: {
+ ADefinitionPredicate pred = new ADefinitionPredicate();
+ pred.setDefLiteral(new TDefLiteralPredicate("ASSERT_TRUE"));
+ ArrayList<PExpression> list = new ArrayList<PExpression>();
+ list.add(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
+ if (n.getArgs()[1] instanceof StringNode) {
+ StringNode stringNode = (StringNode) n.getArgs()[1];
+ list.add(new AStringExpression(new TStringLiteral(stringNode
+ .getRep().toString())));
+ } else {
+ list.add(new AStringExpression(new TStringLiteral("Error")));
+ }
+ pred.setParameters(list);
+ return pred;
+ }
+
}
throw new RuntimeException(n.getOperator().getName().toString());
}
@@ -1175,6 +1257,16 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
// return restrictTail;
}
+ case B_OPCODE_assert: {
+ ADefinitionPredicate pred = new ADefinitionPredicate();
+ pred.setDefLiteral(new TDefLiteralPredicate("ASSERT_TRUE"));
+ ArrayList<PExpression> list = new ArrayList<PExpression>();
+ list.add(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
+ list.add(new AStringExpression(new TStringLiteral("Error")));
+ pred.setParameters(list);
+ return new AConvertBoolExpression(pred);
+ }
+
}
throw new RuntimeException(n.getOperator().getName().toString());
}
@@ -1325,82 +1417,32 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
case OPCODE_sso: { // $SubsetOf Represents {x \in S : P}
FormalParamNode[][] params = n.getBdedQuantSymbolLists();
-
List<PExpression> list = new ArrayList<PExpression>();
- List<PExpression> list2 = new ArrayList<PExpression>();
for (int i = 0; i < params[0].length; i++) {
FormalParamNode p = params[0][i];
list.add(createIdentifierNode(p));
- list2.add(createIdentifierNode(p));
}
-
AComprehensionSetExpression compre = new AComprehensionSetExpression();
compre.setIdentifiers(list);
-
- AMemberPredicate member = new AMemberPredicate();
- if (list2.size() == 1) {
- member.setLeft(list2.get(0));
- } else {
- member.setLeft(new ACoupleExpression(list2));
- }
-
- ExprNode in = n.getBdedQuantBounds()[0];
- member.setRight(visitExprNodeExpression(in));
-
- AConjunctPredicate conj = new AConjunctPredicate(member,
+ PPredicate typing = visitBoundsOfFunctionsVariables(n);
+ AConjunctPredicate conj = new AConjunctPredicate(typing,
visitExprOrOpArgNodePredicate(n.getArgs()[0]));
compre.setPredicates(conj);
return compre;
}
case OPCODE_soa: { // $SetOfAll Represents {e : p1 \in S, p2,p3 \in S2}
-
- AExistsPredicate exist = new AExistsPredicate();
FormalParamNode[][] params = n.getBdedQuantSymbolLists();
-
- List<PExpression> idList = new ArrayList<PExpression>();
+ List<PExpression> idList = createListOfIdentifier(params);
List<PPredicate> predList = new ArrayList<PPredicate>();
- for (int i = 0; i < params.length; i++) {
- if (n.isBdedQuantATuple()[i]) {
- List<PExpression> list = new ArrayList<PExpression>();
- for (FormalParamNode formalParam : params[i]) {
- list.add(createIdentifierNode(formalParam));
- idList.add(createIdentifierNode(formalParam));
- }
- ACoupleExpression couple = new ACoupleExpression(list);
- AMemberPredicate member = new AMemberPredicate();
- member.setLeft(couple);
- ExprNode in = n.getBdedQuantBounds()[i];
- member.setRight(visitExprNodeExpression(in));
- predList.add(member);
- } else {
- for (FormalParamNode formalParam : params[i]) {
- AMemberPredicate member = new AMemberPredicate();
- member.setLeft(createIdentifierNode(formalParam));
- ExprNode in = n.getBdedQuantBounds()[i];
- member.setRight(visitExprNodeExpression(in));
- predList.add(member);
- idList.add(createIdentifierNode(formalParam));
- }
- }
-
- }
- // for (int i = 0; i < bounds.length; i++) {
- //
- // FormalParamNode p = params[i][0];
- // AMemberPredicate member = new AMemberPredicate();
- // member.setLeft(createIdentifierNode(p));
- // ExprNode in = n.getBdedQuantBounds()[i];
- // member.setRight(visitExprNodeExpression(in));
- // predList.add(member);
- // idList.add(createIdentifierNode(p));
- // }
+ predList.add(visitBoundsOfLocalVariables(n));
final String nameOfTempVariable = "t_";
AEqualPredicate equals = new AEqualPredicate();
equals.setLeft(createIdentifierNode(nameOfTempVariable));
equals.setRight(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
predList.add(equals);
+ AExistsPredicate exist = new AExistsPredicate();
exist.setIdentifiers(idList);
exist.setPredicate(createConjunction(predList));
@@ -1418,21 +1460,36 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
FormalParamNode[][] params = n.getBdedQuantSymbolLists();
// ExprNode[] bounds = n.getBdedQuantBounds(); TODO
List<PExpression> idList = new ArrayList<PExpression>();
- List<PPredicate> predList = new ArrayList<PPredicate>();
for (int i = 0; i < params.length; i++) {
for (int j = 0; j < params[i].length; j++) {
FormalParamNode p = params[i][j];
- AMemberPredicate member = new AMemberPredicate();
- member.setLeft(createIdentifierNode(p));
- ExprNode in = n.getBdedQuantBounds()[i];
- member.setRight(visitExprNodeExpression(in));
- predList.add(member);
idList.add(createIdentifierNode(p));
}
}
+
+ boolean[] isTuple = n.isBdedQuantATuple();
+
ALambdaExpression lambda = new ALambdaExpression();
- lambda.setIdentifiers(idList);
- lambda.setPredicate(createConjunction(predList));
+ List<PExpression> idList2 = new ArrayList<PExpression>();
+ for (int i = 0; i < params.length; i++) {
+ if (isTuple[i] && i > 0) {
+ StringBuilder sb = new StringBuilder();
+ for (int j = 0; j < params[i].length; j++) {
+ FormalParamNode p = params[i][j];
+ sb.append(p.getName().toString());
+
+ }
+ idList2.add(createIdentifierNode(sb.toString()));
+ } else {
+ for (int j = 0; j < params[i].length; j++) {
+ FormalParamNode p = params[i][j];
+ idList2.add(createIdentifierNode(p.getName().toString()));
+ }
+ }
+ }
+
+ lambda.setIdentifiers(idList2);
+ lambda.setPredicate(visitBoundsOfFunctionsVariables(n));
lambda.setExpression(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
if (recursiveFunctionHandler.isRecursiveFunction(n)) {
@@ -1466,7 +1523,8 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
if (t != null && t instanceof TupleType) {
NumeralNode num = (NumeralNode) n.getArgs()[1];
int field = num.val();
- return createProjectionFunction(n, field, t);
+ PExpression pair = visitExprOrOpArgNodeExpression(n.getArgs()[0]);
+ return createProjectionFunction(pair, field, t);
} else {
AFunctionExpression func = new AFunctionExpression();
func.setIdentifier(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
@@ -1477,10 +1535,21 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
&& ((OpApplNode) dom).getOperator().getName()
.toString().equals("$Tuple")) {
OpApplNode domOpAppl = (OpApplNode) dom;
- for (int i = 0; i < domOpAppl.getArgs().length; i++) {
- paramList.add(visitExprOrOpArgNodeExpression(domOpAppl
- .getArgs()[i]));
+ if (domOpAppl.getArgs().length == 1) {
+ List<PExpression> list = new ArrayList<PExpression>();
+ list.add(visitExprOrOpArgNodeExpression(domOpAppl
+ .getArgs()[0]));
+ ASequenceExtensionExpression seq = new ASequenceExtensionExpression(
+ list);
+ paramList.add(seq);
+ } else {
+ for (int i = 0; i < domOpAppl.getArgs().length; i++) {
+ paramList
+ .add(visitExprOrOpArgNodeExpression(domOpAppl
+ .getArgs()[i]));
+ }
}
+
} else {
paramList.add(visitExprOrOpArgNodeExpression(dom));
}
@@ -1517,9 +1586,14 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
case OPCODE_cp: // $CartesianProd A \X B \X C
- return new AMultOrCartExpression(
- visitExprOrOpArgNodeExpression(n.getArgs()[0]),
- visitExprOrOpArgNodeExpression(n.getArgs()[1]));
+ {
+ PExpression first = visitExprOrOpArgNodeExpression(n.getArgs()[0]);
+ for (int i = 1; i < n.getArgs().length; i++) {
+ PExpression second = visitExprOrOpArgNodeExpression(n.getArgs()[i]);
+ first = new AMultOrCartExpression(first, second);
+ }
+ return first;
+ }
case OPCODE_sor: { // $SetOfRcds [L1 : e1, L2 : e2]
SetType pow = (SetType) n.getToolObject(TYPE_ID);
@@ -1633,7 +1707,8 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
case OPCODE_rs: { // $RcdSelect r.c
- StructType struct = (StructType) n.getToolObject(TYPE_ID);
+ StructType struct = (StructType) n.getArgs()[0]
+ .getToolObject(TYPE_ID);
if (struct.isExtensible()) {
ARecordFieldExpression rcdSelect = new ARecordFieldExpression();
rcdSelect
@@ -1701,15 +1776,15 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
return createCaseNode(n);
}
- case OPCODE_exc: // Except
+ case OPCODE_exc: // $Except
{
TLAType type = (TLAType) n.getToolObject(TYPE_ID);
+
if (type.getKind() == IType.STRUCT) {
StructType structType = (StructType) type;
- Hashtable<String, PExpression> temp = new Hashtable<String, PExpression>();
+ PExpression res = visitExprOrOpArgNodeExpression(n.getArgs()[0]);
for (int i = 1; i < n.getArgs().length; i++) {
OpApplNode pair = (OpApplNode) n.getArgs()[i];
-
ExprOrOpArgNode first = pair.getArgs()[0];
ExprOrOpArgNode val = pair.getArgs()[1];
OpApplNode seq = (OpApplNode) first;
@@ -1719,44 +1794,16 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
seqList.add(seq.getArgs()[j]);
}
- PExpression oldRec = visitExprOrOpArgNodeExpression(n
- .getArgs()[0]);
- //PExpression val = visitExprOrOpArgNodeExpression(second);
- ARecordFieldExpression select = new ARecordFieldExpression();
- select.setRecord(oldRec);
-
- StringNode stringNode = (StringNode) seqList.poll();
- String fieldName = stringNode.getRep().toString();
- select.setIdentifier(createIdentifierNode(fieldName));
-
- PExpression value = evalExceptValue(select,
- seqList, structType.getType(fieldName), val);
-
- temp.put(fieldName, value);
+ pair.setToolObject(EXCEPT_BASE, res.clone());
+ res = evalExceptValue((PExpression) res.clone(), seqList,
+ structType, val);
}
+ return res;
- StructType st = (StructType) type;
- List<PRecEntry> list = new ArrayList<PRecEntry>();
- for (int i = 0; i < st.getFields().size(); i++) {
- ARecEntry entry = new ARecEntry();
- String fieldName = st.getFields().get(i);
- entry.setIdentifier(createIdentifierNode(fieldName));
- PExpression value = temp.get(fieldName);
- if (value == null) {
- value = new ARecordFieldExpression(
- visitExprOrOpArgNodeExpression(n.getArgs()[0]),
- createIdentifierNode(fieldName)); // TODO
- // renamed
- }
- entry.setValue(value);
- list.add(entry);
- }
- ARecExpression rec = new ARecExpression(list);
- return rec;
} else {
FunctionType func = (FunctionType) type;
- List<PExpression> list = new ArrayList<PExpression>();
+ PExpression res = visitExprOrOpArgNodeExpression(n.getArgs()[0]);
for (int i = 1; i < n.getArgs().length; i++) {
OpApplNode pair = (OpApplNode) n.getArgs()[i];
@@ -1769,32 +1816,11 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
seqList.add(seq.getArgs()[j]);
}
- PExpression oldFunc = visitExprOrOpArgNodeExpression(n
- .getArgs()[0]);
- PExpression firstArg = visitExprOrOpArgNodeExpression(seqList
- .poll());
- AFunctionExpression funcApplication = new AFunctionExpression();
- funcApplication.setIdentifier(oldFunc);
- List<PExpression> argList = new ArrayList<PExpression>();
- argList.add(firstArg);
- funcApplication.setParameters(argList);
-
- PExpression value = evalExceptValue(funcApplication,
- seqList, func.getRange(), val);
- ACoupleExpression couple = new ACoupleExpression();
- List<PExpression> coupleList = new ArrayList<PExpression>();
- coupleList.add(firstArg);
- coupleList.add(value);
- couple.setList(coupleList);
- list.add(couple);
+ pair.setToolObject(EXCEPT_BASE, res.clone());
+ res = evalExceptValue((PExpression) res.clone(), seqList,
+ func, val);
}
- ASetExtensionExpression setExtension = new ASetExtensionExpression(
- list);
- AOverwriteExpression overwrite = new AOverwriteExpression();
- overwrite
- .setLeft(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
- overwrite.setRight(setExtension);
- return overwrite;
+ return res;
}
}
@@ -1820,7 +1846,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
}
AImplicationPredicate implication = new AImplicationPredicate();
- implication.setLeft(visitBounded(n));
+ implication.setLeft(visitBoundsOfLocalVariables(n));
implication.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
return new AConvertBoolExpression(new AForallPredicate(list,
implication));
@@ -1835,7 +1861,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
}
AConjunctPredicate conjunction = new AConjunctPredicate();
- conjunction.setLeft(visitBounded(n));
+ conjunction.setLeft(visitBoundsOfLocalVariables(n));
conjunction.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
AExistsPredicate exists = new AExistsPredicate(list, conjunction);
return new AConvertBoolExpression(exists);
@@ -1846,6 +1872,17 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
throw new RuntimeException(n.getOperator().getName().toString());
}
+ private List<PExpression> createListOfIdentifier(FormalParamNode[][] params) {
+ List<PExpression> list = new ArrayList<PExpression>();
+ for (int i = 0; i < params.length; i++) {
+ for (int j = 0; j < params[i].length; j++) {
+ FormalParamNode param = params[i][j];
+ list.add(createIdentifierNode(param));
+ }
+ }
+ return list;
+ }
+
private PExpression evalExceptValue(PExpression prefix,
LinkedList<ExprOrOpArgNode> seqList, TLAType tlaType,
ExprOrOpArgNode val) {
@@ -1864,23 +1901,22 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
ARecEntry entry = new ARecEntry();
String fieldName = structType.getFields().get(i);
entry.setIdentifier(createIdentifierNode(fieldName));
-
+
PExpression value = null;
ARecordFieldExpression select = new ARecordFieldExpression();
- select.setRecord((PExpression)prefix.clone());
+ select.setRecord((PExpression) prefix.clone());
select.setIdentifier(createIdentifierNode(fieldName));
- if(fieldName.equals(field)){
-
- value = evalExceptValue(select, seqList, structType.getType(fieldName),
- val);
- }else{
+ if (fieldName.equals(field)) {
+ value = evalExceptValue(select, seqList,
+ structType.getType(fieldName), val);
+ } else {
value = select;
}
entry.setValue(value);
list.add(entry);
-
+
}
-
+
ARecExpression rec = new ARecExpression(list);
return rec;
@@ -1910,7 +1946,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
}
- private PExpression createProjectionFunction(OpApplNode n, int field,
+ private PExpression createProjectionFunction(PExpression pair, int field,
TLAType t) {
TupleType tuple = (TupleType) t;
int size = tuple.getTypes().size();
@@ -1930,7 +1966,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
for (int i = 0; i < field - 1; i++) {
typeList.add(tuple.getTypes().get(i));
}
- second.setExp1(createNestedCoupleAsBNode(typeList));
+ second.setExp1(createNestedCouple(typeList));
second.setExp2(tuple.getTypes().get(field - 1).getBNode());
returnFunc.setIdentifier(second);
}
@@ -1942,7 +1978,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
for (int j = 0; j < i; j++) {
typeList.add(tuple.getTypes().get(j));
}
- first.setExp1(createNestedCoupleAsBNode(typeList));
+ first.setExp1(createNestedCouple(typeList));
first.setExp2(tuple.getTypes().get(i).getBNode());
newfunc.setIdentifier(first);
@@ -1952,12 +1988,12 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
func = newfunc;
}
ArrayList<PExpression> list = new ArrayList<PExpression>();
- list.add(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
+ list.add(pair);
func.setParameters(list);
return returnFunc;
}
- public static PExpression createNestedCoupleAsBNode(List<TLAType> typeList) {
+ public static PExpression createNestedCouple(List<TLAType> typeList) {
if (typeList.size() == 1) {
return typeList.get(0).getBNode();
}
@@ -2118,7 +2154,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
}
AConjunctPredicate conjunction = new AConjunctPredicate();
- conjunction.setLeft(visitBounded(n));
+ conjunction.setLeft(visitBoundsOfLocalVariables(n));
conjunction.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
return new AExistsPredicate(list, conjunction);
}
@@ -2132,7 +2168,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
}
AImplicationPredicate implication = new AImplicationPredicate();
- implication.setLeft(visitBounded(n));
+ implication.setLeft(visitBoundsOfLocalVariables(n));
implication.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
return new AForallPredicate(list, implication);
}
@@ -2282,7 +2318,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
throw new RuntimeException(n.getOperator().getName().toString());
}
- public PPredicate visitBounded(OpApplNode n) {
+ public PPredicate visitBoundsOfLocalVariables(OpApplNode n) {
FormalParamNode[][] params = n.getBdedQuantSymbolLists();
ExprNode[] in = n.getBdedQuantBounds();
boolean[] isTuple = n.isBdedQuantATuple();
@@ -2290,15 +2326,87 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
List<PPredicate> predList = new ArrayList<PPredicate>();
for (int i = 0; i < params.length; i++) {
if (isTuple[i]) {
+ if (params[i].length == 1) {
+ // one-tuple is handled is translated as a sequence
+ FormalParamNode param = params[i][0];
+ AMemberPredicate member = new AMemberPredicate();
+ ASequenceExtensionExpression seq = new ASequenceExtensionExpression();
+ List<PExpression> list = new ArrayList<PExpression>();
+ list.add(createIdentifierNode(param));
+ seq.setExpression(list);
+ member.setLeft(seq);
+ member.setRight(visitExprNodeExpression(in[i]));
+ predList.add(member);
- ArrayList<PExpression> list = new ArrayList<PExpression>();
+ } else {
+ ArrayList<PExpression> list = new ArrayList<PExpression>();
+ for (int j = 0; j < params[i].length; j++) {
+ FormalParamNode param = params[i][j];
+ list.add(createIdentifierNode(param));
+ }
+ AMemberPredicate member = new AMemberPredicate();
+ member.setLeft(new ACoupleExpression(list));
+ member.setRight(visitExprNodeExpression(in[i]));
+ predList.add(member);
+ }
+ } else {
for (int j = 0; j < params[i].length; j++) {
- list.add(createIdentifierNode(params[i][j]));
+ AMemberPredicate member = new AMemberPredicate();
+ member.setLeft(createIdentifierNode(params[i][j]));
+ member.setRight(visitExprNodeExpression(in[i]));
+ predList.add(member);
+ }
+ }
+ }
+ return createConjunction(predList);
+ }
+
+ public PPredicate visitBoundsOfFunctionsVariables(OpApplNode n) {
+ FormalParamNode[][] params = n.getBdedQuantSymbolLists();
+ ExprNode[] in = n.getBdedQuantBounds();
+ boolean[] isTuple = n.isBdedQuantATuple();
+
+ List<PPredicate> predList = new ArrayList<PPredicate>();
+ for (int i = 0; i < params.length; i++) {
+ if (isTuple[i]) {
+ if (params[i].length == 1) { // one-tuple is handled as a
+ // sequence
+ FormalParamNode param = params[i][0];
+ param.setToolObject(TUPLE, params[i]);
+
+ AMemberPredicate member = new AMemberPredicate();
+ member.setLeft(createIdentifierNode(param));
+ member.setRight(visitExprNodeExpression(in[i]));
+ predList.add(member);
+
+ } else if (i == 0) {
+ ArrayList<PExpression> list = new ArrayList<PExpression>();
+ for (int j = 0; j < params[i].length; j++) {
+ FormalParamNode param = params[i][j];
+ list.add(createIdentifierNode(param));
+ }
+ AMemberPredicate member = new AMemberPredicate();
+ member.setLeft(new ACoupleExpression(list));
+ member.setRight(visitExprNodeExpression(in[i]));
+ predList.add(member);
+ } else {
+ ArrayList<PExpression> list = new ArrayList<PExpression>();
+ StringBuilder sb = new StringBuilder();
+ for (int j = 0; j < params[i].length; j++) {
+ FormalParamNode param = params[i][j];
+ if (i > 0) { // do not use prj1 & prj2 if it is the
+ // first tuple
+ param.setToolObject(TUPLE, params[i]);
+ }
+ sb.append(param.getName().toString());
+ list.add(createIdentifierNode(param));
+ }
+ PExpression id = createIdentifierNode(sb.toString());
+ AMemberPredicate member = new AMemberPredicate();
+ member.setLeft(id);
+ member.setRight(visitExprNodeExpression(in[i]));
+ predList.add(member);
}
- AMemberPredicate member = new AMemberPredicate();
- member.setLeft(new ACoupleExpression(list));
- member.setRight(visitExprNodeExpression(in[i]));
- predList.add(member);
} else {
for (int j = 0; j < params[i].length; j++) {
AMemberPredicate member = new AMemberPredicate();
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index f3fbf42..3f6ce1f 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -308,7 +308,7 @@ public class Translator implements TranslationGlobals {
}
Renamer renamer = new Renamer(BAst);
- ASTPrettyPrinter aP = new ASTPrettyPrinter(renamer);
+ ASTPrettyPrinter aP = new ASTPrettyPrinter(BAst, renamer);
BAst.apply(aP);
StringBuilder result = aP.getResultAsStringbuilder();
result.insert(0, "/*@ generated by TLA2B " + VERSION + " " + new Date()
diff --git a/src/test/java/de/tla2b/prettyprintb/ExampleFilesTest.java b/src/test/java/de/tla2b/prettyprintb/ExampleFilesTest.java
index efbb272..8aa65fa 100644
--- a/src/test/java/de/tla2b/prettyprintb/ExampleFilesTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/ExampleFilesTest.java
@@ -36,7 +36,7 @@ public class ExampleFilesTest extends AbstractParseModuleTest {
Start start = t.translate();
String resultTree = TestUtil.getTreeAsString(start);
- ASTPrettyPrinter aP = new ASTPrettyPrinter();
+ ASTPrettyPrinter aP = new ASTPrettyPrinter(start);
start.apply(aP);
System.out.println(aP.getResultString());
diff --git a/src/test/java/de/tla2b/prettyprintb/ExceptTest.java b/src/test/java/de/tla2b/prettyprintb/ExceptTest.java
index 790abff..c7c399f 100644
--- a/src/test/java/de/tla2b/prettyprintb/ExceptTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/ExceptTest.java
@@ -17,8 +17,25 @@ public class ExceptTest {
+ "=================================";
final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
- + "PROPERTIES " + " k : BOOL +-> INTEGER "
- + "& k = k <+ {TRUE |-> 0, FALSE |-> 0}" + "END";
+ + "PROPERTIES "
+ + "k : BOOL +-> INTEGER & k = (k <+ {(TRUE,0)}) <+ {(FALSE,0)} \n "
+ + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testFunctionExcept2() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "CONSTANTS k, k2 \n"
+ + "ASSUME k = [i \\in {3} |-> i] /\\ k2 = [k EXCEPT ![3] = @+1, ![3] = @+1] \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "CONSTANTS k, k2\n"
+ + "PROPERTIES "
+ + "(k : INTEGER +-> INTEGER & k2 : INTEGER +-> INTEGER) & (k = %(i).(i : {3} | i) & k2 = (k <+ {(3,k(3) + 1)}) <+ {(3,(k <+ {(3,k(3) + 1)})(3) + 1)}) \n "
+ + "END";
compare(expected, module);
}
@@ -36,6 +53,21 @@ public class ExceptTest {
+ "END";
compare(expected, module);
}
+
+ @Test
+ public void testFunctionTuple() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "CONSTANTS k \n"
+ + "ASSUME k = [i \\in {3,4}, j \\in {5,6} |-> i+j] /\\ k # [k EXCEPT ![3,5] = 1] \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+ + "PROPERTIES "
+ + "k : INTEGER * INTEGER +-> INTEGER & (k = %(i, j).(i : {3, 4} & j : {5, 6} | i + j) & k /= k <+ {((3,5),1)}) \n"
+ + "END";
+ compare(expected, module);
+ }
@Test
public void testNestedFunctionAt() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -60,7 +92,7 @@ public class ExceptTest {
final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+ "PROPERTIES "
- + "k : struct(a:INTEGER, b:BOOL) & (k = rec(a:1, b:TRUE) & k /= rec(a:2, b:FALSE))"
+ + "k : struct(a:INTEGER, b:BOOL) & (k = rec(a:1, b:TRUE) & k /= rec(a:rec(a:2, b:k'b)'a, b:FALSE)) \n"
+ "END";
compare(expected, module);
@@ -70,13 +102,13 @@ public class ExceptTest {
public void testRecordAt() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
- + "CONSTANTS k \n"
- + "ASSUME k = [a |-> 1, b |-> TRUE] /\\ k /= [k EXCEPT !.a = @ + 1] \n"
+ + "CONSTANTS k, k2 \n"
+ + "ASSUME k = [a |-> 1, b |-> 1] /\\ k2 = [k EXCEPT !.b = @ + 1, !.b = @ + 1] \n"
+ "=================================";
- final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+ final String expected = "MACHINE Testing\n" + "CONSTANTS k, k2\n"
+ "PROPERTIES "
- + "k : struct(a:INTEGER, b:BOOL) & (k = rec(a:1, b:TRUE) & k /= rec(a:k'a + 1, b:k'b)) \n"
+ + "(k : struct(a:INTEGER, b:INTEGER) & k2 : struct(a:INTEGER, b:INTEGER)) & (k = rec(a:1, b:1) & k2 = rec(a:rec(a:k'a, b:k'b + 1)'a, b:rec(a:k'a, b:k'b + 1)'b + 1)) \n"
+ "END";
compare(expected, module);
diff --git a/src/test/java/de/tla2b/prettyprintb/ExternelFunctionsTest.java b/src/test/java/de/tla2b/prettyprintb/ExternelFunctionsTest.java
new file mode 100644
index 0000000..c1efbd9
--- /dev/null
+++ b/src/test/java/de/tla2b/prettyprintb/ExternelFunctionsTest.java
@@ -0,0 +1,25 @@
+package de.tla2b.prettyprintb;
+
+import static de.tla2b.util.TestUtil.compare;
+
+import org.junit.Test;
+
+public class ExternelFunctionsTest {
+
+
+ @Test
+ public void testAssert() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS TLC \n"
+ + "ASSUME Assert(TRUE, \"abc\") \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "DEFINITIONS "
+ + "ASSERT_TRUE(P, Msg) == 1 = 1; \n"
+ + "EXTERNAL_PREDICATE_ASSERT_TRUE == BOOL * STRING; \n"
+ + "PROPERTIES ASSERT_TRUE(TRUE, \"abc\") \n"
+ + "END";
+ compare(expected, module);
+ }
+}
diff --git a/src/test/java/de/tla2b/prettyprintb/FunctionTest.java b/src/test/java/de/tla2b/prettyprintb/FunctionTest.java
index ee2f672..e2a58e5 100644
--- a/src/test/java/de/tla2b/prettyprintb/FunctionTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/FunctionTest.java
@@ -52,6 +52,51 @@ public class FunctionTest {
+ "END";
compare(expected, module);
}
+
+ @Test
+ public void testFunctionConstructor4() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "CONSTANTS k\n"
+ + "ASSUME k = [<<x,y>> \\in {1} \\X {2} |-> x + y] \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "CONSTANTS k\n"
+ + "PROPERTIES k : INTEGER * INTEGER +-> INTEGER & k = %(x, y).((x,y) : {1} * {2} | x + y) \n"
+ + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testFunctionConstructorTuple() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "CONSTANTS k\n"
+ + "ASSUME k = [a \\in {1}, <<b,c>> \\in {2} \\X {3} |-> a + b + c] \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "CONSTANTS k\n"
+ + "PROPERTIES k : INTEGER * (INTEGER * INTEGER) +-> INTEGER & k = %(a, bc).(a : {1} & bc : {2} * {3} | (a + prj1(INTEGER, INTEGER)(bc)) + prj2(INTEGER, INTEGER)(bc)) \n"
+ + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testFunctionConstructorSequence() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "CONSTANTS k\n"
+ + "ASSUME k = [<<a>> \\in {<<1>>}, <<b,c>> \\in {2} \\X {3} |-> a + b + c] \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "CONSTANTS k\n"
+ + "PROPERTIES k : (INTEGER +-> INTEGER) * (INTEGER * INTEGER) +-> INTEGER & k = %(a, bc).(a : {[1]} & bc : {2} * {3} | (a(1) + prj1(INTEGER, INTEGER)(bc)) + prj2(INTEGER, INTEGER)(bc)) \n"
+ + "END";
+ compare(expected, module);
+ }
/**********************************************************************
* recursive Function
diff --git a/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java b/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java
index faf7234..5293734 100644
--- a/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java
@@ -136,6 +136,39 @@ public class LogicOperatorsTest {
+ "END";
compare(expected, module);
}
+
+ @Test
+ public void testExistentialQuantifierSequence() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "ASSUME \\E <<x>> \\in {<<1>>} : x = 1 \n"
+ + "=================================";
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES #x.([x] : {[1]} & x = 1) \n"
+ + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testExistentialQuantifierTuple() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "ASSUME \\E <<a,b>> \\in {<<1,TRUE>>} : a = 1 /\\ b = TRUE \n"
+ + "=================================";
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES #(a,b).((a,b) : {(1,TRUE)} & (a = 1 & b = TRUE)) \n"
+ + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testExistentialQuantifierAll() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "ASSUME \\E <<a,b>> \\in {<<1,TRUE>>}, <<c>> \\in {<<3>>}, d,e \\in {TRUE}: a= 1 /\\ b = TRUE /\\ c = 3 /\\ d = TRUE /\\ e \n"
+ + "=================================";
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES #(a,b,c,d,e).(((((a,b) : {(1,TRUE)} & [c] : {[3]}) & d : {TRUE}) & e : {TRUE}) & ((((a = 1 & b = TRUE) & c = 3) & d = TRUE) & e = TRUE)) \n"
+ + "END";
+ compare(expected, module);
+ }
@Test
public void testQuantifier() throws Exception {
diff --git a/src/test/java/de/tla2b/prettyprintb/SetsTest.java b/src/test/java/de/tla2b/prettyprintb/SetsTest.java
index 74f8ffa..7d3496e 100644
--- a/src/test/java/de/tla2b/prettyprintb/SetsTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/SetsTest.java
@@ -159,54 +159,74 @@ public class SetsTest {
+ "PROPERTIES {x | x : {1,2} & x = 1} = {1} \n" + "END";
compare(expected, module);
}
+
+ @Test
+ public void testConstructor1Tuple() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "ASSUME {<<a,b>> \\in {<<1,2>>} : a = 1 /\\ b = 2} = {<<1,2>>} \n"
+ + "=================================";
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES {a,b | (a,b) : {(1,2)} & (a = 1 & b = 2)} = {(1,2)} \n" + "END";
+ compare(expected, module);
+ }
+
@Test
- public void testConstructor2() throws Exception {
+ public void testConstructor1Tuple3Elements() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "ASSUME {<<a,b,c>> \\in {<<1,2,3>>} : a = 1 /\\ b = 2} = {<<1,2,3>>} \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES {a,b,c | (a,b,c) : {(1,2,3)} & (a = 1 & b = 2)} = {(1,2,3)} \n" + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testConstructor2Simple() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
- + "ASSUME {1} = {x + y+ 2: x \\in {1,2}, y \\in {1} } \n"
+ + "ASSUME {x : x \\in {1}} = {1} \n"
+ "=================================";
final String expected = "MACHINE Testing\n"
- + "PROPERTIES {1} = {t_|#x, y.(x : {1, 2} & y : {1} & t_ = x + y + 2)} \n"
+ + "PROPERTIES {t_ | #(x).(x : {1} & t_ = x)} = {1} \n"
+ "END";
compare(expected, module);
}
@Test
- public void testConstructor3() throws Exception {
+ public void testConstructor2Simple2() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
- + "ASSUME {<<1,2>>} = {<<x, y>> \\in {1} \\X {2}: TRUE} \n"
+ + "ASSUME {x + x : x \\in {1}} = {2} \n"
+ "=================================";
final String expected = "MACHINE Testing\n"
- + "PROPERTIES {(1,2)} = {(x, y)| (x,y) : {1} * {2} & TRUE = TRUE} \n"
+ + "PROPERTIES {t_ | #(x).(x : {1} & t_ = x + x)} = {2} \n"
+ "END";
compare(expected, module);
}
-
@Test
- public void testSetConstructor() throws Exception {
+ public void testConstructor2() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
- + "ASSUME {x \\in {1,2,3} : x \\in {1} \\/ x \\in {2}} = {1,2} \n"
+ + "ASSUME {x + y: x \\in {1}, y \\in {2} } = {3} \n"
+ "=================================";
-
final String expected = "MACHINE Testing\n"
- + "PROPERTIES {x|x : {1, 2, 3} & (x : {1} or x : {2})} = {1, 2} \n" + "END";
+ + "PROPERTIES {t_ | #(x,y).((x : {1} & y : {2}) & t_ = x + y)} = {3} \n"
+ + "END";
compare(expected, module);
}
@Test
- public void testConstructor4() throws Exception {
+ public void testConstructor2Tuple() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
- + "ASSUME {1} = {x : <<x, y>> \\in {1} \\X {2}} \n"
+ + "ASSUME {x + y: <<x,y>> \\in {<<1,2>>}} = {3} \n"
+ "=================================";
final String expected = "MACHINE Testing\n"
- + "PROPERTIES {1} = {t_ | #(x,y).((x,y) : {1} * {2} & t_ = x)} \n"
+ + "PROPERTIES {t_ | #(x,y).((x,y) : {(1,2)} & t_ = x + y)} = {3} \n"
+ "END";
compare(expected, module);
}
-
}
diff --git a/src/test/java/de/tla2b/prettyprintb/TupleTest.java b/src/test/java/de/tla2b/prettyprintb/TupleTest.java
index 1e8afec..2f7eca3 100644
--- a/src/test/java/de/tla2b/prettyprintb/TupleTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/TupleTest.java
@@ -5,6 +5,8 @@
package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
+
+import org.junit.Ignore;
import org.junit.Test;
public class TupleTest {
@@ -127,4 +129,18 @@ public class TupleTest {
compare(expected, module);
}
+ @Test
+ public void testTupleCartesianProduct() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "ASSUME {<<1, 4>>, <<2,3>>} \\notin SUBSET ({1,2} \\X {3,4}) \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES {(1,4), (2,3)} /: POW({1, 2} * {3, 4}) \n"
+ + "END";
+ compare(expected, module);
+ }
+
+
+
}
diff --git a/src/test/java/de/tla2b/typechecking/ExceptTest.java b/src/test/java/de/tla2b/typechecking/ExceptTest.java
index ce5086d..e5984d3 100644
--- a/src/test/java/de/tla2b/typechecking/ExceptTest.java
+++ b/src/test/java/de/tla2b/typechecking/ExceptTest.java
@@ -120,5 +120,17 @@ public class ExceptTest {
TestTypeChecker t = TestUtil.typeCheckString(module);
assertEquals("POW(INTEGER*BOOL)", t.getConstantType("k"));
}
+
+ @Test
+ public void testRecordTest() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "CONSTANTS k\n"
+ + "ASSUME k = [ [a |-> [i \\in 1..1 |-> i], b |-> [i \\in 1..1 |-> 2]] EXCEPT !.a[1] = 1].a[1] \n"
+ + "=================================";
+
+ TestTypeChecker t = TestUtil.typeCheckString(module);
+ assertEquals("INTEGER", t.getConstantType("k"));
+ }
}
diff --git a/src/test/java/de/tla2b/typechecking/FunctionTest.java b/src/test/java/de/tla2b/typechecking/FunctionTest.java
index 419fd97..a73ea0b 100644
--- a/src/test/java/de/tla2b/typechecking/FunctionTest.java
+++ b/src/test/java/de/tla2b/typechecking/FunctionTest.java
@@ -113,8 +113,7 @@ public class FunctionTest {
+ "CONSTANTS k \n"
+ "ASSUME k = [<<x,y,z>> \\in ({1} \\times {1}) |-> TRUE] \n"
+ "=================================";
- TestTypeChecker t = TestUtil.typeCheckString(module);
- System.out.println(t.getConstantType("k"));
+ TestUtil.typeCheckString(module);
}
@Test
diff --git a/src/test/java/de/tla2b/typechecking/TupleTest.java b/src/test/java/de/tla2b/typechecking/TupleTest.java
index 611a236..48b0fb9 100644
--- a/src/test/java/de/tla2b/typechecking/TupleTest.java
+++ b/src/test/java/de/tla2b/typechecking/TupleTest.java
@@ -2,7 +2,6 @@ package de.tla2b.typechecking;
import static org.junit.Assert.assertEquals;
-import org.junit.Ignore;
import org.junit.Test;
import de.tla2b.exceptions.FrontEndException;
diff --git a/src/test/java/de/tla2b/util/TestTypeChecker.java b/src/test/java/de/tla2b/util/TestTypeChecker.java
index 5e5960c..7ecc05c 100644
--- a/src/test/java/de/tla2b/util/TestTypeChecker.java
+++ b/src/test/java/de/tla2b/util/TestTypeChecker.java
@@ -10,11 +10,13 @@ import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.global.TranslationGlobals;
import de.tla2b.types.TLAType;
+import de.tla2b.types.TupleOrFunction;
import de.tla2bAst.Translator;
import tla2sany.semantic.FormalParamNode;
import tla2sany.semantic.ModuleNode;
import tla2sany.semantic.OpDeclNode;
import tla2sany.semantic.OpDefNode;
+import tla2sany.semantic.SemanticNode;
public class TestTypeChecker implements TranslationGlobals {
@@ -46,22 +48,28 @@ public class TestTypeChecker implements TranslationGlobals {
init();
}
+
+ private TLAType getBType(SemanticNode node){
+ TLAType type = (TLAType) node.getToolObject(toolId);
+ return type;
+ }
+
private void init() {
for (int i = 0; i < moduleNode.getConstantDecls().length; i++) {
OpDeclNode con = moduleNode.getConstantDecls()[i];
constants.put(con.getName().toString(),
- (TLAType) con.getToolObject(toolId));
+ getBType(con));
}
for (int i = 0; i < moduleNode.getVariableDecls().length; i++) {
OpDeclNode var = moduleNode.getVariableDecls()[i];
variables.put(var.getName().toString(),
- (TLAType) var.getToolObject(toolId));
+ getBType(var));
}
for (int i = 0; i < moduleNode.getOpDefs().length; i++) {
OpDefNode def = moduleNode.getOpDefs()[i];
- DefCon defCon = new DefCon((TLAType) def.getToolObject(5));
+ DefCon defCon = new DefCon(getBType(def));
if (defCon.getType() == null)
continue;
@@ -76,7 +84,7 @@ public class TestTypeChecker implements TranslationGlobals {
for (int j = 0; j < def.getParams().length; j++) {
FormalParamNode p = def.getParams()[j];
defCon.parameters.put(p.getName().toString(),
- (TLAType) p.getToolObject(toolId));
+ getBType(p));
}
definitions.put(def.getName().toString(), defCon);
}
diff --git a/src/test/java/de/tla2b/util/TestUtil.java b/src/test/java/de/tla2b/util/TestUtil.java
index f09e791..851bb27 100644
--- a/src/test/java/de/tla2b/util/TestUtil.java
+++ b/src/test/java/de/tla2b/util/TestUtil.java
@@ -39,7 +39,7 @@ public class TestUtil {
Start start = t.translate();
System.out.println("-------------------");
- ASTPrettyPrinter aP = new ASTPrettyPrinter();
+ ASTPrettyPrinter aP = new ASTPrettyPrinter(start);
start.apply(aP);
System.out.println(aP.getResultString());
@@ -64,7 +64,7 @@ public class TestUtil {
ToolIO.reset();
Start resultNode = Translator.translateTlaExpression(tlaExpr);
Renamer renamer = new Renamer(resultNode);
- ASTPrettyPrinter aP = new ASTPrettyPrinter(renamer);
+ ASTPrettyPrinter aP = new ASTPrettyPrinter(resultNode, renamer);
resultNode.apply(aP);
System.out.println(aP.getResultString());
String bAstString = getAstStringofBExpressionString(bExpr);
@@ -90,7 +90,7 @@ public class TestUtil {
Start resultNode = trans.translate();
String result = getTreeAsString(resultNode);
System.out.println(result);
- ASTPrettyPrinter aP = new ASTPrettyPrinter();
+ ASTPrettyPrinter aP = new ASTPrettyPrinter(resultNode);
resultNode.apply(aP);
System.out.println("-------------------");
System.out.println(aP.getResultString());
@@ -112,7 +112,7 @@ public class TestUtil {
Translator trans = new Translator(tlaModule, config);
Start resultNode = trans.translate();
- ASTPrettyPrinter aP = new ASTPrettyPrinter();
+ ASTPrettyPrinter aP = new ASTPrettyPrinter(resultNode);
resultNode.apply(aP);
System.out.println(aP.getResultString());
@@ -129,45 +129,11 @@ public class TestUtil {
return ast2String.toString();
}
-
-// public static StringBuilder translateString(String moduleString, String configString)
-// throws FrontEndException, TLA2BException, AbortException {
-// ToolIO.setMode(ToolIO.TOOL);
-// ToolIO.reset();
-// Tla2BTranslator translator = new Tla2BTranslator();
-// translator.startTest(moduleString, configString);
-// return translator.translate();
-// }
-
-
-// public static StringBuilder translate(String moduleFileName)
-// throws FrontEndException, TLA2BException, AbortException {
-// ToolIO.setMode(ToolIO.TOOL);
-// ToolIO.reset();
-// moduleFileName = moduleFileName.replace('/', FileUtil.separatorChar);
-// Tla2BTranslator translator = new Tla2BTranslator();
-// translator.start(moduleFileName, null);
-// StringBuilder res = translator.translate();
-// return res;
-// }
-//
-// public static StringBuilder translate(String moduleFileName, String configFileName)
-// throws FrontEndException, TLA2BException {
-// ToolIO.setMode(ToolIO.TOOL);
-// ToolIO.reset();
-// moduleFileName = moduleFileName.replace('/', FileUtil.separatorChar);
-// configFileName = configFileName.replace('/', FileUtil.separatorChar);
-// Tla2BTranslator translator = new Tla2BTranslator();
-// translator.start(moduleFileName, configFileName);
-// return translator.translate();
-// }
-
-
public static void renamerTest(String tlaFile) throws Exception{
Translator t = new Translator(tlaFile);
Start start = t.translate();
Renamer renamer = new Renamer(start);
- ASTPrettyPrinter aP = new ASTPrettyPrinter(renamer);
+ ASTPrettyPrinter aP = new ASTPrettyPrinter(start, renamer);
start.apply(aP);
System.out.println(aP.getResultString());
diff --git a/src/test/resources/regression/Modules/InvariantExpression.tla b/src/test/resources/regression/Modules/InvariantExpression.tla
new file mode 100644
index 0000000..57c9ca8
--- /dev/null
+++ b/src/test/resources/regression/Modules/InvariantExpression.tla
@@ -0,0 +1,6 @@
+--------------- MODULE InvariantExpression -------------
+VARIABLES x
+Init == x = 1
+Inv == TRUE
+Next == 1= 2 /\ UNCHANGED x
+=========================================
\ No newline at end of file
--
GitLab