fix: concrete supertype translation

2 files changed, 149 insertions, 5 deletions

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 <https://refinery.tools/>
+ *
+ * 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));
+        }
+}