Skip to content
Snippets Groups Projects
Commit badde011 authored by Jan Gruteser's avatar Jan Gruteser
Browse files

add simple log file test

parent 86f77dac
No related branches found
No related tags found
No related merge requests found
Pipeline #139909 passed
......@@ -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);
}
}
......
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));
}
}
......@@ -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 {
......
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
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment