diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java index 3457114309b4b670903a02d58fae52b03500fe58..5e7bda9720aeac1446ac72aab2a99820c913cdf0 100644 --- a/src/main/java/de/tlc4b/TLC4B.java +++ b/src/main/java/de/tlc4b/TLC4B.java @@ -84,7 +84,7 @@ public class TLC4B { TLCRunner.runTLC(tlc4b.machineFileNameWithoutFileExtension, tlc4b.buildDir); results = new TLCResults(tlc4b.tlcOutputInfo); results.evalResults(); - tlc4b.printResults(results, TLC4BGlobals.isCreateTraceFile()); + tlc4b.printResults(results); Log log = new Log(tlc4b, results); tlc4b.createLogFile(log); } catch (NoClassDefFoundError e) { @@ -121,7 +121,7 @@ public class TLC4B { } } - private void printResults(TLCResults results, boolean createTraceFile) { + private void printResults(TLCResults results) { printOperationsCount(results); // options printlnSilent("Used Options"); @@ -159,7 +159,8 @@ public class TLC4B { println("Violated Definition: " + violatedDefinition); } - if (results.hasTrace() && createTraceFile) { + System.out.println(TLC4BGlobals.isCreateTraceFile()); + if (results.hasTrace() && TLC4BGlobals.isCreateTraceFile()) { String trace = results.getTrace(); String tracefileName = machineFileNameWithoutFileExtension + ".tla.trace"; traceFile = createFile(buildDir, tracefileName, trace, TLC4BGlobals.isDeleteOnExit()); @@ -189,7 +190,6 @@ public class TLC4B { System.setProperty("apple.awt.UIElement", "true"); // avoiding pop up windows TLC4BGlobals.resetGlobals(); TLC4BGlobals.setDeleteOnExit(deleteFiles); - TLC4BGlobals.setCreateTraceFile(false); TLC4BGlobals.setTestingMode(true); // B2TLAGlobals.setCleanup(true); TLC4B tlc4b = new TLC4B(); @@ -206,7 +206,9 @@ public class TLC4B { MP.TLCOutputStream.resetOutputStream(); TLCResults results = new TLCResults(tlc4b.tlcOutputInfo); results.evalResults(); - tlc4b.printResults(results, false); + tlc4b.printResults(results); + Log log = new Log(tlc4b, results); + tlc4b.createLogFile(log); System.exit(0); } @@ -216,7 +218,6 @@ public class TLC4B { System.setProperty("apple.awt.UIElement", "true"); // avoiding pop up windows TLC4BGlobals.resetGlobals(); TLC4BGlobals.setDeleteOnExit(deleteFiles); - TLC4BGlobals.setCreateTraceFile(false); TLC4BGlobals.setTestingMode(true); // B2TLAGlobals.setCleanup(true); TLC4B tlc4b = new TLC4B(); @@ -246,7 +247,7 @@ public class TLC4B { MP.TLCOutputStream.resetOutputStream(); TLCResults results = new TLCResults(tlc4b.tlcOutputInfo); results.evalResults(); - tlc4b.printResults(results, false); + tlc4b.printResults(results); System.exit(0); } } diff --git a/src/test/java/de/tlc4b/tlc/integration/SpecialTest.java b/src/test/java/de/tlc4b/tlc/integration/SpecialTest.java index 861802e26b4248044875de4a462e5286a7c28f03..545e7f8d45042b63c500e85aaf417ef9369f74bd 100644 --- a/src/test/java/de/tlc4b/tlc/integration/SpecialTest.java +++ b/src/test/java/de/tlc4b/tlc/integration/SpecialTest.java @@ -1,6 +1,6 @@ package de.tlc4b.tlc.integration; -import static de.tlc4b.TLC4BCliOptions.TLCOption.OUTPUT; +import static de.tlc4b.TLC4BCliOptions.TLCOption.*; import static de.tlc4b.tlc.TLCResults.TLCResult.*; import static de.tlc4b.util.TestUtil.test; import static org.junit.Assert.*; @@ -10,6 +10,7 @@ import org.junit.Test; import java.nio.file.Files; import java.nio.file.Path; import java.nio.file.Paths; +import java.util.List; public class SpecialTest { @@ -64,11 +65,41 @@ public class SpecialTest { public void testCustomOutputDir() throws Exception { Path specialDir = Paths.get("./src/test/resources/special/veryspecialoutput"); String[] a = new String[] { "./src/test/resources/errors/InvariantError.mch", OUTPUT.cliArg(), specialDir.toString()}; - assertEquals(InvariantViolation, test(a)); + assertEquals(InvariantViolation, test(a, true)); assertTrue(Files.deleteIfExists(specialDir.resolve("InvariantError.tla"))); assertTrue(Files.deleteIfExists(specialDir.resolve("InvariantError.cfg"))); + assertTrue(Files.deleteIfExists(specialDir.resolve("InvariantError.tla.trace"))); assertTrue(Files.deleteIfExists(specialDir)); } + + @Test + public void testLogFile() throws Exception { + Path logFile = Paths.get("./src/test/resources/special/log.csv"); + Path machineFile = Paths.get("./src/test/resources/special/SimpleForLog.mch"); + Path tracePath = Paths.get("./src/test/resources/special/SimpleForLog/SimpleForLog.tla.trace"); + logFile.toFile().delete(); + + String[] a = new String[] { machineFile.toString(), LOG.cliArg(), logFile.toString(), COVERAGE.cliArg()}; + assertEquals(InvariantViolation, test(a, true)); + + List<String> lines = Files.readAllLines(logFile); + assertEquals(lines.size(), 12); + assertEquals(lines.get(0), "Machine File;" + machineFile.toRealPath()); + assertTrue(lines.get(1).startsWith("TLC Model Checking Time (s);")); + assertTrue(lines.get(2).startsWith("Parsing Time Of B machine (ms);")); + assertTrue(lines.get(3).startsWith("Translation Time (ms);")); + assertTrue(lines.get(4).startsWith("Model Checking Time (ms);")); + assertEquals(lines.get(5), "TLC Result;Invariant Violation"); + assertEquals(lines.get(6), "States analysed;5"); + assertEquals(lines.get(7), "Transitions fired;5"); + assertEquals(lines.get(8), "Violated Definition;Invariant1"); + assertEquals(lines.get(9), "Violated Assertions;"); + assertEquals(lines.get(10), "Operation Coverage;inc;8"); + assertEquals(lines.get(11), "Trace File;" + tracePath.toRealPath()); + + assertTrue(Files.deleteIfExists(tracePath)); + assertTrue(Files.deleteIfExists(logFile)); + } } diff --git a/src/test/java/de/tlc4b/util/TestUtil.java b/src/test/java/de/tlc4b/util/TestUtil.java index d14379f7c65b53cfb5e1a45bf6a0d7574bed3818..0b4aa3b582ecf9954cc218a86507c1f8f4647f5b 100644 --- a/src/test/java/de/tlc4b/util/TestUtil.java +++ b/src/test/java/de/tlc4b/util/TestUtil.java @@ -22,6 +22,7 @@ import de.tlc4b.tlc.TLCResults.TLCResult; import util.ToolIO; +import static de.tlc4b.TLC4BCliOptions.TLCOption.NOTRACE; import static org.junit.Assert.assertEquals; public class TestUtil { @@ -151,8 +152,19 @@ public class TestUtil { } public static TLCResult test(String[] args) throws IOException { + return test(args, false); + } + + public static TLCResult test(String[] args, boolean createTrace) throws IOException { String runnerClassName = TLC4BTester.class.getCanonicalName(); - return runTLC(runnerClassName, args); + String[] newArgs; + if (createTrace) { + newArgs = args; + } else { + newArgs = Arrays.copyOf(args, args.length + 1); + newArgs[args.length] = NOTRACE.cliArg(); + } + return runTLC(runnerClassName, newArgs); } private static TLCResult runTLC(String runnerClassName, String[] args) throws IOException { diff --git a/src/test/resources/special/SimpleForLog.mch b/src/test/resources/special/SimpleForLog.mch new file mode 100644 index 0000000000000000000000000000000000000000..e285feed38af3ce28b5f375f38133896922f1816 --- /dev/null +++ b/src/test/resources/special/SimpleForLog.mch @@ -0,0 +1,6 @@ +MACHINE SimpleForLog +VARIABLES i +INVARIANT i : 1..4 +INITIALISATION i := 1 +OPERATIONS inc = PRE i < 5 THEN i := succ(i) END +END \ No newline at end of file