From 8ff008748adbf969b7fc3cc0b0fcb550d9a17f28 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Wed, 26 Apr 2023 22:42:40 +0200
Subject: [PATCH] Fix tests failing on too fast machines due to states folder
conflicts
---
src/test/java/de/tlc4b/coverage/CoverageTest.java | 14 +++++++++++---
.../java/de/tlc4b/util/TLC4BRunnerTestString.java | 11 +++++++++++
src/test/java/de/tlc4b/util/TLC4BTester.java | 10 ++++++++++
3 files changed, 32 insertions(+), 3 deletions(-)
diff --git a/src/test/java/de/tlc4b/coverage/CoverageTest.java b/src/test/java/de/tlc4b/coverage/CoverageTest.java
index f5d7ca5..11f0ab2 100644
--- a/src/test/java/de/tlc4b/coverage/CoverageTest.java
+++ b/src/test/java/de/tlc4b/coverage/CoverageTest.java
@@ -3,9 +3,6 @@ package de.tlc4b.coverage;
import java.io.File;
import java.util.ArrayList;
-import org.junit.Test;
-import org.junit.runner.RunWith;
-
import de.tlc4b.TLC4B;
import de.tlc4b.tlc.TLCResults.TLCResult;
import de.tlc4b.util.AbstractParseMachineTest;
@@ -13,6 +10,11 @@ import de.tlc4b.util.PolySuite;
import de.tlc4b.util.PolySuite.Config;
import de.tlc4b.util.PolySuite.Configuration;
+import org.junit.Test;
+import org.junit.runner.RunWith;
+
+import tlc2.TLCGlobals;
+
@RunWith(PolySuite.class)
public class CoverageTest extends AbstractParseMachineTest {
@@ -24,6 +26,12 @@ public class CoverageTest extends AbstractParseMachineTest {
@Test
public void testRunTLC() throws Exception {
+ // The subdirectories of the states directory are named after the time when TLC was started.
+ // Old versions of TLC (like the one we use) format the time with second precision only,
+ // leading to name conflicts when two tests are started within the same second.
+ // This line works around the issue by instead using a millisecond timestamp as the name.
+ TLCGlobals.metaDir = TLCGlobals.metaRoot + File.separator + System.currentTimeMillis() + File.separator;
+
String[] a = new String[] { machine.getPath(), "-notlc" };
TLC4B.test(a, true);
}
diff --git a/src/test/java/de/tlc4b/util/TLC4BRunnerTestString.java b/src/test/java/de/tlc4b/util/TLC4BRunnerTestString.java
index 477da9d..a59e221 100644
--- a/src/test/java/de/tlc4b/util/TLC4BRunnerTestString.java
+++ b/src/test/java/de/tlc4b/util/TLC4BRunnerTestString.java
@@ -1,11 +1,22 @@
package de.tlc4b.util;
+import java.io.File;
+
import de.tlc4b.TLC4B;
+import tlc2.TLCGlobals;
+
public class TLC4BRunnerTestString {
public static void main(String[] args) throws Exception {
System.setProperty("apple.awt.UIElement", "true"); // avoiding pop up windows
+
+ // The subdirectories of the states directory are named after the time when TLC was started.
+ // Old versions of TLC (like the one we use) format the time with second precision only,
+ // leading to name conflicts when two tests are started within the same second.
+ // This line works around the issue by instead using a millisecond timestamp as the name.
+ TLCGlobals.metaDir = TLCGlobals.metaRoot + File.separator + System.currentTimeMillis() + File.separator;
+
TLC4B.testString(args[0],true);
}
}
diff --git a/src/test/java/de/tlc4b/util/TLC4BTester.java b/src/test/java/de/tlc4b/util/TLC4BTester.java
index f685baa..a695a51 100644
--- a/src/test/java/de/tlc4b/util/TLC4BTester.java
+++ b/src/test/java/de/tlc4b/util/TLC4BTester.java
@@ -1,11 +1,21 @@
package de.tlc4b.util;
+import java.io.File;
import de.tlc4b.TLC4B;
+import tlc2.TLCGlobals;
+
public class TLC4BTester {
public static void main(String[] args) throws Exception {
System.setProperty("apple.awt.UIElement", "true"); // avoiding pop up windows
+
+ // The subdirectories of the states directory are named after the time when TLC was started.
+ // Old versions of TLC (like the one we use) format the time with second precision only,
+ // leading to name conflicts when two tests are started within the same second.
+ // This line works around the issue by instead using a millisecond timestamp as the name.
+ TLCGlobals.metaDir = TLCGlobals.metaRoot + File.separator + System.currentTimeMillis() + File.separator;
+
TLC4B.test(args,true);
}
}
--
GitLab