From 64f8706af45647b3015abc1bb1378c6be22a515c Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Sat, 29 Jul 2023 16:16:02 +0200 Subject: Initial prototype of the StateCoderAdapter based on NeighbourhoodCalculator. No tests yet. --- subprojects/store/build.gradle.kts | 5 + .../store/statecoding/StateCodeCalculator.java | 10 ++ .../store/statecoding/StateCoderAdapter.java | 12 ++ .../store/statecoding/StateCoderBuilder.java | 29 +++++ .../store/statecoding/StateCoderStoreAdapter.java | 14 +++ .../internal/StateCoderAdapterImpl.java | 47 ++++++++ .../internal/StateCoderBuilderImpl.java | 48 ++++++++ .../internal/StateCoderStoreAdapterImpl.java | 34 ++++++ .../neighbourhood/NeighbourhoodCalculator.java | 129 +++++++++++++++++++++ .../statecoding/neighbourhood/ObjectCode.java | 55 +++++++++ 10 files changed, 383 insertions(+) create mode 100644 subprojects/store/src/main/java/tools/refinery/store/statecoding/StateCodeCalculator.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/statecoding/StateCoderAdapter.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/statecoding/StateCoderBuilder.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/statecoding/StateCoderStoreAdapter.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/statecoding/internal/StateCoderAdapterImpl.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/statecoding/internal/StateCoderBuilderImpl.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/statecoding/internal/StateCoderStoreAdapterImpl.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/statecoding/neighbourhood/NeighbourhoodCalculator.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/statecoding/neighbourhood/ObjectCode.java diff --git a/subprojects/store/build.gradle.kts b/subprojects/store/build.gradle.kts index 2c485020..d653f01d 100644 --- a/subprojects/store/build.gradle.kts +++ b/subprojects/store/build.gradle.kts @@ -8,3 +8,8 @@ plugins { id("tools.refinery.gradle.java-library") id("tools.refinery.gradle.jmh") } + +dependencies { + implementation(libs.eclipseCollections) + implementation(libs.eclipseCollections.api) +} 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 new file mode 100644 index 00000000..479b61ed --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/StateCodeCalculator.java @@ -0,0 +1,10 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.statecoding; + +public interface StateCodeCalculator { + +} 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 new file mode 100644 index 00000000..8795fb68 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/StateCoderAdapter.java @@ -0,0 +1,12 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.statecoding; + +import tools.refinery.store.adapter.ModelAdapter; + +public interface StateCoderAdapter extends ModelAdapter { + int calculateHashCode(); +} diff --git a/subprojects/store/src/main/java/tools/refinery/store/statecoding/StateCoderBuilder.java b/subprojects/store/src/main/java/tools/refinery/store/statecoding/StateCoderBuilder.java new file mode 100644 index 00000000..2f37584f --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/StateCoderBuilder.java @@ -0,0 +1,29 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.statecoding; + +import tools.refinery.store.adapter.ModelAdapterBuilder; +import tools.refinery.store.model.ModelStore; +import tools.refinery.store.representation.AnySymbol; + +import java.util.Collection; +import java.util.List; + +public interface StateCoderBuilder extends ModelAdapterBuilder { + StateCoderBuilder exclude(AnySymbol symbol); + default StateCoderBuilder excludeAll(Collection symbols) { + for(var symbol : symbols) { + exclude(symbol); + } + return this; + } + default StateCoderBuilder excludeAll(AnySymbol... symbols) { + return excludeAll(List.of(symbols)); + } + + @Override + StateCoderStoreAdapter build(ModelStore store); +} 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 new file mode 100644 index 00000000..5946a162 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/StateCoderStoreAdapter.java @@ -0,0 +1,14 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.statecoding; + +import tools.refinery.store.adapter.ModelStoreAdapter; +import tools.refinery.store.model.Model; + +public interface StateCoderStoreAdapter extends ModelStoreAdapter { + @Override + StateCoderAdapter createModelAdapter(Model model); +} 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 new file mode 100644 index 00000000..689db2e3 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/internal/StateCoderAdapterImpl.java @@ -0,0 +1,47 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.statecoding.internal; + +import tools.refinery.store.adapter.ModelStoreAdapter; +import tools.refinery.store.model.Interpretation; +import tools.refinery.store.model.Model; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.statecoding.StateCoderAdapter; +import tools.refinery.store.statecoding.neighbourhood.NeighbourhoodCalculator; + +import java.util.Collection; +import java.util.List; + +public class StateCoderAdapterImpl implements StateCoderAdapter { + final ModelStoreAdapter storeAdapter; + final Model model; + final NeighbourhoodCalculator calculator; + + StateCoderAdapterImpl(ModelStoreAdapter storeAdapter, Model model, Collection> symbols) { + this.storeAdapter = storeAdapter; + this.model = model; + + List> interpretations = symbols.stream().map(model::getInterpretation).toList(); + calculator = new NeighbourhoodCalculator(interpretations); + } + + @Override + public Model getModel() { + return model; + } + + @Override + public ModelStoreAdapter getStoreAdapter() { + return storeAdapter; + } + + @Override + public int calculateHashCode() { + return calculator.calculate(); + } + + +} diff --git a/subprojects/store/src/main/java/tools/refinery/store/statecoding/internal/StateCoderBuilderImpl.java b/subprojects/store/src/main/java/tools/refinery/store/statecoding/internal/StateCoderBuilderImpl.java new file mode 100644 index 00000000..700723f4 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/internal/StateCoderBuilderImpl.java @@ -0,0 +1,48 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.statecoding.internal; + +import tools.refinery.store.model.ModelStore; +import tools.refinery.store.model.ModelStoreBuilder; +import tools.refinery.store.representation.AnySymbol; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.statecoding.StateCoderBuilder; +import tools.refinery.store.statecoding.StateCoderStoreAdapter; + +import java.util.HashSet; +import java.util.LinkedHashSet; +import java.util.Set; + +public class StateCoderBuilderImpl implements StateCoderBuilder { + Set excluded = new HashSet<>(); + + @Override + public StateCoderBuilder exclude(AnySymbol symbol) { + excluded.add(symbol); + return this; + } + + @Override + public boolean isConfigured() { + return true; + } + + @Override + public void configure(ModelStoreBuilder storeBuilder) { + // It does not modify the build process + } + + @Override + public StateCoderStoreAdapter build(ModelStore store) { + Set> symbols = new LinkedHashSet<>(); + for (AnySymbol symbol : store.getSymbols()) { + if (!excluded.contains(symbol) && (symbol instanceof Symbol typed)) { + symbols.add(typed); + } + } + return new StateCoderStoreAdapterImpl(store, symbols); + } +} 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 new file mode 100644 index 00000000..77d36e96 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/internal/StateCoderStoreAdapterImpl.java @@ -0,0 +1,34 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.statecoding.internal; + +import tools.refinery.store.model.Model; +import tools.refinery.store.model.ModelStore; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.statecoding.StateCoderAdapter; +import tools.refinery.store.statecoding.StateCoderStoreAdapter; + +import java.util.Collection; + +public class StateCoderStoreAdapterImpl implements StateCoderStoreAdapter { + final ModelStore store; + final Collection> symbols; + + StateCoderStoreAdapterImpl(ModelStore store, Collection> symbols) { + this.store = store; + this.symbols = symbols; + } + + @Override + public ModelStore getStore() { + return store; + } + + @Override + public StateCoderAdapter createModelAdapter(Model model) { + return new StateCoderAdapterImpl(this,model,symbols); + } +} 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 new file mode 100644 index 00000000..24a7122e --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/neighbourhood/NeighbourhoodCalculator.java @@ -0,0 +1,129 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.statecoding.neighbourhood; + +import org.eclipse.collections.api.set.primitive.MutableLongSet; +import org.eclipse.collections.impl.set.mutable.primitive.LongHashSet; +import tools.refinery.store.model.Interpretation; +import tools.refinery.store.tuple.Tuple; +import tools.refinery.store.tuple.Tuple0; + +import java.util.ArrayList; +import java.util.LinkedHashMap; +import java.util.List; +import java.util.Random; + +public class NeighbourhoodCalculator { + final List> nullImpactValues; + final LinkedHashMap, long[]> impactValues; + + public NeighbourhoodCalculator(List> interpretations) { + this.nullImpactValues = new ArrayList<>(); + this.impactValues = new LinkedHashMap<>(); + Random random = new Random(1); + + for (Interpretation interpretation : interpretations) { + int arity = interpretation.getSymbol().arity(); + if (arity == 0) { + nullImpactValues.add(interpretation); + } else { + long[] impact = new long[arity]; + for (int i = 0; i < arity; i++) { + impact[i] = random.nextLong(); + } + impactValues.put(interpretation, impact); + } + } + } + + public int calculate() { + ObjectCode previous = new ObjectCode(); + ObjectCode next = new ObjectCode(); + + int previousSize = 1; + long lastSum; + boolean grows; + + do{ + for (var impactValueEntry : this.impactValues.entrySet()) { + Interpretation interpretation = impactValueEntry.getKey(); + long[] impact = impactValueEntry.getValue(); + var cursor = interpretation.getAll(); + while (cursor.move()) { + Tuple tuple = cursor.getKey(); + Object value = cursor.getValue(); + long tupleHash = getTupleHash(tuple, value, previous); + addHash(next, tuple, impact, tupleHash); + } + } + + previous = next; + next = null; + lastSum = 0; + MutableLongSet codes = new LongHashSet(); + for (int i = 0; i < previous.getSize(); i++) { + long objectHash = previous.get(i); + codes.add(objectHash); + + final long shifted1 = objectHash>>> 32; + final long shifted2 = objectHash << 32; + lastSum += shifted1 + shifted2; + } + int nextSize = codes.size(); + grows = previousSize < nextSize; + previousSize = nextSize; + + if(grows) { + next = new ObjectCode(previous); + } + } while (grows); + + long result = 1; + for (var nullImpactValue : nullImpactValues) { + result = result * 31 + nullImpactValue.get(Tuple0.INSTANCE).hashCode(); + } + result += lastSum; + + return (int) result; + } + + protected long getTupleHash(Tuple tuple, Object value, ObjectCode objectCode) { + long result = (long) value; + int arity = tuple.getSize(); + if (arity == 1) { + result = result * 31 + objectCode.get(tuple.get(0)); + } else if (arity == 2) { + result = result * 31 + objectCode.get(tuple.get(0)); + result = result * 31 + objectCode.get(tuple.get(1)); + if (tuple.get(0) == tuple.get(1)) { + result++; + } + } else if (arity > 2) { + for (int i = 0; i < arity; i++) { + result = result * 31 + objectCode.get(tuple.get(i)); + } + } + return result; + } + + protected void addHash(ObjectCode objectCode, Tuple tuple, long[] impact, long tupleHashCode) { + if (tuple.getSize() == 1) { + addHash(objectCode, tuple.get(0), impact[0], tupleHashCode); + } else if (tuple.getSize() == 2) { + addHash(objectCode, tuple.get(0), impact[0], tupleHashCode); + addHash(objectCode, tuple.get(1), impact[1], tupleHashCode); + } else if (tuple.getSize() > 2) { + for (int i = 0; i < tuple.getSize(); i++) { + addHash(objectCode, tuple.get(i), impact[i], tupleHashCode); + } + } + } + + protected void addHash(ObjectCode objectCode, int o, long impact, long tupleHash) { + objectCode.set(o, objectCode.get(o) + tupleHash * impact); + } + +} 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/ObjectCode.java new file mode 100644 index 00000000..594d2b3a --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/neighbourhood/ObjectCode.java @@ -0,0 +1,55 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.statecoding.neighbourhood; + +public class ObjectCode { + private long[] vector; + private int size; + + public ObjectCode() { + vector = new long[10]; + size = 0; + } + + public ObjectCode(ObjectCode sameSize) { + this.vector = new long[sameSize.size]; + this.size = sameSize.size; + } + + private void ensureSize(int object) { + if(object >= size) { + size = object+1; + } + + if(object >= vector.length) { + int newLength = vector.length*2; + while(object >= newLength) { + newLength*=2; + } + + long[] newVector = new long[newLength]; + System.arraycopy(vector, 0, newVector, 0, vector.length); + this.vector = newVector; + } + } + + public long get(int object) { + if(object < vector.length) { + return vector[object]; + } else { + return 0; + } + } + + public void set(int object, long value) { + ensureSize(object); + vector[object]=value; + } + + public int getSize() { + return this.size; + } +} -- cgit v1.2.3-54-g00ecf From 4220b2af314201714c5a53e856dff8317557ba76 Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Thu, 3 Aug 2023 19:16:03 +0200 Subject: Intermediate commit with Lazy NeighbourhoodCalculator and StateEquivalenceChecker prototypes --- .../tools/refinery/store/statecoding/Morphism.java | 11 + .../refinery/store/statecoding/ObjectCode.java | 11 + .../store/statecoding/StateCodeCalculator.java | 2 +- .../store/statecoding/StateCoderAdapter.java | 13 +- .../store/statecoding/StateCoderResult.java | 9 + .../store/statecoding/StateCoderStoreAdapter.java | 3 + .../store/statecoding/StateEquivalenceChecker.java | 22 ++ .../internal/StateCoderAdapterImpl.java | 14 +- .../internal/StateCoderStoreAdapterImpl.java | 29 +++ .../CollectionNeighbourhoodCalculator.java | 131 ++++++++++++ .../neighbourhood/LazyNeighbourhoodCalculator.java | 235 +++++++++++++++++++++ .../neighbourhood/NeighbourhoodCalculator.java | 45 ++-- .../statecoding/neighbourhood/ObjectCode.java | 55 ----- .../statecoding/neighbourhood/ObjectCodeImpl.java | 66 ++++++ .../stateequivalence/CombinationNodePairing.java | 96 +++++++++ .../statecoding/stateequivalence/NodePairing.java | 33 +++ .../stateequivalence/PermutationMorphism.java | 64 ++++++ .../StateEquivalenceCheckerImpl.java | 152 +++++++++++++ .../stateequivalence/TrivialNodePairing.java | 36 ++++ .../store/statecoding/ExperimentalSetupTest.java | 107 ++++++++++ .../store/statecoding/StateCoderBuildTest.java | 80 +++++++ 21 files changed, 1129 insertions(+), 85 deletions(-) create mode 100644 subprojects/store/src/main/java/tools/refinery/store/statecoding/Morphism.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/statecoding/ObjectCode.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/statecoding/StateCoderResult.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/statecoding/StateEquivalenceChecker.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/statecoding/neighbourhood/CollectionNeighbourhoodCalculator.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/statecoding/neighbourhood/LazyNeighbourhoodCalculator.java delete mode 100644 subprojects/store/src/main/java/tools/refinery/store/statecoding/neighbourhood/ObjectCode.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/statecoding/neighbourhood/ObjectCodeImpl.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/statecoding/stateequivalence/CombinationNodePairing.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/statecoding/stateequivalence/NodePairing.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/statecoding/stateequivalence/PermutationMorphism.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/statecoding/stateequivalence/StateEquivalenceCheckerImpl.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/statecoding/stateequivalence/TrivialNodePairing.java create mode 100644 subprojects/store/src/test/java/tools/refinery/store/statecoding/ExperimentalSetupTest.java create mode 100644 subprojects/store/src/test/java/tools/refinery/store/statecoding/StateCoderBuildTest.java 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 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.statecoding; + +public interface Morphism { + int get(int object); + int getSize(); +} 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 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.statecoding; + +public interface ObjectCode { + long get(int object); + int getSize(); +} 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 @@ package tools.refinery.store.statecoding; public interface StateCodeCalculator { - + StateCoderResult calculateCodes(); } 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 @@ package tools.refinery.store.statecoding; import tools.refinery.store.adapter.ModelAdapter; +import tools.refinery.store.statecoding.internal.StateCoderBuilderImpl; public interface StateCoderAdapter extends ModelAdapter { - int calculateHashCode(); + StateCoderResult calculateStateCode(); + default int calculateModelCode() { + return calculateStateCode().modelCode(); + } + default ObjectCode calculateObjectCode() { + return calculateStateCode().objectCode(); + } + + static StateCoderBuilderImpl builder() { + return new StateCoderBuilderImpl(); + } } 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 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.statecoding; + +public record StateCoderResult(int modelCode, ObjectCode objectCode) { +} 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 @@ package tools.refinery.store.statecoding; import tools.refinery.store.adapter.ModelStoreAdapter; +import tools.refinery.store.map.Version; import tools.refinery.store.model.Model; public interface StateCoderStoreAdapter extends ModelStoreAdapter { + StateEquivalenceChecker.EquivalenceResult checkEquivalence(Version v1, Version v2); + @Override StateCoderAdapter createModelAdapter(Model model); } 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 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.statecoding; + +import tools.refinery.store.model.Interpretation; + +import java.util.List; + +public interface StateEquivalenceChecker { + enum EquivalenceResult { + ISOMORPHIC, UNKNOWN, DIFFERENT + } + + EquivalenceResult constructMorphism( + List> interpretations1, + ObjectCode code1, List> interpretations2, + ObjectCode code2); +} 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; import tools.refinery.store.model.Interpretation; import tools.refinery.store.model.Model; import tools.refinery.store.representation.Symbol; +import tools.refinery.store.statecoding.StateCodeCalculator; import tools.refinery.store.statecoding.StateCoderAdapter; -import tools.refinery.store.statecoding.neighbourhood.NeighbourhoodCalculator; +import tools.refinery.store.statecoding.StateCoderResult; +import tools.refinery.store.statecoding.neighbourhood.LazyNeighbourhoodCalculator; import java.util.Collection; import java.util.List; @@ -18,14 +20,14 @@ import java.util.List; public class StateCoderAdapterImpl implements StateCoderAdapter { final ModelStoreAdapter storeAdapter; final Model model; - final NeighbourhoodCalculator calculator; + final StateCodeCalculator calculator; StateCoderAdapterImpl(ModelStoreAdapter storeAdapter, Model model, Collection> symbols) { this.storeAdapter = storeAdapter; this.model = model; List> interpretations = symbols.stream().map(model::getInterpretation).toList(); - calculator = new NeighbourhoodCalculator(interpretations); + calculator = new LazyNeighbourhoodCalculator(interpretations); } @Override @@ -39,9 +41,7 @@ public class StateCoderAdapterImpl implements StateCoderAdapter { } @Override - public int calculateHashCode() { - return calculator.calculate(); + public StateCoderResult calculateStateCode() { + return calculator.calculateCodes(); } - - } 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 @@ */ package tools.refinery.store.statecoding.internal; +import tools.refinery.store.map.Version; import tools.refinery.store.model.Model; import tools.refinery.store.model.ModelStore; import tools.refinery.store.representation.Symbol; import tools.refinery.store.statecoding.StateCoderAdapter; import tools.refinery.store.statecoding.StateCoderStoreAdapter; +import tools.refinery.store.statecoding.StateEquivalenceChecker; +import tools.refinery.store.statecoding.stateequivalence.StateEquivalenceCheckerImpl; import java.util.Collection; +import java.util.Objects; public class StateCoderStoreAdapterImpl implements StateCoderStoreAdapter { final ModelStore store; final Collection> symbols; + final StateEquivalenceChecker equivalenceChecker = new StateEquivalenceCheckerImpl(); + StateCoderStoreAdapterImpl(ModelStore store, Collection> symbols) { this.store = store; this.symbols = symbols; @@ -27,8 +33,31 @@ public class StateCoderStoreAdapterImpl implements StateCoderStoreAdapter { return store; } + @Override + public StateEquivalenceChecker.EquivalenceResult checkEquivalence(Version v1, Version v2) { + if(Objects.equals(v1,v2)) { + return StateEquivalenceChecker.EquivalenceResult.ISOMORPHIC; + } + var model1 = this.getStore().createModelForState(v1); + var model2 = this.getStore().createModelForState(v2); + + var s1 = model1.getAdapter(StateCoderAdapter.class).calculateStateCode(); + var s2 = model2.getAdapter(StateCoderAdapter.class).calculateStateCode(); + + if(s1.modelCode() != s2.modelCode()) { + return StateEquivalenceChecker.EquivalenceResult.DIFFERENT; + } + + var i1 = symbols.stream().map(model1::getInterpretation).toList(); + var i2 = symbols.stream().map(model2::getInterpretation).toList(); + + return equivalenceChecker.constructMorphism(i1,s1.objectCode(),i2,s2.objectCode()); + } + @Override public StateCoderAdapter createModelAdapter(Model model) { return new StateCoderAdapterImpl(this,model,symbols); } + + } 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 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.statecoding.neighbourhood; + +import org.eclipse.collections.api.set.primitive.MutableLongSet; +import org.eclipse.collections.impl.set.mutable.primitive.LongHashSet; +import tools.refinery.store.model.Interpretation; +import tools.refinery.store.statecoding.StateCodeCalculator; +import tools.refinery.store.statecoding.StateCoderResult; +import tools.refinery.store.tuple.Tuple; +import tools.refinery.store.tuple.Tuple0; + +import java.util.ArrayList; +import java.util.LinkedHashMap; +import java.util.List; +import java.util.Random; + +public class CollectionNeighbourhoodCalculator implements StateCodeCalculator { + protected final List> nullImpactValues; + protected final LinkedHashMap, long[]> impactValues; + + public CollectionNeighbourhoodCalculator(List> interpretations) { + this.nullImpactValues = new ArrayList<>(); + this.impactValues = new LinkedHashMap<>(); + Random random = new Random(1); + + for (Interpretation interpretation : interpretations) { + int arity = interpretation.getSymbol().arity(); + if (arity == 0) { + nullImpactValues.add(interpretation); + } else { + long[] impact = new long[arity]; + for (int i = 0; i < arity; i++) { + impact[i] = random.nextLong(); + } + impactValues.put(interpretation, impact); + } + } + } + + @Override + public StateCoderResult calculateCodes() { + ObjectCodeImpl previous = new ObjectCodeImpl(); + ObjectCodeImpl next = new ObjectCodeImpl(); + + int previousSize = 1; + long lastSum; + boolean grows; + + do{ + for (var impactValueEntry : this.impactValues.entrySet()) { + Interpretation interpretation = impactValueEntry.getKey(); + long[] impact = impactValueEntry.getValue(); + var cursor = interpretation.getAll(); + while (cursor.move()) { + Tuple tuple = cursor.getKey(); + Object value = cursor.getValue(); + long tupleHash = getTupleHash(tuple, value, previous); + addHash(next, tuple, impact, tupleHash); + } + } + + previous = next; + next = null; + lastSum = 0; + MutableLongSet codes = new LongHashSet(); + for (int i = 0; i < previous.getSize(); i++) { + long objectHash = previous.get(i); + codes.add(objectHash); + + final long shifted1 = objectHash>>> 32; + final long shifted2 = objectHash << 32; + lastSum += shifted1 + shifted2; + } + int nextSize = codes.size(); + grows = previousSize < nextSize; + previousSize = nextSize; + + if(grows) { + next = new ObjectCodeImpl(previous); + } + } while (grows); + + long result = 1; + for (var nullImpactValue : nullImpactValues) { + result = result * 31 + nullImpactValue.get(Tuple0.INSTANCE).hashCode(); + } + result += lastSum; + + return new StateCoderResult((int) result, previous); + } + + protected long getTupleHash(Tuple tuple, Object value, ObjectCodeImpl objectCodeImpl) { + long result = value.hashCode(); + int arity = tuple.getSize(); + if (arity == 1) { + result = result * 31 + objectCodeImpl.get(tuple.get(0)); + } else if (arity == 2) { + result = result * 31 + objectCodeImpl.get(tuple.get(0)); + result = result * 31 + objectCodeImpl.get(tuple.get(1)); + if (tuple.get(0) == tuple.get(1)) { + result++; + } + } else if (arity > 2) { + for (int i = 0; i < arity; i++) { + result = result * 31 + objectCodeImpl.get(tuple.get(i)); + } + } + return result; + } + + protected void addHash(ObjectCodeImpl objectCodeImpl, Tuple tuple, long[] impact, long tupleHashCode) { + if (tuple.getSize() == 1) { + addHash(objectCodeImpl, tuple.get(0), impact[0], tupleHashCode); + } else if (tuple.getSize() == 2) { + addHash(objectCodeImpl, tuple.get(0), impact[0], tupleHashCode); + addHash(objectCodeImpl, tuple.get(1), impact[1], tupleHashCode); + } else if (tuple.getSize() > 2) { + for (int i = 0; i < tuple.getSize(); i++) { + addHash(objectCodeImpl, tuple.get(i), impact[i], tupleHashCode); + } + } + } + + protected void addHash(ObjectCodeImpl objectCodeImpl, int o, long impact, long tupleHash) { + objectCodeImpl.set(o, objectCodeImpl.get(o) + tupleHash * impact); + } +} 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 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.statecoding.neighbourhood; + +import org.eclipse.collections.api.map.primitive.LongIntMap; +import org.eclipse.collections.impl.map.mutable.primitive.LongIntHashMap; +import tools.refinery.store.map.Cursor; +import tools.refinery.store.model.Interpretation; +import tools.refinery.store.statecoding.StateCodeCalculator; +import tools.refinery.store.statecoding.StateCoderResult; +import tools.refinery.store.tuple.Tuple; +import tools.refinery.store.tuple.Tuple0; + +import java.util.ArrayList; +import java.util.LinkedHashMap; +import java.util.List; +import java.util.Random; + +public class LazyNeighbourhoodCalculator implements StateCodeCalculator { + protected final List> nullImpactValues; + protected final LinkedHashMap, long[]> impactValues; + + public LazyNeighbourhoodCalculator(List> interpretations) { + this.nullImpactValues = new ArrayList<>(); + this.impactValues = new LinkedHashMap<>(); + Random random = new Random(1); + + for (Interpretation interpretation : interpretations) { + int arity = interpretation.getSymbol().arity(); + if (arity == 0) { + nullImpactValues.add(interpretation); + } else { + long[] impact = new long[arity]; + for (int i = 0; i < arity; i++) { + impact[i] = random.nextInt(); + } + impactValues.put(interpretation, impact); + } + } + } + + public StateCoderResult calculateCodes() { + ObjectCodeImpl previous = new ObjectCodeImpl(); + ObjectCodeImpl next = new ObjectCodeImpl(); + LongIntMap hash2Amount = new LongIntHashMap(); + + long lastSum; + int lastSize = 1; + boolean grows; + + do { + constructNextObjectCodes(previous, next, hash2Amount); + + LongIntHashMap nextHash2Amount = new LongIntHashMap(); + lastSum = calculateLastSum(previous, next, hash2Amount, nextHash2Amount); + + previous = next; + next = null; + + int nextSize = nextHash2Amount.size(); + grows = nextSize > lastSize; + lastSize = nextSize; + + if (grows) { + next = new ObjectCodeImpl(previous); + } + } while (grows); + + long result = 1; + for (var nullImpactValue : nullImpactValues) { + result = result * 31 + nullImpactValue.get(Tuple0.INSTANCE).hashCode(); + } + result += lastSum; + + return new StateCoderResult((int) result, previous); + } + + private long calculateLastSum(ObjectCodeImpl previous, ObjectCodeImpl next, LongIntMap hash2Amount, + LongIntHashMap nextHash2Amount) { + long lastSum = 0; + for (int i = 0; i < next.getSize(); i++) { + final long hash; + if (isUnique(hash2Amount, previous, i)) { + hash = previous.get(i); + next.set(i, hash); + } else { + hash = next.get(i); + } + + final int amount = nextHash2Amount.get(hash); + nextHash2Amount.put(hash, amount + 1); + + final long shifted1 = hash >>> 8; + final long shifted2 = hash << 8; + final long shifted3 = hash >> 2; + lastSum += shifted1*shifted3 + shifted2; + } + return lastSum; + } + + private void constructNextObjectCodes(ObjectCodeImpl previous, ObjectCodeImpl next, LongIntMap hash2Amount) { + for (var impactValueEntry : this.impactValues.entrySet()) { + Interpretation interpretation = impactValueEntry.getKey(); + var cursor = interpretation.getAll(); + int arity = interpretation.getSymbol().arity(); + long[] impactValue = impactValueEntry.getValue(); + + if (arity == 1) { + while (cursor.move()) { + lazyImpactCalculation1(hash2Amount, previous, next, impactValue, cursor); + } + } else if (arity == 2) { + while (cursor.move()) { + lazyImpactCalculation2(hash2Amount, previous, next, impactValue, cursor); + } + } else { + while (cursor.move()) { + lazyImpactCalculationN(hash2Amount, previous, next, impactValue, cursor); + } + } + } + } + + private boolean isUnique(LongIntMap hash2Amount, ObjectCodeImpl objectCodeImpl, int object) { + final long hash = objectCodeImpl.get(object); + if(hash == 0) { + return false; + } + final int amount = hash2Amount.get(hash); + return amount == 1; + } + + private void lazyImpactCalculation1(LongIntMap hash2Amount, ObjectCodeImpl previous, ObjectCodeImpl next, long[] impactValues, Cursor cursor) { + + Tuple tuple = cursor.getKey(); + int o = tuple.get(0); + + if (isUnique(hash2Amount, previous, o)) { + next.ensureSize(o); + } else { + Object value = cursor.getValue(); + long tupleHash = getTupleHash1(tuple, value, previous); + + addHash(next, o, impactValues[0], tupleHash); + } + } + + private void lazyImpactCalculation2(LongIntMap hash2Amount, ObjectCodeImpl previous, ObjectCodeImpl next, long[] impactValues, Cursor cursor) { + Tuple tuple = cursor.getKey(); + int o1 = tuple.get(0); + int o2 = tuple.get(1); + + boolean u1 = isUnique(hash2Amount, previous, o1); + boolean u2 = isUnique(hash2Amount, previous, o2); + + if (u1 && u2) { + next.ensureSize(o1); + next.ensureSize(o2); + } else { + Object value = cursor.getValue(); + long tupleHash = getTupleHash2(tuple, value, previous); + + if (!u1) { + addHash(next, o1, impactValues[0], tupleHash); + next.ensureSize(o2); + } + if (!u2) { + next.ensureSize(o1); + addHash(next, o2, impactValues[1], tupleHash); + } + } + } + + private void lazyImpactCalculationN(LongIntMap hash2Amount, ObjectCodeImpl previous, ObjectCodeImpl next, long[] impactValues, Cursor cursor) { + Tuple tuple = cursor.getKey(); + + boolean[] uniques = new boolean[tuple.getSize()]; + boolean allUnique = true; + for (int i = 0; i < tuple.getSize(); i++) { + final boolean isUnique = isUnique(hash2Amount, previous, tuple.get(i)); + uniques[i] = isUnique; + allUnique &= isUnique; + } + + if (allUnique) { + for (int i = 0; i < tuple.getSize(); i++) { + next.ensureSize(tuple.get(i)); + } + } else { + Object value = cursor.getValue(); + long tupleHash = getTupleHashN(tuple, value, previous); + + for (int i = 0; i < tuple.getSize(); i++) { + int o = tuple.get(i); + if (!uniques[i]) { + addHash(next, o, impactValues[i], tupleHash); + } else { + next.ensureSize(o); + } + } + } + } + + private long getTupleHash1(Tuple tuple, Object value, ObjectCodeImpl objectCodeImpl) { + long result = value.hashCode(); + result = result * 31 + objectCodeImpl.get(tuple.get(0)); + return result; + } + + private long getTupleHash2(Tuple tuple, Object value, ObjectCodeImpl objectCodeImpl) { + long result = value.hashCode(); + result = result * 31 + objectCodeImpl.get(tuple.get(0)); + result = result * 31 + objectCodeImpl.get(tuple.get(1)); + if (tuple.get(0) == tuple.get(1)) { + result*=31; + } + return result; + } + + private long getTupleHashN(Tuple tuple, Object value, ObjectCodeImpl objectCodeImpl) { + long result = value.hashCode(); + for (int i = 0; i < tuple.getSize(); i++) { + result = result * 31 + objectCodeImpl.get(tuple.get(i)); + } + return result; + } + + protected void addHash(ObjectCodeImpl objectCodeImpl, int o, long impact, long tupleHash) { + long x = tupleHash * impact; + objectCodeImpl.set(o, objectCodeImpl.get(o) + x); + } +} 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; import org.eclipse.collections.api.set.primitive.MutableLongSet; import org.eclipse.collections.impl.set.mutable.primitive.LongHashSet; import tools.refinery.store.model.Interpretation; +import tools.refinery.store.statecoding.StateCodeCalculator; +import tools.refinery.store.statecoding.StateCoderResult; import tools.refinery.store.tuple.Tuple; import tools.refinery.store.tuple.Tuple0; @@ -16,9 +18,9 @@ import java.util.LinkedHashMap; import java.util.List; import java.util.Random; -public class NeighbourhoodCalculator { - final List> nullImpactValues; - final LinkedHashMap, long[]> impactValues; +public class NeighbourhoodCalculator implements StateCodeCalculator { + protected final List> nullImpactValues; + protected final LinkedHashMap, long[]> impactValues; public NeighbourhoodCalculator(List> interpretations) { this.nullImpactValues = new ArrayList<>(); @@ -39,9 +41,10 @@ public class NeighbourhoodCalculator { } } - public int calculate() { - ObjectCode previous = new ObjectCode(); - ObjectCode next = new ObjectCode(); + @Override + public StateCoderResult calculateCodes() { + ObjectCodeImpl previous = new ObjectCodeImpl(); + ObjectCodeImpl next = new ObjectCodeImpl(); int previousSize = 1; long lastSum; @@ -77,7 +80,7 @@ public class NeighbourhoodCalculator { previousSize = nextSize; if(grows) { - next = new ObjectCode(previous); + next = new ObjectCodeImpl(previous); } } while (grows); @@ -87,43 +90,43 @@ public class NeighbourhoodCalculator { } result += lastSum; - return (int) result; + return new StateCoderResult((int) result, previous); } - protected long getTupleHash(Tuple tuple, Object value, ObjectCode objectCode) { - long result = (long) value; + protected long getTupleHash(Tuple tuple, Object value, ObjectCodeImpl objectCodeImpl) { + long result = value.hashCode(); int arity = tuple.getSize(); if (arity == 1) { - result = result * 31 + objectCode.get(tuple.get(0)); + result = result * 31 + objectCodeImpl.get(tuple.get(0)); } else if (arity == 2) { - result = result * 31 + objectCode.get(tuple.get(0)); - result = result * 31 + objectCode.get(tuple.get(1)); + result = result * 31 + objectCodeImpl.get(tuple.get(0)); + result = result * 31 + objectCodeImpl.get(tuple.get(1)); if (tuple.get(0) == tuple.get(1)) { result++; } } else if (arity > 2) { for (int i = 0; i < arity; i++) { - result = result * 31 + objectCode.get(tuple.get(i)); + result = result * 31 + objectCodeImpl.get(tuple.get(i)); } } return result; } - protected void addHash(ObjectCode objectCode, Tuple tuple, long[] impact, long tupleHashCode) { + protected void addHash(ObjectCodeImpl objectCodeImpl, Tuple tuple, long[] impact, long tupleHashCode) { if (tuple.getSize() == 1) { - addHash(objectCode, tuple.get(0), impact[0], tupleHashCode); + addHash(objectCodeImpl, tuple.get(0), impact[0], tupleHashCode); } else if (tuple.getSize() == 2) { - addHash(objectCode, tuple.get(0), impact[0], tupleHashCode); - addHash(objectCode, tuple.get(1), impact[1], tupleHashCode); + addHash(objectCodeImpl, tuple.get(0), impact[0], tupleHashCode); + addHash(objectCodeImpl, tuple.get(1), impact[1], tupleHashCode); } else if (tuple.getSize() > 2) { for (int i = 0; i < tuple.getSize(); i++) { - addHash(objectCode, tuple.get(i), impact[i], tupleHashCode); + addHash(objectCodeImpl, tuple.get(i), impact[i], tupleHashCode); } } } - protected void addHash(ObjectCode objectCode, int o, long impact, long tupleHash) { - objectCode.set(o, objectCode.get(o) + tupleHash * impact); + protected void addHash(ObjectCodeImpl objectCodeImpl, int o, long impact, long tupleHash) { + objectCodeImpl.set(o, objectCodeImpl.get(o) + tupleHash * impact); } } 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/ObjectCode.java deleted file mode 100644 index 594d2b3a..00000000 --- a/subprojects/store/src/main/java/tools/refinery/store/statecoding/neighbourhood/ObjectCode.java +++ /dev/null @@ -1,55 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.statecoding.neighbourhood; - -public class ObjectCode { - private long[] vector; - private int size; - - public ObjectCode() { - vector = new long[10]; - size = 0; - } - - public ObjectCode(ObjectCode sameSize) { - this.vector = new long[sameSize.size]; - this.size = sameSize.size; - } - - private void ensureSize(int object) { - if(object >= size) { - size = object+1; - } - - if(object >= vector.length) { - int newLength = vector.length*2; - while(object >= newLength) { - newLength*=2; - } - - long[] newVector = new long[newLength]; - System.arraycopy(vector, 0, newVector, 0, vector.length); - this.vector = newVector; - } - } - - public long get(int object) { - if(object < vector.length) { - return vector[object]; - } else { - return 0; - } - } - - public void set(int object, long value) { - ensureSize(object); - vector[object]=value; - } - - public int getSize() { - return this.size; - } -} diff --git a/subprojects/store/src/main/java/tools/refinery/store/statecoding/neighbourhood/ObjectCodeImpl.java b/subprojects/store/src/main/java/tools/refinery/store/statecoding/neighbourhood/ObjectCodeImpl.java new file mode 100644 index 00000000..08e3a90b --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/statecoding/neighbourhood/ObjectCodeImpl.java @@ -0,0 +1,66 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.statecoding.neighbourhood; + +import tools.refinery.store.statecoding.ObjectCode; + +import java.util.Arrays; + +public class ObjectCodeImpl implements ObjectCode { + private long[] vector; + private int size; + + public ObjectCodeImpl() { + vector = new long[10]; + size = 0; + } + + public ObjectCodeImpl(ObjectCodeImpl sameSize) { + this.vector = new long[sameSize.size]; + this.size = sameSize.size; + } + + public void ensureSize(int object) { + if(object >= size) { + size = object+1; + } + + if(object >= vector.length) { + int newLength = vector.length*2; + while(object >= newLength) { + newLength*=2; + } + + long[] newVector = new long[newLength]; + System.arraycopy(vector, 0, newVector, 0, vector.length); + this.vector = newVector; + } + } + + public long get(int object) { + if(object < vector.length) { + return vector[object]; + } else { + return 0; + } + } + + public void set(int object, long value) { + ensureSize(object); + vector[object]=value; + } + + public int getSize() { + return this.size; + } + + @Override + public String toString() { + return "ObjectCodeImpl{" + + "vector=" + Arrays.toString(Arrays.copyOf(vector,this.size)) + + '}'; + } +} 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 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.statecoding.stateequivalence; + +import org.eclipse.collections.api.factory.primitive.IntIntMaps; +import org.eclipse.collections.api.map.primitive.IntIntMap; +import org.eclipse.collections.api.set.primitive.IntSet; +import org.eclipse.collections.impl.list.Interval; +import org.eclipse.collections.impl.set.mutable.primitive.IntHashSet; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.List; + +public class CombinationNodePairing implements NodePairing { + private final int[] left; + private final int[] right; + + CombinationNodePairing(IntSet left, IntHashSet right) { + this.left = left.toArray(); + this.right = right.toArray(); + + Arrays.sort(this.left); + Arrays.sort(this.right); + } + + @Override + public int size() { + return left.length; + } + + static final int LIMIT = 5; + static final List> permutations = new ArrayList<>(); + + /** + * Generates and stores permutations up to a given size. If the number would be more than a limit, it provides a + * single permutation only. + * + * @param max The max number in the permutation + * @return A complete list of permutations of numbers 0...max, or a single permutation. + */ + public static List getPermutations(int max) { + if (max < permutations.size()) { + return permutations.get(max); + } + if (max == 0) { + List result = new ArrayList<>(); + result.add(new int[1]); + permutations.add(result); + return result; + } + List result = new ArrayList<>(); + List previousPermutations = getPermutations(max - 1); + for (var permutation : previousPermutations) { + for (int pos = 0; pos <= max; pos++) { + int[] newPermutation = new int[max + 1]; + if (pos >= 0) + System.arraycopy(permutation, 0, newPermutation, 0, pos); + newPermutation[pos] = max; + if (max - (pos + 1) >= 0) + System.arraycopy(permutation, pos + 1, newPermutation, pos + 1 + 1, max - (pos + 1)); + result.add(newPermutation); + } + } + permutations.add(result); + return result; + } + + @Override + public List permutations() { + final var interval = Interval.zeroTo(this.size() - 1); + + if (isComplete()) { + final List p = getPermutations(this.size() - 1); + return p.stream().map(x -> constructPermutationMap(interval, x)).toList(); + } else { + return List.of(constructTrivialMap(interval)); + } + } + + private IntIntMap constructTrivialMap(Interval interval) { + return IntIntMaps.immutable.from(interval, l -> left[l], r -> right[r]); + } + + private IntIntMap constructPermutationMap(Interval interval, int[] permutation) { + return IntIntMaps.immutable.from(interval, l -> left[l], r -> right[permutation[r]]); + } + + @Override + public boolean isComplete() { + return this.size() <= LIMIT; + } +} 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 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.statecoding.stateequivalence; + +import org.eclipse.collections.api.map.primitive.IntIntMap; +import org.eclipse.collections.impl.set.mutable.primitive.IntHashSet; + +import java.util.List; + +public interface NodePairing { + + int size(); + List permutations(); + + boolean isComplete(); + + static NodePairing constructNodePairing(IntHashSet left, IntHashSet right){ + if(left.size() != right.size()) { + return null; + } + + if(left.size() == 1) { + int leftValue = left.intIterator().next(); + int rightValue = right.intIterator().next(); + return new TrivialNodePairing(leftValue, rightValue); + } else { + return new CombinationNodePairing(left,right); + } + } +} 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 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.statecoding.stateequivalence; + +import org.eclipse.collections.api.map.primitive.IntIntMap; +import tools.refinery.store.statecoding.Morphism; + +import java.util.List; + +public class PermutationMorphism implements Morphism { + private final IntIntMap object2PermutationGroup; + private final List> permutationsGroups; + private final int[] selection; + private boolean hasNext; + + PermutationMorphism(IntIntMap object2PermutationGroup, + List> permutationsGroups) { + this.object2PermutationGroup = object2PermutationGroup; + this.permutationsGroups = permutationsGroups; + + this.selection = new int[this.permutationsGroups.size()]; + this.hasNext = true; + } + + public boolean next() { + return next(0); + } + + private boolean next(int position) { + if (position >= permutationsGroups.size()) { + this.hasNext = false; + return false; + } + if (selection[position] + 1 < permutationsGroups.get(position).size()) { + selection[position] = selection[position] + 1; + return true; + } else { + selection[position] = 0; + return next(position + 1); + } + } + + @Override + public int get(int object) { + if(!hasNext) { + throw new IllegalArgumentException("No next permutation!"); + } + + final int groupIndex = object2PermutationGroup.get(object); + final var selectedGroup = permutationsGroups.get(groupIndex); + final int permutationIndex = selection[groupIndex]; + final var selectedPermutation = selectedGroup.get(permutationIndex); + + return selectedPermutation.get(object); + } + + @Override + public int getSize() { + return object2PermutationGroup.size(); + } +} 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 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.statecoding.stateequivalence; + +import org.eclipse.collections.api.map.primitive.IntIntMap; +import org.eclipse.collections.impl.map.mutable.primitive.IntIntHashMap; +import org.eclipse.collections.impl.map.mutable.primitive.LongObjectHashMap; +import org.eclipse.collections.impl.set.mutable.primitive.IntHashSet; +import tools.refinery.store.model.Interpretation; +import tools.refinery.store.statecoding.Morphism; +import tools.refinery.store.statecoding.ObjectCode; +import tools.refinery.store.statecoding.StateEquivalenceChecker; +import tools.refinery.store.tuple.Tuple; + +import java.util.ArrayList; +import java.util.List; +import java.util.Objects; + +public class StateEquivalenceCheckerImpl implements StateEquivalenceChecker { + public static final int LIMIT = 1000; + + @Override + public EquivalenceResult constructMorphism(List> interpretations1, + ObjectCode code1, + List> interpretations2, + ObjectCode code2) { + if (code1.getSize() != code2.getSize()) { + return EquivalenceResult.DIFFERENT; + } + + IntIntHashMap object2PermutationGroup = new IntIntHashMap(); + List> permutationsGroups = new ArrayList<>(); + + final EquivalenceResult permutations = constructPermutationNavigation(indexByHash(code1), indexByHash(code2), + object2PermutationGroup, permutationsGroups); + + if (permutations == EquivalenceResult.DIFFERENT) { + return EquivalenceResult.DIFFERENT; + } + + boolean hasNext; + PermutationMorphism morphism = new PermutationMorphism(object2PermutationGroup, permutationsGroups); + int tried = 0; + do { + if (testMorphism(interpretations1, interpretations2, morphism)) { + return permutations; + } + + if(tried >= LIMIT) { + return EquivalenceResult.UNKNOWN; + } + + hasNext = morphism.next(); + tried++; + } while (hasNext); + + return EquivalenceResult.DIFFERENT; + } + + private LongObjectHashMap indexByHash(ObjectCode code) { + LongObjectHashMap result = new LongObjectHashMap<>(); + for (int o = 0; o < code.getSize(); o++) { + long hash = code.get(o); + var equivalenceClass = result.get(hash); + if (equivalenceClass == null) { + equivalenceClass = new IntHashSet(); + result.put(hash, equivalenceClass); + } + equivalenceClass.add(o); + } + return result; + } + + private EquivalenceResult constructPermutationNavigation(LongObjectHashMap map1, + LongObjectHashMap map2, + IntIntHashMap emptyMapToListOfOptions, + List> emptyListOfOptions) { + if (map1.size() != map2.size()) { + return EquivalenceResult.DIFFERENT; + } + + var iterator = map1.keySet().longIterator(); + + boolean allComplete = true; + + while (iterator.hasNext()) { + long hash = iterator.next(); + var set1 = map1.get(hash); + var set2 = map2.get(hash); + if (set2 == null) { + return EquivalenceResult.DIFFERENT; + } + + var pairing = NodePairing.constructNodePairing(set1, set2); + if (pairing == null) { + return EquivalenceResult.DIFFERENT; + } + + allComplete &= pairing.isComplete(); + + final int optionIndex = emptyListOfOptions.size(); + set1.forEach(key -> emptyMapToListOfOptions.put(key, optionIndex)); + emptyListOfOptions.add(pairing.permutations()); + } + if(allComplete) { + return EquivalenceResult.ISOMORPHIC; + } else { + return EquivalenceResult.UNKNOWN; + } + } + + private boolean testMorphism(List> s, List> t, Morphism m) { + for (int interpretationIndex = 0; interpretationIndex < s.size(); interpretationIndex++) { + var sI = s.get(interpretationIndex); + var tI = t.get(interpretationIndex); + + var cursor = sI.getAll(); + while (cursor.move()) { + final Tuple sTuple = cursor.getKey(); + final Object sValue = cursor.getValue(); + + final Tuple tTuple = apply(sTuple, m); + final Object tValue = tI.get(tTuple); + + if (!Objects.equals(sValue, tValue)) { + return false; + } + } + } + return true; + } + + private Tuple apply(Tuple t, Morphism m) { + final int arity = t.getSize(); + if (arity == 0) { + return Tuple.of(); + } else if (arity == 1) { + return Tuple.of(m.get(t.get(0))); + } else if (arity == 2) { + return Tuple.of(m.get(t.get(0)), m.get(t.get(1))); + } else { + int[] newTupleIndices = new int[arity]; + for (int i = 0; i < arity; i++) { + newTupleIndices[i] = m.get(t.get(i)); + } + return Tuple.of(newTupleIndices); + } + } +} 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 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.statecoding.stateequivalence; + +import org.eclipse.collections.api.factory.primitive.IntIntMaps; +import org.eclipse.collections.api.map.primitive.IntIntMap; + +import java.util.List; + +public class TrivialNodePairing implements NodePairing { + final int left; + final int right; + + TrivialNodePairing(int left, int right) { + this.left = left; + this.right = right; + } + + @Override + public int size() { + return 1; + } + + @Override + public List permutations() { + return List.of(IntIntMaps.immutable.of(left,right)); + } + + @Override + public boolean isComplete() { + return true; + } +} 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 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.statecoding; + +import org.junit.jupiter.api.Test; +import tools.refinery.store.map.Version; +import tools.refinery.store.model.ModelStore; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.tuple.Tuple; + +import java.util.*; + +class ExperimentalSetupTest { + public static void generate(int size) { + Symbol person = new Symbol<>("Person", 1, Boolean.class, false); + Symbol friend = new Symbol<>("friend", 2, Boolean.class, false); + + var store = ModelStore.builder() + .symbols(person, friend) + .with(StateCoderAdapter + .builder()) + .build(); + + Set versions = new HashSet<>(); + Map> codes = new HashMap<>(); + + var empty = store.createEmptyModel(); + var pI = empty.getInterpretation(person); + + for (int i = 0; i < size; i++) { + pI.put(Tuple.of(i), true); + } + + var emptyVersion = empty.commit(); + versions.add(emptyVersion); + var emptyCode = empty.getAdapter(StateCoderAdapter.class).calculateModelCode(); + List emptyList = new ArrayList<>(); + emptyList.add(emptyVersion); + codes.put(emptyCode, emptyList); + + var storeAdapter = store.getAdapter(StateCoderStoreAdapter.class); + + int dif = 0; + int iso = 0; + int unk = 0; + + //int step = 0 + + for (int i = 0; i < size; i++) { + for (int j = 0; j < size; j++) { + var previousVersions = new HashSet<>(versions); + for (var version : previousVersions) { + + var model = store.createModelForState(version); + model.getInterpretation(friend).put(Tuple.of(i, j), true); + + Version version1 = model.commit(); + var stateCode = model.getAdapter(StateCoderAdapter.class).calculateStateCode(); + int code = stateCode.modelCode(); + //System.out.println(step+++" ->" +code); + if (codes.containsKey(code)) { + Version similar = codes.get(code).get(0); + + var outcome = storeAdapter.checkEquivalence(version1, similar); + if (outcome == StateEquivalenceChecker.EquivalenceResult.DIFFERENT) { + System.out.println(); + var c = model.getInterpretation(friend).getAll(); + while (c.move()) { + System.out.println(c.getKey().toString()); + } + System.out.println("vs"); + var c2 = store.createModelForState(similar).getInterpretation(friend).getAll(); + while (c2.move()) { + System.out.println(c2.getKey().toString()); + } + + dif++; + } else if (outcome == StateEquivalenceChecker.EquivalenceResult.UNKNOWN) { + unk++; + } else { + iso++; + } + } else { + versions.add(version1); + + List newList = new ArrayList<>(); + newList.add(version1); + codes.put(code, newList); + } + } + } + } + + System.out.printf("v=%d i=%d d=%d u=%d\n", versions.size(), iso, dif, unk); + } + + @Test + void runTests() { + for (int i = 0; i < 5; i++) { + System.out.println("size = " + i); + generate(i); + } + } +} 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 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.statecoding; + +import org.junit.jupiter.api.Test; +import tools.refinery.store.model.Interpretation; +import tools.refinery.store.model.ModelStore; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.tuple.Tuple; + +import static org.junit.jupiter.api.Assertions.*; + +class StateCoderBuildTest { + Symbol person = new Symbol<>("Person", 1, Boolean.class, false); + Symbol age = new Symbol<>("age", 1, Integer.class, null); + Symbol friend = new Symbol<>("friend", 2, Boolean.class, false); + + @Test + void simpleStateCoderTest() { + var store = ModelStore.builder() + .symbols(person, age, friend) + .with(StateCoderAdapter + .builder()) + .build(); + + var model = store.createEmptyModel(); + var stateCoder = model.getAdapter(StateCoderAdapter.class); + assertNotNull(stateCoder); + + var personI = model.getInterpretation(person); + var friendI = model.getInterpretation(friend); + var ageI = model.getInterpretation(age); + fill(personI, friendI, ageI); + + stateCoder.calculateStateCode(); + } + + @Test + void excludeTest() { + var store = ModelStore.builder() + .symbols(person, age, friend) + .with(StateCoderAdapter.builder() + .exclude(person) + .exclude(age)) + .build(); + + var model = store.createEmptyModel(); + var stateCoder = model.getAdapter(StateCoderAdapter.class); + assertNotNull(stateCoder); + + var personI = model.getInterpretation(person); + var friendI = model.getInterpretation(friend); + var ageI = model.getInterpretation(age); + fill(personI, friendI, ageI); + + int code = stateCoder.calculateStateCode().modelCode(); + + ageI.put(Tuple.of(1),3); + assertEquals(code,stateCoder.calculateStateCode().modelCode()); + + ageI.put(Tuple.of(1),null); + assertEquals(code,stateCoder.calculateStateCode().modelCode()); + + personI.put(Tuple.of(2),false); + assertEquals(code,stateCoder.calculateStateCode().modelCode()); + } + + private static void fill(Interpretation personI, Interpretation friendI, Interpretation ageI) { + personI.put(Tuple.of(1), true); + personI.put(Tuple.of(2), true); + + ageI.put(Tuple.of(1), 5); + ageI.put(Tuple.of(2), 4); + + friendI.put(Tuple.of(1, 2), true); + } +} -- cgit v1.2.3-54-g00ecf