From 07b4048828d9ef8126282c4626dd3f0729213d91 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Sat, 1 Jun 2024 18:37:20 +0200 Subject: feat: partial references References marked as partial are not concretized during model generation. The should be managed by the user manually using propagation rules instead. --- subprojects/frontend/src/language/problem.grammar | 2 +- .../src/language/problemLanguageSupport.ts | 2 +- subprojects/language-model/problem.aird | 16 ++- .../src/main/resources/model/problem.ecore | 1 + .../src/main/resources/model/problem.genmodel | 1 + .../language/semantics/ModelInitializer.java | 2 + .../language/semantics/SolutionSerializer.java | 21 +-- .../java/tools/refinery/language/Problem.xtext | 2 +- .../tools/refinery/language/utils/ProblemUtil.java | 14 +- .../language/validation/ProblemValidator.java | 5 + .../tests/validation/OppositeValidationTest.java | 36 ++++- .../crossreference/CrossReferenceUtils.java | 43 ++++-- .../crossreference/DirectedCrossReferenceInfo.java | 4 +- .../DirectedCrossReferenceTranslator.java | 160 +++++++++++++-------- .../UndirectedCrossReferenceInfo.java | 5 +- .../UndirectedCrossReferenceTranslator.java | 134 ++++++++++------- .../translator/metamodel/MetamodelBuilder.java | 10 +- .../translator/metamodel/ReferenceInfo.java | 9 +- .../translator/metamodel/ReferenceInfoBuilder.java | 8 +- .../InvalidMultiplicityErrorTranslator.java | 12 +- 20 files changed, 329 insertions(+), 158 deletions(-) (limited to 'subprojects') diff --git a/subprojects/frontend/src/language/problem.grammar b/subprojects/frontend/src/language/problem.grammar index ffae220c..a172835d 100644 --- a/subprojects/frontend/src/language/problem.grammar +++ b/subprojects/frontend/src/language/problem.grammar @@ -161,7 +161,7 @@ AssertionActionArgument { VariableName | StarArgument } Constant { Real | String | StarMult | LogicValue } ReferenceKind { - kw<"refers"> | ckw<"contains"> | kw<"container"> + kw<"refers"> | ckw<"contains"> | kw<"container"> | kw<"partial"> } LogicValue { diff --git a/subprojects/frontend/src/language/problemLanguageSupport.ts b/subprojects/frontend/src/language/problemLanguageSupport.ts index ae998d20..5ca162d9 100644 --- a/subprojects/frontend/src/language/problemLanguageSupport.ts +++ b/subprojects/frontend/src/language/problemLanguageSupport.ts @@ -36,7 +36,7 @@ const parserWithMetadata = parser.configure({ 'import as declare atom multi': t.definitionKeyword, 'extern datatype aggregator': t.definitionKeyword, rule: t.definitionKeyword, - 'abstract extends refers contains container opposite': t.modifier, + 'abstract extends refers contains container partial opposite': t.modifier, default: t.modifier, 'propagation decision': t.modifier, 'true false unknown error': t.keyword, diff --git a/subprojects/language-model/problem.aird b/subprojects/language-model/problem.aird index 8682236b..74c658d4 100644 --- a/subprojects/language-model/problem.aird +++ b/subprojects/language-model/problem.aird @@ -7,7 +7,7 @@ build/resources/main/model/problem.genmodel - + @@ -305,11 +305,15 @@ + + + + - + @@ -2226,6 +2230,14 @@ + + + + + + + + diff --git a/subprojects/language-model/src/main/resources/model/problem.ecore b/subprojects/language-model/src/main/resources/model/problem.ecore index ed56d3b1..e830c724 100644 --- a/subprojects/language-model/src/main/resources/model/problem.ecore +++ b/subprojects/language-model/src/main/resources/model/problem.ecore @@ -153,6 +153,7 @@ + diff --git a/subprojects/language-model/src/main/resources/model/problem.genmodel b/subprojects/language-model/src/main/resources/model/problem.genmodel index c7044885..2ceb74a6 100644 --- a/subprojects/language-model/src/main/resources/model/problem.genmodel +++ b/subprojects/language-model/src/main/resources/model/problem.genmodel @@ -32,6 +32,7 @@ + diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java index 6c637e19..bd6a8ec9 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java @@ -347,6 +347,7 @@ public class ModelInitializer { var target = getPartialRelation(referenceDeclaration.getReferenceType()); targetTypes.add(target); boolean containment = referenceDeclaration.getKind() == ReferenceKind.CONTAINMENT; + boolean partial = referenceDeclaration.getKind() == ReferenceKind.PARTIAL; var opposite = referenceDeclaration.getOpposite(); PartialRelation oppositeRelation = null; if (opposite != null) { @@ -367,6 +368,7 @@ public class ModelInitializer { .target(target) .opposite(oppositeRelation) .defaultValue(defaultValue) + .partial(partial) .build()); } catch (RuntimeException e) { throw TracedException.addTrace(classDeclaration, e); diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java index f097143f..ed4841c4 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/SolutionSerializer.java @@ -310,7 +310,7 @@ public class SolutionSerializer { var relation = findPartialRelation(partialRelation); var cursor = reasoningAdapter.getPartialInterpretation(Concreteness.CANDIDATE, partialRelation).getAll(); // Make sure to output assertions in a deterministic order. - var sortedTuples = new TreeSet(); + var sortedTuples = new TreeMap(); while (cursor.move()) { var tuple = cursor.getKey(); var from = nodes.get(tuple.get(0)); @@ -320,17 +320,20 @@ public class SolutionSerializer { continue; } var value = cursor.getValue(); - if (!value.isConcrete()) { - throw new IllegalStateException("Invalid %s %s for tuple %s".formatted(partialRelation, value, tuple)); - } - if (value.may()) { - sortedTuples.add(tuple); - } + var logicValue = switch (value) { + case TRUE -> LogicValue.TRUE; + case FALSE -> throw new IllegalStateException("Invalid %s %s for tuple %s" + .formatted(partialRelation, value, tuple)); + case UNKNOWN -> LogicValue.UNKNOWN; + case ERROR -> LogicValue.ERROR; + }; + sortedTuples.put(tuple, logicValue); } - for (var tuple : sortedTuples) { + for (var entry : sortedTuples.entrySet()) { + var tuple = entry.getKey(); var from = nodes.get(tuple.get(0)); var to = nodes.get(tuple.get(1)); - addAssertion(relation, LogicValue.TRUE, from, to); + addAssertion(relation, entry.getValue(), from, to); } } diff --git a/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext b/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext index ebb5bf71..10e994a0 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext +++ b/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext @@ -45,7 +45,7 @@ AggregatorDeclaration: "extern" "aggregator" name=Identifier "."; enum ReferenceKind: - REFERENCE="refers" | CONTAINMENT="contains" | CONTAINER="container"; + REFERENCE="refers" | CONTAINMENT="contains" | CONTAINER="container" | PARTIAL="partial"; ReferenceDeclaration: (referenceType=[Relation|NonContainmentQualifiedName] | diff --git a/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java b/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java index 9daa8f61..e1820261 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java +++ b/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java @@ -42,13 +42,11 @@ public final class ProblemUtil { } public static boolean isImplicit(EObject eObject) { - if (eObject instanceof Node node) { - return isImplicitNode(node); - } else if (eObject instanceof Variable variable) { - return isImplicitVariable(variable); - } else { - return false; - } + return switch (eObject) { + case Node node -> isImplicitNode(node); + case Variable variable -> isImplicitVariable(variable); + default -> false; + }; } public static boolean isError(EObject eObject) { @@ -119,7 +117,7 @@ public final class ProblemUtil { return false; } return switch (kind) { - case CONTAINMENT -> false; + case CONTAINMENT, PARTIAL -> false; case CONTAINER -> true; case DEFAULT, REFERENCE -> { var opposite = referenceDeclaration.getOpposite(); diff --git a/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java b/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java index 9f5fdeae..754572d1 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java +++ b/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java @@ -318,6 +318,11 @@ public class ProblemValidator extends AbstractProblemValidator { referenceDeclaration, ProblemPackage.Literals.REFERENCE_DECLARATION__OPPOSITE, 0, INVALID_OPPOSITE_ISSUE); } + } else if (kind == ReferenceKind.PARTIAL && opposite != null && opposite.getKind() != ReferenceKind.PARTIAL) { + acceptError("Opposite '%s' of partial reference '%s' is not a partial reference." + .formatted(opposite.getName(), referenceDeclaration.getName()), + referenceDeclaration, ProblemPackage.Literals.REFERENCE_DECLARATION__OPPOSITE, 0, + INVALID_OPPOSITE_ISSUE); } } diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/validation/OppositeValidationTest.java b/subprojects/language/src/test/java/tools/refinery/language/tests/validation/OppositeValidationTest.java index 57602377..d73ef8e7 100644 --- a/subprojects/language/src/test/java/tools/refinery/language/tests/validation/OppositeValidationTest.java +++ b/subprojects/language/src/test/java/tools/refinery/language/tests/validation/OppositeValidationTest.java @@ -57,6 +57,18 @@ class OppositeValidationTest { class Foo { Foo foo[] opposite foo } + """, """ + class Foo { + partial Bar bar opposite foo + } + + class Bar { + partial Foo foo opposite bar + } + """, """ + class Foo { + partial Foo foo[] opposite foo + } """}) void validOppositeTest(String text) { var problem = parseHelper.parse(text); @@ -188,7 +200,7 @@ class OppositeValidationTest { } @ParameterizedTest - @ValueSource(strings = {"Foo foo", "container Foo foo"}) + @ValueSource(strings = {"Foo foo", "container Foo foo", "partial Foo foo"}) void containerInvalidOppositeTest(String reference) { var problem = parseHelper.parse(""" class Foo { @@ -203,7 +215,27 @@ class OppositeValidationTest { assertThat(issues, hasItem(allOf( hasProperty("severity", is(Diagnostic.ERROR)), hasProperty("issueCode", is(ProblemValidator.INVALID_OPPOSITE_ISSUE)), - hasProperty("message", stringContainsInOrder("foo", "bar")) + hasProperty("message", stringContainsInOrder("foo", "container", "bar")) + ))); + } + + @ParameterizedTest + @ValueSource(strings = {"Foo foo", "contains Foo foo", "container Foo foo"}) + void partialWithConcreteOppositeTest(String reference) { + var problem = parseHelper.parse(""" + class Foo { + partial Bar bar opposite foo + } + + class Bar { + %s opposite bar + } + """.formatted(reference)); + var issues = problem.validate(); + assertThat(issues, hasItem(allOf( + hasProperty("severity", is(Diagnostic.ERROR)), + hasProperty("issueCode", is(ProblemValidator.INVALID_OPPOSITE_ISSUE)), + hasProperty("message", stringContainsInOrder("foo", "partial", "bar")) ))); } } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/CrossReferenceUtils.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/CrossReferenceUtils.java index 26449df5..56c9d682 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/CrossReferenceUtils.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/CrossReferenceUtils.java @@ -1,16 +1,18 @@ /* - * SPDX-FileCopyrightText: 2023 The Refinery Authors + * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ package tools.refinery.store.reasoning.translator.crossreference; import tools.refinery.logic.dnf.Query; +import tools.refinery.logic.dnf.QueryBuilder; import tools.refinery.logic.dnf.RelationalQuery; import tools.refinery.logic.literal.Literal; import tools.refinery.logic.term.NodeVariable; import tools.refinery.logic.term.Variable; import tools.refinery.logic.term.uppercardinality.FiniteUpperCardinality; +import tools.refinery.store.reasoning.literal.CountCandidateLowerBoundLiteral; import tools.refinery.store.reasoning.literal.CountLowerBoundLiteral; import tools.refinery.store.reasoning.representation.PartialRelation; import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; @@ -21,6 +23,7 @@ import java.util.List; import static tools.refinery.logic.literal.Literals.check; import static tools.refinery.logic.term.int_.IntTerms.constant; import static tools.refinery.logic.term.int_.IntTerms.less; +import static tools.refinery.store.reasoning.literal.PartialLiterals.candidateMay; import static tools.refinery.store.reasoning.literal.PartialLiterals.may; class CrossReferenceUtils { @@ -30,6 +33,34 @@ class CrossReferenceUtils { public static RelationalQuery createMayHelper(PartialRelation linkType, PartialRelation type, Multiplicity multiplicity, boolean inverse) { + var preparedBuilder = prepareBuilder(linkType, inverse); + var literals = new ArrayList(); + literals.add(may(type.call(preparedBuilder.variable()))); + if (multiplicity.multiplicity().upperBound() instanceof FiniteUpperCardinality(var finiteUpperBound)) { + var existingLinks = Variable.of("existingLinks", Integer.class); + literals.add(new CountLowerBoundLiteral(existingLinks, linkType, preparedBuilder.arguments())); + literals.add(check(less(existingLinks, constant(finiteUpperBound)))); + } + return preparedBuilder.builder().clause(literals).build(); + } + + public static RelationalQuery createCandidateMayHelper(PartialRelation linkType, PartialRelation type, + Multiplicity multiplicity, boolean inverse) { + var preparedBuilder = prepareBuilder(linkType, inverse); + var literals = new ArrayList(); + literals.add(candidateMay(type.call(preparedBuilder.variable()))); + if (multiplicity.multiplicity().upperBound() instanceof FiniteUpperCardinality(var finiteUpperBound)) { + var existingLinks = Variable.of("existingLinks", Integer.class); + literals.add(new CountCandidateLowerBoundLiteral(existingLinks, linkType, preparedBuilder.arguments())); + literals.add(check(less(existingLinks, constant(finiteUpperBound)))); + } + return preparedBuilder.builder().clause(literals).build(); + } + + private record PreparedBuilder(QueryBuilder builder, NodeVariable variable, List arguments) { + } + + private static PreparedBuilder prepareBuilder(PartialRelation linkType, boolean inverse) { String name; NodeVariable variable; List arguments; @@ -44,14 +75,6 @@ class CrossReferenceUtils { } var builder = Query.builder(linkType.name() + "#mayNew" + name); builder.parameter(variable); - var literals = new ArrayList(); - literals.add(may(type.call(variable))); - if (multiplicity.multiplicity().upperBound() instanceof FiniteUpperCardinality finiteUpperCardinality) { - var existingLinks = Variable.of("existingLinks", Integer.class); - literals.add(new CountLowerBoundLiteral(existingLinks, linkType, arguments)); - literals.add(check(less(existingLinks, constant(finiteUpperCardinality.finiteUpperBound())))); - } - builder.clause(literals); - return builder.build(); + return new PreparedBuilder(builder, variable, arguments); } } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInfo.java index 982f835f..ef5bcebb 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInfo.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInfo.java @@ -1,5 +1,5 @@ /* - * SPDX-FileCopyrightText: 2023 The Refinery Authors + * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ @@ -11,7 +11,7 @@ import tools.refinery.logic.term.truthvalue.TruthValue; public record DirectedCrossReferenceInfo(PartialRelation sourceType, Multiplicity sourceMultiplicity, PartialRelation targetType, Multiplicity targetMultiplicity, - TruthValue defaultValue) { + TruthValue defaultValue, boolean partial) { public boolean isConstrained() { return sourceMultiplicity.isConstrained() || targetMultiplicity.isConstrained(); } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java index 5bf1f5ab..1985a43f 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java @@ -1,5 +1,5 @@ /* - * SPDX-FileCopyrightText: 2023 The Refinery Authors + * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ @@ -18,6 +18,7 @@ import tools.refinery.store.reasoning.literal.Concreteness; import tools.refinery.store.reasoning.literal.Modality; import tools.refinery.store.reasoning.representation.PartialRelation; import tools.refinery.store.reasoning.translator.PartialRelationTranslator; +import tools.refinery.store.reasoning.translator.RoundingMode; import tools.refinery.store.reasoning.translator.TranslationException; import tools.refinery.store.reasoning.translator.multiplicity.InvalidMultiplicityErrorTranslator; import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; @@ -42,27 +43,77 @@ public class DirectedCrossReferenceTranslator implements ModelStoreConfiguration @Override public void apply(ModelStoreBuilder storeBuilder) { - var name = linkType.name(); var sourceType = info.sourceType(); var targetType = info.targetType(); - var mayNewSource = createMayHelper(sourceType, info.sourceMultiplicity(), false); - var mayNewTarget = createMayHelper(targetType, info.targetMultiplicity(), true); - var mayName = DnfLifter.decorateName(name, Modality.MAY, Concreteness.PARTIAL); - var defaultValue = info.defaultValue(); if (defaultValue.must()) { throw new TranslationException(linkType, "Unsupported default value %s for directed cross references %s" .formatted(defaultValue, linkType)); } - var translator = PartialRelationTranslator.of(linkType); translator.symbol(symbol); if (defaultValue.may()) { - var forbiddenView = new ForbiddenView(symbol); - translator.may(Query.of(mayName, (builder, source, target) -> { + configureWithDefaultUnknown(translator); + } else { + configureWithDefaultFalse(storeBuilder); + } + translator.refiner(DirectedCrossReferenceRefiner.of(symbol, sourceType, targetType)); + translator.initializer(new DirectedCrossReferenceInitializer(linkType, sourceType, targetType, symbol)); + if (info.partial()) { + translator.roundingMode(RoundingMode.NONE); + } else { + translator.decision(Rule.of(linkType.name(), (builder, source, target) -> builder + .clause( + may(linkType.call(source, target)), + not(candidateMust(linkType.call(source, target))), + not(MULTI_VIEW.call(source)), + not(MULTI_VIEW.call(target)) + ) + .action( + add(linkType, source, target) + ))); + } + storeBuilder.with(translator); + storeBuilder.with(new InvalidMultiplicityErrorTranslator(sourceType, linkType, false, + info.sourceMultiplicity())); + storeBuilder.with(new InvalidMultiplicityErrorTranslator(targetType, linkType, true, + info.targetMultiplicity())); + } + + private void configureWithDefaultUnknown(PartialRelationTranslator translator) { + var name = linkType.name(); + var sourceType = info.sourceType(); + var targetType = info.targetType(); + var mayNewSource = createMayHelper(sourceType, info.sourceMultiplicity(), false); + var mayNewTarget = createMayHelper(targetType, info.targetMultiplicity(), true); + var mayName = DnfLifter.decorateName(name, Modality.MAY, Concreteness.PARTIAL); + var forbiddenView = new ForbiddenView(symbol); + translator.may(Query.of(mayName, (builder, source, target) -> { + builder.clause( + mayNewSource.call(source), + mayNewTarget.call(target), + not(forbiddenView.call(source, target)) + ); + if (info.isConstrained()) { + // Violation of monotonicity: + // Edges violating upper multiplicity will not be marked as {@code ERROR}, but the + // corresponding error pattern will already mark the node as invalid. + builder.clause( + must(linkType.call(source, target)), + not(forbiddenView.call(source, target)), + may(sourceType.call(source)), + may(targetType.call(target)) + ); + } + })); + if (info.partial()) { + var candidateMayNewSource = createCandidateMayHelper(sourceType, info.sourceMultiplicity(), false); + var candidateMayNewTarget = createCandidateMayHelper(targetType, info.targetMultiplicity(), true); + var candidateMayName = DnfLifter.decorateName(name, Modality.MAY, Concreteness.CANDIDATE); + translator.candidateMay(Query.of(candidateMayName, (builder, source, target) -> { builder.clause( - mayNewSource.call(source), - mayNewTarget.call(target), + candidateMayNewSource.call(source), + candidateMayNewTarget.call(target), not(forbiddenView.call(source, target)) ); if (info.isConstrained()) { @@ -70,63 +121,56 @@ public class DirectedCrossReferenceTranslator implements ModelStoreConfiguration // Edges violating upper multiplicity will not be marked as {@code ERROR}, but the // corresponding error pattern will already mark the node as invalid. builder.clause( - must(linkType.call(source, target)), + candidateMust(linkType.call(source, target)), not(forbiddenView.call(source, target)), - may(sourceType.call(source)), - may(targetType.call(target)) + candidateMay(sourceType.call(source)), + candidateMay(targetType.call(target)) ); } })); - } else { - var propagationBuilder = storeBuilder.getAdapter(PropagationBuilder.class); - propagationBuilder.rule(Rule.of(name + "#invalidLink", (builder, p1, p2) -> { + } + } + + private RelationalQuery createMayHelper(PartialRelation type, Multiplicity multiplicity, boolean inverse) { + return CrossReferenceUtils.createMayHelper(linkType, type, multiplicity, inverse); + } + + private RelationalQuery createCandidateMayHelper(PartialRelation type, Multiplicity multiplicity, boolean inverse) { + return CrossReferenceUtils.createCandidateMayHelper(linkType, type, multiplicity, inverse); + } + + private void configureWithDefaultFalse(ModelStoreBuilder storeBuilder) { + var name = linkType.name(); + var sourceType = info.sourceType(); + var targetType = info.targetType(); + var mayNewSource = createMayHelper(sourceType, info.sourceMultiplicity(), false); + var mayNewTarget = createMayHelper(targetType, info.targetMultiplicity(), true); + var propagationBuilder = storeBuilder.getAdapter(PropagationBuilder.class); + propagationBuilder.rule(Rule.of(name + "#invalidLink", (builder, p1, p2) -> { + builder.clause( + may(linkType.call(p1, p2)), + not(may(sourceType.call(p1))) + ); + builder.clause( + may(linkType.call(p1, p2)), + not(may(targetType.call(p2))) + ); + if (info.isConstrained()) { builder.clause( may(linkType.call(p1, p2)), - not(may(sourceType.call(p1))) + not(must(linkType.call(p1, p2))), + not(mayNewSource.call(p1)) ); builder.clause( may(linkType.call(p1, p2)), - not(may(targetType.call(p2))) + not(must(linkType.call(p1, p2))), + not(mayNewTarget.call(p2)) ); - if (info.isConstrained()) { - builder.clause( - may(linkType.call(p1, p2)), - not(must(linkType.call(p1, p2))), - not(mayNewSource.call(p1)) - ); - builder.clause( - may(linkType.call(p1, p2)), - not(must(linkType.call(p1, p2))), - not(mayNewTarget.call(p2)) - ); - } - builder.action( - merge(linkType, TruthValue.FALSE, p1, p2) - ); - })); - } - translator.refiner(DirectedCrossReferenceRefiner.of(symbol, sourceType, targetType)); - translator.initializer(new DirectedCrossReferenceInitializer(linkType, sourceType, targetType, symbol)); - translator.decision(Rule.of(linkType.name(), (builder, source, target) -> builder - .clause( - may(linkType.call(source, target)), - not(candidateMust(linkType.call(source, target))), - not(MULTI_VIEW.call(source)), - not(MULTI_VIEW.call(target)) - ) - .action( - add(linkType, source, target) - ))); - storeBuilder.with(translator); - - storeBuilder.with(new InvalidMultiplicityErrorTranslator(sourceType, linkType, false, - info.sourceMultiplicity())); - - storeBuilder.with(new InvalidMultiplicityErrorTranslator(targetType, linkType, true, - info.targetMultiplicity())); + } + builder.action( + merge(linkType, TruthValue.FALSE, p1, p2) + ); + })); } - private RelationalQuery createMayHelper(PartialRelation type, Multiplicity multiplicity, boolean inverse) { - return CrossReferenceUtils.createMayHelper(linkType, type, multiplicity, inverse); - } } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInfo.java index 560eb04a..78b9cd86 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInfo.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInfo.java @@ -1,5 +1,5 @@ /* - * SPDX-FileCopyrightText: 2023 The Refinery Authors + * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ @@ -9,7 +9,8 @@ import tools.refinery.store.reasoning.representation.PartialRelation; import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; import tools.refinery.logic.term.truthvalue.TruthValue; -public record UndirectedCrossReferenceInfo(PartialRelation type, Multiplicity multiplicity, TruthValue defaultValue) { +public record UndirectedCrossReferenceInfo(PartialRelation type, Multiplicity multiplicity, TruthValue defaultValue, + boolean partial) { public boolean isConstrained() { return multiplicity.isConstrained(); } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java index 97c0b800..af0ddd2e 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java @@ -1,25 +1,26 @@ /* - * SPDX-FileCopyrightText: 2023 The Refinery Authors + * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ package tools.refinery.store.reasoning.translator.crossreference; +import tools.refinery.logic.dnf.Query; +import tools.refinery.logic.term.truthvalue.TruthValue; import tools.refinery.store.dse.propagation.PropagationBuilder; import tools.refinery.store.dse.transition.Rule; import tools.refinery.store.model.ModelStoreBuilder; import tools.refinery.store.model.ModelStoreConfiguration; -import tools.refinery.logic.dnf.Query; import tools.refinery.store.query.view.ForbiddenView; import tools.refinery.store.reasoning.lifting.DnfLifter; import tools.refinery.store.reasoning.literal.Concreteness; import tools.refinery.store.reasoning.literal.Modality; import tools.refinery.store.reasoning.representation.PartialRelation; import tools.refinery.store.reasoning.translator.PartialRelationTranslator; +import tools.refinery.store.reasoning.translator.RoundingMode; import tools.refinery.store.reasoning.translator.TranslationException; import tools.refinery.store.reasoning.translator.multiplicity.InvalidMultiplicityErrorTranslator; import tools.refinery.store.representation.Symbol; -import tools.refinery.logic.term.truthvalue.TruthValue; import static tools.refinery.logic.literal.Literals.not; import static tools.refinery.store.reasoning.actions.PartialActionLiterals.add; @@ -40,73 +41,106 @@ public class UndirectedCrossReferenceTranslator implements ModelStoreConfigurati @Override public void apply(ModelStoreBuilder storeBuilder) { - var name = linkType.name(); var type = info.type(); - var mayName = DnfLifter.decorateName(name, Modality.MAY, Concreteness.PARTIAL); - var defaultValue = info.defaultValue(); if (defaultValue.must()) { throw new TranslationException(linkType, "Unsupported default value %s for directed cross references %s" .formatted(defaultValue, linkType)); } - - var mayNewSource = CrossReferenceUtils.createMayHelper(linkType, type, info.multiplicity(), false); - var translator = PartialRelationTranslator.of(linkType); translator.symbol(symbol); if (defaultValue.may()) { - var forbiddenView = new ForbiddenView(symbol); - translator.may(Query.of(mayName, (builder, source, target) -> { + configureWithDefaultUnknown(translator); + } else { + configureWithDefaultFalse(storeBuilder); + } + translator.refiner(UndirectedCrossReferenceRefiner.of(symbol, type)); + translator.initializer(new UndirectedCrossReferenceInitializer(linkType, type, symbol)); + if (info.partial()) { + translator.roundingMode(RoundingMode.NONE); + } else { + translator.decision(Rule.of(linkType.name(), (builder, source, target) -> builder + .clause( + may(linkType.call(source, target)), + not(candidateMust(linkType.call(source, target))), + not(MULTI_VIEW.call(source)), + not(MULTI_VIEW.call(target)) + ) + .action( + add(linkType, source, target) + ))); + } + storeBuilder.with(translator); + storeBuilder.with(new InvalidMultiplicityErrorTranslator(type, linkType, false, info.multiplicity())); + } + + private void configureWithDefaultUnknown(PartialRelationTranslator translator) { + var name = linkType.name(); + var type = info.type(); + var multiplicity = info.multiplicity(); + var mayName = DnfLifter.decorateName(name, Modality.MAY, Concreteness.PARTIAL); + var mayNewSource = CrossReferenceUtils.createMayHelper(linkType, type, multiplicity, false); + var forbiddenView = new ForbiddenView(symbol); + translator.may(Query.of(mayName, (builder, source, target) -> { + builder.clause( + mayNewSource.call(source), + mayNewSource.call(target), + not(forbiddenView.call(source, target)) + ); + if (info.isConstrained()) { + // Violation of monotonicity: + // Edges violating upper multiplicity will not be marked as {@code ERROR}, but the + // corresponding error pattern will already mark the node as invalid. + builder.clause( + must(linkType.call(source, target)), + not(forbiddenView.call(source, target)), + may(type.call(source)), + may(type.call(target)) + ); + } + })); + if (info.partial()) { + var candidateMayName = DnfLifter.decorateName(name, Modality.MAY, Concreteness.CANDIDATE); + var candidateMayNewSource = CrossReferenceUtils.createCandidateMayHelper(linkType, type, multiplicity, + false); + translator.candidateMay(Query.of(candidateMayName, (builder, source, target) -> { builder.clause( - mayNewSource.call(source), - mayNewSource.call(target), + candidateMayNewSource.call(source), + candidateMayNewSource.call(target), not(forbiddenView.call(source, target)) ); if (info.isConstrained()) { - // Violation of monotonicity: - // Edges violating upper multiplicity will not be marked as {@code ERROR}, but the - // corresponding error pattern will already mark the node as invalid. builder.clause( - must(linkType.call(source, target)), + candidateMust(linkType.call(source, target)), not(forbiddenView.call(source, target)), - may(type.call(source)), - may(type.call(target)) + candidateMay(type.call(source)), + candidateMay(type.call(target)) ); } })); - } else { - var propagationBuilder = storeBuilder.getAdapter(PropagationBuilder.class); - propagationBuilder.rule(Rule.of(name + "#invalidLink", (builder, p1, p2) -> { + } + } + + private void configureWithDefaultFalse(ModelStoreBuilder storeBuilder) { + var name = linkType.name(); + var type = info.type(); + var mayNewSource = CrossReferenceUtils.createMayHelper(linkType, type, info.multiplicity(), false); + var propagationBuilder = storeBuilder.getAdapter(PropagationBuilder.class); + propagationBuilder.rule(Rule.of(name + "#invalidLink", (builder, p1, p2) -> { + builder.clause( + may(linkType.call(p1, p2)), + not(may(type.call(p1))) + ); + if (info.isConstrained()) { builder.clause( may(linkType.call(p1, p2)), - not(may(type.call(p1))) - ); - if (info.isConstrained()) { - builder.clause( - may(linkType.call(p1, p2)), - not(must(linkType.call(p1, p2))), - not(mayNewSource.call(p1)) - ); - } - builder.action( - merge(linkType, TruthValue.FALSE, p1, p2) + not(must(linkType.call(p1, p2))), + not(mayNewSource.call(p1)) ); - })); - } - translator.refiner(UndirectedCrossReferenceRefiner.of(symbol, type)); - translator.initializer(new UndirectedCrossReferenceInitializer(linkType, type, symbol)); - translator.decision(Rule.of(linkType.name(), (builder, source, target) -> builder - .clause( - may(linkType.call(source, target)), - not(candidateMust(linkType.call(source, target))), - not(MULTI_VIEW.call(source)), - not(MULTI_VIEW.call(target)) - ) - .action( - add(linkType, source, target) - ))); - storeBuilder.with(translator); - - storeBuilder.with(new InvalidMultiplicityErrorTranslator(type, linkType, false, info.multiplicity())); + } + builder.action( + merge(linkType, TruthValue.FALSE, p1, p2) + ); + })); } } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilder.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilder.java index d1979b8c..94bf1c5d 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilder.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilder.java @@ -1,5 +1,5 @@ /* - * SPDX-FileCopyrightText: 2023 The Refinery Authors + * SPDX-FileCopyrightText: 2023-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ @@ -143,7 +143,7 @@ public class MetamodelBuilder { targetType, linkType, sourceType)); } undirectedCrossReferences.put(linkType, new UndirectedCrossReferenceInfo(sourceType, - info.multiplicity(), defaultValue)); + info.multiplicity(), defaultValue, info.partial())); return; } oppositeReferences.put(opposite, linkType); @@ -153,7 +153,7 @@ public class MetamodelBuilder { return; } directedCrossReferences.put(linkType, new DirectedCrossReferenceInfo(sourceType, info.multiplicity(), - targetType, targetMultiplicity, defaultValue)); + targetType, targetMultiplicity, defaultValue, info.partial())); } private void processContainmentInfo(PartialRelation linkType, ReferenceInfo info, @@ -197,5 +197,9 @@ public class MetamodelBuilder { throw new TranslationException(opposite, "Opposite %s of containment %s cannot be containment" .formatted(opposite, linkType)); } + if (info.partial() != oppositeInfo.partial()) { + throw new TranslationException(opposite, "Either both %s and %s have to be partial or neither of them" + .formatted(opposite, linkType)); + } } } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfo.java index 47a2e95f..94050dc0 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfo.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfo.java @@ -10,7 +10,14 @@ import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity; import tools.refinery.logic.term.truthvalue.TruthValue; public record ReferenceInfo(boolean containment, PartialRelation sourceType, Multiplicity multiplicity, - PartialRelation targetType, PartialRelation opposite, TruthValue defaultValue) { + PartialRelation targetType, PartialRelation opposite, TruthValue defaultValue, + boolean partial) { + public ReferenceInfo { + if (containment && partial) { + throw new IllegalArgumentException("Containment references cannot be partial"); + } + } + public static ReferenceInfoBuilder builder() { return new ReferenceInfoBuilder(); } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfoBuilder.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfoBuilder.java index 39240d6b..90fb22b5 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfoBuilder.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfoBuilder.java @@ -21,6 +21,7 @@ public final class ReferenceInfoBuilder { private PartialRelation targetType; private PartialRelation opposite; private TruthValue defaultValue = TruthValue.UNKNOWN; + private boolean partial; ReferenceInfoBuilder() { } @@ -72,6 +73,11 @@ public final class ReferenceInfoBuilder { return this; } + public ReferenceInfoBuilder partial(boolean partial) { + this.partial = partial; + return this; + } + public ReferenceInfo build() { if (sourceType == null) { throw new IllegalStateException("Source type is required"); @@ -79,6 +85,6 @@ public final class ReferenceInfoBuilder { if (targetType == null) { throw new IllegalStateException("Target type is required"); } - return new ReferenceInfo(containment, sourceType, multiplicity, targetType, opposite, defaultValue); + return new ReferenceInfo(containment, sourceType, multiplicity, targetType, opposite, defaultValue, partial); } } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/InvalidMultiplicityErrorTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/InvalidMultiplicityErrorTranslator.java index 0ca6eac2..e2eff921 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/InvalidMultiplicityErrorTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/InvalidMultiplicityErrorTranslator.java @@ -1,5 +1,5 @@ /* - * SPDX-FileCopyrightText: 2023 The Refinery Authors + * SPDX-FileCopyrightText: 20232-2024 The Refinery Authors * * SPDX-License-Identifier: EPL-2.0 */ @@ -52,12 +52,11 @@ public class InvalidMultiplicityErrorTranslator implements ModelStoreConfigurati @Override public void apply(ModelStoreBuilder storeBuilder) { - if (!(multiplicity instanceof ConstrainedMultiplicity constrainedMultiplicity)) { + if (!(multiplicity instanceof ConstrainedMultiplicity(var cardinalityInterval, var errorSymbol))) { return; } - var name = constrainedMultiplicity.errorSymbol().name(); - var cardinalityInterval = constrainedMultiplicity.multiplicity(); + var name = errorSymbol.name(); var node = Variable.of("node"); var other = Variable.of("other"); List arguments = inverse ? List.of(other, node) : List.of(node, other); @@ -98,8 +97,7 @@ public class InvalidMultiplicityErrorTranslator implements ModelStoreConfigurati )); } - if (cardinalityInterval.upperBound() instanceof FiniteUpperCardinality finiteUpperCardinality) { - int upperBound = finiteUpperCardinality.finiteUpperBound(); + if (cardinalityInterval.upperBound() instanceof FiniteUpperCardinality(int upperBound)) { mustBuilder.clause(Integer.class, existingContents -> List.of( must(nodeType.call(node)), new CountLowerBoundLiteral(existingContents, linkType, arguments), @@ -128,7 +126,7 @@ public class InvalidMultiplicityErrorTranslator implements ModelStoreConfigurati output.assign(missingBuilder.build().aggregate(INT_SUM, Variable.of())) )); - storeBuilder.with(PartialRelationTranslator.of(constrainedMultiplicity.errorSymbol()) + storeBuilder.with(PartialRelationTranslator.of(errorSymbol) .mayNever() .must(mustBuilder.build()) .candidateMay(candidateMayBuilder.build()) -- cgit v1.2.3-54-g00ecf