diff --git a/build.gradle b/build.gradle
index c7e02d1234f31f89a306cbc191bcc5fca1af1c58..4d3d2c6a75e44747331151cb00aa252c0b0e2b1b 100644
--- a/build.gradle
+++ b/build.gradle
@@ -2,7 +2,7 @@ apply plugin: 'java'
apply plugin: 'eclipse'
apply plugin: 'maven'
apply plugin: 'jacoco'
-//apply plugin: 'findbugs'
+apply plugin: 'findbugs'
project.version = '1.0.5-SNAPSHOT'
project.group = 'de.prob'
@@ -33,8 +33,6 @@ dependencies {
//compile(group: 'de.prob', name: 'de.prob.core.kernel', version: '2.0.0-milestone-13-SNAPSHOT')
-
-
testCompile (group: 'junit', name: 'junit', version: '4.7')
releaseJars (group: 'de.tla', name: 'tlatools', version: '1.0.0-SNAPSHOT')
@@ -57,16 +55,16 @@ jacocoTestReport {
}
}
-//tasks.withType(FindBugs) {
-// reports {
-// xml.enabled = false
-// html.enabled = true
-// }
-//}
+tasks.withType(FindBugs) {
+ reports {
+ xml.enabled = false
+ html.enabled = true
+ }
+}
-//findbugs {
-// ignoreFailures = true
-//}
+findbugs {
+ ignoreFailures = true
+}
test {
diff --git a/src/main/java/de/tla2b/analysis/BOperation.java b/src/main/java/de/tla2b/analysis/BOperation.java
index 8ffcf1b7efb75173da9892a6fa577fd8b8151cf6..43aaac2ac6309ce1fe7d4407023cfc6782f8700c 100644
--- a/src/main/java/de/tla2b/analysis/BOperation.java
+++ b/src/main/java/de/tla2b/analysis/BOperation.java
@@ -208,7 +208,7 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
}
}
-
+ default:
}
}
}
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index 3869d37dc9e7cebab80071d8d34670cf62d46ef9..a2a965cdd9181208d8a1bf6f45fb062163c1b1d4 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -239,7 +239,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
FormalParamNode p = params[i];
if (p.getArity() > 0) {
throw new FrontEndException(String.format(
- "TLA2B do not support 2nd-order operators: '%s'\n %s ",
+ "TLA2B do not support 2nd-order operators: '%s'%n %s ",
def.getName(), def.getLocation()));
}
UntypedType u = new UntypedType();
@@ -288,7 +288,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
} catch (UnificationException e) {
throw new TypeErrorException(
String.format(
- "Expected %s, found %s at '%s'(assigned in the configuration file),\n%s ",
+ "Expected %s, found %s at '%s'(assigned in the configuration file),%n%s ",
expected, valueNode.getType(),
valueNode.getValue(), exprNode.getLocation()));
}
@@ -303,7 +303,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return IntType.getInstance().unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found INTEGER at '%s',\n%s ", expected,
+ "Expected %s, found INTEGER at '%s',%n%s ", expected,
((NumeralNode) exprNode).val(), exprNode.getLocation()));
}
case StringKind: {
@@ -311,7 +311,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return StringType.getInstance().unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found STRING at '%s',\n%s ", expected,
+ "Expected %s, found STRING at '%s',%n%s ", expected,
((StringNode) exprNode).getRep(),
exprNode.getLocation()));
}
@@ -326,7 +326,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return res;
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found %s at '@',\n%s ", expected, type,
+ "Expected %s, found %s at '@',%n%s ", expected, type,
exprNode.getLocation()));
}
@@ -378,7 +378,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return result;
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found %s at constant '%s',\n%s",
+ "Expected %s, found %s at constant '%s',%n%s",
expected, c, con.getName(), n.getLocation())
);
@@ -404,7 +404,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return result;
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found %s at variable '%s',\n%s",
+ "Expected %s, found %s at variable '%s',%n%s",
expected, v, vName, n.getLocation()));
}
}
@@ -426,7 +426,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return result;
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found %s at parameter '%s',\n%s",
+ "Expected %s, found %s at parameter '%s',%n%s",
expected, t, pName, n.getLocation()));
}
}
@@ -451,7 +451,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found %s at definition '%s',\n%s",
+ "Expected %s, found %s at definition '%s',%n%s",
expected, found, def.getName(), n.getLocation()));
}
boolean untyped = false;
@@ -464,7 +464,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
if (pType == null) {
pType = new UntypedType();
// throw new RuntimeException("Parameter " + p.getName()
- // + " has no type yet!\n" + p.getLocation());
+ // + " has no type yet!%n" + p.getLocation());
}
pType = pType.cloneTLAType();
if (pType.isUntyped())
@@ -520,7 +520,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
BoolType.getInstance().unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found BOOL at '%s',\n%s", expected, n
+ "Expected %s, found BOOL at '%s',%n%s", expected, n
.getOperator().getName(), n.getLocation()));
}
TLAType left = visitExprOrOpArgNode(n.getArgs()[0],
@@ -545,7 +545,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
BoolType.getInstance().unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found BOOL at '%s',\n%s", expected, n
+ "Expected %s, found BOOL at '%s',%n%s", expected, n
.getOperator().getName(), n.getLocation()));
}
for (int i = 0; i < n.getArgs().length; i++) {
@@ -564,7 +564,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
BoolType.getInstance().unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found BOOL at '%s',\n%s", expected, n
+ "Expected %s, found BOOL at '%s',%n%s", expected, n
.getOperator().getName(), n.getLocation()));
}
evalBoundedVariables(n);
@@ -582,7 +582,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found POW(_A) at set enumeration,\n%s",
+ "Expected %s, found POW(_A) at set enumeration,%n%s",
expected, n.getLocation()));
}
TLAType current = found.getSubType();
@@ -597,7 +597,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
{
if (!BoolType.getInstance().compare(expected)) {
throw new TypeErrorException(String.format(
- "Expected %s, found BOOL at '%s',\n%s", expected, n
+ "Expected %s, found BOOL at '%s',%n%s", expected, n
.getOperator().getName(), n.getLocation()));
}
TLAType element = visitExprOrOpArgNode(n.getArgs()[0],
@@ -616,7 +616,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found POW(_A) at '%s',\n%s", expected, n
+ "Expected %s, found POW(_A) at '%s',%n%s", expected, n
.getOperator().getName(), n.getLocation()));
}
TLAType left = visitExprOrOpArgNode(n.getArgs()[0], found);
@@ -630,7 +630,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
BoolType.getInstance().unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found BOOL at '%s',\n%s", expected, n
+ "Expected %s, found BOOL at '%s',%n%s", expected, n
.getOperator().getName(), n.getLocation()));
}
TLAType left = visitExprOrOpArgNode(n.getArgs()[0], new SetType(
@@ -651,7 +651,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found %s at '%s',\n%s", expected, found,
+ "Expected %s, found %s at '%s',%n%s", expected, found,
n.getOperator().getName(), n.getLocation()));
}
visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
@@ -665,7 +665,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found POW(_A) at '%s',\n%s", expected, n
+ "Expected %s, found POW(_A) at '%s',%n%s", expected, n
.getOperator().getName(), n.getLocation()));
}
evalBoundedVariables(n);
@@ -680,7 +680,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found POW(_A) at 'SUBSET',\n%s",
+ "Expected %s, found POW(_A) at 'SUBSET',%n%s",
expected, n.getLocation()));
}
visitExprOrOpArgNode(n.getArgs()[0], found.getSubType());
@@ -694,7 +694,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found POW(_A) at 'SUBSET',\n%s",
+ "Expected %s, found POW(_A) at 'SUBSET',%n%s",
expected, n.getLocation()));
}
SetType setOfSet = (SetType) visitExprOrOpArgNode(n.getArgs()[0],
@@ -743,7 +743,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found %s at Tuple,\n%s", expected, found,
+ "Expected %s, found %s at Tuple,%n%s", expected, found,
n.getLocation()));
}
n.setToolObject(TYPE_ID, found);
@@ -845,8 +845,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
res = new SetType(func.getDomain()).unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected '%s', found '%s' at 'DOMAIN(..)',\n%s",
- expected, n.getLocation()));
+ "Expected '%s', found '%s' at 'DOMAIN(..)',%n%s",
+ expected, func, n.getLocation()));
}
return res;
}
@@ -866,7 +866,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected '%s', found '%s' at Set of Function,\n%s",
+ "Expected '%s', found '%s' at Set of Function,%n%s",
expected, found, n.getLocation()));
}
return found;
@@ -897,7 +897,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found %s at Cartesian Product,\n%s",
+ "Expected %s, found %s at Cartesian Product,%n%s",
expected, found, n.getLocation()));
}
return found;
@@ -922,13 +922,11 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found %s at Set of Records,\n%s",
+ "Expected %s, found %s at Set of Records,%n%s",
expected, found, n.getLocation()));
}
n.setToolObject(TYPE_ID, found);
- if (found instanceof AbstractHasFollowers) {
- ((AbstractHasFollowers) found).addFollower(n);
- }
+ found.addFollower(n);
return found;
}
@@ -946,13 +944,12 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found %s at Record,\n%s", expected,
+ "Expected %s, found %s at Record,%n%s", expected,
found, n.getLocation()));
}
n.setToolObject(TYPE_ID, found);
- if (found instanceof AbstractHasFollowers) {
- ((AbstractHasFollowers) found).addFollower(n);
- }
+ found.addFollower(n);
+
recList.add(n);
return found;
@@ -972,7 +969,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
r = r.unify(expectedStruct);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Struct has no field %s with type %s: %s\n%s",
+ "Struct has no field %s with type %s: %s%n%s",
fieldName, r.getType(fieldName), r, n.getLocation()));
}
n.setToolObject(TYPE_ID, r);
@@ -1019,9 +1016,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
TLAType found = new UntypedType();
FormalParamNode x = n.getUnbdedQuantSymbols()[0];
x.setToolObject(TYPE_ID, found);
- if (found instanceof AbstractHasFollowers) {
- ((AbstractHasFollowers) found).addFollower(x);
- }
+ ((AbstractHasFollowers) found).addFollower(x);
visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
found = (TLAType) x.getToolObject(TYPE_ID);
@@ -1029,7 +1024,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found %s at 'CHOOSE',\n%s", expected,
+ "Expected %s, found %s at 'CHOOSE',%n%s", expected,
found, n.getLocation()));
}
return found;
@@ -1050,7 +1045,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found %s at 'CHOOSE',\n%s", expected,
+ "Expected %s, found %s at 'CHOOSE',%n%s", expected,
found, n.getLocation()));
}
FormalParamNode x = n.getBdedQuantSymbolLists()[0][0];
@@ -1112,7 +1107,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
tuple = (TupleType) tuple.unify(subType);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found %s ,\n%s", tuple, subType,
+ "Expected %s, found %s ,%n%s", tuple, subType,
n.getLocation()));
}
@@ -1191,7 +1186,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
t = t.unify(s);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found %s at 'EXCEPT',\n%s", t, s,
+ "Expected %s, found %s at 'EXCEPT',%n%s", t, s,
pair.getLocation()));
}
@@ -1220,7 +1215,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
t = t.unify(func);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found %s at 'EXCEPT',\n%s", t, func,
+ "Expected %s, found %s at 'EXCEPT',%n%s", t, func,
pair.getLocation()));
}
}
@@ -1270,7 +1265,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
BoolType.getInstance().unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found BOOL at '%s',\n%s", expected, n
+ "Expected %s, found BOOL at '%s',%n%s", expected, n
.getOperator().getName(), n.getLocation()));
}
for (int i = 0; i < n.getArgs().length; i++) {
@@ -1289,7 +1284,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
IntType.getInstance().unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found INTEGER at '%s',\n%s", expected, n
+ "Expected %s, found INTEGER at '%s',%n%s", expected, n
.getOperator().getName(), n.getLocation()));
}
for (int i = 0; i < n.getArgs().length; i++) {
@@ -1304,7 +1299,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
expected.unify(new SetType(IntType.getInstance()));
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found POW(INTEGER) at '..',\n%s",
+ "Expected %s, found POW(INTEGER) at '..',%n%s",
expected, n.getLocation()));
}
@@ -1322,7 +1317,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return found;
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found POW(INTEGER) at 'Nat',\n%s",
+ "Expected %s, found POW(INTEGER) at 'Nat',%n%s",
expected, n.getLocation()));
}
}
@@ -1338,7 +1333,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return found;
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found POW(INTEGER) at 'Int',\n%s",
+ "Expected %s, found POW(INTEGER) at 'Int',%n%s",
expected, n.getLocation()));
}
}
@@ -1349,7 +1344,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
IntType.getInstance().unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found INTEGER at '-',\n%s", expected,
+ "Expected %s, found INTEGER at '-',%n%s", expected,
n.getLocation()));
}
visitExprOrOpArgNode(n.getArgs()[0], IntType.getInstance());
@@ -1365,7 +1360,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
BoolType.getInstance().unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found BOOL at 'IsFiniteSet',\n%s",
+ "Expected %s, found BOOL at 'IsFiniteSet',%n%s",
expected, n.getLocation()));
}
visitExprOrOpArgNode(n.getArgs()[0], new SetType(new UntypedType()));
@@ -1378,7 +1373,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
IntType.getInstance().unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found INTEGER at 'Cardinality',\n%s",
+ "Expected %s, found INTEGER at 'Cardinality',%n%s",
expected, n.getLocation()));
}
visitExprOrOpArgNode(n.getArgs()[0], new SetType(new UntypedType()));
@@ -1399,7 +1394,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
set_of_seq = set_of_seq.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found %s at 'Seq',\n%s", expected,
+ "Expected %s, found %s at 'Seq',%n%s", expected,
set_of_seq, n.getLocation()));
}
return set_of_seq;
@@ -1410,7 +1405,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
IntType.getInstance().unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found INTEGER at 'Len',\n%s", expected,
+ "Expected %s, found INTEGER at 'Len',%n%s", expected,
n.getLocation()));
}
visitExprOrOpArgNode(n.getArgs()[0],
@@ -1427,7 +1422,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found POW(INTEGER*_A) at '\\o',\n%s",
+ "Expected %s, found POW(INTEGER*_A) at '\\o',%n%s",
expected, n.getLocation()));
}
return found;
@@ -1443,7 +1438,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found %s at 'Append',\n%s", expected,
+ "Expected %s, found %s at 'Append',%n%s", expected,
found, n.getLocation()));
}
return found;
@@ -1459,7 +1454,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found %s at 'Head',\n%s", expected,
+ "Expected %s, found %s at 'Head',%n%s", expected,
found, n.getLocation()));
}
return found;
@@ -1473,7 +1468,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found %s at 'Tail',\n%s", expected,
+ "Expected %s, found %s at 'Tail',%n%s", expected,
found, n.getLocation()));
}
return found;
@@ -1489,7 +1484,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found %s at 'SubSeq',\n%s", expected,
+ "Expected %s, found %s at 'SubSeq',%n%s", expected,
found, n.getLocation()));
}
return found;
@@ -1510,7 +1505,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
IntType.getInstance().unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found INTEGER at '%s',\n%s", expected, n
+ "Expected %s, found INTEGER at '%s',%n%s", expected, n
.getOperator().getName(), n.getLocation()));
}
visitExprOrOpArgNode(n.getArgs()[0],
@@ -1527,7 +1522,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found %s at 'PermutedSequences',\n%s",
+ "Expected %s, found %s at 'PermutedSequences',%n%s",
expected, found, n.getLocation()));
}
return found;
@@ -1546,8 +1541,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found %s at '%s',\n%s", expected, n
- .getOperator().getName(), n.getLocation()));
+ "Expected %s, found %s at '%s',%n%s", expected, found,
+ n.getOperator().getName(), n.getLocation()));
}
return found;
}
@@ -1568,7 +1563,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found %s at '%s',\n%s", expected, found,
+ "Expected %s, found %s at '%s',%n%s", expected, found,
n.getOperator().getName(), n.getLocation()));
}
return found;
@@ -1584,7 +1579,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return found;
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found POW(BOOL) at 'BOOLEAN',\n%s",
+ "Expected %s, found POW(BOOL) at 'BOOLEAN',%n%s",
expected, n.getLocation()));
}
@@ -1595,7 +1590,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return found;
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
- "Expected %s, found POW(STRING) at 'STRING',\n%s",
+ "Expected %s, found POW(STRING) at 'STRING',%n%s",
expected, n.getLocation()));
}
@@ -1606,7 +1601,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return BoolType.getInstance();
} catch (Exception e) {
throw new TypeErrorException(String.format(
- "Expected %s, found BOOL at '%s',\n%s", expected, n
+ "Expected %s, found BOOL at '%s',%n%s", expected, n
.getOperator().getName(), n.getLocation()));
}
diff --git a/src/main/java/de/tla2b/analysis/UsedExternalFunctions.java b/src/main/java/de/tla2b/analysis/UsedExternalFunctions.java
index 8fabe8f168cdae4700e6f5bd8e1a2e53064c68d4..97576a973d7066a8e466c80f84119a998af53dc2 100644
--- a/src/main/java/de/tla2b/analysis/UsedExternalFunctions.java
+++ b/src/main/java/de/tla2b/analysis/UsedExternalFunctions.java
@@ -41,6 +41,7 @@ public class UsedExternalFunctions extends AbstractASTVisitor {
case OPCODE_bc: {
usedExternalFunctions.add(EXTERNAL_FUNCTIONS.CHOOSE);
}
+ default:
}
ExprNode[] in = n.getBdedQuantBounds();
diff --git a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java b/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
index eb10b360a2b0ed177c7fdf52f4f33286df73b8d3..2f3ac42f9f5036c741e843d382de1a0ad4a6778a 100644
--- a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
+++ b/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
@@ -53,10 +53,10 @@ public class ConfigfileEvaluator {
private final ArrayList<OpDefNode> invariantNodeList = new ArrayList<OpDefNode>();
private ArrayList<String> enumeratedSet;
private LinkedHashMap<String, EnumType> enumeratedTypes;
- private Hashtable<OpDeclNode, ValueObj> constantAssignments;
+ public Hashtable<OpDeclNode, ValueObj> constantAssignments;
// k = 1, the ValueObj describes the right side of the assignment and
// contains it type
- private Hashtable<OpDefNode, ValueObj> operatorAssignments;
+ public Hashtable<OpDefNode, ValueObj> operatorAssignments;
// def = 1
private ArrayList<OpDefNode> operatorModelvalues;
@@ -66,10 +66,10 @@ public class ConfigfileEvaluator {
// a TLA+ constant if the constant is substituted by a modelvalue with the
// same name (the constant name is moved to an enumerated set) or if the
// constants has arguments and is overriden by an operator
- private Hashtable<OpDefNode, OpDefNode> operatorOverrideTable;
+ public Hashtable<OpDefNode, OpDefNode> operatorOverrideTable;
// This table contains mappings for operators which are overridden in the
// configuration file
- private Hashtable<OpDeclNode, OpDefNode> constantOverrideTable;
+ public Hashtable<OpDeclNode, OpDefNode> constantOverrideTable;
// This table contains mappings for constants which are overridden in the
// configuration file. All constants with arguments have to be overridden in
@@ -240,7 +240,7 @@ public class ConfigfileEvaluator {
if (conNode.getArity() != rightDefNode.getArity()) {
throw new ConfigFileErrorException(
String.format(
- "Invalid substitution for %s.\n Constant %s has %s arguments while %s has %s arguments.",
+ "Invalid substitution for %s.%n Constant %s has %s arguments while %s has %s arguments.",
left, left, conNode.getArity(), right,
rightDefNode.getArity()));
}
@@ -254,7 +254,7 @@ public class ConfigfileEvaluator {
if (defNode.getArity() != rightDefNode.getArity()) {
throw new ConfigFileErrorException(
String.format(
- "Invalid substitution for %s.\n Operator %s has %s arguments while %s has %s arguments.",
+ "Invalid substitution for %s.%n Operator %s has %s arguments while %s has %s arguments.",
left, left, defNode.getArity(), right,
rightDefNode.getArity()));
}
@@ -402,7 +402,7 @@ public class ConfigfileEvaluator {
if (defNode.getArity() != rightDefNode.getArity()) {
throw new ConfigFileErrorException(
String.format(
- "Invalid substitution for %s.\n Operator %s has %s arguments while %s has %s arguments.",
+ "Invalid substitution for %s.%n Operator %s has %s arguments while %s has %s arguments.",
left, left, defNode.getArity(), right,
rightDefNode.getArity()));
}
@@ -421,7 +421,7 @@ public class ConfigfileEvaluator {
// */
// throw new ConfigFileErrorException(
// String.format(
- // "Invalid substitution for constant '%s' of module '%s'.\n A Constant of an instanced module can not be overriden.",
+ // "Invalid substitution for constant '%s' of module '%s'.%n A Constant of an instanced module can not be overriden.",
// left, mNode.getName().toString()));
// }
}
@@ -430,7 +430,7 @@ public class ConfigfileEvaluator {
if (conNode.getArity() != rightDefNode.getArity()) {
throw new ConfigFileErrorException(
String.format(
- "Invalid substitution for %s.\n Constant %s has %s arguments while %s has %s arguments.",
+ "Invalid substitution for %s.%n Constant %s has %s arguments while %s has %s arguments.",
left, left, conNode.getArity(), right,
rightDefNode.getArity()));
}
diff --git a/src/main/java/de/tla2b/old/AbstractExpressionPrinter.java b/src/main/java/de/tla2b/old/AbstractExpressionPrinter.java
deleted file mode 100644
index 80fdbbab4748ee01725bb0067d154f59cfed3ea5..0000000000000000000000000000000000000000
--- a/src/main/java/de/tla2b/old/AbstractExpressionPrinter.java
+++ /dev/null
@@ -1,1390 +0,0 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
-package de.tla2b.old;
-
-import java.util.ArrayList;
-import java.util.Hashtable;
-import java.util.LinkedList;
-
-import de.tla2b.config.TLCValueNode;
-import de.tla2b.global.BBuildIns;
-import de.tla2b.global.BBuiltInOPs;
-import de.tla2b.global.Priorities;
-import de.tla2b.global.TranslationGlobals;
-import de.tla2b.types.EnumType;
-import de.tla2b.types.FunctionType;
-import de.tla2b.types.IType;
-import de.tla2b.types.SetType;
-import de.tla2b.types.StructType;
-import de.tla2b.types.TLAType;
-import de.tla2b.types.TupleType;
-import tla2sany.semantic.ASTConstants;
-import tla2sany.semantic.AtNode;
-import tla2sany.semantic.ExprNode;
-import tla2sany.semantic.ExprOrOpArgNode;
-import tla2sany.semantic.FormalParamNode;
-import tla2sany.semantic.LetInNode;
-import tla2sany.semantic.NumeralNode;
-import tla2sany.semantic.OpApplNode;
-import tla2sany.semantic.OpDefNode;
-import tla2sany.semantic.StringNode;
-import tla2sany.semantic.SymbolNode;
-import tlc2.tool.BuiltInOPs;
-
-public abstract class AbstractExpressionPrinter extends BuiltInOPs implements
- ASTConstants, BBuildIns, Priorities, TranslationGlobals {
- // private int substitutionId = 10;
-
- final int NOBOOL = 0;
- final int VALUE = 1;
- final int PREDICATE = 2;
- final int VALUEORPREDICATE = 3;
-
- protected ExprReturn visitExprOrOpArgNode(ExprOrOpArgNode n, DContext d,
- int expected) {
- if (n instanceof ExprNode) {
- return visitExprNode((ExprNode) n, d, expected);
- } else {
- throw new RuntimeException("OpArgNode not implemented jet");
- }
- }
-
- protected ExprReturn visitExprNode(ExprNode n, DContext d, int expected) {
- StringBuilder out = new StringBuilder();
- switch (n.getKind()) {
- case OpApplKind:
- return visitOpApplNode((OpApplNode) n, d, expected);
-
- case NumeralKind: {
- // this is hack to represent a TLCValue in abstract syntax tree of
- // the module
- if (n instanceof TLCValueNode) {
- out.append(((TLCValueNode) n).getValue());
- return new ExprReturn(out);
- }
- out.append(((NumeralNode) n).val());
- return new ExprReturn(out);
- }
-
- case StringKind: {
- StringNode s = (StringNode) n;
- out.append("\"" + s.getRep() + "\"");
- return new ExprReturn(out);
- }
-
- case LetInKind: {
- LetInNode letInNode = (LetInNode) n;
- return visitLetInNode(letInNode, d, expected);
-
- }
- case AtNodeKind: { // @
- AtNode at = (AtNode) n;
- String base = visitExprNode(at.getAtBase(), d, NOBOOL).out
- .toString();
- TLAType t = (TLAType) at.getExceptRef().getToolObject(TYPE_ID);
-
- OpApplNode seq = at.getAtModifier();
-
- LinkedList<ExprOrOpArgNode> list = new LinkedList<ExprOrOpArgNode>();
- for (int j = 0; j < seq.getArgs().length; j++) {
- list.add(seq.getArgs()[j]);
- }
- out.append(base);
- out.append(evalAtValue(list, t));
- return new ExprReturn(out);
- }
- case TLCValueKind: {
- TLCValueNode val = (TLCValueNode) n;
- return new ExprReturn(val.getValue().toString());
- }
-
- }
- throw new RuntimeException(n.toString(2));
- }
-
- /**
- * @param list
- * @param t
- */
- private StringBuilder evalAtValue(LinkedList<ExprOrOpArgNode> list,
- TLAType t) {
- StringBuilder sb = new StringBuilder();
- if (list.size() == 0)
- return sb;
- ExprOrOpArgNode first = list.poll();
- if (t instanceof StructType) {
- StructType s = (StructType) t;
- sb.append("'");
- String fieldName = ((StringNode) first).getRep().toString();
- sb.append(fieldName);
- return sb.append(evalAtValue(list, s.getType(fieldName)));
- } else {
- FunctionType func = (FunctionType) t;
-
- TLAType range = func.getRange();
- sb.append("(");
-
- if (first instanceof OpApplNode
- && ((OpApplNode) first).getOperator().getName().toString()
- .equals("$Tuple")) {
- OpApplNode domOpAppl = (OpApplNode) first;
- for (int j = 0; j < domOpAppl.getArgs().length; j++) {
- if (j != 0) {
- sb.append(", ");
- }
- sb.append(visitExprOrOpArgNode(domOpAppl.getArgs()[j],
- new DContext(), VALUE).out);
- }
- } else {
- sb.append(visitExprOrOpArgNode(first, new DContext(), VALUE).out);
- }
- sb.append(")");
- return sb.append(evalAtValue(list, range));
- }
- }
-
- protected ExprReturn visitLetInNode(LetInNode l, DContext d, int expected) {
- for (int i = 0; i < l.getLets().length; i++) {
- // do something
- }
- return visitExprNode(l.getBody(), d, VALUEORPREDICATE);
- }
-
- private ExprReturn visitOpApplNode(OpApplNode n, DContext d, int expected) {
- StringBuilder out = new StringBuilder();
- switch (n.getOperator().getKind()) {
- case ConstantDeclKind: {
- out.append(getPrintName(n.getOperator()));
- if (expected == PREDICATE) {
- out.append(" = TRUE");
- return new ExprReturn(out, P_equals);
- }
- return new ExprReturn(out);
- }
- case VariableDeclKind: {
- out.append(getPrintName(n.getOperator()));
- if (expected == PREDICATE) {
- out.append(" = TRUE");
- return new ExprReturn(out, P_equals);
- }
- return new ExprReturn(out);
- }
- case BuiltInKind:
- return evalBuiltInKind(n, d, expected);
-
- case FormalParamKind: {
- return visitFormalParamNode(n, d, expected);
- }
-
- case UserDefinedOpKind: {
- return visitUserdefinedOp(n, d, expected);
- }
-
- }
- throw new RuntimeException(n.toString(2));
- }
-
- /**
- * @param n
- * @param d
- * @param expected
- * @return
- */
- protected ExprReturn visitFormalParamNode(OpApplNode n, DContext d,
- int expected) {
- StringBuilder out = new StringBuilder();
- out.append(getPrintName(n.getOperator()));
- if (expected == PREDICATE) {
- out.append(" = TRUE");
- return new ExprReturn(out, P_equals);
- }
- return new ExprReturn(out);
- }
-
- /**
- * @param n
- * @param d
- * @param expected
- * @return
- */
- protected ExprReturn visitUserdefinedOp(OpApplNode n, DContext d,
- int expected) {
- StringBuilder out = new StringBuilder();
- OpDefNode def = (OpDefNode) n.getOperator();
- // Operator is a B built-in operator
- if (BBuiltInOPs.contains(def.getName())
- && STANDARD_MODULES.contains(def.getSource()
- .getOriginallyDefinedInModuleNode().getName()
- .toString())) {
- return evalBBuiltIns(n, d, expected);
- }
-
- out.append(getPrintName(def));
-
- if (n.getArgs().length > 0) {
- out.append("(");
- for (int i = 0; i < n.getArgs().length; i++) {
- out.append(visitExprOrOpArgNode(n.getArgs()[i], d, VALUE).out);
- if (i < n.getArgs().length - 1) {
- out.append(", ");
- }
- }
- out.append(")");
-
- }
- TLAType defType = (TLAType) n.getToolObject(TYPE_ID);
- if (defType != null && defType.getKind() == IType.BOOL) {
- return makeBoolValue(out, expected, P_max);
- }
- return new ExprReturn(out);
- }
-
- /**
- * @param n
- * @param d
- * @param expected
- * @return
- */
- private ExprReturn evalBuiltInKind(OpApplNode n, DContext d, int expected) {
- StringBuilder out = new StringBuilder();
- switch (getOpCode(n.getOperator().getName())) {
-
- /**********************************************************************
- * equality and disequality: =, #, /=
- **********************************************************************/
- case OPCODE_eq: { // =
- out = evalOpMoreArgs(n, " = ", d, VALUE, P_equals);
- return makeBoolValue(out, expected, P_equals);
- }
-
- case OPCODE_noteq: // /=
- {
- out = evalOpMoreArgs(n, " /= ", d, VALUE, P_noteq);
- return makeBoolValue(out, expected, P_noteq);
- }
-
- /**********************************************************************
- * Logic Operators
- **********************************************************************/
- case OPCODE_cl: // $ConjList
- {
- for (int i = 0; i < n.getArgs().length; i++) {
- if (i == 0) {
- out.append(brackets(
- visitExprOrOpArgNode(n.getArgs()[i], d, PREDICATE),
- P_and, true));
- } else {
- out.append("\n" + d.indent + " & ");
- out.append(brackets(
- visitExprOrOpArgNode(n.getArgs()[i], d, PREDICATE),
- P_and, false));
- }
- }
- return makeBoolValue(out, expected, P_and);
- }
- case OPCODE_land: // \land
- {
- out = evalOpMoreArgs(n, " & ", d, PREDICATE, P_and);
- return makeBoolValue(out, expected, P_and);
- }
- case OPCODE_dl: // $DisjList
- {
- for (int i = 0; i < n.getArgs().length; i++) {
- if (i == 0) {
- out.append(brackets(
- visitExprOrOpArgNode(n.getArgs()[i], d, PREDICATE),
- P_or, true));
- } else {
- out.append("\n" + d.indent + " or ");
- out.append(brackets(
- visitExprOrOpArgNode(n.getArgs()[i], d, PREDICATE),
- P_or, false));
- }
- }
- return makeBoolValue(out, expected, P_or);
- }
-
- case OPCODE_lor: // \/
- {
- out = evalOpMoreArgs(n, " or ", d, PREDICATE, P_or);
- return makeBoolValue(out, expected, P_or);
- }
- case OPCODE_equiv: // \equiv
- {
- out = evalOpMoreArgs(n, " <=> ", d, PREDICATE, P_equiv);
- return makeBoolValue(out, expected, P_equiv);
- }
- case OPCODE_implies: // =>
- {
- out = evalOpMoreArgs(n, " => ", d, PREDICATE, P_implies);
- return makeBoolValue(out, expected, P_implies);
- }
-
- case OPCODE_lnot: { // \lnot
- out.append("not(");
- out.append(visitExprOrOpArgNode(n.getArgs()[0], d, PREDICATE).out);
- out.append(")");
- return makeBoolValue(out, expected, P_max);
- }
-
- case OPCODE_be: { // \E x \in S : P
- return evalBoundedQuantor(n, d, expected, "#");
- }
-
- case OPCODE_bf: { // \A x \in S : P
- return evalBoundedQuantor(n, d, expected, "!");
- }
-
- /**********************************************************************
- * Set Operators
- **********************************************************************/
- case OPCODE_se: // SetEnumeration {..}
- {
- out.append("{");
- out.append(evalOpMoreArgs(n, ", ", d, VALUE, P_comma));
- out.append("}");
- return new ExprReturn(out, P_max);
- }
-
- case OPCODE_in: // \in
- {
- ExprReturn r = visitExprOrOpArgNode(n.getArgs()[0], d, VALUE);
- out.append(brackets(r, P_in, true));
- out.append(" : ");
- r = visitExprOrOpArgNode(n.getArgs()[1], d, NOBOOL);
- out.append(brackets(r, P_in, false));
- return makeBoolValue(out, expected, P_in);
- }
- case OPCODE_notin: // \notin
- {
- ExprReturn r = visitExprOrOpArgNode(n.getArgs()[0], d, VALUE);
- out.append(brackets(r, P_notin, true));
- out.append(" /: ");
- r = visitExprOrOpArgNode(n.getArgs()[1], d, NOBOOL);
- out.append(brackets(r, P_notin, false));
- return makeBoolValue(out, expected, P_notin);
- }
-
- case OPCODE_setdiff: // set difference
- {
- out = evalOpMoreArgs(n, " - ", d, NOBOOL, P_setdiff);
- return new ExprReturn(out, P_setdiff);
- }
-
- case OPCODE_cup: // set union
- {
- out = evalOpMoreArgs(n, " \\/ ", d, NOBOOL, P_union);
- return new ExprReturn(out, P_union);
- }
-
- case OPCODE_cap: // set intersection
- {
- out = evalOpMoreArgs(n, " /\\ ", d, NOBOOL, P_intersect);
- return new ExprReturn(out, P_intersect);
- }
-
- case OPCODE_subseteq: // \subseteq {1,2} <: {1,2,3}
- {
- out = evalOpMoreArgs(n, " <: ", d, NOBOOL, P_subseteq);
- return makeBoolValue(out, expected, P_subseteq);
- }
-
- case OPCODE_subset: // SUBSET
- {
- out.append("POW(");
- out.append(visitExprOrOpArgNode(n.getArgs()[0], d, NOBOOL).out);
- out.append(")");
- return new ExprReturn(out);
- }
-
- case OPCODE_union: // Union - Union{{1},{2}}
- {
- out.append("union(");
- out.append(visitExprOrOpArgNode(n.getArgs()[0], d, NOBOOL).out);
- out.append(")");
- return new ExprReturn(out);
- }
-
- /**********************************************************************
- * Set Constructor
- **********************************************************************/
- case OPCODE_sso: { // $SubsetOf Represents {x \in S : P}
- // TODO tuple with more than 2 arguments
- FormalParamNode[][] params = n.getBdedQuantSymbolLists();
- //ExprNode[] bounds = n.getBdedQuantBounds();
-
- StringBuilder temp = new StringBuilder();
- if (params[0].length > 0) {
- temp.append("(");
- for (int j = 0; j < params[0].length; j++) {
- FormalParamNode p = params[0][j];
- temp.append(getPrintName(p));
- if (j < params[0].length - 1)
- temp.append(", ");
- }
- temp.append(")");
- } else {
- FormalParamNode p = n.getBdedQuantSymbolLists()[0][0];
- temp.append(getPrintName(p));
- }
-
- out.append("{");
- out.append(temp);
- out.append("|");
- out.append(temp);
- out.append(" : ");
- ExprNode in = n.getBdedQuantBounds()[0];
- out.append(visitExprNode(in, d, NOBOOL).out);
- out.append(" & ");
- out.append(brackets(
- visitExprOrOpArgNode(n.getArgs()[0], d, PREDICATE), P_and,
- false));
- out.append("}");
- return new ExprReturn(out);
- }
-
- case OPCODE_soa: { // $SetOfAll Represents {e : p1 \in S, p2,p3 \in S2}
- out.append("{t_|#");
- FormalParamNode[][] params = n.getBdedQuantSymbolLists();
- ExprNode[] bounds = n.getBdedQuantBounds();
- for (int i = 0; i < bounds.length; i++) {
- for (int j = 0; j < params[i].length; j++) {
- FormalParamNode p = params[i][j];
- out.append(getPrintName(p));
- if (i < bounds.length - 1 || j < params[i].length - 1)
- out.append(", ");
- }
- }
- out.append(".(");
- out.append(visitBounded(n, d));
- out.append(" & t_ = ");
- out.append(visitExprOrOpArgNode(n.getArgs()[0], d, VALUE).out);
- out.append(")}");
- return new ExprReturn(out);
- }
- /***********************************************************************
- * Tuple: Tuple as Function 1..n to Set (Sequence)
- ***********************************************************************/
- case OPCODE_tup: { // $Tuple
- TLAType t = (TLAType) n.getToolObject(TYPE_ID);
- if (t instanceof TupleType) {
- out.append("(");
- out.append(evalOpMoreArgs(n, ", ", d, VALUE, P_comma));
- out.append(")");
- } else {
- out.append("[");
- out.append(evalOpMoreArgs(n, ", ", d, VALUE, P_comma));
- out.append("]");
- }
- return new ExprReturn(out);
- }
-
- /***********************************************************************
- * Cartesian Product: A \X B
- ***********************************************************************/
- case OPCODE_cp: { // $CartesianProd A \X B \X C
- out.append(evalOpMoreArgs(n, "*", d, VALUE, P_times));
- return new ExprReturn(out, P_times);
- }
-
- /***********************************************************************
- * Functions
- ***********************************************************************/
- case OPCODE_nrfs:
- case OPCODE_fc: // Represents [x \in S |-> e].
- case OPCODE_rfs: {
- out.append("%");
- FormalParamNode[][] vars = n.getBdedQuantSymbolLists();
- for (int i = 0; i < vars.length; i++) {
- for (int j = 0; j < vars[i].length; j++) {
- out.append(getPrintName(vars[i][j]));
- if (j < vars[i].length - 1) {
- out.append(",");
- }
- }
- if (i < vars.length - 1) {
- out.append(",");
- }
- }
- out.append(".(");
- out.append(visitBounded(n, d));
- out.append("| ");
- out.append(visitExprOrOpArgNode(n.getArgs()[0], d, VALUE).out);
- out.append(")");
- return new ExprReturn(out);
- }
-
- case OPCODE_fa: { // f[1]
- out.append(brackets(
- visitExprOrOpArgNode(n.getArgs()[0], d, NOBOOL), P_max,
- true));
- out.append("(");
- ExprOrOpArgNode dom = n.getArgs()[1];
- if (dom instanceof OpApplNode
- && ((OpApplNode) dom).getOperator().getName().toString()
- .equals("$Tuple")) {
- OpApplNode domOpAppl = (OpApplNode) dom;
- for (int i = 0; i < domOpAppl.getArgs().length; i++) {
- if (i != 0)
- out.append(", ");
- out.append(visitExprOrOpArgNode(domOpAppl.getArgs()[i], d,
- VALUE).out);
- }
- } else {
- out.append(visitExprOrOpArgNode(dom, d, VALUE).out);
- }
- out.append(")");
- if (expected == PREDICATE) {
- out.append(" = TRUE");
- return new ExprReturn(out, P_equals);
- }
- return new ExprReturn(out);
- }
-
- case OPCODE_domain:
- out.append("dom(");
- out.append(visitExprOrOpArgNode(n.getArgs()[0], d, NOBOOL).out);
- out.append(")");
- return new ExprReturn(out);
-
- case OPCODE_sof: // [ A -> B]
- {
- out.append(evalOpMoreArgs(n, " --> ", d, NOBOOL, P_total_f));
- return new ExprReturn(out, P_total_f);
- }
-
- /**********************************************************************
- * Except
- **********************************************************************/
- case OPCODE_exc: // Except
- {
- TLAType t = (TLAType) n.getToolObject(TYPE_ID);
- String oldRecOrFunc = visitExprOrOpArgNode(n.getArgs()[0], d,
- NOBOOL).out.toString();
-
- if (t.getKind() == IType.STRUCT) {
- StructType structType = (StructType) t;
-
- Hashtable<String, String> temp = new Hashtable<String, String>();
- 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];
- OpApplNode seq = (OpApplNode) first;
-
- String val = visitExprOrOpArgNode((ExprOrOpArgNode) second,
- d, VALUE).out.toString();
-
- LinkedList<ExprOrOpArgNode> list = new LinkedList<ExprOrOpArgNode>();
- for (int j = 0; j < seq.getArgs().length; j++) {
- list.add(seq.getArgs()[j]);
- }
-
- StringNode s = (StringNode) list.poll();
- String fieldName = s.getRep().toString();
-
- String res = evalExceptValue(list,
- structType.getType(fieldName), val, oldRecOrFunc
- + "'" + fieldName);
- temp.put(fieldName, res);
- }
-
- out.append("rec(");
- StructType st = (StructType) t;
- for (int i = 0; i < st.getFields().size(); i++) {
- String fieldName = st.getFields().get(i);
- out.append(fieldName);
- out.append(" : ");
- String value = temp.get(fieldName);
- if (value == null) {
- value = oldRecOrFunc + "'" + fieldName;
- }
- out.append(value);
-
- if (i < st.getFields().size() - 1) {
- out.append(", ");
- }
- }
- out.append(")");
- return new ExprReturn(out);
-
- } else {
- // function
- FunctionType func = (FunctionType) t;
-
- out.append(visitExprOrOpArgNode(n.getArgs()[0], d, NOBOOL).out);
- out.append(" <+ {");
- for (int i = 1; i < n.getArgs().length; i++) {
- OpApplNode pair = (OpApplNode) n.getArgs()[i];
- OpApplNode domSeq = (OpApplNode) pair.getArgs()[0];
- ExprOrOpArgNode domExpr = domSeq.getArgs()[0];
- StringBuilder dom = new StringBuilder();
- if (domExpr instanceof OpApplNode
- && ((OpApplNode) domExpr).getOperator().getName()
- .toString().equals("$Tuple")) {
- OpApplNode domOpAppl = (OpApplNode) domExpr;
- dom.append("(");
- for (int j = 0; j < domOpAppl.getArgs().length; j++) {
- if (j != 0) {
- dom.append(", ");
- }
- dom.append(visitExprOrOpArgNode(
- domOpAppl.getArgs()[j], d, VALUE).out);
- }
- dom.append(")");
- } else {
- dom.append(visitExprOrOpArgNode(pair.getArgs()[0], d,
- VALUE).out);
- }
- out.append(dom);
-
- out.append(" |-> ");
-
- ExprOrOpArgNode first = pair.getArgs()[0];
- ExprOrOpArgNode second = pair.getArgs()[1];
- OpApplNode seq = (OpApplNode) first;
-
-
- String val = brackets(visitExprOrOpArgNode((ExprOrOpArgNode) second,
- d, VALUE), P_maplet, false).toString();
- //String val = visitExprOrOpArgNode((ExprOrOpArgNode) second,
- // d, VALUE).out.toString();
-
- LinkedList<ExprOrOpArgNode> list = new LinkedList<ExprOrOpArgNode>();
- for (int j = 0; j < seq.getArgs().length; j++) {
- list.add(seq.getArgs()[j]);
- }
- list.poll();
- String res = evalExceptValue(list, func.getRange(), val,
- oldRecOrFunc + "(" + dom + ")");
- out.append(res);
- // out.append(brackets(
- // visitExprOrOpArgNode(pair.getArgs()[1], d, VALUE),
- // P_maplet, false));
- if (i < n.getArgs().length - 1) {
- out.append(", ");
- }
- }
- out.append("}");
- return new ExprReturn(out, P_rel_overriding);
-
- }
- }
-
- /***********************************************************************
- * Records
- ***********************************************************************/
- case OPCODE_sor: { // $SetOfRcds [L1 : e1, L2 : e2]
- SetType pow = (SetType) n.getToolObject(TYPE_ID);
- StructType struct = (StructType) pow.getSubType();
- Hashtable<String, StringBuilder> pairs = new Hashtable<String, StringBuilder>();
- ExprOrOpArgNode[] args = n.getArgs();
- for (int i = 0; i < args.length; i++) {
- OpApplNode pair = (OpApplNode) args[i];
- StringNode stringNode = (StringNode) pair.getArgs()[0];
- pairs.put(stringNode.getRep().toString(),
- visitExprOrOpArgNode(pair.getArgs()[1], d, VALUE).out);
- }
- out.append("struct(");
- for (int i = 0; i < struct.getFields().size(); i++) {
- String fieldName = struct.getFields().get(i);
- out.append(fieldName);
- out.append(" : ");
- if (pairs.containsKey(fieldName)) {
- out.append(pairs.get(fieldName));
- } else {
- out.append(struct.getType(fieldName));
- }
- if (i < struct.getFields().size() - 1)
- out.append(",");
- }
- out.append(")");
- return new ExprReturn(out, P_max);
- }
-
- case OPCODE_rc: { // [h_1 |-> 1, h_2 |-> 2]
- StructType struct = (StructType) n.getToolObject(TYPE_ID);
- Hashtable<String, StringBuilder> pairs = new Hashtable<String, StringBuilder>();
- ExprOrOpArgNode[] args = n.getArgs();
- for (int i = 0; i < args.length; i++) {
- OpApplNode pair = (OpApplNode) args[i];
- StringNode stringNode = (StringNode) pair.getArgs()[0];
- pairs.put(stringNode.getRep().toString(),
- visitExprOrOpArgNode(pair.getArgs()[1], d, VALUE).out);
- }
- out.append("rec(");
- for (int i = 0; i < struct.getFields().size(); i++) {
- String fieldName = struct.getFields().get(i);
- out.append(fieldName);
- out.append(" : ");
- if (pairs.containsKey(fieldName)) {
- out.append(pairs.get(fieldName));
- } else {
- out.append(getDummy(struct.getType(fieldName)));
- }
- if (i < struct.getFields().size() - 1)
- out.append(",");
- }
- out.append(")");
- return new ExprReturn(out, P_max);
- }
-
- case OPCODE_rs: { // $RcdSelect r.c
- out.append(visitExprOrOpArgNode(n.getArgs()[0], d, NOBOOL).out);
- out.append("'");
- StringNode stringNode = (StringNode) n.getArgs()[1];
- out.append(stringNode.getRep().toString());
- if (expected == PREDICATE) {
- out.append(" = TRUE");
- return new ExprReturn(out, P_equals);
- }
- return new ExprReturn(out, P_record_acc);
- }
-
- /***********************************************************************
- * miscellaneous constructs
- ***********************************************************************/
- case OPCODE_ite: // IF THEN ELSE
- {
- return evalIfThenElse(n, d, expected);
-
- }
-
- case OPCODE_case: { // CASE p1 -> e1 [] p2 -> e2
- out.append("(");
- StringBuilder all = new StringBuilder();
- for (int i = 0; i < n.getArgs().length; i++) {
- OpApplNode pair = (OpApplNode) n.getArgs()[i];
- out.append("%t_.(t_ = 0 & ");
- if (pair.getArgs()[0] == null) {
- out.append("not(" + all + ")");
- } else {
- ExprReturn p = visitExprOrOpArgNode(pair.getArgs()[0], d,
- PREDICATE);
- if (i != 0) {
- all.append(" or ");
- }
- all.append(brackets(p, P_or, i == 0));
- out.append(brackets(p, P_and, false));
- }
- out.append(" | ");
- out.append(visitExprOrOpArgNode(pair.getArgs()[1], d, VALUE).out);
- out.append(")");
- if (i < n.getArgs().length - 1) {
- out.append(" \\/ ");
- }
- }
- out.append(")(0)");
- return new ExprReturn(out);
- }
-
- case OPCODE_uc: { // CHOOSE x : P
- out.append("CHOOSE({");
- FormalParamNode x = n.getUnbdedQuantSymbols()[0];
- out.append(getPrintName(x));
- out.append("|");
- out.append(getPrintName(x));
- out.append(visitExprOrOpArgNode(n.getArgs()[0], d, PREDICATE).out);
- out.append("})");
- return new ExprReturn(out);
-
- }
-
- case OPCODE_bc: { // CHOOSE x \in S: P
- out.append("CHOOSE({");
- FormalParamNode x = n.getBdedQuantSymbolLists()[0][0];
- out.append(getPrintName(x));
- out.append("|");
- out.append(getPrintName(x));
- out.append(" : ");
- ExprNode in = n.getBdedQuantBounds()[0];
- out.append(visitExprNode(in, d, NOBOOL).out);
- out.append(" & ");
- out.append(visitExprOrOpArgNode(n.getArgs()[0], d, PREDICATE).out);
- out.append("})");
- return new ExprReturn(out);
-
- }
-
- /***********************************************************************
- * UNCHANGED
- ************************************************************************/
- case OPCODE_unchanged:
- Boolean b = (Boolean) n.getToolObject(USED);
- if (b != null) {
- return new ExprReturn("TRUE = TRUE", P_equals);
- }
- OpApplNode k = (OpApplNode) n.getArgs()[0];
- if (k.getOperator().getKind() == VariableDeclKind) {
- String name = k.getOperator().getName().toString();
- out.append(name + "_n = " + name);
- } else {
- // Tuple
- for (int i = 0; i < k.getArgs().length; i++) {
- String name = visitExprOrOpArgNode(k.getArgs()[i], d, VALUE).out
- .toString();
- out.append(name + "_n = " + name);
- if (i < k.getArgs().length - 1) {
- out.append(" & ");
- }
- }
- }
- return new ExprReturn(out);
-
- /***********************************************************************
- * Prime
- ***********************************************************************/
- case OPCODE_prime: // prime
- {
- out.append(visitExprOrOpArgNode(n.getArgs()[0], d, VALUE).out);
- out.append("_n");
- return new ExprReturn(out);
- }
-
- /***********************************************************************
- * Sany internal
- ***********************************************************************/
- case OPCODE_seq: // !
- {
- return visitExprOrOpArgNode(n.getArgs()[0], d, expected);
- }
-
- /***********************************************************************
- * no TLA+ Built-ins
- ***********************************************************************/
- case 0: {
- return evalBBuiltIns(n, d, expected);
- }
-
- case OPCODE_sa: // []_
- case OPCODE_box: // []
- case OPCODE_diamond: // <>
- case OPCODE_wf: // weak fairness
- {
- throw new RuntimeException("Not supported operator: "
- + n.toString(2));
- }
-
- }
- throw new RuntimeException(n.toString(2));
- }
-
- /**
- * @param list
- * @param type
- * @param string
- * @return
- */
- private String evalExceptValue(LinkedList<ExprOrOpArgNode> list,
- TLAType type, String val, String prefix) {
- StringBuilder sb = new StringBuilder();
- ExprOrOpArgNode head = list.poll();
- if (head == null) {
- return val;
- }
- if (type.getKind() == IType.STRUCT) {
- StructType structType = (StructType) type;
- String field = ((StringNode) head).getRep().toString();
-
- ArrayList<String> fields = structType.getFields();
- sb.append("rec(");
-
- for (int i = 0; i < fields.size(); i++) {
- String currentField = fields.get(i);
- sb.append(currentField);
- sb.append(" : ");
- if (currentField.equals(field)) {
- String value;
- if (list.size() > 0) {
- value = evalExceptValue(list,
- structType.getType(currentField), val, prefix
- + "'" + currentField);
- } else {
- value = val;
- }
-
- sb.append(value);
- } else {
- sb.append(prefix + "'" + currentField);
- }
- if (i < fields.size() - 1) {
- sb.append(", ");
- }
- }
- sb.append(")");
-
- } else {
- FunctionType func = (FunctionType) type;
- sb.append("(");
- sb.append(prefix);
- sb.append(" <+ {");
- String dom = visitExprOrOpArgNode(head, new DContext(), VALUE).out
- .toString();
- sb.append(dom);
- sb.append(" |-> ");
-
- if (list.size() > 0) {
- String res = evalExceptValue(list, func.getRange(), val, prefix
- + "(" + dom + ")");
- sb.append(res);
- } else {
- sb.append(val);
- }
- sb.append("}");
- sb.append(")");
- }
- return sb.toString();
- }
-
- /**
- * @param n
- * @return
- */
- protected ExprReturn evalIfThenElse(OpApplNode n, DContext d, int expected) {
- TLAType t = (TLAType) n.getToolObject(TYPE_ID);
-
- if (t.getKind() == IType.BOOL) {
- d.indent.append(" ");
- ExprReturn iif = visitExprOrOpArgNode(n.getArgs()[0], d, PREDICATE);
- ExprReturn then = visitExprOrOpArgNode(n.getArgs()[1], d, PREDICATE);
- ExprReturn eelse = visitExprOrOpArgNode(n.getArgs()[2], d,
- PREDICATE);
- String res = String.format(
- "(%s \n%s => %s) \n\t & (not(%s) \n%s => %s)",
- brackets(iif, P_implies, true), d.indent,
- brackets(then, P_implies, false), iif.out, d.indent,
- brackets(eelse, P_implies, false));
- return makeBoolValue(new StringBuilder(res), expected, P_and);
- } else {
- // ExprReturn iif = visitExprOrOpArgNode(n.getArgs()[0], d,
- // PREDICATE);
- // ExprReturn then = visitExprOrOpArgNode(n.getArgs()[1], d,
- // VALUE);
- // ExprReturn eelse = visitExprOrOpArgNode(n.getArgs()[2], d,
- // VALUE);
- // String res = String
- // .format("(%%t_.( t_ = 0 & %s | %s )\\/%%t_.( t_ = 0 & not(%s) | %s ))(0)",
- // iif.out, then.out, iif.out, eelse.out);
- // return new ExprReturn(res);
- ExprReturn iif = visitExprOrOpArgNode(n.getArgs()[0], d, VALUE);
- ExprReturn then = visitExprOrOpArgNode(n.getArgs()[1], d, VALUE);
- ExprReturn eelse = visitExprOrOpArgNode(n.getArgs()[2], d, VALUE);
- String res = String.format("IF_THEN_ELSE(%s, %s, %s)", iif.out,
- then.out, eelse.out);
- return new ExprReturn(res);
- }
- }
-
- private ExprReturn evalBoundedQuantor(OpApplNode n, DContext d,
- int expected, String symbol) {
- StringBuilder out = new StringBuilder();
- out.append(symbol);
- FormalParamNode[][] params = n.getBdedQuantSymbolLists();
- for (int i = 0; i < params.length; i++) {
- for (int j = 0; j < params[i].length; j++) {
- out.append(getPrintName(params[i][j]));
- if (j < params[i].length - 1) {
- out.append(",");
- }
- }
- if (i < params.length - 1) {
- out.append(",");
- }
- }
- out.append(".(");
- out.append(visitBounded(n, d));
- out.append(symbol.equals("#") ? " & " : " => ");
- out.append(brackets(visitExprOrOpArgNode(n.getArgs()[0], d, PREDICATE),
- symbol.equals("#") ? P_and : P_implies, false));
- out.append(")");
- return makeBoolValue(out, expected, P_max);
- }
-
- @SuppressWarnings("unused")
- private ExprReturn evalStructOrRec(String string, OpApplNode n, DContext d) {
- StringBuilder out = new StringBuilder();
- out.append(string);
- out.append("(");
- ExprOrOpArgNode[] args = n.getArgs();
- for (int i = 0; i < args.length; i++) {
- OpApplNode pair = (OpApplNode) args[i];
- StringNode stringNode = (StringNode) pair.getArgs()[0];
- out.append(stringNode.getRep().toString());
- out.append(" : ");
- out.append(visitExprOrOpArgNode(pair.getArgs()[1], d, VALUE).out);
- if (i != args.length - 1)
- out.append(", ");
- }
- out.append(")");
- return new ExprReturn(out, P_max);
- }
-
- protected ExprReturn evalBBuiltIns(OpApplNode n, DContext d, int expected) {
- StringBuilder out = new StringBuilder();
-
- switch (BBuiltInOPs.getOpcode(n.getOperator().getName())) {
-
- /**********************************************************************
- * Standard Module Naturals
- **********************************************************************/
- case B_OPCODE_nat: // Nat
- {
- out.append("NATURAL");
- return new ExprReturn(out);
- }
-
- case B_OPCODE_plus: // +
- out.append(evalOpMoreArgs(n, " + ", d, NOBOOL, P_plus));
- return new ExprReturn(out, P_plus);
-
- case B_OPCODE_minus: // -
- {
- out.append(evalOpMoreArgs(n, " - ", d, NOBOOL, P_minus));
- return new ExprReturn(out, P_minus);
- }
-
- case B_OPCODE_times: // *
- {
- out.append(evalOpMoreArgs(n, " * ", d, NOBOOL, P_times));
- return new ExprReturn(out, P_times);
- }
-
- case B_OPCODE_exp: // x^y
- {
- out.append(evalOpMoreArgs(n, " ** ", d, NOBOOL, P_exp));
- return new ExprReturn(out, P_exp);
- }
-
- case B_OPCODE_lt: // <
- {
- out.append(evalOpMoreArgs(n, " < ", d, NOBOOL, P_lt));
- return makeBoolValue(out, expected, P_lt);
- }
-
- case B_OPCODE_gt: // >
- {
- out.append(evalOpMoreArgs(n, " > ", d, NOBOOL, P_gt));
- return makeBoolValue(out, expected, P_gt);
- }
-
- case B_OPCODE_leq: // <=
- {
- out.append(evalOpMoreArgs(n, " <= ", d, NOBOOL, P_leq));
- return makeBoolValue(out, expected, P_leq);
- }
-
- case B_OPCODE_geq: // >=
- {
- out.append(evalOpMoreArgs(n, " >= ", d, NOBOOL, P_geq));
- return makeBoolValue(out, expected, P_geq);
- }
-
- case B_OPCODE_mod: // modulo
- {
- ExprReturn first = visitExprOrOpArgNode(n.getArgs()[0], d, VALUE);
- ExprReturn second = visitExprOrOpArgNode(n.getArgs()[1], d, VALUE);
- String res = String.format("(%s - %s * (%s / %s))",
- brackets(first, P_minus, true),
- brackets(second, P_times, true),
- brackets(first, P_div, true),
- brackets(second, P_div, false));
- return new ExprReturn(res);
- }
-
- case B_OPCODE_div: // /
- {
- out.append(evalOpMoreArgs(n, " / ", d, NOBOOL, P_div));
- return new ExprReturn(out, P_div);
- }
-
- case B_OPCODE_dotdot: // ..
- {
- out.append(evalOpMoreArgs(n, " .. ", d, NOBOOL, P_dotdot));
- return new ExprReturn(out, P_dotdot);
- }
-
- /**********************************************************************
- * Standard Module Integers
- **********************************************************************/
- case B_OPCODE_int: // Int
- {
- out.append("INTEGER");
- return new ExprReturn(out);
- }
-
- case B_OPCODE_uminus: // -x
- {
- out.append("-");
- out.append(visitExprOrOpArgNode(n.getArgs()[0], d, NOBOOL).out);
- return new ExprReturn(out, P_uminus);
- }
-
- /**********************************************************************
- * Standard Module FiniteSets
- **********************************************************************/
- case B_OPCODE_card: // Cardinality
- {
- out.append("card(");
- out.append(visitExprOrOpArgNode(n.getArgs()[0], d, NOBOOL).out);
- out.append(")");
- return new ExprReturn(out);
- }
-
- case B_OPCODE_finite: { // IsFiniteSet
- ExprReturn exprr = visitExprOrOpArgNode(n.getArgs()[0], d, NOBOOL);
- // String res = String
- // .format("#seq_.(seq_ : seq(%s) & !s.(s : %s => #n.(n : 1 .. size(seq_) & seq_(n) = s)))",
- // exprr.out, exprr.out);
- String res = String.format("%s : FIN(%s)", exprr.out, exprr.out);
- out.append(res);
- return makeBoolValue(out, expected, P_max);
- }
-
- /**********************************************************************
- * Standard Module Sequences
- **********************************************************************/
- case B_OPCODE_seq: { // Seq(S) - set of sequences
- out.append("seq(");
- out.append(visitExprOrOpArgNode(n.getArgs()[0], d, NOBOOL).out);
- out.append(")");
- return new ExprReturn(out);
- }
-
- case B_OPCODE_len: { // length of the sequence
- out.append("size(");
- out.append(visitExprOrOpArgNode(n.getArgs()[0], d, NOBOOL).out);
- out.append(")");
- return new ExprReturn(out);
- }
-
- case B_OPCODE_conc: { // s \o s2 - concatenation of s and s2
- out.append(evalOpMoreArgs(n, " ^ ", d, NOBOOL, P_conc));
- return new ExprReturn(out, P_conc);
- }
-
- case B_OPCODE_append: { // Append(s,x)
- out.append(evalOpMoreArgs(n, " <- ", d, NOBOOL, P_append));
- return new ExprReturn(out, P_append);
- }
-
- case B_OPCODE_head: { // Head(s)
- out.append("first(");
- out.append(visitExprOrOpArgNode(n.getArgs()[0], d, NOBOOL).out);
- out.append(")");
- return new ExprReturn(out);
- }
-
- case B_OPCODE_tail: { // Tail(s)
- out.append("tail(");
- out.append(visitExprOrOpArgNode(n.getArgs()[0], d, NOBOOL).out);
- out.append(")");
- return new ExprReturn(out);
- }
-
- case B_OPCODE_subseq: { // SubSeq(s,m,n)
- StringBuilder s = visitExprOrOpArgNode(n.getArgs()[0], d, NOBOOL).out;
- out.append("(");
- out.append(s);
- out.append("/|\\"); // taking first n elements
- out.append(visitExprOrOpArgNode(n.getArgs()[2], d, NOBOOL).out);
- out.append(")\\|/"); // dropping first m-1 elements
- out.append(visitExprOrOpArgNode(n.getArgs()[1], d, NOBOOL).out);
- out.append("-1");
- return new ExprReturn(out, P_drop_last);
- }
-
- /**********************************************************************
- * Standard Module TLA2B
- **********************************************************************/
- case B_OPCODE_min: { // MinOfSet(s)
- out.append("min(");
- out.append(visitExprOrOpArgNode(n.getArgs()[0], d, NOBOOL).out);
- out.append(")");
- return new ExprReturn(out);
- }
-
- case B_OPCODE_max: { // MaxOfSet(s)
- out.append("max(");
- out.append(visitExprOrOpArgNode(n.getArgs()[0], d, NOBOOL).out);
- out.append(")");
- return new ExprReturn(out);
- }
-
- case B_OPCODE_setprod: { // SetProduct(s)
- out.append("PI(z_).(z_:");
- out.append(visitExprOrOpArgNode(n.getArgs()[0], d, NOBOOL).out);
- out.append("|z_)");
- return new ExprReturn(out);
- }
-
- case B_OPCODE_setsum: { // SetSummation(s)
- out.append("SIGMA(z_).(z_:");
- out.append(visitExprOrOpArgNode(n.getArgs()[0], d, NOBOOL).out);
- out.append("|z_)");
- return new ExprReturn(out);
- }
-
- case B_OPCODE_permseq: { // PermutedSequences(s)
- out.append("perm(");
- out.append(visitExprOrOpArgNode(n.getArgs()[0], d, NOBOOL).out);
- out.append(")");
- return new ExprReturn(out);
- }
- /**********************************************************************
- * Standard Module TLA2B
- **********************************************************************/
- case B_OPCODE_pow1: { // POW1
- out.append("POW1(");
- out.append(visitExprOrOpArgNode(n.getArgs()[0], d, NOBOOL).out);
- out.append(")");
- return new ExprReturn(out);
- }
-
- /**********************************************************************
- * Standard Module Relations
- **********************************************************************/
-
- case B_OPCODE_rel_inverse: { // POW1
- out.append("(");
- out.append(visitExprOrOpArgNode(n.getArgs()[0], d, NOBOOL).out);
- out.append("~)");
- return new ExprReturn(out);
- }
-
- /***********************************************************************
- * TLA+ Built-Ins, but not in tlc.tool.BuiltInOPs
- ***********************************************************************/
- case B_OPCODE_bool: // BOOLEAN
- out.append("BOOL");
- return new ExprReturn(out);
-
- case B_OPCODE_true: // TRUE
- out.append("TRUE");
- if (expected == PREDICATE) {
- out.append(" = TRUE");
- return new ExprReturn(out, P_equals);
- }
- return new ExprReturn(out);
-
- case B_OPCODE_false: // FALSE
- out.append("FALSE");
- if (expected == PREDICATE) {
- out.append(" = TRUE");
- return new ExprReturn(out, P_equals);
- }
- return new ExprReturn(out);
-
- case B_OPCODE_string: // STRING
- out.append("STRING");
- return new ExprReturn(out);
-
- }
-
- throw new RuntimeException(n.toString(2));
- }
-
- protected StringBuilder visitBounded(OpApplNode n, DContext d) {
- StringBuilder out = new StringBuilder();
- FormalParamNode[][] params = n.getBdedQuantSymbolLists();
- ExprNode[] in = n.getBdedQuantBounds();
- boolean[] isTuple = n.isBdedQuantATuple();
- for (int i = 0; i < params.length; i++) {
- if (isTuple[i]) {
- out.append("(");
- for (int j = 0; j < params[i].length; j++) {
- out.append(getPrintName(params[i][j]));
- if (j == 0)
- out.append(", ");
- }
- out.append(")");
- out.append(" : ");
- out.append(visitExprNode(in[i], d, NOBOOL).out);
- if (i < params.length - 1) {
- out.append(" & ");
- }
- } else {
- for (int j = 0; j < params[i].length; j++) {
- out.append(getPrintName(params[i][j]));
- out.append(" : ");
- out.append(visitExprNode(in[i], d, NOBOOL).out);
- if (j < params[i].length - 1 || i < params.length - 1) {
- out.append(" & ");
- }
- }
- }
- }
- return out;
- }
-
- protected StringBuilder evalOpMoreArgs(OpApplNode n, String operator,
- DContext d, int expected, int priority) {
- StringBuilder out = new StringBuilder();
- ExprOrOpArgNode[] args = n.getArgs();
- for (int i = 0; i < args.length; i++) {
- ExprReturn r = visitExprOrOpArgNode(args[i], d, expected);
- if (i == 0) {
- out.append(brackets(r, priority, true));
- } else {
- out.append(operator);
- out.append(brackets(r, priority, false));
- }
-
- }
- return out;
- }
-
- protected ExprReturn makeBoolValue(StringBuilder out, int expected,
- int priority) {
- StringBuilder res = new StringBuilder();
- if (expected == VALUE) {
- res.append("bool(" + out + ")");
- return new ExprReturn(res);
- } else {
- return new ExprReturn(out, priority);
- }
- }
-
- protected StringBuilder brackets(ExprReturn r, int p, boolean left) {
- StringBuilder res = new StringBuilder();
- if ((left && r.getPriority() < p) || (!left && r.getPriority() <= p)) {
- res.append("(");
- res.append(r.getOut());
- res.append(")");
- } else
- res.append(r.getOut());
- return res;
- }
-
- protected String getPrintName(SymbolNode node) {
- if (node.getToolObject(NEW_NAME) != null) {
- return (String) node.getToolObject(NEW_NAME);
- } else {
- return node.getName().toString();
- }
- }
-
- private String getDummy(TLAType type) {
- switch (type.getKind()) {
- case IType.INTEGER:
- return "0";
-
- case IType.STRING:
- return "\"\"";
-
- case IType.POW:
- return "{}";
-
- case IType.BOOL:
- return "FALSE";
- case IType.MODELVALUE:
- EnumType e = (EnumType) type;
- return "noVal" + e.id;
- default:
- break;
- }
- return null;
-
- }
-}
diff --git a/src/main/java/de/tla2b/old/BMachinePrinter.java b/src/main/java/de/tla2b/old/BMachinePrinter.java
deleted file mode 100644
index 7fa44733374a680449b1aad8ff7f45fc85cae3af..0000000000000000000000000000000000000000
--- a/src/main/java/de/tla2b/old/BMachinePrinter.java
+++ /dev/null
@@ -1,697 +0,0 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
-package de.tla2b.old;
-
-import java.util.ArrayList;
-import java.util.Hashtable;
-import java.util.Iterator;
-import java.util.Set;
-
-import de.tla2b.analysis.BOperation;
-import de.tla2b.analysis.RecursiveFunktion;
-import de.tla2b.analysis.SpecAnalyser;
-import de.tla2b.config.ConfigfileEvaluator;
-import de.tla2b.config.ValueObj;
-import de.tla2b.global.BBuiltInOPs;
-import de.tla2b.global.TranslationGlobals;
-import de.tla2b.types.EnumType;
-import de.tla2b.types.IType;
-import de.tla2b.types.SetType;
-import de.tla2b.types.TLAType;
-import tla2sany.semantic.AssumeNode;
-import tla2sany.semantic.ExprNode;
-import tla2sany.semantic.FormalParamNode;
-import tla2sany.semantic.LetInNode;
-import tla2sany.semantic.ModuleNode;
-import tla2sany.semantic.OpApplNode;
-import tla2sany.semantic.OpDeclNode;
-import tla2sany.semantic.OpDefNode;
-import tlc2.value.SetEnumValue;
-
-public class BMachinePrinter extends AbstractExpressionPrinter implements
- TranslationGlobals {
- private ModuleNode module;
- private ArrayList<OpDeclNode> bConstants;
- private ArrayList<ExprNode> inits;
- private ArrayList<BOperation> bOperations;
- private ArrayList<OpDefNode> invariants;
- private ArrayList<LetInNode> globalLets;
- private ArrayList<String> setEnumeration;
- private ArrayList<String> definitionMacro;
- private Hashtable<OpDeclNode, ValueObj> constantAssignments;
- private ArrayList<OpDefNode> operatorModelvalues;
- private Set<OpDefNode> bDefinitions;
- // set of OpDefNodes which are called in the specification
- private Hashtable<OpDefNode, FormalParamNode[]> letParams;
-
- private ArrayList<RecursiveFunktion> recursiveFunktions;
- private ArrayList<LetInNode> tempLetInNodes = new ArrayList<LetInNode>();
-
- /**
- * @param moduleNode
- * @param conEval
- * @param specAnalyser
- */
- public BMachinePrinter(ModuleNode moduleNode, ConfigfileEvaluator conEval,
- SpecAnalyser specAnalyser) {
- this.module = moduleNode;
-
- if (conEval == null) {
- bConstants = new ArrayList<OpDeclNode>();
- for (int i = 0; i < moduleNode.getConstantDecls().length; i++) {
- bConstants.add(moduleNode.getConstantDecls()[i]);
- }
- } else {
- this.bConstants = conEval.getbConstantList();
- this.invariants = conEval.getInvariants();
- this.setEnumeration = conEval.getEnumerationSet();
- this.constantAssignments = conEval.getConstantAssignments();
- this.operatorModelvalues = conEval.getOperatorModelvalues();
- }
-
- this.inits = specAnalyser.getInits();
- this.bOperations = specAnalyser.getBOperations();
- this.definitionMacro = specAnalyser.getDefinitionMacros();
- this.bDefinitions = specAnalyser.getBDefinitions();
- this.letParams = specAnalyser.getLetParams();
- //this.recursiveFunktions = specAnalyser.getRecursiveFunctions();
- }
-
- public StringBuilder start() {
- StringBuilder out = new StringBuilder();
- out.append("MACHINE " + module.getName().toString() + "\n");
-
- out.append(evalEnumeratedSets());
- out.append(evalDefinitions());
-
- // Constants and Properties
- out.append(evalConsDecl());
- out.append(evalPropertyStatements());
- tempLetInNodes.clear();
- StringBuilder operations = evalOperations();
- globalLets.addAll(tempLetInNodes);
- tempLetInNodes.clear();
-
-
-
- out.append(evalVariables());
-
- out.append(evalInvariants());
-
- out.append(evalInit());
-
- out.append(operations);
- out.append("END");
- return out;
- }
-
- /**
- * @return
- */
- private StringBuilder evalEnumeratedSets() {
- StringBuilder out = new StringBuilder();
-
- if (setEnumeration == null || setEnumeration.size() == 0)
- return out;
-
- out.append("SETS\n ");
-
- ArrayList<EnumType> printed = new ArrayList<EnumType>();
- int counter = 1;
-
- OpDeclNode[] cons = module.getConstantDecls();
- boolean first = true;
- for (int i = 0; i < cons.length; i++) {
- TLAType type = (TLAType) cons[i].getToolObject(TYPE_ID);
- EnumType e = null;
- if (type instanceof SetType) {
- if (((SetType) type).getSubType() instanceof EnumType) {
- e = (EnumType) ((SetType) type).getSubType();
- } else
- continue;
-
- } else if ((type instanceof EnumType)) {
- e = (EnumType) type;
- } else
- continue;
-
- if (!printed.contains(e)) {
- //e.id = counter;
-// if (!first) {
-// out.append("; ");
-// }
-// out.append("ENUM" + counter + " = {");
-// Iterator<String> it2 = e.modelvalues.iterator();
-// while (it2.hasNext()) {
-// out.append(it2.next());
-// if (it2.hasNext()) {
-// out.append(", ");
-// }
-// }
-// if (e.hasNoVal()) {
-// out.append(", noVal" + counter);
-// }
-// out.append("}");
-// printed.add(e);
-// counter++;
-// first = false;
- }
- }
-
-// if (operatorModelvalues != null && operatorModelvalues.size() > 0) {
-// for (int i = 0; i < operatorModelvalues.size(); i++) {
-// OpDefNode def = operatorModelvalues.get(i);
-// TLAType type = (TLAType) def.getToolObject(TYPE_ID);
-// EnumType e = null;
-// if (type instanceof SetType) {
-// if (((SetType) type).getSubType() instanceof EnumType) {
-// e = (EnumType) ((SetType) type).getSubType();
-// } else
-// continue;
-//
-// } else if ((type instanceof EnumType)) {
-// e = (EnumType) type;
-// } else
-// continue;
-//
-// if (!printed.contains(e)) {
-// e.id = counter;
-// if (!first) {
-// out.append("; ");
-// }
-// out.append("ENUM" + counter + " = {");
-// Iterator<String> it2 = e.modelvalues.iterator();
-// while (it2.hasNext()) {
-// out.append(it2.next());
-// if (it2.hasNext()) {
-// out.append(", ");
-// }
-// }
-// if (e.hasNoVal()) {
-// out.append(", noVal" + counter);
-// }
-// out.append("}");
-// printed.add(e);
-// counter++;
-// first = false;
-// }
-//
-// }
-//
-// }
-
- out.append("\n");
- return out;
- }
-
- private StringBuilder evalInvariants() {
- StringBuilder out = new StringBuilder();
- OpDeclNode[] vars = module.getVariableDecls();
- if (vars.length > 0) {
- out.append("INVARIANT\n ");
- for (int i = 0; i < vars.length; i++) {
- TLAType varType = (TLAType) vars[i].getToolObject(TYPE_ID);
- out.append(getPrintName(vars[i]) + " : " + varType + "\n");
- if (i != vars.length - 1)
- out.append(" & ");
- }
- if (invariants != null) {
- for (int i = 0; i < invariants.size(); i++) {
- out.append(" & " + invariants.get(i).getName().toString()
- + "\n");
- }
- }
- }
- return out;
- }
-
- private StringBuilder evalInit() {
- StringBuilder out = new StringBuilder();
- OpDeclNode[] vars = module.getVariableDecls();
- if (vars.length == 0)
- return out;
- out.append("INITIALISATION\n ");
- for (int i = 0; i < vars.length; i++) {
- out.append(getPrintName(vars[i]));
- if (i < vars.length - 1)
- out.append(", ");
- }
- out.append(":(");
- for (int i = 0; i < inits.size(); i++) {
- if (i != 0) {
- out.append(" & ");
- }
- out.append(visitExprNode(inits.get(i), new DContext(), PREDICATE).out);
- }
- out.append(")\n");
- return out;
- }
-
- private StringBuilder evalOperations() {
- StringBuilder out = new StringBuilder();
- if (bOperations == null)
- return out;
-
- out.append("OPERATIONS\n");
- for (int i = 0; i < bOperations.size(); i++) {
- BOperation op = bOperations.get(i);
- String defName = op.getName();
-
- DContext d = new DContext("\t");
- out.append(" " + defName.replace('!', '_') + "_Op");
- if (op.getOpParams().size() > 0) {
- out.append("(");
- for (int j = 0; j < op.getOpParams().size(); j++) {
- if (j != 0)
- out.append(", ");
- out.append(op.getOpParams().get(j));
- }
- out.append(")");
- }
- out.append(" = ");
- out.append("ANY ");
- OpDeclNode[] vars = module.getVariableDecls();
- boolean first = true;
- for (int j = 0; j < vars.length; j++) {
- String varName = vars[j].getName().toString();
- if (op.getUnchangedVariables().contains(varName))
- continue;
- if (!first) {
- out.append(", ");
- }
- out.append(varName + "_n");
- first = false;
- }
- out.append("\n\tWHERE ");
- if (op.getOpParams().size() > 0) {
- for (int j = 0; j < op.getExistQuans().size(); j++) {
- OpApplNode o = op.getExistQuans().get(j);
- out.append(visitBounded(o, d));
- out.append(" & ");
- }
- out.append("\n\t ");
- }
- for (int j = 0; j < vars.length; j++) {
- String varName = vars[j].getName().toString();
- if (op.getUnchangedVariables().contains(varName))
- continue;
- out.append(varName + "_n : " + vars[j].getToolObject(TYPE_ID));
- out.append(" & ");
- }
- out.append(visitExprOrOpArgNode(op.getNode(), d, PREDICATE).out);
-
- out.append("\n\tTHEN ");
-
- boolean first2 = true;
- for (int j = 0; j < vars.length; j++) {
- String varName = vars[j].getName().toString();
- if (op.getUnchangedVariables().contains(varName))
- continue;
- if (!first2) {
- out.append(", ");
- }
- out.append(varName);
- first2 = false;
- }
-
- out.append(" := ");
-
- boolean first3 = true;
- for (int j = 0; j < vars.length; j++) {
- String varName = vars[j].getName().toString();
- if (op.getUnchangedVariables().contains(varName))
- continue;
- if (!first3) {
- out.append(", ");
- }
- out.append(varName + "_n");
- first3 = false;
- }
- out.append(" END");
- if (i != bOperations.size() - 1) {
- out.append(";\n\n");
- }
- }
- out.append("\n");
- return out;
- }
-
- private StringBuilder evalVariables() {
- StringBuilder out = new StringBuilder();
- OpDeclNode[] vars = module.getVariableDecls();
- if (vars.length > 0) {
- out.append("VARIABLES\n ");
- for (int i = 0; i < vars.length; i++) {
- String[] comments = vars[i].getPreComments();
- if (comments.length > 0) {
- String pragma = comments[comments.length - 1];
- if (pragma.startsWith("(*@")) {
- pragma = pragma.replace('(', '/').replace(')', '/');
- out.append(pragma).append(" ");
- }
-
- }
- out.append(getPrintName(vars[i]));
- if (i != vars.length - 1)
- out.append(",\n ");
- }
- out.append("\n");
- }
- return out;
- }
-
- private StringBuilder evalDefinitions() {
- StringBuilder out = new StringBuilder();
- ArrayList<OpDefNode> bDefs = new ArrayList<OpDefNode>();
- for (int i = 0; i < module.getOpDefs().length; i++) {
- OpDefNode def = module.getOpDefs()[i];
- if (bDefinitions.contains(def))
- bDefs.add(def);
- }
-
- if (bDefs.size() + globalLets.size() + definitionMacro.size() == 0)
- return out;
- out.append("DEFINITIONS\n");
- for (int i = 0; i < definitionMacro.size(); i++) {
- out.append(definitionMacro.get(i));
- if (i != definitionMacro.size() - 1
- || bDefs.size() + globalLets.size() > 0) {
- out.append(";\n");
- }
- }
-
- for (int i = 0; i < bDefs.size(); i++) {
- out.append(visitOpDefNode(bDefs.get(i)));
- if (!(i == bDefs.size() - 1 && globalLets.size() == 0))
- out.append(";\n\n");
- }
-
- for (int i = 0; i < globalLets.size(); i++) {
- LetInNode letInNode = globalLets.get(i);
- for (int j = 0; j < letInNode.getLets().length; j++) {
- out.append(evalLet(letInNode.getLets()[j]));
- if (i != letInNode.getLets().length - 1)
- out.append(";\n");
- }
- if (i != globalLets.size() - 1)
- out.append(";\n");
- }
- out.append("\n");
- return out;
- }
-
- /**
- * @param letDef
- * @return
- */
- private StringBuilder evalLet(OpDefNode letDef) {
- StringBuilder out = new StringBuilder();
- String defName = getPrintName(letDef);
- out.append(" " + defName);
- FormalParamNode[] shiftParams = letParams.get(letDef);
- if (shiftParams == null)
- shiftParams = new FormalParamNode[0];
- if (letDef.getParams().length + shiftParams.length > 0) {
- out.append("(");
- for (int i = 0; i < letDef.getParams().length; i++) {
- if (i != 0)
- out.append(",");
- out.append(letDef.getParams()[i].getName().toString());
- }
- for (int i = 0; i < shiftParams.length; i++) {
- if (letDef.getParams().length > 0 || i != 0)
- out.append(", ");
- out.append(shiftParams[i].getName().toString());
-
- }
- out.append(")");
- }
- out.append(" == ");
- DContext d = new DContext("\t");
- out.append(visitExprNode(letDef.getBody(), d, VALUEORPREDICATE).out);
- return out;
-
- }
-
- /**
- * @param def
- */
- private StringBuilder visitOpDefNode(OpDefNode def) {
- StringBuilder out = new StringBuilder();
- // ConstantObj conObj = (ConstantObj) def.getSource().getToolObject(
- // CONSTANT_OBJECT);
- // if (conObj != null) {
- // System.out.println("hier");
- // // config substitution
- // // out.append(" " + defName.replace('!', '_'));
- // String defName = getPrintName(def);
- // String defValue = conObj.getValue().toString();
- // if(defName.equals(defName.equals(defValue)))
- // return out;
- // out.append(" " + defName);
- // out.append(" == " + defValue);
- // return out;
- // }
-
- DContext d = new DContext("\t");
- tempLetInNodes.clear();
- StringBuilder body = visitExprNode(def.getBody(), d, VALUEORPREDICATE).out;
-
- for (int i = 0; i < tempLetInNodes.size(); i++) {
- LetInNode letInNode = tempLetInNodes.get(i);
- for (int j = 0; j < letInNode.getLets().length; j++) {
- out.append(evalLet(letInNode.getLets()[j]));
- out.append(";\n");
- }
-
- }
- tempLetInNodes.clear();
-
- out.append(" " + getPrintName(def));
- FormalParamNode[] params = def.getParams();
- if (params.length > 0) {
- out.append("(");
- for (int i = 0; i < params.length; i++) {
- if (i != 0)
- out.append(", ");
- out.append(getPrintName(params[i]));
- }
- out.append(")");
- }
- out.append(" == ");
- out.append(body);
- return out;
- }
-
- private StringBuilder evalConsDecl() {
- StringBuilder out = new StringBuilder();
- if (bConstants.size() + recursiveFunktions.size() == 0)
- return out;
- out.append("ABSTRACT_CONSTANTS\n");
- // out.append("CONSTANTS ");
- for (int i = 0; i < bConstants.size(); i++) {
- String[] comments = bConstants.get(i).getPreComments();
- if (comments.length > 0) {
- String pragma = comments[comments.length - 1];
- if (pragma.startsWith("(*@")) {
- pragma = pragma.replace('(', '/').replace(')', '/');
- out.append(pragma).append(" ");
- }
-
- }
- out.append(getPrintName(bConstants.get(i)));
- if (i < bConstants.size() - 1 || recursiveFunktions.size() > 0)
- out.append(",\n ");
- }
- for (int i = 0; i < recursiveFunktions.size(); i++) {
- out.append(getPrintName(recursiveFunktions.get(i).getOpDefNode()));
- if (i < recursiveFunktions.size() - 1)
- out.append(", ");
- }
- out.append("\n");
- return out;
- }
-
- private StringBuilder evalPropertyStatements() {
- StringBuilder out = new StringBuilder();
- if (bConstants.size() == 0 && module.getAssumptions().length == 0) {
- return out;
- }
- out.append("PROPERTIES\n ");
- boolean notFirst = false;
- for (int i = 0; i < bConstants.size(); i++) {
- OpDeclNode con = bConstants.get(i);
- if (notFirst) {
- out.append(" & ");
- }
- if (constantAssignments != null
- && constantAssignments.containsKey(con)) {
- ValueObj v = constantAssignments.get(con);
- TLAType t = v.getType();
- boolean isEnum = false;
- if (t instanceof SetType) {
- TLAType sub = ((SetType) t).getSubType();
- if (sub instanceof EnumType) {
- EnumType en = (EnumType) sub;
- SetEnumValue set = (SetEnumValue) v.getValue();
- if (set.elems.size() == en.modelvalues.size()) {
- isEnum = true;
- }
- }
- }
- if (isEnum) {
- out.append(String.format("%s = %s\n", getPrintName(con),
- ((SetType) t).getSubType()));
- } else {
- out.append(String.format("%s = %s\n", getPrintName(con), v
- .getValue().toString()));
- }
-
- } else {
- out.append(String.format("%s : %s\n", getPrintName(con),
- con.getToolObject(TYPE_ID)));
- }
-
- notFirst = true;
- }
- out.append(evalAssumptions());
- return out;
- }
-
- private StringBuilder evalAssumptions() {
- AssumeNode[] assumes = module.getAssumptions();
- StringBuilder out = new StringBuilder();
- if (assumes.length == 0)
- return out;
- if (bConstants.size() > 0) {
- out.append(" & ");
- }
- tempLetInNodes.clear();
- for (int i = 0; i < assumes.length; i++) {
- if (i != 0) {
- out.append(" & ");
- }
- out.append(visitAssumeNode(assumes[i]));
- out.append("\n");
- }
- globalLets.addAll(tempLetInNodes);
- tempLetInNodes.clear();
-
- if (recursiveFunktions.size() == 0)
- return out;
- if (bConstants.size() + assumes.length > 0) {
- out.append(" & ");
- }
- for (int i = 0; i < recursiveFunktions.size(); i++) {
- if (i != 0) {
- out.append(" & ");
- }
- out.append(visitRecursiveFunction(recursiveFunktions.get(i)));
- out.append("\n");
- }
-
- return out;
- }
-
- /**
- * @param recursiveFunktion
- * @return
- */
- private StringBuilder visitRecursiveFunction(RecursiveFunktion rf) {
- StringBuilder out = new StringBuilder();
- OpApplNode o = rf.getRF();
- OpApplNode ifThenElse = rf.getIfThenElse();
- out.append(getPrintName(rf.getOpDefNode()));
- out.append(" = ");
-
- DContext d = new DContext();
-
- FormalParamNode[][] vars = o.getBdedQuantSymbolLists();
- StringBuilder pre = new StringBuilder();
- for (int i = 0; i < vars.length; i++) {
- for (int j = 0; j < vars[i].length; j++) {
- pre.append(vars[i][j].getName());
- if (j < vars[i].length - 1) {
- pre.append(",");
- }
- }
- if (i < vars.length - 1) {
- pre.append(",");
- }
- }
- StringBuilder bound = visitBounded(o, d);
-
- ExprReturn iif = visitExprOrOpArgNode(ifThenElse.getArgs()[0], d,
- PREDICATE);
- ExprReturn then = visitExprOrOpArgNode(ifThenElse.getArgs()[1], d,
- VALUE);
- ExprReturn eelse = visitExprOrOpArgNode(ifThenElse.getArgs()[2], d,
- VALUE);
- String res = String.format(
- "%%%s.(%s & %s | %s) \\/ %%%s.(%s & not(%s) | %s)", pre, bound,
- iif.out, then.out, pre, bound, iif.out, eelse.out);
- out.append(res);
- return out;
- }
-
- private StringBuilder visitAssumeNode(AssumeNode n) {
- // there are named or unnamend assumptions
- StringBuilder out = new StringBuilder();
- DContext d = new DContext();
- out.append(visitExprNode(n.getAssume(), d, PREDICATE).out);
-
- return out;
- }
-
- @Override
- protected ExprReturn visitLetInNode(LetInNode l, DContext d, int expected) {
- tempLetInNodes.add(l);
- return visitExprNode(l.getBody(), d, VALUEORPREDICATE);
- }
-
- @Override
- protected ExprReturn visitUserdefinedOp(OpApplNode n, DContext d,
- int expected) {
- StringBuilder out = new StringBuilder();
- OpDefNode def = (OpDefNode) n.getOperator();
- // Operator is a B built-in operator
- if (BBuiltInOPs.contains(def.getName())
- && STANDARD_MODULES.contains(def.getSource()
- .getOriginallyDefinedInModuleNode().getName()
- .toString())) {
- return evalBBuiltIns(n, d, expected);
- }
-
- out.append(getPrintName(def));
-
- FormalParamNode[] shiftedParams = letParams.get(def);
- if (n.getArgs().length > 0
- || (shiftedParams != null && shiftedParams.length > 0)) {
- out.append("(");
- for (int i = 0; i < n.getArgs().length; i++) {
- out.append(visitExprOrOpArgNode(n.getArgs()[i], d, VALUE).out);
- if (i < n.getArgs().length - 1) {
- out.append(", ");
- }
- }
- if (shiftedParams != null) {
- for (int i = 0; i < shiftedParams.length; i++) {
- if (n.getArgs().length > 0 || i != 0)
- out.append(", ");
- out.append(shiftedParams[i].getName().toString());
-
- }
- }
- out.append(")");
-
- }
- TLAType defType = (TLAType) n.getToolObject(TYPE_ID);
- if (defType != null && defType.getKind() == IType.BOOL) {
- return makeBoolValue(out, expected, P_max);
- }
- return new ExprReturn(out);
- }
-
-}
diff --git a/src/main/java/de/tla2b/old/DContext.java b/src/main/java/de/tla2b/old/DContext.java
deleted file mode 100644
index 3f2b8b3d268313ccef63e78a0383b18a76b6804c..0000000000000000000000000000000000000000
--- a/src/main/java/de/tla2b/old/DContext.java
+++ /dev/null
@@ -1,18 +0,0 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
-package de.tla2b.old;
-
-public class DContext {
- public StringBuilder indent;
-
-
- public DContext(){
- indent = new StringBuilder();
- }
-
- public DContext(String indent){
- this.indent = new StringBuilder(indent);
- }
-}
diff --git a/src/main/java/de/tla2b/old/ExprReturn.java b/src/main/java/de/tla2b/old/ExprReturn.java
deleted file mode 100644
index e54d6d3e5395adb18df9a7c1fcab8d6fc2ed870c..0000000000000000000000000000000000000000
--- a/src/main/java/de/tla2b/old/ExprReturn.java
+++ /dev/null
@@ -1,53 +0,0 @@
-package de.tla2b.old;
-
-public class ExprReturn {
- public StringBuilder out= new StringBuilder();
- private int priority;
-
-
- public ExprReturn(){
- priority = 300;
- }
-
- public ExprReturn(String s){
- out.append(s);
- priority = 300;
- }
-
- public ExprReturn(StringBuilder out2) {
- out.append(out2);
- priority = 300;
- }
-
- public ExprReturn(StringBuilder out2, int priority2) {
- out.append(out2);
- priority = priority2;
- }
-
- public ExprReturn(String out2, int priority2) {
- out.append(out2);
- priority = priority2;
- }
-
-
-
- public StringBuilder getOut() {
- return out;
- }
- public void setOut(StringBuilder out) {
- this.out = out;
- }
- public int getPriority() {
- return priority;
- }
- public void setPriority(int priority) {
- this.priority = priority;
- }
-
- @Override
- public String toString(){
- String s = "P: "+ priority + " Out: " +out.toString();
- return s;
- }
-
-}
diff --git a/src/main/java/de/tla2b/old/ExpressionPrinter.java b/src/main/java/de/tla2b/old/ExpressionPrinter.java
deleted file mode 100644
index d388259602bbeb3687032a846f8550e590925acf..0000000000000000000000000000000000000000
--- a/src/main/java/de/tla2b/old/ExpressionPrinter.java
+++ /dev/null
@@ -1,103 +0,0 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
-package de.tla2b.old;
-
-
-import java.util.Hashtable;
-
-import de.tla2b.global.BBuiltInOPs;
-import de.tla2b.types.IType;
-import de.tla2b.types.TLAType;
-import tla2sany.semantic.ExprOrOpArgNode;
-import tla2sany.semantic.FormalParamNode;
-import tla2sany.semantic.ModuleNode;
-import tla2sany.semantic.OpApplNode;
-import tla2sany.semantic.OpDefNode;
-
-public class ExpressionPrinter extends AbstractExpressionPrinter {
-
- private Hashtable<FormalParamNode, ExprOrOpArgNode> paramterSubstitution;
- private ModuleNode moduleNode;
- private StringBuilder BExpression;
-
- public ExpressionPrinter(ModuleNode n) {
- this.moduleNode = n;
- paramterSubstitution = new Hashtable<FormalParamNode, ExprOrOpArgNode>();
- }
-
- public void start() {
- OpDefNode[] defs = moduleNode.getOpDefs();
- ExprReturn e = visitExprNode(defs[defs.length - 1].getBody(),
- new DContext(), VALUEORPREDICATE);
- BExpression = e.out;
- }
-
- public StringBuilder getBExpression() {
- return BExpression;
- }
-
- @Override
- protected ExprReturn visitUserdefinedOp(OpApplNode n, DContext d,
- int expected) {
- OpDefNode def = (OpDefNode) n.getOperator();
- if (BBuiltInOPs.contains(def.getName())) {
- return evalBBuiltIns(n, d, expected);
- }
-
- // substitute the parameters and inline the boby of the operator
- FormalParamNode[] params = def.getParams();
- if (params.length > 0) {
- for (int i = 0; i < n.getArgs().length; i++) {
- this.paramterSubstitution.put(params[i], n.getArgs()[i]);
- }
- }
- return visitExprNode(def.getBody(), new DContext(), expected);
- }
-
- @Override
- protected ExprReturn evalIfThenElse(OpApplNode n, DContext d, int expected) {
- TLAType t = (TLAType) n.getToolObject(TYPE_ID);
-
- if (t.getKind() == IType.BOOL) {
- d.indent.append(" ");
- ExprReturn iif = visitExprOrOpArgNode(n.getArgs()[0], d, PREDICATE);
- ExprReturn then = visitExprOrOpArgNode(n.getArgs()[1], d, PREDICATE);
- ExprReturn eelse = visitExprOrOpArgNode(n.getArgs()[2], d,
- PREDICATE);
- String res = String.format(
- "(%s \n%s => %s) \n\t & (not(%s) \n%s => %s)",
- brackets(iif, P_implies, true), d.indent,
- brackets(then, P_implies, false), iif.out, d.indent,
- brackets(eelse, P_implies, false));
- return makeBoolValue(new StringBuilder(res), expected, P_and);
- } else {
- ExprReturn iif = visitExprOrOpArgNode(n.getArgs()[0], d, PREDICATE);
- ExprReturn then = visitExprOrOpArgNode(n.getArgs()[1], d, VALUE);
- ExprReturn eelse = visitExprOrOpArgNode(n.getArgs()[2], d, VALUE);
- String res = String
- .format("(%%t_.( t_ = 0 & %s | %s )\\/%%t_.( t_ = 0 & not(%s) | %s ))(0)",
- iif.out, then.out, iif.out, eelse.out);
- return new ExprReturn(res);
- }
- }
-
- @Override
- protected ExprReturn visitFormalParamNode(OpApplNode n, DContext d,
- int expected) {
- StringBuilder out = new StringBuilder();
- ExprOrOpArgNode e = paramterSubstitution.get((FormalParamNode) n
- .getOperator());
- if (e != null) {
- return visitExprOrOpArgNode(e, d, expected);
- }
- out.append(getPrintName(n.getOperator()));
- if (expected == PREDICATE) {
- out.append(" = TRUE");
- return new ExprReturn(out, P_equals);
- }
- return new ExprReturn(out);
- }
-
-}
diff --git a/src/main/java/de/tla2b/old/ExpressionTranslatorOld.java b/src/main/java/de/tla2b/old/ExpressionTranslatorOld.java
deleted file mode 100644
index 1799d45af3a59e967e435d975e195db2b4199cfb..0000000000000000000000000000000000000000
--- a/src/main/java/de/tla2b/old/ExpressionTranslatorOld.java
+++ /dev/null
@@ -1,349 +0,0 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
-package de.tla2b.old;
-
-import java.io.File;
-import java.io.FileWriter;
-import java.io.IOException;
-import java.util.ArrayList;
-import java.util.HashSet;
-import java.util.Set;
-
-import de.tla2b.analysis.SymbolRenamer;
-import de.tla2b.analysis.TypeChecker;
-import de.tla2b.exceptions.TLA2BException;
-import de.tla2b.exceptions.TLA2BIOException;
-import de.tla2b.exceptions.TypeErrorException;
-import tla2sany.drivers.FrontEndException;
-import tla2sany.drivers.InitException;
-import tla2sany.drivers.SANY;
-import tla2sany.modanalyzer.ParseUnit;
-import tla2sany.modanalyzer.SpecObj;
-import tla2sany.parser.ParseException;
-import tla2sany.semantic.ModuleNode;
-import tla2sany.st.SyntaxTreeConstants;
-import tla2sany.st.TreeNode;
-import util.ToolIO;
-
-public class ExpressionTranslatorOld implements SyntaxTreeConstants {
- private String TLAExpression;
- private ArrayList<String> variables;
- private ArrayList<String> noVariables;
- private StringBuilder BExpression;
-
- public static String translateExpression(String tlaExpression)
- throws TLA2BException {
- ToolIO.reset();
- ToolIO.setMode(ToolIO.TOOL);
- ExpressionTranslatorOld et = new ExpressionTranslatorOld(tlaExpression);
- try {
- et.start();
- } catch (RuntimeException e) {
- throw new TLA2BIOException(e.getMessage());
- }
-
- return et.BExpression.toString();
- }
-
- public ExpressionTranslatorOld(String TLAExpression) {
- this.TLAExpression = TLAExpression;
- this.variables = new ArrayList<String>();
- this.noVariables = new ArrayList<String>();
- }
-
- public void start() throws TLA2BException {
-
- String dir = System.getProperty("java.io.tmpdir");
- ToolIO.setUserDir(dir);
-
- createStandardModule(dir);
-
- File tempFile = null;
- String moduleName = null;
- String module = null;
- try {
- tempFile = File.createTempFile("Testing", ".tla");
-
- moduleName = tempFile.getName().substring(0,
- tempFile.getName().indexOf("."));
-
- module = "----MODULE " + moduleName + " ----\n"
- + "Expression == " + TLAExpression + "\n====";
-
- FileWriter fw = new FileWriter(tempFile);
- fw.write(module);
- fw.close();
- } catch (IOException e) {
- throw new TLA2BIOException("Can not create file "
- + tempFile.getName() + " in directory '" + dir + "'");
- }
-
- SpecObj spec = parseModuleWithoutSemanticAnalyse(moduleName, module);
- evalVariables(spec, moduleName);
-
- StringBuilder sb = new StringBuilder();
- sb.append("----MODULE " + moduleName + " ----\n");
- sb.append("EXTENDS Naturals, Integers, Sequences, FiniteSets, TLA2B \n");
- if (variables.size() > 0) {
- sb.append("VARIABLES ");
- for (int i = 0; i < variables.size(); i++) {
- if (i != 0) {
- sb.append(", ");
- }
- sb.append(variables.get(i));
- }
- sb.append("\n");
- }
- sb.append("Expression");
- sb.append(" == ");
- sb.append(TLAExpression);
- sb.append("\n====================");
- // System.out.println(sb);
-
- try {
- FileWriter fw = new FileWriter(tempFile);
- fw.write(sb.toString());
- fw.close();
- tempFile.deleteOnExit();
- } catch (IOException e) {
- e.printStackTrace();
- throw new TLA2BIOException(e.getMessage());
- }
- ToolIO.reset();
- BExpression = translate(moduleName, sb.toString());
- }
-
- private static StringBuilder translate(String moduleName, String expr)
- throws TLA2BException {
-
- ModuleNode moduleNode = parseModule(moduleName, expr);
-
- TypeChecker tc = null;//= new TypeChecker(moduleNode);
- try {
- tc.start();
- } catch (TLA2BException e) {
- String[] m = ToolIO.getAllMessages();
- String message = m[0] + "\n" + expr + "\n\n****TypeError****\n"
- + e.getLocalizedMessage();
- // System.out.println(message);
- throw new TypeErrorException(message);
- }
-
- SymbolRenamer symRenamer = new SymbolRenamer(moduleNode);
- symRenamer.start();
-
- ExpressionPrinter p = new ExpressionPrinter(moduleNode);
- p.start();
- return p.getBExpression();
-
- }
-
- /**
- * @param moduleFileName
- * @throws de.tla2b.exceptions.FrontEndException
- */
- private SpecObj parseModuleWithoutSemanticAnalyse(String moduleFileName, String module)
- throws de.tla2b.exceptions.FrontEndException {
- SpecObj spec = new SpecObj(moduleFileName, null);
-
- try {
- SANY.frontEndInitialize(spec, ToolIO.out);
- SANY.frontEndParse(spec, ToolIO.out);
-
- } catch (InitException e1) {
- System.out.println(e1);
- } catch (ParseException e1) {
- System.out.println(e1);
- }
-
- if (spec.parseErrors.isFailure()) {
- String message = module + "\n\n";
- message += Tla2BTranslator.allMessagesToString(ToolIO
- .getAllMessages());
- throw new de.tla2b.exceptions.FrontEndException(message, spec);
- }
- return spec;
- }
-
- public static ModuleNode parseModule(String moduleName, String module)
- throws de.tla2b.exceptions.FrontEndException {
- SpecObj spec = new SpecObj(moduleName, null);
- try {
- SANY.frontEndMain(spec, moduleName, ToolIO.out);
- } catch (FrontEndException e) {
- // Error in Frontend, should never happens
- return null;
- }
-
- if (spec.parseErrors.isFailure()) {
- //String[] m = ToolIO.getAllMessages();
- String message = module + "\n\n"
- + spec.parseErrors;
- // System.out.println(spec.parseErrors);
- message += Tla2BTranslator.allMessagesToString(ToolIO
- .getAllMessages());
- throw new de.tla2b.exceptions.FrontEndException(message, spec);
- }
-
- if (spec.semanticErrors.isFailure()) {
- //String[] m = ToolIO.getAllMessages();
- String message = module + "\n\n" + spec.semanticErrors;
- message += Tla2BTranslator.allMessagesToString(ToolIO
- .getAllMessages());
- throw new de.tla2b.exceptions.FrontEndException(message, spec);
- }
-
- // RootModule
- ModuleNode n = spec.getExternalModuleTable().rootModule;
- if (spec.getInitErrors().isFailure()) {
- System.err.println(spec.getInitErrors());
- throw new de.tla2b.exceptions.FrontEndException(
- Tla2BTranslator
- .allMessagesToString(ToolIO.getAllMessages()),
- spec);
- }
-
- if (n == null) { // Parse Error
- // System.out.println("Rootmodule null");
- throw new de.tla2b.exceptions.FrontEndException(
- Tla2BTranslator
- .allMessagesToString(ToolIO.getAllMessages()),
- spec);
- }
- return n;
- }
-
- /**
- * @param spec
- * @return
- */
- private void evalVariables(SpecObj spec, String moduleName) {
- ParseUnit p = (ParseUnit) spec.parseUnitContext.get(moduleName);
- TreeNode n_module = p.getParseTree();
- TreeNode n_body = n_module.heirs()[2];
- TreeNode n_operatorDefintion = n_body.heirs()[0];
- TreeNode expr = n_operatorDefintion.heirs()[2];
- searchVarInSyntaxTree(expr);
-
- for (int i = 0; i < noVariables.size(); i++) {
- variables.remove(noVariables.get(i));
- }
-
- }
-
- private final static Set<String> KEYWORDS = new HashSet<String>();
- static {
- KEYWORDS.add("BOOLEAN");
- KEYWORDS.add("TRUE");
- KEYWORDS.add("FALSE");
- KEYWORDS.add("Nat");
- KEYWORDS.add("Int");
- KEYWORDS.add("Cardinality");
- KEYWORDS.add("IsFiniteSet");
- KEYWORDS.add("Append");
- KEYWORDS.add("Head");
- KEYWORDS.add("Tail");
- KEYWORDS.add("Len");
- KEYWORDS.add("Seq");
- KEYWORDS.add("SubSeq");
- KEYWORDS.add("SelectSeq");
- KEYWORDS.add("MinOfSet");
- KEYWORDS.add("MaxOfSet");
- KEYWORDS.add("SetProduct");
- KEYWORDS.add("SetSummation");
- KEYWORDS.add("PermutedSequences");
- KEYWORDS.add("@");
-
- }
-
- /**
- *
- */
- private void searchVarInSyntaxTree(TreeNode treeNode) {
- // System.out.println(treeNode.getKind() + " " + treeNode.getImage());
- switch (treeNode.getKind()) {
- case N_GeneralId: {
- String con = treeNode.heirs()[1].getImage();
- if (!variables.contains(con) && !KEYWORDS.contains(con)) {
- variables.add(con);
- }
- break;
- }
- case N_IdentLHS: { // left side of a definition
- TreeNode[] children = treeNode.heirs();
- noVariables.add(children[0].getImage());
- break;
- }
- case N_IdentDecl: { // parameter of a LET definition
- // e.g. x in LET foo(x) == e
- noVariables.add(treeNode.heirs()[0].getImage());
- break;
- }
- case N_FunctionDefinition: {
- // the first child is the function name
- noVariables.add(treeNode.heirs()[0].getImage());
- break;
- }
- case N_UnboundQuant: {
- TreeNode[] children = treeNode.heirs();
- for (int i = 1; i < children.length - 2; i = i + 2) {
- // System.out.println(children[i].getImage());
- }
- searchVarInSyntaxTree(treeNode.heirs()[children.length - 1]);
- break;
- }
- case N_QuantBound: {
- TreeNode[] children = treeNode.heirs();
- for (int i = 0; i < children.length - 2; i = i + 2) {
- String boundedVar = children[i].getImage();
- if (!noVariables.contains(boundedVar)) {
- noVariables.add(boundedVar);
- }
- }
- searchVarInSyntaxTree(treeNode.heirs()[children.length - 1]);
- break;
- }
- case N_SubsetOf: { // { x \in S : e }
- TreeNode[] children = treeNode.heirs();
- String boundedVar = children[1].getImage(); // x
- if (!noVariables.contains(boundedVar)) {
- noVariables.add(boundedVar);
- }
- searchVarInSyntaxTree(treeNode.heirs()[3]); // S
- searchVarInSyntaxTree(treeNode.heirs()[5]); // e
- break;
- }
-
- }
-
- for (int i = 0; i < treeNode.heirs().length; i++) {
- searchVarInSyntaxTree(treeNode.heirs()[i]);
- }
- }
-
- private static File tla2b;
- private void createStandardModule(String dir) throws TLA2BIOException {
- tla2b = new File(dir, "TLA2B.tla");
- try {
- tla2b.createNewFile();
- FileWriter fw = new FileWriter(tla2b);
- fw.write(TLA2B);
- fw.close();
- tla2b.deleteOnExit();
- } catch (IOException e) {
- throw new TLA2BIOException(
- "Can not create standard module TLA2B.tla in directory '"
- + dir + "'");
- }
-
- }
-
- private static final String TLA2B = "--------- MODULE TLA2B ---------\n"
- + "LOCAL INSTANCE Naturals \n" + "LOCAL INSTANCE Sequences \n"
- + "MinOfSet(S) == CHOOSE p \\in S: \\A n \\in S: p \\leq n \n"
- + "MaxOfSet(S) == CHOOSE p \\in S: \\A n \\in S: p \\geq n \n"
- + "SetProduct(S) == S \n" + "SetSummation(S) == S \n"
- + "PermutedSequences(S) == S\n" + "==============================";
-}
diff --git a/src/main/java/de/tla2b/old/TLA2B.java b/src/main/java/de/tla2b/old/TLA2B.java
deleted file mode 100644
index af6a7553f6d98e10053e71bf3e467440f111e60b..0000000000000000000000000000000000000000
--- a/src/main/java/de/tla2b/old/TLA2B.java
+++ /dev/null
@@ -1,276 +0,0 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
-package de.tla2b.old;
-
-import java.io.BufferedReader;
-import java.io.File;
-import java.io.FileReader;
-import java.io.FileWriter;
-import java.io.IOException;
-import java.io.Writer;
-import java.util.Date;
-
-import de.tla2b.exceptions.FrontEndException;
-import de.tla2b.exceptions.NotImplementedException;
-import de.tla2b.exceptions.TLA2BException;
-import de.tla2b.global.TranslationGlobals;
-import util.FileUtil;
-import util.ToolIO;
-
-public class TLA2B implements TranslationGlobals {
- private String mainFile;
- private String path;
- private String configFileName;
- private String mainModuleName;
-
- private static boolean error = false;
-
- public static boolean hasError() {
- return error;
- }
-
- public TLA2B() {
- mainFile = null;
- path = null;
- configFileName = null;
- mainModuleName = null;
- }
-
- public void handleParameter(String[] args) {
- int i;
- for (i = 0; (i < args.length) && (args[i].charAt(0) == '-'); i++) {
- if (args[i].equals("-version")) {
- System.out.println("TLA2B version " + VERSION);
- System.exit(-1);
- } else if (args[i].equals("-expr")) {
- if (i + 1 == args.length) {
- System.err.println("Error: expected a module file.");
- System.exit(-1);
- }
- evalExpression(args[i + 1]);
- return;
- }
-
- else if (args[i].equals("-config")) {
- i++;
- if (i < args.length) {
- configFileName = args[i];
- } else {
- System.err
- .println("Error: expect a file name for -config option.");
- }
-
- } else {
- System.err.println("Illegal switch: " + args[i]);
- System.exit(-1);
- }
- }
-
- if (i == args.length) {
- System.err.println("Error: expected a module file.");
- System.exit(-1);
- }
- mainFile = args[i];
- }
-
- private void evalModuleFileName() throws IOException {
- File file = new File(mainFile);
- String canonicalPath;
- if(file.exists()){
- canonicalPath = file.getCanonicalPath();
- }else {
- throw new IOException("File '"+ mainFile + "' does not exit.");
- }
-
-
- String moduleName = canonicalPath;
- if (moduleName.toLowerCase().endsWith(".tla")) {
- moduleName = moduleName.substring(0, moduleName.length() - 4);
- }
-
- moduleName = moduleName.replace("\\", File.separator);
- moduleName = moduleName.replace("/", File.separator);
-
- mainModuleName = moduleName
- .substring(moduleName.lastIndexOf(FileUtil.separator) + 1);
-
- path = moduleName.substring(0, moduleName.lastIndexOf(FileUtil.separator) + 1);
-
- if (path.equals("")) {
- ToolIO.setUserDir("." + File.separator);
- } else {
- ToolIO.setUserDir(path);
- }
-
- }
-
- private void evalConfigFile() {
- // Config file
- File file;
- if (configFileName == null) {
-
- file = new File(path + mainModuleName + ".cfg");
- // use config if it exists
- if (file.exists()) {
- configFileName = mainModuleName + ".cfg";
- }
- } else {
- // user input
- if (!configFileName.toLowerCase().endsWith(".cfg")) {
- configFileName = configFileName + ".cfg";
- }
- }
- }
-
- public static void main(String[] args) {
- // To indicate an error we use the exit code -1
- TLA2B tla2b = new TLA2B();
- tla2b.handleParameter(args);
-
-
- try {
- tla2b.evalModuleFileName();
- } catch (IOException e) {
- System.err.println(e.getMessage());
- System.exit(-1);
- }
-
- tla2b.evalConfigFile();
-
- ToolIO.setMode(ToolIO.TOOL);
- Tla2BTranslator t = new Tla2BTranslator();
- try {
- t.start(tla2b.mainModuleName, tla2b.configFileName);
- } catch (FrontEndException e) {
- error = true;
- System.err.println(e.getMessage());
- System.exit(-1);
- } catch (TLA2BException e) {
- error = true;
- System.err.println(e.getMessage());
- System.exit(-1);
- } catch (RuntimeException e) {
- error = true;
- System.err.println(e.getMessage());
- System.exit(-1);
- }
- StringBuilder s = new StringBuilder();
- try {
- s = t.translate();
- } catch (NotImplementedException e) {
- error = true;
- System.err.print("**** Translation Error ****\n");
- System.err.print("Not implemented:\n");
- System.err.println(e.getMessage());
- System.exit(-1);
- } catch (TLA2BException e) {
- error = true;
- System.err.print("**** Translation Error ****\n");
- System.err.println(e.getMessage());
- System.exit(-1);
- }
- s.insert(0, "/*@ generated by TLA2B " + VERSION + " " + new Date()
- + " */\n");
- tla2b.createMachineFile(s);
- }
-
- private void createMachineFile(StringBuilder s) {
- String machineFileName = path + mainModuleName + "_tla.mch";
- File machineFile;
- machineFile = new File(machineFileName);
- if (machineFile.exists()) {
- try {
- BufferedReader in;
-
- in = new BufferedReader(new FileReader(machineFile));
-
- String firstLine = null;
- firstLine = in.readLine();
- in.close();
- if (!firstLine.startsWith("/*@ generated by TLA2B ")) {
- System.err.println("Error: File " + machineFileName
- + " already exists"
- + " and was not generated by TLA2B.\n"
- + "Delete or move this file.");
- System.exit(-1);
- }
- } catch (IOException e) {
- System.err.println(e.getMessage());
- System.exit(-1);
- }
- }
-
- try {
- machineFile.createNewFile();
- } catch (IOException e) {
- System.err.println(String.format("Could not create File %s.",
- machineFileName));
- System.exit(-1);
- }
-
- Writer fw = null;
- try {
- String res = s.toString();
- fw = new FileWriter(machineFile);
- fw.write(res);
- fw.close();
- System.out.println("B-Machine " + mainModuleName
- + "_tla.mch created.");
- } catch (IOException e) {
- System.err.println("Error while creating file " + mainModuleName
- + "mch.");
- System.exit(-1);
- }
-
- }
-
- public static String translateFile(String mainFile) throws TLA2BException, IOException {
- TLA2B tla2b = new TLA2B();
- tla2b.mainFile = mainFile;
- tla2b.evalModuleFileName();
- Tla2BTranslator t = new Tla2BTranslator();
- t.start(tla2b.mainModuleName, tla2b.configFileName);
- StringBuilder s = t.translate();
- return s.toString();
- }
-
- /**
- * @throws IOException
- *
- */
- private static void evalExpression(String file) {
-
- ToolIO.setMode(ToolIO.TOOL);
- String expr = null;
- try {
- expr = fileToString(file);
- } catch (IOException e) {
- e.printStackTrace();
- }
- ExpressionTranslatorOld et = new ExpressionTranslatorOld(expr);
- try {
- et.start();
- } catch (TLA2BException e) {
- System.err.println("------ExpressionError----------------");
- System.err.println(e.getMessage());
- }
-
- }
-
- public static String fileToString(String fileName) throws IOException {
- StringBuilder res = new StringBuilder();
- BufferedReader in = new BufferedReader(new FileReader(fileName));
- String str;
- boolean first = true;
- while ((str = in.readLine()) != null) {
- if (!first)
- res.append("\n");
- res.append(str);
- }
- in.close();
- return res.toString();
- }
-
-}
diff --git a/src/main/java/de/tla2b/old/Tla2BTranslator.java b/src/main/java/de/tla2b/old/Tla2BTranslator.java
deleted file mode 100644
index 4bad7d482c2f7e0e78e762d6e65b3d906f0cd748..0000000000000000000000000000000000000000
--- a/src/main/java/de/tla2b/old/Tla2BTranslator.java
+++ /dev/null
@@ -1,212 +0,0 @@
-package de.tla2b.old;
-
-import java.io.File;
-import java.io.FileWriter;
-import java.io.IOException;
-
-import de.tla2b.analysis.InstanceTransformation;
-import de.tla2b.analysis.SpecAnalyser;
-import de.tla2b.analysis.SymbolRenamer;
-import de.tla2b.analysis.SymbolSorter;
-import de.tla2b.analysis.TypeChecker;
-import de.tla2b.config.ConfigfileEvaluator;
-import de.tla2b.config.ModuleOverrider;
-import de.tla2b.exceptions.TLA2BException;
-import de.tla2b.global.TranslationGlobals;
-import tla2sany.drivers.FrontEndException;
-import tla2sany.drivers.SANY;
-import tla2sany.modanalyzer.SpecObj;
-import tla2sany.semantic.ModuleNode;
-import tlc2.tool.ModelConfig;
-import util.FileUtil;
-import util.ToolIO;
-
-public class Tla2BTranslator implements TranslationGlobals {
- private ModuleNode moduleNode;
- private ModelConfig modelConfig;
- private TypeChecker typechecker;
- private String moduleName;
-
- public Tla2BTranslator() {
- this.moduleName = "Testing";
- }
-
- public Tla2BTranslator(String moduleName) {
- this.moduleName = moduleName;
- }
-
- public void start(String moduleFileName, String configFileName)
- throws TLA2BException {
- String moduleName = Tla2BTranslator.evalFileName(moduleFileName);
- moduleNode = parseModule(moduleName);
-
- modelConfig = null;
- if (configFileName != null) {
- modelConfig = new ModelConfig(configFileName, null);
- modelConfig.parse();
- }
- }
-
- public static StringBuilder translateString(String moduleName,
- String moduleString, String configString) throws FrontEndException,
- TLA2BException {
- ToolIO.setMode(ToolIO.TOOL);
- ToolIO.reset();
- Tla2BTranslator translator = new Tla2BTranslator(moduleName);
- translator.startTest(moduleString, configString);
- return translator.translate();
- }
-
- public void startTest(String moduleString, String configString)
- throws de.tla2b.exceptions.FrontEndException, TLA2BException {
- File dir = new File("temp/");
- dir.mkdirs();
-
- try {
- File f = new File("temp/" + moduleName + ".tla");
- f.createNewFile();
- FileWriter fw = new FileWriter(f);
- fw.write(moduleString);
- fw.close();
- f.deleteOnExit();
- } catch (IOException e) {
- e.printStackTrace();
- }
-
- ToolIO.setUserDir("temp/");
- moduleNode = parseModule(moduleName + ".tla");
-
- modelConfig = null;
- if (configString != null) {
- File f = new File("temp/" + moduleName + ".cfg");
- try {
- f.createNewFile();
- FileWriter fw = new FileWriter(f);
- fw.write(configString);
- fw.close();
- } catch (IOException e) {
- e.printStackTrace();
- }
- modelConfig = new ModelConfig(moduleName + ".cfg", null);
- modelConfig.parse();
- f.deleteOnExit();
- }
- dir.deleteOnExit();
- }
-
- public StringBuilder translate() throws TLA2BException {
- InstanceTransformation trans = new InstanceTransformation(moduleNode);
- trans.start();
-
- SymbolSorter symbolSorter = new SymbolSorter(moduleNode);
- symbolSorter.sort();
-
- SpecAnalyser specAnalyser;
-
- ConfigfileEvaluator conEval = null;
- if (modelConfig != null) {
-
- conEval = new ConfigfileEvaluator(modelConfig, moduleNode);
- conEval.start();
-
- ModuleOverrider modOver = new ModuleOverrider(moduleNode, conEval);
- modOver.start();
- specAnalyser = SpecAnalyser.createSpecAnalyser(moduleNode, conEval);
- } else {
- specAnalyser = SpecAnalyser.createSpecAnalyser(moduleNode);
- }
-
- specAnalyser.start();
-
- typechecker = new TypeChecker(moduleNode, conEval, specAnalyser);
- typechecker.start();
-
- //specAnalyser.evalIfThenElse();
-
- SymbolRenamer symRenamer = new SymbolRenamer(moduleNode, specAnalyser);
- symRenamer.start();
-// BMachinePrinter p = new BMachinePrinter(moduleNode, conEval,
-// specAnalyser);
- // BAstCreator bAstCreator = new BAstCreator(moduleNode, conEval,
- // specAnalyser);
-
- return null;
- }
-
- public static ModuleNode parseModule(String moduleName)
- throws de.tla2b.exceptions.FrontEndException {
- SpecObj spec = new SpecObj(moduleName, null);
- try {
- SANY.frontEndMain(spec, moduleName, ToolIO.out);
- } catch (FrontEndException e) {
- // Error in Frontend, should never happens
- return null;
- }
-
- if (spec.parseErrors.isFailure()) {
- throw new de.tla2b.exceptions.FrontEndException(
- allMessagesToString(ToolIO.getAllMessages())
- + spec.parseErrors, spec);
- }
-
- if (spec.semanticErrors.isFailure()) {
- throw new de.tla2b.exceptions.FrontEndException(
- // allMessagesToString(ToolIO.getAllMessages())
- "" + spec.semanticErrors, spec);
- }
-
- // RootModule
- ModuleNode n = spec.getExternalModuleTable().rootModule;
- if (spec.getInitErrors().isFailure()) {
- System.err.println(spec.getInitErrors());
- return null;
- }
-
- if (n == null) { // Parse Error
- // System.out.println("Rootmodule null");
- throw new de.tla2b.exceptions.FrontEndException(
- allMessagesToString(ToolIO.getAllMessages()), spec);
- }
- return n;
- }
-
- public static String allMessagesToString(String[] allMessages) {
- StringBuilder sb = new StringBuilder();
- for (int i = 0; i < allMessages.length - 1; i++) {
- sb.append(allMessages[i] + "\n");
- }
- return sb.toString();
- }
-
- public static String evalFileName(String name) {
- if (name.toLowerCase().endsWith(".tla")) {
- name = name.substring(0, name.length() - 4);
- }
-
- if (name.toLowerCase().endsWith(".cfg")) {
- name = name.substring(0, name.length() - 4);
- }
-
- String sourceModuleName = name.substring(name
- .lastIndexOf(FileUtil.separator) + 1);
-
- String path = name.substring(0,
- name.lastIndexOf(FileUtil.separator) + 1);
- if (!path.equals(""))
- ToolIO.setUserDir(path);
- return sourceModuleName;
- }
-
- public ModuleNode getModuleNode() {
- return moduleNode;
- }
-
- public ModelConfig getModelConfig() {
- return modelConfig;
- }
-
- public TypeChecker getTypecheChecker() {
- return typechecker;
- }
-
-}
diff --git a/src/main/java/de/tla2b/output/PrologPrinter.java b/src/main/java/de/tla2b/output/PrologPrinter.java
index ba951aeb67ba03dc2c88e17f8a6c416ae85614af..46ba2b8bfde6657c2d2e3e88483d81f9fb23b129 100644
--- a/src/main/java/de/tla2b/output/PrologPrinter.java
+++ b/src/main/java/de/tla2b/output/PrologPrinter.java
@@ -12,7 +12,6 @@ import java.util.Map;
import de.be4.classicalb.core.parser.BParser;
import de.be4.classicalb.core.parser.analysis.pragma.Pragma;
import de.be4.classicalb.core.parser.analysis.prolog.ASTProlog;
-import de.be4.classicalb.core.parser.analysis.prolog.ClassicalPositionPrinter;
import de.be4.classicalb.core.parser.analysis.prolog.NodeIdAssignment;
import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader;
import de.be4.classicalb.core.parser.node.Node;
@@ -85,16 +84,14 @@ public class PrologPrinter {
pout.fullstop();
}
-// if (bParser.getPragmas().size() > 0) {
-// NodeIdAssignment ids = pprinter.nodeIds;
-//
-// List<Pragma> pragmas = bParser.getPragmas();
-// for (Pragma pragma : pragmas) {
-// pragma.printProlog(pout, ids);
-// pout.fullstop();
-// }
-//
-// }
+ if (bParser.getPragmas().size() > 0) {
+ NodeIdAssignment ids = pprinter.nodeIds;
+ List<Pragma> pragmas = bParser.getPragmas();
+ for (Pragma pragma : pragmas) {
+ pragma.printProlog(pout, ids);
+ pout.fullstop();
+ }
+ }
pout.flush();
}
}
diff --git a/src/main/java/de/tla2b/output/TlaTypePrinter.java b/src/main/java/de/tla2b/output/TlaTypePrinter.java
index 724cfcb52adfb14478f96de54f3668b8103b1671..c6a5dde512ca8c23712e8b70ca4bdc95cffdb366 100644
--- a/src/main/java/de/tla2b/output/TlaTypePrinter.java
+++ b/src/main/java/de/tla2b/output/TlaTypePrinter.java
@@ -48,20 +48,35 @@ public class TlaTypePrinter implements PositionPrinter, TypeVisitorInterface {
}
public void printPosition(final Node node) {
- pout.openTerm("info");
- final Integer id = nodeIds.lookup(node);
- pout.printNumber(id);
-
- pout.openTerm("tla_type");
TLAType type = typeTable.get(node);
- if (type == null) {
+ if (type != null) {
+ pout.openTerm("info");
+ }
+
+ final Integer id = nodeIds.lookup(node);
+ if (id == null) {
pout.printAtom("none");
} else {
- type.apply(this);
+ if (positions == null) {
+ pout.printNumber(id);
+ } else {
+ pout.openTerm("pos", true);
+ pout.printNumber(id);
+ pout.printNumber(nodeIds.lookupFileNumber(node));
+ pout.printNumber(positions.getBeginLine(node));
+ pout.printNumber(positions.getBeginColumn(node));
+ pout.printNumber(positions.getEndLine(node));
+ pout.printNumber(positions.getEndColumn(node));
+ pout.closeTerm();
+ }
}
- pout.closeTerm();
+ if (type != null) {
+ pout.openTerm("tla_type");
+ type.apply(this);
+ pout.closeTerm();
- pout.closeTerm();
+ pout.closeTerm();
+ }
}
public void setPrologTermOutput(final IPrologTermOutput pout) {
@@ -125,8 +140,13 @@ public class TlaTypePrinter implements PositionPrinter, TypeVisitorInterface {
}
public void caseTupleType(TupleType type) {
- // TODO Auto-generated method stub
-
+ pout.openTerm("tuple");
+ pout.openList();
+ for (TLAType t : type.getTypes()) {
+ t.apply(this);
+ }
+ pout.closeList();
+ pout.closeTerm();
}
public void caseUntyped(UntypedType type) {
diff --git a/src/main/java/de/tla2b/translation/OperationsFinder.java b/src/main/java/de/tla2b/translation/OperationsFinder.java
index 78f7925eac3de33023355da974360e7d9f53be18..cf92e6b5d8ffc5230ac463490264bf3faa639fad 100644
--- a/src/main/java/de/tla2b/translation/OperationsFinder.java
+++ b/src/main/java/de/tla2b/translation/OperationsFinder.java
@@ -47,19 +47,19 @@ public class OperationsFinder extends AbstractASTVisitor implements
}
case NumeralKind: {
throw new RuntimeException(String.format(
- "Expected an action.\n%s", n.getLocation().toString()));
+ "Expected an action.%n%s", n.getLocation().toString()));
}
case StringKind: {
throw new RuntimeException(String.format(
- "Expected an action.\n%s", n.getLocation().toString()));
+ "Expected an action.%n%s", n.getLocation().toString()));
}
case SubstInKind: {
throw new RuntimeException(String.format(
- "Expected an action.\n%s", n.getLocation().toString()));
+ "Expected an action.%n%s", n.getLocation().toString()));
}
case AtNodeKind: { // @
throw new RuntimeException(String.format(
- "Expected an action.\n%s", n.getLocation().toString()));
+ "Expected an action.%n%s", n.getLocation().toString()));
}
case LetInKind: {
// we do not visit the local definitions
@@ -148,7 +148,7 @@ public class OperationsFinder extends AbstractASTVisitor implements
}
throw new RuntimeException(String.format(
- "Expected an action at '%s' :\n%s", n.getOperator().getName()
+ "Expected an action at '%s' :%n%s", n.getOperator().getName()
.toString(), n.getLocation().toString()));
}
diff --git a/src/main/java/de/tla2b/types/StructOrFunctionType.java b/src/main/java/de/tla2b/types/StructOrFunctionType.java
index 493bbdedc49d3e441e2b6f0935291a5e9b7dc3d4..9b662311900d1f6c62b823e496caa0575acaf070 100644
--- a/src/main/java/de/tla2b/types/StructOrFunctionType.java
+++ b/src/main/java/de/tla2b/types/StructOrFunctionType.java
@@ -13,8 +13,6 @@ import de.be4.classicalb.core.parser.node.PExpression;
import de.tla2b.exceptions.UnificationException;
import de.tla2b.output.TypeVisitorInterface;
-
-
public class StructOrFunctionType extends AbstractHasFollowers {
private LinkedHashMap<String, TLAType> types;
@@ -49,15 +47,17 @@ public class StructOrFunctionType extends AbstractHasFollowers {
@Override
public String toString() {
- String res = "StructOrFunction(";
+ StringBuilder sb = new StringBuilder();
+ sb.append("StructOrFunction(");
for (Iterator<String> keys = types.keySet().iterator(); keys.hasNext();) {
String key = keys.next();
- res += "\""+key + "\" : " + types.get(key);
+ sb.append("\"").append(key).append("\"");
+ sb.append(" : ").append(types.get(key));
if (keys.hasNext())
- res += ", ";
+ sb.append(", ");
}
- res += ")";
- return res;
+ sb.append(")");
+ return sb.toString();
}
@Override
@@ -168,8 +168,8 @@ public class StructOrFunctionType extends AbstractHasFollowers {
while (itr.hasNext()) {
temp = temp.unify(itr.next());
}
- SetType found = new SetType(new PairType(
- StringType.getInstance(), temp));
+ SetType found = new SetType(new PairType(StringType.getInstance(),
+ temp));
return found.unify(o);
}
if (o instanceof StructType) {
@@ -221,8 +221,7 @@ public class StructOrFunctionType extends AbstractHasFollowers {
public SetType getFunction() {
Iterator<TLAType> itr = types.values().iterator();
- return new SetType(new PairType(StringType.getInstance(),
- itr.next()));
+ return new SetType(new PairType(StringType.getInstance(), itr.next()));
}
@Override
diff --git a/src/main/java/de/tla2b/types/StructType.java b/src/main/java/de/tla2b/types/StructType.java
index b995c714a901c54fd7f97a64b729c83a70162697..61dd2cae8ffbc8cabfda2f946b6f13171632df08 100644
--- a/src/main/java/de/tla2b/types/StructType.java
+++ b/src/main/java/de/tla2b/types/StructType.java
@@ -1,7 +1,6 @@
package de.tla2b.types;
import java.util.ArrayList;
-import java.util.Hashtable;
import java.util.Iterator;
import java.util.LinkedHashMap;
import java.util.List;
@@ -122,7 +121,7 @@ public class StructType extends AbstractHasFollowers {
if (o instanceof StructType) {
StructType s = (StructType) o;
boolean extendStruct = false;
-
+
if (this.incompleteStruct && s.incompleteStruct) {
extendStruct = false;
} else if (this.incompleteStruct) {
@@ -203,18 +202,20 @@ public class StructType extends AbstractHasFollowers {
@Override
public String toString() {
- String res = "struct(";
+ StringBuilder sb = new StringBuilder();
+ sb.append("struct(");
Iterator<String> keys = types.keySet().iterator();
- if (!keys.hasNext())
- res += "...";
+ if (!keys.hasNext()) {
+ sb.append("...");
+ }
while (keys.hasNext()) {
String fieldName = (String) keys.next();
- res += fieldName + ":" + types.get(fieldName);
+ sb.append(fieldName).append(":").append(types.get(fieldName));
if (keys.hasNext())
- res += ",";
+ sb.append(",");
}
- res += ")";
- return res;
+ sb.append(")");
+ return sb.toString();
}
@Override
@@ -241,9 +242,9 @@ public class StructType extends AbstractHasFollowers {
public void apply(TypeVisitorInterface visitor) {
visitor.caseStructType(this);
}
-
- public LinkedHashMap<String, TLAType> getTypeTable(){
+
+ public LinkedHashMap<String, TLAType> getTypeTable() {
return this.types;
}
-
+
}
diff --git a/src/main/java/de/tla2b/types/TupleType.java b/src/main/java/de/tla2b/types/TupleType.java
index 8d03bd3effb8c1a80179e342cd3f2daf6c4d2912..71ed583e283687094a3a5e6c49707d2c519e3779 100644
--- a/src/main/java/de/tla2b/types/TupleType.java
+++ b/src/main/java/de/tla2b/types/TupleType.java
@@ -184,18 +184,17 @@ public class TupleType extends AbstractHasFollowers {
@Override
public String toString() {
- String res = "";
+ StringBuilder sb = new StringBuilder();
for (int i = 0; i < types.size(); i++) {
if (types.get(i) instanceof TupleType && i != 0) {
- res += "(" + types.get(i) + ")";
+ sb.append("(").append(types.get(i)).append(")");
} else
- res += types.get(i);
-
+ sb.append(types.get(i));
if (i < types.size() - 1) {
- res += "*";
+ sb.append("*");
}
}
- return res;
+ return sb.toString();
}
@Override
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 6b98ba280ebbde319b211983a95263cc01ba4eb8..469b7c051c9dddde4b2f9f449073fb40ca65947e 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -9,7 +9,6 @@ import java.util.List;
import java.util.Map.Entry;
import java.util.Set;
-import sun.audio.AudioPlayer;
import tla2sany.semantic.ASTConstants;
import tla2sany.semantic.AssumeNode;
import tla2sany.semantic.AtNode;
@@ -24,7 +23,6 @@ import tla2sany.semantic.OpDeclNode;
import tla2sany.semantic.OpDefNode;
import tla2sany.semantic.StringNode;
import tla2sany.semantic.SymbolNode;
-import tla2tex.TLA;
import tlc2.tool.BuiltInOPs;
import tlc2.value.ModelValue;
import tlc2.value.SetEnumValue;
diff --git a/src/main/java/de/tla2bAst/ExpressionTranslator.java b/src/main/java/de/tla2bAst/ExpressionTranslator.java
index a8b8314f2d7c802d3169a2e0cc7dd936fc08a8d7..0e3397f5a4fb376a21b61c849c859ca2818a2808 100644
--- a/src/main/java/de/tla2bAst/ExpressionTranslator.java
+++ b/src/main/java/de/tla2bAst/ExpressionTranslator.java
@@ -22,7 +22,6 @@ import de.tla2b.analysis.SpecAnalyser;
import de.tla2b.analysis.SymbolRenamer;
import de.tla2b.analysis.TypeChecker;
import de.tla2b.exceptions.TLA2BException;
-import de.tla2b.old.Tla2BTranslator;
public class ExpressionTranslator implements SyntaxTreeConstants {
@@ -33,7 +32,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
private ModuleNode moduleNode;
private String expr;
private Translator translator;
-
+
public Start getBExpressionParseUnit() {
return expressionStart;
}
@@ -67,8 +66,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
fw.write(module);
fw.close();
} catch (IOException e) {
- throw new RuntimeException("Can not create file "
- + tempFile.getName() + " in directory '" + dir + "'");
+ throw new RuntimeException("Can not create file temporary file in directory '" + dir + "'");
}
SpecObj spec = parseModuleWithoutSemanticAnalyse(moduleName, module);
@@ -102,9 +100,9 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
throw new RuntimeException(e.getMessage());
}
ToolIO.reset();
-
+
this.expr = sb.toString();
-
+
this.moduleNode = null;
try {
moduleNode = parseModule(moduleName, sb.toString());
@@ -113,13 +111,12 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
}
}
- public Start translateIncludingModel() throws TLA2BException{
+ public Start translateIncludingModel() throws TLA2BException {
SpecAnalyser specAnalyser = SpecAnalyser
.createSpecAnalyserForTlaExpression(moduleNode);
TypeChecker tc = translator.getTypeChecker();
tc.visitOpDefNode(specAnalyser.getExpressionOpdefNode());
-
-
+
SymbolRenamer symRenamer = new SymbolRenamer(moduleNode, specAnalyser);
symRenamer.start();
BAstCreator bASTCreator = new BAstCreator(moduleNode, specAnalyser);
@@ -127,8 +124,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
this.expressionStart = bASTCreator.expressionStart;
return this.expressionStart;
}
-
-
+
public Start translate() {
SpecAnalyser specAnalyser = SpecAnalyser
.createSpecAnalyserForTlaExpression(moduleNode);
@@ -165,16 +161,14 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
// String[] m = ToolIO.getAllMessages();
String message = module + "\n\n" + spec.parseErrors;
// System.out.println(spec.parseErrors);
- message += Tla2BTranslator.allMessagesToString(ToolIO
- .getAllMessages());
+ message += allMessagesToString(ToolIO.getAllMessages());
throw new de.tla2b.exceptions.FrontEndException(message, spec);
}
if (spec.semanticErrors.isFailure()) {
// String[] m = ToolIO.getAllMessages();
String message = module + "\n\n" + spec.semanticErrors;
- message += Tla2BTranslator.allMessagesToString(ToolIO
- .getAllMessages());
+ message += allMessagesToString(ToolIO.getAllMessages());
throw new de.tla2b.exceptions.FrontEndException(message, spec);
}
@@ -183,17 +177,14 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
if (spec.getInitErrors().isFailure()) {
System.err.println(spec.getInitErrors());
throw new de.tla2b.exceptions.FrontEndException(
- Tla2BTranslator
- .allMessagesToString(ToolIO.getAllMessages()),
- spec);
+
+ allMessagesToString(ToolIO.getAllMessages()), spec);
}
if (n == null) { // Parse Error
// System.out.println("Rootmodule null");
throw new de.tla2b.exceptions.FrontEndException(
- Tla2BTranslator
- .allMessagesToString(ToolIO.getAllMessages()),
- spec);
+ allMessagesToString(ToolIO.getAllMessages()), spec);
}
return n;
}
@@ -218,8 +209,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
if (spec.parseErrors.isFailure()) {
String message = module + "\n\n";
- message += Tla2BTranslator.allMessagesToString(ToolIO
- .getAllMessages());
+ message += allMessagesToString(ToolIO.getAllMessages());
// throw new de.tla2b.exceptions.FrontEndException(message, spec);
throw new RuntimeException(message);
}
@@ -266,7 +256,6 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
KEYWORDS.add("SetSummation");
KEYWORDS.add("PermutedSequences");
KEYWORDS.add("@");
-
}
/**
@@ -333,4 +322,12 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
searchVarInSyntaxTree(treeNode.heirs()[i]);
}
}
+
+ public static String allMessagesToString(String[] allMessages) {
+ StringBuilder sb = new StringBuilder();
+ for (int i = 0; i < allMessages.length - 1; i++) {
+ sb.append(allMessages[i] + "\n");
+ }
+ return sb.toString();
+ }
}
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index 451acbcbd9d5cf3e90f275d9ec8b6c2d5e31e762..f3fbf4202759122fcfdcb698650aeba728eda4c1 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -1,15 +1,18 @@
package de.tla2bAst;
+import java.io.BufferedOutputStream;
import java.io.BufferedReader;
+import java.io.BufferedWriter;
import java.io.File;
import java.io.FileNotFoundException;
+import java.io.FileOutputStream;
import java.io.FileReader;
-import java.io.FileWriter;
import java.io.IOException;
+import java.io.OutputStreamWriter;
+import java.io.PrintStream;
import java.io.PrintWriter;
-import java.io.Writer;
+import java.io.UnsupportedEncodingException;
import java.util.Date;
-import java.util.HashMap;
import java.util.Hashtable;
import de.be4.classicalb.core.parser.BParser;
@@ -55,7 +58,6 @@ public class Translator implements TranslationGlobals {
// private String moduleName;
private ModuleNode moduleNode;
private ModelConfig modelConfig;
- private String bMachineString;
private SpecAnalyser specAnalyser;
private TypeChecker typechecker;
@@ -97,30 +99,34 @@ public class Translator implements TranslationGlobals {
try {
moduleFile = new File("temp/" + moduleName + ".tla");
moduleFile.createNewFile();
- FileWriter fw = new FileWriter(moduleFile);
- fw.write(moduleString);
- fw.close();
- // f.deleteOnExit();
+ BufferedWriter out = new BufferedWriter(new OutputStreamWriter(
+ new FileOutputStream(moduleFile), "UTF-8"));
+ try {
+ out.write(moduleString);
+ } finally {
+ out.close();
+ }
moduleFileName = moduleFile.getAbsolutePath();
} catch (IOException e) {
e.printStackTrace();
}
-
modelConfig = null;
if (configString != null) {
configFile = new File("temp/" + moduleName + ".cfg");
try {
configFile.createNewFile();
- FileWriter fw = new FileWriter(configFile);
- fw.write(configString);
- fw.close();
+ BufferedWriter out = new BufferedWriter(new OutputStreamWriter(
+ new FileOutputStream(configFile), "UTF-8"));
+ try {
+ out.write(configString);
+ } finally {
+ out.close();
+ }
} catch (IOException e) {
e.printStackTrace();
}
- // f.deleteOnExit();
}
dir.deleteOnExit();
-
parse();
}
@@ -246,20 +252,24 @@ public class Translator implements TranslationGlobals {
try {
final RecursiveMachineLoader rml = parseAllMachines(getBAST(),
getModuleFile(), bParser);
- //rml.printAsProlog(new PrintWriter(System.out), false);
- //rml.printAsProlog(new PrintWriter(probFile), false);
+ // rml.printAsProlog(new PrintWriter(System.out), false);
+ // rml.printAsProlog(new PrintWriter(probFile), false);
String moduleName = FileUtils.removeExtention(moduleFile.getName());
PrologPrinter prologPrinter = new PrologPrinter(rml, bParser,
moduleFile, moduleName, typeTable);
- prologPrinter.printAsProlog(new PrintWriter(probFile), false);
+ // prologPrinter.printAsProlog(new PrintWriter(probFile), false);
+ prologPrinter.printAsProlog(new PrintWriter(probFile, "UTF-8"), false);
System.out.println(probFile.getAbsolutePath() + " created.");
-
+
prologPrinter.printAsProlog(new PrintWriter(System.out), false);
+ ;
} catch (BException e) {
e.printStackTrace();
} catch (FileNotFoundException e) {
e.printStackTrace();
+ } catch (UnsupportedEncodingException e) {
+ e.printStackTrace();
}
}
@@ -304,11 +314,14 @@ public class Translator implements TranslationGlobals {
result.insert(0, "/*@ generated by TLA2B " + VERSION + " " + new Date()
+ " */\n");
- Writer fw = null;
try {
- fw = new FileWriter(machineFile);
- fw.write(result.toString());
- fw.close();
+ BufferedWriter out = new BufferedWriter(new OutputStreamWriter(
+ new FileOutputStream(machineFile), "UTF-8"));
+ try {
+ out.write(result.toString());
+ } finally {
+ out.close();
+ }
System.out.println("B-Machine " + machineFile.getAbsolutePath()
+ " created.");
} catch (IOException e) {
@@ -349,10 +362,6 @@ public class Translator implements TranslationGlobals {
return bDefinitions;
}
- public String getBMachineString() {
- return bMachineString;
- }
-
public ModuleNode getModuleNode() {
return moduleNode;
}
diff --git a/src/test/java/de/tla2b/prettyprintb/ExceptTest.java b/src/test/java/de/tla2b/prettyprintb/ExceptTest.java
index 23813f430439f89d72df72d3d55ba996dd5ca693..d7952e0f8bb2a9feb6e09676f200184298a59a60 100644
--- a/src/test/java/de/tla2b/prettyprintb/ExceptTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/ExceptTest.java
@@ -19,12 +19,11 @@ public class ExceptTest {
+ "=================================";
final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
- + "PROPERTIES "
- + " k : BOOL +-> INTEGER "
+ + "PROPERTIES " + " k : BOOL +-> INTEGER "
+ "& k = k <+ {TRUE |-> 0, FALSE |-> 0}" + "END";
compare(expected, module);
}
-
+
@Test
public void testFunctionExcept2() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -33,13 +32,12 @@ public class ExceptTest {
+ "=================================";
final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
- + "PROPERTIES "
- + " k : BOOL +-> INTEGER "
+ + "PROPERTIES " + " k : BOOL +-> INTEGER "
+ "& k = k <+ {TRUE |-> 0, FALSE |-> 0}" + "END";
compare(expected, module);
-
+
}
-
+
@Test
public void testFunctionExceptAt() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -54,6 +52,7 @@ public class ExceptTest {
+ "END";
compare(expected, module);
}
+
@Ignore
@Test
public void testFunctionExceptAt2() throws Exception {
@@ -64,14 +63,11 @@ public class ExceptTest {
+ "ASSUME k = [x,y \\in {1,2} |-> x+y] /\\ k2 = [k EXCEPT ![1,1] = @ + 4] \n"
+ "=================================";
- StringBuilder sb = TestUtil.translateString(module);
- System.out.println(sb);
final String expected = "MACHINE Testing\n"
+ "ABSTRACT_CONSTANTS k, k2\n"
+ "PROPERTIES k : POW(INTEGER*INTEGER*INTEGER) "
+ "& k2 : POW(INTEGER*INTEGER*INTEGER) "
+ "& k = %x,y.(x : {1, 2} & y : {1, 2}| x + y) "
+ "& k2 = k <+ {(1, 1) |-> k(1, 1) + 4} \n" + "END";
- assertEquals(TestUtil.getAstStringofBMachineString(expected), TestUtil.getAstStringofBMachineString(sb.toString()));
}
}
diff --git a/src/test/java/de/tla2b/util/TestTypeChecker.java b/src/test/java/de/tla2b/util/TestTypeChecker.java
index 9c30e3afede6ca20e5c5d89da6f1a131f5a975b8..5e5960cd8eddbd6571af4d681e5c00ec71e86d86 100644
--- a/src/test/java/de/tla2b/util/TestTypeChecker.java
+++ b/src/test/java/de/tla2b/util/TestTypeChecker.java
@@ -9,7 +9,6 @@ import java.util.Hashtable;
import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.global.TranslationGlobals;
-import de.tla2b.old.Tla2BTranslator;
import de.tla2b.types.TLAType;
import de.tla2bAst.Translator;
import tla2sany.semantic.FormalParamNode;
diff --git a/src/test/java/de/tla2b/util/TestUtil.java b/src/test/java/de/tla2b/util/TestUtil.java
index 355e27ec1cdbd74aff51486230ef4c46694e5f42..f09e791d012695b567898b3aa266a09a0798ae8e 100644
--- a/src/test/java/de/tla2b/util/TestUtil.java
+++ b/src/test/java/de/tla2b/util/TestUtil.java
@@ -17,7 +17,6 @@ import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.Start;
import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
-import de.tla2b.old.Tla2BTranslator;
import de.tla2b.output.ASTPrettyPrinter;
import de.tla2b.output.Renamer;
import de.tla2bAst.Translator;
@@ -26,14 +25,14 @@ import util.ToolIO;
public class TestUtil {
- public static StringBuilder translateString(String moduleString)
- throws FrontEndException, TLA2BException, AbortException {
- ToolIO.setMode(ToolIO.TOOL);
- ToolIO.reset();
- Tla2BTranslator translator = new Tla2BTranslator();
- translator.startTest(moduleString, null);
- return translator.translate();
- }
+// public static StringBuilder translateString(String moduleString)
+// throws FrontEndException, TLA2BException, AbortException {
+// ToolIO.setMode(ToolIO.TOOL);
+// ToolIO.reset();
+// Tla2BTranslator translator = new Tla2BTranslator();
+// translator.startTest(moduleString, null);
+// return translator.translate();
+// }
public static void runModule(String tlaFile) throws Exception{
Translator t = new Translator(tlaFile);
@@ -105,22 +104,6 @@ public class TestUtil {
assertEquals(expected, getTreeAsString(ast));
}
- public static void compareWithPrintResult(String tlaModule) throws Exception{
- ToolIO.setMode(ToolIO.TOOL);
-
- Translator trans = new Translator(tlaModule);
- Start resultNode = trans.translate();
-
- String printResult = getAstStringofBMachineString(trans.getBMachineString());
-
- //BParser.printASTasProlog(System.out, new BParser(), new File("./test.mch"), resultNode, false, true, null);
-
- String result = getTreeAsString(resultNode);
- assertEquals(printResult, result);
- System.out.println(result);
- }
-
-
public static void compare(String bMachine, String tlaModule, String config) throws BException, TLA2BException{
ToolIO.setMode(ToolIO.TOOL);
String expected = getAstStringofBMachineString(bMachine);
@@ -147,37 +130,37 @@ public class TestUtil {
}
- 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 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{
diff --git a/src/test/resources/regression/Club/Club.prob b/src/test/resources/regression/Club/Club.prob
index a379719b0d16c6444c3ebbe1c1fb30c8fa723683..037f9f3eb6bed1ed6af56bef64e201879f9ad7db 100644
--- a/src/test/resources/regression/Club/Club.prob
+++ b/src/test/resources/regression/Club/Club.prob
@@ -1,3 +1,3 @@
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(info(1,tla_type(none)),machine(info(2,tla_type(none))),machine_header(info(3,tla_type(none)),'Club',[]),[sets(info(4,tla_type(none)),[enumerated_set(info(5,tla_type(none)),'ENUM1',[identifier(info(6,tla_type(none)),n1),identifier(info(7,tla_type(none)),n2),identifier(info(8,tla_type(none)),n3)])]),abstract_constants(info(9,tla_type(none)),[identifier(info(10,tla_type(integer)),capacity),identifier(info(11,tla_type(set(modelvalue))),'NAME'),identifier(info(12,tla_type(integer)),total)]),properties(info(13,tla_type(none)),conjunct(info(14,tla_type(none)),conjunct(info(15,tla_type(none)),conjunct(info(16,tla_type(none)),conjunct(info(17,tla_type(none)),conjunct(info(18,tla_type(none)),member(info(19,tla_type(none)),identifier(info(20,tla_type(none)),capacity),integer_set(info(21,tla_type(none)))),equal(info(22,tla_type(none)),identifier(info(23,tla_type(none)),'NAME'),identifier(info(24,tla_type(none)),'ENUM1'))),member(info(25,tla_type(none)),identifier(info(26,tla_type(none)),total),integer_set(info(27,tla_type(none))))),conjunct(info(28,tla_type(none)),member(info(29,tla_type(none)),identifier(info(30,tla_type(none)),capacity),natural_set(info(31,tla_type(none)))),equal(info(32,tla_type(none)),identifier(info(33,tla_type(none)),capacity),integer(info(34,tla_type(none)),2)))),greater(info(35,tla_type(none)),card(info(36,tla_type(none)),identifier(info(37,tla_type(none)),'NAME')),identifier(info(38,tla_type(none)),capacity))),conjunct(info(39,tla_type(none)),member(info(40,tla_type(none)),identifier(info(41,tla_type(none)),total),natural_set(info(42,tla_type(none)))),greater(info(43,tla_type(none)),identifier(info(44,tla_type(none)),total),integer(info(45,tla_type(none)),2))))),variables(info(46,tla_type(none)),[identifier(info(47,tla_type(set(modelvalue))),member),identifier(info(48,tla_type(set(modelvalue))),waiting)]),invariant(info(49,tla_type(none)),conjunct(info(50,tla_type(none)),member(info(51,tla_type(none)),identifier(info(52,tla_type(none)),member),pow_subset(info(53,tla_type(none)),identifier(info(54,tla_type(none)),'ENUM1'))),member(info(55,tla_type(none)),identifier(info(56,tla_type(none)),waiting),pow_subset(info(57,tla_type(none)),identifier(info(58,tla_type(none)),'ENUM1'))))),initialisation(info(59,tla_type(none)),becomes_such(info(60,tla_type(none)),[identifier(info(61,tla_type(none)),member),identifier(info(62,tla_type(none)),waiting)],conjunct(info(63,tla_type(none)),equal(info(64,tla_type(none)),identifier(info(65,tla_type(none)),member),empty_set(info(66,tla_type(none)))),equal(info(67,tla_type(none)),identifier(info(68,tla_type(none)),waiting),empty_set(info(69,tla_type(none))))))),operations(info(70,tla_type(none)),[operation(info(71,tla_type(none)),identifier(info(71,tla_type(none)),join_queue),[],[identifier(info(72,tla_type(none)),nn)],any(info(73,tla_type(none)),[identifier(info(74,tla_type(none)),member_n)],conjunct(info(75,tla_type(none)),conjunct(info(76,tla_type(none)),conjunct(info(77,tla_type(none)),conjunct(info(78,tla_type(none)),conjunct(info(79,tla_type(none)),member(info(80,tla_type(none)),identifier(info(81,tla_type(none)),nn),identifier(info(82,tla_type(none)),'NAME')),not_member(info(83,tla_type(none)),identifier(info(84,tla_type(none)),nn),identifier(info(85,tla_type(none)),member))),not_member(info(86,tla_type(none)),identifier(info(87,tla_type(none)),nn),identifier(info(88,tla_type(none)),waiting))),member(info(89,tla_type(none)),identifier(info(90,tla_type(none)),member_n),pow_subset(info(91,tla_type(none)),identifier(info(92,tla_type(none)),'ENUM1')))),less(info(93,tla_type(none)),card(info(94,tla_type(none)),identifier(info(95,tla_type(none)),waiting)),identifier(info(96,tla_type(none)),total))),equal(info(97,tla_type(none)),identifier(info(98,tla_type(none)),member_n),identifier(info(99,tla_type(none)),member))),assign(info(100,tla_type(none)),[identifier(info(101,tla_type(none)),waiting),identifier(info(102,tla_type(none)),member)],[union(info(103,tla_type(none)),identifier(info(104,tla_type(none)),waiting),set_extension(info(105,tla_type(none)),[identifier(info(106,tla_type(none)),nn)])),identifier(info(107,tla_type(none)),member_n)]))),operation(info(108,tla_type(none)),identifier(info(108,tla_type(none)),join),[],[identifier(info(109,tla_type(none)),nn)],select(info(110,tla_type(none)),conjunct(info(111,tla_type(none)),conjunct(info(112,tla_type(none)),conjunct(info(113,tla_type(none)),member(info(114,tla_type(none)),identifier(info(115,tla_type(none)),nn),identifier(info(116,tla_type(none)),'NAME')),member(info(117,tla_type(none)),identifier(info(118,tla_type(none)),nn),identifier(info(119,tla_type(none)),waiting))),less(info(120,tla_type(none)),card(info(121,tla_type(none)),identifier(info(122,tla_type(none)),member)),identifier(info(123,tla_type(none)),capacity))),less(info(124,tla_type(none)),card(info(125,tla_type(none)),identifier(info(126,tla_type(none)),member)),identifier(info(127,tla_type(none)),capacity))),assign(info(128,tla_type(none)),[identifier(info(129,tla_type(none)),member),identifier(info(130,tla_type(none)),waiting)],[union(info(131,tla_type(none)),identifier(info(132,tla_type(none)),member),set_extension(info(133,tla_type(none)),[identifier(info(134,tla_type(none)),nn)])),minus_or_set_subtract(info(135,tla_type(none)),identifier(info(136,tla_type(none)),waiting),set_extension(info(137,tla_type(none)),[identifier(info(138,tla_type(none)),nn)]))]),[])),operation(info(139,tla_type(none)),identifier(info(139,tla_type(none)),remove),[],[identifier(info(140,tla_type(none)),nn)],any(info(141,tla_type(none)),[identifier(info(142,tla_type(none)),waiting_n)],conjunct(info(143,tla_type(none)),conjunct(info(144,tla_type(none)),conjunct(info(145,tla_type(none)),member(info(146,tla_type(none)),identifier(info(147,tla_type(none)),nn),identifier(info(148,tla_type(none)),'NAME')),member(info(149,tla_type(none)),identifier(info(150,tla_type(none)),nn),identifier(info(151,tla_type(none)),member))),member(info(152,tla_type(none)),identifier(info(153,tla_type(none)),waiting_n),pow_subset(info(154,tla_type(none)),identifier(info(155,tla_type(none)),'ENUM1')))),equal(info(156,tla_type(none)),identifier(info(157,tla_type(none)),waiting_n),identifier(info(158,tla_type(none)),waiting))),assign(info(159,tla_type(none)),[identifier(info(160,tla_type(none)),member),identifier(info(161,tla_type(none)),waiting)],[minus_or_set_subtract(info(162,tla_type(none)),identifier(info(163,tla_type(none)),member),set_extension(info(164,tla_type(none)),[identifier(info(165,tla_type(none)),nn)])),identifier(info(166,tla_type(none)),waiting_n)])))])])).
+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)])]),abstract_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)])))])])).