diff --git a/build.gradle b/build.gradle
index d08cf6604c8f8735235920cdb5c190fad7a9c7aa..771bce0c25ba0426750e4ff784145fc3f250b6ea 100644
--- a/build.gradle
+++ b/build.gradle
@@ -72,4 +72,16 @@ jacocoTestReport {
jar { from sourceSets.main.allJava }
jar {
from configurations.releaseJars.collect { it.isDirectory() ? it : zipTree(it) }
+}
+
+manifest.mainAttributes("Main-Class" : 'de.tla2b.TLA2B')
+manifest.mainAttributes("Class-Path": './tla/ tlatools.jar')
+
+task tla2b(dependsOn: build) << {
+ copy {
+ from('build/libs/')
+ into('build/tla2b')
+ include('tla2bAST-'+project.version+'.jar')
+ rename('tla2bAST-(.+)', 'TLA2B.jar')
+ }
}
\ No newline at end of file
diff --git a/src/main/java/de/tla2b/TLA2B.java b/src/main/java/de/tla2b/TLA2B.java
new file mode 100644
index 0000000000000000000000000000000000000000..4436f6243d1559c369cb7b8cb2702db1788fc50a
--- /dev/null
+++ b/src/main/java/de/tla2b/TLA2B.java
@@ -0,0 +1,67 @@
+/**
+ * @author Dominik Hansen <Dominik.Hansen at hhu.de>
+ **/
+
+package de.tla2b;
+
+import de.tla2b.exceptions.FrontEndException;
+import de.tla2b.exceptions.NotImplementedException;
+import de.tla2b.exceptions.TLA2BException;
+import de.tla2b.global.TranslationGlobals;
+import de.tla2bAst.Translator;
+
+public class TLA2B implements TranslationGlobals {
+ private String mainFile;
+
+ private static boolean error = false;
+
+ public static boolean hasError() {
+ return error;
+ }
+
+ public void handleParameter(String[] args) {
+ int i;
+ for (i = 0; (i < args.length) && (args[i].charAt(0) == '-'); i++) {
+ if (args[i].equals("-version")) {
+ System.out.println("TLA2B version " + VERSION);
+ System.exit(-1);
+ } else {
+ System.err.println("Illegal switch: " + args[i]);
+ System.exit(-1);
+ }
+ }
+
+ if (i == args.length) {
+ System.err.println("Error: expected a module file.");
+ System.exit(-1);
+ }
+ mainFile = args[i];
+ }
+
+ public static void main(String[] args) {
+ // To indicate an error we use the exit code -1
+ TLA2B tla2b = new TLA2B();
+ tla2b.handleParameter(args);
+
+ Translator translator = null;
+ try {
+ translator = new Translator(tla2b.mainFile);
+ } catch (FrontEndException e) {
+ System.exit(-1);
+ }
+ try {
+ translator.translate();
+ } catch (NotImplementedException e) {
+ System.err.print("**** Translation Error ****\n");
+ System.err.print("Not implemented:\n");
+ System.err.println(e.getMessage());
+ System.exit(-1);
+ } catch (TLA2BException e) {
+ System.err.print("**** Translation Error ****\n");
+ System.err.println(e.getMessage());
+ System.exit(-1);
+ }
+ translator.createMachineFile();
+ }
+
+}
diff --git a/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java b/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java
new file mode 100644
index 0000000000000000000000000000000000000000..6339c0b67522c65e8c20c36ea83b6f99d3a45f41
--- /dev/null
+++ b/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java
@@ -0,0 +1,166 @@
+package de.tla2b.analysis;
+
+import tla2sany.semantic.ASTConstants;
+import tla2sany.semantic.AssumeNode;
+import tla2sany.semantic.AtNode;
+import tla2sany.semantic.ExprNode;
+import tla2sany.semantic.ExprOrOpArgNode;
+import tla2sany.semantic.LetInNode;
+import tla2sany.semantic.ModuleNode;
+import tla2sany.semantic.NumeralNode;
+import tla2sany.semantic.OpApplNode;
+import tla2sany.semantic.OpDefNode;
+import tla2sany.semantic.StringNode;
+import tla2sany.semantic.SubstInNode;
+import tlc2.tool.BuiltInOPs;
+
+public class AbstractASTVisitor extends BuiltInOPs implements ASTConstants {
+
+ public void visitModuleNode(ModuleNode moduleNode) {
+
+ visitDefinitions(moduleNode.getOpDefs());
+
+ visitAssumptions(moduleNode.getAssumptions());
+ }
+
+ public void visitDefinitions(OpDefNode[] opDefs) {
+ for (OpDefNode opDefNode : opDefs) {
+ visitDefinition(opDefNode);
+ }
+ }
+
+ public void visitAssumptions(AssumeNode[] assumptions) {
+ for (AssumeNode assumeNode : assumptions) {
+ visitAssumeNode(assumeNode);
+ }
+ }
+
+ public void visitAssumeNode(AssumeNode assumeNode) {
+ visitExprNode(assumeNode.getAssume());
+ }
+
+ public void visitDefinition(OpDefNode opDefNode) {
+ visitExprNode(opDefNode.getBody());
+ }
+
+ public void visitExprOrOpArgNode(ExprOrOpArgNode n) {
+ if (n instanceof ExprNode) {
+ visitExprNode((ExprNode) n);
+ } else {
+ throw new RuntimeException("Should not appear.");
+ }
+
+ }
+
+ public void visitExprNode(ExprNode n) {
+
+ switch (n.getKind()) {
+ case OpApplKind: {
+ visitOpApplNode((OpApplNode) n);
+ return;
+ }
+
+ case NumeralKind: {
+ visitNumeralNode((NumeralNode) n);
+ return;
+ }
+
+ case StringKind: {
+ visitStringNode((StringNode) n);
+ return;
+ }
+
+ case SubstInKind: {
+ visitStubstInNode((SubstInNode) n);
+ return;
+ }
+ case AtNodeKind: { // @
+ visitAtNode((AtNode) n);
+ return;
+ }
+
+ case LetInKind: {
+ visitLetInNode((LetInNode) n);
+ return;
+ }
+
+ }
+ }
+
+ public void visitOpApplNode(OpApplNode n) {
+ switch (n.getOperator().getKind()) {
+ case VariableDeclKind: {
+ visitVariableNode(n);
+ return;
+ }
+ case ConstantDeclKind: {
+ visitConstantNode(n);
+ return;
+ }
+
+ case FormalParamKind: {
+ visitFormalParamNode(n);
+ return;
+ }
+
+ case BuiltInKind: {
+ visitBuiltInNode(n);
+ }
+
+ case UserDefinedOpKind: {
+ visitUserDefinedNode(n);
+ }
+ }
+
+ }
+
+ public void visitBuiltInNode(OpApplNode n) {
+ ExprOrOpArgNode[] arguments = n.getArgs();
+ for (ExprOrOpArgNode exprOrOpArgNode : arguments) {
+ visitExprOrOpArgNode(exprOrOpArgNode);
+ }
+ }
+
+ public void visitLetInNode(LetInNode n) {
+ OpDefNode[] lets = n.getLets();
+ for (OpDefNode opDefNode : lets) {
+ visitLocalDefinition(opDefNode);
+ }
+ visitExprNode(n.getBody());
+ }
+
+ public void visitLocalDefinition(OpDefNode opDefNode) {
+ visitExprNode(opDefNode.getBody());
+ }
+
+ public void visitAtNode(AtNode n) {
+ }
+
+ public void visitStubstInNode(SubstInNode n) {
+ visitExprNode(n.getBody());
+ return;
+ }
+
+ public void visitUserDefinedNode(OpApplNode n) {
+ ExprOrOpArgNode[] arguments = n.getArgs();
+ for (ExprOrOpArgNode exprOrOpArgNode : arguments) {
+ visitExprOrOpArgNode(exprOrOpArgNode);
+ }
+ }
+
+ public void visitFormalParamNode(OpApplNode n) {
+ }
+
+ public void visitConstantNode(OpApplNode n) {
+ }
+
+ public void visitVariableNode(OpApplNode n) {
+ }
+
+ public void visitStringNode(StringNode n) {
+ }
+
+ public void visitNumeralNode(NumeralNode n) {
+ }
+
+}
diff --git a/src/main/java/de/tla2b/analysis/BOperation.java b/src/main/java/de/tla2b/analysis/BOperation.java
index b3b96183735c4942ae17408960a4b286211e38bb..ee9a4d89c6114338debcb4c70dd27fc1a778dc82 100644
--- a/src/main/java/de/tla2b/analysis/BOperation.java
+++ b/src/main/java/de/tla2b/analysis/BOperation.java
@@ -9,7 +9,6 @@ import java.util.ArrayList;
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.TranslationGlobals;
-
import tla2sany.semantic.ASTConstants;
import tla2sany.semantic.ExprNode;
import tla2sany.semantic.FormalParamNode;
@@ -18,6 +17,7 @@ import tla2sany.semantic.OpApplNode;
import tla2sany.semantic.OpDefNode;
import tla2sany.semantic.SemanticNode;
import tla2sany.semantic.SubstInNode;
+import tla2sany.semantic.SymbolNode;
import tlc2.tool.BuiltInOPs;
import tlc2.tool.ToolGlobals;
@@ -26,6 +26,7 @@ public class BOperation implements ASTConstants, ToolGlobals, TranslationGlobals
private ExprNode node;
private ArrayList<OpApplNode> existQuans;
private ArrayList<String> opParams;
+ private ArrayList<FormalParamNode> formalParams;
private ArrayList<String> unchangedVariables;
public BOperation(String name, ExprNode n,
@@ -39,17 +40,30 @@ public class BOperation implements ASTConstants, ToolGlobals, TranslationGlobals
private void evalParams() {
opParams = new ArrayList<String>();
+ formalParams = new ArrayList<FormalParamNode>();
for (int i = 0; i < existQuans.size(); i++) {
OpApplNode n = existQuans.get(i);
FormalParamNode[][] params = n.getBdedQuantSymbolLists();
for (int k = 0; k < params.length; k++) {
for (int j = 0; j < params[k].length; j++) {
+ formalParams.add(params[k][j]);
opParams.add(params[k][j].getName().toString());
}
}
}
}
+ public SymbolNode getSymbolNode(){
+ if(node instanceof OpApplNode){
+ OpApplNode n = ((OpApplNode) node);
+ System.out.println(n.getOperator().getKind());
+ if(n.getOperator().getKind() == UserDefinedOpKind){
+ return ((OpApplNode) node).getOperator();
+ }
+ }
+ return null;
+ }
+
public String getName() {
return name;
}
@@ -65,6 +79,10 @@ public class BOperation implements ASTConstants, ToolGlobals, TranslationGlobals
public ArrayList<String> getOpParams() {
return opParams;
}
+
+ public ArrayList<FormalParamNode> getFormalParams(){
+ return formalParams;
+ }
public ArrayList<String> getUnchangedVariables(){
return unchangedVariables;
diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index 7ca3fb7d4e7ce61f310cda29b0d99d256b7cdf59..45c28d535dd540bcc791114628bcdff714dc703a 100644
--- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java
+++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
@@ -232,8 +232,8 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
if (nextExpr == null)
return;
bOperations = new ArrayList<BOperation>();
- ArrayList<OpApplNode> existQuans = new ArrayList<OpApplNode>();
- findOperationsInSemanticNode(nextExpr, nextName, existQuans);
+ findOperationsInSemanticNode(nextExpr, nextName,
+ new ArrayList<OpApplNode>());
}
/**
@@ -635,9 +635,13 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
public ArrayList<RecursiveFunktion> getRecursiveFunctions() {
return recursiveFunctions;
}
-
- public ArrayList<RecursiveDefinition> getRecursiveDefinitions(){
+
+ public ArrayList<RecursiveDefinition> getRecursiveDefinitions() {
return recursiveDefinitions;
}
-
+
+ public ModuleNode getModuleNode() {
+ return this.moduleNode;
+ }
+
}
diff --git a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java b/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
index 518788a9bd75a83d55dd5fe50b5d86bfe8d60e83..749d0b164ce77ca6ec4cb59ea128ead768528438 100644
--- a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
+++ b/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
@@ -10,18 +10,13 @@ import java.util.HashSet;
import java.util.Hashtable;
import java.util.Iterator;
import java.util.LinkedHashMap;
-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;
import de.tla2b.types.BoolType;
import de.tla2b.types.EnumType;
import de.tla2b.types.IntType;
-import de.tla2b.types.ModelValueType;
import de.tla2b.types.SetType;
import de.tla2b.types.StringType;
import de.tla2b.types.TLAType;
diff --git a/src/main/java/de/tla2b/pprint/ASTPrettyPrinter.java b/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
similarity index 94%
rename from src/main/java/de/tla2b/pprint/ASTPrettyPrinter.java
rename to src/main/java/de/tla2b/output/ASTPrettyPrinter.java
index 27f86b256370a5341313673e44d72444e0b235f3..3768be4f6808898ff93eb87e3a24e422c03c0bc5 100644
--- a/src/main/java/de/tla2b/pprint/ASTPrettyPrinter.java
+++ b/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
@@ -1,4 +1,4 @@
-package de.tla2b.pprint;
+package de.tla2b.output;
import java.util.ArrayList;
import java.util.Hashtable;
@@ -11,8 +11,8 @@ 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.AEmptySequenceExpression;
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.AOperation;
import de.be4.classicalb.core.parser.node.AOperationsMachineClause;
@@ -28,6 +28,7 @@ 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 Renamer renamer;
private static final int no = 0;
private static final int left = 1;
@@ -36,6 +37,13 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
private final static Hashtable<String, NodeInfo> infoTable = new Hashtable<String, NodeInfo>();
+ public ASTPrettyPrinter(Renamer renamer) {
+ this.renamer = renamer;
+ }
+
+ public ASTPrettyPrinter() {
+ }
+
private static void putInfixOperator(String nodeName, String symbol,
int precedence, int a) {
infoTable.put(nodeName, new NodeInfo(null, null, null, null, " "
@@ -198,6 +206,23 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
}
+ @Override
+ public void caseAIdentifierExpression(final AIdentifierExpression node) {
+ if (renamer != null) {
+ sb.append(renamer.getNewName(node));
+ } else
+
+ {
+ final List<TIdentifierLiteral> copy = new ArrayList<TIdentifierLiteral>(
+ node.getIdentifier());
+ for (final Iterator<TIdentifierLiteral> iterator = copy.iterator(); iterator
+ .hasNext();) {
+ final TIdentifierLiteral e = iterator.next();
+ e.apply(this);
+ }
+ }
+ }
+
@Override
public String toString() {
return builder.toString();
@@ -240,11 +265,22 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
return false;
}
+ @Override
+ public void caseTIdentifierLiteral(TIdentifierLiteral node) {
+ if (renamer != null) {
+ sb.append(renamer.getNewName(node));
+ } else {
+ sb.append(node.getText());
+ }
+
+ }
+
@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());
@@ -318,10 +354,14 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
return string.trim();
}
- public String getResult() {
+ public String getResultString() {
return sb.toString();
}
+ public StringBuilder getResultAsStringbuilder() {
+ return sb;
+ }
+
@Override
public void caseAAbstractMachineParseUnit(AAbstractMachineParseUnit node) {
sb.append("MACHINE ");
diff --git a/src/main/java/de/tla2b/output/Renamer.java b/src/main/java/de/tla2b/output/Renamer.java
new file mode 100644
index 0000000000000000000000000000000000000000..7c6e707dc9af2483ff851c2a81c17187982d0ee9
--- /dev/null
+++ b/src/main/java/de/tla2b/output/Renamer.java
@@ -0,0 +1,113 @@
+package de.tla2b.output;
+
+import java.util.HashSet;
+import java.util.Hashtable;
+import java.util.Set;
+
+import de.be4.classicalb.core.parser.Utils;
+import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
+import de.be4.classicalb.core.parser.node.AIdentifierExpression;
+import de.be4.classicalb.core.parser.node.Node;
+import de.be4.classicalb.core.parser.node.Start;
+import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
+
+public class Renamer extends DepthFirstAdapter {
+
+ private final java.util.Hashtable<Node, String> namesTables;
+ private final Set<String> globalNames;
+
+ public Renamer(Start start) {
+ this.namesTables = new Hashtable<Node, String>();
+ this.globalNames = new HashSet<String>();
+
+ start.apply(this);
+ }
+
+ private final static Set<String> KEYWORDS = new HashSet<String>();
+ static {
+ KEYWORDS.add("seq");
+ KEYWORDS.add("left");
+ KEYWORDS.add("right");
+ KEYWORDS.add("max");
+ KEYWORDS.add("min");
+ KEYWORDS.add("succ");
+ KEYWORDS.add("pred");
+ KEYWORDS.add("dom");
+ KEYWORDS.add("ran");
+ KEYWORDS.add("fnc");
+ KEYWORDS.add("rel");
+ KEYWORDS.add("id");
+ KEYWORDS.add("card");
+ KEYWORDS.add("POW");
+ KEYWORDS.add("POW1");
+ KEYWORDS.add("FIN");
+ KEYWORDS.add("FIN1");
+ KEYWORDS.add("size");
+ KEYWORDS.add("rev");
+ KEYWORDS.add("first");
+ KEYWORDS.add("last");
+ KEYWORDS.add("front");
+ KEYWORDS.add("tail");
+ KEYWORDS.add("conc");
+ KEYWORDS.add("struct");
+ KEYWORDS.add("rec");
+ KEYWORDS.add("tree");
+ KEYWORDS.add("btree");
+ KEYWORDS.add("skip");
+ KEYWORDS.add("ANY");
+ KEYWORDS.add("WHERE");
+ KEYWORDS.add("END");
+ KEYWORDS.add("BE");
+ KEYWORDS.add("VAR");
+ KEYWORDS.add("ASSERT");
+ KEYWORDS.add("CHOICE");
+ KEYWORDS.add("OR");
+ KEYWORDS.add("SELECT");
+ KEYWORDS.add("EITHER");
+ KEYWORDS.add("WHEN");
+ KEYWORDS.add("BEGIN");
+ KEYWORDS.add("MACHINE");
+ KEYWORDS.add("REFINEMENT");
+ KEYWORDS.add("IMPLEMENTATION");
+ KEYWORDS.add("SETS");
+ KEYWORDS.add("CONSTRAINTS");
+ KEYWORDS.add("MODEL");
+ KEYWORDS.add("SYSTEM");
+ KEYWORDS.add("MACHINE");
+ KEYWORDS.add("EVENTS");
+ KEYWORDS.add("OPERATIONS");
+ }
+
+ @Override
+ public void caseAIdentifierExpression(AIdentifierExpression node) {
+ String name = Utils.getIdentifierAsString(node.getIdentifier());
+ String newName = incName(name, new HashSet<String>());
+ namesTables.put(node, newName);
+ }
+
+ @Override
+ public void caseTIdentifierLiteral(TIdentifierLiteral node){
+ String name = node.getText();
+ String newName = incName(name, new HashSet<String>());
+ namesTables.put(node, newName);
+ }
+
+ private Boolean existingName(String name) {
+ if (globalNames.contains(name) || KEYWORDS.contains(name)) {
+ return true;
+ } else
+ return false;
+ }
+
+ private String incName(String name, Set<String> tempSet) {
+ String res = name;
+ for (int i = 1; existingName(res) || tempSet.contains(res); i++) {
+ res = name + "_" + i;
+ }
+ return res;
+ }
+
+ public String getNewName(Node node) {
+ return namesTables.get(node);
+ }
+}
diff --git a/src/main/java/de/tla2b/translation/BMacroHandler.java b/src/main/java/de/tla2b/translation/BMacroHandler.java
new file mode 100644
index 0000000000000000000000000000000000000000..773309860205ac91fe3339e62d42b55c301eed7e
--- /dev/null
+++ b/src/main/java/de/tla2b/translation/BMacroHandler.java
@@ -0,0 +1,37 @@
+package de.tla2b.translation;
+
+import java.util.ArrayList;
+
+import tla2sany.semantic.ModuleNode;
+import tla2sany.semantic.OpDefNode;
+import de.tla2b.analysis.AbstractASTVisitor;
+import de.tla2b.analysis.SpecAnalyser;
+import de.tla2b.config.ConfigfileEvaluator;
+
+public class BMacroHandler extends AbstractASTVisitor {
+
+ public BMacroHandler(SpecAnalyser specAnalyser, ConfigfileEvaluator conEval) {
+ ModuleNode moduleNode = specAnalyser.getModuleNode();
+ 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);
+ }
+ }
+ for (OpDefNode opDefNode : bDefs) {
+ visitDefinition(opDefNode);
+ }
+ }
+
+ @Override
+ public void visitDefinition(OpDefNode def){
+
+ }
+
+}
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 32d9f5f5f9b95dadd5249c94f0e625ba6195a627..1167a2875243d1841865b89912c1938e30730377 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -23,6 +23,7 @@ import tla2sany.semantic.OpApplNode;
import tla2sany.semantic.OpDeclNode;
import tla2sany.semantic.OpDefNode;
import tla2sany.semantic.StringNode;
+import tla2sany.semantic.SymbolNode;
import tlc2.tool.BuiltInOPs;
import tlc2.value.SetEnumValue;
import tlc2.value.Value;
@@ -195,8 +196,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
AAbstractMachineParseUnit aAbstractMachineParseUnit = new AAbstractMachineParseUnit();
aAbstractMachineParseUnit.setVariant(new AMachineMachineVariant());
AMachineHeader machineHeader = new AMachineHeader();
- List<TIdentifierLiteral> headerName = createTIdentifierLiteral(moduleNode
- .getName().toString());
+ List<TIdentifierLiteral> headerName = createTIdentifierLiteral(getName(moduleNode));
machineHeader.setName(headerName);
aAbstractMachineParseUnit.setHeader(machineHeader);
@@ -210,7 +210,6 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
createOperationsClause();
aAbstractMachineParseUnit.setMachineClauses(machineClauseList);
-
start = new Start(aAbstractMachineParseUnit, new EOF());
}
@@ -283,21 +282,19 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
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()));
+ list.add(createIdentifierNode(p));
}
-
// TLAType type = (TLAType) opDefNode.getToolObject(TYPE_ID);
// if (opDefNode.level == 2 || type instanceof BoolType) {
if (predicateVsExpression.getDefinitionType(opDefNode) == DefinitionType.PREDICATE) {
APredicateDefinitionDefinition d = new APredicateDefinitionDefinition();
- d.setName(new TDefLiteralPredicate(opDefNode.getName()
- .toString()));
+ d.setName(new TDefLiteralPredicate(getName(opDefNode)));
d.setParameters(list);
d.setRhs(visitExprNodePredicate(opDefNode.getBody()));
defs.add(d);
} else {
AExpressionDefinitionDefinition d = new AExpressionDefinitionDefinition();
- d.setName(new TIdentifierLiteral(opDefNode.getName().toString()));
+ d.setName(new TIdentifierLiteral(getName(opDefNode)));
d.setParameters(list);
d.setRhs(visitExprNodeExpression(opDefNode.getBody()));
@@ -361,11 +358,14 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
List<POperation> opList = new ArrayList<POperation>();
for (int i = 0; i < bOperations.size(); i++) {
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.getFormalParams().size(); j++) {
+ paramList
+ .add(createIdentifierNode(op.getFormalParams().get(j)));
}
for (int j = 0; j < op.getExistQuans().size(); j++) {
OpApplNode o = op.getExistQuans().get(j);
@@ -381,7 +381,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
OpDeclNode[] vars = moduleNode.getVariableDecls();
List<PExpression> anyParams = new ArrayList<PExpression>();
for (int j = 0; j < vars.length; j++) {
- String varName = vars[j].getName().toString();
+ String varName = getName(vars[j]);
String nextName = varName + "_n";
if (op.getUnchangedVariables().contains(varName))
continue;
@@ -420,10 +420,11 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
List<PExpression> varList = new ArrayList<PExpression>();
List<PExpression> valueList = new ArrayList<PExpression>();
for (int j = 0; j < vars.length; j++) {
- String varName = vars[j].getName().toString();
+ String varName = getName(vars[j]);
if (op.getUnchangedVariables().contains(varName))
continue;
- varList.add(createIdentifierNode(varName));
+ varList.add(createIdentifierNode(vars[j]));
+
valueList.add(createIdentifierNode(varName + "_n"));
}
AAssignSubstitution assign = new AAssignSubstitution(varList,
@@ -443,7 +444,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
return;
List<PExpression> varList = new ArrayList<PExpression>();
for (int i = 0; i < vars.length; i++) {
- varList.add(createIdentifierNode(vars[i].getName().toString()));
+ varList.add(createIdentifierNode(vars[i]));
}
ABecomesSuchSubstitution becomes = new ABecomesSuchSubstitution();
becomes.setIdentifiers(varList);
@@ -465,8 +466,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
List<PExpression> list = new ArrayList<PExpression>();
for (OpDeclNode opDeclNode : bVariables) {
AIdentifierExpression id = new AIdentifierExpression(
- createTIdentifierLiteral(opDeclNode.getName()
- .toString()));
+ createTIdentifierLiteral(getName(opDeclNode)));
list.add(id);
}
AVariablesMachineClause varClause = new AVariablesMachineClause(
@@ -476,7 +476,6 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
private void createConstantsClause() {
-
List<OpDeclNode> bConstants;
if (conEval != null) {
bConstants = conEval.getbConstantList();
@@ -487,16 +486,14 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
List<PExpression> constantsList = new ArrayList<PExpression>();
for (OpDeclNode opDeclNode : bConstants) {
AIdentifierExpression id = new AIdentifierExpression(
- createTIdentifierLiteral(opDeclNode.getName().toString()));
+ createTIdentifierLiteral(getName(opDeclNode)));
constantsList.add(id);
}
for (RecursiveDefinition recDef : specAnalyser
.getRecursiveDefinitions()) {
-
AIdentifierExpression id = new AIdentifierExpression(
- createTIdentifierLiteral(recDef.getOpDefNode().getName()
- .toString()));
+ createTIdentifierLiteral(getName(recDef.getOpDefNode())));
constantsList.add(id);
}
@@ -508,26 +505,29 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
+ private AIdentifierExpression createIdentifierNode(SymbolNode symbolNode) {
+ return createIdentifierNode(symbolNode.getName().toString());
+ }
+
private void createPropertyClause() {
List<PPredicate> propertiesList = new ArrayList<PPredicate>();
for (RecursiveDefinition recDef : specAnalyser
.getRecursiveDefinitions()) {
OpDefNode def = recDef.getOpDefNode();
- TLAType t = (TLAType) def.getToolObject(TYPE_ID);
+ //TLAType t = (TLAType) def.getToolObject(TYPE_ID);
// OpApplNode ifThenElse = recDef.getIfThenElse();
FormalParamNode[] params = def.getParams();
ArrayList<PExpression> paramList1 = new ArrayList<PExpression>();
ArrayList<PPredicate> typeList = new ArrayList<PPredicate>();
// ArrayList<PExpression> paramList2 = new ArrayList<PExpression>();
for (FormalParamNode p : params) {
- paramList1.add(createIdentifierNode(p.getName().toString()));
+ paramList1.add(createIdentifierNode(p));
// paramList2.add(createIdentifierNode(p.getName().toString()));
TLAType paramType = (TLAType) p.getToolObject(TYPE_ID);
- System.out.println(paramType);
+ // System.out.println(paramType);
AEqualPredicate equal = new AEqualPredicate(
- createIdentifierNode(p.getName().toString()),
- paramType.getBNode());
+ createIdentifierNode(p), paramType.getBNode());
typeList.add(equal);
}
ALambdaExpression lambda1 = new ALambdaExpression();
@@ -546,7 +546,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
// AUnionExpression union = new AUnionExpression(lambda1, lambda2);
AEqualPredicate equals = new AEqualPredicate(
- createIdentifierNode(def.getName().toString()), lambda1);
+ createIdentifierNode(def), lambda1);
propertiesList.add(equals);
}
@@ -569,20 +569,20 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
if (isEnum) {
AEqualPredicate equal = new AEqualPredicate();
- equal.setLeft(createIdentifierNode(con.getName().toString()));
+ equal.setLeft(createIdentifierNode(con));
equal.setRight(createIdentifierNode(((SetType) t)
.getSubType().toString()));
propertiesList.add(equal);
} else {
AEqualPredicate equal = new AEqualPredicate();
- equal.setLeft(createIdentifierNode(con.getName().toString()));
+ equal.setLeft(createIdentifierNode(con));
Value tlcValue = v.getValue();
equal.setRight(createTLCValue(tlcValue));
propertiesList.add(equal);
}
} else {
AMemberPredicate member = new AMemberPredicate();
- member.setLeft(createIdentifierNode(con.getName().toString()));
+ member.setLeft(createIdentifierNode(con));
TLAType t = (TLAType) con.getToolObject(TYPE_ID);
member.setRight(t.getBNode());
propertiesList.add(member);
@@ -609,7 +609,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
AEqualPredicate equal = new AEqualPredicate();
- equal.setLeft(createIdentifierNode(con.getName().toString()));
+ equal.setLeft(createIdentifierNode(con));
equal.setRight(visitExprNodeExpression(def.getBody()));
propertiesList.add(equal);
}
@@ -631,7 +631,6 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
private PExpression createTLCValue(Value tlcValue) {
switch (tlcValue.getKind()) {
case INTVALUE:
-
return new AIntegerExpression(new TIntegerLiteral(
tlcValue.toString()));
@@ -650,7 +649,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
TLAType varType = (TLAType) vars[i].getToolObject(TYPE_ID);
AMemberPredicate member = new AMemberPredicate();
- member.setLeft(createIdentifierNode(vars[i].getName().toString()));
+ member.setLeft(createIdentifierNode(vars[i]));
member.setRight(varType.getBNode());
predList.add(member);
@@ -659,8 +658,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
if (conEval != null) {
for (OpDefNode def : conEval.getInvariants()) {
ADefinitionPredicate defPred = new ADefinitionPredicate();
- defPred.setDefLiteral(new TDefLiteralPredicate(def.getName()
- .toString()));
+ defPred.setDefLiteral(new TDefLiteralPredicate(getName(def)));
predList.add(defPred);
}
}
@@ -735,7 +733,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
select.setRecord(visitExprNodeExpression(at.getAtBase()));
StringNode stringNode = (StringNode) list.get(0);
select.setIdentifier(createIdentifierNode(stringNode.getRep()
- .toString()));
+ .toString())); // TODO renamed
return select;
}
}
@@ -754,12 +752,12 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
private PPredicate visitOpApplNodePredicate(OpApplNode n) {
switch (n.getOperator().getKind()) {
case ConstantDeclKind: {
- return new AEqualPredicate(createIdentifierNode(n.getOperator()
- .getName().toString()), new ABooleanTrueExpression());
+ return new AEqualPredicate(createIdentifierNode(n.getOperator()),
+ new ABooleanTrueExpression());
}
case VariableDeclKind: {
- return new AEqualPredicate(createIdentifierNode(n.getOperator()
- .getName().toString()), new ABooleanTrueExpression());
+ return new AEqualPredicate(createIdentifierNode(n.getOperator()),
+ new ABooleanTrueExpression());
}
case BuiltInKind:
@@ -777,10 +775,10 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
private PExpression visitOpApplNodeExpression(OpApplNode n) {
switch (n.getOperator().getKind()) {
case ConstantDeclKind: {
- return createIdentifierNode(n.getOperator().getName().toString());
+ return createIdentifierNode(n.getOperator());
}
case VariableDeclKind: {
- return createIdentifierNode(n.getOperator().getName().toString());
+ return createIdentifierNode(n.getOperator());
}
case FormalParamKind: {
@@ -788,8 +786,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
ExprOrOpArgNode e = (ExprOrOpArgNode) param
.getToolObject(SUBSTITUTE_PARAM);
if (e == null) {
- return createIdentifierNode(n.getOperator().getName()
- .toString());
+ return createIdentifierNode(n.getOperator());
} else {
return visitExprOrOpArgNodeExpression(e);
}
@@ -810,7 +807,6 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
private PPredicate visitUserdefinedOpPredicate(OpApplNode n) {
OpDefNode def = (OpDefNode) n.getOperator();
-
if (BBuiltInOPs.contains(def.getName()) // Operator is a B built-in
// operator
&& STANDARD_MODULES.contains(def.getSource()
@@ -825,22 +821,23 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
if (predicateVsExpression.getDefinitionType(def) == DefinitionType.EXPRESSION) {
ADefinitionExpression defCall = new ADefinitionExpression();
- defCall.setDefLiteral(new TIdentifierLiteral(def.getName()
- .toString()));
- ;
+ defCall.setDefLiteral(new TIdentifierLiteral(getName(def)));
defCall.setParameters(params);
return new AEqualPredicate(defCall, new ABooleanTrueExpression());
} else {
ADefinitionPredicate defCall = new ADefinitionPredicate();
- defCall.setDefLiteral(new TDefLiteralPredicate(def.getName()
- .toString()));
+ defCall.setDefLiteral(new TDefLiteralPredicate(getName(def)));
defCall.setParameters(params);
return defCall;
}
}
+ private String getName(SymbolNode def) {
+ return def.getName().toString();
+ }
+
private PExpression visitUserdefinedOpExpression(OpApplNode n) {
OpDefNode def = (OpDefNode) n.getOperator();
// Operator is a B built-in operator
@@ -867,7 +864,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
while (iter.hasNext()) {
Entry<OpDeclNode, OpDefNode> entry = iter.next();
if (entry.getValue().equals(def)) {
- name = entry.getKey().getName().toString();
+ name = getName(entry.getKey());
}
}
if (params.size() == 0) {
@@ -880,8 +877,8 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
} else {
ADefinitionExpression defExpr = new ADefinitionExpression();
- defExpr.setDefLiteral(new TIdentifierLiteral(n.getOperator()
- .getName().toString()));
+ defExpr.setDefLiteral(new TIdentifierLiteral(getName(n
+ .getOperator())));
defExpr.setParameters(params);
return defExpr;
}
@@ -1241,18 +1238,18 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
case OPCODE_sso: { // $SubsetOf Represents {x \in S : P}
// TODO tuple with more than 2 arguments
- FormalParamNode[][] params = n.getBdedQuantSymbolLists();
- ExprNode[] bounds = n.getBdedQuantBounds();
+ //FormalParamNode[][] params = n.getBdedQuantSymbolLists();
+ //ExprNode[] bounds = n.getBdedQuantBounds();
List<PExpression> list = new ArrayList<PExpression>();
FormalParamNode p = n.getBdedQuantSymbolLists()[0][0];
- list.add(createIdentifierNode(p.getName().toString()));
+ list.add(createIdentifierNode(p));
AComprehensionSetExpression compre = new AComprehensionSetExpression();
compre.setIdentifiers(list);
AMemberPredicate member = new AMemberPredicate();
- member.setLeft(createIdentifierNode(p.getName().toString()));
+ member.setLeft(createIdentifierNode(p));
ExprNode in = n.getBdedQuantBounds()[0];
member.setRight(visitExprNodeExpression(in));
@@ -1273,11 +1270,11 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
for (int i = 0; i < bounds.length; i++) {
FormalParamNode p = params[i][0];
AMemberPredicate member = new AMemberPredicate();
- member.setLeft(createIdentifierNode(p.getName().toString()));
+ member.setLeft(createIdentifierNode(p));
ExprNode in = n.getBdedQuantBounds()[i];
member.setRight(visitExprNodeExpression(in));
predList.add(member);
- idList.add(createIdentifierNode(p.getName().toString()));
+ idList.add(createIdentifierNode(p));
}
final String nameOfTempVariable = "t_";
AEqualPredicate equals = new AEqualPredicate();
@@ -1299,18 +1296,18 @@ 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();
+ //ExprNode[] bounds = n.getBdedQuantBounds(); TODO
List<PExpression> idList = new ArrayList<PExpression>();
List<PPredicate> predList = new ArrayList<PPredicate>();
for (int i = 0; i < params.length; i++) {
for (int j = 0; j < params[i].length; j++) {
FormalParamNode p = params[i][j];
AMemberPredicate member = new AMemberPredicate();
- member.setLeft(createIdentifierNode(p.getName().toString()));
+ member.setLeft(createIdentifierNode(p));
ExprNode in = n.getBdedQuantBounds()[i];
member.setRight(visitExprNodeExpression(in));
predList.add(member);
- idList.add(createIdentifierNode(p.getName().toString()));
+ idList.add(createIdentifierNode(p));
}
}
ALambdaExpression lambda = new ALambdaExpression();
@@ -1386,7 +1383,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
List<PRecEntry> recList = new ArrayList<PRecEntry>();
for (int i = 0; i < struct.getFields().size(); i++) {
- String fieldName = struct.getFields().get(i);
+ String fieldName = struct.getFields().get(i); // renamed name
AIdentifierExpression field = createIdentifierNode(fieldName);
ARecEntry rec = new ARecEntry();
rec.setIdentifier(field);
@@ -1433,7 +1430,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
rcdSelect.setRecord(visitExprOrOpArgNodeExpression(n.getArgs()[0]));
StringNode stringNode = (StringNode) n.getArgs()[1];
rcdSelect.setIdentifier(createIdentifierNode(stringNode.getRep()
- .toString()));
+ .toString())); // TODO renamed
return rcdSelect;
}
@@ -1510,7 +1507,8 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
if (value == null) {
value = new ARecordFieldExpression(
visitExprOrOpArgNodeExpression(n.getArgs()[0]),
- createIdentifierNode(fieldName));
+ createIdentifierNode(fieldName)); // TODO
+ // renamed
}
entry.setValue(value);
list.add(entry);
@@ -1519,7 +1517,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
return rec;
} else {
- FunctionType func = (FunctionType) type;
+ //FunctionType func = (FunctionType) type;
List<PExpression> list = new ArrayList<PExpression>();
for (int i = 1; i < n.getArgs().length; i++) {
@@ -1568,8 +1566,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
defCall.setDefLiteral(new TIdentifierLiteral("CHOOSE"));
AComprehensionSetExpression comprehension = new AComprehensionSetExpression();
FormalParamNode x = n.getUnbdedQuantSymbols()[0];
- comprehension.setIdentifiers(createIdentifierList(x.getName()
- .toString()));
+ comprehension.setIdentifiers(createIdentifierList(getName(x)));
comprehension
.setPredicates(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
List<PExpression> list = new ArrayList<PExpression>();
@@ -1583,10 +1580,9 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
defCall.setDefLiteral(new TIdentifierLiteral("CHOOSE"));
AComprehensionSetExpression comprehension = new AComprehensionSetExpression();
FormalParamNode x = n.getBdedQuantSymbolLists()[0][0];
- comprehension.setIdentifiers(createIdentifierList(x.getName()
- .toString()));
+ comprehension.setIdentifiers(createIdentifierList(x));
AMemberPredicate member = new AMemberPredicate();
- member.setLeft(createIdentifierNode(x.getName().toString()));
+ member.setLeft(createIdentifierNode(x));
ExprNode in = n.getBdedQuantBounds()[0];
member.setRight(visitExprNodeExpression(in));
AConjunctPredicate conj = new AConjunctPredicate();
@@ -1638,6 +1634,12 @@ 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
@@ -1693,8 +1695,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
ArrayList<PExpression> list = new ArrayList<PExpression>();
for (int i = 0; i < params.length; i++) {
for (int j = 0; j < params[i].length; j++) {
- list.add(createIdentifierNode(params[i][j].getName()
- .toString()));
+ list.add(createIdentifierNode(params[i][j]));
}
}
AConjunctPredicate conjunction = new AConjunctPredicate();
@@ -1708,8 +1709,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
ArrayList<PExpression> list = new ArrayList<PExpression>();
for (int i = 0; i < params.length; i++) {
for (int j = 0; j < params[i].length; j++) {
- list.add(createIdentifierNode(params[i][j].getName()
- .toString()));
+ list.add(createIdentifierNode(params[i][j]));
}
}
AImplicationPredicate implication = new AImplicationPredicate();
@@ -1799,9 +1799,9 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
case OPCODE_prime: // prime
{
OpApplNode node = (OpApplNode) n.getArgs()[0];
- return new AEqualPredicate(createIdentifierNode(node.getOperator()
- .getName().toString()
- + "_n"), new ABooleanTrueExpression());
+ return new AEqualPredicate(
+ createIdentifierNode(getName(node.getOperator()) + "_n"),
+ new ABooleanTrueExpression());
}
case OPCODE_unchanged: {
@@ -1853,8 +1853,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
ArrayList<PExpression> list = new ArrayList<PExpression>();
for (int j = 0; j < params[i].length; j++) {
- list.add(createIdentifierNode(params[i][j].getName()
- .toString()));
+ list.add(createIdentifierNode(params[i][j]));
}
AMemberPredicate member = new AMemberPredicate();
member.setLeft(new ACoupleExpression(list));
@@ -1863,8 +1862,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
} else {
for (int j = 0; j < params[i].length; j++) {
AMemberPredicate member = new AMemberPredicate();
- member.setLeft(createIdentifierNode(params[i][j].getName()
- .toString()));
+ member.setLeft(createIdentifierNode(params[i][j]));
member.setRight(visitExprNodeExpression(in[i]));
predList.add(member);
}
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index 6ac6512c95e4f7fa89dcd6c659ccab766527c7b3..fb81ace48886a75b0a82d7a05430200f6e5e24ca 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -1,8 +1,12 @@
package de.tla2bAst;
+import java.io.BufferedReader;
import java.io.File;
+import java.io.FileReader;
import java.io.FileWriter;
import java.io.IOException;
+import java.io.Writer;
+import java.util.Date;
import de.be4.classicalb.core.parser.Definitions;
import de.be4.classicalb.core.parser.node.Start;
@@ -17,22 +21,24 @@ import de.tla2b.config.ConfigfileEvaluator;
import de.tla2b.config.ModuleOverrider;
import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
+import de.tla2b.global.TranslationGlobals;
+import de.tla2b.output.ASTPrettyPrinter;
import de.tla2b.pprint.BMachinePrinter;
import tla2sany.drivers.SANY;
import tla2sany.modanalyzer.SpecObj;
import tla2sany.semantic.ModuleNode;
import tlc2.tool.ModelConfig;
-import util.FileUtil;
import util.ToolIO;
-public class Translator {
+public class Translator implements TranslationGlobals {
private String moduleFileName;
private File moduleFile;
private File configFile;
+ private Start BAst;
private Definitions bDefinitions;
- //private String moduleName;
+ // private String moduleName;
private ModuleNode moduleNode;
private ModelConfig modelConfig;
@@ -51,13 +57,11 @@ public class Translator {
String configFileName = removeExtention(moduleFile.getAbsolutePath());
configFileName = configFileName + ".cfg";
configFile = new File(configFileName);
- if(!configFile.exists()){
+ if (!configFile.exists()) {
configFile = null;
}
}
-
-
private void findModuleFile() {
moduleFile = new File(moduleFileName);
if (!moduleFile.exists()) {
@@ -103,11 +107,11 @@ public class Translator {
parse();
}
-
- public ModuleNode parseModule2() throws de.tla2b.exceptions.FrontEndException {
+ public ModuleNode parseModule2()
+ throws de.tla2b.exceptions.FrontEndException {
String fileName = moduleFile.getName();
ToolIO.setUserDir(moduleFile.getParent());
-
+
SpecObj spec = new SpecObj(fileName, null);
try {
SANY.frontEndMain(spec, fileName, ToolIO.out);
@@ -143,7 +147,7 @@ public class Translator {
return n;
}
-
+
public static String allMessagesToString(String[] allMessages) {
StringBuilder sb = new StringBuilder();
for (int i = 0; i < allMessages.length - 1; i++) {
@@ -151,10 +155,10 @@ public class Translator {
}
return sb.toString();
}
-
+
private void parse() throws FrontEndException {
moduleNode = parseModule2();
-
+
modelConfig = null;
if (configFile != null) {
modelConfig = new ModelConfig(configFile.getAbsolutePath(),
@@ -206,12 +210,68 @@ public class Translator {
UsedExternalFunctions usedExternalFunctions = new UsedExternalFunctions(
moduleNode, specAnalyser);
+
+ //BMacroHandler bMacroHandler = new BMacroHandler(specAnalyser, conEval);
BAstCreator bAstCreator = new BAstCreator(moduleNode, conEval,
specAnalyser, usedExternalFunctions, predicateVsExpression);
-
+ this.BAst = bAstCreator.getStartNode();
this.bDefinitions = bAstCreator.getBDefinitions();
- System.out.println(bDefinitions.getDefinitionNames());
- return bAstCreator.getStartNode();
+ return BAst;
+ }
+
+ public void createMachineFile() {
+ String bFile = removeExtention(moduleFile.getAbsolutePath());
+ bFile = bFile + "_tla.mch";
+
+ File machineFile;
+ machineFile = new File(bFile);
+ if (machineFile.exists()) {
+ try {
+ BufferedReader in;
+ in = new BufferedReader(new FileReader(machineFile));
+ String firstLine = in.readLine();
+ in.close();
+ if (firstLine != null && !firstLine.startsWith("/*@ generated by TLA2B ")) {
+ System.err.println("Error: File " + machineFile.getName()
+ + " already exists"
+ + " and was not generated by TLA2B.\n"
+ + "Delete or move this file.");
+ System.exit(-1);
+ }
+ } catch (IOException e) {
+ System.err.println(e.getMessage());
+ System.exit(-1);
+ }
+ }
+
+ try {
+ machineFile.createNewFile();
+ } catch (IOException e) {
+ System.err.println(String.format("Could not create File %s.",
+ machineFile.getName()));
+ System.exit(-1);
+ }
+
+
+ ASTPrettyPrinter aP = new ASTPrettyPrinter();
+ BAst.apply(aP);
+ StringBuilder result = aP.getResultAsStringbuilder();
+ result.insert(0, "/*@ generated by TLA2B " + VERSION + " " + new Date()
+ + " */\n");
+
+ Writer fw = null;
+ try {
+ fw = new FileWriter(machineFile);
+ fw.write(result.toString());
+ fw.close();
+ System.out.println("B-Machine " + machineFile.getAbsolutePath()
+ + " created.");
+ } catch (IOException e) {
+ System.err.println("Error while creating file '"
+ + machineFile.getAbsolutePath() + "'.");
+ System.exit(-1);
+ }
+
}
public static String removeExtention(String filePath) {
@@ -236,7 +296,7 @@ public class Translator {
return renamed.getPath();
}
}
-
+
public Definitions getBDefinitions() {
return bDefinitions;
}
diff --git a/src/test/java/de/tla2b/main/MainTest.java b/src/test/java/de/tla2b/main/MainTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..08a620042c6b443690e628010a44b0e9e8a0a1dc
--- /dev/null
+++ b/src/test/java/de/tla2b/main/MainTest.java
@@ -0,0 +1,15 @@
+package de.tla2b.main;
+
+import org.junit.Test;
+
+import de.tla2b.TLA2B;
+
+public class MainTest {
+
+ @Test
+ public void testClub() throws Exception {
+ String file = "src/test/resources/examples/Club/Club.tla";
+ TLA2B.main(new String[] { file });
+ }
+
+}
diff --git a/src/test/java/de/tla2b/main/RenamerTest.java b/src/test/java/de/tla2b/main/RenamerTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..daa61456772ddcf0d668158234e1dadfa4766abc
--- /dev/null
+++ b/src/test/java/de/tla2b/main/RenamerTest.java
@@ -0,0 +1,14 @@
+package de.tla2b.main;
+
+import org.junit.Test;
+
+import de.tla2b.util.TestUtil;
+
+public class RenamerTest {
+
+ @Test
+ public void testKeywords() throws Exception {
+ String file = "src/test/resources/renamer/Keywords.tla";
+ TestUtil.renamerTest(file);
+ }
+}
diff --git a/src/test/java/de/tla2b/prettyprintb/RecursiveFunctionTest.java b/src/test/java/de/tla2b/prettyprintb/RecursiveFunctionTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..298c66e94920edef265dd3cd1eec5e746feef9e6
--- /dev/null
+++ b/src/test/java/de/tla2b/prettyprintb/RecursiveFunctionTest.java
@@ -0,0 +1,50 @@
+package de.tla2b.prettyprintb;
+
+import static de.tla2b.util.TestUtil.compare;
+
+import org.junit.Ignore;
+import org.junit.Test;
+
+public class RecursiveFunctionTest {
+
+ @Ignore
+ @Test
+ public void testRecursiveDefinition() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "RECURSIVE sum(_) \n"
+ + "sum(S) == IF S = {} THEN 0 ELSE (LET x == CHOOSE a \\in S : TRUE IN x + sum(S \\ {x})) \n"
+ + "ASSUME sum({1,2,3}) = 6 \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
+ + "PROPERTIES "
+ + " k : BOOL +-> INTEGER "
+ + "& k = k <+ {TRUE |-> 0, FALSE |-> 0}" + "END";
+ compare(expected, module);
+
+ }
+
+ @Ignore
+ @Test
+ public void testRecursiveDefinition2() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "RECURSIVE Sum(_,_) \n"
+ + " Sum(f,S) == IF S = {} THEN 0 \n"
+ + " ELSE LET x == CHOOSE x \\in S : TRUE \n"
+ + " IN f[x] + Sum(f, S \\ {x}) \n"
+ + "foo[x \\in Nat] == x \n"
+ + "ASSUME Sum(foo, {1,2,3}) = 6 \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
+ + "PROPERTIES "
+ + " k = k <+ {TRUE |-> 0, FALSE |-> 0}" + "END";
+ compare(expected, module);
+
+ }
+
+
+
+}
diff --git a/src/test/java/de/tla2b/util/TestUtil.java b/src/test/java/de/tla2b/util/TestUtil.java
index 0786923b6c285de7417a788f2ec2fe79c732201d..ff6e2832443034006a81432e967cb36ba4dd840c 100644
--- a/src/test/java/de/tla2b/util/TestUtil.java
+++ b/src/test/java/de/tla2b/util/TestUtil.java
@@ -16,7 +16,8 @@ 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.output.ASTPrettyPrinter;
+import de.tla2b.output.Renamer;
import de.tla2b.translation.Tla2BTranslator;
import de.tla2bAst.Translator;
import tla2sany.semantic.AbortException;
@@ -49,11 +50,11 @@ public class TestUtil {
System.out.println("-------------------");
ASTPrettyPrinter aP = new ASTPrettyPrinter();
start.apply(aP);
- System.out.println(aP.getResult());
+ System.out.println(aP.getResultString());
final BParser parser = new BParser("testcase");
- final Start ppStart = parser.parse(aP.getResult(), false);
+ final Start ppStart = parser.parse(aP.getResultString(), false);
String result = getTreeAsString(start);
@@ -79,9 +80,9 @@ public class TestUtil {
ASTPrettyPrinter aP = new ASTPrettyPrinter();
resultNode.apply(aP);
System.out.println("-------------------");
- System.out.println(aP.getResult());
+ System.out.println(aP.getResultString());
final BParser parser = new BParser("testcase");
- Start ast = parser.parse(aP.getResult(), false);
+ Start ast = parser.parse(aP.getResultString(), false);
//BParser.printASTasProlog(System.out, new BParser(), new File("./test.mch"), resultNode, false, true, null);
@@ -161,6 +162,19 @@ public class TestUtil {
}
+ public static void renamerTest(String tlaFile) throws Exception{
+ Translator t = new Translator(tlaFile);
+ Start start = t.translate();
+ Renamer renamer = new Renamer(start);
+ ASTPrettyPrinter aP = new ASTPrettyPrinter(renamer);
+ start.apply(aP);
+ System.out.println(aP.getResultString());
+
+ final BParser parser = new BParser("testcase");
+ parser.parse(aP.getResultString(), false);
+ }
+
+
public static TestTypeChecker typeCheckString(String moduleString) throws FrontEndException, TLA2BException{
ToolIO.setMode(ToolIO.TOOL);
ToolIO.reset();
diff --git a/src/test/resources/renamer/Keywords.tla b/src/test/resources/renamer/Keywords.tla
new file mode 100644
index 0000000000000000000000000000000000000000..72fd514edafec6ab690b596612767b69f76e7fab
--- /dev/null
+++ b/src/test/resources/renamer/Keywords.tla
@@ -0,0 +1,11 @@
+---- MODULE Keywords ----
+min == 1
+ASSUME min = 1
+CONSTANTS max
+ASSUME max = 2
+VARIABLES dom
+Init == dom = 1
+struct == dom' = 2
+
+Next == struct
+=====
\ No newline at end of file