diff --git a/src/main/java/de/tla2b/analysis/InstanceTransformation.java b/src/main/java/de/tla2b/analysis/InstanceTransformation.java
index a3848880a94c8c07602f146c7243f7a40d16953e..3e578c4c7332c2960c85e464f6f7bb4f362a3521 100644
--- a/src/main/java/de/tla2b/analysis/InstanceTransformation.java
+++ b/src/main/java/de/tla2b/analysis/InstanceTransformation.java
@@ -4,11 +4,9 @@
package de.tla2b.analysis;
-
import java.util.Hashtable;
import de.tla2b.global.BBuiltInOPs;
-
import tla2sany.semantic.ASTConstants;
import tla2sany.semantic.AbortException;
import tla2sany.semantic.AtNode;
@@ -16,6 +14,7 @@ import tla2sany.semantic.Context;
import tla2sany.semantic.ExprNode;
import tla2sany.semantic.ExprOrOpArgNode;
import tla2sany.semantic.FormalParamNode;
+import tla2sany.semantic.InstanceNode;
import tla2sany.semantic.LetInNode;
import tla2sany.semantic.ModuleNode;
import tla2sany.semantic.NumeralNode;
@@ -35,6 +34,7 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
Hashtable<String, OpDefNode> defsHash;
private int substitutionId = 11;
+
/**
* @param con
*/
@@ -43,7 +43,8 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
defsHash = new Hashtable<String, OpDefNode>();
for (int i = 0; i < defs.length; i++) {
- defsHash.put(defs[i].getName().toString(), defs[i]);
+ OpDefNode def = defs[i];
+ defsHash.put(def.getName().toString(), def);
}
}
@@ -51,23 +52,26 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
* @throws AbortException
*
*/
- public void start() {
+ public void start() {
for (int i = 0; i < defs.length; i++) {
OpDefNode def = defs[i];
if (def.getSource() != def
&& !BBuiltInOPs.contains(def.getSource().getName())) {
// instance
String defName = def.getName().toString();
- String prefix = defName.substring(0,
- defName.lastIndexOf('!') + 1);
- def.setParams(generateNewParams(def.getParams()));
- ExprNode body;
- try {
- body = generateNewExprNode(def.getBody(), prefix);
- } catch (AbortException e) {
- throw new RuntimeException();
+
+ if (def.getBody() instanceof SubstInNode) {
+ String prefix = defName.substring(0,
+ defName.lastIndexOf('!') + 1);
+ def.setParams(generateNewParams(def.getParams()));
+ ExprNode body;
+ try {
+ body = generateNewExprNode(def.getBody(), prefix);
+ } catch (AbortException e) {
+ throw new RuntimeException();
+ }
+ def.setBody(body);
}
- def.setBody(body);
}
}
}
@@ -116,7 +120,8 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
Subst[] subs = substInNode.getSubsts();
for (int i = 0; i < subs.length; i++) {
OpDeclNode op = subs[i].getOp();
- op.setToolObject(substitutionId, subs[i].getExpr());
+ ExprOrOpArgNode expr = subs[i].getExpr();
+ op.setToolObject(substitutionId, expr);
}
return generateNewExprNode(substInNode.getBody(), prefix);
}
@@ -195,8 +200,7 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
FormalParamNode f = (FormalParamNode) n.getOperator()
.getToolObject(substitutionId);
if (f == null) {
- System.out.println(n.toString(4));
- System.out.println(n);
+ throw new RuntimeException();
}
return new OpApplNode(f, generateNewArgs(n.getArgs(), prefix),
n.getTreeNode(), null);
@@ -224,8 +228,11 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
// normal userdefined Operator
String opName = prefix + n.getOperator().getName().toString();
OpDefNode op = defsHash.get(opName);
- return new OpApplNode(op, generateNewArgs(n.getArgs(), prefix),
- n.getTreeNode(), null);
+ if (op == null) {
+ throw new RuntimeException();
+ }
+ return new OpApplNode(op, generateNewArgs(n.getArgs(),
+ prefix), n.getTreeNode(), null);
}
}
throw new RuntimeException("OpApplkind not implemented jet");
diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index fbf363c760984238d6cb47f5035eed0a95b2b560..c28f195b7e763270a6e61b1c95e73e2a8f2a05c0 100644
--- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java
+++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
@@ -260,9 +260,10 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
Set<OpDefNode> set = new HashSet<OpDefNode>(usedDefinitions);
for (OpDefNode def : set) {
if (def.getInRecursive()) {
- bDefinitionsSet.remove(def);
- RecursiveDefinition rd = new RecursiveDefinition(def);
- recursiveDefinitions.add(rd);
+ throw new NotImplementedException("Recursive definitions are currently not supported.");
+// bDefinitionsSet.remove(def);
+// RecursiveDefinition rd = new RecursiveDefinition(def);
+// recursiveDefinitions.add(rd);
} else
if (def.getBody() instanceof OpApplNode) {
OpApplNode o = (OpApplNode) def.getBody();
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index a2a965cdd9181208d8a1bf6f45fb062163c1b1d4..c090fceb3f44c947ae28b066ed462b86e07f96ca 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -99,6 +99,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
OpDeclNode con = cons[i];
if (constantAssignments != null
&& constantAssignments.containsKey(con)) {
+
TLAType t = constantAssignments.get(con).getType();
con.setToolObject(TYPE_ID, t);
if (t instanceof AbstractHasFollowers) {
@@ -224,7 +225,6 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
if (usedDefinitions.contains(def))
visitOpDefNode(def);
-
}
}
@@ -246,7 +246,10 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
p.setToolObject(paramId, u);
u.addFollower(p);
}
- TLAType defType = visitExprNode(def.getBody(), new UntypedType());
+ UntypedType u = new UntypedType();
+ // def.setToolObject(TYPE_ID, u);
+ // u.addFollower(def);
+ TLAType defType = visitExprNode(def.getBody(), u);
def.setToolObject(TYPE_ID, defType);
if (defType instanceof AbstractHasFollowers) {
((AbstractHasFollowers) defType).addFollower(def);
@@ -826,10 +829,10 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
domType = visitExprOrOpArgNode(n.getArgs()[1],
new UntypedType());
}
+
FunctionType func = new FunctionType(domType, expected);
- FunctionType res = (FunctionType) visitExprOrOpArgNode(
- n.getArgs()[0], func);
- return res.getRange();
+ TLAType res = visitExprOrOpArgNode(n.getArgs()[0], func);
+ return ((FunctionType) res).getRange();
}
/***********************************************************************
diff --git a/src/main/java/de/tla2b/config/ModuleOverrider.java b/src/main/java/de/tla2b/config/ModuleOverrider.java
index d3a95f7d406af9c053f6ae8677fb008c8500f71f..fff7afe5db53ad9da1451b4e3cfabae213c59cd4 100644
--- a/src/main/java/de/tla2b/config/ModuleOverrider.java
+++ b/src/main/java/de/tla2b/config/ModuleOverrider.java
@@ -220,9 +220,12 @@ public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
for (int i = 0; i < n.getArgs().length; i++) {
if (n.getArgs()[i] != null) {
- OpApplNode res = visitExprOrOpArgNode(n.getArgs()[i]);
- if (res != null) {
- n.getArgs()[i] = res;
+ ExprOrOpArgNode arg =n.getArgs()[i];
+ if(arg != null){
+ OpApplNode res = visitExprOrOpArgNode(n.getArgs()[i]);
+ if (res != null) {
+ n.getArgs()[i] = res;
+ }
}
}
diff --git a/src/main/java/de/tla2b/output/ASTPrettyPrinter.java b/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
index a0359d0c4d6c1cf8610ec40b77e9818c61d52706..d89e24030c51ff9f7f772c3bf4bd32f652d0ca2a 100644
--- a/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
+++ b/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
@@ -9,12 +9,12 @@ 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.AConstantsMachineClause;
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.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.ALambdaExpression;
-import de.be4.classicalb.core.parser.node.AMinusOrSetSubtractExpression;
import de.be4.classicalb.core.parser.node.AOperation;
import de.be4.classicalb.core.parser.node.AOperationsMachineClause;
import de.be4.classicalb.core.parser.node.APredicateDefinitionDefinition;
@@ -103,6 +103,8 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
putDeclarationClause("ASetsMachineClause", "SETS", ";");
putDeclarationClause("AAbstractConstantsMachineClause",
"ABSTRACT_CONSTANTS", ",");
+ putDeclarationClause("AConstantsMachineClause",
+ "CONSTANTS", ",");
putDeclarationClause("AVariablesMachineClause", "VARIABLES", ",");
put("AEnumeratedSetSet", null, null, ", ", null, " = {", "}");
diff --git a/src/main/java/de/tla2b/translation/BDefinitionsFinder.java b/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
index 867822f6e78c2fb373d3feb40017bcd179759194..4ffc6069f0c29610e6eb9dccf7401d97c8853bd1 100644
--- a/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
+++ b/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
@@ -53,8 +53,9 @@ public class BDefinitionsFinder extends AbstractASTVisitor implements
public void visitUserDefinedNode(OpApplNode n) {
OpDefNode def = (OpDefNode) n.getOperator();
- bDefinitionsSet.add(def);
- visitExprNode(def.getBody());
+ if(bDefinitionsSet.add(def)){
+ visitExprNode(def.getBody());
+ }
for (ExprOrOpArgNode exprOrOpArgNode : n.getArgs()) {
visitExprOrOpArgNode(exprOrOpArgNode);
}
diff --git a/src/main/java/de/tla2b/types/TupleType.java b/src/main/java/de/tla2b/types/TupleType.java
index 71ed583e283687094a3a5e6c49707d2c519e3779..0c22efd19f312a081a6dba3cf104b1ccfe654f1e 100644
--- a/src/main/java/de/tla2b/types/TupleType.java
+++ b/src/main/java/de/tla2b/types/TupleType.java
@@ -87,6 +87,9 @@ public class TupleType extends AbstractHasFollowers {
return false;
}
}
+ if(!compareToAll(range)){
+ return false;
+ }
return true;
}
return false;
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 469b7c051c9dddde4b2f9f449073fb40ca65947e..cc6d9f61b55730fa5984ed9efd8502e3cd8ca1fa 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -26,6 +26,7 @@ import tla2sany.semantic.SymbolNode;
import tlc2.tool.BuiltInOPs;
import tlc2.value.ModelValue;
import tlc2.value.SetEnumValue;
+import tlc2.value.StringValue;
import tlc2.value.Value;
import tlc2.value.ValueConstants;
import de.be4.classicalb.core.parser.Definitions;
@@ -123,6 +124,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
createSetsClause();
createDefintionClause();
+ createAbstractConstantsClause();
createConstantsClause();
createPropertyClause();
createVariableClause();
@@ -406,29 +408,16 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
}
- private void createConstantsClause() {
- List<OpDeclNode> bConstants;
- if (conEval != null) {
- bConstants = conEval.getbConstantList();
- } else {
- bConstants = Arrays.asList(moduleNode.getConstantDecls());
- }
-
+ private void createAbstractConstantsClause() {
List<PExpression> constantsList = new ArrayList<PExpression>();
- for (OpDeclNode opDeclNode : bConstants) {
- AIdentifierExpression id = new AIdentifierExpression(
- createTIdentifierLiteral(getName(opDeclNode)));
- constantsList.add(id);
- TLAType type = (TLAType) opDeclNode.getToolObject(TYPE_ID);
- typeTable.put(id, type);
- }
for (RecursiveDefinition recDef : specAnalyser
.getRecursiveDefinitions()) {
AIdentifierExpression id = new AIdentifierExpression(
createTIdentifierLiteral(getName(recDef.getOpDefNode())));
constantsList.add(id);
- TLAType type = (TLAType) recDef.getOpDefNode().getToolObject(TYPE_ID);
+ TLAType type = (TLAType) recDef.getOpDefNode().getToolObject(
+ TYPE_ID);
typeTable.put(id, type);
}
@@ -445,9 +434,29 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
constantsList);
machineClauseList.add(abstractConstantsClause);
}
-
-
+ }
+
+ private void createConstantsClause() {
+ List<OpDeclNode> bConstants;
+ if (conEval != null) {
+ bConstants = conEval.getbConstantList();
+ } else {
+ bConstants = Arrays.asList(moduleNode.getConstantDecls());
+ }
+ List<PExpression> constantsList = new ArrayList<PExpression>();
+ for (OpDeclNode opDeclNode : bConstants) {
+ AIdentifierExpression id = new AIdentifierExpression(
+ createTIdentifierLiteral(getName(opDeclNode)));
+ constantsList.add(id);
+ TLAType type = (TLAType) opDeclNode.getToolObject(TYPE_ID);
+ typeTable.put(id, type);
+ }
+ if (constantsList.size() > 0) {
+ AConstantsMachineClause constantsClause = new AConstantsMachineClause(
+ constantsList);
+ machineClauseList.add(constantsClause);
+ }
}
public AIdentifierExpression createIdentifierNode(SymbolNode symbolNode) {
@@ -609,17 +618,25 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
ArrayList<PExpression> list = new ArrayList<PExpression>();
for (int i = 0; i < s.elems.size(); i++) {
Value v = s.elems.elementAt(i);
- ModelValue m = (ModelValue) v;
- AIdentifierExpression id = createIdentifierNode(m.toString());
- list.add(id);
+ list.add(createTLCValue(v));
}
return new ASetExtensionExpression(list);
}
-
+ case MODELVALUE: {
+ ModelValue m = (ModelValue) tlcValue;
+ return createIdentifierNode(m.toString());
}
- System.out.println(tlcValue);
- throw new RuntimeException();
+ case STRINGVALUE: {
+ StringValue stringValue = (StringValue) tlcValue;
+ return new AStringExpression(new TStringLiteral(stringValue
+ .getVal().toString()));
+
+ }
+ default:
+ throw new NotImplementedException(
+ "TLC value in configuration file: " + tlcValue.getClass());
+ }
}
private void createInvariantClause() {
diff --git a/src/test/java/de/tla2b/prettyprintb/ExceptTest.java b/src/test/java/de/tla2b/prettyprintb/ExceptTest.java
index d7952e0f8bb2a9feb6e09676f200184298a59a60..bf758be05efba49326ba8c60b2033b7d57f08def 100644
--- a/src/test/java/de/tla2b/prettyprintb/ExceptTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/ExceptTest.java
@@ -1,13 +1,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 util.ToolIO;
-import de.tla2b.util.TestUtil;
public class ExceptTest {
@@ -18,7 +16,7 @@ public class ExceptTest {
+ "ASSUME k = [k EXCEPT ![TRUE] = 0, ![FALSE] = 0] \n"
+ "=================================";
- final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
+ final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+ "PROPERTIES " + " k : BOOL +-> INTEGER "
+ "& k = k <+ {TRUE |-> 0, FALSE |-> 0}" + "END";
compare(expected, module);
@@ -31,7 +29,7 @@ public class ExceptTest {
+ "ASSUME k = [k EXCEPT ![TRUE] = 0, ![FALSE] = 0] \n"
+ "=================================";
- final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
+ final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+ "PROPERTIES " + " k : BOOL +-> INTEGER "
+ "& k = k <+ {TRUE |-> 0, FALSE |-> 0}" + "END";
compare(expected, module);
@@ -47,7 +45,7 @@ public class ExceptTest {
+ "=================================";
final String expected = "MACHINE Testing\n"
- + "ABSTRACT_CONSTANTS k \n"
+ + "CONSTANTS k \n"
+ "PROPERTIES k : INTEGER +-> INTEGER & (k = %x.(x : {1, 2}| x) & (k <+ {1 |-> k(1) + 1})(1) = 2)\n"
+ "END";
compare(expected, module);
@@ -63,11 +61,12 @@ public class ExceptTest {
+ "ASSUME k = [x,y \\in {1,2} |-> x+y] /\\ k2 = [k EXCEPT ![1,1] = @ + 4] \n"
+ "=================================";
- final String expected = "MACHINE Testing\n"
- + "ABSTRACT_CONSTANTS k, k2\n"
+ final String expected = "MACHINE Testing\n" + "CONSTANTS k, k2\n"
+ "PROPERTIES k : POW(INTEGER*INTEGER*INTEGER) "
+ "& k2 : POW(INTEGER*INTEGER*INTEGER) "
+ "& k = %x,y.(x : {1, 2} & y : {1, 2}| x + y) "
+ "& k2 = k <+ {(1, 1) |-> k(1, 1) + 4} \n" + "END";
+ compare(expected, module);
}
+
}
diff --git a/src/test/java/de/tla2b/prettyprintb/ExtensibleRecordTest.java b/src/test/java/de/tla2b/prettyprintb/ExtensibleRecordTest.java
index 9438ef8fbe49dcc0d5f098c6a02ba665bc033ca7..8f9b37bbfb562eff92907337eae5c6036fb6cb4e 100644
--- a/src/test/java/de/tla2b/prettyprintb/ExtensibleRecordTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/ExtensibleRecordTest.java
@@ -38,7 +38,7 @@ public class ExtensibleRecordTest {
+ "=================================";
final String expected = "MACHINE Testing\n"
- + "ABSTRACT_CONSTANTS k \n"
+ + "CONSTANTS k \n"
+ "PROPERTIES k : struct(b:POW(BOOL * INTEGER), a:POW(BOOL * INTEGER)) & ((k = rec(b:{}, a:{(TRUE,1)}) & k /= rec(b:{(TRUE,1)}, a:{})) & (k'a)(TRUE) = 1) \n"
+ "END";
compare(expected, module);
@@ -76,7 +76,7 @@ public class ExtensibleRecordTest {
+ "=================================";
final String expected = "MACHINE Testing\n"
- + "ABSTRACT_CONSTANTS k \n"
+ + "CONSTANTS k \n"
+ "PROPERTIES k : struct(a:POW(BOOL * INTEGER), b:POW(BOOL * BOOL)) & (k = rec(a:{(TRUE,1)}, b:{}) & TRUE = (k'b)(TRUE)) \n"
+ "END";
compare(expected, module);
diff --git a/src/test/java/de/tla2b/prettyprintb/FunctionTest.java b/src/test/java/de/tla2b/prettyprintb/FunctionTest.java
index 093344021ca97dccb584880e1a43fade6990340c..ee2f6722d9541518f9b25b06245533bc95a964eb 100644
--- a/src/test/java/de/tla2b/prettyprintb/FunctionTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/FunctionTest.java
@@ -5,14 +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 FunctionTest {
@Test
@@ -23,7 +19,7 @@ public class FunctionTest {
+ "=================================";
final String expected = "MACHINE Testing\n"
- + "ABSTRACT_CONSTANTS k\n"
+ + "CONSTANTS k\n"
+ "PROPERTIES k : INTEGER +-> BOOL & k = %x.(x : {1}| bool(TRUE = TRUE)) \n"
+ "END";
compare(expected, module);
@@ -37,7 +33,7 @@ public class FunctionTest {
+ "=================================";
final String expected = "MACHINE Testing\n"
- + "ABSTRACT_CONSTANTS k\n"
+ + "CONSTANTS k\n"
+ "PROPERTIES k : INTEGER * INTEGER +-> INTEGER & k = %x,y.(x : {1,2} & y : {1,2}| 1) \n"
+ "END";
compare(expected, module);
@@ -51,7 +47,7 @@ public class FunctionTest {
+ "=================================";
final String expected = "MACHINE Testing\n"
- + "ABSTRACT_CONSTANTS k\n"
+ + "CONSTANTS k\n"
+ "PROPERTIES k : INTEGER * BOOL +-> INTEGER & k = %x,y.(x : {1} & y : BOOL| 1) \n"
+ "END";
compare(expected, module);
@@ -72,7 +68,7 @@ public class FunctionTest {
+ "=================================";
final String expected = "MACHINE Testing\n"
- + "ABSTRACT_CONSTANTS k,k2,k3\n"
+ + "CONSTANTS k,k2,k3\n"
+ "PROPERTIES k : POW(INTEGER*INTEGER) & k2 : INTEGER & k3 : INTEGER \n"
+ " & k = fact & fact(k2) = k3 \n"
+ "DEFINITIONS IF_THEN_ELSE(P, a, b) == (%t_.(t_=TRUE & P = TRUE | a )\\/%t_.(t_=TRUE & not(P= TRUE) | b ))(TRUE); \n"
@@ -126,7 +122,7 @@ public class FunctionTest {
+ "ASSUME k = [BOOLEAN -> {1}] \n"
+ "=================================";
- final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
+ final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+ "PROPERTIES k : POW(BOOL +-> INTEGER) & k = BOOL --> {1}"
+ "END";
compare(expected, module);
diff --git a/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java b/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java
index 164a417a422931f8d2ac2a9c4bfdcaddfca5908f..faf7234b1d243a0cc266e23e84f2e5840cd3d777 100644
--- a/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java
@@ -17,7 +17,7 @@ public class LogicOperatorsTest {
+ "ASSUME k = (2 # 1)\n"
+ "=================================";
- final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
+ final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+ "PROPERTIES k : BOOL & k = bool(2 /= 1)\n" + "END";
compare(expected, module);
}
@@ -29,7 +29,7 @@ public class LogicOperatorsTest {
+ "ASSUME k = TRUE\n"
+ "=================================";
- final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
+ final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+ "PROPERTIES k : BOOL & k = TRUE \n" + "END";
compare(expected, module);
}
@@ -53,7 +53,7 @@ public class LogicOperatorsTest {
+ "ASSUME k = (FALSE \\land TRUE) \n"
+ "=================================";
final String expected = "MACHINE Testing\n"
- + "ABSTRACT_CONSTANTS k\n"
+ + "CONSTANTS k\n"
+ "PROPERTIES k : BOOL & k = bool(FALSE = TRUE & TRUE = TRUE) \n"
+ "END";
compare(expected, module);
@@ -146,7 +146,7 @@ public class LogicOperatorsTest {
+ "=================================";
final String expected = "MACHINE Testing\n"
- + "ABSTRACT_CONSTANTS S\n"
+ + "CONSTANTS 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/MacroTest.java b/src/test/java/de/tla2b/prettyprintb/MacroTest.java
index 8a216417b5456d45528621221f14600f9fcff9a8..3eabe27bdbdb49308fef7442fb0ecc05e63975dd 100644
--- a/src/test/java/de/tla2b/prettyprintb/MacroTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/MacroTest.java
@@ -96,7 +96,7 @@ public class MacroTest {
final String expected = "MACHINE Testing\n"
+ "DEFINITIONS \n"
+ "def(y) == !(x_1).(x_1 : {1} => y = 3); \n"
- + "ABSTRACT_CONSTANTS x\n"
+ + "CONSTANTS x\n"
+ "PROPERTIES x : INTEGER & (x = 3 & def(x)) \n" + "END";
compare(expected, module);
}
diff --git a/src/test/java/de/tla2b/prettyprintb/RecordTest.java b/src/test/java/de/tla2b/prettyprintb/RecordTest.java
index 5fba3bc60d7fb5e766598d11d11f3722182654a7..175057c6967aab781a00af3d1aa157717a910c79 100644
--- a/src/test/java/de/tla2b/prettyprintb/RecordTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/RecordTest.java
@@ -27,7 +27,7 @@ public class RecordTest {
+ "=================================";
final String expected = "MACHINE Testing\n"
- + "ABSTRACT_CONSTANTS k\n"
+ + "CONSTANTS k\n"
+ "PROPERTIES k : POW(struct(a:INTEGER, b:BOOL)) & k = struct(a : {1}, b : BOOL) \n"
+ "END";
compare(expected, module);
@@ -45,7 +45,7 @@ public class RecordTest {
+ "=================================";
final String expected = "MACHINE Testing\n"
- + "ABSTRACT_CONSTANTS k\n"
+ + "CONSTANTS k\n"
+ "PROPERTIES k : struct(a:INTEGER, b:BOOL) & k = rec(a : 1, b : TRUE) \n"
+ "END";
compare(expected, module);
@@ -88,7 +88,7 @@ public class RecordTest {
+ "=================================";
final String expected = "MACHINE Testing\n"
- + "ABSTRACT_CONSTANTS k\n"
+ + "CONSTANTS k\n"
+ "PROPERTIES k : struct(a:INTEGER, b:BOOL) & (k = rec(a : 1, b : TRUE) & k'b = TRUE) \n"
+ "END";
compare(expected, module);
@@ -104,7 +104,7 @@ public class RecordTest {
+ "ASSUME k = [a |-> 1, b |-> TRUE] /\\ k2 = [k EXCEPT !.a = 2] \n"
+ "=================================";
final String expected = "MACHINE Testing\n"
- + "ABSTRACT_CONSTANTS k, k2\n"
+ + "CONSTANTS k, k2\n"
+ "PROPERTIES k : struct(a:INTEGER, b:BOOL) & k2 : struct(a:INTEGER, b:BOOL) & (k = rec(a : 1, b : TRUE) & k2 = rec(a : 2, b : k'b)) \n"
+ "END";
compare(expected, module);
@@ -122,7 +122,7 @@ public class RecordTest {
+ "=================================";
final String expected = "MACHINE Testing\n"
- + "ABSTRACT_CONSTANTS k, k2\n"
+ + "CONSTANTS k, k2\n"
+ "PROPERTIES k : struct(a:INTEGER, b:BOOL) & k2 : struct(a:INTEGER, b:BOOL) & (k = rec(a : 1, b : TRUE) & k2 = rec(a : k'a + 1, b : k'b)) \n"
+ "END";
compare(expected, module);
diff --git a/src/test/java/de/tla2b/prettyprintb/SetsClauseTest.java b/src/test/java/de/tla2b/prettyprintb/SetsClauseTest.java
index 303283a3e12d6469e701d31c71e6b03ae6da903f..737c0593d5061a27e43bc9324435cd8f79b693cd 100644
--- a/src/test/java/de/tla2b/prettyprintb/SetsClauseTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/SetsClauseTest.java
@@ -16,7 +16,7 @@ public class SetsClauseTest {
final String expected = "MACHINE Testing\n"
+ "SETS ENUM1 = {s1,s2,s3} \n"
- + "ABSTRACT_CONSTANTS S "
+ + "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 e1c16a71a57c0e5c6d1d2a1a6a18fcc67215c966..74f8ffa0bcfd05dcf4569a01ee6bbf73fe468355 100644
--- a/src/test/java/de/tla2b/prettyprintb/SetsTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/SetsTest.java
@@ -17,7 +17,7 @@ public class SetsTest {
+ "ASSUME k = {1,2,3}\n"
+ "=================================";
- final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
+ final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+ "PROPERTIES k : POW(INTEGER) & k = {1,2,3} \n" + "END";
compare(expected, module);
}
@@ -29,7 +29,7 @@ public class SetsTest {
+ "ASSUME k = {TRUE, 1 = 1}\n"
+ "=================================";
- final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
+ final String expected = "MACHINE Testing\n" + "CONSTANTS k\n"
+ "PROPERTIES k : POW(BOOL) & k = {TRUE, bool(1=1)} \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 514a145838df3c85f89ca0edbd486ca23837a494..d5e7472295f60b9ca7ff5c715315d523fea64542 100644
--- a/src/test/java/de/tla2b/prettyprintb/TupleTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/TupleTest.java
@@ -39,7 +39,7 @@ public class TupleTest {
+ "ASSUME k = BOOLEAN \\X ({1} \\X BOOLEAN) \n"
+ "=================================";
- final String expected = "MACHINE Testing\n"+ "ABSTRACT_CONSTANTS k\n"
+ final String expected = "MACHINE Testing\n"+ "CONSTANTS k\n"
+ "PROPERTIES k : POW(BOOL * (INTEGER * BOOL)) & k = BOOL*({1}*BOOL) \n" + "END";
compare(expected, module);
}
diff --git a/src/test/java/de/tla2b/typechecking/TupleTest.java b/src/test/java/de/tla2b/typechecking/TupleTest.java
index 6671f089ace2e6be874f68568d0ba27d6bfdc2ea..2d4fe86ea1ae41e1de92c74b59e6d62925ca18d6 100644
--- a/src/test/java/de/tla2b/typechecking/TupleTest.java
+++ b/src/test/java/de/tla2b/typechecking/TupleTest.java
@@ -2,6 +2,7 @@ package de.tla2b.typechecking;
import static org.junit.Assert.assertEquals;
+import org.junit.Ignore;
import org.junit.Test;
import de.tla2b.exceptions.FrontEndException;
@@ -24,6 +25,20 @@ public class TupleTest {
TestTypeChecker t = TestUtil.typeCheckString(module);
assertEquals("INTEGER*BOOL", t.getConstantType("k").toString());
}
+
+
+ @Ignore
+ @Test
+ public void testTupleFunctionCall() throws FrontEndException, TLA2BException {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "CONSTANTS k \n"
+ + "ASSUME k = <<1,TRUE,1>>[2] \n"
+ + "=================================";
+
+ TestTypeChecker t = TestUtil.typeCheckString(module);
+ assertEquals("ka", t.getConstantType("k").toString());
+ }
@Test
public void testTuple3Components() throws FrontEndException, TLA2BException {
diff --git a/src/test/resources/regression/Club/Club.prob b/src/test/resources/regression/Club/Club.prob
deleted file mode 100644
index 037f9f3eb6bed1ed6af56bef64e201879f9ad7db..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/Club/Club.prob
+++ /dev/null
@@ -1,3 +0,0 @@
-parser_version('2014-03-12 22:57:52.564').
-classical_b('Club',['/Users/hansen/git/tla2bAST/src/test/resources/regression/Club/Club.tla']).
-machine(abstract_machine(1,machine(2),machine_header(3,'Club',[]),[sets(4,[enumerated_set(5,'ENUM1',[identifier(6,n1),identifier(7,n2),identifier(8,n3)])]),abstract_constants(9,[identifier(info(10,tla_type(integer)),capacity),identifier(info(11,tla_type(set(modelvalue))),'NAME'),identifier(info(12,tla_type(integer)),total)]),properties(13,conjunct(14,conjunct(15,conjunct(16,conjunct(17,conjunct(18,member(19,identifier(20,capacity),integer_set(21)),equal(22,identifier(23,'NAME'),identifier(24,'ENUM1'))),member(25,identifier(26,total),integer_set(27))),conjunct(28,member(29,identifier(30,capacity),natural_set(31)),equal(32,identifier(33,capacity),integer(34,2)))),greater(35,card(36,identifier(37,'NAME')),identifier(38,capacity))),conjunct(39,member(40,identifier(41,total),natural_set(42)),greater(43,identifier(44,total),integer(45,2))))),variables(46,[identifier(info(47,tla_type(set(modelvalue))),member),identifier(info(48,tla_type(set(modelvalue))),waiting)]),invariant(49,conjunct(50,member(51,identifier(52,member),pow_subset(53,identifier(54,'ENUM1'))),member(55,identifier(56,waiting),pow_subset(57,identifier(58,'ENUM1'))))),initialisation(59,becomes_such(60,[identifier(61,member),identifier(62,waiting)],conjunct(63,equal(64,identifier(65,member),empty_set(66)),equal(67,identifier(68,waiting),empty_set(69))))),operations(70,[operation(71,identifier(71,join_queue),[],[identifier(72,nn)],any(73,[identifier(74,member_n)],conjunct(75,conjunct(76,conjunct(77,conjunct(78,conjunct(79,member(80,identifier(81,nn),identifier(82,'NAME')),not_member(83,identifier(84,nn),identifier(85,member))),not_member(86,identifier(87,nn),identifier(88,waiting))),member(89,identifier(90,member_n),pow_subset(91,identifier(92,'ENUM1')))),less(93,card(94,identifier(95,waiting)),identifier(96,total))),equal(97,identifier(98,member_n),identifier(99,member))),assign(100,[identifier(101,waiting),identifier(102,member)],[union(103,identifier(104,waiting),set_extension(105,[identifier(106,nn)])),identifier(107,member_n)]))),operation(108,identifier(108,join),[],[identifier(109,nn)],select(110,conjunct(111,conjunct(112,conjunct(113,member(114,identifier(115,nn),identifier(116,'NAME')),member(117,identifier(118,nn),identifier(119,waiting))),less(120,card(121,identifier(122,member)),identifier(123,capacity))),less(124,card(125,identifier(126,member)),identifier(127,capacity))),assign(128,[identifier(129,member),identifier(130,waiting)],[union(131,identifier(132,member),set_extension(133,[identifier(134,nn)])),minus_or_set_subtract(135,identifier(136,waiting),set_extension(137,[identifier(138,nn)]))]),[])),operation(139,identifier(139,remove),[],[identifier(140,nn)],any(141,[identifier(142,waiting_n)],conjunct(143,conjunct(144,conjunct(145,member(146,identifier(147,nn),identifier(148,'NAME')),member(149,identifier(150,nn),identifier(151,member))),member(152,identifier(153,waiting_n),pow_subset(154,identifier(155,'ENUM1')))),equal(156,identifier(157,waiting_n),identifier(158,waiting))),assign(159,[identifier(160,member),identifier(161,waiting)],[minus_or_set_subtract(162,identifier(163,member),set_extension(164,[identifier(165,nn)])),identifier(166,waiting_n)])))])])).