diff --git a/src/main/java/de/tla2b/analysis/PredicateVsExpression.java b/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
new file mode 100644
index 0000000000000000000000000000000000000000..a66c5774fe30f5f346496eb2ef2840fbc2882630
--- /dev/null
+++ b/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
@@ -0,0 +1,122 @@
+package de.tla2b.analysis;
+
+import java.util.HashMap;
+
+import de.tla2b.global.BBuildIns;
+import de.tla2b.global.BBuiltInOPs;
+import de.tla2b.global.TranslationGlobals;
+import tla2sany.semantic.ASTConstants;
+import tla2sany.semantic.LetInNode;
+import tla2sany.semantic.ModuleNode;
+import tla2sany.semantic.OpApplNode;
+import tla2sany.semantic.OpDefNode;
+import tla2sany.semantic.SemanticNode;
+import tlc2.tool.BuiltInOPs;
+
+public class PredicateVsExpression extends BuiltInOPs implements ASTConstants,
+ BBuildIns, TranslationGlobals {
+
+ private final HashMap<OpDefNode, DefinitionType> definitionsTypeMap;
+
+ public enum DefinitionType {
+ PREDICATE, EXPRESSION
+ }
+
+ public DefinitionType getDefinitionType(OpDefNode def) {
+ return definitionsTypeMap.get(def);
+ }
+
+ public PredicateVsExpression(ModuleNode moduleNode) {
+ this.definitionsTypeMap = new HashMap<OpDefNode, PredicateVsExpression.DefinitionType>();
+ OpDefNode[] defs = moduleNode.getOpDefs();
+
+ for (int i = 0; i < defs.length; i++) {
+ OpDefNode def = defs[i];
+ DefinitionType type = visitSemanticNode(defs[i].getBody());
+ definitionsTypeMap.put(def, type);
+ }
+
+ }
+
+ private DefinitionType visitSemanticNode(SemanticNode s) {
+ switch (s.getKind()) {
+ case OpApplKind: {
+ return visitOppApplNode((OpApplNode) s);
+ }
+
+ case LetInKind: {
+ LetInNode letInNode = (LetInNode) s;
+ return visitSemanticNode(letInNode.getBody());
+ }
+
+ }
+
+ return DefinitionType.EXPRESSION;
+ }
+
+ private DefinitionType visitOppApplNode(OpApplNode s) {
+ OpApplNode opApplNode = (OpApplNode) s;
+ int kind = opApplNode.getOperator().getKind();
+
+ if (kind == BuiltInKind) {
+ switch (getOpCode(opApplNode.getOperator().getName())) {
+ case OPCODE_eq: // =
+ case OPCODE_noteq: // /=
+ case OPCODE_cl: // $ConjList
+ case OPCODE_land: // \land
+ case OPCODE_dl: // $DisjList
+ case OPCODE_lor: // \/
+ case OPCODE_equiv: // \equiv
+ case OPCODE_implies: // =>
+ case OPCODE_lnot: // \lnot
+ case OPCODE_be: // \E x \in S : P
+ case OPCODE_bf: // \A x \in S : P
+ case OPCODE_in: // \in
+ case OPCODE_subseteq: // \subseteq {1,2} <: {1,2,3}
+ case OPCODE_unchanged: {
+ return DefinitionType.PREDICATE;
+ }
+
+ case OPCODE_ite: // IF THEN ELSE
+ {
+ return visitSemanticNode(opApplNode.getArgs()[1]);
+ }
+
+ case OPCODE_case: // CASE p1 -> e1 [] p2 -> e2
+ {
+ OpApplNode pair = (OpApplNode) opApplNode.getArgs()[0];
+ return visitSemanticNode(pair.getArgs()[1]);
+ }
+
+ default: {
+ return DefinitionType.EXPRESSION;
+ }
+ }
+ } else if (kind == UserDefinedOpKind) {
+ return visitUserdefinedOp(s);
+ }
+ return DefinitionType.EXPRESSION;
+ }
+
+ private DefinitionType visitUserdefinedOp(OpApplNode s) {
+ OpDefNode def = (OpDefNode) s.getOperator();
+ if (BBuiltInOPs.contains(def.getName())
+ && STANDARD_MODULES.contains(def.getSource()
+ .getOriginallyDefinedInModuleNode().getName()
+ .toString())) {
+
+ switch (BBuiltInOPs.getOpcode(def.getName())) {
+ case B_OPCODE_lt: // <
+ case B_OPCODE_gt: // >
+ case B_OPCODE_leq: // <=
+ case B_OPCODE_geq: // >=
+ case B_OPCODE_finite:
+ return DefinitionType.PREDICATE;
+ default:
+ return DefinitionType.EXPRESSION;
+ }
+
+ }
+ return getDefinitionType(def);
+ }
+}
diff --git a/src/main/java/de/tla2b/analysis/RecursiveDefinition.java b/src/main/java/de/tla2b/analysis/RecursiveDefinition.java
new file mode 100644
index 0000000000000000000000000000000000000000..09b5d7a270664808036d270024beb186bc8bf68e
--- /dev/null
+++ b/src/main/java/de/tla2b/analysis/RecursiveDefinition.java
@@ -0,0 +1,42 @@
+package de.tla2b.analysis;
+
+import tla2sany.semantic.OpApplNode;
+import tla2sany.semantic.OpDefNode;
+import tlc2.tool.BuiltInOPs;
+import de.tla2b.exceptions.NotImplementedException;
+
+public class RecursiveDefinition extends BuiltInOPs{
+
+ private OpDefNode def;
+ private OpApplNode ifThenElse;
+
+ public RecursiveDefinition(OpDefNode def) throws NotImplementedException{
+ this.def = def;
+ evalRecursiveDefinition();
+ }
+
+ private void evalRecursiveDefinition() throws NotImplementedException {
+ if (def.getBody() instanceof OpApplNode) {
+ OpApplNode o = (OpApplNode) def.getBody();
+ switch (getOpCode(o.getOperator().getName())) {
+ case OPCODE_ite: { // IF THEN ELSE
+ ifThenElse = o;
+ return;
+ }
+ }
+ throw new NotImplementedException(
+ "Only IF/THEN/ELSE or CASE constructs are supported at the body of a recursive function.");
+ } else {
+ throw new NotImplementedException(
+ "Only IF/THEN/ELSE or CASE constructs are supported at the body of a recursive function.");
+ }
+ }
+
+ public OpDefNode getOpDefNode() {
+ return def;
+ }
+
+ public OpApplNode getIfThenElse() {
+ return ifThenElse;
+ }
+}
diff --git a/src/main/java/de/tla2b/analysis/RecursiveFunktion.java b/src/main/java/de/tla2b/analysis/RecursiveFunktion.java
index cfae0ae2d934da527e6a165463f70628fcc6cc6f..42975537d586c6924418028496a012068cf74115 100644
--- a/src/main/java/de/tla2b/analysis/RecursiveFunktion.java
+++ b/src/main/java/de/tla2b/analysis/RecursiveFunktion.java
@@ -10,30 +10,31 @@ import tla2sany.semantic.OpApplNode;
import tla2sany.semantic.OpDefNode;
import tlc2.tool.BuiltInOPs;
-public class RecursiveFunktion extends BuiltInOPs{
+public class RecursiveFunktion extends BuiltInOPs {
private OpDefNode def;
private OpApplNode rfs;
private OpApplNode ifThenElse;
- public RecursiveFunktion(OpDefNode n, OpApplNode rfs) throws NotImplementedException {
+ public RecursiveFunktion(OpDefNode n, OpApplNode rfs)
+ throws NotImplementedException {
def = n;
this.rfs = rfs;
evalDef();
}
+
/**
* @throws NotImplementedException
*
*/
private void evalDef() throws NotImplementedException {
ExprOrOpArgNode e = rfs.getArgs()[0];
-
+ System.out.println(rfs.toString(5));
if (e instanceof OpApplNode) {
OpApplNode o = (OpApplNode) e;
- switch (getOpCode(o.getOperator().getName()))
- {
- case OPCODE_ite:{ // IF THEN ELSE
+ switch (getOpCode(o.getOperator().getName())) {
+ case OPCODE_ite: { // IF THEN ELSE
ifThenElse = o;
return;
}
@@ -45,16 +46,16 @@ public class RecursiveFunktion extends BuiltInOPs{
"Only IF/THEN/ELSE or CASE constructs are supported at the body of a recursive function.");
}
}
-
- public OpDefNode getOpDefNode(){
+
+ public OpDefNode getOpDefNode() {
return def;
}
-
- public OpApplNode getRF(){
+
+ public OpApplNode getRF() {
return rfs;
}
-
- public OpApplNode getIfThenElse(){
+
+ public OpApplNode getIfThenElse() {
return ifThenElse;
}
}
diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index 2b19348f581a46f4779f3b2f3697789c07185e61..7ca3fb7d4e7ce61f310cda29b0d99d256b7cdf59 100644
--- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java
+++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
@@ -20,9 +20,6 @@ import de.tla2b.global.TranslationGlobals;
import de.tla2b.types.IType;
import de.tla2b.types.TLAType;
-
-
-
import tla2sany.semantic.ASTConstants;
import tla2sany.semantic.AssumeNode;
import tla2sany.semantic.ExprNode;
@@ -74,9 +71,11 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
private ArrayList<String> definitionMacros = new ArrayList<String>();
private ArrayList<RecursiveFunktion> recursiveFunctions = new ArrayList<RecursiveFunktion>();
-
+
+ private ArrayList<RecursiveDefinition> recursiveDefinitions = new ArrayList<RecursiveDefinition>();
+
private ConfigfileEvaluator conEval;
-
+
/**
* @param m
* @param conEval
@@ -368,23 +367,35 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
*/
private void findDefinitions() throws ConfigFileErrorException {
- if(conEval != null){
+ if (conEval != null) {
bDefinitionsSet.addAll(conEval.getConstantOverrideTable().values());
}
-
+
AssumeNode[] assumes = moduleNode.getAssumptions();
for (int i = 0; i < assumes.length; i++) {
- visitExprNode(assumes[i].getAssume(), null);
+ findDefintionInExprNode(assumes[i].getAssume(), null);
}
if (inits != null) {
for (int i = 0; i < inits.size(); i++) {
- visitExprNode(inits.get(i), null);
+ findDefintionInExprNode(inits.get(i), null);
}
}
+
if (bOperations != null) {
for (int i = 0; i < bOperations.size(); i++) {
- visitExprNode(bOperations.get(i).getNode(), null);
+ ExprNode node = bOperations.get(i).getNode();
+
+ if (node instanceof OpApplNode) {
+ OpApplNode opApplNode = (OpApplNode) node;
+ if (opApplNode.getOperator().getKind() == UserDefinedOpKind
+ && !BBuiltInOPs.contains(opApplNode.getOperator()
+ .getName())) {
+ OpDefNode def = (OpDefNode) opApplNode.getOperator();
+ node = def.getBody();
+ }
+ }
+ findDefintionInExprNode(node, null);
}
}
@@ -392,35 +403,41 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
for (int i = 0; i < invariants.size(); i++) {
OpDefNode def = invariants.get(i);
bDefinitionsSet.add(def);
- visitExprNode(def.getBody(), null);
+ findDefintionInExprNode(def.getBody(), null);
}
}
for (int i = 0; i < globalLets.size(); i++) {
LetInNode letInNode = globalLets.get(i);
for (int j = 0; j < letInNode.getLets().length; j++) {
- visitExprNode(letInNode.getLets()[j].getBody(), null);
+ findDefintionInExprNode(letInNode.getLets()[j].getBody(), null);
}
}
+ HashSet<OpDefNode> defSet = new HashSet<OpDefNode>(bDefinitionsSet);
+ for (OpDefNode def : defSet) {
+ findDefintionInExprNode(def.getBody(), null);
+ }
+
}
/**
* @param exprOrOpArgNode
*/
- private void visitExprOrOpArgNode(ExprOrOpArgNode n,
+ private void findDefintionInExprOrOpArgNode(ExprOrOpArgNode n,
FormalParamNode[] parameters) {
if (n instanceof ExprNode) {
- visitExprNode((ExprNode) n, parameters);
+ findDefintionInExprNode((ExprNode) n, parameters);
} else if (n instanceof OpArgNode) {
}
}
- private void visitExprNode(ExprNode node, FormalParamNode[] parameters) {
+ private void findDefintionInExprNode(ExprNode node,
+ FormalParamNode[] parameters) {
switch (node.getKind()) {
case OpApplKind: {
- visitOpApplNode((OpApplNode) node, parameters);
+ findDefinitionInOpApplNode((OpApplNode) node, parameters);
return;
}
case LetInKind: {
@@ -431,9 +448,9 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
if (parameters != null)
letParams.put(letDef, parameters);
- visitExprNode(letDef.getBody(), letDef.getParams());
+ findDefintionInExprNode(letDef.getBody(), letDef.getParams());
}
- visitExprNode(l.getBody(), parameters);
+ findDefintionInExprNode(l.getBody(), parameters);
return;
}
@@ -444,49 +461,53 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
* @param node
* @throws ConfigFileErrorException
*/
- private void visitOpApplNode(OpApplNode node, FormalParamNode[] parameters) {
+ private void findDefinitionInOpApplNode(OpApplNode node,
+ FormalParamNode[] parameters) {
switch (node.getOperator().getKind()) {
case ConstantDeclKind: {
for (int i = 0; i < node.getArgs().length; i++) {
- visitExprOrOpArgNode(node.getArgs()[i], parameters);
+ findDefintionInExprOrOpArgNode(node.getArgs()[i], parameters);
}
return;
}
case VariableDeclKind: {
for (int i = 0; i < node.getArgs().length; i++) {
- visitExprOrOpArgNode(node.getArgs()[i], parameters);
+ findDefintionInExprOrOpArgNode(node.getArgs()[i], parameters);
}
return;
}
case BuiltInKind: {
- visitBuiltInKind(node, parameters);
+ findDefinitionInBuiltInKind(node, parameters);
return;
}
case UserDefinedOpKind: {
OpDefNode def = (OpDefNode) node.getOperator();
- //TODO
- ModuleNode moduleNode = def.getSource().getOriginallyDefinedInModuleNode();
- if(moduleNode.getName().toString().equals("TLA2B")){
+ // TODO
+ ModuleNode moduleNode = def.getSource()
+ .getOriginallyDefinedInModuleNode();
+ if (moduleNode.getName().toString().equals("TLA2B")) {
return;
}
if (BBuiltInOPs.contains(def.getName())
&& STANDARD_MODULES.contains(def.getSource()
.getOriginallyDefinedInModuleNode().getName()
.toString())) {
-
+
for (int i = 0; i < node.getArgs().length; i++) {
- visitExprOrOpArgNode(node.getArgs()[i], parameters);
+ findDefintionInExprOrOpArgNode(node.getArgs()[i],
+ parameters);
}
return;
}
- bDefinitionsSet.add(def);
- visitExprNode(def.getBody(), def.getParams());
+ if (bDefinitionsSet.add(def)) {
+ findDefintionInExprNode(def.getBody(), def.getParams());
+ }
for (int i = 0; i < node.getArgs().length; i++) {
- visitExprOrOpArgNode(node.getArgs()[i], parameters);
+ findDefintionInExprOrOpArgNode(node.getArgs()[i], parameters);
}
return;
}
@@ -498,7 +519,8 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
/**
* @param node
*/
- private void visitBuiltInKind(OpApplNode node, FormalParamNode[] parameters) {
+ private void findDefinitionInBuiltInKind(OpApplNode node,
+ FormalParamNode[] parameters) {
switch (BuiltInOPs.getOpCode(node.getOperator().getName())) {
case OPCODE_be:
@@ -509,7 +531,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
case OPCODE_fc: {
ExprNode[] in = node.getBdedQuantBounds();
for (int i = 0; i < in.length; i++) {
- visitExprNode(in[i], parameters);
+ findDefintionInExprNode(in[i], parameters);
}
break;
}
@@ -532,7 +554,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
}
}
for (int i = 0; i < node.getArgs().length; i++) {
- visitExprOrOpArgNode(node.getArgs()[i], parameters);
+ findDefintionInExprOrOpArgNode(node.getArgs()[i], parameters);
}
}
@@ -541,8 +563,16 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
*
*/
private void evalRecursiveFunctions() throws NotImplementedException {
-
- for (OpDefNode def : bDefinitionsSet) {
+ Set<OpDefNode> set = new HashSet<OpDefNode>(bDefinitionsSet);
+ for (OpDefNode def : set) {
+ if (def.getInRecursive()) {
+ bDefinitionsSet.remove(def);
+ // System.out.println(def.toString(7));
+ RecursiveDefinition rd = new RecursiveDefinition(def);
+ recursiveDefinitions.add(rd);
+ } else
+
+ // System.out.println(def.toString(4));
if (def.getBody() instanceof OpApplNode) {
OpApplNode o = (OpApplNode) def.getBody();
switch (getOpCode(o.getOperator().getName())) {
@@ -605,4 +635,9 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
public ArrayList<RecursiveFunktion> getRecursiveFunctions() {
return recursiveFunctions;
}
+
+ public ArrayList<RecursiveDefinition> getRecursiveDefinitions(){
+ return recursiveDefinitions;
+ }
+
}
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index 08b9d0b670c0d66e7c54ac6e0935adfa364288a0..b468d57ba7ca3e6705c7eeaa1015522ee58c9339 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -468,7 +468,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
p.setToolObject(TEMP_TYPE_ID, pType);
}
- if (found.isUntyped() || untyped) {
+ if (found.isUntyped() || untyped|| def.getInRecursive() == false) {
// evaluate the body of the definition again
paramId = TEMP_TYPE_ID;
found = visitExprNode(def.getBody(), found);
@@ -1000,6 +1000,26 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
}
+ case OPCODE_uc:{
+ TLAType found = new Untyped();
+ FormalParamNode x = n.getUnbdedQuantSymbols()[0];
+ x.setToolObject(TYPE_ID, found);
+ if (found instanceof AbstractHasFollowers) {
+ ((AbstractHasFollowers) found).addFollower(x);
+ }
+ visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
+
+ found = (TLAType) x.getToolObject(TYPE_ID);
+ try {
+ found = found.unify(expected);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(String.format(
+ "Expected %s, found %s at 'CHOOSE',\n%s", expected,
+ found, n.getLocation()));
+ }
+ return found;
+ }
+
case OPCODE_bc: { // CHOOSE x \in S: P
if (n.isBdedQuantATuple()[0]) {
throw new TypeErrorException(
@@ -1026,7 +1046,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
return found;
}
-
+
case OPCODE_unchanged: {
return BoolType.getInstance().unify(expected);
}
diff --git a/src/main/java/de/tla2b/analysis/UsedExternalFunctions.java b/src/main/java/de/tla2b/analysis/UsedExternalFunctions.java
new file mode 100644
index 0000000000000000000000000000000000000000..c73b870bb6438b4cc2f2dfa43a3b00535188d8ee
--- /dev/null
+++ b/src/main/java/de/tla2b/analysis/UsedExternalFunctions.java
@@ -0,0 +1,97 @@
+package de.tla2b.analysis;
+
+import java.util.HashSet;
+import java.util.Hashtable;
+import java.util.Set;
+
+import tla2sany.semantic.ASTConstants;
+import tla2sany.semantic.AssumeNode;
+import tla2sany.semantic.ExprNode;
+import tla2sany.semantic.ExprOrOpArgNode;
+import tla2sany.semantic.LetInNode;
+import tla2sany.semantic.ModuleNode;
+import tla2sany.semantic.OpApplNode;
+import tla2sany.semantic.OpDefNode;
+import tla2sany.semantic.SemanticNode;
+import tlc2.tool.BuiltInOPs;
+
+public class UsedExternalFunctions extends BuiltInOPs implements ASTConstants {
+
+ public enum EXTERNAL_FUNCTIONS {
+ CHOOSE
+ }
+
+ private final Set<EXTERNAL_FUNCTIONS> usedExternalFunctions;
+
+ public Set<EXTERNAL_FUNCTIONS> getUsedExternalFunctions() {
+ return usedExternalFunctions;
+ }
+
+ public UsedExternalFunctions(ModuleNode moduleNode,
+ SpecAnalyser specAnalyser) {
+ usedExternalFunctions = new HashSet<UsedExternalFunctions.EXTERNAL_FUNCTIONS>();
+
+ AssumeNode[] assumes = moduleNode.getAssumptions();
+ for (int i = 0; i < assumes.length; i++) {
+ AssumeNode assume = assumes[i];
+ visitSemanticNode(assume.getAssume());
+ }
+
+ for (OpDefNode def : specAnalyser.getUsedDefinitions()) {
+ visitSemanticNode(def.getBody());
+ }
+
+ }
+
+ private void findExternalFunctions(Hashtable<Integer, SemanticNode> table) {
+ for (SemanticNode sNode : table.values()) {
+ if (sNode instanceof OpApplNode) {
+ OpApplNode opApplNode = (OpApplNode) sNode;
+ int kind = opApplNode.getOperator().getKind();
+ if (kind == BuiltInKind) {
+ switch (getOpCode(opApplNode.getOperator().getName())) {
+ case OPCODE_case: {
+ usedExternalFunctions.add(EXTERNAL_FUNCTIONS.CHOOSE);
+ }
+ case OPCODE_bc: {
+ usedExternalFunctions.add(EXTERNAL_FUNCTIONS.CHOOSE);
+ }
+ }
+
+ }
+ }
+ }
+ }
+
+ private void visitSemanticNode(SemanticNode s) {
+ if (s == null)
+ return;
+ if (s instanceof OpApplNode) {
+ OpApplNode opApplNode = (OpApplNode) s;
+ int kind = opApplNode.getOperator().getKind();
+ if (kind == BuiltInKind) {
+ switch (getOpCode(opApplNode.getOperator().getName())) {
+ case OPCODE_case:
+ case OPCODE_bc:
+ case OPCODE_uc: {
+ usedExternalFunctions.add(EXTERNAL_FUNCTIONS.CHOOSE);
+ break;
+ }
+ }
+
+ }
+ for (SemanticNode arg : opApplNode.getArgs()) {
+ visitSemanticNode(arg);
+ }
+
+ }
+
+ SemanticNode[] children = s.getChildren();
+ if (children != null) {
+ for (SemanticNode semanticNode : children) {
+ visitSemanticNode(semanticNode);
+ }
+ }
+ }
+
+}
diff --git a/src/main/java/de/tla2b/pprint/ASTPrettyPrinter.java b/src/main/java/de/tla2b/pprint/ASTPrettyPrinter.java
index 16c4ca33929995d6bca34c91d0d6e8c5566d4152..27f86b256370a5341313673e44d72444e0b235f3 100644
--- a/src/main/java/de/tla2b/pprint/ASTPrettyPrinter.java
+++ b/src/main/java/de/tla2b/pprint/ASTPrettyPrinter.java
@@ -11,6 +11,7 @@ import de.be4.classicalb.core.parser.node.AAnySubstitution;
import de.be4.classicalb.core.parser.node.ABecomesSuchSubstitution;
import de.be4.classicalb.core.parser.node.ADefinitionExpression;
import de.be4.classicalb.core.parser.node.ADefinitionPredicate;
+import de.be4.classicalb.core.parser.node.AEmptySequenceExpression;
import de.be4.classicalb.core.parser.node.AExpressionDefinitionDefinition;
import de.be4.classicalb.core.parser.node.ALambdaExpression;
import de.be4.classicalb.core.parser.node.AOperation;
@@ -178,6 +179,7 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
putPreEnd("ACardExpression", "card(", ")");
putPreEnd("AFirstExpression", "first(", ")");
putPreEnd("ATailExpression", "tail(", ")");
+ putPreEnd("AEmptySequenceExpression", "[", "]");
put("ASetExtensionExpression", null, "{", ", ", "}", null, null);
put("AStructExpression", "struct", "(", ", ", ")", null, null);
diff --git a/src/main/java/de/tla2b/pprint/AbstractExpressionPrinter.java b/src/main/java/de/tla2b/pprint/AbstractExpressionPrinter.java
index c00c494b16388995f1a71fb5c6517f4bc5be71fa..1504c6b1edc25e18e87d5e14c82eac64d38465b9 100644
--- a/src/main/java/de/tla2b/pprint/AbstractExpressionPrinter.java
+++ b/src/main/java/de/tla2b/pprint/AbstractExpressionPrinter.java
@@ -781,6 +781,18 @@ public abstract class AbstractExpressionPrinter extends BuiltInOPs implements
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];
diff --git a/src/main/java/de/tla2b/types/EnumType.java b/src/main/java/de/tla2b/types/EnumType.java
index c75dc52fbeee1a7e67629892edf3ef41c78538a1..3cbe1fb2fc1230ea959a09c1543e9cfd462ca84b 100644
--- a/src/main/java/de/tla2b/types/EnumType.java
+++ b/src/main/java/de/tla2b/types/EnumType.java
@@ -9,7 +9,7 @@ import java.util.LinkedHashSet;
import de.be4.classicalb.core.parser.node.PExpression;
import de.tla2b.exceptions.UnificationException;
-import de.tla2b.pprint.BAstCreator;
+import de.tla2bAst.BAstCreator;
diff --git a/src/main/java/de/tla2b/types/StructType.java b/src/main/java/de/tla2b/types/StructType.java
index 34e52e01bfe27a9e01a97b8ad23aaf16d5f1841d..96e6cbefb3017c714c47382d5a1c4ebceb21e610 100644
--- a/src/main/java/de/tla2b/types/StructType.java
+++ b/src/main/java/de/tla2b/types/StructType.java
@@ -12,7 +12,7 @@ import de.be4.classicalb.core.parser.node.AStructExpression;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.PRecEntry;
import de.tla2b.exceptions.UnificationException;
-import de.tla2b.pprint.BAstCreator;
+import de.tla2bAst.BAstCreator;
diff --git a/src/main/java/de/tla2b/pprint/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
similarity index 76%
rename from src/main/java/de/tla2b/pprint/BAstCreator.java
rename to src/main/java/de/tla2bAst/BAstCreator.java
index ce21166589c99f54267724e9d22a2b16c81344a7..5197cbb1fd4bd66d02468933d7776baacb716da0 100644
--- a/src/main/java/de/tla2b/pprint/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -1,12 +1,14 @@
-package de.tla2b.pprint;
+package de.tla2bAst;
import java.util.ArrayList;
import java.util.Arrays;
+import java.util.HashSet;
import java.util.Hashtable;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
import java.util.Map.Entry;
+import java.util.Set;
import tla2sany.semantic.ASTConstants;
import tla2sany.semantic.AssumeNode;
@@ -14,6 +16,7 @@ import tla2sany.semantic.AtNode;
import tla2sany.semantic.ExprNode;
import tla2sany.semantic.ExprOrOpArgNode;
import tla2sany.semantic.FormalParamNode;
+import tla2sany.semantic.LetInNode;
import tla2sany.semantic.ModuleNode;
import tla2sany.semantic.NumeralNode;
import tla2sany.semantic.OpApplNode;
@@ -22,6 +25,8 @@ import tla2sany.semantic.OpDefNode;
import tla2sany.semantic.StringNode;
import tlc2.tool.BuiltInOPs;
import tlc2.value.SetEnumValue;
+import tlc2.value.Value;
+import tlc2.value.ValueConstants;
import de.be4.classicalb.core.parser.Definitions;
import de.be4.classicalb.core.parser.node.AAbstractConstantsMachineClause;
import de.be4.classicalb.core.parser.node.AAbstractMachineParseUnit;
@@ -44,6 +49,7 @@ import de.be4.classicalb.core.parser.node.ADefinitionsMachineClause;
import de.be4.classicalb.core.parser.node.ADisjunctPredicate;
import de.be4.classicalb.core.parser.node.ADivExpression;
import de.be4.classicalb.core.parser.node.ADomainExpression;
+import de.be4.classicalb.core.parser.node.AEmptySequenceExpression;
import de.be4.classicalb.core.parser.node.AEmptySetExpression;
import de.be4.classicalb.core.parser.node.AEnumeratedSetSet;
import de.be4.classicalb.core.parser.node.AEqualPredicate;
@@ -118,14 +124,18 @@ import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
import de.be4.classicalb.core.parser.node.TIntegerLiteral;
import de.be4.classicalb.core.parser.node.TStringLiteral;
import de.tla2b.analysis.BOperation;
+import de.tla2b.analysis.PredicateVsExpression;
+import de.tla2b.analysis.RecursiveDefinition;
import de.tla2b.analysis.SpecAnalyser;
+import de.tla2b.analysis.UsedExternalFunctions;
+import de.tla2b.analysis.PredicateVsExpression.DefinitionType;
+import de.tla2b.analysis.UsedExternalFunctions.EXTERNAL_FUNCTIONS;
import de.tla2b.config.ConfigfileEvaluator;
import de.tla2b.config.ValueObj;
import de.tla2b.global.BBuildIns;
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.Priorities;
import de.tla2b.global.TranslationGlobals;
-import de.tla2b.types.BoolType;
import de.tla2b.types.EnumType;
import de.tla2b.types.FunctionType;
import de.tla2b.types.IType;
@@ -135,15 +145,21 @@ import de.tla2b.types.TLAType;
import de.tla2b.types.TupleType;
public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
- ASTConstants, IType, BBuildIns, Priorities {
+ ASTConstants, IType, BBuildIns, Priorities, ValueConstants {
Start start;
List<PMachineClause> machineClauseList;
ConfigfileEvaluator conEval;
SpecAnalyser specAnalyser;
+ private final PredicateVsExpression predicateVsExpression;
+ final int SUBSTITUTE_PARAM = 29;
+
+ final HashSet<OpDefNode> allTLADefinitions;
List<OpDeclNode> bConstants;
private ModuleNode moduleNode;
+ private final UsedExternalFunctions usedExternalFunctions;
+
private Definitions bDefinitions = new Definitions();
public Start getStartNode() {
@@ -156,10 +172,16 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
public BAstCreator(ModuleNode moduleNode, ConfigfileEvaluator conEval,
- SpecAnalyser specAnalyser) {
+ SpecAnalyser specAnalyser,
+ UsedExternalFunctions usedExternalFunctions,
+ PredicateVsExpression predicateVsExpression) {
+ this.predicateVsExpression = predicateVsExpression;
this.conEval = conEval;
this.moduleNode = moduleNode;
this.specAnalyser = specAnalyser;
+ this.usedExternalFunctions = usedExternalFunctions;
+ this.allTLADefinitions = new HashSet<OpDefNode>(
+ Arrays.asList(moduleNode.getOpDefs()));
if (conEval != null) {
this.bConstants = conEval.getbConstantList();
@@ -249,24 +271,31 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
}
+ Set<EXTERNAL_FUNCTIONS> set = usedExternalFunctions
+ .getUsedExternalFunctions();
- if (bDefs.size() == 0) {
+ if (bDefs.size() == 0 && set.size() == 0) {
return;
}
ADefinitionsMachineClause defClause = new ADefinitionsMachineClause();
List<PDefinition> defs = new ArrayList<PDefinition>();
+
+ defs.addAll(createDefinitionsForExternalFunctions(set));
+
for (OpDefNode opDefNode : bDefs) {
- TLAType type = (TLAType) opDefNode.getToolObject(TYPE_ID);
- if (opDefNode.level == 2 || type instanceof BoolType) {
+ List<PExpression> list = new ArrayList<PExpression>();
+ for (int i = 0; i < opDefNode.getParams().length; i++) {
+ FormalParamNode p = opDefNode.getParams()[i];
+ list.add(createIdentifierNode(p.getName().toString()));
+ }
+
+ // TLAType type = (TLAType) opDefNode.getToolObject(TYPE_ID);
+ // if (opDefNode.level == 2 || type instanceof BoolType) {
+ if (predicateVsExpression.getDefinitionType(opDefNode) == DefinitionType.PREDICATE) {
APredicateDefinitionDefinition d = new APredicateDefinitionDefinition();
d.setName(new TDefLiteralPredicate(opDefNode.getName()
- .toString() + "_def"));
- List<PExpression> list = new ArrayList<PExpression>();
- for (int i = 0; i < opDefNode.getParams().length; i++) {
- FormalParamNode p = opDefNode.getParams()[i];
- list.add(createIdentifierNode(p.getName().toString()));
- }
+ .toString()));
d.setParameters(list);
d.setRhs(visitExprNodePredicate(opDefNode.getBody()));
defs.add(d);
@@ -274,11 +303,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
} else {
AExpressionDefinitionDefinition d = new AExpressionDefinitionDefinition();
d.setName(new TIdentifierLiteral(opDefNode.getName().toString()));
- List<PExpression> list = new ArrayList<PExpression>();
- for (int i = 0; i < opDefNode.getParams().length; i++) {
- FormalParamNode p = opDefNode.getParams()[i];
- list.add(createIdentifierNode(p.getName().toString()));
- }
+
d.setParameters(list);
d.setRhs(visitExprNodeExpression(opDefNode.getBody()));
defs.add(d);
@@ -290,6 +315,29 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
machineClauseList.add(defClause);
}
+ private ArrayList<PDefinition> createDefinitionsForExternalFunctions(
+ Set<EXTERNAL_FUNCTIONS> set) {
+ ArrayList<PDefinition> list = new ArrayList<PDefinition>();
+
+ if (set.contains(UsedExternalFunctions.EXTERNAL_FUNCTIONS.CHOOSE)) {
+ AExpressionDefinitionDefinition def1 = new AExpressionDefinitionDefinition();
+ def1.setName(new TIdentifierLiteral("CHOOSE"));
+ def1.setParameters(createIdentifierList("X"));
+ def1.setRhs(new AStringExpression(new TStringLiteral(
+ "a member of X")));
+ list.add(def1);
+ AExpressionDefinitionDefinition def2 = new AExpressionDefinitionDefinition();
+ def2.setName(new TIdentifierLiteral("EXTERNAL_FUNCTION_CHOOSE"));
+ def2.setParameters(createIdentifierList("T"));
+ ATotalFunctionExpression total = new ATotalFunctionExpression();
+ total.setLeft(new APowSubsetExpression(createIdentifierNode("T")));
+ total.setRight(createIdentifierNode("T"));
+ def2.setRhs(total);
+ list.add(def2);
+ }
+ return list;
+ }
+
private void createOperationsClause() {
ArrayList<BOperation> bOperations = specAnalyser.getBOperations();
if (bOperations == null || bOperations.size() == 0) {
@@ -309,7 +357,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
OpApplNode o = op.getExistQuans().get(j);
whereList.add(visitBounded(o));
}
-
+
AOperation operation = new AOperation();
operation.setOpName(createTIdentifierLiteral(defName));
operation.setParameters(paramList);
@@ -333,7 +381,27 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
any.setIdentifiers(anyParams);
- whereList.add(visitExprOrOpArgNodePredicate(op.getNode()));
+ PPredicate body = null;
+ if (op.getNode() instanceof OpApplNode) {
+ OpApplNode opApplNode = (OpApplNode) op.getNode();
+ if (opApplNode.getOperator().getKind() == UserDefinedOpKind
+ && !BBuiltInOPs.contains(opApplNode.getOperator()
+ .getName())) {
+ OpDefNode def = (OpDefNode) opApplNode.getOperator();
+ System.out.println(def.getName());
+ FormalParamNode[] params = def.getParams();
+ for (int j = 0; j < params.length; j++) {
+ FormalParamNode param = params[j];
+ param.setToolObject(SUBSTITUTE_PARAM,
+ opApplNode.getArgs()[j]);
+ }
+ body = visitExprNodePredicate(def.getBody());
+ }
+ }
+ if (body == null) {
+ body = visitExprOrOpArgNodePredicate(op.getNode());
+ }
+ whereList.add(body);
any.setWhere(createConjunction(whereList));
List<PExpression> varList = new ArrayList<PExpression>();
@@ -403,22 +471,71 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
bConstants = Arrays.asList(moduleNode.getConstantDecls());
}
- if (bConstants.size() > 0) {
- List<PExpression> list = new ArrayList<PExpression>();
- for (OpDeclNode opDeclNode : bConstants) {
- AIdentifierExpression id = new AIdentifierExpression(
- createTIdentifierLiteral(opDeclNode.getName()
- .toString()));
- list.add(id);
- }
+ List<PExpression> constantsList = new ArrayList<PExpression>();
+ for (OpDeclNode opDeclNode : bConstants) {
+ AIdentifierExpression id = new AIdentifierExpression(
+ createTIdentifierLiteral(opDeclNode.getName().toString()));
+ constantsList.add(id);
+ }
+
+ for (RecursiveDefinition recDef : specAnalyser
+ .getRecursiveDefinitions()) {
+
+ AIdentifierExpression id = new AIdentifierExpression(
+ createTIdentifierLiteral(recDef.getOpDefNode().getName()
+ .toString()));
+ constantsList.add(id);
+ }
+
+ if (constantsList.size() > 0) {
AAbstractConstantsMachineClause abstractConstantsClause = new AAbstractConstantsMachineClause(
- list);
+ constantsList);
machineClauseList.add(abstractConstantsClause);
}
+
}
private void createPropertyClause() {
- List<PPredicate> list = new ArrayList<PPredicate>();
+ List<PPredicate> propertiesList = new ArrayList<PPredicate>();
+
+ for (RecursiveDefinition recDef : specAnalyser
+ .getRecursiveDefinitions()) {
+ OpDefNode def = recDef.getOpDefNode();
+ TLAType t = (TLAType) def.getToolObject(TYPE_ID);
+ // OpApplNode ifThenElse = recDef.getIfThenElse();
+ FormalParamNode[] params = def.getParams();
+ ArrayList<PExpression> paramList1 = new ArrayList<PExpression>();
+ ArrayList<PPredicate> typeList = new ArrayList<PPredicate>();
+ // ArrayList<PExpression> paramList2 = new ArrayList<PExpression>();
+ for (FormalParamNode p : params) {
+ paramList1.add(createIdentifierNode(p.getName().toString()));
+ // paramList2.add(createIdentifierNode(p.getName().toString()));
+ TLAType paramType = (TLAType) p.getToolObject(TYPE_ID);
+ System.out.println(paramType);
+ AEqualPredicate equal = new AEqualPredicate(
+ createIdentifierNode(p.getName().toString()),
+ paramType.getBNode());
+ typeList.add(equal);
+ }
+ ALambdaExpression lambda1 = new ALambdaExpression();
+ lambda1.setIdentifiers(paramList1);
+ lambda1.setPredicate(createConjunction(typeList));
+ lambda1.setExpression(visitExprNodeExpression(def.getBody()));
+ // lambda1.setPredicate(visitExprOrOpArgNodePredicate(ifThenElse.getArgs()[0]));
+ // lambda1.setExpression(visitExprOrOpArgNodeExpression(ifThenElse.getArgs()[1]));
+
+ // ALambdaExpression lambda2 = new ALambdaExpression();
+ // lambda2.setIdentifiers(paramList2);
+ // ANegationPredicate not = new
+ // ANegationPredicate(visitExprOrOpArgNodePredicate(ifThenElse.getArgs()[0]));
+ // lambda2.setPredicate(not);
+ // lambda2.setExpression(visitExprOrOpArgNodeExpression(ifThenElse.getArgs()[2]));
+ // AUnionExpression union = new AUnionExpression(lambda1, lambda2);
+
+ AEqualPredicate equals = new AEqualPredicate(
+ createIdentifierNode(def.getName().toString()), lambda1);
+ propertiesList.add(equals);
+ }
for (OpDeclNode con : bConstants) {
if (conEval != null
@@ -442,19 +559,20 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
equal.setLeft(createIdentifierNode(con.getName().toString()));
equal.setRight(createIdentifierNode(((SetType) t)
.getSubType().toString()));
- list.add(equal);
+ propertiesList.add(equal);
} else {
AEqualPredicate equal = new AEqualPredicate();
equal.setLeft(createIdentifierNode(con.getName().toString()));
- equal.setRight(createIdentifierNode(v.getValue().toString()));
- list.add(equal);
+ Value tlcValue = v.getValue();
+ equal.setRight(createTLCValue(tlcValue));
+ propertiesList.add(equal);
}
} else {
AMemberPredicate member = new AMemberPredicate();
member.setLeft(createIdentifierNode(con.getName().toString()));
TLAType t = (TLAType) con.getToolObject(TYPE_ID);
member.setRight(t.getBNode());
- list.add(member);
+ propertiesList.add(member);
}
}
@@ -464,27 +582,49 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
while (iter.hasNext()) {
Entry<OpDeclNode, OpDefNode> entry = iter.next();
OpDeclNode con = entry.getKey();
- OpDefNode def = entry.getValue();
+ OpDefNode generatedDef = entry.getValue();
+ OpDefNode def = null;
+ try {
+ OpApplNode opApplNode = (OpApplNode) generatedDef.getBody();
+ if (opApplNode.getKind() == UserDefinedOpKind) {
+ def = (OpDefNode) opApplNode.getOperator();
+ } else {
+ def = generatedDef;
+ }
+ } catch (ClassCastException e) {
+ def = generatedDef;
+ }
AEqualPredicate equal = new AEqualPredicate();
equal.setLeft(createIdentifierNode(con.getName().toString()));
equal.setRight(visitExprNodeExpression(def.getBody()));
- list.add(equal);
+ propertiesList.add(equal);
}
}
AssumeNode[] assumes = moduleNode.getAssumptions();
for (AssumeNode assumeNode : assumes) {
- list.add(visitAssumeNode(assumeNode));
+ propertiesList.add(visitAssumeNode(assumeNode));
}
- if (list.size() == 0)
- return;
+ if (propertiesList.size() > 0) {
+ APropertiesMachineClause propertiesClause = new APropertiesMachineClause();
+ propertiesClause.setPredicates(createConjunction(propertiesList));
+
+ machineClauseList.add(propertiesClause);
+ }
+ }
- APropertiesMachineClause propertiesClause = new APropertiesMachineClause();
- propertiesClause.setPredicates(createConjunction(list));
+ private PExpression createTLCValue(Value tlcValue) {
+ switch (tlcValue.getKind()) {
+ case INTVALUE:
- machineClauseList.add(propertiesClause);
+ return new AIntegerExpression(new TIntegerLiteral(
+ tlcValue.toString()));
+
+ }
+
+ throw new RuntimeException();
}
private void createInvariantClause() {
@@ -507,7 +647,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
for (OpDefNode def : conEval.getInvariants()) {
ADefinitionPredicate defPred = new ADefinitionPredicate();
defPred.setDefLiteral(new TDefLiteralPredicate(def.getName()
- .toString() + "_def"));
+ .toString()));
predList.add(defPred);
}
}
@@ -526,11 +666,19 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
case OpApplKind:
return visitOpApplNodePredicate((OpApplNode) n);
+ case LetInKind: {
+ LetInNode letInNode = (LetInNode) n;
+ return visitExprNodePredicate(letInNode.getBody());
+ }
+
case NumeralKind: {
+ throw new RuntimeException();
}
}
+ System.out.println(n);
+ System.out.println(n.getClass());
throw new RuntimeException();
}
@@ -551,30 +699,42 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
return new AStringExpression(new TStringLiteral(s.getRep()
.toString()));
}
-
+
case AtNodeKind: { // @
AtNode at = (AtNode) n;
TLAType type = (TLAType) at.getExceptRef().getToolObject(TYPE_ID);
- if(type instanceof FunctionType){
-
- OpApplNode seq = at.getAtModifier();
- LinkedList<ExprOrOpArgNode> list = new LinkedList<ExprOrOpArgNode>();
- for (int j = 0; j < seq.getArgs().length; j++) {
- list.add(seq.getArgs()[j]);
- }
+ OpApplNode seq = at.getAtModifier();
+ LinkedList<ExprOrOpArgNode> list = new LinkedList<ExprOrOpArgNode>();
+ for (int j = 0; j < seq.getArgs().length; j++) {
+ list.add(seq.getArgs()[j]);
+ }
+ if (type instanceof FunctionType) {
+
List<PExpression> params = new ArrayList<PExpression>();
params.add(visitExprOrOpArgNodeExpression(list.get(0)));
-
+
AFunctionExpression funCall = new AFunctionExpression();
funCall.setIdentifier(visitExprNodeExpression(at.getAtBase()));
funCall.setParameters(params);
return funCall;
+ } else {
+ ARecordFieldExpression select = new ARecordFieldExpression();
+ select.setRecord(visitExprNodeExpression(at.getAtBase()));
+ StringNode stringNode = (StringNode) list.get(0);
+ select.setIdentifier(createIdentifierNode(stringNode.getRep()
+ .toString()));
+ return select;
}
- throw new RuntimeException();
}
+ case LetInKind: {
+ LetInNode letInNode = (LetInNode) n;
+ return visitExprNodeExpression(letInNode.getBody());
}
+ }
+
+ System.out.println(n.getClass());
throw new RuntimeException();
}
@@ -611,7 +771,16 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
case FormalParamKind: {
- return createIdentifierNode(n.getOperator().getName().toString());
+ FormalParamNode param = (FormalParamNode) n.getOperator();
+ ExprOrOpArgNode e = (ExprOrOpArgNode) param
+ .getToolObject(SUBSTITUTE_PARAM);
+ if (e == null) {
+ return createIdentifierNode(n.getOperator().getName()
+ .toString());
+ } else {
+ return visitExprOrOpArgNodeExpression(e);
+ }
+
}
case BuiltInKind:
@@ -628,23 +797,35 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
private PPredicate visitUserdefinedOpPredicate(OpApplNode n) {
OpDefNode def = (OpDefNode) n.getOperator();
- // Operator is a B built-in operator
- if (BBuiltInOPs.contains(def.getName())
+
+ if (BBuiltInOPs.contains(def.getName()) // Operator is a B built-in
+ // operator
&& STANDARD_MODULES.contains(def.getSource()
.getOriginallyDefinedInModuleNode().getName()
.toString())) {
return visitBBuitInsPredicate(n);
}
- ADefinitionPredicate defCall = new ADefinitionPredicate();
- defCall.setDefLiteral(new TDefLiteralPredicate(def.getName().toString()
- + "_def"));
- List<PExpression> list = new ArrayList<PExpression>();
+ List<PExpression> params = new ArrayList<PExpression>();
for (int i = 0; i < n.getArgs().length; i++) {
- list.add(visitExprOrOpArgNodeExpression(n.getArgs()[i]));
+ params.add(visitExprOrOpArgNodeExpression(n.getArgs()[i]));
+ }
+ if (predicateVsExpression.getDefinitionType(def) == DefinitionType.EXPRESSION) {
+ ADefinitionExpression defCall = new ADefinitionExpression();
+ defCall.setDefLiteral(new TIdentifierLiteral(def.getName()
+ .toString()));
+ ;
+ defCall.setParameters(params);
+ return new AEqualPredicate(defCall, new ABooleanTrueExpression());
+
+ } else {
+ ADefinitionPredicate defCall = new ADefinitionPredicate();
+ defCall.setDefLiteral(new TDefLiteralPredicate(def.getName()
+ .toString()));
+
+ defCall.setParameters(params);
+ return defCall;
}
- defCall.setParameters(list);
- return defCall;
}
private PExpression visitUserdefinedOpExpression(OpApplNode n) {
@@ -657,16 +838,50 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
return visitBBuitInsExpression(n);
}
- // new Definition or what else
- ADefinitionExpression defExpr = new ADefinitionExpression();
- defExpr.setDefLiteral(new TIdentifierLiteral(n.getOperator().getName()
- .toString()));
- List<PExpression> list = new ArrayList<PExpression>();
- for (int i = 0; i < n.getArgs().length; i++) {
- list.add(visitExprOrOpArgNodeExpression(n.getArgs()[i]));
+ if (allTLADefinitions.contains(def)) {
+ List<PExpression> params = new ArrayList<PExpression>();
+ for (int i = 0; i < n.getArgs().length; i++) {
+ params.add(visitExprOrOpArgNodeExpression(n.getArgs()[i]));
+ }
+
+ if (conEval != null
+ && conEval.getConstantOverrideTable().containsValue(def)) {
+ // used constants name instead of the definition overriding the
+ // constant
+ Iterator<Entry<OpDeclNode, OpDefNode>> iter = conEval
+ .getConstantOverrideTable().entrySet().iterator();
+ String name = null;
+ while (iter.hasNext()) {
+ Entry<OpDeclNode, OpDefNode> entry = iter.next();
+ if (entry.getValue().equals(def)) {
+ name = entry.getKey().getName().toString();
+ }
+ }
+ if (params.size() == 0) {
+ return createIdentifierNode(name);
+ } else {
+ AFunctionExpression funcCall = new AFunctionExpression();
+ funcCall.setIdentifier(createIdentifierNode(name));
+ funcCall.setParameters(params);
+ return funcCall;
+ }
+ } else {
+ ADefinitionExpression defExpr = new ADefinitionExpression();
+ defExpr.setDefLiteral(new TIdentifierLiteral(n.getOperator()
+ .getName().toString()));
+ defExpr.setParameters(params);
+ return defExpr;
+ }
+
+ } else {
+ FormalParamNode[] params = def.getParams();
+ for (int i = 0; i < params.length; i++) {
+ FormalParamNode param = params[i];
+ param.setToolObject(SUBSTITUTE_PARAM, n.getArgs()[i]);
+ }
+ PExpression result = visitExprNodeExpression(def.getBody());
+ return result;
}
- defExpr.setParameters(list);
- return defExpr;
}
@@ -1131,7 +1346,11 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
if (t instanceof TupleType) {
return new ACoupleExpression(list);
} else {
- return new ASequenceExtensionExpression(list);
+ if (list.size() == 0) {
+ return new AEmptySequenceExpression();
+ } else {
+ return new ASequenceExtensionExpression(list);
+ }
}
}
@@ -1246,12 +1465,45 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
return funCall;
}
+ case OPCODE_case: {
+ return createCaseNode(n);
+ }
+
case OPCODE_exc: // Except
{
TLAType type = (TLAType) n.getToolObject(TYPE_ID);
if (type.getKind() == STRUCT) {
- System.out.println(n.getOperator().getName());
- throw new RuntimeException();
+ Hashtable<String, PExpression> temp = new Hashtable<String, PExpression>();
+ for (int i = 1; i < n.getArgs().length; i++) {
+ OpApplNode pair = (OpApplNode) n.getArgs()[i];
+ ExprOrOpArgNode first = pair.getArgs()[0];
+ ExprOrOpArgNode second = pair.getArgs()[1];
+ OpApplNode seq = (OpApplNode) first;
+
+ PExpression val = visitExprOrOpArgNodeExpression(second);
+
+ StringNode stringNode = (StringNode) seq.getArgs()[0];
+ String fieldName = stringNode.getRep().toString();
+ temp.put(fieldName, val);
+ }
+
+ StructType st = (StructType) type;
+ List<PRecEntry> list = new ArrayList<PRecEntry>();
+ for (int i = 0; i < st.getFields().size(); i++) {
+ ARecEntry entry = new ARecEntry();
+ String fieldName = st.getFields().get(i);
+ entry.setIdentifier(createIdentifierNode(fieldName));
+ PExpression value = temp.get(fieldName);
+ if (value == null) {
+ value = new ARecordFieldExpression(
+ visitExprOrOpArgNodeExpression(n.getArgs()[0]),
+ createIdentifierNode(fieldName));
+ }
+ entry.setValue(value);
+ list.add(entry);
+ }
+ ARecExpression rec = new ARecExpression(list);
+ return rec;
} else {
FunctionType func = (FunctionType) type;
@@ -1284,12 +1536,89 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
return visitExprOrOpArgNodeExpression(n.getArgs()[0]);
}
+ case OPCODE_uc: { // CHOOSE x : P
+ return createUnboundedChoose(n);
+ }
+
+ case OPCODE_bc: { // CHOOSE x \in S: P
+ return createBoundedChoose(n);
+ }
+
}
System.out.println(n.getOperator().getName());
throw new RuntimeException();
}
+ private PExpression createUnboundedChoose(OpApplNode n) {
+ ADefinitionExpression defCall = new ADefinitionExpression();
+ defCall.setDefLiteral(new TIdentifierLiteral("CHOOSE"));
+ AComprehensionSetExpression comprehension = new AComprehensionSetExpression();
+ FormalParamNode x = n.getUnbdedQuantSymbols()[0];
+ comprehension.setIdentifiers(createIdentifierList(x.getName()
+ .toString()));
+ comprehension
+ .setPredicates(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
+ List<PExpression> list = new ArrayList<PExpression>();
+ list.add(comprehension);
+ defCall.setParameters(list);
+ return defCall;
+ }
+
+ private PExpression createBoundedChoose(OpApplNode n) {
+ ADefinitionExpression defCall = new ADefinitionExpression();
+ defCall.setDefLiteral(new TIdentifierLiteral("CHOOSE"));
+ AComprehensionSetExpression comprehension = new AComprehensionSetExpression();
+ FormalParamNode x = n.getBdedQuantSymbolLists()[0][0];
+ comprehension.setIdentifiers(createIdentifierList(x.getName()
+ .toString()));
+ AMemberPredicate member = new AMemberPredicate();
+ member.setLeft(createIdentifierNode(x.getName().toString()));
+ ExprNode in = n.getBdedQuantBounds()[0];
+ member.setRight(visitExprNodeExpression(in));
+ AConjunctPredicate conj = new AConjunctPredicate();
+ conj.setLeft(member);
+ conj.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
+ comprehension.setPredicates(conj);
+ List<PExpression> list = new ArrayList<PExpression>();
+ list.add(comprehension);
+ defCall.setParameters(list);
+ return defCall;
+ }
+
+ private PExpression createCaseNode(OpApplNode n) {
+ List<PPredicate> conditions = new ArrayList<PPredicate>();
+ List<PPredicate> disjunctionList = new ArrayList<PPredicate>();
+ for (int i = 0; i < n.getArgs().length; i++) {
+ OpApplNode pair = (OpApplNode) n.getArgs()[i];
+
+ AConjunctPredicate conj = new AConjunctPredicate();
+ if (pair.getArgs()[0] == null) {
+ ANegationPredicate neg = new ANegationPredicate();
+ neg.setPredicate(createDisjunction(conditions));
+ conj.setLeft(neg);
+ } else {
+ conditions
+ .add(visitExprOrOpArgNodePredicate(pair.getArgs()[0]));
+ conj.setLeft(visitExprOrOpArgNodePredicate(pair.getArgs()[0]));
+ }
+ AEqualPredicate equals = new AEqualPredicate();
+ equals.setLeft(createIdentifierNode("t_"));
+ equals.setRight(visitExprOrOpArgNodeExpression(pair.getArgs()[1]));
+ conj.setRight(equals);
+ disjunctionList.add(conj);
+ }
+ AComprehensionSetExpression comprehension = new AComprehensionSetExpression();
+ comprehension.setIdentifiers(createIdentifierList("t_"));
+ comprehension.setPredicates(createDisjunction(disjunctionList));
+ ADefinitionExpression defCall = new ADefinitionExpression();
+ defCall.setDefLiteral(new TIdentifierLiteral("CHOOSE"));
+ List<PExpression> params = new ArrayList<PExpression>();
+ params.add(comprehension);
+ defCall.setParameters(params);
+ return defCall;
+ }
+
private List<PExpression> createIdentifierList(String name) {
ArrayList<PExpression> list = new ArrayList<PExpression>();
list.add(createIdentifierNode(name));
@@ -1449,6 +1778,11 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
return new AEqualPredicate(rcdSelect, new ABooleanTrueExpression());
}
+ case OPCODE_case: {
+ return new AEqualPredicate(createCaseNode(n),
+ new ABooleanTrueExpression());
+ }
+
case OPCODE_prime: // prime
{
OpApplNode node = (OpApplNode) n.getArgs()[0];
@@ -1462,6 +1796,30 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
new ABooleanTrueExpression());
}
+ case OPCODE_uc: { // CHOOSE x : P
+ return new AEqualPredicate(createUnboundedChoose(n),
+ new ABooleanTrueExpression());
+ }
+
+ case OPCODE_bc: { // CHOOSE x \in S: P
+ return new AEqualPredicate(createBoundedChoose(n),
+ new ABooleanTrueExpression());
+ }
+
+ case OPCODE_ite: // IF THEN ELSE
+ {
+ AImplicationPredicate impl1 = new AImplicationPredicate();
+ impl1.setLeft(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
+ impl1.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[1]));
+
+ AImplicationPredicate impl2 = new AImplicationPredicate();
+ ANegationPredicate neg = new ANegationPredicate(
+ visitExprOrOpArgNodePredicate(n.getArgs()[0]));
+ impl2.setLeft(neg);
+ impl2.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[2]));
+ return new AConjunctPredicate(impl1, impl2);
+ }
+
case 0:
return visitBBuitInsPredicate(n);
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index 38bff13b6a669ad59ce6e5151fdafd8907c3d28c..1ffbcc86cbe02883960b83e5729a2ea324099289 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -7,15 +7,16 @@ import java.io.IOException;
import de.be4.classicalb.core.parser.Definitions;
import de.be4.classicalb.core.parser.node.Start;
import de.tla2b.analysis.InstanceTransformation;
+import de.tla2b.analysis.PredicateVsExpression;
import de.tla2b.analysis.SpecAnalyser;
import de.tla2b.analysis.SymbolRenamer;
import de.tla2b.analysis.SymbolSorter;
import de.tla2b.analysis.TypeChecker;
+import de.tla2b.analysis.UsedExternalFunctions;
import de.tla2b.config.ConfigfileEvaluator;
import de.tla2b.config.ModuleOverrider;
import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
-import de.tla2b.pprint.BAstCreator;
import de.tla2b.pprint.BMachinePrinter;
import tla2sany.semantic.ModuleNode;
import tlc2.tool.ModelConfig;
@@ -25,25 +26,26 @@ import util.ToolIO;
public class Translator {
private String moduleFileName;
private String configFileName;
-
+
private Definitions bDefinitions;
-
+
private String moduleName;
private ModuleNode moduleNode;
private ModelConfig modelConfig;
private String bMachineString;
-
- public Translator(String moduleFileName, String configFileName) throws FrontEndException {
+
+ public Translator(String moduleFileName, String configFileName)
+ throws FrontEndException {
this.moduleFileName = moduleFileName;
- this.configFileName = configFileName;
-
+ this.configFileName = configFileName;
+
parse();
}
-
-
- //Used for Testing
- public Translator(String moduleString, String configString, int i) throws FrontEndException {
+
+ // Used for Testing
+ public Translator(String moduleString, String configString, int i)
+ throws FrontEndException {
moduleName = "Testing";
File dir = new File("temp/");
dir.mkdirs();
@@ -54,7 +56,7 @@ public class Translator {
FileWriter fw = new FileWriter(f);
fw.write(moduleString);
fw.close();
- //f.deleteOnExit();
+ // f.deleteOnExit();
moduleFileName = f.getAbsolutePath();
} catch (IOException e) {
e.printStackTrace();
@@ -63,7 +65,7 @@ public class Translator {
modelConfig = null;
if (configString != null) {
File f = new File("temp/" + moduleName + ".cfg");
-
+
try {
f.createNewFile();
FileWriter fw = new FileWriter(f);
@@ -72,15 +74,15 @@ public class Translator {
} catch (IOException e) {
e.printStackTrace();
}
- //f.deleteOnExit();
+ // f.deleteOnExit();
configFileName = f.getAbsolutePath();
}
dir.deleteOnExit();
-
+
parse();
}
-
- //Used for Testing
+
+ // Used for Testing
public Translator(String moduleString) throws FrontEndException {
moduleName = "Testing";
File dir = new File("temp/");
@@ -92,7 +94,7 @@ public class Translator {
FileWriter fw = new FileWriter(f);
fw.write(moduleString);
fw.close();
- //f.deleteOnExit();
+ // f.deleteOnExit();
moduleFileName = f.getAbsolutePath();
} catch (IOException e) {
e.printStackTrace();
@@ -100,8 +102,7 @@ public class Translator {
parseModule();
}
-
-
+
private void parseModule() throws FrontEndException {
moduleName = evalFileName(moduleFileName);
@@ -109,8 +110,7 @@ public class Translator {
moduleNode = tlaParser.parseModule(moduleName);
}
-
- private void parse() throws FrontEndException{
+ private void parse() throws FrontEndException {
moduleName = evalFileName(moduleFileName);
TLAParser tlaParser = new TLAParser(null);
@@ -119,18 +119,19 @@ public class Translator {
modelConfig = null;
if (configFileName != null) {
File f = new File(configFileName);
- if(f.exists()){
+ if (f.exists()) {
modelConfig = new ModelConfig(f.getName(), null);
modelConfig.parse();
}
- }else {
+ } else {
String fileNameWithoutSuffix = moduleFileName;
if (fileNameWithoutSuffix.toLowerCase().endsWith(".tla")) {
- fileNameWithoutSuffix = fileNameWithoutSuffix.substring(0, fileNameWithoutSuffix.length() - 4);
+ fileNameWithoutSuffix = fileNameWithoutSuffix.substring(0,
+ fileNameWithoutSuffix.length() - 4);
}
String configFile = fileNameWithoutSuffix + ".cfg";
File f = new File(configFile);
- if(f.exists()){
+ if (f.exists()) {
modelConfig = new ModelConfig(f.getName(), null);
modelConfig.parse();
}
@@ -144,6 +145,9 @@ public class Translator {
SymbolSorter symbolSorter = new SymbolSorter(moduleNode);
symbolSorter.sort();
+ PredicateVsExpression predicateVsExpression = new PredicateVsExpression(
+ moduleNode);
+
SpecAnalyser specAnalyser;
ConfigfileEvaluator conEval = null;
@@ -172,11 +176,15 @@ public class Translator {
BMachinePrinter p = new BMachinePrinter(moduleNode, conEval,
specAnalyser);
bMachineString = p.start().toString();
+
+ UsedExternalFunctions usedExternalFunctions = new UsedExternalFunctions(
+ moduleNode, specAnalyser);
+
BAstCreator bAstCreator = new BAstCreator(moduleNode, conEval,
- specAnalyser);
-
+ specAnalyser, usedExternalFunctions, predicateVsExpression);
+
this.bDefinitions = bAstCreator.getBDefinitions();
-
+
return bAstCreator.getStartNode();
}
@@ -188,8 +196,7 @@ public class Translator {
if (name.toLowerCase().endsWith(".cfg")) {
name = name.substring(0, name.length() - 4);
}
-
-
+
String sourceModuleName = name.substring(name
.lastIndexOf(FileUtil.separator) + 1);
@@ -199,13 +206,13 @@ public class Translator {
ToolIO.setUserDir(path);
return sourceModuleName;
}
-
- public Definitions getBDefinitions(){
+
+ public Definitions getBDefinitions() {
return bDefinitions;
}
- public String getBMachineString(){
+ public String getBMachineString() {
return bMachineString;
}
-
+
}
diff --git a/src/test/java/de/tla2b/examples/ForDistribution.java b/src/test/java/de/tla2b/examples/ForDistribution.java
deleted file mode 100644
index 64e927653428edfe4c70d51462cef949b2051b28..0000000000000000000000000000000000000000
--- a/src/test/java/de/tla2b/examples/ForDistribution.java
+++ /dev/null
@@ -1,46 +0,0 @@
-package de.tla2b.examples;
-
-import org.junit.Test;
-import static de.tla2b.util.TestUtil.runModule;
-
-
-public class ForDistribution {
-
-
- @Test
- public void testClub() throws Exception {
- String file = "src/test/resources/examples/Club/Club.tla";
- runModule(file);
- }
-
- @Test
- public void testSimpleMC() throws Exception {
- String file = "src/test/resources/MCTests/simple/MC.tla";
- runModule(file);
- }
-
- @Test
- public void testConstantSetupMC() throws Exception {
- String file = "src/test/resources/MCTests/constantsetup/MC.tla";
- runModule(file);
- }
-
- @Test
- public void testModelValuesMC() throws Exception {
- String file = "src/test/resources/MCTests/modelvalues/MC.tla";
- runModule(file);
- }
-
- @Test
- public void testDieHardMC() throws Exception {
- String file = "src/test/resources/MCTests/DieHard/MC.tla";
- runModule(file);
- }
-
- @Test
- public void testSimpleAllocatorMC() throws Exception {
- String file = "src/test/resources/MCTests/SimpleAllocator/MC.tla";
- runModule(file);
- }
-
-}
diff --git a/src/test/java/de/tla2b/examples/MCTest.java b/src/test/java/de/tla2b/examples/MCTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..19d068fdb4842ba123ed187904d6507a2b3a8d5b
--- /dev/null
+++ b/src/test/java/de/tla2b/examples/MCTest.java
@@ -0,0 +1,96 @@
+package de.tla2b.examples;
+
+import org.junit.Ignore;
+import org.junit.Test;
+
+import static de.tla2b.util.TestUtil.runModule;
+
+public class MCTest {
+
+ @Test
+ public void testClub() throws Exception {
+ String file = "src/test/resources/examples/Club/Club.tla";
+ runModule(file);
+ }
+
+ @Test
+ public void testSimpleMC() throws Exception {
+ String file = "src/test/resources/MCTests/simple/MC.tla";
+ runModule(file);
+ }
+
+ @Test
+ public void testConstantSetupMC() throws Exception {
+ String file = "src/test/resources/MCTests/constantsetup/MC.tla";
+ runModule(file);
+ }
+
+ @Test
+ public void testModelValuesMC() throws Exception {
+ String file = "src/test/resources/MCTests/modelvalues/MC.tla";
+ runModule(file);
+ }
+
+ @Test
+ public void testDieHardMC() throws Exception {
+ String file = "src/test/resources/MCTests/DieHard/MC.tla";
+ runModule(file);
+ }
+
+ @Test
+ public void testSimpleAllocatorMC() throws Exception {
+ String file = "src/test/resources/MCTests/SimpleAllocator/MC.tla";
+ runModule(file);
+ }
+
+ @Test
+ public void testMCDieHarder() throws Exception {
+ String file = "src/test/resources/MCTests/MCDieHarder/MCDieHarder.tla";
+ runModule(file);
+ }
+
+ @Test
+ public void testDieHarder() throws Exception {
+ String file = "src/test/resources/MCTests/DieHarder/MC.tla";
+ runModule(file);
+ }
+
+ @Test
+ public void testChannel() throws Exception {
+ String file = "src/test/resources/examples/Channel/Channel.tla";
+ runModule(file);
+ }
+
+ @Ignore
+ @Test
+ public void testCarTalkPuzzle() throws Exception {
+ String file = "src/test/resources/MCTests/CarTalkPuzzle/MC.tla";
+ runModule(file);
+ }
+
+ @Ignore
+ @Test
+ public void testCarTalkPuzzleModel2() throws Exception {
+ String file = "src/test/resources/MCTests/CarTalkPuzzle/Model2/MC.tla";
+ runModule(file);
+ }
+
+ @Test
+ public void testSequences() throws Exception {
+ String file = "src/test/resources/examples/MySequence/MySequence.tla";
+ runModule(file);
+ }
+
+ @Ignore
+ @Test
+ public void testRecursiveFunciton() throws Exception {
+ String file = "src/test/resources/examples/RecursiveFunction/RecursiveFunction.tla";
+ runModule(file);
+ }
+
+ @Test
+ public void testQueens() throws Exception {
+ String file = "src/test/resources/MCTests/Queens/MC.tla";
+ runModule(file);
+ }
+}
diff --git a/src/test/java/de/tla2b/prettyprintb/DefinitionsTest.java b/src/test/java/de/tla2b/prettyprintb/DefinitionsTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..d120ee40d67fed3b5b8606533911699164480ca3
--- /dev/null
+++ b/src/test/java/de/tla2b/prettyprintb/DefinitionsTest.java
@@ -0,0 +1,36 @@
+package de.tla2b.prettyprintb;
+
+import static de.tla2b.util.TestUtil.compare;
+
+import org.junit.Test;
+
+public class DefinitionsTest {
+
+ @Test
+ public void testMakePredicate() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "foo == TRUE \n"
+ + "ASSUME foo\n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "DEFINITIONS foo == TRUE;"
+ + "PROPERTIES foo = TRUE\n"
+ + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testPredicate() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "foo == TRUE = TRUE \n"
+ + "ASSUME foo\n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "DEFINITIONS foo == TRUE= TRUE;"
+ + "PROPERTIES foo\n"
+ + "END";
+ compare(expected, module);
+ }
+}
diff --git a/src/test/java/de/tla2b/prettyprintb/ExceptTest.java b/src/test/java/de/tla2b/prettyprintb/ExceptTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..23813f430439f89d72df72d3d55ba996dd5ca693
--- /dev/null
+++ b/src/test/java/de/tla2b/prettyprintb/ExceptTest.java
@@ -0,0 +1,77 @@
+package de.tla2b.prettyprintb;
+
+import static de.tla2b.util.TestUtil.compare;
+import static org.junit.Assert.assertEquals;
+
+import org.junit.Ignore;
+import org.junit.Test;
+
+import util.ToolIO;
+import de.tla2b.util.TestUtil;
+
+public class ExceptTest {
+
+ @Test
+ public void testFunctionExcept() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "CONSTANTS k \n"
+ + "ASSUME k = [k EXCEPT ![TRUE] = 0, ![FALSE] = 0] \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
+ + "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"
+ + "CONSTANTS k \n"
+ + "ASSUME k = [k EXCEPT ![TRUE] = 0, ![FALSE] = 0] \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
+ + "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"
+ + "EXTENDS Naturals \n"
+ + "CONSTANTS k \n"
+ + "ASSUME k = [x \\in {1,2} |-> x] /\\ [k EXCEPT ![1] = @ + 1][1] = 2 \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "ABSTRACT_CONSTANTS k \n"
+ + "PROPERTIES k : INTEGER +-> INTEGER & (k = %x.(x : {1, 2}| x) & (k <+ {1 |-> k(1) + 1})(1) = 2)\n"
+ + "END";
+ compare(expected, module);
+ }
+ @Ignore
+ @Test
+ public void testFunctionExceptAt2() throws Exception {
+ ToolIO.reset();
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "CONSTANTS k, k2 \n"
+ + "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/prettyprintb/FunctionTest.java b/src/test/java/de/tla2b/prettyprintb/FunctionTest.java
index c6d14fae72e540f46cdcaaafb69c5fb460369a68..093344021ca97dccb584880e1a43fade6990340c 100644
--- a/src/test/java/de/tla2b/prettyprintb/FunctionTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/FunctionTest.java
@@ -132,55 +132,5 @@ public class FunctionTest {
compare(expected, module);
}
- @Test
- public void testFunctionExcept() throws Exception {
- final String module = "-------------- MODULE Testing ----------------\n"
- + "CONSTANTS k \n"
- + "ASSUME k = [k EXCEPT ![TRUE] = 0, ![FALSE] = 0] \n"
- + "=================================";
-
- final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
- + "PROPERTIES "
- + " k : BOOL +-> INTEGER "
- + "& k = k <+ {TRUE |-> 0, FALSE |-> 0}" + "END";
- compare(expected, module);
- }
-
- /**********************************************************************
- * Record Except @
- **********************************************************************/
- @Test
- public void testFunctionExceptAt() throws Exception {
- final String module = "-------------- MODULE Testing ----------------\n"
- + "EXTENDS Naturals \n"
- + "CONSTANTS k \n"
- + "ASSUME k = [x \\in {1,2} |-> x] /\\ [k EXCEPT ![1] = @ + 1][1] = 2 \n"
- + "=================================";
-
- final String expected = "MACHINE Testing\n"
- + "ABSTRACT_CONSTANTS k \n"
- + "PROPERTIES k : INTEGER +-> INTEGER & (k = %x.(x : {1, 2}| x) & (k <+ {1 |-> k(1) + 1})(1) = 2)\n"
- + "END";
- compare(expected, module);
- }
- @Ignore
- @Test
- public void testFunctionExceptAt2() throws Exception {
- ToolIO.reset();
- final String module = "-------------- MODULE Testing ----------------\n"
- + "EXTENDS Naturals \n"
- + "CONSTANTS k, k2 \n"
- + "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/prettyprintb/MiscellaneousConstructsTest.java b/src/test/java/de/tla2b/prettyprintb/MiscellaneousConstructsTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..366bb0a4a8b3b4a730f50dfe4c22bd4418ce0c4c
--- /dev/null
+++ b/src/test/java/de/tla2b/prettyprintb/MiscellaneousConstructsTest.java
@@ -0,0 +1,145 @@
+package de.tla2b.prettyprintb;
+
+import static de.tla2b.util.TestUtil.compare;
+
+import org.junit.Test;
+
+public class MiscellaneousConstructsTest {
+
+ @Test
+ public void testSimpleLet() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "ASSUME LET foo(a) == a + a IN 4 = foo(2)\n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES 4 = 2 + 2 \n" + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testLet2Definitions() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "ASSUME LET foo(a) == a + a bar(b) == b * b IN bar(2) = foo(2)\n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES 2 * 2 = 2 + 2 \n" + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testNestedLet() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "ASSUME LET foo(a) == LET bar(b) == b * b IN bar(a+1) IN 9 = foo(2)\n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES 9 = (2 + 1) * (2 + 1) \n" + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testSimpleCase() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "ASSUME 2 = CASE 1 = 1 -> 2 \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "DEFINITIONS CHOOSE(X) == \"a member of X\"; EXTERNAL_FUNCTION_CHOOSE(T) == POW(T) --> T;"
+ + "PROPERTIES 2 = CHOOSE({t_ | 1=1 & t_ = 2}) \n" + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testCase2Conditions() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "ASSUME 2 = CASE 1 = 1 -> 2 [] 1 = 2 -> 3\n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "DEFINITIONS CHOOSE(X) == \"a member of X\"; EXTERNAL_FUNCTION_CHOOSE(T) == POW(T) --> T;"
+ + "PROPERTIES 2 = CHOOSE({t_ | (1 = 1 & t_ = 2) or (1 = 2 & t_ = 3)}) \n" + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testCaseOtherCondition() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "ASSUME 4 = CASE 1 = 2 -> 2 [] 1 = 3 -> 3 [] OTHER -> 4\n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "DEFINITIONS CHOOSE(X) == \"a member of X\"; EXTERNAL_FUNCTION_CHOOSE(T) == POW(T) --> T;"
+ + "PROPERTIES 4 = CHOOSE({t_ | ((1 = 2 & t_ = 2) or (1 = 3 & t_ = 3)) or (not(1 = 2 or 1 = 3) & t_ = 4)}) \n" + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testCasePredicate() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "ASSUME CASE 1 = 2 -> TRUE [] TRUE -> 1=1\n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "DEFINITIONS CHOOSE(X) == \"a member of X\"; EXTERNAL_FUNCTION_CHOOSE(T) == POW(T) --> T;"
+ + "PROPERTIES CHOOSE({t_ | (1 = 2 & t_ = TRUE) or (TRUE = TRUE & t_ = bool(1 = 1))}) = TRUE \n" + "END";
+ compare(expected, module);
+ }
+
+
+ @Test
+ public void testUnboundedChoose() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "ASSUME (CHOOSE x : x = 1) = 1\n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "DEFINITIONS CHOOSE(X) == \"a member of X\"; EXTERNAL_FUNCTION_CHOOSE(T) == POW(T) --> T;"
+ + "PROPERTIES CHOOSE({x | x = 1}) = 1 \n" + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testUnboundedChoosePredicate() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "ASSUME (CHOOSE x : x = TRUE)\n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "DEFINITIONS CHOOSE(X) == \"a member of X\"; EXTERNAL_FUNCTION_CHOOSE(T) == POW(T) --> T;"
+ + "PROPERTIES CHOOSE({x | x = TRUE}) = TRUE \n" + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testBoundedChoose() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "ASSUME (CHOOSE x \\in {1}: TRUE) = 1\n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "DEFINITIONS CHOOSE(X) == \"a member of X\"; EXTERNAL_FUNCTION_CHOOSE(T) == POW(T) --> T;"
+ + "PROPERTIES CHOOSE({x | x : {1} & TRUE = TRUE}) = 1 \n" + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testBoundedChoosePredicate() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "ASSUME (CHOOSE x \\in {TRUE}: TRUE) = TRUE\n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "DEFINITIONS CHOOSE(X) == \"a member of X\"; EXTERNAL_FUNCTION_CHOOSE(T) == POW(T) --> T;"
+ + "PROPERTIES CHOOSE({x | x : {TRUE} & TRUE = TRUE}) = TRUE \n" + "END";
+ compare(expected, module);
+ }
+}
diff --git a/src/test/java/de/tla2b/prettyprintb/StructTest.java b/src/test/java/de/tla2b/prettyprintb/RecordTest.java
similarity index 90%
rename from src/test/java/de/tla2b/prettyprintb/StructTest.java
rename to src/test/java/de/tla2b/prettyprintb/RecordTest.java
index 55f852b53269e46095c55eb2fd0338abe97e9f04..92fa439b707ee0d5c9642c773bcf25fb748991d6 100644
--- a/src/test/java/de/tla2b/prettyprintb/StructTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/RecordTest.java
@@ -11,7 +11,7 @@ import org.junit.Test;
import util.ToolIO;
-public class StructTest {
+public class RecordTest {
static {
ToolIO.setMode(ToolIO.TOOL);
}
@@ -109,7 +109,6 @@ public class StructTest {
/**********************************************************************
* Record Except
**********************************************************************/
- @Ignore
@Test
public void testRecordExcept() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -118,7 +117,7 @@ public class StructTest {
+ "=================================";
final String expected = "MACHINE Testing\n"
+ "ABSTRACT_CONSTANTS k, k2\n"
- + "PROPERTIES k = rec(a : 1, b : TRUE) & k2 = rec(a : 2, b : k'b) \n"
+ + "PROPERTIES k : struct(a:INTEGER, b:BOOL) & k2 : struct(a:INTEGER, b:BOOL) & (k = rec(a : 1, b : TRUE) & k2 = rec(a : 2, b : k'b)) \n"
+ "END";
compare(expected, module);
}
@@ -126,7 +125,6 @@ public class StructTest {
/**********************************************************************
* Record Except @
**********************************************************************/
- @Ignore
@Test
public void testRecordExceptAt() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -137,7 +135,7 @@ public class StructTest {
final String expected = "MACHINE Testing\n"
+ "ABSTRACT_CONSTANTS k, k2\n"
- + "PROPERTIES k : struct(a:INTEGER,b:BOOL) & k2 : struct(a:INTEGER,b:BOOL) & k = rec(a : 1, b : TRUE) & k2 = rec(a : k'a + 1, b : k'b) \n"
+ + "PROPERTIES k : struct(a:INTEGER, b:BOOL) & k2 : struct(a:INTEGER, b:BOOL) & (k = rec(a : 1, b : TRUE) & k2 = rec(a : k'a + 1, b : k'b)) \n"
+ "END";
compare(expected, module);
}
diff --git a/src/test/java/de/tla2b/typechecking/TupleVsSequenceTest.java b/src/test/java/de/tla2b/typechecking/TupleVsSequenceTest.java
index 24cf8a104acb0a11d248f9d22b619725d70986fd..6f3699da480aa2d3e5d0f1a6b9f9ae0e404eea01 100644
--- a/src/test/java/de/tla2b/typechecking/TupleVsSequenceTest.java
+++ b/src/test/java/de/tla2b/typechecking/TupleVsSequenceTest.java
@@ -47,4 +47,17 @@ public class TupleVsSequenceTest {
assertEquals("INTEGER", t.getConstantType("c"));
}
+ @Test
+ public void testTupleVsSequence4() throws FrontEndException, TLA2BException {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "CONSTANTS a, b, c\n"
+ + "ASSUME a = 1 /\\ b = TRUE /\\ c = <<a,b>>\n"
+ + "=================================";
+ TestTypeChecker t = TestUtil.typeCheckString(module);
+ assertEquals("INTEGER", t.getConstantType("a"));
+ assertEquals("BOOL", t.getConstantType("b"));
+ assertEquals("INTEGER*BOOL", t.getConstantType("c"));
+ }
+
+
}
diff --git a/src/test/resources/MCTests/DieHarder/DieHarder.tla b/src/test/resources/MCTests/DieHarder/DieHarder.tla
new file mode 100644
index 0000000000000000000000000000000000000000..62b5771ea83b2baba251e2847a39be659a324a1d
--- /dev/null
+++ b/src/test/resources/MCTests/DieHarder/DieHarder.tla
@@ -0,0 +1,93 @@
+----------------------------- MODULE DieHarder ------------------------------
+(***************************************************************************)
+(* We now generalize the problem from Die Hard into one with an arbitrary *)
+(* number of jugs, each holding some specified amount of water. *)
+(***************************************************************************)
+EXTENDS Naturals
+
+(***************************************************************************)
+(* We now declare two constant parameters. *)
+(***************************************************************************)
+
+CONSTANT Jug, \* The set of all jugs.
+ Capacity, \* A function, where Capacity[j] is the capacity of jug j.
+ Goal \* The quantity of water our heros must measure.
+(***************************************************************************)
+(* We make an assumption about these constants--namely, that Capacity is a *)
+(* function from jugs to positive integers, and Goal is a natural number. *)
+(***************************************************************************)
+ASSUME /\ Capacity \in [Jug -> {n \in Nat : n > 0}]
+ /\ Goal \in Nat
+(***************************************************************************)
+(* We are going to need the Min operator again, so let's define it here. *)
+(* (I prefer defining constant operators like this in the part of the *)
+(* spec where constants are declared. *)
+(***************************************************************************)
+Min(m,n) == IF m < n THEN m ELSE n
+-----------------------------------------------------------------------------
+(***************************************************************************)
+(* We declare the specification's single variable and define its type *)
+(* invariant and initial predicate. *)
+(***************************************************************************)
+VARIABLE contents \* contents[j] is the amount of water in jug j
+
+TypeOK == contents \in [Jug -> Nat]
+
+Init == contents = [j \in Jug |-> 0]
+-----------------------------------------------------------------------------
+(***************************************************************************)
+(* Now we define the actions that can be performed. They are the obvious *)
+(* generalizations of the ones from the simple DieHard spec. First come *)
+(* the actions of filling and emptying jug j, then the action of *)
+(* pouring water from jug j to jug k. *)
+(* *)
+(* Note: The definitions use the TLA+ notation *)
+(* *)
+(* [f EXCEPT ![c]=e] *)
+(* *)
+(* which is the function g that is the same as f except g[c]=e. In the *)
+(* expression e, the symbol @ stands for f[c]. This has the more general *)
+(* form *)
+(* *)
+(* [f EXCEPT ![c1] = e1, ... , ![ck] = ek] *)
+(* *)
+(* that has the expected meaning. *)
+(***************************************************************************)
+FillJug(j) == contents' = [contents EXCEPT ![j] = Capacity[j]]
+
+EmptyJug(j) == contents' = [contents EXCEPT ![j] = 0]
+
+JugToJug(j, k) ==
+ LET amountPoured == Min(contents[j], Capacity[k]-contents[k])
+ IN contents' = [contents EXCEPT ![j] = @ - amountPoured,
+ ![k] = @ + amountPoured]
+
+(***************************************************************************)
+(* As usual, the next-state relation Next is the disjunction of all *)
+(* possible actions, where existential quantification is a general form of *)
+(* disjunction. *)
+(***************************************************************************)
+Next == \E j \in Jug : \/ FillJug(j)
+ \/ EmptyJug(j)
+ \/ \E k \in Jug \ {j} : JugToJug(j, k)
+
+(***************************************************************************)
+(* We define the formula Spec to be the complete specification, asserting *)
+(* of a behavior that it begins in a state satisfying Init, and that every *)
+(* step either satisfies Next or else leaves contents unchanged. *)
+(***************************************************************************)
+Spec == Init /\ [][Next]_contents
+-----------------------------------------------------------------------------
+(***************************************************************************)
+(* We define NotSolved to be true of a state iff no jug contains Goal *)
+(* gallons of water. *)
+(***************************************************************************)
+NotSolved == \A j \in Jug : contents[j] # Goal
+
+(***************************************************************************)
+(* We find a solution by having TLC check if NotSolved is an invariant, *)
+(* which will cause it to print out an "error trace" consisting of a *)
+(* behavior ending in a states where NotSolved is false. Such a *)
+(* behavior is the desired solution. *)
+(***************************************************************************)
+=============================================================================
diff --git a/src/test/resources/MCTests/DieHarder/MC.cfg b/src/test/resources/MCTests/DieHarder/MC.cfg
new file mode 100644
index 0000000000000000000000000000000000000000..05484f50619dc7bd57cbe1aec981bbdd1844c716
--- /dev/null
+++ b/src/test/resources/MCTests/DieHarder/MC.cfg
@@ -0,0 +1,13 @@
+\* CONSTANT definitions
+CONSTANT
+Jug <- const_13977234641526000
+\* CONSTANT definitions
+CONSTANT
+Goal <- const_13977234641637000
+\* CONSTANT definitions
+CONSTANT
+Capacity <- const_13977234641748000
+\* SPECIFICATION definition
+SPECIFICATION
+spec_13977234641859000
+\* Generated on Thu Apr 17 10:31:04 CEST 2014
\ No newline at end of file
diff --git a/src/test/resources/MCTests/DieHarder/MC.out b/src/test/resources/MCTests/DieHarder/MC.out
new file mode 100644
index 0000000000000000000000000000000000000000..46a9a05447634db941c7e9f7c559c8bcc2fdad74
--- /dev/null
+++ b/src/test/resources/MCTests/DieHarder/MC.out
@@ -0,0 +1,67 @@
+@!@!@STARTMSG 2262:0 @!@!@
+TLC2 Version 2.05 of 23 July 2013
+@!@!@ENDMSG 2262 @!@!@
+@!@!@STARTMSG 2187:0 @!@!@
+Running in Model-Checking mode.
+@!@!@ENDMSG 2187 @!@!@
+@!@!@STARTMSG 2220:0 @!@!@
+Starting SANY...
+@!@!@ENDMSG 2220 @!@!@
+Parsing file MC.tla
+Parsing file MCDieHarder.tla
+Parsing file /Users/hansen/git/tlaprob/tlatools/class/tla2sany/StandardModules/TLC.tla
+Parsing file DieHarder.tla
+Parsing file /Users/hansen/git/tlaprob/tlatools/class/tla2sany/StandardModules/Naturals.tla
+Parsing file /Users/hansen/git/tlaprob/tlatools/class/tla2sany/StandardModules/Sequences.tla
+Semantic processing of module Naturals
+Semantic processing of module DieHarder
+Semantic processing of module MCDieHarder
+Semantic processing of module Sequences
+Semantic processing of module TLC
+Semantic processing of module MC
+@!@!@STARTMSG 2219:0 @!@!@
+SANY finished.
+@!@!@ENDMSG 2219 @!@!@
+@!@!@STARTMSG 2185:0 @!@!@
+Starting... (2014-04-17 10:31:05)
+@!@!@ENDMSG 2185 @!@!@
+@!@!@STARTMSG 2189:0 @!@!@
+Computing initial states...
+@!@!@ENDMSG 2189 @!@!@
+@!@!@STARTMSG 2190:0 @!@!@
+Finished computing initial states: 1 distinct state generated.
+@!@!@ENDMSG 2190 @!@!@
+@!@!@STARTMSG 2193:0 @!@!@
+Model checking completed. No error has been found.
+ Estimates of the probability that TLC did not check all reachable states
+ because two distinct states had the same fingerprint:
+ calculated (optimistic): val = 7.0E-17
+ based on the actual fingerprints: val = 2.7E-18
+@!@!@ENDMSG 2193 @!@!@
+@!@!@STARTMSG 2201:0 @!@!@
+The coverage statistics at 2014-04-17 10:31:05
+@!@!@ENDMSG 2201 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+ line 56, col 16 to line 56, col 63 of module DieHarder: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+ line 58, col 16 to line 58, col 53 of module DieHarder: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+ line 62, col 7 to line 63, col 59 of module DieHarder: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2202:0 @!@!@
+End of statistics.
+@!@!@ENDMSG 2202 @!@!@
+@!@!@STARTMSG 2200:0 @!@!@
+Progress(9) at 2014-04-17 10:31:05: 97 states generated (153.157 s/min), 16 distinct states found (25.263 ds/min), 0 states left on queue.
+@!@!@ENDMSG 2200 @!@!@
+@!@!@STARTMSG 2199:0 @!@!@
+97 states generated, 16 distinct states found, 0 states left on queue.
+@!@!@ENDMSG 2199 @!@!@
+@!@!@STARTMSG 2194:0 @!@!@
+The depth of the complete state graph search is 9.
+@!@!@ENDMSG 2194 @!@!@
+@!@!@STARTMSG 2186:0 @!@!@
+Finished. (2014-04-17 10:31:05)
+@!@!@ENDMSG 2186 @!@!@
diff --git a/src/test/resources/MCTests/DieHarder/MC.tla b/src/test/resources/MCTests/DieHarder/MC.tla
new file mode 100644
index 0000000000000000000000000000000000000000..7d950ff54aea2246382c18e23878fa0e23e96838
--- /dev/null
+++ b/src/test/resources/MCTests/DieHarder/MC.tla
@@ -0,0 +1,25 @@
+---- MODULE MC ----
+EXTENDS MCDieHarder, TLC
+
+\* CONSTANT definitions @modelParameterConstants:0Jug
+const_13977234641526000 ==
+MCJug
+----
+
+\* CONSTANT definitions @modelParameterConstants:1Goal
+const_13977234641637000 ==
+4
+----
+
+\* CONSTANT definitions @modelParameterConstants:2Capacity
+const_13977234641748000 ==
+MCCapacity
+----
+
+\* SPECIFICATION definition @modelBehaviorSpec:0
+spec_13977234641859000 ==
+Spec
+----
+=============================================================================
+\* Modification History
+\* Created Thu Apr 17 10:31:04 CEST 2014 by hansen
diff --git a/src/test/resources/MCTests/DieHarder/MCDieHarder.cfg b/src/test/resources/MCTests/DieHarder/MCDieHarder.cfg
new file mode 100644
index 0000000000000000000000000000000000000000..a2b049287576d6aae25238d3e03b5aa4ae2e6371
--- /dev/null
+++ b/src/test/resources/MCTests/DieHarder/MCDieHarder.cfg
@@ -0,0 +1,7 @@
+CONSTANTS Goal = 4
+ Jug <- MCJug
+ Capacity <- MCCapacity
+
+SPECIFICATION Spec
+INVARIANTS TypeOK NotSolved
+
diff --git a/src/test/resources/MCTests/DieHarder/MCDieHarder.tla b/src/test/resources/MCTests/DieHarder/MCDieHarder.tla
new file mode 100644
index 0000000000000000000000000000000000000000..a4b83157f22f1012b090f53ac80472286199dd3c
--- /dev/null
+++ b/src/test/resources/MCTests/DieHarder/MCDieHarder.tla
@@ -0,0 +1,20 @@
+---------------------------- MODULE MCDieHarder -----------------------------
+EXTENDS DieHarder
+
+(***************************************************************************)
+(* To have TLC find a solution, we must tell it what values to use for the *)
+(* constant parameters Jug, Capacity, and Goal. However, TLC does not *)
+(* allow one to write write function-valued expressions in a configuration *)
+(* file. So, we use this module, which extends module DieHarder, to *)
+(* define a function MCCapacity and have the configuration file TLC to *)
+(* substitute MCCapacity for Capacity. Since we need to know the value of *)
+(* Jug to define Capacity (which is a function having Jug as its domain), *)
+(* we also define MCJug and tell TLC to substitute it for Jug. *)
+(***************************************************************************)
+
+\* The following definitions duplicate the original Die Hard problem.
+MCJug == {"j1", "j2"}
+MCCapacity ==
+ [j \in MCJug |-> CASE j = "j1" -> 3
+ [] j = "j2" -> 5 ]
+=============================================================================
diff --git a/src/test/resources/MCTests/DieHarder/MC_TE.out b/src/test/resources/MCTests/DieHarder/MC_TE.out
new file mode 100644
index 0000000000000000000000000000000000000000..46a9a05447634db941c7e9f7c559c8bcc2fdad74
--- /dev/null
+++ b/src/test/resources/MCTests/DieHarder/MC_TE.out
@@ -0,0 +1,67 @@
+@!@!@STARTMSG 2262:0 @!@!@
+TLC2 Version 2.05 of 23 July 2013
+@!@!@ENDMSG 2262 @!@!@
+@!@!@STARTMSG 2187:0 @!@!@
+Running in Model-Checking mode.
+@!@!@ENDMSG 2187 @!@!@
+@!@!@STARTMSG 2220:0 @!@!@
+Starting SANY...
+@!@!@ENDMSG 2220 @!@!@
+Parsing file MC.tla
+Parsing file MCDieHarder.tla
+Parsing file /Users/hansen/git/tlaprob/tlatools/class/tla2sany/StandardModules/TLC.tla
+Parsing file DieHarder.tla
+Parsing file /Users/hansen/git/tlaprob/tlatools/class/tla2sany/StandardModules/Naturals.tla
+Parsing file /Users/hansen/git/tlaprob/tlatools/class/tla2sany/StandardModules/Sequences.tla
+Semantic processing of module Naturals
+Semantic processing of module DieHarder
+Semantic processing of module MCDieHarder
+Semantic processing of module Sequences
+Semantic processing of module TLC
+Semantic processing of module MC
+@!@!@STARTMSG 2219:0 @!@!@
+SANY finished.
+@!@!@ENDMSG 2219 @!@!@
+@!@!@STARTMSG 2185:0 @!@!@
+Starting... (2014-04-17 10:31:05)
+@!@!@ENDMSG 2185 @!@!@
+@!@!@STARTMSG 2189:0 @!@!@
+Computing initial states...
+@!@!@ENDMSG 2189 @!@!@
+@!@!@STARTMSG 2190:0 @!@!@
+Finished computing initial states: 1 distinct state generated.
+@!@!@ENDMSG 2190 @!@!@
+@!@!@STARTMSG 2193:0 @!@!@
+Model checking completed. No error has been found.
+ Estimates of the probability that TLC did not check all reachable states
+ because two distinct states had the same fingerprint:
+ calculated (optimistic): val = 7.0E-17
+ based on the actual fingerprints: val = 2.7E-18
+@!@!@ENDMSG 2193 @!@!@
+@!@!@STARTMSG 2201:0 @!@!@
+The coverage statistics at 2014-04-17 10:31:05
+@!@!@ENDMSG 2201 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+ line 56, col 16 to line 56, col 63 of module DieHarder: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+ line 58, col 16 to line 58, col 53 of module DieHarder: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+ line 62, col 7 to line 63, col 59 of module DieHarder: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2202:0 @!@!@
+End of statistics.
+@!@!@ENDMSG 2202 @!@!@
+@!@!@STARTMSG 2200:0 @!@!@
+Progress(9) at 2014-04-17 10:31:05: 97 states generated (153.157 s/min), 16 distinct states found (25.263 ds/min), 0 states left on queue.
+@!@!@ENDMSG 2200 @!@!@
+@!@!@STARTMSG 2199:0 @!@!@
+97 states generated, 16 distinct states found, 0 states left on queue.
+@!@!@ENDMSG 2199 @!@!@
+@!@!@STARTMSG 2194:0 @!@!@
+The depth of the complete state graph search is 9.
+@!@!@ENDMSG 2194 @!@!@
+@!@!@STARTMSG 2186:0 @!@!@
+Finished. (2014-04-17 10:31:05)
+@!@!@ENDMSG 2186 @!@!@
diff --git a/src/test/resources/MCTests/MCDieHarder/DieHarder.tla b/src/test/resources/MCTests/MCDieHarder/DieHarder.tla
new file mode 100644
index 0000000000000000000000000000000000000000..62b5771ea83b2baba251e2847a39be659a324a1d
--- /dev/null
+++ b/src/test/resources/MCTests/MCDieHarder/DieHarder.tla
@@ -0,0 +1,93 @@
+----------------------------- MODULE DieHarder ------------------------------
+(***************************************************************************)
+(* We now generalize the problem from Die Hard into one with an arbitrary *)
+(* number of jugs, each holding some specified amount of water. *)
+(***************************************************************************)
+EXTENDS Naturals
+
+(***************************************************************************)
+(* We now declare two constant parameters. *)
+(***************************************************************************)
+
+CONSTANT Jug, \* The set of all jugs.
+ Capacity, \* A function, where Capacity[j] is the capacity of jug j.
+ Goal \* The quantity of water our heros must measure.
+(***************************************************************************)
+(* We make an assumption about these constants--namely, that Capacity is a *)
+(* function from jugs to positive integers, and Goal is a natural number. *)
+(***************************************************************************)
+ASSUME /\ Capacity \in [Jug -> {n \in Nat : n > 0}]
+ /\ Goal \in Nat
+(***************************************************************************)
+(* We are going to need the Min operator again, so let's define it here. *)
+(* (I prefer defining constant operators like this in the part of the *)
+(* spec where constants are declared. *)
+(***************************************************************************)
+Min(m,n) == IF m < n THEN m ELSE n
+-----------------------------------------------------------------------------
+(***************************************************************************)
+(* We declare the specification's single variable and define its type *)
+(* invariant and initial predicate. *)
+(***************************************************************************)
+VARIABLE contents \* contents[j] is the amount of water in jug j
+
+TypeOK == contents \in [Jug -> Nat]
+
+Init == contents = [j \in Jug |-> 0]
+-----------------------------------------------------------------------------
+(***************************************************************************)
+(* Now we define the actions that can be performed. They are the obvious *)
+(* generalizations of the ones from the simple DieHard spec. First come *)
+(* the actions of filling and emptying jug j, then the action of *)
+(* pouring water from jug j to jug k. *)
+(* *)
+(* Note: The definitions use the TLA+ notation *)
+(* *)
+(* [f EXCEPT ![c]=e] *)
+(* *)
+(* which is the function g that is the same as f except g[c]=e. In the *)
+(* expression e, the symbol @ stands for f[c]. This has the more general *)
+(* form *)
+(* *)
+(* [f EXCEPT ![c1] = e1, ... , ![ck] = ek] *)
+(* *)
+(* that has the expected meaning. *)
+(***************************************************************************)
+FillJug(j) == contents' = [contents EXCEPT ![j] = Capacity[j]]
+
+EmptyJug(j) == contents' = [contents EXCEPT ![j] = 0]
+
+JugToJug(j, k) ==
+ LET amountPoured == Min(contents[j], Capacity[k]-contents[k])
+ IN contents' = [contents EXCEPT ![j] = @ - amountPoured,
+ ![k] = @ + amountPoured]
+
+(***************************************************************************)
+(* As usual, the next-state relation Next is the disjunction of all *)
+(* possible actions, where existential quantification is a general form of *)
+(* disjunction. *)
+(***************************************************************************)
+Next == \E j \in Jug : \/ FillJug(j)
+ \/ EmptyJug(j)
+ \/ \E k \in Jug \ {j} : JugToJug(j, k)
+
+(***************************************************************************)
+(* We define the formula Spec to be the complete specification, asserting *)
+(* of a behavior that it begins in a state satisfying Init, and that every *)
+(* step either satisfies Next or else leaves contents unchanged. *)
+(***************************************************************************)
+Spec == Init /\ [][Next]_contents
+-----------------------------------------------------------------------------
+(***************************************************************************)
+(* We define NotSolved to be true of a state iff no jug contains Goal *)
+(* gallons of water. *)
+(***************************************************************************)
+NotSolved == \A j \in Jug : contents[j] # Goal
+
+(***************************************************************************)
+(* We find a solution by having TLC check if NotSolved is an invariant, *)
+(* which will cause it to print out an "error trace" consisting of a *)
+(* behavior ending in a states where NotSolved is false. Such a *)
+(* behavior is the desired solution. *)
+(***************************************************************************)
+=============================================================================
diff --git a/src/test/resources/MCTests/MCDieHarder/MCDieHarder.cfg b/src/test/resources/MCTests/MCDieHarder/MCDieHarder.cfg
new file mode 100644
index 0000000000000000000000000000000000000000..a2b049287576d6aae25238d3e03b5aa4ae2e6371
--- /dev/null
+++ b/src/test/resources/MCTests/MCDieHarder/MCDieHarder.cfg
@@ -0,0 +1,7 @@
+CONSTANTS Goal = 4
+ Jug <- MCJug
+ Capacity <- MCCapacity
+
+SPECIFICATION Spec
+INVARIANTS TypeOK NotSolved
+
diff --git a/src/test/resources/MCTests/MCDieHarder/MCDieHarder.tla b/src/test/resources/MCTests/MCDieHarder/MCDieHarder.tla
new file mode 100644
index 0000000000000000000000000000000000000000..a4b83157f22f1012b090f53ac80472286199dd3c
--- /dev/null
+++ b/src/test/resources/MCTests/MCDieHarder/MCDieHarder.tla
@@ -0,0 +1,20 @@
+---------------------------- MODULE MCDieHarder -----------------------------
+EXTENDS DieHarder
+
+(***************************************************************************)
+(* To have TLC find a solution, we must tell it what values to use for the *)
+(* constant parameters Jug, Capacity, and Goal. However, TLC does not *)
+(* allow one to write write function-valued expressions in a configuration *)
+(* file. So, we use this module, which extends module DieHarder, to *)
+(* define a function MCCapacity and have the configuration file TLC to *)
+(* substitute MCCapacity for Capacity. Since we need to know the value of *)
+(* Jug to define Capacity (which is a function having Jug as its domain), *)
+(* we also define MCJug and tell TLC to substitute it for Jug. *)
+(***************************************************************************)
+
+\* The following definitions duplicate the original Die Hard problem.
+MCJug == {"j1", "j2"}
+MCCapacity ==
+ [j \in MCJug |-> CASE j = "j1" -> 3
+ [] j = "j2" -> 5 ]
+=============================================================================
diff --git a/src/test/resources/MCTests/Queens/MC.cfg b/src/test/resources/MCTests/Queens/MC.cfg
new file mode 100644
index 0000000000000000000000000000000000000000..d8e4aeae30c5958141e8744b990a8e7b9b0a3fb0
--- /dev/null
+++ b/src/test/resources/MCTests/Queens/MC.cfg
@@ -0,0 +1,14 @@
+\* CONSTANT definitions
+CONSTANT
+N <- const_129269506133433000
+\* SPECIFICATION definition
+SPECIFICATION
+spec_129269506134534000
+\* INVARIANT definition
+INVARIANT
+inv_129269506135535000
+inv_129269506136536000
+\* PROPERTY definition
+PROPERTY
+prop_129269506137537000
+\* Generated at Sat Dec 18 18:57:41 CET 2010
\ No newline at end of file
diff --git a/src/test/resources/MCTests/Queens/MC.tla b/src/test/resources/MCTests/Queens/MC.tla
new file mode 100644
index 0000000000000000000000000000000000000000..56f27aec7477b98e396b7e954d80c43148d63795
--- /dev/null
+++ b/src/test/resources/MCTests/Queens/MC.tla
@@ -0,0 +1,27 @@
+---- MODULE MC ----
+EXTENDS QueensPlusCal, TLC
+
+\* CONSTANT definitions @modelParameterConstants:0N
+const_129269506133433000 ==
+4
+----
+
+\* SPECIFICATION definition @modelBehaviorSpec:0
+spec_129269506134534000 ==
+LiveSpec
+----
+\* INVARIANT definition @modelCorrectnessInvariants:0
+inv_129269506135535000 ==
+TypeInvariant
+----
+\* INVARIANT definition @modelCorrectnessInvariants:1
+inv_129269506136536000 ==
+Invariant
+----
+\* PROPERTY definition @modelCorrectnessProperties:0
+prop_129269506137537000 ==
+Termination
+----
+=============================================================================
+\* Modification History
+\* Created Sat Dec 18 18:57:41 CET 2010 by merz
diff --git a/src/test/resources/MCTests/Queens/QueensPlusCal.tla b/src/test/resources/MCTests/Queens/QueensPlusCal.tla
new file mode 100644
index 0000000000000000000000000000000000000000..bc1d9cc946187a01615f40d55acee0408ae0f807
--- /dev/null
+++ b/src/test/resources/MCTests/Queens/QueensPlusCal.tla
@@ -0,0 +1,124 @@
+-------------------------- MODULE QueensPlusCal -----------------------------
+EXTENDS Naturals, Sequences
+(***************************************************************************)
+(* Formulation of the N-queens problem and an iterative algorithm to solve *)
+(* the problem in TLA+. Since there must be exactly one queen in every row *)
+(* we represent placements of queens as functions of the form *)
+(* queens \in [ 1..N -> 1..N ] *)
+(* where queens[i] gives the column of the queen in row i. Note that such *)
+(* a function is just a sequence of length N. *)
+(* We will also consider partial solutions, also represented as sequences *)
+(* of length \leq N. *)
+(***************************************************************************)
+
+CONSTANT N \** number of queens and size of the board
+ASSUME N \in Nat \ {0}
+
+(* The following predicate determines if queens i and j attack each other
+ in a placement of queens (represented by a sequence as above). *)
+Attacks(queens,i,j) ==
+ \/ queens[i] = queens[j] \** same column
+ \/ queens[i] - queens[j] = i - j \** first diagonal
+ \/ queens[j] - queens[i] = i - j \** second diagonal
+
+(* A placement represents a (partial) solution if no two different queens
+ attack each other in it. *)
+IsSolution(queens) ==
+ \A i \in 1 .. Len(queens)-1 : \A j \in i+1 .. Len(queens) :
+ ~ Attacks(queens,i,j)
+
+(* Compute the set of solutions of the N-queens problem. *)
+Solutions == { queens \in [1..N -> 1..N] : IsSolution(queens) }
+
+(***************************************************************************)
+(* We now describe an algorithm that iteratively computes the set of *)
+(* solutions of the N-queens problem by successively placing queens. *)
+(* The current state of the algorithm is given by two variables: *)
+(* - todo contains a set of partial solutions, *)
+(* - sols contains the set of full solutions found so far. *)
+(* At every step, the algorithm picks some partial solution and computes *)
+(* all possible extensions by the next queen. If N queens have been placed *)
+(* these extensions are in fact full solutions, otherwise they are added *)
+(* to the set todo. *)
+(***************************************************************************)
+
+(* --algorithm Queens
+ variables
+ todo = { << >> };
+ sols = {};
+
+ begin
+nxtQ: while todo # {}
+ do
+ with queens \in todo,
+ nxtQ = Len(queens) + 1,
+ cols = { c \in 1..N : ~ \E i \in 1 .. Len(queens) :
+ Attacks( Append(queens, c), i, nxtQ ) },
+ exts = { Append(queens,c) : c \in cols }
+ do
+ if (nxtQ = N)
+ then todo := todo \ {queens}; sols := sols \union exts;
+ else todo := (todo \ {queens}) \union exts;
+ end if;
+ end with;
+ end while;
+ end algorithm
+*)
+
+\** BEGIN TRANSLATION
+VARIABLES todo, sols, pc
+
+vars == << todo, sols, pc >>
+
+Init == (* Global variables *)
+ /\ todo = { << >> }
+ /\ sols = {}
+ /\ pc = "nxtQ"
+
+nxtQ == /\ pc = "nxtQ"
+ /\ IF todo # {}
+ THEN /\ \E queens \in todo:
+ LET nxtQ == Len(queens) + 1 IN
+ LET cols == { c \in 1..N : ~ \E i \in 1 .. Len(queens) :
+ Attacks( Append(queens, c), i, nxtQ ) } IN
+ LET exts == { Append(queens,c) : c \in cols } IN
+ IF (nxtQ = N)
+ THEN /\ todo' = todo \ {queens}
+ /\ sols' = (sols \union exts)
+ ELSE /\ todo' = ((todo \ {queens}) \union exts)
+ /\ UNCHANGED sols
+ /\ pc' = "nxtQ"
+ ELSE /\ pc' = "Done"
+ /\ UNCHANGED << todo, sols >>
+
+Next == nxtQ
+ \/ (* Disjunct to prevent deadlock on termination *)
+ (pc = "Done" /\ UNCHANGED vars)
+
+Spec == Init /\ [][Next]_vars
+
+Termination == <>(pc = "Done")
+
+\** END TRANSLATION
+
+TypeInvariant ==
+ /\ todo \in SUBSET Seq(1 .. N) /\ \A s \in todo : Len(s) < N
+ /\ sols \in SUBSET Seq(1 .. N) /\ \A s \in sols : Len(s) = N
+
+(* The set of sols contains only solutions, and contains all solutions
+ when todo is empty. *)
+Invariant ==
+ /\ sols \subseteq Solutions
+ /\ todo = {} => Solutions \subseteq sols
+
+(* Assert that no solutions are ever computed so that TLC displays one *)
+NoSolutions == sols = {}
+
+(* Add a fairness condition to ensure progress as long as todo is nonempty *)
+Liveness == WF_vars(nxtQ)
+LiveSpec == Spec /\ Liveness
+
+=============================================================================
+\* Modification History
+\* Last modified Sat Dec 18 18:57:03 CET 2010 by merz
+\* Created Sat Dec 11 08:50:24 CET 2010 by merz