Fix tests failing on too fast machines due to states folder conflicts

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);
 	}

src/test/java/de/tlc4b/util/TLC4BRunnerTestString.java

 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);
 	}
 }

src/test/java/de/tlc4b/util/TLC4BTester.java

 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);
 	}
 }