From 0b0c0b84a58ebcf1fc8c7d8dda7fec34d15c47c4 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Wed, 11 Jun 2014 17:10:40 +0200
Subject: [PATCH] nested except statements
---
.../java/de/tla2b/analysis/TypeChecker.java | 5 +-
.../java/de/tla2b/types/TupleOrFunction.java | 282 ++++++++++++++----
src/main/java/de/tla2b/types/TupleType.java | 6 +-
src/main/java/de/tla2bAst/BAstCreator.java | 122 +++++++-
.../expression/ComplexExpressionTest.java | 2 +-
.../de/tla2b/prettyprintb/ExceptTest.java | 101 ++++++-
.../java/de/tla2b/prettyprintb/TupleTest.java | 12 +
.../java/de/tla2b/typechecking/TupleTest.java | 4 +-
.../typechecking/TupleVsSequenceTest.java | 19 ++
src/test/resources/regression/Club/Club.prob | 3 -
10 files changed, 477 insertions(+), 79 deletions(-)
delete mode 100644 src/test/resources/regression/Club/Club.prob
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index c78aac7..f15ee18 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -740,7 +740,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
} else if (list.size() == 1) {
found = new FunctionType(IntType.getInstance(), list.get(0));
} else {
- found = new TupleType(list);
+ found = TupleOrFunction.createTupleOrFunctionType(list);
+ //found = new TupleType(list);
}
try {
found = found.unify(expected);
@@ -920,7 +921,6 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
new SetType(new UntypedType()));
list.add(t.getSubType());
}
-
SetType found = new SetType(new TupleType(list));
try {
found = found.unify(expected);
@@ -929,6 +929,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
"Expected %s, found %s at Cartesian Product,%n%s",
expected, found, n.getLocation()));
}
+
return found;
}
diff --git a/src/main/java/de/tla2b/types/TupleOrFunction.java b/src/main/java/de/tla2b/types/TupleOrFunction.java
index 868ab5e..cf32443 100644
--- a/src/main/java/de/tla2b/types/TupleOrFunction.java
+++ b/src/main/java/de/tla2b/types/TupleOrFunction.java
@@ -1,8 +1,10 @@
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;
@@ -25,6 +27,26 @@ public class TupleOrFunction extends AbstractHasFollowers {
super(TUPLE_OR_FUNCTION);
}
+ public static TLAType createTupleOrFunctionType(List<TLAType> list) {
+ if (comparable(list)) {
+ TupleOrFunction tOrF = new TupleOrFunction();
+ tOrF.add(list);
+ return tOrF;
+ } else {
+ return new TupleType(list);
+ }
+ }
+
+ public void add(List<TLAType> list) {
+ for (int i = 0; i < list.size(); i++) {
+ TLAType type = list.get(i);
+ types.put(i + 1, type);
+ if (type instanceof AbstractHasFollowers) {
+ ((AbstractHasFollowers) type).addFollower(this);
+ }
+ }
+ }
+
public void apply(TypeVisitorInterface visitor) {
throw new RuntimeException("Type " + this + " is not a complete type.");
}
@@ -37,46 +59,92 @@ public class TupleOrFunction extends AbstractHasFollowers {
FunctionType res;
try {
res = func.unify(this);
+ return res.toString();
} catch (UnificationException e) {
- StringBuilder sb = new StringBuilder();
- sb.append("TupleOrFunction(");
- 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");
+ // 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");
+ }
+
}
-
- return res.toString();
-
}
@Override
public PExpression getBNode() {
- return null;
+ FunctionType func = new FunctionType();
+ func.setDomain(IntType.getInstance());
+ func.setRange(new UntypedType());
+ FunctionType res;
+ try {
+ res = func.unify(this);
+ return res.getBNode();
+ } 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).getBNode();
+ } 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");
+ }
+
+ }
+
}
@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)
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;
- }
- }
- }
+
if (o instanceof FunctionType) {
FunctionType t = (FunctionType) o;
if (!t.getDomain().compare(IntType.getInstance())) {
@@ -100,10 +168,51 @@ public class TupleOrFunction extends AbstractHasFollowers {
}
return true;
}
+ if (o instanceof TupleOrFunction) {
+ TupleOrFunction other = (TupleOrFunction) o;
+ if (isTupleOrFunction(this, other)) {
+ return true;
+ }
+
+ try {
+ for (int i = 1; i <= types.keySet().size(); i++) {
+ if (!types.get(i).compare(other.types.get(i))) {
+ return false;
+ }
+ }
+ } catch (Exception e) {
+ return false;
+ }
+
+ 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
return false;
}
+ private static boolean isTupleOrFunction(TupleOrFunction t1,
+ TupleOrFunction t2) {
+ List<TLAType> typeList = new ArrayList<TLAType>();
+ typeList.addAll(t1.types.values());
+ typeList.addAll(t2.types.values());
+ if (comparable(typeList)) {
+ return true;
+ }
+ return false;
+ }
+
@Override
public boolean contains(TLAType o) {
for (TLAType type : this.types.values()) {
@@ -161,47 +270,116 @@ public class TupleOrFunction extends AbstractHasFollowers {
}
if (o instanceof TupleType) {
TupleType tupleType = (TupleType) o;
- 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);
+
+ 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));
+ typeList.add(res);
+ }else {
+ typeList.add(tupleType.getTypes().get(i));
+ }
+ }
+ TupleType r = new TupleType(typeList);
+ 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);
}
- 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);
+ 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);
}
- range = range.unify(type);
}
- FunctionType funcType = new FunctionType(IntType.getInstance(),
- range);
- return funcType.unify(tupleType);
+ 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);
}
+
}
+
throw new RuntimeException();
}
- public void setNewType(AbstractHasFollowers oldType,
- TLAType newType) {
- LinkedHashMap<Integer, TLAType> temp = new LinkedHashMap<Integer, TLAType>(types);
+ public void setNewType(AbstractHasFollowers oldType, TLAType newType) {
+ LinkedHashMap<Integer, TLAType> temp = new LinkedHashMap<Integer, TLAType>(
+ types);
for (Entry<Integer, TLAType> entry : temp.entrySet()) {
- if(entry.getValue().equals(oldType)){
+ if (entry.getValue().equals(oldType)) {
types.put(entry.getKey(), newType);
if (newType instanceof AbstractHasFollowers) {
- ((AbstractHasFollowers) newType).addFollower(this);;
+ ((AbstractHasFollowers) newType).addFollower(this);
+ ;
}
}
}
-
+
+ }
+
+ private static boolean comparable(List<TLAType> typeList) {
+ for (int i = 0; i < typeList.size() - 1; i++) {
+ TLAType t1 = typeList.get(i);
+ for (int j = 1; j < typeList.size(); j++) {
+ TLAType t2 = typeList.get(j);
+ if (!t1.compare(t2))
+ return false; // tuple
+ }
+ }
+ return true;
}
}
diff --git a/src/main/java/de/tla2b/types/TupleType.java b/src/main/java/de/tla2b/types/TupleType.java
index b93441c..7e2d45e 100644
--- a/src/main/java/de/tla2b/types/TupleType.java
+++ b/src/main/java/de/tla2b/types/TupleType.java
@@ -9,9 +9,9 @@ import de.tla2b.exceptions.UnificationException;
import de.tla2b.output.TypeVisitorInterface;
public class TupleType extends AbstractHasFollowers {
- private ArrayList<TLAType> types;
+ private List<TLAType> types;
- public TupleType(ArrayList<TLAType> typeList) {
+ public TupleType(List<TLAType> typeList) {
super(TUPLE);
setTypes(typeList);
}
@@ -29,7 +29,7 @@ public class TupleType extends AbstractHasFollowers {
return new ArrayList<TLAType>(types);
}
- public void setTypes(ArrayList<TLAType> types) {
+ public void setTypes(List<TLAType> types) {
this.types = types;
types = new ArrayList<TLAType>(types);
for (TLAType tlaType : types) {
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index e89a539..b3528e5 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -1693,18 +1693,34 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
{
TLAType type = (TLAType) n.getToolObject(TYPE_ID);
if (type.getKind() == IType.STRUCT) {
+ StructType structType = (StructType) type;
Hashtable<String, PExpression> temp = new Hashtable<String, PExpression>();
for (int i = 1; i < n.getArgs().length; i++) {
OpApplNode pair = (OpApplNode) n.getArgs()[i];
+
ExprOrOpArgNode first = pair.getArgs()[0];
- ExprOrOpArgNode second = pair.getArgs()[1];
+ ExprOrOpArgNode val = pair.getArgs()[1];
OpApplNode seq = (OpApplNode) first;
- PExpression val = visitExprOrOpArgNodeExpression(second);
+ LinkedList<ExprOrOpArgNode> seqList = new LinkedList<ExprOrOpArgNode>();
+ for (int j = 0; j < seq.getArgs().length; j++) {
+ seqList.add(seq.getArgs()[j]);
+ }
- StringNode stringNode = (StringNode) seq.getArgs()[0];
+ 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();
- temp.put(fieldName, val);
+ select.setIdentifier(createIdentifierNode(fieldName));
+
+ PExpression value = evalExceptValue(select,
+ seqList, structType.getType(fieldName), val);
+
+ temp.put(fieldName, value);
}
StructType st = (StructType) type;
@@ -1725,20 +1741,38 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
ARecExpression rec = new ARecExpression(list);
return rec;
-
} else {
- // FunctionType func = (FunctionType) type;
+ FunctionType func = (FunctionType) type;
List<PExpression> list = new ArrayList<PExpression>();
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;
+
+ LinkedList<ExprOrOpArgNode> seqList = new LinkedList<ExprOrOpArgNode>();
+ for (int j = 0; j < seq.getArgs().length; j++) {
+ 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(visitExprOrOpArgNodeExpression(pair
- .getArgs()[0]));
- coupleList.add(visitExprOrOpArgNodeExpression(pair
- .getArgs()[1]));
+ coupleList.add(firstArg);
+ coupleList.add(value);
couple.setList(coupleList);
list.add(couple);
}
@@ -1800,6 +1834,70 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
throw new RuntimeException(n.getOperator().getName().toString());
}
+ private PExpression evalExceptValue(PExpression prefix,
+ LinkedList<ExprOrOpArgNode> seqList, TLAType tlaType,
+ ExprOrOpArgNode val) {
+
+ ExprOrOpArgNode head = seqList.poll();
+ if (head == null) {
+ return visitExprOrOpArgNodeExpression(val);
+ }
+
+ if (tlaType instanceof StructType) {
+ StructType structType = (StructType) tlaType;
+ String field = ((StringNode) head).getRep().toString();
+
+ List<PRecEntry> list = new ArrayList<PRecEntry>();
+ for (int i = 0; i < structType.getFields().size(); i++) {
+ 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.setIdentifier(createIdentifierNode(fieldName));
+ 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;
+
+ } else {
+ FunctionType func = (FunctionType) tlaType;
+
+ ACoupleExpression couple = new ACoupleExpression();
+ List<PExpression> coupleList = new ArrayList<PExpression>();
+ coupleList.add(visitExprOrOpArgNodeExpression(head));
+
+ AFunctionExpression funcCall = new AFunctionExpression();
+ funcCall.setIdentifier(prefix);
+ List<PExpression> argList = new ArrayList<PExpression>();
+ argList.add(visitExprOrOpArgNodeExpression(head));
+ funcCall.setParameters(argList);
+ coupleList.add(evalExceptValue(funcCall, seqList, func.getRange(),
+ val));
+ couple.setList(coupleList);
+ List<PExpression> setList = new ArrayList<PExpression>();
+ setList.add(couple);
+ ASetExtensionExpression setExtension = new ASetExtensionExpression(
+ setList);
+ AOverwriteExpression overwrite = new AOverwriteExpression();
+ overwrite.setLeft((PExpression) prefix.clone());
+ overwrite.setRight(setExtension);
+ return overwrite;
+ }
+ }
+
private PExpression createProjectionFunction(OpApplNode n, int field,
TLAType t) {
TupleType tuple = (TupleType) t;
@@ -1813,7 +1911,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
first.setExp1(tuple.getTypes().get(0).getBNode());
first.setExp2(tuple.getTypes().get(1).getBNode());
returnFunc.setIdentifier(first);
- }else{
+ } else {
index = field;
ASecondProjectionExpression second = new ASecondProjectionExpression();
ArrayList<TLAType> typeList = new ArrayList<TLAType>();
@@ -1835,7 +1933,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
first.setExp1(createNestedCoupleAsBNode(typeList));
first.setExp2(tuple.getTypes().get(i).getBNode());
newfunc.setIdentifier(first);
-
+
ArrayList<PExpression> list = new ArrayList<PExpression>();
list.add(newfunc);
func.setParameters(list);
diff --git a/src/test/java/de/tla2b/expression/ComplexExpressionTest.java b/src/test/java/de/tla2b/expression/ComplexExpressionTest.java
index 3a22a3a..ccc38c6 100644
--- a/src/test/java/de/tla2b/expression/ComplexExpressionTest.java
+++ b/src/test/java/de/tla2b/expression/ComplexExpressionTest.java
@@ -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:2, b:r'b))",
+ 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))",
"r = [a |-> [x|->1,y|->TRUE], b |-> 1] "
+ "/\\ r2 = [r EXCEPT !.a.x = 2]");
}
diff --git a/src/test/java/de/tla2b/prettyprintb/ExceptTest.java b/src/test/java/de/tla2b/prettyprintb/ExceptTest.java
index bf758be..ddd109c 100644
--- a/src/test/java/de/tla2b/prettyprintb/ExceptTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/ExceptTest.java
@@ -23,15 +23,61 @@ public class ExceptTest {
}
@Test
- public void testFunctionExcept2() throws Exception {
+ public void testRecordExcept() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
- + "ASSUME k = [k EXCEPT ![TRUE] = 0, ![FALSE] = 0] \n"
+ + "ASSUME k = [a |-> 1, b |-> TRUE] /\\ k /= [k EXCEPT !.a = 2, !.b = FALSE] \n"
+ "=================================";
final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
- + "PROPERTIES " + " k : BOOL +-> INTEGER "
- + "& k = k <+ {TRUE |-> 0, FALSE |-> 0}" + "END";
+ + "PROPERTIES "
+ + "k : struct(a:INTEGER, b:BOOL) & (k = rec(a:1, b:TRUE) & k /= rec(a:2, b:FALSE))"
+ + "END";
+ compare(expected, module);
+
+ }
+
+ @Test
+ public void testRecordFunctionExcept() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "CONSTANTS k \n"
+ + "ASSUME k = [a |-> <<3>>] /\\ k /= [k EXCEPT !.a[1] = 4] \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+ + "PROPERTIES "
+ + "k : struct(a:INTEGER +-> INTEGER) & (k = rec(a:[3]) & k /= rec(a:k'a <+ {(1,4)})) \n"
+ + "END";
+ compare(expected, module);
+
+ }
+
+ @Test
+ public void testFunctionRecordExcept() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "CONSTANTS k \n"
+ + "ASSUME k = [i \\in {3,4} |->[a |-> i, b |-> TRUE ] ] /\\ k /= [k EXCEPT ![3].b = FALSE] \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+ + "PROPERTIES "
+ + "k : INTEGER +-> struct(a:INTEGER, b:BOOL) & (k = %(i).(i : {3, 4} | rec(a:i, b:TRUE)) & k /= k <+ {(3,rec(a:k(3)'a, b:FALSE))}) \n"
+ + "END";
+ compare(expected, module);
+
+ }
+
+ @Test
+ public void testRecordExceptNested() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "CONSTANTS k \n"
+ + "ASSUME k = [a |-> [b |-> 1, c |-> 2]] /\\ k /= [k EXCEPT !.a.b = 2] \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+ + "PROPERTIES "
+ + "k : struct(a:struct(b:INTEGER, c:INTEGER)) & (k = rec(a:rec(b:1, c:2)) & k /= rec(a:rec(b:2, c:(k'a)'c))) \n"
+ + "END";
compare(expected, module);
}
@@ -68,5 +114,52 @@ public class ExceptTest {
+ "& k2 = k <+ {(1, 1) |-> k(1, 1) + 4} \n" + "END";
compare(expected, module);
}
+
+ @Test
+ public void testFunctionExcept9() throws Exception {
+ ToolIO.reset();
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "CONSTANTS k \n"
+ + "ASSUME k = [i \\in {3,4} |-> <<i, 7>>] /\\ [k EXCEPT ![4] = <<4, 8>>] # [k EXCEPT ![4][2] = 9] \n"
+ + "=================================";
+ final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+ + "PROPERTIES "
+ + "k : INTEGER +-> (INTEGER +-> INTEGER) & (k = %(i).(i : {3, 4} | [i,7]) & k <+ {(4,[4,8])} /= k <+ {(4,k(4) <+ {(2,9)})}) \n"
+ + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testFunctionExceptNested() throws Exception {
+ ToolIO.reset();
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "CONSTANTS k \n"
+ + "ASSUME k = [i \\in {3,4} |-> <<i, 7>>] /\\ k # [k EXCEPT ![4][2] = 8] \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+ + "PROPERTIES "
+ + "k : INTEGER +-> (INTEGER +-> INTEGER) & (k = %(i).(i : {3, 4} | [i,7]) & k /= k <+ {(4,k(4) <+ {(2,8)})}) \n"
+ + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testFunctionExceptNested2() throws Exception {
+ ToolIO.reset();
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "CONSTANTS k \n"
+ + "ASSUME k = [i \\in {3,4} |-> << <<8>> >>] /\\ k # [k EXCEPT ![4][1][1] = 7] \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+ + "PROPERTIES "
+ + "k : INTEGER +-> (INTEGER +-> (INTEGER +-> INTEGER)) & (k = %(i).(i : {3, 4} | [[8]]) & k /= k <+ {(4,k(4) <+ {(1,(k(4))(1) <+ {(1,7)})})}) \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 8894cea..1e8afec 100644
--- a/src/test/java/de/tla2b/prettyprintb/TupleTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/TupleTest.java
@@ -114,5 +114,17 @@ public class TupleTest {
+ "END";
compare(expected, module);
}
+
+ @Test
+ public void testDomainOfTuple() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "ASSUME {1,2,3} = DOMAIN <<\"a\", \"b\", \"c\">> \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES {1, 2, 3} = dom([\"a\", \"b\", \"c\"]) \n"
+ + "END";
+ compare(expected, module);
+ }
}
diff --git a/src/test/java/de/tla2b/typechecking/TupleTest.java b/src/test/java/de/tla2b/typechecking/TupleTest.java
index 7ac78dc..611a236 100644
--- a/src/test/java/de/tla2b/typechecking/TupleTest.java
+++ b/src/test/java/de/tla2b/typechecking/TupleTest.java
@@ -72,7 +72,7 @@ public class TupleTest {
+ "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("INTEGER*INTEGER*INTEGER", t.getConstantType("k").toString());
+ assertEquals("POW(INTEGER*INTEGER)", t.getConstantType("k").toString());
}
@Test
@@ -84,7 +84,7 @@ public class TupleTest {
+ "ASSUME k = <<1,1>> \n" + "=================================";
TestTypeChecker t = TestUtil.typeCheckString(module);
- assertEquals("INTEGER*INTEGER", t.getConstantType("k").toString());
+ assertEquals("POW(INTEGER*INTEGER)", t.getConstantType("k").toString());
}
@Test
diff --git a/src/test/java/de/tla2b/typechecking/TupleVsSequenceTest.java b/src/test/java/de/tla2b/typechecking/TupleVsSequenceTest.java
index 6f3699d..c626abd 100644
--- a/src/test/java/de/tla2b/typechecking/TupleVsSequenceTest.java
+++ b/src/test/java/de/tla2b/typechecking/TupleVsSequenceTest.java
@@ -59,5 +59,24 @@ public class TupleVsSequenceTest {
assertEquals("INTEGER*BOOL", t.getConstantType("c"));
}
+ @Test
+ public void testTupleVsSequence5() throws FrontEndException, TLA2BException {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "CONSTANTS k\n"
+ + "ASSUME k = <<1,2>> /\\ k \\in {1} \\X {2} \n"
+ + "=================================";
+ TestTypeChecker t = TestUtil.typeCheckString(module);
+ assertEquals("INTEGER*INTEGER", t.getConstantType("k"));
+ }
+
+ @Test
+ public void testTupleVsSequence6() throws FrontEndException, TLA2BException {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "CONSTANTS k\n"
+ + "ASSUME {k} = {<<x, y>> \\in {1} \\X {2}: TRUE} \n"
+ + "=================================";
+ TestTypeChecker t = TestUtil.typeCheckString(module);
+ assertEquals("INTEGER*INTEGER", t.getConstantType("k"));
+ }
}
diff --git a/src/test/resources/regression/Club/Club.prob b/src/test/resources/regression/Club/Club.prob
deleted file mode 100644
index e531ebf..0000000
--- a/src/test/resources/regression/Club/Club.prob
+++ /dev/null
@@ -1,3 +0,0 @@
-parser_version('2014-03-12 22:57:52.564').
-classical_b('Club',['/Users/hansen/git/tla2bAST/src/test/resources/regression/Club/Club.tla']).
-machine(abstract_machine(1,machine(2),machine_header(3,'Club',[]),[sets(4,[enumerated_set(5,'ENUM1',[identifier(6,n1),identifier(7,n2),identifier(8,n3)])]),constants(9,[identifier(info(10,tla_type(integer)),capacity),identifier(info(11,tla_type(set(modelvalue))),'NAME'),identifier(info(12,tla_type(integer)),total)]),properties(13,conjunct(14,conjunct(15,conjunct(16,conjunct(17,conjunct(18,member(19,identifier(20,capacity),integer_set(21)),equal(22,identifier(23,'NAME'),identifier(24,'ENUM1'))),member(25,identifier(26,total),integer_set(27))),conjunct(28,member(29,identifier(30,capacity),natural_set(31)),equal(32,identifier(33,capacity),integer(34,2)))),greater(35,card(36,identifier(37,'NAME')),identifier(38,capacity))),conjunct(39,member(40,identifier(41,total),natural_set(42)),greater(43,identifier(44,total),integer(45,2))))),variables(46,[identifier(info(47,tla_type(set(modelvalue))),member),identifier(info(48,tla_type(set(modelvalue))),waiting)]),invariant(49,conjunct(50,member(51,identifier(52,member),pow_subset(53,identifier(54,'ENUM1'))),member(55,identifier(56,waiting),pow_subset(57,identifier(58,'ENUM1'))))),initialisation(59,becomes_such(60,[identifier(61,member),identifier(62,waiting)],conjunct(63,equal(64,identifier(65,member),empty_set(66)),equal(67,identifier(68,waiting),empty_set(69))))),operations(70,[operation(71,identifier(71,join_queue),[],[identifier(72,nn)],any(73,[identifier(74,member_n)],conjunct(75,conjunct(76,conjunct(77,conjunct(78,conjunct(79,member(80,identifier(81,nn),identifier(82,'NAME')),not_member(83,identifier(84,nn),identifier(85,member))),not_member(86,identifier(87,nn),identifier(88,waiting))),member(89,identifier(90,member_n),pow_subset(91,identifier(92,'ENUM1')))),less(93,card(94,identifier(95,waiting)),identifier(96,total))),equal(97,identifier(98,member_n),identifier(99,member))),assign(100,[identifier(101,waiting),identifier(102,member)],[union(103,identifier(104,waiting),set_extension(105,[identifier(106,nn)])),identifier(107,member_n)]))),operation(108,identifier(108,join),[],[identifier(109,nn)],select(110,conjunct(111,conjunct(112,conjunct(113,member(114,identifier(115,nn),identifier(116,'NAME')),member(117,identifier(118,nn),identifier(119,waiting))),less(120,card(121,identifier(122,member)),identifier(123,capacity))),less(124,card(125,identifier(126,member)),identifier(127,capacity))),assign(128,[identifier(129,member),identifier(130,waiting)],[union(131,identifier(132,member),set_extension(133,[identifier(134,nn)])),minus_or_set_subtract(135,identifier(136,waiting),set_extension(137,[identifier(138,nn)]))]),[])),operation(139,identifier(139,remove),[],[identifier(140,nn)],any(141,[identifier(142,waiting_n)],conjunct(143,conjunct(144,conjunct(145,member(146,identifier(147,nn),identifier(148,'NAME')),member(149,identifier(150,nn),identifier(151,member))),member(152,identifier(153,waiting_n),pow_subset(154,identifier(155,'ENUM1')))),equal(156,identifier(157,waiting_n),identifier(158,waiting))),assign(159,[identifier(160,member),identifier(161,waiting)],[minus_or_set_subtract(162,identifier(163,member),set_extension(164,[identifier(165,nn)])),identifier(166,waiting_n)])))])])).
--
GitLab