diff --git a/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java b/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java
index 6339c0b67522c65e8c20c36ea83b6f99d3a45f41..9be8b30208d0444890f8c7c5c22dbdf55aa48eb6 100644
--- a/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java
+++ b/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java
@@ -1,5 +1,6 @@
package de.tla2b.analysis;
+import de.tla2b.global.BBuiltInOPs;
import tla2sany.semantic.ASTConstants;
import tla2sany.semantic.AssumeNode;
import tla2sany.semantic.AtNode;
@@ -105,22 +106,53 @@ public class AbstractASTVisitor extends BuiltInOPs implements ASTConstants {
case BuiltInKind: {
visitBuiltInNode(n);
+ return;
}
case UserDefinedOpKind: {
- visitUserDefinedNode(n);
+
+ if(BBuiltInOPs.contains(n.getOperator().getName())){
+ visitBBuiltinsNode(n);
+ return;
+ }else{
+ visitUserDefinedNode(n);
+ return;
+ }
+
+
}
}
}
- public void visitBuiltInNode(OpApplNode n) {
+ private void visitBBuiltinsNode(OpApplNode n) {
+ ExprNode[] in = n.getBdedQuantBounds();
+ for (ExprNode exprNode : in) {
+ visitExprNode(exprNode);
+ }
+
ExprOrOpArgNode[] arguments = n.getArgs();
for (ExprOrOpArgNode exprOrOpArgNode : arguments) {
visitExprOrOpArgNode(exprOrOpArgNode);
}
}
+ public void visitBuiltInNode(OpApplNode n) {
+ ExprNode[] in = n.getBdedQuantBounds();
+ for (ExprNode exprNode : in) {
+ visitExprNode(exprNode);
+ }
+
+ ExprOrOpArgNode[] arguments = n.getArgs();
+ for (ExprOrOpArgNode exprOrOpArgNode : arguments) {
+ // exprOrOpArgNode == null in case the OTHER construct
+ if(exprOrOpArgNode != null){
+ visitExprOrOpArgNode(exprOrOpArgNode);
+ }
+
+ }
+ }
+
public void visitLetInNode(LetInNode n) {
OpDefNode[] lets = n.getLets();
for (OpDefNode opDefNode : lets) {
diff --git a/src/main/java/de/tla2b/analysis/RecursiveFunktion.java b/src/main/java/de/tla2b/analysis/RecursiveFunktion.java
index 42975537d586c6924418028496a012068cf74115..6496f4cef454dfdeda39249dd7142f370125aa92 100644
--- a/src/main/java/de/tla2b/analysis/RecursiveFunktion.java
+++ b/src/main/java/de/tla2b/analysis/RecursiveFunktion.java
@@ -30,7 +30,7 @@ public class RecursiveFunktion extends BuiltInOPs {
*/
private void evalDef() throws NotImplementedException {
ExprOrOpArgNode e = rfs.getArgs()[0];
- System.out.println(rfs.toString(5));
+ //System.out.println(rfs.toString(5));
if (e instanceof OpApplNode) {
OpApplNode o = (OpApplNode) e;
switch (getOpCode(o.getOperator().getName())) {
diff --git a/src/main/java/de/tla2b/translation/BMacroHandler.java b/src/main/java/de/tla2b/translation/BMacroHandler.java
index 773309860205ac91fe3339e62d42b55c301eed7e..4852956defe7b4098cab47a26a9ab569de318a4a 100644
--- a/src/main/java/de/tla2b/translation/BMacroHandler.java
+++ b/src/main/java/de/tla2b/translation/BMacroHandler.java
@@ -1,9 +1,19 @@
package de.tla2b.translation;
import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.HashSet;
+import java.util.Hashtable;
+import java.util.Set;
+import tla2sany.semantic.AssumeNode;
+import tla2sany.semantic.ExprNode;
+import tla2sany.semantic.ExprOrOpArgNode;
+import tla2sany.semantic.FormalParamNode;
import tla2sany.semantic.ModuleNode;
+import tla2sany.semantic.OpApplNode;
import tla2sany.semantic.OpDefNode;
+import tla2sany.semantic.SymbolNode;
import de.tla2b.analysis.AbstractASTVisitor;
import de.tla2b.analysis.SpecAnalyser;
import de.tla2b.config.ConfigfileEvaluator;
@@ -24,14 +34,186 @@ public class BMacroHandler extends AbstractASTVisitor {
bDefs.add(def);
}
}
+
for (OpDefNode opDefNode : bDefs) {
visitDefinition(opDefNode);
}
+
+ visitAssumptions(moduleNode.getAssumptions());
}
-
+
+ private HashSet<FormalParamNode> definitionParameters;
+ private HashSet<FormalParamNode> localVariables;
+ private final Hashtable<FormalParamNode, Set<FormalParamNode>> parameterContext = new Hashtable<FormalParamNode, Set<FormalParamNode>>();
+
+ @Override
+ public void visitDefinition(OpDefNode def) {
+ definitionParameters = new HashSet<FormalParamNode>();
+ definitionParameters.addAll(Arrays.asList(def.getParams()));
+ for (FormalParamNode param : definitionParameters) {
+ parameterContext.put(param, new HashSet<FormalParamNode>());
+ }
+ localVariables = new HashSet<FormalParamNode>();
+
+ visitExprNode(def.getBody());
+
+ definitionParameters = null;
+ localVariables = null;
+ }
+
@Override
- public void visitDefinition(OpDefNode def){
-
+ public void visitAssumeNode(AssumeNode assumeNode) {
+ definitionParameters = new HashSet<FormalParamNode>();
+ localVariables = new HashSet<FormalParamNode>();
+
+ visitExprNode(assumeNode.getAssume());
+
+ definitionParameters = null;
+ localVariables = null;
+
+ }
+
+ @Override
+ public void visitBuiltInNode(OpApplNode n) {
+ switch (getOpCode(n.getOperator().getName())) {
+ case OPCODE_rfs:
+ case OPCODE_nrfs:
+ case OPCODE_fc: // Represents [x \in S |-> e]
+ case OPCODE_be: // \E x \in S : P
+ case OPCODE_bf: // \A x \in S : P
+ case OPCODE_bc: // CHOOSE x \in S: P
+ case OPCODE_sso: // $SubsetOf Represents {x \in S : P}
+ case OPCODE_soa: // $SetOfAll Represents {e : p1 \in S, p2,p3 \in S2}
+ {
+ ExprNode[] in = n.getBdedQuantBounds();
+ for (ExprNode exprNode : in) {
+ visitExprNode(exprNode);
+ }
+
+ FormalParamNode[][] params = n.getBdedQuantSymbolLists();
+ HashSet<FormalParamNode> set = new HashSet<FormalParamNode>();
+ for (int i = 0; i < params.length; i++) {
+ for (int j = 0; j < params[i].length; j++) {
+ FormalParamNode param = params[i][j];
+ set.add(param);
+ }
+ }
+ localVariables.addAll(set);
+ ExprOrOpArgNode[] arguments = n.getArgs();
+ for (ExprOrOpArgNode exprOrOpArgNode : arguments) {
+ visitExprOrOpArgNode(exprOrOpArgNode);
+ }
+ localVariables.removeAll(set);
+ return;
+ }
+ default: {
+ super.visitBuiltInNode(n);
+ return;
+ }
+
+ }
+
+ }
+
+
+ private Set<String> getStringSet(Set<FormalParamNode> set) {
+ HashSet<String> stringSet = new HashSet<String>();
+ for (FormalParamNode formalParamNode : set) {
+ stringSet.add(formalParamNode.getName().toString());
+ }
+ return stringSet;
+ }
+
+ private HashSet<FormalParamNode> illegalParams;
+
+ private void addToIllegalParams(Set<FormalParamNode> set) {
+ if (illegalParams == null) {
+ illegalParams = new HashSet<FormalParamNode>(set);
+ } else {
+ illegalParams.addAll(set);
+ }
+ }
+
+ private Set<FormalParamNode> getContextOfParam(FormalParamNode param) {
+ Set<FormalParamNode> set = parameterContext.get(param);
+ if (set == null) {
+ set = new HashSet<FormalParamNode>();
+ }
+ return set;
+ }
+
+ public void visitUserDefinedNode(OpApplNode n) {
+ OpDefNode operator = (OpDefNode) n.getOperator();
+ FormalParamNode[] params = operator.getParams();
+
+ ExprOrOpArgNode[] arguments = n.getArgs();
+ for (int i = 0; i < arguments.length; i++) {
+ Set<FormalParamNode> set = getContextOfParam(params[i]);
+ addToIllegalParams(set);
+ visitExprOrOpArgNode(arguments[i]);
+ illegalParams.removeAll(set);
+ }
+ }
+
+ Hashtable<FormalParamNode, String> renamingTable = new Hashtable<FormalParamNode, String>();
+
+ @Override
+ public void visitFormalParamNode(OpApplNode n) {
+ FormalParamNode param = (FormalParamNode) n.getOperator();
+ if (definitionParameters.contains(param)) {
+ parameterContext.get(param).addAll(localVariables);
+ }
+
+ hasSymbolAValidName(n);
+ }
+
+
+ public void visitConstantNode(OpApplNode n) {
+ hasSymbolAValidName(n);
+ }
+
+ public void visitVariableNode(OpApplNode n) {
+ hasSymbolAValidName(n);
}
+ private void hasSymbolAValidName(OpApplNode n){
+ SymbolNode symbol = n.getOperator();
+ String symbolName = symbol.getName().toString();
+ if (illegalParams != null) {
+ for (FormalParamNode illegalParam : illegalParams) {
+ if (symbolName.equals(illegalParam.getName().toString())) {
+ Set<String> illgalNames = getStringSet(illegalParams);
+ String newName = incName(symbolName, illgalNames);
+ renamingTable.put(illegalParam, newName);
+ }
+ }
+ }
+ }
+
+
+ Set<String> globalNames = new HashSet<String>();
+
+ private Boolean existingName(String name) {
+ if (globalNames.contains(name)) {
+ return true;
+ } else
+ return false;
+ }
+
+ private String incName(String name, Set<String> tempSet) {
+ String res = name;
+ for (int i = 1; existingName(res) || tempSet.contains(res); i++) {
+ res = name + "_" + i;
+ }
+ return res;
+ }
+
+ public boolean containsSymbolNode(SymbolNode s) {
+ return renamingTable.containsKey(s);
+ }
+
+ public String getNewName(SymbolNode s) {
+ return renamingTable.get(s);
+ }
+
}
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 1167a2875243d1841865b89912c1938e30730377..49df90e5a8c95cbfb7bd1e65f302847d6306f71f 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -2,6 +2,7 @@ package de.tla2bAst;
import java.util.ArrayList;
import java.util.Arrays;
+import java.util.Collection;
import java.util.HashSet;
import java.util.Hashtable;
import java.util.Iterator;
@@ -128,6 +129,7 @@ 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.RecursiveFunktion;
import de.tla2b.analysis.SpecAnalyser;
import de.tla2b.analysis.UsedExternalFunctions;
import de.tla2b.analysis.PredicateVsExpression.DefinitionType;
@@ -138,6 +140,7 @@ import de.tla2b.global.BBuildIns;
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.Priorities;
import de.tla2b.global.TranslationGlobals;
+import de.tla2b.translation.BMacroHandler;
import de.tla2b.types.EnumType;
import de.tla2b.types.FunctionType;
import de.tla2b.types.IType;
@@ -153,6 +156,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
ConfigfileEvaluator conEval;
SpecAnalyser specAnalyser;
private final PredicateVsExpression predicateVsExpression;
+ private final BMacroHandler bMacroHandler;
final int SUBSTITUTE_PARAM = 29;
@@ -176,8 +180,10 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
public BAstCreator(ModuleNode moduleNode, ConfigfileEvaluator conEval,
SpecAnalyser specAnalyser,
UsedExternalFunctions usedExternalFunctions,
- PredicateVsExpression predicateVsExpression) {
+ PredicateVsExpression predicateVsExpression,
+ BMacroHandler bMacroHandler) {
this.predicateVsExpression = predicateVsExpression;
+ this.bMacroHandler = bMacroHandler;
this.conEval = conEval;
this.moduleNode = moduleNode;
this.specAnalyser = specAnalyser;
@@ -497,6 +503,12 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
constantsList.add(id);
}
+ for (RecursiveFunktion recFunc : specAnalyser.getRecursiveFunctions()) {
+ AIdentifierExpression id = new AIdentifierExpression(
+ createTIdentifierLiteral(getName(recFunc.getOpDefNode())));
+ constantsList.add(id);
+ }
+
if (constantsList.size() > 0) {
AAbstractConstantsMachineClause abstractConstantsClause = new AAbstractConstantsMachineClause(
constantsList);
@@ -506,49 +518,19 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
private AIdentifierExpression createIdentifierNode(SymbolNode symbolNode) {
- return createIdentifierNode(symbolNode.getName().toString());
+ if (bMacroHandler.containsSymbolNode(symbolNode)) {
+ return createIdentifierNode(bMacroHandler.getNewName(symbolNode));
+ } else {
+ return createIdentifierNode(symbolNode.getName().toString());
+ }
}
private void createPropertyClause() {
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));
- // paramList2.add(createIdentifierNode(p.getName().toString()));
- TLAType paramType = (TLAType) p.getToolObject(TYPE_ID);
- // System.out.println(paramType);
- AEqualPredicate equal = new AEqualPredicate(
- createIdentifierNode(p), 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);
+ propertiesList.addAll(evalRecursiveDefinitions());
- AEqualPredicate equals = new AEqualPredicate(
- createIdentifierNode(def), lambda1);
- propertiesList.add(equals);
- }
+ //propertiesList.addAll(evalRecursiveFunctions());
for (OpDeclNode con : bConstants) {
if (conEval != null
@@ -628,6 +610,83 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
}
+ private List<PPredicate> evalRecursiveFunctions() {
+ List<PPredicate> propertiesList = new ArrayList<PPredicate>();
+ for (RecursiveFunktion recDef : specAnalyser.getRecursiveFunctions()) {
+
+
+ OpDefNode def = recDef.getOpDefNode();
+ 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));
+ // paramList2.add(createIdentifierNode(p.getName().toString()));
+ TLAType paramType = (TLAType) p.getToolObject(TYPE_ID);
+ // System.out.println(paramType);
+ AEqualPredicate equal = new AEqualPredicate(
+ createIdentifierNode(p), paramType.getBNode());
+ typeList.add(equal);
+ }
+ ALambdaExpression lambda1 = new ALambdaExpression();
+ lambda1.setIdentifiers(paramList1);
+ lambda1.setPredicate(createConjunction(typeList));
+ lambda1.setExpression(visitExprNodeExpression(def.getBody()));
+ AEqualPredicate equals = new AEqualPredicate(
+ createIdentifierNode(def), lambda1);
+ propertiesList.add(equals);
+
+
+ }
+
+ return propertiesList;
+ }
+
+ private List<PPredicate> evalRecursiveDefinitions() {
+ 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));
+ // paramList2.add(createIdentifierNode(p.getName().toString()));
+ TLAType paramType = (TLAType) p.getToolObject(TYPE_ID);
+ // System.out.println(paramType);
+ AEqualPredicate equal = new AEqualPredicate(
+ createIdentifierNode(p), 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), lambda1);
+ propertiesList.add(equals);
+ }
+
+ return propertiesList;
+ }
+
private PExpression createTLCValue(Value tlcValue) {
switch (tlcValue.getKind()) {
case INTVALUE:
@@ -876,11 +935,19 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
return funcCall;
}
} else {
- ADefinitionExpression defExpr = new ADefinitionExpression();
- defExpr.setDefLiteral(new TIdentifierLiteral(getName(n
- .getOperator())));
- defExpr.setParameters(params);
- return defExpr;
+ if (predicateVsExpression.getDefinitionType(def) == DefinitionType.PREDICATE) {
+ ADefinitionPredicate defPred = new ADefinitionPredicate();
+ defPred.setDefLiteral(new TDefLiteralPredicate(getName(n
+ .getOperator())));
+ defPred.setParameters(params);
+ return new AConvertBoolExpression(defPred);
+ } else {
+ ADefinitionExpression defExpr = new ADefinitionExpression();
+ defExpr.setDefLiteral(new TIdentifierLiteral(getName(n
+ .getOperator())));
+ defExpr.setParameters(params);
+ return defExpr;
+ }
}
} else {
@@ -1237,19 +1304,26 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
case OPCODE_sso: { // $SubsetOf Represents {x \in S : P}
- // TODO tuple with more than 2 arguments
- //FormalParamNode[][] params = n.getBdedQuantSymbolLists();
- //ExprNode[] bounds = n.getBdedQuantBounds();
+ FormalParamNode[][] params = n.getBdedQuantSymbolLists();
List<PExpression> list = new ArrayList<PExpression>();
- FormalParamNode p = n.getBdedQuantSymbolLists()[0][0];
- list.add(createIdentifierNode(p));
+ List<PExpression> list2 = new ArrayList<PExpression>();
+ for (int i = 0; i < params[0].length; i++) {
+ FormalParamNode p = params[0][i];
+ list.add(createIdentifierNode(p));
+ list2.add(createIdentifierNode(p));
+ }
AComprehensionSetExpression compre = new AComprehensionSetExpression();
compre.setIdentifiers(list);
AMemberPredicate member = new AMemberPredicate();
- member.setLeft(createIdentifierNode(p));
+ if (list2.size() == 1) {
+ member.setLeft(list2.get(0));
+ } else {
+ member.setLeft(new ACoupleExpression(list2));
+ }
+
ExprNode in = n.getBdedQuantBounds()[0];
member.setRight(visitExprNodeExpression(in));
@@ -1296,7 +1370,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
case OPCODE_fc: // Represents [x \in S |-> e].
case OPCODE_rfs: {
FormalParamNode[][] params = n.getBdedQuantSymbolLists();
- //ExprNode[] bounds = n.getBdedQuantBounds(); TODO
+ // ExprNode[] bounds = n.getBdedQuantBounds(); TODO
List<PExpression> idList = new ArrayList<PExpression>();
List<PPredicate> predList = new ArrayList<PPredicate>();
for (int i = 0; i < params.length; i++) {
@@ -1517,7 +1591,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
return rec;
} else {
- //FunctionType func = (FunctionType) type;
+ // FunctionType func = (FunctionType) type;
List<PExpression> list = new ArrayList<PExpression>();
for (int i = 1; i < n.getArgs().length; i++) {
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index fb81ace48886a75b0a82d7a05430200f6e5e24ca..4d62bcc7f348fa5728226c7955498e1844c58791 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -24,6 +24,7 @@ import de.tla2b.exceptions.TLA2BException;
import de.tla2b.global.TranslationGlobals;
import de.tla2b.output.ASTPrettyPrinter;
import de.tla2b.pprint.BMachinePrinter;
+import de.tla2b.translation.BMacroHandler;
import tla2sany.drivers.SANY;
import tla2sany.modanalyzer.SpecObj;
import tla2sany.semantic.ModuleNode;
@@ -211,9 +212,9 @@ public class Translator implements TranslationGlobals {
moduleNode, specAnalyser);
- //BMacroHandler bMacroHandler = new BMacroHandler(specAnalyser, conEval);
+ BMacroHandler bMacroHandler = new BMacroHandler(specAnalyser, conEval);
BAstCreator bAstCreator = new BAstCreator(moduleNode, conEval,
- specAnalyser, usedExternalFunctions, predicateVsExpression);
+ specAnalyser, usedExternalFunctions, predicateVsExpression, bMacroHandler);
this.BAst = bAstCreator.getStartNode();
this.bDefinitions = bAstCreator.getBDefinitions();
return BAst;
diff --git a/src/test/java/de/tla2b/examples/MCTest.java b/src/test/java/de/tla2b/examples/MCTest.java
index f8bad910022269da67bf7241cb8065f99e16d4da..c70a1d5aa0871f453dc6874a8a3b03d5d8bb6242 100644
--- a/src/test/java/de/tla2b/examples/MCTest.java
+++ b/src/test/java/de/tla2b/examples/MCTest.java
@@ -94,4 +94,22 @@ public class MCTest {
String file = "src/test/resources/MCTests/Queens/MC.tla";
runModule(file);
}
+
+ @Test
+ public void testSumAndProduct() throws Exception {
+ String file = "src/test/resources/examples/SumAndProduct/SumAndProductTransition.tla";
+ runModule(file);
+ }
+
+ @Test
+ public void testMacroTest() throws Exception {
+ String file = "src/test/resources/renamer/MacroTest/MacroTest.tla";
+ runModule(file);
+ }
+
+ @Test
+ public void testSumAndProductConstraint() throws Exception {
+ String file = "src/test/resources/examples/SumAndProduct/SumAndProductConstraint.tla";
+ runModule(file);
+ }
}
diff --git a/src/test/java/de/tla2b/prettyprintb/MacroTest.java b/src/test/java/de/tla2b/prettyprintb/MacroTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..8a216417b5456d45528621221f14600f9fcff9a8
--- /dev/null
+++ b/src/test/java/de/tla2b/prettyprintb/MacroTest.java
@@ -0,0 +1,104 @@
+package de.tla2b.prettyprintb;
+
+import static de.tla2b.util.TestUtil.compare;
+
+import org.junit.Test;
+
+public class MacroTest {
+
+
+ @Test
+ public void testRenaming1() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "def(y) == \\A x \\in {1}: y = 3 \n"
+ + "ASSUME \\E x \\in {3}: def(x) \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "DEFINITIONS def(y) == !(x_1).(x_1 : {1} => y = 3); "
+ + "PROPERTIES #(x).(x : {3} & def(x)) \n" + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testRenaming2() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "def(y) == \\A x \\in {1}: y = 3 \n"
+ + "ASSUME \\E x \\in {2}: def(x+1) \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "DEFINITIONS def(y) == !(x_1).(x_1 : {1} => y = 3); "
+ + "PROPERTIES #(x).(x : {2} & def(x+1)) \n" + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testRenaming3() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "foo(a) == a \n"
+ + "def(y) == \\A x \\in {1}: y = 3 \n"
+ + "ASSUME \\E x \\in {2}: foo(def(x)) \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "DEFINITIONS foo(a) == a; \n"
+ + "def(y) == !(x_1).(x_1 : {1} => y = 3) \n"
+ + "PROPERTIES #(x).(x : {2} & foo(bool(def(x))) = TRUE) \n" + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testRenaming4() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "def(y) == \\A x \\in {1}: y = 3 \n"
+ + "foo == \\E x \\in {2}: def(x) \n"
+ + "ASSUME foo \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "DEFINITIONS \n"
+ + "def(y) == !(x_1).(x_1 : {1} => y = 3); \n"
+ + "foo == #(x).(x : {2} & def(x)); \n"
+ + "PROPERTIES foo \n" + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testRenaming5() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "def(y) == \\A x \\in {1}: y = 3 \n"
+ + "foo(x) == def(x) \n"
+ + "ASSUME \\E x \\in {2}: foo(x) \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "DEFINITIONS \n"
+ + "def(y) == !(x_1).(x_1 : {1} => y = 3); \n"
+ + "foo(x) == def(x); \n"
+ + "PROPERTIES #(x).(x : {2} & foo(x)) \n" + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testRenamingGlobal() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "def(y) == \\A x \\in {1}: y = 3 \n"
+ + "CONSTANTS x\n"
+ + "ASSUME x = 3 /\\ def(x) \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "DEFINITIONS \n"
+ + "def(y) == !(x_1).(x_1 : {1} => y = 3); \n"
+ + "ABSTRACT_CONSTANTS x\n"
+ + "PROPERTIES x : INTEGER & (x = 3 & def(x)) \n" + "END";
+ compare(expected, module);
+ }
+
+}
diff --git a/src/test/java/de/tla2b/prettyprintb/RecursiveDefinitionTest.java b/src/test/java/de/tla2b/prettyprintb/RecursiveDefinitionTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..00e01859d48698d11e0a66b4e0c10a3fe2bd24df
--- /dev/null
+++ b/src/test/java/de/tla2b/prettyprintb/RecursiveDefinitionTest.java
@@ -0,0 +1,50 @@
+package de.tla2b.prettyprintb;
+
+import static de.tla2b.util.TestUtil.compare;
+
+import org.junit.Ignore;
+import org.junit.Test;
+
+public class RecursiveDefinitionTest {
+
+ @Ignore
+ @Test
+ public void testRecursiveDefinition() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "RECURSIVE sum(_) \n"
+ + "sum(S) == IF S = {} THEN 0 ELSE (LET x == CHOOSE a \\in S : TRUE IN x + sum(S \\ {x})) \n"
+ + "ASSUME sum({1,2,3}) = 6 \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);
+
+ }
+
+ @Ignore
+ @Test
+ public void testRecursiveDefinition2() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "RECURSIVE Sum(_,_) \n"
+ + " Sum(f,S) == IF S = {} THEN 0 \n"
+ + " ELSE LET x == CHOOSE x \\in S : TRUE \n"
+ + " IN f[x] + Sum(f, S \\ {x}) \n"
+ + "foo[x \\in Nat] == x \n"
+ + "ASSUME Sum(foo, {1,2,3}) = 6 \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
+ + "PROPERTIES "
+ + " k = k <+ {TRUE |-> 0, FALSE |-> 0}" + "END";
+ compare(expected, module);
+
+ }
+
+
+
+}
diff --git a/src/test/java/de/tla2b/prettyprintb/RecursiveFunctionTest.java b/src/test/java/de/tla2b/prettyprintb/RecursiveFunctionTest.java
index 298c66e94920edef265dd3cd1eec5e746feef9e6..df0cdc6df06653ed79002ec7fa0c9837639d7b74 100644
--- a/src/test/java/de/tla2b/prettyprintb/RecursiveFunctionTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/RecursiveFunctionTest.java
@@ -6,15 +6,14 @@ import org.junit.Ignore;
import org.junit.Test;
public class RecursiveFunctionTest {
-
+
@Ignore
@Test
public void testRecursiveDefinition() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
- + "RECURSIVE sum(_) \n"
- + "sum(S) == IF S = {} THEN 0 ELSE (LET x == CHOOSE a \\in S : TRUE IN x + sum(S \\ {x})) \n"
- + "ASSUME sum({1,2,3}) = 6 \n"
+ + "sum[S \\in SUBSET(Nat)] == IF S = {} THEN 0 ELSE LET x == CHOOSE a \\in S : TRUE IN x + sum[S \\ {x}] \n"
+ + "ASSUME sum[{1,2,3}] = 6 \n"
+ "=================================";
final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
@@ -24,27 +23,4 @@ public class RecursiveFunctionTest {
compare(expected, module);
}
-
- @Ignore
- @Test
- public void testRecursiveDefinition2() throws Exception {
- final String module = "-------------- MODULE Testing ----------------\n"
- + "EXTENDS Naturals \n"
- + "RECURSIVE Sum(_,_) \n"
- + " Sum(f,S) == IF S = {} THEN 0 \n"
- + " ELSE LET x == CHOOSE x \\in S : TRUE \n"
- + " IN f[x] + Sum(f, S \\ {x}) \n"
- + "foo[x \\in Nat] == x \n"
- + "ASSUME Sum(foo, {1,2,3}) = 6 \n"
- + "=================================";
-
- final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
- + "PROPERTIES "
- + " k = k <+ {TRUE |-> 0, FALSE |-> 0}" + "END";
- compare(expected, module);
-
- }
-
-
-
}
diff --git a/src/test/java/de/tla2b/prettyprintb/SetsTest.java b/src/test/java/de/tla2b/prettyprintb/SetsTest.java
index c795eeb1ecf471267c5567d9418664de4797da59..3aa124e52abb19eb1d797a47ed239a785befa289 100644
--- a/src/test/java/de/tla2b/prettyprintb/SetsTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/SetsTest.java
@@ -171,6 +171,18 @@ public class SetsTest {
+ "END";
compare(expected, module);
}
+
+ @Test
+ public void testConstructor3() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "ASSUME {<<1,2>>} = {<<x, y>> \\in {1} \\X {2}: TRUE} \n"
+ + "=================================";
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES {(1,2)} = {(x, y)| (x,y) : {1} * {2} & TRUE = TRUE} \n"
+ + "END";
+ compare(expected, module);
+ }
@Test
diff --git a/src/test/java/de/tla2b/util/TestUtil.java b/src/test/java/de/tla2b/util/TestUtil.java
index ff6e2832443034006a81432e967cb36ba4dd840c..ed216ee08e6f51deea8f6e34181fb24027049238 100644
--- a/src/test/java/de/tla2b/util/TestUtil.java
+++ b/src/test/java/de/tla2b/util/TestUtil.java
@@ -65,7 +65,7 @@ public class TestUtil {
System.out.println("-------------------");
assertEquals(result, ppResult);
- System.out.println(t.getBDefinitions().getDefinitionNames());
+ //System.out.println(t.getBDefinitions().getDefinitionNames());
}
public static void compare(String bMachine, String tlaModule) throws BException, TLA2BException{
diff --git a/src/test/resources/examples/FastPaxos/FastPaxos.tla b/src/test/resources/examples/FastPaxos/FastPaxos.tla
deleted file mode 100644
index f2494dffbae85a751c3936fa54f393442ff9c00b..0000000000000000000000000000000000000000
--- a/src/test/resources/examples/FastPaxos/FastPaxos.tla
+++ /dev/null
@@ -1,210 +0,0 @@
------------------------------- MODULE FastPaxos -----------------------------
-CONSTANTS PVal, Acceptor, FastNum, ClassicNum, Quorum(_), _\prec_, NextNum(_)
-
-i \preceq j == (i \prec j) \/ (i = j)
-
-Max(S) == CHOOSE i \in S : \A j \in S : j \preceq i
-
-RNum == FastNum \cup ClassicNum
-
-ASSUME
- /\ FastNum \cap ClassicNum = {}
- /\ \A i, j, k \in RNum : (i \prec j) /\ (j \prec k) => (i \prec k)
- /\ \A i \in RNum : ~(i \prec i)
- /\ \A i, j \in RNum : (i \preceq j) \/ (j \preceq i)
- /\ (0 \notin RNum) /\ \A i \in RNum : 0 \prec i
- /\ \A i \in FastNum : NextNum(i) \in RNum =>
- ~\E j \in RNum : (i \prec j) /\ (j \prec NextNum(i))
-
-R3 == \A i, j \in RNum :
- \A Q \in Quorum(i), R \in Quorum(j) : Q \cap R # {}
-R5b == \A i, j \in RNum :
- (j \in FastNum) => \A Q \in Quorum(i), R1, R2 \in Quorum(j) :
- Q \cap R1 \cap R2 # {}
-
-ASSUME
- /\ \A i \in RNum : Quorum(i) \subseteq SUBSET Acceptor
- /\ R3 /\ R5b
-
-any == CHOOSE v : v \notin PVal
-
-Message ==
- [type : {"propose"}, pval : PVal]
- \cup [type : {"phase1a"}, rnd : RNum]
- \cup [type : {"phase1b"}, rnd : RNum, vrnd : RNum \cup {0},
- pval : PVal \cup {any}, acc : Acceptor]
- \cup [type : {"phase2a"}, rnd : RNum, pval : PVal \cup {any}]
- \cup [type : {"phase2b"}, rnd : RNum, pval : PVal, acc : Acceptor]
-
-
-VARIABLES rnd, vrnd, pval, sentMsg, learned
-vars == <<rnd, vrnd, pval, sentMsg, learned>>
-
-TypeOK ==
- /\ rnd \in [Acceptor -> RNum \cup {0}]
- /\ vrnd \in [Acceptor -> RNum \cup {0}]
- /\ pval \in [Acceptor -> PVal \cup {any}]
- /\ sentMsg \in SUBSET Message
- /\ learned \in SUBSET PVal
-
-Init ==
- /\ rnd = [a \in Acceptor |-> 0]
- /\ vrnd = [a \in Acceptor |-> 0]
- /\ pval = [a \in Acceptor |-> any]
- /\ sentMsg = {}
- /\ learned = {}
------------------------------------------------------------------------------
-Send(m) == sentMsg' = sentMsg \cup {m}
-
-Propose(v) ==
- /\ Send([type |-> "propose", pval |-> v])
- /\ UNCHANGED <<rnd, vrnd, pval, learned>>
-
-Phase1a(i) ==
- /\ Send([type |-> "phase1a", rnd |-> i])
- /\ UNCHANGED <<rnd, vrnd, pval, learned>>
-
-Phase1b(a, i) ==
- /\ rnd[a] \prec i
- /\ \E m \in sentMsg : (m.type = "phase1a") /\ (m.rnd = i)
- /\ rnd' = [rnd EXCEPT ![a] = i]
- /\ Send([type |-> "phase1b", rnd |-> i, vrnd |-> vrnd[a], pval |-> pval[a],
- acc |-> a])
- /\ UNCHANGED <<vrnd, pval, learned>>
-
-P1bMsg(Q, i) ==
- {m \in sentMsg : (m.type = "phase1b") /\ (m.acc \in Q) /\ (m.rnd = i)}
-
-SafeSet(M, Q, i) ==
- LET k == Max({m.vrnd : m \in M})
- Vk == {m.pval : m \in {mm \in M : mm.vrnd = k}}
- Only(v) == \/ Vk = {v}
- \/ /\ k \in FastNum
- /\ \E R \in Quorum(k) :
- \A a \in Q \cap R :
- \E m \in M : /\ m.vrnd = k
- /\ m.pval = v
- /\ m.acc = a
- IN IF k = 0
- THEN PVal
- ELSE IF \E v \in Vk : Only(v)
- THEN {CHOOSE v \in Vk : Only(v)}
- ELSE PVal
-
-Phase2a(i, va) ==
- /\ ~\E m \in sentMsg : (m.type = "phase2a") /\ (m.rnd = i)
- /\ \E Q \in Quorum(i) :
- /\ \A a \in Q : \E m \in sentMsg : /\ m.type = "phase1b"
- /\ m.rnd = i
- /\ m.acc = a
- /\ \/ /\ va \in SafeSet(P1bMsg(Q,i), Q, i)
- /\ \E m \in sentMsg : /\ m.type \in {"propose", "phase1b"}
- /\ m.pval = va
- \/ /\ SafeSet(P1bMsg(Q,i), Q, i) = PVal
- /\ i \in FastNum
- /\ va = any
- /\ Send([type |-> "phase2a", rnd |-> i, pval |-> va])
- /\ UNCHANGED <<rnd, vrnd, pval, learned>>
-
-Phase2b(i, a, v) ==
- /\ rnd[a] \preceq i
- /\ vrnd[a] \prec i
- /\ \E m \in sentMsg :
- /\ m.type = "phase2a"
- /\ m.rnd = i
- /\ \/ m.pval = v
- \/ /\ m.pval = any
- /\ \E mm \in sentMsg : (mm.type = "propose") /\ (mm.pval = v)
- /\ rnd' = [rnd EXCEPT ![a] = i]
- /\ vrnd' = [vrnd EXCEPT ![a] = i]
- /\ pval' = [pval EXCEPT ![a] = v]
- /\ Send([type |-> "phase2b", rnd |-> i, pval |-> v, acc |-> a])
- /\ UNCHANGED learned
-
-Learn(v) ==
- /\ \E i \in RNum :
- \E Q \in Quorum(i) :
- \A a \in Q :
- \E m \in sentMsg : /\ m.type = "phase2b"
- /\ m.rnd = i
- /\ m.pval = v
- /\ m.acc = a
- /\ learned' = learned \cup {v}
- /\ UNCHANGED <<rnd, vrnd, pval, sentMsg>>
------------------------------------------------------------------------------
-P2bToP1b(Q, i) ==
- LET iMsg ==
- {m \in sentMsg : (m.type = "phase2b") /\ (m.rnd = i) /\ (m.acc \in Q)}
- IN {[type |-> "phase1b", rnd |-> NextNum(i), vrnd |-> i,
- pval |-> m.pval, acc |-> m.acc] : m \in iMsg}
-
-LeaderRecovery(i, v) ==
- /\ ~\E m \in sentMsg : (m.type = "phase2a") /\ (m.rnd = NextNum(i))
- /\ \E Q \in Quorum(i) :
- /\ \A a \in Q : \E m \in P2bToP1b(Q, i) : m.acc = a
- /\ v \in SafeSet(P2bToP1b(Q, i), Q, NextNum(i))
- /\ \E m \in P2bToP1b(Q, i) : m.pval = v
- /\ Send([type |-> "phase2a", rnd |-> NextNum(i), pval |-> v])
- /\ UNCHANGED <<rnd, vrnd, pval, learned>>
-
-LeaderlessRecovery(i, a, v) ==
- /\ NextNum(i) \in FastNum
- /\ rnd[a] = i
- /\ vrnd[a] = i
- /\ \E Q \in Quorum(i) :
- /\ \A b \in Q : \E m \in P2bToP1b(Q, i) : m.acc = b
- /\ v \in SafeSet(P2bToP1b(Q, i), Q, NextNum(i))
- /\ \E m \in P2bToP1b(Q, i): m.pval = v
- /\ rnd' = [rnd EXCEPT ![a] = NextNum(i)]
- /\ vrnd' = [vrnd EXCEPT ![a] = NextNum(i)]
- /\ pval' = [pval EXCEPT ![a] = v]
- /\ Send([type |-> "phase2b", rnd |-> NextNum(i), pval |-> v, acc |-> a])
- /\ UNCHANGED learned
-
-
------------------------------------------------------------------------------
-Next ==
- \/ \E v \in PVal : Propose(v) \/ Learn(v)
- \/ \E i \in RNum : \/ Phase1a(i)
- \/ \E a \in Acceptor : \/ Phase1b(a, i)
- \/ \E v \in PVal : Phase2b(i, a, v)
- \/ \E va \in PVal \cup {any} : Phase2a(i, va)
- (*\/ \E i \in FastNum, v \in PVal :
- \/ LeaderRecovery(i, v)
- \/ \E a \in Acceptor :LeaderlessRecovery(i, a, v)*)
-
-Spec == Init /\ [][Next]_vars
-
-VotedForIn(a, v, i) ==
- \E m \in sentMsg : /\ m.type = "phase2b"
- /\ m.acc = a
- /\ m.pval = v
- /\ m.rnd = i
-
-VotedorAbstainedIn(a, i) ==
- \/ \E v \in PVal : VotedForIn(a, v, i)
- \/ i \prec rnd[a]
-
-R1 == \A m \in sentMsg :
- (m.type = "phase2b") => \E mm \in sentMsg : /\ mm.type = "propose"
- /\ mm.pval = m.pval
-
-R2 == \A a \in Acceptor, v1, v2 \in PVal, i \in RNum :
- VotedForIn(a, v1, i) /\ VotedForIn(a, v2, i) => (v1 = v2)
-
-ChooseableIn(v, i) ==
- \E Q \in Quorum(i) :
- \A a \in Q : (~ VotedorAbstainedIn(a, i)) \/ VotedForIn(a, v, i)
-
-NOC(v, i) == \A w \in PVal : ChooseableIn(w, i) => (w = v)
-
-SafeIn(v, i) == \A j \in RNum : (j \prec i) => NOC(v, j)
-
-R4 == \A a \in Acceptor, v \in PVal, i \in RNum :
- VotedForIn(a, v, i) => SafeIn(v, i)
-
-R5a == \A j \in ClassicNum :
- \A a1, a2 \in Acceptor :
- \A v1, v2 \in PVal :
- VotedForIn(a1, v1, j) /\ VotedForIn(a2, v2, j) => (v1 = v2)
-=============================================================================
diff --git a/src/test/resources/examples/FastPaxos/MCFastPaxos.cfg b/src/test/resources/examples/FastPaxos/MCFastPaxos.cfg
deleted file mode 100644
index 7988268bf808945b1ee5c763df8f5d3b7def732d..0000000000000000000000000000000000000000
--- a/src/test/resources/examples/FastPaxos/MCFastPaxos.cfg
+++ /dev/null
@@ -1,13 +0,0 @@
-CONSTANTS
- ClassicNum = {1,3}
- FastNum = {2}
- Acceptor = {a1,a2,a3}
- PVal = {v1,v2}
- Quorum <- MCQuorum
- any =[FastPaxos] any
- a1=a1 a2=a2 a3=a3 v1=v1 v2=v2
-
-SPECIFICATION Spec
-INVARIANT TypeOK Correctness \* R1 R2 R4 R5a
-
-
diff --git a/src/test/resources/examples/FastPaxos/MCFastPaxos.tla b/src/test/resources/examples/FastPaxos/MCFastPaxos.tla
deleted file mode 100644
index e1cd84b489711c5ebaf80f45be6b2145a426eed4..0000000000000000000000000000000000000000
--- a/src/test/resources/examples/FastPaxos/MCFastPaxos.tla
+++ /dev/null
@@ -1,25 +0,0 @@
------------------------------ MODULE MCFastPaxos ----------------------------
-EXTENDS FiniteSets, Naturals
-
-CONSTANTS PVal, Acceptor, FastNum, ClassicNum, Quorum(_) \* , _\prec_
-VARIABLES rnd, vrnd, pval, sentMsg, learned
-
-NextNum(a) == IF a+1 \in FastNum \cup ClassicNum THEN a+1 ELSE 0
-
-INSTANCE FastPaxos WITH \prec <- <
-CONSTANTS a1, a2, a3, v1, v2
-
-MCQuorum(i) == IF i \in ClassicNum THEN {{a1,a2}, {a1,a3}, {a2, a3}}
- ELSE {{a1,a2,a3}}
-Correctness ==
- /\ Cardinality(learned) \leq 1
- /\ \A v \in learned : \E m \in sentMsg : /\ m.type = "propose"
- /\ m.pval = v
-TSpec == Init /\ [][Next]_vars
-
-(*
-TInit ==
-
-TSpec == TInit /\ [][Next]_vars
-*)
-=============================================================================
diff --git a/src/test/resources/examples/SumAndProduct/SumAndProductConstraint.tla b/src/test/resources/examples/SumAndProduct/SumAndProductConstraint.tla
new file mode 100644
index 0000000000000000000000000000000000000000..2472c5b259793e95aa32994682b4938c7ea1da66
--- /dev/null
+++ b/src/test/resources/examples/SumAndProduct/SumAndProductConstraint.tla
@@ -0,0 +1,56 @@
+------------------------- MODULE SumAndProductConstraint -------------------------
+(****************************************************************************)
+(* This module formalizes the "sum and product" puzzle, due to Freudenthal *)
+(* (1969), and which goes as follows: *)
+(* J says to S and P: I have chosen two integers x and y such that *)
+(* 1 < x <= y < 100. In a moment, I will inform S only of the sum x+y *)
+(* and P only of the product x*y. These announcements remain private. *)
+(* You are required to determine the pair (x,y). He acts as said. *)
+(* The following conversation now takes place: *)
+(* 1. P says: "I don't know it." *)
+(* 2. S says: "I knew you didn't." *)
+(* 3. P says: "Now I know it." *)
+(* 4. S says: "I now also know it." *)
+(* Determine the pair (x,y). *)
+(* In fact, the first announcement is implied by the second one, so we will *)
+(* not take it into account in the following formal. *)
+(****************************************************************************)
+
+EXTENDS Naturals, FiniteSets, TLC
+
+Pairs == { <<i,j>> \in (2 .. 99) \X (2 .. 99) : i <= j }
+
+(* S and P can only observe the sum and product of a pair of numbers *)
+obsS(i,j) == i+j
+obsP(i,j) == i*j
+
+equivS(i,j,k,l) == obsS(i,j) = obsS(k,l)
+equivP(i,j,k,l) == obsP(i,j) = obsP(k,l)
+
+(* Assertions are formalized as sets of pairs, and a "world" is a pair.
+ S and P know an assertion A in world <<i,j>> \in W if all worlds in W
+ equivalent to (i,j) satisfy A. *)
+knowsS(W,i,j,A) == \A <<k,l>> \in W : equivS(i,j,k,l) => <<k,l>> \in A
+knowsP(W,i,j,A) == \A <<k,l>> \in W : equivP(i,j,k,l) => <<k,l>> \in A
+
+(* S and P know that A is false in world <<i,j>> if no world equivalent to
+ (i,j) satisfies A. *)
+knowsS_neg(W,i,j,A) == \A <<k,l>> \in W : equivS(i,j,k,l) => <<k,l>> \notin A
+knowsP_neg(W,i,j,A) == \A <<k,l>> \in W : equivP(i,j,k,l) => <<k,l>> \notin A
+
+(* worlds in which P can identify the pair uniquely *)
+knowP_pair == { <<i,j>> \in Pairs : knowsP(Pairs, i,j, {<<i,j>>}) }
+(* worlds in which S knows that P cannot know the pair *)
+Step2 == { <<i,j>> \in Pairs : knowsS_neg(Pairs, i,j, knowP_pair) }
+(* filter out worlds in Step2 for which P now knows the pair uniquely *)
+Step3 == { <<i,j>> \in Step2 : knowsP(Step2, i,j, {<<i,j>>}) }
+(* now restrict to worlds in Step3 for which also S knows the pair uniquely *)
+Step4 == { <<i,j>> \in Step3 : knowsS(Step3, i,j, {<<i,j>>}) }
+
+CONSTANTS k
+ASSUME k = Step4
+
+==================================================================================
+\* Modification History
+\* Last modified Mon Apr 22 11:02:28 CEST 2013 by merz
+\* Created Sun Apr 21 19:19:53 CEST 2013 by merz
diff --git a/src/test/resources/renamer/MacroTest/MacroTest.cfg b/src/test/resources/renamer/MacroTest/MacroTest.cfg
new file mode 100644
index 0000000000000000000000000000000000000000..4fc3c0fe9718a752b2bf2a21b6a8e756c02ae4e5
--- /dev/null
+++ b/src/test/resources/renamer/MacroTest/MacroTest.cfg
@@ -0,0 +1,2 @@
+INIT Init
+INVARIANT Invariant
\ No newline at end of file
diff --git a/src/test/resources/renamer/MacroTest/MacroTest.tla b/src/test/resources/renamer/MacroTest/MacroTest.tla
new file mode 100644
index 0000000000000000000000000000000000000000..a91f3be13728882e69a11f32379f42c98763e144
--- /dev/null
+++ b/src/test/resources/renamer/MacroTest/MacroTest.tla
@@ -0,0 +1,9 @@
+---- MODULE MacroTest ----
+EXTENDS Integers
+egt(x) == \E y \in Nat \ {0}: y<100 /\ x<y
+egt2(x) == \E yy \in Nat \ {0}: yy<100 /\ x<yy
+VARIABLES y
+Invariant == y \in Int /\ egt(y+1) (* is false ! *)
+ /\ egt2(y+1) (* is true *)
+Init == y = 5
+======
\ No newline at end of file