diff options
author | Kristóf Marussy <marussy@mit.bme.hu> | 2023-09-14 19:29:36 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2023-09-14 19:29:36 +0200 |
commit | 98ed3b6db5f4e51961a161050cc31c66015116e8 (patch) | |
tree | 8bfd6d9bc8d6ed23b9eb0f889dd40b6c24fe8f92 /subprojects/language/src/test/java | |
parent | Merge pull request #38 from nagilooh/design-space-exploration (diff) | |
parent | Merge remote-tracking branch 'upstream/main' into partial-interpretation (diff) | |
download | refinery-98ed3b6db5f4e51961a161050cc31c66015116e8.tar.gz refinery-98ed3b6db5f4e51961a161050cc31c66015116e8.tar.zst refinery-98ed3b6db5f4e51961a161050cc31c66015116e8.zip |
Merge pull request #39 from kris7t/partial-interpretation
Implement partial interpretation based model generation
Diffstat (limited to 'subprojects/language/src/test/java')
4 files changed, 3 insertions, 251 deletions
diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/ProblemParsingTest.java b/subprojects/language/src/test/java/tools/refinery/language/tests/ProblemParsingTest.java index c7952369..96e7cf9c 100644 --- a/subprojects/language/src/test/java/tools/refinery/language/tests/ProblemParsingTest.java +++ b/subprojects/language/src/test/java/tools/refinery/language/tests/ProblemParsingTest.java | |||
@@ -31,7 +31,6 @@ class ProblemParsingTest { | |||
31 | class Person { | 31 | class Person { |
32 | Person[0..*] children opposite parent | 32 | Person[0..*] children opposite parent |
33 | Person[0..1] parent opposite children | 33 | Person[0..1] parent opposite children |
34 | int age | ||
35 | TaxStatus taxStatus | 34 | TaxStatus taxStatus |
36 | } | 35 | } |
37 | 36 | ||
@@ -51,8 +50,6 @@ class ProblemParsingTest { | |||
51 | children(anne, ciri). | 50 | children(anne, ciri). |
52 | ?children(bob, ciri). | 51 | ?children(bob, ciri). |
53 | taxStatus(anne, ADULT). | 52 | taxStatus(anne, ADULT). |
54 | age(bob): 21..35. | ||
55 | age(ciri): 10. | ||
56 | """); | 53 | """); |
57 | assertThat(problem.errors(), empty()); | 54 | assertThat(problem.errors(), empty()); |
58 | } | 55 | } |
diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/parser/antlr/TransitiveClosureParserTest.java b/subprojects/language/src/test/java/tools/refinery/language/tests/parser/antlr/TransitiveClosureParserTest.java index 1180d131..ed193e90 100644 --- a/subprojects/language/src/test/java/tools/refinery/language/tests/parser/antlr/TransitiveClosureParserTest.java +++ b/subprojects/language/src/test/java/tools/refinery/language/tests/parser/antlr/TransitiveClosureParserTest.java | |||
@@ -29,9 +29,7 @@ class TransitiveClosureParserTest { | |||
29 | @Test | 29 | @Test |
30 | void binaryAddOperatorTest() { | 30 | void binaryAddOperatorTest() { |
31 | var problem = parseHelper.parse(""" | 31 | var problem = parseHelper.parse(""" |
32 | fn int a(). | 32 | pred foo(a, b) <-> a + (b) > 10. |
33 | fn int b(). | ||
34 | pred foo() <-> a() + (b()) > 10. | ||
35 | """); | 33 | """); |
36 | assertThat(problem.errors(), empty()); | 34 | assertThat(problem.errors(), empty()); |
37 | var literal = problem.pred("foo").conj(0).lit(0).get(); | 35 | var literal = problem.pred("foo").conj(0).lit(0).get(); |
diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/serializer/ProblemSerializerTest.java b/subprojects/language/src/test/java/tools/refinery/language/tests/serializer/ProblemSerializerTest.java index 3f3a081f..9f4f2bbf 100644 --- a/subprojects/language/src/test/java/tools/refinery/language/tests/serializer/ProblemSerializerTest.java +++ b/subprojects/language/src/test/java/tools/refinery/language/tests/serializer/ProblemSerializerTest.java | |||
@@ -178,7 +178,7 @@ class ProblemSerializerTest { | |||
178 | var variable = ProblemFactory.eINSTANCE.createImplicitVariable(); | 178 | var variable = ProblemFactory.eINSTANCE.createImplicitVariable(); |
179 | variable.setName("q"); | 179 | variable.setName("q"); |
180 | conjunction.getImplicitVariables().add(variable); | 180 | conjunction.getImplicitVariables().add(variable); |
181 | var equals = nodeType.feature("equals"); | 181 | var equals = builtin.pred("equals").get(); |
182 | conjunction.getLiterals().add(createAtom(equals, parameter1, variable)); | 182 | conjunction.getLiterals().add(createAtom(equals, parameter1, variable)); |
183 | conjunction.getLiterals().add(createAtom(equals, variable, parameter2)); | 183 | conjunction.getLiterals().add(createAtom(equals, variable, parameter2)); |
184 | pred.getBodies().add(conjunction); | 184 | pred.getBodies().add(conjunction); |
@@ -212,7 +212,7 @@ class ProblemSerializerTest { | |||
212 | pred.getParameters().add(parameter); | 212 | pred.getParameters().add(parameter); |
213 | var conjunction = ProblemFactory.eINSTANCE.createConjunction(); | 213 | var conjunction = ProblemFactory.eINSTANCE.createConjunction(); |
214 | var atom = ProblemFactory.eINSTANCE.createAtom(); | 214 | var atom = ProblemFactory.eINSTANCE.createAtom(); |
215 | var equals = nodeType.feature("equals"); | 215 | var equals = builtin.pred("equals").get(); |
216 | atom.setRelation(equals); | 216 | atom.setRelation(equals); |
217 | var arg1 = ProblemFactory.eINSTANCE.createVariableOrNodeExpr(); | 217 | var arg1 = ProblemFactory.eINSTANCE.createVariableOrNodeExpr(); |
218 | arg1.setVariableOrNode(parameter); | 218 | arg1.setVariableOrNode(parameter); |
diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/utils/SymbolCollectorTest.java b/subprojects/language/src/test/java/tools/refinery/language/tests/utils/SymbolCollectorTest.java deleted file mode 100644 index d200eeff..00000000 --- a/subprojects/language/src/test/java/tools/refinery/language/tests/utils/SymbolCollectorTest.java +++ /dev/null | |||
@@ -1,243 +0,0 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.language.tests.utils; | ||
7 | |||
8 | import com.google.inject.Inject; | ||
9 | import org.eclipse.xtext.testing.InjectWith; | ||
10 | import org.eclipse.xtext.testing.extensions.InjectionExtension; | ||
11 | import org.hamcrest.Matcher; | ||
12 | import org.junit.jupiter.api.Disabled; | ||
13 | import org.junit.jupiter.api.Test; | ||
14 | import org.junit.jupiter.api.extension.ExtendWith; | ||
15 | import org.junit.jupiter.params.ParameterizedTest; | ||
16 | import org.junit.jupiter.params.provider.Arguments; | ||
17 | import org.junit.jupiter.params.provider.MethodSource; | ||
18 | import tools.refinery.language.model.problem.*; | ||
19 | import tools.refinery.language.model.tests.utils.ProblemParseHelper; | ||
20 | import tools.refinery.language.tests.ProblemInjectorProvider; | ||
21 | import tools.refinery.language.utils.ContainmentRole; | ||
22 | import tools.refinery.language.utils.ProblemDesugarer; | ||
23 | |||
24 | import java.util.stream.Stream; | ||
25 | |||
26 | import static org.hamcrest.MatcherAssert.assertThat; | ||
27 | import static org.hamcrest.Matchers.*; | ||
28 | import static org.junit.jupiter.api.Assertions.assertDoesNotThrow; | ||
29 | |||
30 | @ExtendWith(InjectionExtension.class) | ||
31 | @InjectWith(ProblemInjectorProvider.class) | ||
32 | class SymbolCollectorTest { | ||
33 | @Inject | ||
34 | private ProblemParseHelper parseHelper; | ||
35 | |||
36 | @Inject | ||
37 | private ProblemDesugarer desugarer; | ||
38 | |||
39 | @Test | ||
40 | void implicitNodeTest() { | ||
41 | var problem = parseHelper.parse(""" | ||
42 | exists(a). | ||
43 | """); | ||
44 | var collectedSymbols = desugarer.collectSymbols(problem.get()); | ||
45 | var node = problem.node("a"); | ||
46 | assertThat(collectedSymbols.nodes(), hasKey(node)); | ||
47 | assertThat(collectedSymbols.nodes().get(node).individual(), is(false)); | ||
48 | } | ||
49 | |||
50 | @Test | ||
51 | void individualNodeTest() { | ||
52 | var problem = parseHelper.parse(""" | ||
53 | indiv a. | ||
54 | """); | ||
55 | var collectedSymbols = desugarer.collectSymbols(problem.get()); | ||
56 | var node = problem.individualNode("a"); | ||
57 | assertThat(collectedSymbols.nodes(), hasKey(node)); | ||
58 | assertThat(collectedSymbols.nodes().get(node).individual(), is(true)); | ||
59 | } | ||
60 | |||
61 | @Test | ||
62 | void classTest() { | ||
63 | var problem = parseHelper.parse(""" | ||
64 | class Foo. | ||
65 | """); | ||
66 | var collectedSymbols = desugarer.collectSymbols(problem.get()); | ||
67 | var classDeclaration = problem.findClass("Foo").get(); | ||
68 | assertThat(collectedSymbols.relations(), hasKey(classDeclaration)); | ||
69 | var classInfo = collectedSymbols.relations().get(classDeclaration); | ||
70 | assertThat(classInfo.parameters(), hasSize(1)); | ||
71 | assertThat(classInfo.containmentRole(), is(ContainmentRole.CONTAINED)); | ||
72 | assertThat(classInfo.hasDefinition(), is(false)); | ||
73 | var newNode = classDeclaration.getNewNode(); | ||
74 | assertThat(collectedSymbols.nodes(), hasKey(newNode)); | ||
75 | assertThat(collectedSymbols.nodes().get(newNode).individual(), is(false)); | ||
76 | assertThat(classInfo.assertions(), assertsNode(newNode, LogicValue.TRUE)); | ||
77 | assertThat(collectedSymbols.relations().get(problem.builtinSymbols().exists()).assertions(), | ||
78 | assertsNode(newNode, LogicValue.UNKNOWN)); | ||
79 | assertThat(collectedSymbols.relations().get(problem.builtinSymbols().equals()).assertions(), | ||
80 | assertsNode(newNode, LogicValue.UNKNOWN)); | ||
81 | } | ||
82 | |||
83 | @Test | ||
84 | void abstractClassTest() { | ||
85 | var problem = parseHelper.parse(""" | ||
86 | abstract class Foo. | ||
87 | """); | ||
88 | var collectedSymbols = desugarer.collectSymbols(problem.get()); | ||
89 | assertThat(collectedSymbols.relations().get(problem.findClass("Foo").get()).assertions(), hasSize(0)); | ||
90 | } | ||
91 | |||
92 | @Test | ||
93 | void referenceTest() { | ||
94 | var problem = parseHelper.parse(""" | ||
95 | class Foo { | ||
96 | refers Foo[] bar opposite quux | ||
97 | refers Foo quux opposite bar | ||
98 | } | ||
99 | """); | ||
100 | var collectedSymbols = desugarer.collectSymbols(problem.get()); | ||
101 | var fooClass = problem.findClass("Foo"); | ||
102 | var barReference = fooClass.feature("bar"); | ||
103 | var barInfo = collectedSymbols.relations().get(barReference); | ||
104 | var quuxReference = fooClass.feature("quux"); | ||
105 | var quuxInfo = collectedSymbols.relations().get(quuxReference); | ||
106 | assertThat(barInfo.containmentRole(), is(ContainmentRole.NONE)); | ||
107 | assertThat(barInfo.opposite(), is(quuxReference)); | ||
108 | assertThat(barInfo.multiplicity(), is(instanceOf(UnboundedMultiplicity.class))); | ||
109 | assertThat(barInfo.hasDefinition(), is(false)); | ||
110 | assertThat(quuxInfo.containmentRole(), is(ContainmentRole.NONE)); | ||
111 | assertThat(quuxInfo.opposite(), is(barReference)); | ||
112 | assertThat(quuxInfo.multiplicity(), is(instanceOf(ExactMultiplicity.class))); | ||
113 | assertThat(quuxInfo.multiplicity(), hasProperty("exactValue", is(1))); | ||
114 | assertThat(quuxInfo.hasDefinition(), is(false)); | ||
115 | } | ||
116 | |||
117 | @Test | ||
118 | void containmentReferenceTest() { | ||
119 | var problem = parseHelper.parse(""" | ||
120 | class Foo { | ||
121 | contains Foo[] bar | ||
122 | } | ||
123 | """); | ||
124 | var collectedSymbols = desugarer.collectSymbols(problem.get()); | ||
125 | assertThat(collectedSymbols.relations().get(problem.findClass("Foo").feature("bar")).containmentRole(), | ||
126 | is(ContainmentRole.CONTAINMENT)); | ||
127 | } | ||
128 | |||
129 | @Disabled("TODO: Rework numerical references") | ||
130 | @Test | ||
131 | void dataReferenceTest() { | ||
132 | var problem = parseHelper.parse(""" | ||
133 | class Foo { | ||
134 | int bar | ||
135 | } | ||
136 | """); | ||
137 | var collectedSymbols = desugarer.collectSymbols(problem.get()); | ||
138 | assertThat(collectedSymbols.relations().get(problem.findClass("Foo").feature("bar")).containmentRole(), | ||
139 | is(ContainmentRole.CONTAINMENT)); | ||
140 | } | ||
141 | |||
142 | @Test | ||
143 | void enumTest() { | ||
144 | var problem = parseHelper.parse(""" | ||
145 | enum Foo { | ||
146 | bar, quux | ||
147 | } | ||
148 | """); | ||
149 | var collectedSymbols = desugarer.collectSymbols(problem.get()); | ||
150 | var enumDeclaration = problem.findEnum("Foo"); | ||
151 | var enumInfo = collectedSymbols.relations().get(enumDeclaration.get()); | ||
152 | assertThat(enumInfo.containmentRole(), is(ContainmentRole.NONE)); | ||
153 | assertThat(enumInfo.assertions(), assertsNode(enumDeclaration.literal("bar"), LogicValue.TRUE)); | ||
154 | assertThat(enumInfo.assertions(), assertsNode(enumDeclaration.literal("quux"), LogicValue.TRUE)); | ||
155 | } | ||
156 | |||
157 | @ParameterizedTest | ||
158 | @MethodSource | ||
159 | void predicateTest(String keyword, ContainmentRole containmentRole) { | ||
160 | var problem = parseHelper.parse(keyword + " foo(node x) <-> domain(x); data(x)."); | ||
161 | var collectedSymbols = desugarer.collectSymbols(problem.get()); | ||
162 | var predicateInfo = collectedSymbols.relations().get(problem.pred("foo").get()); | ||
163 | assertThat(predicateInfo.containmentRole(), is(containmentRole)); | ||
164 | assertThat(predicateInfo.parameters(), hasSize(1)); | ||
165 | assertThat(predicateInfo.bodies(), hasSize(2)); | ||
166 | assertThat(predicateInfo.hasDefinition(), is(true)); | ||
167 | } | ||
168 | |||
169 | static Stream<Arguments> predicateTest() { | ||
170 | return Stream.of(Arguments.of("pred", ContainmentRole.NONE), Arguments.of("error", ContainmentRole.NONE), | ||
171 | Arguments.of("contained pred", ContainmentRole.CONTAINED), Arguments.of("containment pred", | ||
172 | ContainmentRole.CONTAINMENT)); | ||
173 | } | ||
174 | |||
175 | @ParameterizedTest | ||
176 | @MethodSource("logicValues") | ||
177 | void assertionTest(String keyword, LogicValue value) { | ||
178 | var problem = parseHelper.parse(""" | ||
179 | pred foo(node x). | ||
180 | foo(a): %s. | ||
181 | """.formatted(keyword)); | ||
182 | var collectedSymbols = desugarer.collectSymbols(problem.get()); | ||
183 | assertThat(collectedSymbols.relations().get(problem.pred("foo").get()).assertions(), | ||
184 | assertsNode(problem.node("a"), value)); | ||
185 | } | ||
186 | |||
187 | @ParameterizedTest | ||
188 | @MethodSource("logicValues") | ||
189 | void defaultAssertionTest(String keyword, LogicValue value) { | ||
190 | var problem = parseHelper.parse(""" | ||
191 | pred foo(node x). | ||
192 | default foo(a): %s. | ||
193 | """.formatted(keyword)); | ||
194 | var collectedSymbols = desugarer.collectSymbols(problem.get()); | ||
195 | assertThat(collectedSymbols.relations().get(problem.pred("foo").get()).assertions(), | ||
196 | assertsNode(problem.node("a"), value)); | ||
197 | } | ||
198 | |||
199 | static Stream<Arguments> logicValues() { | ||
200 | return Stream.of(Arguments.of("true", LogicValue.TRUE), Arguments.of("false", LogicValue.FALSE), | ||
201 | Arguments.of("unknown", LogicValue.UNKNOWN), Arguments.of("error", LogicValue.ERROR)); | ||
202 | } | ||
203 | |||
204 | @Test | ||
205 | void invalidAssertionArityTest() { | ||
206 | var problem = parseHelper.parse(""" | ||
207 | pred foo(node x). | ||
208 | foo(a, b). | ||
209 | """); | ||
210 | var collectedSymbols = desugarer.collectSymbols(problem.get()); | ||
211 | assertThat(collectedSymbols.relations().get(problem.pred("foo").get()).assertions(), hasSize(0)); | ||
212 | } | ||
213 | |||
214 | @Test | ||
215 | void invalidProblemTest() { | ||
216 | var problem = parseHelper.parse(""" | ||
217 | class Foo { | ||
218 | bar[] opposite quux | ||
219 | Foo quux opposite bar | ||
220 | } | ||
221 | """).get(); | ||
222 | assertDoesNotThrow(() -> desugarer.collectSymbols(problem)); | ||
223 | } | ||
224 | |||
225 | @Test | ||
226 | void errorAssertionTest() { | ||
227 | var problem = parseHelper.parse(""" | ||
228 | error foo(node a, node b) <-> equals(a, b). | ||
229 | """); | ||
230 | var collectedSymbols = desugarer.collectSymbols(problem.get()); | ||
231 | var fooInfo = collectedSymbols.relations().get(problem.pred("foo").get()); | ||
232 | assertThat(fooInfo.assertions(), hasSize(1)); | ||
233 | var assertion = fooInfo.assertions().stream().findFirst().orElseThrow(); | ||
234 | assertThat(assertion.getValue(), hasProperty("logicValue", is(LogicValue.FALSE))); | ||
235 | assertThat(assertion.getArguments(), hasSize(2)); | ||
236 | assertThat(assertion.getArguments(), everyItem(instanceOf(WildcardAssertionArgument.class))); | ||
237 | } | ||
238 | |||
239 | private static Matcher<Iterable<? super Assertion>> assertsNode(Node node, LogicValue value) { | ||
240 | return hasItem(allOf(hasProperty("arguments", hasItem(hasProperty("node", is(node)))), hasProperty("value", | ||
241 | hasProperty("logicValue", is(value))))); | ||
242 | } | ||
243 | } | ||