From b6a9820e27eede7e38c6801e07a54f1e224eeba0 Mon Sep 17 00:00:00 2001 From: dgelessus <dgelessus@users.noreply.github.com> Date: Tue, 30 Jul 2024 19:42:15 +0200 Subject: [PATCH] Replace PolySuite with standard JUnit Parameterized runner --- .../de/tlc4b/tlc/integration/BasicTest.java | 37 ++--- .../probprivate/AssertionErrorTest.java | 28 ++-- .../integration/probprivate/CoverageTest.java | 37 ++--- .../integration/probprivate/DeadlockTest.java | 28 ++-- .../tlc/integration/probprivate/GoalTest.java | 28 ++-- .../probprivate/InvariantViolationTest.java | 28 ++-- .../integration/probprivate/NoErrorTest.java | 29 ++-- .../probprivate/WellDefinednessTest.java | 27 ++-- .../tlc4b/util/AbstractParseMachineTest.java | 64 -------- src/test/java/de/tlc4b/util/PolySuite.java | 140 ------------------ 10 files changed, 86 insertions(+), 360 deletions(-) delete mode 100644 src/test/java/de/tlc4b/util/AbstractParseMachineTest.java delete mode 100644 src/test/java/de/tlc4b/util/PolySuite.java diff --git a/src/test/java/de/tlc4b/tlc/integration/BasicTest.java b/src/test/java/de/tlc4b/tlc/integration/BasicTest.java index 556c0ec..b61ef90 100644 --- a/src/test/java/de/tlc4b/tlc/integration/BasicTest.java +++ b/src/test/java/de/tlc4b/tlc/integration/BasicTest.java @@ -2,52 +2,47 @@ package de.tlc4b.tlc.integration; import java.io.File; import java.util.ArrayList; +import java.util.Arrays; import java.util.List; import de.tlc4b.tlc.TLCResults.TLCResult; -import de.tlc4b.util.AbstractParseMachineTest; -import de.tlc4b.util.PolySuite; -import de.tlc4b.util.PolySuite.Config; -import de.tlc4b.util.PolySuite.Configuration; +import de.tlc4b.util.TestUtil; import org.junit.Test; import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; import static de.tlc4b.TLC4BOption.DFID; -import static de.tlc4b.tlc.TLCResults.TLCResult.NoError; import static de.tlc4b.util.TestUtil.test; import static org.junit.Assert.assertEquals; -@RunWith(PolySuite.class) -public class BasicTest extends AbstractParseMachineTest { - +@RunWith(Parameterized.class) +public class BasicTest { private final File machine; - private final TLCResult error; - public BasicTest(File machine, TLCResult result) { + public BasicTest(File machine) { this.machine = machine; - this.error = result; } @Test public void testRunTLC() throws Exception { String[] a = new String[] { machine.getPath() }; - assertEquals(error, test(a)); + assertEquals(TLCResult.NoError, test(a)); } @Test public void testRunTLCDFS() throws Exception { String[] a = new String[] { machine.getPath(), DFID.cliArg(), "20" }; - assertEquals(error, test(a)); + assertEquals(TLCResult.NoError, test(a)); } - @Config - public static Configuration getConfig() { - List<String> list = new ArrayList<>(); - list.add("./src/test/resources/composition/sees"); - list.add("./src/test/resources/composition/sees2"); - list.add("./src/test/resources/basics"); - list.add("./src/test/resources/laws"); - return getConfiguration(list, NoError); + @Parameterized.Parameters(name = "{0}") + public static List<File> data() { + List<File> machines = new ArrayList<>(); + machines.addAll(Arrays.asList(TestUtil.getMachines("./src/test/resources/composition/sees"))); + machines.addAll(Arrays.asList(TestUtil.getMachines("./src/test/resources/composition/sees2"))); + machines.addAll(Arrays.asList(TestUtil.getMachines("./src/test/resources/basics"))); + machines.addAll(Arrays.asList(TestUtil.getMachines("./src/test/resources/laws"))); + return machines; } } diff --git a/src/test/java/de/tlc4b/tlc/integration/probprivate/AssertionErrorTest.java b/src/test/java/de/tlc4b/tlc/integration/probprivate/AssertionErrorTest.java index ee6c53e..f3f341c 100644 --- a/src/test/java/de/tlc4b/tlc/integration/probprivate/AssertionErrorTest.java +++ b/src/test/java/de/tlc4b/tlc/integration/probprivate/AssertionErrorTest.java @@ -1,43 +1,33 @@ package de.tlc4b.tlc.integration.probprivate; import java.io.File; -import java.util.ArrayList; -import java.util.List; import de.tlc4b.tlc.TLCResults.TLCResult; -import de.tlc4b.util.AbstractParseMachineTest; -import de.tlc4b.util.PolySuite; -import de.tlc4b.util.PolySuite.Config; -import de.tlc4b.util.PolySuite.Configuration; +import de.tlc4b.util.TestUtil; import org.junit.Test; import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; -import static de.tlc4b.tlc.TLCResults.TLCResult.AssertionError; import static de.tlc4b.util.TestUtil.test; import static org.junit.Assert.assertEquals; -@RunWith(PolySuite.class) -public class AssertionErrorTest extends AbstractParseMachineTest { - +@RunWith(Parameterized.class) +public class AssertionErrorTest { private final File machine; - private final TLCResult error; - public AssertionErrorTest(File machine, TLCResult result) { + public AssertionErrorTest(File machine) { this.machine = machine; - this.error = result; } @Test public void testRunTLC() throws Exception { String[] a = new String[] { machine.getPath() }; - assertEquals(error, test(a)); + assertEquals(TLCResult.AssertionError, test(a)); } - @Config - public static Configuration getConfig() { - List<String> list = new ArrayList<>(); - list.add("build/prob_examples/public_examples/TLC/AssertionError"); - return getConfiguration(list, AssertionError); + @Parameterized.Parameters(name = "{0}") + public static File[] data() { + return TestUtil.getMachines("build/prob_examples/public_examples/TLC/AssertionError"); } } diff --git a/src/test/java/de/tlc4b/tlc/integration/probprivate/CoverageTest.java b/src/test/java/de/tlc4b/tlc/integration/probprivate/CoverageTest.java index 8b7b3f0..98be04c 100644 --- a/src/test/java/de/tlc4b/tlc/integration/probprivate/CoverageTest.java +++ b/src/test/java/de/tlc4b/tlc/integration/probprivate/CoverageTest.java @@ -5,23 +5,19 @@ import java.util.ArrayList; import java.util.List; import de.tlc4b.TLC4B; -import de.tlc4b.tlc.TLCResults.TLCResult; -import de.tlc4b.util.AbstractParseMachineTest; -import de.tlc4b.util.PolySuite; -import de.tlc4b.util.PolySuite.Config; -import de.tlc4b.util.PolySuite.Configuration; +import de.tlc4b.util.TestUtil; import org.junit.Test; import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; import tlc2.TLCGlobals; -@RunWith(PolySuite.class) -public class CoverageTest extends AbstractParseMachineTest { - +@RunWith(Parameterized.class) +public class CoverageTest { private final File machine; - public CoverageTest(File machine, TLCResult result) { + public CoverageTest(File machine) { this.machine = machine; } @@ -37,18 +33,17 @@ public class CoverageTest extends AbstractParseMachineTest { TLC4B.test(a, true); } - @Config - public static Configuration getConfig() { - List<String> list = new ArrayList<>(); - list.add("build/prob_examples/public_examples/TLC/"); + @Parameterized.Parameters(name = "{0}") + public static List<File> data() { + List<File> machines = new ArrayList<>(); + machines.addAll(TestUtil.getMachinesRecursively("build/prob_examples/public_examples/TLC/")); // The subdirectories bugs, compound, and test are intentionally not included here. - list.add("src/test/resources/basics/"); - list.add("src/test/resources/composition/"); - list.add("src/test/resources/errors/"); - list.add("src/test/resources/laws/"); - list.add("src/test/resources/ltl/"); - list.add("src/test/resources/special/"); - return getConfiguration2(list); + machines.addAll(TestUtil.getMachinesRecursively("src/test/resources/basics/")); + machines.addAll(TestUtil.getMachinesRecursively("src/test/resources/composition/")); + machines.addAll(TestUtil.getMachinesRecursively("src/test/resources/errors/")); + machines.addAll(TestUtil.getMachinesRecursively("src/test/resources/laws/")); + machines.addAll(TestUtil.getMachinesRecursively("src/test/resources/ltl/")); + machines.addAll(TestUtil.getMachinesRecursively("src/test/resources/special/")); + return machines; } - } diff --git a/src/test/java/de/tlc4b/tlc/integration/probprivate/DeadlockTest.java b/src/test/java/de/tlc4b/tlc/integration/probprivate/DeadlockTest.java index b2a84f9..23dd45b 100644 --- a/src/test/java/de/tlc4b/tlc/integration/probprivate/DeadlockTest.java +++ b/src/test/java/de/tlc4b/tlc/integration/probprivate/DeadlockTest.java @@ -1,43 +1,33 @@ package de.tlc4b.tlc.integration.probprivate; import java.io.File; -import java.util.ArrayList; -import java.util.List; import de.tlc4b.tlc.TLCResults.TLCResult; -import de.tlc4b.util.AbstractParseMachineTest; -import de.tlc4b.util.PolySuite; -import de.tlc4b.util.PolySuite.Config; -import de.tlc4b.util.PolySuite.Configuration; +import de.tlc4b.util.TestUtil; import org.junit.Test; import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; -import static de.tlc4b.tlc.TLCResults.TLCResult.Deadlock; import static de.tlc4b.util.TestUtil.test; import static org.junit.Assert.assertEquals; -@RunWith(PolySuite.class) -public class DeadlockTest extends AbstractParseMachineTest { - +@RunWith(Parameterized.class) +public class DeadlockTest { private final File machine; - private final TLCResult error; - public DeadlockTest(File machine, TLCResult result) { + public DeadlockTest(File machine) { this.machine = machine; - this.error = result; } @Test public void testRunTLC() throws Exception { String[] a = new String[] { machine.getPath() }; - assertEquals(error, test(a)); + assertEquals(TLCResult.Deadlock, test(a)); } - @Config - public static Configuration getConfig() { - List<String> list = new ArrayList<>(); - list.add("build/prob_examples/public_examples/TLC/Deadlock"); - return getConfiguration(list, Deadlock); + @Parameterized.Parameters(name = "{0}") + public static File[] data() { + return TestUtil.getMachines("build/prob_examples/public_examples/TLC/Deadlock"); } } diff --git a/src/test/java/de/tlc4b/tlc/integration/probprivate/GoalTest.java b/src/test/java/de/tlc4b/tlc/integration/probprivate/GoalTest.java index 937f228..509beb4 100644 --- a/src/test/java/de/tlc4b/tlc/integration/probprivate/GoalTest.java +++ b/src/test/java/de/tlc4b/tlc/integration/probprivate/GoalTest.java @@ -1,43 +1,33 @@ package de.tlc4b.tlc.integration.probprivate; import java.io.File; -import java.util.ArrayList; -import java.util.List; import de.tlc4b.tlc.TLCResults.TLCResult; -import de.tlc4b.util.AbstractParseMachineTest; -import de.tlc4b.util.PolySuite; -import de.tlc4b.util.PolySuite.Config; -import de.tlc4b.util.PolySuite.Configuration; +import de.tlc4b.util.TestUtil; import org.junit.Test; import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; -import static de.tlc4b.tlc.TLCResults.TLCResult.Goal; import static de.tlc4b.util.TestUtil.test; import static org.junit.Assert.assertEquals; -@RunWith(PolySuite.class) -public class GoalTest extends AbstractParseMachineTest { - +@RunWith(Parameterized.class) +public class GoalTest { private final File machine; - private final TLCResult error; - public GoalTest(File machine, TLCResult result) { + public GoalTest(File machine) { this.machine = machine; - this.error = result; } @Test public void testRunTLC() throws Exception { String[] a = new String[] { machine.getPath() }; - assertEquals(error, test(a)); + assertEquals(TLCResult.Goal, test(a)); } - @Config - public static Configuration getConfig() { - List<String> list = new ArrayList<>(); - list.add("build/prob_examples/public_examples/TLC/GOAL"); - return getConfiguration(list, Goal); + @Parameterized.Parameters(name = "{0}") + public static File[] data() { + return TestUtil.getMachines("build/prob_examples/public_examples/TLC/GOAL"); } } diff --git a/src/test/java/de/tlc4b/tlc/integration/probprivate/InvariantViolationTest.java b/src/test/java/de/tlc4b/tlc/integration/probprivate/InvariantViolationTest.java index 27990f0..c83ca85 100644 --- a/src/test/java/de/tlc4b/tlc/integration/probprivate/InvariantViolationTest.java +++ b/src/test/java/de/tlc4b/tlc/integration/probprivate/InvariantViolationTest.java @@ -1,43 +1,33 @@ package de.tlc4b.tlc.integration.probprivate; import java.io.File; -import java.util.ArrayList; -import java.util.List; import de.tlc4b.tlc.TLCResults.TLCResult; -import de.tlc4b.util.AbstractParseMachineTest; -import de.tlc4b.util.PolySuite; -import de.tlc4b.util.PolySuite.Config; -import de.tlc4b.util.PolySuite.Configuration; +import de.tlc4b.util.TestUtil; import org.junit.Test; import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; -import static de.tlc4b.tlc.TLCResults.TLCResult.InvariantViolation; import static de.tlc4b.util.TestUtil.test; import static org.junit.Assert.assertEquals; -@RunWith(PolySuite.class) -public class InvariantViolationTest extends AbstractParseMachineTest { - +@RunWith(Parameterized.class) +public class InvariantViolationTest { private final File machine; - private final TLCResult error; - public InvariantViolationTest(File machine, TLCResult result) { + public InvariantViolationTest(File machine) { this.machine = machine; - this.error = result; } @Test public void testRunTLC() throws Exception { String[] a = new String[] { machine.getPath() }; - assertEquals(error, test(a)); + assertEquals(TLCResult.InvariantViolation, test(a)); } - @Config - public static Configuration getConfig() { - List<String> list = new ArrayList<>(); - list.add("build/prob_examples/public_examples/TLC/InvariantViolation"); - return getConfiguration(list, InvariantViolation); + @Parameterized.Parameters(name = "{0}") + public static File[] data() { + return TestUtil.getMachines("build/prob_examples/public_examples/TLC/InvariantViolation"); } } diff --git a/src/test/java/de/tlc4b/tlc/integration/probprivate/NoErrorTest.java b/src/test/java/de/tlc4b/tlc/integration/probprivate/NoErrorTest.java index d8a42a4..1c42dae 100644 --- a/src/test/java/de/tlc4b/tlc/integration/probprivate/NoErrorTest.java +++ b/src/test/java/de/tlc4b/tlc/integration/probprivate/NoErrorTest.java @@ -1,44 +1,33 @@ package de.tlc4b.tlc.integration.probprivate; import java.io.File; -import java.util.ArrayList; -import java.util.List; import de.tlc4b.tlc.TLCResults.TLCResult; -import de.tlc4b.util.AbstractParseMachineTest; -import de.tlc4b.util.PolySuite; -import de.tlc4b.util.PolySuite.Config; -import de.tlc4b.util.PolySuite.Configuration; +import de.tlc4b.util.TestUtil; import org.junit.Test; import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; -import static de.tlc4b.tlc.TLCResults.TLCResult.NoError; import static de.tlc4b.util.TestUtil.test; import static org.junit.Assert.assertEquals; -@RunWith(PolySuite.class) -public class NoErrorTest extends AbstractParseMachineTest { - +@RunWith(Parameterized.class) +public class NoErrorTest { private final File machine; - private final TLCResult error; - public NoErrorTest(File machine, TLCResult result) { + public NoErrorTest(File machine) { this.machine = machine; - this.error = result; } @Test public void testRunTLC() throws Exception { String[] a = new String[] { machine.getPath() }; - assertEquals(error, test(a)); + assertEquals(TLCResult.NoError, test(a)); } - @Config - public static Configuration getConfig() { - List<String> list = new ArrayList<>(); - list.add("build/prob_examples/public_examples/TLC/NoError"); - return getConfiguration(list, NoError); + @Parameterized.Parameters(name = "{0}") + public static File[] data() { + return TestUtil.getMachines("build/prob_examples/public_examples/TLC/NoError"); } - } diff --git a/src/test/java/de/tlc4b/tlc/integration/probprivate/WellDefinednessTest.java b/src/test/java/de/tlc4b/tlc/integration/probprivate/WellDefinednessTest.java index 02ba852..84dd04e 100644 --- a/src/test/java/de/tlc4b/tlc/integration/probprivate/WellDefinednessTest.java +++ b/src/test/java/de/tlc4b/tlc/integration/probprivate/WellDefinednessTest.java @@ -1,42 +1,33 @@ package de.tlc4b.tlc.integration.probprivate; import java.io.File; -import java.util.ArrayList; -import java.util.List; import de.tlc4b.tlc.TLCResults.TLCResult; -import de.tlc4b.util.AbstractParseMachineTest; -import de.tlc4b.util.PolySuite; -import de.tlc4b.util.PolySuite.Config; -import de.tlc4b.util.PolySuite.Configuration; +import de.tlc4b.util.TestUtil; import org.junit.Test; import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; -import static de.tlc4b.tlc.TLCResults.TLCResult.WellDefinednessError; import static de.tlc4b.util.TestUtil.test; import static org.junit.Assert.assertEquals; -@RunWith(PolySuite.class) -public class WellDefinednessTest extends AbstractParseMachineTest { +@RunWith(Parameterized.class) +public class WellDefinednessTest { private final File machine; - private final TLCResult error; - public WellDefinednessTest(File machine, TLCResult result) { + public WellDefinednessTest(File machine) { this.machine = machine; - this.error = result; } @Test public void testRunTLC() throws Exception { String[] a = new String[] { machine.getPath(), "-wdcheck" }; - assertEquals(error, test(a)); + assertEquals(TLCResult.WellDefinednessError, test(a)); } - @Config - public static Configuration getConfig() { - List<String> list = new ArrayList<>(); - list.add("build/prob_examples/public_examples/TLC/WellDefinednessError"); - return getConfiguration(list, WellDefinednessError); + @Parameterized.Parameters(name = "{0}") + public static File[] data() { + return TestUtil.getMachines("build/prob_examples/public_examples/TLC/WellDefinednessError"); } } diff --git a/src/test/java/de/tlc4b/util/AbstractParseMachineTest.java b/src/test/java/de/tlc4b/util/AbstractParseMachineTest.java deleted file mode 100644 index e6f0e66..0000000 --- a/src/test/java/de/tlc4b/util/AbstractParseMachineTest.java +++ /dev/null @@ -1,64 +0,0 @@ -package de.tlc4b.util; - -import java.io.File; -import java.util.ArrayList; -import java.util.Arrays; -import java.util.List; - -import de.tlc4b.tlc.TLCResults.TLCResult; -import de.tlc4b.util.PolySuite.Configuration; - -public abstract class AbstractParseMachineTest { - protected static Configuration getConfiguration2(List<String> list) { - List<File> allMachines = new ArrayList<>(); - - for (String path : list) { - allMachines.addAll(TestUtil.getMachinesRecursively(path)); - } - - return new Configuration() { - public int size() { - return allMachines.size(); - } - - public File getTestValue(int index) { - return allMachines.get(index); - } - - public String getTestName(int index) { - return allMachines.get(index).getName(); - } - - public TLCResult getExpectedValue(int index) { - return TLCResult.NoError; - } - }; - } - - protected static Configuration getConfiguration(List<String> list, TLCResult expectedResult) { - List<File> allMachines = new ArrayList<>(); - - for (String path : list) { - allMachines.addAll(Arrays.asList(TestUtil.getMachines(path))); - } - - return new Configuration() { - public int size() { - return allMachines.size(); - } - - public File getTestValue(int index) { - return allMachines.get(index); - } - - public String getTestName(int index) { - return allMachines.get(index).getName(); - } - - public TLCResult getExpectedValue(int index) { - return expectedResult; - } - }; - } - -} \ No newline at end of file diff --git a/src/test/java/de/tlc4b/util/PolySuite.java b/src/test/java/de/tlc4b/util/PolySuite.java deleted file mode 100644 index 660e67f..0000000 --- a/src/test/java/de/tlc4b/util/PolySuite.java +++ /dev/null @@ -1,140 +0,0 @@ -package de.tlc4b.util; - -import java.lang.annotation.ElementType; -import java.lang.annotation.Retention; -import java.lang.annotation.RetentionPolicy; -import java.lang.annotation.Target; -import java.lang.reflect.Modifier; -import java.util.ArrayList; -import java.util.Collections; -import java.util.List; - -import org.junit.runner.Runner; -import org.junit.runner.notification.RunNotifier; -import org.junit.runners.BlockJUnit4ClassRunner; -import org.junit.runners.Suite; -import org.junit.runners.model.FrameworkMethod; -import org.junit.runners.model.InitializationError; -import org.junit.runners.model.Statement; -import org.junit.runners.model.TestClass; - -public class PolySuite extends Suite { - - // ////////////////////////////// - // Public helper interfaces - - /** - * Annotation for a method which returns a {@link Configuration} - * to be injected into the test class constructor - */ - @Retention(RetentionPolicy.RUNTIME) - @Target(ElementType.METHOD) - public @interface Config { - } - - public interface Configuration { - int size(); - Object getTestValue(int index); - Object getExpectedValue(int index); - String getTestName(int index); - } - - // ////////////////////////////// - // Fields - - private final List<Runner> runners; - - // ////////////////////////////// - // Constructor - - /** - * Only called reflectively. Do not use programmatically. - * @param c the test class - * @throws Throwable if something bad happens - */ - public PolySuite(Class<?> c) throws Throwable { - super(c, Collections.emptyList()); - TestClass testClass = getTestClass(); - Class<?> jTestClass = testClass.getJavaClass(); - Configuration configuration = getConfiguration(testClass); - List<Runner> runners = new ArrayList<>(); - for (int i = 0, size = configuration.size(); i < size; i++) { - SingleRunner runner = new SingleRunner(jTestClass, configuration.getTestValue(i), configuration.getTestName(i), configuration.getExpectedValue(i)); - runners.add(runner); - } - this.runners = runners; - } - - // ////////////////////////////// - // Overrides - - @Override - protected List<Runner> getChildren() { - return runners; - } - - // ////////////////////////////// - // Private - - private Configuration getConfiguration(TestClass testClass) throws Throwable { - return (Configuration) getConfigMethod(testClass).invokeExplosively(null); - } - - private FrameworkMethod getConfigMethod(TestClass testClass) { - List<FrameworkMethod> methods = testClass.getAnnotatedMethods(Config.class); - if (methods.isEmpty()) { - throw new IllegalStateException("@" + Config.class.getSimpleName() + " method not found"); - } - if (methods.size() > 1) { - throw new IllegalStateException("Too many @" + Config.class.getSimpleName() + " methods"); - } - FrameworkMethod method = methods.get(0); - int modifiers = method.getMethod().getModifiers(); - if (!(Modifier.isStatic(modifiers) && Modifier.isPublic(modifiers))) { - throw new IllegalStateException("@" + Config.class.getSimpleName() + " method \"" + method.getName() + "\" must be public static"); - } - return method; - } - - // ////////////////////////////// - // Helper classes - - private static class SingleRunner extends BlockJUnit4ClassRunner { - - private final Object testVal; - private final Object expectedVal; - private final String testName; - - SingleRunner(Class<?> testClass, Object testVal, String testName, Object expectedVal) throws InitializationError { - super(testClass); - this.testVal = testVal; - this.expectedVal = expectedVal; - this.testName = testName; - } - - @Override - protected Object createTest() throws Exception { - return getTestClass().getOnlyConstructor().newInstance(testVal, expectedVal); - } - - @Override - protected String getName() { - return testName; - } - - @Override - protected String testName(FrameworkMethod method) { - return testName + ": " + method.getName(); - } - - @Override - protected void validateConstructor(List<Throwable> errors) { - validateOnlyOneConstructor(errors); - } - - @Override - protected Statement classBlock(RunNotifier notifier) { - return childrenInvoker(notifier); - } - } -} \ No newline at end of file -- GitLab