diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index 2d820787637d4b5afef246644d05c9426b131e82..abf389bacfc6572e98396b88f2068d5fbab8d5fd 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -961,19 +961,21 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
String fieldName = ((StringNode) n.getArgs()[1]).getRep()
.toString();
StructType r = (StructType) visitExprOrOpArgNode(n.getArgs()[0],
- new StructType());
+ StructType.getIncompleteStruct());
- StructType expectedStruct = new StructType();
+ StructType expectedStruct = StructType.getIncompleteStruct();
expectedStruct.add(fieldName, expected);
try {
r = r.unify(expectedStruct);
- return r.getType(fieldName);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
"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);
+ return r.getType(fieldName);
}
/***********************************************************************
diff --git a/src/main/java/de/tla2b/exceptions/NotImplementedException.java b/src/main/java/de/tla2b/exceptions/NotImplementedException.java
index d386450ccf274b3f2957468d126e0efbba697fef..a9376b5d877a7a7537e41b13e3d914791c5c8197 100644
--- a/src/main/java/de/tla2b/exceptions/NotImplementedException.java
+++ b/src/main/java/de/tla2b/exceptions/NotImplementedException.java
@@ -2,7 +2,7 @@ package de.tla2b.exceptions;
@SuppressWarnings("serial")
-public class NotImplementedException extends TLA2BException {
+public class NotImplementedException extends RuntimeException {
public NotImplementedException(String e){
super(e);
}
diff --git a/src/main/java/de/tla2b/types/StructOrFunction.java b/src/main/java/de/tla2b/types/StructOrFunction.java
index f62233497737e0307cdf1f8943ddc0b6720ac329..7f18ef0b2b96a8b094222c0fd1044c2566977748 100644
--- a/src/main/java/de/tla2b/types/StructOrFunction.java
+++ b/src/main/java/de/tla2b/types/StructOrFunction.java
@@ -172,7 +172,7 @@ public class StructOrFunction extends AbstractHasFollowers {
return found.unify(o);
}
if (o instanceof StructType) {
- StructType res = new StructType();
+ StructType res = StructType.getIncompleteStruct();
for (String field : types.keySet()) {
res.add(field, this.types.get(field));
diff --git a/src/main/java/de/tla2b/types/StructType.java b/src/main/java/de/tla2b/types/StructType.java
index 96e6cbefb3017c714c47382d5a1c4ebceb21e610..f7df4862b029ecaa69d5f669003496ad62b4aa6b 100644
--- a/src/main/java/de/tla2b/types/StructType.java
+++ b/src/main/java/de/tla2b/types/StructType.java
@@ -7,6 +7,9 @@ import java.util.List;
import java.util.Map.Entry;
import java.util.Set;
+import de.be4.classicalb.core.parser.node.ABoolSetExpression;
+import de.be4.classicalb.core.parser.node.AMultOrCartExpression;
+import de.be4.classicalb.core.parser.node.APowSubsetExpression;
import de.be4.classicalb.core.parser.node.ARecEntry;
import de.be4.classicalb.core.parser.node.AStructExpression;
import de.be4.classicalb.core.parser.node.PExpression;
@@ -14,14 +17,26 @@ import de.be4.classicalb.core.parser.node.PRecEntry;
import de.tla2b.exceptions.UnificationException;
import de.tla2bAst.BAstCreator;
-
-
public class StructType extends AbstractHasFollowers {
private LinkedHashMap<String, TLAType> types;
+ private boolean extensible;
+ private boolean incompleteStruct;
public StructType() {
super(STRUCT);
types = new LinkedHashMap<String, TLAType>();
+ extensible = false;
+ incompleteStruct = false;
+ }
+
+ public static StructType getIncompleteStruct() {
+ StructType s = new StructType();
+ s.incompleteStruct = true;
+ return s;
+ }
+
+ public boolean isExtensible() {
+ return extensible;
}
public TLAType getType(String fieldName) {
@@ -65,12 +80,12 @@ public class StructType extends AbstractHasFollowers {
}
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 StructOrFunction){
+
+ if (o instanceof StructOrFunction) {
return o.compare(this);
}
if (o instanceof StructType) {
@@ -98,12 +113,33 @@ public class StructType extends AbstractHasFollowers {
if (o instanceof AbstractHasFollowers)
((AbstractHasFollowers) o).setFollowersTo(this);
- if (o instanceof StructOrFunction){
+ if (o instanceof StructOrFunction) {
return (StructType) o.unify(this);
}
-
+
if (o instanceof StructType) {
StructType s = (StructType) o;
+ boolean extendStruct = false;
+
+ if (this.incompleteStruct && s.incompleteStruct) {
+ extendStruct = false;
+ } else if (this.incompleteStruct) {
+ if (s.types.keySet().containsAll(this.types.keySet())) {
+ extendStruct = false;
+ } else {
+ extendStruct = true;
+ }
+ } else if (s.incompleteStruct) {
+ if (this.types.keySet().containsAll(s.types.keySet())) {
+ extendStruct = false;
+ } else {
+ extendStruct = true;
+ }
+ } else {
+ extendStruct = !s.types.keySet().equals(this.types.keySet());
+ }
+ this.extensible = this.extensible || s.extensible || extendStruct;
+
Iterator<String> keys = s.types.keySet().iterator();
while (keys.hasNext()) {
String fieldName = (String) keys.next();
@@ -118,6 +154,7 @@ public class StructType extends AbstractHasFollowers {
}
this.types.put(fieldName, sType);
}
+ this.incompleteStruct = false;
}
return this;
}
@@ -166,7 +203,7 @@ public class StructType extends AbstractHasFollowers {
public String toString() {
String res = "struct(";
Iterator<String> keys = types.keySet().iterator();
- if(!keys.hasNext())
+ if (!keys.hasNext())
res += "...";
while (keys.hasNext()) {
String fieldName = (String) keys.next();
@@ -177,14 +214,23 @@ public class StructType extends AbstractHasFollowers {
res += ")";
return res;
}
-
+
@Override
public PExpression getBNode() {
List<PRecEntry> recList = new ArrayList<PRecEntry>();
for (Entry<String, TLAType> entry : types.entrySet()) {
ARecEntry rec = new ARecEntry();
rec.setIdentifier(BAstCreator.createIdentifierNode(entry.getKey()));
- rec.setValue(entry.getValue().getBNode());
+ if (extensible) {
+
+ AMultOrCartExpression cart = new AMultOrCartExpression();
+ cart.setLeft(new ABoolSetExpression());
+ cart.setRight(entry.getValue().getBNode());
+ APowSubsetExpression pow = new APowSubsetExpression(cart);
+ rec.setValue(pow);
+ } else {
+ rec.setValue(entry.getValue().getBNode());
+ }
recList.add(rec);
}
return new AStructExpression(recList);
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index a6e7987992785c623d59cf8c8af01d3fac11a89c..52efad9f54d9b07858eaa64a9399bbab17a5b31d 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -137,6 +137,7 @@ import de.tla2b.analysis.PredicateVsExpression.DefinitionType;
import de.tla2b.analysis.UsedExternalFunctions.EXTERNAL_FUNCTIONS;
import de.tla2b.config.ConfigfileEvaluator;
import de.tla2b.config.ValueObj;
+import de.tla2b.exceptions.NotImplementedException;
import de.tla2b.global.BBuildIns;
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.Priorities;
@@ -238,8 +239,6 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
-
-
private void createSetsClause() {
if (conEval == null || conEval.getEnumerationSet() == null
|| conEval.getEnumerationSet().size() == 0)
@@ -266,7 +265,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
}
}
-
+
ArrayList<PSet> sets = new ArrayList<PSet>();
for (int i = 0; i < printed.size(); i++) {
AEnumeratedSetSet eSet = new AEnumeratedSetSet();
@@ -1194,13 +1193,14 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
visitExprOrOpArgNodeExpression(n.getArgs()[0]));
case B_OPCODE_subseq: { // SubSeq(s,a,b)
- //%p.(p : 1..(b-a+1)| s(p+a-1))
+ // %p.(p : 1..(b-a+1)| s(p+a-1))
ALambdaExpression lambda = new ALambdaExpression();
lambda.setIdentifiers(createIdentifierList("t_"));
AMemberPredicate member = new AMemberPredicate();
member.setLeft(createIdentifierNode("t_"));
AIntervalExpression interval = new AIntervalExpression();
- interval.setLeftBorder(new AIntegerExpression(new TIntegerLiteral("1")));
+ interval.setLeftBorder(new AIntegerExpression(new TIntegerLiteral(
+ "1")));
AMinusOrSetSubtractExpression minus = new AMinusOrSetSubtractExpression();
minus.setLeft(visitExprOrOpArgNodeExpression(n.getArgs()[2]));
minus.setRight(visitExprOrOpArgNodeExpression(n.getArgs()[1]));
@@ -1223,18 +1223,20 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
func.setParameters(params);
lambda.setExpression(func);
return lambda;
-
-// ARestrictFrontExpression restrictFront = new ARestrictFrontExpression();
-// restrictFront
-// .setLeft(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
-// restrictFront
-// .setRight(visitExprOrOpArgNodeExpression(n.getArgs()[2]));
-//
-// ARestrictTailExpression restrictTail = new ARestrictTailExpression();
-// restrictTail.setLeft(restrictFront);
-// restrictTail
-// .setRight(visitExprOrOpArgNodeExpression(n.getArgs()[1]));
-// return restrictTail;
+
+ // ARestrictFrontExpression restrictFront = new
+ // ARestrictFrontExpression();
+ // restrictFront
+ // .setLeft(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
+ // restrictFront
+ // .setRight(visitExprOrOpArgNodeExpression(n.getArgs()[2]));
+ //
+ // ARestrictTailExpression restrictTail = new
+ // ARestrictTailExpression();
+ // restrictTail.setLeft(restrictFront);
+ // restrictTail
+ // .setRight(visitExprOrOpArgNodeExpression(n.getArgs()[1]));
+ // return restrictTail;
}
}
@@ -1589,56 +1591,125 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
List<PRecEntry> recList = new ArrayList<PRecEntry>();
- for (int i = 0; i < struct.getFields().size(); i++) {
- String fieldName = struct.getFields().get(i); // renamed name
- AIdentifierExpression field = createIdentifierNode(fieldName);
- ARecEntry rec = new ARecEntry();
- rec.setIdentifier(field);
- if (pairTable.containsKey(fieldName)) {
- rec.setValue(pairTable.get(fieldName));
- } else {
- rec.setValue(struct.getType(fieldName).getBNode());
+ if (struct.isExtensible()) {
+ for (int i = 0; i < struct.getFields().size(); i++) {
+ String fieldName = struct.getFields().get(i); // name
+ AIdentifierExpression field = createIdentifierNode(fieldName);
+ ARecEntry rec = new ARecEntry();
+ rec.setIdentifier(field);
+ AMultOrCartExpression cart = new AMultOrCartExpression();
+ cart.setLeft(new ABoolSetExpression());
+ if (pairTable.containsKey(fieldName)) {
+ cart.setRight(pairTable.get(fieldName));
+ } else {
+ cart.setRight(struct.getType(fieldName).getBNode());
+ }
+ rec.setValue(new APowSubsetExpression(cart));
+ recList.add(rec);
+ }
+ } else {
+ for (int i = 0; i < struct.getFields().size(); i++) {
+ String fieldName = struct.getFields().get(i);
+ AIdentifierExpression field = createIdentifierNode(fieldName);
+ ARecEntry rec = new ARecEntry();
+ rec.setIdentifier(field);
+ if (pairTable.containsKey(fieldName)) {
+ rec.setValue(pairTable.get(fieldName));
+ } else {
+ rec.setValue(struct.getType(fieldName).getBNode());
+ }
+ recList.add(rec);
}
- recList.add(rec);
- }
+ }
return new AStructExpression(recList);
}
case OPCODE_rc: { // [h_1 |-> 1, h_2 |-> 2]
StructType struct = (StructType) n.getToolObject(TYPE_ID);
- Hashtable<String, PExpression> pairTable = new Hashtable<String, PExpression>();
- ExprOrOpArgNode[] args = n.getArgs();
- for (int i = 0; i < args.length; i++) {
- OpApplNode pair = (OpApplNode) args[i];
- StringNode stringNode = (StringNode) pair.getArgs()[0];
- pairTable.put(stringNode.getRep().toString(),
- visitExprOrOpArgNodeExpression(pair.getArgs()[1]));
- }
- List<PRecEntry> recList = new ArrayList<PRecEntry>();
- for (int i = 0; i < struct.getFields().size(); i++) {
- String fieldName = struct.getFields().get(i);
- AIdentifierExpression field = createIdentifierNode(fieldName);
- ARecEntry rec = new ARecEntry();
- rec.setIdentifier(field);
- if (pairTable.containsKey(fieldName)) {
- rec.setValue(pairTable.get(fieldName));
- } else {
- // insert null element
+ if (struct.isExtensible()) {
+ Hashtable<String, PExpression> pairTable = new Hashtable<String, PExpression>();
+ ExprOrOpArgNode[] args = n.getArgs();
+ for (int i = 0; i < args.length; i++) {
+ OpApplNode pair = (OpApplNode) args[i];
+ StringNode stringNode = (StringNode) pair.getArgs()[0];
+ pairTable.put(stringNode.getRep().toString(),
+ visitExprOrOpArgNodeExpression(pair.getArgs()[1]));
+ }
+ List<PRecEntry> recList = new ArrayList<PRecEntry>();
+ for (int i = 0; i < struct.getFields().size(); i++) {
+ String fieldName = struct.getFields().get(i);
+ AIdentifierExpression field = createIdentifierNode(fieldName);
+ ARecEntry rec = new ARecEntry();
+ rec.setIdentifier(field);
+ if (pairTable.containsKey(fieldName)) {
+
+ ACoupleExpression couple = new ACoupleExpression();
+ List<PExpression> coupleList = new ArrayList<PExpression>();
+ coupleList.add(new ABooleanTrueExpression());
+ coupleList.add(pairTable.get(fieldName));
+ couple.setList(coupleList);
+ ASetExtensionExpression set = new ASetExtensionExpression(
+ makePexpressionList(couple));
+ rec.setValue(set);
+ } else {
+ AEmptySetExpression emptySet = new AEmptySetExpression();
+ rec.setValue(emptySet);
+ }
+ recList.add(rec);
+ }
+ return new ARecExpression(recList);
+
+ } else {
+ Hashtable<String, PExpression> pairTable = new Hashtable<String, PExpression>();
+ ExprOrOpArgNode[] args = n.getArgs();
+ for (int i = 0; i < args.length; i++) {
+ OpApplNode pair = (OpApplNode) args[i];
+ StringNode stringNode = (StringNode) pair.getArgs()[0];
+ pairTable.put(stringNode.getRep().toString(),
+ visitExprOrOpArgNodeExpression(pair.getArgs()[1]));
+ }
+ List<PRecEntry> recList = new ArrayList<PRecEntry>();
+ for (int i = 0; i < struct.getFields().size(); i++) {
+ String fieldName = struct.getFields().get(i);
+ AIdentifierExpression field = createIdentifierNode(fieldName);
+ ARecEntry rec = new ARecEntry();
+ rec.setIdentifier(field);
+ if (pairTable.containsKey(fieldName)) {
+ rec.setValue(pairTable.get(fieldName));
+ } else {
+ // this struct is extensible
+ throw new NotImplementedException("Missing case handling extensible structs.");
+ }
+ recList.add(rec);
}
- recList.add(rec);
+ return new ARecExpression(recList);
}
- return new ARecExpression(recList);
}
case OPCODE_rs: { // $RcdSelect r.c
- ARecordFieldExpression rcdSelect = new ARecordFieldExpression();
- rcdSelect.setRecord(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
- StringNode stringNode = (StringNode) n.getArgs()[1];
- rcdSelect.setIdentifier(createIdentifierNode(stringNode.getRep()
- .toString())); // TODO renamed
- return rcdSelect;
+ StructType struct = (StructType) n.getToolObject(TYPE_ID);
+ if (struct.isExtensible()) {
+ ARecordFieldExpression rcdSelect = new ARecordFieldExpression();
+ rcdSelect
+ .setRecord(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
+ StringNode stringNode = (StringNode) n.getArgs()[1];
+ rcdSelect.setIdentifier(createIdentifierNode(stringNode
+ .getRep().toString()));
+ AFunctionExpression funcCall = new AFunctionExpression();
+ funcCall.setIdentifier(rcdSelect);
+ funcCall.setParameters(makePexpressionList(new ABooleanTrueExpression()));
+ return funcCall;
+ } else {
+ ARecordFieldExpression rcdSelect = new ARecordFieldExpression();
+ rcdSelect
+ .setRecord(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
+ StringNode stringNode = (StringNode) n.getArgs()[1];
+ rcdSelect.setIdentifier(createIdentifierNode(stringNode
+ .getRep().toString()));
+ return rcdSelect;
+ }
}
case OPCODE_prime: // prime
@@ -2190,4 +2261,9 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
return list;
}
+ public static List<PExpression> makePexpressionList(PExpression expr) {
+ ArrayList<PExpression> list = new ArrayList<PExpression>();
+ list.add(expr);
+ return list;
+ }
}
diff --git a/src/test/java/de/tla2b/expression/TestComplexExpression.java b/src/test/java/de/tla2b/expression/ComplexExpressionTest.java
similarity index 94%
rename from src/test/java/de/tla2b/expression/TestComplexExpression.java
rename to src/test/java/de/tla2b/expression/ComplexExpressionTest.java
index deb92d0bfa2621ea29aaa3bf1ff070bbba751191..3a22a3a972475eaa14f7399463a3001585b905f0 100644
--- a/src/test/java/de/tla2b/expression/TestComplexExpression.java
+++ b/src/test/java/de/tla2b/expression/ComplexExpressionTest.java
@@ -8,7 +8,7 @@ import org.junit.Test;
import static de.tla2b.util.TestUtil.compareExpr;
-public class TestComplexExpression {
+public class ComplexExpressionTest {
@Test
public void testExcept() throws Exception {
diff --git a/src/test/java/de/tla2b/prettyprintb/ExtensibleRecordTest.java b/src/test/java/de/tla2b/prettyprintb/ExtensibleRecordTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..9438ef8fbe49dcc0d5f098c6a02ba665bc033ca7
--- /dev/null
+++ b/src/test/java/de/tla2b/prettyprintb/ExtensibleRecordTest.java
@@ -0,0 +1,85 @@
+package de.tla2b.prettyprintb;
+
+import static de.tla2b.util.TestUtil.compare;
+
+import org.junit.Test;
+
+public class ExtensibleRecordTest {
+
+ @Test
+ public void testRecord1() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "ASSUME [a |-> 1] = [b |-> TRUE, a |-> 4] \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES rec(b:{}, a:{(TRUE,1)}) = rec(b:{(TRUE,TRUE)}, a:{(TRUE,4)}) \n"
+ + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testRecord2() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "ASSUME [a |-> 1] = [b |-> TRUE] \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES rec(b:{}, a:{(TRUE,1)}) = rec(b:{(TRUE,TRUE)}, a:{}) \n"
+ + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testSelect() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "CONSTANTS k \n"
+ + "ASSUME k = [a |-> 1] /\\ k # [b |-> 1] /\\ k.a = 1 \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "ABSTRACT_CONSTANTS k \n"
+ + "PROPERTIES k : struct(b:POW(BOOL * INTEGER), a:POW(BOOL * INTEGER)) & ((k = rec(b:{}, a:{(TRUE,1)}) & k /= rec(b:{(TRUE,1)}, a:{})) & (k'a)(TRUE) = 1) \n"
+ + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testSelect2() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "ASSUME [a |-> 1].b = TRUE \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES (rec(a:{(TRUE,1)}, b:{})'b)(TRUE) = TRUE \n"
+ + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testStructExpansion() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "ASSUME [a: {2}] = [a : {1}, b : BOOLEAN] \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES struct(a:POW(BOOL * {2}), b:POW(BOOL * BOOL)) = struct(a:POW(BOOL * {1}), b:POW(BOOL * BOOL)) \n"
+ + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testRecExpansion2() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "CONSTANTS k \n"
+ + "ASSUME k = [a |-> 1] /\\ TRUE = k.b \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "ABSTRACT_CONSTANTS k \n"
+ + "PROPERTIES k : struct(a:POW(BOOL * INTEGER), b:POW(BOOL * BOOL)) & (k = rec(a:{(TRUE,1)}, b:{}) & TRUE = (k'b)(TRUE)) \n"
+ + "END";
+ compare(expected, module);
+ }
+
+}
diff --git a/src/test/java/de/tla2b/prettyprintb/RecordTest.java b/src/test/java/de/tla2b/prettyprintb/RecordTest.java
index 92fa439b707ee0d5c9642c773bcf25fb748991d6..5fba3bc60d7fb5e766598d11d11f3722182654a7 100644
--- a/src/test/java/de/tla2b/prettyprintb/RecordTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/RecordTest.java
@@ -33,18 +33,6 @@ public class RecordTest {
compare(expected, module);
}
-
- @Test
- public void testStructExpansion() throws Exception {
- final String module = "-------------- MODULE Testing ----------------\n"
- + "ASSUME [a: {2}] = [a : {1}, b : BOOLEAN] \n"
- + "=================================";
-
- final String expected = "MACHINE Testing\n"
- + "PROPERTIES struct(a : {2},b : BOOL) = struct(a : {1},b : BOOL) \n"
- + "END";
- compare(expected, module);
- }
/**********************************************************************
* Record: [L1 |-> e1, L2 |-> e2]