diff options
author | Kristóf Marussy <kristof@marussy.com> | 2024-07-02 20:08:33 +0200 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2024-07-02 20:44:48 +0200 |
commit | d5b54f9b3f07bf6b2e044ad0b35176c4f428077e (patch) | |
tree | 87b5423ade2a8ca82402ddd4df925c75deaa7e2f /subprojects/store-reasoning/src/main | |
parent | fix(semantics): traceability for internal rules (diff) | |
download | refinery-d5b54f9b3f07bf6b2e044ad0b35176c4f428077e.tar.gz refinery-d5b54f9b3f07bf6b2e044ad0b35176c4f428077e.tar.zst refinery-d5b54f9b3f07bf6b2e044ad0b35176c4f428077e.zip |
fix(reasoning): do not propagate invalidated objects
Diffstat (limited to 'subprojects/store-reasoning/src/main')
4 files changed, 80 insertions, 19 deletions
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java index e8e6880a..18f238d7 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java | |||
@@ -36,8 +36,4 @@ public final class PartialActionLiterals { | |||
36 | public static FocusActionLiteral focus(NodeVariable parent, NodeVariable child) { | 36 | public static FocusActionLiteral focus(NodeVariable parent, NodeVariable child) { |
37 | return new FocusActionLiteral(parent, child); | 37 | return new FocusActionLiteral(parent, child); |
38 | } | 38 | } |
39 | |||
40 | public static CleanupActionLiteral cleanup(NodeVariable node) { | ||
41 | return new CleanupActionLiteral(node); | ||
42 | } | ||
43 | } | 39 | } |
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 be9fcb9d..41d185d7 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 | |||
@@ -30,10 +30,10 @@ import static tools.refinery.logic.literal.Literals.check; | |||
30 | import static tools.refinery.logic.literal.Literals.not; | 30 | import static tools.refinery.logic.literal.Literals.not; |
31 | import static tools.refinery.logic.term.int_.IntTerms.constant; | 31 | import static tools.refinery.logic.term.int_.IntTerms.constant; |
32 | import static tools.refinery.logic.term.int_.IntTerms.less; | 32 | import static tools.refinery.logic.term.int_.IntTerms.less; |
33 | import static tools.refinery.store.reasoning.ReasoningAdapter.EQUALS_SYMBOL; | ||
33 | import static tools.refinery.store.reasoning.actions.PartialActionLiterals.add; | 34 | import static tools.refinery.store.reasoning.actions.PartialActionLiterals.add; |
34 | import static tools.refinery.store.reasoning.actions.PartialActionLiterals.remove; | 35 | import static tools.refinery.store.reasoning.actions.PartialActionLiterals.remove; |
35 | import static tools.refinery.store.reasoning.literal.PartialLiterals.*; | 36 | import static tools.refinery.store.reasoning.literal.PartialLiterals.*; |
36 | import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW; | ||
37 | 37 | ||
38 | public class CrossReferenceUtils { | 38 | public class CrossReferenceUtils { |
39 | private CrossReferenceUtils() { | 39 | private CrossReferenceUtils() { |
@@ -93,7 +93,6 @@ public class CrossReferenceUtils { | |||
93 | var lowerBoundCardinality = UpperCardinalities.atMost(lowerBound); | 93 | var lowerBoundCardinality = UpperCardinalities.atMost(lowerBound); |
94 | propagationBuilder.rule(Rule.of(name + "#lowerSource", (builder, p1, p2) -> builder | 94 | propagationBuilder.rule(Rule.of(name + "#lowerSource", (builder, p1, p2) -> builder |
95 | .clause(UpperCardinality.class, upperBound -> List.of( | 95 | .clause(UpperCardinality.class, upperBound -> List.of( |
96 | not(MULTI_VIEW.call(p1)), | ||
97 | must(sourceType.call(p1)), | 96 | must(sourceType.call(p1)), |
98 | new CountUpperBoundLiteral(upperBound, linkType, List.of(p1, Variable.of())), | 97 | new CountUpperBoundLiteral(upperBound, linkType, List.of(p1, Variable.of())), |
99 | check(UpperCardinalityTerms.lessEq(upperBound, | 98 | check(UpperCardinalityTerms.lessEq(upperBound, |
@@ -127,7 +126,6 @@ public class CrossReferenceUtils { | |||
127 | var lowerBoundCardinality = UpperCardinalities.atMost(lowerBound); | 126 | var lowerBoundCardinality = UpperCardinalities.atMost(lowerBound); |
128 | propagationBuilder.rule(Rule.of(name + "#lowerTarget", (builder, p1, p2) -> builder | 127 | propagationBuilder.rule(Rule.of(name + "#lowerTarget", (builder, p1, p2) -> builder |
129 | .clause(UpperCardinality.class, upperBound -> List.of( | 128 | .clause(UpperCardinality.class, upperBound -> List.of( |
130 | not(MULTI_VIEW.call(p2)), | ||
131 | must(targetType.call(p2)), | 129 | must(targetType.call(p2)), |
132 | new CountUpperBoundLiteral(upperBound, linkType, List.of(Variable.of(), p2)), | 130 | new CountUpperBoundLiteral(upperBound, linkType, List.of(Variable.of(), p2)), |
133 | check(UpperCardinalityTerms.lessEq(upperBound, | 131 | check(UpperCardinalityTerms.lessEq(upperBound, |
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/CleanupPropagator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/CleanupPropagator.java new file mode 100644 index 00000000..f14b4783 --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/CleanupPropagator.java | |||
@@ -0,0 +1,78 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.reasoning.translator.multiobject; | ||
7 | |||
8 | import tools.refinery.logic.dnf.Query; | ||
9 | import tools.refinery.logic.dnf.RelationalQuery; | ||
10 | import tools.refinery.logic.term.uppercardinality.UpperCardinalities; | ||
11 | import tools.refinery.logic.term.uppercardinality.UpperCardinality; | ||
12 | import tools.refinery.logic.term.uppercardinality.UpperCardinalityTerms; | ||
13 | import tools.refinery.store.dse.propagation.BoundPropagator; | ||
14 | import tools.refinery.store.dse.propagation.PropagationResult; | ||
15 | import tools.refinery.store.dse.propagation.Propagator; | ||
16 | import tools.refinery.store.model.Model; | ||
17 | import tools.refinery.store.model.ModelStoreBuilder; | ||
18 | import tools.refinery.store.query.ModelQueryAdapter; | ||
19 | import tools.refinery.store.query.ModelQueryBuilder; | ||
20 | import tools.refinery.store.query.resultset.ResultSet; | ||
21 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
22 | |||
23 | import java.util.List; | ||
24 | |||
25 | import static tools.refinery.logic.literal.Literals.check; | ||
26 | import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.UPPER_CARDINALITY_VIEW; | ||
27 | |||
28 | /** | ||
29 | * Clean up non-existing objects in a separate propagator to avoid interference with propagation rules that assume | ||
30 | * that each object in their activation set is still part of the model when they are called. | ||
31 | */ | ||
32 | public class CleanupPropagator implements Propagator { | ||
33 | private static final RelationalQuery CLEANUP_QUERY = Query.of("exists#cleanup", (builder, node) -> builder | ||
34 | .clause(UpperCardinality.class, upper -> List.of( | ||
35 | UPPER_CARDINALITY_VIEW.call(node, upper), | ||
36 | check(UpperCardinalityTerms.less(upper, | ||
37 | UpperCardinalityTerms.constant(UpperCardinalities.ONE))) | ||
38 | )) | ||
39 | ); | ||
40 | |||
41 | @Override | ||
42 | public void configure(ModelStoreBuilder storeBuilder) { | ||
43 | storeBuilder.getAdapter(ModelQueryBuilder.class).query(CLEANUP_QUERY); | ||
44 | } | ||
45 | |||
46 | @Override | ||
47 | public BoundPropagator bindToModel(Model model) { | ||
48 | return new BoundCleanupPropagator(model); | ||
49 | } | ||
50 | |||
51 | private static class BoundCleanupPropagator implements BoundPropagator { | ||
52 | private final Model model; | ||
53 | private final ModelQueryAdapter queryEngine; | ||
54 | private final ResultSet<Boolean> resultSet; | ||
55 | private ReasoningAdapter reasoningAdapter; | ||
56 | |||
57 | public BoundCleanupPropagator(Model model) { | ||
58 | this.model = model; | ||
59 | queryEngine = model.getAdapter(ModelQueryAdapter.class); | ||
60 | resultSet = queryEngine.getResultSet(CLEANUP_QUERY); | ||
61 | } | ||
62 | |||
63 | @Override | ||
64 | public PropagationResult propagateOne() { | ||
65 | if (reasoningAdapter == null) { | ||
66 | reasoningAdapter = model.getAdapter(ReasoningAdapter.class); | ||
67 | } | ||
68 | queryEngine.flushChanges(); | ||
69 | boolean propagated = false; | ||
70 | var cursor = resultSet.getAll(); | ||
71 | while (cursor.move()) { | ||
72 | propagated = true; | ||
73 | reasoningAdapter.cleanup(cursor.getKey().get(0)); | ||
74 | } | ||
75 | return propagated ? PropagationResult.PROPAGATED : PropagationResult.UNCHANGED; | ||
76 | } | ||
77 | } | ||
78 | } | ||
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java index be15b6d7..05d96689 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java | |||
@@ -15,7 +15,6 @@ import tools.refinery.logic.term.uppercardinality.UpperCardinalities; | |||
15 | import tools.refinery.logic.term.uppercardinality.UpperCardinality; | 15 | import tools.refinery.logic.term.uppercardinality.UpperCardinality; |
16 | import tools.refinery.logic.term.uppercardinality.UpperCardinalityTerms; | 16 | import tools.refinery.logic.term.uppercardinality.UpperCardinalityTerms; |
17 | import tools.refinery.store.dse.propagation.PropagationBuilder; | 17 | import tools.refinery.store.dse.propagation.PropagationBuilder; |
18 | import tools.refinery.store.dse.transition.Rule; | ||
19 | import tools.refinery.store.dse.transition.objectives.Criteria; | 18 | import tools.refinery.store.dse.transition.objectives.Criteria; |
20 | import tools.refinery.store.dse.transition.objectives.Objectives; | 19 | import tools.refinery.store.dse.transition.objectives.Objectives; |
21 | import tools.refinery.store.model.ModelStoreBuilder; | 20 | import tools.refinery.store.model.ModelStoreBuilder; |
@@ -23,7 +22,6 @@ import tools.refinery.store.model.ModelStoreConfiguration; | |||
23 | import tools.refinery.store.query.view.AnySymbolView; | 22 | import tools.refinery.store.query.view.AnySymbolView; |
24 | import tools.refinery.store.reasoning.ReasoningAdapter; | 23 | import tools.refinery.store.reasoning.ReasoningAdapter; |
25 | import tools.refinery.store.reasoning.ReasoningBuilder; | 24 | import tools.refinery.store.reasoning.ReasoningBuilder; |
26 | import tools.refinery.store.reasoning.actions.PartialActionLiterals; | ||
27 | import tools.refinery.store.reasoning.representation.PartialFunction; | 25 | import tools.refinery.store.reasoning.representation.PartialFunction; |
28 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; | 26 | import tools.refinery.store.reasoning.translator.PartialRelationTranslator; |
29 | import tools.refinery.store.reasoning.translator.RoundingMode; | 27 | import tools.refinery.store.reasoning.translator.RoundingMode; |
@@ -93,15 +91,6 @@ public class MultiObjectTranslator implements ModelStoreConfiguration { | |||
93 | reasoningBuilder.storageRefiner(COUNT_STORAGE, MultiObjectStorageRefiner::new); | 91 | reasoningBuilder.storageRefiner(COUNT_STORAGE, MultiObjectStorageRefiner::new); |
94 | 92 | ||
95 | storeBuilder.tryGetAdapter(PropagationBuilder.class) | 93 | storeBuilder.tryGetAdapter(PropagationBuilder.class) |
96 | .ifPresent(propagationBuilder -> propagationBuilder.rule( | 94 | .ifPresent(propagationBuilder -> propagationBuilder.propagator(new CleanupPropagator())); |
97 | Rule.of("exists#cleanup", (builder, node) -> builder | ||
98 | .clause(UpperCardinality.class, upper -> List.of( | ||
99 | UPPER_CARDINALITY_VIEW.call(node, upper), | ||
100 | check(UpperCardinalityTerms.less(upper, | ||
101 | UpperCardinalityTerms.constant(UpperCardinalities.ONE))) | ||
102 | )) | ||
103 | .action( | ||
104 | PartialActionLiterals.cleanup(node) | ||
105 | )))); | ||
106 | } | 95 | } |
107 | } | 96 | } |