From 6b0c83a05cd55d3508ca7dc7d7d1648d602bc613 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Sun, 13 Aug 2023 23:33:03 +0200 Subject: fix: concrete supertype translation --- .../typehierarchy/TypeHierarchyTranslator.java | 9 +- .../typehierarchy/ConcreteSupertypeTest.java | 145 +++++++++++++++++++++ 2 files changed, 149 insertions(+), 5 deletions(-) create mode 100644 subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/ConcreteSupertypeTest.java (limited to 'subprojects/store-reasoning') diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java index 4bff4557..67e8035f 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java @@ -45,13 +45,12 @@ public class TypeHierarchyTranslator implements ModelStoreConfiguration { private ModelStoreConfiguration createPreservedTypeTranslator(PartialRelation type, TypeAnalysisResult result) { var may = Query.of(type.name() + "#partial#may", (builder, p1) -> { - if (result.isAbstractType()) { - for (var subtype : result.getDirectSubtypes()) { - builder.clause(PartialLiterals.may(subtype.call(p1))); - } - } else { + if (!result.isAbstractType()) { builder.clause(new MayTypeView(typeSymbol, type).call(p1)); } + for (var subtype : result.getDirectSubtypes()) { + builder.clause(PartialLiterals.may(subtype.call(p1))); + } }); var must = Query.of(type.name() + "#partial#must", (builder, p1) -> builder.clause( diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/ConcreteSupertypeTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/ConcreteSupertypeTest.java new file mode 100644 index 00000000..3658d603 --- /dev/null +++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/ConcreteSupertypeTest.java @@ -0,0 +1,145 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.translator.typehierarchy; + +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; +import tools.refinery.store.model.ModelStore; +import tools.refinery.store.query.viatra.ViatraModelQueryAdapter; +import tools.refinery.store.reasoning.ReasoningAdapter; +import tools.refinery.store.reasoning.ReasoningStoreAdapter; +import tools.refinery.store.reasoning.literal.Concreteness; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.seed.ModelSeed; +import tools.refinery.store.representation.TruthValue; +import tools.refinery.store.tuple.Tuple; + +import static org.hamcrest.MatcherAssert.assertThat; +import static org.hamcrest.Matchers.is; + +class ConcreteSupertypeTest { + private final PartialRelation c1 = new PartialRelation("C1", 1); + private final PartialRelation c2 = new PartialRelation("C2", 1); + + private ModelStore store; + + @BeforeEach + void beforeEach() { + var typeHierarchy = TypeHierarchy.builder() + .type(c1) + .type(c2, c1) + .build(); + + store = ModelStore.builder() + .with(ViatraModelQueryAdapter.builder()) + .with(ReasoningAdapter.builder()) + .with(new TypeHierarchyTranslator(typeHierarchy)) + .build(); + } + + @Test + void inheritedTypeTrueTest() { + var seed = ModelSeed.builder(1) + .seed(c1, builder -> builder.reducedValue(TruthValue.UNKNOWN)) + .seed(c2, builder -> builder + .reducedValue(TruthValue.UNKNOWN) + .put(Tuple.of(0), TruthValue.TRUE)) + .build(); + + var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(seed); + var adapter = model.getAdapter(ReasoningAdapter.class); + + assertThat(adapter.getPartialInterpretation(Concreteness.PARTIAL, c1).get(Tuple.of(0)), is(TruthValue.TRUE)); + assertThat(adapter.getPartialInterpretation(Concreteness.PARTIAL, c2).get(Tuple.of(0)), is(TruthValue.TRUE)); + } + + @Test + void inheritedTypeFalseTest() { + var seed = ModelSeed.builder(1) + .seed(c1, builder -> builder.reducedValue(TruthValue.UNKNOWN)) + .seed(c2, builder -> builder + .reducedValue(TruthValue.UNKNOWN) + .put(Tuple.of(0), TruthValue.FALSE)) + .build(); + + var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(seed); + var adapter = model.getAdapter(ReasoningAdapter.class); + + assertThat(adapter.getPartialInterpretation(Concreteness.PARTIAL, c1).get(Tuple.of(0)), + is(TruthValue.UNKNOWN)); + assertThat(adapter.getPartialInterpretation(Concreteness.PARTIAL, c2).get(Tuple.of(0)), is(TruthValue.FALSE)); + } + + @Test + void supertypeTrueTest() { + var seed = ModelSeed.builder(1) + .seed(c1, builder -> builder + .reducedValue(TruthValue.UNKNOWN) + .put(Tuple.of(0), TruthValue.TRUE)) + .seed(c2, builder -> builder.reducedValue(TruthValue.UNKNOWN)) + .build(); + + var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(seed); + var adapter = model.getAdapter(ReasoningAdapter.class); + + assertThat(adapter.getPartialInterpretation(Concreteness.PARTIAL, c1).get(Tuple.of(0)), is(TruthValue.TRUE)); + assertThat(adapter.getPartialInterpretation(Concreteness.PARTIAL, c2).get(Tuple.of(0)), + is(TruthValue.UNKNOWN)); + } + + @Test + void supertypeFalseTest() { + var seed = ModelSeed.builder(1) + .seed(c1, builder -> builder + .reducedValue(TruthValue.UNKNOWN) + .put(Tuple.of(0), TruthValue.FALSE)) + .seed(c2, builder -> builder.reducedValue(TruthValue.UNKNOWN)) + .build(); + + var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(seed); + var adapter = model.getAdapter(ReasoningAdapter.class); + + assertThat(adapter.getPartialInterpretation(Concreteness.PARTIAL, c1).get(Tuple.of(0)), is(TruthValue.FALSE)); + assertThat(adapter.getPartialInterpretation(Concreteness.PARTIAL, c2).get(Tuple.of(0)), is(TruthValue.FALSE)); + } + + @Test + void supertypeOnlyTest() { + var seed = ModelSeed.builder(1) + .seed(c1, builder -> builder + .reducedValue(TruthValue.UNKNOWN) + .put(Tuple.of(0), TruthValue.TRUE)) + .seed(c2, builder -> builder + .reducedValue(TruthValue.UNKNOWN) + .put(Tuple.of(0), TruthValue.FALSE)) + .build(); + + var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(seed); + var adapter = model.getAdapter(ReasoningAdapter.class); + + assertThat(adapter.getPartialInterpretation(Concreteness.PARTIAL, c1).get(Tuple.of(0)), is(TruthValue.TRUE)); + assertThat(adapter.getPartialInterpretation(Concreteness.PARTIAL, c2).get(Tuple.of(0)), is(TruthValue.FALSE)); + } + + + @Test + void inheritedTypeErrorTest() { + var seed = ModelSeed.builder(1) + .seed(c1, builder -> builder + .reducedValue(TruthValue.UNKNOWN) + .put(Tuple.of(0), TruthValue.FALSE)) + .seed(c2, builder -> builder + .reducedValue(TruthValue.UNKNOWN) + .put(Tuple.of(0), TruthValue.TRUE)) + .build(); + + var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(seed); + var adapter = model.getAdapter(ReasoningAdapter.class); + + assertThat(adapter.getPartialInterpretation(Concreteness.PARTIAL, c1).get(Tuple.of(0)), is(TruthValue.ERROR)); + assertThat(adapter.getPartialInterpretation(Concreteness.PARTIAL, c2).get(Tuple.of(0)), is(TruthValue.ERROR)); + } +} -- cgit v1.2.3-70-g09d2