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 --- .../language/semantics/model/ModelInitializer.java | 23 +- .../semantics/model/CountPropagationTest.java | 82 +++++++ .../semantics/model/ModelGenerationTest.java | 272 +++++++++++++++++++++ 3 files changed, 370 insertions(+), 7 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 (limited to 'subprojects/language-semantics/src') 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(); + } + } +} -- cgit v1.2.3-70-g09d2