diff --git a/src/main/java/de/tla2b/analysis/BOperation.java b/src/main/java/de/tla2b/analysis/BOperation.java
index ee9a4d89c6114338debcb4c70dd27fc1a778dc82..2a0a2e8d992a6a5e22b35a7b520be41a585190ad 100644
--- a/src/main/java/de/tla2b/analysis/BOperation.java
+++ b/src/main/java/de/tla2b/analysis/BOperation.java
@@ -4,16 +4,35 @@
package de.tla2b.analysis;
-
import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.HashSet;
+import java.util.Hashtable;
+import java.util.LinkedHashMap;
+import java.util.List;
+import java.util.Map.Entry;
+import java.util.Set;
+import de.be4.classicalb.core.parser.node.AAnySubstitution;
+import de.be4.classicalb.core.parser.node.AAssignSubstitution;
+import de.be4.classicalb.core.parser.node.ABlockSubstitution;
+import de.be4.classicalb.core.parser.node.AMemberPredicate;
+import de.be4.classicalb.core.parser.node.AOperation;
+import de.be4.classicalb.core.parser.node.ASelectSubstitution;
+import de.be4.classicalb.core.parser.node.ASkipSubstitution;
+import de.be4.classicalb.core.parser.node.PExpression;
+import de.be4.classicalb.core.parser.node.PPredicate;
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.TranslationGlobals;
+import de.tla2b.types.TLAType;
+import de.tla2bAst.BAstCreator;
import tla2sany.semantic.ASTConstants;
import tla2sany.semantic.ExprNode;
+import tla2sany.semantic.ExprOrOpArgNode;
import tla2sany.semantic.FormalParamNode;
import tla2sany.semantic.LetInNode;
import tla2sany.semantic.OpApplNode;
+import tla2sany.semantic.OpDeclNode;
import tla2sany.semantic.OpDefNode;
import tla2sany.semantic.SemanticNode;
import tla2sany.semantic.SubstInNode;
@@ -21,21 +40,217 @@ import tla2sany.semantic.SymbolNode;
import tlc2.tool.BuiltInOPs;
import tlc2.tool.ToolGlobals;
-public class BOperation implements ASTConstants, ToolGlobals, TranslationGlobals {
- private String name;
- private ExprNode node;
- private ArrayList<OpApplNode> existQuans;
+public class BOperation extends BuiltInOPs implements ASTConstants,
+ ToolGlobals, TranslationGlobals {
+ private final String name;
+ private final ExprNode node;
+ private final ArrayList<OpApplNode> existQuans;
private ArrayList<String> opParams;
private ArrayList<FormalParamNode> formalParams;
private ArrayList<String> unchangedVariables;
+ private final ArrayList<OpDeclNode> unchangedVariablesList;
+ private final ArrayList<ExprOrOpArgNode> guards;
+ private final ArrayList<ExprOrOpArgNode> beforeAfterPredicates;
+ private LinkedHashMap<SymbolNode, ExprOrOpArgNode> assignments = new LinkedHashMap<SymbolNode, ExprOrOpArgNode>();
+ private List<OpDeclNode> anyVariables;
+
+ final int SUBSTITUTE_PARAM = 29;
public BOperation(String name, ExprNode n,
- ArrayList<OpApplNode> existQuans) {
+ ArrayList<OpApplNode> existQuans, SpecAnalyser specAnalyser) {
this.name = name;
this.node = n;
this.existQuans = existQuans;
+ this.unchangedVariablesList = new ArrayList<OpDeclNode>();
+ this.guards = new ArrayList<ExprOrOpArgNode>();
+ this.beforeAfterPredicates = new ArrayList<ExprOrOpArgNode>();
+ anyVariables = new ArrayList<OpDeclNode>(Arrays.asList(specAnalyser
+ .getModuleNode().getVariableDecls()));
+
evalParams();
findUnchangedVariables();
+ separateGuardsAndBeforeAfterPredicates(node);
+ findAssignments();
+ }
+
+ public AOperation getBOperation(BAstCreator bASTCreator) {
+
+ AOperation operation = new AOperation();
+ List<PExpression> paramList = new ArrayList<PExpression>();
+ ArrayList<PPredicate> whereList = new ArrayList<PPredicate>();
+ for (int j = 0; j < this.getFormalParams().size(); j++) {
+ paramList.add(bASTCreator.createIdentifierNode(this
+ .getFormalParams().get(j)));
+ }
+ for (int j = 0; j < this.getExistQuans().size(); j++) {
+ OpApplNode o = this.getExistQuans().get(j);
+ whereList.add(bASTCreator.visitBounded(o));
+ }
+
+ operation.setOpName(BAstCreator.createTIdentifierLiteral(name));
+ operation.setParameters(paramList);
+ operation.setReturnValues(new ArrayList<PExpression>());
+
+ for (ExprOrOpArgNode g : guards) {
+ whereList.add(bASTCreator.visitExprOrOpArgNodePredicate(g));
+ }
+
+ ArrayList<PExpression> left = new ArrayList<PExpression>();
+ ArrayList<PExpression> right = new ArrayList<PExpression>();
+ for (Entry<SymbolNode, ExprOrOpArgNode> entry : assignments.entrySet()) {
+ left.add(bASTCreator.createIdentifierNode(entry.getKey()));
+ right.add(bASTCreator.visitExprOrOpArgNodeExpression(entry
+ .getValue()));
+ }
+ AAssignSubstitution assign = new AAssignSubstitution();
+
+ if (anyVariables.size() > 0) { // ANY x_n WHERE P THEN A END
+ AAnySubstitution any = new AAnySubstitution();
+ any = new AAnySubstitution();
+ List<PExpression> anyParams = new ArrayList<PExpression>();
+ for (OpDeclNode var : anyVariables) {
+ String varName = var.getName().toString();
+ String nextName = varName + "_n";
+ anyParams.add(BAstCreator.createIdentifierNode(nextName));
+
+ AMemberPredicate member = new AMemberPredicate();
+ member.setLeft(BAstCreator.createIdentifierNode(nextName));
+ TLAType t = (TLAType) var.getToolObject(TYPE_ID);
+ member.setRight(t.getBNode());
+ whereList.add(member);
+ left.add(bASTCreator.createIdentifierNode(var));
+ right.add(BAstCreator.createIdentifierNode(nextName));
+ }
+ any.setIdentifiers(anyParams);
+ whereList.addAll(createBeforeAfterPredicates(bASTCreator));
+ any.setWhere(bASTCreator.createConjunction(whereList));
+ any.setThen(assign);
+ operation.setOperationBody(any);
+ } else if (whereList.size() > 0) { // SELECT P THEN A END
+ ASelectSubstitution select = new ASelectSubstitution();
+ whereList.addAll(createBeforeAfterPredicates(bASTCreator));
+ for (ExprOrOpArgNode e : beforeAfterPredicates) {
+ whereList.add(bASTCreator.visitExprOrOpArgNodePredicate(e));
+ }
+ select.setCondition(bASTCreator.createConjunction(whereList));
+ select.setThen(assign);
+ operation.setOperationBody(select);
+ } else { // BEGIN A END
+ ABlockSubstitution block = new ABlockSubstitution(assign);
+ operation.setOperationBody(block);
+ }
+
+ if (left.size() > 0) {
+ assign.setLhsExpression(left);
+ assign.setRhsExpressions(right);
+ } else { // skip
+ assign.replaceBy(new ASkipSubstitution());
+ }
+
+ return operation;
+ }
+
+ private ArrayList<PPredicate> createBeforeAfterPredicates(
+ BAstCreator bAstCreator) {
+ ArrayList<PPredicate> predicates = new ArrayList<PPredicate>();
+ for (ExprOrOpArgNode e : beforeAfterPredicates) {
+ PPredicate body = null;
+ if (e instanceof OpApplNode) {
+ OpApplNode opApplNode = (OpApplNode) e;
+ if (opApplNode.getOperator().getKind() == UserDefinedOpKind
+ && !BBuiltInOPs.contains(opApplNode.getOperator()
+ .getName())) {
+ OpDefNode def = (OpDefNode) opApplNode.getOperator();
+ FormalParamNode[] params = def.getParams();
+ for (int j = 0; j < params.length; j++) {
+ FormalParamNode param = params[j];
+ param.setToolObject(SUBSTITUTE_PARAM,
+ opApplNode.getArgs()[j]);
+ }
+ body = bAstCreator.visitExprNodePredicate(def.getBody());
+ }
+ }
+ if (body == null) {
+ body = bAstCreator.visitExprOrOpArgNodePredicate(e);
+ }
+ predicates.add(body);
+ }
+ return predicates;
+ }
+
+ private void findAssignments() {
+ PrimedVariablesFinder primedVariablesFinder = new PrimedVariablesFinder(
+ beforeAfterPredicates);
+ for (ExprOrOpArgNode node : new ArrayList<ExprOrOpArgNode>(
+ beforeAfterPredicates)) {
+ if (node instanceof OpApplNode) {
+ OpApplNode opApplNode = (OpApplNode) node;
+ if (opApplNode.getOperator().getKind() == BuiltInKind) {
+ switch (getOpCode(opApplNode.getOperator().getName())) {
+ case OPCODE_eq: {
+ ExprOrOpArgNode arg1 = opApplNode.getArgs()[0];
+ try {
+ OpApplNode arg11 = (OpApplNode) arg1;
+ if (getOpCode(arg11.getOperator().getName()) == OPCODE_prime) {
+ OpApplNode v = (OpApplNode) arg11.getArgs()[0];
+ SymbolNode var = v.getOperator();
+ if (!primedVariablesFinder
+ .getTwiceUsedVariables().contains(var)) {
+ // var is only used once in all before after
+ // predicates
+ assignments.put(v.getOperator(),
+ opApplNode.getArgs()[1]);
+ beforeAfterPredicates.remove(node);
+ }
+
+ }
+ } catch (ClassCastException e) {
+
+ }
+
+ }
+
+ }
+ }
+ }
+ }
+
+ anyVariables.removeAll(assignments.keySet());
+ }
+
+ private void separateGuardsAndBeforeAfterPredicates(ExprOrOpArgNode node) {
+ if (node instanceof OpApplNode) {
+ OpApplNode opApplNode = (OpApplNode) node;
+ if (opApplNode.getOperator().getKind() == BuiltInKind) {
+ switch (getOpCode(opApplNode.getOperator().getName())) {
+ case OPCODE_land: // \land
+ {
+ separateGuardsAndBeforeAfterPredicates(opApplNode.getArgs()[0]);
+ separateGuardsAndBeforeAfterPredicates(opApplNode.getArgs()[1]);
+ return;
+ }
+ case OPCODE_cl: // $ConjList
+ {
+ for (int i = 0; i < opApplNode.getArgs().length; i++) {
+ separateGuardsAndBeforeAfterPredicates(opApplNode
+ .getArgs()[i]);
+ }
+ return;
+ }
+ default: {
+ if (opApplNode.level < 2) {
+ guards.add(node);
+ return;
+ } else {
+ beforeAfterPredicates.add(node);
+ return;
+ }
+ }
+
+ }
+ }
+ }
+ beforeAfterPredicates.add(node);
}
private void evalParams() {
@@ -53,17 +268,16 @@ public class BOperation implements ASTConstants, ToolGlobals, TranslationGlobals
}
}
- public SymbolNode getSymbolNode(){
- if(node instanceof OpApplNode){
+ public SymbolNode getSymbolNode() {
+ if (node instanceof OpApplNode) {
OpApplNode n = ((OpApplNode) node);
- System.out.println(n.getOperator().getKind());
- if(n.getOperator().getKind() == UserDefinedOpKind){
+ if (n.getOperator().getKind() == UserDefinedOpKind) {
return ((OpApplNode) node).getOperator();
}
}
- return null;
+ return null;
}
-
+
public String getName() {
return name;
}
@@ -79,20 +293,20 @@ public class BOperation implements ASTConstants, ToolGlobals, TranslationGlobals
public ArrayList<String> getOpParams() {
return opParams;
}
-
- public ArrayList<FormalParamNode> getFormalParams(){
+
+ public ArrayList<FormalParamNode> getFormalParams() {
return formalParams;
}
- public ArrayList<String> getUnchangedVariables(){
+ public ArrayList<String> getUnchangedVariables() {
return unchangedVariables;
}
-
+
private void findUnchangedVariables() {
unchangedVariables = new ArrayList<String>();
findUnchangedVaribalesInSemanticNode(node);
+ anyVariables.removeAll(unchangedVariablesList);
}
-
/**
* @param node2
@@ -138,25 +352,81 @@ public class BOperation implements ASTConstants, ToolGlobals, TranslationGlobals
}
return;
}
- case OPCODE_unchanged:{
+ case OPCODE_unchanged: {
n.setToolObject(USED, false);
OpApplNode k = (OpApplNode) n.getArgs()[0];
if (k.getOperator().getKind() == VariableDeclKind) {
+ unchangedVariablesList.add((OpDeclNode) k.getOperator());
String name = k.getOperator().getName().toString();
unchangedVariables.add(name);
} else {
// Tuple
for (int i = 0; i < k.getArgs().length; i++) {
OpApplNode var = (OpApplNode) k.getArgs()[i];
+ unchangedVariablesList.add((OpDeclNode) var
+ .getOperator());
String name = var.getOperator().getName().toString();
unchangedVariables.add(name);
}
}
}
-
+
}
}
}
-
-
+
+}
+
+class PrimedVariablesFinder extends AbstractASTVisitor {
+ private final Set<SymbolNode> all;
+ private final Set<SymbolNode> twiceUsedVariables;
+ private final Hashtable<SemanticNode, Set<SymbolNode>> table;
+ private Set<SymbolNode> currentSet;
+
+ public PrimedVariablesFinder(ArrayList<ExprOrOpArgNode> list) {
+ this.all = new HashSet<SymbolNode>();
+ this.twiceUsedVariables = new HashSet<SymbolNode>();
+ this.table = new Hashtable<SemanticNode, Set<SymbolNode>>();
+
+ for (ExprOrOpArgNode exprOrOpArgNode : list) {
+ findPrimedVariables(exprOrOpArgNode);
+ }
+ }
+
+ public void findPrimedVariables(ExprOrOpArgNode n) {
+ currentSet = new HashSet<SymbolNode>();
+ this.visitExprOrOpArgNode(n);
+ table.put(n, currentSet);
+ }
+
+ public void visitBuiltInNode(OpApplNode n) {
+ switch (getOpCode(n.getOperator().getName())) {
+
+ case OPCODE_prime: // prime
+ {
+ if (n.getArgs()[0] instanceof OpApplNode){
+ OpApplNode varNode = (OpApplNode) n.getArgs()[0];
+ SymbolNode var = varNode.getOperator();
+
+ currentSet.add(var);
+
+ if (all.contains(var)) {
+ twiceUsedVariables.add(var);
+ } else {
+ all.add(var);
+ }
+ }
+ }
+
+ default: {
+ super.visitBuiltInNode(n);
+ }
+
+ }
+ }
+
+ public Set<SymbolNode> getTwiceUsedVariables() {
+ return this.twiceUsedVariables;
+ }
+
}
diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index f0de31afdc577bbfafa9e67785bc52cf8a90732a..2152ce5c212a3cb19d9779dc3cad628b9b73a976 100644
--- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java
+++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
@@ -44,14 +44,15 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
private OpDefNode next;
private ArrayList<OpDefNode> invariants;
- private ModuleNode moduleNode;
+ private final ModuleNode moduleNode;
private ExprNode nextExpr;
private String nextName;
+
private ArrayList<OpDeclNode> bConstants;
// used to check if a b constant has arguments and is not overriden in the
// configfile
- private ArrayList<BOperation> bOperations;
+ private final ArrayList<BOperation> bOperations = new ArrayList<BOperation>();
private ArrayList<ExprNode> inits;
private ArrayList<LetInNode> globalLets = new ArrayList<LetInNode>();
// these local definitions occur in assume nodes or in BOperations and will
@@ -75,40 +76,44 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
private ConfigfileEvaluator conEval;
- /**
- * @param m
- * @param conEval
- */
- public SpecAnalyser(ModuleNode m, ConfigfileEvaluator conEval) {
+ private SpecAnalyser(ModuleNode m) {
this.moduleNode = m;
- this.spec = conEval.getSpecNode();
- this.init = conEval.getInitNode();
- this.next = conEval.getNextNode();
- this.invariants = conEval.getInvariants();
- this.bConstants = conEval.getbConstantList();
- this.conEval = conEval;
+ this.bConstants = new ArrayList<OpDeclNode>();
}
- public SpecAnalyser(ModuleNode m) {
- this.moduleNode = m;
+ public static SpecAnalyser createSpecAnalyser(ModuleNode m,
+ ConfigfileEvaluator conEval) {
+ SpecAnalyser specAnalyser = new SpecAnalyser(m);
+ specAnalyser.spec = conEval.getSpecNode();
+ specAnalyser.init = conEval.getInitNode();
+ specAnalyser.next = conEval.getNextNode();
+ specAnalyser.invariants = conEval.getInvariants();
+ specAnalyser.bConstants = conEval.getbConstantList();
+ specAnalyser.conEval = conEval;
+
+ return specAnalyser;
+ }
+
+ public static SpecAnalyser createSpecAnalyser(ModuleNode m) {
+ SpecAnalyser specAnalyser = new SpecAnalyser(m);
Hashtable<String, OpDefNode> definitions = new Hashtable<String, OpDefNode>();
for (int i = 0; i < m.getOpDefs().length; i++) {
definitions.put(m.getOpDefs()[i].getName().toString(),
m.getOpDefs()[i]);
}
- this.spec = definitions.get("Spec");
- this.init = definitions.get("Init");
- this.next = definitions.get("Next");
-
+ specAnalyser.spec = definitions.get("Spec");
+ specAnalyser.init = definitions.get("Init");
+ specAnalyser.next = definitions.get("Next");
// TODO are constant in the right order
- this.bConstants = new ArrayList<OpDeclNode>();
- this.bConstants.addAll(Arrays.asList(m.getConstantDecls()));
+
+ specAnalyser.bConstants.addAll(Arrays.asList(m.getConstantDecls()));
+
+ return specAnalyser;
}
public void start() throws SemanticErrorException, FrontEndException,
ConfigFileErrorException, NotImplementedException {
-
-
+
if (spec != null) {
evalSpec();
} else {
@@ -231,7 +236,6 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
ConfigFileErrorException {
if (nextExpr == null)
return;
- bOperations = new ArrayList<BOperation>();
findOperationsInSemanticNode(nextExpr, nextName,
new ArrayList<OpApplNode>());
}
@@ -293,7 +297,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
usedDefinitions.add(def);
if (def.getParams().length > 0) {
BOperation op = new BOperation(def.getName().toString(), n,
- existQuans);
+ existQuans, this);
bOperations.add(op);
return;
} else {
@@ -349,7 +353,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
case OPCODE_fa: // $FcnApply f[1]
case OPCODE_ite: // IF THEN ELSE
case OPCODE_case: {
- BOperation op = new BOperation(name, n, existQuans);
+ BOperation op = new BOperation(name, n, existQuans, this);
bOperations.add(op);
return;
}
@@ -585,17 +589,17 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
}
}
-// public void evalIfThenElse() {
-// boolean b = false;
-// for (int i = 0; i < ifThenElseNodes.size() && !b; i++) {
-// OpApplNode node = ifThenElseNodes.get(i);
-// TLAType t = (TLAType) node.getToolObject(TYPE_ID);
-// if (t.getKind() != BOOL)
-// b = true;
-// }
-// if (b)
-// definitionMacros.add(IF_THEN_ELSE);
-// }
+ // public void evalIfThenElse() {
+ // boolean b = false;
+ // for (int i = 0; i < ifThenElseNodes.size() && !b; i++) {
+ // OpApplNode node = ifThenElseNodes.get(i);
+ // TLAType t = (TLAType) node.getToolObject(TYPE_ID);
+ // if (t.getKind() != BOOL)
+ // b = true;
+ // }
+ // if (b)
+ // definitionMacros.add(IF_THEN_ELSE);
+ // }
public ArrayList<LetInNode> getGlobalLets() {
return this.globalLets;
diff --git a/src/main/java/de/tla2b/output/ASTPrettyPrinter.java b/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
index 3768be4f6808898ff93eb87e3a24e422c03c0bc5..f36db50939a1a31ed0d1a567a6dc90e843c0dd1e 100644
--- a/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
+++ b/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
@@ -9,6 +9,7 @@ import de.be4.classicalb.core.parser.analysis.ExtendedDFAdapter;
import de.be4.classicalb.core.parser.node.AAbstractMachineParseUnit;
import de.be4.classicalb.core.parser.node.AAnySubstitution;
import de.be4.classicalb.core.parser.node.ABecomesSuchSubstitution;
+import de.be4.classicalb.core.parser.node.ABlockSubstitution;
import de.be4.classicalb.core.parser.node.ADefinitionExpression;
import de.be4.classicalb.core.parser.node.ADefinitionPredicate;
import de.be4.classicalb.core.parser.node.AExpressionDefinitionDefinition;
@@ -17,10 +18,13 @@ import de.be4.classicalb.core.parser.node.ALambdaExpression;
import de.be4.classicalb.core.parser.node.AOperation;
import de.be4.classicalb.core.parser.node.AOperationsMachineClause;
import de.be4.classicalb.core.parser.node.APredicateDefinitionDefinition;
+import de.be4.classicalb.core.parser.node.ASelectSubstitution;
+import de.be4.classicalb.core.parser.node.ASkipSubstitution;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.PMachineClause;
import de.be4.classicalb.core.parser.node.POperation;
+import de.be4.classicalb.core.parser.node.PSubstitution;
import de.be4.classicalb.core.parser.node.Start;
import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
import de.be4.classicalb.core.parser.node.Token;
@@ -173,7 +177,8 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
putSymbol("AEmptySetExpression", "{}");
putSymbol("ABoolSetExpression", "BOOL");
putSymbol("AStringSetExpression", "STRING");
-
+ putSymbol("ASkipSubstitution", "skip");
+
putPreEnd("APowSubsetExpression", "POW(", ")");
putPreEnd("AConvertBoolExpression", "bool(", ")");
putPreEnd("ADomainExpression", "dom(", ")");
@@ -189,6 +194,10 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
putPreEnd("ATailExpression", "tail(", ")");
putPreEnd("AEmptySequenceExpression", "[", "]");
+ putPreEnd("ABlockSubstitution", "BEGIN ", " END");
+ // TODO other substitutions
+
+
put("ASetExtensionExpression", null, "{", ", ", "}", null, null);
put("AStructExpression", "struct", "(", ", ", ")", null, null);
put("ARecExpression", "rec", "(", ", ", ")", null, null);
@@ -474,6 +483,35 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
sb.append(" END");
}
+ @Override
+ public void caseASelectSubstitution(final ASelectSubstitution node) {
+ sb.append("SELECT ");
+ node.getCondition().apply(this);
+ sb.append(" THEN ");
+ betweenChildren(node);
+ node.getThen().apply(this);
+ {
+ final List<PSubstitution> copy = new ArrayList<PSubstitution>(
+ node.getWhenSubstitutions());
+ beginList(node);
+ for (final Iterator<PSubstitution> iterator = copy.iterator(); iterator
+ .hasNext();) {
+ final PSubstitution e = iterator.next();
+ e.apply(this);
+
+ if (iterator.hasNext()) {
+ betweenListElements(node);
+ }
+ }
+ endList(node);
+ }
+ betweenChildren(node);
+ if (node.getElse() != null) {
+ node.getElse().apply(this);
+ }
+ sb.append(" END");
+ }
+
@Override
public void caseAPredicateDefinitionDefinition(
APredicateDefinitionDefinition node) {
diff --git a/src/main/java/de/tla2b/translation/BMacroHandler.java b/src/main/java/de/tla2b/translation/BMacroHandler.java
index 4852956defe7b4098cab47a26a9ab569de318a4a..21443fb9aed69c4ae5206561b762d7bb1c18bd76 100644
--- a/src/main/java/de/tla2b/translation/BMacroHandler.java
+++ b/src/main/java/de/tla2b/translation/BMacroHandler.java
@@ -15,6 +15,7 @@ import tla2sany.semantic.OpApplNode;
import tla2sany.semantic.OpDefNode;
import tla2sany.semantic.SymbolNode;
import de.tla2b.analysis.AbstractASTVisitor;
+import de.tla2b.analysis.BOperation;
import de.tla2b.analysis.SpecAnalyser;
import de.tla2b.config.ConfigfileEvaluator;
@@ -25,7 +26,7 @@ public class BMacroHandler extends AbstractASTVisitor {
ArrayList<OpDefNode> bDefs = new ArrayList<OpDefNode>();
for (int i = 0; i < moduleNode.getOpDefs().length; i++) {
OpDefNode def = moduleNode.getOpDefs()[i];
- if (specAnalyser.getBDefinitions().contains(def)) {
+ if(specAnalyser.getUsedDefinitions().contains(def)){
if (conEval != null
&& conEval.getConstantOverrideTable()
.containsValue(def)) {
@@ -40,6 +41,16 @@ public class BMacroHandler extends AbstractASTVisitor {
}
visitAssumptions(moduleNode.getAssumptions());
+
+ for (BOperation op : specAnalyser.getBOperations()) {
+ definitionParameters = new HashSet<FormalParamNode>();
+ localVariables = new HashSet<FormalParamNode>();
+
+ visitExprNode(op.getNode());
+
+ definitionParameters = null;
+ localVariables = null;
+ }
}
private HashSet<FormalParamNode> definitionParameters;
@@ -72,6 +83,7 @@ public class BMacroHandler extends AbstractASTVisitor {
localVariables = null;
}
+
@Override
public void visitBuiltInNode(OpApplNode n) {
diff --git a/src/main/java/de/tla2b/translation/RecursiveFunctionHandler.java b/src/main/java/de/tla2b/translation/RecursiveFunctionHandler.java
new file mode 100644
index 0000000000000000000000000000000000000000..fe1a737e9bd9afc5f7ec09d4d51f4b639dfcc0d2
--- /dev/null
+++ b/src/main/java/de/tla2b/translation/RecursiveFunctionHandler.java
@@ -0,0 +1,66 @@
+package de.tla2b.translation;
+
+import java.util.ArrayList;
+import java.util.HashSet;
+import java.util.Hashtable;
+
+import tla2sany.semantic.FormalParamNode;
+import tla2sany.semantic.OpApplNode;
+import tla2sany.semantic.OpDefNode;
+import tla2sany.semantic.SemanticNode;
+import tla2sany.semantic.SymbolNode;
+import de.tla2b.analysis.AbstractASTVisitor;
+import de.tla2b.analysis.SpecAnalyser;
+
+public class RecursiveFunctionHandler extends AbstractASTVisitor {
+
+ private ArrayList<FormalParamNode> paramList;
+ private ArrayList<SymbolNode> externParams;
+
+ private HashSet<OpApplNode> recursiveFunctions = new HashSet<OpApplNode>();
+ private Hashtable<SemanticNode, ArrayList<SymbolNode>> additionalParamsTable = new Hashtable<SemanticNode, ArrayList<SymbolNode>>();
+
+ public RecursiveFunctionHandler(SpecAnalyser specAnalyser) {
+ for (OpDefNode recFunc : specAnalyser.getRecursiveFunctions()) {
+ OpApplNode body = (OpApplNode) recFunc.getBody();
+ recursiveFunctions.add(body);
+ FormalParamNode[][] params = body.getBdedQuantSymbolLists();
+
+ paramList = new ArrayList<FormalParamNode>();
+ FormalParamNode self = body.getUnbdedQuantSymbols()[0];
+ paramList.add(self);
+ for (int i = 0; i < params.length; i++) {
+ for (int j = 0; j < params[i].length; j++) {
+ paramList.add(params[i][j]);
+ }
+ }
+ externParams = new ArrayList<SymbolNode>();
+ visitExprNode(recFunc.getBody());
+ paramList = null;
+ additionalParamsTable.put(body, externParams);
+ additionalParamsTable.put(recFunc, externParams);
+ additionalParamsTable.put(self, externParams);
+ }
+ }
+
+ public void visitFormalParamNode(OpApplNode n) {
+ FormalParamNode param = (FormalParamNode) n.getOperator();
+ if (!paramList.contains(param)) {
+ externParams.add(param);
+ }
+ }
+
+ public void visitVariableNode(OpApplNode n) {
+ externParams.add(n.getOperator());
+ }
+
+ public ArrayList<SymbolNode> getAdditionalParams(SemanticNode n) {
+ return additionalParamsTable.get(n);
+ }
+
+
+ public boolean isRecursiveFunction(SemanticNode n) {
+ return additionalParamsTable.containsKey(n);
+ }
+
+}
diff --git a/src/main/java/de/tla2b/translation/TLA2B.java b/src/main/java/de/tla2b/translation/TLA2B.java
index 0875681a782c9a442f3a961cfd5aae1a2802eab3..9c01419449232e866b3f019decf85e05a426919c 100644
--- a/src/main/java/de/tla2b/translation/TLA2B.java
+++ b/src/main/java/de/tla2b/translation/TLA2B.java
@@ -16,6 +16,7 @@ import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.NotImplementedException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.global.TranslationGlobals;
+import de.tla2b.util.FileUtils;
import util.FileUtil;
import util.ToolIO;
diff --git a/src/main/java/de/tla2b/translation/Tla2BTranslator.java b/src/main/java/de/tla2b/translation/Tla2BTranslator.java
index 7ec593ee29303a4629a23d696613764c1b222999..64c0659c17601600389997416b3383f509d87da3 100644
--- a/src/main/java/de/tla2b/translation/Tla2BTranslator.java
+++ b/src/main/java/de/tla2b/translation/Tla2BTranslator.java
@@ -13,7 +13,7 @@ import de.tla2b.config.ConfigfileEvaluator;
import de.tla2b.config.ModuleOverrider;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.global.TranslationGlobals;
-import de.tla2b.pprint.BMachinePrinter;
+import de.tla2b.util.FileUtils;
import tla2sany.drivers.FrontEndException;
import tla2sany.drivers.SANY;
import tla2sany.modanalyzer.SpecObj;
@@ -112,9 +112,9 @@ public class Tla2BTranslator implements TranslationGlobals {
ModuleOverrider modOver = new ModuleOverrider(moduleNode, conEval);
modOver.start();
- specAnalyser = new SpecAnalyser(moduleNode, conEval);
+ specAnalyser = SpecAnalyser.createSpecAnalyser(moduleNode, conEval);
} else {
- specAnalyser = new SpecAnalyser(moduleNode);
+ specAnalyser = SpecAnalyser.createSpecAnalyser(moduleNode);
}
specAnalyser.start();
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index c885712c9baf614e488f8250f518936f26e9d2b2..3366bc9e3ab857f6c9af06879dcdb9c3fadccf2a 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -140,6 +140,7 @@ import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.Priorities;
import de.tla2b.global.TranslationGlobals;
import de.tla2b.translation.BMacroHandler;
+import de.tla2b.translation.RecursiveFunctionHandler;
import de.tla2b.types.EnumType;
import de.tla2b.types.FunctionType;
import de.tla2b.types.IType;
@@ -156,6 +157,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
SpecAnalyser specAnalyser;
private final PredicateVsExpression predicateVsExpression;
private final BMacroHandler bMacroHandler;
+ private final RecursiveFunctionHandler recursiveFunctionHandler;
final int SUBSTITUTE_PARAM = 29;
@@ -180,9 +182,12 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
SpecAnalyser specAnalyser,
UsedExternalFunctions usedExternalFunctions,
PredicateVsExpression predicateVsExpression,
- BMacroHandler bMacroHandler) {
+ BMacroHandler bMacroHandler,
+ RecursiveFunctionHandler recursiveFunctionHandler) {
this.predicateVsExpression = predicateVsExpression;
this.bMacroHandler = bMacroHandler;
+ this.recursiveFunctionHandler = recursiveFunctionHandler;
+
this.conEval = conEval;
this.moduleNode = moduleNode;
this.specAnalyser = specAnalyser;
@@ -437,7 +442,8 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
valueList);
any.setThen(assign);
operation.setOperationBody(any);
- opList.add(operation);
+ //opList.add(operation);
+ opList.add(op.getBOperation(this));
}
AOperationsMachineClause opClause = new AOperationsMachineClause(opList);
@@ -517,7 +523,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
- private AIdentifierExpression createIdentifierNode(SymbolNode symbolNode) {
+ public AIdentifierExpression createIdentifierNode(SymbolNode symbolNode) {
if (bMacroHandler.containsSymbolNode(symbolNode)) {
return createIdentifierNode(bMacroHandler.getNewName(symbolNode));
} else {
@@ -638,7 +644,6 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
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);
@@ -710,7 +715,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
return visitExprNodePredicate(assumeNode.getAssume());
}
- private PPredicate visitExprNodePredicate(ExprNode n) {
+ public PPredicate visitExprNodePredicate(ExprNode n) {
switch (n.getKind()) {
case OpApplKind:
return visitOpApplNodePredicate((OpApplNode) n);
@@ -726,9 +731,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
- System.out.println(n);
- System.out.println(n.getClass());
- throw new RuntimeException();
+ throw new RuntimeException(n.getClass().toString());
}
private PExpression visitExprNodeExpression(ExprNode n) {
@@ -783,8 +786,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
- System.out.println(n.getClass());
- throw new RuntimeException();
+ throw new RuntimeException(n.getClass().toString());
}
private PPredicate visitOpApplNodePredicate(OpApplNode n) {
@@ -803,8 +805,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
}
- System.out.println(n.getOperator().getName());
- throw new RuntimeException();
+ throw new RuntimeException(n.getOperator().getName().toString());
}
private PExpression visitOpApplNodeExpression(OpApplNode n) {
@@ -821,6 +822,19 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
ExprOrOpArgNode e = (ExprOrOpArgNode) param
.getToolObject(SUBSTITUTE_PARAM);
if (e == null) {
+ if (recursiveFunctionHandler.isRecursiveFunction(param)) {
+ ArrayList<SymbolNode> list = recursiveFunctionHandler.getAdditionalParams(param);
+ if (list.size() > 0) {
+ AFunctionExpression call = new AFunctionExpression();
+ call.setIdentifier(createIdentifierNode(param));
+ ArrayList<PExpression> params = new ArrayList<PExpression>();
+ for (SymbolNode symbolNode : list) {
+ params.add(createIdentifierNode(symbolNode));
+ }
+ call.setParameters(params);
+ return call;
+ }
+ }
return createIdentifierNode(n.getOperator());
} else {
return visitExprOrOpArgNodeExpression(e);
@@ -836,8 +850,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
}
- System.out.println(n.getOperator().getName());
- throw new RuntimeException();
+ throw new RuntimeException(n.getOperator().getName().toString());
}
private PPredicate visitUserdefinedOpPredicate(OpApplNode n) {
@@ -850,15 +863,16 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
return visitBBuitInsPredicate(n);
}
- List<PExpression> params = new ArrayList<PExpression>();
- for (int i = 0; i < n.getArgs().length; i++) {
- params.add(visitExprOrOpArgNodeExpression(n.getArgs()[i]));
- }
if (specAnalyser.getRecursiveFunctions().contains(def)) {
return new AEqualPredicate(createIdentifierNode(def),
new ABooleanTrueExpression());
}
+ List<PExpression> params = new ArrayList<PExpression>();
+ for (int i = 0; i < n.getArgs().length; i++) {
+ params.add(visitExprOrOpArgNodeExpression(n.getArgs()[i]));
+ }
+
if (predicateVsExpression.getDefinitionType(def) == DefinitionType.EXPRESSION) {
ADefinitionExpression defCall = new ADefinitionExpression();
defCall.setDefLiteral(new TIdentifierLiteral(getName(def)));
@@ -889,7 +903,19 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
if (specAnalyser.getRecursiveFunctions().contains(def)) {
- return createIdentifierNode(def);
+ ArrayList<SymbolNode> list = recursiveFunctionHandler.getAdditionalParams(def);
+ if (list.size() > 0) {
+ AFunctionExpression call = new AFunctionExpression();
+ call.setIdentifier(createIdentifierNode(def));
+ ArrayList<PExpression> params = new ArrayList<PExpression>();
+ for (SymbolNode symbolNode : list) {
+ params.add(createIdentifierNode(symbolNode));
+ }
+ call.setParameters(params);
+ return call;
+ } else {
+ return createIdentifierNode(def);
+ }
}
if (allTLADefinitions.contains(def)) {
@@ -987,8 +1013,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
new ABooleanTrueExpression());
}
- System.out.println(n.getOperator().getName());
- throw new RuntimeException();
+ throw new RuntimeException(n.getOperator().getName().toString());
}
private PExpression visitBBuitInsExpression(OpApplNode n) {
@@ -1140,8 +1165,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
}
- System.out.println(n.getOperator().getName());
- throw new RuntimeException();
+ throw new RuntimeException(n.getOperator().getName().toString());
}
private PExpression visitBuiltInKindExpression(OpApplNode n) {
@@ -1400,6 +1424,29 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
lambda.setIdentifiers(idList);
lambda.setPredicate(createConjunction(predList));
lambda.setExpression(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
+
+ if (recursiveFunctionHandler.isRecursiveFunction(n)) {
+
+ ArrayList<SymbolNode> externParams = recursiveFunctionHandler.getAdditionalParams(n);
+ if(externParams.size()>0){
+ ALambdaExpression lambda2 = new ALambdaExpression();
+ ArrayList<PExpression> shiftedParams = new ArrayList<PExpression>();
+ List<PPredicate> predList2 = new ArrayList<PPredicate>();
+ for (SymbolNode p :externParams) {
+ shiftedParams.add(createIdentifierNode(p));
+
+ AMemberPredicate member = new AMemberPredicate();
+ member.setLeft(createIdentifierNode(p));
+ TLAType t = (TLAType) p.getToolObject(TYPE_ID);
+ member.setRight(t.getBNode());
+ predList2.add(member);
+ }
+ lambda2.setIdentifiers(shiftedParams);
+ lambda2.setPredicate(createConjunction(predList2));
+ lambda2.setExpression(lambda);
+ return lambda2;
+ }
+ }
return lambda;
}
@@ -1658,8 +1705,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
- System.out.println(n.getOperator().getName());
- throw new RuntimeException();
+ throw new RuntimeException(n.getOperator().getName().toString());
}
private PExpression createUnboundedChoose(OpApplNode n) {
@@ -1939,11 +1985,10 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
- System.out.println(n.getOperator().getName());
- throw new RuntimeException();
+ throw new RuntimeException(n.getOperator().getName().toString());
}
- private PPredicate visitBounded(OpApplNode n) {
+ public PPredicate visitBounded(OpApplNode n) {
FormalParamNode[][] params = n.getBdedQuantSymbolLists();
ExprNode[] in = n.getBdedQuantBounds();
boolean[] isTuple = n.isBdedQuantATuple();
@@ -1972,7 +2017,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
return createConjunction(predList);
}
- private PPredicate visitExprOrOpArgNodePredicate(ExprOrOpArgNode n) {
+ public PPredicate visitExprOrOpArgNodePredicate(ExprOrOpArgNode n) {
if (n instanceof ExprNode) {
return visitExprNodePredicate((ExprNode) n);
} else {
@@ -1980,7 +2025,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
}
- private PExpression visitExprOrOpArgNodeExpression(ExprOrOpArgNode n) {
+ public PExpression visitExprOrOpArgNodeExpression(ExprOrOpArgNode n) {
if (n instanceof ExprNode) {
return visitExprNodeExpression((ExprNode) n);
@@ -1993,7 +2038,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
return new AIdentifierExpression(createTIdentifierLiteral(name));
}
- private PPredicate createConjunction(List<PPredicate> list) {
+ public PPredicate createConjunction(List<PPredicate> list) {
if (list.size() == 1)
return list.get(0);
AConjunctPredicate conj = new AConjunctPredicate();
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index 199fb4812b2574845785a178402e3a47254b14dd..83aeb9218d963174912028ab5b67de67e9a39ce0 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -25,6 +25,8 @@ import de.tla2b.global.TranslationGlobals;
import de.tla2b.output.ASTPrettyPrinter;
import de.tla2b.pprint.BMachinePrinter;
import de.tla2b.translation.BMacroHandler;
+import de.tla2b.translation.RecursiveFunctionHandler;
+import de.tla2b.util.FileUtils;
import tla2sany.drivers.SANY;
import tla2sany.modanalyzer.SpecObj;
import tla2sany.semantic.ModuleNode;
@@ -55,7 +57,7 @@ public class Translator implements TranslationGlobals {
}
private void findConfigFile() {
- String configFileName = removeExtention(moduleFile.getAbsolutePath());
+ String configFileName = FileUtils.removeExtention(moduleFile.getAbsolutePath());
configFileName = configFileName + ".cfg";
configFile = new File(configFileName);
if (!configFile.exists()) {
@@ -189,35 +191,36 @@ public class Translator implements TranslationGlobals {
ModuleOverrider modOver = new ModuleOverrider(moduleNode, conEval);
modOver.start();
- specAnalyser = new SpecAnalyser(moduleNode, conEval);
+ specAnalyser = SpecAnalyser.createSpecAnalyser(moduleNode, conEval);
} else {
- specAnalyser = new SpecAnalyser(moduleNode);
+ specAnalyser = SpecAnalyser.createSpecAnalyser(moduleNode);
}
specAnalyser.start();
TypeChecker typechecker = new TypeChecker(moduleNode, conEval,
specAnalyser);
typechecker.start();
- //specAnalyser.evalIfThenElse();
+ // specAnalyser.evalIfThenElse();
SymbolRenamer symRenamer = new SymbolRenamer(moduleNode, specAnalyser);
symRenamer.start();
-// BMachinePrinter p = new BMachinePrinter(moduleNode, conEval,
-// specAnalyser);
-// bMachineString = p.start().toString();
-
+ // BMachinePrinter p = new BMachinePrinter(moduleNode, conEval,
+ // specAnalyser);
+ // bMachineString = p.start().toString();
UsedExternalFunctions usedExternalFunctions = new UsedExternalFunctions(
moduleNode, specAnalyser);
-
+ RecursiveFunctionHandler recursiveFunctionHandler = new RecursiveFunctionHandler(
+ specAnalyser);
BMacroHandler bMacroHandler = new BMacroHandler(specAnalyser, conEval);
BAstCreator bAstCreator = new BAstCreator(moduleNode, conEval,
- specAnalyser, usedExternalFunctions, predicateVsExpression, bMacroHandler);
+ specAnalyser, usedExternalFunctions, predicateVsExpression,
+ bMacroHandler, recursiveFunctionHandler);
this.BAst = bAstCreator.getStartNode();
this.bDefinitions = bAstCreator.getBDefinitions();
return BAst;
}
public void createMachineFile() {
- String bFile = removeExtention(moduleFile.getAbsolutePath());
+ String bFile = FileUtils.removeExtention(moduleFile.getAbsolutePath());
bFile = bFile + "_tla.mch";
File machineFile;
@@ -228,7 +231,8 @@ public class Translator implements TranslationGlobals {
in = new BufferedReader(new FileReader(machineFile));
String firstLine = in.readLine();
in.close();
- if (firstLine != null && !firstLine.startsWith("/*@ generated by TLA2B ")) {
+ if (firstLine != null
+ && !firstLine.startsWith("/*@ generated by TLA2B ")) {
System.err.println("Error: File " + machineFile.getName()
+ " already exists"
+ " and was not generated by TLA2B.\n"
@@ -249,7 +253,6 @@ public class Translator implements TranslationGlobals {
System.exit(-1);
}
-
ASTPrettyPrinter aP = new ASTPrettyPrinter();
BAst.apply(aP);
StringBuilder result = aP.getResultAsStringbuilder();
@@ -271,28 +274,7 @@ public class Translator implements TranslationGlobals {
}
- public static String removeExtention(String filePath) {
- File f = new File(filePath);
- // if it's a directory, don't remove the extention
- if (f.isDirectory())
- return filePath;
-
- String name = f.getName();
-
- // Now we know it's a file - don't need to do any special hidden
- // checking or contains() checking because of:
- final int lastPeriodPos = name.lastIndexOf('.');
- if (lastPeriodPos <= 0) {
- // No period after first character - return name as it was passed in
- return filePath;
- } else {
- // Remove the last period and everything after it
- File renamed = new File(f.getParent(), name.substring(0,
- lastPeriodPos));
- return renamed.getPath();
- }
- }
public Definitions getBDefinitions() {
return bDefinitions;
@@ -301,8 +283,8 @@ public class Translator implements TranslationGlobals {
public String getBMachineString() {
return bMachineString;
}
-
- public ModuleNode getModuleNode(){
+
+ public ModuleNode getModuleNode() {
return moduleNode;
}
diff --git a/src/test/java/de/tla2b/prettyprintb/RecursiveFunctionTest.java b/src/test/java/de/tla2b/prettyprintb/RecursiveFunctionTest.java
index 3341f3cecf25f5cebf32cd3a3daf2f06606b4021..645819dd4e87e9e98b78e5cf288292741e7c3d38 100644
--- a/src/test/java/de/tla2b/prettyprintb/RecursiveFunctionTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/RecursiveFunctionTest.java
@@ -69,7 +69,7 @@ public class RecursiveFunctionTest {
+ "END";
compare(expected, module);
}
-
+
}
diff --git a/src/test/java/de/tla2b/prettyprintb/SimpleModulesTest.java b/src/test/java/de/tla2b/prettyprintb/SimpleModulesTest.java
index 59879408384a5491b3c3843ef243307cf4c215c9..97dc470262498e22646cff9ac2b7914f272d5369 100644
--- a/src/test/java/de/tla2b/prettyprintb/SimpleModulesTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/SimpleModulesTest.java
@@ -17,7 +17,6 @@ public class SimpleModulesTest {
compare(expected, module);
}
-
@Test
public void testSingleOperator() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -49,11 +48,32 @@ public class SimpleModulesTest {
+ "INVARIANT x : INTEGER \n"
+ "INITIALISATION x :(x = 1) \n"
+ "OPERATIONS \n"
- + "e1 = ANY x_n WHERE x_n : INTEGER & x_n = 1 THEN x := x_n END; \n"
- + "e2 = ANY x_n WHERE x_n : INTEGER & x_n = 2 THEN x := x_n END \n"
+ + "e1 = BEGIN x := 1 END; \n"
+ + "e2 = BEGIN x := 2 END \n"
+ "END";
compare(expected, module);
}
+ @Test
+ public void testVariables2() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals\n"
+ + "VARIABLES x \n"
+ + "Init == x = 1\n"
+ + "e1 == /\\ 1= 2 /\\ x'+ 1= 1 \n"
+ + "e2 == x = 1 /\\ x'= 2 \n"
+ + "Next == e1 \\/ e2 \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "VARIABLES x \n"
+ + "INVARIANT x : INTEGER \n"
+ + "INITIALISATION x :(x = 1) \n"
+ + "OPERATIONS \n"
+ + "e1 = ANY x_n WHERE 1 = 2 & x_n : INTEGER & x_n + 1 = 1 THEN x := x_n END; \n"
+ + "e2 = SELECT x = 1 THEN x := 2 END \n"
+ + "END";
+ compare(expected, module);
+ }
}
diff --git a/src/test/java/de/tla2b/regression/RegressionTests.java b/src/test/java/de/tla2b/regression/RegressionTests.java
new file mode 100644
index 0000000000000000000000000000000000000000..36e9651dceceb6632ba14cc29415c0f0749fae4c
--- /dev/null
+++ b/src/test/java/de/tla2b/regression/RegressionTests.java
@@ -0,0 +1,40 @@
+package de.tla2b.regression;
+
+import static de.tla2b.util.TestUtil.runModule;
+
+import java.io.File;
+import java.util.ArrayList;
+
+import org.junit.Test;
+import org.junit.runner.RunWith;
+
+import de.tla2b.util.AbstractParseModuleTest;
+import de.tla2b.util.PolySuite;
+import de.tla2b.util.PolySuite.Config;
+import de.tla2b.util.PolySuite.Configuration;
+
+@RunWith(PolySuite.class)
+public class RegressionTests extends AbstractParseModuleTest{
+ private final File moduleFile;
+
+ public RegressionTests(File machine, Object result) {
+ this.moduleFile = machine;
+ }
+
+ @Test
+ public void testRunTLC() throws Exception {
+ //String[] a = new String[] { moduleFile.getPath() };
+ System.out.println(moduleFile.getPath());
+ runModule(moduleFile.getPath());
+ }
+
+ @Config
+ public static Configuration getConfig() {
+ final ArrayList<String> list = new ArrayList<String>();
+ final ArrayList<String> ignoreList = new ArrayList<String>();
+
+ list.add("./src/test/resources/examples");
+ ignoreList.add("./src/test/resources/testing/");
+ return getConfiguration2(list, ignoreList);
+ }
+}
diff --git a/src/test/java/de/tla2b/util/TestUtil.java b/src/test/java/de/tla2b/util/TestUtil.java
index f7146256f376753125e04a429e303c8700fd5302..4d9e0d079f09b063011722f5469db3c7df2348a5 100644
--- a/src/test/java/de/tla2b/util/TestUtil.java
+++ b/src/test/java/de/tla2b/util/TestUtil.java
@@ -10,6 +10,7 @@ import java.io.BufferedReader;
import java.io.FileReader;
import java.io.IOException;
+import util.FileUtil;
import de.be4.classicalb.core.parser.BParser;
import de.be4.classicalb.core.parser.exceptions.BException;
import de.be4.classicalb.core.parser.node.Node;
@@ -21,7 +22,6 @@ import de.tla2b.output.Renamer;
import de.tla2b.translation.Tla2BTranslator;
import de.tla2bAst.Translator;
import tla2sany.semantic.AbortException;
-import util.FileUtil;
import util.ToolIO;
public class TestUtil {
@@ -38,8 +38,6 @@ public class TestUtil {
public static void runModule(String tlaFile) throws Exception{
Translator t = new Translator(tlaFile);
Start start = t.translate();
- System.out.println(t.getBMachineString());
- System.out.println("---------------------");
//String printResult = getAstStringofBMachineString(t.getBMachineString());
//System.out.println(printResult);
//System.out.println(getTreeAsString(start));
@@ -205,19 +203,6 @@ public class TestUtil {
return testTypeChecker;
}
-
- public static String fileToString(String fileName) throws IOException {
- StringBuilder res = new StringBuilder();
- BufferedReader in = new BufferedReader(new FileReader(fileName));
- String str;
- while ((str = in.readLine()) != null) {
- res.append(str + "\n");
- }
- in.close();
- return res.toString();
- }
-
-
public static String getAstStringofBMachineString(final String testMachine)
throws BException {
final BParser parser = new BParser("testcase");
diff --git a/src/test/resources/prettyprint/OperationsTest/OperationsTest.mch b/src/test/resources/prettyprint/OperationsTest/OperationsTest.mch
new file mode 100644
index 0000000000000000000000000000000000000000..7d8c2bc85a39abb63edfc6e6a3d3a9580da6d8b2
--- /dev/null
+++ b/src/test/resources/prettyprint/OperationsTest/OperationsTest.mch
@@ -0,0 +1,19 @@
+MACHINE OperationsTest
+VARIABLES a, b, c
+INVARIANT
+(a : INTEGER & b : INTEGER) & c : INTEGER
+INITIALISATION
+a, b, c:((a = 1 & b = 2) & c = 3)
+OPERATIONS
+ begin1 = BEGIN skip END;
+
+ begin2 = BEGIN a,b,c := 1,2,3 END;
+
+ any1 = ANY a_n WHERE (a_n : INTEGER & a_n + 1 = 2) & TRUE = TRUE THEN a := a_n END;
+
+ any2 = ANY a_n WHERE ((1 = 1 & a_n : INTEGER) & a_n + 1 = 2) & TRUE = TRUE THEN a := a_n END;
+
+ any3 = ANY a_n WHERE ((a_n : INTEGER & a_n = 2) & a_n > 1) & TRUE = TRUE THEN a := a_n END;
+
+ select = SELECT 1 = 1 THEN a,b,c := 1,2,3 END
+END
diff --git a/src/test/resources/prettyprint/OperationsTest/OperationsTest.tla b/src/test/resources/prettyprint/OperationsTest/OperationsTest.tla
new file mode 100644
index 0000000000000000000000000000000000000000..6ba867cafcef0d110efa12a5141af9720017d7ac
--- /dev/null
+++ b/src/test/resources/prettyprint/OperationsTest/OperationsTest.tla
@@ -0,0 +1,22 @@
+-------------- MODULE OperationsTest ----------------
+EXTENDS Naturals
+VARIABLES a,b,c
+Init == a = 1 /\ b = 2 /\ c =3
+
+begin1 == UNCHANGED<<a,b,c>>
+begin2 == a' = 1 /\ b' = 2 /\ c' = 3
+
+any1 == a' + 1 = 2 /\ UNCHANGED<<b,c>>
+any2 == 1 = 1 /\ a' + 1 = 2 /\ UNCHANGED<<b,c>>
+any3 == a'= 2 /\ a' >1 /\ UNCHANGED<<b,c>>
+
+select == 1 = 1 /\ a' = 1 /\ b' = 2 /\ c' =3
+
+Next ==
+ \/ begin1
+ \/ begin2
+ \/ any1
+ \/ any2
+ \/ any3
+ \/ select
+=================================
\ No newline at end of file
diff --git a/src/test/resources/prettyprint/realworld/FastPaxos.cfg b/src/test/resources/prettyprint/realworld/FastPaxos.cfg
deleted file mode 100644
index abc34f264e9817eac70466647bbf4e109f3fa4d5..0000000000000000000000000000000000000000
--- a/src/test/resources/prettyprint/realworld/FastPaxos.cfg
+++ /dev/null
@@ -1,11 +0,0 @@
-INIT Init
-NEXT Next
-CONSTANTS
- ClassicNum = {1,3}
- FastNum = {2}
- Acceptor = {a1,a2,a3}
- PVal = {v1,v2}
- any = any
- a1=a1 a2=a2 a3=a3 v1=v1 v2=v2
- Max <- MaxOfSet
-INVARIANT TypeOK
\ No newline at end of file
diff --git a/src/test/resources/prettyprint/realworld/FastPaxos.tla b/src/test/resources/prettyprint/realworld/FastPaxos.tla
deleted file mode 100644
index 1b7faa5424bb1afbdc7071dc347360787b15d677..0000000000000000000000000000000000000000
--- a/src/test/resources/prettyprint/realworld/FastPaxos.tla
+++ /dev/null
@@ -1,178 +0,0 @@
------------------------------- MODULE FastPaxos -----------------------------
-EXTENDS Naturals
-CONSTANTS PVal, Acceptor, FastNum, ClassicNum, a1, a2, a3, v1, v2
-
-NextNum(a) == IF a+1 \in FastNum \cup ClassicNum THEN a+1 ELSE 0
-
-RNum == FastNum \cup ClassicNum
-
-any == CHOOSE v : v \notin PVal
-
-i \prec j == i < j
-i \preceq j == (i \prec j) \/ (i = j)
-
-MaxOfSet(S) == CHOOSE p \in S: \A n \in S: p \geq n
-Max(S) == CHOOSE i \in S : \A j \in S : j \preceq i
-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]
-
-Quorum(i) == IF i \in ClassicNum THEN {{a1,a2}, {a1,a3}, {a2, a3}}
- ELSE {{a1,a2,a3}}
-
-
-
-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))
-
-
-
-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 {v1}(*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)
-
-
-
-=============================================================================
diff --git a/src/test/resources/prettyprint/realworld/ManyAssumes.tla b/src/test/resources/prettyprint/realworld/ManyAssumes.tla
deleted file mode 100644
index 64d96f930c9bd6268f40a9cb4821098b58b65536..0000000000000000000000000000000000000000
--- a/src/test/resources/prettyprint/realworld/ManyAssumes.tla
+++ /dev/null
@@ -1,518 +0,0 @@
------ MODULE ManyAssumes -----
-CONSTANTS a, b, c, d
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-ASSUME a = 1 /\ b = 1 /\ c = 1 /\ d = 1
-
-
-
-
-==========
\ No newline at end of file
diff --git a/src/test/resources/prettyprint/realworld/fowler.mch b/src/test/resources/prettyprint/realworld/fowler.mch
index 7b52dd004d45604ce2eebca929c6dc8abd8b97a1..df9602cdf4f980e91261510e756845221d49c6da 100644
--- a/src/test/resources/prettyprint/realworld/fowler.mch
+++ b/src/test/resources/prettyprint/realworld/fowler.mch
@@ -1,55 +1,17 @@
MACHINE fowler
DEFINITIONS
- Init == state = "idle"
- & light = "off"
- & draw = "closed"
- & door = "unlocked"
- & panel = "locked"
+ Init == (((state = "idle" & light = "off") & draw = "closed") & door = "unlocked") & panel = "locked";
VARIABLES state, light, draw, panel, door
INVARIANT
- state : STRING
- & light : STRING
- & draw : STRING
- & panel : STRING
- & door : STRING
+(((state : STRING & light : STRING) & draw : STRING) & panel : STRING) & door : STRING
INITIALISATION
- state, light, draw, panel, door:(Init)
+state, light, draw, panel, door:(Init)
OPERATIONS
- CloseDoor_Op = ANY state_n, door_n
- WHERE state_n : STRING & door_n : STRING & door = "unlocked"
- & door_n = "locked"
- & state_n = "active"
- & TRUE = TRUE
- THEN state, door := state_n, door_n END;
+ CloseDoor = SELECT (door = "unlocked" & TRUE = TRUE) & TRUE = TRUE THEN door,state := "locked","active" END;
- LightOn_Op = ANY state_n, light_n, panel_n, door_n
- WHERE state_n : STRING & light_n : STRING & panel_n : STRING & door_n : STRING & light = "off"
- & light_n = "on"
- & ((draw = "opened"
- => state_n = "unlockedPanel" & panel_n = "unlocked" & door_n = "locked")
- & (not(draw = "opened")
- => state_n = "waitingForDraw"
- & panel_n = panel & door_n = door))
- & TRUE = TRUE
- THEN state, light, panel, door := state_n, light_n, panel_n, door_n END;
+ LightOn = ANY state_n, panel_n, door_n WHERE ((((light = "off" & state_n : STRING) & panel_n : STRING) & door_n : STRING) & ((draw = "opened" => (state_n = "unlockedPanel" & panel_n = "unlocked") & door_n = "locked") & (not(draw = "opened") => state_n = "waitingForDraw" & TRUE = TRUE))) & TRUE = TRUE THEN light,state,panel,door := "on",state_n,panel_n,door_n END;
- OpenDraw_Op = ANY state_n, draw_n, panel_n, door_n
- WHERE state_n : STRING & draw_n : STRING & panel_n : STRING & door_n : STRING & draw = "closed"
- & draw_n = "opened"
- & ((light = "on"
- => state_n = "unlockedPanel" & panel_n = "unlocked" & door_n = "locked")
- & (not(light = "on")
- => state_n = "waitingForLight"
- & panel_n = panel & door_n = door))
- & TRUE = TRUE
- THEN state, draw, panel, door := state_n, draw_n, panel_n, door_n END;
+ OpenDraw = ANY state_n, panel_n, door_n WHERE ((((draw = "closed" & state_n : STRING) & panel_n : STRING) & door_n : STRING) & ((light = "on" => (state_n = "unlockedPanel" & panel_n = "unlocked") & door_n = "locked") & (not(light = "on") => state_n = "waitingForLight" & TRUE = TRUE))) & TRUE = TRUE THEN draw,state,panel,door := "opened",state_n,panel_n,door_n END;
- ClosePanel_Op = ANY state_n, light_n, draw_n, panel_n, door_n
- WHERE state_n : STRING & light_n : STRING & draw_n : STRING & panel_n : STRING & door_n : STRING & panel = "unlocked"
- & panel_n = "locked"
- & light_n = "off"
- & draw_n = "closed"
- & door_n = "unlocked"
- & state_n = "idle"
- THEN state, light, draw, panel, door := state_n, light_n, draw_n, panel_n, door_n END
-END
+ ClosePanel = SELECT panel = "unlocked" THEN panel,light,draw,door,state := "locked","off","closed","unlocked","idle" END
+END
\ No newline at end of file
diff --git a/src/test/resources/prettyprint/realworld/microwave.mch b/src/test/resources/prettyprint/realworld/microwave.mch
index 9a31d390f00429985df08f9d5946dfa82c35a097..479ea776d580db4c7bdcb17744c7311115d5f9f6 100644
--- a/src/test/resources/prettyprint/realworld/microwave.mch
+++ b/src/test/resources/prettyprint/realworld/microwave.mch
@@ -1,94 +1,24 @@
MACHINE microwave
DEFINITIONS
- Init == magnetron_running = FALSE
- & door_open = FALSE
- & button_locked = FALSE
- & error = FALSE
- & time = 0;
-
- Action_Start == error = FALSE
- & magnetron_running = FALSE
- & door_open = FALSE
- & time /= 0
- & magnetron_running_n = TRUE
- & button_locked_n = TRUE
- & door_open_n = door_open & time_n = time & error_n = error;
-
- Action_Stop == magnetron_running = TRUE
- & magnetron_running_n = FALSE
- & button_locked_n = FALSE
- & time_n = 0
- & door_open_n = door_open & error_n = error;
-
- Door_Locked_When_Heating == (magnetron_running = TRUE => door_open = FALSE)
- & (magnetron_running = TRUE => button_locked = TRUE);
-
+ Init == (((magnetron_running = FALSE & door_open = FALSE) & button_locked = FALSE) & error = FALSE) & time = 0;
+ Action_Start == (((((error = FALSE & magnetron_running = FALSE) & door_open = FALSE) & time /= 0) & magnetron_running_n = TRUE) & button_locked_n = TRUE) & TRUE = TRUE;
+ Action_Stop == (((magnetron_running = TRUE & magnetron_running_n = FALSE) & button_locked_n = FALSE) & time_n = 0) & TRUE = TRUE;
+ Door_Locked_When_Heating == (magnetron_running = TRUE => door_open = FALSE) & (magnetron_running = TRUE => button_locked = TRUE);
VARIABLES magnetron_running, door_open, button_locked, time, error
INVARIANT
- magnetron_running : BOOL
- & door_open : BOOL
- & button_locked : BOOL
- & time : INTEGER
- & error : BOOL
- & Door_Locked_When_Heating
+((((magnetron_running : BOOL & door_open : BOOL) & button_locked : BOOL) & time : INTEGER) & error : BOOL) & Door_Locked_When_Heating
INITIALISATION
- magnetron_running, door_open, button_locked, time, error:(Init)
+magnetron_running, door_open, button_locked, time, error:(Init)
OPERATIONS
- Action_Open_Door_Op = ANY door_open_n
- WHERE door_open_n : BOOL & button_locked = FALSE
- & magnetron_running = FALSE
- & door_open = FALSE
- & door_open_n = TRUE
- & TRUE = TRUE
- THEN door_open := door_open_n END;
+ Action_Open_Door = SELECT (((button_locked = FALSE & magnetron_running = FALSE) & door_open = FALSE) & TRUE = TRUE) & TRUE = TRUE THEN door_open := TRUE END;
- Action_Close_Door_Op = ANY door_open_n
- WHERE door_open_n : BOOL & door_open = TRUE
- & door_open_n = FALSE
- & TRUE = TRUE
- THEN door_open := door_open_n END;
+ Action_Close_Door = SELECT (door_open = TRUE & TRUE = TRUE) & TRUE = TRUE THEN door_open := FALSE END;
- Action_Change_Time_Op = ANY time_n
- WHERE time_n : INTEGER & magnetron_running = FALSE
- & (time = 180
- & time_n = 120
- or (time = 120
- & time_n = 90)
- or (time = 90
- & time_n = 60)
- or (time = 60
- & time_n = 30)
- or (time = 30
- & time_n = 15)
- or (time = 15
- & time_n = 180)
- or (time = 0
- & time_n = 180))
- & TRUE = TRUE
- THEN time := time_n END;
+ Action_Change_Time = ANY time_n WHERE ((magnetron_running = FALSE & time_n : INTEGER) & (((((((time = 180 & time_n = 120) or (time = 120 & time_n = 90)) or (time = 90 & time_n = 60)) or (time = 60 & time_n = 30)) or (time = 30 & time_n = 15)) or (time = 15 & time_n = 180)) or (time = 0 & time_n = 180))) & TRUE = TRUE THEN time := time_n END;
- Action_Button_S_Op = ANY magnetron_running_n, door_open_n, button_locked_n, time_n, error_n
- WHERE magnetron_running_n : BOOL & door_open_n : BOOL & button_locked_n : BOOL & time_n : INTEGER & error_n : BOOL & (magnetron_running = FALSE
- => Action_Start)
- & (not(magnetron_running = FALSE)
- => Action_Stop)
- THEN magnetron_running, door_open, button_locked, time, error := magnetron_running_n, door_open_n, button_locked_n, time_n, error_n END;
+ Action_Button_S = ANY magnetron_running_n, door_open_n, button_locked_n, time_n, error_n WHERE ((((magnetron_running_n : BOOL & door_open_n : BOOL) & button_locked_n : BOOL) & time_n : INTEGER) & error_n : BOOL) & ((magnetron_running = FALSE => Action_Start) & (not(magnetron_running = FALSE) => Action_Stop)) THEN magnetron_running,door_open,button_locked,time,error := magnetron_running_n,door_open_n,button_locked_n,time_n,error_n END;
- Action_Error_Op = ANY magnetron_running_n, error_n
- WHERE magnetron_running_n : BOOL & error_n : BOOL & error_n = TRUE
- & magnetron_running_n = FALSE
- & TRUE = TRUE
- THEN magnetron_running, error := magnetron_running_n, error_n END;
+ Action_Error = BEGIN error,magnetron_running := TRUE,FALSE END;
- Action_Tick_Op = ANY magnetron_running_n, door_open_n, button_locked_n, time_n, error_n
- WHERE magnetron_running_n : BOOL & door_open_n : BOOL & button_locked_n : BOOL & time_n : INTEGER & error_n : BOOL & magnetron_running = TRUE
- & ((time /= 1
- => time_n = time - 1
- & door_open_n = door_open & magnetron_running_n = magnetron_running & button_locked_n = button_locked & error_n = error)
- & (not(time /= 1)
- => time_n = 0
- & magnetron_running_n = FALSE
- & button_locked_n = FALSE
- & door_open_n = door_open & error_n = error))
- THEN magnetron_running, door_open, button_locked, time, error := magnetron_running_n, door_open_n, button_locked_n, time_n, error_n END
+ Action_Tick = ANY magnetron_running_n, door_open_n, button_locked_n, time_n, error_n WHERE (((((magnetron_running = TRUE & magnetron_running_n : BOOL) & door_open_n : BOOL) & button_locked_n : BOOL) & time_n : INTEGER) & error_n : BOOL) & ((time /= 1 => time_n = time - 1 & TRUE = TRUE) & (not(time /= 1) => ((time_n = 0 & magnetron_running_n = FALSE) & button_locked_n = FALSE) & TRUE = TRUE)) THEN magnetron_running,door_open,button_locked,time,error := magnetron_running_n,door_open_n,button_locked_n,time_n,error_n END
END
\ No newline at end of file
diff --git a/src/test/resources/simpleModules/Foo1.tla b/src/test/resources/simpleModules/Foo1.tla
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000