diff --git a/build.gradle b/build.gradle
index e597ae06e90f0eb78e2320b8893222784e2a47d6..e28a2f3abf94680b829c3de36e5ae2183bf64190 100644
--- a/build.gradle
+++ b/build.gradle
@@ -2,7 +2,7 @@ apply plugin: 'java'
apply plugin: 'eclipse'
apply plugin: 'maven'
apply plugin: 'jacoco'
-apply plugin: 'findbugs'
+//apply plugin: 'findbugs'
project.version = '1.0.0-SNAPSHOT'
project.group = 'de.prob'
@@ -57,16 +57,16 @@ jacocoTestReport {
}
}
-tasks.withType(FindBugs) {
- reports {
- xml.enabled = false
- html.enabled = true
- }
-}
+//tasks.withType(FindBugs) {
+// reports {
+// xml.enabled = false
+// html.enabled = true
+// }
+//}
-findbugs {
- ignoreFailures = true
-}
+//findbugs {
+// ignoreFailures = true
+//}
jar { from sourceSets.main.allJava }
diff --git a/src/main/java/de/tla2b/analysis/BOperation.java b/src/main/java/de/tla2b/analysis/BOperation.java
index 7e99a87e6c885df66a873d8d8f73a0e811a6126b..b3b96183735c4942ae17408960a4b286211e38bb 100644
--- a/src/main/java/de/tla2b/analysis/BOperation.java
+++ b/src/main/java/de/tla2b/analysis/BOperation.java
@@ -6,7 +6,6 @@ package de.tla2b.analysis;
import java.util.ArrayList;
-import java.util.LinkedHashMap;
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.TranslationGlobals;
diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index 023c3c8764b0b9c2d65d778d9900f94d365a9c0f..2b19348f581a46f4779f3b2f3697789c07185e61 100644
--- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java
+++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
@@ -74,7 +74,9 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
private ArrayList<String> definitionMacros = new ArrayList<String>();
private ArrayList<RecursiveFunktion> recursiveFunctions = new ArrayList<RecursiveFunktion>();
-
+
+ private ConfigfileEvaluator conEval;
+
/**
* @param m
* @param conEval
@@ -86,6 +88,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
this.next = conEval.getNextNode();
this.invariants = conEval.getInvariants();
this.bConstants = conEval.getbConstantList();
+ this.conEval = conEval;
}
public SpecAnalyser(ModuleNode m) {
@@ -365,6 +368,10 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
*/
private void findDefinitions() throws ConfigFileErrorException {
+ if(conEval != null){
+ bDefinitionsSet.addAll(conEval.getConstantOverrideTable().values());
+ }
+
AssumeNode[] assumes = moduleNode.getAssumptions();
for (int i = 0; i < assumes.length; i++) {
visitExprNode(assumes[i].getAssume(), null);
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index 604118c9573427cd31ff5dc9c9931f2a2cbfa499..08b9d0b670c0d66e7c54ac6e0935adfa364288a0 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -7,8 +7,10 @@ package de.tla2b.analysis;
import java.util.ArrayList;
import java.util.HashSet;
import java.util.Hashtable;
+import java.util.Iterator;
import java.util.LinkedList;
import java.util.Set;
+import java.util.Map.Entry;
import de.tla2b.config.ConfigfileEvaluator;
import de.tla2b.config.TLCValueNode;
@@ -22,7 +24,6 @@ import de.tla2b.global.BBuildIns;
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.TranslationGlobals;
import de.tla2b.types.*;
-
import tla2sany.semantic.ASTConstants;
import tla2sany.semantic.AssumeNode;
import tla2sany.semantic.AtNode;
@@ -56,6 +57,8 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
private Hashtable<OpDeclNode, ValueObj> constantAssignments;
+ private ConfigfileEvaluator conEval;
+
/**
* @param moduleNode2
* @param conEval
@@ -67,6 +70,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
if (conEval != null) {
this.bConstList = conEval.getbConstantList();
this.constantAssignments = conEval.getConstantAssignments();
+ this.conEval = conEval;
}
this.inits = specAnalyser.getInits();
this.nextExpr = specAnalyser.getNext();
@@ -111,6 +115,32 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
}
evalDefinitions(moduleNode.getOpDefs());
+
+ if(conEval != null){
+ Iterator<Entry<OpDeclNode, OpDefNode>> iter = conEval
+ .getConstantOverrideTable().entrySet().iterator();
+ while (iter.hasNext()) {
+ Entry<OpDeclNode, OpDefNode> entry = iter.next();
+ OpDeclNode con = entry.getKey();
+ if(!bConstList.contains(con)){
+ continue;
+ }
+ OpDefNode def = entry.getValue();
+ TLAType defType = (TLAType) def.getToolObject(TYPE_ID);
+ TLAType conType = (TLAType) con.getToolObject(TYPE_ID);
+
+ try {
+ TLAType result = defType.unify(conType);
+ con.setToolObject(TYPE_ID, result);
+ } catch (UnificationException e) {
+ throw new TypeErrorException(String.format(
+ "Expected %s, found %s at constant '%s'.", defType,
+ conType, con.getName())
+ );
+ }
+ }
+ }
+
evalAssumptions(moduleNode.getAssumptions());
if (inits != null) {
@@ -129,7 +159,7 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
TLAType varType = (TLAType) var.getToolObject(TYPE_ID);
if (varType.isUntyped()) {
throw new TypeErrorException("Variable '" + var.getName()
- + "' has no cype!");
+ + "' has no type!");
}
}
@@ -311,11 +341,10 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
"SubstInKind should never occur after InstanceTransformation");
}
- case DecimalKind:{
+ case DecimalKind: {
// currently not supported
}
-
-
+
}
throw new NotImplementedException(exprNode.toString(2));
diff --git a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java b/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
index 99793b4b8d880fbffb2441219fbff3da1f04560a..518788a9bd75a83d55dd5fe50b5d86bfe8d60e83 100644
--- a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
+++ b/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
@@ -14,6 +14,7 @@ import java.util.LinkedHashSet;
import java.util.Map;
import java.util.Set;
import java.util.SortedSet;
+import java.util.Map.Entry;
import de.tla2b.exceptions.ConfigFileErrorException;
import de.tla2b.exceptions.UnificationException;
@@ -25,9 +26,6 @@ import de.tla2b.types.SetType;
import de.tla2b.types.StringType;
import de.tla2b.types.TLAType;
import de.tla2b.types.Untyped;
-
-
-
import tla2sany.semantic.InstanceNode;
import tla2sany.semantic.ModuleNode;
import tla2sany.semantic.OpDeclNode;
@@ -57,8 +55,7 @@ public class ConfigfileEvaluator {
private OpDefNode specNode; // SPECIFICATION node, may be null
private OpDefNode nextNode; // NEXT node, may be null
private OpDefNode initNode; // INIT node, may be null
- private ArrayList<OpDefNode> invariantNodeList;
- // INVARIANT nodes, may be null
+ private final ArrayList<OpDefNode> invariantNodeList = new ArrayList<OpDefNode>();
private ArrayList<String> enumeratedSet;
private LinkedHashMap<String, EnumType> enumeratedTypes;
private Hashtable<OpDeclNode, ValueObj> constantAssignments;
@@ -66,10 +63,10 @@ public class ConfigfileEvaluator {
// contains it type
private Hashtable<OpDefNode, ValueObj> operatorAssignments;
// def = 1
-
+
private ArrayList<OpDefNode> operatorModelvalues;
- private ArrayList<OpDeclNode> bConstantList;
+ private final ArrayList<OpDeclNode> bConstantList = new ArrayList<OpDeclNode>();
// List of constants in the resulting B machine. This list does not contain
// a TLA+ constant if the constant is substituted by a modelvalue with the
// same name (the constant name is moved to an enumerated set) or if the
@@ -83,6 +80,7 @@ public class ConfigfileEvaluator {
// configuration file. All constants with arguments have to be overridden in
// the configuration file.
+
/**
* @param configAst
* @param moduleNode
@@ -98,13 +96,20 @@ public class ConfigfileEvaluator {
}
constants = new Hashtable<String, OpDeclNode>();
- bConstantList = new ArrayList<OpDeclNode>();
OpDeclNode[] cons = moduleNode.getConstantDecls();
for (int i = 0; i < cons.length; i++) {
constants.put(cons[i].getName().toString(), cons[i]);
bConstantList.add(cons[i]);
}
+ initialize();
+ }
+
+ public ConfigfileEvaluator() {
+ initialize();
+ }
+
+ private void initialize() {
this.constantOverrideTable = new Hashtable<OpDeclNode, OpDefNode>();
this.operatorOverrideTable = new Hashtable<OpDefNode, OpDefNode>();
@@ -142,8 +147,10 @@ public class ConfigfileEvaluator {
evalModConOrDefAssignments();
evalModConOrDefOverrides();
+
}
+
private void evalNext() throws ConfigFileErrorException {
String next = configAst.getNext();
if (!next.equals("")) {
@@ -196,7 +203,6 @@ public class ConfigfileEvaluator {
Vect v = configAst.getInvariants();
if (v.capacity() != 0) {
- invariantNodeList = new ArrayList<OpDefNode>();
for (int i = 0; i < v.capacity(); i++) {
if (v.elementAt(i) != null) {
String inv = (String) v.elementAt(i);
@@ -243,7 +249,9 @@ public class ConfigfileEvaluator {
left, left, conNode.getArity(), right,
rightDefNode.getArity()));
}
- bConstantList.remove(conNode);
+ if(conNode.getArity()>0){
+ bConstantList.remove(conNode);
+ }
constantOverrideTable.put(conNode, rightDefNode);
} else if (definitions.containsKey(left)) {
// an operator is overridden by another operator
@@ -287,14 +295,15 @@ public class ConfigfileEvaluator {
* same as the name of constants, then the constant declaration
* in the resulting B machine disappears
**/
- if (symbolType instanceof EnumType && symbolName.equals(symbolValue.toString())) {
+ if (symbolType instanceof EnumType
+ && symbolName.equals(symbolValue.toString())) {
bConstantList.remove(c);
}
} else if (definitions.containsKey(symbolName)) {
OpDefNode def = definitions.get(symbolName);
ValueObj valueObj = new ValueObj(symbolValue, symbolType);
operatorAssignments.put(def, valueObj);
-
+
if (symbolType instanceof SetType) {
if (((SetType) symbolType).getSubType() instanceof EnumType) {
operatorModelvalues.add(def);
@@ -302,7 +311,7 @@ public class ConfigfileEvaluator {
} else if ((symbolType instanceof EnumType)) {
operatorModelvalues.add(def);
}
-
+
} else {
// every constants or operator in the configuration file must
// appear in the TLA+
@@ -359,7 +368,7 @@ public class ConfigfileEvaluator {
} else if ((symbolType instanceof EnumType)) {
operatorModelvalues.add(def);
}
-
+
}
}
}
@@ -408,18 +417,18 @@ public class ConfigfileEvaluator {
else {
InstanceNode[] instanceNodes = moduleNode.getInstances();
for (int i = 0; i < instanceNodes.length; i++) {
-// if (instanceNodes[i].getModule().getName().toString()
-// .equals(moduleName)) {
-// /*
-// * A constant overridden in a instanced module make
-// * no sence. Such a constant will be overridden by
-// * the instance statement
-// */
-// throw new ConfigFileErrorException(
-// String.format(
-// "Invalid substitution for constant '%s' of module '%s'.\n A Constant of an instanced module can not be overriden.",
-// left, mNode.getName().toString()));
-// }
+ // if (instanceNodes[i].getModule().getName().toString()
+ // .equals(moduleName)) {
+ // /*
+ // * A constant overridden in a instanced module make
+ // * no sence. Such a constant will be overridden by
+ // * the instance statement
+ // */
+ // throw new ConfigFileErrorException(
+ // String.format(
+ // "Invalid substitution for constant '%s' of module '%s'.\n A Constant of an instanced module can not be overriden.",
+ // left, mNode.getName().toString()));
+ // }
}
// a constant is overridden by an operator
OpDeclNode conNode = (OpDeclNode) opDefOrDeclNode;
@@ -457,17 +466,16 @@ public class ConfigfileEvaluator {
/*
* search module in instanced modules
*/
-
- OpDefNode [] defs = moduleNode.getOpDefs();
- for (int j = defs.length-1; j > 0; j--) {
+ OpDefNode[] defs = moduleNode.getOpDefs();
+ for (int j = defs.length - 1; j > 0; j--) {
OpDefNode def = null;
OpDefNode source = defs[j];
- while(def!=source){
+ while (def != source) {
def = source;
source = def.getSource();
ModuleNode m = def.getOriginallyDefinedInModuleNode();
- if(m.getName().toString().equals(moduleName)){
+ if (m.getName().toString().equals(moduleName)) {
return m;
}
}
@@ -617,8 +625,8 @@ public class ConfigfileEvaluator {
public ArrayList<String> getEnumerationSet() {
return this.enumeratedSet;
}
-
- public ArrayList<OpDefNode> getOperatorModelvalues(){
+
+ public ArrayList<OpDefNode> getOperatorModelvalues() {
return this.operatorModelvalues;
}
}
diff --git a/src/main/java/de/tla2b/config/ModuleOverrider.java b/src/main/java/de/tla2b/config/ModuleOverrider.java
index e344f8d70fd12964749248ec2ddd35d9667b0608..b90e218bf0caaa96fe45925544d10243a7ad4c2f 100644
--- a/src/main/java/de/tla2b/config/ModuleOverrider.java
+++ b/src/main/java/de/tla2b/config/ModuleOverrider.java
@@ -49,6 +49,7 @@ public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
this.constantOverrideTable = conEval.getConstantOverrideTable();
this.operatorOverrideTable = conEval.getOperatorOverrideTable();
this.operatorAssignments = conEval.getOperatorAssignments();
+
}
public void start() {
@@ -146,7 +147,7 @@ public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
SymbolNode s = n.getOperator();
switch (s.getKind()) {
case ConstantDeclKind: {
- if (constantOverrideTable.containsKey(s)) {
+ if (constantOverrideTable.containsKey(s) && s.getArity() > 0) {
SymbolNode newOperator = constantOverrideTable.get(s);
OpApplNode newNode = null;
try {
@@ -162,7 +163,6 @@ public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
n.getArgs()[i] = res;
}
}
-
}
// n.setOperator(constantOverrideTable.get(s));
return newNode;
@@ -170,7 +170,7 @@ public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
break;
}
- case FormalParamKind: // Params are not global in the modul
+ case FormalParamKind: // Params are not global in the module
case VariableDeclKind: // TODO try to override variable
break;
@@ -193,7 +193,8 @@ public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
OpDefNode def = (OpDefNode) n.getOperator();
try {
newNode = new OpApplNode(newOperator, n.getArgs(),
- n.getTreeNode(), def.getOriginallyDefinedInModuleNode());
+ n.getTreeNode(),
+ def.getOriginallyDefinedInModuleNode());
} catch (AbortException e) {
e.printStackTrace();
}
diff --git a/src/main/java/de/tla2b/pprint/ASTPrettyPrinter.java b/src/main/java/de/tla2b/pprint/ASTPrettyPrinter.java
new file mode 100644
index 0000000000000000000000000000000000000000..16c4ca33929995d6bca34c91d0d6e8c5566d4152
--- /dev/null
+++ b/src/main/java/de/tla2b/pprint/ASTPrettyPrinter.java
@@ -0,0 +1,643 @@
+package de.tla2b.pprint;
+
+import java.util.ArrayList;
+import java.util.Hashtable;
+import java.util.Iterator;
+import java.util.List;
+
+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.ADefinitionExpression;
+import de.be4.classicalb.core.parser.node.ADefinitionPredicate;
+import de.be4.classicalb.core.parser.node.AExpressionDefinitionDefinition;
+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.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.Start;
+import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
+import de.be4.classicalb.core.parser.node.Token;
+
+public class ASTPrettyPrinter extends ExtendedDFAdapter {
+ private final StringBuilder builder = new StringBuilder();
+ private final StringBuilder sb = new StringBuilder();
+
+ private static final int no = 0;
+ private static final int left = 1;
+ private static final int right = 2;
+ public static final int max = 500;
+
+ private final static Hashtable<String, NodeInfo> infoTable = new Hashtable<String, NodeInfo>();
+
+ private static void putInfixOperator(String nodeName, String symbol,
+ int precedence, int a) {
+ infoTable.put(nodeName, new NodeInfo(null, null, null, null, " "
+ + symbol + " ", null, precedence, a));
+ }
+
+ private static void putPrefixOperator(String nodeName, String symbol,
+ int precedence, int a) {
+ infoTable.put(nodeName, new NodeInfo(symbol, null, null, null, null,
+ null, precedence, a));
+ }
+
+ private static void putInfixOperatorWithoutSpaces(String nodeName,
+ String symbol, int precedence, int a) {
+ infoTable.put(nodeName, new NodeInfo(null, null, null, null, symbol,
+ null, precedence, a));
+ }
+
+ private static void putPreEnd(String nodeName, String pre, String end) {
+ infoTable.put(nodeName, new NodeInfo(pre, null, null, null, null, end,
+ null, null));
+ }
+
+ private static void putClause(String nodeName, String pre, String end) {
+ infoTable.put(nodeName, new NodeInfo(pre + "\n", null, null, null,
+ null, end, null, null));
+ }
+
+ private static void putSymbol(String nodeName, String symbol) {
+ infoTable.put(nodeName, new NodeInfo(symbol, null, null, null, null,
+ null, null, null));
+ }
+
+ private static void put(String nodeName, String pre, String beginList,
+ String betweenListElements, String endList, String betweenChildren,
+ String end) {
+ infoTable
+ .put(nodeName, new NodeInfo(pre, beginList,
+ betweenListElements, endList, betweenChildren, end,
+ null, null));
+ }
+
+ private static void putDeclarationClause(String nodeName,
+ String clauseName, String betweenListElements) {
+ NodeInfo info = new NodeInfo();
+ info.setPre(clauseName + " ");
+ info.setBetweenListElements(betweenListElements + " ");
+ info.setEnd("\n");
+ infoTable.put(nodeName, info);
+ }
+
+ static {
+
+ putDeclarationClause("ASetsMachineClause", "SETS", ";");
+ putDeclarationClause("AAbstractConstantsMachineClause",
+ "ABSTRACT_CONSTANTS", ",");
+ putDeclarationClause("AVariablesMachineClause", "VARIABLES", ",");
+
+ put("AEnumeratedSetSet", null, null, ", ", null, " = {", "}");
+ // AEnumeratedSetSet e;e.g
+ putClause("ADefinitionsMachineClause", "DEFINITIONS", "");
+ putClause("APropertiesMachineClause", "PROPERTIES", "\n");
+ putClause("AInvariantMachineClause", "INVARIANT", "\n");
+ putClause("AInitialisationMachineClause", "INITIALISATION", "\n");
+ putClause("AOperationsMachineClause", "OPERATIONS", "\n");
+
+ // infix operators
+ putInfixOperator("AImplicationPredicate", "=>", 30, left);
+ putInfixOperator("AEquivalencePredicate", "<=>", 30, left);
+
+ putInfixOperator("AConjunctPredicate", "&", 40, left);
+ putInfixOperator("ADisjunctPredicate", "or", 40, left);
+
+ putInfixOperator("ALessPredicate", "<", 50, left);
+ putInfixOperator("AGreaterPredicate", ">", 50, left);
+ putInfixOperator("ALessEqualPredicate", "<=", 50, left);
+ putInfixOperator("AGreaterEqualPredicate", ">=", 50, left);
+
+ putInfixOperator("AEqualPredicate", "=", 50, left);
+ putInfixOperator("ANotEqualPredicate", "/=", 50, left);
+
+ putInfixOperator("AMemberPredicate", ":", 60, left);
+ putInfixOperator("ANotMemberPredicate", "/:", 60, left);
+
+ putInfixOperator("ASubsetPredicate", "<:", 60, left); // <: subseteq
+
+ putInfixOperator("APartialFunctionExpression", "+->", 125, left);
+ putInfixOperator("ATotalFunctionExpression", "-->", 125, left);
+
+ putInfixOperator("AOverwriteExpression", "<+", 160, left);
+ putInfixOperator("AUnionExpression", "\\/", 160, left);
+ putInfixOperator("AIntersectionExpression", "/\\", 160, left);
+
+ putInfixOperator("AInsertTailExpression", "<-", 160, left);
+ putInfixOperator("AConcatExpression", "^", 160, left);
+
+ putInfixOperator("ARestrictFrontExpression", "/|\\", 160, left);
+ putInfixOperator("ARestrictTailExpression", "\\|/", 160, left);
+
+ putInfixOperator("AIntervalExpression", "..", 170, left);
+
+ putInfixOperator("AAddExpression", "+", 180, left);
+ putInfixOperator("AMinusOrSetSubtractExpression", "-", 180, left);
+
+ putInfixOperator("ACartesianProductExpression", "*", 190, left);
+ putInfixOperator("AMultOrCartExpression", "*", 190, left);
+ putInfixOperator("ADivExpression", "/", 190, left);
+
+ putInfixOperator("APowerOfExpression", "**", 200, right);
+
+ putPrefixOperator("AUnaryMinusExpression", "-", 210, no);
+
+ putInfixOperatorWithoutSpaces("ARecordFieldExpression", "'", 250, left);
+
+ infoTable.put("AFunctionExpression", new NodeInfo(null, "(", ", ", ")",
+ null, null, 300, no));
+
+ // single symbols
+ putSymbol("AIntegerSetExpression", "INTEGER");
+ putSymbol("AIntSetExpression", "INT");
+ putSymbol("ANaturalSetExpression", "NATURAL");
+ putSymbol("ANatural1SetExpression", "NATURAL1");
+ putSymbol("ANatSetExpression", "NAT");
+ putSymbol("ANat1SetExpression", "NAT1");
+ putSymbol("ABooleanTrueExpression", "TRUE");
+ putSymbol("ABooleanFalseExpression", "FALSE");
+ putSymbol("AEmptySetExpression", "{}");
+ putSymbol("ABoolSetExpression", "BOOL");
+ putSymbol("AStringSetExpression", "STRING");
+
+ putPreEnd("APowSubsetExpression", "POW(", ")");
+ putPreEnd("AConvertBoolExpression", "bool(", ")");
+ putPreEnd("ADomainExpression", "dom(", ")");
+ putPreEnd("ANegationPredicate", "not(", ")");
+ putPreEnd("ASizeExpression", "size(", ")");
+ putPreEnd("ASeqExpression", "seq(", ")");
+ putPreEnd("ASeq1Expression", "seq1(", ")");
+ putPreEnd("AGeneralUnionExpression", "union(", ")");
+ putPreEnd("AStringExpression", "\"", "\"");
+ putPreEnd("AFinSubsetExpression", "FIN(", ")");
+ putPreEnd("ACardExpression", "card(", ")");
+ putPreEnd("AFirstExpression", "first(", ")");
+ putPreEnd("ATailExpression", "tail(", ")");
+
+ put("ASetExtensionExpression", null, "{", ", ", "}", null, null);
+ put("AStructExpression", "struct", "(", ", ", ")", null, null);
+ put("ARecExpression", "rec", "(", ", ", ")", null, null);
+ put("ARecEntry", null, null, null, null, ":", null);
+
+ put("ACoupleExpression", null, "(", ",", ")", null, null);
+ put("ASequenceExtensionExpression", null, "[", ",", "]", null, null);
+
+ put("AForallPredicate", "!", "(", ",", ")", ".(", ")");
+ put("AExistsPredicate", "#", "(", ",", ")", ".(", ")");
+
+ put("AAssignSubstitution", null, null, ",", null, " := ", null);
+
+ put("AComprehensionSetExpression", "{", "", ",", "", " | ", "}");
+
+ }
+
+ @Override
+ public String toString() {
+ return builder.toString();
+ }
+
+ private NodeInfo getInfo(final Node node) {
+ final String nodeName = node.getClass().getSimpleName();
+ if (infoTable.containsKey(nodeName)) {
+ return infoTable.get(nodeName);
+ } else {
+ return new NodeInfo();
+ }
+ }
+
+ @Override
+ public void defaultIn(final Node node) {
+ super.defaultIn(node);
+ if (makeBrackets(node)) {
+ sb.append("(");
+ }
+ sb.append(getInfo(node).pre);
+ builder.append(node.getClass().getSimpleName());
+ builder.append("(");
+ }
+
+ private boolean makeBrackets(Node node) {
+ NodeInfo infoNode = getInfo(node);
+ Node parent = node.parent();
+ if (parent == null) {
+ return false;
+ }
+ NodeInfo infoParent = getInfo(parent);
+ if (infoNode.precedence == max || infoParent.precedence == max)
+ return false;
+
+ if (infoParent.precedence >= infoNode.precedence) {
+ return true;
+ }
+
+ return false;
+ }
+
+ @Override
+ public void defaultCase(final Node node) {
+ super.defaultCase(node);
+ if (node instanceof Token) {
+ builder.append(((Token) node).getText());
+ sb.append(((Token) node).getText());
+ } else {
+ builder.append(node.toString());
+ sb.append(node.toString());
+ }
+
+ }
+
+ @Override
+ public void defaultOut(final Node node) {
+ super.defaultOut(node);
+ builder.append(")");
+ sb.append(getInfo(node).end);
+ if (makeBrackets(node)) {
+ sb.append(")");
+ }
+ }
+
+ @Override
+ public void beginList(final Node parent) {
+ builder.append('[');
+ sb.append(getInfo(parent).beginList);
+ }
+
+ @Override
+ public void betweenListElements(final Node parent) {
+ builder.append(',');
+ sb.append(getInfo(parent).betweenListElements);
+ }
+
+ @Override
+ public void endList(final Node parent) {
+ builder.append(']');
+ sb.append(getInfo(parent).endList);
+ }
+
+ @Override
+ public void betweenChildren(final Node parent) {
+ builder.append(',');
+ sb.append(getInfo(parent).betweenChildren);
+ }
+
+ @Override
+ public void caseStart(final Start node) {
+ inStart(node);
+ node.getPParseUnit().apply(this);
+ node.getEOF().apply(this);
+ outStart(node);
+ }
+
+ public static String getIdentifierAsString(
+ final List<TIdentifierLiteral> idElements) {
+ final String string;
+ if (idElements.size() == 1) {
+ // faster version for the simple case
+ string = idElements.get(0).getText();
+ } else {
+ final StringBuilder idName = new StringBuilder();
+
+ boolean first = true;
+ for (final TIdentifierLiteral e : idElements) {
+ if (first) {
+ first = false;
+ } else {
+ idName.append('.');
+ }
+ idName.append(e.getText());
+ }
+ string = idName.toString();
+ }
+ return string.trim();
+ }
+
+ public String getResult() {
+ return sb.toString();
+ }
+
+ @Override
+ public void caseAAbstractMachineParseUnit(AAbstractMachineParseUnit node) {
+ sb.append("MACHINE ");
+ if (node.getVariant() != null) {
+ node.getVariant().apply(this);
+ }
+ if (node.getHeader() != null) {
+ node.getHeader().apply(this);
+ }
+ sb.append("\n");
+ List<PMachineClause> copy = new ArrayList<PMachineClause>(
+ node.getMachineClauses());
+ for (PMachineClause e : copy) {
+ e.apply(this);
+ }
+ sb.append("END");
+ }
+
+ @Override
+ public void caseAOperationsMachineClause(final AOperationsMachineClause node) {
+ sb.append("OPERATIONS\n");
+ final List<POperation> copy = new ArrayList<POperation>(
+ node.getOperations());
+ for (final Iterator<POperation> iterator = copy.iterator(); iterator
+ .hasNext();) {
+ final POperation e = iterator.next();
+ e.apply(this);
+ if (iterator.hasNext()) {
+ sb.append(";\n");
+ }
+ sb.append("\n");
+ }
+ }
+
+ @Override
+ public void caseAOperation(AOperation node) {
+ sb.append(" ");
+ List<PExpression> output = new ArrayList<PExpression>(
+ node.getReturnValues());
+ if (output.size() > 0) {
+ for (final Iterator<PExpression> iterator = output.iterator(); iterator
+ .hasNext();) {
+ final PExpression e = iterator.next();
+ e.apply(this);
+ if (iterator.hasNext()) {
+ sb.append(", ");
+ }
+ }
+ sb.append("<-- ");
+ }
+ List<TIdentifierLiteral> copy = new ArrayList<TIdentifierLiteral>(
+ node.getOpName());
+ for (TIdentifierLiteral e : copy) {
+ e.apply(this);
+ }
+ List<PExpression> parameters = new ArrayList<PExpression>(
+ node.getParameters());
+ if (parameters.size() > 0) {
+ sb.append("(");
+ for (final Iterator<PExpression> iterator = parameters.iterator(); iterator
+ .hasNext();) {
+ final PExpression e = iterator.next();
+ e.apply(this);
+
+ if (iterator.hasNext()) {
+ sb.append(", ");
+ }
+ }
+ sb.append(")");
+ }
+ sb.append(" = ");
+ node.getOperationBody().apply(this);
+ }
+
+ @Override
+ public void caseABecomesSuchSubstitution(final ABecomesSuchSubstitution node) {
+ final List<PExpression> copy = new ArrayList<PExpression>(
+ node.getIdentifiers());
+ for (final Iterator<PExpression> iterator = copy.iterator(); iterator
+ .hasNext();) {
+ final PExpression e = iterator.next();
+ e.apply(this);
+ if (iterator.hasNext()) {
+ sb.append(", ");
+ }
+ }
+ sb.append(":(");
+ node.getPredicate().apply(this);
+ sb.append(")");
+ }
+
+ public void caseAAnySubstitution(final AAnySubstitution node) {
+ sb.append("ANY ");
+ final List<PExpression> copy = new ArrayList<PExpression>(
+ node.getIdentifiers());
+ beginList(node);
+ for (final Iterator<PExpression> iterator = copy.iterator(); iterator
+ .hasNext();) {
+ final PExpression e = iterator.next();
+ e.apply(this);
+ if (iterator.hasNext()) {
+ sb.append(", ");
+ }
+ }
+ endList(node);
+ sb.append(" WHERE ");
+ node.getWhere().apply(this);
+ sb.append(" THEN ");
+ node.getThen().apply(this);
+ sb.append(" END");
+ }
+
+ @Override
+ public void caseAPredicateDefinitionDefinition(
+ APredicateDefinitionDefinition node) {
+ sb.append(" ");
+ node.getName().apply(this);
+ List<PExpression> copy = new ArrayList<PExpression>(
+ node.getParameters());
+ if (copy.size() > 0) {
+ sb.append("(");
+ for (final Iterator<PExpression> iterator = copy.iterator(); iterator
+ .hasNext();) {
+ final PExpression e = iterator.next();
+ e.apply(this);
+ if (iterator.hasNext()) {
+ sb.append(", ");
+ }
+ }
+ sb.append(")");
+ }
+ sb.append(" == ");
+ node.getRhs().apply(this);
+ sb.append(";\n");
+ }
+
+ @Override
+ public void caseADefinitionPredicate(final ADefinitionPredicate node) {
+ node.getDefLiteral().apply(this);
+ final List<PExpression> copy = new ArrayList<PExpression>(
+ node.getParameters());
+ if (copy.size() > 0) {
+ sb.append("(");
+ for (final Iterator<PExpression> iterator = copy.iterator(); iterator
+ .hasNext();) {
+ final PExpression e = iterator.next();
+ e.apply(this);
+ if (iterator.hasNext()) {
+ sb.append(", ");
+ }
+ }
+ sb.append(")");
+ }
+ }
+
+ @Override
+ public void caseAExpressionDefinitionDefinition(
+ final AExpressionDefinitionDefinition node) {
+ sb.append(" ");
+ node.getName().apply(this);
+ List<PExpression> copy = new ArrayList<PExpression>(
+ node.getParameters());
+ if (copy.size() > 0) {
+ sb.append("(");
+ for (final Iterator<PExpression> iterator = copy.iterator(); iterator
+ .hasNext();) {
+ final PExpression e = iterator.next();
+ e.apply(this);
+ if (iterator.hasNext()) {
+ sb.append(", ");
+ }
+ }
+ sb.append(")");
+ }
+ sb.append(" == ");
+ node.getRhs().apply(this);
+ sb.append(";\n");
+ }
+
+ @Override
+ public void caseADefinitionExpression(final ADefinitionExpression node) {
+ node.getDefLiteral().apply(this);
+ final List<PExpression> copy = new ArrayList<PExpression>(
+ node.getParameters());
+ if (copy.size() > 0) {
+ sb.append("(");
+ for (final Iterator<PExpression> iterator = copy.iterator(); iterator
+ .hasNext();) {
+ final PExpression e = iterator.next();
+ e.apply(this);
+ if (iterator.hasNext()) {
+ sb.append(", ");
+ }
+ }
+ sb.append(")");
+ }
+ }
+
+ @Override
+ public void caseALambdaExpression(final ALambdaExpression node) {
+ final List<PExpression> copy = new ArrayList<PExpression>(
+ node.getIdentifiers());
+ sb.append("%(");
+ for (final Iterator<PExpression> iterator = copy.iterator(); iterator
+ .hasNext();) {
+ final PExpression e = iterator.next();
+ e.apply(this);
+
+ if (iterator.hasNext()) {
+ sb.append(", ");
+ }
+ }
+ sb.append(").(");
+ node.getPredicate().apply(this);
+ sb.append(" | ");
+ node.getExpression().apply(this);
+ sb.append(")");
+ }
+
+}
+
+class NodeInfo {
+ String pre = "";
+ String beginList = "";
+ String betweenListElements = "";
+ String endList = "";
+ String betweenChildren = "";
+ String end = "";
+ Integer precedence = ASTPrettyPrinter.max;
+ Integer associative = 0;
+
+ public String getPre() {
+ return pre;
+ }
+
+ public void setPre(String pre) {
+ this.pre = pre;
+ }
+
+ public String getBeginList() {
+ return beginList;
+ }
+
+ public void setBeginList(String beginList) {
+ this.beginList = beginList;
+ }
+
+ public String getBetweenListElements() {
+ return betweenListElements;
+ }
+
+ public void setBetweenListElements(String betweenListElements) {
+ this.betweenListElements = betweenListElements;
+ }
+
+ public String getEndList() {
+ return endList;
+ }
+
+ public void setEndList(String endList) {
+ this.endList = endList;
+ }
+
+ public String getBetweenChildren() {
+ return betweenChildren;
+ }
+
+ public void setBetweenChildren(String betweenChildren) {
+ this.betweenChildren = betweenChildren;
+ }
+
+ public String getEnd() {
+ return end;
+ }
+
+ public void setEnd(String end) {
+ this.end = end;
+ }
+
+ public Integer getPrecedence() {
+ return precedence;
+ }
+
+ public void setPrecedence(Integer precedence) {
+ this.precedence = precedence;
+ }
+
+ public Integer getAssociative() {
+ return associative;
+ }
+
+ public void setAssociative(Integer associative) {
+ this.associative = associative;
+ }
+
+ public NodeInfo() {
+
+ }
+
+ public NodeInfo(String pre, String beginList, String betweenListElements,
+ String endList, String betweenChildren, String end,
+ Integer precedence, Integer associative) {
+ if (pre != null)
+ this.pre = pre;
+ if (beginList != null)
+ this.beginList = beginList;
+ if (betweenListElements != null)
+ this.betweenListElements = betweenListElements;
+ if (endList != null)
+ this.endList = endList;
+ if (betweenChildren != null)
+ this.betweenChildren = betweenChildren;
+ if (end != null)
+ this.end = end;
+ if (precedence != null)
+ this.precedence = precedence;
+ if (associative != null)
+ this.associative = associative;
+ }
+
+}
\ No newline at end of file
diff --git a/src/main/java/de/tla2b/pprint/AbstractExpressionPrinter.java b/src/main/java/de/tla2b/pprint/AbstractExpressionPrinter.java
index 78231d91570b2b7319b73ca9f2e91db907c0b46e..c00c494b16388995f1a71fb5c6517f4bc5be71fa 100644
--- a/src/main/java/de/tla2b/pprint/AbstractExpressionPrinter.java
+++ b/src/main/java/de/tla2b/pprint/AbstractExpressionPrinter.java
@@ -414,7 +414,7 @@ public abstract class AbstractExpressionPrinter extends BuiltInOPs implements
case OPCODE_sso: { // $SubsetOf Represents {x \in S : P}
// TODO tuple with more than 2 arguments
FormalParamNode[][] params = n.getBdedQuantSymbolLists();
- ExprNode[] bounds = n.getBdedQuantBounds();
+ //ExprNode[] bounds = n.getBdedQuantBounds();
StringBuilder temp = new StringBuilder();
if (params[0].length > 0) {
diff --git a/src/main/java/de/tla2b/pprint/BAstCreator.java b/src/main/java/de/tla2b/pprint/BAstCreator.java
index 1cf06cba92228dd5ae5c99e8b49a239d60c675a2..ce21166589c99f54267724e9d22a2b16c81344a7 100644
--- a/src/main/java/de/tla2b/pprint/BAstCreator.java
+++ b/src/main/java/de/tla2b/pprint/BAstCreator.java
@@ -3,10 +3,14 @@ package de.tla2b.pprint;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Hashtable;
+import java.util.Iterator;
+import java.util.LinkedList;
import java.util.List;
+import java.util.Map.Entry;
import tla2sany.semantic.ASTConstants;
import tla2sany.semantic.AssumeNode;
+import tla2sany.semantic.AtNode;
import tla2sany.semantic.ExprNode;
import tla2sany.semantic.ExprOrOpArgNode;
import tla2sany.semantic.FormalParamNode;
@@ -17,6 +21,8 @@ import tla2sany.semantic.OpDeclNode;
import tla2sany.semantic.OpDefNode;
import tla2sany.semantic.StringNode;
import tlc2.tool.BuiltInOPs;
+import tlc2.value.SetEnumValue;
+import de.be4.classicalb.core.parser.Definitions;
import de.be4.classicalb.core.parser.node.AAbstractConstantsMachineClause;
import de.be4.classicalb.core.parser.node.AAbstractMachineParseUnit;
import de.be4.classicalb.core.parser.node.AAddExpression;
@@ -32,13 +38,18 @@ import de.be4.classicalb.core.parser.node.AConcatExpression;
import de.be4.classicalb.core.parser.node.AConjunctPredicate;
import de.be4.classicalb.core.parser.node.AConvertBoolExpression;
import de.be4.classicalb.core.parser.node.ACoupleExpression;
+import de.be4.classicalb.core.parser.node.ADefinitionExpression;
+import de.be4.classicalb.core.parser.node.ADefinitionPredicate;
+import de.be4.classicalb.core.parser.node.ADefinitionsMachineClause;
import de.be4.classicalb.core.parser.node.ADisjunctPredicate;
import de.be4.classicalb.core.parser.node.ADivExpression;
import de.be4.classicalb.core.parser.node.ADomainExpression;
import de.be4.classicalb.core.parser.node.AEmptySetExpression;
+import de.be4.classicalb.core.parser.node.AEnumeratedSetSet;
import de.be4.classicalb.core.parser.node.AEqualPredicate;
import de.be4.classicalb.core.parser.node.AEquivalencePredicate;
import de.be4.classicalb.core.parser.node.AExistsPredicate;
+import de.be4.classicalb.core.parser.node.AExpressionDefinitionDefinition;
import de.be4.classicalb.core.parser.node.AFinSubsetExpression;
import de.be4.classicalb.core.parser.node.AFirstExpression;
import de.be4.classicalb.core.parser.node.AForallPredicate;
@@ -69,15 +80,20 @@ import de.be4.classicalb.core.parser.node.ANotEqualPredicate;
import de.be4.classicalb.core.parser.node.ANotMemberPredicate;
import de.be4.classicalb.core.parser.node.AOperation;
import de.be4.classicalb.core.parser.node.AOperationsMachineClause;
+import de.be4.classicalb.core.parser.node.AOverwriteExpression;
import de.be4.classicalb.core.parser.node.APowSubsetExpression;
import de.be4.classicalb.core.parser.node.APowerOfExpression;
+import de.be4.classicalb.core.parser.node.APredicateDefinitionDefinition;
import de.be4.classicalb.core.parser.node.APropertiesMachineClause;
import de.be4.classicalb.core.parser.node.ARecEntry;
import de.be4.classicalb.core.parser.node.ARecExpression;
import de.be4.classicalb.core.parser.node.ARecordFieldExpression;
+import de.be4.classicalb.core.parser.node.ARestrictFrontExpression;
+import de.be4.classicalb.core.parser.node.ARestrictTailExpression;
import de.be4.classicalb.core.parser.node.ASeqExpression;
import de.be4.classicalb.core.parser.node.ASequenceExtensionExpression;
import de.be4.classicalb.core.parser.node.ASetExtensionExpression;
+import de.be4.classicalb.core.parser.node.ASetsMachineClause;
import de.be4.classicalb.core.parser.node.ASizeExpression;
import de.be4.classicalb.core.parser.node.AStringExpression;
import de.be4.classicalb.core.parser.node.AStringSetExpression;
@@ -89,22 +105,29 @@ import de.be4.classicalb.core.parser.node.AUnaryMinusExpression;
import de.be4.classicalb.core.parser.node.AUnionExpression;
import de.be4.classicalb.core.parser.node.AVariablesMachineClause;
import de.be4.classicalb.core.parser.node.EOF;
+import de.be4.classicalb.core.parser.node.PDefinition;
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.PPredicate;
import de.be4.classicalb.core.parser.node.PRecEntry;
+import de.be4.classicalb.core.parser.node.PSet;
import de.be4.classicalb.core.parser.node.Start;
+import de.be4.classicalb.core.parser.node.TDefLiteralPredicate;
import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
import de.be4.classicalb.core.parser.node.TIntegerLiteral;
import de.be4.classicalb.core.parser.node.TStringLiteral;
import de.tla2b.analysis.BOperation;
import de.tla2b.analysis.SpecAnalyser;
import de.tla2b.config.ConfigfileEvaluator;
+import de.tla2b.config.ValueObj;
import de.tla2b.global.BBuildIns;
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.Priorities;
import de.tla2b.global.TranslationGlobals;
+import de.tla2b.types.BoolType;
+import de.tla2b.types.EnumType;
+import de.tla2b.types.FunctionType;
import de.tla2b.types.IType;
import de.tla2b.types.SetType;
import de.tla2b.types.StructType;
@@ -118,18 +141,32 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
ConfigfileEvaluator conEval;
SpecAnalyser specAnalyser;
+ List<OpDeclNode> bConstants;
+
private ModuleNode moduleNode;
+ private Definitions bDefinitions = new Definitions();
public Start getStartNode() {
return start;
}
+ public Definitions getBDefinitions() {
+ // used for the recursive machine loader
+ return bDefinitions;
+ }
+
public BAstCreator(ModuleNode moduleNode, ConfigfileEvaluator conEval,
SpecAnalyser specAnalyser) {
this.conEval = conEval;
this.moduleNode = moduleNode;
this.specAnalyser = specAnalyser;
+ if (conEval != null) {
+ this.bConstants = conEval.getbConstantList();
+ } else {
+ this.bConstants = Arrays.asList(moduleNode.getConstantDecls());
+ }
+
machineClauseList = new ArrayList<PMachineClause>();
AAbstractMachineParseUnit aAbstractMachineParseUnit = new AAbstractMachineParseUnit();
@@ -140,6 +177,8 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
machineHeader.setName(headerName);
aAbstractMachineParseUnit.setHeader(machineHeader);
+ createSetsClause();
+ createDefintionClause();
createConstantsClause();
createPropertyClause();
createVariableClause();
@@ -153,6 +192,104 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
+ private void createSetsClause() {
+ if (conEval == null || conEval.getEnumerationSet() == null
+ || conEval.getEnumerationSet().size() == 0)
+ return;
+ ASetsMachineClause setsClause = new ASetsMachineClause();
+
+ ArrayList<EnumType> printed = new ArrayList<EnumType>();
+ OpDeclNode[] cons = moduleNode.getConstantDecls();
+ for (int i = 0; i < cons.length; i++) {
+ TLAType type = (TLAType) cons[i].getToolObject(TYPE_ID);
+ EnumType e = null;
+ if (type instanceof SetType) {
+ if (((SetType) type).getSubType() instanceof EnumType) {
+ e = (EnumType) ((SetType) type).getSubType();
+ if (!printed.contains(e)) {
+ printed.add(e);
+ }
+ }
+ } else if ((type instanceof EnumType)) {
+ e = (EnumType) type;
+ if (!printed.contains(e)) {
+ printed.add(e);
+ }
+ }
+ }
+
+ ArrayList<PSet> sets = new ArrayList<PSet>();
+ for (int i = 0; i < printed.size(); i++) {
+ AEnumeratedSetSet eSet = new AEnumeratedSetSet();
+ eSet.setIdentifier(createTIdentifierLiteral("ENUM" + (i + 1)));
+ List<PExpression> list = new ArrayList<PExpression>();
+ for (Iterator<String> iterator = printed.get(i).modelvalues
+ .iterator(); iterator.hasNext();) {
+ list.add(createIdentifierNode(iterator.next()));
+ }
+ eSet.setElements(list);
+ sets.add(eSet);
+ }
+ setsClause.setSetDefinitions(sets);
+ machineClauseList.add(setsClause);
+
+ }
+
+ private void createDefintionClause() {
+ 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 (conEval != null
+ && conEval.getConstantOverrideTable()
+ .containsValue(def)) {
+ continue;
+ }
+ bDefs.add(def);
+ }
+
+ }
+
+ if (bDefs.size() == 0) {
+ return;
+ }
+
+ ADefinitionsMachineClause defClause = new ADefinitionsMachineClause();
+ List<PDefinition> defs = new ArrayList<PDefinition>();
+ for (OpDefNode opDefNode : bDefs) {
+ TLAType type = (TLAType) opDefNode.getToolObject(TYPE_ID);
+ if (opDefNode.level == 2 || type instanceof BoolType) {
+ APredicateDefinitionDefinition d = new APredicateDefinitionDefinition();
+ d.setName(new TDefLiteralPredicate(opDefNode.getName()
+ .toString() + "_def"));
+ List<PExpression> list = new ArrayList<PExpression>();
+ for (int i = 0; i < opDefNode.getParams().length; i++) {
+ FormalParamNode p = opDefNode.getParams()[i];
+ list.add(createIdentifierNode(p.getName().toString()));
+ }
+ d.setParameters(list);
+ d.setRhs(visitExprNodePredicate(opDefNode.getBody()));
+ defs.add(d);
+ bDefinitions.addDefinition(d, Definitions.Type.Expression);
+ } else {
+ AExpressionDefinitionDefinition d = new AExpressionDefinitionDefinition();
+ d.setName(new TIdentifierLiteral(opDefNode.getName().toString()));
+ List<PExpression> list = new ArrayList<PExpression>();
+ for (int i = 0; i < opDefNode.getParams().length; i++) {
+ FormalParamNode p = opDefNode.getParams()[i];
+ list.add(createIdentifierNode(p.getName().toString()));
+ }
+ d.setParameters(list);
+ d.setRhs(visitExprNodeExpression(opDefNode.getBody()));
+ defs.add(d);
+ bDefinitions.addDefinition(d, Definitions.Type.Expression);
+ }
+
+ }
+ defClause.setDefinitions(defs);
+ machineClauseList.add(defClause);
+ }
+
private void createOperationsClause() {
ArrayList<BOperation> bOperations = specAnalyser.getBOperations();
if (bOperations == null || bOperations.size() == 0) {
@@ -164,9 +301,15 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
BOperation op = bOperations.get(i);
String defName = op.getName();
List<PExpression> paramList = new ArrayList<PExpression>();
+ ArrayList<PPredicate> whereList = new ArrayList<PPredicate>();
for (int j = 0; j < op.getOpParams().size(); j++) {
paramList.add(createIdentifierNode(op.getOpParams().get(j)));
}
+ for (int j = 0; j < op.getExistQuans().size(); j++) {
+ OpApplNode o = op.getExistQuans().get(j);
+ whereList.add(visitBounded(o));
+ }
+
AOperation operation = new AOperation();
operation.setOpName(createTIdentifierLiteral(defName));
operation.setParameters(paramList);
@@ -177,12 +320,21 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
List<PExpression> anyParams = new ArrayList<PExpression>();
for (int j = 0; j < vars.length; j++) {
String varName = vars[j].getName().toString();
+ String nextName = varName + "_n";
if (op.getUnchangedVariables().contains(varName))
continue;
- anyParams.add(createIdentifierNode(varName + "_n"));
+ anyParams.add(createIdentifierNode(nextName));
+
+ AMemberPredicate member = new AMemberPredicate();
+ member.setLeft(createIdentifierNode(nextName));
+ TLAType t = (TLAType) vars[j].getToolObject(TYPE_ID);
+ member.setRight(t.getBNode());
+ whereList.add(member);
}
any.setIdentifiers(anyParams);
- any.setWhere(visitExprOrOpArgNodePredicate(op.getNode()));
+
+ whereList.add(visitExprOrOpArgNodePredicate(op.getNode()));
+ any.setWhere(createConjunction(whereList));
List<PExpression> varList = new ArrayList<PExpression>();
List<PExpression> valueList = new ArrayList<PExpression>();
@@ -243,8 +395,14 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
private void createConstantsClause() {
- List<OpDeclNode> bConstants = Arrays.asList(moduleNode
- .getConstantDecls());
+
+ List<OpDeclNode> bConstants;
+ if (conEval != null) {
+ bConstants = conEval.getbConstantList();
+ } else {
+ bConstants = Arrays.asList(moduleNode.getConstantDecls());
+ }
+
if (bConstants.size() > 0) {
List<PExpression> list = new ArrayList<PExpression>();
for (OpDeclNode opDeclNode : bConstants) {
@@ -261,14 +419,68 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
private void createPropertyClause() {
List<PPredicate> list = new ArrayList<PPredicate>();
- AssumeNode[] assumes = moduleNode.getAssumptions();
- if (assumes.length == 0) {
- return;
+
+ for (OpDeclNode con : bConstants) {
+ if (conEval != null
+ && conEval.getConstantAssignments().containsKey(con)
+ && bConstants.contains(con)) {
+ ValueObj v = conEval.getConstantAssignments().get(con);
+ TLAType t = v.getType();
+ boolean isEnum = false;
+ if (t instanceof SetType) {
+ TLAType sub = ((SetType) t).getSubType();
+ if (sub instanceof EnumType) {
+ EnumType en = (EnumType) sub;
+ SetEnumValue set = (SetEnumValue) v.getValue();
+ if (set.elems.size() == en.modelvalues.size()) {
+ isEnum = true;
+ }
+ }
+ }
+ if (isEnum) {
+ AEqualPredicate equal = new AEqualPredicate();
+ equal.setLeft(createIdentifierNode(con.getName().toString()));
+ equal.setRight(createIdentifierNode(((SetType) t)
+ .getSubType().toString()));
+ list.add(equal);
+ } else {
+ AEqualPredicate equal = new AEqualPredicate();
+ equal.setLeft(createIdentifierNode(con.getName().toString()));
+ equal.setRight(createIdentifierNode(v.getValue().toString()));
+ list.add(equal);
+ }
+ } else {
+ AMemberPredicate member = new AMemberPredicate();
+ member.setLeft(createIdentifierNode(con.getName().toString()));
+ TLAType t = (TLAType) con.getToolObject(TYPE_ID);
+ member.setRight(t.getBNode());
+ list.add(member);
+ }
}
+
+ if (conEval != null) {
+ Iterator<Entry<OpDeclNode, OpDefNode>> iter = conEval
+ .getConstantOverrideTable().entrySet().iterator();
+ while (iter.hasNext()) {
+ Entry<OpDeclNode, OpDefNode> entry = iter.next();
+ OpDeclNode con = entry.getKey();
+ OpDefNode def = entry.getValue();
+
+ AEqualPredicate equal = new AEqualPredicate();
+ equal.setLeft(createIdentifierNode(con.getName().toString()));
+ equal.setRight(visitExprNodeExpression(def.getBody()));
+ list.add(equal);
+ }
+ }
+
+ AssumeNode[] assumes = moduleNode.getAssumptions();
for (AssumeNode assumeNode : assumes) {
list.add(visitAssumeNode(assumeNode));
}
+ if (list.size() == 0)
+ return;
+
APropertiesMachineClause propertiesClause = new APropertiesMachineClause();
propertiesClause.setPredicates(createConjunction(list));
@@ -286,10 +498,20 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
AMemberPredicate member = new AMemberPredicate();
member.setLeft(createIdentifierNode(vars[i].getName().toString()));
- member.setRight(new AIntegerSetExpression());
+ member.setRight(varType.getBNode());
predList.add(member);
}
+
+ if (conEval != null) {
+ for (OpDefNode def : conEval.getInvariants()) {
+ ADefinitionPredicate defPred = new ADefinitionPredicate();
+ defPred.setDefLiteral(new TDefLiteralPredicate(def.getName()
+ .toString() + "_def"));
+ predList.add(defPred);
+ }
+ }
+
AInvariantMachineClause invClause = new AInvariantMachineClause(
createConjunction(predList));
machineClauseList.add(invClause);
@@ -329,6 +551,27 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
return new AStringExpression(new TStringLiteral(s.getRep()
.toString()));
}
+
+ case AtNodeKind: { // @
+ AtNode at = (AtNode) n;
+ TLAType type = (TLAType) at.getExceptRef().getToolObject(TYPE_ID);
+ if(type instanceof FunctionType){
+
+ OpApplNode seq = at.getAtModifier();
+ LinkedList<ExprOrOpArgNode> list = new LinkedList<ExprOrOpArgNode>();
+ for (int j = 0; j < seq.getArgs().length; j++) {
+ list.add(seq.getArgs()[j]);
+ }
+ List<PExpression> params = new ArrayList<PExpression>();
+ params.add(visitExprOrOpArgNodeExpression(list.get(0)));
+
+ AFunctionExpression funCall = new AFunctionExpression();
+ funCall.setIdentifier(visitExprNodeExpression(at.getAtBase()));
+ funCall.setParameters(params);
+ return funCall;
+ }
+ throw new RuntimeException();
+ }
}
@@ -393,9 +636,15 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
return visitBBuitInsPredicate(n);
}
- // new Definition or what else
-
- throw new RuntimeException();
+ ADefinitionPredicate defCall = new ADefinitionPredicate();
+ defCall.setDefLiteral(new TDefLiteralPredicate(def.getName().toString()
+ + "_def"));
+ List<PExpression> list = new ArrayList<PExpression>();
+ for (int i = 0; i < n.getArgs().length; i++) {
+ list.add(visitExprOrOpArgNodeExpression(n.getArgs()[i]));
+ }
+ defCall.setParameters(list);
+ return defCall;
}
private PExpression visitUserdefinedOpExpression(OpApplNode n) {
@@ -409,8 +658,16 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
// new Definition or what else
+ ADefinitionExpression defExpr = new ADefinitionExpression();
+ defExpr.setDefLiteral(new TIdentifierLiteral(n.getOperator().getName()
+ .toString()));
+ List<PExpression> list = new ArrayList<PExpression>();
+ for (int i = 0; i < n.getArgs().length; i++) {
+ list.add(visitExprOrOpArgNodeExpression(n.getArgs()[i]));
+ }
+ defExpr.setParameters(list);
+ return defExpr;
- throw new RuntimeException();
}
private PPredicate visitBBuitInsPredicate(OpApplNode n) {
@@ -592,16 +849,17 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
visitExprOrOpArgNodeExpression(n.getArgs()[0]));
case B_OPCODE_subseq: { // SubSeq(s,m,n)
- // StringBuilder s = visitExprOrOpArgNode(n.getArgs()[0], d,
- // NOBOOL).out;
- // out.append("(");
- // out.append(s);
- // out.append("/|\\"); // taking first n elements
- // out.append(visitExprOrOpArgNode(n.getArgs()[2], d, NOBOOL).out);
- // out.append(")\\|/"); // dropping first m-1 elements
- // out.append(visitExprOrOpArgNode(n.getArgs()[1], d, NOBOOL).out);
- // out.append("-1");
- // return new ExprReturn(out, P_drop_last);
+ ARestrictFrontExpression restrictFront = new ARestrictFrontExpression();
+ restrictFront
+ .setLeft(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
+ restrictFront
+ .setRight(visitExprOrOpArgNodeExpression(n.getArgs()[2]));
+
+ ARestrictTailExpression restrictTail = new ARestrictTailExpression();
+ restrictTail.setLeft(restrictFront);
+ restrictTail
+ .setRight(visitExprOrOpArgNodeExpression(n.getArgs()[1]));
+ return restrictTail;
}
}
@@ -954,12 +1212,90 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
+ "_n");
}
+ case OPCODE_ite: { // IF THEN ELSE
+ ALambdaExpression lambda1 = new ALambdaExpression();
+ lambda1.setIdentifiers(createIdentifierList("t_"));
+ AEqualPredicate eq1 = new AEqualPredicate(
+ createIdentifierNode("t_"), new AIntegerExpression(
+ new TIntegerLiteral("0")));
+ AConjunctPredicate c1 = new AConjunctPredicate();
+ c1.setLeft(eq1);
+ c1.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
+ lambda1.setPredicate(c1);
+ lambda1.setExpression(visitExprOrOpArgNodeExpression(n.getArgs()[1]));
+
+ ALambdaExpression lambda2 = new ALambdaExpression();
+ lambda2.setIdentifiers(createIdentifierList("t_"));
+ AEqualPredicate eq2 = new AEqualPredicate(
+ createIdentifierNode("t_"), new AIntegerExpression(
+ new TIntegerLiteral("0")));
+ AConjunctPredicate c2 = new AConjunctPredicate();
+ c2.setLeft(eq2);
+ ANegationPredicate not = new ANegationPredicate(
+ visitExprOrOpArgNodePredicate(n.getArgs()[0]));
+ c2.setRight(not);
+ lambda2.setPredicate(c2);
+ lambda2.setExpression(visitExprOrOpArgNodeExpression(n.getArgs()[2]));
+
+ AUnionExpression union = new AUnionExpression(lambda1, lambda2);
+ AFunctionExpression funCall = new AFunctionExpression();
+ funCall.setIdentifier(union);
+ List<PExpression> list = new ArrayList<PExpression>();
+ list.add(new AIntegerExpression(new TIntegerLiteral("0")));
+ funCall.setParameters(list);
+ return funCall;
+ }
+
+ case OPCODE_exc: // Except
+ {
+ TLAType type = (TLAType) n.getToolObject(TYPE_ID);
+ if (type.getKind() == STRUCT) {
+ System.out.println(n.getOperator().getName());
+ throw new RuntimeException();
+
+ } else {
+ FunctionType func = (FunctionType) type;
+
+ List<PExpression> list = new ArrayList<PExpression>();
+ for (int i = 1; i < n.getArgs().length; i++) {
+ OpApplNode pair = (OpApplNode) n.getArgs()[i];
+
+ ACoupleExpression couple = new ACoupleExpression();
+ List<PExpression> coupleList = new ArrayList<PExpression>();
+ coupleList.add(visitExprOrOpArgNodeExpression(pair
+ .getArgs()[0]));
+ coupleList.add(visitExprOrOpArgNodeExpression(pair
+ .getArgs()[1]));
+ couple.setList(coupleList);
+ list.add(couple);
+ }
+ ASetExtensionExpression setExtension = new ASetExtensionExpression(
+ list);
+ AOverwriteExpression overwrite = new AOverwriteExpression();
+ overwrite
+ .setLeft(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
+ overwrite.setRight(setExtension);
+ return overwrite;
+ }
+ }
+
+ case OPCODE_seq: // !
+ {
+ return visitExprOrOpArgNodeExpression(n.getArgs()[0]);
+ }
+
}
System.out.println(n.getOperator().getName());
throw new RuntimeException();
}
+ private List<PExpression> createIdentifierList(String name) {
+ ArrayList<PExpression> list = new ArrayList<PExpression>();
+ list.add(createIdentifierNode(name));
+ return list;
+ }
+
private PPredicate visitBuiltInKindPredicate(OpApplNode n) {
switch (getOpCode(n.getOperator().getName())) {
case OPCODE_land: // \land
@@ -1121,6 +1457,11 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
+ "_n"), new ABooleanTrueExpression());
}
+ case OPCODE_unchanged: {
+ return new AEqualPredicate(new ABooleanTrueExpression(),
+ new ABooleanTrueExpression());
+ }
+
case 0:
return visitBBuitInsPredicate(n);
@@ -1189,8 +1530,10 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
conj.setLeft(list.get(0));
for (int i = 1; i < list.size(); i++) {
if (i < list.size() - 1) {
- conj.setRight(list.get(i));
- conj = new AConjunctPredicate(conj, null);
+ AConjunctPredicate old = conj;
+ old.setRight(list.get(i));
+ conj = new AConjunctPredicate();
+ conj.setLeft(old);
} else {
conj.setRight(list.get(i));
}
diff --git a/src/main/java/de/tla2b/pprint/BMachinePrinter.java b/src/main/java/de/tla2b/pprint/BMachinePrinter.java
index 555df520e439cb5ad8f0164c39e00e8651402024..952d3923019cee23e29f4287fcff3ddfb47fe8e3 100644
--- a/src/main/java/de/tla2b/pprint/BMachinePrinter.java
+++ b/src/main/java/de/tla2b/pprint/BMachinePrinter.java
@@ -85,7 +85,8 @@ public class BMachinePrinter extends AbstractExpressionPrinter implements
out.append("MACHINE " + module.getName().toString() + "\n");
out.append(evalEnumeratedSets());
-
+ out.append(evalDefinitions());
+
// Constants and Properties
out.append(evalConsDecl());
out.append(evalPropertyStatements());
@@ -94,7 +95,7 @@ public class BMachinePrinter extends AbstractExpressionPrinter implements
globalLets.addAll(tempLetInNodes);
tempLetInNodes.clear();
- out.append(evalDefinitions());
+
out.append(evalVariables());
diff --git a/src/main/java/de/tla2b/translation/ExpressionTranslator.java b/src/main/java/de/tla2b/translation/ExpressionTranslator.java
index 61096f5f8ad306a47ca2db88c106769d4da8c8fd..beffd415df3de4fdf3ef5082b72acd7ccd98dd7e 100644
--- a/src/main/java/de/tla2b/translation/ExpressionTranslator.java
+++ b/src/main/java/de/tla2b/translation/ExpressionTranslator.java
@@ -180,7 +180,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
}
if (spec.parseErrors.isFailure()) {
- String[] m = ToolIO.getAllMessages();
+ //String[] m = ToolIO.getAllMessages();
String message = module + "\n\n"
+ spec.parseErrors;
// System.out.println(spec.parseErrors);
@@ -190,7 +190,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
}
if (spec.semanticErrors.isFailure()) {
- String[] m = ToolIO.getAllMessages();
+ //String[] m = ToolIO.getAllMessages();
String message = module + "\n\n" + spec.semanticErrors;
message += Tla2BTranslator.allMessagesToString(ToolIO
.getAllMessages());
diff --git a/src/main/java/de/tla2b/translation/Tla2BTranslator.java b/src/main/java/de/tla2b/translation/Tla2BTranslator.java
index bba0f4436b6c8717a234e1030129d26c29bff548..8e67de3e736bb02be21cb972aed8c4082682238c 100644
--- a/src/main/java/de/tla2b/translation/Tla2BTranslator.java
+++ b/src/main/java/de/tla2b/translation/Tla2BTranslator.java
@@ -13,7 +13,6 @@ import de.tla2b.config.ConfigfileEvaluator;
import de.tla2b.config.ModuleOverrider;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.global.TranslationGlobals;
-import de.tla2b.pprint.BAstCreator;
import de.tla2b.pprint.BMachinePrinter;
import tla2sany.drivers.FrontEndException;
import tla2sany.drivers.SANY;
@@ -63,9 +62,9 @@ public class Tla2BTranslator implements TranslationGlobals {
throws de.tla2b.exceptions.FrontEndException, TLA2BException {
File dir = new File("temp/");
dir.mkdirs();
-
+
try {
- File f = new File("temp/"+ moduleName+ ".tla");
+ File f = new File("temp/" + moduleName + ".tla");
f.createNewFile();
FileWriter fw = new FileWriter(f);
fw.write(moduleString);
@@ -74,14 +73,13 @@ public class Tla2BTranslator implements TranslationGlobals {
} catch (IOException e) {
e.printStackTrace();
}
-
+
ToolIO.setUserDir("temp/");
moduleNode = parseModule(moduleName + ".tla");
-
-
+
modelConfig = null;
if (configString != null) {
- File f = new File("temp/" + moduleName +".cfg");
+ File f = new File("temp/" + moduleName + ".cfg");
try {
f.createNewFile();
FileWriter fw = new FileWriter(f);
@@ -90,14 +88,13 @@ public class Tla2BTranslator implements TranslationGlobals {
} catch (IOException e) {
e.printStackTrace();
}
- modelConfig = new ModelConfig(moduleName +".cfg", null);
+ modelConfig = new ModelConfig(moduleName + ".cfg", null);
modelConfig.parse();
f.deleteOnExit();
}
dir.deleteOnExit();
}
-
public StringBuilder translate() throws TLA2BException {
InstanceTransformation trans = new InstanceTransformation(moduleNode);
trans.start();
@@ -121,7 +118,7 @@ public class Tla2BTranslator implements TranslationGlobals {
}
specAnalyser.start();
-
+
typechecker = new TypeChecker(moduleNode, conEval, specAnalyser);
typechecker.start();
@@ -131,11 +128,12 @@ public class Tla2BTranslator implements TranslationGlobals {
symRenamer.start();
BMachinePrinter p = new BMachinePrinter(moduleNode, conEval,
specAnalyser);
- //BAstCreator bAstCreator = new BAstCreator(moduleNode, conEval, specAnalyser);
-
+ // BAstCreator bAstCreator = new BAstCreator(moduleNode, conEval,
+ // specAnalyser);
+
return p.start();
}
-
+
public static ModuleNode parseModule(String moduleName)
throws de.tla2b.exceptions.FrontEndException {
SpecObj spec = new SpecObj(moduleName, null);
diff --git a/src/main/java/de/tla2b/types/EnumType.java b/src/main/java/de/tla2b/types/EnumType.java
index c36ed7c712899662edd51c0982be9b7b6a448d0d..c75dc52fbeee1a7e67629892edf3ef41c78538a1 100644
--- a/src/main/java/de/tla2b/types/EnumType.java
+++ b/src/main/java/de/tla2b/types/EnumType.java
@@ -9,6 +9,7 @@ import java.util.LinkedHashSet;
import de.be4.classicalb.core.parser.node.PExpression;
import de.tla2b.exceptions.UnificationException;
+import de.tla2b.pprint.BAstCreator;
@@ -80,7 +81,6 @@ public class EnumType extends AbstractHasFollowers {
@Override
public PExpression getBNode() {
- // TODO Auto-generated method stub
- return null;
+ return BAstCreator.createIdentifierNode("ENUM" + id);
}
}
\ No newline at end of file
diff --git a/src/main/java/de/tla2b/types/PairType.java b/src/main/java/de/tla2b/types/PairType.java
index 29d382d62439aa78fc3dc5fbcfe590113b115f24..8eaf54a0693973e6d918fa4edba54f5c0a6fa155 100644
--- a/src/main/java/de/tla2b/types/PairType.java
+++ b/src/main/java/de/tla2b/types/PairType.java
@@ -1,9 +1,7 @@
package de.tla2b.types;
-import java.util.ArrayList;
-import java.util.List;
-import de.be4.classicalb.core.parser.node.ACoupleExpression;
+import de.be4.classicalb.core.parser.node.AMultOrCartExpression;
import de.be4.classicalb.core.parser.node.PExpression;
import de.tla2b.exceptions.UnificationException;
@@ -131,10 +129,10 @@ public class PairType extends AbstractHasFollowers {
@Override
public PExpression getBNode() {
- List<PExpression> list = new ArrayList<PExpression>();
- list.add(first.getBNode());
- list.add(second.getBNode());
- return new ACoupleExpression(list);
+ AMultOrCartExpression card = new AMultOrCartExpression();
+ card.setLeft(first.getBNode());
+ card.setRight(second.getBNode());
+ return card;
}
}
diff --git a/src/main/java/de/tla2b/types/TupleType.java b/src/main/java/de/tla2b/types/TupleType.java
index 4adcfefc87992f9a345967e97d13fa3bbe3a4980..001f3d1af5a458ff8bb6c3d37cf994c440e25dfa 100644
--- a/src/main/java/de/tla2b/types/TupleType.java
+++ b/src/main/java/de/tla2b/types/TupleType.java
@@ -3,7 +3,7 @@ package de.tla2b.types;
import java.util.ArrayList;
import java.util.List;
-import de.be4.classicalb.core.parser.node.ACoupleExpression;
+import de.be4.classicalb.core.parser.node.AMultOrCartExpression;
import de.be4.classicalb.core.parser.node.PExpression;
import de.tla2b.exceptions.UnificationException;
@@ -38,7 +38,6 @@ public class TupleType extends AbstractHasFollowers {
}
}
-
public void update(TLAType oldType, TLAType newType) {
for (int i = 0; i < types.size(); i++) {
TLAType t = types.get(i);
@@ -74,7 +73,7 @@ public class TupleType extends AbstractHasFollowers {
return true;
}
if (o instanceof FunctionType) {
- //TODO
+ // TODO
FunctionType func = (FunctionType) o;
if (!(func.getDomain() instanceof IntType)) {
return false;
@@ -162,9 +161,9 @@ public class TupleType extends AbstractHasFollowers {
}
}
if (o instanceof FunctionType) {
- //TODO
- if(compareToAll(new Untyped())){
- //Function
+ // TODO
+ if (compareToAll(new Untyped())) {
+ // Function
TLAType t = types.get(0);
for (int i = 1; i < types.size(); i++) {
t = t.unify(types.get(i));
@@ -172,16 +171,16 @@ public class TupleType extends AbstractHasFollowers {
FunctionType func = new FunctionType(IntType.getInstance(), t);
this.setFollowersTo(func);
return func.unify(o);
- }else{
+ } else {
TLAType res = types.get(1).unify(((FunctionType) o).getRange());
types.set(1, res);
return this;
}
-
+
}
throw new RuntimeException();
}
-
+
@Override
public String toString() {
String res = "";
@@ -204,7 +203,20 @@ public class TupleType extends AbstractHasFollowers {
for (TLAType t : types) {
list.add(t.getBNode());
}
- return new ACoupleExpression(list);
+ AMultOrCartExpression card = new AMultOrCartExpression();
+ card.setLeft(list.get(0));
+ for (int i = 1; i < list.size(); i++) {
+ if (i < list.size() - 1) {
+ AMultOrCartExpression old = card;
+ old.setRight(list.get(i));
+ card = new AMultOrCartExpression();
+ card.setLeft(old);
+ } else {
+ card.setRight(list.get(i));
+ }
+
+ }
+ return card;
}
}
diff --git a/src/main/java/de/tla2bAst/TLAParser.java b/src/main/java/de/tla2bAst/TLAParser.java
index 32b92ca2db8ee3b76900f44c480223ddd647d818..c67d9b7fafa532114260b07c6fb7725afdd8ba74 100644
--- a/src/main/java/de/tla2bAst/TLAParser.java
+++ b/src/main/java/de/tla2bAst/TLAParser.java
@@ -15,7 +15,7 @@ public class TLAParser {
this.filenameToStream = filenameToStream;
}
- public ModuleNode parseModule(String moduleName) {
+ public ModuleNode parseModule(String moduleName) throws de.tla2b.exceptions.FrontEndException {
SpecObj spec = new SpecObj(moduleName, filenameToStream);
try {
SANY.frontEndMain(spec, moduleName, ToolIO.out);
@@ -25,9 +25,15 @@ public class TLAParser {
}
if (spec.parseErrors.isFailure()) {
+ throw new de.tla2b.exceptions.FrontEndException(
+ allMessagesToString(ToolIO.getAllMessages())
+ + spec.parseErrors, spec);
}
if (spec.semanticErrors.isFailure()) {
+ throw new de.tla2b.exceptions.FrontEndException(
+ // allMessagesToString(ToolIO.getAllMessages())
+ "" + spec.semanticErrors, spec);
}
// RootModule
@@ -38,7 +44,19 @@ public class TLAParser {
}
if (n == null) { // Parse Error
+ // System.out.println("Rootmodule null");
+ throw new de.tla2b.exceptions.FrontEndException(
+ allMessagesToString(ToolIO.getAllMessages()), spec);
}
+
return n;
}
+
+ public static String allMessagesToString(String[] allMessages) {
+ StringBuilder sb = new StringBuilder();
+ for (int i = 0; i < allMessages.length - 1; i++) {
+ sb.append(allMessages[i] + "\n");
+ }
+ return sb.toString();
+ }
}
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index fbbe9a36479f4f90aebde9c1d118ac07dfe9c836..38bff13b6a669ad59ce6e5151fdafd8907c3d28c 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -4,7 +4,7 @@ import java.io.File;
import java.io.FileWriter;
import java.io.IOException;
-import de.be4.classicalb.core.parser.node.Node;
+import de.be4.classicalb.core.parser.Definitions;
import de.be4.classicalb.core.parser.node.Start;
import de.tla2b.analysis.InstanceTransformation;
import de.tla2b.analysis.SpecAnalyser;
@@ -13,10 +13,7 @@ import de.tla2b.analysis.SymbolSorter;
import de.tla2b.analysis.TypeChecker;
import de.tla2b.config.ConfigfileEvaluator;
import de.tla2b.config.ModuleOverrider;
-import de.tla2b.exceptions.ConfigFileErrorException;
import de.tla2b.exceptions.FrontEndException;
-import de.tla2b.exceptions.NotImplementedException;
-import de.tla2b.exceptions.SemanticErrorException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.pprint.BAstCreator;
import de.tla2b.pprint.BMachinePrinter;
@@ -29,13 +26,15 @@ public class Translator {
private String moduleFileName;
private String configFileName;
-
+ private Definitions bDefinitions;
private String moduleName;
private ModuleNode moduleNode;
private ModelConfig modelConfig;
- public Translator(String moduleFileName, String configFileName) {
+ private String bMachineString;
+
+ public Translator(String moduleFileName, String configFileName) throws FrontEndException {
this.moduleFileName = moduleFileName;
this.configFileName = configFileName;
@@ -44,7 +43,7 @@ public class Translator {
//Used for Testing
- public Translator(String moduleString, String configString, int i) {
+ public Translator(String moduleString, String configString, int i) throws FrontEndException {
moduleName = "Testing";
File dir = new File("temp/");
dir.mkdirs();
@@ -55,7 +54,7 @@ public class Translator {
FileWriter fw = new FileWriter(f);
fw.write(moduleString);
fw.close();
- f.deleteOnExit();
+ //f.deleteOnExit();
moduleFileName = f.getAbsolutePath();
} catch (IOException e) {
e.printStackTrace();
@@ -73,7 +72,7 @@ public class Translator {
} catch (IOException e) {
e.printStackTrace();
}
- f.deleteOnExit();
+ //f.deleteOnExit();
configFileName = f.getAbsolutePath();
}
dir.deleteOnExit();
@@ -81,7 +80,37 @@ public class Translator {
parse();
}
- private void parse(){
+ //Used for Testing
+ public Translator(String moduleString) throws FrontEndException {
+ moduleName = "Testing";
+ File dir = new File("temp/");
+ dir.mkdirs();
+
+ try {
+ File f = new File("temp/" + moduleName + ".tla");
+ f.createNewFile();
+ FileWriter fw = new FileWriter(f);
+ fw.write(moduleString);
+ fw.close();
+ //f.deleteOnExit();
+ moduleFileName = f.getAbsolutePath();
+ } catch (IOException e) {
+ e.printStackTrace();
+ }
+
+ parseModule();
+ }
+
+
+ private void parseModule() throws FrontEndException {
+ moduleName = evalFileName(moduleFileName);
+
+ TLAParser tlaParser = new TLAParser(null);
+ moduleNode = tlaParser.parseModule(moduleName);
+ }
+
+
+ private void parse() throws FrontEndException{
moduleName = evalFileName(moduleFileName);
TLAParser tlaParser = new TLAParser(null);
@@ -89,8 +118,22 @@ public class Translator {
modelConfig = null;
if (configFileName != null) {
- modelConfig = new ModelConfig(configFileName, null);
- modelConfig.parse();
+ File f = new File(configFileName);
+ if(f.exists()){
+ modelConfig = new ModelConfig(f.getName(), null);
+ modelConfig.parse();
+ }
+ }else {
+ String fileNameWithoutSuffix = moduleFileName;
+ if (fileNameWithoutSuffix.toLowerCase().endsWith(".tla")) {
+ fileNameWithoutSuffix = fileNameWithoutSuffix.substring(0, fileNameWithoutSuffix.length() - 4);
+ }
+ String configFile = fileNameWithoutSuffix + ".cfg";
+ File f = new File(configFile);
+ if(f.exists()){
+ modelConfig = new ModelConfig(f.getName(), null);
+ modelConfig.parse();
+ }
}
}
@@ -128,9 +171,12 @@ public class Translator {
symRenamer.start();
BMachinePrinter p = new BMachinePrinter(moduleNode, conEval,
specAnalyser);
- //System.out.println(p.start());
+ bMachineString = p.start().toString();
BAstCreator bAstCreator = new BAstCreator(moduleNode, conEval,
specAnalyser);
+
+ this.bDefinitions = bAstCreator.getBDefinitions();
+
return bAstCreator.getStartNode();
}
@@ -142,7 +188,8 @@ public class Translator {
if (name.toLowerCase().endsWith(".cfg")) {
name = name.substring(0, name.length() - 4);
}
-
+
+
String sourceModuleName = name.substring(name
.lastIndexOf(FileUtil.separator) + 1);
@@ -152,5 +199,13 @@ public class Translator {
ToolIO.setUserDir(path);
return sourceModuleName;
}
+
+ public Definitions getBDefinitions(){
+ return bDefinitions;
+ }
+ public String getBMachineString(){
+ return bMachineString;
+ }
+
}
diff --git a/src/test/java/de/tla2b/examples/ForDistribution.java b/src/test/java/de/tla2b/examples/ForDistribution.java
new file mode 100644
index 0000000000000000000000000000000000000000..64e927653428edfe4c70d51462cef949b2051b28
--- /dev/null
+++ b/src/test/java/de/tla2b/examples/ForDistribution.java
@@ -0,0 +1,46 @@
+package de.tla2b.examples;
+
+import org.junit.Test;
+import static de.tla2b.util.TestUtil.runModule;
+
+
+public class ForDistribution {
+
+
+ @Test
+ public void testClub() throws Exception {
+ String file = "src/test/resources/examples/Club/Club.tla";
+ runModule(file);
+ }
+
+ @Test
+ public void testSimpleMC() throws Exception {
+ String file = "src/test/resources/MCTests/simple/MC.tla";
+ runModule(file);
+ }
+
+ @Test
+ public void testConstantSetupMC() throws Exception {
+ String file = "src/test/resources/MCTests/constantsetup/MC.tla";
+ runModule(file);
+ }
+
+ @Test
+ public void testModelValuesMC() throws Exception {
+ String file = "src/test/resources/MCTests/modelvalues/MC.tla";
+ runModule(file);
+ }
+
+ @Test
+ public void testDieHardMC() throws Exception {
+ String file = "src/test/resources/MCTests/DieHard/MC.tla";
+ runModule(file);
+ }
+
+ @Test
+ public void testSimpleAllocatorMC() throws Exception {
+ String file = "src/test/resources/MCTests/SimpleAllocator/MC.tla";
+ runModule(file);
+ }
+
+}
diff --git a/src/test/java/de/tla2b/prettyprintb/BBuiltInsTest.java b/src/test/java/de/tla2b/prettyprintb/BBuiltInsTest.java
index 93f059306fe65ebe5b6a504711c299a3b9009aa6..c434d8a2e7ebe96935e192726fc320d38c8d74db 100644
--- a/src/test/java/de/tla2b/prettyprintb/BBuiltInsTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/BBuiltInsTest.java
@@ -5,13 +5,9 @@
package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
-import static org.junit.Assert.assertEquals;
import org.junit.Test;
-import de.tla2b.util.TestUtil;
-import util.ToolIO;
-
public class BBuiltInsTest {
@Test
@@ -48,14 +44,12 @@ public class BBuiltInsTest {
@Test
public void testBoolValue2() throws Exception {
- ToolIO.reset();
final String module = "-------------- MODULE Testing ----------------\n"
+ "ASSUME TRUE = FALSE \n"
+ "=================================";
- StringBuilder sb = TestUtil.translateString(module);
final String expected = "MACHINE Testing\n"
+ "PROPERTIES TRUE = FALSE \n" + "END";
- assertEquals(TestUtil.getBTreeofMachineString(expected), TestUtil.getBTreeofMachineString(sb.toString()));
+ compare(expected, module);
}
}
diff --git a/src/test/java/de/tla2b/prettyprintb/FunctionTest.java b/src/test/java/de/tla2b/prettyprintb/FunctionTest.java
index b8846c5719e0ddeddcc363d4ab3e203991fad3ec..c6d14fae72e540f46cdcaaafb69c5fb460369a68 100644
--- a/src/test/java/de/tla2b/prettyprintb/FunctionTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/FunctionTest.java
@@ -24,7 +24,7 @@ public class FunctionTest {
final String expected = "MACHINE Testing\n"
+ "ABSTRACT_CONSTANTS k\n"
- + "PROPERTIES k = %x.(x : {1}| bool(TRUE = TRUE)) \n"
+ + "PROPERTIES k : INTEGER +-> BOOL & k = %x.(x : {1}| bool(TRUE = TRUE)) \n"
+ "END";
compare(expected, module);
}
@@ -33,12 +33,12 @@ public class FunctionTest {
public void testFunctionConstructor2() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k\n"
- + "ASSUME k = [x,y \\in {1} |-> 1] \n"
+ + "ASSUME k = [x,y \\in {1,2} |-> 1] \n"
+ "=================================";
final String expected = "MACHINE Testing\n"
+ "ABSTRACT_CONSTANTS k\n"
- + "PROPERTIES k = %x,y.(x : {1} & y : {1}| 1) \n"
+ + "PROPERTIES k : INTEGER * INTEGER +-> INTEGER & k = %x,y.(x : {1,2} & y : {1,2}| 1) \n"
+ "END";
compare(expected, module);
}
@@ -52,7 +52,7 @@ public class FunctionTest {
final String expected = "MACHINE Testing\n"
+ "ABSTRACT_CONSTANTS k\n"
- + "PROPERTIES k = %x,y.(x : {1} & y : BOOL| 1) \n"
+ + "PROPERTIES k : INTEGER * BOOL +-> INTEGER & k = %x,y.(x : {1} & y : BOOL| 1) \n"
+ "END";
compare(expected, module);
}
@@ -88,12 +88,11 @@ public class FunctionTest {
public void testFunctionCall() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
- + "CONSTANTS k\n"
- + "ASSUME k = [x,y \\in {1} |-> x+y] /\\ k[1,2] = 1 \n"
+ + "ASSUME [x,y \\in {1,2} |-> x+y] [1,2] = 3 \n"
+ "=================================";
- final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
- + "PROPERTIES k = %x,y.(x : {1} & y : {1}| x + y) & k(1, 2) = 1"
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES %x,y.(x : {1,2} & y : {1,2}| x + y) (1, 2) = 3 \n"
+ "END";
compare(expected, module);
}
@@ -101,26 +100,22 @@ public class FunctionTest {
@Test
public void testFunctionCall2() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
- + "EXTENDS Naturals \n"
- + "CONSTANTS k\n"
- + "ASSUME k = [x \\in {1} |-> TRUE] /\\ k[1] \n"
+ + "ASSUME[x \\in {1} |-> TRUE][1] \n"
+ "=================================";
- final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
- + "PROPERTIES k = %x.(x : {1}| TRUE) & k(1) = TRUE\n" + "END";
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES %x.(x : {1}| TRUE)(1) = TRUE\n" + "END";
compare(expected, module);
}
@Test
public void testDomain() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
- + "EXTENDS Naturals \n"
- + "CONSTANTS k\n"
- + "ASSUME k = [x \\in {1} |-> x] /\\ DOMAIN k = {1} \n"
+ + "ASSUME DOMAIN[x \\in {1} |-> x] = {1} \n"
+ "=================================";
- final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
- + "PROPERTIES k = %x.(x : {1}| x) & dom(k) = {1}" + "END";
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES dom(%x.(x : {1}| x)) = {1}" + "END";
compare(expected, module);
}
@@ -132,47 +127,41 @@ public class FunctionTest {
+ "=================================";
final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
- + "PROPERTIES k = BOOL --> {1}"
+ + "PROPERTIES k : POW(BOOL +-> INTEGER) & k = BOOL --> {1}"
+ "END";
compare(expected, module);
}
- @Ignore
@Test
public void testFunctionExcept() throws Exception {
- ToolIO.reset();
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS k \n"
+ "ASSUME k = [k EXCEPT ![TRUE] = 0, ![FALSE] = 0] \n"
+ "=================================";
- StringBuilder sb = TestUtil.translateString(module);
final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
- + "PROPERTIES " + " k : POW(BOOL*INTEGER)"
+ + "PROPERTIES "
+ + " k : BOOL +-> INTEGER "
+ "& k = k <+ {TRUE |-> 0, FALSE |-> 0}" + "END";
- assertEquals(TestUtil.getBTreeofMachineString(expected), TestUtil.getBTreeofMachineString(sb.toString()));
+ compare(expected, module);
}
/**********************************************************************
* Record Except @
**********************************************************************/
- @Ignore
@Test
public void testFunctionExceptAt() throws Exception {
- ToolIO.reset();
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
- + "CONSTANTS k, k2 \n"
- + "ASSUME k = [x \\in {1,2} |-> x] /\\ k2 = [k EXCEPT ![1] = @ + 1] \n"
+ + "CONSTANTS k \n"
+ + "ASSUME k = [x \\in {1,2} |-> x] /\\ [k EXCEPT ![1] = @ + 1][1] = 2 \n"
+ "=================================";
- StringBuilder sb = TestUtil.translateString(module);
- System.out.println(sb);
final String expected = "MACHINE Testing\n"
- + "ABSTRACT_CONSTANTS k, k2\n"
- + "PROPERTIES k : POW(INTEGER*INTEGER) & k2 : POW(INTEGER*INTEGER) & k = %x.(x : {1, 2}| x) & k2 = k <+ {1 |-> k(1) + 1} \n"
+ + "ABSTRACT_CONSTANTS k \n"
+ + "PROPERTIES k : INTEGER +-> INTEGER & (k = %x.(x : {1, 2}| x) & (k <+ {1 |-> k(1) + 1})(1) = 2)\n"
+ "END";
- assertEquals(TestUtil.getBTreeofMachineString(expected), TestUtil.getBTreeofMachineString(sb.toString()));
+ compare(expected, module);
}
@Ignore
@Test
@@ -192,6 +181,6 @@ public class FunctionTest {
+ "& k2 : POW(INTEGER*INTEGER*INTEGER) "
+ "& k = %x,y.(x : {1, 2} & y : {1, 2}| x + y) "
+ "& k2 = k <+ {(1, 1) |-> k(1, 1) + 4} \n" + "END";
- assertEquals(TestUtil.getBTreeofMachineString(expected), TestUtil.getBTreeofMachineString(sb.toString()));
+ assertEquals(TestUtil.getAstStringofBMachineString(expected), TestUtil.getAstStringofBMachineString(sb.toString()));
}
}
diff --git a/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java b/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java
index ae3d6e136fd61c5877aeb079d55303d8d23cce4f..9d4044acf558c3d2c15dfa7f2697513c3571b481 100644
--- a/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java
@@ -6,22 +6,20 @@ package de.tla2b.prettyprintb;
import org.junit.Test;
-import de.tla2b.util.TestUtil;
import static de.tla2b.util.TestUtil.compare;
-import static org.junit.Assert.*;
public class LogicOperatorsTest {
@Test
public void testEquality() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
- + "CONSTANTS k, k2\n"
- + "ASSUME k = (k2 # 1)\n"
+ + "CONSTANTS k\n"
+ + "ASSUME k = (2 # 1)\n"
+ "=================================";
final String expected = "MACHINE Testing\n"
- + "ABSTRACT_CONSTANTS k, k2\n"
- + "PROPERTIES k = bool(k2 /= 1)\n"
+ + "ABSTRACT_CONSTANTS k\n"
+ + "PROPERTIES k : BOOL & k = bool(2 /= 1)\n"
+ "END";
compare(expected, module);
}
@@ -34,7 +32,7 @@ public class LogicOperatorsTest {
+ "=================================";
final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
- + "PROPERTIES k = TRUE \n" + "END";
+ + "PROPERTIES k : BOOL & k = TRUE \n" + "END";
compare(expected, module);
}
@@ -53,12 +51,12 @@ public class LogicOperatorsTest {
@Test
public void testAnd() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
- + "CONSTANTS k, k2\n"
- + "ASSUME k = (FALSE \\land k2) \n"
+ + "CONSTANTS k\n"
+ + "ASSUME k = (FALSE \\land TRUE) \n"
+ "=================================";
final String expected = "MACHINE Testing\n"
- + "ABSTRACT_CONSTANTS k, k2\n"
- + "PROPERTIES k = bool(FALSE = TRUE & k2 = TRUE) \n"
+ + "ABSTRACT_CONSTANTS k\n"
+ + "PROPERTIES k : BOOL & k = bool(FALSE = TRUE & TRUE = TRUE) \n"
+ "END";
compare(expected, module);
}
@@ -140,18 +138,7 @@ public class LogicOperatorsTest {
+ "END";
compare(expected, module);
}
-
- @Test
- public void testAppend() throws Exception {
- final String module = "-------------- MODULE Testing ----------------\n"
- + "EXTENDS Sequences \n"
- + "ASSUME Append(<<1>>, 2) = <<1,2>> \n"
- + "=================================";
- final String expected = "MACHINE Testing\n"
- + "PROPERTIES [1] <- 2 = [1,2] \n"
- + "END";
- compare(expected, module);
- }
+
@Test
public void testQuantifier() throws Exception {
@@ -163,7 +150,7 @@ public class LogicOperatorsTest {
final String expected = "MACHINE Testing\n"
+ "ABSTRACT_CONSTANTS S\n"
- + "PROPERTIES S = {1, 2, 3} & #u.(u : seq(S) & !s.(s : S => #n.(n : 1 .. size(u) & u(n) = s))) \n"
+ + "PROPERTIES S : POW(INTEGER) & (S = {1, 2, 3} & #u.(u : seq(S) & !s.(s : S => #n.(n : 1 .. size(u) & u(n) = s)))) \n"
+ "END";
compare(expected, module);
}
diff --git a/src/test/java/de/tla2b/prettyprintb/PrecedenceTest.java b/src/test/java/de/tla2b/prettyprintb/PrecedenceTest.java
index 479f8a55a5d70a7af9846b3cf5613947a2e0b51e..fa457c914fd29cd9b5259939209bc55612f8d226 100644
--- a/src/test/java/de/tla2b/prettyprintb/PrecedenceTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/PrecedenceTest.java
@@ -5,28 +5,11 @@
package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
-import static org.junit.Assert.assertEquals;
-import org.junit.Ignore;
import org.junit.Test;
-import de.tla2b.util.TestUtil;
-import util.ToolIO;
-
public class PrecedenceTest {
- @Test
- public void testSetConstructor() throws Exception {
- final String module = "-------------- MODULE Testing ----------------\n"
- + "EXTENDS Naturals \n"
- + "ASSUME {x \\in {1,2,3} : x \\in {1} \\/ x \\in {2}} = {1,2} \n"
- + "=================================";
-
- final String expected = "MACHINE Testing\n"
- + "PROPERTIES {x|x : {1, 2, 3} & (x : {1} or x : {2})} = {1, 2} \n" + "END";
- compare(expected, module);
- }
-
@Test
public void testPrecedence() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -37,7 +20,6 @@ public class PrecedenceTest {
+ "PROPERTIES 1 + 2 * 3 = 7 \n" + "END";
compare(expected, module);
}
-
@Test
diff --git a/src/test/java/de/tla2b/prettyprintb/SetsClauseTest.java b/src/test/java/de/tla2b/prettyprintb/SetsClauseTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..303283a3e12d6469e701d31c71e6b03ae6da903f
--- /dev/null
+++ b/src/test/java/de/tla2b/prettyprintb/SetsClauseTest.java
@@ -0,0 +1,23 @@
+package de.tla2b.prettyprintb;
+
+import static de.tla2b.util.TestUtil.compare;
+
+import org.junit.Test;
+
+public class SetsClauseTest {
+
+ @Test
+ public void testSetEnumeration() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "CONSTANTS S\n"
+ + "ASSUME S = S\n"
+ + "=================================";
+ final String config = "CONSTANTS S = {s1,s2,s3}";
+
+ final String expected = "MACHINE Testing\n"
+ + "SETS ENUM1 = {s1,s2,s3} \n"
+ + "ABSTRACT_CONSTANTS S "
+ + "PROPERTIES S = ENUM1 & S = S \n" + "END";
+ compare(expected, module, config);
+ }
+}
diff --git a/src/test/java/de/tla2b/prettyprintb/SetsTest.java b/src/test/java/de/tla2b/prettyprintb/SetsTest.java
index b3090c42b87c5aee5beee0e2f3737b34eb08e2ef..c795eeb1ecf471267c5567d9418664de4797da59 100644
--- a/src/test/java/de/tla2b/prettyprintb/SetsTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/SetsTest.java
@@ -18,7 +18,7 @@ public class SetsTest {
+ "=================================";
final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
- + "PROPERTIES k = {1,2,3} \n" + "END";
+ + "PROPERTIES k : POW(INTEGER) & k = {1,2,3} \n" + "END";
compare(expected, module);
}
@@ -30,7 +30,7 @@ public class SetsTest {
+ "=================================";
final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
- + "PROPERTIES k = {TRUE, bool(1=1)} \n" + "END";
+ + "PROPERTIES k : POW(BOOL) & k = {TRUE, bool(1=1)} \n" + "END";
compare(expected, module);
}
@@ -38,7 +38,7 @@ public class SetsTest {
* Element of: \in, \notin
**********************************************************************/
@Test
- public void testIn() throws Exception {
+ public void testMemberOf() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
+ "ASSUME TRUE \\in BOOLEAN \n"
+ "=================================";
@@ -49,7 +49,7 @@ public class SetsTest {
}
@Test
- public void testIn2() throws Exception {
+ public void testMemberOf2() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
+ "ASSUME 1 \\in {1,2,3} \n"
+ "=================================";
@@ -59,7 +59,7 @@ public class SetsTest {
}
@Test
- public void testNotIn() throws Exception {
+ public void testNotMemberOf() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
+ "ASSUME 1 \\notin {} \n"
+ "=================================";
@@ -172,4 +172,16 @@ public class SetsTest {
compare(expected, module);
}
+
+ @Test
+ public void testSetConstructor() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "ASSUME {x \\in {1,2,3} : x \\in {1} \\/ x \\in {2}} = {1,2} \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES {x|x : {1, 2, 3} & (x : {1} or x : {2})} = {1, 2} \n" + "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 2a895f7bc98ceadeca78666e7a9643ced8ff66cf..59879408384a5491b3c3843ef243307cf4c215c9 100644
--- a/src/test/java/de/tla2b/prettyprintb/SimpleModulesTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/SimpleModulesTest.java
@@ -17,4 +17,43 @@ public class SimpleModulesTest {
compare(expected, module);
}
+
+ @Test
+ public void testSingleOperator() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals\n"
+ + "add(a,b) == a + b \n"
+ + "ASSUME add(1,3) = 4 \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "DEFINITIONS add(a,b) == a + b \n"
+ + "PROPERTIES add(1,3) = 4\n"
+ + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testVariables() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals\n"
+ + "VARIABLES x \n"
+ + "Init == x = 1\n"
+ + "e1 == x'= 1 \n"
+ + "e2 == 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 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"
+ + "END";
+ compare(expected, module);
+ }
+
+
}
diff --git a/src/test/java/de/tla2b/prettyprintb/StructTest.java b/src/test/java/de/tla2b/prettyprintb/StructTest.java
index 78d0d0f6de7c95c6ba70961aa33400dd821d0aeb..55f852b53269e46095c55eb2fd0338abe97e9f04 100644
--- a/src/test/java/de/tla2b/prettyprintb/StructTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/StructTest.java
@@ -5,12 +5,10 @@
package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
-import static org.junit.Assert.assertEquals;
import org.junit.Ignore;
import org.junit.Test;
-import de.tla2b.util.TestUtil;
import util.ToolIO;
public class StructTest {
@@ -30,7 +28,7 @@ public class StructTest {
final String expected = "MACHINE Testing\n"
+ "ABSTRACT_CONSTANTS k\n"
- + "PROPERTIES k = struct(a : {1}, b : BOOL) \n"
+ + "PROPERTIES k : POW(struct(a:INTEGER, b:BOOL)) & k = struct(a : {1}, b : BOOL) \n"
+ "END";
compare(expected, module);
}
@@ -60,7 +58,7 @@ public class StructTest {
final String expected = "MACHINE Testing\n"
+ "ABSTRACT_CONSTANTS k\n"
- + "PROPERTIES k = rec(a : 1, b : TRUE) \n"
+ + "PROPERTIES k : struct(a:INTEGER, b:BOOL) & k = rec(a : 1, b : TRUE) \n"
+ "END";
compare(expected, module);
}
@@ -85,13 +83,11 @@ public class StructTest {
@Test
public void testRecordSelect() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
- + "CONSTANTS k, k2 \n"
- + "ASSUME k = [a |-> 1, b |-> TRUE] /\\ k2 = k.a \n"
+ + "ASSUME [a |-> 1, b |-> TRUE].a = 1 \n"
+ "=================================";
final String expected = "MACHINE Testing\n"
- + "ABSTRACT_CONSTANTS k, k2\n"
- + "PROPERTIES k = rec(a : 1, b : TRUE) & k2 = k'a \n"
+ + "PROPERTIES rec(a : 1, b : TRUE)'a = 1\n"
+ "END";
compare(expected, module);
}
@@ -105,7 +101,7 @@ public class StructTest {
final String expected = "MACHINE Testing\n"
+ "ABSTRACT_CONSTANTS k\n"
- + "PROPERTIES k = rec(a : 1, b : TRUE) & k'b = TRUE \n"
+ + "PROPERTIES k : struct(a:INTEGER, b:BOOL) & (k = rec(a : 1, b : TRUE) & k'b = TRUE) \n"
+ "END";
compare(expected, module);
}
diff --git a/src/test/java/de/tla2b/prettyprintb/TupleTest.java b/src/test/java/de/tla2b/prettyprintb/TupleTest.java
index 507ab4cb2f128d53757a0cada2e117dbc3904f6d..514a145838df3c85f89ca0edbd486ca23837a494 100644
--- a/src/test/java/de/tla2b/prettyprintb/TupleTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/TupleTest.java
@@ -5,36 +5,30 @@
package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
-import static org.junit.Assert.assertEquals;
-
import org.junit.Test;
-import de.tla2b.util.TestUtil;
-
public class TupleTest {
@Test
public void testTuple() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
- + "CONSTANTS k\n"
- + "ASSUME k = <<TRUE,FALSE,TRUE>>\n"
+ + "ASSUME <<TRUE,1,TRUE>> /= <<TRUE,2,TRUE>>\n"
+ "=================================";
- final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
- + "PROPERTIES k = (TRUE,FALSE,TRUE) \n" + "END";
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES (TRUE,1,TRUE) /= (TRUE,2,TRUE) \n" + "END";
compare(expected, module);
}
@Test
public void testCartesianProduct() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
- + "CONSTANTS k \n"
- + "ASSUME k = BOOLEAN \\X {1} \n"
+ + "ASSUME <<TRUE,1>> \\in BOOLEAN \\X {1} \n"
+ "=================================";
- final String expected = "MACHINE Testing\n"+ "ABSTRACT_CONSTANTS k\n"
- + "PROPERTIES k = BOOL*{1} \n" + "END";
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES (TRUE,1) : BOOL*{1} \n" + "END";
compare(expected, module);
}
@@ -46,7 +40,7 @@ public class TupleTest {
+ "=================================";
final String expected = "MACHINE Testing\n"+ "ABSTRACT_CONSTANTS k\n"
- + "PROPERTIES k = BOOL*({1}*BOOL) \n" + "END";
+ + "PROPERTIES k : POW(BOOL * (INTEGER * BOOL)) & k = BOOL*({1}*BOOL) \n" + "END";
compare(expected, module);
}
diff --git a/src/test/java/de/tla2b/prettyprintb/standardmodules/TestModuleFiniteSets.java b/src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleFiniteSetsTest.java
similarity index 89%
rename from src/test/java/de/tla2b/prettyprintb/standardmodules/TestModuleFiniteSets.java
rename to src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleFiniteSetsTest.java
index 507bfb84d6be5738ac7c201fb9d45e1b0506b27e..7daa5a4aa834d12f96d61b6bbf4540a5ef6d4e35 100644
--- a/src/test/java/de/tla2b/prettyprintb/standardmodules/TestModuleFiniteSets.java
+++ b/src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleFiniteSetsTest.java
@@ -5,14 +5,12 @@
package de.tla2b.prettyprintb.standardmodules;
import static de.tla2b.util.TestUtil.compare;
-import static org.junit.Assert.*;
import org.junit.Test;
-import de.tla2b.util.TestUtil;
-public class TestModuleFiniteSets {
+public class ModuleFiniteSetsTest {
@Test
public void testIsFiniteSet() throws Exception {
diff --git a/src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleIntegersTest.java b/src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleIntegersTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..3f09be161893bd24da126d0582ec41135634f0ed
--- /dev/null
+++ b/src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleIntegersTest.java
@@ -0,0 +1,32 @@
+package de.tla2b.prettyprintb.standardmodules;
+
+import static de.tla2b.util.TestUtil.compare;
+
+import org.junit.Test;
+
+public class ModuleIntegersTest {
+
+ @Test
+ public void testUnaryMinus() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Integers \n"
+ + "ASSUME 1 - 2 = -1 \n"
+ + "=================================";
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES 1 - 2 = -1 \n"
+ + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testInt() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Integers \n"
+ + "ASSUME -1 \\in Int \n"
+ + "=================================";
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES -1 : INTEGER \n"
+ + "END";
+ compare(expected, module);
+ }
+}
diff --git a/src/test/java/de/tla2b/prettyprintb/standardmodules/TestModuleNaturals.java b/src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleNaturalsTest.java
similarity index 93%
rename from src/test/java/de/tla2b/prettyprintb/standardmodules/TestModuleNaturals.java
rename to src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleNaturalsTest.java
index fbd087135098a74165c5a6b969fc7e89a2d6464e..5ab40a18c450ace4421892b3338d0e918d173234 100644
--- a/src/test/java/de/tla2b/prettyprintb/standardmodules/TestModuleNaturals.java
+++ b/src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleNaturalsTest.java
@@ -5,14 +5,12 @@
package de.tla2b.prettyprintb.standardmodules;
import static de.tla2b.util.TestUtil.compare;
-import static org.junit.Assert.assertEquals;
import org.junit.Test;
-import de.tla2b.util.TestUtil;
-public class TestModuleNaturals {
+public class ModuleNaturalsTest {
/**********************************************************************
* >, <, <=, >=
diff --git a/src/test/java/de/tla2b/prettyprintb/standardmodules/SequencesTest.java b/src/test/java/de/tla2b/prettyprintb/standardmodules/SequencesTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..70094e42e33fe891c82457e087c183172d597e5f
--- /dev/null
+++ b/src/test/java/de/tla2b/prettyprintb/standardmodules/SequencesTest.java
@@ -0,0 +1,95 @@
+package de.tla2b.prettyprintb.standardmodules;
+
+import static de.tla2b.util.TestUtil.compare;
+
+import org.junit.Test;
+
+public class SequencesTest {
+
+ @Test
+ public void testSeq() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Sequences \n"
+ + "ASSUME <<1,2>> \\in Seq({1,2})\n"
+ + "=================================";
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES [1,2] : seq({1,2}) \n"
+ + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testLen() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Sequences \n"
+ + "ASSUME Len(<<1,2>>) = 2\n"
+ + "=================================";
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES size([1,2]) = 2 \n"
+ + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testConcatenation() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Sequences \n"
+ + "ASSUME <<1,2>> \\o <<3>> = <<1,2,3>>\n"
+ + "=================================";
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES [1,2] ^ [3] = [1,2,3] \n"
+ + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testAppend() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Sequences \n"
+ + "ASSUME Append(<<1>>, 2) = <<1,2>> \n"
+ + "=================================";
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES [1] <- 2 = [1,2] \n"
+ + "END";
+ compare(expected, module);
+ }
+
+
+ @Test
+ public void testHead() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Sequences \n"
+ + "ASSUME Head(<<1,2>>) = 1 \n"
+ + "=================================";
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES first([1,2]) = 1 \n"
+ + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testTail() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Sequences \n"
+ + "ASSUME Tail(<<1,2,3>>) = <<2,3>> \n"
+ + "=================================";
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES tail([1,2,3]) = [2,3] \n"
+ + "END";
+ compare(expected, module);
+ }
+
+ @Test
+ public void testSubSeq() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Sequences \n"
+ + "ASSUME SubSeq(<<1,2,3,4,5>>, 2, 3) = <<2,3>> \n"
+ + "=================================";
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES ([1,2,3,4,5] /|\\ 3) \\|/ 2 = [2,3] \n"
+ + "END";
+ compare(expected, module);
+ }
+
+
+}
diff --git a/src/test/java/de/tla2b/typechecking/InstanceTest.java b/src/test/java/de/tla2b/typechecking/InstanceTest.java
index 60fd53e881e6a737e7450caada11d302259d35e8..44241dcd1326a44bf7b79bd3c5adcf3bd9b41bfb 100644
--- a/src/test/java/de/tla2b/typechecking/InstanceTest.java
+++ b/src/test/java/de/tla2b/typechecking/InstanceTest.java
@@ -10,8 +10,6 @@ import org.junit.Test;
import de.tla2b.util.TestTypeChecker;
import de.tla2b.util.TestUtil;
-import util.ToolIO;
-
public class InstanceTest {
private static String path = "src/test/resources/typechecking/modules/";
diff --git a/src/test/java/de/tla2b/typechecking/OpArgTest.java b/src/test/java/de/tla2b/typechecking/OpArgTest.java
index a1c305305020ba7698ce99a88b23921cf5fd1097..a000e9be0c60e2caa9bed3ff6e07fabf3395258a 100644
--- a/src/test/java/de/tla2b/typechecking/OpArgTest.java
+++ b/src/test/java/de/tla2b/typechecking/OpArgTest.java
@@ -12,8 +12,6 @@ import de.tla2b.exceptions.ConfigFileErrorException;
import de.tla2b.util.TestTypeChecker;
import de.tla2b.util.TestUtil;
-
-
public class OpArgTest {
@Test
diff --git a/src/test/java/de/tla2b/typechecking/TypeConflictsTest.java b/src/test/java/de/tla2b/typechecking/TypeConflictsTest.java
index e4a1b9b25c0987732c4293ce3316cf0e9cf205ed..413014fb12af5b6c178cc805c131a55ebf7f1675 100644
--- a/src/test/java/de/tla2b/typechecking/TypeConflictsTest.java
+++ b/src/test/java/de/tla2b/typechecking/TypeConflictsTest.java
@@ -9,10 +9,8 @@ import org.junit.Test;
import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.exceptions.TypeErrorException;
-import de.tla2b.util.TestTypeChecker;
import de.tla2b.util.TestUtil;
-import util.ToolIO;
public class TypeConflictsTest {
diff --git a/src/test/java/de/tla2b/util/TestTypeChecker.java b/src/test/java/de/tla2b/util/TestTypeChecker.java
index f858a8646930b01aa8f8f65de3f0809b6efd370c..c80cb23e45c15c653d2f8024950b8439f3e7be85 100644
--- a/src/test/java/de/tla2b/util/TestTypeChecker.java
+++ b/src/test/java/de/tla2b/util/TestTypeChecker.java
@@ -6,7 +6,6 @@ package de.tla2b.util;
import java.util.Hashtable;
-import de.tla2b.analysis.TypeChecker;
import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.global.TranslationGlobals;
diff --git a/src/test/java/de/tla2b/util/TestUtil.java b/src/test/java/de/tla2b/util/TestUtil.java
index a57adc55d2e70d10ab8cf5c27239c8cc9193ca8d..ff154ba5698e5fb25653db4654616fa40630398f 100644
--- a/src/test/java/de/tla2b/util/TestUtil.java
+++ b/src/test/java/de/tla2b/util/TestUtil.java
@@ -7,17 +7,16 @@ package de.tla2b.util;
import static org.junit.Assert.assertEquals;
import java.io.BufferedReader;
-import java.io.File;
import java.io.FileReader;
import java.io.IOException;
import de.be4.classicalb.core.parser.BParser;
import de.be4.classicalb.core.parser.exceptions.BException;
-import de.be4.classicalb.core.parser.node.AAbstractMachineParseUnit;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.Start;
import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
+import de.tla2b.pprint.ASTPrettyPrinter;
import de.tla2b.translation.Tla2BTranslator;
import de.tla2bAst.Translator;
import tla2sany.semantic.AbortException;
@@ -35,12 +34,84 @@ public class TestUtil {
return translator.translate();
}
+ public static void runModule(String tlaFile) throws Exception{
+ Translator t = new Translator(tlaFile, null);
+ 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));
+ //BParser.printASTasProlog(System.out, new BParser(), new File("./test.mch"), resultNode, false, true, null);
+
+
+
+ System.out.println("-------------------");
+ ASTPrettyPrinter aP = new ASTPrettyPrinter();
+ start.apply(aP);
+ System.out.println(aP.getResult());
+
+
+ final BParser parser = new BParser("testcase");
+ final Start ppStart = parser.parse(aP.getResult(), false);
+
+
+ String result = getTreeAsString(start);
+ System.out.println(result);
+ String ppResult = getTreeAsString(ppStart);
+ System.out.println(ppResult);
+
+
+ System.out.println("-------------------");
+
+ assertEquals(result, ppResult);
+ }
+
public static void compare(String bMachine, String tlaModule) throws BException, TLA2BException{
ToolIO.setMode(ToolIO.TOOL);
- String expected = getBTreeofMachineString(bMachine);
+ String expected = getAstStringofBMachineString(bMachine);
+ System.out.println(expected);
+
+ Translator trans = new Translator(tlaModule);
+ Start resultNode = trans.translate();
+ String result = getTreeAsString(resultNode);
+ System.out.println(result);
+ ASTPrettyPrinter aP = new ASTPrettyPrinter();
+ resultNode.apply(aP);
+ System.out.println("-------------------");
+ System.out.println(aP.getResult());
+ final BParser parser = new BParser("testcase");
+ Start ast = parser.parse(aP.getResult(), false);
+ //BParser.printASTasProlog(System.out, new BParser(), new File("./test.mch"), resultNode, false, true, null);
+
+
+ //System.out.println(result);
+ assertEquals(expected, result);
+ assertEquals(expected, getTreeAsString(ast));
+ }
+
+ public static void compareWithPrintResult(String tlaModule) throws Exception{
+ ToolIO.setMode(ToolIO.TOOL);
+
+ Translator trans = new Translator(tlaModule);
+ Start resultNode = trans.translate();
+
+ String printResult = getAstStringofBMachineString(trans.getBMachineString());
+
+ //BParser.printASTasProlog(System.out, new BParser(), new File("./test.mch"), resultNode, false, true, null);
+
+ String result = getTreeAsString(resultNode);
+ assertEquals(printResult, result);
+ System.out.println(result);
+ }
+
+
+ public static void compare(String bMachine, String tlaModule, String config) throws BException, TLA2BException{
+ ToolIO.setMode(ToolIO.TOOL);
+ String expected = getAstStringofBMachineString(bMachine);
System.out.println(expected);
- Translator trans = new Translator(tlaModule, null, 1);
+ Translator trans = new Translator(tlaModule, config, 1);
Start resultNode = trans.translate();
//BParser.printASTasProlog(System.out, new BParser(), new File("./test.mch"), resultNode, false, true, null);
@@ -139,7 +210,7 @@ public class TestUtil {
}
- public static String getBTreeofMachineString(final String testMachine)
+ public static String getAstStringofBMachineString(final String testMachine)
throws BException {
final BParser parser = new BParser("testcase");
final Start startNode = parser.parse(testMachine, false);
diff --git a/src/test/resources/MCTests/DieHard/DieHard.tla b/src/test/resources/MCTests/DieHard/DieHard.tla
new file mode 100644
index 0000000000000000000000000000000000000000..23591399929e95816ee40b382b444ab4117e78ea
--- /dev/null
+++ b/src/test/resources/MCTests/DieHard/DieHard.tla
@@ -0,0 +1,136 @@
+------------------------------ MODULE DieHard -------------------------------
+(***************************************************************************)
+(* In the movie Die Hard 3, the heros must obtain exactly 4 gallons of *)
+(* water using a 5 gallon jug, a 3 gallon jug, and a water faucet. Our *)
+(* goal: to get TLC to solve the problem for us. *)
+(* *)
+(* First, we write a spec that describes all allowable behaviors of our *)
+(* heros. *)
+(***************************************************************************)
+EXTENDS Naturals
+ (*************************************************************************)
+ (* This statement imports the definitions of the ordinary operators on *)
+ (* natural numbers, such as +. *)
+ (*************************************************************************)
+
+(***************************************************************************)
+(* We next declare the specification's variables. *)
+(***************************************************************************)
+VARIABLES big, \* The number of gallons of water in the 5 gallon jug.
+ small \* The number of gallons of water in the 3 gallon jug.
+
+
+(***************************************************************************)
+(* We now define TypeOK to be the type invariant, asserting that the value *)
+(* of each variable is an element of the appropriate set. A type *)
+(* invariant like this is not part of the specification, but it's *)
+(* generally a good idea to include it because it helps the reader *)
+(* understand the spec. Moreover, having TLC check that it is an *)
+(* invariant of the spec catches errors that, in a typed language, are *)
+(* caught by type checking. *)
+(* *)
+(* Note: TLA+ uses the convention that a list of formulas bulleted by /\ *)
+(* or \/ denotes the conjunction or disjunction of those formulas. *)
+(* Indentation of subitems is significant, allowing one to eliminate lots *)
+(* of parentheses. This makes a large formula much easier to read. *)
+(* However, it does mean that you have to be careful with your indentation.*)
+(***************************************************************************)
+TypeOK == /\ small \in 0..3
+ /\ big \in 0..5
+
+
+(***************************************************************************)
+(* Now we define of the initial predicate, that specifies the initial *)
+(* values of the variables. I like to name this predicate Init, but the *)
+(* name doesn't matter. *)
+(***************************************************************************)
+Init == /\ big = 0
+ /\ small = 0
+
+(***************************************************************************)
+(* Now we define the actions that our hero can perform. There are three *)
+(* things they can do: *)
+(* *)
+(* - Pour water from the faucet into a jug. *)
+(* *)
+(* - Pour water from a jug onto the ground. *)
+(* *)
+(* - Pour water from one jug into another *)
+(* *)
+(* We now consider the first two. Since the jugs are not calibrated, *)
+(* partially filling or partially emptying a jug accomplishes nothing. *)
+(* So, the first two possibilities yield the following four possible *)
+(* actions. *)
+(***************************************************************************)
+FillSmallJug == /\ small' = 3
+ /\ big' = big
+
+FillBigJug == /\ big' = 5
+ /\ small' = small
+
+EmptySmallJug == /\ small' = 0
+ /\ big' = big
+
+EmptyBigJug == /\ big' = 0
+ /\ small' = small
+
+(***************************************************************************)
+(* We now consider pouring water from one jug into another. Again, since *)
+(* the jugs are not callibrated, when pouring from jug A to jug B, it *)
+(* makes sense only to either fill B or empty A. And there's no point in *)
+(* emptying A if this will cause B to overflow, since that could be *)
+(* accomplished by the two actions of first filling B and then emptying A. *)
+(* So, pouring water from A to B leaves B with the lesser of (i) the water *)
+(* contained in both jugs and (ii) the volume of B. To express this *)
+(* mathematically, we first define Min(m,n) to equal the minimum of the *)
+(* numbers m and n. *)
+(***************************************************************************)
+Min(m,n) == IF m < n THEN m ELSE n
+
+(***************************************************************************)
+(* Now we define the last two pouring actions. From the observation *)
+(* above, these definitions should be clear. *)
+(***************************************************************************)
+SmallToBig == /\ big' = Min(big + small, 5)
+ /\ small' = small - (big' - big)
+
+BigToSmall == /\ small' = Min(big + small, 3)
+ /\ big' = big - (small' - small)
+
+(***************************************************************************)
+(* We define the next-state relation, which I like to call Next. A Next *)
+(* step is a step of one of the six actions defined above. Hence, Next is *)
+(* the disjunction of those actions. *)
+(***************************************************************************)
+Next == \/ FillSmallJug
+ \/ FillBigJug
+ \/ EmptySmallJug
+ \/ EmptyBigJug
+ \/ SmallToBig
+ \/ BigToSmall
+
+(***************************************************************************)
+(* We define the formula Spec to be the complete specification, asserting *)
+(* of a behavior that it begins in a state satisfying Init, and that every *)
+(* step either satisfies Next or else leaves the pair <<big, small>> *)
+(* unchanged. *)
+(***************************************************************************)
+Spec == Init /\ [][Next]_<<big, small>>
+-----------------------------------------------------------------------------
+
+(***************************************************************************)
+(* Remember that our heros must measure out 4 gallons of water. *)
+(* Obviously, those 4 gallons must be in the 5 gallon jug. So, they have *)
+(* solved their problem when they reach a state with big = 4. So, we *)
+(* define NotSolved to be the predicate asserting that big # 4. *)
+(***************************************************************************)
+NotSolved == big # 4
+
+(***************************************************************************)
+(* We find a solution by having TLC check if NotSolved is an invariant, *)
+(* which will cause it to print out an "error trace" consisting of a *)
+(* behavior ending in a states where NotSolved is false. Such a *)
+(* behavior is the desired solution. (Because TLC uses a breadth-first *)
+(* search, it will find the shortest solution.) *)
+(***************************************************************************)
+=============================================================================
diff --git a/src/test/resources/MCTests/DieHard/MC.cfg b/src/test/resources/MCTests/DieHard/MC.cfg
new file mode 100644
index 0000000000000000000000000000000000000000..4ef4a20af815fcf65465754a2b527c4db21bc764
--- /dev/null
+++ b/src/test/resources/MCTests/DieHard/MC.cfg
@@ -0,0 +1,4 @@
+\* SPECIFICATION definition
+SPECIFICATION
+spec_13975672038532000
+\* Generated on Tue Apr 15 15:06:43 CEST 2014
\ No newline at end of file
diff --git a/src/test/resources/MCTests/DieHard/MC.tla b/src/test/resources/MCTests/DieHard/MC.tla
new file mode 100644
index 0000000000000000000000000000000000000000..cf5200a55e045cb84b83f9c7bb7b062e938bcd47
--- /dev/null
+++ b/src/test/resources/MCTests/DieHard/MC.tla
@@ -0,0 +1,10 @@
+---- MODULE MC ----
+EXTENDS DieHard, TLC
+
+\* SPECIFICATION definition @modelBehaviorSpec:0
+spec_13975672038532000 ==
+Spec
+----
+=============================================================================
+\* Modification History
+\* Created Tue Apr 15 15:06:43 CEST 2014 by hansen
diff --git a/src/test/resources/MCTests/SimpleAllocator/MC.cfg b/src/test/resources/MCTests/SimpleAllocator/MC.cfg
new file mode 100644
index 0000000000000000000000000000000000000000..53610493c558da05e14353d6099bc2b1bdaf98a4
--- /dev/null
+++ b/src/test/resources/MCTests/SimpleAllocator/MC.cfg
@@ -0,0 +1,23 @@
+\* MV CONSTANT declarations
+CONSTANTS
+c1 = c1
+c2 = c2
+c3 = c3
+\* MV CONSTANT declarations
+CONSTANTS
+r1 = r1
+r2 = r2
+r3 = r3
+\* MV CONSTANT definitions
+CONSTANT
+Clients <- const_13975725253553000
+\* MV CONSTANT definitions
+CONSTANT
+Resources <- const_13975725253664000
+\* INIT definition
+INIT
+init_13975725253775000
+\* NEXT definition
+NEXT
+next_13975725253886000
+\* Generated on Tue Apr 15 16:35:25 CEST 2014
\ No newline at end of file
diff --git a/src/test/resources/MCTests/SimpleAllocator/MC.tla b/src/test/resources/MCTests/SimpleAllocator/MC.tla
new file mode 100644
index 0000000000000000000000000000000000000000..1fc4e92a774a1ee59067efefff1608f98461751c
--- /dev/null
+++ b/src/test/resources/MCTests/SimpleAllocator/MC.tla
@@ -0,0 +1,34 @@
+---- MODULE MC ----
+EXTENDS SimpleAllocator, TLC
+
+\* MV CONSTANT declarations@modelParameterConstants
+CONSTANTS
+c1, c2, c3
+----
+
+\* MV CONSTANT declarations@modelParameterConstants
+CONSTANTS
+r1, r2, r3
+----
+
+\* MV CONSTANT definitions Clients
+const_13975725253553000 ==
+{c1, c2, c3}
+----
+
+\* MV CONSTANT definitions Resources
+const_13975725253664000 ==
+{r1, r2, r3}
+----
+
+\* INIT definition @modelBehaviorInit:0
+init_13975725253775000 ==
+Init
+----
+\* NEXT definition @modelBehaviorNext:0
+next_13975725253886000 ==
+Next
+----
+=============================================================================
+\* Modification History
+\* Created Tue Apr 15 16:35:25 CEST 2014 by hansen
diff --git a/src/test/resources/MCTests/SimpleAllocator/SimpleAllocator.tla b/src/test/resources/MCTests/SimpleAllocator/SimpleAllocator.tla
new file mode 100644
index 0000000000000000000000000000000000000000..65db89884b2ec2bb750eb6001d7dd5adea59d9f9
--- /dev/null
+++ b/src/test/resources/MCTests/SimpleAllocator/SimpleAllocator.tla
@@ -0,0 +1,118 @@
+------------------------ MODULE SimpleAllocator -------------------------
+(***********************************************************************)
+(* Specification of an allocator managing a set of resources: *)
+(* - Clients can request sets of resources whenever all their previous *)
+(* requests have been satisfied. *)
+(* - Requests can be partly fulfilled, and resources can be returned *)
+(* even before the full request has been satisfied. However, clients *)
+(* only have an obligation to return resources after they have *)
+(* obtained all resources they requested. *)
+(***********************************************************************)
+
+EXTENDS FiniteSets, TLC
+
+CONSTANTS
+ Clients, \* set of all clients
+ Resources \* set of all resources
+
+ASSUME
+ IsFiniteSet(Resources)
+
+VARIABLES
+ unsat, \* set of all outstanding requests per process
+ alloc \* set of resources allocated to given process
+
+TypeInvariant ==
+ /\ unsat \in [Clients -> SUBSET Resources]
+ /\ alloc \in [Clients -> SUBSET Resources]
+
+-------------------------------------------------------------------------
+
+(* Resources are available iff they have not been allocated. *)
+available == Resources \ (UNION {alloc[c] : c \in Clients})
+
+(* Initially, no resources have been requested or allocated. *)
+Init ==
+ /\ unsat = [c \in Clients |-> {}]
+ /\ alloc = [c \in Clients |-> {}]
+
+(* A client c may request a set of resources provided that all of its *)
+(* previous requests have been satisfied and that it doesn't hold any *)
+(* resources. *)
+Request(c,S) ==
+ /\ unsat[c] = {} /\ alloc[c] = {}
+ /\ S # {} /\ unsat' = [unsat EXCEPT ![c] = S]
+ /\ UNCHANGED alloc
+
+(* Allocation of a set of available resources to a client that *)
+(* requested them (the entire request does not have to be filled). *)
+Allocate(c,S) ==
+ /\ S # {} /\ S \subseteq available \cap unsat[c]
+ /\ alloc' = [alloc EXCEPT ![c] = @ \cup S]
+ /\ unsat' = [unsat EXCEPT ![c] = @ \ S]
+
+(* Client c returns a set of resources that it holds. It may do so *)
+(* even before its full request has been honored. *)
+Return(c,S) ==
+ /\ S # {} /\ S \subseteq alloc[c]
+ /\ alloc' = [alloc EXCEPT ![c] = @ \ S]
+ /\ UNCHANGED unsat
+
+(* The next-state relation. *)
+Next ==
+ \E c \in Clients, S \in SUBSET Resources :
+ Request(c,S) \/ Allocate(c,S) \/ Return(c,S)
+
+vars == <<unsat,alloc>>
+
+-------------------------------------------------------------------------
+
+(* The complete high-level specification. *)
+SimpleAllocator ==
+ /\ Init /\ [][Next]_vars
+ /\ \A c \in Clients: WF_vars(Return(c, alloc[c]))
+ /\ \A c \in Clients: SF_vars(\E S \in SUBSET Resources: Allocate(c,S))
+
+-------------------------------------------------------------------------
+
+ResourceMutex ==
+ \A c1,c2 \in Clients : c1 # c2 => alloc[c1] \cap alloc[c2] = {}
+
+ClientsWillReturn ==
+ \A c \in Clients : unsat[c]={} ~> alloc[c]={}
+
+ClientsWillObtain ==
+ \A c \in Clients, r \in Resources : r \in unsat[c] ~> r \in alloc[c]
+
+InfOftenSatisfied ==
+ \A c \in Clients : []<>(unsat[c] = {})
+
+-------------------------------------------------------------------------
+
+(* Used for symmetry reduction with TLC *)
+Symmetry == Permutations(Clients) \cup Permutations(Resources)
+
+-------------------------------------------------------------------------
+
+(* The following version states a weaker fairness requirement for the *)
+(* clients: resources need be returned only if the entire request has *)
+(* been satisfied. *)
+
+SimpleAllocator2 ==
+ /\ Init /\ [][Next]_vars
+ /\ \A c \in Clients: WF_vars(unsat[c] = {} /\ Return(c, alloc[c]))
+ /\ \A c \in Clients: SF_vars(\E S \in SUBSET Resources: Allocate(c,S))
+
+
+-------------------------------------------------------------------------
+
+THEOREM SimpleAllocator => []TypeInvariant
+THEOREM SimpleAllocator => []ResourceMutex
+THEOREM SimpleAllocator => ClientsWillReturn
+THEOREM SimpleAllocator2 => ClientsWillReturn
+THEOREM SimpleAllocator => ClientsWillObtain
+THEOREM SimpleAllocator => InfOftenSatisfied
+(** The following do not hold: **)
+(** THEOREM SimpleAllocator2 => ClientsWillObtain **)
+(** THEOREM SimpleAllocator2 => InfOftenSatisfied **)
+=========================================================================
diff --git a/src/test/resources/MCTests/constantsetup/MC.cfg b/src/test/resources/MCTests/constantsetup/MC.cfg
new file mode 100644
index 0000000000000000000000000000000000000000..7726eb83cc520b4c19d379754739f654ac9d49c1
--- /dev/null
+++ b/src/test/resources/MCTests/constantsetup/MC.cfg
@@ -0,0 +1,13 @@
+\* CONSTANT definitions
+CONSTANT
+k <- const_13975555301786000
+\* CONSTANT definitions
+CONSTANT
+k2 <- const_13975555301897000
+\* INIT definition
+INIT
+init_13975555302008000
+\* NEXT definition
+NEXT
+next_13975555302119000
+\* Generated on Tue Apr 15 11:52:10 CEST 2014
\ No newline at end of file
diff --git a/src/test/resources/MCTests/constantsetup/MC.tla b/src/test/resources/MCTests/constantsetup/MC.tla
new file mode 100644
index 0000000000000000000000000000000000000000..076c3b6e1a6f1e1bdee3c30ea30e39c49ff0df1c
--- /dev/null
+++ b/src/test/resources/MCTests/constantsetup/MC.tla
@@ -0,0 +1,24 @@
+---- MODULE MC ----
+EXTENDS constantsetup, TLC
+
+\* CONSTANT definitions @modelParameterConstants:0k
+const_13975555301786000 ==
+1
+----
+
+\* CONSTANT definitions @modelParameterConstants:1k2
+const_13975555301897000 ==
+2
+----
+
+\* INIT definition @modelBehaviorInit:0
+init_13975555302008000 ==
+i
+----
+\* NEXT definition @modelBehaviorNext:0
+next_13975555302119000 ==
+n
+----
+=============================================================================
+\* Modification History
+\* Created Tue Apr 15 11:52:10 CEST 2014 by hansen
diff --git a/src/test/resources/MCTests/constantsetup/constantsetup.tla b/src/test/resources/MCTests/constantsetup/constantsetup.tla
new file mode 100644
index 0000000000000000000000000000000000000000..a9b8606051e804a99defaf42d308e88ae3f11992
--- /dev/null
+++ b/src/test/resources/MCTests/constantsetup/constantsetup.tla
@@ -0,0 +1,12 @@
+--------------------------- MODULE constantsetup ---------------------------
+CONSTANTS
+k, k2
+ASSUME k = 1
+VARIABLES x
+i == x = 1
+n == x' = 2
+
+=============================================================================
+\* Modification History
+\* Last modified Tue Apr 15 11:51:56 CEST 2014 by hansen
+\* Created Tue Apr 15 11:50:55 CEST 2014 by hansen
diff --git a/src/test/resources/MCTests/modelvalues/MC.cfg b/src/test/resources/MCTests/modelvalues/MC.cfg
new file mode 100644
index 0000000000000000000000000000000000000000..0eaca2779087cad9bd27bebe4882deefb96f36d8
--- /dev/null
+++ b/src/test/resources/MCTests/modelvalues/MC.cfg
@@ -0,0 +1,22 @@
+\* MV CONSTANT declarations
+CONSTANTS
+a2 = a2
+d = d
+e = e
+\* CONSTANT declarations
+CONSTANT b = b
+\* CONSTANT declarations
+CONSTANT c = c
+\* MV CONSTANT definitions
+CONSTANT
+Set <- const_13975656563232000
+\* CONSTANT definitions
+CONSTANT
+a <- const_13975656563343000
+\* INIT definition
+INIT
+init_13975656563454000
+\* NEXT definition
+NEXT
+next_13975656563565000
+\* Generated on Tue Apr 15 14:40:56 CEST 2014
\ No newline at end of file
diff --git a/src/test/resources/MCTests/modelvalues/MC.tla b/src/test/resources/MCTests/modelvalues/MC.tla
new file mode 100644
index 0000000000000000000000000000000000000000..710a22fea630fad99f4f2e20a04e3ec38e06dd8c
--- /dev/null
+++ b/src/test/resources/MCTests/modelvalues/MC.tla
@@ -0,0 +1,29 @@
+---- MODULE MC ----
+EXTENDS modelvalues, TLC
+
+\* MV CONSTANT declarations@modelParameterConstants
+CONSTANTS
+a2, d, e
+----
+
+\* MV CONSTANT definitions Set
+const_13975656563232000 ==
+{a2, d, e}
+----
+
+\* CONSTANT definitions @modelParameterConstants:0a
+const_13975656563343000 ==
+a2
+----
+
+\* INIT definition @modelBehaviorInit:0
+init_13975656563454000 ==
+Init
+----
+\* NEXT definition @modelBehaviorNext:0
+next_13975656563565000 ==
+Next
+----
+=============================================================================
+\* Modification History
+\* Created Tue Apr 15 14:40:56 CEST 2014 by hansen
diff --git a/src/test/resources/MCTests/modelvalues/modelvalues.tla b/src/test/resources/MCTests/modelvalues/modelvalues.tla
new file mode 100644
index 0000000000000000000000000000000000000000..3003f2e84249bedd542ecfee370e7aed9d6b6a8d
--- /dev/null
+++ b/src/test/resources/MCTests/modelvalues/modelvalues.tla
@@ -0,0 +1,9 @@
+---------------------------- MODULE modelvalues ----------------------------
+CONSTANTS a, b, c, Set
+VARIABLES x
+Init == x = 1
+Next == x' = 2
+=============================================================================
+\* Modification History
+\* Last modified Tue Apr 15 14:38:43 CEST 2014 by hansen
+\* Created Tue Apr 15 14:37:45 CEST 2014 by hansen
diff --git a/src/test/resources/MCTests/simple/MC.cfg b/src/test/resources/MCTests/simple/MC.cfg
new file mode 100644
index 0000000000000000000000000000000000000000..060fe678e26045a4c9cba1b90b1da82f90375c44
--- /dev/null
+++ b/src/test/resources/MCTests/simple/MC.cfg
@@ -0,0 +1,7 @@
+\* INIT definition
+INIT
+init_139755348766932000
+\* NEXT definition
+NEXT
+next_139755348767933000
+\* Generated on Tue Apr 15 11:18:07 CEST 2014
\ No newline at end of file
diff --git a/src/test/resources/MCTests/simple/MC.tla b/src/test/resources/MCTests/simple/MC.tla
new file mode 100644
index 0000000000000000000000000000000000000000..8f8f8d87ff537021f1ae55edaf275a7733a10861
--- /dev/null
+++ b/src/test/resources/MCTests/simple/MC.tla
@@ -0,0 +1,14 @@
+---- MODULE MC ----
+EXTENDS simple, TLC
+
+\* INIT definition @modelBehaviorInit:0
+init_139755348766932000 ==
+Init
+----
+\* NEXT definition @modelBehaviorNext:0
+next_139755348767933000 ==
+Next
+----
+=============================================================================
+\* Modification History
+\* Created Tue Apr 15 11:18:07 CEST 2014 by hansen
diff --git a/src/test/resources/MCTests/simple/simple.tla b/src/test/resources/MCTests/simple/simple.tla
new file mode 100644
index 0000000000000000000000000000000000000000..ccb234fa69eee5fe879e02bb68a08a930965d148
--- /dev/null
+++ b/src/test/resources/MCTests/simple/simple.tla
@@ -0,0 +1,10 @@
+------------------------------- MODULE simple -------------------------------
+VARIABLE x
+Init == x = 1
+Next == x' = 2
+
+
+=============================================================================
+\* Modification History
+\* Last modified Tue Apr 15 11:17:53 CEST 2014 by hansen
+\* Created Tue Apr 15 11:17:24 CEST 2014 by hansen
diff --git a/src/test/resources/simpleModules/Foo1.tla b/src/test/resources/simpleModules/Foo1.tla
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391