diff --git a/build.gradle b/build.gradle
index 0ab2cb8b7d47027e22faca02dadef2efc6e64579..49a23748ca2357026196fcb476ca755f7a2983e9 100644
--- a/build.gradle
+++ b/build.gradle
@@ -4,7 +4,7 @@ apply plugin: 'maven'
apply plugin: 'jacoco'
//apply plugin: 'findbugs'
-project.version = '1.0.1-SNAPSHOT'
+project.version = '1.0.3-SNAPSHOT'
project.group = 'de.prob'
sourceCompatibility = 1.5
diff --git a/src/main/java/de/tla2bAst/SimpleResolver.java b/src/main/java/de/tla2bAst/SimpleResolver.java
new file mode 100644
index 0000000000000000000000000000000000000000..8ffd983b673aa3ee133b1a7a48875bc8ee9a65e6
--- /dev/null
+++ b/src/main/java/de/tla2bAst/SimpleResolver.java
@@ -0,0 +1,19 @@
+package de.tla2bAst;
+
+import java.io.File;
+
+import util.FilenameToStream;
+
+public class SimpleResolver implements FilenameToStream {
+
+ public boolean isStandardModule(String arg0) {
+ return false;
+ }
+
+ public File resolve(String arg0, boolean arg1) {
+
+ File file = new File(arg0);
+ return file;
+ }
+
+}
\ No newline at end of file
diff --git a/src/main/java/de/tla2bAst/TLAParser.java b/src/main/java/de/tla2bAst/TLAParser.java
deleted file mode 100644
index c67d9b7fafa532114260b07c6fb7725afdd8ba74..0000000000000000000000000000000000000000
--- a/src/main/java/de/tla2bAst/TLAParser.java
+++ /dev/null
@@ -1,62 +0,0 @@
-package de.tla2bAst;
-
-import tla2sany.drivers.FrontEndException;
-import tla2sany.drivers.SANY;
-import tla2sany.modanalyzer.SpecObj;
-import tla2sany.semantic.ModuleNode;
-import util.FilenameToStream;
-import util.ToolIO;
-
-public class TLAParser {
-
- private FilenameToStream filenameToStream;
-
- public TLAParser(FilenameToStream filenameToStream) {
- this.filenameToStream = filenameToStream;
- }
-
- public ModuleNode parseModule(String moduleName) throws de.tla2b.exceptions.FrontEndException {
- SpecObj spec = new SpecObj(moduleName, filenameToStream);
- try {
- SANY.frontEndMain(spec, moduleName, ToolIO.out);
- } catch (FrontEndException e) {
- // Error in Frontend, should never happens
- return null;
- }
-
- if (spec.parseErrors.isFailure()) {
- throw new de.tla2b.exceptions.FrontEndException(
- allMessagesToString(ToolIO.getAllMessages())
- + spec.parseErrors, spec);
- }
-
- if (spec.semanticErrors.isFailure()) {
- throw new de.tla2b.exceptions.FrontEndException(
- // allMessagesToString(ToolIO.getAllMessages())
- "" + spec.semanticErrors, spec);
- }
-
- // RootModule
- ModuleNode n = spec.getExternalModuleTable().rootModule;
- if (spec.getInitErrors().isFailure()) {
- System.err.println(spec.getInitErrors());
- return null;
- }
-
- if (n == null) { // Parse Error
- // System.out.println("Rootmodule null");
- throw new de.tla2b.exceptions.FrontEndException(
- allMessagesToString(ToolIO.getAllMessages()), spec);
- }
-
- return n;
- }
-
- public static String allMessagesToString(String[] allMessages) {
- StringBuilder sb = new StringBuilder();
- for (int i = 0; i < allMessages.length - 1; i++) {
- sb.append(allMessages[i] + "\n");
- }
- return sb.toString();
- }
-}
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index 1ffbcc86cbe02883960b83e5729a2ea324099289..2e98e1336292367aeede118615532ddab7e1d4c6 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -18,124 +18,146 @@ import de.tla2b.config.ModuleOverrider;
import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
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 {
private String moduleFileName;
- private String configFileName;
+ private File moduleFile;
+ private File configFile;
private Definitions bDefinitions;
- private String moduleName;
+ // private String moduleName;
private ModuleNode moduleNode;
private ModelConfig modelConfig;
private String bMachineString;
- public Translator(String moduleFileName, String configFileName)
- throws FrontEndException {
+ public Translator(String moduleFileName) throws FrontEndException {
this.moduleFileName = moduleFileName;
- this.configFileName = configFileName;
+
+ findModuleFile();
+ findConfigFile();
parse();
}
+ private void findConfigFile() {
+ String configFileName = removeExtention(moduleFile.getAbsolutePath());
+ configFileName = configFileName + ".cfg";
+ configFile = new File(configFileName);
+ if (!configFile.exists()) {
+ configFile = null;
+ }
+ }
+
+ private void findModuleFile() {
+ moduleFile = new File(moduleFileName);
+ if (!moduleFile.exists()) {
+ throw new RuntimeException("Can not find module file: '"
+ + moduleFileName + "'");
+ }
+ }
+
// Used for Testing
- public Translator(String moduleString, String configString, int i)
+ public Translator(String moduleString, String configString)
throws FrontEndException {
- moduleName = "Testing";
+ String moduleName = "Testing";
File dir = new File("temp/");
dir.mkdirs();
try {
- File f = new File("temp/" + moduleName + ".tla");
- f.createNewFile();
- FileWriter fw = new FileWriter(f);
+ moduleFile = new File("temp/" + moduleName + ".tla");
+ moduleFile.createNewFile();
+ FileWriter fw = new FileWriter(moduleFile);
fw.write(moduleString);
fw.close();
// f.deleteOnExit();
- moduleFileName = f.getAbsolutePath();
+ moduleFileName = moduleFile.getAbsolutePath();
} catch (IOException e) {
e.printStackTrace();
}
- modelConfig = null;
if (configString != null) {
- File f = new File("temp/" + moduleName + ".cfg");
-
+ configFile = new File("temp/" + moduleName + ".cfg");
try {
- f.createNewFile();
- FileWriter fw = new FileWriter(f);
+ configFile.createNewFile();
+ FileWriter fw = new FileWriter(configFile);
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();
+ public ModuleNode parseModule2()
+ throws de.tla2b.exceptions.FrontEndException {
+ String fileName = moduleFile.getName();
+ ToolIO.setUserDir(moduleFile.getParent());
+ SpecObj spec = new SpecObj(fileName, null);
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) {
+ SANY.frontEndMain(spec, fileName, ToolIO.out);
+ } catch (tla2sany.drivers.FrontEndException e) {
+ // should never happen
e.printStackTrace();
}
- parseModule();
- }
+ if (spec.parseErrors.isFailure()) {
+ throw new de.tla2b.exceptions.FrontEndException(
+ allMessagesToString(ToolIO.getAllMessages())
+ + spec.parseErrors, spec);
+ }
- private void parseModule() throws FrontEndException {
- moduleName = evalFileName(moduleFileName);
+ if (spec.semanticErrors.isFailure()) {
+ throw new de.tla2b.exceptions.FrontEndException(
+ // allMessagesToString(ToolIO.getAllMessages())
+ "" + spec.semanticErrors, spec);
+ }
+
+ // RootModule
+ ModuleNode n = spec.getExternalModuleTable().rootModule;
+ if (spec.getInitErrors().isFailure()) {
+ System.err.println(spec.getInitErrors());
+ return null;
+ }
+
+ if (n == null) { // Parse Error
+ // System.out.println("Rootmodule null");
+ throw new de.tla2b.exceptions.FrontEndException(
+ allMessagesToString(ToolIO.getAllMessages()), spec);
+ }
- TLAParser tlaParser = new TLAParser(null);
- moduleNode = tlaParser.parseModule(moduleName);
+ return n;
}
- private void parse() throws FrontEndException {
- moduleName = evalFileName(moduleFileName);
+ public static String allMessagesToString(String[] allMessages) {
+ StringBuilder sb = new StringBuilder();
+ for (int i = 0; i < allMessages.length - 1; i++) {
+ sb.append(allMessages[i] + "\n");
+ }
+ return sb.toString();
+ }
- TLAParser tlaParser = new TLAParser(null);
- moduleNode = tlaParser.parseModule(moduleName);
+ private void parse() throws FrontEndException {
+ moduleNode = parseModule2();
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();
- }
+ if (configFile != null) {
+ modelConfig = new ModelConfig(configFile.getAbsolutePath(),
+ new SimpleResolver());
+ modelConfig.parse();
}
+
}
public Start translate() throws TLA2BException {
@@ -188,23 +210,27 @@ public class Translator {
return bAstCreator.getStartNode();
}
- public static String evalFileName(String name) {
- if (name.toLowerCase().endsWith(".tla")) {
- name = name.substring(0, name.length() - 4);
- }
+ public static String removeExtention(String filePath) {
+ File f = new File(filePath);
- if (name.toLowerCase().endsWith(".cfg")) {
- name = name.substring(0, name.length() - 4);
- }
+ // if it's a directory, don't remove the extention
+ if (f.isDirectory())
+ return filePath;
- String sourceModuleName = name.substring(name
- .lastIndexOf(FileUtil.separator) + 1);
+ String name = f.getName();
- String path = name.substring(0,
- name.lastIndexOf(FileUtil.separator) + 1);
- if (!path.equals(""))
- ToolIO.setUserDir(path);
- return sourceModuleName;
+ // Now we know it's a file - don't need to do any special hidden
+ // checking or contains() checking because of:
+ final int lastPeriodPos = name.lastIndexOf('.');
+ if (lastPeriodPos <= 0) {
+ // No period after first character - return name as it was passed in
+ return filePath;
+ } else {
+ // Remove the last period and everything after it
+ File renamed = new File(f.getParent(), name.substring(0,
+ lastPeriodPos));
+ return renamed.getPath();
+ }
}
public Definitions getBDefinitions() {
diff --git a/src/test/java/de/tla2b/util/TestUtil.java b/src/test/java/de/tla2b/util/TestUtil.java
index ff154ba5698e5fb25653db4654616fa40630398f..278f62905caefeb65867fb1f5deaf1035c47eda4 100644
--- a/src/test/java/de/tla2b/util/TestUtil.java
+++ b/src/test/java/de/tla2b/util/TestUtil.java
@@ -35,7 +35,7 @@ public class TestUtil {
}
public static void runModule(String tlaFile) throws Exception{
- Translator t = new Translator(tlaFile, null);
+ Translator t = new Translator(tlaFile);
Start start = t.translate();
System.out.println(t.getBMachineString());
System.out.println("---------------------");
@@ -72,7 +72,7 @@ public class TestUtil {
String expected = getAstStringofBMachineString(bMachine);
System.out.println(expected);
- Translator trans = new Translator(tlaModule);
+ Translator trans = new Translator(tlaModule, null);
Start resultNode = trans.translate();
String result = getTreeAsString(resultNode);
System.out.println(result);
@@ -111,7 +111,7 @@ public class TestUtil {
String expected = getAstStringofBMachineString(bMachine);
System.out.println(expected);
- Translator trans = new Translator(tlaModule, config, 1);
+ Translator trans = new Translator(tlaModule, config);
Start resultNode = trans.translate();
//BParser.printASTasProlog(System.out, new BParser(), new File("./test.mch"), resultNode, false, true, null);