From 0bdb400deef88cb2a7c0b8c90afebf84b29c04d5 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Sat, 9 Sep 2023 12:57:49 +0200 Subject: feat: integrate DSE with partial interpretation --- subprojects/language-semantics/build.gradle.kts | 3 + .../language/semantics/model/ModelInitializer.java | 23 +- .../semantics/model/CountPropagationTest.java | 82 +++++++ .../semantics/model/ModelGenerationTest.java | 272 +++++++++++++++++++++ .../store/dse/propagation/BoundPropagator.java | 11 + .../store/dse/propagation/PropagationAdapter.java | 20 ++ .../store/dse/propagation/PropagationBuilder.java | 32 +++ .../store/dse/propagation/PropagationResult.java | 28 +++ .../dse/propagation/PropagationStoreAdapter.java | 14 ++ .../refinery/store/dse/propagation/Propagator.java | 17 ++ .../propagation/impl/PropagationAdapterImpl.java | 72 ++++++ .../propagation/impl/PropagationBuilderImpl.java | 53 ++++ .../impl/PropagationStoreAdapterImpl.java | 38 +++ .../impl/rule/BoundPropagationRule.java | 37 +++ .../impl/rule/BoundRuleBasedPropagator.java | 43 ++++ .../propagation/impl/rule/RuleBasedPropagator.java | 36 +++ .../store/dse/strategy/BestFirstExplorer.java | 8 +- .../store/dse/strategy/BestFirstWorker.java | 63 ++--- .../store/dse/transition/actions/BoundAction.java | 23 +- .../dse/transition/objectives/QueryObjective.java | 4 +- .../statespace/internal/ActivationStoreImpl.java | 23 +- .../statespace/internal/ActivationStoreWorker.java | 6 +- .../reasoning/scope/BoundScopePropagator.java | 229 +++++++++++++++++ .../reasoning/scope/LowerTypeScopePropagator.java | 86 +++++++ .../store/reasoning/scope/RoundingUtil.java | 26 ++ .../store/reasoning/scope/ScopePropagator.java | 102 ++++++++ .../reasoning/scope/ScopePropagatorAdapter.java | 21 -- .../reasoning/scope/ScopePropagatorBuilder.java | 21 -- .../scope/ScopePropagatorStoreAdapter.java | 16 -- .../store/reasoning/scope/TypeScopePropagator.java | 66 +++++ .../reasoning/scope/UpperTypeScopePropagator.java | 59 +++++ .../scope/internal/LowerTypeScopePropagator.java | 86 ------- .../reasoning/scope/internal/RoundingUtil.java | 26 -- .../scope/internal/ScopePropagatorAdapterImpl.java | 253 ------------------- .../scope/internal/ScopePropagatorBuilderImpl.java | 86 ------- .../internal/ScopePropagatorStoreAdapterImpl.java | 58 ----- .../scope/internal/TypeScopePropagator.java | 67 ----- .../scope/internal/UpperTypeScopePropagator.java | 59 ----- .../store/reasoning/scope/MultiObjectTest.java | 38 +-- .../store/reasoning/scope/RoundingUtilTest.java | 69 ++++++ .../reasoning/scope/internal/RoundingUtilTest.java | 69 ------ .../reasoning/actions/CleanupActionLiteral.java | 43 ++++ .../reasoning/actions/PartialActionLiterals.java | 4 + .../reasoning/internal/ReasoningBuilderImpl.java | 9 +- .../internal/ReasoningStoreAdapterImpl.java | 6 + .../reasoning/refinement/RefinementResult.java | 24 -- .../ContainmentHierarchyTranslator.java | 2 +- .../containment/InferredContainment.java | 44 +++- .../multiobject/MultiObjectTranslator.java | 21 ++ .../translator/typehierarchy/InferredType.java | 45 +++- .../typehierarchy/TypeHierarchyTranslator.java | 15 +- .../cardinality/FiniteUpperCardinality.java | 13 + .../cardinality/NonEmptyCardinalityInterval.java | 14 ++ .../cardinality/UnboundedUpperCardinality.java | 10 + 54 files changed, 1719 insertions(+), 876 deletions(-) create mode 100644 subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/CountPropagationTest.java create mode 100644 subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/ModelGenerationTest.java create mode 100644 subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/BoundPropagator.java create mode 100644 subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationAdapter.java create mode 100644 subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationBuilder.java create mode 100644 subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationResult.java create mode 100644 subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationStoreAdapter.java create mode 100644 subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/Propagator.java create mode 100644 subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationAdapterImpl.java create mode 100644 subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationBuilderImpl.java create mode 100644 subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationStoreAdapterImpl.java create mode 100644 subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/BoundPropagationRule.java create mode 100644 subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/BoundRuleBasedPropagator.java create mode 100644 subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/RuleBasedPropagator.java create mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/BoundScopePropagator.java create mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/LowerTypeScopePropagator.java create mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/RoundingUtil.java create mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagator.java delete mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorAdapter.java delete mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorBuilder.java delete mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorStoreAdapter.java create mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/TypeScopePropagator.java create mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/UpperTypeScopePropagator.java delete mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/LowerTypeScopePropagator.java delete mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/RoundingUtil.java delete mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorAdapterImpl.java delete mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorBuilderImpl.java delete mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorStoreAdapterImpl.java delete mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/TypeScopePropagator.java delete mode 100644 subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/UpperTypeScopePropagator.java create mode 100644 subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/RoundingUtilTest.java delete mode 100644 subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/internal/RoundingUtilTest.java create mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/CleanupActionLiteral.java delete mode 100644 subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementResult.java diff --git a/subprojects/language-semantics/build.gradle.kts b/subprojects/language-semantics/build.gradle.kts index 4374f78c..338ae345 100644 --- a/subprojects/language-semantics/build.gradle.kts +++ b/subprojects/language-semantics/build.gradle.kts @@ -16,4 +16,7 @@ dependencies { api(project(":refinery-store-reasoning")) implementation(project(":refinery-store-reasoning-scope")) runtimeOnly(libs.eclipseCollections) + testImplementation(project(":refinery-store-dse-visualization")) + testImplementation(project(":refinery-store-query-viatra")) + testImplementation(testFixtures(project(":refinery-language"))) } diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java index 89c41a8e..a14b40d0 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/model/ModelInitializer.java @@ -13,6 +13,7 @@ import tools.refinery.language.semantics.model.internal.MutableSeed; import tools.refinery.language.utils.BuiltinSymbols; import tools.refinery.language.utils.ProblemDesugarer; import tools.refinery.language.utils.ProblemUtil; +import tools.refinery.store.dse.propagation.PropagationBuilder; import tools.refinery.store.model.ModelStoreBuilder; import tools.refinery.store.query.Constraint; import tools.refinery.store.query.dnf.InvalidClauseException; @@ -24,7 +25,7 @@ import tools.refinery.store.query.term.Variable; import tools.refinery.store.reasoning.ReasoningAdapter; import tools.refinery.store.reasoning.representation.AnyPartialSymbol; import tools.refinery.store.reasoning.representation.PartialRelation; -import tools.refinery.store.reasoning.scope.ScopePropagatorBuilder; +import tools.refinery.store.reasoning.scope.ScopePropagator; import tools.refinery.store.reasoning.seed.ModelSeed; import tools.refinery.store.reasoning.seed.Seed; import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator; @@ -73,7 +74,9 @@ public class ModelInitializer { private Metamodel metamodel; - private Map countSeed = new LinkedHashMap<>(); + private final Map countSeed = new LinkedHashMap<>(); + + private ScopePropagator scopePropagator; private ModelSeed modelSeed; @@ -139,6 +142,12 @@ public class ModelInitializer { modelSeedBuilder.seed(partialRelation, info.toSeed(nodeCount)); } collectScopes(); + if (scopePropagator != null) { + if (storeBuilder.tryGetAdapter(PropagationBuilder.class).isEmpty()) { + throw new TracedException(problem, "Type scopes require a PropagationBuilder"); + } + storeBuilder.with(scopePropagator); + } modelSeedBuilder.seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder .reducedValue(CardinalityIntervals.SET) .putAll(countSeed)); @@ -534,8 +543,7 @@ public class ModelInitializer { } } - private void toLiterals(Expr expr, Map localScope, + private void toLiterals(Expr expr, Map localScope, List literals) { if (expr instanceof LogicConstant logicConstant) { switch (logicConstant.getLogicValue()) { @@ -645,14 +653,15 @@ public class ModelInitializer { } private void collectTypeScope(TypeScope typeScope) { - var scopePropagatorBuilder = storeBuilder.tryGetAdapter(ScopePropagatorBuilder.class).orElseThrow( - () -> new TracedException(typeScope, "Type scopes require a ScopePropagatorBuilder")); var type = relationTrace.get(typeScope.getTargetType()); if (type == null) { throw new TracedException(typeScope, "Unknown target type"); } var interval = getCardinalityInterval(typeScope.getMultiplicity()); - scopePropagatorBuilder.scope(type, interval); + if (scopePropagator == null) { + scopePropagator = new ScopePropagator(); + } + scopePropagator.scope(type, interval); } private record RelationInfo(PartialRelation partialRelation, MutableSeed assertions, diff --git a/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/CountPropagationTest.java b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/CountPropagationTest.java new file mode 100644 index 00000000..a383d043 --- /dev/null +++ b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/CountPropagationTest.java @@ -0,0 +1,82 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.semantics.model; + +import org.junit.jupiter.api.Test; +import tools.refinery.store.dse.propagation.PropagationAdapter; +import tools.refinery.store.dse.propagation.PropagationResult; +import tools.refinery.store.dse.transition.DesignSpaceExplorationAdapter; +import tools.refinery.store.model.ModelStore; +import tools.refinery.store.query.viatra.ViatraModelQueryAdapter; +import tools.refinery.store.reasoning.ReasoningAdapter; +import tools.refinery.store.reasoning.ReasoningStoreAdapter; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.scope.ScopePropagator; +import tools.refinery.store.reasoning.seed.ModelSeed; +import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; +import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchy; +import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchyTranslator; +import tools.refinery.store.representation.TruthValue; +import tools.refinery.store.representation.cardinality.CardinalityIntervals; +import tools.refinery.store.tuple.Tuple; + +import static org.hamcrest.MatcherAssert.assertThat; +import static org.hamcrest.Matchers.is; + +class CountPropagationTest { + @Test + void countPropagationTest() { + var a1 = new PartialRelation("A1", 1); + var c1 = new PartialRelation("C1", 1); + var c2 = new PartialRelation("C2", 1); + + var typeHierarchy = TypeHierarchy.builder() + .type(a1, true) + .type(c1, a1) + .type(c2, a1) + .build(); + + var store = ModelStore.builder() + .with(ViatraModelQueryAdapter.builder()) + .with(PropagationAdapter.builder()) + .with(DesignSpaceExplorationAdapter.builder()) + .with(ReasoningAdapter.builder()) + .with(new MultiObjectTranslator()) + .with(new TypeHierarchyTranslator(typeHierarchy)) + .with(new ScopePropagator() + .scope(a1, CardinalityIntervals.between(1000, 1100)) + .scope(c1, CardinalityIntervals.between(100, 150))) + .build(); + + var modelSeed = ModelSeed.builder(4) + .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder + .reducedValue(CardinalityIntervals.ONE) + .put(Tuple.of(0), CardinalityIntervals.SET) + .put(Tuple.of(1), CardinalityIntervals.SET)) + .seed(a1, builder -> builder.reducedValue(TruthValue.UNKNOWN)) + .seed(c1, builder -> builder + .reducedValue(TruthValue.FALSE) + .put(Tuple.of(0), TruthValue.TRUE) + .put(Tuple.of(2), TruthValue.TRUE)) + .seed(c2, builder -> builder + .reducedValue(TruthValue.FALSE) + .put(Tuple.of(1), TruthValue.TRUE) + .put(Tuple.of(3), TruthValue.TRUE)) + .build(); + + var model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed); + var reasoningAdapter = model.getAdapter(ReasoningAdapter.class); + var propagationAdapter = model.getAdapter(PropagationAdapter.class); + model.commit(); + + reasoningAdapter.split(0); + assertThat(propagationAdapter.propagate(), is(PropagationResult.UNCHANGED)); + model.commit(); + + reasoningAdapter.split(0); + assertThat(propagationAdapter.propagate(), is(PropagationResult.UNCHANGED)); + } +} diff --git a/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/ModelGenerationTest.java b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/ModelGenerationTest.java new file mode 100644 index 00000000..779e18ab --- /dev/null +++ b/subprojects/language-semantics/src/test/java/tools/refinery/language/semantics/model/ModelGenerationTest.java @@ -0,0 +1,272 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.semantics.model; + +import com.google.inject.Inject; +import org.eclipse.xtext.testing.InjectWith; +import org.eclipse.xtext.testing.extensions.InjectionExtension; +import org.junit.jupiter.api.Disabled; +import org.junit.jupiter.api.Test; +import org.junit.jupiter.api.extension.ExtendWith; +import tools.refinery.language.ProblemStandaloneSetup; +import tools.refinery.language.model.tests.utils.ProblemParseHelper; +import tools.refinery.language.tests.ProblemInjectorProvider; +import tools.refinery.store.dse.propagation.PropagationAdapter; +import tools.refinery.store.dse.strategy.BestFirstStoreManager; +import tools.refinery.store.dse.transition.DesignSpaceExplorationAdapter; +import tools.refinery.store.model.ModelStore; +import tools.refinery.store.query.viatra.ViatraModelQueryAdapter; +import tools.refinery.store.reasoning.ReasoningAdapter; +import tools.refinery.store.reasoning.ReasoningStoreAdapter; +import tools.refinery.store.reasoning.literal.Concreteness; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchyTranslator; +import tools.refinery.store.statecoding.StateCoderAdapter; +import tools.refinery.visualization.ModelVisualizerAdapter; +import tools.refinery.visualization.internal.FileFormat; + +import java.util.LinkedHashMap; + +import static org.hamcrest.MatcherAssert.assertThat; +import static org.hamcrest.Matchers.empty; + +@ExtendWith(InjectionExtension.class) +@InjectWith(ProblemInjectorProvider.class) +@Disabled("For debugging purposes only") +class ModelGenerationTest { + @Inject + private ProblemParseHelper parseHelper; + + @Inject + private ModelInitializer modelInitializer; + + @Test + void socialNetworkTest() { + var parsedProblem = parseHelper.parse(""" + % Metamodel + class Person { + contains Post posts opposite author + Person friend opposite friend + } + + class Post { + container Person[0..1] author opposite posts + Post replyTo + } + + % Constraints + error replyToNotFriend(Post x, Post y) <-> + replyTo(x, y), + author(x, xAuthor), + author(y, yAuthor), + xAuthor != yAuthor, + !friend(xAuthor, yAuthor). + + error replyToCycle(Post x) <-> replyTo+(x, x). + + % Instance model + !friend(a, b). + author(p1, a). + author(p2, b). + + !author(Post::new, a). + + % Scope + scope Post = 5, Person = 5. + """); + assertThat(parsedProblem.errors(), empty()); + var problem = parsedProblem.problem(); + + var storeBuilder = ModelStore.builder() + .with(ViatraModelQueryAdapter.builder()) + .with(ModelVisualizerAdapter.builder() + .withOutputPath("test_output") + .withFormat(FileFormat.DOT) + .withFormat(FileFormat.SVG) +// .saveStates() + .saveDesignSpace()) + .with(PropagationAdapter.builder()) + .with(StateCoderAdapter.builder()) + .with(DesignSpaceExplorationAdapter.builder()) + .with(ReasoningAdapter.builder()); + + var modelSeed = modelInitializer.createModel(problem, storeBuilder); + + var store = storeBuilder.build(); + + var initialModel = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed); + + var initialVersion = initialModel.commit(); + + var bestFirst = new BestFirstStoreManager(store, 1); + bestFirst.startExploration(initialVersion); + var resultStore = bestFirst.getSolutionStore(); + System.out.println("states size: " + resultStore.getSolutions().size()); +// initialModel.getAdapter(ModelVisualizerAdapter.class).visualize(bestFirst.getVisualizationStore()); + } + + @Test + void statechartTest() { + var parsedProblem = parseHelper.parse(""" + // Metamodel + abstract class CompositeElement { + contains Region[] regions + } + + class Region { + contains Vertex[] vertices opposite region + } + + abstract class Vertex { + container Region[0..1] region opposite vertices + Transition[] outgoingTransition opposite source + Transition[] incomingTransition opposite target + } + + class Transition { + Vertex source opposite outgoingTransition + Vertex target opposite incomingTransition + } + + abstract class Pseudostate extends Vertex {} + + abstract class RegularState extends Vertex {} + + class Entry extends Pseudostate {} + + class Exit extends Pseudostate {} + + class Choice extends Pseudostate {} + + class FinalState extends RegularState {} + + class State extends RegularState, CompositeElement {} + + class Statechart extends CompositeElement {} + + // Constraints + + ///////// + // Entry + ///////// + + pred entryInRegion(Region r, Entry e) <-> + vertices(r, e). + + error noEntryInRegion(Region r) <-> + !entryInRegion(r, _). + + error multipleEntryInRegion(Region r) <-> + entryInRegion(r, e1), + entryInRegion(r, e2), + e1 != e2. + + error incomingToEntry(Transition t, Entry e) <-> + target(t, e). + + error noOutgoingTransitionFromEntry(Entry e) <-> + !source(_, e). + + error multipleTransitionFromEntry(Entry e, Transition t1, Transition t2) <-> + outgoingTransition(e, t1), + outgoingTransition(e, t2), + t1 != t2. + + ///////// + // Exit + ///////// + + error outgoingFromExit(Transition t, Exit e) <-> + source(t, e). + + ///////// + // Final + ///////// + + error outgoingFromFinal(Transition t, FinalState e) <-> + source(t, e). + + ///////// + // State vs Region + ///////// + + pred stateInRegion(Region r, State s) <-> + vertices(r, s). + + error noStateInRegion(Region r) <-> + !stateInRegion(r, _). + + ///////// + // Choice + ///////// + + error choiceHasNoOutgoing(Choice c) <-> + !source(_, c). + + error choiceHasNoIncoming(Choice c) <-> + !target(_, c). + + scope node = 50..60, Statechart = 1. + """); + assertThat(parsedProblem.errors(), empty()); + var problem = parsedProblem.problem(); + + var storeBuilder = ModelStore.builder() + .with(ViatraModelQueryAdapter.builder()) +// .with(ModelVisualizerAdapter.builder() +// .withOutputPath("test_output") +// .withFormat(FileFormat.DOT) +// .withFormat(FileFormat.SVG) +// .saveStates() +// .saveDesignSpace()) + .with(PropagationAdapter.builder()) + .with(StateCoderAdapter.builder()) + .with(DesignSpaceExplorationAdapter.builder()) + .with(ReasoningAdapter.builder()); + + var modelSeed = modelInitializer.createModel(problem, storeBuilder); + + var store = storeBuilder.build(); + + var initialModel = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed); + + var initialVersion = initialModel.commit(); + + var bestFirst = new BestFirstStoreManager(store, 1); + bestFirst.startExploration(initialVersion); + var resultStore = bestFirst.getSolutionStore(); + System.out.println("states size: " + resultStore.getSolutions().size()); + + var model = store.createModelForState(resultStore.getSolutions().get(0).version()); + var interpretation = model.getAdapter(ReasoningAdapter.class) + .getPartialInterpretation(Concreteness.CANDIDATE, ReasoningAdapter.EXISTS_SYMBOL); + var cursor = interpretation.getAll(); + int max = -1; + var types = new LinkedHashMap(); + var typeInterpretation = model.getInterpretation(TypeHierarchyTranslator.TYPE_SYMBOL); + while (cursor.move()) { + max = Math.max(max, cursor.getKey().get(0)); + var type = typeInterpretation.get(cursor.getKey()); + if (type != null) { + types.compute(type.candidateType(), (ignoredKey, oldValue) -> oldValue == null ? 1 : oldValue + 1); + } + } + System.out.println("Model size: " + (max + 1)); + System.out.println(types); +// initialModel.getAdapter(ModelVisualizerAdapter.class).visualize(bestFirst.getVisualizationStore()); + } + + public static void main(String[] args) { + ProblemStandaloneSetup.doSetup(); + var injector = new ProblemStandaloneSetup().createInjectorAndDoEMFRegistration(); + var test = injector.getInstance(ModelGenerationTest.class); + try { + test.statechartTest(); + } catch (AssertionError e) { + e.printStackTrace(); + } + } +} diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/BoundPropagator.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/BoundPropagator.java new file mode 100644 index 00000000..5ad61463 --- /dev/null +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/BoundPropagator.java @@ -0,0 +1,11 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.dse.propagation; + +@FunctionalInterface +public interface BoundPropagator { + PropagationResult propagateOne(); +} diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationAdapter.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationAdapter.java new file mode 100644 index 00000000..3ea5a75f --- /dev/null +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationAdapter.java @@ -0,0 +1,20 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.dse.propagation; + +import tools.refinery.store.adapter.ModelAdapter; +import tools.refinery.store.dse.propagation.impl.PropagationBuilderImpl; + +public interface PropagationAdapter extends ModelAdapter { + @Override + PropagationStoreAdapter getStoreAdapter(); + + PropagationResult propagate(); + + static PropagationBuilder builder() { + return new PropagationBuilderImpl(); + } +} diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationBuilder.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationBuilder.java new file mode 100644 index 00000000..f8a89b30 --- /dev/null +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationBuilder.java @@ -0,0 +1,32 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.dse.propagation; + +import tools.refinery.store.adapter.ModelAdapterBuilder; +import tools.refinery.store.dse.transition.Rule; +import tools.refinery.store.model.ModelStore; + +import java.util.Collection; +import java.util.List; + +@SuppressWarnings("UnusedReturnValue") +public interface PropagationBuilder extends ModelAdapterBuilder { + PropagationBuilder rule(Rule propagationRule); + + default PropagationBuilder rules(Rule... propagationRules) { + return rules(List.of(propagationRules)); + } + + default PropagationBuilder rules(Collection propagationRules) { + propagationRules.forEach(this::rule); + return this; + } + + PropagationBuilder propagator(Propagator propagator); + + @Override + PropagationStoreAdapter build(ModelStore store); +} diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationResult.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationResult.java new file mode 100644 index 00000000..ea56653a --- /dev/null +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationResult.java @@ -0,0 +1,28 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.dse.propagation; + +public enum PropagationResult { + UNCHANGED, + PROPAGATED, + REJECTED; + + public PropagationResult andThen(PropagationResult next) { + return switch (this) { + case UNCHANGED -> next; + case PROPAGATED -> next == REJECTED ? REJECTED : PROPAGATED; + case REJECTED -> REJECTED; + }; + } + + public boolean isRejected() { + return this == REJECTED; + } + + public boolean isChanged() { + return this == PROPAGATED; + } +} diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationStoreAdapter.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationStoreAdapter.java new file mode 100644 index 00000000..82cba909 --- /dev/null +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/PropagationStoreAdapter.java @@ -0,0 +1,14 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.dse.propagation; + +import tools.refinery.store.adapter.ModelStoreAdapter; +import tools.refinery.store.model.Model; + +public interface PropagationStoreAdapter extends ModelStoreAdapter { + @Override + PropagationAdapter createModelAdapter(Model model); +} diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/Propagator.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/Propagator.java new file mode 100644 index 00000000..c6b4e1c9 --- /dev/null +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/Propagator.java @@ -0,0 +1,17 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.dse.propagation; + +import tools.refinery.store.model.Model; +import tools.refinery.store.model.ModelStoreBuilder; + +@FunctionalInterface +public interface Propagator { + default void configure(ModelStoreBuilder storeBuilder) { + } + + BoundPropagator bindToModel(Model model); +} diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationAdapterImpl.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationAdapterImpl.java new file mode 100644 index 00000000..586a8d7a --- /dev/null +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationAdapterImpl.java @@ -0,0 +1,72 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.dse.propagation.impl; + +import tools.refinery.store.dse.propagation.BoundPropagator; +import tools.refinery.store.dse.propagation.PropagationAdapter; +import tools.refinery.store.dse.propagation.PropagationResult; +import tools.refinery.store.dse.propagation.PropagationStoreAdapter; +import tools.refinery.store.model.Model; + +class PropagationAdapterImpl implements PropagationAdapter { + private final Model model; + private final PropagationStoreAdapterImpl storeAdapter; + private final BoundPropagator[] boundPropagators; + + public PropagationAdapterImpl(Model model, PropagationStoreAdapterImpl storeAdapter) { + this.model = model; + this.storeAdapter = storeAdapter; + var propagators = storeAdapter.getPropagators(); + boundPropagators = new BoundPropagator[propagators.size()]; + for (int i = 0; i < boundPropagators.length; i++) { + boundPropagators[i] = propagators.get(i).bindToModel(model); + } + } + + @Override + public PropagationResult propagate() { + PropagationResult result = PropagationResult.UNCHANGED; + PropagationResult lastResult; + do { + lastResult = propagateOne(); + result = result.andThen(lastResult); + } while (lastResult.isChanged()); + return result; + } + + private PropagationResult propagateOne() { + PropagationResult result = PropagationResult.UNCHANGED; + for (int i = 0; i < boundPropagators.length; i++) { + var lastResult = propagateUntilFixedPoint(i); + result = result.andThen(lastResult); + if (result.isRejected()) { + break; + } + } + return result; + } + + private PropagationResult propagateUntilFixedPoint(int propagatorIndex) { + var propagator = boundPropagators[propagatorIndex]; + PropagationResult result = PropagationResult.UNCHANGED; + PropagationResult lastResult; + do { + lastResult = propagator.propagateOne(); + result = result.andThen(lastResult); + } while (lastResult.isChanged()); + return result; + } + + @Override + public Model getModel() { + return model; + } + + @Override + public PropagationStoreAdapter getStoreAdapter() { + return storeAdapter; + } +} diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationBuilderImpl.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationBuilderImpl.java new file mode 100644 index 00000000..c844a89f --- /dev/null +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationBuilderImpl.java @@ -0,0 +1,53 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.dse.propagation.impl; + +import tools.refinery.store.adapter.AbstractModelAdapterBuilder; +import tools.refinery.store.dse.propagation.PropagationBuilder; +import tools.refinery.store.dse.propagation.PropagationStoreAdapter; +import tools.refinery.store.dse.propagation.Propagator; +import tools.refinery.store.dse.propagation.impl.rule.RuleBasedPropagator; +import tools.refinery.store.dse.transition.Rule; +import tools.refinery.store.model.ModelStore; +import tools.refinery.store.model.ModelStoreBuilder; + +import java.util.*; + +public class PropagationBuilderImpl extends AbstractModelAdapterBuilder + implements PropagationBuilder { + private final Set propagationRules = new LinkedHashSet<>(); + private final Deque propagators = new ArrayDeque<>(); + + @Override + public PropagationBuilder rule(Rule propagationRule) { + checkNotConfigured(); + propagationRules.add(propagationRule); + return this; + } + + @Override + public PropagationBuilder propagator(Propagator propagator) { + checkNotConfigured(); + propagators.addFirst(propagator); + return this; + } + + @Override + protected void doConfigure(ModelStoreBuilder storeBuilder) { + super.doConfigure(storeBuilder); + if (!propagationRules.isEmpty()) { + propagators.addFirst(new RuleBasedPropagator(List.copyOf(propagationRules))); + } + for (var propagator : propagators) { + propagator.configure(storeBuilder); + } + } + + @Override + protected PropagationStoreAdapter doBuild(ModelStore store) { + return new PropagationStoreAdapterImpl(store, List.copyOf(propagators)); + } +} diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationStoreAdapterImpl.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationStoreAdapterImpl.java new file mode 100644 index 00000000..a223caed --- /dev/null +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/PropagationStoreAdapterImpl.java @@ -0,0 +1,38 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.dse.propagation.impl; + +import tools.refinery.store.dse.propagation.PropagationAdapter; +import tools.refinery.store.dse.propagation.PropagationStoreAdapter; +import tools.refinery.store.dse.propagation.Propagator; +import tools.refinery.store.model.Model; +import tools.refinery.store.model.ModelStore; + +import java.util.List; + +class PropagationStoreAdapterImpl implements PropagationStoreAdapter { + private final ModelStore store; + private final List propagators; + + PropagationStoreAdapterImpl(ModelStore store, List propagators) { + this.store = store; + this.propagators = propagators; + } + + @Override + public ModelStore getStore() { + return store; + } + + @Override + public PropagationAdapter createModelAdapter(Model model) { + return new PropagationAdapterImpl(model, this); + } + + List getPropagators() { + return propagators; + } +} diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/BoundPropagationRule.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/BoundPropagationRule.java new file mode 100644 index 00000000..6e6a78d2 --- /dev/null +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/BoundPropagationRule.java @@ -0,0 +1,37 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.dse.propagation.impl.rule; + +import tools.refinery.store.dse.propagation.PropagationResult; +import tools.refinery.store.dse.transition.Rule; +import tools.refinery.store.dse.transition.actions.BoundAction; +import tools.refinery.store.model.Model; +import tools.refinery.store.query.ModelQueryAdapter; +import tools.refinery.store.query.resultset.ResultSet; + +class BoundPropagationRule { + private final ResultSet resultSet; + private final BoundAction action; + + public BoundPropagationRule(Model model, Rule rule) { + resultSet = model.getAdapter(ModelQueryAdapter.class).getResultSet(rule.getPrecondition()); + action = rule.createAction(model); + } + + public PropagationResult fireAll() { + if (resultSet.size() == 0) { + return PropagationResult.UNCHANGED; + } + var cursor = resultSet.getAll(); + while (cursor.move()) { + var result = action.fire(cursor.getKey()); + if (!result) { + return PropagationResult.REJECTED; + } + } + return PropagationResult.PROPAGATED; + } +} diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/BoundRuleBasedPropagator.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/BoundRuleBasedPropagator.java new file mode 100644 index 00000000..bd03f923 --- /dev/null +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/BoundRuleBasedPropagator.java @@ -0,0 +1,43 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.dse.propagation.impl.rule; + +import tools.refinery.store.dse.propagation.BoundPropagator; +import tools.refinery.store.dse.propagation.PropagationResult; +import tools.refinery.store.dse.transition.Rule; +import tools.refinery.store.model.Model; +import tools.refinery.store.query.ModelQueryAdapter; + +import java.util.List; + +public class BoundRuleBasedPropagator implements BoundPropagator { + private final ModelQueryAdapter queryEngine; + private final BoundPropagationRule[] boundRules; + + public BoundRuleBasedPropagator(Model model, List propagationRules) { + queryEngine = model.getAdapter(ModelQueryAdapter.class); + boundRules = new BoundPropagationRule[propagationRules.size()]; + for (int i = 0; i < boundRules.length; i++) { + boundRules[i] = new BoundPropagationRule(model, propagationRules.get(i)); + } + } + + @Override + public PropagationResult propagateOne() { + queryEngine.flushChanges(); + PropagationResult result = PropagationResult.UNCHANGED; + // Use a classic for loop to avoid allocating an iterator. + //noinspection ForLoopReplaceableByForEach + for (int i = 0; i < boundRules.length; i++) { + var lastResult = boundRules[i].fireAll(); + result = result.andThen(lastResult); + if (result.isRejected()) { + break; + } + } + return result; + } +} diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/RuleBasedPropagator.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/RuleBasedPropagator.java new file mode 100644 index 00000000..709b2416 --- /dev/null +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/propagation/impl/rule/RuleBasedPropagator.java @@ -0,0 +1,36 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.dse.propagation.impl.rule; + +import tools.refinery.store.dse.propagation.BoundPropagator; +import tools.refinery.store.dse.propagation.Propagator; +import tools.refinery.store.dse.transition.Rule; +import tools.refinery.store.model.Model; +import tools.refinery.store.model.ModelStoreBuilder; +import tools.refinery.store.query.ModelQueryBuilder; + +import java.util.List; + +public class RuleBasedPropagator implements Propagator { + private final List propagationRules; + + public RuleBasedPropagator(List propagationRules) { + this.propagationRules = propagationRules; + } + + @Override + public void configure(ModelStoreBuilder storeBuilder) { + var queryBuilder = storeBuilder.getAdapter(ModelQueryBuilder.class); + for (var propagationRule : propagationRules) { + queryBuilder.query(propagationRule.getPrecondition()); + } + } + + @Override + public BoundPropagator bindToModel(Model model) { + return new BoundRuleBasedPropagator(model, propagationRules); + } +} diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstExplorer.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstExplorer.java index 8f7e3bdc..4a75a3a6 100644 --- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstExplorer.java +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstExplorer.java @@ -33,7 +33,11 @@ public class BestFirstExplorer extends BestFirstWorker { var lastBest = submit().newVersion(); while (shouldRun()) { if (lastBest == null) { - lastBest = restoreToBest(); + if (random.nextInt(10) == 0) { + lastBest = restoreToRandom(random); + } else { + lastBest = restoreToBest(); + } if (lastBest == null) { return; } @@ -49,7 +53,7 @@ public class BestFirstExplorer extends BestFirstWorker { } else { var newVisit = newSubmit.newVersion(); int compareResult = compare(lastBest, newVisit); - if (compareResult >= 0) { + if (compareResult >= 0) { lastBest = newVisit; } else { lastBest = null; diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstWorker.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstWorker.java index 5d738297..aca800a3 100644 --- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstWorker.java +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/strategy/BestFirstWorker.java @@ -5,6 +5,8 @@ */ package tools.refinery.store.dse.strategy; +import org.jetbrains.annotations.Nullable; +import tools.refinery.store.dse.propagation.PropagationAdapter; import tools.refinery.store.dse.transition.DesignSpaceExplorationAdapter; import tools.refinery.store.dse.transition.ObjectiveValue; import tools.refinery.store.dse.transition.VersionWithObjectiveValue; @@ -24,6 +26,7 @@ public class BestFirstWorker { final StateCoderAdapter stateCoderAdapter; final DesignSpaceExplorationAdapter explorationAdapter; final ModelQueryAdapter queryAdapter; + final @Nullable PropagationAdapter propagationAdapter; final VisualizationStore visualizationStore; final boolean isVisualizationEnabled; @@ -34,6 +37,7 @@ public class BestFirstWorker { explorationAdapter = model.getAdapter(DesignSpaceExplorationAdapter.class); stateCoderAdapter = model.getAdapter(StateCoderAdapter.class); queryAdapter = model.getAdapter(ModelQueryAdapter.class); + propagationAdapter = model.tryGetAdapter(PropagationAdapter.class).orElse(null); activationStoreWorker = new ActivationStoreWorker(storeManager.getActivationStore(), explorationAdapter.getTransformations()); visualizationStore = storeManager.getVisualizationStore(); @@ -96,7 +100,11 @@ public class BestFirstWorker { } public VersionWithObjectiveValue restoreToRandom(Random random) { - var randomVersion = storeManager.getObjectiveStore().getRandom(random); + var objectiveStore = storeManager.getObjectiveStore(); + if (objectiveStore.getSize() == 0) { + return null; + } + var randomVersion = objectiveStore.getRandom(random); last = randomVersion; if (randomVersion != null) { this.model.restore(randomVersion.version()); @@ -108,41 +116,40 @@ public class BestFirstWorker { return storeManager.getObjectiveStore().getComparator().compare(s1, s2); } - public boolean stateHasUnvisited() { - if (!model.hasUncommittedChanges()) { - return storeManager.getActivationStore().hasUnmarkedActivation(last); - } else { - throw new IllegalStateException("The model has uncommitted changes!"); - } - } - public record RandomVisitResult(SubmitResult submitResult, boolean shouldRetry) { } public RandomVisitResult visitRandomUnvisited(Random random) { checkSynchronized(); - if (!model.hasUncommittedChanges()) { - var visitResult = activationStoreWorker.fireRandomActivation(this.last, random); - queryAdapter.flushChanges(); - - if (visitResult.successfulVisit()) { - Version oldVersion = null; - if (isVisualizationEnabled) { - oldVersion = last.version(); - } - var submitResult = submit(); - if (isVisualizationEnabled && submitResult.newVersion() != null) { - var newVersion = submitResult.newVersion().version(); - visualizationStore.addTransition(oldVersion, newVersion, - "fire: " + visitResult.transformation() + ", " + visitResult.activation()); - } - return new RandomVisitResult(submitResult, visitResult.mayHaveMore()); - } else { + if (model.hasUncommittedChanges()) { + throw new IllegalStateException("The model has uncommitted changes!"); + } + + var visitResult = activationStoreWorker.fireRandomActivation(this.last, random); + + if (!visitResult.successfulVisit()) { + return new RandomVisitResult(null, visitResult.mayHaveMore()); + } + + if (propagationAdapter != null) { + var propagationResult = propagationAdapter.propagate(); + if (propagationResult.isRejected()) { return new RandomVisitResult(null, visitResult.mayHaveMore()); } - } else { - throw new IllegalStateException("The model has uncommitted changes!"); } + queryAdapter.flushChanges(); + + Version oldVersion = null; + if (isVisualizationEnabled) { + oldVersion = last.version(); + } + var submitResult = submit(); + if (isVisualizationEnabled && submitResult.newVersion() != null) { + var newVersion = submitResult.newVersion().version(); + visualizationStore.addTransition(oldVersion, newVersion, + "fire: " + visitResult.transformation() + ", " + visitResult.activation()); + } + return new RandomVisitResult(submitResult, visitResult.mayHaveMore()); } public boolean hasEnoughSolution() { diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/actions/BoundAction.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/actions/BoundAction.java index 55f43735..ed2ff33d 100644 --- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/actions/BoundAction.java +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/actions/BoundAction.java @@ -11,18 +11,14 @@ import tools.refinery.store.tuple.Tuple; public class BoundAction { private final Action action; - private final BoundActionLiteral[] boundLiterals; + private final Model model; + private BoundActionLiteral @Nullable [] boundLiterals; private Tuple activation; private final int[] localVariables; BoundAction(Action action, Model model) { this.action = action; - var actionLiterals = action.getActionLiterals(); - int size = actionLiterals.size(); - boundLiterals = new BoundActionLiteral[size]; - for (int i = 0; i < size; i++) { - boundLiterals[i] = actionLiterals.get(i).bindToModel(model); - } + this.model = model; localVariables = new int[action.getLocalVariables().size()]; } @@ -31,6 +27,9 @@ public class BoundAction { throw new IllegalStateException("Reentrant firing is not allowed"); } this.activation = activation; + if (boundLiterals == null) { + boundLiterals = bindLiterals(); + } try { int size = boundLiterals.length; for (int i = 0; i < size; i++) { @@ -50,6 +49,16 @@ public class BoundAction { return true; } + private BoundActionLiteral[] bindLiterals() { + var actionLiterals = action.getActionLiterals(); + int size = actionLiterals.size(); + var boundLiteralsArray = new BoundActionLiteral[size]; + for (int i = 0; i < size; i++) { + boundLiteralsArray[i] = actionLiterals.get(i).bindToModel(model); + } + return boundLiteralsArray; + } + private Tuple getInputTuple(int @Nullable [] inputAllocation) { if (inputAllocation == null) { // Identity allocation. diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/QueryObjective.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/QueryObjective.java index 9f4bb536..5a7ba8f4 100644 --- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/QueryObjective.java +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/objectives/QueryObjective.java @@ -28,9 +28,9 @@ public class QueryObjective implements Objective { return () -> { var cursor = resultSet.getAll(); if (!cursor.move()) { - throw new IllegalStateException("Query providing the objective function has no values!"); + return 0; } - return cursor.getValue().doubleValue(); + return Math.max(cursor.getValue().doubleValue(), 0); }; } diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreImpl.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreImpl.java index d9e29eca..82f89db7 100644 --- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreImpl.java +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreImpl.java @@ -104,9 +104,16 @@ public class ActivationStoreImpl implements ActivationStore { public synchronized VisitResult getRandomAndMarkAsVisited(VersionWithObjectiveValue version, Random random) { var entries = versionToActivations.get(version); + var weights = new double[entries.size()]; + double totalWeight = 0; int numberOfAllUnvisitedActivations = 0; - for (var entry : entries) { - numberOfAllUnvisitedActivations += entry.getNumberOfUnvisitedActivations(); + for (int i = 0; i < weights.length; i++) { + var entry = entries.get(i); + int unvisited = entry.getNumberOfUnvisitedActivations(); + double weight = unvisited == 0 ? 0 : unvisited; //(Math.log(unvisited) + 1.0); + weights[i] = weight; + totalWeight += weight; + numberOfAllUnvisitedActivations += unvisited; } if (numberOfAllUnvisitedActivations == 0) { @@ -114,18 +121,18 @@ public class ActivationStoreImpl implements ActivationStore { return new VisitResult(false, false, -1, -1); } - int offset = random.nextInt(numberOfAllUnvisitedActivations); + double offset = random.nextDouble(totalWeight); int transformation = 0; for (; transformation < entries.size(); transformation++) { - var entry = entries.get(transformation); - int unvisited = entry.getNumberOfUnvisitedActivations(); - if (unvisited > 0 && offset < unvisited) { + double weight = weights[transformation]; + if (weight > 0 && offset < weight) { + var entry = entries.get(transformation); int activation = random.nextInt(entry.getNumberOfActivations()); return this.visitActivation(version, transformation, activation); } - offset -= unvisited; + offset -= weight; } - throw new AssertionError("Unvisited activation %d not found".formatted(offset)); + throw new AssertionError("Unvisited activation %f not found".formatted(offset)); } } diff --git a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreWorker.java b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreWorker.java index 881b133c..1d7c5ce5 100644 --- a/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreWorker.java +++ b/subprojects/store-dse/src/main/java/tools/refinery/store/dse/transition/statespace/internal/ActivationStoreWorker.java @@ -32,7 +32,7 @@ public class ActivationStoreWorker { public ActivationStore.VisitResult fireRandomActivation(VersionWithObjectiveValue thisVersion, Random random) { var result = store.getRandomAndMarkAsVisited(thisVersion, random); - if(result.successfulVisit()) { + if (result.successfulVisit()) { int selectedTransformation = result.transformation(); int selectedActivation = result.activation(); @@ -40,13 +40,13 @@ public class ActivationStoreWorker { var tuple = transformation.getActivation(selectedActivation); boolean success = transformation.fireActivation(tuple); - if(success) { + if (success) { return result; } else { return new ActivationStore.VisitResult( false, result.mayHaveMore(), - selectedActivation, + selectedTransformation, selectedActivation); } } diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/BoundScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/BoundScopePropagator.java new file mode 100644 index 00000000..62aadb4a --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/BoundScopePropagator.java @@ -0,0 +1,229 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.scope; + +import com.google.ortools.linearsolver.MPConstraint; +import com.google.ortools.linearsolver.MPObjective; +import com.google.ortools.linearsolver.MPSolver; +import com.google.ortools.linearsolver.MPVariable; +import org.eclipse.collections.api.factory.primitive.IntObjectMaps; +import org.eclipse.collections.api.factory.primitive.IntSets; +import org.eclipse.collections.api.map.primitive.MutableIntObjectMap; +import org.eclipse.collections.api.set.primitive.MutableIntSet; +import tools.refinery.store.dse.propagation.BoundPropagator; +import tools.refinery.store.dse.propagation.PropagationResult; +import tools.refinery.store.model.Interpretation; +import tools.refinery.store.model.Model; +import tools.refinery.store.query.ModelQueryAdapter; +import tools.refinery.store.representation.cardinality.*; +import tools.refinery.store.tuple.Tuple; + +class BoundScopePropagator implements BoundPropagator { + private final ModelQueryAdapter queryEngine; + private final Interpretation countInterpretation; + private final MPSolver solver; + private final MPObjective objective; + private final MutableIntObjectMap variables = IntObjectMaps.mutable.empty(); + private final MutableIntSet activeVariables = IntSets.mutable.empty(); + private final TypeScopePropagator[] propagators; + private boolean changed = true; + + public BoundScopePropagator(Model model, ScopePropagator storeAdapter) { + queryEngine = model.getAdapter(ModelQueryAdapter.class); + countInterpretation = model.getInterpretation(storeAdapter.getCountSymbol()); + solver = MPSolver.createSolver("GLOP"); + objective = solver.objective(); + initializeVariables(); + countInterpretation.addListener(this::countChanged, true); + var propagatorFactories = storeAdapter.getTypeScopePropagatorFactories(); + propagators = new TypeScopePropagator[propagatorFactories.size()]; + for (int i = 0; i < propagators.length; i++) { + propagators[i] = propagatorFactories.get(i).createPropagator(this); + } + } + + ModelQueryAdapter getQueryEngine() { + return queryEngine; + } + + private void initializeVariables() { + var cursor = countInterpretation.getAll(); + while (cursor.move()) { + var interval = cursor.getValue(); + if (!interval.equals(CardinalityIntervals.ONE)) { + int nodeId = cursor.getKey().get(0); + createVariable(nodeId, interval); + activeVariables.add(nodeId); + } + } + } + + private MPVariable createVariable(int nodeId, CardinalityInterval interval) { + double lowerBound = interval.lowerBound(); + double upperBound = getUpperBound(interval); + var variable = solver.makeNumVar(lowerBound, upperBound, "x" + nodeId); + variables.put(nodeId, variable); + return variable; + } + + private void countChanged(Tuple key, CardinalityInterval fromValue, CardinalityInterval toValue, + boolean ignoredRestoring) { + int nodeId = key.get(0); + if ((toValue == null || toValue.equals(CardinalityIntervals.ONE))) { + if (fromValue != null && !fromValue.equals(CardinalityIntervals.ONE)) { + removeActiveVariable(toValue, nodeId); + } + return; + } + if (fromValue == null || fromValue.equals(CardinalityIntervals.ONE)) { + activeVariables.add(nodeId); + } + var variable = variables.get(nodeId); + if (variable == null) { + createVariable(nodeId, toValue); + markAsChanged(); + return; + } + double lowerBound = toValue.lowerBound(); + double upperBound = getUpperBound(toValue); + if (variable.lb() != lowerBound) { + variable.setLb(lowerBound); + markAsChanged(); + } + if (variable.ub() != upperBound) { + variable.setUb(upperBound); + markAsChanged(); + } + } + + private void removeActiveVariable(CardinalityInterval toValue, int nodeId) { + var variable = variables.get(nodeId); + if (variable == null || !activeVariables.remove(nodeId)) { + throw new AssertionError("Variable not active: " + nodeId); + } + if (toValue == null) { + variable.setBounds(0, 0); + } else { + // Until queries are flushed and the constraints can be properly updated, + // the variable corresponding to the (previous) multi-object has to stand in for a single object. + variable.setBounds(1, 1); + } + markAsChanged(); + } + + MPConstraint makeConstraint() { + return solver.makeConstraint(); + } + + MPVariable getVariable(int nodeId) { + var variable = variables.get(nodeId); + if (variable != null) { + return variable; + } + var interval = countInterpretation.get(Tuple.of(nodeId)); + if (interval == null || interval.equals(CardinalityIntervals.ONE)) { + interval = CardinalityIntervals.NONE; + } else { + activeVariables.add(nodeId); + markAsChanged(); + } + return createVariable(nodeId, interval); + } + + void markAsChanged() { + changed = true; + } + + @Override + public PropagationResult propagateOne() { + queryEngine.flushChanges(); + if (!changed) { + return PropagationResult.UNCHANGED; + } + changed = false; + for (var propagator : propagators) { + propagator.updateBounds(); + } + var result = PropagationResult.UNCHANGED; + if (activeVariables.isEmpty()) { + return checkEmptiness(); + } + var iterator = activeVariables.intIterator(); + while (iterator.hasNext()) { + int nodeId = iterator.next(); + var variable = variables.get(nodeId); + if (variable == null) { + throw new AssertionError("Missing active variable: " + nodeId); + } + result = result.andThen(propagateNode(nodeId, variable)); + if (result.isRejected()) { + return result; + } + } + return result; + } + + private PropagationResult checkEmptiness() { + var emptinessCheckingResult = solver.solve(); + return switch (emptinessCheckingResult) { + case OPTIMAL, UNBOUNDED -> PropagationResult.UNCHANGED; + case INFEASIBLE -> PropagationResult.REJECTED; + default -> throw new IllegalStateException("Failed to check for consistency: " + emptinessCheckingResult); + }; + } + + private PropagationResult propagateNode(int nodeId, MPVariable variable) { + objective.setCoefficient(variable, 1); + try { + objective.setMinimization(); + var minimizationResult = solver.solve(); + int lowerBound; + switch (minimizationResult) { + case OPTIMAL -> lowerBound = RoundingUtil.roundUp(objective.value()); + case UNBOUNDED -> lowerBound = 0; + case INFEASIBLE -> { + return PropagationResult.REJECTED; + } + default -> throw new IllegalStateException("Failed to solve for minimum of %s: %s" + .formatted(variable, minimizationResult)); + } + + objective.setMaximization(); + var maximizationResult = solver.solve(); + UpperCardinality upperBound; + switch (maximizationResult) { + case OPTIMAL -> upperBound = UpperCardinalities.atMost(RoundingUtil.roundDown(objective.value())); + // Problem was feasible when minimizing, the only possible source of {@code UNBOUNDED_OR_INFEASIBLE} is + // an unbounded maximization problem. See https://github.com/google/or-tools/issues/3319 + case UNBOUNDED, INFEASIBLE -> upperBound = UpperCardinalities.UNBOUNDED; + default -> throw new IllegalStateException("Failed to solve for maximum of %s: %s" + .formatted(variable, minimizationResult)); + } + + var newInterval = CardinalityIntervals.between(lowerBound, upperBound); + var oldInterval = countInterpretation.put(Tuple.of(nodeId), newInterval); + if (newInterval.lowerBound() < oldInterval.lowerBound() || + newInterval.upperBound().compareTo(oldInterval.upperBound()) > 0) { + throw new IllegalArgumentException("Failed to refine multiplicity %s of node %d to %s" + .formatted(oldInterval, nodeId, newInterval)); + } + return newInterval.equals(oldInterval) ? PropagationResult.UNCHANGED : PropagationResult.PROPAGATED; + } finally { + objective.setCoefficient(variable, 0); + } + } + + private static double getUpperBound(CardinalityInterval interval) { + var upperBound = interval.upperBound(); + if (upperBound instanceof FiniteUpperCardinality finiteUpperCardinality) { + return finiteUpperCardinality.finiteUpperBound(); + } else if (upperBound instanceof UnboundedUpperCardinality) { + return Double.POSITIVE_INFINITY; + } else { + throw new IllegalArgumentException("Unknown upper bound: " + upperBound); + } + } +} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/LowerTypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/LowerTypeScopePropagator.java new file mode 100644 index 00000000..5d903f41 --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/LowerTypeScopePropagator.java @@ -0,0 +1,86 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.scope; + +import tools.refinery.store.dse.transition.DesignSpaceExplorationBuilder; +import tools.refinery.store.dse.transition.objectives.Criteria; +import tools.refinery.store.dse.transition.objectives.Objectives; +import tools.refinery.store.model.ModelStoreBuilder; +import tools.refinery.store.query.dnf.AnyQuery; +import tools.refinery.store.query.dnf.Query; +import tools.refinery.store.query.dnf.RelationalQuery; +import tools.refinery.store.query.term.Variable; +import tools.refinery.store.reasoning.ReasoningBuilder; +import tools.refinery.store.reasoning.literal.CountCandidateLowerBoundLiteral; +import tools.refinery.store.reasoning.representation.PartialRelation; + +import java.util.Collection; +import java.util.List; + +import static tools.refinery.store.query.literal.Literals.check; +import static tools.refinery.store.query.term.int_.IntTerms.*; +import static tools.refinery.store.reasoning.literal.PartialLiterals.may; +import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW; + +class LowerTypeScopePropagator extends TypeScopePropagator { + private final int lowerBound; + + private LowerTypeScopePropagator(BoundScopePropagator adapter, int lowerBound, RelationalQuery allQuery, + RelationalQuery multiQuery) { + super(adapter, allQuery, multiQuery); + this.lowerBound = lowerBound; + } + + @Override + public void updateBounds() { + constraint.setLb((lowerBound - getSingleCount())); + } + + public static class Factory extends TypeScopePropagator.Factory { + private final PartialRelation type; + private final int lowerBound; + private final RelationalQuery allMay; + private final RelationalQuery multiMay; + + public Factory(PartialRelation type, int lowerBound) { + this.type = type; + this.lowerBound = lowerBound; + allMay = Query.of(type.name() + "#may", (builder, instance) -> builder.clause( + may(type.call(instance)) + )); + multiMay = Query.of(type.name() + "#multiMay", (builder, instance) -> builder.clause( + may(type.call(instance)), + MULTI_VIEW.call(instance) + )); + } + + @Override + public TypeScopePropagator createPropagator(BoundScopePropagator adapter) { + return new LowerTypeScopePropagator(adapter, lowerBound, allMay, multiMay); + } + + @Override + protected Collection getQueries() { + return List.of(allMay, multiMay); + } + + @Override + public void configure(ModelStoreBuilder storeBuilder) { + super.configure(storeBuilder); + + var requiredObjects = Query.of(type.name() + "#required", Integer.class, (builder, output) -> builder + .clause(Integer.class, candidateLowerBound -> List.of( + new CountCandidateLowerBoundLiteral(candidateLowerBound, type, List.of(Variable.of())), + output.assign(sub(constant(lowerBound), candidateLowerBound)), + check(greater(output, constant(0))) + ))); + + storeBuilder.getAdapter(ReasoningBuilder.class).objective(Objectives.value(requiredObjects)); + storeBuilder.tryGetAdapter(DesignSpaceExplorationBuilder.class).ifPresent(dseBuilder -> + dseBuilder.accept(Criteria.whenNoMatch(requiredObjects))); + } + } +} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/RoundingUtil.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/RoundingUtil.java new file mode 100644 index 00000000..986771a1 --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/RoundingUtil.java @@ -0,0 +1,26 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.scope; + +final class RoundingUtil { + private static final double TOLERANCE = 0.01; + + private RoundingUtil() { + throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); + } + + public static int roundUp(double value) { + double ceil = Math.ceil(value - TOLERANCE); + int intCeil = (int) ceil; + return Math.max(intCeil, 0); + } + + public static int roundDown(double value) { + double floor = Math.floor(value + TOLERANCE); + int intFloor = (int) floor; + return Math.max(intFloor, 0); + } +} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagator.java new file mode 100644 index 00000000..25b1966c --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagator.java @@ -0,0 +1,102 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.scope; + +import com.google.ortools.Loader; +import tools.refinery.store.dse.propagation.PropagationBuilder; +import tools.refinery.store.model.ModelStoreBuilder; +import tools.refinery.store.model.ModelStoreConfiguration; +import tools.refinery.store.reasoning.representation.PartialRelation; +import tools.refinery.store.reasoning.translator.TranslationException; +import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; +import tools.refinery.store.representation.Symbol; +import tools.refinery.store.representation.cardinality.CardinalityInterval; +import tools.refinery.store.representation.cardinality.FiniteUpperCardinality; + +import java.util.*; + +public class ScopePropagator implements ModelStoreConfiguration { + private final Symbol countSymbol; + private final Map scopes = new LinkedHashMap<>(); + private final List typeScopePropagatorFactories = new ArrayList<>(); + + public ScopePropagator() { + this(MultiObjectTranslator.COUNT_STORAGE); + } + + public ScopePropagator(Symbol countSymbol) { + if (countSymbol.arity() != 1) { + throw new IllegalArgumentException("Count symbol must have arty 1, got %s with arity %d instead" + .formatted(countSymbol, countSymbol.arity())); + } + if (!countSymbol.valueType().equals(CardinalityInterval.class)) { + throw new IllegalArgumentException("Count symbol must have CardinalityInterval values"); + } + if (countSymbol.defaultValue() != null) { + throw new IllegalArgumentException("Count symbol must default value null"); + } + this.countSymbol = countSymbol; + } + + public ScopePropagator scope(PartialRelation type, CardinalityInterval interval) { + if (type.arity() != 1) { + throw new TranslationException(type, "Only types with arity 1 may have scopes, got %s with arity %d" + .formatted(type, type.arity())); + } + var newValue = scopes.compute(type, (ignoredKey, oldValue) -> + oldValue == null ? interval : oldValue.meet(interval)); + if (newValue.isEmpty()) { + throw new TranslationException(type, "Unsatisfiable scope for type %s".formatted(type)); + } + return this; + } + + public ScopePropagator scopes(Map scopes) { + return scopes(scopes.entrySet()); + } + + public ScopePropagator scopes(Collection> scopes) { + for (var entry : scopes) { + scope(entry.getKey(), entry.getValue()); + } + return this; + } + + @Override + public void apply(ModelStoreBuilder storeBuilder) { + createTypeScopePropagatorFactories(); + Loader.loadNativeLibraries(); + for (var factory : typeScopePropagatorFactories) { + factory.configure(storeBuilder); + } + storeBuilder.getAdapter(PropagationBuilder.class) + .propagator(model -> new BoundScopePropagator(model, this)); + } + + private void createTypeScopePropagatorFactories() { + for (var entry : scopes.entrySet()) { + var type = entry.getKey(); + var bounds = entry.getValue(); + if (bounds.lowerBound() > 0) { + var lowerFactory = new LowerTypeScopePropagator.Factory(type, bounds.lowerBound()); + typeScopePropagatorFactories.add(lowerFactory); + } + if (bounds.upperBound() instanceof FiniteUpperCardinality finiteUpperCardinality) { + var upperFactory = new UpperTypeScopePropagator.Factory(type, + finiteUpperCardinality.finiteUpperBound()); + typeScopePropagatorFactories.add(upperFactory); + } + } + } + + Symbol getCountSymbol() { + return countSymbol; + } + + List getTypeScopePropagatorFactories() { + return typeScopePropagatorFactories; + } +} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorAdapter.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorAdapter.java deleted file mode 100644 index c2d3f59e..00000000 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorAdapter.java +++ /dev/null @@ -1,21 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.scope; - -import tools.refinery.store.adapter.ModelAdapter; -import tools.refinery.store.reasoning.refinement.RefinementResult; -import tools.refinery.store.reasoning.scope.internal.ScopePropagatorBuilderImpl; - -public interface ScopePropagatorAdapter extends ModelAdapter { - @Override - ScopePropagatorStoreAdapter getStoreAdapter(); - - RefinementResult propagate(); - - static ScopePropagatorBuilder builder() { - return new ScopePropagatorBuilderImpl(); - } -} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorBuilder.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorBuilder.java deleted file mode 100644 index a17e04a4..00000000 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorBuilder.java +++ /dev/null @@ -1,21 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.scope; - -import tools.refinery.store.adapter.ModelAdapterBuilder; -import tools.refinery.store.model.ModelStore; -import tools.refinery.store.reasoning.representation.PartialRelation; -import tools.refinery.store.representation.Symbol; -import tools.refinery.store.representation.cardinality.CardinalityInterval; - -public interface ScopePropagatorBuilder extends ModelAdapterBuilder { - ScopePropagatorBuilder countSymbol(Symbol countSymbol); - - ScopePropagatorBuilder scope(PartialRelation type, CardinalityInterval interval); - - @Override - ScopePropagatorStoreAdapter build(ModelStore store); -} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorStoreAdapter.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorStoreAdapter.java deleted file mode 100644 index 65d9c38d..00000000 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/ScopePropagatorStoreAdapter.java +++ /dev/null @@ -1,16 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.scope; - -import tools.refinery.store.adapter.ModelStoreAdapter; -import tools.refinery.store.reasoning.representation.PartialRelation; -import tools.refinery.store.representation.cardinality.CardinalityInterval; - -import java.util.Map; - -public interface ScopePropagatorStoreAdapter extends ModelStoreAdapter { - Map getScopes(); -} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/TypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/TypeScopePropagator.java new file mode 100644 index 00000000..db80be7f --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/TypeScopePropagator.java @@ -0,0 +1,66 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.scope; + +import com.google.ortools.linearsolver.MPConstraint; +import tools.refinery.store.model.ModelStoreBuilder; +import tools.refinery.store.query.ModelQueryBuilder; +import tools.refinery.store.query.dnf.AnyQuery; +import tools.refinery.store.query.dnf.RelationalQuery; +import tools.refinery.store.query.resultset.ResultSet; +import tools.refinery.store.tuple.Tuple; + +import java.util.Collection; + +abstract class TypeScopePropagator { + private final BoundScopePropagator adapter; + private final ResultSet allNodes; + private final ResultSet multiNodes; + protected final MPConstraint constraint; + + protected TypeScopePropagator(BoundScopePropagator adapter, RelationalQuery allQuery, + RelationalQuery multiQuery) { + this.adapter = adapter; + var queryEngine = adapter.getQueryEngine(); + allNodes = queryEngine.getResultSet(allQuery); + multiNodes = queryEngine.getResultSet(multiQuery); + constraint = adapter.makeConstraint(); + constraint.setBounds(0, Double.POSITIVE_INFINITY); + var cursor = multiNodes.getAll(); + while (cursor.move()) { + var variable = adapter.getVariable(cursor.getKey().get(0)); + constraint.setCoefficient(variable, 1); + } + allNodes.addListener(this::allChanged); + multiNodes.addListener(this::multiChanged); + } + + public abstract void updateBounds(); + + protected int getSingleCount() { + return allNodes.size() - multiNodes.size(); + } + + private void allChanged(Tuple ignoredKey, Boolean ignoredOldValue, Boolean ignoredNewValue) { + adapter.markAsChanged(); + } + + private void multiChanged(Tuple key, Boolean ignoredOldValue, Boolean newValue) { + var variable = adapter.getVariable(key.get(0)); + constraint.setCoefficient(variable, Boolean.TRUE.equals(newValue) ? 1 : 0); + adapter.markAsChanged(); + } + + public abstract static class Factory { + public abstract TypeScopePropagator createPropagator(BoundScopePropagator adapter); + + protected abstract Collection getQueries(); + + public void configure(ModelStoreBuilder storeBuilder) { + storeBuilder.getAdapter(ModelQueryBuilder.class).queries(getQueries()); + } + } +} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/UpperTypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/UpperTypeScopePropagator.java new file mode 100644 index 00000000..062f976c --- /dev/null +++ b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/UpperTypeScopePropagator.java @@ -0,0 +1,59 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.scope; + +import tools.refinery.store.query.dnf.AnyQuery; +import tools.refinery.store.query.dnf.Query; +import tools.refinery.store.query.dnf.RelationalQuery; +import tools.refinery.store.reasoning.representation.PartialRelation; + +import java.util.Collection; +import java.util.List; + +import static tools.refinery.store.reasoning.literal.PartialLiterals.must; +import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW; + +class UpperTypeScopePropagator extends TypeScopePropagator { + private final int upperBound; + + private UpperTypeScopePropagator(BoundScopePropagator adapter, int upperBound, RelationalQuery allQuery, + RelationalQuery multiQuery) { + super(adapter, allQuery, multiQuery); + this.upperBound = upperBound; + } + + @Override + public void updateBounds() { + constraint.setUb(upperBound - getSingleCount()); + } + + public static class Factory extends TypeScopePropagator.Factory { + private final int upperBound; + private final RelationalQuery allMust; + private final RelationalQuery multiMust; + + public Factory(PartialRelation type, int upperBound) { + this.upperBound = upperBound; + allMust = Query.of(type.name() + "#must", (builder, instance) -> builder.clause( + must(type.call(instance)) + )); + multiMust = Query.of(type.name() + "#multiMust", (builder, instance) -> builder.clause( + must(type.call(instance)), + MULTI_VIEW.call(instance) + )); + } + + @Override + public TypeScopePropagator createPropagator(BoundScopePropagator adapter) { + return new UpperTypeScopePropagator(adapter, upperBound, allMust, multiMust); + } + + @Override + protected Collection getQueries() { + return List.of(allMust, multiMust); + } + } +} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/LowerTypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/LowerTypeScopePropagator.java deleted file mode 100644 index 393c4b72..00000000 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/LowerTypeScopePropagator.java +++ /dev/null @@ -1,86 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.scope.internal; - -import tools.refinery.store.dse.transition.DesignSpaceExplorationBuilder; -import tools.refinery.store.dse.transition.objectives.Criteria; -import tools.refinery.store.dse.transition.objectives.Objectives; -import tools.refinery.store.model.ModelStoreBuilder; -import tools.refinery.store.query.dnf.AnyQuery; -import tools.refinery.store.query.dnf.Query; -import tools.refinery.store.query.dnf.RelationalQuery; -import tools.refinery.store.query.term.Variable; -import tools.refinery.store.reasoning.ReasoningBuilder; -import tools.refinery.store.reasoning.literal.CountCandidateLowerBoundLiteral; -import tools.refinery.store.reasoning.representation.PartialRelation; - -import java.util.Collection; -import java.util.List; - -import static tools.refinery.store.query.literal.Literals.check; -import static tools.refinery.store.query.term.int_.IntTerms.*; -import static tools.refinery.store.reasoning.literal.PartialLiterals.may; -import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW; - -class LowerTypeScopePropagator extends TypeScopePropagator { - private final int lowerBound; - - private LowerTypeScopePropagator(ScopePropagatorAdapterImpl adapter, int lowerBound, RelationalQuery allQuery, - RelationalQuery multiQuery) { - super(adapter, allQuery, multiQuery); - this.lowerBound = lowerBound; - } - - @Override - public void updateBounds() { - constraint.setLb((lowerBound - getSingleCount())); - } - - public static class Factory extends TypeScopePropagator.Factory { - private final PartialRelation type; - private final int lowerBound; - private final RelationalQuery allMay; - private final RelationalQuery multiMay; - - public Factory(PartialRelation type, int lowerBound) { - this.type = type; - this.lowerBound = lowerBound; - allMay = Query.of(type.name() + "#may", (builder, instance) -> builder.clause( - may(type.call(instance)) - )); - multiMay = Query.of(type.name() + "#multiMay", (builder, instance) -> builder.clause( - may(type.call(instance)), - MULTI_VIEW.call(instance) - )); - } - - @Override - public TypeScopePropagator createPropagator(ScopePropagatorAdapterImpl adapter) { - return new LowerTypeScopePropagator(adapter, lowerBound, allMay, multiMay); - } - - @Override - protected Collection getQueries() { - return List.of(allMay, multiMay); - } - - @Override - public void configure(ModelStoreBuilder storeBuilder) { - super.configure(storeBuilder); - - var requiredObjects = Query.of(type.name() + "#required", Integer.class, (builder, output) -> builder - .clause(Integer.class, currentCount -> List.of( - new CountCandidateLowerBoundLiteral(currentCount, type, List.of(Variable.of())), - output.assign(sub(currentCount, constant(lowerBound))), - check(greater(currentCount, constant(0))) - ))); - - storeBuilder.getAdapter(ReasoningBuilder.class).objective(Objectives.value(requiredObjects)); - storeBuilder.tryGetAdapter(DesignSpaceExplorationBuilder.class).ifPresent(dseBuilder -> - dseBuilder.accept(Criteria.whenNoMatch(requiredObjects))); - } - } -} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/RoundingUtil.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/RoundingUtil.java deleted file mode 100644 index a6d663ea..00000000 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/RoundingUtil.java +++ /dev/null @@ -1,26 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.scope.internal; - -final class RoundingUtil { - private static final double TOLERANCE = 0.01; - - private RoundingUtil() { - throw new IllegalStateException("This is a static utility class and should not be instantiated directly"); - } - - public static int roundUp(double value) { - double ceil = Math.ceil(value - TOLERANCE); - int intCeil = (int) ceil; - return Math.max(intCeil, 0); - } - - public static int roundDown(double value) { - double floor = Math.floor(value + TOLERANCE); - int intFloor = (int) floor; - return Math.max(intFloor, 0); - } -} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorAdapterImpl.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorAdapterImpl.java deleted file mode 100644 index 99c501ce..00000000 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorAdapterImpl.java +++ /dev/null @@ -1,253 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.scope.internal; - -import com.google.ortools.linearsolver.MPConstraint; -import com.google.ortools.linearsolver.MPObjective; -import com.google.ortools.linearsolver.MPSolver; -import com.google.ortools.linearsolver.MPVariable; -import org.eclipse.collections.api.factory.primitive.IntObjectMaps; -import org.eclipse.collections.api.factory.primitive.IntSets; -import org.eclipse.collections.api.map.primitive.MutableIntObjectMap; -import org.eclipse.collections.api.set.primitive.MutableIntSet; -import tools.refinery.store.model.Interpretation; -import tools.refinery.store.model.Model; -import tools.refinery.store.query.ModelQueryAdapter; -import tools.refinery.store.reasoning.refinement.RefinementResult; -import tools.refinery.store.reasoning.scope.ScopePropagatorAdapter; -import tools.refinery.store.reasoning.scope.ScopePropagatorStoreAdapter; -import tools.refinery.store.representation.cardinality.*; -import tools.refinery.store.tuple.Tuple; - -class ScopePropagatorAdapterImpl implements ScopePropagatorAdapter { - private final Model model; - private final ScopePropagatorStoreAdapterImpl storeAdapter; - private final ModelQueryAdapter queryEngine; - private final Interpretation countInterpretation; - private final MPSolver solver; - private final MPObjective objective; - private final MutableIntObjectMap variables = IntObjectMaps.mutable.empty(); - private final MutableIntSet activeVariables = IntSets.mutable.empty(); - private final TypeScopePropagator[] propagators; - private boolean changed = true; - - public ScopePropagatorAdapterImpl(Model model, ScopePropagatorStoreAdapterImpl storeAdapter) { - this.model = model; - this.storeAdapter = storeAdapter; - queryEngine = model.getAdapter(ModelQueryAdapter.class); - countInterpretation = model.getInterpretation(storeAdapter.getCountSymbol()); - solver = MPSolver.createSolver("GLOP"); - objective = solver.objective(); - initializeVariables(); - countInterpretation.addListener(this::countChanged, true); - var propagatorFactories = storeAdapter.getPropagatorFactories(); - propagators = new TypeScopePropagator[propagatorFactories.size()]; - for (int i = 0; i < propagators.length; i++) { - propagators[i] = propagatorFactories.get(i).createPropagator(this); - } - } - - @Override - public Model getModel() { - return model; - } - - @Override - public ScopePropagatorStoreAdapter getStoreAdapter() { - return storeAdapter; - } - - private void initializeVariables() { - var cursor = countInterpretation.getAll(); - while (cursor.move()) { - var interval = cursor.getValue(); - if (!interval.equals(CardinalityIntervals.ONE)) { - int nodeId = cursor.getKey().get(0); - createVariable(nodeId, interval); - activeVariables.add(nodeId); - } - } - } - - private MPVariable createVariable(int nodeId, CardinalityInterval interval) { - double lowerBound = interval.lowerBound(); - double upperBound = getUpperBound(interval); - var variable = solver.makeNumVar(lowerBound, upperBound, "x" + nodeId); - variables.put(nodeId, variable); - return variable; - } - - private void countChanged(Tuple key, CardinalityInterval fromValue, CardinalityInterval toValue, - boolean ignoredRestoring) { - int nodeId = key.get(0); - if ((toValue == null || toValue.equals(CardinalityIntervals.ONE))) { - if (fromValue != null && !fromValue.equals(CardinalityIntervals.ONE)) { - removeActiveVariable(toValue, nodeId); - } - return; - } - if (fromValue == null || fromValue.equals(CardinalityIntervals.ONE)) { - activeVariables.add(nodeId); - } - var variable = variables.get(nodeId); - if (variable == null) { - createVariable(nodeId, toValue); - markAsChanged(); - return; - } - double lowerBound = toValue.lowerBound(); - double upperBound = getUpperBound(toValue); - if (variable.lb() != lowerBound) { - variable.setLb(lowerBound); - markAsChanged(); - } - if (variable.ub() != upperBound) { - variable.setUb(upperBound); - markAsChanged(); - } - } - - private void removeActiveVariable(CardinalityInterval toValue, int nodeId) { - var variable = variables.get(nodeId); - if (variable == null || !activeVariables.remove(nodeId)) { - throw new AssertionError("Variable not active: " + nodeId); - } - if (toValue == null) { - variable.setBounds(0, 0); - } else { - // Until queries are flushed and the constraints can be properly updated, - // the variable corresponding to the (previous) multi-object has to stand in for a single object. - variable.setBounds(1, 1); - } - markAsChanged(); - } - - MPConstraint makeConstraint() { - return solver.makeConstraint(); - } - - MPVariable getVariable(int nodeId) { - var variable = variables.get(nodeId); - if (variable != null) { - return variable; - } - var interval = countInterpretation.get(Tuple.of(nodeId)); - if (interval == null || interval.equals(CardinalityIntervals.ONE)) { - interval = CardinalityIntervals.NONE; - } else { - activeVariables.add(nodeId); - markAsChanged(); - } - return createVariable(nodeId, interval); - } - - void markAsChanged() { - changed = true; - } - - @Override - public RefinementResult propagate() { - var result = RefinementResult.UNCHANGED; - RefinementResult currentRoundResult; - do { - currentRoundResult = propagateOne(); - result = result.andThen(currentRoundResult); - if (result.isRejected()) { - return result; - } - } while (currentRoundResult != RefinementResult.UNCHANGED); - return result; - } - - private RefinementResult propagateOne() { - queryEngine.flushChanges(); - if (!changed) { - return RefinementResult.UNCHANGED; - } - changed = false; - for (var propagator : propagators) { - propagator.updateBounds(); - } - var result = RefinementResult.UNCHANGED; - if (activeVariables.isEmpty()) { - return checkEmptiness(); - } - var iterator = activeVariables.intIterator(); - while (iterator.hasNext()) { - int nodeId = iterator.next(); - var variable = variables.get(nodeId); - if (variable == null) { - throw new AssertionError("Missing active variable: " + nodeId); - } - result = result.andThen(propagateNode(nodeId, variable)); - if (result.isRejected()) { - return result; - } - } - return result; - } - - private RefinementResult checkEmptiness() { - var emptinessCheckingResult = solver.solve(); - return switch (emptinessCheckingResult) { - case OPTIMAL, UNBOUNDED -> RefinementResult.UNCHANGED; - case INFEASIBLE -> RefinementResult.REJECTED; - default -> throw new IllegalStateException("Failed to check for consistency: " + emptinessCheckingResult); - }; - } - - private RefinementResult propagateNode(int nodeId, MPVariable variable) { - objective.setCoefficient(variable, 1); - try { - objective.setMinimization(); - var minimizationResult = solver.solve(); - int lowerBound; - switch (minimizationResult) { - case OPTIMAL -> lowerBound = RoundingUtil.roundUp(objective.value()); - case UNBOUNDED -> lowerBound = 0; - case INFEASIBLE -> { - return RefinementResult.REJECTED; - } - default -> throw new IllegalStateException("Failed to solve for minimum of %s: %s" - .formatted(variable, minimizationResult)); - } - - objective.setMaximization(); - var maximizationResult = solver.solve(); - UpperCardinality upperBound; - switch (maximizationResult) { - case OPTIMAL -> upperBound = UpperCardinalities.atMost(RoundingUtil.roundDown(objective.value())); - // Problem was feasible when minimizing, the only possible source of {@code UNBOUNDED_OR_INFEASIBLE} is - // an unbounded maximization problem. See https://github.com/google/or-tools/issues/3319 - case UNBOUNDED, INFEASIBLE -> upperBound = UpperCardinalities.UNBOUNDED; - default -> throw new IllegalStateException("Failed to solve for maximum of %s: %s" - .formatted(variable, minimizationResult)); - } - - var newInterval = CardinalityIntervals.between(lowerBound, upperBound); - var oldInterval = countInterpretation.put(Tuple.of(nodeId), newInterval); - if (newInterval.lowerBound() < oldInterval.lowerBound() || - newInterval.upperBound().compareTo(oldInterval.upperBound()) > 0) { - throw new IllegalArgumentException("Failed to refine multiplicity %s of node %d to %s" - .formatted(oldInterval, nodeId, newInterval)); - } - return newInterval.equals(oldInterval) ? RefinementResult.UNCHANGED : RefinementResult.REFINED; - } finally { - objective.setCoefficient(variable, 0); - } - } - - private static double getUpperBound(CardinalityInterval interval) { - var upperBound = interval.upperBound(); - if (upperBound instanceof FiniteUpperCardinality finiteUpperCardinality) { - return finiteUpperCardinality.finiteUpperBound(); - } else if (upperBound instanceof UnboundedUpperCardinality) { - return Double.POSITIVE_INFINITY; - } else { - throw new IllegalArgumentException("Unknown upper bound: " + upperBound); - } - } -} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorBuilderImpl.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorBuilderImpl.java deleted file mode 100644 index 531a7440..00000000 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorBuilderImpl.java +++ /dev/null @@ -1,86 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.scope.internal; - -import com.google.ortools.Loader; -import tools.refinery.store.adapter.AbstractModelAdapterBuilder; -import tools.refinery.store.model.ModelStore; -import tools.refinery.store.model.ModelStoreBuilder; -import tools.refinery.store.reasoning.representation.PartialRelation; -import tools.refinery.store.reasoning.scope.ScopePropagatorBuilder; -import tools.refinery.store.reasoning.scope.ScopePropagatorStoreAdapter; -import tools.refinery.store.reasoning.translator.TranslationException; -import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator; -import tools.refinery.store.representation.Symbol; -import tools.refinery.store.representation.cardinality.CardinalityInterval; -import tools.refinery.store.representation.cardinality.FiniteUpperCardinality; - -import java.util.*; - -public class ScopePropagatorBuilderImpl extends AbstractModelAdapterBuilder - implements ScopePropagatorBuilder { - private Symbol countSymbol = MultiObjectTranslator.COUNT_STORAGE; - private final Map scopes = new LinkedHashMap<>(); - private List typeScopePropagatorFactories; - - @Override - public ScopePropagatorBuilder countSymbol(Symbol countSymbol) { - if (countSymbol.arity() != 1) { - throw new IllegalArgumentException("Count symbol must have arty 1, got %s with arity %d instead" - .formatted(countSymbol, countSymbol.arity())); - } - if (!countSymbol.valueType().equals(CardinalityInterval.class)) { - throw new IllegalArgumentException("Count symbol must have CardinalityInterval values"); - } - if (countSymbol.defaultValue() != null) { - throw new IllegalArgumentException("Count symbol must default value null"); - } - this.countSymbol = countSymbol; - return this; - } - - @Override - public ScopePropagatorBuilder scope(PartialRelation type, CardinalityInterval interval) { - if (type.arity() != 1) { - throw new TranslationException(type, "Only types with arity 1 may have scopes, got %s with arity %d" - .formatted(type, type.arity())); - } - var newValue = scopes.compute(type, (ignoredKey, oldValue) -> - oldValue == null ? interval : oldValue.meet(interval)); - if (newValue.isEmpty()) { - throw new TranslationException(type, "Unsatisfiable scope for type %s".formatted(type)); - } - return this; - } - - @Override - protected void doConfigure(ModelStoreBuilder storeBuilder) { - typeScopePropagatorFactories = new ArrayList<>(scopes.size()); - for (var entry : scopes.entrySet()) { - var type = entry.getKey(); - var bounds = entry.getValue(); - if (bounds.lowerBound() > 0) { - var lowerFactory = new LowerTypeScopePropagator.Factory(type, bounds.lowerBound()); - typeScopePropagatorFactories.add(lowerFactory); - } - if (bounds.upperBound() instanceof FiniteUpperCardinality finiteUpperCardinality) { - var upperFactory = new UpperTypeScopePropagator.Factory(type, - finiteUpperCardinality.finiteUpperBound()); - typeScopePropagatorFactories.add(upperFactory); - } - } - for (var factory : typeScopePropagatorFactories) { - factory.configure(storeBuilder); - } - } - - @Override - protected ScopePropagatorStoreAdapter doBuild(ModelStore store) { - Loader.loadNativeLibraries(); - return new ScopePropagatorStoreAdapterImpl(store, countSymbol, Collections.unmodifiableMap(scopes), - Collections.unmodifiableList(typeScopePropagatorFactories)); - } -} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorStoreAdapterImpl.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorStoreAdapterImpl.java deleted file mode 100644 index 282ffe6f..00000000 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/ScopePropagatorStoreAdapterImpl.java +++ /dev/null @@ -1,58 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.scope.internal; - -import tools.refinery.store.adapter.ModelAdapter; -import tools.refinery.store.model.Model; -import tools.refinery.store.model.ModelStore; -import tools.refinery.store.reasoning.representation.PartialRelation; -import tools.refinery.store.reasoning.scope.ScopePropagatorStoreAdapter; -import tools.refinery.store.representation.Symbol; -import tools.refinery.store.representation.cardinality.CardinalityInterval; - -import java.util.List; -import java.util.Map; - -// Not a record, because we want to control getter visibility. -@SuppressWarnings("ClassCanBeRecord") -class ScopePropagatorStoreAdapterImpl implements ScopePropagatorStoreAdapter { - private final ModelStore store; - private final Symbol countSymbol; - private final Map scopes; - private final List propagatorFactories; - - public ScopePropagatorStoreAdapterImpl( - ModelStore store, Symbol countSymbol, - Map scopes, List propagatorFactories) { - this.store = store; - this.countSymbol = countSymbol; - this.scopes = scopes; - this.propagatorFactories = propagatorFactories; - } - - @Override - public ModelStore getStore() { - return store; - } - - Symbol getCountSymbol() { - return countSymbol; - } - - @Override - public Map getScopes() { - return scopes; - } - - public List getPropagatorFactories() { - return propagatorFactories; - } - - @Override - public ModelAdapter createModelAdapter(Model model) { - return new ScopePropagatorAdapterImpl(model, this); - } -} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/TypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/TypeScopePropagator.java deleted file mode 100644 index cfb95829..00000000 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/TypeScopePropagator.java +++ /dev/null @@ -1,67 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.scope.internal; - -import com.google.ortools.linearsolver.MPConstraint; -import tools.refinery.store.model.ModelStoreBuilder; -import tools.refinery.store.query.ModelQueryAdapter; -import tools.refinery.store.query.ModelQueryBuilder; -import tools.refinery.store.query.dnf.AnyQuery; -import tools.refinery.store.query.dnf.RelationalQuery; -import tools.refinery.store.query.resultset.ResultSet; -import tools.refinery.store.tuple.Tuple; - -import java.util.Collection; - -abstract class TypeScopePropagator { - private final ScopePropagatorAdapterImpl adapter; - private final ResultSet allNodes; - private final ResultSet multiNodes; - protected final MPConstraint constraint; - - protected TypeScopePropagator(ScopePropagatorAdapterImpl adapter, RelationalQuery allQuery, - RelationalQuery multiQuery) { - this.adapter = adapter; - var queryEngine = adapter.getModel().getAdapter(ModelQueryAdapter.class); - allNodes = queryEngine.getResultSet(allQuery); - multiNodes = queryEngine.getResultSet(multiQuery); - constraint = adapter.makeConstraint(); - constraint.setBounds(0, Double.POSITIVE_INFINITY); - var cursor = multiNodes.getAll(); - while (cursor.move()) { - var variable = adapter.getVariable(cursor.getKey().get(0)); - constraint.setCoefficient(variable, 1); - } - allNodes.addListener(this::allChanged); - multiNodes.addListener(this::multiChanged); - } - - public abstract void updateBounds(); - - protected int getSingleCount() { - return allNodes.size() - multiNodes.size(); - } - - private void allChanged(Tuple ignoredKey, Boolean ignoredOldValue, Boolean ignoredNewValue) { - adapter.markAsChanged(); - } - - private void multiChanged(Tuple key, Boolean ignoredOldValue, Boolean newValue) { - var variable = adapter.getVariable(key.get(0)); - constraint.setCoefficient(variable, Boolean.TRUE.equals(newValue) ? 1 : 0); - adapter.markAsChanged(); - } - - public abstract static class Factory { - public abstract TypeScopePropagator createPropagator(ScopePropagatorAdapterImpl adapter); - - protected abstract Collection getQueries(); - - public void configure(ModelStoreBuilder storeBuilder) { - storeBuilder.getAdapter(ModelQueryBuilder.class).queries(getQueries()); - } - } -} diff --git a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/UpperTypeScopePropagator.java b/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/UpperTypeScopePropagator.java deleted file mode 100644 index a0be0fb4..00000000 --- a/subprojects/store-reasoning-scope/src/main/java/tools/refinery/store/reasoning/scope/internal/UpperTypeScopePropagator.java +++ /dev/null @@ -1,59 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.scope.internal; - -import tools.refinery.store.query.dnf.AnyQuery; -import tools.refinery.store.query.dnf.Query; -import tools.refinery.store.query.dnf.RelationalQuery; -import tools.refinery.store.reasoning.representation.PartialRelation; - -import java.util.Collection; -import java.util.List; - -import static tools.refinery.store.reasoning.literal.PartialLiterals.must; -import static tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator.MULTI_VIEW; - -class UpperTypeScopePropagator extends TypeScopePropagator { - private final int upperBound; - - private UpperTypeScopePropagator(ScopePropagatorAdapterImpl adapter, int upperBound, RelationalQuery allQuery, - RelationalQuery multiQuery) { - super(adapter, allQuery, multiQuery); - this.upperBound = upperBound; - } - - @Override - public void updateBounds() { - constraint.setUb(upperBound - getSingleCount()); - } - - public static class Factory extends TypeScopePropagator.Factory { - private final int upperBound; - private final RelationalQuery allMust; - private final RelationalQuery multiMust; - - public Factory(PartialRelation type, int upperBound) { - this.upperBound = upperBound; - allMust = Query.of(type.name() + "#must", (builder, instance) -> builder.clause( - must(type.call(instance)) - )); - multiMust = Query.of(type.name() + "#multiMust", (builder, instance) -> builder.clause( - must(type.call(instance)), - MULTI_VIEW.call(instance) - )); - } - - @Override - public TypeScopePropagator createPropagator(ScopePropagatorAdapterImpl adapter) { - return new UpperTypeScopePropagator(adapter, upperBound, allMust, multiMust); - } - - @Override - protected Collection getQueries() { - return List.of(allMust, multiMust); - } - } -} diff --git a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MultiObjectTest.java b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MultiObjectTest.java index 42ce2f56..5fc70ae1 100644 --- a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MultiObjectTest.java +++ b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/MultiObjectTest.java @@ -7,13 +7,14 @@ package tools.refinery.store.reasoning.scope; import org.junit.jupiter.api.BeforeEach; import org.junit.jupiter.api.Test; +import tools.refinery.store.dse.propagation.PropagationAdapter; +import tools.refinery.store.dse.propagation.PropagationResult; import tools.refinery.store.model.Interpretation; import tools.refinery.store.model.Model; import tools.refinery.store.model.ModelStore; import tools.refinery.store.query.viatra.ViatraModelQueryAdapter; import tools.refinery.store.reasoning.ReasoningAdapter; import tools.refinery.store.reasoning.ReasoningStoreAdapter; -import tools.refinery.store.reasoning.refinement.RefinementResult; import tools.refinery.store.reasoning.representation.PartialRelation; import tools.refinery.store.reasoning.seed.ModelSeed; import tools.refinery.store.reasoning.translator.PartialRelationTranslator; @@ -38,11 +39,12 @@ class MultiObjectTest { void beforeEach() { store = ModelStore.builder() .with(ViatraModelQueryAdapter.builder()) + .with(PropagationAdapter.builder()) .with(ReasoningAdapter.builder()) .with(new MultiObjectTranslator()) .with(PartialRelationTranslator.of(person) .symbol(Symbol.of("Person", 1, TruthValue.class, TruthValue.FALSE))) - .with(ScopePropagatorAdapter.builder() + .with(new ScopePropagator() .scope(person, CardinalityIntervals.between(5, 15))) .build(); model = null; @@ -57,7 +59,7 @@ class MultiObjectTest { .put(Tuple.of(0), CardinalityIntervals.SET)) .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) .build()); - assertThat(propagate(), is(RefinementResult.REFINED)); + assertThat(propagate(), is(PropagationResult.PROPAGATED)); assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.between(2, 12))); } @@ -69,7 +71,7 @@ class MultiObjectTest { .put(Tuple.of(0), CardinalityIntervals.between(5, 20))) .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) .build()); - assertThat(propagate(), is(RefinementResult.REFINED)); + assertThat(propagate(), is(PropagationResult.PROPAGATED)); assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.between(5, 12))); } @@ -81,7 +83,7 @@ class MultiObjectTest { .put(Tuple.of(0), CardinalityIntervals.SET)) .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) .build()); - assertThat(propagate(), is(RefinementResult.REJECTED)); + assertThat(propagate(), is(PropagationResult.REJECTED)); } @Test @@ -90,7 +92,7 @@ class MultiObjectTest { .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder.reducedValue(CardinalityIntervals.ONE)) .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) .build()); - assertThat(propagate(), is(RefinementResult.UNCHANGED)); + assertThat(propagate(), is(PropagationResult.UNCHANGED)); } @Test @@ -99,7 +101,7 @@ class MultiObjectTest { .seed(MultiObjectTranslator.COUNT_SYMBOL, builder -> builder.reducedValue(CardinalityIntervals.ONE)) .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) .build()); - assertThat(propagate(), is(RefinementResult.REJECTED)); + assertThat(propagate(), is(PropagationResult.REJECTED)); } @Test @@ -110,7 +112,7 @@ class MultiObjectTest { .put(Tuple.of(0), CardinalityIntervals.atLeast(20))) .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) .build()); - assertThat(propagate(), is(RefinementResult.REJECTED)); + assertThat(propagate(), is(PropagationResult.REJECTED)); } @Test @@ -121,7 +123,7 @@ class MultiObjectTest { .put(Tuple.of(0), CardinalityIntervals.atMost(1))) .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) .build()); - assertThat(propagate(), is(RefinementResult.REJECTED)); + assertThat(propagate(), is(PropagationResult.REJECTED)); } @Test @@ -133,7 +135,7 @@ class MultiObjectTest { .put(Tuple.of(1), CardinalityIntervals.SET)) .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) .build()); - assertThat(propagate(), is(RefinementResult.REFINED)); + assertThat(propagate(), is(PropagationResult.PROPAGATED)); assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.atMost(12))); assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.atMost(12))); } @@ -147,7 +149,7 @@ class MultiObjectTest { .put(Tuple.of(1), CardinalityIntervals.atMost(11))) .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) .build()); - assertThat(propagate(), is(RefinementResult.REFINED)); + assertThat(propagate(), is(PropagationResult.PROPAGATED)); assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.between(7, 12))); assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.atMost(5))); } @@ -161,7 +163,7 @@ class MultiObjectTest { .put(Tuple.of(1), CardinalityIntervals.exactly(11))) .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) .build()); - assertThat(propagate(), is(RefinementResult.REJECTED)); + assertThat(propagate(), is(PropagationResult.REJECTED)); } @Test @@ -173,7 +175,7 @@ class MultiObjectTest { .put(Tuple.of(1), CardinalityIntervals.atMost(2))) .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) .build()); - assertThat(propagate(), is(RefinementResult.REJECTED)); + assertThat(propagate(), is(PropagationResult.REJECTED)); } @Test @@ -185,14 +187,14 @@ class MultiObjectTest { .put(Tuple.of(1), CardinalityIntervals.SET)) .seed(person, builder -> builder.reducedValue(TruthValue.TRUE)) .build()); - assertThat(propagate(), is(RefinementResult.REFINED)); + assertThat(propagate(), is(PropagationResult.PROPAGATED)); assertThat(countStorage.get(Tuple.of(0)), is(CardinalityIntervals.LONE)); assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.between(1, 12))); countStorage.put(Tuple.of(0), CardinalityIntervals.ONE); - assertThat(propagate(), is(RefinementResult.REFINED)); + assertThat(propagate(), is(PropagationResult.PROPAGATED)); assertThat(countStorage.get(Tuple.of(1)), is(CardinalityIntervals.between(1, 11))); countStorage.put(Tuple.of(1), CardinalityIntervals.ONE); - assertThat(propagate(), is(RefinementResult.UNCHANGED)); + assertThat(propagate(), is(PropagationResult.UNCHANGED)); } private void createModel(ModelSeed modelSeed) { @@ -200,7 +202,7 @@ class MultiObjectTest { countStorage = model.getInterpretation(MultiObjectTranslator.COUNT_STORAGE); } - private RefinementResult propagate() { - return model.getAdapter(ScopePropagatorAdapter.class).propagate(); + private PropagationResult propagate() { + return model.getAdapter(PropagationAdapter.class).propagate(); } } diff --git a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/RoundingUtilTest.java b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/RoundingUtilTest.java new file mode 100644 index 00000000..e697298e --- /dev/null +++ b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/RoundingUtilTest.java @@ -0,0 +1,69 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.scope; + +import org.junit.jupiter.params.ParameterizedTest; +import org.junit.jupiter.params.provider.Arguments; +import org.junit.jupiter.params.provider.MethodSource; + +import java.util.stream.Stream; + +import static org.hamcrest.MatcherAssert.assertThat; +import static org.hamcrest.Matchers.is; + +class RoundingUtilTest { + @ParameterizedTest + @MethodSource + void roundUpTest(double value, int expected) { + int actual = RoundingUtil.roundUp(value); + assertThat(actual, is(expected)); + } + + static Stream roundUpTest() { + return Stream.of( + Arguments.of(0.0, 0), + Arguments.of(-0.0, 0), + Arguments.of(-0.9, 0), + Arguments.of(-2, 0), + Arguments.of(0.009, 0), + Arguments.of(0.011, 1), + Arguments.of(0.1, 1), + Arguments.of(0.991, 1), + Arguments.of(1, 1), + Arguments.of(1.009, 1), + Arguments.of(1.011, 2), + Arguments.of(1.5, 2), + Arguments.of(2, 2), + Arguments.of(100.5, 101) + ); + } + + @ParameterizedTest + @MethodSource + void roundDownTest(double value, int expected) { + int actual = RoundingUtil.roundDown(value); + assertThat(actual, is(expected)); + } + + static Stream roundDownTest() { + return Stream.of( + Arguments.of(0.0, 0), + Arguments.of(-0.0, 0), + Arguments.of(-0.9, 0), + Arguments.of(-2, 0), + Arguments.of(0.989, 0), + Arguments.of(0.991, 1), + Arguments.of(1, 1), + Arguments.of(1.5, 1), + Arguments.of(1.009, 1), + Arguments.of(1.989, 1), + Arguments.of(1.991, 2), + Arguments.of(2, 2), + Arguments.of(2.009, 2), + Arguments.of(100.5, 100) + ); + } +} diff --git a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/internal/RoundingUtilTest.java b/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/internal/RoundingUtilTest.java deleted file mode 100644 index 9daed660..00000000 --- a/subprojects/store-reasoning-scope/src/test/java/tools/refinery/store/reasoning/scope/internal/RoundingUtilTest.java +++ /dev/null @@ -1,69 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.scope.internal; - -import org.junit.jupiter.params.ParameterizedTest; -import org.junit.jupiter.params.provider.Arguments; -import org.junit.jupiter.params.provider.MethodSource; - -import java.util.stream.Stream; - -import static org.hamcrest.MatcherAssert.assertThat; -import static org.hamcrest.Matchers.is; - -class RoundingUtilTest { - @ParameterizedTest - @MethodSource - void roundUpTest(double value, int expected) { - int actual = RoundingUtil.roundUp(value); - assertThat(actual, is(expected)); - } - - static Stream roundUpTest() { - return Stream.of( - Arguments.of(0.0, 0), - Arguments.of(-0.0, 0), - Arguments.of(-0.9, 0), - Arguments.of(-2, 0), - Arguments.of(0.009, 0), - Arguments.of(0.011, 1), - Arguments.of(0.1, 1), - Arguments.of(0.991, 1), - Arguments.of(1, 1), - Arguments.of(1.009, 1), - Arguments.of(1.011, 2), - Arguments.of(1.5, 2), - Arguments.of(2, 2), - Arguments.of(100.5, 101) - ); - } - - @ParameterizedTest - @MethodSource - void roundDownTest(double value, int expected) { - int actual = RoundingUtil.roundDown(value); - assertThat(actual, is(expected)); - } - - static Stream roundDownTest() { - return Stream.of( - Arguments.of(0.0, 0), - Arguments.of(-0.0, 0), - Arguments.of(-0.9, 0), - Arguments.of(-2, 0), - Arguments.of(0.989, 0), - Arguments.of(0.991, 1), - Arguments.of(1, 1), - Arguments.of(1.5, 1), - Arguments.of(1.009, 1), - Arguments.of(1.989, 1), - Arguments.of(1.991, 2), - Arguments.of(2, 2), - Arguments.of(2.009, 2), - Arguments.of(100.5, 100) - ); - } -} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/CleanupActionLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/CleanupActionLiteral.java new file mode 100644 index 00000000..62c35cee --- /dev/null +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/CleanupActionLiteral.java @@ -0,0 +1,43 @@ +/* + * SPDX-FileCopyrightText: 2023 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.store.reasoning.actions; + +import tools.refinery.store.dse.transition.actions.AbstractActionLiteral; +import tools.refinery.store.dse.transition.actions.BoundActionLiteral; +import tools.refinery.store.model.Model; +import tools.refinery.store.query.term.NodeVariable; +import tools.refinery.store.reasoning.ReasoningAdapter; +import tools.refinery.store.tuple.Tuple; + +import java.util.List; + +public class CleanupActionLiteral extends AbstractActionLiteral { + private final NodeVariable node; + + public CleanupActionLiteral(NodeVariable node) { + this.node = node; + } + + public NodeVariable getNode() { + return node; + } + + @Override + public List getInputVariables() { + return List.of(node); + } + + @Override + public List getOutputVariables() { + return List.of(); + } + + @Override + public BoundActionLiteral bindToModel(Model model) { + var reasoningAdapter = model.getAdapter(ReasoningAdapter.class); + return tuple -> reasoningAdapter.cleanup(tuple.get(0)) ? Tuple.of() : null; + } +} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java index 990d11e5..f36fde44 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/actions/PartialActionLiterals.java @@ -35,4 +35,8 @@ public final class PartialActionLiterals { public static FocusActionLiteral focus(NodeVariable parent, NodeVariable child) { return new FocusActionLiteral(parent, child); } + + public static CleanupActionLiteral cleanup(NodeVariable node) { + return new CleanupActionLiteral(node); + } } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java index d2cd2eb0..722458c8 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java @@ -18,18 +18,19 @@ import tools.refinery.store.query.dnf.Query; import tools.refinery.store.query.dnf.RelationalQuery; import tools.refinery.store.reasoning.ReasoningBuilder; import tools.refinery.store.reasoning.interpretation.PartialInterpretation; -import tools.refinery.store.reasoning.refinement.DefaultStorageRefiner; -import tools.refinery.store.reasoning.translator.AnyPartialSymbolTranslator; -import tools.refinery.store.reasoning.translator.PartialRelationTranslator; import tools.refinery.store.reasoning.lifting.DnfLifter; import tools.refinery.store.reasoning.literal.Concreteness; import tools.refinery.store.reasoning.literal.Modality; +import tools.refinery.store.reasoning.refinement.DefaultStorageRefiner; import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner; import tools.refinery.store.reasoning.refinement.PartialModelInitializer; import tools.refinery.store.reasoning.refinement.StorageRefiner; import tools.refinery.store.reasoning.representation.AnyPartialSymbol; +import tools.refinery.store.reasoning.translator.AnyPartialSymbolTranslator; +import tools.refinery.store.reasoning.translator.PartialRelationTranslator; import tools.refinery.store.representation.AnySymbol; import tools.refinery.store.representation.Symbol; +import tools.refinery.store.statecoding.StateCoderBuilder; import java.util.*; @@ -109,6 +110,8 @@ public class ReasoningBuilderImpl extends AbstractModelAdapterBuilder stateCoderBuilder.exclude(ReasoningAdapterImpl.NODE_COUNT_SYMBOL)); for (var translator : translators.values()) { translator.configure(storeBuilder); if (translator instanceof PartialRelationTranslator relationConfiguration) { diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java index 8eb5a034..9ef6fb16 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java @@ -5,6 +5,7 @@ */ package tools.refinery.store.reasoning.internal; +import tools.refinery.store.dse.propagation.PropagationAdapter; import tools.refinery.store.model.Model; import tools.refinery.store.model.ModelStore; import tools.refinery.store.query.ModelQueryAdapter; @@ -103,6 +104,11 @@ class ReasoningStoreAdapterImpl implements ReasoningStoreAdapter { for (var initializer : initializers) { initializer.initialize(model, modelSeed); } + model.tryGetAdapter(PropagationAdapter.class).ifPresent(propagationAdapter -> { + if (propagationAdapter.propagate().isRejected()) { + throw new IllegalArgumentException("Inconsistent initial mode: propagation failed"); + } + }); model.getAdapter(ModelQueryAdapter.class).flushChanges(); return model; } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementResult.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementResult.java deleted file mode 100644 index 1bc537d1..00000000 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementResult.java +++ /dev/null @@ -1,24 +0,0 @@ -/* - * SPDX-FileCopyrightText: 2023 The Refinery Authors - * - * SPDX-License-Identifier: EPL-2.0 - */ -package tools.refinery.store.reasoning.refinement; - -public enum RefinementResult { - UNCHANGED, - REFINED, - REJECTED; - - public RefinementResult andThen(RefinementResult next) { - return switch (this) { - case UNCHANGED -> next; - case REFINED -> next == REJECTED ? REJECTED : REFINED; - case REJECTED -> REJECTED; - }; - } - - public boolean isRejected() { - return this == REJECTED; - } -} diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java index 5c3298ac..61037be3 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java @@ -243,7 +243,7 @@ public class ContainmentHierarchyTranslator implements ModelStoreConfiguration { MultiObjectTranslator.MULTI_VIEW.call(multi), not(may(CONTAINED_SYMBOL.call(multi))) ) - .clause((container) -> List.of( + .clause(container -> List.of( MultiObjectTranslator.MULTI_VIEW.call(multi), must(CONTAINS_SYMBOL.call(container, multi)), not(MultiObjectTranslator.MULTI_VIEW.call(container)) diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java index 90802864..8df23d9a 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java @@ -8,18 +8,23 @@ package tools.refinery.store.reasoning.translator.containment; import tools.refinery.store.reasoning.representation.PartialRelation; import tools.refinery.store.representation.TruthValue; +import java.util.Objects; import java.util.Set; -record InferredContainment(TruthValue contains, Set mustLinks, - Set forbiddenLinks) { +final class InferredContainment { public static final InferredContainment UNKNOWN = new InferredContainment( TruthValue.UNKNOWN, Set.of(), Set.of()); + private final TruthValue contains; + private final Set mustLinks; + private final Set forbiddenLinks; + private final int hashCode; public InferredContainment(TruthValue contains, Set mustLinks, Set forbiddenLinks) { this.contains = adjustContains(contains, mustLinks, forbiddenLinks); this.mustLinks = mustLinks; this.forbiddenLinks = forbiddenLinks; + hashCode = Objects.hash(contains, mustLinks, forbiddenLinks); } private static TruthValue adjustContains(TruthValue contains, Set mustLinks, @@ -34,4 +39,39 @@ record InferredContainment(TruthValue contains, Set mustLinks, } return result; } + + public TruthValue contains() { + return contains; + } + + public Set mustLinks() { + return mustLinks; + } + + public Set forbiddenLinks() { + return forbiddenLinks; + } + + @Override + public boolean equals(Object obj) { + if (obj == this) return true; + if (obj == null || obj.getClass() != this.getClass()) return false; + var that = (InferredContainment) obj; + return Objects.equals(this.contains, that.contains) && + Objects.equals(this.mustLinks, that.mustLinks) && + Objects.equals(this.forbiddenLinks, that.forbiddenLinks); + } + + @Override + public int hashCode() { + return hashCode; + } + + @Override + public String toString() { + return "InferredContainment[" + + "contains=" + contains + ", " + + "mustLinks=" + mustLinks + ", " + + "forbiddenLinks=" + forbiddenLinks + ']'; + } } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java index 05704096..bad96a66 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java @@ -5,17 +5,21 @@ */ package tools.refinery.store.reasoning.translator.multiobject; +import tools.refinery.store.dse.propagation.PropagationBuilder; +import tools.refinery.store.dse.transition.Rule; import tools.refinery.store.dse.transition.objectives.Criteria; import tools.refinery.store.dse.transition.objectives.Objectives; import tools.refinery.store.model.ModelStoreBuilder; import tools.refinery.store.model.ModelStoreConfiguration; import tools.refinery.store.query.dnf.Query; +import tools.refinery.store.query.literal.Literals; import tools.refinery.store.query.term.Variable; import tools.refinery.store.query.term.int_.IntTerms; import tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms; import tools.refinery.store.query.view.AnySymbolView; import tools.refinery.store.reasoning.ReasoningAdapter; import tools.refinery.store.reasoning.ReasoningBuilder; +import tools.refinery.store.reasoning.actions.PartialActionLiterals; import tools.refinery.store.reasoning.representation.PartialFunction; import tools.refinery.store.reasoning.translator.PartialRelationTranslator; import tools.refinery.store.reasoning.translator.RoundingMode; @@ -66,6 +70,11 @@ public class MultiObjectTranslator implements ModelStoreConfiguration { LOWER_CARDINALITY_VIEW.call(p1, lower), check(greaterEq(lower, constant(1))) )))) + .candidate(Query.of("exists#candidate", (builder, p1) -> builder + .clause( + LOWER_CARDINALITY_VIEW.call(p1, Variable.of(Integer.class)), + Literals.not(MULTI_VIEW.call(p1)) + ))) .roundingMode(RoundingMode.PREFER_FALSE) .refiner(ExistsRefiner.of(COUNT_STORAGE)) .exclude(null) @@ -82,5 +91,17 @@ public class MultiObjectTranslator implements ModelStoreConfiguration { var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class); reasoningBuilder.initializer(new MultiObjectInitializer(COUNT_STORAGE)); reasoningBuilder.storageRefiner(COUNT_STORAGE, MultiObjectStorageRefiner::new); + + storeBuilder.tryGetAdapter(PropagationBuilder.class) + .ifPresent(propagationBuilder -> propagationBuilder.rule( + Rule.of("exists#cleanup", (builder, node) -> builder + .clause(UpperCardinality.class, upper -> List.of( + UPPER_CARDINALITY_VIEW.call(node, upper), + check(UpperCardinalityTerms.less(upper, + UpperCardinalityTerms.constant(UpperCardinalities.ONE))) + )) + .action( + PartialActionLiterals.cleanup(node) + )))); } } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java index 1ae94ae1..9a0c2b0f 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java @@ -8,17 +8,22 @@ package tools.refinery.store.reasoning.translator.typehierarchy; import tools.refinery.store.reasoning.representation.PartialRelation; import java.util.Collections; +import java.util.Objects; import java.util.Set; -record InferredType(Set mustTypes, Set mayConcreteTypes, - PartialRelation candidateType) { +public final class InferredType { public static final InferredType UNTYPED = new InferredType(Set.of(), Set.of(), null); + private final Set mustTypes; + private final Set mayConcreteTypes; + private final PartialRelation candidateType; + private final int hashCode; public InferredType(Set mustTypes, Set mayConcreteTypes, PartialRelation candidateType) { this.mustTypes = Collections.unmodifiableSet(mustTypes); this.mayConcreteTypes = Collections.unmodifiableSet(mayConcreteTypes); this.candidateType = candidateType; + hashCode = Objects.hash(mustTypes, mayConcreteTypes, candidateType); } public boolean isConsistent() { @@ -32,4 +37,40 @@ record InferredType(Set mustTypes, Set mayConc public boolean isMayConcrete(PartialRelation partialRelation) { return mayConcreteTypes.contains(partialRelation); } + + + public Set mustTypes() { + return mustTypes; + } + + public Set mayConcreteTypes() { + return mayConcreteTypes; + } + + public PartialRelation candidateType() { + return candidateType; + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + InferredType that = (InferredType) o; + return Objects.equals(mustTypes, that.mustTypes) && + Objects.equals(mayConcreteTypes, that.mayConcreteTypes) && + Objects.equals(candidateType, that.candidateType); + } + + @Override + public int hashCode() { + return hashCode; + } + + @Override + public String toString() { + return "InferredType[" + + "mustTypes=" + mustTypes + ", " + + "mayConcreteTypes=" + mayConcreteTypes + ", " + + "candidateType=" + candidateType + ']'; + } } diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java index dc8a1d36..37ea1448 100644 --- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java +++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java @@ -26,7 +26,8 @@ import static tools.refinery.store.reasoning.literal.PartialLiterals.candidateMu import static tools.refinery.store.reasoning.literal.PartialLiterals.may; public class TypeHierarchyTranslator implements ModelStoreConfiguration { - private final Symbol typeSymbol = Symbol.of("TYPE", 1, InferredType.class, InferredType.UNTYPED); + public static final Symbol TYPE_SYMBOL = Symbol.of("TYPE", 1, InferredType.class, + InferredType.UNTYPED); private final TypeHierarchy typeHierarchy; public TypeHierarchyTranslator(TypeHierarchy typeHierarchy) { @@ -39,7 +40,7 @@ public class TypeHierarchyTranslator implements ModelStoreConfiguration { return; } - storeBuilder.symbol(typeSymbol); + storeBuilder.symbol(TYPE_SYMBOL); for (var entry : typeHierarchy.getPreservedTypes().entrySet()) { storeBuilder.with(createPreservedTypeTranslator(entry.getKey(), entry.getValue())); @@ -50,13 +51,13 @@ public class TypeHierarchyTranslator implements ModelStoreConfiguration { } var reasoningBuilder = storeBuilder.getAdapter(ReasoningBuilder.class); - reasoningBuilder.initializer(new TypeHierarchyInitializer(typeHierarchy, typeSymbol)); + reasoningBuilder.initializer(new TypeHierarchyInitializer(typeHierarchy, TYPE_SYMBOL)); } private ModelStoreConfiguration createPreservedTypeTranslator(PartialRelation type, TypeAnalysisResult result) { var may = Query.of(type.name() + "#partial#may", (builder, p1) -> { if (!result.isAbstractType()) { - builder.clause(new MayTypeView(typeSymbol, type).call(p1)); + builder.clause(new MayTypeView(TYPE_SYMBOL, type).call(p1)); } for (var subtype : result.getDirectSubtypes()) { builder.clause(may(subtype.call(p1))); @@ -64,12 +65,12 @@ public class TypeHierarchyTranslator implements ModelStoreConfiguration { }); var must = Query.of(type.name() + "#partial#must", (builder, p1) -> builder.clause( - new MustTypeView(typeSymbol, type).call(p1) + new MustTypeView(TYPE_SYMBOL, type).call(p1) )); var candidate = Query.of(type.name() + "#candidate", (builder, p1) -> { if (!result.isAbstractType()) { - builder.clause(new CandidateTypeView(typeSymbol, type).call(p1)); + builder.clause(new CandidateTypeView(TYPE_SYMBOL, type).call(p1)); } for (var subtype : result.getDirectSubtypes()) { builder.clause(PartialLiterals.candidateMust(subtype.call(p1))); @@ -80,7 +81,7 @@ public class TypeHierarchyTranslator implements ModelStoreConfiguration { .may(may) .must(must) .candidate(candidate) - .refiner(InferredTypeRefiner.of(typeSymbol, result)); + .refiner(InferredTypeRefiner.of(TYPE_SYMBOL, result)); if (!result.isAbstractType()) { var decision = Rule.of(type.name(), (builder, instance) -> builder diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/FiniteUpperCardinality.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/FiniteUpperCardinality.java index 088e3925..b63a8637 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/FiniteUpperCardinality.java +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/FiniteUpperCardinality.java @@ -67,4 +67,17 @@ public record FiniteUpperCardinality(int finiteUpperBound) implements UpperCardi } throw new IllegalArgumentException("Unknown UpperCardinality: " + other); } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + FiniteUpperCardinality that = (FiniteUpperCardinality) o; + return finiteUpperBound == that.finiteUpperBound; + } + + @Override + public int hashCode() { + return finiteUpperBound; + } } diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/NonEmptyCardinalityInterval.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/NonEmptyCardinalityInterval.java index bfaeea25..6bd66df7 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/NonEmptyCardinalityInterval.java +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/NonEmptyCardinalityInterval.java @@ -5,6 +5,7 @@ */ package tools.refinery.store.representation.cardinality; +import java.util.Objects; import java.util.function.BinaryOperator; import java.util.function.IntBinaryOperator; @@ -89,4 +90,17 @@ public record NonEmptyCardinalityInterval(int lowerBound, UpperCardinality upper } return "[%d..%s]".formatted(lowerBound, upperBound); } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o == null || getClass() != o.getClass()) return false; + NonEmptyCardinalityInterval that = (NonEmptyCardinalityInterval) o; + return lowerBound == that.lowerBound && Objects.equals(upperBound, that.upperBound); + } + + @Override + public int hashCode() { + return lowerBound * 31 + upperBound.hashCode(); + } } diff --git a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UnboundedUpperCardinality.java b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UnboundedUpperCardinality.java index e3a334cd..03c701ae 100644 --- a/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UnboundedUpperCardinality.java +++ b/subprojects/store/src/main/java/tools/refinery/store/representation/cardinality/UnboundedUpperCardinality.java @@ -53,4 +53,14 @@ public final class UnboundedUpperCardinality implements UpperCardinality { public String toString() { return "*"; } + + @Override + public boolean equals(Object obj) { + return this == obj || (obj != null && getClass() == obj.getClass()); + } + + @Override + public int hashCode() { + return -1; + } } -- cgit v1.2.3-70-g09d2