From 2a4bbd9d91f6f283c845ae1fa1050f820d2671d9 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Fri, 7 Nov 2014 12:00:50 +0100
Subject: [PATCH] Fixed bug: 'can not find config file'
---
src/main/java/de/tlc4b/TLC4B.java | 30 +++++++------------
src/main/java/de/tlc4b/TLCRunner.java | 7 ++---
src/main/java/de/tlc4b/tlc/TLCResults.java | 3 ++
src/test/java/testing/Testing2.java | 4 +--
.../EnumerationError/EnumerationError.cfg | 3 --
.../EnumerationError/EnumerationError.tla | 8 -----
6 files changed, 19 insertions(+), 36 deletions(-)
delete mode 100644 src/test/resources/errors/EnumerationError/EnumerationError.cfg
delete mode 100644 src/test/resources/errors/EnumerationError/EnumerationError.tla
diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index 28d3f9e..6817f71 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/src/main/java/de/tlc4b/TLC4B.java
@@ -23,9 +23,9 @@ public class TLC4B {
private String filename;
private File mainfile;
- private String machineFileNameWithoutFileExtension;
+ private String machineFileNameWithoutFileExtension;
// e.g. Test of file foo/bar/Test.mch
-
+
private File buildDir;
private String tlaModule;
@@ -55,8 +55,7 @@ public class TLC4B {
if (TLC4BGlobals.isRunTLC()) {
try {
TLCRunner.runTLC(tlc4b.machineFileNameWithoutFileExtension,
- tlc4b.mainfile.getParentFile());
-
+ tlc4b.buildDir);
TLCResults results = new TLCResults(tlc4b.tlcOutputInfo);
results.evalResults();
tlc4b.printResults(results, TLC4BGlobals.isCreateTraceFile());
@@ -89,7 +88,8 @@ public class TLC4B {
String trace = results.getTrace();
String tracefileName = machineFileNameWithoutFileExtension
+ ".tla.trace";
- File traceFile = createFile(mainfile.getParentFile(), tracefileName, trace, false);
+ File traceFile = createFile(mainfile.getParentFile(),
+ tracefileName, trace, false);
if (traceFile != null) {
System.out.println("Trace file '" + traceFile.getAbsolutePath()
+ "' created.");
@@ -113,17 +113,14 @@ public class TLC4B {
System.err.println(e.getMessage());
throw e;
}
- // System.out.println(tlc4b.tlaModule);
if (TLC4BGlobals.isRunTLC()) {
TLCRunner.runTLC(tlc4b.machineFileNameWithoutFileExtension,
tlc4b.buildDir);
TLCResults results = new TLCResults(tlc4b.tlcOutputInfo);
results.evalResults();
- // System.out.println("Result: " + results.getTLCResult());
tlc4b.printResults(results, false);
- // System.out.println(results.getTrace());
System.exit(0);
}
@@ -239,27 +236,22 @@ public class TLC4B {
throw new TLC4BIOException("The file '" + mainfile.getPath()
+ "' can not be accessed.");
}
-
-
machineFileNameWithoutFileExtension = mainfile.getName().substring(0,
mainfile.getName().length() - 4); // deleting .mch
-
-
if (buildDir == null) {
buildDir = new File(mainfile.getParentFile(),
machineFileNameWithoutFileExtension);
}
-
}
private void createFiles() {
- buildDir.mkdir();
- if(TLC4BGlobals.isDeleteOnExit()){
+ boolean dirCreated = buildDir.mkdir();
+ if (dirCreated && TLC4BGlobals.isDeleteOnExit()) {
buildDir.deleteOnExit();
}
-
+
File moduleFile = createFile(buildDir,
machineFileNameWithoutFileExtension + ".tla", tlaModule,
TLC4BGlobals.isDeleteOnExit());
@@ -391,9 +383,9 @@ public class TLC4B {
boolean deleteOnExit) {
File file = new File(dir, fileName);
-
+ boolean exists = false;
try {
- file.createNewFile();
+ exists = file.createNewFile();
BufferedWriter out = new BufferedWriter(new OutputStreamWriter(
new FileOutputStream(file), "UTF-8"));
out.write(text);
@@ -406,7 +398,7 @@ public class TLC4B {
} catch (IOException e) {
throw new TLC4BIOException(e.getMessage());
} finally {
- if (deleteOnExit && file.exists()) {
+ if (deleteOnExit && exists) {
file.deleteOnExit();
}
}
diff --git a/src/main/java/de/tlc4b/TLCRunner.java b/src/main/java/de/tlc4b/TLCRunner.java
index df9e4d6..e1ff75d 100644
--- a/src/main/java/de/tlc4b/TLCRunner.java
+++ b/src/main/java/de/tlc4b/TLCRunner.java
@@ -68,7 +68,6 @@ public class TLCRunner {
// list.add("1");
String[] args = list.toArray(new String[list.size()]);
- System.out.println("Starting JVM...");
final Process p = startJVM("", TLCRunner.class.getCanonicalName(), args);
StreamGobbler stdOut = new StreamGobbler(p.getInputStream());
stdOut.start();
@@ -97,12 +96,12 @@ public class TLCRunner {
list.add("" + TLC4BGlobals.getWorkers());
}
- list.add("-config");
- list.add(machineName + ".cfg");
+ //list.add("-config");
+ //list.add(machineName + ".cfg");
list.add(machineName);
+ System.out.println(path.getPath());
ToolIO.setUserDir(path.getPath());
String[] args = list.toArray(new String[list.size()]);
-
TLC tlc = new TLC();
// handle parameters
diff --git a/src/main/java/de/tlc4b/tlc/TLCResults.java b/src/main/java/de/tlc4b/tlc/TLCResults.java
index 6d824ff..62bb3fa 100644
--- a/src/main/java/de/tlc4b/tlc/TLCResults.java
+++ b/src/main/java/de/tlc4b/tlc/TLCResults.java
@@ -51,6 +51,9 @@ public class TLCResults {
}
public int getModelCheckingTime() {
+ if(endTime == null || startTime == null){
+ return -1;
+ }
return (int) (endTime.getTime() - startTime.getTime()) / 1000;
}
diff --git a/src/test/java/testing/Testing2.java b/src/test/java/testing/Testing2.java
index 1ba2fc6..40596ce 100644
--- a/src/test/java/testing/Testing2.java
+++ b/src/test/java/testing/Testing2.java
@@ -29,8 +29,8 @@ public class Testing2 extends AbstractParseMachineTest {
@Test
public void testRunTLC() throws Exception {
String[] a = new String[] { machine.getPath() };
- // TLC4B.main(a);
- TLC4B.test(a, false);
+ TLC4B.main(a);
+ //TLC4B.test(a, false);
// test(a);
}
diff --git a/src/test/resources/errors/EnumerationError/EnumerationError.cfg b/src/test/resources/errors/EnumerationError/EnumerationError.cfg
deleted file mode 100644
index 1a3b3e9..0000000
--- a/src/test/resources/errors/EnumerationError/EnumerationError.cfg
+++ /dev/null
@@ -1,3 +0,0 @@
-INIT Init
-NEXT Next
-INVARIANT Invariant1
diff --git a/src/test/resources/errors/EnumerationError/EnumerationError.tla b/src/test/resources/errors/EnumerationError/EnumerationError.tla
deleted file mode 100644
index 8ba2af5..0000000
--- a/src/test/resources/errors/EnumerationError/EnumerationError.tla
+++ /dev/null
@@ -1,8 +0,0 @@
----- MODULE EnumerationError ----
-EXTENDS Sequences
-VARIABLES x
-Invariant1 == x = <<1>>
-Init == x \in Seq({1}) /\ x \o x = <<1, 1>>
-
-Next == 1 = 2 /\ UNCHANGED <<x>>
-====
\ No newline at end of file
--
GitLab