Measurements WIP

8 files changed, 162 insertions, 22 deletions

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 1abde0a8..aa02cd30 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
@@ -12,12 +12,15 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory

 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult

 import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.ModelGenerationMethodProvider

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.ScopePropagatorStrategy

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.PartialInterpretationInitialiser

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialinterpretationPackage

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.AbstractNeighbourhoodBasedStateCoderFactory

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.IdentifierBasedStateCoderFactory

+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedHashStateCoderFactory

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.PairwiseNeighbourhoodBasedStateCoderFactory

+import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BasicScopeGlobalConstraint

 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.BestFirstStrategyForModelGeneration

 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.DiversityChecker

 import hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse.InconsistentScopeGlobalConstraint

@@ -39,7 +42,6 @@ import org.eclipse.viatra.dse.api.DesignSpaceExplorer
 import org.eclipse.viatra.dse.api.DesignSpaceExplorer.DseLoggingLevel

 import org.eclipse.viatra.dse.solutionstore.SolutionStore

 import org.eclipse.viatra.dse.statecode.IStateCoderFactory

-import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.statecoder.NeighbourhoodBasedStateCoderFactory

 

 class ViatraReasoner extends LogicReasoner {

         val PartialInterpretationInitialiser initialiser = new PartialInterpretationInitialiser()

@@ -71,6 +73,11 @@ class ViatraReasoner extends LogicReasoner {
                         workspace.writeModel(emptySolution, "init.partialmodel")

                 }

                 emptySolution.problemConainer = problem

+                var BasicScopeGlobalConstraint basicScopeGlobalConstraint = null

+                if (viatraConfig.scopePropagatorStrategy == ScopePropagatorStrategy.None) {

+                        basicScopeGlobalConstraint = new BasicScopeGlobalConstraint(emptySolution)

+                        emptySolution.scopes.clear

+                }

 

                 val method = modelGenerationMethodProvider.createModelGenerationMethod(

                         problem,

@@ -79,11 +86,12 @@ class ViatraReasoner extends LogicReasoner {
                         viatraConfig.nameNewElements,

                         viatraConfig.typeInferenceMethod,

                         viatraConfig.scopePropagatorStrategy,

+                        viatraConfig.hints,

                         viatraConfig.documentationLevel

                 )

 

                 dse.addObjective(new ModelGenerationCompositeObjective(

-                        new ScopeObjective,

+                        basicScopeGlobalConstraint ?: new ScopeObjective,

                         method.unfinishedMultiplicities.map[new UnfinishedMultiplicityObjective(it)],

                         wf2ObjectiveConverter.createCompletenessObjective(method.unfinishedWF)

                 ))

@@ -132,6 +140,9 @@ class ViatraReasoner extends LogicReasoner {
                 dse.addGlobalConstraint(wf2ObjectiveConverter.createInvalidationGlobalConstraint(method.invalidWF))

                 dse.addGlobalConstraint(new SurelyViolatedObjectiveGlobalConstraint(solutionSaver))

                 dse.addGlobalConstraint(new InconsistentScopeGlobalConstraint)

+                if (basicScopeGlobalConstraint !== null) {

+                        dse.addGlobalConstraint(basicScopeGlobalConstraint)

+                }

                 for (additionalConstraint : viatraConfig.searchSpaceConstraints.additionalGlobalConstraints) {

                         dse.addGlobalConstraint(additionalConstraint.apply(method))

                 }

@@ -140,7 +151,7 @@ class ViatraReasoner extends LogicReasoner {
 

                 val IStateCoderFactory statecoder = switch (viatraConfig.stateCoderStrategy) {

                         case Neighbourhood:

-                                new NeighbourhoodBasedStateCoderFactory

+                                new NeighbourhoodBasedHashStateCoderFactory

                         case PairwiseNeighbourhood:

                                 new PairwiseNeighbourhoodBasedStateCoderFactory

                         default:

@@ -216,9 +227,17 @@ class ViatraReasoner extends LogicReasoner {
                                 it.value = method.statistics.decisionsTried

                         ]

                         it.entries += createIntStatisticEntry => [

+                                it.name = "Transformations"

+                                it.value = method.statistics.transformationInvocations

+                        ]

+                        it.entries += createIntStatisticEntry => [

                                 it.name = "ScopePropagations"

                                 it.value = method.statistics.scopePropagatorInvocations

                         ]

+                        it.entries += createIntStatisticEntry => [

+                                it.name = "ScopePropagationsSolverCalls"

+                                it.value = method.statistics.scopePropagatorSolverInvocations

+                        ]

                         if (diversityChecker.isActive) {

                                 it.entries += createIntStatisticEntry => [

                                         it.name = "SolutionDiversityCheckTime"

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 a5f42a5f..6f38d261 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
@@ -16,6 +16,7 @@ import java.util.LinkedList
 import java.util.List

 import java.util.Set

 import org.eclipse.xtext.xbase.lib.Functions.Function1

+import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality.LinearTypeConstraintHint

 

 enum StateCoderStrategy {

         Neighbourhood,

@@ -56,6 +57,8 @@ class ViatraReasonerConfiguration extends LogicSolverConfiguration {
 

         public var ScopePropagatorStrategy scopePropagatorStrategy = new ScopePropagatorStrategy.Polyhedral(

                 PolyhedralScopePropagatorConstraints.Relational, PolyhedralScopePropagatorSolver.Clp)

+        

+        public var List<LinearTypeConstraintHint> hints = newArrayList

 

         public var List<CostObjectiveConfiguration> costObjectives = newArrayList

 }

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BasicScopeGlobalConstraint.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BasicScopeGlobalConstraint.xtend
new file mode 100644
index 00000000..67f447ed
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BasicScopeGlobalConstraint.xtend
@@ -0,0 +1,103 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner.dse
+
+import com.google.common.collect.ImmutableList
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation
+import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation
+import java.util.Comparator
+import java.util.List
+import org.eclipse.viatra.dse.base.ThreadContext
+import org.eclipse.viatra.dse.objectives.Comparators
+import org.eclipse.viatra.dse.objectives.IGlobalConstraint
+import org.eclipse.viatra.dse.objectives.IObjective
+import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
+
+class BasicScopeGlobalConstraint implements IGlobalConstraint, IObjective {
+        val PartialInterpretation p
+        val List<ScopeAssertion> assertions
+
+        new(PartialInterpretation p) {
+                this.p = p
+                assertions = ImmutableList.copyOf(p.scopes.map [
+                        val currentSize = targetTypeInterpretation.elements.size
+                        val minElements = minNewElements + currentSize
+                        val maxElements = if (maxNewElements < 0) {
+                                -1
+                        } else {
+                                maxNewElements + currentSize
+                        }
+                        new ScopeAssertion(minElements, maxElements, targetTypeInterpretation)
+                ])
+        }
+
+        override init(ThreadContext context) {
+                if (context.model != p) {
+                        throw new IllegalArgumentException(
+                                "Partial model must be passed to the constructor of BasicScopeGlobalConstraint")
+                }
+        }
+
+        override checkGlobalConstraint(ThreadContext context) {
+                assertions.forall[upperBoundSatisfied]
+        }
+
+        override getFitness(ThreadContext context) {
+                var double fitness = p.minNewElements
+                for (assertion : assertions) {
+                        if (!assertion.lowerBoundSatisfied) {
+                                fitness += 1
+                        }
+                }
+                fitness
+        }
+
+        override satisifiesHardObjective(Double fitness) {
+                fitness <= 0.01
+        }
+
+        override BasicScopeGlobalConstraint createNew() {
+                this
+        }
+
+        override getName() {
+                class.name
+        }
+
+        override getComparator() {
+                Comparators.LOWER_IS_BETTER
+        }
+
+        override getLevel() {
+                2
+        }
+
+        override isHardObjective() {
+                true
+        }
+
+        override setComparator(Comparator<Double> comparator) {
+                throw new UnsupportedOperationException
+        }
+
+        override setLevel(int level) {
+                throw new UnsupportedOperationException
+        }
+
+        @FinalFieldsConstructor
+        private static class ScopeAssertion {
+                val int lowerBound
+                val int upperBound
+                val PartialTypeInterpratation typeDefinitions
+
+                private def getCount() {
+                        typeDefinitions.elements.size
+                }
+
+                private def isLowerBoundSatisfied() {
+                        count >= lowerBound
+                }
+
+                private def isUpperBoundSatisfied() {
+                        upperBound < 0 || count <= upperBound
+                }
+        }
+}
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
index 5af7fc69..081e48fa 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java
@@ -255,7 +255,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy {
                         activationIds = new ArrayList<Object>(context.getUntraversedActivationIds());

                         Collections.shuffle(activationIds);

                 } catch (NullPointerException e) {

-                        logger.warn("Unexpected state code: " + context.getDesignSpaceManager().getCurrentState());

+//                      logger.warn("Unexpected state code: " + context.getDesignSpaceManager().getCurrentState());

                         numberOfStatecoderFail++;

                         activationIds = Collections.emptyList();

                 }

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 9a33753c..2976bebe 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
@@ -59,7 +59,7 @@ class ModelGenerationCompositeObjective implements IThreeValuedObjective {
                 }

                 sum += multiplicity

                 sum += unfinishedWFsFitness // *0.5

-                // println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''')

+//              println('''Sum=«sum»|Scope=«scopeFitnes»|Multiplicity=«multiplicity»|WFs=«unfinishedWFsFitness»''')

                 return sum

         }

         

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend
index 69efe0d7..e7967b00 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ScopeObjective.xtend
@@ -23,9 +23,9 @@ class ScopeObjective implements IObjective{
         

         override getFitness(ThreadContext context) {

                 val interpretation = context.model as PartialInterpretation

-                var res = interpretation.minNewElements.doubleValue

+                var res = interpretation.minNewElementsHeuristic.doubleValue

                 for(scope : interpretation.scopes) {

-                        res += scope.minNewElements*2

+                        res += scope.minNewElementsHeuristic*2

                 }

                 return res

         }

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend
index bf34aeeb..1b61ffa5 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/UnfinishedWFObjective.xtend
@@ -14,41 +14,51 @@ import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
 class UnfinishedWFObjective implements IObjective {

         Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFs

         val List<ViatraQueryMatcher<?>> matchers

-        

-        new(Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFs) {

+

+        new(

+                Collection<? extends IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> unfinishedWFs) {

                 this.unfinishedWFs = unfinishedWFs

                 matchers = new ArrayList(unfinishedWFs.size)

         }

+

         override getName() '''unfinishedWFs'''

+

         override createNew() {

                 return new UnfinishedWFObjective(unfinishedWFs)

         }

+

         override init(ThreadContext context) {

-                val engine = context.queryEngine//ViatraQueryEngine.on(new EMFScope(context.model))

-                for(unfinishedWF : unfinishedWFs) {

+                val engine = context.queryEngine // ViatraQueryEngine.on(new EMFScope(context.model))

+                for (unfinishedWF : unfinishedWFs) {

                         matchers += unfinishedWF.getMatcher(engine)

                 }

         }

-        

+

         override getComparator() { Comparators.LOWER_IS_BETTER }

+

         override getFitness(ThreadContext context) {

                 var sumOfMatches = 0

-                for(matcher : matchers) {

+                for (matcher : matchers) {

                         val number = matcher.countMatches

-                        //println('''«matcher.patternName» = «number»''')

-                        sumOfMatches+=number

+//                      if (number > 0) {

+//                              println('''«matcher.patternName» = «number»''')

+//                      }

+                        sumOfMatches += number

                 }

                 return sumOfMatches.doubleValue

         }

-        

+

         override getLevel() { 2 }

+

         override isHardObjective() { true }

-        override satisifiesHardObjective(Double fitness) { return fitness <=0.01 }

-        

+

+        override satisifiesHardObjective(Double fitness) { return fitness <= 0.01 }

+

         override setComparator(Comparator<Double> comparator) {

                 throw new UnsupportedOperationException()

         }

+

         override setLevel(int level) {

                 throw new UnsupportedOperationException()

         }

-}
\ No newline at end of file
+}

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend
index 6bffeb59..74500cc2 100644
--- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/ViatraReasonerSolutionSaver.xtend
@@ -42,7 +42,7 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver {
 
         private def saveBestSolutionOnly(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) {
                 val fitness = context.lastFitness
-                if (!fitness.satisifiesHardObjectives) {
+                if (!shouldSaveSolution(fitness, context)) {
                         return false
                 }
                 val dominatedTrajectories = newArrayList
@@ -83,7 +83,7 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver {
 
         private def saveAnyDiverseSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory) {
                 val fitness = context.lastFitness
-                if (!fitness.satisifiesHardObjectives) {
+                if (!shouldSaveSolution(fitness, context)) {
                         return false
                 }
                 if (!diversityChecker.newSolution(context, id, emptyList)) {
@@ -92,7 +92,12 @@ class ViatraReasonerSolutionSaver implements ISolutionSaver {
                 basicSaveSolution(context, id, solutionTrajectory, fitness)
         }
 
-        private def basicSaveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory, Fitness fitness) {
+        private def shouldSaveSolution(Fitness fitness, ThreadContext context) {
+                return fitness.satisifiesHardObjectives
+        }
+
+        private def basicSaveSolution(ThreadContext context, Object id, SolutionTrajectory solutionTrajectory,
+                Fitness fitness) {
                 var boolean solutionSaved = false
                 var dseSolution = solutionsCollection.get(id)
                 if (dseSolution === null) {