diff --git a/src/test/java/de/tlc4b/coverage/CoverageTest.java b/src/test/java/de/tlc4b/coverage/CoverageTest.java index f5d7ca539988f540f5d0d07506970b49e8767ce2..11f0ab23eb5318201c2d764c87c28944e35d6c8c 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 477da9de6eb72e470e6ca7396ec1eff2ce7b6519..a59e2217320786428d618bcaa75d8398c86113b0 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 f685baa9d2d638f13a6411f199192e1d890e843a..a695a5160271c084d409d645a240a13a93699dcc 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); } }