diff options
20 files changed, 1078 insertions, 34 deletions
diff --git a/subprojects/store/src/main/java/tools/refinery/store/statecoding/Morphism.java b/subprojects/store/src/main/java/tools/refinery/store/statecoding/Morphism.java new file mode 100644 index 00000000..d4ac3b58 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/Morphism.java | |||
@@ -0,0 +1,11 @@ | |||
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.statecoding; | ||
7 | |||
8 | public interface Morphism { | ||
9 | int get(int object); | ||
10 | int getSize(); | ||
11 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/statecoding/ObjectCode.java b/subprojects/store/src/main/java/tools/refinery/store/statecoding/ObjectCode.java new file mode 100644 index 00000000..840253ea --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/ObjectCode.java | |||
@@ -0,0 +1,11 @@ | |||
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.statecoding; | ||
7 | |||
8 | public interface ObjectCode { | ||
9 | long get(int object); | ||
10 | int getSize(); | ||
11 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/statecoding/StateCodeCalculator.java b/subprojects/store/src/main/java/tools/refinery/store/statecoding/StateCodeCalculator.java index 479b61ed..b7f1d81a 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/statecoding/StateCodeCalculator.java +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/StateCodeCalculator.java | |||
@@ -6,5 +6,5 @@ | |||
6 | package tools.refinery.store.statecoding; | 6 | package tools.refinery.store.statecoding; |
7 | 7 | ||
8 | public interface StateCodeCalculator { | 8 | public interface StateCodeCalculator { |
9 | 9 | StateCoderResult calculateCodes(); | |
10 | } | 10 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/statecoding/StateCoderAdapter.java b/subprojects/store/src/main/java/tools/refinery/store/statecoding/StateCoderAdapter.java index 8795fb68..8cfd24d5 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/statecoding/StateCoderAdapter.java +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/StateCoderAdapter.java | |||
@@ -6,7 +6,18 @@ | |||
6 | package tools.refinery.store.statecoding; | 6 | package tools.refinery.store.statecoding; |
7 | 7 | ||
8 | import tools.refinery.store.adapter.ModelAdapter; | 8 | import tools.refinery.store.adapter.ModelAdapter; |
9 | import tools.refinery.store.statecoding.internal.StateCoderBuilderImpl; | ||
9 | 10 | ||
10 | public interface StateCoderAdapter extends ModelAdapter { | 11 | public interface StateCoderAdapter extends ModelAdapter { |
11 | int calculateHashCode(); | 12 | StateCoderResult calculateStateCode(); |
13 | default int calculateModelCode() { | ||
14 | return calculateStateCode().modelCode(); | ||
15 | } | ||
16 | default ObjectCode calculateObjectCode() { | ||
17 | return calculateStateCode().objectCode(); | ||
18 | } | ||
19 | |||
20 | static StateCoderBuilderImpl builder() { | ||
21 | return new StateCoderBuilderImpl(); | ||
22 | } | ||
12 | } | 23 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/statecoding/StateCoderResult.java b/subprojects/store/src/main/java/tools/refinery/store/statecoding/StateCoderResult.java new file mode 100644 index 00000000..d2aff836 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/StateCoderResult.java | |||
@@ -0,0 +1,9 @@ | |||
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.statecoding; | ||
7 | |||
8 | public record StateCoderResult(int modelCode, ObjectCode objectCode) { | ||
9 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/statecoding/StateCoderStoreAdapter.java b/subprojects/store/src/main/java/tools/refinery/store/statecoding/StateCoderStoreAdapter.java index 5946a162..c6509521 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/statecoding/StateCoderStoreAdapter.java +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/StateCoderStoreAdapter.java | |||
@@ -6,9 +6,12 @@ | |||
6 | package tools.refinery.store.statecoding; | 6 | package tools.refinery.store.statecoding; |
7 | 7 | ||
8 | import tools.refinery.store.adapter.ModelStoreAdapter; | 8 | import tools.refinery.store.adapter.ModelStoreAdapter; |
9 | import tools.refinery.store.map.Version; | ||
9 | import tools.refinery.store.model.Model; | 10 | import tools.refinery.store.model.Model; |
10 | 11 | ||
11 | public interface StateCoderStoreAdapter extends ModelStoreAdapter { | 12 | public interface StateCoderStoreAdapter extends ModelStoreAdapter { |
13 | StateEquivalenceChecker.EquivalenceResult checkEquivalence(Version v1, Version v2); | ||
14 | |||
12 | @Override | 15 | @Override |
13 | StateCoderAdapter createModelAdapter(Model model); | 16 | StateCoderAdapter createModelAdapter(Model model); |
14 | } | 17 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/statecoding/StateEquivalenceChecker.java b/subprojects/store/src/main/java/tools/refinery/store/statecoding/StateEquivalenceChecker.java new file mode 100644 index 00000000..6d8dc6c7 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/StateEquivalenceChecker.java | |||
@@ -0,0 +1,22 @@ | |||
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.statecoding; | ||
7 | |||
8 | import tools.refinery.store.model.Interpretation; | ||
9 | |||
10 | import java.util.List; | ||
11 | |||
12 | public interface StateEquivalenceChecker { | ||
13 | enum EquivalenceResult { | ||
14 | ISOMORPHIC, UNKNOWN, DIFFERENT | ||
15 | } | ||
16 | |||
17 | EquivalenceResult constructMorphism( | ||
18 | List<? extends Interpretation<?>> interpretations1, | ||
19 | ObjectCode code1, List<? | ||
20 | extends Interpretation<?>> interpretations2, | ||
21 | ObjectCode code2); | ||
22 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/statecoding/internal/StateCoderAdapterImpl.java b/subprojects/store/src/main/java/tools/refinery/store/statecoding/internal/StateCoderAdapterImpl.java index 689db2e3..b66fc86d 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/statecoding/internal/StateCoderAdapterImpl.java +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/internal/StateCoderAdapterImpl.java | |||
@@ -9,8 +9,10 @@ import tools.refinery.store.adapter.ModelStoreAdapter; | |||
9 | import tools.refinery.store.model.Interpretation; | 9 | import tools.refinery.store.model.Interpretation; |
10 | import tools.refinery.store.model.Model; | 10 | import tools.refinery.store.model.Model; |
11 | import tools.refinery.store.representation.Symbol; | 11 | import tools.refinery.store.representation.Symbol; |
12 | import tools.refinery.store.statecoding.StateCodeCalculator; | ||
12 | import tools.refinery.store.statecoding.StateCoderAdapter; | 13 | import tools.refinery.store.statecoding.StateCoderAdapter; |
13 | import tools.refinery.store.statecoding.neighbourhood.NeighbourhoodCalculator; | 14 | import tools.refinery.store.statecoding.StateCoderResult; |
15 | import tools.refinery.store.statecoding.neighbourhood.LazyNeighbourhoodCalculator; | ||
14 | 16 | ||
15 | import java.util.Collection; | 17 | import java.util.Collection; |
16 | import java.util.List; | 18 | import java.util.List; |
@@ -18,14 +20,14 @@ import java.util.List; | |||
18 | public class StateCoderAdapterImpl implements StateCoderAdapter { | 20 | public class StateCoderAdapterImpl implements StateCoderAdapter { |
19 | final ModelStoreAdapter storeAdapter; | 21 | final ModelStoreAdapter storeAdapter; |
20 | final Model model; | 22 | final Model model; |
21 | final NeighbourhoodCalculator calculator; | 23 | final StateCodeCalculator calculator; |
22 | 24 | ||
23 | StateCoderAdapterImpl(ModelStoreAdapter storeAdapter, Model model, Collection<Symbol<?>> symbols) { | 25 | StateCoderAdapterImpl(ModelStoreAdapter storeAdapter, Model model, Collection<Symbol<?>> symbols) { |
24 | this.storeAdapter = storeAdapter; | 26 | this.storeAdapter = storeAdapter; |
25 | this.model = model; | 27 | this.model = model; |
26 | 28 | ||
27 | List<? extends Interpretation<?>> interpretations = symbols.stream().map(model::getInterpretation).toList(); | 29 | List<? extends Interpretation<?>> interpretations = symbols.stream().map(model::getInterpretation).toList(); |
28 | calculator = new NeighbourhoodCalculator(interpretations); | 30 | calculator = new LazyNeighbourhoodCalculator(interpretations); |
29 | } | 31 | } |
30 | 32 | ||
31 | @Override | 33 | @Override |
@@ -39,9 +41,7 @@ public class StateCoderAdapterImpl implements StateCoderAdapter { | |||
39 | } | 41 | } |
40 | 42 | ||
41 | @Override | 43 | @Override |
42 | public int calculateHashCode() { | 44 | public StateCoderResult calculateStateCode() { |
43 | return calculator.calculate(); | 45 | return calculator.calculateCodes(); |
44 | } | 46 | } |
45 | |||
46 | |||
47 | } | 47 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/statecoding/internal/StateCoderStoreAdapterImpl.java b/subprojects/store/src/main/java/tools/refinery/store/statecoding/internal/StateCoderStoreAdapterImpl.java index 77d36e96..5374755d 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/statecoding/internal/StateCoderStoreAdapterImpl.java +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/internal/StateCoderStoreAdapterImpl.java | |||
@@ -5,18 +5,24 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.statecoding.internal; | 6 | package tools.refinery.store.statecoding.internal; |
7 | 7 | ||
8 | import tools.refinery.store.map.Version; | ||
8 | import tools.refinery.store.model.Model; | 9 | import tools.refinery.store.model.Model; |
9 | import tools.refinery.store.model.ModelStore; | 10 | import tools.refinery.store.model.ModelStore; |
10 | import tools.refinery.store.representation.Symbol; | 11 | import tools.refinery.store.representation.Symbol; |
11 | import tools.refinery.store.statecoding.StateCoderAdapter; | 12 | import tools.refinery.store.statecoding.StateCoderAdapter; |
12 | import tools.refinery.store.statecoding.StateCoderStoreAdapter; | 13 | import tools.refinery.store.statecoding.StateCoderStoreAdapter; |
14 | import tools.refinery.store.statecoding.StateEquivalenceChecker; | ||
15 | import tools.refinery.store.statecoding.stateequivalence.StateEquivalenceCheckerImpl; | ||
13 | 16 | ||
14 | import java.util.Collection; | 17 | import java.util.Collection; |
18 | import java.util.Objects; | ||
15 | 19 | ||
16 | public class StateCoderStoreAdapterImpl implements StateCoderStoreAdapter { | 20 | public class StateCoderStoreAdapterImpl implements StateCoderStoreAdapter { |
17 | final ModelStore store; | 21 | final ModelStore store; |
18 | final Collection<Symbol<?>> symbols; | 22 | final Collection<Symbol<?>> symbols; |
19 | 23 | ||
24 | final StateEquivalenceChecker equivalenceChecker = new StateEquivalenceCheckerImpl(); | ||
25 | |||
20 | StateCoderStoreAdapterImpl(ModelStore store, Collection<Symbol<?>> symbols) { | 26 | StateCoderStoreAdapterImpl(ModelStore store, Collection<Symbol<?>> symbols) { |
21 | this.store = store; | 27 | this.store = store; |
22 | this.symbols = symbols; | 28 | this.symbols = symbols; |
@@ -28,7 +34,30 @@ public class StateCoderStoreAdapterImpl implements StateCoderStoreAdapter { | |||
28 | } | 34 | } |
29 | 35 | ||
30 | @Override | 36 | @Override |
37 | public StateEquivalenceChecker.EquivalenceResult checkEquivalence(Version v1, Version v2) { | ||
38 | if(Objects.equals(v1,v2)) { | ||
39 | return StateEquivalenceChecker.EquivalenceResult.ISOMORPHIC; | ||
40 | } | ||
41 | var model1 = this.getStore().createModelForState(v1); | ||
42 | var model2 = this.getStore().createModelForState(v2); | ||
43 | |||
44 | var s1 = model1.getAdapter(StateCoderAdapter.class).calculateStateCode(); | ||
45 | var s2 = model2.getAdapter(StateCoderAdapter.class).calculateStateCode(); | ||
46 | |||
47 | if(s1.modelCode() != s2.modelCode()) { | ||
48 | return StateEquivalenceChecker.EquivalenceResult.DIFFERENT; | ||
49 | } | ||
50 | |||
51 | var i1 = symbols.stream().map(model1::getInterpretation).toList(); | ||
52 | var i2 = symbols.stream().map(model2::getInterpretation).toList(); | ||
53 | |||
54 | return equivalenceChecker.constructMorphism(i1,s1.objectCode(),i2,s2.objectCode()); | ||
55 | } | ||
56 | |||
57 | @Override | ||
31 | public StateCoderAdapter createModelAdapter(Model model) { | 58 | public StateCoderAdapter createModelAdapter(Model model) { |
32 | return new StateCoderAdapterImpl(this,model,symbols); | 59 | return new StateCoderAdapterImpl(this,model,symbols); |
33 | } | 60 | } |
61 | |||
62 | |||
34 | } | 63 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/statecoding/neighbourhood/CollectionNeighbourhoodCalculator.java b/subprojects/store/src/main/java/tools/refinery/store/statecoding/neighbourhood/CollectionNeighbourhoodCalculator.java new file mode 100644 index 00000000..058750ee --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/neighbourhood/CollectionNeighbourhoodCalculator.java | |||
@@ -0,0 +1,131 @@ | |||
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.statecoding.neighbourhood; | ||
7 | |||
8 | import org.eclipse.collections.api.set.primitive.MutableLongSet; | ||
9 | import org.eclipse.collections.impl.set.mutable.primitive.LongHashSet; | ||
10 | import tools.refinery.store.model.Interpretation; | ||
11 | import tools.refinery.store.statecoding.StateCodeCalculator; | ||
12 | import tools.refinery.store.statecoding.StateCoderResult; | ||
13 | import tools.refinery.store.tuple.Tuple; | ||
14 | import tools.refinery.store.tuple.Tuple0; | ||
15 | |||
16 | import java.util.ArrayList; | ||
17 | import java.util.LinkedHashMap; | ||
18 | import java.util.List; | ||
19 | import java.util.Random; | ||
20 | |||
21 | public class CollectionNeighbourhoodCalculator implements StateCodeCalculator { | ||
22 | protected final List<Interpretation<?>> nullImpactValues; | ||
23 | protected final LinkedHashMap<Interpretation<?>, long[]> impactValues; | ||
24 | |||
25 | public CollectionNeighbourhoodCalculator(List<? extends Interpretation<?>> interpretations) { | ||
26 | this.nullImpactValues = new ArrayList<>(); | ||
27 | this.impactValues = new LinkedHashMap<>(); | ||
28 | Random random = new Random(1); | ||
29 | |||
30 | for (Interpretation<?> interpretation : interpretations) { | ||
31 | int arity = interpretation.getSymbol().arity(); | ||
32 | if (arity == 0) { | ||
33 | nullImpactValues.add(interpretation); | ||
34 | } else { | ||
35 | long[] impact = new long[arity]; | ||
36 | for (int i = 0; i < arity; i++) { | ||
37 | impact[i] = random.nextLong(); | ||
38 | } | ||
39 | impactValues.put(interpretation, impact); | ||
40 | } | ||
41 | } | ||
42 | } | ||
43 | |||
44 | @Override | ||
45 | public StateCoderResult calculateCodes() { | ||
46 | ObjectCodeImpl previous = new ObjectCodeImpl(); | ||
47 | ObjectCodeImpl next = new ObjectCodeImpl(); | ||
48 | |||
49 | int previousSize = 1; | ||
50 | long lastSum; | ||
51 | boolean grows; | ||
52 | |||
53 | do{ | ||
54 | for (var impactValueEntry : this.impactValues.entrySet()) { | ||
55 | Interpretation<?> interpretation = impactValueEntry.getKey(); | ||
56 | long[] impact = impactValueEntry.getValue(); | ||
57 | var cursor = interpretation.getAll(); | ||
58 | while (cursor.move()) { | ||
59 | Tuple tuple = cursor.getKey(); | ||
60 | Object value = cursor.getValue(); | ||
61 | long tupleHash = getTupleHash(tuple, value, previous); | ||
62 | addHash(next, tuple, impact, tupleHash); | ||
63 | } | ||
64 | } | ||
65 | |||
66 | previous = next; | ||
67 | next = null; | ||
68 | lastSum = 0; | ||
69 | MutableLongSet codes = new LongHashSet(); | ||
70 | for (int i = 0; i < previous.getSize(); i++) { | ||
71 | long objectHash = previous.get(i); | ||
72 | codes.add(objectHash); | ||
73 | |||
74 | final long shifted1 = objectHash>>> 32; | ||
75 | final long shifted2 = objectHash << 32; | ||
76 | lastSum += shifted1 + shifted2; | ||
77 | } | ||
78 | int nextSize = codes.size(); | ||
79 | grows = previousSize < nextSize; | ||
80 | previousSize = nextSize; | ||
81 | |||
82 | if(grows) { | ||
83 | next = new ObjectCodeImpl(previous); | ||
84 | } | ||
85 | } while (grows); | ||
86 | |||
87 | long result = 1; | ||
88 | for (var nullImpactValue : nullImpactValues) { | ||
89 | result = result * 31 + nullImpactValue.get(Tuple0.INSTANCE).hashCode(); | ||
90 | } | ||
91 | result += lastSum; | ||
92 | |||
93 | return new StateCoderResult((int) result, previous); | ||
94 | } | ||
95 | |||
96 | protected long getTupleHash(Tuple tuple, Object value, ObjectCodeImpl objectCodeImpl) { | ||
97 | long result = value.hashCode(); | ||
98 | int arity = tuple.getSize(); | ||
99 | if (arity == 1) { | ||
100 | result = result * 31 + objectCodeImpl.get(tuple.get(0)); | ||
101 | } else if (arity == 2) { | ||
102 | result = result * 31 + objectCodeImpl.get(tuple.get(0)); | ||
103 | result = result * 31 + objectCodeImpl.get(tuple.get(1)); | ||
104 | if (tuple.get(0) == tuple.get(1)) { | ||
105 | result++; | ||
106 | } | ||
107 | } else if (arity > 2) { | ||
108 | for (int i = 0; i < arity; i++) { | ||
109 | result = result * 31 + objectCodeImpl.get(tuple.get(i)); | ||
110 | } | ||
111 | } | ||
112 | return result; | ||
113 | } | ||
114 | |||
115 | protected void addHash(ObjectCodeImpl objectCodeImpl, Tuple tuple, long[] impact, long tupleHashCode) { | ||
116 | if (tuple.getSize() == 1) { | ||
117 | addHash(objectCodeImpl, tuple.get(0), impact[0], tupleHashCode); | ||
118 | } else if (tuple.getSize() == 2) { | ||
119 | addHash(objectCodeImpl, tuple.get(0), impact[0], tupleHashCode); | ||
120 | addHash(objectCodeImpl, tuple.get(1), impact[1], tupleHashCode); | ||
121 | } else if (tuple.getSize() > 2) { | ||
122 | for (int i = 0; i < tuple.getSize(); i++) { | ||
123 | addHash(objectCodeImpl, tuple.get(i), impact[i], tupleHashCode); | ||
124 | } | ||
125 | } | ||
126 | } | ||
127 | |||
128 | protected void addHash(ObjectCodeImpl objectCodeImpl, int o, long impact, long tupleHash) { | ||
129 | objectCodeImpl.set(o, objectCodeImpl.get(o) + tupleHash * impact); | ||
130 | } | ||
131 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/statecoding/neighbourhood/LazyNeighbourhoodCalculator.java b/subprojects/store/src/main/java/tools/refinery/store/statecoding/neighbourhood/LazyNeighbourhoodCalculator.java new file mode 100644 index 00000000..79317679 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/neighbourhood/LazyNeighbourhoodCalculator.java | |||
@@ -0,0 +1,235 @@ | |||
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.statecoding.neighbourhood; | ||
7 | |||
8 | import org.eclipse.collections.api.map.primitive.LongIntMap; | ||
9 | import org.eclipse.collections.impl.map.mutable.primitive.LongIntHashMap; | ||
10 | import tools.refinery.store.map.Cursor; | ||
11 | import tools.refinery.store.model.Interpretation; | ||
12 | import tools.refinery.store.statecoding.StateCodeCalculator; | ||
13 | import tools.refinery.store.statecoding.StateCoderResult; | ||
14 | import tools.refinery.store.tuple.Tuple; | ||
15 | import tools.refinery.store.tuple.Tuple0; | ||
16 | |||
17 | import java.util.ArrayList; | ||
18 | import java.util.LinkedHashMap; | ||
19 | import java.util.List; | ||
20 | import java.util.Random; | ||
21 | |||
22 | public class LazyNeighbourhoodCalculator implements StateCodeCalculator { | ||
23 | protected final List<Interpretation<?>> nullImpactValues; | ||
24 | protected final LinkedHashMap<Interpretation<?>, long[]> impactValues; | ||
25 | |||
26 | public LazyNeighbourhoodCalculator(List<? extends Interpretation<?>> interpretations) { | ||
27 | this.nullImpactValues = new ArrayList<>(); | ||
28 | this.impactValues = new LinkedHashMap<>(); | ||
29 | Random random = new Random(1); | ||
30 | |||
31 | for (Interpretation<?> interpretation : interpretations) { | ||
32 | int arity = interpretation.getSymbol().arity(); | ||
33 | if (arity == 0) { | ||
34 | nullImpactValues.add(interpretation); | ||
35 | } else { | ||
36 | long[] impact = new long[arity]; | ||
37 | for (int i = 0; i < arity; i++) { | ||
38 | impact[i] = random.nextInt(); | ||
39 | } | ||
40 | impactValues.put(interpretation, impact); | ||
41 | } | ||
42 | } | ||
43 | } | ||
44 | |||
45 | public StateCoderResult calculateCodes() { | ||
46 | ObjectCodeImpl previous = new ObjectCodeImpl(); | ||
47 | ObjectCodeImpl next = new ObjectCodeImpl(); | ||
48 | LongIntMap hash2Amount = new LongIntHashMap(); | ||
49 | |||
50 | long lastSum; | ||
51 | int lastSize = 1; | ||
52 | boolean grows; | ||
53 | |||
54 | do { | ||
55 | constructNextObjectCodes(previous, next, hash2Amount); | ||
56 | |||
57 | LongIntHashMap nextHash2Amount = new LongIntHashMap(); | ||
58 | lastSum = calculateLastSum(previous, next, hash2Amount, nextHash2Amount); | ||
59 | |||
60 | previous = next; | ||
61 | next = null; | ||
62 | |||
63 | int nextSize = nextHash2Amount.size(); | ||
64 | grows = nextSize > lastSize; | ||
65 | lastSize = nextSize; | ||
66 | |||
67 | if (grows) { | ||
68 | next = new ObjectCodeImpl(previous); | ||
69 | } | ||
70 | } while (grows); | ||
71 | |||
72 | long result = 1; | ||
73 | for (var nullImpactValue : nullImpactValues) { | ||
74 | result = result * 31 + nullImpactValue.get(Tuple0.INSTANCE).hashCode(); | ||
75 | } | ||
76 | result += lastSum; | ||
77 | |||
78 | return new StateCoderResult((int) result, previous); | ||
79 | } | ||
80 | |||
81 | private long calculateLastSum(ObjectCodeImpl previous, ObjectCodeImpl next, LongIntMap hash2Amount, | ||
82 | LongIntHashMap nextHash2Amount) { | ||
83 | long lastSum = 0; | ||
84 | for (int i = 0; i < next.getSize(); i++) { | ||
85 | final long hash; | ||
86 | if (isUnique(hash2Amount, previous, i)) { | ||
87 | hash = previous.get(i); | ||
88 | next.set(i, hash); | ||
89 | } else { | ||
90 | hash = next.get(i); | ||
91 | } | ||
92 | |||
93 | final int amount = nextHash2Amount.get(hash); | ||
94 | nextHash2Amount.put(hash, amount + 1); | ||
95 | |||
96 | final long shifted1 = hash >>> 8; | ||
97 | final long shifted2 = hash << 8; | ||
98 | final long shifted3 = hash >> 2; | ||
99 | lastSum += shifted1*shifted3 + shifted2; | ||
100 | } | ||
101 | return lastSum; | ||
102 | } | ||
103 | |||
104 | private void constructNextObjectCodes(ObjectCodeImpl previous, ObjectCodeImpl next, LongIntMap hash2Amount) { | ||
105 | for (var impactValueEntry : this.impactValues.entrySet()) { | ||
106 | Interpretation<?> interpretation = impactValueEntry.getKey(); | ||
107 | var cursor = interpretation.getAll(); | ||
108 | int arity = interpretation.getSymbol().arity(); | ||
109 | long[] impactValue = impactValueEntry.getValue(); | ||
110 | |||
111 | if (arity == 1) { | ||
112 | while (cursor.move()) { | ||
113 | lazyImpactCalculation1(hash2Amount, previous, next, impactValue, cursor); | ||
114 | } | ||
115 | } else if (arity == 2) { | ||
116 | while (cursor.move()) { | ||
117 | lazyImpactCalculation2(hash2Amount, previous, next, impactValue, cursor); | ||
118 | } | ||
119 | } else { | ||
120 | while (cursor.move()) { | ||
121 | lazyImpactCalculationN(hash2Amount, previous, next, impactValue, cursor); | ||
122 | } | ||
123 | } | ||
124 | } | ||
125 | } | ||
126 | |||
127 | private boolean isUnique(LongIntMap hash2Amount, ObjectCodeImpl objectCodeImpl, int object) { | ||
128 | final long hash = objectCodeImpl.get(object); | ||
129 | if(hash == 0) { | ||
130 | return false; | ||
131 | } | ||
132 | final int amount = hash2Amount.get(hash); | ||
133 | return amount == 1; | ||
134 | } | ||
135 | |||
136 | private void lazyImpactCalculation1(LongIntMap hash2Amount, ObjectCodeImpl previous, ObjectCodeImpl next, long[] impactValues, Cursor<Tuple, ?> cursor) { | ||
137 | |||
138 | Tuple tuple = cursor.getKey(); | ||
139 | int o = tuple.get(0); | ||
140 | |||
141 | if (isUnique(hash2Amount, previous, o)) { | ||
142 | next.ensureSize(o); | ||
143 | } else { | ||
144 | Object value = cursor.getValue(); | ||
145 | long tupleHash = getTupleHash1(tuple, value, previous); | ||
146 | |||
147 | addHash(next, o, impactValues[0], tupleHash); | ||
148 | } | ||
149 | } | ||
150 | |||
151 | private void lazyImpactCalculation2(LongIntMap hash2Amount, ObjectCodeImpl previous, ObjectCodeImpl next, long[] impactValues, Cursor<Tuple, ?> cursor) { | ||
152 | Tuple tuple = cursor.getKey(); | ||
153 | int o1 = tuple.get(0); | ||
154 | int o2 = tuple.get(1); | ||
155 | |||
156 | boolean u1 = isUnique(hash2Amount, previous, o1); | ||
157 | boolean u2 = isUnique(hash2Amount, previous, o2); | ||
158 | |||
159 | if (u1 && u2) { | ||
160 | next.ensureSize(o1); | ||
161 | next.ensureSize(o2); | ||
162 | } else { | ||
163 | Object value = cursor.getValue(); | ||
164 | long tupleHash = getTupleHash2(tuple, value, previous); | ||
165 | |||
166 | if (!u1) { | ||
167 | addHash(next, o1, impactValues[0], tupleHash); | ||
168 | next.ensureSize(o2); | ||
169 | } | ||
170 | if (!u2) { | ||
171 | next.ensureSize(o1); | ||
172 | addHash(next, o2, impactValues[1], tupleHash); | ||
173 | } | ||
174 | } | ||
175 | } | ||
176 | |||
177 | private void lazyImpactCalculationN(LongIntMap hash2Amount, ObjectCodeImpl previous, ObjectCodeImpl next, long[] impactValues, Cursor<Tuple, ?> cursor) { | ||
178 | Tuple tuple = cursor.getKey(); | ||
179 | |||
180 | boolean[] uniques = new boolean[tuple.getSize()]; | ||
181 | boolean allUnique = true; | ||
182 | for (int i = 0; i < tuple.getSize(); i++) { | ||
183 | final boolean isUnique = isUnique(hash2Amount, previous, tuple.get(i)); | ||
184 | uniques[i] = isUnique; | ||
185 | allUnique &= isUnique; | ||
186 | } | ||
187 | |||
188 | if (allUnique) { | ||
189 | for (int i = 0; i < tuple.getSize(); i++) { | ||
190 | next.ensureSize(tuple.get(i)); | ||
191 | } | ||
192 | } else { | ||
193 | Object value = cursor.getValue(); | ||
194 | long tupleHash = getTupleHashN(tuple, value, previous); | ||
195 | |||
196 | for (int i = 0; i < tuple.getSize(); i++) { | ||
197 | int o = tuple.get(i); | ||
198 | if (!uniques[i]) { | ||
199 | addHash(next, o, impactValues[i], tupleHash); | ||
200 | } else { | ||
201 | next.ensureSize(o); | ||
202 | } | ||
203 | } | ||
204 | } | ||
205 | } | ||
206 | |||
207 | private long getTupleHash1(Tuple tuple, Object value, ObjectCodeImpl objectCodeImpl) { | ||
208 | long result = value.hashCode(); | ||
209 | result = result * 31 + objectCodeImpl.get(tuple.get(0)); | ||
210 | return result; | ||
211 | } | ||
212 | |||
213 | private long getTupleHash2(Tuple tuple, Object value, ObjectCodeImpl objectCodeImpl) { | ||
214 | long result = value.hashCode(); | ||
215 | result = result * 31 + objectCodeImpl.get(tuple.get(0)); | ||
216 | result = result * 31 + objectCodeImpl.get(tuple.get(1)); | ||
217 | if (tuple.get(0) == tuple.get(1)) { | ||
218 | result*=31; | ||
219 | } | ||
220 | return result; | ||
221 | } | ||
222 | |||
223 | private long getTupleHashN(Tuple tuple, Object value, ObjectCodeImpl objectCodeImpl) { | ||
224 | long result = value.hashCode(); | ||
225 | for (int i = 0; i < tuple.getSize(); i++) { | ||
226 | result = result * 31 + objectCodeImpl.get(tuple.get(i)); | ||
227 | } | ||
228 | return result; | ||
229 | } | ||
230 | |||
231 | protected void addHash(ObjectCodeImpl objectCodeImpl, int o, long impact, long tupleHash) { | ||
232 | long x = tupleHash * impact; | ||
233 | objectCodeImpl.set(o, objectCodeImpl.get(o) + x); | ||
234 | } | ||
235 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/statecoding/neighbourhood/NeighbourhoodCalculator.java b/subprojects/store/src/main/java/tools/refinery/store/statecoding/neighbourhood/NeighbourhoodCalculator.java index 24a7122e..212291c3 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/statecoding/neighbourhood/NeighbourhoodCalculator.java +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/neighbourhood/NeighbourhoodCalculator.java | |||
@@ -8,6 +8,8 @@ package tools.refinery.store.statecoding.neighbourhood; | |||
8 | import org.eclipse.collections.api.set.primitive.MutableLongSet; | 8 | import org.eclipse.collections.api.set.primitive.MutableLongSet; |
9 | import org.eclipse.collections.impl.set.mutable.primitive.LongHashSet; | 9 | import org.eclipse.collections.impl.set.mutable.primitive.LongHashSet; |
10 | import tools.refinery.store.model.Interpretation; | 10 | import tools.refinery.store.model.Interpretation; |
11 | import tools.refinery.store.statecoding.StateCodeCalculator; | ||
12 | import tools.refinery.store.statecoding.StateCoderResult; | ||
11 | import tools.refinery.store.tuple.Tuple; | 13 | import tools.refinery.store.tuple.Tuple; |
12 | import tools.refinery.store.tuple.Tuple0; | 14 | import tools.refinery.store.tuple.Tuple0; |
13 | 15 | ||
@@ -16,9 +18,9 @@ import java.util.LinkedHashMap; | |||
16 | import java.util.List; | 18 | import java.util.List; |
17 | import java.util.Random; | 19 | import java.util.Random; |
18 | 20 | ||
19 | public class NeighbourhoodCalculator { | 21 | public class NeighbourhoodCalculator implements StateCodeCalculator { |
20 | final List<Interpretation<?>> nullImpactValues; | 22 | protected final List<Interpretation<?>> nullImpactValues; |
21 | final LinkedHashMap<Interpretation<?>, long[]> impactValues; | 23 | protected final LinkedHashMap<Interpretation<?>, long[]> impactValues; |
22 | 24 | ||
23 | public NeighbourhoodCalculator(List<? extends Interpretation<?>> interpretations) { | 25 | public NeighbourhoodCalculator(List<? extends Interpretation<?>> interpretations) { |
24 | this.nullImpactValues = new ArrayList<>(); | 26 | this.nullImpactValues = new ArrayList<>(); |
@@ -39,9 +41,10 @@ public class NeighbourhoodCalculator { | |||
39 | } | 41 | } |
40 | } | 42 | } |
41 | 43 | ||
42 | public int calculate() { | 44 | @Override |
43 | ObjectCode previous = new ObjectCode(); | 45 | public StateCoderResult calculateCodes() { |
44 | ObjectCode next = new ObjectCode(); | 46 | ObjectCodeImpl previous = new ObjectCodeImpl(); |
47 | ObjectCodeImpl next = new ObjectCodeImpl(); | ||
45 | 48 | ||
46 | int previousSize = 1; | 49 | int previousSize = 1; |
47 | long lastSum; | 50 | long lastSum; |
@@ -77,7 +80,7 @@ public class NeighbourhoodCalculator { | |||
77 | previousSize = nextSize; | 80 | previousSize = nextSize; |
78 | 81 | ||
79 | if(grows) { | 82 | if(grows) { |
80 | next = new ObjectCode(previous); | 83 | next = new ObjectCodeImpl(previous); |
81 | } | 84 | } |
82 | } while (grows); | 85 | } while (grows); |
83 | 86 | ||
@@ -87,43 +90,43 @@ public class NeighbourhoodCalculator { | |||
87 | } | 90 | } |
88 | result += lastSum; | 91 | result += lastSum; |
89 | 92 | ||
90 | return (int) result; | 93 | return new StateCoderResult((int) result, previous); |
91 | } | 94 | } |
92 | 95 | ||
93 | protected long getTupleHash(Tuple tuple, Object value, ObjectCode objectCode) { | 96 | protected long getTupleHash(Tuple tuple, Object value, ObjectCodeImpl objectCodeImpl) { |
94 | long result = (long) value; | 97 | long result = value.hashCode(); |
95 | int arity = tuple.getSize(); | 98 | int arity = tuple.getSize(); |
96 | if (arity == 1) { | 99 | if (arity == 1) { |
97 | result = result * 31 + objectCode.get(tuple.get(0)); | 100 | result = result * 31 + objectCodeImpl.get(tuple.get(0)); |
98 | } else if (arity == 2) { | 101 | } else if (arity == 2) { |
99 | result = result * 31 + objectCode.get(tuple.get(0)); | 102 | result = result * 31 + objectCodeImpl.get(tuple.get(0)); |
100 | result = result * 31 + objectCode.get(tuple.get(1)); | 103 | result = result * 31 + objectCodeImpl.get(tuple.get(1)); |
101 | if (tuple.get(0) == tuple.get(1)) { | 104 | if (tuple.get(0) == tuple.get(1)) { |
102 | result++; | 105 | result++; |
103 | } | 106 | } |
104 | } else if (arity > 2) { | 107 | } else if (arity > 2) { |
105 | for (int i = 0; i < arity; i++) { | 108 | for (int i = 0; i < arity; i++) { |
106 | result = result * 31 + objectCode.get(tuple.get(i)); | 109 | result = result * 31 + objectCodeImpl.get(tuple.get(i)); |
107 | } | 110 | } |
108 | } | 111 | } |
109 | return result; | 112 | return result; |
110 | } | 113 | } |
111 | 114 | ||
112 | protected void addHash(ObjectCode objectCode, Tuple tuple, long[] impact, long tupleHashCode) { | 115 | protected void addHash(ObjectCodeImpl objectCodeImpl, Tuple tuple, long[] impact, long tupleHashCode) { |
113 | if (tuple.getSize() == 1) { | 116 | if (tuple.getSize() == 1) { |
114 | addHash(objectCode, tuple.get(0), impact[0], tupleHashCode); | 117 | addHash(objectCodeImpl, tuple.get(0), impact[0], tupleHashCode); |
115 | } else if (tuple.getSize() == 2) { | 118 | } else if (tuple.getSize() == 2) { |
116 | addHash(objectCode, tuple.get(0), impact[0], tupleHashCode); | 119 | addHash(objectCodeImpl, tuple.get(0), impact[0], tupleHashCode); |
117 | addHash(objectCode, tuple.get(1), impact[1], tupleHashCode); | 120 | addHash(objectCodeImpl, tuple.get(1), impact[1], tupleHashCode); |
118 | } else if (tuple.getSize() > 2) { | 121 | } else if (tuple.getSize() > 2) { |
119 | for (int i = 0; i < tuple.getSize(); i++) { | 122 | for (int i = 0; i < tuple.getSize(); i++) { |
120 | addHash(objectCode, tuple.get(i), impact[i], tupleHashCode); | 123 | addHash(objectCodeImpl, tuple.get(i), impact[i], tupleHashCode); |
121 | } | 124 | } |
122 | } | 125 | } |
123 | } | 126 | } |
124 | 127 | ||
125 | protected void addHash(ObjectCode objectCode, int o, long impact, long tupleHash) { | 128 | protected void addHash(ObjectCodeImpl objectCodeImpl, int o, long impact, long tupleHash) { |
126 | objectCode.set(o, objectCode.get(o) + tupleHash * impact); | 129 | objectCodeImpl.set(o, objectCodeImpl.get(o) + tupleHash * impact); |
127 | } | 130 | } |
128 | 131 | ||
129 | } | 132 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/statecoding/neighbourhood/ObjectCode.java b/subprojects/store/src/main/java/tools/refinery/store/statecoding/neighbourhood/ObjectCodeImpl.java index 594d2b3a..08e3a90b 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/statecoding/neighbourhood/ObjectCode.java +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/neighbourhood/ObjectCodeImpl.java | |||
@@ -5,21 +5,25 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.store.statecoding.neighbourhood; | 6 | package tools.refinery.store.statecoding.neighbourhood; |
7 | 7 | ||
8 | public class ObjectCode { | 8 | import tools.refinery.store.statecoding.ObjectCode; |
9 | |||
10 | import java.util.Arrays; | ||
11 | |||
12 | public class ObjectCodeImpl implements ObjectCode { | ||
9 | private long[] vector; | 13 | private long[] vector; |
10 | private int size; | 14 | private int size; |
11 | 15 | ||
12 | public ObjectCode() { | 16 | public ObjectCodeImpl() { |
13 | vector = new long[10]; | 17 | vector = new long[10]; |
14 | size = 0; | 18 | size = 0; |
15 | } | 19 | } |
16 | 20 | ||
17 | public ObjectCode(ObjectCode sameSize) { | 21 | public ObjectCodeImpl(ObjectCodeImpl sameSize) { |
18 | this.vector = new long[sameSize.size]; | 22 | this.vector = new long[sameSize.size]; |
19 | this.size = sameSize.size; | 23 | this.size = sameSize.size; |
20 | } | 24 | } |
21 | 25 | ||
22 | private void ensureSize(int object) { | 26 | public void ensureSize(int object) { |
23 | if(object >= size) { | 27 | if(object >= size) { |
24 | size = object+1; | 28 | size = object+1; |
25 | } | 29 | } |
@@ -52,4 +56,11 @@ public class ObjectCode { | |||
52 | public int getSize() { | 56 | public int getSize() { |
53 | return this.size; | 57 | return this.size; |
54 | } | 58 | } |
59 | |||
60 | @Override | ||
61 | public String toString() { | ||
62 | return "ObjectCodeImpl{" + | ||
63 | "vector=" + Arrays.toString(Arrays.copyOf(vector,this.size)) + | ||
64 | '}'; | ||
65 | } | ||
55 | } | 66 | } |
diff --git a/subprojects/store/src/main/java/tools/refinery/store/statecoding/stateequivalence/CombinationNodePairing.java b/subprojects/store/src/main/java/tools/refinery/store/statecoding/stateequivalence/CombinationNodePairing.java new file mode 100644 index 00000000..2877bd0f --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/stateequivalence/CombinationNodePairing.java | |||
@@ -0,0 +1,96 @@ | |||
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.statecoding.stateequivalence; | ||
7 | |||
8 | import org.eclipse.collections.api.factory.primitive.IntIntMaps; | ||
9 | import org.eclipse.collections.api.map.primitive.IntIntMap; | ||
10 | import org.eclipse.collections.api.set.primitive.IntSet; | ||
11 | import org.eclipse.collections.impl.list.Interval; | ||
12 | import org.eclipse.collections.impl.set.mutable.primitive.IntHashSet; | ||
13 | |||
14 | import java.util.ArrayList; | ||
15 | import java.util.Arrays; | ||
16 | import java.util.List; | ||
17 | |||
18 | public class CombinationNodePairing implements NodePairing { | ||
19 | private final int[] left; | ||
20 | private final int[] right; | ||
21 | |||
22 | CombinationNodePairing(IntSet left, IntHashSet right) { | ||
23 | this.left = left.toArray(); | ||
24 | this.right = right.toArray(); | ||
25 | |||
26 | Arrays.sort(this.left); | ||
27 | Arrays.sort(this.right); | ||
28 | } | ||
29 | |||
30 | @Override | ||
31 | public int size() { | ||
32 | return left.length; | ||
33 | } | ||
34 | |||
35 | static final int LIMIT = 5; | ||
36 | static final List<List<int[]>> permutations = new ArrayList<>(); | ||
37 | |||
38 | /** | ||
39 | * Generates and stores permutations up to a given size. If the number would be more than a limit, it provides a | ||
40 | * single permutation only. | ||
41 | * | ||
42 | * @param max The max number in the permutation | ||
43 | * @return A complete list of permutations of numbers 0...max, or a single permutation. | ||
44 | */ | ||
45 | public static List<int[]> getPermutations(int max) { | ||
46 | if (max < permutations.size()) { | ||
47 | return permutations.get(max); | ||
48 | } | ||
49 | if (max == 0) { | ||
50 | List<int[]> result = new ArrayList<>(); | ||
51 | result.add(new int[1]); | ||
52 | permutations.add(result); | ||
53 | return result; | ||
54 | } | ||
55 | List<int[]> result = new ArrayList<>(); | ||
56 | List<int[]> previousPermutations = getPermutations(max - 1); | ||
57 | for (var permutation : previousPermutations) { | ||
58 | for (int pos = 0; pos <= max; pos++) { | ||
59 | int[] newPermutation = new int[max + 1]; | ||
60 | if (pos >= 0) | ||
61 | System.arraycopy(permutation, 0, newPermutation, 0, pos); | ||
62 | newPermutation[pos] = max; | ||
63 | if (max - (pos + 1) >= 0) | ||
64 | System.arraycopy(permutation, pos + 1, newPermutation, pos + 1 + 1, max - (pos + 1)); | ||
65 | result.add(newPermutation); | ||
66 | } | ||
67 | } | ||
68 | permutations.add(result); | ||
69 | return result; | ||
70 | } | ||
71 | |||
72 | @Override | ||
73 | public List<IntIntMap> permutations() { | ||
74 | final var interval = Interval.zeroTo(this.size() - 1); | ||
75 | |||
76 | if (isComplete()) { | ||
77 | final List<int[]> p = getPermutations(this.size() - 1); | ||
78 | return p.stream().map(x -> constructPermutationMap(interval, x)).toList(); | ||
79 | } else { | ||
80 | return List.of(constructTrivialMap(interval)); | ||
81 | } | ||
82 | } | ||
83 | |||
84 | private IntIntMap constructTrivialMap(Interval interval) { | ||
85 | return IntIntMaps.immutable.from(interval, l -> left[l], r -> right[r]); | ||
86 | } | ||
87 | |||
88 | private IntIntMap constructPermutationMap(Interval interval, int[] permutation) { | ||
89 | return IntIntMaps.immutable.from(interval, l -> left[l], r -> right[permutation[r]]); | ||
90 | } | ||
91 | |||
92 | @Override | ||
93 | public boolean isComplete() { | ||
94 | return this.size() <= LIMIT; | ||
95 | } | ||
96 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/statecoding/stateequivalence/NodePairing.java b/subprojects/store/src/main/java/tools/refinery/store/statecoding/stateequivalence/NodePairing.java new file mode 100644 index 00000000..7e5db7a3 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/stateequivalence/NodePairing.java | |||
@@ -0,0 +1,33 @@ | |||
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.statecoding.stateequivalence; | ||
7 | |||
8 | import org.eclipse.collections.api.map.primitive.IntIntMap; | ||
9 | import org.eclipse.collections.impl.set.mutable.primitive.IntHashSet; | ||
10 | |||
11 | import java.util.List; | ||
12 | |||
13 | public interface NodePairing { | ||
14 | |||
15 | int size(); | ||
16 | List<IntIntMap> permutations(); | ||
17 | |||
18 | boolean isComplete(); | ||
19 | |||
20 | static NodePairing constructNodePairing(IntHashSet left, IntHashSet right){ | ||
21 | if(left.size() != right.size()) { | ||
22 | return null; | ||
23 | } | ||
24 | |||
25 | if(left.size() == 1) { | ||
26 | int leftValue = left.intIterator().next(); | ||
27 | int rightValue = right.intIterator().next(); | ||
28 | return new TrivialNodePairing(leftValue, rightValue); | ||
29 | } else { | ||
30 | return new CombinationNodePairing(left,right); | ||
31 | } | ||
32 | } | ||
33 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/statecoding/stateequivalence/PermutationMorphism.java b/subprojects/store/src/main/java/tools/refinery/store/statecoding/stateequivalence/PermutationMorphism.java new file mode 100644 index 00000000..6be0f3e7 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/stateequivalence/PermutationMorphism.java | |||
@@ -0,0 +1,64 @@ | |||
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.statecoding.stateequivalence; | ||
7 | |||
8 | import org.eclipse.collections.api.map.primitive.IntIntMap; | ||
9 | import tools.refinery.store.statecoding.Morphism; | ||
10 | |||
11 | import java.util.List; | ||
12 | |||
13 | public class PermutationMorphism implements Morphism { | ||
14 | private final IntIntMap object2PermutationGroup; | ||
15 | private final List<List<IntIntMap>> permutationsGroups; | ||
16 | private final int[] selection; | ||
17 | private boolean hasNext; | ||
18 | |||
19 | PermutationMorphism(IntIntMap object2PermutationGroup, | ||
20 | List<List<IntIntMap>> permutationsGroups) { | ||
21 | this.object2PermutationGroup = object2PermutationGroup; | ||
22 | this.permutationsGroups = permutationsGroups; | ||
23 | |||
24 | this.selection = new int[this.permutationsGroups.size()]; | ||
25 | this.hasNext = true; | ||
26 | } | ||
27 | |||
28 | public boolean next() { | ||
29 | return next(0); | ||
30 | } | ||
31 | |||
32 | private boolean next(int position) { | ||
33 | if (position >= permutationsGroups.size()) { | ||
34 | this.hasNext = false; | ||
35 | return false; | ||
36 | } | ||
37 | if (selection[position] + 1 < permutationsGroups.get(position).size()) { | ||
38 | selection[position] = selection[position] + 1; | ||
39 | return true; | ||
40 | } else { | ||
41 | selection[position] = 0; | ||
42 | return next(position + 1); | ||
43 | } | ||
44 | } | ||
45 | |||
46 | @Override | ||
47 | public int get(int object) { | ||
48 | if(!hasNext) { | ||
49 | throw new IllegalArgumentException("No next permutation!"); | ||
50 | } | ||
51 | |||
52 | final int groupIndex = object2PermutationGroup.get(object); | ||
53 | final var selectedGroup = permutationsGroups.get(groupIndex); | ||
54 | final int permutationIndex = selection[groupIndex]; | ||
55 | final var selectedPermutation = selectedGroup.get(permutationIndex); | ||
56 | |||
57 | return selectedPermutation.get(object); | ||
58 | } | ||
59 | |||
60 | @Override | ||
61 | public int getSize() { | ||
62 | return object2PermutationGroup.size(); | ||
63 | } | ||
64 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/statecoding/stateequivalence/StateEquivalenceCheckerImpl.java b/subprojects/store/src/main/java/tools/refinery/store/statecoding/stateequivalence/StateEquivalenceCheckerImpl.java new file mode 100644 index 00000000..fd704086 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/stateequivalence/StateEquivalenceCheckerImpl.java | |||
@@ -0,0 +1,152 @@ | |||
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.statecoding.stateequivalence; | ||
7 | |||
8 | import org.eclipse.collections.api.map.primitive.IntIntMap; | ||
9 | import org.eclipse.collections.impl.map.mutable.primitive.IntIntHashMap; | ||
10 | import org.eclipse.collections.impl.map.mutable.primitive.LongObjectHashMap; | ||
11 | import org.eclipse.collections.impl.set.mutable.primitive.IntHashSet; | ||
12 | import tools.refinery.store.model.Interpretation; | ||
13 | import tools.refinery.store.statecoding.Morphism; | ||
14 | import tools.refinery.store.statecoding.ObjectCode; | ||
15 | import tools.refinery.store.statecoding.StateEquivalenceChecker; | ||
16 | import tools.refinery.store.tuple.Tuple; | ||
17 | |||
18 | import java.util.ArrayList; | ||
19 | import java.util.List; | ||
20 | import java.util.Objects; | ||
21 | |||
22 | public class StateEquivalenceCheckerImpl implements StateEquivalenceChecker { | ||
23 | public static final int LIMIT = 1000; | ||
24 | |||
25 | @Override | ||
26 | public EquivalenceResult constructMorphism(List<? extends Interpretation<?>> interpretations1, | ||
27 | ObjectCode code1, | ||
28 | List<? extends Interpretation<?>> interpretations2, | ||
29 | ObjectCode code2) { | ||
30 | if (code1.getSize() != code2.getSize()) { | ||
31 | return EquivalenceResult.DIFFERENT; | ||
32 | } | ||
33 | |||
34 | IntIntHashMap object2PermutationGroup = new IntIntHashMap(); | ||
35 | List<List<IntIntMap>> permutationsGroups = new ArrayList<>(); | ||
36 | |||
37 | final EquivalenceResult permutations = constructPermutationNavigation(indexByHash(code1), indexByHash(code2), | ||
38 | object2PermutationGroup, permutationsGroups); | ||
39 | |||
40 | if (permutations == EquivalenceResult.DIFFERENT) { | ||
41 | return EquivalenceResult.DIFFERENT; | ||
42 | } | ||
43 | |||
44 | boolean hasNext; | ||
45 | PermutationMorphism morphism = new PermutationMorphism(object2PermutationGroup, permutationsGroups); | ||
46 | int tried = 0; | ||
47 | do { | ||
48 | if (testMorphism(interpretations1, interpretations2, morphism)) { | ||
49 | return permutations; | ||
50 | } | ||
51 | |||
52 | if(tried >= LIMIT) { | ||
53 | return EquivalenceResult.UNKNOWN; | ||
54 | } | ||
55 | |||
56 | hasNext = morphism.next(); | ||
57 | tried++; | ||
58 | } while (hasNext); | ||
59 | |||
60 | return EquivalenceResult.DIFFERENT; | ||
61 | } | ||
62 | |||
63 | private LongObjectHashMap<IntHashSet> indexByHash(ObjectCode code) { | ||
64 | LongObjectHashMap<IntHashSet> result = new LongObjectHashMap<>(); | ||
65 | for (int o = 0; o < code.getSize(); o++) { | ||
66 | long hash = code.get(o); | ||
67 | var equivalenceClass = result.get(hash); | ||
68 | if (equivalenceClass == null) { | ||
69 | equivalenceClass = new IntHashSet(); | ||
70 | result.put(hash, equivalenceClass); | ||
71 | } | ||
72 | equivalenceClass.add(o); | ||
73 | } | ||
74 | return result; | ||
75 | } | ||
76 | |||
77 | private EquivalenceResult constructPermutationNavigation(LongObjectHashMap<IntHashSet> map1, | ||
78 | LongObjectHashMap<IntHashSet> map2, | ||
79 | IntIntHashMap emptyMapToListOfOptions, | ||
80 | List<List<IntIntMap>> emptyListOfOptions) { | ||
81 | if (map1.size() != map2.size()) { | ||
82 | return EquivalenceResult.DIFFERENT; | ||
83 | } | ||
84 | |||
85 | var iterator = map1.keySet().longIterator(); | ||
86 | |||
87 | boolean allComplete = true; | ||
88 | |||
89 | while (iterator.hasNext()) { | ||
90 | long hash = iterator.next(); | ||
91 | var set1 = map1.get(hash); | ||
92 | var set2 = map2.get(hash); | ||
93 | if (set2 == null) { | ||
94 | return EquivalenceResult.DIFFERENT; | ||
95 | } | ||
96 | |||
97 | var pairing = NodePairing.constructNodePairing(set1, set2); | ||
98 | if (pairing == null) { | ||
99 | return EquivalenceResult.DIFFERENT; | ||
100 | } | ||
101 | |||
102 | allComplete &= pairing.isComplete(); | ||
103 | |||
104 | final int optionIndex = emptyListOfOptions.size(); | ||
105 | set1.forEach(key -> emptyMapToListOfOptions.put(key, optionIndex)); | ||
106 | emptyListOfOptions.add(pairing.permutations()); | ||
107 | } | ||
108 | if(allComplete) { | ||
109 | return EquivalenceResult.ISOMORPHIC; | ||
110 | } else { | ||
111 | return EquivalenceResult.UNKNOWN; | ||
112 | } | ||
113 | } | ||
114 | |||
115 | private boolean testMorphism(List<? extends Interpretation<?>> s, List<? extends Interpretation<?>> t, Morphism m) { | ||
116 | for (int interpretationIndex = 0; interpretationIndex < s.size(); interpretationIndex++) { | ||
117 | var sI = s.get(interpretationIndex); | ||
118 | var tI = t.get(interpretationIndex); | ||
119 | |||
120 | var cursor = sI.getAll(); | ||
121 | while (cursor.move()) { | ||
122 | final Tuple sTuple = cursor.getKey(); | ||
123 | final Object sValue = cursor.getValue(); | ||
124 | |||
125 | final Tuple tTuple = apply(sTuple, m); | ||
126 | final Object tValue = tI.get(tTuple); | ||
127 | |||
128 | if (!Objects.equals(sValue, tValue)) { | ||
129 | return false; | ||
130 | } | ||
131 | } | ||
132 | } | ||
133 | return true; | ||
134 | } | ||
135 | |||
136 | private Tuple apply(Tuple t, Morphism m) { | ||
137 | final int arity = t.getSize(); | ||
138 | if (arity == 0) { | ||
139 | return Tuple.of(); | ||
140 | } else if (arity == 1) { | ||
141 | return Tuple.of(m.get(t.get(0))); | ||
142 | } else if (arity == 2) { | ||
143 | return Tuple.of(m.get(t.get(0)), m.get(t.get(1))); | ||
144 | } else { | ||
145 | int[] newTupleIndices = new int[arity]; | ||
146 | for (int i = 0; i < arity; i++) { | ||
147 | newTupleIndices[i] = m.get(t.get(i)); | ||
148 | } | ||
149 | return Tuple.of(newTupleIndices); | ||
150 | } | ||
151 | } | ||
152 | } | ||
diff --git a/subprojects/store/src/main/java/tools/refinery/store/statecoding/stateequivalence/TrivialNodePairing.java b/subprojects/store/src/main/java/tools/refinery/store/statecoding/stateequivalence/TrivialNodePairing.java new file mode 100644 index 00000000..f5eadfb9 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/stateequivalence/TrivialNodePairing.java | |||
@@ -0,0 +1,36 @@ | |||
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.statecoding.stateequivalence; | ||
7 | |||
8 | import org.eclipse.collections.api.factory.primitive.IntIntMaps; | ||
9 | import org.eclipse.collections.api.map.primitive.IntIntMap; | ||
10 | |||
11 | import java.util.List; | ||
12 | |||
13 | public class TrivialNodePairing implements NodePairing { | ||
14 | final int left; | ||
15 | final int right; | ||
16 | |||
17 | TrivialNodePairing(int left, int right) { | ||
18 | this.left = left; | ||
19 | this.right = right; | ||
20 | } | ||
21 | |||
22 | @Override | ||
23 | public int size() { | ||
24 | return 1; | ||
25 | } | ||
26 | |||
27 | @Override | ||
28 | public List<IntIntMap> permutations() { | ||
29 | return List.of(IntIntMaps.immutable.of(left,right)); | ||
30 | } | ||
31 | |||
32 | @Override | ||
33 | public boolean isComplete() { | ||
34 | return true; | ||
35 | } | ||
36 | } | ||
diff --git a/subprojects/store/src/test/java/tools/refinery/store/statecoding/ExperimentalSetupTest.java b/subprojects/store/src/test/java/tools/refinery/store/statecoding/ExperimentalSetupTest.java new file mode 100644 index 00000000..87b1623c --- /dev/null +++ b/subprojects/store/src/test/java/tools/refinery/store/statecoding/ExperimentalSetupTest.java | |||
@@ -0,0 +1,107 @@ | |||
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.statecoding; | ||
7 | |||
8 | import org.junit.jupiter.api.Test; | ||
9 | import tools.refinery.store.map.Version; | ||
10 | import tools.refinery.store.model.ModelStore; | ||
11 | import tools.refinery.store.representation.Symbol; | ||
12 | import tools.refinery.store.tuple.Tuple; | ||
13 | |||
14 | import java.util.*; | ||
15 | |||
16 | class ExperimentalSetupTest { | ||
17 | public static void generate(int size) { | ||
18 | Symbol<Boolean> person = new Symbol<>("Person", 1, Boolean.class, false); | ||
19 | Symbol<Boolean> friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
20 | |||
21 | var store = ModelStore.builder() | ||
22 | .symbols(person, friend) | ||
23 | .with(StateCoderAdapter | ||
24 | .builder()) | ||
25 | .build(); | ||
26 | |||
27 | Set<Version> versions = new HashSet<>(); | ||
28 | Map<Integer, List<Version>> codes = new HashMap<>(); | ||
29 | |||
30 | var empty = store.createEmptyModel(); | ||
31 | var pI = empty.getInterpretation(person); | ||
32 | |||
33 | for (int i = 0; i < size; i++) { | ||
34 | pI.put(Tuple.of(i), true); | ||
35 | } | ||
36 | |||
37 | var emptyVersion = empty.commit(); | ||
38 | versions.add(emptyVersion); | ||
39 | var emptyCode = empty.getAdapter(StateCoderAdapter.class).calculateModelCode(); | ||
40 | List<Version> emptyList = new ArrayList<>(); | ||
41 | emptyList.add(emptyVersion); | ||
42 | codes.put(emptyCode, emptyList); | ||
43 | |||
44 | var storeAdapter = store.getAdapter(StateCoderStoreAdapter.class); | ||
45 | |||
46 | int dif = 0; | ||
47 | int iso = 0; | ||
48 | int unk = 0; | ||
49 | |||
50 | //int step = 0 | ||
51 | |||
52 | for (int i = 0; i < size; i++) { | ||
53 | for (int j = 0; j < size; j++) { | ||
54 | var previousVersions = new HashSet<>(versions); | ||
55 | for (var version : previousVersions) { | ||
56 | |||
57 | var model = store.createModelForState(version); | ||
58 | model.getInterpretation(friend).put(Tuple.of(i, j), true); | ||
59 | |||
60 | Version version1 = model.commit(); | ||
61 | var stateCode = model.getAdapter(StateCoderAdapter.class).calculateStateCode(); | ||
62 | int code = stateCode.modelCode(); | ||
63 | //System.out.println(step+++" ->" +code); | ||
64 | if (codes.containsKey(code)) { | ||
65 | Version similar = codes.get(code).get(0); | ||
66 | |||
67 | var outcome = storeAdapter.checkEquivalence(version1, similar); | ||
68 | if (outcome == StateEquivalenceChecker.EquivalenceResult.DIFFERENT) { | ||
69 | System.out.println(); | ||
70 | var c = model.getInterpretation(friend).getAll(); | ||
71 | while (c.move()) { | ||
72 | System.out.println(c.getKey().toString()); | ||
73 | } | ||
74 | System.out.println("vs"); | ||
75 | var c2 = store.createModelForState(similar).getInterpretation(friend).getAll(); | ||
76 | while (c2.move()) { | ||
77 | System.out.println(c2.getKey().toString()); | ||
78 | } | ||
79 | |||
80 | dif++; | ||
81 | } else if (outcome == StateEquivalenceChecker.EquivalenceResult.UNKNOWN) { | ||
82 | unk++; | ||
83 | } else { | ||
84 | iso++; | ||
85 | } | ||
86 | } else { | ||
87 | versions.add(version1); | ||
88 | |||
89 | List<Version> newList = new ArrayList<>(); | ||
90 | newList.add(version1); | ||
91 | codes.put(code, newList); | ||
92 | } | ||
93 | } | ||
94 | } | ||
95 | } | ||
96 | |||
97 | System.out.printf("v=%d i=%d d=%d u=%d\n", versions.size(), iso, dif, unk); | ||
98 | } | ||
99 | |||
100 | @Test | ||
101 | void runTests() { | ||
102 | for (int i = 0; i < 5; i++) { | ||
103 | System.out.println("size = " + i); | ||
104 | generate(i); | ||
105 | } | ||
106 | } | ||
107 | } | ||
diff --git a/subprojects/store/src/test/java/tools/refinery/store/statecoding/StateCoderBuildTest.java b/subprojects/store/src/test/java/tools/refinery/store/statecoding/StateCoderBuildTest.java new file mode 100644 index 00000000..b0b80af7 --- /dev/null +++ b/subprojects/store/src/test/java/tools/refinery/store/statecoding/StateCoderBuildTest.java | |||
@@ -0,0 +1,80 @@ | |||
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.statecoding; | ||
7 | |||
8 | import org.junit.jupiter.api.Test; | ||
9 | import tools.refinery.store.model.Interpretation; | ||
10 | import tools.refinery.store.model.ModelStore; | ||
11 | import tools.refinery.store.representation.Symbol; | ||
12 | import tools.refinery.store.tuple.Tuple; | ||
13 | |||
14 | import static org.junit.jupiter.api.Assertions.*; | ||
15 | |||
16 | class StateCoderBuildTest { | ||
17 | Symbol<Boolean> person = new Symbol<>("Person", 1, Boolean.class, false); | ||
18 | Symbol<Integer> age = new Symbol<>("age", 1, Integer.class, null); | ||
19 | Symbol<Boolean> friend = new Symbol<>("friend", 2, Boolean.class, false); | ||
20 | |||
21 | @Test | ||
22 | void simpleStateCoderTest() { | ||
23 | var store = ModelStore.builder() | ||
24 | .symbols(person, age, friend) | ||
25 | .with(StateCoderAdapter | ||
26 | .builder()) | ||
27 | .build(); | ||
28 | |||
29 | var model = store.createEmptyModel(); | ||
30 | var stateCoder = model.getAdapter(StateCoderAdapter.class); | ||
31 | assertNotNull(stateCoder); | ||
32 | |||
33 | var personI = model.getInterpretation(person); | ||
34 | var friendI = model.getInterpretation(friend); | ||
35 | var ageI = model.getInterpretation(age); | ||
36 | fill(personI, friendI, ageI); | ||
37 | |||
38 | stateCoder.calculateStateCode(); | ||
39 | } | ||
40 | |||
41 | @Test | ||
42 | void excludeTest() { | ||
43 | var store = ModelStore.builder() | ||
44 | .symbols(person, age, friend) | ||
45 | .with(StateCoderAdapter.builder() | ||
46 | .exclude(person) | ||
47 | .exclude(age)) | ||
48 | .build(); | ||
49 | |||
50 | var model = store.createEmptyModel(); | ||
51 | var stateCoder = model.getAdapter(StateCoderAdapter.class); | ||
52 | assertNotNull(stateCoder); | ||
53 | |||
54 | var personI = model.getInterpretation(person); | ||
55 | var friendI = model.getInterpretation(friend); | ||
56 | var ageI = model.getInterpretation(age); | ||
57 | fill(personI, friendI, ageI); | ||
58 | |||
59 | int code = stateCoder.calculateStateCode().modelCode(); | ||
60 | |||
61 | ageI.put(Tuple.of(1),3); | ||
62 | assertEquals(code,stateCoder.calculateStateCode().modelCode()); | ||
63 | |||
64 | ageI.put(Tuple.of(1),null); | ||
65 | assertEquals(code,stateCoder.calculateStateCode().modelCode()); | ||
66 | |||
67 | personI.put(Tuple.of(2),false); | ||
68 | assertEquals(code,stateCoder.calculateStateCode().modelCode()); | ||
69 | } | ||
70 | |||
71 | private static void fill(Interpretation<Boolean> personI, Interpretation<Boolean> friendI, Interpretation<Integer> ageI) { | ||
72 | personI.put(Tuple.of(1), true); | ||
73 | personI.put(Tuple.of(2), true); | ||
74 | |||
75 | ageI.put(Tuple.of(1), 5); | ||
76 | ageI.put(Tuple.of(2), 4); | ||
77 | |||
78 | friendI.put(Tuple.of(1, 2), true); | ||
79 | } | ||
80 | } | ||