package de.tla2bAst; import java.io.File; import java.io.FileWriter; import java.io.IOException; import de.be4.classicalb.core.parser.Definitions; import de.be4.classicalb.core.parser.node.Start; import de.tla2b.analysis.InstanceTransformation; import de.tla2b.analysis.SpecAnalyser; import de.tla2b.analysis.SymbolRenamer; import de.tla2b.analysis.SymbolSorter; import de.tla2b.analysis.TypeChecker; import de.tla2b.config.ConfigfileEvaluator; import de.tla2b.config.ModuleOverrider; import de.tla2b.exceptions.FrontEndException; import de.tla2b.exceptions.TLA2BException; import de.tla2b.pprint.BAstCreator; import de.tla2b.pprint.BMachinePrinter; import tla2sany.semantic.ModuleNode; import tlc2.tool.ModelConfig; import util.FileUtil; import util.ToolIO; public class Translator { private String moduleFileName; private String configFileName; private Definitions bDefinitions; private String moduleName; private ModuleNode moduleNode; private ModelConfig modelConfig; private String bMachineString; public Translator(String moduleFileName, String configFileName) throws FrontEndException { this.moduleFileName = moduleFileName; this.configFileName = configFileName; parse(); } //Used for Testing public Translator(String moduleString, String configString, int i) throws FrontEndException { moduleName = "Testing"; File dir = new File("temp/"); dir.mkdirs(); try { File f = new File("temp/" + moduleName + ".tla"); f.createNewFile(); FileWriter fw = new FileWriter(f); fw.write(moduleString); fw.close(); //f.deleteOnExit(); moduleFileName = f.getAbsolutePath(); } catch (IOException e) { e.printStackTrace(); } modelConfig = null; if (configString != null) { File f = new File("temp/" + moduleName + ".cfg"); try { f.createNewFile(); FileWriter fw = new FileWriter(f); fw.write(configString); fw.close(); } catch (IOException e) { e.printStackTrace(); } //f.deleteOnExit(); configFileName = f.getAbsolutePath(); } dir.deleteOnExit(); parse(); } //Used for Testing public Translator(String moduleString) throws FrontEndException { moduleName = "Testing"; File dir = new File("temp/"); dir.mkdirs(); try { File f = new File("temp/" + moduleName + ".tla"); f.createNewFile(); FileWriter fw = new FileWriter(f); fw.write(moduleString); fw.close(); //f.deleteOnExit(); moduleFileName = f.getAbsolutePath(); } catch (IOException e) { e.printStackTrace(); } parseModule(); } private void parseModule() throws FrontEndException { moduleName = evalFileName(moduleFileName); TLAParser tlaParser = new TLAParser(null); moduleNode = tlaParser.parseModule(moduleName); } private void parse() throws FrontEndException{ moduleName = evalFileName(moduleFileName); TLAParser tlaParser = new TLAParser(null); moduleNode = tlaParser.parseModule(moduleName); modelConfig = null; if (configFileName != null) { File f = new File(configFileName); if(f.exists()){ modelConfig = new ModelConfig(f.getName(), null); modelConfig.parse(); } }else { String fileNameWithoutSuffix = moduleFileName; if (fileNameWithoutSuffix.toLowerCase().endsWith(".tla")) { fileNameWithoutSuffix = fileNameWithoutSuffix.substring(0, fileNameWithoutSuffix.length() - 4); } String configFile = fileNameWithoutSuffix + ".cfg"; File f = new File(configFile); if(f.exists()){ modelConfig = new ModelConfig(f.getName(), null); modelConfig.parse(); } } } public Start translate() throws TLA2BException { InstanceTransformation trans = new InstanceTransformation(moduleNode); trans.start(); SymbolSorter symbolSorter = new SymbolSorter(moduleNode); symbolSorter.sort(); SpecAnalyser specAnalyser; ConfigfileEvaluator conEval = null; if (modelConfig != null) { conEval = new ConfigfileEvaluator(modelConfig, moduleNode); conEval.start(); ModuleOverrider modOver = new ModuleOverrider(moduleNode, conEval); modOver.start(); specAnalyser = new SpecAnalyser(moduleNode, conEval); } else { specAnalyser = new SpecAnalyser(moduleNode); } specAnalyser.start(); TypeChecker typechecker = new TypeChecker(moduleNode, conEval, specAnalyser); typechecker.start(); specAnalyser.evalIfThenElse(); SymbolRenamer symRenamer = new SymbolRenamer(moduleNode, specAnalyser); symRenamer.start(); BMachinePrinter p = new BMachinePrinter(moduleNode, conEval, specAnalyser); bMachineString = p.start().toString(); BAstCreator bAstCreator = new BAstCreator(moduleNode, conEval, specAnalyser); this.bDefinitions = bAstCreator.getBDefinitions(); return bAstCreator.getStartNode(); } public static String evalFileName(String name) { if (name.toLowerCase().endsWith(".tla")) { name = name.substring(0, name.length() - 4); } if (name.toLowerCase().endsWith(".cfg")) { name = name.substring(0, name.length() - 4); } String sourceModuleName = name.substring(name .lastIndexOf(FileUtil.separator) + 1); String path = name.substring(0, name.lastIndexOf(FileUtil.separator) + 1); if (!path.equals("")) ToolIO.setUserDir(path); return sourceModuleName; } public Definitions getBDefinitions(){ return bDefinitions; } public String getBMachineString(){ return bMachineString; } }