From 2b4f19dddfafc21a48c899c748b660ae6b376d7b Mon Sep 17 00:00:00 2001 From: Michael Langowski Date: Wed, 24 Jul 2024 11:28:16 +0200 Subject: [PATCH] Improvement: End2End-Tests using ASP unit tests --- .../kr/alpha/core/parser/ParserTest.java | 25 +++++++ .../kr/alpha/e2etests/End2EndTests.java | 74 +++++++++++++++++++ .../src/test/resources/e2e-tests/3col.asp | 66 +++++++++++++++++ 3 files changed, 165 insertions(+) create mode 100644 alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/e2etests/End2EndTests.java create mode 100644 alpha-solver/src/test/resources/e2e-tests/3col.asp diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/parser/ParserTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/parser/ParserTest.java index 8feb5bc04..5bd5de0fa 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/parser/ParserTest.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/parser/ParserTest.java @@ -92,6 +92,8 @@ public class ParserTest { private static final String MODULE_WITH_REGULAR_STMTS = "p(a). p(b). q(X) :- p(X). #module aSimpleModule(input/1 => {out1/2, out2/3}) { p(a). p(b). q(X) :- p(X). }"; + private static final String MODULE_MULTIPLE_DEFINITIONS = "a. b(5). #module aSimpleModule(input/1 => {out1/2, out2/3}) { p(a). p(b). q(X) :- p(X). } q(Y) :- r(S, Y), t(S). #module anotherModule(input/1 => {out1/2, out2/3}) { p(a). p(b). q(X) :- p(X). }"; + private final ProgramParserImpl parser = new ProgramParserImpl(); @Test @@ -369,4 +371,27 @@ public void moduleAndRegularStmts() { assertEquals(1, implementation.getRules().size()); } + @Test + public void multipleModuleDefinitions() { + InputProgram prog = parser.parse(MODULE_MULTIPLE_DEFINITIONS); + assertEquals(2, prog.getFacts().size()); + assertEquals(1, prog.getRules().size()); + + List modules = prog.getModules(); + assertFalse(modules.isEmpty()); + assertEquals(2, modules.size()); + } + + @Test + public void invalidNestedModule() { + assertThrows(IllegalStateException.class, () -> + parser.parse("#module aSimpleModule(input/1 => {out1/2, out2/3}) { p(a). p(b). #module anotherModule(input/1 => {out1/2, out2/3}) { p(a). p(b). } }")); + } + + @Test + public void invalidNestedTest() { + assertThrows(IllegalStateException.class, () -> + parser.parse("#module mod(foo/1 => {*}) { #test test(expect: 1) { given { b. } assertForAll { :- a. } } }")); + } + } diff --git a/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/e2etests/End2EndTests.java b/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/e2etests/End2EndTests.java new file mode 100644 index 000000000..23ee7f3ee --- /dev/null +++ b/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/e2etests/End2EndTests.java @@ -0,0 +1,74 @@ +package at.ac.tuwien.kr.alpha.e2etests; + +import at.ac.tuwien.kr.alpha.api.Alpha; +import at.ac.tuwien.kr.alpha.api.impl.AlphaFactory; +import at.ac.tuwien.kr.alpha.api.programs.InputProgram; +import at.ac.tuwien.kr.alpha.api.programs.tests.Assertion; +import at.ac.tuwien.kr.alpha.api.programs.tests.TestResult; +import at.ac.tuwien.kr.alpha.commons.programs.Programs; +import org.junit.jupiter.api.Assertions; +import org.junit.jupiter.api.DynamicTest; +import org.junit.jupiter.api.TestFactory; + +import java.io.IOException; +import java.io.InputStream; +import java.util.List; +import java.util.Map; +import java.util.function.Predicate; +import java.util.stream.Stream; + +import static org.junit.jupiter.api.Assertions.assertTrue; +import static org.junit.jupiter.api.Assertions.fail; + +/** + * Runs tests written in ASP from a given set of files. + * Dynamic tests generated by this class use Alpha's default configuration. + * A test fails when any ASP test in the corresponding fileset fails. + */ +public class End2EndTests { + + private static final String E2E_TESTS_DIR = "/e2e-tests/"; + + private static void runAspTests(String testName, String... fileset) { + Alpha alpha = AlphaFactory.newAlpha(); + Programs.InputProgramBuilder programBuilder = Programs.builder(); + for (String file : fileset) { + try(InputStream is = End2EndTests.class.getResourceAsStream(file)) { + programBuilder.accumulate(alpha.readProgramStream(is)); + } catch (IOException ex) { + throw new RuntimeException("Failed to read test file: " + file, ex); + } + } + InputProgram program = programBuilder.build(); + TestResult testResult = alpha.test(program); + if (!testResult.isSuccess()) { + StringBuilder msgBuilder = new StringBuilder("Test ").append(testName).append(" failed:").append(System.lineSeparator()); + testResult.getTestCaseResults().stream().filter(Predicate.not(TestResult.TestCaseResult::isSuccess)).forEach(tcResult -> { + msgBuilder.append("Assertion failures for test case ").append(tcResult.getTestCaseName()).append(": ").append(System.lineSeparator()); + if (tcResult.answerSetCountVerificationResult().isPresent()) { + msgBuilder.append(tcResult.answerSetCountVerificationResult().get()).append(System.lineSeparator()); + } + for (Map.Entry> assertionError : tcResult.getAssertionErrors().entrySet()) { + for (String errMsg : assertionError.getValue()) { + msgBuilder.append("Assertion failed: ").append(assertionError.getKey()).append(", error = ").append(errMsg).append(System.lineSeparator()); + } + } + }); + fail(msgBuilder.toString()); + } + } + + private static DynamicTest alphaEnd2EndTest(String testName, String... fileset) { + return DynamicTest.dynamicTest(testName, () -> runAspTests(testName, fileset)); + } + + @TestFactory + Stream alphaEnd2EndTests() { + return Stream.of( + alphaEnd2EndTest("3-Coloring", E2E_TESTS_DIR + "3col.asp") + ); + } + + + +} diff --git a/alpha-solver/src/test/resources/e2e-tests/3col.asp b/alpha-solver/src/test/resources/e2e-tests/3col.asp new file mode 100644 index 000000000..8b7620cde --- /dev/null +++ b/alpha-solver/src/test/resources/e2e-tests/3col.asp @@ -0,0 +1,66 @@ +%%% Basic Encoding of the Graph 3-Coloring Problem %%% +% Graphs are interpreted as having undirected edges. + +% Edges are undirected +edge(Y, X) :- edge(X, Y). + +% Guess color for each vertex +red(V) :- vertex(V), not green(V), not blue(V). +green(V) :- vertex(V), not red(V), not blue(V). +blue(V) :- vertex(V), not red(V), not green(V). + +% Check for invalid colorings +:- vertex(V1), vertex(V2), edge(V1, V2), red(V1), red(V2). +:- vertex(V1), vertex(V2), edge(V1, V2), green(V1), green(V2). +:- vertex(V1), vertex(V2), edge(V1, V2), blue(V1), blue(V2). + +%% Verify that directed edges are converted to undirected ones. +#test no_asymmetric_edge(expect: >0) { + given { + vertex(a). + vertex(b). + vertex(c). + edge(a, b). + edge(b, c). + edge(c, a). + } + assertForAll { + :- edge(A, B), not edge(B, A). + } +} + +#test triangle_colorings(expect: 6) { + given { + vertex(a). + vertex(b). + vertex(c). + edge(a, b). + edge(b, c). + edge(c, a). + } + % Make sure all vertices are colored in all answer sets + assertForAll { + colored(V) :- vertex(V), red(V). + colored(V) :- vertex(V), green(V). + colored(V) :- vertex(V), blue(V). + :- vertex(V), not colored(V). + } + % Make sure we do not have neighboring vertices of same color in any answer set + assertForAll { + :- edge(V1, V2), red(V1), red(V2). + :- edge(V1, V2), green(V1), green(V2). + :- edge(V1, V2), blue(V1), blue(V2). + } + % In at least one answer set, vertex a should be red + assertForSome { + :- not red(a). + } + % In at least one answer set, vertex a should be green + assertForSome { + :- not green(a). + } + % In at least one answer set, vertex a should be blue + assertForSome { + :- not blue(a). + } +} \ No newline at end of file