Skip to content
Snippets Groups Projects
Select Git revision
  • 0a4f120cfac7c5e610ef1d858e025287e8a293c6
  • master default protected
  • release/1.1.4
  • release/1.1.3
  • release/1.1.1
  • 1.4.2
  • 1.4.1
  • 1.4.0
  • 1.3.0
  • 1.2.1
  • 1.2.0
  • 1.1.5
  • 1.1.4
  • 1.1.3
  • 1.1.1
  • 1.1.0
  • 1.0.9
  • 1.0.8
  • 1.0.7
  • v1.0.5
  • 1.0.5
21 results

ExpressionTranslator.java

Blame
  • 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");