diff --git a/src/main/java/de/tla2b/output/ASTPrettyPrinter.java b/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
index 5ad97b0e06348ea8a2ee6ff6a292f468332cca9b..a2cf80c51e889f69d55383e1b1c007ccbedd7eaf 100644
--- a/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
+++ b/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
@@ -6,8 +6,13 @@ import java.util.Iterator;
import java.util.List;
import de.be4.classicalb.core.parser.node.*;
+import de.be4.classicalb.core.parser.util.PrettyPrinter;
import de.tla2b.util.ExtendedDFAdapter;
+/**
+ * @deprecated Use {@link PrettyPrinter} from the B parser library instead.
+ */
+@Deprecated
public class ASTPrettyPrinter extends ExtendedDFAdapter {
private final StringBuilder sb = new StringBuilder();
private Renamer renamer;
@@ -726,6 +731,7 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
}
+@Deprecated
class PrettyPrintNode {
private String begin = "";
private String beginList = "";
diff --git a/src/main/java/de/tla2b/output/Renamer.java b/src/main/java/de/tla2b/output/Renamer.java
index 1e768d72b0bbd9e5b53b0dcffbc04cf8fda14a0d..2f55f7e08098baea2521dc05b6ba657c618ce9db 100644
--- a/src/main/java/de/tla2b/output/Renamer.java
+++ b/src/main/java/de/tla2b/output/Renamer.java
@@ -4,13 +4,18 @@ import java.util.HashMap;
import java.util.HashSet;
import java.util.Set;
-import de.be4.classicalb.core.parser.util.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;
+import de.be4.classicalb.core.parser.util.SuffixIdentifierRenaming;
+import de.be4.classicalb.core.parser.util.Utils;
+/**
+ * @deprecated Use {@link SuffixIdentifierRenaming} from the B parser library instead.
+ */
+@Deprecated
public class Renamer extends DepthFirstAdapter {
private final HashMap<Node, String> namesTables;
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index df6ee7126e8580779e203c0835ebc3cb6ac15d99..ef24f2dcf19afef273a624c72ec00fde5796af86 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -20,6 +20,8 @@ import de.be4.classicalb.core.parser.exceptions.BCompoundException;
import de.be4.classicalb.core.parser.exceptions.PreParseException;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.Start;
+import de.be4.classicalb.core.parser.util.PrettyPrinter;
+import de.be4.classicalb.core.parser.util.SuffixIdentifierRenaming;
import de.tla2b.analysis.InstanceTransformation;
import de.tla2b.analysis.PredicateVsExpression;
import de.tla2b.analysis.SpecAnalyser;
@@ -32,17 +34,18 @@ 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.output.PrologPrinter;
-import de.tla2b.output.Renamer;
import de.tla2b.translation.BMacroHandler;
import de.tla2b.translation.RecursiveFunctionHandler;
import de.tla2b.types.TLAType;
import de.tla2b.util.FileUtils;
+
import tla2sany.drivers.SANY;
import tla2sany.modanalyzer.SpecObj;
import tla2sany.semantic.ModuleNode;
+
import tlc2.tool.ModelConfig;
+
import util.ToolIO;
public class Translator implements TranslationGlobals {
@@ -100,10 +103,10 @@ public class Translator implements TranslationGlobals {
throws TLA2BException {
Translator translator = new Translator(moduleName, moduleString, configString);
Start bAST = translator.getBAST();
- Renamer renamer = new Renamer(bAST);
- ASTPrettyPrinter aP = new ASTPrettyPrinter(bAST, renamer);
- bAST.apply(aP);
- return aP.getResultString();
+ PrettyPrinter pp = new PrettyPrinter();
+ pp.setRenaming(new SuffixIdentifierRenaming());
+ bAST.apply(pp);
+ return pp.getPrettyPrint();
}
public Translator(String moduleName, String moduleString, String configString) throws TLA2BException {
@@ -317,16 +320,15 @@ public class Translator implements TranslationGlobals {
System.exit(-1);
}
- Renamer renamer = new Renamer(BAst);
- ASTPrettyPrinter aP = new ASTPrettyPrinter(BAst, renamer);
- BAst.apply(aP);
- StringBuilder result = aP.getResultAsStringbuilder();
- result.insert(0, "/*@ generated by TLA2B " + VERSION_NUMBER + " " + new Date() + " */\n");
+ PrettyPrinter pp = new PrettyPrinter();
+ pp.setRenaming(new SuffixIdentifierRenaming());
+ BAst.apply(pp);
+ String result = "/*@ generated by TLA2B " + VERSION_NUMBER + " " + new Date() + " */\n" + pp.getPrettyPrint();
try {
BufferedWriter out = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(machineFile), "UTF-8"));
try {
- out.write(result.toString());
+ out.write(result);
} finally {
out.close();
}
diff --git a/src/test/java/de/tla2b/util/TestUtil.java b/src/test/java/de/tla2b/util/TestUtil.java
index 40078282bd2d55665a746a076c8a7a3bf7139de8..4ba66b456802949249d83c2af974c1b911e59e50 100644
--- a/src/test/java/de/tla2b/util/TestUtil.java
+++ b/src/test/java/de/tla2b/util/TestUtil.java
@@ -5,10 +5,10 @@ import de.be4.classicalb.core.parser.analysis.prolog.ASTProlog;
import de.be4.classicalb.core.parser.exceptions.BCompoundException;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.Start;
+import de.be4.classicalb.core.parser.util.PrettyPrinter;
+import de.be4.classicalb.core.parser.util.SuffixIdentifierRenaming;
import de.prob.prolog.output.PrologTermStringOutput;
import de.tla2b.exceptions.TLA2BException;
-import de.tla2b.output.ASTPrettyPrinter;
-import de.tla2b.output.Renamer;
import de.tla2bAst.Translator;
import util.FileUtil;
@@ -27,10 +27,12 @@ public class TestUtil {
Translator t = new Translator(tlaFile);
Start start = t.translate();
- ASTPrettyPrinter aP = new ASTPrettyPrinter(start);
- start.apply(aP);
+ PrettyPrinter pp = new PrettyPrinter();
+ // FIXME Is it intentional that we don't use SuffixIdentifierRenaming here?
+ start.apply(pp);
+ System.out.println(pp.getPrettyPrint());
final BParser parser = new BParser("testcase");
- final Start ppStart = parser.parse(aP.getResultString(), false);
+ final Start ppStart = parser.parse(pp.getPrettyPrint(), false);
String result = getTreeAsString(start);
String ppResult = getTreeAsString(ppStart);
@@ -43,11 +45,11 @@ public class TestUtil {
ToolIO.setMode(ToolIO.TOOL);
ToolIO.reset();
Start resultNode = Translator.translateTlaExpression(tlaExpr);
- Renamer renamer = new Renamer(resultNode);
- ASTPrettyPrinter aP = new ASTPrettyPrinter(resultNode, renamer);
- resultNode.apply(aP);
+ PrettyPrinter pp = new PrettyPrinter();
+ pp.setRenaming(new SuffixIdentifierRenaming());
+ resultNode.apply(pp);
String bAstString = getAstStringofBExpressionString(bExpr);
- String result = getAstStringofBExpressionString(aP.getResultString());
+ String result = getAstStringofBExpressionString(pp.getPrettyPrint());
// String tlaAstString = getTreeAsString(resultNode);
assertEquals(bAstString, result);
}
@@ -56,11 +58,11 @@ public class TestUtil {
Translator trans = new Translator(moduleString, null);
trans.translate();
Start resultNode = trans.translateExpression(tlaExpr);
- Renamer renamer = new Renamer(resultNode);
- ASTPrettyPrinter aP = new ASTPrettyPrinter(resultNode, renamer);
- resultNode.apply(aP);
+ PrettyPrinter pp = new PrettyPrinter();
+ pp.setRenaming(new SuffixIdentifierRenaming());
+ resultNode.apply(pp);
String bAstString = getAstStringofBExpressionString(bExpr);
- String result = getAstStringofBExpressionString(aP.getResultString());
+ String result = getAstStringofBExpressionString(pp.getPrettyPrint());
assertEquals(bAstString, result);
}
@@ -94,11 +96,11 @@ public class TestUtil {
public static void renamerTest(String tlaFile) throws BCompoundException, TLA2BException {
Translator t = new Translator(tlaFile);
Start start = t.translate();
- Renamer renamer = new Renamer(start);
- ASTPrettyPrinter aP = new ASTPrettyPrinter(start, renamer);
- start.apply(aP);
+ PrettyPrinter pp = new PrettyPrinter();
+ pp.setRenaming(new SuffixIdentifierRenaming());
+ start.apply(pp);
final BParser parser = new BParser("testcase");
- parser.parse(aP.getResultString(), false);
+ parser.parse(pp.getPrettyPrint(), false);
}
public static TestTypeChecker typeCheckString(String moduleString) throws TLA2BException {
diff --git a/src/test/java/testing/ExampleFilesTest.java b/src/test/java/testing/ExampleFilesTest.java
index 241befa6c62271cde994fd64582c3ee0146c91a0..ad2dfc1c3b545b6039855343be802052b910548d 100644
--- a/src/test/java/testing/ExampleFilesTest.java
+++ b/src/test/java/testing/ExampleFilesTest.java
@@ -3,19 +3,20 @@ package testing;
import java.io.File;
import java.util.ArrayList;
-import org.junit.Test;
-import org.junit.runner.RunWith;
-
import de.be4.classicalb.core.parser.BParser;
import de.be4.classicalb.core.parser.node.Start;
-import de.tla2b.output.ASTPrettyPrinter;
+import de.be4.classicalb.core.parser.util.PrettyPrinter;
import de.tla2b.util.AbstractParseModuleTest;
import de.tla2b.util.FileUtils;
import de.tla2b.util.PolySuite;
-import de.tla2b.util.TestUtil;
import de.tla2b.util.PolySuite.Config;
import de.tla2b.util.PolySuite.Configuration;
+import de.tla2b.util.TestUtil;
import de.tla2bAst.Translator;
+
+import org.junit.Test;
+import org.junit.runner.RunWith;
+
import static org.junit.Assert.assertEquals;
@RunWith(PolySuite.class)
@@ -35,12 +36,13 @@ public class ExampleFilesTest extends AbstractParseModuleTest {
Start start = t.translate();
String resultTree = TestUtil.getTreeAsString(start);
- ASTPrettyPrinter aP = new ASTPrettyPrinter(start);
- start.apply(aP);
+ PrettyPrinter pp = new PrettyPrinter();
+ // FIXME Is it intentional that we don't use SuffixIdentifierRenaming here?
+ start.apply(pp);
// parse pretty print result
final BParser parser = new BParser("testcase");
- final Start ppStart = parser.parse(aP.getResultString(), false);
+ final Start ppStart = parser.parse(pp.getPrettyPrint(), false);
String ppTree = TestUtil.getTreeAsString(ppStart);
// comparing result with pretty print