From bc742b20fa187200def2809e5aef71547f75c65a Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Tue, 18 Jul 2023 20:18:48 +0200 Subject: feat: basic partial interpretation infrastructure --- .../java/tools/refinery/store/map/Cursors.java | 11 ++++++ .../refinery/store/map/IteratorBasedCursor.java | 44 ++++++++++++++++++++++ .../refinery/store/model/ModelStoreBuilder.java | 4 +- .../store/model/ModelStoreConfiguration.java | 11 ++++++ .../refinery/store/model/internal/BaseIndexer.java | 41 ++------------------ .../model/internal/ModelStoreBuilderImpl.java | 19 +++++++--- .../store/representation/AbstractDomain.java | 5 ++- .../refinery/store/representation/TruthValue.java | 17 ++++++++- .../store/representation/TruthValueDomain.java | 29 +++++++------- .../java/tools/refinery/store/tuple/Tuple.java | 2 + .../java/tools/refinery/store/tuple/Tuple0.java | 5 +++ .../java/tools/refinery/store/tuple/Tuple1.java | 8 ++++ .../java/tools/refinery/store/tuple/Tuple2.java | 9 +++++ .../java/tools/refinery/store/tuple/Tuple3.java | 10 +++++ .../java/tools/refinery/store/tuple/Tuple4.java | 11 ++++++ .../java/tools/refinery/store/tuple/TupleN.java | 10 +++++ 16 files changed, 176 insertions(+), 60 deletions(-) create mode 100644 subprojects/store/src/main/java/tools/refinery/store/map/IteratorBasedCursor.java create mode 100644 subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreConfiguration.java (limited to 'subprojects/store') diff --git a/subprojects/store/src/main/java/tools/refinery/store/map/Cursors.java b/subprojects/store/src/main/java/tools/refinery/store/map/Cursors.java index 1080a248..5e69e7af 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/map/Cursors.java +++ b/subprojects/store/src/main/java/tools/refinery/store/map/Cursors.java @@ -5,6 +5,9 @@ */ package tools.refinery.store.map; +import java.util.Iterator; +import java.util.Map; + public final class Cursors { private Cursors() { throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); @@ -18,6 +21,14 @@ public final class Cursors { return new Singleton<>(key, value); } + public static Cursor of(Iterator> iterator) { + return new IteratorBasedCursor<>(iterator); + } + + public static Cursor of(Map map) { + return of(map.entrySet().iterator()); + } + private static class Empty implements Cursor { private boolean terminated = false; diff --git a/subprojects/store/src/main/java/tools/refinery/store/map/IteratorBasedCursor.java b/subprojects/store/src/main/java/tools/refinery/store/map/IteratorBasedCursor.java new file mode 100644 index 00000000..0ed9b730 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/map/IteratorBasedCursor.java @@ -0,0 +1,44 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.map; + +import java.util.Iterator; +import java.util.Map; + +public class IteratorBasedCursor implements Cursor { + private final Iterator> iterator; + private Map.Entry entry; + private boolean terminated; + + public IteratorBasedCursor(Iterator> iterator) { + this.iterator = iterator; + } + + @Override + public K getKey() { + return entry.getKey(); + } + + @Override + public V getValue() { + return entry.getValue(); + } + + @Override + public boolean isTerminated() { + return terminated; + } + + @Override + public boolean move() { + if (!terminated && iterator.hasNext()) { + entry = iterator.next(); + return true; + } + terminated = true; + return false; + } +} diff --git a/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreBuilder.java b/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreBuilder.java index 3a4024b5..8f652762 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreBuilder.java +++ b/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreBuilder.java @@ -29,7 +29,9 @@ public interface ModelStoreBuilder { ModelStoreBuilder symbol(Symbol symbol); - ModelStoreBuilder with(T adapterBuilder); + ModelStoreBuilder with(ModelAdapterBuilder adapterBuilder); + + ModelStoreBuilder with(ModelStoreConfiguration configuration); Optional tryGetAdapter(Class adapterType); diff --git a/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreConfiguration.java b/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreConfiguration.java new file mode 100644 index 00000000..e94af5f8 --- /dev/null +++ b/subprojects/store/src/main/java/tools/refinery/store/model/ModelStoreConfiguration.java @@ -0,0 +1,11 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.model; + +@FunctionalInterface +public interface ModelStoreConfiguration { + void apply(ModelStoreBuilder storeBuilder); +} diff --git a/subprojects/store/src/main/java/tools/refinery/store/model/internal/BaseIndexer.java b/subprojects/store/src/main/java/tools/refinery/store/model/internal/BaseIndexer.java index d9245c1d..3d7f59d7 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/model/internal/BaseIndexer.java +++ b/subprojects/store/src/main/java/tools/refinery/store/model/internal/BaseIndexer.java @@ -9,14 +9,9 @@ import org.eclipse.collections.api.factory.Maps; import org.eclipse.collections.api.factory.primitive.IntObjectMaps; import org.eclipse.collections.api.map.MutableMap; import org.eclipse.collections.api.map.primitive.MutableIntObjectMap; -import tools.refinery.store.map.AnyVersionedMap; -import tools.refinery.store.map.Cursor; -import tools.refinery.store.map.Cursors; -import tools.refinery.store.map.VersionedMap; +import tools.refinery.store.map.*; import tools.refinery.store.tuple.Tuple; -import java.util.Iterator; -import java.util.Map; import java.util.Set; class BaseIndexer { @@ -91,40 +86,12 @@ class BaseIndexer { return new IndexCursor<>(adjacentTuples, versionedMap); } - private static class IndexCursor implements Cursor { + private static class IndexCursor extends IteratorBasedCursor { private final Set dependingMaps; - private final Iterator> iterator; - private Map.Entry entry; - private boolean terminated; - public IndexCursor(MutableMap adjacentTuples, VersionedMap versionedMap) { + public IndexCursor(MutableMap map, VersionedMap versionedMap) { + super(map.entrySet().iterator()); dependingMaps = versionedMap == null ? Set.of() : Set.of(versionedMap); - iterator = adjacentTuples.entrySet().iterator(); - } - - @Override - public Tuple getKey() { - return entry.getKey(); - } - - @Override - public T getValue() { - return entry.getValue(); - } - - @Override - public boolean isTerminated() { - return terminated; - } - - @Override - public boolean move() { - if (!terminated && iterator.hasNext()) { - entry = iterator.next(); - return true; - } - terminated = true; - return false; } @Override diff --git a/subprojects/store/src/main/java/tools/refinery/store/model/internal/ModelStoreBuilderImpl.java b/subprojects/store/src/main/java/tools/refinery/store/model/internal/ModelStoreBuilderImpl.java index aafbe130..5c688178 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/model/internal/ModelStoreBuilderImpl.java +++ b/subprojects/store/src/main/java/tools/refinery/store/model/internal/ModelStoreBuilderImpl.java @@ -11,6 +11,7 @@ import tools.refinery.store.map.VersionedMapStore; import tools.refinery.store.map.VersionedMapStoreImpl; import tools.refinery.store.model.ModelStore; import tools.refinery.store.model.ModelStoreBuilder; +import tools.refinery.store.model.ModelStoreConfiguration; import tools.refinery.store.model.TupleHashProvider; import tools.refinery.store.representation.AnySymbol; import tools.refinery.store.representation.Symbol; @@ -26,7 +27,8 @@ public class ModelStoreBuilderImpl implements ModelStoreBuilder { @Override public ModelStoreBuilder symbol(Symbol symbol) { if (!allSymbols.add(symbol)) { - throw new IllegalArgumentException("Symbol %s already added".formatted(symbol)); + // No need to add symbol twice. + return this; } var equivalenceClass = new SymbolEquivalenceClass<>(symbol); var symbolsInEquivalenceClass = equivalenceClasses.computeIfAbsent(equivalenceClass, @@ -36,7 +38,7 @@ public class ModelStoreBuilderImpl implements ModelStoreBuilder { } @Override - public ModelStoreBuilder with(T adapterBuilder) { + public ModelStoreBuilder with(ModelAdapterBuilder adapterBuilder) { for (var existingAdapter : adapters) { if (existingAdapter.getClass().equals(adapterBuilder.getClass())) { throw new IllegalArgumentException("%s adapter was already configured for store builder" @@ -47,6 +49,12 @@ public class ModelStoreBuilderImpl implements ModelStoreBuilder { return this; } + @Override + public ModelStoreBuilder with(ModelStoreConfiguration configuration) { + configuration.apply(this); + return this; + } + @Override public Optional tryGetAdapter(Class adapterType) { return AdapterUtils.tryGetAdapter(adapters, adapterType); @@ -59,13 +67,14 @@ public class ModelStoreBuilderImpl implements ModelStoreBuilder { @Override public ModelStore build() { + // First configure adapters and let them register any symbols we don't know about yet. + for (int i = adapters.size() - 1; i >= 0; i--) { + adapters.get(i).configure(this); + } var stores = new HashMap>(allSymbols.size()); for (var entry : equivalenceClasses.entrySet()) { createStores(stores, entry.getKey(), entry.getValue()); } - for (int i = adapters.size() - 1; i >= 0; i--) { - adapters.get(i).configure(this); - } var modelStore = new ModelStoreImpl(stores, adapters.size()); for (var adapterBuilder : adapters) { var storeAdapter = adapterBuilder.build(modelStore); diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/AbstractDomain.java b/subprojects/store/src/main/java/tools/refinery/store/representation/AbstractDomain.java index 52c740e8..dfdb43bd 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/representation/AbstractDomain.java +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/AbstractDomain.java @@ -5,6 +5,7 @@ */ package tools.refinery.store.representation; +import java.util.Objects; import java.util.Optional; public non-sealed interface AbstractDomain extends AnyAbstractDomain { @@ -22,7 +23,9 @@ public non-sealed interface AbstractDomain extends AnyAbstractDomain { return toConcrete(abstractValue).isPresent(); } - boolean isRefinement(A originalValue, A refinedValue); + default boolean isRefinement(A originalValue, A refinedValue) { + return Objects.equals(commonRefinement(originalValue, refinedValue), refinedValue); + } A commonRefinement(A leftValue, A rightValue); diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValue.java b/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValue.java index 40baf9a5..f81ee9a4 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValue.java +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValue.java @@ -36,6 +36,10 @@ public enum TruthValue { return this != UNKNOWN; } + public boolean isConcrete() { + return this == TRUE || this == FALSE; + } + public boolean must() { return this == TRUE || this == ERROR; } @@ -55,9 +59,18 @@ public enum TruthValue { public TruthValue merge(TruthValue other) { return switch (this) { case TRUE -> other == UNKNOWN || other == TRUE ? TRUE : ERROR; - case FALSE -> other == TruthValue.UNKNOWN || other == TruthValue.FALSE ? FALSE : ERROR; + case FALSE -> other == UNKNOWN || other == FALSE ? FALSE : ERROR; case UNKNOWN -> other; - default -> ERROR; + case ERROR -> ERROR; + }; + } + + public TruthValue join(TruthValue other) { + return switch (this) { + case TRUE -> other == ERROR || other == TRUE ? TRUE : UNKNOWN; + case FALSE -> other == ERROR || other == FALSE ? FALSE : UNKNOWN; + case UNKNOWN -> UNKNOWN; + case ERROR -> other; }; } } diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValueDomain.java b/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValueDomain.java index 89f8dd19..61696dca 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValueDomain.java +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/TruthValueDomain.java @@ -7,6 +7,8 @@ package tools.refinery.store.representation; import java.util.Optional; +// Singleton pattern, because there is only one domain for truth values. +@SuppressWarnings("squid:S6548") public final class TruthValueDomain implements AbstractDomain { public static final TruthValueDomain INSTANCE = new TruthValueDomain(); @@ -15,51 +17,50 @@ public final class TruthValueDomain implements AbstractDomain abstractType() { - return null; + return TruthValue.class; } @Override public Class concreteType() { - return null; + return Boolean.class; } @Override public TruthValue toAbstract(Boolean concreteValue) { - return null; + return TruthValue.toTruthValue(concreteValue); } @Override public Optional toConcrete(TruthValue abstractValue) { - return Optional.empty(); + return switch (abstractValue) { + case TRUE -> Optional.of(true); + case FALSE -> Optional.of(false); + default -> Optional.empty(); + }; } @Override public boolean isConcrete(TruthValue abstractValue) { - return AbstractDomain.super.isConcrete(abstractValue); - } - - @Override - public boolean isRefinement(TruthValue originalValue, TruthValue refinedValue) { - return false; + return abstractValue.isConcrete(); } @Override public TruthValue commonRefinement(TruthValue leftValue, TruthValue rightValue) { - return null; + return leftValue.merge(rightValue); } @Override public TruthValue commonAncestor(TruthValue leftValue, TruthValue rightValue) { - return null; + return leftValue.join(rightValue); } @Override public TruthValue unknown() { - return null; + return TruthValue.UNKNOWN; } @Override public boolean isError(TruthValue abstractValue) { - return false; + return !abstractValue.isConsistent(); } } diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple.java index aae7b344..e9761763 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple.java +++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple.java @@ -12,6 +12,8 @@ public sealed interface Tuple extends Comparable permits Tuple0, Tuple1, int get(int element); + Tuple set(int element, int value); + @Override default int compareTo(@NotNull Tuple other) { int size = getSize(); diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple0.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple0.java index a9aa9bf2..5f525798 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple0.java +++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple0.java @@ -28,6 +28,11 @@ public final class Tuple0 implements Tuple { throw new IndexOutOfBoundsException(element); } + @Override + public Tuple set(int element, int value) { + throw new IndexOutOfBoundsException(element); + } + @Override public String toString() { return TUPLE_BEGIN + TUPLE_END; diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple1.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple1.java index 388ee3a9..fb9497d2 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple1.java +++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple1.java @@ -37,6 +37,14 @@ public final class Tuple1 implements Tuple { throw new IndexOutOfBoundsException(element); } + @Override + public Tuple set(int element, int value) { + if (element == 0) { + return Tuple.of(value); + } + throw new IndexOutOfBoundsException(element); + } + @Override public String toString() { return TUPLE_BEGIN + value0 + TUPLE_END; diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple2.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple2.java index 6d886fd3..2213df97 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple2.java +++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple2.java @@ -24,6 +24,15 @@ public record Tuple2(int value0, int value1) implements Tuple { }; } + @Override + public Tuple set(int element, int value) { + return switch (element) { + case 0 -> Tuple.of(value, value1); + case 1 -> Tuple.of(value0, value); + default -> throw new ArrayIndexOutOfBoundsException(element); + }; + } + @Override public String toString() { return TUPLE_BEGIN + value0 + TUPLE_SEPARATOR + value1 + TUPLE_END; diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple3.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple3.java index 734e45c2..417770e8 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple3.java +++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple3.java @@ -25,6 +25,16 @@ public record Tuple3(int value0, int value1, int value2) implements Tuple { }; } + @Override + public Tuple set(int element, int value) { + return switch (element) { + case 0 -> Tuple.of(value, value1, value2); + case 1 -> Tuple.of(value0, value, value2); + case 2 -> Tuple.of(value0, value1, value); + default -> throw new ArrayIndexOutOfBoundsException(element); + }; + } + @Override public String toString() { return TUPLE_BEGIN + value0 + TUPLE_SEPARATOR + value1 + TUPLE_SEPARATOR + value2 + TUPLE_END; diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple4.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple4.java index e1b93e7b..c4915198 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple4.java +++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/Tuple4.java @@ -26,6 +26,17 @@ public record Tuple4(int value0, int value1, int value2, int value3) implements }; } + @Override + public Tuple set(int element, int value) { + return switch (element) { + case 0 -> Tuple.of(value, value1, value2, value3); + case 1 -> Tuple.of(value0, value, value2, value3); + case 2 -> Tuple.of(value0, value1, value, value3); + case 3 -> Tuple.of(value0, value1, value2, value); + default -> throw new ArrayIndexOutOfBoundsException(element); + }; + } + @Override public String toString() { return TUPLE_BEGIN + value0 + TUPLE_SEPARATOR + value1 + TUPLE_SEPARATOR + value2 + TUPLE_SEPARATOR + value3 + diff --git a/subprojects/store/src/main/java/tools/refinery/store/tuple/TupleN.java b/subprojects/store/src/main/java/tools/refinery/store/tuple/TupleN.java index b66af491..b42b4b6a 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/tuple/TupleN.java +++ b/subprojects/store/src/main/java/tools/refinery/store/tuple/TupleN.java @@ -31,6 +31,16 @@ public final class TupleN implements Tuple { return values[element]; } + @Override + public Tuple set(int element, int value) { + int size = getSize(); + var newValues = new int[size]; + for (int i = 0; i < size; i++) { + newValues[i] = element == i ? value : values[i]; + } + return Tuple.of(newValues); + } + @Override public String toString() { var valuesString = Arrays.stream(values) -- cgit v1.2.3-54-g00ecf