Select Git revision
ExpressionTranslator.java
Code owners
Assign users and groups as approvers for specific file changes. Learn more.
ExpressionTranslator.java 10.08 KiB
/**
* @author Dominik Hansen <Dominik.Hansen at hhu.de>
**/
package de.tla2b.translation;
import java.io.File;
import java.io.FileWriter;
import java.io.IOException;
import java.util.ArrayList;
import java.util.HashSet;
import java.util.Set;
import de.tla2b.analysis.SymbolRenamer;
import de.tla2b.analysis.TypeChecker;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.exceptions.TLA2BIOException;
import de.tla2b.exceptions.TypeErrorException;
import de.tla2b.pprint.ExpressionPrinter;
import tla2sany.drivers.FrontEndException;
import tla2sany.drivers.InitException;
import tla2sany.drivers.SANY;
import tla2sany.modanalyzer.ParseUnit;
import tla2sany.modanalyzer.SpecObj;
import tla2sany.parser.ParseException;
import tla2sany.semantic.ModuleNode;
import tla2sany.st.SyntaxTreeConstants;
import tla2sany.st.TreeNode;
import util.ToolIO;
public class ExpressionTranslator implements SyntaxTreeConstants {
private String TLAExpression;
private ArrayList<String> variables;
private ArrayList<String> noVariables;
private StringBuilder BExpression;
public static String translateExpression(String tlaExpression)
throws TLA2BException {
ToolIO.reset();
ToolIO.setMode(ToolIO.TOOL);
ExpressionTranslator et = new ExpressionTranslator(tlaExpression);
try {
et.start();
} catch (RuntimeException e) {
throw new TLA2BIOException(e.getMessage());
}
return et.BExpression.toString();
}
public ExpressionTranslator(String TLAExpression) {
this.TLAExpression = TLAExpression;
this.variables = new ArrayList<String>();
this.noVariables = new ArrayList<String>();
}
public void start() throws TLA2BException {
String dir = System.getProperty("java.io.tmpdir");
ToolIO.setUserDir(dir);
createStandardModule(dir);
File tempFile = null;
String moduleName = null;
String module = null;
try {
tempFile = File.createTempFile("Testing", ".tla");