diff --git a/src/main/java/de/tla2b/analysis/BOperation.java b/src/main/java/de/tla2b/analysis/BOperation.java
index fec96cc0902c6451193201a8a256d8f2ce40f617..f27b3a2ce47e34d7f268886a3a851bdbbf4bd607 100644
--- a/src/main/java/de/tla2b/analysis/BOperation.java
+++ b/src/main/java/de/tla2b/analysis/BOperation.java
@@ -185,8 +185,9 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
if (node instanceof OpApplNode) {
OpApplNode opApplNode = (OpApplNode) node;
if (opApplNode.getOperator().getKind() == BuiltInKind) {
- switch (getOpCode(opApplNode.getOperator().getName())) {
- case OPCODE_eq: {
+
+ if (OPCODE_eq == getOpCode(opApplNode.getOperator()
+ .getName())) {
ExprOrOpArgNode arg1 = opApplNode.getArgs()[0];
try {
OpApplNode arg11 = (OpApplNode) arg1;
@@ -204,12 +205,9 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
}
} catch (ClassCastException e) {
-
}
-
- }
- default:
}
+
}
}
}
@@ -263,7 +261,7 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
beforeAfterPredicates.add(node);
return;
}
- //beforeAfterPredicates.add(node);
+ // beforeAfterPredicates.add(node);
}
private void evalParams() {
diff --git a/src/main/java/de/tla2b/analysis/InstanceTransformation.java b/src/main/java/de/tla2b/analysis/InstanceTransformation.java
index 3e578c4c7332c2960c85e464f6f7bb4f362a3521..c8987c0997f9f243cf1919dbdda6e6e433c58571 100644
--- a/src/main/java/de/tla2b/analysis/InstanceTransformation.java
+++ b/src/main/java/de/tla2b/analysis/InstanceTransformation.java
@@ -14,7 +14,6 @@ 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;
diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index eebb4d18ee1145a3014b7a2c6e7f49862d909b6a..7e1a3ab923cfb961b38cc5d5969c86adf895ac33 100644
--- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java
+++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
@@ -20,7 +20,6 @@ import de.tla2b.global.TranslationGlobals;
import de.tla2b.translation.BDefinitionsFinder;
import de.tla2b.translation.OperationsFinder;
import de.tla2b.translation.UsedDefinitionsFinder;
-import de.tla2b.types.IType;
import tla2sany.semantic.ASTConstants;
import tla2sany.semantic.ExprNode;
import tla2sany.semantic.ExprOrOpArgNode;
@@ -43,8 +42,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
private OpDefNode expressionOpdefNode;
private Hashtable<String, SymbolNode> namingHashTable = new Hashtable<String, SymbolNode>();
-
-
+
private final ModuleNode moduleNode;
private ExprNode nextExpr;
@@ -87,18 +85,16 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
return specAnalyser;
}
-
-
-
- public static SpecAnalyser createSpecAnalyserForTlaExpression(ModuleNode m){
+
+ public static SpecAnalyser createSpecAnalyserForTlaExpression(ModuleNode m) {
SpecAnalyser specAnalyser = new SpecAnalyser(m);
-
- specAnalyser.expressionOpdefNode = m.getOpDefs()[m.getOpDefs().length-1];
+
+ specAnalyser.expressionOpdefNode = m.getOpDefs()[m.getOpDefs().length - 1];
specAnalyser.usedDefinitions.add(specAnalyser.expressionOpdefNode);
specAnalyser.bDefinitionsSet.add(specAnalyser.expressionOpdefNode);
return specAnalyser;
}
-
+
public static SpecAnalyser createSpecAnalyser(ModuleNode m) {
SpecAnalyser specAnalyser = new SpecAnalyser(m);
Hashtable<String, OpDefNode> definitions = new Hashtable<String, OpDefNode>();
@@ -109,7 +105,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
specAnalyser.spec = definitions.get("Spec");
specAnalyser.init = definitions.get("Init");
specAnalyser.next = definitions.get("Next");
- if(definitions.containsKey("Inv")){
+ if (definitions.containsKey("Inv")) {
specAnalyser.invariants.add(definitions.get("Inv"));
}
// TODO are constant in the right order
@@ -132,27 +128,27 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
for (OpDefNode inv : new ArrayList<OpDefNode>(invariants)) {
try {
OpApplNode opApplNode = (OpApplNode) inv.getBody();
-
+
OpDefNode opDefNode = (OpDefNode) opApplNode.getOperator();
-
- if (opDefNode.getKind() == UserDefinedOpKind && !BBuiltInOPs.contains(opDefNode.getName())){
+
+ if (opDefNode.getKind() == UserDefinedOpKind
+ && !BBuiltInOPs.contains(opDefNode.getName())) {
int i = invariants.indexOf(inv);
invariants.set(i, opDefNode);
- }
+ }
} catch (ClassCastException e) {
}
}
-
-
+
OperationsFinder operationsFinder = new OperationsFinder(this);
bOperations = operationsFinder.getBOperations();
-
+
UsedDefinitionsFinder definitionFinder = new UsedDefinitionsFinder(this);
this.usedDefinitions = definitionFinder.getUsedDefinitions();
-
+
BDefinitionsFinder bDefinitionFinder = new BDefinitionsFinder(this);
this.bDefinitionsSet = bDefinitionFinder.getBDefinitionsSet();
- //usedDefinitions.addAll(bDefinitionsSet);
+ // usedDefinitions.addAll(bDefinitionsSet);
// test whether there is a init predicate if there is a variable
if (moduleNode.getVariableDecls().length > 0 && inits == null) {
@@ -170,9 +166,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
}
}
findRecursiveConstructs();
-
-
-
+
for (OpDeclNode var : moduleNode.getVariableDecls()) {
namingHashTable.put(var.getName().toString(), var);
}
@@ -182,7 +176,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
for (OpDefNode def : usedDefinitions) {
namingHashTable.put(def.getName().toString(), def);
}
-
+
}
private void evalInit() {
@@ -263,12 +257,12 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
Set<OpDefNode> set = new HashSet<OpDefNode>(usedDefinitions);
for (OpDefNode def : set) {
if (def.getInRecursive()) {
- 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) {
+ 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();
switch (getOpCode(o.getOperator().getName())) {
case OPCODE_rfs: { // recursive Function
@@ -297,7 +291,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
}
public Hashtable<OpDefNode, FormalParamNode[]> getLetParams() {
- return letParams;
+ return new Hashtable<OpDefNode, FormalParamNode[]>(letParams);
}
public ArrayList<String> getDefinitionMacros() {
@@ -320,24 +314,24 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
return this.moduleNode;
}
- public ConfigfileEvaluator getConfigFileEvaluator(){
+ public ConfigfileEvaluator getConfigFileEvaluator() {
return configFileEvaluator;
}
-
- public ArrayList<OpDefNode> getInvariants(){
+
+ public ArrayList<OpDefNode> getInvariants() {
return invariants;
}
-
- public OpDefNode getInitDef(){
+
+ public OpDefNode getInitDef() {
return init;
}
-
- public OpDefNode getExpressionOpdefNode(){
+
+ public OpDefNode getExpressionOpdefNode() {
return expressionOpdefNode;
}
-
- public SymbolNode getSymbolNodeByName(String name){
+
+ public SymbolNode getSymbolNodeByName(String name) {
return namingHashTable.get(name);
}
-
+
}
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index 48653e2efd103a878378efe94911d35cc53dfe5f..0132e66c6cd2a9cfe732f3a4c4333cf84d46d078 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -45,7 +45,7 @@ import tlc2.tool.BuiltInOPs;
public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
TranslationGlobals {
- private final int TEMP_TYPE_ID = 6;
+ private static final int TEMP_TYPE_ID = 6;
private int paramId;
private ArrayList<ExprNode> inits;
@@ -461,14 +461,15 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
TLAType found = ((TLAType) def.getToolObject(TYPE_ID));
- if (found == null){
+ if (found == null) {
found = new UntypedType();
- // throw new RuntimeException(def.getName() + " has no type yet!");
+ // throw new RuntimeException(def.getName() +
+ // " has no type yet!");
}
- if(n.getArgs().length != 0){
+ if (n.getArgs().length != 0) {
found = found.cloneTLAType();
}
-
+
try {
found = found.unify(expected);
} catch (UnificationException e) {
diff --git a/src/main/java/de/tla2b/output/ASTPrettyPrinter.java b/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
index 1f899732e529be0521edc516dc31f776a2c77db8..829da96e102eaf625c78c1a05aa05ad2beabe070 100644
--- a/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
+++ b/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
@@ -13,14 +13,12 @@ import de.be4.classicalb.core.parser.node.AConjunctPredicate;
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.AFirstProjectionExpression;
import de.be4.classicalb.core.parser.node.AGeneralSumExpression;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
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.ASecondProjectionExpression;
import de.be4.classicalb.core.parser.node.ASelectSubstitution;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PExpression;
diff --git a/src/main/java/de/tla2b/translation/BDefinitionsFinder.java b/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
index 4ffc6069f0c29610e6eb9dccf7401d97c8853bd1..93351e844bb9f05f85d128988b567f2113b2108a 100644
--- a/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
+++ b/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
@@ -12,7 +12,6 @@ import de.tla2b.analysis.AbstractASTVisitor;
import de.tla2b.analysis.BOperation;
import de.tla2b.analysis.SpecAnalyser;
import de.tla2b.global.TranslationGlobals;
-import de.tla2b.types.IType;
public class BDefinitionsFinder extends AbstractASTVisitor implements
ASTConstants, ToolGlobals, TranslationGlobals {
diff --git a/src/main/java/de/tla2b/types/TLAType.java b/src/main/java/de/tla2b/types/TLAType.java
index 6ea3bde10be490c154830f1266a088e596182292..e403352e91ca069ffa70bdbdb98694288d77ec57 100644
--- a/src/main/java/de/tla2b/types/TLAType.java
+++ b/src/main/java/de/tla2b/types/TLAType.java
@@ -2,8 +2,6 @@ package de.tla2b.types;
import de.be4.classicalb.core.parser.node.PExpression;
import de.tla2b.exceptions.UnificationException;
-import de.tla2b.output.TypeVisitorInterface;
-
public abstract class TLAType implements IType {
private int kind;
diff --git a/src/main/java/de/tla2b/types/TupleOrFunction.java b/src/main/java/de/tla2b/types/TupleOrFunction.java
index 07be646bf51a3796a44305c7582cf2ab6de2eaf2..f120eb7fb867b2ed2e4f47c5bfcb8cca72bd4f05 100644
--- a/src/main/java/de/tla2b/types/TupleOrFunction.java
+++ b/src/main/java/de/tla2b/types/TupleOrFunction.java
@@ -204,7 +204,7 @@ public class TupleOrFunction extends AbstractHasFollowers {
public TLAType cloneTLAType() {
TupleOrFunction res = new TupleOrFunction();
for (Entry<Integer, TLAType> entry : this.types.entrySet()) {
- res.types.put(new Integer(entry.getKey().intValue()), entry
+ res.types.put(Integer.valueOf(entry.getKey().intValue()), entry
.getValue().cloneTLAType());
}
return res;
@@ -390,14 +390,4 @@ public class TupleOrFunction extends AbstractHasFollowers {
}
return true;
}
-
- private static boolean allTyped(List<TLAType> typeList) {
- for (int i = 0; i < typeList.size(); i++) {
- if (typeList.get(i).isUntyped()) {
- return false;
- }
- }
- return true;
- }
-
}
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index f906e9975fc3e71cf1860d303c3d6815790f4f99..969fa2903cd71014879d8a1e14bb1911807930e6 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -94,7 +94,6 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
ExprNode expr = moduleNode.getOpDefs()[moduleNode.getOpDefs().length - 1]
.getBody();
- System.out.println(expressionIsAPredicate(expr));
if (expressionIsAPredicate(expr)) {
APredicateParseUnit predicateParseUnit = new APredicateParseUnit();
predicateParseUnit.setPredicate(visitExprNodePredicate(expr));
@@ -832,7 +831,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
switch (n.getOperator().getKind()) {
case VariableDeclKind:
case ConstantDeclKind:
- case FormalParamKind: { // TODO
+ case FormalParamKind: {
return new AEqualPredicate(createIdentifierNode(n.getOperator()),
new ABooleanTrueExpression());
}
@@ -1503,7 +1502,6 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
case OPCODE_fc: // Represents [x \in S |-> e].
case OPCODE_rfs: {
FormalParamNode[][] params = n.getBdedQuantSymbolLists();
- // ExprNode[] bounds = n.getBdedQuantBounds(); TODO
List<PExpression> idList = new ArrayList<PExpression>();
for (int i = 0; i < params.length; i++) {
for (int j = 0; j < params[i].length; j++) {
@@ -1511,9 +1509,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
idList.add(createIdentifierNode(p));
}
}
-
boolean[] isTuple = n.isBdedQuantATuple();
-
ALambdaExpression lambda = new ALambdaExpression();
List<PExpression> idList2 = new ArrayList<PExpression>();
for (int i = 0; i < params.length; i++) {
@@ -2137,12 +2133,6 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
return list;
}
- private List<PExpression> createIdentifierList(SymbolNode symbolNode) {
- ArrayList<PExpression> list = new ArrayList<PExpression>();
- list.add(createIdentifierNode(getName(symbolNode)));
- return list;
- }
-
private PPredicate visitBuiltInKindPredicate(OpApplNode n) {
switch (getOpCode(n.getOperator().getName())) {
case OPCODE_land: // \land
diff --git a/src/main/java/de/tla2bAst/ExpressionTranslator.java b/src/main/java/de/tla2bAst/ExpressionTranslator.java
index c4da22f1a9cd49d128de74efce430749868897e3..ea33cfb29a8e96cacadd7e9a5386b157d2cf74fc 100644
--- a/src/main/java/de/tla2bAst/ExpressionTranslator.java
+++ b/src/main/java/de/tla2bAst/ExpressionTranslator.java
@@ -137,7 +137,6 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
+ "\n" + expr + "\n";
throw new ExpressionTranslationException(message);
}
-
SymbolRenamer symRenamer = new SymbolRenamer(moduleNode, specAnalyser);
symRenamer.start();
BAstCreator bASTCreator = new BAstCreator(moduleNode, specAnalyser);
diff --git a/src/test/java/de/tla2b/expression/ModuleAndExpressionTest.java b/src/test/java/de/tla2b/expression/ModuleAndExpressionTest.java
index 449e378b48dfc042fb5c90640f458a7dd9a0c1f2..69e312ac56525c46344ddbc9404cc272f6bc245c 100644
--- a/src/test/java/de/tla2b/expression/ModuleAndExpressionTest.java
+++ b/src/test/java/de/tla2b/expression/ModuleAndExpressionTest.java
@@ -7,11 +7,12 @@ import org.junit.Test;
import de.tla2b.exceptions.TypeErrorException;
public class ModuleAndExpressionTest {
+
@Test
public void testCon() throws Exception {
String module = "---- MODULE Testing ----\n" + "CONSTANTS k \n"
+ "ASSUME k = 4" + "===============";
- compareExprIncludingModel("bool(k = 1)", "k = 1", module);
+ compareExprIncludingModel("k = 1", "k = 1", module);
}
@Test(expected = TypeErrorException.class)
diff --git a/src/test/java/de/tla2b/util/TestTypeChecker.java b/src/test/java/de/tla2b/util/TestTypeChecker.java
index 7ecc05c67060605f632daf3d15ae3468b5f4ce7e..2dd2c112007892d403b2dd46aa6cf4a06a2f76e6 100644
--- a/src/test/java/de/tla2b/util/TestTypeChecker.java
+++ b/src/test/java/de/tla2b/util/TestTypeChecker.java
@@ -10,7 +10,6 @@ import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.global.TranslationGlobals;
import de.tla2b.types.TLAType;
-import de.tla2b.types.TupleOrFunction;
import de.tla2bAst.Translator;
import tla2sany.semantic.FormalParamNode;
import tla2sany.semantic.ModuleNode;
diff --git a/src/test/java/de/tla2b/util/TestUtil.java b/src/test/java/de/tla2b/util/TestUtil.java
index 4850e7882e893ff9cf355f7cc29f6815b0d5e802..a11a4dd11a0f2870c3fe8254f1e9caf024e1817a 100644
--- a/src/test/java/de/tla2b/util/TestUtil.java
+++ b/src/test/java/de/tla2b/util/TestUtil.java
@@ -64,7 +64,7 @@ public class TestUtil {
Renamer renamer = new Renamer(resultNode);
ASTPrettyPrinter aP = new ASTPrettyPrinter(resultNode, renamer);
resultNode.apply(aP);
- System.out.println(aP.getResultString());
+ //System.out.println(aP.getResultString());
String bAstString = getAstStringofBExpressionString(bExpr);
String result = getAstStringofBExpressionString(aP.getResultString());
// String tlaAstString = getTreeAsString(resultNode);
@@ -72,11 +72,16 @@ public class TestUtil {
}
public static void compareExprIncludingModel(String bExpr, String tlaExpr,
- String moduleString) throws TLA2BException {
+ String moduleString) throws TLA2BException, BException {
Translator trans = new Translator(moduleString, null);
trans.translate();
- Start result = trans.translateExpression(tlaExpr);
- // TODO
+ Start resultNode = trans.translateExpression(tlaExpr);
+ Renamer renamer = new Renamer(resultNode);
+ ASTPrettyPrinter aP = new ASTPrettyPrinter(resultNode, renamer);
+ resultNode.apply(aP);
+ String bAstString = getAstStringofBExpressionString(bExpr);
+ String result = getAstStringofBExpressionString(aP.getResultString());
+ assertEquals(bAstString, result);
}
public static void compare(String bMachine, String tlaModule)