From c1f185fd8fc2c3dfc123d9271726c588963c7c01 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Mon, 8 Apr 2019 00:58:00 +0200 Subject: Objective POC implementation --- .../viatrasolver/reasoner/ViatraReasoner.xtend | 33 ++++++- .../reasoner/ViatraReasonerConfiguration.xtend | 32 +++++-- .../viatrasolver/reasoner/dse/DseUtils.xtend | 1 + .../reasoner/dse/IThreeValuedObjective.xtend | 10 -- .../dse/ModelGenerationCompositeObjective.xtend | 1 + .../AbstractThreeValuedObjective.xtend | 102 +++++++++++++++++++++ .../optimization/IThreeValuedObjective.xtend | 10 ++ .../reasoner/optimization/ObjectiveKind.java | 36 ++++++++ .../optimization/ThreeValuedCostObjective.xtend | 86 +++++++++++++++++ 9 files changed, 293 insertions(+), 18 deletions(-) delete mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/IThreeValuedObjective.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/AbstractThreeValuedObjective.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IThreeValuedObjective.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ObjectiveKind.java create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend index 8831b0ff..6898550d 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasoner.xtend @@ -1,5 +1,7 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner +import com.google.common.collect.ImmutableList +import com.google.common.collect.Lists import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException @@ -25,6 +27,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.SurelyViolatedObject import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.UnfinishedMultiplicityObjective import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.ViatraReasonerSolutionSaver import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.WF2ObjectiveConverter +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostElement +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ThreeValuedCostObjective import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace import java.util.List import java.util.Map @@ -84,9 +88,36 @@ class ViatraReasoner extends LogicReasoner { wf2ObjectiveConverter.createCompletenessObjective(method.unfinishedWF) )) + val extermalObjectives = Lists.newArrayListWithExpectedSize(viatraConfig.costObjectives.size) + for (entry : viatraConfig.costObjectives.indexed) { + val objectiveName = '''costObjective«entry.key»''' + val objectiveConfig = entry.value + val elementsBuilder = ImmutableList.builder + for (elementConfig : objectiveConfig.elements) { + val relationName = elementConfig.patternQualifiedName + val modalQueries = method.modalRelationQueries.get(relationName) + if (modalQueries === null) { + throw new IllegalArgumentException("Unknown relation: " + relationName) + } + elementsBuilder.add(new ThreeValuedCostElement( + modalQueries.currentQuery, + modalQueries.mayQuery, + modalQueries.mustQuery, + elementConfig.weight + )) + } + val costElements = elementsBuilder.build + val costObjective = new ThreeValuedCostObjective(objectiveName, costElements, objectiveConfig.kind, + objectiveConfig.threshold, 3) + dse.addObjective(costObjective) + if (objectiveConfig.findExtremum) { + extermalObjectives += costObjective + } + } + val solutionStore = new SolutionStore(configuration.solutionScope.numberOfRequiredSolutions) solutionStore.registerSolutionFoundHandler(new LoggerSolutionFoundHandler(viatraConfig)) - val solutionSaver = new ViatraReasonerSolutionSaver(newArrayOfSize(0, 0)) + val solutionSaver = new ViatraReasonerSolutionSaver(newArrayList(extermalObjectives)) val solutionCopier = solutionSaver.solutionCopier solutionStore.withSolutionSaver(solutionSaver) dse.solutionStore = solutionStore diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend index 9ef23c59..e6aee20c 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/ViatraReasonerConfiguration.xtend @@ -7,18 +7,22 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethod import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeInferenceMethod import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualiser +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveKind +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold import java.util.LinkedList import java.util.List import java.util.Set import org.eclipse.xtext.xbase.lib.Functions.Function1 enum StateCoderStrategy { - Neighbourhood, NeighbourhoodWithEquivalence, IDBased, DefinedByDiversity + Neighbourhood, + NeighbourhoodWithEquivalence, + IDBased, + DefinedByDiversity } -class ViatraReasonerConfiguration extends LogicSolverConfiguration{ - //public var Iterable existingQueries - +class ViatraReasonerConfiguration extends LogicSolverConfiguration { + // public var Iterable existingQueries public var nameNewElements = false public var StateCoderStrategy stateCoderStrategy = StateCoderStrategy.Neighbourhood public var TypeInferenceMethod typeInferenceMethod = TypeInferenceMethod.PreliminaryAnalysis @@ -26,7 +30,7 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration{ * Once per 1/randomBacktrackChance the search selects a random state. */ public var int randomBacktrackChance = 20; - + /** * Describes the required diversity between the solutions. * Null means that the solutions have to have different state codes only. @@ -44,7 +48,9 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration{ /** * Configuration for cutting search space. */ - public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint + public var SearchSpaceConstraint searchSpaceConstraints = new SearchSpaceConstraint + + public var List costObjectives = newArrayList } class DiversityDescriptor { @@ -73,4 +79,16 @@ class SearchSpaceConstraint { public static val UNLIMITED_MAXDEPTH = Integer.MAX_VALUE public var int maxDepth = UNLIMITED_MAXDEPTH public var List> additionalGlobalConstraints = new LinkedList -} \ No newline at end of file +} + +class CostObjectiveConfiguration { + public var List elements = newArrayList + public var ObjectiveKind kind + public var ObjectiveThreshold threshold + public var boolean findExtremum +} + +class CostObjectiveElementConfiguration { + public var String patternQualifiedName + public var int weight +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DseUtils.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DseUtils.xtend index 3a897aa3..3c2e3319 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DseUtils.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/DseUtils.xtend @@ -1,5 +1,6 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.IThreeValuedObjective import org.eclipse.viatra.dse.base.ThreadContext import org.eclipse.viatra.dse.objectives.Comparators import org.eclipse.viatra.dse.objectives.Fitness diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/IThreeValuedObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/IThreeValuedObjective.xtend deleted file mode 100644 index 8c93d4ec..00000000 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/IThreeValuedObjective.xtend +++ /dev/null @@ -1,10 +0,0 @@ -package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse - -import org.eclipse.viatra.dse.base.ThreadContext -import org.eclipse.viatra.dse.objectives.IObjective - -interface IThreeValuedObjective extends IObjective { - def Double getWorstPossibleFitness(ThreadContext threadContext) - - def Double getBestPossibleFitness(ThreadContext threadContext) -} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend index af6d1bbd..9a33753c 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ModelGenerationCompositeObjective.xtend @@ -1,6 +1,7 @@ package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse import com.google.common.collect.ImmutableList +import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.IThreeValuedObjective import java.util.Comparator import java.util.List import org.eclipse.viatra.dse.base.ThreadContext diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/AbstractThreeValuedObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/AbstractThreeValuedObjective.xtend new file mode 100644 index 00000000..241bef2a --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/AbstractThreeValuedObjective.xtend @@ -0,0 +1,102 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization + +import java.util.Comparator +import org.eclipse.viatra.dse.base.ThreadContext +import org.eclipse.xtend.lib.annotations.Accessors +import org.eclipse.xtend.lib.annotations.Data + +abstract class ObjectiveThreshold { + public static val NO_THRESHOLD = new hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization.ObjectiveThreshold { + override isHard() { + false + } + + override satisfiesThreshold(double cost, Comparator comparator) { + true + } + } + + private new() { + } + + def boolean isHard() { + true + } + + def boolean satisfiesThreshold(double cost, Comparator comparator) + + @Data + static class Exclusive extends ObjectiveThreshold { + val double threshold + + override satisfiesThreshold(double cost, Comparator comparator) { + comparator.compare(threshold, cost) > 0 + } + } + + @Data + static class Inclusive extends ObjectiveThreshold { + val double threshold + + override satisfiesThreshold(double cost, Comparator comparator) { + comparator.compare(threshold, cost) >= 0 + } + } +} + +abstract class AbstractThreeValuedObjective implements IThreeValuedObjective { + @Accessors val String name + @Accessors ObjectiveKind kind + @Accessors ObjectiveThreshold threshold + @Accessors int level + + protected new(String name, ObjectiveKind kind, ObjectiveThreshold threshold, int level) { + this.name = name + this.kind = kind + this.threshold = threshold + this.level = level + } + + abstract def double getLowestPossibleFitness(ThreadContext threadContext) + + abstract def double getHighestPossibleFitness(ThreadContext threadContext) + + override getWorstPossibleFitness(ThreadContext threadContext) { + switch (kind) { + case LOWER_IS_BETTER: + getHighestPossibleFitness(threadContext) + case HIGHER_IS_BETTER: + getLowestPossibleFitness(threadContext) + default: + throw new IllegalStateException("Unknown three valued objective kind: " + kind) + } + } + + override getBestPossibleFitness(ThreadContext threadContext) { + switch (kind) { + case LOWER_IS_BETTER: + getLowestPossibleFitness(threadContext) + case HIGHER_IS_BETTER: + getHighestPossibleFitness(threadContext) + default: + throw new IllegalStateException("Unknown three valued objective kind: " + kind) + } + } + + override isHardObjective() { + threshold.hard + } + + override satisifiesHardObjective(Double fitness) { + threshold.satisfiesThreshold(fitness, comparator) + } + + override getComparator() { + kind.comparator + } + + override setComparator(Comparator comparator) { + kind = ObjectiveKind.fromComparator(comparator) + } + +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IThreeValuedObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IThreeValuedObjective.xtend new file mode 100644 index 00000000..4a870a3e --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/IThreeValuedObjective.xtend @@ -0,0 +1,10 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization + +import org.eclipse.viatra.dse.base.ThreadContext +import org.eclipse.viatra.dse.objectives.IObjective + +interface IThreeValuedObjective extends IObjective { + def Double getWorstPossibleFitness(ThreadContext threadContext) + + def Double getBestPossibleFitness(ThreadContext threadContext) +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ObjectiveKind.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ObjectiveKind.java new file mode 100644 index 00000000..f65428fe --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ObjectiveKind.java @@ -0,0 +1,36 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization; + +import java.util.Comparator; + +import org.eclipse.viatra.dse.objectives.Comparators; + +public enum ObjectiveKind { + LOWER_IS_BETTER { + + @Override + public Comparator getComparator() { + return Comparators.LOWER_IS_BETTER; + } + + }, + HIGHER_IS_BETTER { + + @Override + public Comparator getComparator() { + return Comparators.HIGHER_IS_BETTER; + } + + }; + + public abstract Comparator getComparator(); + + public static ObjectiveKind fromComparator(Comparator comparator) { + if (Comparators.LOWER_IS_BETTER.equals(comparator)) { + return ObjectiveKind.LOWER_IS_BETTER; + } else if (Comparators.HIGHER_IS_BETTER.equals(comparator)) { + return ObjectiveKind.HIGHER_IS_BETTER; + } else { + throw new IllegalStateException("Only LOWER_IS_BETTER and HIGHER_IS_BETTER comparators are supported."); + } + } +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend new file mode 100644 index 00000000..362ef4a3 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/optimization/ThreeValuedCostObjective.xtend @@ -0,0 +1,86 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.optimization + +import com.google.common.collect.ImmutableList +import java.util.Collection +import org.eclipse.viatra.dse.base.ThreadContext +import org.eclipse.viatra.query.runtime.api.IPatternMatch +import org.eclipse.viatra.query.runtime.api.IQuerySpecification +import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher +import org.eclipse.xtend.lib.annotations.Data + +@Data +class ThreeValuedCostElement { + val IQuerySpecification> currentMatchQuery + val IQuerySpecification> mayMatchQuery + val IQuerySpecification> mustMatchQuery + val int weight +} + +class ThreeValuedCostObjective extends AbstractThreeValuedObjective { + val Collection costElements + Collection matchers + + new(String name, Collection costElements, ObjectiveKind kind, ObjectiveThreshold threshold, + int level) { + super(name, kind, threshold, level) + this.costElements = costElements + } + + override createNew() { + new ThreeValuedCostObjective(name, costElements, kind, threshold, level) + } + + override init(ThreadContext context) { + val queryEngine = context.queryEngine + matchers = ImmutableList.copyOf(costElements.map [ element | + new CostElementMatchers( + queryEngine.getMatcher(element.currentMatchQuery), + queryEngine.getMatcher(element.mayMatchQuery), + queryEngine.getMatcher(element.mustMatchQuery), + element.weight + ) + ]) + } + + override getFitness(ThreadContext context) { + var int cost = 0 + for (matcher : matchers) { + cost += matcher.weight * matcher.currentMatcher.countMatches + } + cost as double + } + + override getLowestPossibleFitness(ThreadContext threadContext) { + var int cost = 0 + for (matcher : matchers) { + if (matcher.weight >= 0) { + cost += matcher.weight * matcher.mustMatcher.countMatches + } else if (matcher.mayMatcher.countMatches > 0) { + // TODO Count may matches. + return Double.NEGATIVE_INFINITY + } + } + cost as double + } + + override getHighestPossibleFitness(ThreadContext threadContext) { + var int cost = 0 + for (matcher : matchers) { + if (matcher.weight <= 0) { + cost += matcher.weight * matcher.mustMatcher.countMatches + } else if (matcher.mayMatcher.countMatches > 0) { + // TODO Count may matches. + return Double.POSITIVE_INFINITY + } + } + cost as double + } + + @Data + private static class CostElementMatchers { + val ViatraQueryMatcher currentMatcher + val ViatraQueryMatcher mayMatcher + val ViatraQueryMatcher mustMatcher + val int weight + } +} -- cgit v1.2.3-54-g00ecf