diff options
author | Kristóf Marussy <kristof@marussy.com> | 2023-07-25 16:06:36 +0200 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2023-07-25 16:06:36 +0200 |
commit | 6a25ba145844c79d3507f8eabdbed854be2b8097 (patch) | |
tree | 0ea9d4c7a9b5b94a0d4341eaa25eeb7e4d3f4f56 /subprojects/store/src | |
parent | feat: custom connected component RETE node (diff) | |
download | refinery-6a25ba145844c79d3507f8eabdbed854be2b8097.tar.gz refinery-6a25ba145844c79d3507f8eabdbed854be2b8097.tar.zst refinery-6a25ba145844c79d3507f8eabdbed854be2b8097.zip |
feat: concrete count in partial models
Diffstat (limited to 'subprojects/store/src')
6 files changed, 76 insertions, 11 deletions
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/CardinalityDomain.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/CardinalityDomain.java new file mode 100644 index 00000000..7ae2d935 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/CardinalityDomain.java | |||
@@ -0,0 +1,68 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.store.representation.cardinality; | ||
7 | |||
8 | import tools.refinery.store.representation.AbstractDomain; | ||
9 | |||
10 | import java.util.Optional; | ||
11 | |||
12 | // Singleton pattern, because there is only one domain for truth values. | ||
13 | @SuppressWarnings("squid:S6548") | ||
14 | public class CardinalityDomain implements AbstractDomain<CardinalityInterval, Integer> { | ||
15 | public static final CardinalityDomain INSTANCE = new CardinalityDomain(); | ||
16 | |||
17 | private CardinalityDomain() { | ||
18 | } | ||
19 | |||
20 | @Override | ||
21 | public Class<CardinalityInterval> abstractType() { | ||
22 | return CardinalityInterval.class; | ||
23 | } | ||
24 | |||
25 | @Override | ||
26 | public Class<Integer> concreteType() { | ||
27 | return Integer.class; | ||
28 | } | ||
29 | |||
30 | @Override | ||
31 | public CardinalityInterval toAbstract(Integer concreteValue) { | ||
32 | return CardinalityIntervals.exactly(concreteValue); | ||
33 | } | ||
34 | |||
35 | @Override | ||
36 | public Optional<Integer> toConcrete(CardinalityInterval abstractValue) { | ||
37 | return isConcrete(abstractValue) ? Optional.of(abstractValue.lowerBound()) : Optional.empty(); | ||
38 | } | ||
39 | |||
40 | @Override | ||
41 | public boolean isConcrete(CardinalityInterval abstractValue) { | ||
42 | if (!(abstractValue instanceof NonEmptyCardinalityInterval nonEmptyValue) || | ||
43 | !((nonEmptyValue.upperBound()) instanceof FiniteUpperCardinality finiteUpperCardinality)) { | ||
44 | return false; | ||
45 | } | ||
46 | return nonEmptyValue.lowerBound() == finiteUpperCardinality.finiteUpperBound(); | ||
47 | } | ||
48 | |||
49 | @Override | ||
50 | public CardinalityInterval commonRefinement(CardinalityInterval leftValue, CardinalityInterval rightValue) { | ||
51 | return leftValue.meet(rightValue); | ||
52 | } | ||
53 | |||
54 | @Override | ||
55 | public CardinalityInterval commonAncestor(CardinalityInterval leftValue, CardinalityInterval rightValue) { | ||
56 | return leftValue.join(rightValue); | ||
57 | } | ||
58 | |||
59 | @Override | ||
60 | public CardinalityInterval unknown() { | ||
61 | return CardinalityIntervals.SET; | ||
62 | } | ||
63 | |||
64 | @Override | ||
65 | public boolean isError(CardinalityInterval abstractValue) { | ||
66 | return abstractValue.isEmpty(); | ||
67 | } | ||
68 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/CardinalityIntervals.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/CardinalityIntervals.java index ad16a3e8..855fd248 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/CardinalityIntervals.java +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/CardinalityIntervals.java | |||
@@ -30,7 +30,7 @@ public final class CardinalityIntervals { | |||
30 | } | 30 | } |
31 | 31 | ||
32 | public static CardinalityInterval between(int lowerBound, int upperBound) { | 32 | public static CardinalityInterval between(int lowerBound, int upperBound) { |
33 | return between(lowerBound, UpperCardinalities.valueOf(upperBound)); | 33 | return between(lowerBound, UpperCardinalities.atMost(upperBound)); |
34 | } | 34 | } |
35 | 35 | ||
36 | public static CardinalityInterval atMost(UpperCardinality upperBound) { | 36 | public static CardinalityInterval atMost(UpperCardinality upperBound) { |
@@ -38,7 +38,7 @@ public final class CardinalityIntervals { | |||
38 | } | 38 | } |
39 | 39 | ||
40 | public static CardinalityInterval atMost(int upperBound) { | 40 | public static CardinalityInterval atMost(int upperBound) { |
41 | return atMost(UpperCardinalities.valueOf(upperBound)); | 41 | return atMost(UpperCardinalities.atMost(upperBound)); |
42 | } | 42 | } |
43 | 43 | ||
44 | public static CardinalityInterval atLeast(int lowerBound) { | 44 | public static CardinalityInterval atLeast(int lowerBound) { |
@@ -46,6 +46,6 @@ public final class CardinalityIntervals { | |||
46 | } | 46 | } |
47 | 47 | ||
48 | public static CardinalityInterval exactly(int lowerBound) { | 48 | public static CardinalityInterval exactly(int lowerBound) { |
49 | return new NonEmptyCardinalityInterval(lowerBound, UpperCardinalities.valueOf(lowerBound)); | 49 | return new NonEmptyCardinalityInterval(lowerBound, UpperCardinalities.atMost(lowerBound)); |
50 | } | 50 | } |
51 | } | 51 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/FiniteUpperCardinality.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/FiniteUpperCardinality.java index acd82beb..088e3925 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/FiniteUpperCardinality.java +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/FiniteUpperCardinality.java | |||
@@ -59,7 +59,7 @@ public record FiniteUpperCardinality(int finiteUpperBound) implements UpperCardi | |||
59 | 59 | ||
60 | private UpperCardinality lift(@NotNull UpperCardinality other, IntBinaryOperator operator) { | 60 | private UpperCardinality lift(@NotNull UpperCardinality other, IntBinaryOperator operator) { |
61 | if (other instanceof FiniteUpperCardinality finiteUpperCardinality) { | 61 | if (other instanceof FiniteUpperCardinality finiteUpperCardinality) { |
62 | return UpperCardinalities.valueOf(operator.applyAsInt(finiteUpperBound, | 62 | return UpperCardinalities.atMost(operator.applyAsInt(finiteUpperBound, |
63 | finiteUpperCardinality.finiteUpperBound)); | 63 | finiteUpperCardinality.finiteUpperBound)); |
64 | } | 64 | } |
65 | if (other instanceof UnboundedUpperCardinality) { | 65 | if (other instanceof UnboundedUpperCardinality) { |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UpperCardinalities.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UpperCardinalities.java index 1e18dde0..17d1b292 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UpperCardinalities.java +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UpperCardinalities.java | |||
@@ -26,7 +26,7 @@ public final class UpperCardinalities { | |||
26 | throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); | 26 | throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); |
27 | } | 27 | } |
28 | 28 | ||
29 | public static UpperCardinality valueOf(int upperBound) { | 29 | public static UpperCardinality atMost(int upperBound) { |
30 | if (upperBound < 0) { | 30 | if (upperBound < 0) { |
31 | return UNBOUNDED; | 31 | return UNBOUNDED; |
32 | } | 32 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UpperCardinality.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UpperCardinality.java index 5600ab4c..3f0db028 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UpperCardinality.java +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UpperCardinality.java | |||
@@ -27,6 +27,6 @@ public sealed interface UpperCardinality extends Comparable<UpperCardinality> pe | |||
27 | int compareToInt(int value); | 27 | int compareToInt(int value); |
28 | 28 | ||
29 | static UpperCardinality of(int upperBound) { | 29 | static UpperCardinality of(int upperBound) { |
30 | return UpperCardinalities.valueOf(upperBound); | 30 | return UpperCardinalities.atMost(upperBound); |
31 | } | 31 | } |
32 | } | 32 | } |
diff --git a/subprojects/store/src/test/java/tools/refinery/store/representation/cardinality/UpperCardinalitiesTest.java b/subprojects/store/src/test/java/tools/refinery/store/representation/cardinality/UpperCardinalitiesTest.java index e61f7b36..e403eec2 100644 --- a/subprojects/store/src/test/java/tools/refinery/store/representation/cardinality/UpperCardinalitiesTest.java +++ b/subprojects/store/src/test/java/tools/refinery/store/representation/cardinality/UpperCardinalitiesTest.java | |||
@@ -8,9 +8,6 @@ package tools.refinery.store.representation.cardinality; | |||
8 | import org.junit.jupiter.api.Test; | 8 | import org.junit.jupiter.api.Test; |
9 | import org.junit.jupiter.params.ParameterizedTest; | 9 | import org.junit.jupiter.params.ParameterizedTest; |
10 | import org.junit.jupiter.params.provider.ValueSource; | 10 | import org.junit.jupiter.params.provider.ValueSource; |
11 | import tools.refinery.store.representation.cardinality.FiniteUpperCardinality; | ||
12 | import tools.refinery.store.representation.cardinality.UnboundedUpperCardinality; | ||
13 | import tools.refinery.store.representation.cardinality.UpperCardinalities; | ||
14 | 11 | ||
15 | import static org.hamcrest.MatcherAssert.assertThat; | 12 | import static org.hamcrest.MatcherAssert.assertThat; |
16 | import static org.hamcrest.Matchers.equalTo; | 13 | import static org.hamcrest.Matchers.equalTo; |
@@ -20,14 +17,14 @@ class UpperCardinalitiesTest { | |||
20 | @ParameterizedTest | 17 | @ParameterizedTest |
21 | @ValueSource(ints = {0, 1, 255, 256, 1000, Integer.MAX_VALUE}) | 18 | @ValueSource(ints = {0, 1, 255, 256, 1000, Integer.MAX_VALUE}) |
22 | void valueOfBoundedTest(int value) { | 19 | void valueOfBoundedTest(int value) { |
23 | var upperCardinality = UpperCardinalities.valueOf(value); | 20 | var upperCardinality = UpperCardinalities.atMost(value); |
24 | assertThat(upperCardinality, instanceOf(FiniteUpperCardinality.class)); | 21 | assertThat(upperCardinality, instanceOf(FiniteUpperCardinality.class)); |
25 | assertThat(((FiniteUpperCardinality) upperCardinality).finiteUpperBound(), equalTo(value)); | 22 | assertThat(((FiniteUpperCardinality) upperCardinality).finiteUpperBound(), equalTo(value)); |
26 | } | 23 | } |
27 | 24 | ||
28 | @Test | 25 | @Test |
29 | void valueOfUnboundedTest() { | 26 | void valueOfUnboundedTest() { |
30 | var upperCardinality = UpperCardinalities.valueOf(-1); | 27 | var upperCardinality = UpperCardinalities.atMost(-1); |
31 | assertThat(upperCardinality, instanceOf(UnboundedUpperCardinality.class)); | 28 | assertThat(upperCardinality, instanceOf(UnboundedUpperCardinality.class)); |
32 | } | 29 | } |
33 | } | 30 | } |