diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java index 28d3f9e637d645d5860b9394e3ccec42fa3b1535..6817f7107d220c52c9f6b2803a5ad86f4c496e1a 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 df9e4d620f4304d32a24cfd058a92e61485f1015..e1ff75d56932e5c2b3c34e46a7bfa7da31b94864 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 6d824ff568f4d7160d2a0443fb0db8e851dbd750..62bb3fad7f56e4de85a9e7013abe178c82b43238 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 1ba2fc635e07f0c731e788f538982fd2138a5f4a..40596ce62bf46f32ea3c96e9a04031c6b4d2367f 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 1a3b3e94e9baad9534a25dcc9f6307ef82c563d2..0000000000000000000000000000000000000000 --- 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 8ba2af500c87cede4ffc0bd9040d0dcc50222313..0000000000000000000000000000000000000000 --- 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